From 762d591a4755fbabfe8d2556bab10b77ec1d5bb5 Mon Sep 17 00:00:00 2001 From: chriseth Date: Wed, 22 Nov 2017 15:20:26 +0100 Subject: Introduce sorts for smt expressions. --- libsolidity/formal/SMTLib2Interface.cpp | 11 +----- libsolidity/formal/SMTLib2Interface.h | 8 ---- libsolidity/formal/SolverInterface.h | 66 +++++++++++++++++---------------- 3 files changed, 37 insertions(+), 48 deletions(-) diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp index c627057a..0e00665a 100644 --- a/libsolidity/formal/SMTLib2Interface.cpp +++ b/libsolidity/formal/SMTLib2Interface.cpp @@ -64,8 +64,6 @@ void SMTLib2Interface::pop() Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codomain) { - solAssert(!m_variables.count(_name), ""); - m_variables[_name] = SMTVariableType::Function; write( "(declare-fun |" + _name + @@ -80,16 +78,12 @@ Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codom Expression SMTLib2Interface::newInteger(string _name) { - solAssert(!m_variables.count(_name), ""); - m_variables[_name] = SMTVariableType::Integer; write("(declare-const |" + _name + "| Int)"); return SolverInterface::newInteger(move(_name)); } Expression SMTLib2Interface::newBool(string _name) { - solAssert(!m_variables.count(_name), ""); - m_variables[_name] = SMTVariableType::Bool; write("(declare-const |" + _name + "| Bool)"); return SolverInterface::newBool(std::move(_name)); } @@ -151,9 +145,8 @@ string SMTLib2Interface::checkSatAndGetValuesCommand(vector const& _ for (size_t i = 0; i < _expressionsToEvaluate.size(); i++) { auto const& e = _expressionsToEvaluate.at(i); - solAssert(m_variables.count(e.name), ""); - solAssert(m_variables[e.name] == SMTVariableType::Integer, ""); - command += "(declare-const |EVALEXPR_" + to_string(i) + "| Int)\n"; + solAssert(e.sort == Sort::Int || e.sort == Sort::Bool, "Invalid sort for expression to evaluate."); + command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + (e.sort == Sort::Int ? "Int" : "Bool") + "\n"; command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n"; } command += "(check-sat)\n"; diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h index e827449f..63188acd 100644 --- a/libsolidity/formal/SMTLib2Interface.h +++ b/libsolidity/formal/SMTLib2Interface.h @@ -68,14 +68,6 @@ private: ReadCallback::Callback m_queryCallback; std::vector m_accumulatedOutput; - - enum class SMTVariableType { - Function, - Integer, - Bool - }; - - std::map m_variables; }; } diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h index a69d19d5..ac722dad 100644 --- a/libsolidity/formal/SolverInterface.h +++ b/libsolidity/formal/SolverInterface.h @@ -44,7 +44,7 @@ enum class CheckResult enum class Sort { - Int, Bool + Int, Bool, IntIntFun }; /// C++ representation of an SMTLIB2 expression. @@ -52,10 +52,10 @@ class Expression { friend class SolverInterface; public: - explicit Expression(bool _v): name(_v ? "true" : "false") {} - Expression(size_t _number): name(std::to_string(_number)) {} - Expression(u256 const& _number): name(_number.str()) {} - Expression(bigint const& _number): name(_number.str()) {} + explicit Expression(bool _v): name(_v ? "true" : "false"), sort(Sort::Bool) {} + Expression(size_t _number): name(std::to_string(_number)), sort(Sort::Int) {} + Expression(u256 const& _number): name(_number.str()), sort(Sort::Int) {} + Expression(bigint const& _number): name(_number.str()), sort(Sort::Int) {} Expression(Expression const&) = default; Expression(Expression&&) = default; @@ -64,26 +64,27 @@ public: static Expression ite(Expression _condition, Expression _trueValue, Expression _falseValue) { + solAssert(_trueValue.sort == _falseValue.sort, ""); return Expression("ite", std::vector{ std::move(_condition), std::move(_trueValue), std::move(_falseValue) - }); + }, _trueValue.sort); } friend Expression operator!(Expression _a) { - return Expression("not", std::move(_a)); + return Expression("not", std::move(_a), Sort::Bool); } friend Expression operator&&(Expression _a, Expression _b) { - return Expression("and", std::move(_a), std::move(_b)); + return Expression("and", std::move(_a), std::move(_b), Sort::Bool); } friend Expression operator||(Expression _a, Expression _b) { - return Expression("or", std::move(_a), std::move(_b)); + return Expression("or", std::move(_a), std::move(_b), Sort::Bool); } friend Expression operator==(Expression _a, Expression _b) { - return Expression("=", std::move(_a), std::move(_b)); + return Expression("=", std::move(_a), std::move(_b), Sort::Bool); } friend Expression operator!=(Expression _a, Expression _b) { @@ -91,52 +92,54 @@ public: } friend Expression operator<(Expression _a, Expression _b) { - return Expression("<", std::move(_a), std::move(_b)); + return Expression("<", std::move(_a), std::move(_b), Sort::Bool); } friend Expression operator<=(Expression _a, Expression _b) { - return Expression("<=", std::move(_a), std::move(_b)); + return Expression("<=", std::move(_a), std::move(_b), Sort::Bool); } friend Expression operator>(Expression _a, Expression _b) { - return Expression(">", std::move(_a), std::move(_b)); + return Expression(">", std::move(_a), std::move(_b), Sort::Bool); } friend Expression operator>=(Expression _a, Expression _b) { - return Expression(">=", std::move(_a), std::move(_b)); + return Expression(">=", std::move(_a), std::move(_b), Sort::Bool); } friend Expression operator+(Expression _a, Expression _b) { - return Expression("+", std::move(_a), std::move(_b)); + return Expression("+", std::move(_a), std::move(_b), Sort::Int); } friend Expression operator-(Expression _a, Expression _b) { - return Expression("-", std::move(_a), std::move(_b)); + return Expression("-", std::move(_a), std::move(_b), Sort::Int); } friend Expression operator*(Expression _a, Expression _b) { - return Expression("*", std::move(_a), std::move(_b)); + return Expression("*", std::move(_a), std::move(_b), Sort::Int); } Expression operator()(Expression _a) const { + solAssert(sort == Sort::IntIntFun, "Attempted function application to non-function."); solAssert(arguments.empty(), "Attempted function application to non-function."); - return Expression(name, _a); + return Expression(name, _a, Sort::Int); } std::string const name; std::vector const arguments; + Sort sort; private: /// Manual constructor, should only be used by SolverInterface and this class itself. - Expression(std::string _name, std::vector _arguments): - name(std::move(_name)), arguments(std::move(_arguments)) {} - - explicit Expression(std::string _name): - Expression(std::move(_name), std::vector{}) {} - Expression(std::string _name, Expression _arg): - Expression(std::move(_name), std::vector{std::move(_arg)}) {} - Expression(std::string _name, Expression _arg1, Expression _arg2): - Expression(std::move(_name), std::vector{std::move(_arg1), std::move(_arg2)}) {} + Expression(std::string _name, std::vector _arguments, Sort _sort): + name(std::move(_name)), arguments(std::move(_arguments)), sort(_sort) {} + + explicit Expression(std::string _name, Sort _sort): + Expression(std::move(_name), std::vector{}, _sort) {} + Expression(std::string _name, Expression _arg, Sort _sort): + Expression(std::move(_name), std::vector{std::move(_arg)}, _sort) {} + Expression(std::string _name, Expression _arg1, Expression _arg2, Sort _sort): + Expression(std::move(_name), std::vector{std::move(_arg1), std::move(_arg2)}, _sort) {} }; DEV_SIMPLE_EXCEPTION(SolverError); @@ -149,20 +152,21 @@ public: virtual void push() = 0; virtual void pop() = 0; - virtual Expression newFunction(std::string _name, Sort /*_domain*/, Sort /*_codomain*/) + virtual Expression newFunction(std::string _name, Sort _domain, Sort _codomain) { + solAssert(_domain == Sort::Int && _codomain == Sort::Int, "Function sort not supported."); // Subclasses should do something here - return Expression(std::move(_name), {}); + return Expression(std::move(_name), {}, Sort::IntIntFun); } virtual Expression newInteger(std::string _name) { // Subclasses should do something here - return Expression(std::move(_name), {}); + return Expression(std::move(_name), {}, Sort::Int); } virtual Expression newBool(std::string _name) { // Subclasses should do something here - return Expression(std::move(_name), {}); + return Expression(std::move(_name), {}, Sort::Bool); } virtual void addAssertion(Expression const& _expr) = 0; -- cgit From 0e2a9658d231f75e5ac89fd58c5c880b46c4f4dc Mon Sep 17 00:00:00 2001 From: chriseth Date: Wed, 22 Nov 2017 17:12:22 +0100 Subject: Explain IntIntFun and merge assertion. --- libsolidity/formal/SolverInterface.h | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h index ac722dad..c9adf863 100644 --- a/libsolidity/formal/SolverInterface.h +++ b/libsolidity/formal/SolverInterface.h @@ -44,7 +44,9 @@ enum class CheckResult enum class Sort { - Int, Bool, IntIntFun + Int, + Bool, + IntIntFun // Function of one Int returning a single Int }; /// C++ representation of an SMTLIB2 expression. @@ -120,8 +122,10 @@ public: } Expression operator()(Expression _a) const { - solAssert(sort == Sort::IntIntFun, "Attempted function application to non-function."); - solAssert(arguments.empty(), "Attempted function application to non-function."); + solAssert( + sort == Sort::IntIntFun && arguments.empty(), + "Attempted function application to non-function." + ); return Expression(name, _a, Sort::Int); } -- cgit