EVM: Support exp aka pow

.travis.yml

@@ -19,6 +19,7 @@ env:
   matrix:
     - TEST_TYPE=examples
     - TEST_TYPE=ethereum
+    - TEST_TYPE=ethereum_vm
     - TEST_TYPE=native
     - TEST_TYPE=other
 
@@ -52,7 +53,7 @@ install:
   - scripts/travis_install.sh $TEST_TYPE
 
 script:
-  - scripts/travis_test.sh $TEST_TYPE
+  - travis_wait 60 scripts/travis_test.sh $TEST_TYPE
 
 after_success:
   - ./cc-test-reporter format-coverage -t coverage.py -o "coverage/codeclimate.$TEST_TYPE.json"

manticore/platforms/evm.py

@@ -432,10 +432,18 @@ def wrapper(*args, **kwargs):
                 if policy == "ACCOUNTS":
                     value = args[index]
                     world = args[0].world
-                    #special handler for EVM only policy
+                    # special handler for EVM only policy
                     cond = world._constraint_to_accounts(value, ty='both', include_zero=True)
                     world.constraints.add(cond)
                     policy = 'ALL'
+
+                if args[index].taint:
+                    # TODO / FIXME: The taint should persist!
+                    logger.warning(
+                        f"Concretizing {func.__name__}'s {index} argument and dropping its taints: "
+                        "the value might not be tracked properly (in case of using detectors)"
+                    )
+
                 raise ConcretizeArgument(index, policy=policy)
             return func(*args, **kwargs)
         wrapper.__signature__ = inspect.signature(func)
@@ -1209,12 +1217,22 @@ def nbytes(e):
             return result
         return EXP_SUPPLEMENTAL_GAS * nbytes(exponent)
 
+    @concretized_args(base='SAMPLED', exponent='SAMPLED')
     def EXP(self, base, exponent):
         """
-            Exponential operation
-            The zero-th power of zero 0^0 is defined to be one
+        Exponential operation
+        The zero-th power of zero 0^0 is defined to be one.
+
+        :param base: exponential base, concretized with sampled values
+        :param exponent: exponent value, concretized with sampled values
+        :return: BitVec* EXP result
         """
-        # fixme integer bitvec
+        if exponent == 0:
+            return 1
+
+        if base == 0:
+            return 0
+
         return pow(base, exponent, TT256)
 
     def SIGNEXTEND(self, size, value):
@@ -1284,7 +1302,7 @@ def try_simplify_to_constant(self, data):
             if isinstance(simplified, Constant):
                 concrete_data.append(simplified.value)
             else:
-                #simplify by solving. probably means that we need to improve simplification
+                # simplify by solving. probably means that we need to improve simplification
                 solutions = solver.get_all_values(self.constraints, simplified, 2, silent=True)
                 if len(solutions) != 1:
                     break

scripts/travis_test.sh

@@ -93,8 +93,9 @@ run_examples() {
 
 # Test type
 case $1 in
-    native)     ;&  # Fallthrough
-    ethereum)   ;&  # Fallthrough
+    native)         ;&  # Fallthrough
+    ethereum)       ;&  # Fallthrough
+    ethereum_vm)    ;&  # Fallthrough
     other)
         echo "Running only the tests from 'tests/$1' directory"
         run_tests_from_dir $1
@@ -114,6 +115,8 @@ case $1 in
         RV=$(($RV + $?))
         run_tests_from_dir ethereum
         RV=$(($RV + $?))
+        run_tests_from_dir ethereum_vm
+        RV=$(($RV + $?))
         run_tests_from_dir other
         RV=$(($RV + $?))
         run_examples

tests/auto_generators/make_VMTests.py

@@ -4,14 +4,14 @@
 ### TO GENERATE ALL:
 
 ## Initialize env:
-cd manticore/tests/ethereum && mkdir VMTests_concrete && mkdir VMTests_symbolic
+cd manticore/tests/ && mkdir -p  ethereum_vm/VMTests_concrete && mkdir ethereum_vm/VMTests_symbolic
 git clone https://github.com/ethereum/tests --depth=1
 
 ## Generate concrete tests:
