Decompilation

[d-xo]

Adds a certified decompiler that can automatically derive act specifications from evm bytecode. The process operates in the following stages:

1. Symbolically execute the bytecode to produce an EVM.Expr
2. Transform that Expr into one that can be safely represented using Integers
3. Convert that Expr into an Act spec (trusts solc compiler output)
4. Compile the generated Act spec back to Expr and check equivalence (solc compiler output no longer trusted)

This currently supports only very simple contracts, basically value types, simple arithmethic, and storage writes. Mappings in storage are currently not supported, but doing so should be in principle possible.

Some simple tests are added, but still todo is to hook this up to the main CLI interface.

Starting from the existing solidity code produces the following spec (I'm currently unsure where the case True comes from):

contract C {
  uint x = 0;
  function f(uint v) public {
    x = v;
  }
}

constructor of C
interface C()

iff

  (CALLVALUE == 0)

creates

  uint256 x := 0


behaviour f of C
interface f(uint256 v)

iff

  (CALLVALUE == 0)

case

  true:

storage

  x => v

[msooseth]

Hi!

Is this still being worked on? Should I review? Sounds cool :)

Mate

[d-xo]

Thanks for fixing this up and getting it ready to merge.
Mostly curious if some of the soundness concerns still in the TODO comments are valid.

[msooseth]

Should I review? Is this active, do you want this merged? Looks like a lot of cool work!

[d-xo]

I'm not allowed to approve because I opened the PR originally, but all your changes look good to me @zoep and I'm fine to merge this whenever.

[zoep]

LGTM