add more test contracts

examples/simple_token.rs

@@ -6,13 +6,22 @@ use ser::{
 use z3::ast::*;
 
 pub const SIMPLE_TOKEN: &str = r#"608060405234801561001057600080fd5b50600436106100415760003560e01c806327e235e314610046578063a9059cbb14610078578063f8b2cb4f1461008d575b600080fd5b610066610054366004610143565b60006020819052908152604090205481565b60405190815260200160405180910390f35b61008b610086366004610165565b6100b6565b005b61006661009b366004610143565b6001600160a01b031660009081526020819052604090205490565b336000908152602081905260409020548111156100d257600080fd5b33600090815260208190526040812080548392906100f19084906101a5565b90915550506001600160a01b0382166000908152602081905260408120805483929061011e9084906101be565b90915550505050565b80356001600160a01b038116811461013e57600080fd5b919050565b60006020828403121561015557600080fd5b61015e82610127565b9392505050565b6000806040838503121561017857600080fd5b61018183610127565b946020939093013593505050565b634e487b7160e01b600052601160045260246000fd5b818103818111156101b8576101b861018f565b92915050565b808201808211156101b8576101b861018f56fea264697066735822122041d29a76727a31c9e4ec86703553a675712f98921d6c4bc9b23f274a963de18264736f6c63430008130033"#;
-pub const SIMPLE_TOKEN_2: &str = r#"608060405234801561001057600080fd5b50600436106100365760003560e01c806327e235e31461003b578063a9059cbb1461006d575b600080fd5b61005b610049366004610117565b60006020819052908152604090205481565b60405190815260200160405180910390f35b61008061007b366004610139565b610082565b005b33600090815260208190526040812080548392906100a1908490610179565b909155505033600090815260208190526040812080548392906100c5908490610192565b90915550506001600160a01b038216600090815260208190526040812080548392906100f2908490610179565b90915550505050565b80356001600160a01b038116811461011257600080fd5b919050565b60006020828403121561012957600080fd5b610132826100fb565b9392505050565b6000806040838503121561014c57600080fd5b610155836100fb565b946020939093013593505050565b634e487b7160e01b600052601160045260246000fd5b8082018082111561018c5761018c610163565b92915050565b8181038181111561018c5761018c61016356fea26469706673582212201cf1ad42b1d09ece2257b07f3c87313378c1740e47897aef8282a8bce21f250564736f6c63430008130033"#;
+
+// https://bytegraph.xyz/bytecode/f071451779e262f80002103a167eb2f1/graph
+pub const SIMPLE_TOKEN_2: &str = r#"608060405234801561001057600080fd5b50600436106100365760003560e01c806327e235e31461003b578063a9059cbb1461006d575b600080fd5b61005b61004936600461012f565b60006020819052908152604090205481565b60405190815260200160405180910390f35b61008061007b366004610151565b610082565b005b336000908152602081905260409020548111156100be5733600090815260208190526040812080548392906100b8908490610191565b90915550505b33600090815260208190526040812080548392906100dd9084906101aa565b90915550506001600160a01b0382166000908152602081905260408120805483929061010a908490610191565b90915550505050565b80356001600160a01b038116811461012a57600080fd5b919050565b60006020828403121561014157600080fd5b61014a82610113565b9392505050565b6000806040838503121561016457600080fd5b61016d83610113565b946020939093013593505050565b634e487b7160e01b600052601160045260246000fd5b808201808211156101a4576101a461017b565b92915050565b818103818111156101a4576101a461017b56fea264697066735822122002375043ca1d0851e805e58031cc47e9bb47caa1515071bfced15061a969b36964736f6c63430008130033"#;
+
+// https://bytegraph.xyz/bytecode/b4fa92c48a8c207cd6b014513d614699/graph
+pub const SUPER_SIMPLE_TOKEN: &str = r#"608060405234801561001057600080fd5b50600436106100365760003560e01c806327e235e31461003b578063a9059cbb1461006d575b600080fd5b61005b610049366004610117565b60006020819052908152604090205481565b60405190815260200160405180910390f35b61008061007b366004610139565b610082565b005b33600090815260208190526040812080548392906100a1908490610179565b909155505033600090815260208190526040812080548392906100c5908490610192565b90915550506001600160a01b038216600090815260208190526040812080548392906100f2908490610179565b90915550505050565b80356001600160a01b038116811461011257600080fd5b919050565b60006020828403121561012957600080fd5b610132826100fb565b9392505050565b6000806040838503121561014c57600080fd5b610155836100fb565b946020939093013593505050565b634e487b7160e01b600052601160045260246000fd5b8082018082111561018c5761018c610163565b92915050565b8181038181111561018c5761018c61016356fea26469706673582212200417ff0a30c9d018ec755002b2d0f9276dbaed0859f1680b25a255d393ee763264736f6c63430008130033"#;
+// https://bytegraph.xyz/bytecode/8ef52691295a1b8938ee5bb37aaea8e7
+pub const SIMPLE_TOKEN_GIVER: &str = r#"608060405234801561001057600080fd5b50600436106100365760003560e01c806327e235e31461003b578063f00388f71461006d575b600080fd5b61005b6100493660046100cf565b60006020819052908152604090205481565b60405190815260200160405180910390f35b61008061007b3660046100f1565b610082565b005b6001600160a01b038216600090815260208190526040812080548392906100aa90849061011b565b90915550505050565b80356001600160a01b03811681146100ca57600080fd5b919050565b6000602082840312156100e157600080fd5b6100ea826100b3565b9392505050565b6000806040838503121561010457600080fd5b61010d836100b3565b946020939093013593505050565b8082018082111561013c57634e487b7160e01b600052601160045260246000fd5b9291505056fea26469706673582212204a963d4eb5e44cc3f559c5931426b8d2bbd46a2f6c2bdf9d2723aead9406520364736f6c63430008130033"#;
+
 fn main() {
-    let pgm = Parser::with_pgm(SIMPLE_TOKEN_2).parse();
+    let pgm = Parser::with_pgm(SUPER_SIMPLE_TOKEN).parse();
     let mut evm = Evm::with_pgm(pgm);
 
     let execution = evm.exec();
     {
+       // eprintln!("STATE TREE: {:#?}", execution.states);
         let leaf = execution.states.leaves();
         eprintln!("LEAVES: {:#?}", leaf);
         assert_eq!(14, leaf.len());
@@ -31,4 +40,5 @@ fn main() {
         .filter(|t| *t.last().unwrap().clone() == Instruction::Revert)
         .collect::<Vec<_>>();
     eprintln!("TRACES WITH REVERTS {:#?}", reverted_traces);
+    //assert_eq!(8, reverted_traces.len());
 }

src/parser.rs

@@ -263,7 +263,7 @@ fn push_op(sz: u8, val: &[u8]) -> Instruction {
             let val = zero_extend::<21>(val).into();
             push21(val)
         }
-        21 => {
+        22 => {
             let val = zero_extend::<22>(val).into();
             push22(val)
         }

src/traits.rs

@@ -11,8 +11,21 @@ use crate::stack::Stack;
 use crate::state::context::ExecutionEnv;
 use crate::state::evm::EvmState;
 use crate::storage::{AccountStorage, StorageValue};
+use uuid::Uuid;
 use z3_ext::ast::Bool;
 
+
+pub trait NodeLike {
+    fn parent(&self) -> &Self;
+}
+pub trait Tree {
+    type Node;
+    fn insert_left_of(&mut self, id: Uuid, node: Self::Node) -> Option<Uuid>;
+    fn insert_right_of(&mut self, id: Uuid, node: Self::Node) -> Option<Uuid>;
+    fn leaves(&self) -> Vec<Self::Node>;
+    fn path_to(&self, id: Uuid) -> Vec<Self::Node>;
+    fn all_paths(&self) -> Vec<Vec<Self::Node>>;
+}
 pub trait MachineState<const STACK_ITEM_SZ: usize> {
     type PC;
 

test-contracts/src/SimpleToken2.sol

@@ -0,0 +1,18 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.13;
+
+contract SimpleToken {
+    mapping(address => uint256) public balances;
+
+    constructor() {
+        balances[msg.sender] = 100;
+    }
+
+    function transfer(address recipient, uint256 amt) public {
+        if (balances[msg.sender] < amt) {
+            balances[msg.sender] += amt;
+        }
+        balances[msg.sender] -= amt;
+        balances[recipient] += amt;
+    }
+}

test-contracts/src/SimpleTokenGiver.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.13;
+
+contract SimpleToken {
+    mapping(address => uint256) public balances;
+
+    constructor() {
+        balances[msg.sender] = 100;
+    }
+
+    function give(address recipient, uint256 amt) public {
+        balances[recipient] += amt;
+    }
+
+}

test-contracts/src/SuperSimpleToken.sol

@@ -0,0 +1,16 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.13;
+
+contract SimpleToken {
+    mapping(address => uint256) public balances;
+
+    constructor() {
+        balances[msg.sender] = 100;
+    }
+
+    function transfer(address recipient, uint256 amt) public {
+        balances[msg.sender] += amt;
+        balances[msg.sender] -= amt;
+        balances[recipient] += amt;
+    }
+}