Improvements to PHI instruction handling

.github/workflows/python-app.yml

@@ -4,6 +4,7 @@
 name: Tests
 
 on:
+  pull_request:
   workflow_dispatch:
   schedule:
     - cron: "0 0 * * *"
@@ -15,7 +16,7 @@ jobs:
     outputs:
       should_run: ${{ steps.should_run.outputs.should_run }}
     steps:
-    - uses: actions/checkout@v3
+    - uses: actions/checkout@v4
     - name: print latest_commit
       run: echo ${{ github.sha }}
     - id: should_run
@@ -28,9 +29,9 @@ jobs:
     if: ${{ needs.check_date.outputs.should_run != 'false' }}
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v3
+    - uses: actions/checkout@v4
     - name: Set up Python 3.8
-      uses: actions/setup-python@v4
+      uses: actions/setup-python@v5
       with:
         python-version: 3.8
     - uses: actions/cache@v3

.vscode/settings.json

@@ -0,0 +1,7 @@
+{
+    "python.testing.pytestArgs": [
+        "tests"
+    ],
+    "python.testing.unittestEnabled": false,
+    "python.testing.pytestEnabled": true
+}

docs/docs/core.md

@@ -113,7 +113,7 @@ A state offers many API for its inspection:
 
 ```python
 >>> entry_state.curr_stmt # print the current statement ready for execution
->>> entry_state.revert # weather the state reverted or not
+>>> entry_state.revert # whether the state reverted or not
 >>> entry_state.instruction_count # how many instructions have been executed up to this point
 >>> entry_state.pc # current program counter 
 >>> entry_state.registers # overview of all the virtual registers defined during the execution up to this point
@@ -162,4 +162,4 @@ The default solver employed by greed is [Yices2](https://github.com/SRI-CSL/yice
 We made this decision based on the impressive results obtained in the latest SMT solving competition, and based on the results showed by Frank et al. in [ETHBMC](https://www.usenix.org/system/files/sec20fall_frank_prepub_0.pdf).
 That being said, greed offers a modular architecure and implementing support for a new solver backend is quite straigthforward.
 
-By default, we give unlimited time to the solver to solve the constraints. However, it can be sometimes helpful to timeout after a certain amount of time. You can do this by using the option `SOLVER_TIMEOUT`. Keep in mind that, when the timeout fires, the state will be reported as `errored`.
+By default, we give unlimited time to the solver to solve the constraints. However, it can be sometimes helpful to timeout after a certain amount of time. You can do this by using the option `SOLVER_TIMEOUT`. Keep in mind that, when the timeout fires, the state will be reported as `errored`.

greed/TAC/TAC_parser.py

@@ -5,6 +5,7 @@
 from ast import literal_eval
 from collections import defaultdict
 from typing import Dict, List, Mapping, Tuple
+import networkx as nx
 
 from eth_utils import keccak
 
@@ -18,28 +19,42 @@
 
 log = logging.getLogger(__name__)
 
-
 class TAC_parser:
     """
     This class parses the TAC facts generated by Gigahorse and builds the CFG.
     """
     factory: Factory
     target_dir: str
 
-    phimap: Mapping[str, str]
     statement_to_blocks_map: Mapping[str, List[str]]
 
 
     def __init__(self, factory: Factory, target_dir: str):
         self.factory = factory
         self.target_dir = target_dir
 
-        self.phimap = None
         self.statement_to_blocks_map = None
 
     @staticmethod
     def stmt_sort_key(stmt_id: str) -> int:
-        return int(stmt_id.split('0x')[1].split('_')[0], base=16)
+        """
+        Statements may be identified by a number of different formats. This function
+        returns a key that can be used to sort them in a consistent way.
+
+        Possible formats:
+        - 0x12345
+        - 0x12345_0x456
+        - 0x12345S0x456
+        """
+        if '_' in stmt_id:
+            assert 'S' not in stmt_id
+            return int(stmt_id.split('_')[1], base=16)
+        elif 'S' in stmt_id:
+            assert '_' not in stmt_id
+            return int(stmt_id.split('0x')[1].split('S')[0], base=16)
+        else:
+            return int(stmt_id.split('0x')[1], base=16)
+
 
     def parse_statements(self) -> Dict[str, TAC_Statement]:
         # Load facts
@@ -87,7 +102,7 @@ def parse_statements(self) -> Dict[str, TAC_Statement]:
         # parse all statements block after block
         statements: Dict[str, TAC_Statement] = dict()
         for block_id in itertools.chain(*tac_function_blocks.values()):
-            for stmt_id in sorted(tac_block_stmts[block_id], key=TAC_parser.stmt_sort_key):
+            for stmt_id in tac_block_stmts[block_id]:
                 opcode = tac_op[stmt_id]
                 raw_uses = [var for var, _ in sorted(tac_uses[stmt_id], key=lambda x: x[1])]
                 raw_defs = [var for var, _ in sorted(tac_defs[stmt_id], key=lambda x: x[1])]
@@ -101,7 +116,7 @@ def parse_statements(self) -> Dict[str, TAC_Statement]:
                 # Adding metadata for CALL statements
                 if stmt_id in fixed_calls:
                     log.debug(f"Setting {statement} as fixed call to {fixed_calls[stmt_id]}")
-                    statement.set_likeyl_known_target_func(fixed_calls[stmt_id])
+                    statement.set_likely_known_target_func(fixed_calls[stmt_id])
 
             if not tac_block_stmts[block_id]:
                 # Gigahorse sometimes creates empty basic blocks. If so, inject a NOP statement
@@ -112,46 +127,6 @@ def parse_statements(self) -> Dict[str, TAC_Statement]:
         fake_exit_stmt = TAC_Stop(block_id='fake_exit', stmt_id='fake_exit')
         statements['fake_exit'] = fake_exit_stmt
 
-        # parse phi-map and re-write statements
-        # build phi-map (as in gigahorse decompiler)
-        phimap = dict()
-        for stmt in statements.values():
-            if stmt.__internal_name__ != 'PHI':
-                continue
-            #phimap[stmt.res1_var] = stmt.res1_var
-            for v in stmt.arg_vars:
-                if v in phimap:
-                    phimap[stmt.res1_var] = phimap[v]
-                    continue
-                phimap[v] = stmt.res1_var
-
-        # propagate phi map
-        fixpoint = False
-        while not fixpoint:
-            fixpoint = True
-            for v_old, v_new in phimap.items():
-                # (phimap[v_old] != phimap[v_new]) --> means "not already at local fixpoint"
-                if v_new in phimap and (phimap[v_old] != phimap[v_new]):
-                    phimap[v_old] = phimap[v_new]
-                    fixpoint = False
-
-        self.phimap = phimap
-
-        # rewrite statements according to PHI map
-        for stmt in statements.values():
-            if stmt.__internal_name__ == "PHI":
-                # remove all phi statements
-                statements[stmt.id] = TAC_Nop(block_id=stmt.block_id, stmt_id=stmt.id)
-                continue
-            # rewrite other statements according to the phi map
-            stmt.arg_vars = [phimap.get(v, v) for v in stmt.arg_vars]
-            stmt.arg_vals = {phimap.get(v, v): val for v, val in stmt.arg_vals.items()}
-            stmt.res_vars = [phimap.get(v, v) for v in stmt.res_vars]
-            stmt.res_vals = {phimap.get(v, v): val for v, val in stmt.res_vals.items()}
-
-            # re-process args
-            stmt.process_args()
-
         return statements
 
     def parse_blocks(self) -> Dict[str, Block]:
@@ -188,6 +163,7 @@ def parse_blocks(self) -> Dict[str, Block]:
 
         return blocks
 
+
     def parse_functions(self) -> Dict[str, TAC_Function]:
         # Load facts
         tac_block_function = load_csv_map(f"{self.target_dir}/InFunction.csv")
@@ -229,7 +205,7 @@ def parse_functions(self) -> Dict[str, TAC_Function]:
         # rewrite aliases according to PHI map
         translate_alias = lambda alias: 'v' + alias.replace('0x', '')
         for function in functions.values():
-            function.arguments = [self.phimap.get(translate_alias(a), translate_alias(a)) for a in function.arguments]
+            function.arguments = [translate_alias(a) for a in function.arguments]
 
         return functions
 
@@ -239,7 +215,7 @@ def parse_blocks_in_loop(self):
 
     def parse_induction_variables(self):
         induction_variables = load_csv_multimap(f"{self.target_dir}/InductionVariable.csv", reverse=True)
-        induction_variables = {x: {self.phimap.get('v' + _y.replace('0x', ''), 'v' + _y.replace('0x', '')) for _y in y}
+        induction_variables = {x: {'v' + _y.replace('0x', '') for _y in y}
                                for x, y in induction_variables.items()}
         return induction_variables
 
@@ -249,7 +225,6 @@ def parse_induction_variable_starts_at_const(self):
         for _x, _y, _z in values:
             y = _y[1:-1].split(", ")[1]
             y = 'v' + y.replace('0x', '')
-            y = self.phimap.get(y, y)
             starts_at_const[_x][y] = literal_eval(_z) # seems to not have a consistent base (either 10 or 16)
         return starts_at_const
 
@@ -259,7 +234,6 @@ def parse_induction_variable_increases_by_const(self):
         for _x, _y, _z in values:
             y = _y[1:-1].split(", ")[1]
             y = 'v' + y.replace('0x', '')
-            y = self.phimap.get(y, y)
             increases_by_const[_x][y] = literal_eval(_z) # seems to not have a consistent base (either 10 or 16)
         return increases_by_const
 
@@ -269,8 +243,7 @@ def parse_induction_variable_upper_bounds(self):
         for _x, _y, _z in values:
             y = _y[1:-1].split(", ")[1]
             y = 'v' + y.replace('0x', '')
-            y = self.phimap.get(y, y)
-            upper_bounds[_x][y] = self.phimap.get('v' + _z.replace('0x', ''), 'v' + _z.replace('0x', ''))
+            upper_bounds[_x][y] = 'v' + _z.replace('0x', '')
         return upper_bounds
 
     def parse_guarding_slots(self):
@@ -330,4 +303,4 @@ def parse_recovered_abi(self):
             if proto:
                 f.name = proto
 
-        return abi
+        return abi

greed/TAC/base.py

@@ -4,7 +4,6 @@
 
 from greed.solver.shortcuts import *
 from greed.state import SymbolicEVMState
-from greed.utils.exceptions import VMException
 
 log = logging.getLogger(__name__)
 
@@ -118,9 +117,12 @@ def set_arg_val(self, state: SymbolicEVMState):
                 if arg_val is not None:
                     log.warning(f"Uninitialized var {var} RECOVERED WITH CACHED CONSTANT VALUE")
                 else:
-                    raise VMException(f"Uninitialized var {var}")
+                    # raise VMException(f"Uninitialized var {var}")
+                    log.warning(f"Uninitialized var {var} - VERY LIKELY TO CAUSE PROBLEMS")
             val = state.registers.get(var, None) if arg_val is None else arg_val
-            state.registers[var] = val
+            # avoid assigning the same value to the register
+            if arg_val is not None:
+                state.registers[var] = val
             self.arg_vals[var] = val
             object.__setattr__(self, "arg{}_val".format(i + 1), val)
 

greed/TAC/flow_ops.py

@@ -1,7 +1,6 @@
 import logging
 
 from greed import options
-from greed import utils
 from greed.TAC.base import TAC_Statement
 from greed.solver.shortcuts import *
 from greed.state import SymbolicEVMState
@@ -112,22 +111,26 @@ def _handle(self, state: SymbolicEVMState, gas_val=None, address_val=None, value
         state.returndata['instruction_count'] = state.instruction_count
 
         if is_concrete(address_val) and bv_unsigned_value(address_val) == 0:
-            logging.info("Calling into burn contract")
+            log.info("Calling into burn contract")
+            if is_concrete(olen):
+                # If we have a concrete len for the return value we set the output memory to symbolic data
+                for i in range(bv_unsigned_value(olen)):
+                    state.memory[BV_Add(ostart, BVV(i, 256))] = BVS(f'EXT_{state.instruction_count}_{i}_{state.xid}', 8)
         elif is_concrete(address_val) and bv_unsigned_value(address_val) >= 1 and bv_unsigned_value(address_val) <= 8:
             # This is a pre-compiled contract
             #  --> https://www.evm.codes/precompiled?fork=arrowGlacier
             if bv_unsigned_value(address_val) == 1:
                 # ECRecover precompiled contract
                 # FIXME
-                logging.info("Calling precompiled ecRecover contract")
+                log.info("Calling precompiled ecRecover contract")
                 raise VMSymbolicError(f"Precompiled contract [ecRecover] not implemented")
             elif bv_unsigned_value(address_val) == 2:
                 # SHA256 precompiled contract
                 # FIXME
-                logging.info("Calling precompiled SHA2-256 contract")
+                log.info("Calling precompiled SHA2-256 contract")
                 raise VMSymbolicError(f"Precompiled contract [SHA2-256] not implemented")
             elif bv_unsigned_value(address_val) == 4:
-                logging.info("Calling precompiled identity contract")
+                log.info("Calling precompiled identity contract")
                 istart = argsOffset_val
                 ilen = argsSize_val
                 state.memory.memcopy(ostart, state.memory.copy(state), istart, ilen)
@@ -139,10 +142,8 @@ def _handle(self, state: SymbolicEVMState, gas_val=None, address_val=None, value
             # If we have a concrete len for the return value we set the output memory to symbolic data
             for i in range(bv_unsigned_value(olen)):
                 state.memory[BV_Add(ostart, BVV(i, 256))] = BVS(f'EXT_{state.instruction_count}_{i}_{state.xid}', 8)
-            log_address_val = bv_unsigned_value(address_val) if is_concrete(address_val) else "<SYMBOLIC>"
-
-            if log_address_val != "<SYMBOLIC>":
-                logging.info(f"Calling contract {hex(log_address_val)} ({state.instruction_count}_{state.xid})")
+            log_address_val = hex(bv_unsigned_value(address_val)) if is_concrete(address_val) else "<SYMBOLIC>"
+            log.info(f"Calling contract {log_address_val} ({state.instruction_count}_{state.xid})")
         else:
             # FIXME: maybe consider a MAX_RETURN_SIZE option and use similar strategy used in SHA3
             raise VMSymbolicError("Unsupported symbolic retSize_val in CALL")
@@ -155,7 +156,7 @@ def _handle(self, state: SymbolicEVMState, gas_val=None, address_val=None, value
         state.set_next_pc()
         return [state]
 
-    def set_likeyl_known_target_func(self, target_function):
+    def set_likely_known_target_func(self, target_function):
         self.likely_known_target = target_function
 
 class TAC_Call(TAC_BaseCall):