fix memcopy

src/main.rs

@@ -16,7 +16,7 @@ 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, VM, W256};
+use rhoevm::modules::types::{ContractCode, Env, Expr, Prop, RuntimeCodeStruct, EXPR_MEMPTY, VM, W256};
 
 #[derive(Debug)]
 struct Args {
@@ -118,7 +118,7 @@ fn dummy_symvm_from_command(cmd: &SymbolicCommand, calldata: (Expr, Vec<Box<Prop
     (_, _, Some(code)) => {
       let bs = hex_byte_string("bytes", &strip_0x(code));
       let mc = if cmd.create {
-        ContractCode::InitCode(Box::new(bs), Box::new(Expr::Mempty))
+        ContractCode::InitCode(Box::new(bs), Box::new(EXPR_MEMPTY))
       } else {
         ContractCode::RuntimeCode(RuntimeCodeStruct::ConcreteRuntimeCode(Box::new(bs)))
       };

src/modules/cli.rs

@@ -11,7 +11,7 @@ use crate::modules::format::{hex_byte_string, strip_0x};
 use crate::modules::symexec::mk_calldata;
 use crate::modules::transactions::init_tx;
 use crate::modules::types::{
-  Addr, BaseState, Contract, ContractCode, Expr, Gas, Prop, RuntimeCodeStruct, VMOpts, VM, W256,
+  Addr, BaseState, Contract, ContractCode, Expr, Gas, Prop, RuntimeCodeStruct, VMOpts, EXPR_MEMPTY, VM, W256,
 };
 
 type URL = String;
@@ -110,7 +110,7 @@ pub async fn symvm_from_command(cmd: &SymbolicCommand, calldata: (Expr, Vec<Box<
           Some(code) => {
             let bs = hex_byte_string("bytes", &strip_0x(code));
             let mc = if cmd.create {
-              ContractCode::InitCode(Box::new(bs), Box::new(Expr::Mempty))
+              ContractCode::InitCode(Box::new(bs), Box::new(EXPR_MEMPTY))
             } else {
               ContractCode::RuntimeCode(RuntimeCodeStruct::ConcreteRuntimeCode(Box::new(bs)))
             };
@@ -127,7 +127,7 @@ pub async fn symvm_from_command(cmd: &SymbolicCommand, calldata: (Expr, Vec<Box<
     (_, _, Some(code)) => {
       let bs = hex_byte_string("bytes", &strip_0x(code));
       let mc = if cmd.create {
-        ContractCode::InitCode(Box::new(bs), Box::new(Expr::Mempty))
+        ContractCode::InitCode(Box::new(bs), Box::new(EXPR_MEMPTY))
       } else {
         ContractCode::RuntimeCode(RuntimeCodeStruct::ConcreteRuntimeCode(Box::new(bs)))
       };

src/modules/expr.rs

@@ -7,7 +7,8 @@ use crate::modules::cse::BufEnv;
 use crate::modules::rlp::{rlp_addr_full, rlp_list, rlp_word_256};
 use crate::modules::traversals::{fold_expr, map_expr, map_prop, map_prop_prime};
 use crate::modules::types::{
-  keccak, keccak_prime, maybe_lit_byte, pad_right, until_fixpoint, word256_bytes, Addr, Expr, GVar, Prop, W256, W64,
+  keccak, keccak_prime, maybe_lit_byte, pad_right, until_fixpoint, word256_bytes, Addr, Expr, GVar, Prop, EXPR_MEMPTY,
+  W256, W64,
 };
 
 use super::types::{ByteString, Word8};
@@ -871,7 +872,11 @@ pub fn copy_slice(src_offset: &Expr, dst_offset: &Expr, size: &Expr, src: &Expr,
         let sl: Vec<Expr> = ((src_offset.0)..(src_offset.0) + (size.0))
           .map(|i| read_byte(Box::new(Expr::Lit(W256(i as u128, 0))), Box::new(src.clone())))
           .collect();
-        let tl = &dst_buf[dst_offset.0 as usize + size.0 as usize..];
+        let tl = if (dst_offset.0 as usize + size.0 as usize) < dst_buf.len() {
+          &dst_buf[dst_offset.0 as usize + size.0 as usize..]
+        } else {
+          &vec![]
+        };
 
         if sl.iter().all(|arg0: &Expr| is_lit_byte(Box::new(arg0.clone()))) {
           let packed_sl: Vec<u8> = sl.into_iter().filter_map(maybe_lit_byte).collect();
@@ -1012,15 +1017,11 @@ fn conc_keccak_one_pass(expr: Box<Expr>) -> Expr {
 
 // Main simplify function
 pub fn simplify(expr: Box<Expr>) -> Expr {
-  if *expr != Expr::Mempty {
-    let simplified = map_expr(|arg0: &Expr| go_expr(arg0), *expr.clone());
-    if simplified == *expr {
-      simplified
-    } else {
-      simplify(Box::new(map_expr(|arg0: &Expr| go_expr(arg0), structure_array_slots(Box::new(*expr.clone())))))
-    }
+  let simplified = map_expr(|arg0: &Expr| go_expr(arg0), *expr.clone());
+  if simplified == *expr {
+    simplified
   } else {
-    Expr::Mempty
+    simplify(Box::new(map_expr(|arg0: &Expr| go_expr(arg0), structure_array_slots(Box::new(*expr.clone())))))
   }
 }
 
@@ -1872,7 +1873,7 @@ pub fn drop(n: W256, buf: &Expr) -> Expr {
 }
 
 pub fn slice(offset: Box<Expr>, size: Box<Expr>, src: Box<Expr>) -> Expr {
-  copy_slice(&offset, &(Expr::Lit(W256(0, 0))), &size, &src, &(Expr::Mempty))
+  copy_slice(&offset, &(Expr::Lit(W256(0, 0))), &size, &src, &(EXPR_MEMPTY))
 }
 
 pub fn buf_length(buf: &Expr) -> Expr {
@@ -1905,7 +1906,6 @@ pub fn buf_length_env(env: &HashMap<usize, Expr>, use_env: bool, buf: Expr) -> E
           emax(Box::new(l), Box::new(Expr::BufLength(Box::new(Expr::GVar(GVar::BufVar(a))))))
         }
       }
-      Expr::Mempty => l,
       _ => panic!("unsupported expression: {}", buf),
     }
   }

src/modules/smt.rs

@@ -1,3 +1,4 @@
+use log::info;
 use regex::Regex;
 use std::collections::{HashMap, HashSet};
 use std::{fmt, vec};
@@ -12,7 +13,7 @@ use crate::modules::expr::{
 use crate::modules::format::format_prop;
 use crate::modules::keccak::{keccak_assumptions, keccak_compute};
 use crate::modules::traversals::{fold_prop, TraversableTerm};
-use crate::modules::types::{AddableVec, Addr, Expr, GVar, Prop, W256W256Map, W256};
+use crate::modules::types::{AddableVec, Addr, Expr, GVar, Prop, W256W256Map, EXPR_MEMPTY, W256};
 
 // Type aliases for convenience
 type Text = String;
@@ -1103,7 +1104,7 @@ fn expr_to_smt(expr: Expr) -> String {
     },
     Expr::ReadByte(idx, src) => op2("select", *src, *idx),
     Expr::ConcreteBuf(bs) if bs.len() == 0 => "((as const Buf) #b00000000)".to_string(),
-    Expr::ConcreteBuf(bs) => write_bytes(&bs, Expr::Mempty),
+    Expr::ConcreteBuf(bs) => write_bytes(&bs, EXPR_MEMPTY),
     Expr::AbstractBuf(s) => s,
     Expr::ReadWord(idx, prev) => op2("readWord", *idx, *prev),
 
@@ -1243,7 +1244,7 @@ fn expand_exp(base: Expr, expnt: W256) -> Builder {
 
 // Concatenates a list of bytes into a larger bitvector
 fn write_bytes(bytes: &[u8], buf: Expr) -> Builder {
-  let skip_zeros = buf == Expr::Mempty;
+  let skip_zeros = buf == EXPR_MEMPTY;
   let mut idx = 0;
   let mut inner = expr_to_smt(buf);
   for &byte in bytes {

src/modules/traversals.rs

@@ -355,11 +355,7 @@ pub fn fold_expr<B>(f: &mut dyn FnMut(&Expr) -> B, acc: B, expr: &Expr) -> B
 where
   B: Add<B, Output = B> + Default + Clone,
 {
-  if *expr == Expr::Mempty {
-    acc.clone()
-  } else {
-    acc.clone() + go_expr(f, acc.clone(), expr.clone())
-  }
+  acc.clone() + go_expr(f, acc.clone(), expr.clone())
 }
 
 /// A trait for types that can map a function over their `Expr` components.
@@ -777,7 +773,6 @@ impl ExprMappable for Expr {
         let a = a.map_expr_m(f);
         f(&Expr::BufLength(Box::new(a)))
       }
-      Expr::Mempty => Expr::Mempty,
       _ => panic!("unuexpected expr {}", self),
     }
   }
@@ -798,11 +793,7 @@ pub fn map_expr<F>(mut f: F, expr: Expr) -> Expr
 where
   F: FnMut(&Expr) -> Expr,
 {
-  if expr == Expr::Mempty {
-    expr
-  } else {
-    expr.map_expr_m(&mut f)
-  }
+  expr.map_expr_m(&mut f)
 }
 
 /// Recursively applies a given function `f` to each `Expr` within a `Prop`.

src/modules/types.rs

@@ -402,7 +402,6 @@ impl fmt::Display for GVar {
 
 #[derive(Debug, Clone)]
 pub enum Expr {
-  Mempty,
   // Identifiers
   Lit(W256),
   Var(String),
@@ -515,7 +514,6 @@ pub enum Expr {
 impl fmt::Display for Expr {
   fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
     match self {
-      Expr::Mempty => write!(f, "Mempty"),
       Expr::Lit(val) => write!(f, "Lit(0x{})", val.to_hex()),
       Expr::Var(name) => write!(f, "Var({})", name),
       Expr::GVar(gvar) => write!(f, "GVar({})", gvar),
@@ -601,14 +599,15 @@ impl fmt::Display for Expr {
   }
 }
 
+pub const EXPR_MEMPTY: Expr = Expr::ConcreteBuf(vec![]);
+
 impl Eq for Expr {}
 
 impl PartialEq for Expr {
   fn eq(&self, other: &Self) -> bool {
     use Expr::*;
 
     match (self, other) {
-      (Mempty, Mempty) => true,
       (Lit(val1), Lit(val2)) => val1 == val2,
       (Var(name1), Var(name2)) => name1 == name2,
       (GVar(gvar1), GVar(gvar2)) => gvar1 == gvar2,
@@ -710,9 +709,6 @@ impl Hash for Expr {
     use Expr::*;
 
     match self {
-      Mempty => {
-        "Mempty".hash(state);
-      }
       Lit(val) => {
         "Lit".hash(state);
         val.hash(state);
@@ -1167,7 +1163,7 @@ pub fn update_balance(c: Contract, new_balance: Expr) -> Contract {
 impl Contract {
   pub fn bytecode(&self) -> Option<Expr> {
     match &self.code {
-      ContractCode::InitCode(_, _) => Some(Expr::Mempty), // Equivalent to Just mempty
+      ContractCode::InitCode(_, _) => Some(EXPR_MEMPTY), // Equivalent to Just mempty
       ContractCode::RuntimeCode(RuntimeCodeStruct::ConcreteRuntimeCode(bs)) => Some(Expr::ConcreteBuf(*bs.clone())),
       ContractCode::RuntimeCode(RuntimeCodeStruct::SymbolicRuntimeCode(ops)) => Some(from_list(ops.to_vec())),
       ContractCode::UnKnownCode(_) => None,
@@ -1587,7 +1583,7 @@ where
 // Implement the Default trait for AddableVec
 impl Default for Expr {
   fn default() -> Expr {
-    Expr::Mempty // Return an empty vector
+    EXPR_MEMPTY // Return an empty vector
   }
 }
 

tests/evm_test.rs

@@ -6,7 +6,7 @@ use rhoevm::modules::format::{hex_byte_string, strip_0x};
 
 //use rhoevm::modules::solvers::{with_solvers, Solver};
 use rhoevm::modules::transactions::init_tx;
-use rhoevm::modules::types::{ContractCode, Expr, Memory, Prop, RuntimeCodeStruct, VM, W256};
+use rhoevm::modules::types::{ContractCode, Expr, Memory, Prop, RuntimeCodeStruct, EXPR_MEMPTY, VM, W256};
 
 const MAX_NUM_ITERATIONS: u32 = 1;
 
@@ -22,7 +22,7 @@ fn dummy_symvm_from_command(cmd: &SymbolicCommand, calldata: (Expr, Vec<Box<Prop
     (_, _, Some(code)) => {
       let bs = hex_byte_string("bytes", &strip_0x(code));
       let mc = if cmd.create {
-        ContractCode::InitCode(Box::new(bs), Box::new(Expr::Mempty))
+        ContractCode::InitCode(Box::new(bs), Box::new(EXPR_MEMPTY))
       } else {
         ContractCode::RuntimeCode(RuntimeCodeStruct::ConcreteRuntimeCode(Box::new(bs)))
       };