Join GitHub today
GitHub is home to over 50 million developers working together to host and review code, manage projects, and build software together.
Sign upGitHub is where the world builds software
Millions of developers and companies build, ship, and maintain their software on GitHub — the largest and most advanced development platform in the world.
[SMTChecker] Support to external calls to unknown code #8950
Conversation
|
For the record: this needs a rebase ;-), but this looks quite good to me! I'm actually almost approving it right away, but maybe I should take some more time trying to come up with something that might break it... One remark though: we could actually check if the function called is |
|
Right, that makes sense! (re Yea, I also have a few test cases in mind that I still want to add. |
ff789e6
to
2f49300
|
Rebased on top of #9176 to see if the nondet problem is gone |
a629ec4
to
e89fcd5
|
Apparently the nondeterminism in the tests in my local arch build vs CI was that the arch z3 uses gmp whereas the others don't. |
|
Rebased, ready for review. |
2027e87
to
35d8f2a
|
#9159 helps with the nondeterminism |
b998790
to
bdfead5
| } | ||
| } | ||
| // ---- | ||
| // Warning: (306-320): Assertion violation happens here |
ekpyron
Jun 12, 2020
Member
Which one is this?
Which one is this?
leonardoalt
Jun 12, 2020
Author
Member
z == y
z == y
leonardoalt
Jun 12, 2020
Author
Member
it fails because State.c is not necessarily the caller
it fails because State.c is not necessarily the caller
leonardoalt
Jun 12, 2020
Author
Member
and since the state is not carried over to the called contract, it doesn't know anything about c's state
and since the state is not carried over to the called contract, it doesn't know anything about c's state
|
This needs a rebase to resolve the conflicts |
dfec5ef
to
9a15de4
|
We decided to change the implemented pure function case. |
|
@ekpyron updated |
|
I wonder what's the best way to have CHC track if we know that the address in a state variable like Maybe there's just a boolean flag for But yeah - maybe we can really just assume that everything named |
Fixes #8972
Depends on #9159
tl;dr
Support reentrancy from unknown code without losing all knowledge.
This PR extends the CHC model to support external calls to unknown code. Since the code is unknown, it is sound to assume that it can nondeterministically call the analyzed contract, any number of times.
Because of that, the model is extended with 2 new types of rules that encode this nondeterminism, using a new predicate
nondet_interface(state, state')for each analyzed contract, that allow the state to change nondeterministically fromstatetostate'.The first rule is a fact added for each contract:
nondet_interface(state, state)This fact is the base case of the inductive rule, and allows the nondeterministic step to be applied without state changes.
The second rule is the inductive rule over each public function
fof the contract:2.
nondet_interface(state, state') && summary_f(state', state'') => nondet_interface(state, state'')When an external call to unknown code is seen, CHC simply adds the constraint
nondet_interface(currentState, postState)to the current block/rule. This means that the current contract can be called nondeterministically any number of times (including zero) before moving on to the next block.Note that because it is nondeterministic, if a certain path allows for state changes in the contract, it will necessarily be reached and taken into account, so this model is sound.
If the contract has public functions that allow arbitrary state changes, knowledge will be lost at this point, but there's not much else one can do.
However, if the contract has a certain behavior where the current state might limit state changes in reentrant calls, this will be taken into account when generating invariants.
See the
mutex.solexample added in this PR.