diff --git a/Changelog.md b/Changelog.md index 407bd342e..df3848d1f 100644 --- a/Changelog.md +++ b/Changelog.md @@ -12,6 +12,8 @@ Compiler Features: * SMTChecker: Support inline arrays. * SMTChecker: Support variables ``block``, ``msg`` and ``tx`` in the CHC engine. * Control Flow Graph: Print warning for non-empty functions with unnamed return parameters that are not assigned a value in all code paths. + * Command Line Interface: New option ``model-checker-engine`` allows to choose a specific SMTChecker engine. Options are ``all`` (default), ``bmc``, ``chc`` and ``none``. + * Standard JSON: New option ``settings.modelCheckerEngine`` allows to choose a specific SMTChecker engine. Options are ``all`` (default), ``bmc``, ``chc`` and ``none``. Bugfixes: diff --git a/docs/using-the-compiler.rst b/docs/using-the-compiler.rst index f8d9c133c..568d20f2c 100644 --- a/docs/using-the-compiler.rst +++ b/docs/using-the-compiler.rst @@ -341,7 +341,9 @@ Input Description "def": { "MyContract": [ "abi", "evm.bytecode.opcodes" ] } - } + }, + // Choose which model checker engine to use: all (default), bmc, chc, none. + "modelCheckerEngine": "chc" } } diff --git a/liblangutil/SourceReferenceFormatterHuman.cpp b/liblangutil/SourceReferenceFormatterHuman.cpp index e90cadec2..282f0a0c9 100644 --- a/liblangutil/SourceReferenceFormatterHuman.cpp +++ b/liblangutil/SourceReferenceFormatterHuman.cpp @@ -165,7 +165,7 @@ void SourceReferenceFormatterHuman::printExceptionInformation(SourceReferenceExt for (auto const& secondary: _msg.secondary) { secondaryColored() << "Note"; - messageColored() << ": " << secondary.message << '\n'; + messageColored() << ":" << (secondary.message.empty() ? "" : (" " + secondary.message)) << '\n'; printSourceLocation(secondary); } diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index b319bfd42..8b4d460e2 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -836,7 +836,7 @@ void BMC::checkCondition( "\nNote that some information is erased after the execution of loops.\n" "You can re-introduce information using require()."; if (m_externalFunctionCallHappened) - extraComment+= + extraComment += "\nNote that external function calls are not inlined," " even if the source code of the function is available." " This is due to the possibility that the actual called contract" @@ -854,7 +854,7 @@ void BMC::checkCondition( if (_callStack.size()) { std::ostringstream modelMessage; - modelMessage << "\nCounterexample:\n"; + modelMessage << "Counterexample:\n"; solAssert(values.size() == expressionNames.size(), ""); map sortedModel; for (size_t i = 0; i < values.size(); ++i) @@ -863,6 +863,7 @@ void BMC::checkCondition( for (auto const& eval: sortedModel) modelMessage << " " << eval.first << " = " << eval.second << "\n"; + m_errorReporter.warning( _errorHappens, _location, diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 2356a2b14..e24d5a6e7 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -1298,7 +1298,7 @@ void CHC::checkAndReportTarget( _errorReporterId, _scope->location(), "CHC: " + _satMsg, - SecondarySourceLocation().append("\nCounterexample:\n" + *cex, SourceLocation{}) + SecondarySourceLocation().append("Counterexample:\n" + *cex, SourceLocation{}) ); else m_outerErrorReporter.warning( @@ -1402,9 +1402,13 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& } } else + { + auto modelMsg = formatVariableModel(*stateVars, stateValues, ", "); /// We report the state after every tx in the trace except for the last, which is reported /// first in the code above. - path.emplace_back("State: " + formatVariableModel(*stateVars, stateValues, ", ")); + if (!modelMsg.empty()) + path.emplace_back("State: " + modelMsg); + } string txCex = summaryPredicate->formatSummaryCall(summaryArgs); path.emplace_back(txCex); diff --git a/libsolidity/formal/ModelChecker.cpp b/libsolidity/formal/ModelChecker.cpp index 9465dd342..40317e2ca 100644 --- a/libsolidity/formal/ModelChecker.cpp +++ b/libsolidity/formal/ModelChecker.cpp @@ -27,9 +27,11 @@ using namespace solidity::frontend; ModelChecker::ModelChecker( ErrorReporter& _errorReporter, map const& _smtlib2Responses, + ModelCheckerEngine _engine, ReadCallback::Callback const& _smtCallback, smtutil::SMTSolverChoice _enabledSolvers ): + m_engine(_engine), m_context(), m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers), m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers) @@ -41,13 +43,15 @@ void ModelChecker::analyze(SourceUnit const& _source) if (!_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker)) return; - m_chc.analyze(_source); + if (m_engine.chc) + m_chc.analyze(_source); auto solvedTargets = m_chc.safeTargets(); for (auto const& target: m_chc.unsafeTargets()) solvedTargets[target.first] += target.second; - m_bmc.analyze(_source, solvedTargets); + if (m_engine.bmc) + m_bmc.analyze(_source, solvedTargets); } vector ModelChecker::unhandledQueries() diff --git a/libsolidity/formal/ModelChecker.h b/libsolidity/formal/ModelChecker.h index 42d116b28..658bfb6da 100644 --- a/libsolidity/formal/ModelChecker.h +++ b/libsolidity/formal/ModelChecker.h @@ -32,6 +32,8 @@ #include #include +#include + namespace solidity::langutil { class ErrorReporter; @@ -41,6 +43,34 @@ struct SourceLocation; namespace solidity::frontend { +struct ModelCheckerEngine +{ + bool bmc = false; + bool chc = false; + + static constexpr ModelCheckerEngine All() { return {true, true}; } + static constexpr ModelCheckerEngine BMC() { return {true, false}; } + static constexpr ModelCheckerEngine CHC() { return {false, true}; } + static constexpr ModelCheckerEngine None() { return {false, false}; } + + bool none() const { return !any(); } + bool any() const { return bmc || chc; } + bool all() const { return bmc && chc; } + + static std::optional fromString(std::string const& _engine) + { + static std::map engineMap{ + {"all", All()}, + {"bmc", BMC()}, + {"chc", CHC()}, + {"none", None()} + }; + if (engineMap.count(_engine)) + return engineMap.at(_engine); + return {}; + } +}; + class ModelChecker { public: @@ -49,6 +79,7 @@ public: ModelChecker( langutil::ErrorReporter& _errorReporter, std::map const& _smtlib2Responses, + ModelCheckerEngine _engine = ModelCheckerEngine::All(), ReadCallback::Callback const& _smtCallback = ReadCallback::Callback(), smtutil::SMTSolverChoice _enabledSolvers = smtutil::SMTSolverChoice::All() ); @@ -64,6 +95,8 @@ public: static smtutil::SMTSolverChoice availableSolvers(); private: + ModelCheckerEngine m_engine; + /// Stores the context of the encoding. smt::EncodingContext m_context; diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index c9f9d6fbd..d5cdaa4a4 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -2132,7 +2132,7 @@ SecondarySourceLocation SMTEncoder::callStackMessage(vector cons { SecondarySourceLocation callStackLocation; solAssert(!_callStack.empty(), ""); - callStackLocation.append("Callstack: ", SourceLocation()); + callStackLocation.append("Callstack:", SourceLocation()); for (auto const& call: _callStack | boost::adaptors::reversed) if (call.second) callStackLocation.append("", call.second->location()); diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp index 0c1b6b49d..e57d7c823 100644 --- a/libsolidity/interface/CompilerStack.cpp +++ b/libsolidity/interface/CompilerStack.cpp @@ -87,6 +87,7 @@ static int g_compilerStackCounts = 0; CompilerStack::CompilerStack(ReadCallback::Callback _readFile): m_readFile{std::move(_readFile)}, + m_modelCheckerEngine{ModelCheckerEngine::All()}, m_enabledSMTSolvers{smtutil::SMTSolverChoice::All()}, m_errorReporter{m_errorList} { @@ -138,6 +139,13 @@ void CompilerStack::setEVMVersion(langutil::EVMVersion _version) m_evmVersion = _version; } +void CompilerStack::setModelCheckerEngine(ModelCheckerEngine _engine) +{ + if (m_stackState >= ParsedAndImported) + BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set enabled model checking engines before parsing.")); + m_modelCheckerEngine = _engine; +} + void CompilerStack::setSMTSolverChoice(smtutil::SMTSolverChoice _enabledSMTSolvers) { if (m_stackState >= ParsedAndImported) @@ -207,6 +215,7 @@ void CompilerStack::reset(bool _keepSettings) m_remappings.clear(); m_libraries.clear(); m_evmVersion = langutil::EVMVersion(); + m_modelCheckerEngine = ModelCheckerEngine::All(); m_enabledSMTSolvers = smtutil::SMTSolverChoice::All(); m_generateIR = false; m_generateEwasm = false; @@ -443,7 +452,7 @@ bool CompilerStack::analyze() if (noErrors) { - ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_readFile, m_enabledSMTSolvers); + ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses, m_modelCheckerEngine, m_readFile, m_enabledSMTSolvers); for (Source const* source: m_sourceOrder) if (source->ast) modelChecker.analyze(*source->ast); diff --git a/libsolidity/interface/CompilerStack.h b/libsolidity/interface/CompilerStack.h index c7f4e4494..fd82c8feb 100644 --- a/libsolidity/interface/CompilerStack.h +++ b/libsolidity/interface/CompilerStack.h @@ -29,6 +29,8 @@ #include #include +#include + #include #include @@ -165,6 +167,8 @@ public: /// Must be set before parsing. void setEVMVersion(langutil::EVMVersion _version = langutil::EVMVersion{}); + /// Set which model checking engines should be used. + void setModelCheckerEngine(ModelCheckerEngine _engine); /// Set which SMT solvers should be enabled. void setSMTSolverChoice(smtutil::SMTSolverChoice _enabledSolvers); @@ -452,6 +456,7 @@ private: RevertStrings m_revertStrings = RevertStrings::Default; State m_stopAfter = State::CompilationSuccessful; langutil::EVMVersion m_evmVersion; + ModelCheckerEngine m_modelCheckerEngine; smtutil::SMTSolverChoice m_enabledSMTSolvers; std::map> m_requestedContractNames; bool m_generateEvmBytecode = true; diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp index 419e7d568..bb58abf9b 100644 --- a/libsolidity/interface/StandardCompiler.cpp +++ b/libsolidity/interface/StandardCompiler.cpp @@ -414,7 +414,7 @@ std::optional checkAuxiliaryInputKeys(Json::Value const& _input) std::optional checkSettingsKeys(Json::Value const& _input) { - static set keys{"parserErrorRecovery", "debug", "evmVersion", "libraries", "metadata", "optimizer", "outputSelection", "remappings", "stopAfter"}; + static set keys{"parserErrorRecovery", "debug", "evmVersion", "libraries", "metadata", "optimizer", "outputSelection", "remappings", "stopAfter", "modelCheckerEngine"}; return checkKeys(_input, keys, "settings"); } @@ -527,6 +527,7 @@ std::optional checkOutputSelection(Json::Value const& _outputSelect return std::nullopt; } + /// Validates the optimizer settings and returns them in a parsed object. /// On error returns the json-formatted error message. std::variant parseOptimizerSettings(Json::Value const& _jsonInput) @@ -866,6 +867,16 @@ std::variant StandardCompiler: "Requested output selection conflicts with \"settings.stopAfter\"." ); + if (settings.isMember("modelCheckerEngine")) + { + if (!settings["modelCheckerEngine"].isString()) + return formatFatalError("JSONError", "modelCheckerEngine must be a string."); + std::optional engine = ModelCheckerEngine::fromString(settings["modelCheckerEngine"].asString()); + if (!engine) + return formatFatalError("JSONError", "Invalid model checker engine requested."); + ret.modelCheckerEngine = *engine; + } + return { std::move(ret) }; } @@ -886,6 +897,7 @@ Json::Value StandardCompiler::compileSolidity(StandardCompiler::InputsAndSetting compilerStack.useMetadataLiteralSources(_inputsAndSettings.metadataLiteralSources); compilerStack.setMetadataHash(_inputsAndSettings.metadataHash); compilerStack.setRequestedContractNames(requestedContractNames(_inputsAndSettings.outputSelection)); + compilerStack.setModelCheckerEngine(_inputsAndSettings.modelCheckerEngine); compilerStack.enableEvmBytecodeGeneration(isEvmBytecodeRequested(_inputsAndSettings.outputSelection)); compilerStack.enableIRGeneration(isIRRequested(_inputsAndSettings.outputSelection)); diff --git a/libsolidity/interface/StandardCompiler.h b/libsolidity/interface/StandardCompiler.h index ccfe92827..d517b2eec 100644 --- a/libsolidity/interface/StandardCompiler.h +++ b/libsolidity/interface/StandardCompiler.h @@ -71,6 +71,7 @@ private: bool metadataLiteralSources = false; CompilerStack::MetadataHash metadataHash = CompilerStack::MetadataHash::IPFS; Json::Value outputSelection; + ModelCheckerEngine modelCheckerEngine = ModelCheckerEngine::All(); }; /// Parses the input json (and potentially invokes the read callback) and either returns diff --git a/solc/CommandLineInterface.cpp b/solc/CommandLineInterface.cpp index 2d0c6c33f..3ba999e09 100644 --- a/solc/CommandLineInterface.cpp +++ b/solc/CommandLineInterface.cpp @@ -146,6 +146,7 @@ static string const g_strMachine = "machine"; static string const g_strMetadata = "metadata"; static string const g_strMetadataHash = "metadata-hash"; static string const g_strMetadataLiteral = "metadata-literal"; +static string const g_strModelCheckerEngine = "model-checker-engine"; static string const g_strNatspecDev = "devdoc"; static string const g_strNatspecUser = "userdoc"; static string const g_strNone = "none"; @@ -215,6 +216,7 @@ static string const g_argMachine = g_strMachine; static string const g_argMetadata = g_strMetadata; static string const g_argMetadataHash = g_strMetadataHash; static string const g_argMetadataLiteral = g_strMetadataLiteral; +static string const g_argModelCheckerEngine = g_strModelCheckerEngine; static string const g_argNatspecDev = g_strNatspecDev; static string const g_argNatspecUser = g_strNatspecUser; static string const g_argOpcodes = g_strOpcodes; @@ -993,6 +995,16 @@ General Information)").c_str(), ; desc.add(optimizerOptions); + po::options_description smtCheckerOptions("Model Checker Options"); + smtCheckerOptions.add_options() + ( + g_strModelCheckerEngine.c_str(), + po::value()->value_name("all,bmc,chc,none")->default_value("all"), + "Select model checker engine." + ) + ; + desc.add(smtCheckerOptions); + po::options_description allOptions = desc; allOptions.add_options()(g_argInputFile.c_str(), po::value>(), "input file"); @@ -1379,6 +1391,18 @@ bool CommandLineInterface::processInput() } } + if (m_args.count(g_argModelCheckerEngine)) + { + string engineStr = m_args[g_argModelCheckerEngine].as(); + optional engine = ModelCheckerEngine::fromString(engineStr); + if (!engine) + { + serr() << "Invalid option for --" << g_argModelCheckerEngine << ": " << engineStr << endl; + return false; + } + m_modelCheckerEngine = *engine; + } + m_compiler = make_unique(fileReader); unique_ptr formatter; @@ -1393,6 +1417,8 @@ bool CommandLineInterface::processInput() m_compiler->useMetadataLiteralSources(true); if (m_args.count(g_argMetadataHash)) m_compiler->setMetadataHash(m_metadataHash); + if (m_args.count(g_argModelCheckerEngine)) + m_compiler->setModelCheckerEngine(m_modelCheckerEngine); if (m_args.count(g_argInputFile)) m_compiler->setRemappings(m_remappings); diff --git a/solc/CommandLineInterface.h b/solc/CommandLineInterface.h index c8762d3de..12ed819e9 100644 --- a/solc/CommandLineInterface.h +++ b/solc/CommandLineInterface.h @@ -79,7 +79,6 @@ private: void handleABI(std::string const& _contract); void handleNatspec(bool _natspecDev, std::string const& _contract); void handleGasEstimation(std::string const& _contract); - void handleFormal(); void handleStorageLayout(std::string const& _contract); /// Fills @a m_sourceCodes initially and @a m_redirects. @@ -134,6 +133,8 @@ private: RevertStrings m_revertStrings = RevertStrings::Default; /// Chosen hash method for the bytecode metadata. CompilerStack::MetadataHash m_metadataHash = CompilerStack::MetadataHash::IPFS; + /// Chosen model checker engine. + ModelCheckerEngine m_modelCheckerEngine = ModelCheckerEngine::All(); /// Whether or not to colorize diagnostics output. bool m_coloredOutput = true; /// Whether or not to output error IDs. diff --git a/test/cmdlineTests/model_checker_engine_all/args b/test/cmdlineTests/model_checker_engine_all/args new file mode 100644 index 000000000..5aeb1490e --- /dev/null +++ b/test/cmdlineTests/model_checker_engine_all/args @@ -0,0 +1 @@ +--model-checker-engine all diff --git a/test/cmdlineTests/model_checker_engine_all/err b/test/cmdlineTests/model_checker_engine_all/err new file mode 100644 index 000000000..f3f9a6586 --- /dev/null +++ b/test/cmdlineTests/model_checker_engine_all/err @@ -0,0 +1,13 @@ +Warning: CHC: Assertion violation happens here. + --> model_checker_engine_all/input.sol:6:3: + | +6 | assert(x > 0); + | ^^^^^^^^^^^^^ +Note: Counterexample: + +x = 0 + + +Transaction trace: +constructor() +f(0) diff --git a/test/cmdlineTests/model_checker_engine_all/input.sol b/test/cmdlineTests/model_checker_engine_all/input.sol new file mode 100644 index 000000000..166416c06 --- /dev/null +++ b/test/cmdlineTests/model_checker_engine_all/input.sol @@ -0,0 +1,8 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +pragma experimental SMTChecker; +contract test { + function f(uint x) public pure { + assert(x > 0); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_engine_bmc/args b/test/cmdlineTests/model_checker_engine_bmc/args new file mode 100644 index 000000000..549f20236 --- /dev/null +++ b/test/cmdlineTests/model_checker_engine_bmc/args @@ -0,0 +1 @@ +--model-checker-engine bmc diff --git a/test/cmdlineTests/model_checker_engine_bmc/err b/test/cmdlineTests/model_checker_engine_bmc/err new file mode 100644 index 000000000..82d3b6e0a --- /dev/null +++ b/test/cmdlineTests/model_checker_engine_bmc/err @@ -0,0 +1,10 @@ +Warning: BMC: Assertion violation happens here. + --> model_checker_engine_bmc/input.sol:6:3: + | +6 | assert(x > 0); + | ^^^^^^^^^^^^^ +Note: Counterexample: + x = 0 + +Note: Callstack: +Note: diff --git a/test/cmdlineTests/model_checker_engine_bmc/input.sol b/test/cmdlineTests/model_checker_engine_bmc/input.sol new file mode 100644 index 000000000..166416c06 --- /dev/null +++ b/test/cmdlineTests/model_checker_engine_bmc/input.sol @@ -0,0 +1,8 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +pragma experimental SMTChecker; +contract test { + function f(uint x) public pure { + assert(x > 0); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_engine_chc/args b/test/cmdlineTests/model_checker_engine_chc/args new file mode 100644 index 000000000..7458a47d3 --- /dev/null +++ b/test/cmdlineTests/model_checker_engine_chc/args @@ -0,0 +1 @@ +--model-checker-engine chc diff --git a/test/cmdlineTests/model_checker_engine_chc/err b/test/cmdlineTests/model_checker_engine_chc/err new file mode 100644 index 000000000..e3edf380f --- /dev/null +++ b/test/cmdlineTests/model_checker_engine_chc/err @@ -0,0 +1,13 @@ +Warning: CHC: Assertion violation happens here. + --> model_checker_engine_chc/input.sol:6:3: + | +6 | assert(x > 0); + | ^^^^^^^^^^^^^ +Note: Counterexample: + +x = 0 + + +Transaction trace: +constructor() +f(0) diff --git a/test/cmdlineTests/model_checker_engine_chc/input.sol b/test/cmdlineTests/model_checker_engine_chc/input.sol new file mode 100644 index 000000000..166416c06 --- /dev/null +++ b/test/cmdlineTests/model_checker_engine_chc/input.sol @@ -0,0 +1,8 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity >=0.0; +pragma experimental SMTChecker; +contract test { + function f(uint x) public pure { + assert(x > 0); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/model_checker_engine_none/args b/test/cmdlineTests/model_checker_engine_none/args new file mode 100644 index 000000000..cac942cb2 --- /dev/null +++ b/test/cmdlineTests/model_checker_engine_none/args @@ -0,0 +1 @@ +--model-checker-engine none diff --git a/test/cmdlineTests/model_checker_engine_none/err b/test/cmdlineTests/model_checker_engine_none/err new file mode 100644 index 000000000..5b30ff59a --- /dev/null +++ b/test/cmdlineTests/model_checker_engine_none/err @@ -0,0 +1,5 @@ +Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing "SPDX-License-Identifier: " to each source file. Use "SPDX-License-Identifier: UNLICENSED" for non-open-source code. Please see https://spdx.org for more information. +--> model_checker_engine_none/input.sol + +Warning: Source file does not specify required compiler version! +--> model_checker_engine_none/input.sol diff --git a/test/cmdlineTests/model_checker_engine_none/input.sol b/test/cmdlineTests/model_checker_engine_none/input.sol new file mode 100644 index 000000000..8727d4b40 --- /dev/null +++ b/test/cmdlineTests/model_checker_engine_none/input.sol @@ -0,0 +1,9 @@ +// Removed to yield a warning, otherwise CI test fails with the expectation +// "no output requested" +//pragma solidity >=0.0; +pragma experimental SMTChecker; +contract test { + function f(uint x) public pure { + assert(x > 0); + } +} \ No newline at end of file diff --git a/test/cmdlineTests/standard_model_checker_engine_all/input.json b/test/cmdlineTests/standard_model_checker_engine_all/input.json new file mode 100644 index 000000000..0fd433d90 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_engine_all/input.json @@ -0,0 +1,14 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract C { function f(uint x) public pure { assert(x > 0); } }" + } + }, + "settings": + { + "modelCheckerEngine": "all" + } +} diff --git a/test/cmdlineTests/standard_model_checker_engine_all/output.json b/test/cmdlineTests/standard_model_checker_engine_all/output.json new file mode 100644 index 000000000..c8e59e0d8 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_engine_all/output.json @@ -0,0 +1,19 @@ +{"errors":[{"component":"general","errorCode":"6328","formattedMessage":"A:4:47: Warning: CHC: Assertion violation happens here. +contract C { function f(uint x) public pure { assert(x > 0); } } + ^-----------^ +Counterexample: + +x = 0 + + +Transaction trace: +constructor() +f(0) +","message":"CHC: Assertion violation happens here.","secondarySourceLocations":[{"message":"Counterexample: + +x = 0 + + +Transaction trace: +constructor() +f(0)"}],"severity":"warning","sourceLocation":{"end":150,"file":"A","start":137},"type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_engine_bmc/input.json b/test/cmdlineTests/standard_model_checker_engine_bmc/input.json new file mode 100644 index 000000000..f78bfe838 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_engine_bmc/input.json @@ -0,0 +1,14 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract C { function f(uint x) public pure { assert(x > 0); } }" + } + }, + "settings": + { + "modelCheckerEngine": "bmc" + } +} diff --git a/test/cmdlineTests/standard_model_checker_engine_bmc/output.json b/test/cmdlineTests/standard_model_checker_engine_bmc/output.json new file mode 100644 index 000000000..60f83c038 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_engine_bmc/output.json @@ -0,0 +1,30 @@ +{"auxiliaryInputRequested":{"smtlib2queries":{"0x4ca2adc24a17cd524cf3113f3b2cddff216f428f804e884cf76d27dd3e72cd68":"(set-option :produce-models true) +(set-logic ALL) +(declare-fun |error_0| () Int) +(declare-fun |this_0| () Int) +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-fun |state_0| () |state_type|) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-fun |tx_0| () |tx_type|) +(declare-fun |x_4_0| () Int) +(declare-fun |expr_8_0| () Int) +(declare-fun |expr_9_0| () Int) +(declare-fun |expr_10_1| () Bool) + +(assert (and (and true (and (= expr_10_1 (> expr_8_0 expr_9_0)) (and (= expr_9_0 0) (and (= expr_8_0 x_4_0) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true))))) (not expr_10_1))) +(declare-const |EVALEXPR_0| Int) +(assert (= |EVALEXPR_0| x_4_0)) +(check-sat) +(get-value (|EVALEXPR_0| )) +"}},"errors":[{"component":"general","errorCode":"4661","formattedMessage":"A:4:47: Warning: BMC: Assertion violation happens here. +contract C { function f(uint x) public pure { assert(x > 0); } } + ^-----------^ +Counterexample: + x = 0 + +Callstack: + +","message":"BMC: Assertion violation happens here.","secondarySourceLocations":[{"message":"Counterexample: + x = 0 +"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":150,"file":"A","start":137},"type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_engine_chc/input.json b/test/cmdlineTests/standard_model_checker_engine_chc/input.json new file mode 100644 index 000000000..fa887c8da --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_engine_chc/input.json @@ -0,0 +1,14 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract C { function f(uint x) public pure { assert(x > 0); } }" + } + }, + "settings": + { + "modelCheckerEngine": "chc" + } +} diff --git a/test/cmdlineTests/standard_model_checker_engine_chc/output.json b/test/cmdlineTests/standard_model_checker_engine_chc/output.json new file mode 100644 index 000000000..c8e59e0d8 --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_engine_chc/output.json @@ -0,0 +1,19 @@ +{"errors":[{"component":"general","errorCode":"6328","formattedMessage":"A:4:47: Warning: CHC: Assertion violation happens here. +contract C { function f(uint x) public pure { assert(x > 0); } } + ^-----------^ +Counterexample: + +x = 0 + + +Transaction trace: +constructor() +f(0) +","message":"CHC: Assertion violation happens here.","secondarySourceLocations":[{"message":"Counterexample: + +x = 0 + + +Transaction trace: +constructor() +f(0)"}],"severity":"warning","sourceLocation":{"end":150,"file":"A","start":137},"type":"Warning"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_engine_none/input.json b/test/cmdlineTests/standard_model_checker_engine_none/input.json new file mode 100644 index 000000000..8804dfcbf --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_engine_none/input.json @@ -0,0 +1,14 @@ +{ + "language": "Solidity", + "sources": + { + "A": + { + "content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract C { function f(uint x) public pure { assert(x > 0); } }" + } + }, + "settings": + { + "modelCheckerEngine": "none" + } +} diff --git a/test/cmdlineTests/standard_model_checker_engine_none/output.json b/test/cmdlineTests/standard_model_checker_engine_none/output.json new file mode 100644 index 000000000..59b90c8cc --- /dev/null +++ b/test/cmdlineTests/standard_model_checker_engine_none/output.json @@ -0,0 +1 @@ +{"sources":{"A":{"id":0}}}