From d9ce9cab99d71c9c112eb2f7125e71d2e7b011af Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 4 Jun 2019 14:23:44 +0200 Subject: [PATCH] [SMTChecker] Use smtlib's implies instead of \!a or b --- libsolidity/formal/CVC4Interface.cpp | 2 ++ libsolidity/formal/SolverInterface.h | 8 +++++++- libsolidity/formal/Z3Interface.cpp | 2 ++ test/libsolidity/smtCheckerTestsJSON/multi.json | 4 ++-- 4 files changed, 13 insertions(+), 3 deletions(-) diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp index 71f657471..b46d8ec38 100644 --- a/libsolidity/formal/CVC4Interface.cpp +++ b/libsolidity/formal/CVC4Interface.cpp @@ -145,6 +145,8 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr) return arguments[0].andExpr(arguments[1]); else if (n == "or") return arguments[0].orExpr(arguments[1]); + else if (n == "implies") + return m_context.mkExpr(CVC4::kind::IMPLIES, arguments[0], arguments[1]); else if (n == "=") return m_context.mkExpr(CVC4::kind::EQUAL, arguments[0], arguments[1]); else if (n == "<") diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h index 0c7f1dbdf..5610a5fd6 100644 --- a/libsolidity/formal/SolverInterface.h +++ b/libsolidity/formal/SolverInterface.h @@ -133,6 +133,7 @@ public: {"not", 1}, {"and", 2}, {"or", 2}, + {"implies", 2}, {"=", 2}, {"<", 2}, {"<=", 2}, @@ -160,7 +161,12 @@ public: static Expression implies(Expression _a, Expression _b) { - return !std::move(_a) || std::move(_b); + return Expression( + "implies", + std::move(_a), + std::move(_b), + Kind::Bool + ); } /// select is the SMT representation of an array index access. diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp index 4d7ea8347..20c7452b5 100644 --- a/libsolidity/formal/Z3Interface.cpp +++ b/libsolidity/formal/Z3Interface.cpp @@ -144,6 +144,8 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) return arguments[0] && arguments[1]; else if (n == "or") return arguments[0] || arguments[1]; + else if (n == "implies") + return z3::implies(arguments[0], arguments[1]); else if (n == "=") return arguments[0] == arguments[1]; else if (n == "<") diff --git a/test/libsolidity/smtCheckerTestsJSON/multi.json b/test/libsolidity/smtCheckerTestsJSON/multi.json index ba4cf2637..f892c28fe 100644 --- a/test/libsolidity/smtCheckerTestsJSON/multi.json +++ b/test/libsolidity/smtCheckerTestsJSON/multi.json @@ -3,8 +3,8 @@ { "smtlib2responses": { - "0x092d52dc5c2b54c1909592f7b3c8efedfd87afc0223ce421a24a1cc7905006b4": "sat\n((|EVALEXPR_0| 1))\n", - "0x8faacfc008b6f2278b5927ff22d76832956dfb46b3c21a64fab96583c241b88f": "unsat\n", + "0x0a0e9583fd983e7ce82e96bd95f7c0eb831e2dd3ce3364035e30bf1d22823b34": "sat\n((|EVALEXPR_0| 1))\n", + "0x15353582486fb1dac47801edbb366ae40a59ef0191ebe7c09ca32bdabecc2f1a": "unsat\n", "0xa66d08de30c873ca7d0e7e9e426f278640e0ee463a1aed2e4e80baee916b6869": "sat\n((|EVALEXPR_0| 0))\n" } }