We could improve our final query performance by doing slicing

[msooseth]

The final Expr can contain parts that have nothing to do with the query. This means that the solver will be given & compute things that are utterly useless from a UNSAT perspective, and could be queried if needed for a counterexample (e.g. a variable in the function call that is never touched). So what we need to do is to do slicing [1] -- figuring out what is actually needed by the final query. A simple taint analysis could do the trick.

If you think about it, this would be SOMEWHAT similar to what Certora is doing with the weakest precondition calculation. I think it would simulate SOME of it. Maybe a poor man's version of it, but I don't think it would be a bad idea. Could significantly improve performance I think?

[1] https://en.wikipedia.org/wiki/Program_slicing

[msooseth]

Example:

            contract MyContract {
              uint[] x;
              function fun(uint256 a, uint256 b, uint256 c) external {
                unchecked {
                  x[0] = c+2;
                  uint z = 0;
                  if (x[0]>20) { z = 10; }
                  require(a > b);
                  assert(a > b);
                }
              }
             }

Gives:

(declare-const arg2 (_ BitVec 256))
(declare-const arg1 (_ BitVec 256))
(declare-const arg3 (_ BitVec 256))

; frame context
(declare-const txvalue (_ BitVec 256))
[... comments...]

(assert (bvult txdata_length (_ bv18446744073709551616 256)))
(assert (= (ite (bvult arg2 arg1) (_ bv1 256) (_ bv0 256)) (_ bv0 256)))
(assert (bvult arg2 arg1))
(assert (= (ite (bvult (_ bv20 256) (bvadd (_ bv2 256) arg3)) (_ bv1 256) (_ bv0 256)) (_ bv0 256)))
(assert (bvult (_ bv0 256) (select baseStore_symaddr_entrypoint (_ bv0 256))))
(assert (= txvalue (_ bv0 256)))
(assert (bvult txdata_length (_ bv18446744073709551616 256)))

where arg3 is unneccessary for the UNSAT, and we could determine that statically.

[msooseth]

Have to be careful, here a has nothing to do with the assert(false):

require (a <10);
if (a > 10) {
    assert(false);
}

A form of data taint analysis: if we never read from a write, it can be deleted. -- stripWrites could be improved possibly with interval graphs(?) or send to the solver? But in order to remove the if above, we'd need also(?) control-flow based taint analysis