You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
In this case, the key assertion is y == 1 implies (x / y) == x. With this, the test returns a valid result immediately and does not require refining the query.
study the power of the added axioms (are we able to solve more tests?)
study the performance trade-off (are we solving real problems faster? is adding many assertions making the query too big?)
study the performance trade-off for a couple of solvers: the effect could be different on z3 vs boolector, cvc5, etc.
is it possible to do better than eagerly adding assertions for all operations?
Related
Hozzová, Petra, et al. "Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification." Proceedings of 24th International Conference on Logic. Vol. 94. 2023.
The text was updated successfully, but these errors were encountered:
karmacoma-eth
changed the title
Research: explore performance benefits of adding explicit non-linear arithmetic axioms
Research: explicit SMT assertions for non-linear arithmetic
Jan 10, 2024
Problem
Non-linear arithmetic on bitvectors is very expensive for SMT solvers. Simple queries take a very long time to complete, for instance:
As a result, the equivalent tests in halmos also take a long time:
(run with
halmos --solver-timeout-assertion 0 --statistics
)Let's break down how halmos processes check_divRoundsDown:
evm_bvudiv
) to avoid the cost of bitvector divisionevm_bvudiv
(i.e. it doesn't know that we're asking about the actual division operation)evm_bvudiv
with the real bvudiv operator) and asks the solver againProposed solution
This test is simple enough that it can be solved without refinement, i.e. no need to do any actual bitvector division.
We could explicitly tell the solver some properties of
evm_bvudiv
that are sufficient to return a counterexample:In this case, the key assertion is
y == 1 implies (x / y) == x
. With this, the test returns a valid result immediately and does not require refining the query.Work to do
Related
Hozzová, Petra, et al. "Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification." Proceedings of 24th International Conference on Logic. Vol. 94. 2023.
The text was updated successfully, but these errors were encountered: