Add SHL/SHR/SAR (#1498)

* Test skeleton

* Naive shift implementation

This should be interesting

* Revert "Add error for unsupported solc versions (#1488)"

This reverts commit 65c8930.

* Update readme

* Fix unclosed file warning

* Fix Truffle tests (maybe)

README.md

@@ -215,6 +215,10 @@ brew install unicorn
 UNICORN_QEMU_FLAGS="--python=`whereis python`" pip install unicorn
 ```
 
+### Solidity Versions
+Note that we're still in the process of implementing full support for the EVM Constantinople instruction semantics, so certain opcodes may not be supported.
+You may want to consider using a version of `solc` that's less likely to generate these opcodes (eg pre-0.5.0).
+
 ## Getting Help
 
 Feel free to stop by our #manticore slack channel in [Empire Hacking](https://empireslacking.herokuapp.com/) for help using or extending Manticore.

manticore/ethereum/manticore.py

@@ -6,7 +6,6 @@
 from queue import Empty as EmptyQueue
 from subprocess import check_output, Popen, PIPE
 from typing import Dict, Optional, Union
-from pkg_resources import parse_version
 
 import io
 import os
@@ -17,7 +16,6 @@
 import tempfile
 
 from crytic_compile import CryticCompile, InvalidCompilation, is_supported
-from crytic_compile.platform.solc import get_version
 
 from ..core.manticore import ManticoreBase
 from ..core.smtlib import (
@@ -734,14 +732,6 @@ def solidity_create_contract(
         while contract_names:
             contract_name_i = contract_names.pop()
             try:
-                # version check
-                binary = crytic_compile_args.get("solc", "solc")
-                version = get_version(binary)
-                if not parse_version(version) < parse_version("0.5.0"):
-                    raise EthereumError(
-                        f"Manticore requires a solc version < 0.5.0 and {version} was found"
-                    )
-
                 compile_results = self._compile(
                     source_code,
                     contract_name_i,

manticore/platforms/evm.py

@@ -73,7 +73,7 @@
 MASK160 = 2 ** 160 - 1
 TT255 = 2 ** 255
 TOOHIGHMEM = 0x1000
-DEFAULT_FORK = "byzantium"
+DEFAULT_FORK = "constantinople"
 
 # FIXME. We should just use a Transaction() for this
 PendingTransaction = namedtuple(
@@ -1509,6 +1509,18 @@ def BYTE(self, offset, value):
         offset = Operators.ITEBV(256, offset < 32, (31 - offset) * 8, 256)
         return Operators.ZEXTEND(Operators.EXTRACT(value, offset, 8), 256)
 
+    def SHL(self, a, b):
+        """Shift Left operation"""
+        return b << a
+
+    def SHR(self, a, b):
+        """Logical Shift Right operation"""
+        return b >> a
+
+    def SAR(self, a, b):
+        """Arithmetic Shift Right operation"""
+        return Operators.SAR(256, b, a)
+
     def try_simplify_to_constant(self, data):
         concrete_data = bytearray()
         for c in data:

scripts/travis_test.sh

@@ -88,11 +88,14 @@ run_truffle_tests(){
     cd truffle_tests
     truffle unbox metacoin
     manticore . --contract MetaCoin --workspace output
+    ### The original comment says we should get 41 states, but after implementing the shift
+    ### insructions, we get 31. Was the original comment a typo?
+
     # The correct answer should be 41
     # but Manticore fails to explore the paths due to the lack of the 0x1f opcode support
     # see https://github.com/trailofbits/manticore/issues/1166
     # if [ "$(ls output/*tx -l | wc -l)" != "41" ]; then
-    if [ "$(ls output/*tx -l | wc -l)" != "3" ]; then
+    if [ "$(ls output/*tx -l | wc -l)" != "31" ]; then
         echo "Truffle test failed"
         return 1
     fi

tests/auto_generators/make_VMTests.py

@@ -375,7 +375,9 @@ def _solve(self, constraints, val):
                 continue
 
             filename = os.path.join(folder, filename)
-            testcase = dict(json.loads(open(filename).read()))
+            fp = open(filename)
+            testcase = dict(json.loads(fp.read()))
+            fp.close()
             for name, testcase in testcase.items():
                 output += (
                     gen_test(testcase, filename, symbolic=symbolic, skip="Performance" in filename)
@@ -387,7 +389,9 @@ def _solve(self, constraints, val):
     else:
         folder = None
         filename = os.path.abspath(filename_or_folder)
-        testcase = dict(json.loads(open(filename).read()))
+        fp = open(filename)
+        testcase = dict(json.loads(fp.read()))
+        fp.close()
         for name, testcase in testcase.items():
             output += (
                 gen_test(testcase, filename, symbolic=symbolic, skip="Performance" in filename)