-for i in ./tests/VMTests/*; do python ../auto_generators/make_VMTests.py $i; done
+for i in ./tests/VMTests/*; do python ./auto_generators/make_VMTests.py $i; done
 
 ## Generate symbolic tests:
-$ for i in ./tests/VMTests/*; do python ../auto_generators/make_VMTests.py $i --symbolic; done
+$ for i in ./tests/VMTests/*; do python ./auto_generators/make_VMTests.py $i --symbolic; done
 
 ## Remove the eth tests repo
 $ rm -rf ./tests  # cleanup/remove the ethereum/tests repo
@@ -90,7 +90,7 @@ def solve(val):
             Those tests are **auto-generated** and `solve` is used in symbolic tests.
             So yes, this returns just val; it makes it easier to generate tests like this.
             """
-            return val
+            return to_constant(val)
 '''
 
     env = testcase['env']
@@ -164,7 +164,7 @@ def format_var(name, val):
 '''
             else:
                 output += f'''
-        world.set_storage_data(acc['address'], {key}, {value})
+        world.set_storage_data(acc_addr, {key}, {value})
 '''
 
     address = int(testcase['exec']['address'], 0)
@@ -269,7 +269,7 @@ def generate_post_output(testcase):
 
     output += '''
         # check logs
-        logs = [Log(unhexlify('{:040x}'.format(l.address)), l.topics, to_constant(l.memlog)) for l in world.logs]
+        logs = [Log(unhexlify('{:040x}'.format(l.address)), l.topics, solve(l.memlog)) for l in world.logs]
         data = rlp.encode(logs)'''
     output += f'''
         self.assertEqual(sha3.keccak_256(data).hexdigest(), '{testcase['logs'][2:]}')
@@ -366,9 +366,9 @@ def tearDownClass(cls):
 
     if folder:
         testname = folder.split('/')[-1]
-        with open(f'VMTests_{postfix}/test_{testname}.py', 'w') as f:
+        with open(f'ethereum_vm/VMTests_{postfix}/test_{testname}.py', 'w') as f:
             f.write(output)
-        with open(f'VMTests_{postfix}/__init__.py', 'w') as f:
+        with open(f'ethereum_vm/VMTests_{postfix}/__init__.py', 'w') as f:
             f.write("# DO NOT DELETE")
         print("Tests generated. If this is the only output, u did sth bad.", file=sys.stderr)
     else:

tests/ethereum/VMTests_concrete/test_VMTests.py → tests/ethereum_vm/VMTests_concrete/test_VMTests.py

@@ -53,7 +53,7 @@ def solve(val):
             Those tests are **auto-generated** and `solve` is used in symbolic tests.
             So yes, this returns just val; it makes it easier to generate tests like this.
             """
-            return val
+            return to_constant(val)
 
         constraints = ConstraintSet()
 
@@ -91,7 +91,7 @@ def solve(val):
         except evm.EndTx as e:
             result = e.result
             if result in ('RETURN', 'REVERT'):
-                returndata = to_constant(e.data)
+                returndata = solve(e.data)
         except evm.StartTx as e:
             self.fail('This tests should not initiate an internal tx (no CALLs allowed)')
 
@@ -110,7 +110,7 @@ def solve(val):
         # check outs
         self.assertEqual(returndata, unhexlify(''))
         # check logs
-        logs = [Log(unhexlify('{:040x}'.format(l.address)), l.topics, to_constant(l.memlog)) for l in world.logs]
+        logs = [Log(unhexlify('{:040x}'.format(l.address)), l.topics, solve(l.memlog)) for l in world.logs]
         data = rlp.encode(logs)
         self.assertEqual(sha3.keccak_256(data).hexdigest(), '1dcc4de8dec75d7aab85b567b6ccd41ad312451b948a7413f0a142fd40d49347')