The "FormalArgs" relation missing some of the facts.

[MingxiYe]

Breif Introduction

I am trying to add a custom data flow analysis module. However, during developing, I notice that some of the facts of the relation FormalArgs(func:IRFunction, var:TACVariable, n:number) is missing. I wonder if this is on purpose? If not, maybe the reproduction script will help to fix it.

Bug Reproduction

• using the runtime bytecode of the wEth contract and store it in example/wEth.hex.
• adding the following datalog script in logic/decompiler_output.dl

.decl NewFormalArgs(func:IRFunction, var:TACVariable, n:number)
.output NewFormalArgs

NewFormalArgs(func, tacVar, n) :-
  FunctionArgument(func, n, var),
  Variable_String(var, var_rep),
  tacVar = as(var_rep, TACVariable).

• using the following script to run gigahorse

./gigahorse.py examples/wEth.hex

• checking the difference between .temp/wEth/FormalArgs.csv and .temp/wEth/NewFormalArgs.csv. We shall see the following result:

  ## FormalArgs
  0x4dd   0x4ddarg0x0 0
  0x68c   0x68carg0x2 2
  0x68c   0x68carg0x0 0
  0x68c   0x68carg0x1 1
  0x68c   0x68carg0x3 3
  0xb30   0xb30arg0x0 0

## NewFormalArgs
0x440   0x440arg0x0 0
0x4dd   0x4ddarg0x0 0
0x68c   0x68carg0x0 0
0x68c   0x68carg0x1 1
0x68c   0x68carg0x2 2
0x68c   0x68carg0x3 3
0xb30   0xb30arg0x0 0
0xbce   0xbcearg0x0 0
0xbce   0xbcearg0x1 1
0xbce   0xbcearg0x2 2

[sifislag]

Thanks for your report, I'll check it out in the next couple of days and report back.

[yanniss]

Is there any indication that this is a bug? Is there unreachable code? The private functions inferred could well differ for newer versions of the decompiler.

[MingxiYe]

It seems like a bug to me, as I only move the type cast as(var_rep, TACVariable) from the LHS of the rule to the RHS. It seems like a pretty small change for me and should not result in missing two of the private functions. I also check that facts in FunctionArgument(func, n, var) and Variable_String(var, var_rep) are correct, meaning that these functions should be reachable. I wonder if this is relevant with casting type to subtype (i.e., symbol to TACVariable)?

[sifislag]

Hi, I've been unable to reproduce it on my setup (ubuntu20.04, souffle2.3). When I decompile weth I get the expected output. What is your setup like?

[MingxiYe]

Hi, Sifis! That's odd. I am also using ubuntu 20.04 and souffle 2.3 (my local server). Also I just try to reproduce it on a cloud server (Alicloud) with ubuntu 22.04 and souffle 2.4, and I got the following output.

## FormalArgs
0x68c   0x68carg0x2 2
0x68c   0x68carg0x0 0
0x68c   0x68carg0x1 1
0x68c   0x68carg0x3 3

## NewFormalArgs
0x440   0x440arg0x0 0
0x4dd   0x4ddarg0x0 0
0x68c   0x68carg0x0 0
0x68c   0x68carg0x1 1
0x68c   0x68carg0x2 2
0x68c   0x68carg0x3 3
0xb30   0xb30arg0x0 0
0xbce   0xbcearg0x0 0
0xbce   0xbcearg0x1 1
0xbce   0xbcearg0x2 2

[sifislag]

Ok, I got the issue. These private functions are removed via our inliner. Its use is explained on the README. You can disable that using --disable_inline to get all the original inferred functions. You can understand the removal of these functions by inspecting the output of visualizeout.py.

[MingxiYe]

Oh, I see. Really appreciate it!

[sifislag]

Glad to help, let me know if you have any questions. You can also reach us via the dedaub discord.