Clean examples/evm (#661)

* Clean examples/evm, add a new one

integer_overflow.py -> simple_int_overflow.sol
simple_functions.py -> simple_multi_func.sol
simple_transaction.py -> simple_value_check.sol

* Add umd example

examples/evm/integer_overflow.py

@@ -1,37 +0,0 @@
-from manticore.seth import ManticoreEVM, IntegerOverflow
-m = ManticoreEVM()
-m.register_detector(IntegerOverflow())
-
-#And now make the contract account to analyze
-source_code = '''
-pragma solidity ^0.4.15;
-contract Overflow {
-    uint private sellerBalance=0;
-    
-    function add(uint value) returns (uint){
-        sellerBalance += value; // complicated math with possible overflow
-
-        // possible auditor assert
-        assert(sellerBalance >= value); 
-        return sellerBalance;
-    } 
-}
-'''
-#Initialize user and contracts
-user_account = m.create_account(balance=1000)
-contract_account = m.solidity_create_contract(source_code, owner=user_account, balance=0)
-
-#First add won't overflow uint256 representation
-contract_account.add(m.make_symbolic_value())
-
-#Potential overflow
-contract_account.add(m.make_symbolic_value())
-
-#Let seth know we are not sending more transactions so it can output 
-# info about running states and global statistics
-m.finalize()
-print "[+] Look for results in %s"% m.workspace
-
-
-
-

examples/evm/simple_functions.py

@@ -1,37 +0,0 @@
-from manticore.seth import ManticoreEVM
-################ Script #######################
-
-m = ManticoreEVM()
-m.verbosity(2)
-#And now make the contract account to analyze
-# cat  | solc --bin 
-source_code = '''
-pragma solidity ^0.4.13;
-
-contract Test {
-    event Log(string);
-    mapping(address => uint) private balances;
-
-    function Test() {}
-    function target1() public {} 
-    function target2() internal {} 
-    function target3() private {} 
-    function() {}
-
-}
-'''
-#Initialize accounts
-user_account = m.create_account(balance=1000)
-contract_account = m.solidity_create_contract(source_code, owner=user_account)
-
-symbolic_data = m.make_symbolic_buffer(4) 
-symbolic_value = None 
-m.transaction(  caller=user_account,
-                   address=contract_account,
-                   value=symbolic_value,
-                   data=symbolic_data
-                 )
-
-m.finalize()
-print "[+] Look for results in %s"% m.workspace
-

examples/evm/simple_int_overflow.sol

@@ -0,0 +1,11 @@
+pragma solidity ^0.4.15;
+contract Overflow {
+    uint private sellerBalance=0;
+    
+    function add(uint value) returns (bool, uint){
+        sellerBalance += value; // complicated math with possible overflow
+
+        // possible auditor assert
+        assert(sellerBalance >= value); 
+    }
+}

examples/evm/simple_multi_func.sol

@@ -0,0 +1,13 @@
+pragma solidity ^0.4.13;
+
+contract Test {
+    event Log(string);
+    mapping(address => uint) private balances;
+
+    function Test() {}
+    function target1() public {} 
+    function target2() internal {} 
+    function target3() private {} 
+    function() {}
+
+}

examples/evm/simple_transaction.py

@@ -1,43 +0,0 @@
-from manticore.seth import ManticoreEVM
-################ Script #######################
-
-m = ManticoreEVM()
-m.verbosity(0)
-#And now make the contract account to analyze
-# cat  | solc --bin 
-source_code = '''
-pragma solidity ^0.4.13;
-
-contract Test {
-    event Log(string);
-
-    function target() payable public {
-        if (msg.value > 10)
-            Log("Value greater than 10");
-        else
-            Log("Value less or equal than 10");
-
-    } 
-
-}
-'''
-#Initialize accounts
-user_account = m.create_account(balance=1000)  
-contract_account = m.solidity_create_contract(source_code, owner=user_account)
-
-
-contract_account.target(value=m.SValue)
-
-
-print "[+] There are %d reverted states now"% len(m.final_state_ids)
-for state_id in m.final_state_ids:
-    print m.report(state_id)
-
-print "[+] There are %d alive states now"% len(m.running_state_ids)
-for state_id in m.running_state_ids:
-    print m.report(state_id)
-
-print "[+] Global coverage:"
-print m.coverage(contract_account)
-
-

examples/evm/simple_value_check.sol

@@ -0,0 +1,14 @@
+pragma solidity ^0.4.13;
+
+contract Test {
+    event Log(string);
+
+    function target() payable public {
+        if (msg.value > 10)
+            Log("Value greater than 10");
+        else
+            Log("Value less or equal than 10");
+
+    } 
+
+}

examples/evm/two_tx_ovf.sol

@@ -0,0 +1,28 @@
+pragma solidity ^0.4.15;
+
+contract SymExExample {
+    uint did_init = 0;
+
+    event Log(string);
+
+    // function id: 0x13371337
+    function test_me(int input) {
+        if (did_init == 0) {
+            did_init = 1;
+            Log("initialized");
+            return;
+        }
+
+        if (input < 42) {
+            // safe
+            Log("safe");
+            return;
+        } else {
+            // overflow possibly!
+            int could_overflow = input + 1;
+            Log("overflow");
+        }
+
+    }
+}
+

examples/evm/umd_example.sol

@@ -0,0 +1,30 @@
+// Smart contract based on a classic symbolic execution example from slides
+// by Michael Hicks, University of Maryland.
+// https://www.cs.umd.edu/~mwh/se-tutorial/symbolic-exec.pdf
+
+pragma solidity ^0.4.15;
+
+contract SymExExample {
+
+
+    function test_me(int a, int b, int c) public pure {
+        int x = 0;
+        int y = 0;
+        int z = 0;
+
+        if (a != 0) {
+            x = -2;
+        }
+
+        if (b < 5) {
+            if (a == 0 && c != 0) {
+                y = 1;
+            }
+            z = 2;
+        }
+
+        // will fail when: a == 0 && b < 5 && c != 0
+        assert(x + y + z != 3);
+    }
+
+}