Merge pull request #10668 from ethereum/fuzzer-always-add-smt-pragma

ossfuzz: Add option to force SMT pragma and set it in solc fuzzers
This commit is contained in:
Bhargava Shastry 2020-12-21 12:38:44 +01:00 committed by GitHub
commit beed9de7d5
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 40 additions and 6 deletions

View File

@ -72,7 +72,16 @@ void FuzzerUtil::testCompilerJsonInterface(string const& _input, bool _optimize,
runCompiler(jsonCompactPrint(config), _quiet); runCompiler(jsonCompactPrint(config), _quiet);
} }
void FuzzerUtil::testCompiler(StringMap const& _input, bool _optimize, unsigned _rand) void FuzzerUtil::forceSMT(StringMap& _input)
{
// Add SMT checker pragma if not already present in source
static const char* smtPragma = "pragma experimental SMTChecker;";
for (auto &sourceUnit: _input)
if (sourceUnit.second.find(smtPragma) == string::npos)
sourceUnit.second += smtPragma;
}
void FuzzerUtil::testCompiler(StringMap& _input, bool _optimize, unsigned _rand, bool _forceSMT)
{ {
frontend::CompilerStack compiler; frontend::CompilerStack compiler;
EVMVersion evmVersion = s_evmVersions[_rand % s_evmVersions.size()]; EVMVersion evmVersion = s_evmVersions[_rand % s_evmVersions.size()];
@ -81,6 +90,11 @@ void FuzzerUtil::testCompiler(StringMap const& _input, bool _optimize, unsigned
optimiserSettings = frontend::OptimiserSettings::standard(); optimiserSettings = frontend::OptimiserSettings::standard();
else else
optimiserSettings = frontend::OptimiserSettings::minimal(); optimiserSettings = frontend::OptimiserSettings::minimal();
if (_forceSMT)
{
forceSMT(_input);
compiler.setModelCheckerSettings({frontend::ModelCheckerEngine::All(), /*timeout=*/1});
}
compiler.setSources(_input); compiler.setSources(_input);
compiler.setEVMVersion(evmVersion); compiler.setEVMVersion(evmVersion);
compiler.setOptimiserSettings(optimiserSettings); compiler.setOptimiserSettings(optimiserSettings);

View File

@ -33,7 +33,17 @@ struct FuzzerUtil
static void testStandardCompiler(std::string const& _input, bool _quiet); static void testStandardCompiler(std::string const& _input, bool _quiet);
/// Compiles @param _input which is a map of input file name to source code /// Compiles @param _input which is a map of input file name to source code
/// string with optimisation turned on if @param _optimize is true /// string with optimisation turned on if @param _optimize is true
/// (off otherwise) and a pseudo-random @param _rand that selects the EVM /// (off otherwise), a pseudo-random @param _rand that selects the EVM
/// version to be compiled for. /// version to be compiled for, and bool @param _forceSMT that, if true,
static void testCompiler(solidity::StringMap const& _input, bool _optimize, unsigned _rand); /// adds the experimental SMTChecker pragma to each source file in the
/// source map.
static void testCompiler(
solidity::StringMap& _input,
bool _optimize,
unsigned _rand,
bool _forceSMT
);
/// Adds the experimental SMTChecker pragma to each source file in the
/// source map.
static void forceSMT(solidity::StringMap& _input);
}; };

View File

@ -43,7 +43,12 @@ extern "C" int LLVMFuzzerTestOneInput(uint8_t const* _data, size_t _size)
{ {
return 0; return 0;
} }
FuzzerUtil::testCompiler(sourceCode, /*optimize=*/false, /*_rand=*/static_cast<unsigned>(_size)); FuzzerUtil::testCompiler(
sourceCode,
/*optimize=*/false,
/*_rand=*/static_cast<unsigned>(_size),
/*forceSMT=*/true
);
} }
return 0; return 0;
} }

View File

@ -43,7 +43,12 @@ extern "C" int LLVMFuzzerTestOneInput(uint8_t const* _data, size_t _size)
{ {
return 0; return 0;
} }
FuzzerUtil::testCompiler(sourceCode, /*optimize=*/true, /*rand=*/static_cast<unsigned>(_size)); FuzzerUtil::testCompiler(
sourceCode,
/*optimize=*/true,
/*rand=*/static_cast<unsigned>(_size),
/*forceSMT=*/true
);
} }
return 0; return 0;
} }