Formally check custom Solidity assertions

CONTRIBUTING.md

@@ -12,7 +12,7 @@ Or even better, send us a PR :)
 # Running the tests
 
 There are two options to run the tests, which are concrete execution and symbolic execution.
-Before running the test you have to choose an option. There is a global variable named `UNIT_TEST` in `test_evm/global_test_params.py` to set the type of the tests.
+Before running the test you have to choose an option. There is a global variable named `UNIT_TEST` in `global_test_params.py` to set the type of the tests.
 
 ```
 # Testing concrete execution

assertion.py

@@ -0,0 +1,82 @@
+class Assertion:
+    def __init__(self, block_from):
+        # Block that contains the test (assertion)
+        self.block_from = block_from
+
+        # Was the assertion violated?
+        self.violated = False
+
+        # If the assertion was violated,
+        # store the counterexample
+        self.model = None
+
+        # SMT2 query to decide the assertion
+        self.query = None
+
+        # Solidity function that might contain this assertion
+        self.function = None
+
+        # Branch that led to the assertion failure
+        self.path = None
+
+        # Symbolic constraints of that path
+        self.sym = None
+
+    def set_sym(self, sym):
+        self.sym = sym
+
+    def get_sym(self):
+        return self.sym
+
+    def set_path(self, path):
+        self.path = path
+
+    def get_path(self):
+        return self.path
+
+    def set_function(self, function):
+        self.function = function
+
+    def get_function(self):
+        return self.function
+
+    def get_block_from(self):
+        return self.block_from
+
+    def is_violated(self):
+        return self.violated
+
+    def set_violated(self, violated):
+        self.violated = violated
+
+    def get_model(self):
+        return self.model
+
+    def set_model(self, model):
+        self.model = model
+
+    def get_query(self):
+        return self.query
+
+    def set_query(self, query):
+        self.query = query
+
+    def __str__(self):
+        s =  "================\n"
+        s += "Assertion from block " + str(self.block_from) + "\n"
+        #s += "SMT2 query:\n" + str(self.query) + "\n"
+        s += "Violated: " + str(self.violated) + "\n"
+        s += "Function: "
+        if self.function == None:
+            s += "?\n"
+        else:
+            s += self.function + "\n"
+        if self.violated:
+            s += "Model:\n"
+            for decl in self.model.decls():
+                s += str(decl.name()) + " = " + str(self.model[decl]) + ", "
+        return s
+
+    def display(self):
+        print self.__str__()
+

global_params.py

@@ -51,3 +51,6 @@
 
 # Take state data from state.json to speed up the symbolic execution
 INPUT_STATE = 0
+
+# Check assertions
+CHECK_ASSERTIONS = 0

opcodes.py

@@ -71,6 +71,7 @@
     "CALLCODE": [0xf2, 7, 1],
     "RETURN": [0xf3, 2, 0],
     "REVERT": [0xfd, 2, 0],
+    "ASSERTFAIL": [0xfe, 0, 0],
     "DELEGATECALL": [0xf4, 6, 1],
     "BREAKPOINT": [0xf5, 0, 0],
     "RNGSEED": [0xf6, 1, 1],
@@ -126,7 +127,7 @@
     "Gblockhash": 20
 }
 
-Wzero = ("STOP", "RETURN", "REVERT")
+Wzero = ("STOP", "RETURN", "REVERT", "ASSERTFAIL")
 
 Wbase = ("ADDRESS", "ORIGIN", "CALLER", "CALLVALUE", "CALLDATASIZE",
          "CODESIZE", "GASPRICE", "COINBASE", "TIMESTAMP", "NUMBER",

oyente.py

@@ -84,11 +84,13 @@ def analyze(processed_evm_file, disasm_file):
         of.write(disasm_out)
 
     # Run symExec
-    symExec.main(disasm_file)
-
+    symExec.main(disasm_file, args.source)
+    
 def main():
     # TODO: Implement -o switch.
 
+    global args
+
     parser = argparse.ArgumentParser()
     group = parser.add_mutually_exclusive_group(required=True)
     group.add_argument("-s", "--source", type=str,
@@ -125,6 +127,8 @@ def main():
     parser.add_argument(
         "-w", "--web", help="Run Oyente for web service", action="store_true")
     parser.add_argument("-glt", "--global-timeout", help="Timeout for symbolic execution", action="store", dest="global_timeout", type=int)
+    parser.add_argument(
+        "-a", "--assertion", help="Check assertion failures.", action="store_true")
 
     args = parser.parse_args()
 
@@ -142,6 +146,7 @@ def main():
     global_params.INPUT_STATE = 1 if args.state else 0
     global_params.WEB = 1 if args.web else 0
     global_params.STORE_RESULT = 1 if args.json else 0
+    global_params.CHECK_ASSERTIONS = 1 if args.assertion else 0
 
     if args.depth_limit:
         global_params.DEPTH_LIMIT = args.depth_limit