From 5bb4e7369359658d8bc064fad98c930efacc3887 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 14 Jul 2020 17:41:19 +0200 Subject: [PATCH] Review 1 --- libsmtutil/Z3CHCInterface.cpp | 42 +++++++------------ libsmtutil/Z3CHCInterface.h | 3 +- libsolidity/formal/CHC.cpp | 28 +++++++++---- libsolidity/formal/CHC.h | 4 +- test/InteractiveTests.h | 1 - .../operators/delete_multid_array.sol | 4 +- .../smtCheckerTestsJSON/multi.json | 10 ----- .../libsolidity/smtCheckerTestsJSON/multi.sol | 14 ------- .../smtCheckerTestsJSON/simple.json | 9 ---- .../smtCheckerTestsJSON/simple.sol | 11 ----- 10 files changed, 40 insertions(+), 86 deletions(-) delete mode 100644 test/libsolidity/smtCheckerTestsJSON/multi.json delete mode 100644 test/libsolidity/smtCheckerTestsJSON/multi.sol delete mode 100644 test/libsolidity/smtCheckerTestsJSON/simple.json delete mode 100644 test/libsolidity/smtCheckerTestsJSON/simple.sol diff --git a/libsmtutil/Z3CHCInterface.cpp b/libsmtutil/Z3CHCInterface.cpp index 4baf3bd0a..9ea155621 100644 --- a/libsmtutil/Z3CHCInterface.cpp +++ b/libsmtutil/Z3CHCInterface.cpp @@ -36,7 +36,7 @@ Z3CHCInterface::Z3CHCInterface(): z3::set_param("rewriter.pull_cheap_ite", true); z3::set_param("rlimit", Z3Interface::resourceLimit); - enablePreProcessing(); + setSpacerOptions(); } void Z3CHCInterface::declareVariable(string const& _name, SortPointer const& _sort) @@ -104,7 +104,7 @@ pair Z3CHCInterface::query(Expression return {result, cex}; } -void Z3CHCInterface::enablePreProcessing() +void Z3CHCInterface::setSpacerOptions(bool _preProcessing) { // Spacer options. // These needs to be set in the solver. @@ -117,31 +117,12 @@ void Z3CHCInterface::enablePreProcessing() // Ground pobs by using values from a model. p.set("fp.spacer.ground_pobs", false); - // Enable Spacer optimization for better solving. - p.set("fp.xform.slice", true); - p.set("fp.xform.inline_linear", true); - p.set("fp.xform.inline_eager", true); - - m_solver.set(p); -} - -void Z3CHCInterface::disablePreProcessing() -{ - // Spacer options. - // These needs to be set in the solver. - // https://github.com/Z3Prover/z3/blob/master/src/muz/base/fp_params.pyg - z3::params p(*m_context); - // These are useful for solving problems with arrays and loops. - // Use quantified lemma generalizer. - p.set("fp.spacer.q3.use_qgen", true); - p.set("fp.spacer.mbqi", false); - // Ground pobs by using values from a model. - p.set("fp.spacer.ground_pobs", false); - - // Disable Spacer optimization for counterexample generation. - p.set("fp.xform.slice", false); - p.set("fp.xform.inline_linear", false); - p.set("fp.xform.inline_eager", false); + // Spacer optimization should be + // - enabled for better solving (default) + // - disable for counterexample generation + p.set("fp.xform.slice", _preProcessing); + p.set("fp.xform.inline_linear", _preProcessing); + p.set("fp.xform.inline_eager", _preProcessing); m_solver.set(p); } @@ -151,6 +132,13 @@ Convert a ground refutation into a linear or nonlinear counterexample. The counterexample is given as an implication graph of the form `premises => conclusion` where `premises` are the predicates from the body of nonlinear clauses, representing the proof graph. + +This function is based on and similar to +https://github.com/Z3Prover/z3/blob/z3-4.8.8/src/muz/spacer/spacer_context.cpp#L2919 +(spacer::context::get_ground_sat_answer) +which generates linear counterexamples. +It is modified here to accept nonlinear CHCs as well, generating a DAG +instead of a path. */ CHCSolverInterface::CexGraph Z3CHCInterface::cexGraph(z3::expr const& _proof) { diff --git a/libsmtutil/Z3CHCInterface.h b/libsmtutil/Z3CHCInterface.h index e30611f0f..00e4ca285 100644 --- a/libsmtutil/Z3CHCInterface.h +++ b/libsmtutil/Z3CHCInterface.h @@ -46,8 +46,7 @@ public: Z3Interface* z3Interface() const { return m_z3Interface.get(); } - void enablePreProcessing(); - void disablePreProcessing(); + void setSpacerOptions(bool _preProcessing = true); private: /// Constructs a nonlinear counterexample graph from the refutation. diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index e687dffec..3a865c4bc 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -32,6 +32,8 @@ #include #include +#include + using namespace std; using namespace solidity; using namespace solidity::util; @@ -569,6 +571,7 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall) m_context.variable(*var)->increaseIndex(); auto nondet = (*m_nondetInterfaces.at(m_currentContract))(preCallState + currentStateVariables()); + m_symbolFunction[nondet.name] = &_funCall; m_context.addAssertion(nondet); m_context.addAssertion(m_error.currentValue() == 0); @@ -1134,7 +1137,7 @@ pair CHC::query(smtutil::Exp // We now disable those optimizations and check whether we can still solve the problem. auto* spacer = dynamic_cast(m_interface.get()); solAssert(spacer, ""); - spacer->disablePreProcessing(); + spacer->setSpacerOptions(false); smtutil::CheckResult resultNoOpt; CHCSolverInterface::CexGraph cexNoOpt; @@ -1143,7 +1146,7 @@ pair CHC::query(smtutil::Exp if (resultNoOpt == smtutil::CheckResult::SATISFIABLE) cex = move(cexNoOpt); - spacer->enablePreProcessing(); + spacer->setSpacerOptions(true); #endif break; } @@ -1312,7 +1315,8 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& string localState; unsigned node = *rootId; - optional lastTxSeen; + /// The first summary node seen in this loop represents the last transaction. + bool lastTxSeen = false; while (_graph.edges.at(node).size() >= 1) { auto const& edges = _graph.edges.at(node); @@ -1328,6 +1332,8 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& swap(summaryId, *interfaceId); solAssert(_graph.nodes.at(*interfaceId).first.rfind("interface", 0) == 0, ""); } + /// The children are unordered, so we need to check which is the summary and + /// which is the interface. solAssert(_graph.nodes.at(summaryId).first.rfind("summary", 0) == 0, ""); /// At this point property 2 from the function description is verified for this node. @@ -1360,9 +1366,9 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& /// but not necessarily the summary of the function that contains the error. if (!lastTxSeen) { - lastTxSeen = summaryNode.first; + lastTxSeen = true; /// Generate counterexample message local to the failed target. - localState = generatePostStateCounterexample(stateVars, calledFun, summaryNode.second) + "\n"; + localState = formatStateCounterexample(stateVars, calledFun, summaryNode.second) + "\n"; if (calledFun) { /// The signature of a summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars). @@ -1389,9 +1395,9 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& else /// 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: " + generatePostStateCounterexample(stateVars, calledFun, summaryNode.second)); + path.emplace_back("State: " + formatStateCounterexample(stateVars, calledFun, summaryNode.second)); - string txCex = calledContract ? "constructor()" : generatePreTxCounterexample(stateVars, *calledFun, summaryNode.second); + string txCex = calledContract ? "constructor()" : formatFunctionCallCounterexample(stateVars, *calledFun, summaryNode.second); path.emplace_back(txCex); /// Recurse on the next interface node which represents the previous transaction @@ -1405,7 +1411,7 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& return localState + "\nTransaction trace:\n" + boost::algorithm::join(boost::adaptors::reverse(path), "\n"); } -string CHC::generatePostStateCounterexample(vector const& _stateVars, FunctionDefinition const* _function, vector const& _summaryValues) +string CHC::formatStateCounterexample(vector const& _stateVars, FunctionDefinition const* _function, vector const& _summaryValues) { /// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars). /// The signature of an implicit constructor summary predicate is: summary(error, postStateVars). @@ -1423,6 +1429,8 @@ string CHC::generatePostStateCounterexample(vector c stateLast = stateFirst + static_cast(_stateVars.size()); } + solAssert(stateFirst >= _summaryValues.begin() && stateFirst <= _summaryValues.end(), ""); + solAssert(stateLast >= _summaryValues.begin() && stateLast <= _summaryValues.end(), ""); vector stateArgs(stateFirst, stateLast); solAssert(stateArgs.size() == _stateVars.size(), ""); @@ -1437,12 +1445,14 @@ string CHC::generatePostStateCounterexample(vector c return boost::algorithm::join(stateCex, ", "); } -string CHC::generatePreTxCounterexample(vector const& _stateVars, FunctionDefinition const& _function, vector const& _summaryValues) +string CHC::formatFunctionCallCounterexample(vector const& _stateVars, FunctionDefinition const& _function, vector const& _summaryValues) { /// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars). /// Here we are interested in preInputVars. vector::const_iterator first = _summaryValues.begin() + static_cast(_stateVars.size()) + 1; vector::const_iterator last = first + static_cast(_function.parameters().size()); + solAssert(first >= _summaryValues.begin() && first <= _summaryValues.end(), ""); + solAssert(last >= _summaryValues.begin() && last <= _summaryValues.end(), ""); vector functionArgsCex(first, last); vector functionArgs; diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 3334a45e4..1b2ec493d 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -218,11 +218,11 @@ private: /// _function was executed. /// _function = nullptr means the transaction was the deployment of a /// contract without an explicit constructor. - std::string generatePostStateCounterexample(std::vector const& _stateVariables, FunctionDefinition const* _function, std::vector const& _summaryValues); + std::string formatStateCounterexample(std::vector const& _stateVariables, FunctionDefinition const* _function, std::vector const& _summaryValues); /// @returns a formatted text representing a call to _function /// with the concrete values for value type parameters and /// the parameter name for reference types. - std::string generatePreTxCounterexample(std::vector const& _stateVariables, FunctionDefinition const& _function, std::vector const& _summaryValues); + std::string formatFunctionCallCounterexample(std::vector const& _stateVariables, FunctionDefinition const& _function, std::vector const& _summaryValues); //@} /// Misc. diff --git a/test/InteractiveTests.h b/test/InteractiveTests.h index 46d8a2973..7ecc8de5e 100644 --- a/test/InteractiveTests.h +++ b/test/InteractiveTests.h @@ -67,7 +67,6 @@ Testsuite const g_interactiveTestsuites[] = { {"JSON AST", "libsolidity", "ASTJSON", false, false, &ASTJSONTest::create}, {"JSON ABI", "libsolidity", "ABIJson", false, false, &ABIJsonTest::create}, {"SMT Checker", "libsolidity", "smtCheckerTests", true, false, &SMTCheckerTest::create, {"nooptions"}}, - {"SMT Checker JSON", "libsolidity", "smtCheckerTestsJSON", true, false, &SMTCheckerJSONTest::create, {"nooptions"}}, {"Gas Estimates", "libsolidity", "gasTests", false, false, &GasTest::create} }; diff --git a/test/libsolidity/smtCheckerTests/operators/delete_multid_array.sol b/test/libsolidity/smtCheckerTests/operators/delete_multid_array.sol index 91527b8c7..f52da7a3d 100644 --- a/test/libsolidity/smtCheckerTests/operators/delete_multid_array.sol +++ b/test/libsolidity/smtCheckerTests/operators/delete_multid_array.sol @@ -37,6 +37,8 @@ contract C { b[x][y] = z; } } +// ==== +// SMTSolvers: cvc4 // ---- -// Warning 6328: (617-637): Assertion violation happens here. // Warning 4661: (372-392): Assertion violation happens here +// Warning 4661: (617-637): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTestsJSON/multi.json b/test/libsolidity/smtCheckerTestsJSON/multi.json deleted file mode 100644 index 986429dac..000000000 --- a/test/libsolidity/smtCheckerTestsJSON/multi.json +++ /dev/null @@ -1,10 +0,0 @@ -{ - "auxiliaryInput": - { - "smtlib2responses": - { - "0x45598870c7c0bc4c4f61acad7e0dd9399fb28aa3df198379dd36a95d70814ef8": "sat\n((|EVALEXPR_0| 1))\n", - "0xee335f8104fdb81b6e5fb418725923b81f7d78ffbd6bf95fb82e5593a1ac366a": "sat\n((|EVALEXPR_0| 0))\n" - } - } -} diff --git a/test/libsolidity/smtCheckerTestsJSON/multi.sol b/test/libsolidity/smtCheckerTestsJSON/multi.sol deleted file mode 100644 index d81d76cb0..000000000 --- a/test/libsolidity/smtCheckerTestsJSON/multi.sol +++ /dev/null @@ -1,14 +0,0 @@ -==== Source: A ==== -pragma experimental SMTChecker; - -contract C -{ - function f(uint x) public pure { - assert(x > 0); - assert(x > 100); - assert(x >= 0); - } -} -// ---- -// Warning: (82-95): Assertion violation happens here -// Warning: (99-114): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTestsJSON/simple.json b/test/libsolidity/smtCheckerTestsJSON/simple.json deleted file mode 100644 index 0b70ea24b..000000000 --- a/test/libsolidity/smtCheckerTestsJSON/simple.json +++ /dev/null @@ -1,9 +0,0 @@ -{ - "auxiliaryInput": - { - "smtlib2responses": - { - "0x535c76d6b87d14bd4b4bf1014d14b8e91b648f073a68f9f267c4fe1df570bc14": "sat\n((|EVALEXPR_0| 0))\n" - } - } -} diff --git a/test/libsolidity/smtCheckerTestsJSON/simple.sol b/test/libsolidity/smtCheckerTestsJSON/simple.sol deleted file mode 100644 index f93c8fd79..000000000 --- a/test/libsolidity/smtCheckerTestsJSON/simple.sol +++ /dev/null @@ -1,11 +0,0 @@ -==== Source: A ==== -pragma experimental SMTChecker; - -contract C -{ - function f(uint x) public pure { - assert(x > 0); - } -} -// ---- -// Warning: (82-95): Assertion violation happens here