This PR includes various additions to the client libraries:
Add support for OZ style reentrancy guards. Results are populating relation ReentrancyGuard(storageVar:Value).
Make guards.dl use the memory modeling by default.
Introduced various top-down control-flow related components. These work inter-procedurally and efficiently by computing the results only for the subset of the CFG that is relevant to our query, defined at every instantiation of the component.
MayHappenBeforeGlobal: This can be used to produce results for queries such as "Find all external calls that can be followed by an sstore for any program path"
MayHappenBeforeGlobalWithArg: This can be used to produce results for queries such as "Find all sstores that write to the same storage address, with one following the other"
MayHappenInBetweenGlobal: Internally uses two instantiations of MayHappenBeforeGlobal to support more complex queries.
Overview
This PR includes various additions to the client libraries:
ReentrancyGuard(storageVar:Value).guards.dluse the memory modeling by default.MayHappenBeforeGlobal: This can be used to produce results for queries such as "Find all external calls that can be followed by an sstore for any program path"MayHappenBeforeGlobalWithArg: This can be used to produce results for queries such as "Find all sstores that write to the same storage address, with one following the other"MayHappenInBetweenGlobal: Internally uses two instantiations ofMayHappenBeforeGlobalto support more complex queries.