Better control of gas accounting

manticore/platforms/evm.py

@@ -67,6 +67,18 @@ def globalfakesha3(data):
     return None
 
 
+consts.add(
+    "gas",
+    default="static",
+    description=(
+        "Control how to keep the gas count"
+        "insane: Keep static and dynamic gas including transaction fee VERY EXPENSIVE (INSANE)."
+        "full: Keep static and dynamic gas excluding the dynamic aspect of transaction related fee."
+        "static: Use a static fee for each instruction. Dynamic gas is ignored. For example, memory, storage, refunds, tx dynamic fees are ignored"
+        "ignore: Ignore gas completely. Instructions won't consume gas"
+    ),
+)
+
 consts.add(
     "oog",
     default="ignore",
@@ -102,11 +114,7 @@ def globalfakesha3(data):
     default=-1,
     description="Max calldata size to explore in each CALLDATACOPY. Iff size in a calldata related instruction are symbolic it will be constrained to be less than this constant. -1 means free(only use when gas is being tracked)",
 )
-consts.add(
-    "ignore_balance",
-    default=False,
-    description="Do not try to solve symbolic balances",
-)
+consts.add("ignore_balance", default=False, description="Do not try to solve symbolic balances")
 
 
 # Auxiliary constants and functions
@@ -1061,6 +1069,11 @@ def _pop(self):
         return self.stack.pop()
 
     def _consume(self, fee):
+        if consts.gas == "ignore":
+            return 0
+        if consts.gas == "static":
+            assert not issymbolic(fee)
+
         # Check type and bitvec size
         if isinstance(fee, int):
             if fee > (1 << 512) - 1:
@@ -1167,11 +1180,14 @@ def _push_results(self, instruction, result):
             assert result is None
 
     def _calculate_gas(self, *arguments):
+        if consts.gas == "ignore":
+            return 0
         current = self.instruction
         implementation = getattr(self, f"{current.semantics}_gas", None)
-        if implementation is None:
-            return current.fee
-        return current.fee + implementation(*arguments)
+        fee = current.fee
+        if implementation is not None and consts.gas != "static":
+            fee += implementation(*arguments)
+        return fee
 
     def _handler(self, *arguments):
         current = self.instruction
@@ -2124,12 +2140,13 @@ def SWAP(self, *operands):
     ############################################################################
     # Logging Operations
     def LOG_gas(self, address, size, *topics):
-        return self._get_memfee(address, size)
+        GLOGBYTE = 8
+        fee = self.safe_mul(size, GLOGBYTE)
+        fee += self._get_memfee(address, size)
+        return fee
 
     @concretized_args(size="ONE")
     def LOG(self, address, size, *topics):
-        GLOGBYTE = 8
-        self._consume(self.safe_mul(size, GLOGBYTE))
         memlog = self.read_buffer(address, size)
         self.world.log(self.address, topics, memlog)
 
@@ -2164,14 +2181,15 @@ def CALL_gas(self, wanted_gas, address, value, in_offset, in_size, out_offset, o
         )
         fee += self._get_memfee(in_offset, in_size)
 
-        exception = False
         available_gas = self._gas
         available_gas -= fee
 
         exception = Operators.OR(
             Operators.UGT(fee, self._gas),
             Operators.ULT(self.safe_mul(available_gas, 63), available_gas),
         )
+        self.fail_if(exception)
+
         available_gas *= 63
         available_gas //= 64
 
