diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp index 909202094..dfe0cb913 100644 --- a/libsolidity/formal/CVC4Interface.cpp +++ b/libsolidity/formal/CVC4Interface.cpp @@ -137,6 +137,8 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr) return m_context.mkConst(true); else if (n == "false") return m_context.mkConst(false); + else if (auto sortSort = dynamic_pointer_cast(_expr.sort)) + return m_context.mkVar(n, cvc4Sort(*sortSort->inner)); else try { @@ -187,6 +189,12 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr) return m_context.mkExpr(CVC4::kind::SELECT, arguments[0], arguments[1]); else if (n == "store") return m_context.mkExpr(CVC4::kind::STORE, arguments[0], arguments[1], arguments[2]); + else if (n == "const_array") + { + shared_ptr sortSort = std::dynamic_pointer_cast(_expr.arguments[0].sort); + solAssert(sortSort, ""); + return m_context.mkConst(CVC4::ArrayStoreAll(cvc4Sort(*sortSort->inner), arguments[1])); + } solAssert(false, ""); } diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp index a23dbe559..7d6e5d457 100644 --- a/libsolidity/formal/SMTLib2Interface.cpp +++ b/libsolidity/formal/SMTLib2Interface.cpp @@ -17,8 +17,6 @@ #include -#include -#include #include #include @@ -30,7 +28,6 @@ #include #include #include -#include using namespace std; using namespace dev; diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h index 5610a5fd6..0004e1726 100644 --- a/libsolidity/formal/SolverInterface.h +++ b/libsolidity/formal/SolverInterface.h @@ -17,6 +17,7 @@ #pragma once +#include #include #include #include @@ -45,7 +46,8 @@ enum class Kind Int, Bool, Function, - Array + Array, + Sort }; struct Sort @@ -110,12 +112,33 @@ struct ArraySort: public Sort SortPointer range; }; +struct SortSort: public Sort +{ + SortSort(SortPointer _inner): Sort(Kind::Sort), inner(std::move(_inner)) {} + bool operator==(Sort const& _other) const override + { + if (!Sort::operator==(_other)) + return false; + auto _otherSort = dynamic_cast(&_other); + solAssert(_otherSort, ""); + solAssert(_otherSort->inner, ""); + solAssert(inner, ""); + return *inner == *_otherSort->inner; + } + + SortPointer inner; +}; + +// Forward declaration. +SortPointer smtSort(solidity::Type const& _type); + /// C++ representation of an SMTLIB2 expression. class Expression { friend class SolverInterface; public: explicit Expression(bool _v): Expression(_v ? "true" : "false", Kind::Bool) {} + explicit Expression(solidity::TypePointer _type): Expression(_type->toString(), {}, std::make_shared(smtSort(*_type))) {} Expression(size_t _number): Expression(std::to_string(_number), Kind::Int) {} Expression(u256 const& _number): Expression(_number.str(), Kind::Int) {} Expression(s256 const& _number): Expression(_number.str(), Kind::Int) {} @@ -145,7 +168,8 @@ public: {"/", 2}, {"mod", 2}, {"select", 2}, - {"store", 3} + {"store", 3}, + {"const_array", 2} }; return operatorsArity.count(name) && operatorsArity.at(name) == arguments.size(); } @@ -202,6 +226,21 @@ public: ); } + static Expression const_array(Expression _sort, Expression _value) + { + solAssert(_sort.sort->kind == Kind::Sort, ""); + auto sortSort = std::dynamic_pointer_cast(_sort.sort); + auto arraySort = std::dynamic_pointer_cast(sortSort->inner); + solAssert(sortSort && arraySort, ""); + solAssert(_value.sort, ""); + solAssert(*arraySort->range == *_value.sort, ""); + return Expression( + "const_array", + std::vector{std::move(_sort), std::move(_value)}, + arraySort + ); + } + friend Expression operator!(Expression _a) { return Expression("not", std::move(_a), Kind::Bool); diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index 6b9f26d82..c6f964b0a 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -276,10 +276,31 @@ void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _c void setSymbolicZeroValue(Expression _expr, solidity::TypePointer const& _type, EncodingContext& _context) { solAssert(_type, ""); - if (isNumber(_type->category())) - _context.addAssertion(_expr == 0); - else if (isBool(_type->category())) - _context.addAssertion(_expr == Expression(false)); + _context.addAssertion(_expr == zeroValue(_type)); +} + +Expression zeroValue(solidity::TypePointer const& _type) +{ + solAssert(_type, ""); + if (isSupportedType(_type->category())) + { + if (isNumber(_type->category())) + return 0; + if (isBool(_type->category())) + return Expression(false); + if (isArray(_type->category()) || isMapping(_type->category())) + { + if (auto arrayType = dynamic_cast(_type)) + return Expression::const_array(Expression(arrayType), zeroValue(arrayType->baseType())); + auto mappingType = dynamic_cast(_type); + solAssert(mappingType, ""); + return Expression::const_array(Expression(mappingType), zeroValue(mappingType->valueType())); + + } + solAssert(false, ""); + } + // Unsupported types are abstracted as Int. + return 0; } void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& _context) diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h index 355c25328..30a341431 100644 --- a/libsolidity/formal/SymbolicTypes.h +++ b/libsolidity/formal/SymbolicTypes.h @@ -63,6 +63,7 @@ std::pair> newSymbolicVariable(solidity: Expression minValue(solidity::IntegerType const& _type); Expression maxValue(solidity::IntegerType const& _type); +Expression zeroValue(solidity::TypePointer const& _type); void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _context); void setSymbolicZeroValue(Expression _expr, solidity::TypePointer const& _type, EncodingContext& _context); diff --git a/libsolidity/formal/Z3CHCInterface.cpp b/libsolidity/formal/Z3CHCInterface.cpp index 7b8de2c91..909a34b02 100644 --- a/libsolidity/formal/Z3CHCInterface.cpp +++ b/libsolidity/formal/Z3CHCInterface.cpp @@ -33,6 +33,17 @@ Z3CHCInterface::Z3CHCInterface(): z3::set_param("rewriter.pull_cheap_ite", true); // This needs to be set in the context. m_context->set("timeout", queryTimeout); + + // 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); + // Ground pobs by using values from a model. + p.set("fp.spacer.ground_pobs", false); + m_solver.set(p); } void Z3CHCInterface::declareVariable(string const& _name, Sort const& _sort) @@ -82,9 +93,11 @@ pair> Z3CHCInterface::query(Expression const& _expr) break; } case z3::check_result::unknown: + { result = CheckResult::UNKNOWN; break; } + } // TODO retrieve model / invariants } catch (z3::exception const& _e) diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp index 1039dd1f8..e07bacdb7 100644 --- a/libsolidity/formal/Z3Interface.cpp +++ b/libsolidity/formal/Z3Interface.cpp @@ -132,6 +132,12 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) return m_context.bool_val(true); else if (n == "false") return m_context.bool_val(false); + else if (_expr.sort->kind == Kind::Sort) + { + auto sortSort = dynamic_pointer_cast(_expr.sort); + solAssert(sortSort, ""); + return m_context.constant(n.c_str(), z3Sort(*sortSort->inner)); + } else try { @@ -178,6 +184,14 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) return z3::select(arguments[0], arguments[1]); else if (n == "store") return z3::store(arguments[0], arguments[1], arguments[2]); + else if (n == "const_array") + { + shared_ptr sortSort = std::dynamic_pointer_cast(_expr.arguments[0].sort); + solAssert(sortSort, ""); + auto arraySort = dynamic_pointer_cast(sortSort->inner); + solAssert(arraySort && arraySort->domain, ""); + return z3::const_array(z3Sort(*arraySort->domain), arguments[1]); + } solAssert(false, ""); } diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index 3e5a69a3c..c7414d824 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -212,7 +212,7 @@ BOOST_AUTO_TEST_CASE(compound_assignment_division) uint[] array; function f(uint x, uint p) public { require(x == 2); - require(array[p] == 10); + array[p] = 10; array[p] /= array[p] / x; assert(array[p] == x); assert(array[p] == 0); @@ -225,7 +225,7 @@ BOOST_AUTO_TEST_CASE(compound_assignment_division) mapping (uint => uint) map; function f(uint x, uint p) public { require(x == 2); - require(map[p] == 10); + map[p] = 10; map[p] /= map[p] / x; assert(map[p] == x); assert(map[p] == 0); diff --git a/test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol b/test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol index 816aff23a..c4acd3842 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol @@ -5,11 +5,11 @@ contract C uint[] array; function f(uint x, uint p) public { require(x < 100); - require(array[p] == 100); + array[p] = 100; array[p] += array[p] + x; assert(array[p] < 300); assert(array[p] < 110); } } // ---- -// Warning: (202-224): Assertion violation happens here +// Warning: (192-214): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/compound_add_mapping.sol b/test/libsolidity/smtCheckerTests/operators/compound_add_mapping.sol index f342ab97d..eab7df2f0 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_add_mapping.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_add_mapping.sol @@ -5,11 +5,11 @@ contract C mapping (uint => uint) map; function f(uint x, uint p) public { require(x < 100); - require(map[p] == 100); + map[p] = 100; map[p] += map[p] + x; assert(map[p] < 300); assert(map[p] < 110); } } // ---- -// Warning: (208-228): Assertion violation happens here +// Warning: (198-218): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/compound_mul_array_index.sol b/test/libsolidity/smtCheckerTests/operators/compound_mul_array_index.sol index ea837801d..110eb868e 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_mul_array_index.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_mul_array_index.sol @@ -5,11 +5,11 @@ contract C uint[] array; function f(uint x, uint p) public { require(x < 10); - require(array[p] == 10); + array[p] = 10; array[p] *= array[p] + x; assert(array[p] <= 190); assert(array[p] < 50); } } // ---- -// Warning: (201-222): Assertion violation happens here +// Warning: (191-212): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/compound_mul_mapping.sol b/test/libsolidity/smtCheckerTests/operators/compound_mul_mapping.sol index fbcb5d88c..cd73bc687 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_mul_mapping.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_mul_mapping.sol @@ -5,11 +5,11 @@ contract C mapping (uint => uint) map; function f(uint x, uint p) public { require(x < 10); - require(map[p] == 10); + map[p] = 10; map[p] *= map[p] + x; assert(map[p] <= 190); assert(map[p] < 50); } } // ---- -// Warning: (207-226): Assertion violation happens here +// Warning: (197-216): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/compound_sub_array_index.sol b/test/libsolidity/smtCheckerTests/operators/compound_sub_array_index.sol index b966337e9..8c8f84627 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_sub_array_index.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_sub_array_index.sol @@ -5,11 +5,11 @@ contract C uint[] array; function f(uint x, uint p) public { require(x < 100); - require(array[p] == 200); + array[p] = 200; array[p] -= array[p] - x; assert(array[p] >= 0); assert(array[p] < 90); } } // ---- -// Warning: (201-222): Assertion violation happens here +// Warning: (191-212): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/compound_sub_mapping.sol b/test/libsolidity/smtCheckerTests/operators/compound_sub_mapping.sol index df20d3712..92e315832 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_sub_mapping.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_sub_mapping.sol @@ -5,11 +5,11 @@ contract C mapping (uint => uint) map; function f(uint x, uint p) public { require(x < 100); - require(map[p] == 200); + map[p] = 200; map[p] -= map[p] - x; assert(map[p] >= 0); assert(map[p] < 90); } } // ---- -// Warning: (207-226): Assertion violation happens here +// Warning: (197-216): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/delete_array.sol b/test/libsolidity/smtCheckerTests/operators/delete_array.sol index 0a223d2a5..d34b0862c 100644 --- a/test/libsolidity/smtCheckerTests/operators/delete_array.sol +++ b/test/libsolidity/smtCheckerTests/operators/delete_array.sol @@ -10,12 +10,9 @@ contract C delete a; else delete a[2]; - // Assertion fails as false positive because - // setZeroValue for arrays needs \forall i . a[i] = 0 - // which is still unimplemented. assert(a[2] == 0); + assert(a[1] == 0); } } // ---- // Warning: (118-119): Condition is always true. -// Warning: (297-314): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/delete_array_2d.sol b/test/libsolidity/smtCheckerTests/operators/delete_array_2d.sol index b8ce28f58..deff5bd10 100644 --- a/test/libsolidity/smtCheckerTests/operators/delete_array_2d.sol +++ b/test/libsolidity/smtCheckerTests/operators/delete_array_2d.sol @@ -6,10 +6,6 @@ contract C function f() public { require(a[2][3] == 4); delete a; - // Fails as false positive. - // setZeroValue needs forall for arrays. assert(a[2][3] == 0); } } -// ---- -// Warning: (194-214): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol b/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol index cafc09207..3e13c7f84 100644 --- a/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol +++ b/test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol @@ -9,11 +9,7 @@ contract C delete a; else delete a[2]; - // Fails as false positive since - // setZeroValue for arrays needs forall - // which is unimplemented. assert(a[2][3] == 0); + assert(a[1][1] == 0); } } -// ---- -// Warning: (266-286): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/delete_function.sol b/test/libsolidity/smtCheckerTests/operators/delete_function.sol index 5c730b3d8..62579d7da 100644 --- a/test/libsolidity/smtCheckerTests/operators/delete_function.sol +++ b/test/libsolidity/smtCheckerTests/operators/delete_function.sol @@ -16,12 +16,9 @@ contract C g(); else h(); - // Assertion fails as false positive because - // setZeroValue for arrays needs \forall i . a[i] = 0 - // which is still unimplemented. assert(a[2] == 0); + assert(a[1] == 0); } } // ---- // Warning: (201-202): Condition is always true. -// Warning: (367-384): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_dynamic_2_fail.sol b/test/libsolidity/smtCheckerTests/types/array_dynamic_2_fail.sol index 725e51ba2..8555b0613 100644 --- a/test/libsolidity/smtCheckerTests/types/array_dynamic_2_fail.sol +++ b/test/libsolidity/smtCheckerTests/types/array_dynamic_2_fail.sol @@ -4,10 +4,11 @@ contract C { uint[][] array; function f(uint x, uint y, uint z, uint t) public view { - require(array[x][y] == 200); + // TODO change to = 200 when 2d assignments are supported. + require(array[x][y] < 200); require(x == z && y == t); assert(array[z][t] > 300); } } // ---- -// Warning: (183-208): Assertion violation happens here +// Warning: (243-268): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_dynamic_3_fail.sol b/test/libsolidity/smtCheckerTests/types/array_dynamic_3_fail.sol index 3a34ce5dd..d7eb8bccb 100644 --- a/test/libsolidity/smtCheckerTests/types/array_dynamic_3_fail.sol +++ b/test/libsolidity/smtCheckerTests/types/array_dynamic_3_fail.sol @@ -4,10 +4,11 @@ contract C { uint[][][] array; function f(uint x, uint y, uint z, uint t, uint w, uint v) public view { - require(array[x][y][z] == 200); + // TODO change to = 200 when 3d assignments are supported. + require(array[x][y][z] < 200); require(x == t && y == w && z == v); assert(array[t][w][v] > 300); } } // ---- -// Warning: (214-242): Assertion violation happens here +// Warning: (274-302): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_static_2_fail.sol b/test/libsolidity/smtCheckerTests/types/array_static_2_fail.sol index 789308c57..b230886de 100644 --- a/test/libsolidity/smtCheckerTests/types/array_static_2_fail.sol +++ b/test/libsolidity/smtCheckerTests/types/array_static_2_fail.sol @@ -4,10 +4,10 @@ contract C { uint[10][20] array; function f(uint x, uint y, uint z, uint t) public view { - require(array[x][y] == 200); + require(array[x][y] < 200); require(x == z && y == t); assert(array[z][t] > 300); } } // ---- -// Warning: (187-212): Assertion violation happens here +// Warning: (186-211): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_static_3_fail.sol b/test/libsolidity/smtCheckerTests/types/array_static_3_fail.sol index 240a11067..22a2f0506 100644 --- a/test/libsolidity/smtCheckerTests/types/array_static_3_fail.sol +++ b/test/libsolidity/smtCheckerTests/types/array_static_3_fail.sol @@ -4,10 +4,11 @@ contract C { uint[10][20][30] array; function f(uint x, uint y, uint z, uint t, uint w, uint v) public view { - require(array[x][y][z] == 200); + // TODO change to = 200 when 3d assignments are supported. + require(array[x][y][z] < 200); require(x == t && y == w && z == v); assert(array[t][w][v] > 300); } } // ---- -// Warning: (220-248): Assertion violation happens here +// Warning: (280-308): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/mapping_4.sol b/test/libsolidity/smtCheckerTests/types/mapping_4.sol index d02042113..7356a3b6b 100644 --- a/test/libsolidity/smtCheckerTests/types/mapping_4.sol +++ b/test/libsolidity/smtCheckerTests/types/mapping_4.sol @@ -9,4 +9,3 @@ contract C } } // ---- -// Warning: (125-144): Assertion violation happens here