search

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

Add the `Callgraph` module #1144

Closed jubnzv closed 2 years ago

jubnzv commented 2 years ago

The Callgraph module is required to finish #1097 and it will be useful in other analyses in the future.

I also added a simple .dot printer based on the ocamlgraph library, because it is easy to implement and it could be helpful when auditing smart contracts.

I'd like to check possible corner-cases, mostly related to type functions, so I'll leave it as a draft for a while.

The callgraph doesn't support partial application of functions and type functions. It is designed to generate warnings for the user, so we intentionally don't handle these cases to make the checker work faster. Otherwise, we'll need to use an algorithm with n^3 complexity to collect such cases in the program.

anton-trunov commented 2 years ago

If a procedure is called using the forall statement, it's not shown as a dependency.

In the counter-example below, DisallowAddress won't be reported as a dependency of Disallow, however, it should be.

procedure DisallowAddress(address: ByStr20)
  delete allowed_addresses[address]
end

transition Disallow(address_list: List ByStr20)
  forall address_list DisallowAddress;
end
anton-trunov commented 2 years ago

Related scilla-docs issue: https://github.com/Zilliqa/scilla-docs/issues/160