@@ -2185,13 +2203,23 @@ def CALL_gas(self, wanted_gas, address, value, in_offset, in_size, out_offset, o
     @concretized_args(address="ACCOUNTS", in_offset="SAMPLED", in_size="SAMPLED")
     def CALL(self, gas, address, value, in_offset, in_size, out_offset, out_size):
         """Message-call into an account"""
+        if consts.gas in ("dynamic", "insane"):
+            tx_gas = self._temp_call_gas + Operators.ITEBV(512, value != 0, 2300, 0)
+        else:
+
+            available_gas = self._gas
+            available_gas *= 63
+            available_gas //= 64
+            wanted_gas = gas
+            tx_gas = Operators.ITEBV(256, available_gas < wanted_gas, available_gas, wanted_gas)
+
         self.world.start_transaction(
             "CALL",
             address,
             data=self.read_buffer(in_offset, in_size),
             caller=self.address,
             value=value,
-            gas=self._temp_call_gas + Operators.ITEBV(512, value != 0, 2300, 0),
+            gas=tx_gas,
         )
         raise StartTx()
 
@@ -2555,19 +2583,22 @@ def _transaction_fee(self, sort, address, price, bytecode_or_data, caller, value
 
         zerocount = 0
         nonzerocount = 0
-        if isinstance(bytecode_or_data, (Array, ArrayProxy)):
-            # if nothing was written we can assume all elements are default to zero
-            if len(bytecode_or_data.written) == 0:
-                zerocount = len(bytecode_or_data)
-        else:
-            for index in range(len(bytecode_or_data)):
-                try:
-                    c = bytecode_or_data.get(index, 0)
-                except AttributeError:
-                    c = bytecode_or_data[index]
-
-                zerocount += Operators.ITEBV(256, c == 0, 1, 0)
-                nonzerocount += Operators.ITEBV(256, c == 0, 0, 1)
+        if consts.gas == "insane":
+            if isinstance(bytecode_or_data, (Array, ArrayProxy)):
+                # if nothing was written we can assume all elements are default to zero
+                if len(bytecode_or_data.written) == 0:
+                    zerocount = len(bytecode_or_data)
+            else:
+                for index in range(len(bytecode_or_data)):
+                    try:
+                        c = bytecode_or_data.get(index, 0)
+                    except AttributeError:
+                        c = bytecode_or_data[index]
+
+                    zerocount += Operators.ITEBV(256, c == 0, 1, 0)
+                    nonzerocount += Operators.ITEBV(256, c == 0, 0, 1)
+        elif consts.gas == "full":
+            nonzerocount = len(bytecode_or_data)
 
         tx_fee += zerocount * GTXDATAZERO
         tx_fee += nonzerocount * GTXDATANONZERO

setup.py

@@ -65,7 +65,7 @@ def rtd_dependent_deps():
         "pysha3",
         "prettytable",
         "ply",
-        "rlp",
+        "rusty-rlp",
         "crytic-compile>=0.1.8",
         "wasm",
         "dataclasses; python_version < '3.7'",

tests/auto_generators/make_VMTests.py

@@ -7,11 +7,16 @@
 cd manticore/tests/ && mkdir -p  ethereum_vm/VMTests_concrete 
 git clone https://github.com/ethereum/tests --depth=1
 
+#(At manticore/tests/ folder)
 ## Get help
-python make_VMTest.py --help 
+python auto_generators/make_VMTest.py --help 
 
 ## Generate concrete tests:
-for i in  tests/BlockchainTests/ValidBlocks/VMTests/*/*json; do python make_VMTest.py -i $i --fork Istanbul -o ethereum_vm/VMTests_concrete; done
+for i in  tests/BlockchainTests/ValidBlocks/VMTests/*/*json; do python auto_generators/make_VMTest.py -i $i --fork Istanbul -o ethereum_vm/VMTests_concrete; done
+
+
+#Dependencies
+pip install py_evm
 
 """
 import argparse
@@ -90,6 +95,7 @@ class Log(rlp.Serializable):
 consts.mprocessing = consts.mprocessing.single
 consts = config.get_group('evm')
 consts.oog = 'pedantic'
+consts.gas = 'insane'
 
 class EVMTest(unittest.TestCase):
     # https://nose.readthedocs.io/en/latest/doc_tests/test_multiprocess/multiprocess.html#controlling-distribution
@@ -113,8 +119,8 @@ def gen_body(name, testcase):
     body = f'''
     def test_{name}(self):
         """
-        Testcase taken from https://github.com/ethereum/tests
         Source: {testcase['_info']['source']} 
+        Testcase taken from https://github.com/ethereum/tests
         """
         class UsedGas(Plugin):
             @property