Zilliqa / scilla

Scilla - A Smart Contract Intermediate Level Language
https://scilla-lang.org
GNU General Public License v3.0
240 stars 78 forks source link

Warn if multiple procedure calls have the same effect as one call (procedure idempotence) #1157

Closed anton-trunov closed 1 year ago

anton-trunov commented 2 years ago

Warn if a parameterless procedure gets called in a loop, possibly transitively, but the procedure only reads unmodified contract fields and it does not modify the contract's state nor it issues events and/or messages, i.e. its behavior is the same across all loop iterations.

A usual use case for such procedures is access control, handling pausing/unpausing of the contract, etc. These procedures usually check some property on contract fields that cannot be modified in the same transition and abort contract execution in case the property is violated.

The point of the analysis is to warn excessive gas usage by such iterative procedure calls.

jubnzv commented 1 year ago

We should take into account that we only need to report such procedures that do not return a value (when #578 is finished).