Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

We could improve our final query performance by doing slicing #428

Closed
msooseth opened this issue Nov 23, 2023 · 3 comments
Closed

We could improve our final query performance by doing slicing #428

msooseth opened this issue Nov 23, 2023 · 3 comments
Assignees
Labels
enhancement New feature or request

Comments

@msooseth
Copy link
Collaborator

msooseth commented Nov 23, 2023

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 msooseth added the enhancement New feature or request label Nov 23, 2023
@msooseth msooseth self-assigned this Nov 23, 2023
@msooseth
Copy link
Collaborator Author

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
Copy link
Collaborator Author

msooseth commented Nov 23, 2023

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

@msooseth
Copy link
Collaborator Author

msooseth commented Dec 5, 2024

I'm closing this one. I know this is possible, but it's not so important right now. And we'd still need to do a check for an assignment for the things outside of the cone of influence if it's SAT

@msooseth msooseth closed this as completed Dec 5, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

1 participant