Zilliqa / scilla

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

`accept` analysis improvement #1141

Closed anton-trunov closed 1 year ago

anton-trunov commented 2 years ago

There is an analysis of accept statements in the Scilla codebase (see Accept.ml). The analysis checks

We can improve accept-checking in Scilla. For example, to remove false positives in case of non-native token contracts we can check that all send statements have the _amount message field equal to zero and turn this warning off in this case. (This is not going to be precise, but for many practical contracts it's easy to establish the _amount field is zero). See, for instance, https://github.com/Zilliqa/ZRC/blob/main/reference-contracts/FungibleToken.scilla

jubnzv commented 1 year ago

For example, to remove false positives in case of non-native token contracts we can check that all send statements have the _amount message field equal to zero and turn this warning off in this case. (This is not going to be precise, but for many practical contracts it's easy to establish the _amount field is zero)

How accurate should such an analysis be?

If we just use a zero constant, it could be trivially implemented. But in more complex cases we need some kind of constant propagation and maybe some other dataflow analyses.

anton-trunov commented 1 year ago

@jubnzv It's usually a Uint128 0 directly or just a constant that unfolds to Uint128 0.