Ignore Overflow

README.md

@@ -87,9 +87,7 @@ pragma solidity ^0.8.0;
 
 contract SimpleContract {
     function check(uint32 x, uint32 y) public pure {
-        if (x > 0 && x < 100 && y > 0 && y < 100) {
-            assert(x + y != 142);
-        }
+        assert(x + y != 142);
     }
 }
 ```

example/ERC721A.t.sol

@@ -82,34 +82,37 @@ contract ERC721ATest is ERC721A {
     }
 
     function testMintRequirements(address to, uint quantity) public {
-        mint(to, quantity);
-
-        assert(to != address(0));
-        assert(quantity > 0);
+        if (to != address(0) && quantity > 0) {
+            mint(to, quantity);
+        }
     }
 
     function testMintNextTokenIdUpdate(address to, uint quantity) public {
-        uint oldNextTokenId = _nextTokenId();
-        require(oldNextTokenId <= type(uint96).max); // practical assumption needed for overflow/underflow not occurring
+        if (to != address(0) && quantity > 0) {
+            uint oldNextTokenId = _nextTokenId();
+            require(oldNextTokenId <= type(uint96).max); // practical assumption needed for overflow/underflow not occurring
 
-        mint(to, quantity);
+            mint(to, quantity);
 
-        uint newNextTokenId = _nextTokenId();
+            uint newNextTokenId = _nextTokenId();
 
-        assert(newNextTokenId >= oldNextTokenId); // ensuring no overflow
-        assert(newNextTokenId == oldNextTokenId + quantity);
+            assert(newNextTokenId >= oldNextTokenId); // ensuring no overflow
+            assert(newNextTokenId == oldNextTokenId + quantity);
+        }
     }
 
     function testMintBalanceUpdate(address to, uint quantity) public {
-        uint oldBalanceTo = balanceOf(to);
-        require(oldBalanceTo <= type(uint64).max / 2); // practical assumption needed for balance staying within uint64
+        if (to != address(0) && quantity > 0) {
+            uint oldBalanceTo = balanceOf(to);
+            require(oldBalanceTo <= type(uint64).max / 2); // practical assumption needed for balance staying within uint64
 
-        mint(to, quantity);
+            mint(to, quantity);
 
-        uint newBalanceTo = balanceOf(to);
+            uint newBalanceTo = balanceOf(to);
 
-        assert(newBalanceTo >= oldBalanceTo); // ensuring no overflow
-        assert(newBalanceTo == oldBalanceTo + quantity);
+            assert(newBalanceTo >= oldBalanceTo); // ensuring no overflow
+            assert(newBalanceTo == oldBalanceTo + quantity);
+        }
     }
 
     function testMintOwnershipUpdate(address to, uint quantity, uint _newNextTokenId) public {

example/build/SimpleContract.bin

@@ -1 +1 @@
-608060405234801561000f575f80fd5b506101f58061001d5f395ff3fe608060405234801561000f575f80fd5b5060043610610029575f3560e01c8063c5eb648f1461002d575b5f80fd5b610047600480360381019061004291906100f0565b610049565b005b5f8263ffffffff16118015610064575060648263ffffffff16105b801561007557505f8163ffffffff16115b8015610087575060648163ffffffff16105b156100af57608e818361009a919061015b565b63ffffffff16036100ae576100ad610192565b5b5b5050565b5f80fd5b5f63ffffffff82169050919050565b6100cf816100b7565b81146100d9575f80fd5b50565b5f813590506100ea816100c6565b92915050565b5f8060408385031215610106576101056100b3565b5b5f610113858286016100dc565b9250506020610124858286016100dc565b9150509250929050565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b5f610165826100b7565b9150610170836100b7565b9250828201905063ffffffff81111561018c5761018b61012e565b5b92915050565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52600160045260245ffdfea2646970667358221220a39c51491088ffef55d73d836a5e82f6f2ddd811d09d15817259da0ab8114d9264736f6c63430008180033
+6080604052348015600e575f80fd5b506101b18061001c5f395ff3fe608060405234801561000f575f80fd5b5060043610610029575f3560e01c8063c5eb648f1461002d575b5f80fd5b610047600480360381019061004291906100ac565b610049565b005b608e81836100579190610117565b63ffffffff160361006b5761006a61014e565b5b5050565b5f80fd5b5f63ffffffff82169050919050565b61008b81610073565b8114610095575f80fd5b50565b5f813590506100a681610082565b92915050565b5f80604083850312156100c2576100c161006f565b5b5f6100cf85828601610098565b92505060206100e085828601610098565b9150509250929050565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52601160045260245ffd5b5f61012182610073565b915061012c83610073565b9250828201905063ffffffff811115610148576101476100ea565b5b92915050565b7f4e487b71000000000000000000000000000000000000000000000000000000005f52600160045260245ffdfea2646970667358221220b1927f8ca246d643c2c1b152b3f5e93b02491ed08c60d3fe057dea580cc74ea264736f6c63430008190033

example/simple.sol

@@ -3,8 +3,8 @@ pragma solidity ^0.8.0;
 
 contract SimpleContract {
     function check(uint32 x, uint32 y) public pure {
-        if (x > 0 && x < 100 && y > 0 && y < 100) {
-            assert(x + y != 142);
-        }
+        //if (x > 0 && x < 100 && y > 0 && y < 100) {
+        assert(x + y != 142);
+        //}
     }
 }

src/main.rs

@@ -1,29 +1,36 @@
 use env_logger;
 use getopts::Options;
 use log::{debug, error, info, warn};
-use std::collections::HashMap;
+use std::collections::{HashMap, HashSet};
 use std::error::Error;
 use std::fs::File;
 use std::io::Read;
 use std::time;
 use std::{env, process};
 use tokio::task;
 
-use rhoevm::modules::abi::{AbiType, Sig};
+use rhoevm::modules::abi::{selector, AbiType, Sig};
 use rhoevm::modules::cli::{build_calldata, vm0, SymbolicCommand};
 use rhoevm::modules::evm::{abstract_contract, opslen, solve_constraints};
 use rhoevm::modules::expr::is_function_sig_check_prop;
 use rhoevm::modules::format::{hex_byte_string, strip_0x};
 use rhoevm::modules::smt::parse_z3_output;
 use rhoevm::modules::transactions::init_tx;
-use rhoevm::modules::types::{ContractCode, Env, Expr, Prop, RuntimeCodeStruct, EXPR_MEMPTY, VM, W256};
+use rhoevm::modules::types::{
+  ByteString, ContractCode, Env, EvmError, Expr, Prop, RuntimeCodeStruct, VMResult, EXPR_MEMPTY, VM, W256,
+};
+
+const DEFAULT_MAX_NUM_ITERATIONS: u32 = 10;
+const DEFAULT_IGNORED_REVERT_LISTS: [u8; 1] = [0x11];
+const DEFAULT_REVERT_STATEMENT: &str = "Panic(uint256)";
 
 #[derive(Debug)]
 struct Args {
   bin_file_path: String,
   function_signatures: String,
   max_num_iterations: Option<u32>,
   verbose_level: Option<String>,
+  ignored_panic_codes: HashSet<u8>,
   execute_entire_binary: bool,
   stop_at_the_first_reachable_revert: bool,
 }
@@ -34,15 +41,14 @@ fn print_usage(program: &str, opts: &Options) {
   process::exit(0);
 }
 
-const DEFAULT_MAX_NUM_ITERATIONS: u32 = 10;
-
 fn parse_args() -> Args {
   let args: Vec<String> = env::args().collect();
   let program = args[0].clone();
 
   let mut opts = Options::new();
   opts.optopt("i", "max_num_iterations", "Maximum number of iterations for loop", "MAX_NUM_ITER");
   opts.optopt("v", "verbose", "Level of verbose", "LEVEL");
+  opts.optopt("p", "ignored_panic_codes", "List of ignored panic codes", "IGNORED_PANIC_CODES");
   opts.optflag(
     "e",
     "execute_entire_binary",
@@ -83,7 +89,13 @@ fn parse_args() -> Args {
   } else {
     None
   };
+
   let verbose_level = matches.opt_str("v");
+  let ignored_panic_codes: HashSet<u8> = if let Some(s) = matches.opt_str("p") {
+    s.split('|').map(|s| s.parse::<u8>().unwrap()).collect()
+  } else {
+    HashSet::from_iter(DEFAULT_IGNORED_REVERT_LISTS.to_vec().iter().cloned())
+  };
 
   let execute_entire_binary = matches.opt_present("e");
   let stop_at_the_first_reachable_revert = matches.opt_present("s");
@@ -93,6 +105,7 @@ fn parse_args() -> Args {
     function_signatures,
     max_num_iterations,
     verbose_level,
+    ignored_panic_codes,
     execute_entire_binary,
     stop_at_the_first_reachable_revert,
   }
@@ -181,6 +194,8 @@ async fn main() {
   }
   debug!("File '{}' read successfully.", args.bin_file_path);
 
+  let panic_bytes: ByteString = selector(DEFAULT_REVERT_STATEMENT);
+
   // utility variables
   let mut normalized_function_names_vec: Vec<String> = vec![];
   let mut function_names_vec: Vec<String> = vec![];
@@ -339,7 +354,29 @@ async fn main() {
           }
 
           if found_calldataload && prev_op == "REVERT" {
-            potential_reverts.push((vm.state.pc, vm.constraints.clone()));
+            let mut ignore: bool = false;
+            if vm.result.clone().is_some() {
+              if let VMResult::VMFailure(e) = vm.result.clone().unwrap() {
+                if let EvmError::Revert(r) = e {
+                  if let Expr::ConcreteBuf(b) = *r {
+                    if panic_bytes.len() < b.len() {
+                      for i in 1..panic_bytes.len() {
+                        if panic_bytes[i] != b[i] {
+                          ignore = true;
+                          break;
+                        }
+                      }
+                      if !ignore {
+                        ignore = args.ignored_panic_codes.contains(&b[b.len() - 1]);
+                      }
+                    }
+                  }
+                }
+              }
+            }
+            if !ignore {
+              potential_reverts.push((vm.state.pc, vm.constraints.clone()));
+            }
             end = true;
           }
 

src/modules/expr.rs

@@ -820,7 +820,7 @@ pub fn copy_slice(src_offset: &Expr, dst_offset: &Expr, size: &Expr, src: &Expr,
         let hd = vec![0; dst_offset.0 as usize];
         let sl = pad_right(
           size.0 as usize,
-          (&src_buf[src_offset.0 as usize..src_offset.0 as usize + size.0 as usize]).to_vec(),
+          (&src_buf[src_offset.0 as usize..min(src_buf.len(), src_offset.0 as usize + size.0 as usize)]).to_vec(),
         );
         return Expr::ConcreteBuf([hd, sl].concat());
       } else {