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

Implement State Subsumption #207

Open
DavePearce opened this issue Sep 26, 2023 · 0 comments
Open

Implement State Subsumption #207

DavePearce opened this issue Sep 26, 2023 · 0 comments

Comments

@DavePearce
Copy link
Collaborator

DavePearce commented Sep 26, 2023

(see also #205)

With the introduction of the havoc instruction, it is now possible for states to end up being "subsumed". Whilst that was possible before, it now becomes more likely. A good example is this:

.code
        push 0x10
        calldatasize
        push loop
        jumpi
        pop
        push 0x5
loop:
        jumpdest
        havoc stack[0]
        dup1
        iszero
        push exit
        jumpi
        push 0x1
        swap1
        sub
        push loop
        jump
exit:
        stop

Looking at the debug trace, we can see the following:

.code
        ;; ||
        push 0x10
        ;; |0x10|
        calldatasize
        ;; |??,0x10|
        push 0x000a
        ;; |0x0a,??,0x10|
        jumpi
        ;; |0x10|
        pop
        ;; ||
        push 0x05
_0x000a:
        ;; |0x10|
        ;; |??|
        ;; |0x05|
        jumpdest
        ;; |0x10|
        ;; |??|
        ;; |0x05|
        havoc stack[0]
        ...

In particular, looking at the states going into _0x000a we can see that |0x10| and |0x05| should be subsumed by |??|.

Implementing this should be reasonably straightforward. We need to extend the existing notion of dedup which is applied to states.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant