Merge pull request #154 from luongnt95/update

Update

README.md

@@ -20,17 +20,25 @@ and you are done!
 
 Note - If need the [version of Oyente](https://github.com/melonproject/oyente/tree/290f1ae1bbb295b8e61cbf0eed93dbde6f287e69) referred to in the paper, run the container from [here](https://hub.docker.com/r/hrishioa/oyente/)
 
+## Installation
+
+To install Oyente, simply:
+
+```
+$ pip install oyente
+```
+
 ## Full install
 
 ### Install the following dependencies
-#### solc v0.4.13
+#### solc version 0.4.13
 ```
 $ sudo add-apt-repository ppa:ethereum/ethereum
 $ sudo apt-get update
 $ sudo apt-get install solc
 ```
 
-#### evm from [go-ethereum](https://github.com/ethereum/go-ethereum) version 1.6.1. 
+#### evm from [go-ethereum](https://github.com/ethereum/go-ethereum) version 1.6.1.
 
 1. https://geth.ethereum.org/downloads/ or
 2. By from PPA if your using Ubuntu
@@ -72,6 +80,9 @@ pip install web3
 #evaluate a local solidity contract
 python oyente.py -s <contract filename>
 
+#evaluate a local solidity with option -a to verify assertions in the contract
+pyhon oyente.py -a -s <contract filename>
+
 #evaluate a local evm contract
 python oyente.py -s <contract filename> -b
 
@@ -107,4 +118,4 @@ Some analytics regarding the number of contracts tested, number of contracts ana
 
 ## Contributing
 
-Checkout out our [contribution guide](https://github.com/melonproject/oyente/blob/master/CONTRIBUTING.md) and the code structure [here](https://github.com/melonproject/oyente/blob/master/code.md). 
+Checkout out our [contribution guide](https://github.com/melonproject/oyente/blob/master/CONTRIBUTING.md) and the code structure [here](https://github.com/melonproject/oyente/blob/master/code.md).

oyente/assertion.py

@@ -80,3 +80,11 @@ def __str__(self):
     def display(self):
         print self.__str__()
 
+    def display_on_web(self):
+        s =  "================\n"
+        s += "Assertion failure from function: "
+        if self.function == None:
+            s += "?\n"
+        else:
+            s += self.function + "\n"
+        return s

oyente/global_params.py

@@ -17,7 +17,7 @@
 CHECK_CONCURRENCY_FP = 0
 
 # Timeout for z3 in ms
-TIMEOUT = 1000
+TIMEOUT = 100
 
 # Set this flag to 1 if we want to do unit test from file unit_test.json
 # Set this flag to 2 if we want to do evm real value unit test
@@ -40,11 +40,11 @@
 STORE_RESULT = 0
 
 # depth limit for DFS
-DEPTH_LIMIT = 1000
+DEPTH_LIMIT = 50
 
 GAS_LIMIT = 4000000
 
-LOOP_LIMIT = 100
+LOOP_LIMIT = 10
 
 # Use a public blockchain to speed up the symbolic execution
 USE_GLOBAL_BLOCKCHAIN = 0

oyente/oyente.py

@@ -87,7 +87,7 @@ def analyze(processed_evm_file, disasm_file):
 
     # Run symExec
     symExec.main(disasm_file, args.source)
-    
+
 def main():
     # TODO: Implement -o switch.
 
@@ -100,6 +100,7 @@ def main():
     group.add_argument("-ru", "--remoteURL", type=str,
                        help="Get contract from remote URL. Solidity by default. Use -b to process evm instead.", dest="remote_URL")
 
+    parser.add_argument("--version", action="version", version="oyente one-north 0.2.0")
     parser.add_argument(
         "-b", "--bytecode", help="read bytecode in source instead of solidity file.", action="store_true")
 

oyente/run_tests.py

@@ -27,7 +27,7 @@ def status(exit_code):
 
 def main():
     test_dir = 'test_evm/test_data'
-    files = glob.glob(test_dir + '/vmArithmeticTest.json')
+    files = glob.glob(test_dir + '/*.json')
     test_cases = {}
 
     num_tests = num_passes = num_fails = \

oyente/symExec.py

@@ -127,9 +127,9 @@ def compare_stack_unit_test(stack):
         log.warning("FAILED UNIT-TEST")
         log.warning(e.message)
 
-def compare_storage_and_memory_unit_test(global_state, mem, analysis):
+def compare_storage_and_gas_unit_test(global_state, analysis):
     unit_test = pickle.load(open(PICKLE_PATH, 'rb'))
-    test_status = unit_test.compare_with_symExec_result(global_state, mem, analysis)
+    test_status = unit_test.compare_with_symExec_result(global_state, analysis)
     exit(test_status)
 
 def handler(signum, frame):
@@ -166,8 +166,9 @@ def detect_bugs():
         results['assertion_failure'] = is_fail
         if not isTesting():
             log.info("\t  Assertion fails: \t %s", str(is_fail))
-        for asrt in assertion_fails:
-            asrt.display()
+        if not global_params.WEB:
+            for asrt in assertion_fails:
+                asrt.display()
 
 def check_assertions():
     global assertions
@@ -293,6 +294,9 @@ def results_for_web():
         if not results.has_key("assertion_failure"):
             results["assertion_failure"] = False
         print "Assertion failure:", results['assertion_failure']
+        assertion_fails = [assertion for assertion in assertions if assertion.is_violated()]
+        for asrt in assertion_fails:
+            print asrt.display_on_web()
 
 
 def closing_message():
@@ -802,7 +806,7 @@ def sym_exec_block(block, pre_block, visited, depth, stack, mem, memory, global_
         if global_params.UNIT_TEST == 1:
             compare_stack_unit_test(stack)
         if global_params.UNIT_TEST == 2 or global_params.UNIT_TEST == 3:
-            compare_storage_and_memory_unit_test(global_state, mem, analysis)
+            compare_storage_and_gas_unit_test(global_state, analysis)
 
     elif jump_type[block] == "unconditional":  # executing "JUMP"
         successor = vertices[block].get_jump_target()

oyente/test_evm/evm_unit_test.py

@@ -20,13 +20,6 @@ def storage(self):
         storage = self.data['post'].values()[0]['storage']
         return storage if storage != None else {"0": "0"}
 
-    def mem(self):
-        memory = self.data['out']
-        if memory == "0x":
-            return memory + "00"
-        else:
-            return memory
-
     def gas_info(self):
         gas_limit = long(self.data['exec']['gas'], 0)
         gas_remaining = long(self.data['gas'], 0)
@@ -47,16 +40,14 @@ def _create_bytecode_file(self, bytecode):
             code_file.write('\n')
             code_file.close()
 
-    def compare_with_symExec_result(self, global_state, mem, analysis):
-        if UNIT_TEST == 2: return self.compare_real_value(global_state, mem, analysis)
+    def compare_with_symExec_result(self, global_state, analysis):
+        if UNIT_TEST == 2: return self.compare_real_value(global_state, analysis)
         if UNIT_TEST == 3: return self.compare_symbolic(global_state)
 
-    def compare_real_value(self, global_state, mem, analysis):
+    def compare_real_value(self, global_state, analysis):
         storage_status = self._compare_storage_value(global_state)
-        mem_status = self._compare_memory_value(mem)
         gas_status = self._compare_gas_value(analysis)
         if storage_status != PASS: return storage_status
-        if mem_status != PASS: return mem_status
         if gas_status != PASS: return gas_status
         return PASS
 
@@ -73,14 +64,6 @@ def _compare_storage_value(self, global_state):
                 return FAIL
         return PASS
 
-    def _compare_memory_value(self, mem):
-        memory = 0 if not mem else mem.values()[0]
-        memory = to_unsigned(long(memory))
-
-        if memory != long(self.mem(), 0):
-            return FAIL
-        return PASS
-
     def _compare_gas_value(self, analysis):
         gas_used = analysis['gas']
         gas_limit, gas_remaining = self.gas_info()

web/app/controllers/home_controller.rb

@@ -11,7 +11,7 @@ def analyze
       begin
         file.write oyente_params[:source]
         file.close
-        @output += `python #{ENV['OYENTE']}/oyente.py -s #{file.path} -w#{options} `
+        @output += `python #{ENV['OYENTE']}/oyente.py -s #{file.path} -w#{options} -a`
         UserMailer.analyzer_result_notification(oyente_params[:filename], file.path, @output, oyente_params[:email]).deliver_later
       rescue
         file.close