mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Update
This commit is contained in:
Leonardo Alt
parent
1718f4ff39
commit
ffbf281332
@ -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)
|
||||
|
||||
@ -23,7 +23,7 @@ using namespace solidity;
|
||||
using namespace solidity::util;
|
||||
using namespace solidity::smtutil;
|
||||
|
||||
OpenSMT2Interface::OpenSMT2Interface():
|
||||
OpenSMT2Interface::OpenSMT2Interface(optional<unsigned> /*_queryTimeout*/):
|
||||
m_opensmt(make_unique<Opensmt>(qf_lia, "OpenSMT")),
|
||||
m_logic(m_opensmt->getLIALogic()),
|
||||
m_solver(m_opensmt->getMainSolver())
|
||||
|
||||
@ -29,7 +29,7 @@ namespace solidity::smtutil
|
||||
class OpenSMT2Interface: public SolverInterface, public boost::noncopyable
|
||||
{
|
||||
public:
|
||||
OpenSMT2Interface();
|
||||
OpenSMT2Interface(std::optional<unsigned> _queryTimeout = {});
|
||||
|
||||
void reset() override;
|
||||
|
||||
|
||||
@ -24,6 +24,9 @@
|
||||
#ifdef HAVE_CVC4
|
||||
#include <libsmtutil/CVC4Interface.h>
|
||||
#endif
|
||||
#ifdef HAVE_OSMT2
|
||||
#include <libsmtutil/OpenSMT2Interface.h>
|
||||
#endif
|
||||
#include <libsmtutil/SMTLib2Interface.h>
|
||||
|
||||
using namespace std;
|
||||
@ -49,6 +52,9 @@ SMTPortfolio::SMTPortfolio(
|
||||
if (_enabledSolvers.cvc4)
|
||||
m_solvers.emplace_back(make_unique<CVC4Interface>(m_queryTimeout));
|
||||
#endif
|
||||
#ifdef HAVE_OSMT2
|
||||
m_solvers.emplace_back(make_unique<OpenSMT2Interface>(m_queryTimeout));
|
||||
#endif
|
||||
}
|
||||
|
||||
void SMTPortfolio::reset()
|
||||
|
||||
@ -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 { } }
|
||||
// }
|
||||
@ -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)
|
||||
// }
|
||||
// }
|
||||
// }
|
||||
// }
|
||||
@ -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 { } }
|
||||
// }
|
||||
@ -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 { }
|
||||
// }
|
||||
@ -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) } }
|
||||
// }
|
||||
// }
|
||||
@ -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) } }
|
||||
// }
|
||||
// }
|
||||
Loading…
Reference in New Issue
Block a user