From 087605ea021d1180791f3b34d162aa9d954f250b Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 18 May 2020 17:42:24 +0200 Subject: [PATCH 1/6] Create libsmtutil --- CMakeLists.txt | 18 ++++++++ .../CHCSmtLib2Interface.cpp | 2 +- .../CHCSmtLib2Interface.h | 4 +- .../CHCSolverInterface.h | 2 +- libsmtutil/CMakeLists.txt | 34 ++++++++++++++ .../formal => libsmtutil}/CVC4Interface.cpp | 2 +- .../formal => libsmtutil}/CVC4Interface.h | 2 +- .../SMTLib2Interface.cpp | 2 +- .../formal => libsmtutil}/SMTLib2Interface.h | 2 +- .../formal => libsmtutil}/SMTPortfolio.cpp | 8 ++-- .../formal => libsmtutil}/SMTPortfolio.h | 2 +- .../formal => libsmtutil}/SolverInterface.h | 2 +- {libsolidity/formal => libsmtutil}/Sorts.cpp | 2 +- {libsolidity/formal => libsmtutil}/Sorts.h | 0 .../formal => libsmtutil}/Z3CHCInterface.cpp | 2 +- .../formal => libsmtutil}/Z3CHCInterface.h | 4 +- .../formal => libsmtutil}/Z3Interface.cpp | 2 +- .../formal => libsmtutil}/Z3Interface.h | 2 +- libsolidity/CMakeLists.txt | 44 +------------------ libsolidity/formal/BMC.cpp | 3 +- libsolidity/formal/BMC.h | 3 +- libsolidity/formal/CHC.cpp | 5 +-- libsolidity/formal/CHC.h | 4 +- libsolidity/formal/EncodingContext.h | 3 +- libsolidity/formal/ModelChecker.h | 3 +- libsolidity/formal/SMTEncoder.cpp | 3 +- libsolidity/formal/SymbolicState.h | 5 ++- libsolidity/formal/SymbolicVariables.h | 3 +- libsolidity/interface/CompilerStack.h | 3 +- test/CMakeLists.txt | 2 +- test/libsolidity/SMTCheckerTest.h | 2 +- 31 files changed, 97 insertions(+), 78 deletions(-) rename {libsolidity/formal => libsmtutil}/CHCSmtLib2Interface.cpp (98%) rename {libsolidity/formal => libsmtutil}/CHCSmtLib2Interface.h (95%) rename {libsolidity/formal => libsmtutil}/CHCSolverInterface.h (96%) create mode 100644 libsmtutil/CMakeLists.txt rename {libsolidity/formal => libsmtutil}/CVC4Interface.cpp (99%) rename {libsolidity/formal => libsmtutil}/CVC4Interface.h (97%) rename {libsolidity/formal => libsmtutil}/SMTLib2Interface.cpp (99%) rename {libsolidity/formal => libsmtutil}/SMTLib2Interface.h (98%) rename {libsolidity/formal => libsmtutil}/SMTPortfolio.cpp (96%) rename {libsolidity/formal => libsmtutil}/SMTPortfolio.h (97%) rename {libsolidity/formal => libsmtutil}/SolverInterface.h (99%) rename {libsolidity/formal => libsmtutil}/Sorts.cpp (95%) rename {libsolidity/formal => libsmtutil}/Sorts.h (100%) rename {libsolidity/formal => libsmtutil}/Z3CHCInterface.cpp (98%) rename {libsolidity/formal => libsmtutil}/Z3CHCInterface.h (93%) rename {libsolidity/formal => libsmtutil}/Z3Interface.cpp (99%) rename {libsolidity/formal => libsmtutil}/Z3Interface.h (97%) diff --git a/CMakeLists.txt b/CMakeLists.txt index a5689009e..7aa6647b2 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -51,8 +51,26 @@ configure_file("${CMAKE_SOURCE_DIR}/cmake/templates/license.h.in" include/licens include(EthOptions) configure_project(TESTS) +find_package(Z3 4.6.0) +if (${Z3_FOUND}) + add_definitions(-DHAVE_Z3) + message("Z3 SMT solver found. This enables optional SMT checking with Z3.") +endif() + +find_package(CVC4 QUIET) +if (${CVC4_FOUND}) + add_definitions(-DHAVE_CVC4) + message("CVC4 SMT solver found. This enables optional SMT checking with CVC4.") +endif() + +if (NOT (${Z3_FOUND} OR ${CVC4_FOUND})) + message("No SMT solver found (or it has been forcefully disabled). Optional SMT checking will not be available.\ + \nPlease install Z3 or CVC4 or remove the option disabling them (USE_Z3, USE_CVC4).") +endif() + add_subdirectory(libsolutil) add_subdirectory(liblangutil) +add_subdirectory(libsmtutil) add_subdirectory(libevmasm) add_subdirectory(libyul) add_subdirectory(libsolidity) diff --git a/libsolidity/formal/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp similarity index 98% rename from libsolidity/formal/CHCSmtLib2Interface.cpp rename to libsmtutil/CHCSmtLib2Interface.cpp index 4b52b7d5a..d5895fc69 100644 --- a/libsolidity/formal/CHCSmtLib2Interface.cpp +++ b/libsmtutil/CHCSmtLib2Interface.cpp @@ -15,7 +15,7 @@ along with solidity. If not, see . */ -#include +#include #include diff --git a/libsolidity/formal/CHCSmtLib2Interface.h b/libsmtutil/CHCSmtLib2Interface.h similarity index 95% rename from libsolidity/formal/CHCSmtLib2Interface.h rename to libsmtutil/CHCSmtLib2Interface.h index d184cd9a4..9fd1489a4 100644 --- a/libsolidity/formal/CHCSmtLib2Interface.h +++ b/libsmtutil/CHCSmtLib2Interface.h @@ -21,9 +21,9 @@ #pragma once -#include +#include -#include +#include namespace solidity::frontend::smt { diff --git a/libsolidity/formal/CHCSolverInterface.h b/libsmtutil/CHCSolverInterface.h similarity index 96% rename from libsolidity/formal/CHCSolverInterface.h rename to libsmtutil/CHCSolverInterface.h index 91198e1a8..588e42ce1 100644 --- a/libsolidity/formal/CHCSolverInterface.h +++ b/libsmtutil/CHCSolverInterface.h @@ -21,7 +21,7 @@ #pragma once -#include +#include namespace solidity::frontend::smt { diff --git a/libsmtutil/CMakeLists.txt b/libsmtutil/CMakeLists.txt new file mode 100644 index 000000000..d5df3633f --- /dev/null +++ b/libsmtutil/CMakeLists.txt @@ -0,0 +1,34 @@ +set(sources + CHCSmtLib2Interface.cpp + CHCSmtLib2Interface.h + SMTLib2Interface.cpp + SMTLib2Interface.h + SMTPortfolio.cpp + SMTPortfolio.h + SolverInterface.h + Sorts.cpp + Sorts.h +) + +if (${Z3_FOUND}) + set(z3_SRCS Z3Interface.cpp Z3Interface.h Z3CHCInterface.cpp Z3CHCInterface.h) +else() + set(z3_SRCS) +endif() + +if (${CVC4_FOUND}) + set(cvc4_SRCS CVC4Interface.cpp CVC4Interface.h) +else() + set(cvc4_SRCS) +endif() + +add_library(smtutil ${sources} ${z3_SRCS} ${cvc4_SRCS}) +target_link_libraries(smtutil PUBLIC langutil solutil Boost::boost) + +if (${Z3_FOUND}) + target_link_libraries(smtutil PUBLIC z3::libz3) +endif() + +if (${CVC4_FOUND}) + target_link_libraries(smtutil PUBLIC CVC4::CVC4) +endif() diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsmtutil/CVC4Interface.cpp similarity index 99% rename from libsolidity/formal/CVC4Interface.cpp rename to libsmtutil/CVC4Interface.cpp index 86688e0b1..71ab81f51 100644 --- a/libsolidity/formal/CVC4Interface.cpp +++ b/libsmtutil/CVC4Interface.cpp @@ -15,7 +15,7 @@ along with solidity. If not, see . */ -#include +#include #include #include diff --git a/libsolidity/formal/CVC4Interface.h b/libsmtutil/CVC4Interface.h similarity index 97% rename from libsolidity/formal/CVC4Interface.h rename to libsmtutil/CVC4Interface.h index b5c2a3fd6..2399dc453 100644 --- a/libsolidity/formal/CVC4Interface.h +++ b/libsmtutil/CVC4Interface.h @@ -17,7 +17,7 @@ #pragma once -#include +#include #include #if defined(__GLIBC__) diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp similarity index 99% rename from libsolidity/formal/SMTLib2Interface.cpp rename to libsmtutil/SMTLib2Interface.cpp index 97ccc2c91..081d87f61 100644 --- a/libsolidity/formal/SMTLib2Interface.cpp +++ b/libsmtutil/SMTLib2Interface.cpp @@ -15,7 +15,7 @@ along with solidity. If not, see . */ -#include +#include #include diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsmtutil/SMTLib2Interface.h similarity index 98% rename from libsolidity/formal/SMTLib2Interface.h rename to libsmtutil/SMTLib2Interface.h index 5310f7e95..1acbcde2c 100644 --- a/libsolidity/formal/SMTLib2Interface.h +++ b/libsmtutil/SMTLib2Interface.h @@ -17,7 +17,7 @@ #pragma once -#include +#include #include #include diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsmtutil/SMTPortfolio.cpp similarity index 96% rename from libsolidity/formal/SMTPortfolio.cpp rename to libsmtutil/SMTPortfolio.cpp index 2ce698bdf..67cb3803c 100644 --- a/libsolidity/formal/SMTPortfolio.cpp +++ b/libsmtutil/SMTPortfolio.cpp @@ -15,15 +15,15 @@ along with solidity. If not, see . */ -#include +#include #ifdef HAVE_Z3 -#include +#include #endif #ifdef HAVE_CVC4 -#include +#include #endif -#include +#include using namespace std; using namespace solidity; diff --git a/libsolidity/formal/SMTPortfolio.h b/libsmtutil/SMTPortfolio.h similarity index 97% rename from libsolidity/formal/SMTPortfolio.h rename to libsmtutil/SMTPortfolio.h index 7799f2268..1ffce37ee 100644 --- a/libsolidity/formal/SMTPortfolio.h +++ b/libsmtutil/SMTPortfolio.h @@ -18,7 +18,7 @@ #pragma once -#include +#include #include #include diff --git a/libsolidity/formal/SolverInterface.h b/libsmtutil/SolverInterface.h similarity index 99% rename from libsolidity/formal/SolverInterface.h rename to libsmtutil/SolverInterface.h index 4532c1b3e..078eaef73 100644 --- a/libsolidity/formal/SolverInterface.h +++ b/libsmtutil/SolverInterface.h @@ -17,7 +17,7 @@ #pragma once -#include +#include #include #include diff --git a/libsolidity/formal/Sorts.cpp b/libsmtutil/Sorts.cpp similarity index 95% rename from libsolidity/formal/Sorts.cpp rename to libsmtutil/Sorts.cpp index 195048e56..dba0dc4b7 100644 --- a/libsolidity/formal/Sorts.cpp +++ b/libsmtutil/Sorts.cpp @@ -16,7 +16,7 @@ */ -#include +#include using namespace std; diff --git a/libsolidity/formal/Sorts.h b/libsmtutil/Sorts.h similarity index 100% rename from libsolidity/formal/Sorts.h rename to libsmtutil/Sorts.h diff --git a/libsolidity/formal/Z3CHCInterface.cpp b/libsmtutil/Z3CHCInterface.cpp similarity index 98% rename from libsolidity/formal/Z3CHCInterface.cpp rename to libsmtutil/Z3CHCInterface.cpp index c64da2edc..3be40d396 100644 --- a/libsolidity/formal/Z3CHCInterface.cpp +++ b/libsmtutil/Z3CHCInterface.cpp @@ -15,7 +15,7 @@ along with solidity. If not, see . */ -#include +#include #include #include diff --git a/libsolidity/formal/Z3CHCInterface.h b/libsmtutil/Z3CHCInterface.h similarity index 93% rename from libsolidity/formal/Z3CHCInterface.h rename to libsmtutil/Z3CHCInterface.h index a7b7d6aeb..bc0e6cf92 100644 --- a/libsolidity/formal/Z3CHCInterface.h +++ b/libsmtutil/Z3CHCInterface.h @@ -21,8 +21,8 @@ #pragma once -#include -#include +#include +#include namespace solidity::frontend::smt { diff --git a/libsolidity/formal/Z3Interface.cpp b/libsmtutil/Z3Interface.cpp similarity index 99% rename from libsolidity/formal/Z3Interface.cpp rename to libsmtutil/Z3Interface.cpp index d49314b6c..4303c76ac 100644 --- a/libsolidity/formal/Z3Interface.cpp +++ b/libsmtutil/Z3Interface.cpp @@ -15,7 +15,7 @@ along with solidity. If not, see . */ -#include +#include #include #include diff --git a/libsolidity/formal/Z3Interface.h b/libsmtutil/Z3Interface.h similarity index 97% rename from libsolidity/formal/Z3Interface.h rename to libsmtutil/Z3Interface.h index 3791af4c5..282b87a09 100644 --- a/libsolidity/formal/Z3Interface.h +++ b/libsmtutil/Z3Interface.h @@ -17,7 +17,7 @@ #pragma once -#include +#include #include #include diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index 7b66e533e..8e930b6ab 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -94,22 +94,12 @@ set(sources formal/BMC.h formal/CHC.cpp formal/CHC.h - formal/CHCSmtLib2Interface.cpp - formal/CHCSmtLib2Interface.h - formal/CHCSolverInterface.h formal/EncodingContext.cpp formal/EncodingContext.h formal/ModelChecker.cpp formal/ModelChecker.h formal/SMTEncoder.cpp formal/SMTEncoder.h - formal/SMTLib2Interface.cpp - formal/SMTLib2Interface.h - formal/SMTPortfolio.cpp - formal/SMTPortfolio.h - formal/SolverInterface.h - formal/Sorts.cpp - formal/Sorts.h formal/SSAVariable.cpp formal/SSAVariable.h formal/SymbolicState.cpp @@ -144,36 +134,6 @@ set(sources parsing/Token.h ) -find_package(Z3 4.6.0) -if (${Z3_FOUND}) - add_definitions(-DHAVE_Z3) - message("Z3 SMT solver found. This enables optional SMT checking with Z3.") - set(z3_SRCS formal/Z3Interface.cpp formal/Z3Interface.h formal/Z3CHCInterface.cpp formal/Z3CHCInterface.h) -else() - set(z3_SRCS) -endif() +add_library(solidity ${sources}) +target_link_libraries(solidity PUBLIC yul evmasm langutil smtutil solutil Boost::boost) -find_package(CVC4 QUIET) -if (${CVC4_FOUND}) - add_definitions(-DHAVE_CVC4) - message("CVC4 SMT solver found. This enables optional SMT checking with CVC4.") - set(cvc4_SRCS formal/CVC4Interface.cpp formal/CVC4Interface.h) -else() - set(cvc4_SRCS) -endif() - -if (NOT (${Z3_FOUND} OR ${CVC4_FOUND})) - message("No SMT solver found (or it has been forcefully disabled). Optional SMT checking will not be available.\ - \nPlease install Z3 or CVC4 or remove the option disabling them (USE_Z3, USE_CVC4).") -endif() - -add_library(solidity ${sources} ${z3_SRCS} ${cvc4_SRCS}) -target_link_libraries(solidity PUBLIC yul evmasm langutil solutil Boost::boost) - -if (${Z3_FOUND}) - target_link_libraries(solidity PUBLIC z3::libz3) -endif() - -if (${CVC4_FOUND}) - target_link_libraries(solidity PUBLIC CVC4::CVC4) -endif() diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 952eb1c50..7c2bc4818 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -17,10 +17,11 @@ #include -#include #include #include +#include + using namespace std; using namespace solidity; using namespace solidity::util; diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h index 8b30f073d..16ef665c0 100644 --- a/libsolidity/formal/BMC.h +++ b/libsolidity/formal/BMC.h @@ -30,9 +30,10 @@ #include #include -#include #include + +#include #include #include diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index f30959972..9cc01e26e 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -17,16 +17,15 @@ #include -#include - #ifdef HAVE_Z3 -#include +#include #endif #include #include +#include #include using namespace std; diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 87f902732..9315da70f 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -32,10 +32,10 @@ #include -#include - #include +#include + #include namespace solidity::frontend diff --git a/libsolidity/formal/EncodingContext.h b/libsolidity/formal/EncodingContext.h index d62de055d..e8cf48ed0 100644 --- a/libsolidity/formal/EncodingContext.h +++ b/libsolidity/formal/EncodingContext.h @@ -17,10 +17,11 @@ #pragma once -#include #include #include +#include + #include #include diff --git a/libsolidity/formal/ModelChecker.h b/libsolidity/formal/ModelChecker.h index 546f2df86..663bae869 100644 --- a/libsolidity/formal/ModelChecker.h +++ b/libsolidity/formal/ModelChecker.h @@ -25,9 +25,10 @@ #include #include #include -#include #include + +#include #include namespace solidity::langutil diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 44bec4d85..7a62199b2 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -18,10 +18,11 @@ #include #include -#include #include #include +#include + #include #include diff --git a/libsolidity/formal/SymbolicState.h b/libsolidity/formal/SymbolicState.h index 380bfda51..087ea9985 100644 --- a/libsolidity/formal/SymbolicState.h +++ b/libsolidity/formal/SymbolicState.h @@ -17,10 +17,11 @@ #pragma once -#include -#include #include +#include +#include + namespace solidity::frontend::smt { diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h index 3f5379d9b..46d3520cf 100644 --- a/libsolidity/formal/SymbolicVariables.h +++ b/libsolidity/formal/SymbolicVariables.h @@ -17,10 +17,11 @@ #pragma once -#include #include #include #include + +#include #include namespace solidity::frontend::smt diff --git a/libsolidity/interface/CompilerStack.h b/libsolidity/interface/CompilerStack.h index 96dbc4f04..fbd32b382 100644 --- a/libsolidity/interface/CompilerStack.h +++ b/libsolidity/interface/CompilerStack.h @@ -27,7 +27,8 @@ #include #include #include -#include + +#include #include #include diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 1834d3b30..6c6d12c1e 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -188,7 +188,7 @@ add_executable(soltest ${sources} ${libsolidity_util_sources} ${yul_phaser_sources} ) -target_link_libraries(soltest PRIVATE libsolc yul solidity yulInterpreter evmasm solutil Boost::boost Boost::filesystem Boost::program_options Boost::unit_test_framework evmc) +target_link_libraries(soltest PRIVATE libsolc yul solidity yulInterpreter evmasm smtutil solutil Boost::boost Boost::filesystem Boost::program_options Boost::unit_test_framework evmc) # Special compilation flag for Visual Studio (version 2019 at least affected) diff --git a/test/libsolidity/SMTCheckerTest.h b/test/libsolidity/SMTCheckerTest.h index ad38af25c..674564f57 100644 --- a/test/libsolidity/SMTCheckerTest.h +++ b/test/libsolidity/SMTCheckerTest.h @@ -19,7 +19,7 @@ #include -#include +#include #include From 802d66244d3ce4f2be9ee7cbcadbd611f4da1c38 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 19 May 2020 12:23:01 +0200 Subject: [PATCH 2/6] Do not link unnecessarily --- libsmtutil/CMakeLists.txt | 2 +- test/CMakeLists.txt | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/libsmtutil/CMakeLists.txt b/libsmtutil/CMakeLists.txt index d5df3633f..e46b80df6 100644 --- a/libsmtutil/CMakeLists.txt +++ b/libsmtutil/CMakeLists.txt @@ -23,7 +23,7 @@ else() endif() add_library(smtutil ${sources} ${z3_SRCS} ${cvc4_SRCS}) -target_link_libraries(smtutil PUBLIC langutil solutil Boost::boost) +target_link_libraries(smtutil PUBLIC solutil Boost::boost) if (${Z3_FOUND}) target_link_libraries(smtutil PUBLIC z3::libz3) diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 6c6d12c1e..06a082e66 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -188,7 +188,7 @@ add_executable(soltest ${sources} ${libsolidity_util_sources} ${yul_phaser_sources} ) -target_link_libraries(soltest PRIVATE libsolc yul solidity yulInterpreter evmasm smtutil solutil Boost::boost Boost::filesystem Boost::program_options Boost::unit_test_framework evmc) +target_link_libraries(soltest PRIVATE libsolc yul solidity smtutil solutil Boost::boost yulInterpreter evmasm Boost::filesystem Boost::program_options Boost::unit_test_framework evmc) # Special compilation flag for Visual Studio (version 2019 at least affected) From 45eba274242b386a37e4809636d678fca73bac52 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 19 May 2020 14:14:46 +0200 Subject: [PATCH 3/6] Rename namespace --- libsmtutil/CHCSmtLib2Interface.cpp | 12 +- libsmtutil/CHCSmtLib2Interface.h | 6 +- libsmtutil/CHCSolverInterface.h | 2 +- libsmtutil/CVC4Interface.cpp | 2 +- libsmtutil/CVC4Interface.h | 6 +- libsmtutil/SMTLib2Interface.cpp | 12 +- libsmtutil/SMTLib2Interface.h | 14 +- libsmtutil/SMTPortfolio.cpp | 16 +-- libsmtutil/SMTPortfolio.h | 12 +- libsmtutil/SolverInterface.h | 5 +- libsmtutil/Sorts.cpp | 2 +- libsmtutil/Sorts.h | 2 +- libsmtutil/Z3CHCInterface.cpp | 2 +- libsmtutil/Z3CHCInterface.h | 2 +- libsmtutil/Z3Interface.cpp | 4 +- libsmtutil/Z3Interface.h | 6 +- libsolidity/formal/BMC.cpp | 90 ++++++------ libsolidity/formal/BMC.h | 40 +++--- libsolidity/formal/CHC.cpp | 175 ++++++++++++----------- libsolidity/formal/CHC.h | 76 +++++----- libsolidity/formal/EncodingContext.cpp | 8 +- libsolidity/formal/EncodingContext.h | 16 +-- libsolidity/formal/ModelChecker.cpp | 6 +- libsolidity/formal/ModelChecker.h | 4 +- libsolidity/formal/SMTEncoder.cpp | 112 +++++++-------- libsolidity/formal/SMTEncoder.h | 48 +++---- libsolidity/formal/SymbolicState.cpp | 17 +-- libsolidity/formal/SymbolicState.h | 12 +- libsolidity/formal/SymbolicTypes.cpp | 29 ++-- libsolidity/formal/SymbolicTypes.h | 22 +-- libsolidity/formal/SymbolicVariables.cpp | 43 +++--- libsolidity/formal/SymbolicVariables.h | 62 ++++---- libsolidity/interface/CompilerStack.cpp | 6 +- libsolidity/interface/CompilerStack.h | 4 +- test/libsolidity/SMTCheckerTest.cpp | 8 +- test/libsolidity/SMTCheckerTest.h | 2 +- 36 files changed, 444 insertions(+), 441 deletions(-) diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp index d5895fc69..960e75ead 100644 --- a/libsmtutil/CHCSmtLib2Interface.cpp +++ b/libsmtutil/CHCSmtLib2Interface.cpp @@ -32,7 +32,7 @@ using namespace std; using namespace solidity; using namespace solidity::util; using namespace solidity::frontend; -using namespace solidity::frontend::smt; +using namespace solidity::smtutil; CHCSmtLib2Interface::CHCSmtLib2Interface( map const& _queryResponses, @@ -51,10 +51,10 @@ void CHCSmtLib2Interface::reset() m_variables.clear(); } -void CHCSmtLib2Interface::registerRelation(smt::Expression const& _expr) +void CHCSmtLib2Interface::registerRelation(Expression const& _expr) { solAssert(_expr.sort, ""); - solAssert(_expr.sort->kind == smt::Kind::Function, ""); + solAssert(_expr.sort->kind == Kind::Function, ""); if (!m_variables.count(_expr.name)) { auto fSort = dynamic_pointer_cast(_expr.sort); @@ -71,7 +71,7 @@ void CHCSmtLib2Interface::registerRelation(smt::Expression const& _expr) } } -void CHCSmtLib2Interface::addRule(smt::Expression const& _expr, std::string const& _name) +void CHCSmtLib2Interface::addRule(Expression const& _expr, std::string const& _name) { write( "(rule (! " + @@ -82,7 +82,7 @@ void CHCSmtLib2Interface::addRule(smt::Expression const& _expr, std::string cons ); } -pair> CHCSmtLib2Interface::query(smt::Expression const& _block) +pair> CHCSmtLib2Interface::query(Expression const& _block) { string accumulated{}; swap(m_accumulatedOutput, accumulated); @@ -125,7 +125,7 @@ void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const void CHCSmtLib2Interface::declareFunction(string const& _name, SortPointer const& _sort) { solAssert(_sort, ""); - solAssert(_sort->kind == smt::Kind::Function, ""); + solAssert(_sort->kind == Kind::Function, ""); // TODO Use domain and codomain as key as well if (!m_variables.count(_name)) { diff --git a/libsmtutil/CHCSmtLib2Interface.h b/libsmtutil/CHCSmtLib2Interface.h index 9fd1489a4..8ec3f8dd2 100644 --- a/libsmtutil/CHCSmtLib2Interface.h +++ b/libsmtutil/CHCSmtLib2Interface.h @@ -25,7 +25,7 @@ #include -namespace solidity::frontend::smt +namespace solidity::smtutil { class CHCSmtLib2Interface: public CHCSolverInterface @@ -33,7 +33,7 @@ class CHCSmtLib2Interface: public CHCSolverInterface public: explicit CHCSmtLib2Interface( std::map const& _queryResponses, - ReadCallback::Callback const& _smtCallback + frontend::ReadCallback::Callback const& _smtCallback ); void reset(); @@ -67,7 +67,7 @@ private: std::map const& m_queryResponses; std::vector m_unhandledQueries; - ReadCallback::Callback m_smtCallback; + frontend::ReadCallback::Callback m_smtCallback; }; } diff --git a/libsmtutil/CHCSolverInterface.h b/libsmtutil/CHCSolverInterface.h index 588e42ce1..f2d14cbcf 100644 --- a/libsmtutil/CHCSolverInterface.h +++ b/libsmtutil/CHCSolverInterface.h @@ -23,7 +23,7 @@ #include -namespace solidity::frontend::smt +namespace solidity::smtutil { class CHCSolverInterface diff --git a/libsmtutil/CVC4Interface.cpp b/libsmtutil/CVC4Interface.cpp index 71ab81f51..3a678429a 100644 --- a/libsmtutil/CVC4Interface.cpp +++ b/libsmtutil/CVC4Interface.cpp @@ -23,7 +23,7 @@ using namespace std; using namespace solidity; using namespace solidity::util; -using namespace solidity::frontend::smt; +using namespace solidity::smtutil; CVC4Interface::CVC4Interface(): m_solver(&m_context) diff --git a/libsmtutil/CVC4Interface.h b/libsmtutil/CVC4Interface.h index 2399dc453..990590351 100644 --- a/libsmtutil/CVC4Interface.h +++ b/libsmtutil/CVC4Interface.h @@ -33,7 +33,7 @@ #undef _GLIBCXX_PERMIT_BACKWARD_HASH #endif -namespace solidity::frontend::smt +namespace solidity::smtutil { class CVC4Interface: public SolverInterface, public boost::noncopyable @@ -53,8 +53,8 @@ public: private: CVC4::Expr toCVC4Expr(Expression const& _expr); - CVC4::Type cvc4Sort(smt::Sort const& _sort); - std::vector cvc4Sort(std::vector const& _sorts); + CVC4::Type cvc4Sort(Sort const& _sort); + std::vector cvc4Sort(std::vector const& _sorts); CVC4::ExprManager m_context; CVC4::SmtEngine m_solver; diff --git a/libsmtutil/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp index 081d87f61..a9083a291 100644 --- a/libsmtutil/SMTLib2Interface.cpp +++ b/libsmtutil/SMTLib2Interface.cpp @@ -34,7 +34,7 @@ using namespace std; using namespace solidity; using namespace solidity::util; using namespace solidity::frontend; -using namespace solidity::frontend::smt; +using namespace solidity::smtutil; SMTLib2Interface::SMTLib2Interface( map const& _queryResponses, @@ -82,7 +82,7 @@ void SMTLib2Interface::declareVariable(string const& _name, SortPointer const& _ void SMTLib2Interface::declareFunction(string const& _name, SortPointer const& _sort) { solAssert(_sort, ""); - solAssert(_sort->kind == smt::Kind::Function, ""); + solAssert(_sort->kind == Kind::Function, ""); // TODO Use domain and codomain as key as well if (!m_variables.count(_name)) { @@ -102,12 +102,12 @@ void SMTLib2Interface::declareFunction(string const& _name, SortPointer const& _ } } -void SMTLib2Interface::addAssertion(smt::Expression const& _expr) +void SMTLib2Interface::addAssertion(Expression const& _expr) { write("(assert " + toSExpr(_expr) + ")"); } -pair> SMTLib2Interface::check(vector const& _expressionsToEvaluate) +pair> SMTLib2Interface::check(vector const& _expressionsToEvaluate) { string response = querySolver( boost::algorithm::join(m_accumulatedOutput, "\n") + @@ -131,7 +131,7 @@ pair> SMTLib2Interface::check(vector const& _expressionsToEvaluate) +string SMTLib2Interface::checkSatAndGetValuesCommand(vector const& _expressionsToEvaluate) { string command; if (_expressionsToEvaluate.empty()) diff --git a/libsmtutil/SMTLib2Interface.h b/libsmtutil/SMTLib2Interface.h index 1acbcde2c..6d97adac2 100644 --- a/libsmtutil/SMTLib2Interface.h +++ b/libsmtutil/SMTLib2Interface.h @@ -31,7 +31,7 @@ #include #include -namespace solidity::frontend::smt +namespace solidity::smtutil { class SMTLib2Interface: public SolverInterface, public boost::noncopyable @@ -39,7 +39,7 @@ class SMTLib2Interface: public SolverInterface, public boost::noncopyable public: explicit SMTLib2Interface( std::map const& _queryResponses, - ReadCallback::Callback _smtCallback + frontend::ReadCallback::Callback _smtCallback ); void reset() override; @@ -49,13 +49,13 @@ public: void declareVariable(std::string const&, SortPointer const&) override; - void addAssertion(smt::Expression const& _expr) override; - std::pair> check(std::vector const& _expressionsToEvaluate) override; + void addAssertion(Expression const& _expr) override; + std::pair> check(std::vector const& _expressionsToEvaluate) override; std::vector unhandledQueries() override { return m_unhandledQueries; } // Used by CHCSmtLib2Interface - std::string toSExpr(smt::Expression const& _expr); + std::string toSExpr(Expression const& _expr); std::string toSmtLibSort(Sort const& _sort); std::string toSmtLibSort(std::vector const& _sort); @@ -66,7 +66,7 @@ private: void write(std::string _data); - std::string checkSatAndGetValuesCommand(std::vector const& _expressionsToEvaluate); + std::string checkSatAndGetValuesCommand(std::vector const& _expressionsToEvaluate); std::vector parseValues(std::string::const_iterator _start, std::string::const_iterator _end); /// Communicates with the solver via the callback. Throws SMTSolverError on error. @@ -79,7 +79,7 @@ private: std::map const& m_queryResponses; std::vector m_unhandledQueries; - ReadCallback::Callback m_smtCallback; + frontend::ReadCallback::Callback m_smtCallback; }; } diff --git a/libsmtutil/SMTPortfolio.cpp b/libsmtutil/SMTPortfolio.cpp index 67cb3803c..dc7e69fa1 100644 --- a/libsmtutil/SMTPortfolio.cpp +++ b/libsmtutil/SMTPortfolio.cpp @@ -29,22 +29,22 @@ using namespace std; using namespace solidity; using namespace solidity::util; using namespace solidity::frontend; -using namespace solidity::frontend::smt; +using namespace solidity::smtutil; SMTPortfolio::SMTPortfolio( map const& _smtlib2Responses, - ReadCallback::Callback const& _smtCallback, + frontend::ReadCallback::Callback const& _smtCallback, [[maybe_unused]] SMTSolverChoice _enabledSolvers ) { - m_solvers.emplace_back(make_unique(_smtlib2Responses, _smtCallback)); + m_solvers.emplace_back(make_unique(_smtlib2Responses, _smtCallback)); #ifdef HAVE_Z3 if (_enabledSolvers.z3) - m_solvers.emplace_back(make_unique()); + m_solvers.emplace_back(make_unique()); #endif #ifdef HAVE_CVC4 if (_enabledSolvers.cvc4) - m_solvers.emplace_back(make_unique()); + m_solvers.emplace_back(make_unique()); #endif } @@ -73,7 +73,7 @@ void SMTPortfolio::declareVariable(string const& _name, SortPointer const& _sort s->declareVariable(_name, _sort); } -void SMTPortfolio::addAssertion(smt::Expression const& _expr) +void SMTPortfolio::addAssertion(Expression const& _expr) { for (auto const& s: m_solvers) s->addAssertion(_expr); @@ -109,7 +109,7 @@ void SMTPortfolio::addAssertion(smt::Expression const& _expr) * * If all solvers return ERROR, the result is ERROR. */ -pair> SMTPortfolio::check(vector const& _expressionsToEvaluate) +pair> SMTPortfolio::check(vector const& _expressionsToEvaluate) { CheckResult lastResult = CheckResult::ERROR; vector finalValues; @@ -142,7 +142,7 @@ vector SMTPortfolio::unhandledQueries() // This code assumes that the constructor guarantees that // SmtLib2Interface is in position 0. solAssert(!m_solvers.empty(), ""); - solAssert(dynamic_cast(m_solvers.front().get()), ""); + solAssert(dynamic_cast(m_solvers.front().get()), ""); return m_solvers.front()->unhandledQueries(); } diff --git a/libsmtutil/SMTPortfolio.h b/libsmtutil/SMTPortfolio.h index 1ffce37ee..0399ac033 100644 --- a/libsmtutil/SMTPortfolio.h +++ b/libsmtutil/SMTPortfolio.h @@ -26,7 +26,7 @@ #include #include -namespace solidity::frontend::smt +namespace solidity::smtutil { /** @@ -40,7 +40,7 @@ class SMTPortfolio: public SolverInterface, public boost::noncopyable public: SMTPortfolio( std::map const& _smtlib2Responses, - ReadCallback::Callback const& _smtCallback, + frontend::ReadCallback::Callback const& _smtCallback, SMTSolverChoice _enabledSolvers ); @@ -51,18 +51,18 @@ public: void declareVariable(std::string const&, SortPointer const&) override; - void addAssertion(smt::Expression const& _expr) override; + void addAssertion(Expression const& _expr) override; - std::pair> check(std::vector const& _expressionsToEvaluate) override; + std::pair> check(std::vector const& _expressionsToEvaluate) override; std::vector unhandledQueries() override; unsigned solvers() override { return m_solvers.size(); } private: static bool solverAnswered(CheckResult result); - std::vector> m_solvers; + std::vector> m_solvers; - std::vector m_assertions; + std::vector m_assertions; }; } diff --git a/libsmtutil/SolverInterface.h b/libsmtutil/SolverInterface.h index 078eaef73..260dcc7a7 100644 --- a/libsmtutil/SolverInterface.h +++ b/libsmtutil/SolverInterface.h @@ -20,7 +20,6 @@ #include #include -#include #include #include #include @@ -32,7 +31,7 @@ #include #include -namespace solidity::frontend::smt +namespace solidity::smtutil { struct SMTSolverChoice @@ -56,7 +55,7 @@ enum class CheckResult }; // Forward declaration. -SortPointer smtSort(Type const& _type); +SortPointer smtSort(frontend::Type const& _type); /// C++ representation of an SMTLIB2 expression. class Expression diff --git a/libsmtutil/Sorts.cpp b/libsmtutil/Sorts.cpp index dba0dc4b7..7a45a1746 100644 --- a/libsmtutil/Sorts.cpp +++ b/libsmtutil/Sorts.cpp @@ -20,7 +20,7 @@ using namespace std; -namespace solidity::frontend::smt +namespace solidity::smtutil { shared_ptr const SortProvider::boolSort{make_shared(Kind::Bool)}; diff --git a/libsmtutil/Sorts.h b/libsmtutil/Sorts.h index 2acd46975..903db1907 100644 --- a/libsmtutil/Sorts.h +++ b/libsmtutil/Sorts.h @@ -24,7 +24,7 @@ #include #include -namespace solidity::frontend::smt +namespace solidity::smtutil { enum class Kind diff --git a/libsmtutil/Z3CHCInterface.cpp b/libsmtutil/Z3CHCInterface.cpp index 3be40d396..8346ea647 100644 --- a/libsmtutil/Z3CHCInterface.cpp +++ b/libsmtutil/Z3CHCInterface.cpp @@ -22,7 +22,7 @@ using namespace std; using namespace solidity; -using namespace solidity::frontend::smt; +using namespace solidity::smtutil; Z3CHCInterface::Z3CHCInterface(): m_z3Interface(make_unique()), diff --git a/libsmtutil/Z3CHCInterface.h b/libsmtutil/Z3CHCInterface.h index bc0e6cf92..f36ee2caa 100644 --- a/libsmtutil/Z3CHCInterface.h +++ b/libsmtutil/Z3CHCInterface.h @@ -24,7 +24,7 @@ #include #include -namespace solidity::frontend::smt +namespace solidity::smtutil { class Z3CHCInterface: public CHCSolverInterface diff --git a/libsmtutil/Z3Interface.cpp b/libsmtutil/Z3Interface.cpp index 4303c76ac..3c4ea16ed 100644 --- a/libsmtutil/Z3Interface.cpp +++ b/libsmtutil/Z3Interface.cpp @@ -21,7 +21,7 @@ #include using namespace std; -using namespace solidity::frontend::smt; +using namespace solidity::smtutil; Z3Interface::Z3Interface(): m_solver(m_context) @@ -61,7 +61,7 @@ void Z3Interface::declareVariable(string const& _name, SortPointer const& _sort) void Z3Interface::declareFunction(string const& _name, Sort const& _sort) { - solAssert(_sort.kind == smt::Kind::Function, ""); + solAssert(_sort.kind == Kind::Function, ""); FunctionSort fSort = dynamic_cast(_sort); if (m_functions.count(_name)) m_functions.at(_name) = m_context.function(_name.c_str(), z3Sort(fSort.domain), z3Sort(*fSort.codomain)); diff --git a/libsmtutil/Z3Interface.h b/libsmtutil/Z3Interface.h index 282b87a09..1662323bc 100644 --- a/libsmtutil/Z3Interface.h +++ b/libsmtutil/Z3Interface.h @@ -21,7 +21,7 @@ #include #include -namespace solidity::frontend::smt +namespace solidity::smtutil { class Z3Interface: public SolverInterface, public boost::noncopyable @@ -55,8 +55,8 @@ public: private: void declareFunction(std::string const& _name, Sort const& _sort); - z3::sort z3Sort(smt::Sort const& _sort); - z3::sort_vector z3Sort(std::vector const& _sorts); + z3::sort z3Sort(Sort const& _sort); + z3::sort_vector z3Sort(std::vector const& _sorts); z3::context m_context; z3::solver m_solver; diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 7c2bc4818..8ec6b3564 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -33,10 +33,10 @@ BMC::BMC( ErrorReporter& _errorReporter, map const& _smtlib2Responses, ReadCallback::Callback const& _smtCallback, - smt::SMTSolverChoice _enabledSolvers + smtutil::SMTSolverChoice _enabledSolvers ): SMTEncoder(_context), - m_interface(make_unique(_smtlib2Responses, _smtCallback, _enabledSolvers)), + m_interface(make_unique(_smtlib2Responses, _smtCallback, _enabledSolvers)), m_outerErrorReporter(_errorReporter) { #if defined (HAVE_Z3) || defined (HAVE_CVC4) @@ -133,7 +133,7 @@ void BMC::endVisit(ContractDefinition const& _contract) { inlineConstructorHierarchy(_contract); /// Check targets created by state variable initialization. - smt::Expression constraints = m_context.assertions(); + smtutil::Expression constraints = m_context.assertions(); checkVerificationTargets(constraints); m_verificationTargets.clear(); } @@ -167,7 +167,7 @@ void BMC::endVisit(FunctionDefinition const& _function) { if (isRootFunction()) { - smt::Expression constraints = m_context.assertions(); + smtutil::Expression constraints = m_context.assertions(); checkVerificationTargets(constraints); m_verificationTargets.clear(); } @@ -294,7 +294,7 @@ bool BMC::visit(ForStatement const& _node) if (_node.condition()) _node.condition()->accept(*this); - auto forCondition = _node.condition() ? expr(*_node.condition()) : smt::Expression(true); + auto forCondition = _node.condition() ? expr(*_node.condition()) : smtutil::Expression(true); mergeVariables(touchedVars, forCondition, indicesAfterLoop, copyVariableIndices()); m_loopExecutionHappened = true; @@ -381,7 +381,7 @@ void BMC::endVisit(FunctionCall const& _funCall) SMTEncoder::endVisit(_funCall); auto value = _funCall.arguments().front(); solAssert(value, ""); - smt::Expression thisBalance = m_context.state().balance(); + smtutil::Expression thisBalance = m_context.state().balance(); addVerificationTarget( VerificationTarget::Type::Balance, @@ -453,7 +453,7 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall) void BMC::abstractFunctionCall(FunctionCall const& _funCall) { - vector smtArguments; + vector smtArguments; for (auto const& arg: _funCall.arguments()) smtArguments.push_back(expr(*arg)); defineExpr(_funCall, (*m_context.expression(_funCall.expression()))(smtArguments)); @@ -480,10 +480,10 @@ void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall) } } -pair BMC::arithmeticOperation( +pair BMC::arithmeticOperation( Token _op, - smt::Expression const& _left, - smt::Expression const& _right, + smtutil::Expression const& _left, + smtutil::Expression const& _right, TypePointer const& _commonType, Expression const& _expression ) @@ -516,9 +516,9 @@ void BMC::reset() m_loopExecutionHappened = false; } -pair, vector> BMC::modelExpressions() +pair, vector> BMC::modelExpressions() { - vector expressionsToEvaluate; + vector expressionsToEvaluate; vector expressionNames; for (auto const& var: m_context.variables()) if (var.first->type()->isValueType()) @@ -531,7 +531,7 @@ pair, vector> BMC::modelExpressions() auto const& type = var.second->type(); if ( type->isValueType() && - smt::smtKind(type->category()) != smt::Kind::Function + smt::smtKind(type->category()) != smtutil::Kind::Function ) { expressionsToEvaluate.emplace_back(var.second->currentValue()); @@ -550,13 +550,13 @@ pair, vector> BMC::modelExpressions() /// Verification targets. -void BMC::checkVerificationTargets(smt::Expression const& _constraints) +void BMC::checkVerificationTargets(smtutil::Expression const& _constraints) { for (auto& target: m_verificationTargets) checkVerificationTarget(target, _constraints); } -void BMC::checkVerificationTarget(BMCVerificationTarget& _target, smt::Expression const& _constraints) +void BMC::checkVerificationTarget(BMCVerificationTarget& _target, smtutil::Expression const& _constraints) { switch (_target.type) { @@ -597,7 +597,7 @@ void BMC::checkConstantCondition(BMCVerificationTarget& _target) ); } -void BMC::checkUnderflow(BMCVerificationTarget& _target, smt::Expression const& _constraints) +void BMC::checkUnderflow(BMCVerificationTarget& _target, smtutil::Expression const& _constraints) { solAssert( _target.type == VerificationTarget::Type::Underflow || @@ -619,7 +619,7 @@ void BMC::checkUnderflow(BMCVerificationTarget& _target, smt::Expression const& ); } -void BMC::checkOverflow(BMCVerificationTarget& _target, smt::Expression const& _constraints) +void BMC::checkOverflow(BMCVerificationTarget& _target, smtutil::Expression const& _constraints) { solAssert( _target.type == VerificationTarget::Type::Overflow || @@ -689,7 +689,7 @@ void BMC::checkAssert(BMCVerificationTarget& _target) void BMC::addVerificationTarget( VerificationTarget::Type _type, - smt::Expression const& _value, + smtutil::Expression const& _value, Expression const* _expression ) { @@ -712,21 +712,21 @@ void BMC::addVerificationTarget( /// Solving. void BMC::checkCondition( - smt::Expression _condition, + smtutil::Expression _condition, vector const& _callStack, - pair, vector> const& _modelExpressions, + pair, vector> const& _modelExpressions, SourceLocation const& _location, ErrorId _errorHappens, ErrorId _errorMightHappen, string const& _description, string const& _additionalValueName, - smt::Expression const* _additionalValue + smtutil::Expression const* _additionalValue ) { m_interface->push(); m_interface->addAssertion(_condition); - vector expressionsToEvaluate; + vector expressionsToEvaluate; vector expressionNames; tie(expressionsToEvaluate, expressionNames) = _modelExpressions; if (_callStack.size()) @@ -735,7 +735,7 @@ void BMC::checkCondition( expressionsToEvaluate.emplace_back(*_additionalValue); expressionNames.push_back(_additionalValueName); } - smt::CheckResult result; + smtutil::CheckResult result; vector values; tie(result, values) = checkSatisfiableAndGenerateModel(expressionsToEvaluate); @@ -756,7 +756,7 @@ void BMC::checkCondition( switch (result) { - case smt::CheckResult::SATISFIABLE: + case smtutil::CheckResult::SATISFIABLE: { std::ostringstream message; message << _description << " happens here"; @@ -788,15 +788,15 @@ void BMC::checkCondition( } break; } - case smt::CheckResult::UNSATISFIABLE: + case smtutil::CheckResult::UNSATISFIABLE: break; - case smt::CheckResult::UNKNOWN: + case smtutil::CheckResult::UNKNOWN: m_errorReporter.warning(_errorMightHappen, _location, _description + " might happen here.", secondaryLocation); break; - case smt::CheckResult::CONFLICTING: + case smtutil::CheckResult::CONFLICTING: m_errorReporter.warning(1584_error, _location, "At least two SMT solvers provided conflicting answers. Results might not be sound."); break; - case smt::CheckResult::ERROR: + case smtutil::CheckResult::ERROR: m_errorReporter.warning(1823_error, _location, "Error trying to invoke SMT solver."); break; } @@ -806,8 +806,8 @@ void BMC::checkCondition( void BMC::checkBooleanNotConstant( Expression const& _condition, - smt::Expression const& _constraints, - smt::Expression const& _value, + smtutil::Expression const& _constraints, + smtutil::Expression const& _value, vector const& _callStack ) { @@ -825,32 +825,32 @@ void BMC::checkBooleanNotConstant( auto negatedResult = checkSatisfiable(); m_interface->pop(); - if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR) + if (positiveResult == smtutil::CheckResult::ERROR || negatedResult == smtutil::CheckResult::ERROR) m_errorReporter.warning(8592_error, _condition.location(), "Error trying to invoke SMT solver."); - else if (positiveResult == smt::CheckResult::CONFLICTING || negatedResult == smt::CheckResult::CONFLICTING) + else if (positiveResult == smtutil::CheckResult::CONFLICTING || negatedResult == smtutil::CheckResult::CONFLICTING) m_errorReporter.warning(3356_error, _condition.location(), "At least two SMT solvers provided conflicting answers. Results might not be sound."); - else if (positiveResult == smt::CheckResult::SATISFIABLE && negatedResult == smt::CheckResult::SATISFIABLE) + else if (positiveResult == smtutil::CheckResult::SATISFIABLE && negatedResult == smtutil::CheckResult::SATISFIABLE) { // everything fine. } - else if (positiveResult == smt::CheckResult::UNKNOWN || negatedResult == smt::CheckResult::UNKNOWN) + else if (positiveResult == smtutil::CheckResult::UNKNOWN || negatedResult == smtutil::CheckResult::UNKNOWN) { // can't do anything. } - else if (positiveResult == smt::CheckResult::UNSATISFIABLE && negatedResult == smt::CheckResult::UNSATISFIABLE) + else if (positiveResult == smtutil::CheckResult::UNSATISFIABLE && negatedResult == smtutil::CheckResult::UNSATISFIABLE) m_errorReporter.warning(2512_error, _condition.location(), "Condition unreachable.", SMTEncoder::callStackMessage(_callStack)); else { string description; - if (positiveResult == smt::CheckResult::SATISFIABLE) + if (positiveResult == smtutil::CheckResult::SATISFIABLE) { - solAssert(negatedResult == smt::CheckResult::UNSATISFIABLE, ""); + solAssert(negatedResult == smtutil::CheckResult::UNSATISFIABLE, ""); description = "Condition is always true."; } else { - solAssert(positiveResult == smt::CheckResult::UNSATISFIABLE, ""); - solAssert(negatedResult == smt::CheckResult::SATISFIABLE, ""); + solAssert(positiveResult == smtutil::CheckResult::UNSATISFIABLE, ""); + solAssert(negatedResult == smtutil::CheckResult::SATISFIABLE, ""); description = "Condition is always false."; } m_errorReporter.warning( @@ -862,22 +862,22 @@ void BMC::checkBooleanNotConstant( } } -pair> -BMC::checkSatisfiableAndGenerateModel(vector const& _expressionsToEvaluate) +pair> +BMC::checkSatisfiableAndGenerateModel(vector const& _expressionsToEvaluate) { - smt::CheckResult result; + smtutil::CheckResult result; vector values; try { tie(result, values) = m_interface->check(_expressionsToEvaluate); } - catch (smt::SolverError const& _e) + catch (smtutil::SolverError const& _e) { string description("Error querying SMT solver"); if (_e.comment()) description += ": " + *_e.comment(); m_errorReporter.warning(8140_error, description); - result = smt::CheckResult::ERROR; + result = smtutil::CheckResult::ERROR; } for (string& value: values) @@ -893,7 +893,7 @@ BMC::checkSatisfiableAndGenerateModel(vector const& _expression return make_pair(result, values); } -smt::CheckResult BMC::checkSatisfiable() +smtutil::CheckResult BMC::checkSatisfiable() { return checkSatisfiableAndGenerateModel({}).first; } diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h index 16ef665c0..4f0a98023 100644 --- a/libsolidity/formal/BMC.h +++ b/libsolidity/formal/BMC.h @@ -60,7 +60,7 @@ public: langutil::ErrorReporter& _errorReporter, std::map const& _smtlib2Responses, ReadCallback::Callback const& _smtCallback, - smt::SMTSolverChoice _enabledSolvers + smtutil::SMTSolverChoice _enabledSolvers ); void analyze(SourceUnit const& _sources, std::set _safeAssertions); @@ -103,10 +103,10 @@ private: void internalOrExternalFunctionCall(FunctionCall const& _funCall); /// Creates underflow/overflow verification targets. - std::pair arithmeticOperation( + std::pair arithmeticOperation( Token _op, - smt::Expression const& _left, - smt::Expression const& _right, + smtutil::Expression const& _left, + smtutil::Expression const& _right, TypePointer const& _commonType, Expression const& _expression ) override; @@ -114,7 +114,7 @@ private: void resetStorageReferences(); void reset(); - std::pair, std::vector> modelExpressions(); + std::pair, std::vector> modelExpressions(); //@} /// Verification targets. @@ -123,20 +123,20 @@ private: { Expression const* expression; std::vector callStack; - std::pair, std::vector> modelExpressions; + std::pair, std::vector> modelExpressions; }; - void checkVerificationTargets(smt::Expression const& _constraints); - void checkVerificationTarget(BMCVerificationTarget& _target, smt::Expression const& _constraints = smt::Expression(true)); + void checkVerificationTargets(smtutil::Expression const& _constraints); + void checkVerificationTarget(BMCVerificationTarget& _target, smtutil::Expression const& _constraints = smtutil::Expression(true)); void checkConstantCondition(BMCVerificationTarget& _target); - void checkUnderflow(BMCVerificationTarget& _target, smt::Expression const& _constraints); - void checkOverflow(BMCVerificationTarget& _target, smt::Expression const& _constraints); + void checkUnderflow(BMCVerificationTarget& _target, smtutil::Expression const& _constraints); + void checkOverflow(BMCVerificationTarget& _target, smtutil::Expression const& _constraints); void checkDivByZero(BMCVerificationTarget& _target); void checkBalance(BMCVerificationTarget& _target); void checkAssert(BMCVerificationTarget& _target); void addVerificationTarget( VerificationTarget::Type _type, - smt::Expression const& _value, + smtutil::Expression const& _value, Expression const* _expression ); //@} @@ -145,31 +145,31 @@ private: //@{ /// Check that a condition can be satisfied. void checkCondition( - smt::Expression _condition, + smtutil::Expression _condition, std::vector const& _callStack, - std::pair, std::vector> const& _modelExpressions, + std::pair, std::vector> const& _modelExpressions, langutil::SourceLocation const& _location, langutil::ErrorId _errorHappens, langutil::ErrorId _errorMightHappen, std::string const& _description, std::string const& _additionalValueName = "", - smt::Expression const* _additionalValue = nullptr + smtutil::Expression const* _additionalValue = nullptr ); /// Checks that a boolean condition is not constant. Do not warn if the expression /// is a literal constant. void checkBooleanNotConstant( Expression const& _condition, - smt::Expression const& _constraints, - smt::Expression const& _value, + smtutil::Expression const& _constraints, + smtutil::Expression const& _value, std::vector const& _callStack ); - std::pair> - checkSatisfiableAndGenerateModel(std::vector const& _expressionsToEvaluate); + std::pair> + checkSatisfiableAndGenerateModel(std::vector const& _expressionsToEvaluate); - smt::CheckResult checkSatisfiable(); + smtutil::CheckResult checkSatisfiable(); //@} - std::unique_ptr m_interface; + std::unique_ptr m_interface; /// Flags used for better warning messages. bool m_loopExecutionHappened = false; diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 9cc01e26e..fe63c198d 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -32,6 +32,7 @@ using namespace std; using namespace solidity; using namespace solidity::util; using namespace solidity::langutil; +using namespace solidity::smtutil; using namespace solidity::frontend; CHC::CHC( @@ -39,7 +40,7 @@ CHC::CHC( ErrorReporter& _errorReporter, map const& _smtlib2Responses, ReadCallback::Callback const& _smtCallback, - [[maybe_unused]] smt::SMTSolverChoice _enabledSolvers + [[maybe_unused]] smtutil::SMTSolverChoice _enabledSolvers ): SMTEncoder(_context), m_outerErrorReporter(_errorReporter), @@ -47,10 +48,10 @@ CHC::CHC( { #ifdef HAVE_Z3 if (_enabledSolvers.z3) - m_interface = make_unique(); + m_interface = make_unique(); #endif if (!m_interface) - m_interface = make_unique(_smtlib2Responses, _smtCallback); + m_interface = make_unique(_smtlib2Responses, _smtCallback); } void CHC::analyze(SourceUnit const& _source) @@ -62,14 +63,14 @@ void CHC::analyze(SourceUnit const& _source) usesZ3 = m_enabledSolvers.z3; if (usesZ3) { - auto z3Interface = dynamic_cast(m_interface.get()); + auto z3Interface = dynamic_cast(m_interface.get()); solAssert(z3Interface, ""); m_context.setSolver(z3Interface->z3Interface()); } #endif if (!usesZ3) { - auto smtlib2Interface = dynamic_cast(m_interface.get()); + auto smtlib2Interface = dynamic_cast(m_interface.get()); solAssert(smtlib2Interface, ""); m_context.setSolver(smtlib2Interface->smtlib2Interface()); } @@ -79,9 +80,9 @@ void CHC::analyze(SourceUnit const& _source) resetSourceAnalysis(); - auto genesisSort = make_shared( - vector(), - smt::SortProvider::boolSort + auto genesisSort = make_shared( + vector(), + smtutil::SortProvider::boolSort ); m_genesisPredicate = createSymbolicBlock(genesisSort, "genesis"); addRule(genesis(), "genesis"); @@ -107,7 +108,7 @@ void CHC::analyze(SourceUnit const& _source) auto [result, model] = query(error(), assertion->location()); // This should be fine but it's a bug in the old compiler (void)model; - if (result == smt::CheckResult::UNSATISFIABLE) + if (result == smtutil::CheckResult::UNSATISFIABLE) m_safeAssertions.insert(assertion); } } @@ -119,10 +120,10 @@ void CHC::analyze(SourceUnit const& _source) auto [result, model] = query(error(), scope->location()); // This should be fine but it's a bug in the old compiler (void)model; - if (result != smt::CheckResult::UNSATISFIABLE) + if (result != smtutil::CheckResult::UNSATISFIABLE) { string msg = "Empty array \"pop\" "; - if (result == smt::CheckResult::SATISFIABLE) + if (result == smtutil::CheckResult::SATISFIABLE) msg += "detected here."; else msg += "might happen here."; @@ -141,7 +142,7 @@ void CHC::analyze(SourceUnit const& _source) vector CHC::unhandledQueries() const { - if (auto smtlib2 = dynamic_cast(m_interface.get())) + if (auto smtlib2 = dynamic_cast(m_interface.get())) return smtlib2->unhandledQueries(); return {}; @@ -181,14 +182,14 @@ void CHC::endVisit(ContractDefinition const& _contract) else inlineConstructorHierarchy(_contract); - auto summary = predicate(*m_constructorSummaryPredicate, vector{m_error.currentValue()} + currentStateVariables()); + auto summary = predicate(*m_constructorSummaryPredicate, vector{m_error.currentValue()} + currentStateVariables()); connectBlocks(m_currentBlock, summary); clearIndices(m_currentContract, nullptr); - auto stateExprs = vector{m_error.currentValue()} + currentStateVariables(); + auto stateExprs = vector{m_error.currentValue()} + currentStateVariables(); setCurrentBlock(*m_constructorSummaryPredicate, &stateExprs); - addAssertVerificationTarget(m_currentContract, m_currentBlock, smt::Expression(true), m_error.currentValue()); + addAssertVerificationTarget(m_currentContract, m_currentBlock, smtutil::Expression(true), m_error.currentValue()); connectBlocks(m_currentBlock, interface(), m_error.currentValue() == 0); SMTEncoder::endVisit(_contract); @@ -264,10 +265,10 @@ void CHC::endVisit(FunctionDefinition const& _function) { string suffix = m_currentContract->name() + "_" + to_string(m_currentContract->id()); auto constructorExit = createSymbolicBlock(constructorSort(), "constructor_exit_" + suffix); - connectBlocks(m_currentBlock, predicate(*constructorExit, vector{m_error.currentValue()} + currentStateVariables())); + connectBlocks(m_currentBlock, predicate(*constructorExit, vector{m_error.currentValue()} + currentStateVariables())); clearIndices(m_currentContract, m_currentFunction); - auto stateExprs = vector{m_error.currentValue()} + currentStateVariables(); + auto stateExprs = vector{m_error.currentValue()} + currentStateVariables(); setCurrentBlock(*constructorExit, &stateExprs); } else @@ -416,7 +417,7 @@ bool CHC::visit(ForStatement const& _for) connectBlocks(m_currentBlock, predicate(*loopHeaderBlock)); setCurrentBlock(*loopHeaderBlock); - auto condition = smt::Expression(true); + auto condition = smtutil::Expression(true); if (auto forCondition = _for.condition()) { forCondition->accept(*this); @@ -655,7 +656,7 @@ bool CHC::shouldVisit(FunctionDefinition const& _function) const void CHC::setCurrentBlock( smt::SymbolicFunctionVariable const& _block, - vector const* _arguments + vector const* _arguments ) { if (m_context.solverStackHeigh() > 0) @@ -669,7 +670,7 @@ void CHC::setCurrentBlock( m_currentBlock = predicate(_block); } -set CHC::transactionAssertions(ASTNode const* _txRoot) +set CHC::transactionAssertions(ASTNode const* _txRoot) { set assertions; solidity::util::BreadthFirstSearch{{_txRoot}}.run([&](auto const* function, auto&& _addChild) { @@ -689,7 +690,7 @@ vector CHC::stateVariablesIncludingInheritedAndPriva ); } -vector CHC::stateSorts(ContractDefinition const& _contract) +vector CHC::stateSorts(ContractDefinition const& _contract) { return applyMap( stateVariablesIncludingInheritedAndPrivate(_contract), @@ -697,35 +698,35 @@ vector CHC::stateSorts(ContractDefinition const& _contract) ); } -smt::SortPointer CHC::constructorSort() +smtutil::SortPointer CHC::constructorSort() { - return make_shared( - vector{smt::SortProvider::intSort} + m_stateSorts, - smt::SortProvider::boolSort + return make_shared( + vector{smtutil::SortProvider::intSort} + m_stateSorts, + smtutil::SortProvider::boolSort ); } -smt::SortPointer CHC::interfaceSort() +smtutil::SortPointer CHC::interfaceSort() { - return make_shared( + return make_shared( m_stateSorts, - smt::SortProvider::boolSort + smtutil::SortProvider::boolSort ); } -smt::SortPointer CHC::interfaceSort(ContractDefinition const& _contract) +smtutil::SortPointer CHC::interfaceSort(ContractDefinition const& _contract) { - return make_shared( + return make_shared( stateSorts(_contract), - smt::SortProvider::boolSort + smtutil::SortProvider::boolSort ); } -smt::SortPointer CHC::arity0FunctionSort() +smtutil::SortPointer CHC::arity0FunctionSort() { - return make_shared( - vector(), - smt::SortProvider::boolSort + return make_shared( + vector(), + smtutil::SortProvider::boolSort ); } @@ -740,33 +741,33 @@ smt::SortPointer CHC::arity0FunctionSort() /// - Current input variables /// At the beginning of the function these must equal set 1 /// - 1 set of output variables -smt::SortPointer CHC::sort(FunctionDefinition const& _function) +smtutil::SortPointer CHC::sort(FunctionDefinition const& _function) { auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }; auto inputSorts = applyMap(_function.parameters(), smtSort); auto outputSorts = applyMap(_function.returnParameters(), smtSort); - return make_shared( - vector{smt::SortProvider::intSort} + m_stateSorts + inputSorts + m_stateSorts + inputSorts + outputSorts, - smt::SortProvider::boolSort + return make_shared( + vector{smtutil::SortProvider::intSort} + m_stateSorts + inputSorts + m_stateSorts + inputSorts + outputSorts, + smtutil::SortProvider::boolSort ); } -smt::SortPointer CHC::sort(ASTNode const* _node) +smtutil::SortPointer CHC::sort(ASTNode const* _node) { if (auto funDef = dynamic_cast(_node)) return sort(*funDef); - auto fSort = dynamic_pointer_cast(sort(*m_currentFunction)); + auto fSort = dynamic_pointer_cast(sort(*m_currentFunction)); solAssert(fSort, ""); auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }; - return make_shared( + return make_shared( fSort->domain + applyMap(m_currentFunction->localVariables(), smtSort), - smt::SortProvider::boolSort + smtutil::SortProvider::boolSort ); } -smt::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract) +smtutil::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract) { auto stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract); auto sorts = stateSorts(_contract); @@ -774,13 +775,13 @@ smt::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractD auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }; auto inputSorts = applyMap(_function.parameters(), smtSort); auto outputSorts = applyMap(_function.returnParameters(), smtSort); - return make_shared( - vector{smt::SortProvider::intSort} + sorts + inputSorts + sorts + outputSorts, - smt::SortProvider::boolSort + return make_shared( + vector{smtutil::SortProvider::intSort} + sorts + inputSorts + sorts + outputSorts, + smtutil::SortProvider::boolSort ); } -unique_ptr CHC::createSymbolicBlock(smt::SortPointer _sort, string const& _name) +unique_ptr CHC::createSymbolicBlock(smtutil::SortPointer _sort, string const& _name) { auto block = make_unique( _sort, @@ -807,7 +808,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) } } -smt::Expression CHC::interface() +smtutil::Expression CHC::interface() { auto paramExprs = applyMap( m_stateVariables, @@ -816,32 +817,32 @@ smt::Expression CHC::interface() return (*m_interfaces.at(m_currentContract))(paramExprs); } -smt::Expression CHC::interface(ContractDefinition const& _contract) +smtutil::Expression CHC::interface(ContractDefinition const& _contract) { return (*m_interfaces.at(&_contract))(stateVariablesAtIndex(0, _contract)); } -smt::Expression CHC::error() +smtutil::Expression CHC::error() { return (*m_errorPredicate)({}); } -smt::Expression CHC::error(unsigned _idx) +smtutil::Expression CHC::error(unsigned _idx) { return m_errorPredicate->functionValueAtIndex(_idx)({}); } -smt::Expression CHC::summary(ContractDefinition const&) +smtutil::Expression CHC::summary(ContractDefinition const&) { return (*m_constructorSummaryPredicate)( - vector{m_error.currentValue()} + + vector{m_error.currentValue()} + currentStateVariables() ); } -smt::Expression CHC::summary(FunctionDefinition const& _function) +smtutil::Expression CHC::summary(FunctionDefinition const& _function) { - vector args{m_error.currentValue()}; + vector args{m_error.currentValue()}; auto contract = _function.annotation().contract; args += contract->isLibrary() ? stateVariablesAtIndex(0, *contract) : initialStateVariables(); args += applyMap(_function.parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }); @@ -876,27 +877,27 @@ void CHC::createErrorBlock() m_interface->registerRelation(m_errorPredicate->currentFunctionValue()); } -void CHC::connectBlocks(smt::Expression const& _from, smt::Expression const& _to, smt::Expression const& _constraints) +void CHC::connectBlocks(smtutil::Expression const& _from, smtutil::Expression const& _to, smtutil::Expression const& _constraints) { - smt::Expression edge = smt::Expression::implies( + smtutil::Expression edge = smtutil::Expression::implies( _from && m_context.assertions() && _constraints, _to ); addRule(edge, _from.name + "_to_" + _to.name); } -vector CHC::initialStateVariables() +vector CHC::initialStateVariables() { return stateVariablesAtIndex(0); } -vector CHC::stateVariablesAtIndex(int _index) +vector CHC::stateVariablesAtIndex(int _index) { solAssert(m_currentContract, ""); return applyMap(m_stateVariables, [&](auto _var) { return valueAtIndex(*_var, _index); }); } -vector CHC::stateVariablesAtIndex(int _index, ContractDefinition const& _contract) +vector CHC::stateVariablesAtIndex(int _index, ContractDefinition const& _contract) { return applyMap( stateVariablesIncludingInheritedAndPrivate(_contract), @@ -904,23 +905,23 @@ vector CHC::stateVariablesAtIndex(int _index, ContractDefinitio ); } -vector CHC::currentStateVariables() +vector CHC::currentStateVariables() { solAssert(m_currentContract, ""); return applyMap(m_stateVariables, [this](auto _var) { return currentValue(*_var); }); } -vector CHC::currentFunctionVariables() +vector CHC::currentFunctionVariables() { - vector initInputExprs; - vector mutableInputExprs; + vector initInputExprs; + vector mutableInputExprs; for (auto const& var: m_currentFunction->parameters()) { initInputExprs.push_back(m_context.variable(*var)->valueAtIndex(0)); mutableInputExprs.push_back(m_context.variable(*var)->currentValue()); } auto returnExprs = applyMap(m_currentFunction->returnParameters(), [this](auto _var) { return currentValue(*_var); }); - return vector{m_error.currentValue()} + + return vector{m_error.currentValue()} + initialStateVariables() + initInputExprs + currentStateVariables() + @@ -928,7 +929,7 @@ vector CHC::currentFunctionVariables() returnExprs; } -vector CHC::currentBlockVariables() +vector CHC::currentBlockVariables() { if (m_currentFunction) return currentFunctionVariables() + applyMap(m_currentFunction->localVariables(), [this](auto _var) { return currentValue(*_var); }); @@ -953,27 +954,27 @@ string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contr return prefix + "_" + to_string(_node->id()) + "_" + to_string(contract->id()); } -smt::Expression CHC::predicate(smt::SymbolicFunctionVariable const& _block) +smtutil::Expression CHC::predicate(smt::SymbolicFunctionVariable const& _block) { return _block(currentBlockVariables()); } -smt::Expression CHC::predicate( +smtutil::Expression CHC::predicate( smt::SymbolicFunctionVariable const& _block, - vector const& _arguments + vector const& _arguments ) { return _block(_arguments); } -smt::Expression CHC::predicate(FunctionCall const& _funCall) +smtutil::Expression CHC::predicate(FunctionCall const& _funCall) { auto const* function = functionCallToDefinition(_funCall); if (!function) - return smt::Expression(true); + return smtutil::Expression(true); m_error.increaseIndex(); - vector args{m_error.currentValue()}; + vector args{m_error.currentValue()}; auto const* contract = function->annotation().contract; args += contract->isLibrary() ? stateVariablesAtIndex(0, *contract) : currentStateVariables(); @@ -997,28 +998,28 @@ smt::Expression CHC::predicate(FunctionCall const& _funCall) return (*m_summaries.at(m_currentContract).at(function))(args); } -void CHC::addRule(smt::Expression const& _rule, string const& _ruleName) +void CHC::addRule(smtutil::Expression const& _rule, string const& _ruleName) { m_interface->addRule(_rule, _ruleName); } -pair> CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _location) +pair> CHC::query(smtutil::Expression const& _query, langutil::SourceLocation const& _location) { - smt::CheckResult result; + smtutil::CheckResult result; vector values; tie(result, values) = m_interface->query(_query); switch (result) { - case smt::CheckResult::SATISFIABLE: + case smtutil::CheckResult::SATISFIABLE: break; - case smt::CheckResult::UNSATISFIABLE: + case smtutil::CheckResult::UNSATISFIABLE: break; - case smt::CheckResult::UNKNOWN: + case smtutil::CheckResult::UNKNOWN: break; - case smt::CheckResult::CONFLICTING: + case smtutil::CheckResult::CONFLICTING: m_outerErrorReporter.warning(1988_error, _location, "At least two SMT solvers provided conflicting answers. Results might not be sound."); break; - case smt::CheckResult::ERROR: + case smtutil::CheckResult::ERROR: m_outerErrorReporter.warning(1218_error, _location, "Error trying to invoke SMT solver."); break; } @@ -1028,26 +1029,26 @@ pair> CHC::query(smt::Expression const& _query, void CHC::addVerificationTarget( ASTNode const* _scope, VerificationTarget::Type _type, - smt::Expression _from, - smt::Expression _constraints, - smt::Expression _errorId + smtutil::Expression _from, + smtutil::Expression _constraints, + smtutil::Expression _errorId ) { m_verificationTargets.emplace(_scope, CHCVerificationTarget{{_type, _from, _constraints}, _errorId}); } -void CHC::addAssertVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId) +void CHC::addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId) { addVerificationTarget(_scope, VerificationTarget::Type::Assert, _from, _constraints, _errorId); } -void CHC::addArrayPopVerificationTarget(ASTNode const* _scope, smt::Expression _errorId) +void CHC::addArrayPopVerificationTarget(ASTNode const* _scope, smtutil::Expression _errorId) { solAssert(m_currentContract, ""); solAssert(m_currentFunction, ""); if (m_currentFunction->isConstructor()) - addVerificationTarget(_scope, VerificationTarget::Type::PopEmptyArray, summary(*m_currentContract), smt::Expression(true), _errorId); + addVerificationTarget(_scope, VerificationTarget::Type::PopEmptyArray, summary(*m_currentContract), smtutil::Expression(true), _errorId); else { auto iface = (*m_interfaces.at(m_currentContract))(initialStateVariables()); diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 9315da70f..b1235a188 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -49,7 +49,7 @@ public: langutil::ErrorReporter& _errorReporter, std::map const& _smtlib2Responses, ReadCallback::Callback const& _smtCallback, - smt::SMTSolverChoice _enabledSolvers + smtutil::SMTSolverChoice _enabledSolvers ); void analyze(SourceUnit const& _sources); @@ -96,43 +96,43 @@ private: void eraseKnowledge(); void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override; bool shouldVisit(FunctionDefinition const& _function) const; - void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector const* _arguments = nullptr); + void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector const* _arguments = nullptr); std::set transactionAssertions(ASTNode const* _txRoot); static std::vector stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract); //@} /// Sort helpers. //@{ - static std::vector stateSorts(ContractDefinition const& _contract); - smt::SortPointer constructorSort(); - smt::SortPointer interfaceSort(); - static smt::SortPointer interfaceSort(ContractDefinition const& _const); - smt::SortPointer arity0FunctionSort(); - smt::SortPointer sort(FunctionDefinition const& _function); - smt::SortPointer sort(ASTNode const* _block); + static std::vector stateSorts(ContractDefinition const& _contract); + smtutil::SortPointer constructorSort(); + smtutil::SortPointer interfaceSort(); + static smtutil::SortPointer interfaceSort(ContractDefinition const& _const); + smtutil::SortPointer arity0FunctionSort(); + smtutil::SortPointer sort(FunctionDefinition const& _function); + smtutil::SortPointer sort(ASTNode const* _block); /// @returns the sort of a predicate that represents the summary of _function in the scope of _contract. /// The _contract is also needed because the same function might be in many contracts due to inheritance, /// where the sort changes because the set of state variables might change. - static smt::SortPointer summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract); + static smtutil::SortPointer summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract); //@} /// Predicate helpers. //@{ /// @returns a new block of given _sort and _name. - std::unique_ptr createSymbolicBlock(smt::SortPointer _sort, std::string const& _name); + std::unique_ptr createSymbolicBlock(smtutil::SortPointer _sort, std::string const& _name); /// Creates summary predicates for all functions of all contracts /// in a given _source. void defineInterfacesAndSummaries(SourceUnit const& _source); /// Genesis predicate. - smt::Expression genesis() { return (*m_genesisPredicate)({}); } + smtutil::Expression genesis() { return (*m_genesisPredicate)({}); } /// Interface predicate over current variables. - smt::Expression interface(); - smt::Expression interface(ContractDefinition const& _contract); + smtutil::Expression interface(); + smtutil::Expression interface(ContractDefinition const& _contract); /// Error predicate over current variables. - smt::Expression error(); - smt::Expression error(unsigned _idx); + smtutil::Expression error(); + smtutil::Expression error(unsigned _idx); /// Creates a block for the given _node. std::unique_ptr createBlock(ASTNode const* _node, std::string const& _prefix = ""); @@ -144,48 +144,48 @@ private: /// Also registers the predicate. void createErrorBlock(); - void connectBlocks(smt::Expression const& _from, smt::Expression const& _to, smt::Expression const& _constraints = smt::Expression(true)); + void connectBlocks(smtutil::Expression const& _from, smtutil::Expression const& _to, smtutil::Expression const& _constraints = smtutil::Expression(true)); /// @returns the symbolic values of the state variables at the beginning /// of the current transaction. - std::vector initialStateVariables(); - std::vector stateVariablesAtIndex(int _index); - std::vector stateVariablesAtIndex(int _index, ContractDefinition const& _contract); + std::vector initialStateVariables(); + std::vector stateVariablesAtIndex(int _index); + std::vector stateVariablesAtIndex(int _index, ContractDefinition const& _contract); /// @returns the current symbolic values of the current state variables. - std::vector currentStateVariables(); + std::vector currentStateVariables(); /// @returns the current symbolic values of the current function's /// input and output parameters. - std::vector currentFunctionVariables(); + std::vector currentFunctionVariables(); /// @returns the same as currentFunctionVariables plus /// local variables. - std::vector currentBlockVariables(); + std::vector currentBlockVariables(); /// @returns the predicate name for a given node. std::string predicateName(ASTNode const* _node, ContractDefinition const* _contract = nullptr); /// @returns a predicate application over the current scoped variables. - smt::Expression predicate(smt::SymbolicFunctionVariable const& _block); + smtutil::Expression predicate(smt::SymbolicFunctionVariable const& _block); /// @returns a predicate application over @param _arguments. - smt::Expression predicate(smt::SymbolicFunctionVariable const& _block, std::vector const& _arguments); + smtutil::Expression predicate(smt::SymbolicFunctionVariable const& _block, std::vector const& _arguments); /// @returns the summary predicate for the called function. - smt::Expression predicate(FunctionCall const& _funCall); + smtutil::Expression predicate(FunctionCall const& _funCall); /// @returns a predicate that defines a constructor summary. - smt::Expression summary(ContractDefinition const& _contract); + smtutil::Expression summary(ContractDefinition const& _contract); /// @returns a predicate that defines a function summary. - smt::Expression summary(FunctionDefinition const& _function); + smtutil::Expression summary(FunctionDefinition const& _function); //@} /// Solver related. //@{ /// Adds Horn rule to the solver. - void addRule(smt::Expression const& _rule, std::string const& _ruleName); + void addRule(smtutil::Expression const& _rule, std::string const& _ruleName); /// @returns if query is unsatisfiable (safe). /// @returns otherwise. - std::pair> query(smt::Expression const& _query, langutil::SourceLocation const& _location); + std::pair> query(smtutil::Expression const& _query, langutil::SourceLocation const& _location); - void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId); - void addAssertVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId); - void addArrayPopVerificationTarget(ASTNode const* _scope, smt::Expression _errorId); + void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId); + void addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId); + void addArrayPopVerificationTarget(ASTNode const* _scope, smtutil::Expression _errorId); //@} /// Misc. @@ -231,7 +231,7 @@ private: //@{ /// State variables sorts. /// Used by all predicates. - std::vector m_stateSorts; + std::vector m_stateSorts; /// State variables. /// Used to create all predicates. std::vector m_stateVariables; @@ -241,7 +241,7 @@ private: //@{ struct CHCVerificationTarget: VerificationTarget { - smt::Expression errorId; + smtutil::Expression errorId; }; std::map m_verificationTargets; @@ -261,7 +261,7 @@ private: std::map, IdCompare> m_functionAssertions; /// The current block. - smt::Expression m_currentBlock = smt::Expression(true); + smtutil::Expression m_currentBlock = smtutil::Expression(true); /// Counter to generate unique block names. unsigned m_blockCounter = 0; @@ -276,13 +276,13 @@ private: //@} /// CHC solver. - std::unique_ptr m_interface; + std::unique_ptr m_interface; /// ErrorReporter that comes from CompilerStack. langutil::ErrorReporter& m_outerErrorReporter; /// SMT solvers that are chosen at runtime. - smt::SMTSolverChoice m_enabledSolvers; + smtutil::SMTSolverChoice m_enabledSolvers; }; } diff --git a/libsolidity/formal/EncodingContext.cpp b/libsolidity/formal/EncodingContext.cpp index 3e0e4fa7e..51dd37a3d 100644 --- a/libsolidity/formal/EncodingContext.cpp +++ b/libsolidity/formal/EncodingContext.cpp @@ -92,7 +92,7 @@ void EncodingContext::resetAllVariables() resetVariables([&](frontend::VariableDeclaration const&) { return true; }); } -Expression EncodingContext::newValue(frontend::VariableDeclaration const& _decl) +smtutil::Expression EncodingContext::newValue(frontend::VariableDeclaration const& _decl) { solAssert(knownVariable(_decl), ""); return m_variables.at(&_decl)->increaseIndex(); @@ -179,10 +179,10 @@ bool EncodingContext::knownGlobalSymbol(string const& _var) const /// Solver. -Expression EncodingContext::assertions() +smtutil::Expression EncodingContext::assertions() { if (m_assertions.empty()) - return Expression(true); + return smtutil::Expression(true); return m_assertions.back(); } @@ -201,7 +201,7 @@ void EncodingContext::popSolver() m_assertions.pop_back(); } -void EncodingContext::addAssertion(Expression const& _expr) +void EncodingContext::addAssertion(smtutil::Expression const& _expr) { if (m_assertions.empty()) m_assertions.push_back(_expr); diff --git a/libsolidity/formal/EncodingContext.h b/libsolidity/formal/EncodingContext.h index e8cf48ed0..79f9567a5 100644 --- a/libsolidity/formal/EncodingContext.h +++ b/libsolidity/formal/EncodingContext.h @@ -46,7 +46,7 @@ public: /// Sets the current solver used by the current engine for /// SMT variable declaration. - void setSolver(SolverInterface* _solver) + void setSolver(smtutil::SolverInterface* _solver) { solAssert(_solver, ""); m_solver = _solver; @@ -56,7 +56,7 @@ public: void setAssertionAccumulation(bool _acc) { m_accumulateAssertions = _acc; } /// Forwards variable creation to the solver. - Expression newVariable(std::string _name, SortPointer _sort) + smtutil::Expression newVariable(std::string _name, smtutil::SortPointer _sort) { solAssert(m_solver, ""); return m_solver->newVariable(move(_name), move(_sort)); @@ -86,7 +86,7 @@ public: /// Allocates a new index for the declaration, updates the current /// index to this value and returns the expression. - Expression newValue(frontend::VariableDeclaration const& _decl); + smtutil::Expression newValue(frontend::VariableDeclaration const& _decl); /// Sets the value of the declaration to zero. void setZeroValue(frontend::VariableDeclaration const& _decl); void setZeroValue(SymbolicVariable& _variable); @@ -126,12 +126,12 @@ public: /// Solver. //@{ /// @returns conjunction of all added assertions. - Expression assertions(); + smtutil::Expression assertions(); void pushSolver(); void popSolver(); - void addAssertion(Expression const& _e); + void addAssertion(smtutil::Expression const& _e); unsigned solverStackHeigh() { return m_assertions.size(); } const - SolverInterface* solver() + smtutil::SolverInterface* solver() { solAssert(m_solver, ""); return m_solver; @@ -160,10 +160,10 @@ private: /// Solver related. //@{ /// Solver can be SMT solver or Horn solver in the future. - SolverInterface* m_solver = nullptr; + smtutil::SolverInterface* m_solver = nullptr; /// Assertion stack. - std::vector m_assertions; + std::vector m_assertions; /// Whether to conjoin assertions in the assertion stack. bool m_accumulateAssertions = true; diff --git a/libsolidity/formal/ModelChecker.cpp b/libsolidity/formal/ModelChecker.cpp index ebc1a8751..f74e1327d 100644 --- a/libsolidity/formal/ModelChecker.cpp +++ b/libsolidity/formal/ModelChecker.cpp @@ -27,7 +27,7 @@ ModelChecker::ModelChecker( ErrorReporter& _errorReporter, map const& _smtlib2Responses, ReadCallback::Callback const& _smtCallback, - smt::SMTSolverChoice _enabledSolvers + smtutil::SMTSolverChoice _enabledSolvers ): m_context(), m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers), @@ -49,9 +49,9 @@ vector ModelChecker::unhandledQueries() return m_bmc.unhandledQueries() + m_chc.unhandledQueries(); } -smt::SMTSolverChoice ModelChecker::availableSolvers() +solidity::smtutil::SMTSolverChoice ModelChecker::availableSolvers() { - smt::SMTSolverChoice available = smt::SMTSolverChoice::None(); + smtutil::SMTSolverChoice available = smtutil::SMTSolverChoice::None(); #ifdef HAVE_Z3 available.z3 = true; #endif diff --git a/libsolidity/formal/ModelChecker.h b/libsolidity/formal/ModelChecker.h index 663bae869..b4378e629 100644 --- a/libsolidity/formal/ModelChecker.h +++ b/libsolidity/formal/ModelChecker.h @@ -49,7 +49,7 @@ public: langutil::ErrorReporter& _errorReporter, std::map const& _smtlib2Responses, ReadCallback::Callback const& _smtCallback = ReadCallback::Callback(), - smt::SMTSolverChoice _enabledSolvers = smt::SMTSolverChoice::All() + smtutil::SMTSolverChoice _enabledSolvers = smtutil::SMTSolverChoice::All() ); void analyze(SourceUnit const& _sources); @@ -60,7 +60,7 @@ public: std::vector unhandledQueries(); /// @returns SMT solvers that are available via the C++ API. - static smt::SMTSolverChoice availableSolvers(); + static smtutil::SMTSolverChoice availableSolvers(); private: /// Stores the context of the encoding. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 7a62199b2..afaf8ea7e 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -181,7 +181,7 @@ void SMTEncoder::inlineModifierInvocation(ModifierInvocation const* _invocation, solAssert(_invocation, ""); _invocation->accept(*this); - vector args; + vector args; if (auto const* arguments = _invocation->arguments()) { auto const& modifierParams = _definition->parameters(); @@ -367,7 +367,7 @@ void SMTEncoder::endVisit(Assignment const& _assignment) else { auto const& type = _assignment.annotation().type; - vector rightArguments; + vector rightArguments; if (auto const* tupleTypeRight = dynamic_cast(_assignment.rightHandSide().annotation().type)) { auto symbTupleLeft = dynamic_pointer_cast(m_context.expression(_assignment.leftHandSide())); @@ -641,7 +641,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall) auto const& value = args.front(); solAssert(value, ""); - smt::Expression thisBalance = m_context.state().balance(); + smtutil::Expression thisBalance = m_context.state().balance(); setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), m_context); m_context.state().transfer(m_context.state().thisAddress(), expr(address), expr(*value)); @@ -779,7 +779,7 @@ void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall) else { auto const& intType = dynamic_cast(*m_context.expression(_funCall)->type()); - defineExpr(_funCall, smt::Expression::ite( + defineExpr(_funCall, smtutil::Expression::ite( expr(*argument) >= smt::minValue(intType) && expr(*argument) <= smt::maxValue(intType), expr(*argument), expr(_funCall) @@ -810,9 +810,9 @@ void SMTEncoder::endVisit(Literal const& _literal) solAssert(_literal.annotation().type, "Expected type for AST node"); Type const& type = *_literal.annotation().type; if (smt::isNumber(type.category())) - defineExpr(_literal, smt::Expression(type.literalValue(&_literal))); + defineExpr(_literal, smtutil::Expression(type.literalValue(&_literal))); else if (smt::isBool(type.category())) - defineExpr(_literal, smt::Expression(_literal.token() == Token::TrueLiteral ? true : false)); + defineExpr(_literal, smtutil::Expression(_literal.token() == Token::TrueLiteral ? true : false)); else if (smt::isStringLiteral(type.category())) createExpr(_literal); else @@ -965,7 +965,7 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess) auto arrayVar = dynamic_pointer_cast(array); solAssert(arrayVar, ""); - defineExpr(_indexAccess, smt::Expression::select( + defineExpr(_indexAccess, smtutil::Expression::select( arrayVar->elements(), expr(*_indexAccess.indexExpression()) )); @@ -992,7 +992,7 @@ void SMTEncoder::arrayAssignment() m_arrayAssignmentHappened = true; } -void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression const& _rightHandSide) +void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide) { auto toStore = _rightHandSide; auto indexAccess = dynamic_cast(&_expr); @@ -1039,7 +1039,7 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression c }); auto symbArray = dynamic_pointer_cast(m_context.variable(*varDecl)); - smt::Expression store = smt::Expression::store( + smtutil::Expression store = smtutil::Expression::store( symbArray->elements(), expr(*indexAccess->indexExpression()), toStore @@ -1050,7 +1050,7 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression c m_context.addAssertion(symbArray->length() == oldLength); // Update the SMT select value after the assignment, // necessary for sound models. - defineExpr(*indexAccess, smt::Expression::select( + defineExpr(*indexAccess, smtutil::Expression::select( symbArray->elements(), expr(*indexAccess->indexExpression()) )); @@ -1061,9 +1061,9 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression c { auto symbArray = dynamic_pointer_cast(m_context.expression(*base)); solAssert(symbArray, ""); - toStore = smt::Expression::tuple_constructor( - smt::Expression(base->annotation().type), - {smt::Expression::store(symbArray->elements(), expr(*indexAccess->indexExpression()), toStore), symbArray->length()} + toStore = smtutil::Expression::tuple_constructor( + smtutil::Expression(base->annotation().type), + {smtutil::Expression::store(symbArray->elements(), expr(*indexAccess->indexExpression()), toStore), symbArray->length()} ); indexAccess = base; } @@ -1092,10 +1092,10 @@ void SMTEncoder::arrayPush(FunctionCall const& _funCall) m_context.addAssertion(oldLength + 1 < (smt::maxValue(*TypeProvider::uint256()) - 1)); auto const& arguments = _funCall.arguments(); - smt::Expression element = arguments.empty() ? + smtutil::Expression element = arguments.empty() ? smt::zeroValue(_funCall.annotation().type) : expr(*arguments.front()); - smt::Expression store = smt::Expression::store( + smtutil::Expression store = smtutil::Expression::store( symbArray->elements(), oldLength, element @@ -1125,7 +1125,7 @@ void SMTEncoder::arrayPop(FunctionCall const& _funCall) symbArray->increaseIndex(); m_context.addAssertion(symbArray->elements() == oldElements); - auto newLength = smt::Expression::ite( + auto newLength = smtutil::Expression::ite( oldLength == 0, smt::maxValue(*TypeProvider::uint256()), oldLength - 1 @@ -1135,7 +1135,7 @@ void SMTEncoder::arrayPop(FunctionCall const& _funCall) arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue()); } -void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smt::Expression const& _array) +void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression const& _array) { if (auto const* id = dynamic_cast(&_expr)) { @@ -1176,9 +1176,9 @@ bool SMTEncoder::shortcutRationalNumber(Expression const& _expr) auto rationalType = dynamic_cast(_expr.annotation().type); solAssert(rationalType, ""); if (rationalType->isNegative()) - defineExpr(_expr, smt::Expression(u2s(rationalType->literalValue(nullptr)))); + defineExpr(_expr, smtutil::Expression(u2s(rationalType->literalValue(nullptr)))); else - defineExpr(_expr, smt::Expression(rationalType->literalValue(nullptr))); + defineExpr(_expr, smtutil::Expression(rationalType->literalValue(nullptr))); return true; } return false; @@ -1224,10 +1224,10 @@ void SMTEncoder::arithmeticOperation(BinaryOperation const& _op) ); } -pair SMTEncoder::arithmeticOperation( +pair SMTEncoder::arithmeticOperation( Token _op, - smt::Expression const& _left, - smt::Expression const& _right, + smtutil::Expression const& _left, + smtutil::Expression const& _right, TypePointer const& _commonType, Expression const& ) @@ -1244,7 +1244,7 @@ pair SMTEncoder::arithmeticOperation( solAssert(_commonType->category() == Type::Category::Integer, ""); auto const& intType = dynamic_cast(*_commonType); - smt::Expression valueNoMod( + smtutil::Expression valueNoMod( _op == Token::Add ? _left + _right : _op == Token::Sub ? _left - _right : _op == Token::Div ? division(_left, _right, intType) : @@ -1255,11 +1255,11 @@ pair SMTEncoder::arithmeticOperation( if (_op == Token::Div || _op == Token::Mod) m_context.addAssertion(_right != 0); - smt::Expression intValueRange = (0 - smt::minValue(intType)) + smt::maxValue(intType) + 1; - auto value = smt::Expression::ite( + smtutil::Expression intValueRange = (0 - smt::minValue(intType)) + smt::maxValue(intType) + 1; + auto value = smtutil::Expression::ite( valueNoMod > smt::maxValue(intType), valueNoMod % intValueRange, - smt::Expression::ite( + smtutil::Expression::ite( valueNoMod < smt::minValue(intType), valueNoMod % intValueRange, valueNoMod @@ -1267,7 +1267,7 @@ pair SMTEncoder::arithmeticOperation( ); if (intType.isSigned()) - value = smt::Expression::ite( + value = smtutil::Expression::ite( value > smt::maxValue(intType), value - intValueRange, value @@ -1282,13 +1282,13 @@ void SMTEncoder::compareOperation(BinaryOperation const& _op) solAssert(commonType, ""); if (smt::isSupportedType(commonType->category())) { - smt::Expression left(expr(_op.leftExpression(), commonType)); - smt::Expression right(expr(_op.rightExpression(), commonType)); + smtutil::Expression left(expr(_op.leftExpression(), commonType)); + smtutil::Expression right(expr(_op.rightExpression(), commonType)); Token op = _op.getOperator(); - shared_ptr value; + shared_ptr value; if (smt::isNumber(commonType->category())) { - value = make_shared( + value = make_shared( op == Token::Equal ? (left == right) : op == Token::NotEqual ? (left != right) : op == Token::LessThan ? (left < right) : @@ -1300,7 +1300,7 @@ void SMTEncoder::compareOperation(BinaryOperation const& _op) else // Bool { solUnimplementedAssert(smt::isBool(commonType->category()), "Operation not yet supported"); - value = make_shared( + value = make_shared( op == Token::Equal ? (left == right) : /*op == Token::NotEqual*/ (left != right) ); @@ -1345,14 +1345,14 @@ void SMTEncoder::booleanOperation(BinaryOperation const& _op) ); } -smt::Expression SMTEncoder::division(smt::Expression _left, smt::Expression _right, IntegerType const& _type) +smtutil::Expression SMTEncoder::division(smtutil::Expression _left, smtutil::Expression _right, IntegerType const& _type) { // Signed division in SMTLIB2 rounds differently for negative division. if (_type.isSigned()) - return (smt::Expression::ite( + return (smtutil::Expression::ite( _left >= 0, - smt::Expression::ite(_right >= 0, _left / _right, 0 - (_left / (0 - _right))), - smt::Expression::ite(_right >= 0, 0 - ((0 - _left) / _right), (0 - _left) / (0 - _right)) + smtutil::Expression::ite(_right >= 0, _left / _right, 0 - (_left / (0 - _right))), + smtutil::Expression::ite(_right >= 0, 0 - ((0 - _left) / _right), (0 - _left) / (0 - _right)) )); else return _left / _right; @@ -1360,7 +1360,7 @@ smt::Expression SMTEncoder::division(smt::Expression _left, smt::Expression _rig void SMTEncoder::assignment( Expression const& _left, - vector const& _right, + vector const& _right, TypePointer const& _type, langutil::SourceLocation const& _location ) @@ -1406,7 +1406,7 @@ void SMTEncoder::assignment( ); } -smt::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment) +smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment) { static map const compoundToArithmetic{ {Token::AssignAdd, Token::Add}, @@ -1440,7 +1440,7 @@ void SMTEncoder::assignment(VariableDeclaration const& _variable, Expression con // TODO else { store each string literal byte into the array } } -void SMTEncoder::assignment(VariableDeclaration const& _variable, smt::Expression const& _value) +void SMTEncoder::assignment(VariableDeclaration const& _variable, smtutil::Expression const& _value) { TypePointer type = _variable.type(); if (type->category() == Type::Category::Mapping) @@ -1448,12 +1448,12 @@ void SMTEncoder::assignment(VariableDeclaration const& _variable, smt::Expressio m_context.addAssertion(m_context.newValue(_variable) == _value); } -SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, smt::Expression _condition) +SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, smtutil::Expression _condition) { return visitBranch(_statement, &_condition); } -SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, smt::Expression const* _condition) +SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, smtutil::Expression const* _condition) { auto indicesBeforeBranch = copyVariableIndices(); if (_condition) @@ -1466,7 +1466,7 @@ SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, s return indicesAfterBranch; } -void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _function, vector const& _callArgs) +void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _function, vector const& _callArgs) { auto const& funParams = _function.parameters(); solAssert(funParams.size() == _callArgs.size(), ""); @@ -1563,7 +1563,7 @@ TypePointer SMTEncoder::typeWithoutPointer(TypePointer const& _type) return _type; } -void SMTEncoder::mergeVariables(set const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse) +void SMTEncoder::mergeVariables(set const& _variables, smtutil::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse) { auto cmp = [] (VariableDeclaration const* var1, VariableDeclaration const* var2) { return var1->id() < var2->id(); @@ -1590,7 +1590,7 @@ void SMTEncoder::mergeVariables(set const& _variable int trueIndex = _indicesEndTrue.at(decl); int falseIndex = _indicesEndFalse.at(decl); solAssert(trueIndex != falseIndex, ""); - m_context.addAssertion(m_context.newValue(*decl) == smt::Expression::ite( + m_context.addAssertion(m_context.newValue(*decl) == smtutil::Expression::ite( _condition, valueAtIndex(*decl, trueIndex), valueAtIndex(*decl, falseIndex)) @@ -1598,13 +1598,13 @@ void SMTEncoder::mergeVariables(set const& _variable } } -smt::Expression SMTEncoder::currentValue(VariableDeclaration const& _decl) +smtutil::Expression SMTEncoder::currentValue(VariableDeclaration const& _decl) { solAssert(m_context.knownVariable(_decl), ""); return m_context.variable(_decl)->currentValue(); } -smt::Expression SMTEncoder::valueAtIndex(VariableDeclaration const& _decl, int _index) +smtutil::Expression SMTEncoder::valueAtIndex(VariableDeclaration const& _decl, int _index) { solAssert(m_context.knownVariable(_decl), ""); return m_context.variable(_decl)->valueAtIndex(_index); @@ -1627,7 +1627,7 @@ bool SMTEncoder::createVariable(VariableDeclaration const& _varDecl) return true; } -smt::Expression SMTEncoder::expr(Expression const& _e, TypePointer _targetType) +smtutil::Expression SMTEncoder::expr(Expression const& _e, TypePointer _targetType) { if (!m_context.knownExpression(_e)) { @@ -1649,10 +1649,10 @@ void SMTEncoder::createExpr(Expression const& _e) ); } -void SMTEncoder::defineExpr(Expression const& _e, smt::Expression _value) +void SMTEncoder::defineExpr(Expression const& _e, smtutil::Expression _value) { createExpr(_e); - solAssert(_value.sort->kind != smt::Kind::Function, "Equality operator applied to type that is not fully supported"); + solAssert(_value.sort->kind != smtutil::Kind::Function, "Equality operator applied to type that is not fully supported"); m_context.addAssertion(expr(_e) == _value); } @@ -1662,15 +1662,15 @@ void SMTEncoder::popPathCondition() m_pathConditions.pop_back(); } -void SMTEncoder::pushPathCondition(smt::Expression const& _e) +void SMTEncoder::pushPathCondition(smtutil::Expression const& _e) { m_pathConditions.push_back(currentPathConditions() && _e); } -smt::Expression SMTEncoder::currentPathConditions() +smtutil::Expression SMTEncoder::currentPathConditions() { if (m_pathConditions.empty()) - return smt::Expression(true); + return smtutil::Expression(true); return m_pathConditions.back(); } @@ -1698,9 +1698,9 @@ void SMTEncoder::pushCallStack(CallStackEntry _entry) m_callStack.push_back(_entry); } -void SMTEncoder::addPathImpliedExpression(smt::Expression const& _e) +void SMTEncoder::addPathImpliedExpression(smtutil::Expression const& _e) { - m_context.addAssertion(smt::Expression::implies(currentPathConditions(), _e)); + m_context.addAssertion(smtutil::Expression::implies(currentPathConditions(), _e)); } bool SMTEncoder::isRootFunction() @@ -1836,12 +1836,12 @@ void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall) defineExpr(_funCall, currentValue(*returnParams.front())); } -vector SMTEncoder::symbolicArguments(FunctionCall const& _funCall) +vector SMTEncoder::symbolicArguments(FunctionCall const& _funCall) { auto const* function = functionCallToDefinition(_funCall); solAssert(function, ""); - vector args; + vector args; Expression const* calledExpr = &_funCall.expression(); auto const& funType = dynamic_cast(calledExpr->annotation().type); solAssert(funType, ""); diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index f62f18558..63bbd45df 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -99,10 +99,10 @@ protected: /// @returns _op(_left, _right) with and without modular arithmetic. /// Used by the function above, compound assignments and /// unary increment/decrement. - virtual std::pair arithmeticOperation( + virtual std::pair arithmeticOperation( Token _op, - smt::Expression const& _left, - smt::Expression const& _right, + smtutil::Expression const& _left, + smtutil::Expression const& _right, TypePointer const& _commonType, Expression const& _expression ); @@ -135,32 +135,32 @@ protected: /// while aliasing is not supported. void arrayAssignment(); /// Handles assignment to SMT array index. - void arrayIndexAssignment(Expression const& _expr, smt::Expression const& _rightHandSide); + void arrayIndexAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide); void arrayPush(FunctionCall const& _funCall); void arrayPop(FunctionCall const& _funCall); - void arrayPushPopAssign(Expression const& _expr, smt::Expression const& _array); + void arrayPushPopAssign(Expression const& _expr, smtutil::Expression const& _array); /// Allows BMC and CHC to create verification targets for popping /// an empty array. virtual void makeArrayPopVerificationTarget(FunctionCall const&) {} /// Division expression in the given type. Requires special treatment because /// of rounding for signed division. - smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type); + smtutil::Expression division(smtutil::Expression _left, smtutil::Expression _right, IntegerType const& _type); void assignment(VariableDeclaration const& _variable, Expression const& _value); /// Handles assignments to variables of different types. - void assignment(VariableDeclaration const& _variable, smt::Expression const& _value); + void assignment(VariableDeclaration const& _variable, smtutil::Expression const& _value); /// Handles assignments between generic expressions. /// Will also be used for assignments of tuple components. void assignment( Expression const& _left, - std::vector const& _right, + std::vector const& _right, TypePointer const& _type, langutil::SourceLocation const& _location ); /// Computes the right hand side of a compound assignment. - smt::Expression compoundAssignment(Assignment const& _assignment); + smtutil::Expression compoundAssignment(Assignment const& _assignment); /// Maps a variable to an SSA index. using VariableIndices = std::unordered_map; @@ -168,8 +168,8 @@ protected: /// Visits the branch given by the statement, pushes and pops the current path conditions. /// @param _condition if present, asserts that this condition is true within the branch. /// @returns the variable indices after visiting the branch. - VariableIndices visitBranch(ASTNode const* _statement, smt::Expression const* _condition = nullptr); - VariableIndices visitBranch(ASTNode const* _statement, smt::Expression _condition); + VariableIndices visitBranch(ASTNode const* _statement, smtutil::Expression const* _condition = nullptr); + VariableIndices visitBranch(ASTNode const* _statement, smtutil::Expression _condition); using CallStackEntry = std::pair; @@ -177,7 +177,7 @@ protected: void initializeStateVariables(ContractDefinition const& _contract); void createLocalVariables(FunctionDefinition const& _function); void initializeLocalVariables(FunctionDefinition const& _function); - void initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector const& _callArgs); + void initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector const& _callArgs); void resetStateVariables(); /// @returns the type without storage pointer information if it has it. TypePointer typeWithoutPointer(TypePointer const& _type); @@ -185,31 +185,31 @@ protected: /// Given two different branches and the touched variables, /// merge the touched variables into after-branch ite variables /// using the branch condition as guard. - void mergeVariables(std::set const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse); + void mergeVariables(std::set const& _variables, smtutil::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse); /// Tries to create an uninitialized variable and returns true on success. bool createVariable(VariableDeclaration const& _varDecl); /// @returns an expression denoting the value of the variable declared in @a _decl /// at the current point. - smt::Expression currentValue(VariableDeclaration const& _decl); + smtutil::Expression currentValue(VariableDeclaration const& _decl); /// @returns an expression denoting the value of the variable declared in @a _decl /// at the given index. Does not ensure that this index exists. - smt::Expression valueAtIndex(VariableDeclaration const& _decl, int _index); + smtutil::Expression valueAtIndex(VariableDeclaration const& _decl, int _index); /// Returns the expression corresponding to the AST node. /// If _targetType is not null apply conversion. /// Throws if the expression does not exist. - smt::Expression expr(Expression const& _e, TypePointer _targetType = nullptr); + smtutil::Expression expr(Expression const& _e, TypePointer _targetType = nullptr); /// Creates the expression (value can be arbitrary) void createExpr(Expression const& _e); /// Creates the expression and sets its value. - void defineExpr(Expression const& _e, smt::Expression _value); + void defineExpr(Expression const& _e, smtutil::Expression _value); /// Adds a new path condition - void pushPathCondition(smt::Expression const& _e); + void pushPathCondition(smtutil::Expression const& _e); /// Remove the last path condition void popPathCondition(); /// Returns the conjunction of all path conditions or True if empty - smt::Expression currentPathConditions(); + smtutil::Expression currentPathConditions(); /// @returns a human-readable call stack. Used for models. langutil::SecondarySourceLocation callStackMessage(std::vector const& _callStack); /// Copies and pops the last called node. @@ -217,7 +217,7 @@ protected: /// Adds (_definition, _node) to the callstack. void pushCallStack(CallStackEntry _entry); /// Add to the solver: the given expression implied by the current path conditions - void addPathImpliedExpression(smt::Expression const& _e); + void addPathImpliedExpression(smtutil::Expression const& _e); /// Copy the SSA indices of m_variables. VariableIndices copyVariableIndices(); @@ -240,7 +240,7 @@ protected: /// @returns the symbolic arguments for a function call, /// taking into account bound functions and /// type conversion. - std::vector symbolicArguments(FunctionCall const& _funCall); + std::vector symbolicArguments(FunctionCall const& _funCall); /// @returns a note to be added to warnings. std::string extraComment(); @@ -248,8 +248,8 @@ protected: struct VerificationTarget { enum class Type { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert, PopEmptyArray } type; - smt::Expression value; - smt::Expression constraints; + smtutil::Expression value; + smtutil::Expression constraints; }; smt::VariableUsage m_variableUsage; @@ -261,7 +261,7 @@ protected: /// These may be direct application of UFs or Array index access. /// Used to retrieve models. std::set m_uninterpretedTerms; - std::vector m_pathConditions; + std::vector m_pathConditions; /// Local SMTEncoder ErrorReporter. /// This is necessary to show the "No SMT solver available" /// warning before the others in case it's needed. diff --git a/libsolidity/formal/SymbolicState.cpp b/libsolidity/formal/SymbolicState.cpp index 5ae8922fb..1ab6e1860 100644 --- a/libsolidity/formal/SymbolicState.cpp +++ b/libsolidity/formal/SymbolicState.cpp @@ -20,6 +20,7 @@ #include using namespace std; +using namespace solidity; using namespace solidity::frontend::smt; SymbolicState::SymbolicState(EncodingContext& _context): @@ -35,22 +36,22 @@ void SymbolicState::reset() // Blockchain -Expression SymbolicState::thisAddress() +smtutil::Expression SymbolicState::thisAddress() { return m_thisAddress.currentValue(); } -Expression SymbolicState::balance() +smtutil::Expression SymbolicState::balance() { return balance(m_thisAddress.currentValue()); } -Expression SymbolicState::balance(Expression _address) +smtutil::Expression SymbolicState::balance(smtutil::Expression _address) { - return Expression::select(m_balances.elements(), move(_address)); + return smtutil::Expression::select(m_balances.elements(), move(_address)); } -void SymbolicState::transfer(Expression _from, Expression _to, Expression _value) +void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value) { unsigned indexBefore = m_balances.index(); addBalance(_from, 0 - _value); @@ -59,7 +60,7 @@ void SymbolicState::transfer(Expression _from, Expression _to, Expression _value solAssert(indexAfter > indexBefore, ""); m_balances.increaseIndex(); /// Do not apply the transfer operation if _from == _to. - auto newBalances = Expression::ite( + auto newBalances = smtutil::Expression::ite( move(_from) == move(_to), m_balances.valueAtIndex(indexBefore), m_balances.valueAtIndex(indexAfter) @@ -69,9 +70,9 @@ void SymbolicState::transfer(Expression _from, Expression _to, Expression _value /// Private helpers. -void SymbolicState::addBalance(Expression _address, Expression _value) +void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _value) { - auto newBalances = Expression::store( + auto newBalances = smtutil::Expression::store( m_balances.elements(), _address, balance(_address) + move(_value) diff --git a/libsolidity/formal/SymbolicState.h b/libsolidity/formal/SymbolicState.h index 087ea9985..f33faf9f2 100644 --- a/libsolidity/formal/SymbolicState.h +++ b/libsolidity/formal/SymbolicState.h @@ -40,18 +40,18 @@ public: /// Blockchain. //@{ /// Value of `this` address. - Expression thisAddress(); + smtutil::Expression thisAddress(); /// @returns the symbolic balance of address `this`. - Expression balance(); + smtutil::Expression balance(); /// @returns the symbolic balance of an address. - Expression balance(Expression _address); + smtutil::Expression balance(smtutil::Expression _address); /// Transfer _value from _from to _to. - void transfer(Expression _from, Expression _to, Expression _value); + void transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value); //@} private: /// Adds _value to _account's balance. - void addBalance(Expression _account, Expression _value); + void addBalance(smtutil::Expression _account, smtutil::Expression _value); EncodingContext& m_context; @@ -63,7 +63,7 @@ private: /// Symbolic balances. SymbolicArrayVariable m_balances{ - std::make_shared(SortProvider::intSort, SortProvider::intSort), + std::make_shared(smtutil::SortProvider::intSort, smtutil::SortProvider::intSort), "balances", m_context }; diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index be6cc1b37..bf4f38daa 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -24,6 +24,7 @@ #include using namespace std; +using namespace solidity::smtutil; namespace solidity::frontend::smt { @@ -334,14 +335,14 @@ bool isStringLiteral(frontend::Type::Category _category) return _category == frontend::Type::Category::StringLiteral; } -Expression minValue(frontend::IntegerType const& _type) +smtutil::Expression minValue(frontend::IntegerType const& _type) { - return Expression(_type.minValue()); + return smtutil::Expression(_type.minValue()); } -Expression maxValue(frontend::IntegerType const& _type) +smtutil::Expression maxValue(frontend::IntegerType const& _type) { - return Expression(_type.maxValue()); + return smtutil::Expression(_type.maxValue()); } void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _context) @@ -349,13 +350,13 @@ void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _c setSymbolicZeroValue(_variable.currentValue(), _variable.type(), _context); } -void setSymbolicZeroValue(Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context) +void setSymbolicZeroValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context) { solAssert(_type, ""); _context.addAssertion(_expr == zeroValue(_type)); } -Expression zeroValue(frontend::TypePointer const& _type) +smtutil::Expression zeroValue(frontend::TypePointer const& _type) { solAssert(_type, ""); if (isSupportedType(_type->category())) @@ -363,28 +364,28 @@ Expression zeroValue(frontend::TypePointer const& _type) if (isNumber(_type->category())) return 0; if (isBool(_type->category())) - return Expression(false); + return smtutil::Expression(false); if (isArray(_type->category()) || isMapping(_type->category())) { auto tupleSort = dynamic_pointer_cast(smtSort(*_type)); solAssert(tupleSort, ""); auto sortSort = make_shared(tupleSort->components.front()); - std::optional zeroArray; + std::optional zeroArray; auto length = bigint(0); if (auto arrayType = dynamic_cast(_type)) { - zeroArray = Expression::const_array(Expression(sortSort), zeroValue(arrayType->baseType())); + zeroArray = smtutil::Expression::const_array(smtutil::Expression(sortSort), zeroValue(arrayType->baseType())); if (!arrayType->isDynamicallySized()) length = bigint(arrayType->length()); } else if (auto mappingType = dynamic_cast(_type)) - zeroArray = Expression::const_array(Expression(sortSort), zeroValue(mappingType->valueType())); + zeroArray = smtutil::Expression::const_array(smtutil::Expression(sortSort), zeroValue(mappingType->valueType())); else solAssert(false, ""); solAssert(zeroArray, ""); - return Expression::tuple_constructor(Expression(_type), vector{*zeroArray, length}); + return smtutil::Expression::tuple_constructor(smtutil::Expression(_type), vector{*zeroArray, length}); } solAssert(false, ""); @@ -398,7 +399,7 @@ void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& setSymbolicUnknownValue(_variable.currentValue(), _variable.type(), _context); } -void setSymbolicUnknownValue(Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context) +void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context) { solAssert(_type, ""); if (isEnum(_type->category())) @@ -417,7 +418,7 @@ void setSymbolicUnknownValue(Expression _expr, frontend::TypePointer const& _typ } } -optional symbolicTypeConversion(TypePointer _from, TypePointer _to) +optional symbolicTypeConversion(TypePointer _from, TypePointer _to) { if (_to && _from) // StringLiterals are encoded as SMT arrays in the generic case, @@ -425,7 +426,7 @@ optional symbolicTypeConversion(TypePointer _from, TypePointer _to) // case they'd need to be encoded as numbers. if (auto strType = dynamic_cast(_from)) if (_to->category() == frontend::Type::Category::FixedBytes) - return smt::Expression(u256(toHex(util::asBytes(strType->value()), util::HexPrefix::Add))); + return smtutil::Expression(u256(toHex(util::asBytes(strType->value()), util::HexPrefix::Add))); return std::nullopt; } diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h index a05d606fe..2e06f4c86 100644 --- a/libsolidity/formal/SymbolicTypes.h +++ b/libsolidity/formal/SymbolicTypes.h @@ -26,14 +26,14 @@ namespace solidity::frontend::smt { /// Returns the SMT sort that models the Solidity type _type. -SortPointer smtSort(frontend::Type const& _type); -std::vector smtSort(std::vector const& _types); +smtutil::SortPointer smtSort(frontend::Type const& _type); +std::vector smtSort(std::vector const& _types); /// If _type has type Function, abstract it to Integer. /// Otherwise return smtSort(_type). -SortPointer smtSortAbstractFunction(frontend::Type const& _type); -std::vector smtSortAbstractFunction(std::vector const& _types); +smtutil::SortPointer smtSortAbstractFunction(frontend::Type const& _type); +std::vector smtSortAbstractFunction(std::vector const& _types); /// Returns the SMT kind that models the Solidity type type category _category. -Kind smtKind(frontend::Type::Category _category); +smtutil::Kind smtKind(frontend::Type::Category _category); /// Returns true if type is fully supported (declaration and operations). bool isSupportedType(frontend::Type::Category _category); @@ -61,14 +61,14 @@ bool isStringLiteral(frontend::Type::Category _category); /// which is true for unsupported types. std::pair> newSymbolicVariable(frontend::Type const& _type, std::string const& _uniqueName, EncodingContext& _context); -Expression minValue(frontend::IntegerType const& _type); -Expression maxValue(frontend::IntegerType const& _type); -Expression zeroValue(frontend::TypePointer const& _type); +smtutil::Expression minValue(frontend::IntegerType const& _type); +smtutil::Expression maxValue(frontend::IntegerType const& _type); +smtutil::Expression zeroValue(frontend::TypePointer const& _type); void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _context); -void setSymbolicZeroValue(Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context); +void setSymbolicZeroValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context); void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& _context); -void setSymbolicUnknownValue(Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context); +void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context); -std::optional symbolicTypeConversion(TypePointer _from, TypePointer _to); +std::optional symbolicTypeConversion(TypePointer _from, TypePointer _to); } diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp index 519588abd..558e7ccd1 100644 --- a/libsolidity/formal/SymbolicVariables.cpp +++ b/libsolidity/formal/SymbolicVariables.cpp @@ -22,6 +22,7 @@ using namespace std; using namespace solidity; +using namespace solidity::smtutil; using namespace solidity::frontend; using namespace solidity::frontend::smt; @@ -55,7 +56,7 @@ SymbolicVariable::SymbolicVariable( solAssert(m_sort, ""); } -smt::Expression SymbolicVariable::currentValue(frontend::TypePointer const&) const +smtutil::Expression SymbolicVariable::currentValue(frontend::TypePointer const&) const { return valueAtIndex(m_ssa->index()); } @@ -65,7 +66,7 @@ string SymbolicVariable::currentName() const return uniqueSymbol(m_ssa->index()); } -smt::Expression SymbolicVariable::valueAtIndex(int _index) const +smtutil::Expression SymbolicVariable::valueAtIndex(int _index) const { return m_context.newVariable(uniqueSymbol(_index), m_sort); } @@ -80,19 +81,19 @@ string SymbolicVariable::uniqueSymbol(unsigned _index) const return m_uniqueName + "_" + to_string(_index); } -smt::Expression SymbolicVariable::resetIndex() +smtutil::Expression SymbolicVariable::resetIndex() { m_ssa->resetIndex(); return currentValue(); } -smt::Expression SymbolicVariable::setIndex(unsigned _index) +smtutil::Expression SymbolicVariable::setIndex(unsigned _index) { m_ssa->setIndex(_index); return currentValue(); } -smt::Expression SymbolicVariable::increaseIndex() +smtutil::Expression SymbolicVariable::increaseIndex() { ++(*m_ssa); return currentValue(); @@ -159,39 +160,39 @@ SymbolicFunctionVariable::SymbolicFunctionVariable( solAssert(m_sort->kind == Kind::Function, ""); } -smt::Expression SymbolicFunctionVariable::currentValue(frontend::TypePointer const& _targetType) const +smtutil::Expression SymbolicFunctionVariable::currentValue(frontend::TypePointer const& _targetType) const { return m_abstract.currentValue(_targetType); } -smt::Expression SymbolicFunctionVariable::currentFunctionValue() const +smtutil::Expression SymbolicFunctionVariable::currentFunctionValue() const { return m_declaration; } -smt::Expression SymbolicFunctionVariable::valueAtIndex(int _index) const +smtutil::Expression SymbolicFunctionVariable::valueAtIndex(int _index) const { return m_abstract.valueAtIndex(_index); } -smt::Expression SymbolicFunctionVariable::functionValueAtIndex(int _index) const +smtutil::Expression SymbolicFunctionVariable::functionValueAtIndex(int _index) const { return SymbolicVariable::valueAtIndex(_index); } -smt::Expression SymbolicFunctionVariable::resetIndex() +smtutil::Expression SymbolicFunctionVariable::resetIndex() { SymbolicVariable::resetIndex(); return m_abstract.resetIndex(); } -smt::Expression SymbolicFunctionVariable::setIndex(unsigned _index) +smtutil::Expression SymbolicFunctionVariable::setIndex(unsigned _index) { SymbolicVariable::setIndex(_index); return m_abstract.setIndex(_index); } -smt::Expression SymbolicFunctionVariable::increaseIndex() +smtutil::Expression SymbolicFunctionVariable::increaseIndex() { ++(*m_ssa); resetDeclaration(); @@ -199,7 +200,7 @@ smt::Expression SymbolicFunctionVariable::increaseIndex() return m_abstract.currentValue(); } -smt::Expression SymbolicFunctionVariable::operator()(vector _arguments) const +smtutil::Expression SymbolicFunctionVariable::operator()(vector _arguments) const { return m_declaration(_arguments); } @@ -246,17 +247,17 @@ vector const& SymbolicTupleVariable::components() return tupleSort->components; } -smt::Expression SymbolicTupleVariable::component( +smtutil::Expression SymbolicTupleVariable::component( size_t _index, TypePointer _fromType, TypePointer _toType ) { - optional conversion = symbolicTypeConversion(_fromType, _toType); + optional conversion = symbolicTypeConversion(_fromType, _toType); if (conversion) return *conversion; - return smt::Expression::tuple_get(currentValue(), _index); + return smtutil::Expression::tuple_get(currentValue(), _index); } SymbolicArrayVariable::SymbolicArrayVariable( @@ -294,26 +295,26 @@ SymbolicArrayVariable::SymbolicArrayVariable( solAssert(m_sort->kind == Kind::Array, ""); } -smt::Expression SymbolicArrayVariable::currentValue(frontend::TypePointer const& _targetType) const +smtutil::Expression SymbolicArrayVariable::currentValue(frontend::TypePointer const& _targetType) const { - optional conversion = symbolicTypeConversion(m_originalType, _targetType); + optional conversion = symbolicTypeConversion(m_originalType, _targetType); if (conversion) return *conversion; return m_pair.currentValue(); } -smt::Expression SymbolicArrayVariable::valueAtIndex(int _index) const +smtutil::Expression SymbolicArrayVariable::valueAtIndex(int _index) const { return m_pair.valueAtIndex(_index); } -smt::Expression SymbolicArrayVariable::elements() +smtutil::Expression SymbolicArrayVariable::elements() { return m_pair.component(0); } -smt::Expression SymbolicArrayVariable::length() +smtutil::Expression SymbolicArrayVariable::length() { return m_pair.component(1); } diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h index 46d3520cf..a7c0bd170 100644 --- a/libsolidity/formal/SymbolicVariables.h +++ b/libsolidity/formal/SymbolicVariables.h @@ -43,7 +43,7 @@ public: EncodingContext& _context ); SymbolicVariable( - SortPointer _sort, + smtutil::SortPointer _sort, std::string _uniqueName, EncodingContext& _context ); @@ -52,14 +52,14 @@ public: virtual ~SymbolicVariable() = default; - virtual Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const; + virtual smtutil::Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const; std::string currentName() const; - virtual Expression valueAtIndex(int _index) const; + virtual smtutil::Expression valueAtIndex(int _index) const; virtual std::string nameAtIndex(int _index) const; - virtual Expression resetIndex(); - virtual Expression setIndex(unsigned _index); - virtual Expression increaseIndex(); - virtual Expression operator()(std::vector /*_arguments*/) const + virtual smtutil::Expression resetIndex(); + virtual smtutil::Expression setIndex(unsigned _index); + virtual smtutil::Expression increaseIndex(); + virtual smtutil::Expression operator()(std::vector /*_arguments*/) const { solAssert(false, "Function application to non-function."); } @@ -67,7 +67,7 @@ public: unsigned index() const { return m_ssa->index(); } unsigned& index() { return m_ssa->index(); } - SortPointer const& sort() const { return m_sort; } + smtutil::SortPointer const& sort() const { return m_sort; } frontend::TypePointer const& type() const { return m_type; } frontend::TypePointer const& originalType() const { return m_originalType; } @@ -75,7 +75,7 @@ protected: std::string uniqueSymbol(unsigned _index) const; /// SMT sort. - SortPointer m_sort; + smtutil::SortPointer m_sort; /// Solidity type, used for size and range in number types. frontend::TypePointer m_type; /// Solidity original type, used for type conversion if necessary. @@ -155,33 +155,33 @@ public: EncodingContext& _context ); SymbolicFunctionVariable( - SortPointer _sort, + smtutil::SortPointer _sort, std::string _uniqueName, EncodingContext& _context ); - Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override; + smtutil::Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override; // Explicit request the function declaration. - Expression currentFunctionValue() const; + smtutil::Expression currentFunctionValue() const; - Expression valueAtIndex(int _index) const override; + smtutil::Expression valueAtIndex(int _index) const override; // Explicit request the function declaration. - Expression functionValueAtIndex(int _index) const; + smtutil::Expression functionValueAtIndex(int _index) const; - Expression resetIndex() override; - Expression setIndex(unsigned _index) override; - Expression increaseIndex() override; + smtutil::Expression resetIndex() override; + smtutil::Expression setIndex(unsigned _index) override; + smtutil::Expression increaseIndex() override; - Expression operator()(std::vector _arguments) const override; + smtutil::Expression operator()(std::vector _arguments) const override; private: /// Creates a new function declaration. void resetDeclaration(); /// Stores the current function declaration. - Expression m_declaration; + smtutil::Expression m_declaration; /// Abstract representation. SymbolicIntVariable m_abstract{ @@ -217,13 +217,13 @@ public: EncodingContext& _context ); SymbolicTupleVariable( - SortPointer _sort, + smtutil::SortPointer _sort, std::string _uniqueName, EncodingContext& _context ); - std::vector const& components(); - Expression component( + std::vector const& components(); + smtutil::Expression component( size_t _index, TypePointer _fromType = nullptr, TypePointer _toType = nullptr @@ -243,22 +243,22 @@ public: EncodingContext& _context ); SymbolicArrayVariable( - SortPointer _sort, + smtutil::SortPointer _sort, std::string _uniqueName, EncodingContext& _context ); SymbolicArrayVariable(SymbolicArrayVariable&&) = default; - Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override; - Expression valueAtIndex(int _index) const override; - Expression resetIndex() override { SymbolicVariable::resetIndex(); return m_pair.resetIndex(); } - Expression setIndex(unsigned _index) override { SymbolicVariable::setIndex(_index); return m_pair.setIndex(_index); } - Expression increaseIndex() override { SymbolicVariable::increaseIndex(); return m_pair.increaseIndex(); } - Expression elements(); - Expression length(); + smtutil::Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override; + smtutil::Expression valueAtIndex(int _index) const override; + smtutil::Expression resetIndex() override { SymbolicVariable::resetIndex(); return m_pair.resetIndex(); } + smtutil::Expression setIndex(unsigned _index) override { SymbolicVariable::setIndex(_index); return m_pair.setIndex(_index); } + smtutil::Expression increaseIndex() override { SymbolicVariable::increaseIndex(); return m_pair.increaseIndex(); } + smtutil::Expression elements(); + smtutil::Expression length(); - SortPointer tupleSort() { return m_pair.sort(); } + smtutil::SortPointer tupleSort() { return m_pair.sort(); } private: SymbolicTupleVariable m_pair; diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp index 558c262d0..cf67d2d7e 100644 --- a/libsolidity/interface/CompilerStack.cpp +++ b/libsolidity/interface/CompilerStack.cpp @@ -82,7 +82,7 @@ static int g_compilerStackCounts = 0; CompilerStack::CompilerStack(ReadCallback::Callback _readFile): m_readFile{std::move(_readFile)}, - m_enabledSMTSolvers{smt::SMTSolverChoice::All()}, + m_enabledSMTSolvers{smtutil::SMTSolverChoice::All()}, m_generateIR{false}, m_generateEwasm{false}, m_errorList{}, @@ -136,7 +136,7 @@ void CompilerStack::setEVMVersion(langutil::EVMVersion _version) m_evmVersion = _version; } -void CompilerStack::setSMTSolverChoice(smt::SMTSolverChoice _enabledSMTSolvers) +void CompilerStack::setSMTSolverChoice(smtutil::SMTSolverChoice _enabledSMTSolvers) { if (m_stackState >= ParsingPerformed) BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set enabled SMT solvers before parsing.")); @@ -205,7 +205,7 @@ void CompilerStack::reset(bool _keepSettings) m_remappings.clear(); m_libraries.clear(); m_evmVersion = langutil::EVMVersion(); - m_enabledSMTSolvers = smt::SMTSolverChoice::All(); + m_enabledSMTSolvers = smtutil::SMTSolverChoice::All(); m_generateIR = false; m_generateEwasm = false; m_revertStrings = RevertStrings::Default; diff --git a/libsolidity/interface/CompilerStack.h b/libsolidity/interface/CompilerStack.h index fbd32b382..bbf68f225 100644 --- a/libsolidity/interface/CompilerStack.h +++ b/libsolidity/interface/CompilerStack.h @@ -164,7 +164,7 @@ public: void setEVMVersion(langutil::EVMVersion _version = langutil::EVMVersion{}); /// Set which SMT solvers should be enabled. - void setSMTSolverChoice(smt::SMTSolverChoice _enabledSolvers); + void setSMTSolverChoice(smtutil::SMTSolverChoice _enabledSolvers); /// Sets the requested contract names by source. /// If empty, no filtering is performed and every contract @@ -434,7 +434,7 @@ private: OptimiserSettings m_optimiserSettings; RevertStrings m_revertStrings = RevertStrings::Default; langutil::EVMVersion m_evmVersion; - smt::SMTSolverChoice m_enabledSMTSolvers; + smtutil::SMTSolverChoice m_enabledSMTSolvers; std::map> m_requestedContractNames; bool m_generateIR; bool m_generateEwasm; diff --git a/test/libsolidity/SMTCheckerTest.cpp b/test/libsolidity/SMTCheckerTest.cpp index 28c98ffab..7daa6f182 100644 --- a/test/libsolidity/SMTCheckerTest.cpp +++ b/test/libsolidity/SMTCheckerTest.cpp @@ -30,13 +30,13 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename, langutil::EVMVersion _ev { auto const& choice = m_reader.stringSetting("SMTSolvers", "any"); if (choice == "any") - m_enabledSolvers = smt::SMTSolverChoice::All(); + m_enabledSolvers = smtutil::SMTSolverChoice::All(); else if (choice == "z3") - m_enabledSolvers = smt::SMTSolverChoice::Z3(); + m_enabledSolvers = smtutil::SMTSolverChoice::Z3(); else if (choice == "cvc4") - m_enabledSolvers = smt::SMTSolverChoice::CVC4(); + m_enabledSolvers = smtutil::SMTSolverChoice::CVC4(); else if (choice == "none") - m_enabledSolvers = smt::SMTSolverChoice::None(); + m_enabledSolvers = smtutil::SMTSolverChoice::None(); else BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT solver choice.")); diff --git a/test/libsolidity/SMTCheckerTest.h b/test/libsolidity/SMTCheckerTest.h index 674564f57..34f526cd9 100644 --- a/test/libsolidity/SMTCheckerTest.h +++ b/test/libsolidity/SMTCheckerTest.h @@ -41,7 +41,7 @@ protected: /// This is set via option SMTSolvers in the test. /// The possible options are `all`, `z3`, `cvc4`, `none`, /// where if none is given the default used option is `all`. - smt::SMTSolverChoice m_enabledSolvers; + smtutil::SMTSolverChoice m_enabledSolvers; }; } From 7a91c9b971ad8d2bb67aaa00374abeb4acda39f4 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 19 May 2020 14:23:41 +0200 Subject: [PATCH 4/6] Remove Type from SolverInterface --- libsmtutil/SolverInterface.h | 7 +------ libsolidity/formal/SMTEncoder.cpp | 3 ++- libsolidity/formal/SymbolicTypes.cpp | 5 ++++- 3 files changed, 7 insertions(+), 8 deletions(-) diff --git a/libsmtutil/SolverInterface.h b/libsmtutil/SolverInterface.h index 260dcc7a7..0dd8e5bcd 100644 --- a/libsmtutil/SolverInterface.h +++ b/libsmtutil/SolverInterface.h @@ -19,7 +19,6 @@ #include -#include #include #include #include @@ -54,17 +53,13 @@ enum class CheckResult SATISFIABLE, UNSATISFIABLE, UNKNOWN, CONFLICTING, ERROR }; -// Forward declaration. -SortPointer smtSort(frontend::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(frontend::TypePointer _type): Expression(_type->toString(true), {}, std::make_shared(smtSort(*_type))) {} - explicit Expression(std::shared_ptr _sort): Expression("", {}, _sort) {} + explicit Expression(std::shared_ptr _sort, std::string _name = ""): Expression(std::move(_name), {}, _sort) {} 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) {} diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index afaf8ea7e..a8e0e32b7 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -1061,8 +1061,9 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smtutil::Expressi { auto symbArray = dynamic_pointer_cast(m_context.expression(*base)); solAssert(symbArray, ""); + auto baseType = base->annotation().type; toStore = smtutil::Expression::tuple_constructor( - smtutil::Expression(base->annotation().type), + smtutil::Expression(make_shared(smt::smtSort(*baseType)), baseType->toString(true)), {smtutil::Expression::store(symbArray->elements(), expr(*indexAccess->indexExpression()), toStore), symbArray->length()} ); indexAccess = base; diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index bf4f38daa..38f72cb66 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -385,7 +385,10 @@ smtutil::Expression zeroValue(frontend::TypePointer const& _type) solAssert(false, ""); solAssert(zeroArray, ""); - return smtutil::Expression::tuple_constructor(smtutil::Expression(_type), vector{*zeroArray, length}); + return smtutil::Expression::tuple_constructor( + smtutil::Expression(std::make_shared(smtSort(*_type)), _type->toString(true)), + vector{*zeroArray, length} + ); } solAssert(false, ""); From 25de3975ce6747c249bcabdbc4aeae37184f1579 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 19 May 2020 14:52:31 +0200 Subject: [PATCH 5/6] Add SMTLogicException --- libsmtutil/CHCSmtLib2Interface.cpp | 12 +++---- libsmtutil/CMakeLists.txt | 1 + libsmtutil/CVC4Interface.cpp | 35 ++++++++++---------- libsmtutil/Exceptions.h | 31 ++++++++++++++++++ libsmtutil/SMTLib2Interface.cpp | 30 +++++++++--------- libsmtutil/SMTLib2Interface.h | 2 +- libsmtutil/SMTPortfolio.cpp | 6 ++-- libsmtutil/SolverInterface.h | 51 +++++++++++++++--------------- libsmtutil/Sorts.h | 28 ++++++++-------- libsmtutil/Z3CHCInterface.cpp | 3 +- libsmtutil/Z3Interface.cpp | 27 ++++++++-------- 11 files changed, 127 insertions(+), 99 deletions(-) create mode 100644 libsmtutil/Exceptions.h diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp index 960e75ead..8116ea2a2 100644 --- a/libsmtutil/CHCSmtLib2Interface.cpp +++ b/libsmtutil/CHCSmtLib2Interface.cpp @@ -53,8 +53,8 @@ void CHCSmtLib2Interface::reset() void CHCSmtLib2Interface::registerRelation(Expression const& _expr) { - solAssert(_expr.sort, ""); - solAssert(_expr.sort->kind == Kind::Function, ""); + smtAssert(_expr.sort, ""); + smtAssert(_expr.sort->kind == Kind::Function, ""); if (!m_variables.count(_expr.name)) { auto fSort = dynamic_pointer_cast(_expr.sort); @@ -112,7 +112,7 @@ pair> CHCSmtLib2Interface::query(Expression const& _ void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const& _sort) { - solAssert(_sort, ""); + smtAssert(_sort, ""); if (_sort->kind == Kind::Function) declareFunction(_name, _sort); else if (!m_variables.count(_name)) @@ -124,13 +124,13 @@ void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const void CHCSmtLib2Interface::declareFunction(string const& _name, SortPointer const& _sort) { - solAssert(_sort, ""); - solAssert(_sort->kind == Kind::Function, ""); + smtAssert(_sort, ""); + smtAssert(_sort->kind == Kind::Function, ""); // TODO Use domain and codomain as key as well if (!m_variables.count(_name)) { auto fSort = dynamic_pointer_cast(_sort); - solAssert(fSort->codomain, ""); + smtAssert(fSort->codomain, ""); string domain = m_smtlib2->toSmtLibSort(fSort->domain); string codomain = m_smtlib2->toSmtLibSort(*fSort->codomain); m_variables.insert(_name); diff --git a/libsmtutil/CMakeLists.txt b/libsmtutil/CMakeLists.txt index e46b80df6..62b52f5c6 100644 --- a/libsmtutil/CMakeLists.txt +++ b/libsmtutil/CMakeLists.txt @@ -1,6 +1,7 @@ set(sources CHCSmtLib2Interface.cpp CHCSmtLib2Interface.h + Exceptions.h SMTLib2Interface.cpp SMTLib2Interface.h SMTPortfolio.cpp diff --git a/libsmtutil/CVC4Interface.cpp b/libsmtutil/CVC4Interface.cpp index 3a678429a..4c1ef378a 100644 --- a/libsmtutil/CVC4Interface.cpp +++ b/libsmtutil/CVC4Interface.cpp @@ -17,7 +17,6 @@ #include -#include #include using namespace std; @@ -51,7 +50,7 @@ void CVC4Interface::pop() void CVC4Interface::declareVariable(string const& _name, SortPointer const& _sort) { - solAssert(_sort, ""); + smtAssert(_sort, ""); m_variables[_name] = m_context.mkVar(_name.c_str(), cvc4Sort(*_sort)); } @@ -63,19 +62,19 @@ void CVC4Interface::addAssertion(Expression const& _expr) } catch (CVC4::TypeCheckingException const& _e) { - solAssert(false, _e.what()); + smtAssert(false, _e.what()); } catch (CVC4::LogicException const& _e) { - solAssert(false, _e.what()); + smtAssert(false, _e.what()); } catch (CVC4::UnsafeInterruptException const& _e) { - solAssert(false, _e.what()); + smtAssert(false, _e.what()); } catch (CVC4::Exception const& _e) { - solAssert(false, _e.what()); + smtAssert(false, _e.what()); } } @@ -97,7 +96,7 @@ pair> CVC4Interface::check(vector const& result = CheckResult::UNKNOWN; break; default: - solAssert(false, ""); + smtAssert(false, ""); } if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty()) @@ -147,15 +146,15 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr) } catch (CVC4::TypeCheckingException const& _e) { - solAssert(false, _e.what()); + smtAssert(false, _e.what()); } catch (CVC4::Exception const& _e) { - solAssert(false, _e.what()); + smtAssert(false, _e.what()); } } - solAssert(_expr.hasCorrectArity(), ""); + smtAssert(_expr.hasCorrectArity(), ""); if (n == "ite") return arguments[0].iteExpr(arguments[1], arguments[2]); else if (n == "not") @@ -193,13 +192,13 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr) else if (n == "const_array") { shared_ptr sortSort = std::dynamic_pointer_cast(_expr.arguments[0].sort); - solAssert(sortSort, ""); + smtAssert(sortSort, ""); return m_context.mkConst(CVC4::ArrayStoreAll(cvc4Sort(*sortSort->inner), arguments[1])); } else if (n == "tuple_get") { shared_ptr tupleSort = std::dynamic_pointer_cast(_expr.arguments[0].sort); - solAssert(tupleSort, ""); + smtAssert(tupleSort, ""); CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components)); CVC4::Datatype const& dt = tt.getDatatype(); size_t index = std::stoi(_expr.arguments[1].name); @@ -209,25 +208,25 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr) else if (n == "tuple_constructor") { shared_ptr tupleSort = std::dynamic_pointer_cast(_expr.sort); - solAssert(tupleSort, ""); + smtAssert(tupleSort, ""); CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components)); CVC4::Datatype const& dt = tt.getDatatype(); CVC4::Expr c = dt[0].getConstructor(); return m_context.mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, c, arguments); } - solAssert(false, ""); + smtAssert(false, ""); } catch (CVC4::TypeCheckingException const& _e) { - solAssert(false, _e.what()); + smtAssert(false, _e.what()); } catch (CVC4::Exception const& _e) { - solAssert(false, _e.what()); + smtAssert(false, _e.what()); } - solAssert(false, ""); + smtAssert(false, ""); } CVC4::Type CVC4Interface::cvc4Sort(Sort const& _sort) @@ -256,7 +255,7 @@ CVC4::Type CVC4Interface::cvc4Sort(Sort const& _sort) default: break; } - solAssert(false, ""); + smtAssert(false, ""); // Cannot be reached. return m_context.integerType(); } diff --git a/libsmtutil/Exceptions.h b/libsmtutil/Exceptions.h new file mode 100644 index 000000000..6321c4f6a --- /dev/null +++ b/libsmtutil/Exceptions.h @@ -0,0 +1,31 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see . +*/ + +#pragma once + +#include +#include + +namespace solidity::smtutil +{ + +struct SMTLogicError: virtual util::Exception {}; + +#define smtAssert(CONDITION, DESCRIPTION) \ + assertThrow(CONDITION, SMTLogicError, DESCRIPTION) + +} diff --git a/libsmtutil/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp index a9083a291..4e81444fe 100644 --- a/libsmtutil/SMTLib2Interface.cpp +++ b/libsmtutil/SMTLib2Interface.cpp @@ -63,13 +63,13 @@ void SMTLib2Interface::push() void SMTLib2Interface::pop() { - solAssert(!m_accumulatedOutput.empty(), ""); + smtAssert(!m_accumulatedOutput.empty(), ""); m_accumulatedOutput.pop_back(); } void SMTLib2Interface::declareVariable(string const& _name, SortPointer const& _sort) { - solAssert(_sort, ""); + smtAssert(_sort, ""); if (_sort->kind == Kind::Function) declareFunction(_name, _sort); else if (!m_variables.count(_name)) @@ -81,8 +81,8 @@ void SMTLib2Interface::declareVariable(string const& _name, SortPointer const& _ void SMTLib2Interface::declareFunction(string const& _name, SortPointer const& _sort) { - solAssert(_sort, ""); - solAssert(_sort->kind == Kind::Function, ""); + smtAssert(_sort, ""); + smtAssert(_sort->kind == Kind::Function, ""); // TODO Use domain and codomain as key as well if (!m_variables.count(_name)) { @@ -139,26 +139,26 @@ string SMTLib2Interface::toSExpr(Expression const& _expr) std::string sexpr = "("; if (_expr.name == "const_array") { - solAssert(_expr.arguments.size() == 2, ""); + smtAssert(_expr.arguments.size() == 2, ""); auto sortSort = std::dynamic_pointer_cast(_expr.arguments.at(0).sort); - solAssert(sortSort, ""); + smtAssert(sortSort, ""); auto arraySort = dynamic_pointer_cast(sortSort->inner); - solAssert(arraySort, ""); + smtAssert(arraySort, ""); sexpr += "(as const " + toSmtLibSort(*arraySort) + ") "; sexpr += toSExpr(_expr.arguments.at(1)); } else if (_expr.name == "tuple_get") { - solAssert(_expr.arguments.size() == 2, ""); + smtAssert(_expr.arguments.size() == 2, ""); auto tupleSort = dynamic_pointer_cast(_expr.arguments.at(0).sort); unsigned index = std::stoi(_expr.arguments.at(1).name); - solAssert(index < tupleSort->members.size(), ""); + smtAssert(index < tupleSort->members.size(), ""); sexpr += "|" + tupleSort->members.at(index) + "| " + toSExpr(_expr.arguments.at(0)); } else if (_expr.name == "tuple_constructor") { auto tupleSort = dynamic_pointer_cast(_expr.sort); - solAssert(tupleSort, ""); + smtAssert(tupleSort, ""); sexpr += "|" + tupleSort->name + "|"; for (auto const& arg: _expr.arguments) sexpr += " " + toSExpr(arg); @@ -184,7 +184,7 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort) case Kind::Array: { auto const& arraySort = dynamic_cast(_sort); - solAssert(arraySort.domain && arraySort.range, ""); + smtAssert(arraySort.domain && arraySort.range, ""); return "(Array " + toSmtLibSort(*arraySort.domain) + ' ' + toSmtLibSort(*arraySort.range) + ')'; } case Kind::Tuple: @@ -195,7 +195,7 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort) { m_userSorts.insert(tupleName); string decl("(declare-datatypes ((" + tupleName + " 0)) (((" + tupleName); - solAssert(tupleSort.members.size() == tupleSort.components.size(), ""); + smtAssert(tupleSort.members.size() == tupleSort.components.size(), ""); for (unsigned i = 0; i < tupleSort.members.size(); ++i) decl += " (|" + tupleSort.members.at(i) + "| " + toSmtLibSort(*tupleSort.components.at(i)) + ")"; decl += "))))"; @@ -205,7 +205,7 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort) return tupleName; } default: - solAssert(false, "Invalid SMT sort"); + smtAssert(false, "Invalid SMT sort"); } } @@ -220,7 +220,7 @@ string SMTLib2Interface::toSmtLibSort(vector const& _sorts) void SMTLib2Interface::write(string _data) { - solAssert(!m_accumulatedOutput.empty(), ""); + smtAssert(!m_accumulatedOutput.empty(), ""); m_accumulatedOutput.back() += move(_data) + "\n"; } @@ -235,7 +235,7 @@ string SMTLib2Interface::checkSatAndGetValuesCommand(vector const& _ for (size_t i = 0; i < _expressionsToEvaluate.size(); i++) { auto const& e = _expressionsToEvaluate.at(i); - solAssert(e.sort->kind == Kind::Int || e.sort->kind == Kind::Bool, "Invalid sort for expression to evaluate."); + smtAssert(e.sort->kind == Kind::Int || e.sort->kind == Kind::Bool, "Invalid sort for expression to evaluate."); command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + (e.sort->kind == Kind::Int ? "Int" : "Bool") + ")\n"; command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n"; } diff --git a/libsmtutil/SMTLib2Interface.h b/libsmtutil/SMTLib2Interface.h index 6d97adac2..dfb32a959 100644 --- a/libsmtutil/SMTLib2Interface.h +++ b/libsmtutil/SMTLib2Interface.h @@ -20,7 +20,7 @@ #include #include -#include + #include #include diff --git a/libsmtutil/SMTPortfolio.cpp b/libsmtutil/SMTPortfolio.cpp index dc7e69fa1..80c1a4750 100644 --- a/libsmtutil/SMTPortfolio.cpp +++ b/libsmtutil/SMTPortfolio.cpp @@ -68,7 +68,7 @@ void SMTPortfolio::pop() void SMTPortfolio::declareVariable(string const& _name, SortPointer const& _sort) { - solAssert(_sort, ""); + smtAssert(_sort, ""); for (auto const& s: m_solvers) s->declareVariable(_name, _sort); } @@ -141,8 +141,8 @@ vector SMTPortfolio::unhandledQueries() { // This code assumes that the constructor guarantees that // SmtLib2Interface is in position 0. - solAssert(!m_solvers.empty(), ""); - solAssert(dynamic_cast(m_solvers.front().get()), ""); + smtAssert(!m_solvers.empty(), ""); + smtAssert(dynamic_cast(m_solvers.front().get()), ""); return m_solvers.front()->unhandledQueries(); } diff --git a/libsmtutil/SolverInterface.h b/libsmtutil/SolverInterface.h index 0dd8e5bcd..13fcae4f2 100644 --- a/libsmtutil/SolverInterface.h +++ b/libsmtutil/SolverInterface.h @@ -17,11 +17,10 @@ #pragma once +#include #include -#include #include -#include #include #include @@ -75,7 +74,7 @@ public: if (name == "tuple_constructor") { auto tupleSort = std::dynamic_pointer_cast(sort); - solAssert(tupleSort, ""); + smtAssert(tupleSort, ""); return arguments.size() == tupleSort->components.size(); } @@ -105,7 +104,7 @@ public: static Expression ite(Expression _condition, Expression _trueValue, Expression _falseValue) { - solAssert(*_trueValue.sort == *_falseValue.sort, ""); + smtAssert(*_trueValue.sort == *_falseValue.sort, ""); SortPointer sort = _trueValue.sort; return Expression("ite", std::vector{ std::move(_condition), std::move(_trueValue), std::move(_falseValue) @@ -125,11 +124,11 @@ public: /// select is the SMT representation of an array index access. static Expression select(Expression _array, Expression _index) { - solAssert(_array.sort->kind == Kind::Array, ""); + smtAssert(_array.sort->kind == Kind::Array, ""); std::shared_ptr arraySort = std::dynamic_pointer_cast(_array.sort); - solAssert(arraySort, ""); - solAssert(_index.sort, ""); - solAssert(*arraySort->domain == *_index.sort, ""); + smtAssert(arraySort, ""); + smtAssert(_index.sort, ""); + smtAssert(*arraySort->domain == *_index.sort, ""); return Expression( "select", std::vector{std::move(_array), std::move(_index)}, @@ -142,11 +141,11 @@ public: static Expression store(Expression _array, Expression _index, Expression _element) { auto arraySort = std::dynamic_pointer_cast(_array.sort); - solAssert(arraySort, ""); - solAssert(_index.sort, ""); - solAssert(_element.sort, ""); - solAssert(*arraySort->domain == *_index.sort, ""); - solAssert(*arraySort->range == *_element.sort, ""); + smtAssert(arraySort, ""); + smtAssert(_index.sort, ""); + smtAssert(_element.sort, ""); + smtAssert(*arraySort->domain == *_index.sort, ""); + smtAssert(*arraySort->range == *_element.sort, ""); return Expression( "store", std::vector{std::move(_array), std::move(_index), std::move(_element)}, @@ -156,12 +155,12 @@ public: static Expression const_array(Expression _sort, Expression _value) { - solAssert(_sort.sort->kind == Kind::Sort, ""); + smtAssert(_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, ""); + smtAssert(sortSort && arraySort, ""); + smtAssert(_value.sort, ""); + smtAssert(*arraySort->range == *_value.sort, ""); return Expression( "const_array", std::vector{std::move(_sort), std::move(_value)}, @@ -171,10 +170,10 @@ public: static Expression tuple_get(Expression _tuple, size_t _index) { - solAssert(_tuple.sort->kind == Kind::Tuple, ""); + smtAssert(_tuple.sort->kind == Kind::Tuple, ""); std::shared_ptr tupleSort = std::dynamic_pointer_cast(_tuple.sort); - solAssert(tupleSort, ""); - solAssert(_index < tupleSort->components.size(), ""); + smtAssert(tupleSort, ""); + smtAssert(_index < tupleSort->components.size(), ""); return Expression( "tuple_get", std::vector{std::move(_tuple), Expression(_index)}, @@ -184,11 +183,11 @@ public: static Expression tuple_constructor(Expression _tuple, std::vector _arguments) { - solAssert(_tuple.sort->kind == Kind::Sort, ""); + smtAssert(_tuple.sort->kind == Kind::Sort, ""); auto sortSort = std::dynamic_pointer_cast(_tuple.sort); auto tupleSort = std::dynamic_pointer_cast(sortSort->inner); - solAssert(tupleSort, ""); - solAssert(_arguments.size() == tupleSort->components.size(), ""); + smtAssert(tupleSort, ""); + smtAssert(_arguments.size() == tupleSort->components.size(), ""); return Expression( "tuple_constructor", std::move(_arguments), @@ -254,12 +253,12 @@ public: } Expression operator()(std::vector _arguments) const { - solAssert( + smtAssert( sort->kind == Kind::Function, "Attempted function application to non-function." ); auto fSort = dynamic_cast(sort.get()); - solAssert(fSort, ""); + smtAssert(fSort, ""); return Expression(name, std::move(_arguments), fSort->codomain); } @@ -297,7 +296,7 @@ public: Expression newVariable(std::string _name, SortPointer const& _sort) { // Subclasses should do something here - solAssert(_sort, ""); + smtAssert(_sort, ""); declareVariable(_name, _sort); return Expression(std::move(_name), {}, _sort); } diff --git a/libsmtutil/Sorts.h b/libsmtutil/Sorts.h index 903db1907..228dd057b 100644 --- a/libsmtutil/Sorts.h +++ b/libsmtutil/Sorts.h @@ -17,9 +17,9 @@ #pragma once -#include +#include + #include -#include #include #include @@ -57,7 +57,7 @@ struct FunctionSort: public Sort if (!Sort::operator==(_other)) return false; auto _otherFunction = dynamic_cast(&_other); - solAssert(_otherFunction, ""); + smtAssert(_otherFunction, ""); if (domain.size() != _otherFunction->domain.size()) return false; if (!std::equal( @@ -67,8 +67,8 @@ struct FunctionSort: public Sort [&](SortPointer _a, SortPointer _b) { return *_a == *_b; } )) return false; - solAssert(codomain, ""); - solAssert(_otherFunction->codomain, ""); + smtAssert(codomain, ""); + smtAssert(_otherFunction->codomain, ""); return *codomain == *_otherFunction->codomain; } @@ -87,11 +87,11 @@ struct ArraySort: public Sort if (!Sort::operator==(_other)) return false; auto _otherArray = dynamic_cast(&_other); - solAssert(_otherArray, ""); - solAssert(_otherArray->domain, ""); - solAssert(_otherArray->range, ""); - solAssert(domain, ""); - solAssert(range, ""); + smtAssert(_otherArray, ""); + smtAssert(_otherArray->domain, ""); + smtAssert(_otherArray->range, ""); + smtAssert(domain, ""); + smtAssert(range, ""); return *domain == *_otherArray->domain && *range == *_otherArray->range; } @@ -107,9 +107,9 @@ struct SortSort: public Sort if (!Sort::operator==(_other)) return false; auto _otherSort = dynamic_cast(&_other); - solAssert(_otherSort, ""); - solAssert(_otherSort->inner, ""); - solAssert(inner, ""); + smtAssert(_otherSort, ""); + smtAssert(_otherSort->inner, ""); + smtAssert(inner, ""); return *inner == *_otherSort->inner; } @@ -134,7 +134,7 @@ struct TupleSort: public Sort if (!Sort::operator==(_other)) return false; auto _otherTuple = dynamic_cast(&_other); - solAssert(_otherTuple, ""); + smtAssert(_otherTuple, ""); if (name != _otherTuple->name) return false; if (members != _otherTuple->members) diff --git a/libsmtutil/Z3CHCInterface.cpp b/libsmtutil/Z3CHCInterface.cpp index 8346ea647..d2bce2f1c 100644 --- a/libsmtutil/Z3CHCInterface.cpp +++ b/libsmtutil/Z3CHCInterface.cpp @@ -17,7 +17,6 @@ #include -#include #include using namespace std; @@ -48,7 +47,7 @@ Z3CHCInterface::Z3CHCInterface(): void Z3CHCInterface::declareVariable(string const& _name, SortPointer const& _sort) { - solAssert(_sort, ""); + smtAssert(_sort, ""); m_z3Interface->declareVariable(_name, _sort); } diff --git a/libsmtutil/Z3Interface.cpp b/libsmtutil/Z3Interface.cpp index 3c4ea16ed..b42bc4765 100644 --- a/libsmtutil/Z3Interface.cpp +++ b/libsmtutil/Z3Interface.cpp @@ -17,7 +17,6 @@ #include -#include #include using namespace std; @@ -50,7 +49,7 @@ void Z3Interface::pop() void Z3Interface::declareVariable(string const& _name, SortPointer const& _sort) { - solAssert(_sort, ""); + smtAssert(_sort, ""); if (_sort->kind == Kind::Function) declareFunction(_name, *_sort); else if (m_constants.count(_name)) @@ -61,7 +60,7 @@ void Z3Interface::declareVariable(string const& _name, SortPointer const& _sort) void Z3Interface::declareFunction(string const& _name, Sort const& _sort) { - solAssert(_sort.kind == Kind::Function, ""); + smtAssert(_sort.kind == Kind::Function, ""); FunctionSort fSort = dynamic_cast(_sort); if (m_functions.count(_name)) m_functions.at(_name) = m_context.function(_name.c_str(), z3Sort(fSort.domain), z3Sort(*fSort.codomain)); @@ -124,7 +123,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) return m_functions.at(n)(arguments); else if (m_constants.count(n)) { - solAssert(arguments.empty(), ""); + smtAssert(arguments.empty(), ""); return m_constants.at(n); } else if (arguments.empty()) @@ -136,7 +135,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) else if (_expr.sort->kind == Kind::Sort) { auto sortSort = dynamic_pointer_cast(_expr.sort); - solAssert(sortSort, ""); + smtAssert(sortSort, ""); return m_context.constant(n.c_str(), z3Sort(*sortSort->inner)); } else @@ -146,11 +145,11 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) } catch (z3::exception const& _e) { - solAssert(false, _e.msg()); + smtAssert(false, _e.msg()); } } - solAssert(_expr.hasCorrectArity(), ""); + smtAssert(_expr.hasCorrectArity(), ""); if (n == "ite") return z3::ite(arguments[0], arguments[1], arguments[2]); else if (n == "not") @@ -188,9 +187,9 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) else if (n == "const_array") { shared_ptr sortSort = std::dynamic_pointer_cast(_expr.arguments[0].sort); - solAssert(sortSort, ""); + smtAssert(sortSort, ""); auto arraySort = dynamic_pointer_cast(sortSort->inner); - solAssert(arraySort && arraySort->domain, ""); + smtAssert(arraySort && arraySort->domain, ""); return z3::const_array(z3Sort(*arraySort->domain), arguments[1]); } else if (n == "tuple_get") @@ -201,21 +200,21 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) else if (n == "tuple_constructor") { auto constructor = z3::func_decl(m_context, Z3_get_tuple_sort_mk_decl(m_context, z3Sort(*_expr.sort))); - solAssert(constructor.arity() == arguments.size(), ""); + smtAssert(constructor.arity() == arguments.size(), ""); z3::expr_vector args(m_context); for (auto const& arg: arguments) args.push_back(arg); return constructor(args); } - solAssert(false, ""); + smtAssert(false, ""); } catch (z3::exception const& _e) { - solAssert(false, _e.msg()); + smtAssert(false, _e.msg()); } - solAssert(false, ""); + smtAssert(false, ""); } z3::sort Z3Interface::z3Sort(Sort const& _sort) @@ -256,7 +255,7 @@ z3::sort Z3Interface::z3Sort(Sort const& _sort) default: break; } - solAssert(false, ""); + smtAssert(false, ""); // Cannot be reached. return m_context.int_sort(); } From 0eb067ae4fec6af4faa2a73bdbf2f36b93bd54e0 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 20 May 2020 12:55:12 +0200 Subject: [PATCH 6/6] Add SMTLogicError exception catches --- libsolidity/interface/StandardCompiler.cpp | 11 +++++++++++ solc/CommandLineInterface.cpp | 10 ++++++++++ 2 files changed, 21 insertions(+) diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp index 6cf13c309..feda8fc53 100644 --- a/libsolidity/interface/StandardCompiler.cpp +++ b/libsolidity/interface/StandardCompiler.cpp @@ -28,6 +28,7 @@ #include #include #include +#include #include #include #include @@ -921,6 +922,16 @@ Json::Value StandardCompiler::compileSolidity(StandardCompiler::InputsAndSetting "Yul exception" )); } + catch (smtutil::SMTLogicError const& _exception) + { + errors.append(formatErrorWithException( + _exception, + false, + "SMTLogicException", + "general", + "SMT logic exception" + )); + } catch (util::Exception const& _exception) { errors.append(formatError( diff --git a/solc/CommandLineInterface.cpp b/solc/CommandLineInterface.cpp index 1342ef1f6..cd792d9c0 100644 --- a/solc/CommandLineInterface.cpp +++ b/solc/CommandLineInterface.cpp @@ -47,6 +47,8 @@ #include #include +#include + #include #include #include @@ -1295,6 +1297,14 @@ bool CommandLineInterface::processInput() boost::diagnostic_information(_exception); return false; } + catch (smtutil::SMTLogicError const& _exception) + { + serr() << + "SMT logic error during analysis:" << + endl << + boost::diagnostic_information(_exception); + return false; + } catch (Error const& _error) { if (_error.type() == Error::Type::DocstringParsingError)