--- title: Control Flow Graph for EVM bytecode tags: EVM, Ethereum, Dafny, Semantics breaks: false --- [Franck Cassez](https://franck44.github.io), Head of Research at [Mantle](https://www.mantle.xyz). — all views expressed are my own. [![Twitter URL](https://img.shields.io/twitter/url/https/twitter.com/franckDownunder.svg?style=social&label=Follow%20%40FranckDownunder)](https://twitter.com/franckDownunder) --- A version of this post (27/12/24) has been published as a [Mantle blog post](https://www.mantle.xyz/blog/research/decompiling-evm-bytecode). This version differs in the following aspects: - the CFG in Figure 1 is interactive: hovering some components (instructions, segments) reveals some information about the component. - minor rewording of some paragraphs. I have recently developed and implemented an algorithm to generate Control Flow Graphs (CFGs) from EVM bytecode. The details of the algorithm can be found in [this note](https://hackmd.io/@FranckC/rJIRA43Na), and the implementation is available in the [evm-dis](https://github.com/franck44/evm-dis) repository. In this post I'll discuss the following aspects: - what kind of information do CFGs provide and what can we do with them? - how can you use the CFG generator and who can benefit from using it? - how I implemented the CFG generator. ## What is the purpose of a CFG? Control flow graphs (CFGs) provide an abstract semantics of programs. :::info :bulb: As the name suggests, the CFG of a program captures how the _control location_ is updated during the _program execution_. The control location indicates what instruction in the program is to be executed next. ::: A CFG is a standard _directed graph_ with _nodes_ and _edges_. The nodes are _labelled_ with control locations. A CFG has a designated _initial node_. _Paths_ in the graph can be constructed by starting at the initial node and following the (directed) edges. A path defines a sequence of nodes. As nodes can be mapped to their labels that are control locations, a path in the CFG defines a _sequence_ of control locations. The set of paths in the graph defines a set of sequences of control locations. ### Jumps in the EVM Most of the EVM instructions update the control location to the _next line of code in the program_ except for`JUMP` and `JUMPI`. `JUMP` is an _inconditional_ jump instruction that updates the control location to the value that is at the top of the stack; it is like a `goto` statement. `JUMPI` is similar but _conditional_: it jumps only if the second topmost element on the stack is non-zero, otherwise it progresses to the next instruction in the code. Note that relative `JUMP`s, `RJUMP`s are similar to `JUMP`s so we omit them in this discussion. :::info :bulb: A (code) _segment_ is a _linear sequence_ of instructions i.e. a sequence that contains no `JUMP/JUMPI`s. Instead of treating each control location/instruction in the bytecode as a CFG node, we collapse _linear sequences_ of instructions into a _single node_ and each node in the CFG is _labelled with a segment_ rather than with a single control location. ::: ### Example Figure 1^[Hovering on the instructions/segments will reveal some information on the semantics and link to the Dafny-EVM semantics of the instruction. Hovering the :fuelpump: reveals gas cost when it is constant.] below provides an example of CFG. The bytecode of the source program is the sequence of instructions in Segments 0 to 6, put together, in that order. Each node is labelled by the Segment number and the line of code with which the segment starts. The initial node in Figure 1 is the node labelled with _Segment 0_ at the top. An execution of the program starts at the first control location^[The control location is displayed on the left, in hexadecimal with the prefix`0x`.] of the initial node i.e. `0x00`. _Plain black arrows_ denote a _normal update_ of the control location i.e. it goes to the next instruction in the code: for example, the arrow `Segment 0 --> Segment 1` indicates that the program executes `PUSH1 0x01, PUSH0`, and progresses to the instruction after `PUSH0` in the code, at `0x03`, and executes`JUMPDEST, PUSH1 0x0a, ...`. In contrast, _dashed green arrows_ indicate `JUMP`s: `Segment 5 - - > Segment 1` goes from control location `0x2b: JUMP` to control location `0x03` and not to the next instruction in the code. :::warning :warning: In the example of Figure 1, each node is labelled with a different segment. However, the same (code) segment can be associated with different nodes. This may reflect that the context of the execution of a segment is different in two occurrences. An example is a program with two calls to the same "function" (segment). ::: <center> <figure> ```graphviz digraph G { graph[labelloc="t", labeljust="c", label=<<B>Program Name: </B> doubleLoop.bin<BR ALIGN="left"/><B>Control Flow Graph Info: </B><BR ALIGN="left"/>Max depth: 100 [Was not reached]<BR ALIGN="left"/>7 nodes/8 edges<BR ALIGN="left"/>>] node [shape=none, fontname=arial, style="rounded, filled", fillcolor= "whitesmoke"] edge [fontname=arial,penwidth=4,color=slategrey] ranking=TB nodesep=2.5; {rank = same; s_1; s_3, s_4;} s_0 [label=<<TABLE ALIGN="LEFT" CELLBORDER="0" BORDER="0" cellpadding="0" CELLSPACING="1"> <TR><TD >Segment 0 [0x0]</TD><TD href="" tooltip="Stack Size &#916;: +2&#10;Stack Size on Entry for this segment &#8805; 0&#10;Stack Size on Entry for this segment at this node &#8805; 0"><FONT color="black">&#8505;&#65039;</FONT></TD></TR><HR/> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" PORT="entry">0x00 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1479" target="_blank" tooltip="Push 1 byte" ><FONT color="royalblue">PUSH1</FONT></TD><TD width="1" fixedsize="true" align="left"> 0x01</TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x02 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1428" target="_blank" tooltip="Push 0 on stack" ><FONT color="royalblue">PUSH0</FONT></TD></TR></TABLE></TD></TR> </TABLE> >] s_1 [label=<<TABLE ALIGN="LEFT" CELLBORDER="0" BORDER="0" cellpadding="0" CELLSPACING="1"> <TR><TD >Segment 1 [0x3]</TD><TD href="" tooltip="Stack Size &#916;: 0&#10;Stack Size on Entry for this segment &#8805; 1&#10;Stack Size on Entry for this segment at this node &#8805; 2&#10;Exit Jump target: Constant 0x14"><FONT color="black">&#8505;&#65039;</FONT></TD></TR><HR/> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" PORT="entry">0x03 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 1 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="thistle" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1334" target="_blank" tooltip="A valid destination for a jump" ><FONT color="purple">JUMPDEST</FONT></TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x04 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1479" target="_blank" tooltip="Push 1 byte" ><FONT color="royalblue">PUSH1</FONT></TD><TD width="1" fixedsize="true" align="left"> 0x0a</TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x06 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1568" target="_blank" tooltip="Duplicate 2nd element on top of the stack" ><FONT color="royalblue">DUP2</FONT></TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x07 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="bisque" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L314" target="_blank" tooltip="Unsigned Less than" ><FONT color="darkgoldenrod">LT</FONT></TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x08 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1479" target="_blank" tooltip="Push 1 byte" ><FONT color="royalblue">PUSH1</FONT></TD><TD width="1" fixedsize="true" align="left"> 0x14</TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x0a </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 10 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="thistle" align="left" cellpadding="3" PORT="exit" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1277" target="_blank" tooltip="Conditional Jump" ><FONT color="purple">JUMPI</FONT></TD></TR></TABLE></TD></TR> </TABLE> >] s_2 [label=<<TABLE ALIGN="LEFT" CELLBORDER="0" BORDER="0" cellpadding="0" CELLSPACING="1"> <TR><TD >Segment 2 [0xb]</TD><TD href="" tooltip="Stack Size &#916;: -2&#10;Stack Size on Entry for this segment &#8805; 2&#10;Stack Size on Entry for this segment at this node &#8805; 2"><FONT color="black">&#8505;&#65039;</FONT></TD></TR><HR/> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" PORT="entry">0x0b </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 2 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1097" target="_blank" tooltip="Pop top of stack" ><FONT color="royalblue">POP</FONT></TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x0c </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1479" target="_blank" tooltip="Push 1 byte" ><FONT color="royalblue">PUSH1</FONT></TD><TD width="1" fixedsize="true" align="left"> 0x40</TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x0e </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: Depends on memory expansion " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="wheat" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1165" target="_blank" tooltip="Store a word to memory" ><FONT color="sienna">MSTORE</FONT></TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x0f </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1479" target="_blank" tooltip="Push 1 byte" ><FONT color="royalblue">PUSH1</FONT></TD><TD width="1" fixedsize="true" align="left"> 0x20</TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x11 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1479" target="_blank" tooltip="Push 1 byte" ><FONT color="royalblue">PUSH1</FONT></TD><TD width="1" fixedsize="true" align="left"> 0x40</TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x13 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: Depends on memory expansion " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="greenyellow" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1742" target="_blank" tooltip="Halt execution and return data" ><FONT color="teal">RETURN</FONT></TD></TR></TABLE></TD></TR> </TABLE> >] s_3 [label=<<TABLE ALIGN="LEFT" CELLBORDER="0" BORDER="0" cellpadding="0" CELLSPACING="1"> <TR><TD >Segment 3 [0x14]</TD><TD href="" tooltip="Stack Size &#916;: +1&#10;Stack Size on Entry for this segment &#8805; 2&#10;Stack Size on Entry for this segment at this node &#8805; 2"><FONT color="black">&#8505;&#65039;</FONT></TD></TR><HR/> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" PORT="entry">0x14 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 1 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="thistle" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1334" target="_blank" tooltip="A valid destination for a jump" ><FONT color="purple">JUMPDEST</FONT></TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x15 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1577" target="_blank" tooltip="Swap top and 2nd element of the stack" ><FONT color="royalblue">SWAP1</FONT></TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x16 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1428" target="_blank" tooltip="Push 0 on stack" ><FONT color="royalblue">PUSH0</FONT></TD></TR></TABLE></TD></TR> </TABLE> >] s_4 [label=<<TABLE ALIGN="LEFT" CELLBORDER="0" BORDER="0" cellpadding="0" CELLSPACING="1"> <TR><TD >Segment 4 [0x17]</TD><TD href="" tooltip="Stack Size &#916;: 0&#10;Stack Size on Entry for this segment &#8805; 1&#10;Stack Size on Entry for this segment at this node &#8805; 3&#10;Exit Jump target: Constant 0x2c"><FONT color="black">&#8505;&#65039;</FONT></TD></TR><HR/> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" PORT="entry">0x17 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 1 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="thistle" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1334" target="_blank" tooltip="A valid destination for a jump" ><FONT color="purple">JUMPDEST</FONT></TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x18 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1479" target="_blank" tooltip="Push 1 byte" ><FONT color="royalblue">PUSH1</FONT></TD><TD width="1" fixedsize="true" align="left"> 0x0a</TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x1a </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1568" target="_blank" tooltip="Duplicate 2nd element on top of the stack" ><FONT color="royalblue">DUP2</FONT></TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x1b </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="bisque" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L314" target="_blank" tooltip="Unsigned Less than" ><FONT color="darkgoldenrod">LT</FONT></TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x1c </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1479" target="_blank" tooltip="Push 1 byte" ><FONT color="royalblue">PUSH1</FONT></TD><TD width="1" fixedsize="true" align="left"> 0x2c</TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x1e </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 10 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="thistle" align="left" cellpadding="3" PORT="exit" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1277" target="_blank" tooltip="Conditional Jump" ><FONT color="purple">JUMPI</FONT></TD></TR></TABLE></TD></TR> </TABLE> >] s_5 [label=<<TABLE ALIGN="LEFT" CELLBORDER="0" BORDER="0" cellpadding="0" CELLSPACING="1"> <TR><TD >Segment 5 [0x1f]</TD><TD href="" tooltip="Stack Size &#916;: -1&#10;Stack Size on Entry for this segment &#8805; 3&#10;Stack Size on Entry for this segment at this node &#8805; 3&#10;Exit Jump target: Constant 0x3"><FONT color="black">&#8505;&#65039;</FONT></TD></TR><HR/> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" PORT="entry">0x1f </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 2 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1097" target="_blank" tooltip="Pop top of stack" ><FONT color="royalblue">POP</FONT></TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x20 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1479" target="_blank" tooltip="Push 1 byte" ><FONT color="royalblue">PUSH1</FONT></TD><TD width="1" fixedsize="true" align="left"> 0x01</TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x22 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1479" target="_blank" tooltip="Push 1 byte" ><FONT color="royalblue">PUSH1</FONT></TD><TD width="1" fixedsize="true" align="left"> 0x0a</TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x24 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1577" target="_blank" tooltip="Swap top and 3rd element of the stack" ><FONT color="royalblue">SWAP2</FONT></TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x25 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="#c6eb76" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L40" target="_blank" tooltip="Unsigned integer addition modulo TWO_256" ><FONT color="#316152">ADD</FONT></TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x26 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1577" target="_blank" tooltip="Swap top and 3rd element of the stack" ><FONT color="royalblue">SWAP2</FONT></TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x27 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1577" target="_blank" tooltip="Swap top and 2nd element of the stack" ><FONT color="royalblue">SWAP1</FONT></TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x28 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 2 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1097" target="_blank" tooltip="Pop top of stack" ><FONT color="royalblue">POP</FONT></TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x29 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1479" target="_blank" tooltip="Push 1 byte" ><FONT color="royalblue">PUSH1</FONT></TD><TD width="1" fixedsize="true" align="left"> 0x03</TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x2b </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 8 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="thistle" align="left" cellpadding="3" PORT="exit" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1255" target="_blank" tooltip="Uncoditional Jump" ><FONT color="purple">JUMP</FONT></TD></TR></TABLE></TD></TR> </TABLE> >] s_6 [label=<<TABLE ALIGN="LEFT" CELLBORDER="0" BORDER="0" cellpadding="0" CELLSPACING="1"> <TR><TD >Segment 6 [0x2c]</TD><TD href="" tooltip="Stack Size &#916;: 0&#10;Stack Size on Entry for this segment &#8805; 2&#10;Stack Size on Entry for this segment at this node &#8805; 3&#10;Exit Jump target: Constant 0x17"><FONT color="black">&#8505;&#65039;</FONT></TD></TR><HR/> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" PORT="entry">0x2c </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 1 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="thistle" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1334" target="_blank" tooltip="A valid destination for a jump" ><FONT color="purple">JUMPDEST</FONT></TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x2d </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1577" target="_blank" tooltip="Swap top and 2nd element of the stack" ><FONT color="royalblue">SWAP1</FONT></TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x2e </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1479" target="_blank" tooltip="Push 1 byte" ><FONT color="royalblue">PUSH1</FONT></TD><TD width="1" fixedsize="true" align="left"> 0x02</TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x30 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 5 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="#c6eb76" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L61" target="_blank" tooltip="Unsigned integer multiplication modulo TWO_256" ><FONT color="#316152">MUL</FONT></TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x31 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1577" target="_blank" tooltip="Swap top and 2nd element of the stack" ><FONT color="royalblue">SWAP1</FONT></TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x32 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 3 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="powderblue" align="left" cellpadding="3" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1479" target="_blank" tooltip="Push 1 byte" ><FONT color="royalblue">PUSH1</FONT></TD><TD width="1" fixedsize="true" align="left"> 0x17</TD></TR></TABLE></TD></TR> <TR><TD width="1" fixedsize="true" align="left"> <TABLE border="0" cellpadding="0" cellborder="0" CELLSPACING="1"><TR><TD width="1" fixedsize="false" align="left" cellpadding="1" >0x34 </TD> <TD width="1" fixedsize="false" align="left" cellpadding="1" tooltip="Gas: 8 " target="_blank" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/evm.dfy#L103">&#9981;</TD><TD width="1" fixedsize="true" style="Rounded" BORDER="0" BGCOLOR="thistle" align="left" cellpadding="3" PORT="exit" href="https://github.com/Consensys/evm-dafny/blob/60bce44ee75978a4c97b9eab8e03424c9c233bbd/src/dafny/bytecode.dfy#L1255" target="_blank" tooltip="Uncoditional Jump" ><FONT color="purple">JUMP</FONT></TD></TR></TABLE></TD></TR> </TABLE> >] s_0 -> s_1 [tooltip="Next"]; s_1 -> s_2 [tooltip="Next"]; s_1 -> s_3 [tooltip="Jump",color=forestgreen,style=dashed]; s_3 -> s_4 [tooltip="Next"]; s_4 -> s_5 [tooltip="Next"]; s_4 -> s_6 [tooltip="Jump",color=forestgreen,style=dashed]; s_5 -> s_1 [tooltip="Jump",color=forestgreen,style=dashed]; s_6 -> s_4 [tooltip="Jump",color=forestgreen,style=dashed]; } //----------------- Minimised CFG ------------------- ``` <caption><B>Figure 1</B>: A CFG with nested loops. Jumps are indicated with dashed arrows.</caption> </figure> </center> ### Valid CFGs One of the expected properties of CFGs is that they should [_over-approximate_](https://hackmd.io/@FranckC/rJIRA43Na#An-Algorithm-to-build-CFGs) the set of _feasible_ sequences of control locations in the concrete program. In other words, if the concrete program has an execution (for some input) that corresponds to a sequence of control locations $pc_0, pc_1, \ldots, pc_k$, then the CFG must contain a path that corresponds to $pc_0, pc_1, \ldots, pc_k$. CFGs that satisfy this property are **valid** CFGs. A trivial valid CFG is a graph that has edges between any two control locations. This is too coarse an over-approximation to be of any use. We want CFGs that are also **precise** enough to capture some useful information of the program. And this is why the CFG reconstruction problem is non-trivial. In a previous [note](https://hackmd.io/@FranckC/rJIRA43Na) I have presented an algorithm to construct valid and precise CFGs. ### What can we do with CFGs? #### Graph properties In the example of Figure 1 above we have a valid and precise enough CFG to learn some interesting properties from the graph. A first property is that there are _strongly connected components_^[A strongly connected component is a subgraph in which there is a path from each node to any another node.] in the graph. This indicates that there are probably loops (in fact there is a nested loop) in the EVM bytecode. A second property is that the code at Segments 0 and 2 is only executed once (it is not on a loop). Another _surfacing_ property is that the EVM is definitely a stack machine :smiley:: the blue instructions in the CFG are stack operations and they obviously form the majority of the code. #### Optimisations CFGs are used by compilers to _optimise_ the code. Optimisations like _contants propagation_, _minimisation of the number of registers_ are often computed using a CFG and some program analysis techniques (e.g. reaching definitions, slicing). A CFG can also be the input to _static analysers_ e.g. in _software verification_ techniques based on abstraction refinement. #### Known limitations As the CFG is an over-approximation there are properties of the program that are not captured by its CFG: for instance, how many times a loop can be entered. The CFG above accepts arbitrary number of iterations for each of the two loops. More generally, a CFG does not _evaluate_ conditions but rather assumes that any condition that is used in a `JUMPI` can be sometimes true and sometimes false. ## How to use the CFG generator and Who can use it? ### Usage The CFG generator is available in C#, Java and Python. You can find the artefacts in the [build](https://github.com/franck44/evm-dis/tree/main/build/libs) folder of the repository. For instance, the Java build is run as follows: ```zsh macbook1> java -jar evmdis.jar usage: <this program> [--help] [--dis] [--proof] [--segment] [--all] [--lib] arg0 [--cfg] arg0 [--raw] arg0 <string> options --help [-h] Display help and exit --dis [-d] Disassemble <string> --proof [-p] Generate proof object for <string> --segment [-s] Print segment of <string> --all [-a] Same as -d -p --lib [-l] The path to the Dafny-EVM source code. Used to add includes files in the proof object. --cfg [-c] Max depth. Control flow graph in DOT format --raw [-r] Display non-minimised and minimised CFGs ``` The input to the CFG generator is a _string_, hexadecimal bytecode, like the one produced by `solc -bin-runtime`. If you want to feed the CFG generator with a file you may just use `$(<file.bin)` to _pipe_ the content of the file to the input to the CFG generator. The [usage](https://github.com/franck44/evm-dis#usage) section of the `README` in the git repository provides guidance how to use the generator. The generator can output several artefacts: - the **disassembled bytecode** (`--dis`) i.e. a readable version of the hexadecimal string; - the **list of segments** in the bytecode (`--segment`); - the **CFG of the bytecode** (`--cfg`). This option takes a parameter which is the maximum depth when unfolding the graph. For large contracts e.g. an ERC-20, or the Deposit Contract, a max depth of 100 is enough. This max depth is there to ensure termination of the algorithm. If the max depth is not large enough, some traces may not be fully explored and this is reflected in the ouput by self-loops on some nodes in the graph. If that happens, you may increase the max depth and start again. - **minimised CFGS** and _raw_ CFGs. The `--raw` flag will output two versions of the CFG: a non-minimised and a minimised one. This is only useful for small code snippets, otherwise it gets very large very quickly, so better use the minimised version if you can. ### Who is it for? Generating CFG is useful if you want to **learn** what EVM bytecode is and how it works. CFGs as the one in Figure 1 provides a readable view of the bytecode. If you want to learn how the `solc` compiler compiles Solidity code with `if-the-else`, `while loops` or complex data structures, using this tool may help you to do so. There are _tooltips_ and annotations to the instructions and segments so you can check what the _semantics of an instruction is_ or what is the effect of a segment on the stack size, or gas costs of simple instructions. If you are interested in **analysing** or **auditing** the bytecode^[Compilers from Solidity to EVM bytecode are not _certified_ correct, so even if you are confident your high-level code is good enough, the bytecode generated by the compiler may be flawed. Several serious compilers bugs have been reported in the last year.], this tool may also help. You can use the CFG directly to _review_ the code, but also feed the CFG to automatic analysis tools e.g. [Rattle](https://www.alchemy.com/dapps/rattle), [EthIR](https://github.com/costa-group/EthIR). A direct inspection of the graph may reveal that there are some `INVALID` instructions that are reachable and this may need further investigation. It may also reveal that there is no `RETURN` instruction that is reachable in the CFG and in that case the bytecode never terminates normally. At the moment the CFG is generated in [DOT](https://graphviz.org/doc/info/lang.html) format but it is relatively easy to implement the generation to other target languages. If you are a **compiler** developer, and this is true not only for Solidity to EVM but for other compilers too, you may use the CFG generator to check compilation strategies and compare the results of different ones, or to _optimise_ some sections of the compiled code. For instance, if you look at the CFG of the [Deposit Contrat in the repository](https://github.com/franck44/evm-dis/blob/21e2c7496a627bb9b66f3f7df95d29b8a4a153fd/src/dafny/tests/src/Deposit/depositContract-cfg.svg), you may see that there are a few `INVALID` isntructions in the compiled code, and that several segments are duplicated: the same sequence of instructions appear several times in the bytecode at different locations. This may be optimised away and save some precious space. Regarding optimisations, `solc` does not seem to have a lot of strategies to apply and using a precise CFG may help desiging better optimisations (e.g. using reaching definitions, slicing, etc). Finally, another avenue is to use this tool for **formal verification**. This is actually my primary motivation and you may have noticed that there is a `--proof` option in the generator that I have not discussed yet. This option produces some [Dafny](https://github.com/dafny-lang/dafny) code, a _proof object_, that uses the [Dafny-EVM](https://github.com/Consensys/evm-dafny) semantics [1]. This provides a way to _automatically reason_ about the bytecode. This feature is not fully implemented and I'll discuss it in another post. ## How I implemented the Algorithm I have used [Dafny](https://github.com/dafny-lang/dafny) a lot in the last five years, mostly for _formal verification_ purposes, e.g. [1], [2], [3] and [4]. Dafny is a _verification-friendly programming language_ and I was eager to try and develop real software with Dafny. The overall experience is great, although I am strongly biased as I am a formal verification person. How did I benefit from using a verification-friendly programming language to develop this piece of software? 1. I never had to debug errors like `array-out-of-bounds`, `undeflow/overflow`, loop termination. The Dafny compiler enforces the programmer to fix these issues before executing the code. To be fair, you can bypass the verification stage in Dafny, and I have tried that in two instances. My motivation was that the "functions" I had written were so obvious that I did not need to provide a proof _now_, I could do it later and _execute_ the code now. In both instances, this was a mistake. The code I had written was flawed, and I discovered the flaws (`infinite loop` and `off-by-one` in a list) when writing the proofs. 2. I could write _tests_ that are _exhaustive_, e.g. in the sense that I start with an arbitrary input sequence of `nat`s, and can prove some properties of my functions _for all_ sequences of `nat`s. At the same time I wrote some real and concrete tests to check that some functions were computing the expected results. Both approaches are complementary. 4. I used _constrained types_ a lot. This is similar to _dependent types_ and provides a lot of safety in the code. For instance, I have defined an [Instruction datatype](https://github.com/franck44/evm-dis/blob/74eaca0c0c887f320768f69c87b9e122e9a185a9/src/dafny/utils/Instructions.dfy#L48). I have added a predicate to define _valid_ instructions and a type `ValidInstruction` that are the `Instruction`s that satisfy the `Valid` predicate. I have done that for several datatypes in the code base. What does it buy me? I saved a huge amount of time^[Arguably this is not a specific property of Dafny but a common property of _dependent type_ or strongly typed languages.] not having to deal with _ill-formed_ `Instruction`s, for instance whe pretty-priting them. 5. One of the main "idioms" in Dafny is to use pre- and postconditions to prove properties of functions. I have used it a lot, and the Dafny verification engine makes sure that every time you _call a function_ the preconditions are satisfied. What is amazing is that some postconditions can be proved by Dafny _without any hints_ but under the hood the proof requires reasoning by _induction_. A good example is the [BuildCFG function](https://github.com/franck44/evm-dis/blob/74eaca0c0c887f320768f69c87b9e122e9a185a9/src/dafny/CFGBuilder/BuildCFG.dfy#L39) that builds the CFG for which I have written several constraints and postconditions on the sizes of _paths_. This helps the programmer to understand their code better and get more confidence about what is computed. 6. Dafny has several backends to generate artefacts in different languages. I have been able to generate the Java, C# and Python arfetacts. This makes the Dafny code I have written available in several languages and it can be re-used in projects suign these languages. More Dafny backends generators^[The code generators are not _certified_ correct, so there may be (and there are) bugs in the translation to some target languages.] are being developed (e.g. Go, Rust, JS) and I expect to generate more artefacts in a near future. ## Conclusion CFGs are instrumental to code analysis and optimisations. Hopefully a tool like the one I presented in this post to generate precise CFGs, can help to get a better understanding of EVM bytecode. A online demo version is available at [www.bytespector.org](https://bytespector.org/#). My main motivation in building CFGs is to use the CFGs to generate _proof objects_ for EVM bytecode. A _proof object_ can be thought of as _instrumented bytecode_ and can be used with the [Dafny-EVM](https://github.com/Consensys/evm-dafny) to reason and prove properties of contracts at the bytecode level. I'll report on this work later in a separate post. ## References [1] Cassez, F., Fuller, J., Ghale, M.K., Pearce, D.J., Quiles, H.M.A. (2023). **Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny**. In: Chechik, M., Katoen, JP., Leucker, M. (eds) _Formal Methods_. FM 2023. Lecture Notes in Computer Science, vol 14000. Springer, Cham. [DOI](https://doi.org/10.1007/978-3-031-27481-7_32) [2] Cassez, F., Fuller, J., Asgaonkar, A. (2022). **Formal Verification of the Ethereum 2.0 Beacon Chain**. In: Fisman, D., Rosu, G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022. Lecture Notes in Computer Science, vol 13243. Springer, Cham. [DOI](https://doi.org/10.1007/978-3-030-99524-9_9) [3] Cassez, F., Fuller, J., Quiles, H.M.A. (2022). **Deductive Verification of Smart Contracts with Dafny**. In: Groote, J.F., Huisman, M. (eds) Formal Methods for Industrial Critical Systems. FMICS 2022. Lecture Notes in Computer Science, vol 13487. Springer, Cham. [DOI](https://doi.org/10.1007/978-3-031-15008-1_5) [4] Cassez, F. (2021). **Verification of the Incremental Merkle Tree Algorithm with Dafny**. In: Huisman, M., Păsăreanu, C., Zhan, N. (eds) Formal Methods. FM 2021. Lecture Notes in Computer Science(), vol 13047. Springer, Cham. [DOI](https://doi.org/10.1007/978-3-030-90870-6_24) [^fn]: