diff --git a/cmake/FindOSMT2.cmake b/cmake/FindOSMT2.cmake index 5236e86d2..5d5eaca4c 100644 --- a/cmake/FindOSMT2.cmake +++ b/cmake/FindOSMT2.cmake @@ -1,6 +1,6 @@ if (USE_OSMT2) find_path(OSMT2_INCLUDE_DIR opensmt/opensmt2.h) - find_library(OSMT2_LIBRARY NAMES opensmt2) + find_library(OSMT2_LIBRARY NAMES opensmt) include(FindPackageHandleStandardArgs) find_package_handle_standard_args(OSMT2 DEFAULT_MSG OSMT2_LIBRARY OSMT2_INCLUDE_DIR) if(OSMT2_FOUND) diff --git a/libsmtutil/OpenSMT2Interface.cpp b/libsmtutil/OpenSMT2Interface.cpp index 80ebb05a5..3eb43f9f4 100644 --- a/libsmtutil/OpenSMT2Interface.cpp +++ b/libsmtutil/OpenSMT2Interface.cpp @@ -23,7 +23,7 @@ using namespace solidity; using namespace solidity::util; using namespace solidity::smtutil; -OpenSMT2Interface::OpenSMT2Interface(): +OpenSMT2Interface::OpenSMT2Interface(optional /*_queryTimeout*/): m_opensmt(make_unique(qf_lia, "OpenSMT")), m_logic(m_opensmt->getLIALogic()), m_solver(m_opensmt->getMainSolver()) diff --git a/libsmtutil/OpenSMT2Interface.h b/libsmtutil/OpenSMT2Interface.h index bc443c906..b7698bbcc 100644 --- a/libsmtutil/OpenSMT2Interface.h +++ b/libsmtutil/OpenSMT2Interface.h @@ -29,7 +29,7 @@ namespace solidity::smtutil class OpenSMT2Interface: public SolverInterface, public boost::noncopyable { public: - OpenSMT2Interface(); + OpenSMT2Interface(std::optional _queryTimeout = {}); void reset() override; diff --git a/libsmtutil/SMTPortfolio.cpp b/libsmtutil/SMTPortfolio.cpp index de00c1f79..783bfb06d 100644 --- a/libsmtutil/SMTPortfolio.cpp +++ b/libsmtutil/SMTPortfolio.cpp @@ -24,6 +24,9 @@ #ifdef HAVE_CVC4 #include #endif +#ifdef HAVE_OSMT2 +#include +#endif #include using namespace std; @@ -49,6 +52,9 @@ SMTPortfolio::SMTPortfolio( if (_enabledSolvers.cvc4) m_solvers.emplace_back(make_unique(m_queryTimeout)); #endif +#ifdef HAVE_OSMT2 + m_solvers.emplace_back(make_unique(m_queryTimeout)); +#endif } void SMTPortfolio::reset() diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/addmod.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/addmod.yul deleted file mode 100644 index 5ea7e7cdc..000000000 --- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/addmod.yul +++ /dev/null @@ -1,36 +0,0 @@ -{ - let x := calldataload(0) - let y := calldataload(32) - let z := calldataload(64) - let result := addmod(x, y, z) - - // should be zero - if gt(result, z) { sstore(0, 1) } - - // addmod is equal to mod of sum for small numbers - if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000)) { - // z3 <4.8.10 was able to infer that the - // condition below is always true. - if eq(result, mod(add(x, y), z)) { sstore(0, 9) } - } - - // but not in general - if and(and(gt(x, sub(0, 5)), gt(y, sub(0, 2))), eq(z, 3)) { - if eq(result, mod(add(x, y), z)) { sstore(0, 5) } - } -} -// ---- -// step: reasoningBasedSimplifier -// -// { -// let x := calldataload(0) -// let y := calldataload(32) -// let z := calldataload(64) -// let result := addmod(x, y, z) -// if 0 { } -// if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000)) -// { -// if eq(result, mod(add(x, y), z)) { sstore(0, 9) } -// } -// if and(and(gt(x, sub(0, 5)), gt(y, sub(0, 2))), eq(z, 3)) { if 0 { } } -// } diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulcheck.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulcheck.yul deleted file mode 100644 index 31a342339..000000000 --- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulcheck.yul +++ /dev/null @@ -1,32 +0,0 @@ -{ - let vloc_x := calldataload(0) - let vloc_y := calldataload(1) - if lt(vloc_x, shl(100, 1)) { - if lt(vloc_y, shl(100, 1)) { - if iszero(and(iszero(iszero(vloc_x)), gt(vloc_y, div(not(0), vloc_x)))) { - let vloc := mul(vloc_x, vloc_y) - sstore(0, vloc) - } - } - } -} -// ==== -// EVMVersion: >=constantinople -// ---- -// step: reasoningBasedSimplifier -// -// { -// let vloc_x := calldataload(0) -// let vloc_y := calldataload(1) -// if lt(vloc_x, shl(100, 1)) -// { -// if lt(vloc_y, shl(100, 1)) -// { -// if 1 -// { -// let vloc := mul(vloc_x, vloc_y) -// sstore(0, vloc) -// } -// } -// } -// } diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulmod.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulmod.yul deleted file mode 100644 index f5226acf7..000000000 --- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulmod.yul +++ /dev/null @@ -1,31 +0,0 @@ -{ - let x := calldataload(0) - let y := calldataload(32) - let z := calldataload(64) - let result := mulmod(x, y, z) - - // should be zero - if gt(result, z) { sstore(0, 1) } - - // mulmod is equal to mod of product for small numbers - if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000)) { - if eq(result, mod(mul(x, y), z)) { sstore(0, 9) } - } - - // but not in general - if and(and(gt(x, sub(0, 5)), eq(y, 2)), eq(z, 3)) { - if eq(result, mod(mul(x, y), z)) { sstore(0, 5) } - } -} -// ---- -// step: reasoningBasedSimplifier -// -// { -// let x := calldataload(0) -// let y := calldataload(32) -// let z := calldataload(64) -// let result := mulmod(x, y, z) -// if 0 { } -// if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000)) { if 1 { sstore(0, 9) } } -// if and(and(gt(x, sub(0, 5)), eq(y, 2)), eq(z, 3)) { if 0 { } } -// } diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/negative_rounding.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/negative_rounding.yul deleted file mode 100644 index 6e4b3f5ed..000000000 --- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/negative_rounding.yul +++ /dev/null @@ -1,16 +0,0 @@ -{ - let x := sub(0, 7) - let y := 2 - // (-7)/2 == -3 on the evm - if iszero(add(sdiv(x, y), 3)) { } - if iszero(add(sdiv(x, y), 4)) { } -} -// ---- -// step: reasoningBasedSimplifier -// -// { -// let x := sub(0, 7) -// let y := 2 -// if 1 { } -// if 0 { } -// } diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/signed_division.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/signed_division.yul deleted file mode 100644 index 1e409079e..000000000 --- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/signed_division.yul +++ /dev/null @@ -1,31 +0,0 @@ -{ - let y := calldataload(0) - let t := calldataload(32) - - if sgt(sub(y, 1), y) { - // y - 1 > y, i.e. y is the most negative value - if eq(sdiv(y, sub(0, 1)), y) { - // should be true: y / -1 == y - sstore(0, 7) - } - if iszero(eq(y, t)) { - // t is not the most negative value - if eq(sdiv(t, sub(0, 1)), sub(0, t)) { - // should be true: t / -1 = 0 - t - sstore(1, 7) - } - } - } -} -// ---- -// step: reasoningBasedSimplifier -// -// { -// let y := calldataload(0) -// let t := calldataload(32) -// if sgt(sub(y, 1), y) -// { -// if 1 { sstore(0, 7) } -// if iszero(eq(y, t)) { if 1 { sstore(1, 7) } } -// } -// } diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smod.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smod.yul deleted file mode 100644 index 12f04c857..000000000 --- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smod.yul +++ /dev/null @@ -1,53 +0,0 @@ -{ - // 7 % 5 == 2 - // 7 % -5 == 2 - // -7 % 5 == -2 - // -7 % -5 == -2 - // -5 % -5 == 0 - let x := calldataload(0) - let y := calldataload(32) - let result := smod(x, y) - if eq(x, 7) { - if eq(y, 5) { - if eq(result, 2) { sstore(0, 7)} - } - if eq(y, sub(0, 5)) { - if eq(result, 2) { sstore(0, 7)} - } - } - if eq(x, sub(0, 7)) { - if eq(y, 5) { - if eq(result, sub(0, 2)) { sstore(0, 7)} - } - if eq(y, sub(0, 5)) { - if eq(result, sub(0, 2)) { sstore(0, 7)} - } - } - if eq(x, sub(0, 5)) { - if eq(y, sub(0, 5)) { - if eq(result, 0) { sstore(0, 7)} - } - } -} -// ---- -// step: reasoningBasedSimplifier -// -// { -// let x := calldataload(0) -// let y := calldataload(32) -// let result := smod(x, y) -// if eq(x, 7) -// { -// if eq(y, 5) { if 1 { sstore(0, 7) } } -// if eq(y, sub(0, 5)) { if 1 { sstore(0, 7) } } -// } -// if eq(x, sub(0, 7)) -// { -// if eq(y, 5) { if 1 { sstore(0, 7) } } -// if eq(y, sub(0, 5)) { if 1 { sstore(0, 7) } } -// } -// if eq(x, sub(0, 5)) -// { -// if eq(y, sub(0, 5)) { if 1 { sstore(0, 7) } } -// } -// }