diff --git a/src/encoder.rs b/src/encoder.rs index 2d7eeec..2c8d20a 100644 --- a/src/encoder.rs +++ b/src/encoder.rs @@ -1,7 +1,8 @@ -use crate::evm_context; +use crate::evaluator::Evaluator; use crate::execution_position::ExecutionPositionManager; -use crate::smt::{self, SMTExpr, SMTFormat, SMTSort, SMTStatement, SMTVariable}; +use crate::smt::{SMTExpr, SMTFormat, SMTSort, SMTStatement, SMTVariable}; use crate::ssa_tracker::SSATracker; +use crate::{evm_context, smt}; use num_traits::Num; use yultsur::dialect::{Builtin, Dialect}; @@ -29,6 +30,7 @@ pub struct Encoder { ssa_tracker: SSATracker, output: Vec, interpreter: InstructionsType, + evaluator: Evaluator, loop_unroll: u64, path_conditions: Vec, execution_position: ExecutionPositionManager, @@ -57,6 +59,31 @@ pub fn encode_revert_reachable( encode_with_counterexamples(&mut encoder, counterexamples) } +pub fn encode_with_evaluator( + ast: &Block, + loop_unroll: u64, + evaluator: Evaluator, + ssa_tracker: SSATracker, +) -> (String, Evaluator, SSATracker) { + let mut encoder = Encoder:: { + evaluator, + ssa_tracker, + ..Default::default() + }; + encoder.encode(ast, loop_unroll); + let query = encoder + .output + .iter() + .map(|s| s.as_smt()) + .collect::>() + .join("\n"); + ( + query, + std::mem::take(&mut encoder.evaluator), + std::mem::take(&mut encoder.ssa_tracker), + ) +} + pub fn encode_solc_panic_reachable( ast: &Block, loop_unroll: u64, @@ -139,8 +166,13 @@ impl Encoder { assert_eq!(function.parameters.len(), arguments.len()); for (param, arg) in function.parameters.iter().zip(arguments) { let var = self.ssa_tracker.introduce_variable(param); - self.out(smt::define_const(var, smt::SMTExpr::from(arg.clone()))) + self.out(smt::define_const( + var.clone(), + smt::SMTExpr::from(arg.clone()), + )); + self.evaluator.define_from_variable(&var, arg); } + self.encode_variable_declaration(&VariableDeclaration { variables: function.returns.clone(), value: None, @@ -200,7 +232,14 @@ impl Encoder { fn encode_if(&mut self, expr: &yul::If) { let cond = self.encode_expression(&expr.condition); assert!(cond.len() == 1); + if self + .evaluator + .variable_known_equal(&cond[0], &"0".to_string()) + { + return; + } let prev_ssa = self.ssa_tracker.copy_current_ssa(); + let prev_eval = self.evaluator.copy_state(); self.push_path_condition(smt::neq(cond[0].clone(), 0)); self.encode_block(&expr.body); @@ -209,6 +248,7 @@ impl Encoder { let output = self .ssa_tracker .join_branches(smt::eq(cond[0].clone(), 0), prev_ssa); + self.evaluator.join_with_old_state(prev_eval); self.out_vec(output); } @@ -221,6 +261,8 @@ impl Encoder { let cond = self.encode_expression(&for_loop.condition); assert!(cond.len() == 1); let prev_ssa = self.ssa_tracker.copy_current_ssa(); + let prev_eval = self.evaluator.copy_state(); + // TODO the evaluator does not have path conditions - is that OK? self.push_path_condition(smt::neq(cond[0].clone(), 0)); self.encode_block(&for_loop.body); @@ -230,6 +272,7 @@ impl Encoder { let output = self .ssa_tracker .join_branches(smt::eq(cond[0].clone(), 0), prev_ssa); + self.evaluator.join_with_old_state(prev_eval); self.out_vec(output); } } @@ -239,6 +282,7 @@ impl Encoder { assert!(discriminator.len() == 1); let pre_switch_ssa = self.ssa_tracker.copy_current_ssa(); let mut post_switch_ssa = self.ssa_tracker.take_current_ssa(); + let prev_eval = self.evaluator.copy_state(); for Case { literal, @@ -247,6 +291,15 @@ impl Encoder { } in &switch.cases { let is_default = literal.is_none(); + // TODO this will always run the default case. + // We should first go through all case labels and see if we only need to execute a single one. + if !is_default + && self + .evaluator + .variable_known_unequal(&discriminator[0], &literal.as_ref().unwrap().literal) + { + continue; + } self.ssa_tracker.set_current_ssa(pre_switch_ssa.clone()); @@ -259,7 +312,8 @@ impl Encoder { .map(|case| { smt::eq( discriminator[0].clone(), - self.encode_literal_value(case.literal.as_ref().unwrap()), + self.encode_literal_value(case.literal.as_ref().unwrap()) + .unwrap(), ) }) .collect::>(), @@ -267,7 +321,8 @@ impl Encoder { } else { smt::neq( discriminator[0].clone(), - self.encode_literal_value(literal.as_ref().unwrap()), + self.encode_literal_value(literal.as_ref().unwrap()) + .unwrap(), ) }; @@ -279,9 +334,13 @@ impl Encoder { .ssa_tracker .join_branches(skip_condition, post_switch_ssa); self.out_vec(output); + // TODO check if this is correct. + self.evaluator.join_with_old_state(prev_eval.clone()); post_switch_ssa = self.ssa_tracker.take_current_ssa(); post_switch_ssa.retain(|key, _| pre_switch_ssa.contains_key(key)); } + // TODO we should actually reset thet state of the evaluator, because + // we do not know in which branch we ended up self.ssa_tracker.set_current_ssa(post_switch_ssa); } @@ -297,10 +356,12 @@ impl Encoder { fn encode_literal(&mut self, literal: &Literal) -> SMTVariable { let sort = SMTSort::BV(256); let var = self.new_temporary_variable(sort); - self.out(smt::define_const( - var.clone(), - self.encode_literal_value(literal), - )); + self.evaluator.define_from_literal(&var, literal); + if let Some(value) = self.encode_literal_value(literal) { + self.out(smt::define_const(var.clone(), value)); + } else { + self.out(smt::declare_const(var.clone())) + } var } @@ -309,7 +370,7 @@ impl Encoder { } fn encode_function_call(&mut self, call: &FunctionCall) -> Vec { - let arguments = call + let arguments: Vec = call .arguments .iter() .rev() @@ -344,6 +405,15 @@ impl Encoder { .map(|_i| self.new_temporary_variable(SMTSort::BV(256))) .collect(); + // TODO call evaluator first or interpreter first? + self.evaluator + .builtin_call(builtin, &arguments, &return_vars); + if builtin.name == "call" { + // if let Some((ast, calldata)) = self.evaluator.is_call_to_knon_contract(arguments) { + + // // TODO + // } + } let result = self.interpreter.encode_builtin_call( builtin, arguments, @@ -394,17 +464,26 @@ impl Encoder { for (v, val) in variables.iter().zip(values.into_iter()) { let var = self.ssa_tracker.allocate_new_ssa_index(v); + self.evaluator.define_from_variable(&var, &val); self.out(smt::define_const(var, val.into())); } } - fn encode_literal_value(&self, literal: &Literal) -> SMTExpr { - let parsed = if literal.literal.starts_with("0x") { - num_bigint::BigUint::from_str_radix(&literal.literal[2..], 16).unwrap() + /// Returns the literal value encoded as an SMT expression. + /// Might fail if the literal is a data object reference or something else that + /// does not have a specific 256 bit value. + fn encode_literal_value(&self, literal: &Literal) -> Option { + (if let Some(hex) = literal.literal.strip_prefix("0x") { + Some(num_bigint::BigUint::from_str_radix(hex, 16).unwrap()) + } else if let Some(string) = literal.literal.strip_prefix('\"') { + assert!(string.len() >= 2 && string.ends_with('\"')); + // This is usually only used for references to data objects, + // so we do not encode it. + None } else { - literal.literal.parse::().unwrap() - }; - smt::literal_32_bytes(parsed) + Some(literal.literal.parse::().unwrap()) + }) + .map(smt::literal_32_bytes) } fn push_path_condition(&mut self, cond: SMTExpr) { diff --git a/src/evaluator/engine.rs b/src/evaluator/engine.rs new file mode 100644 index 0000000..bb028a2 --- /dev/null +++ b/src/evaluator/engine.rs @@ -0,0 +1,436 @@ +use std::collections::HashMap; + +use num_bigint::BigUint; +use num_traits::{Num, ToPrimitive}; +use yultsur::{dialect::Builtin, yul::Literal}; + +use crate::smt::SMTVariable; + +use super::simplifier::simplify; +use super::Value; + +#[derive(Default)] +pub struct Evaluator { + calldata: Option>, + ssa_values: HashMap, + storage: HashMap, + memory: HashMap, + memory_slices: HashMap, + unknown_memory_is_zero: bool, + stopped: bool, +} + +#[derive(Clone)] +pub struct EvaluatorState { + storage: HashMap, + memory: HashMap, + memory_slices: HashMap, + unknown_memory_is_zero: bool, + stopped: bool, +} + +#[derive(PartialEq, Clone)] +struct ValueByte { + data: Value, + /// Byte of the data, 0 is most significant byte. + byte: u32, +} + +// TODO +// As soon as we handle side-effecty things, we might have to include +// "executing regularly": +// sstore(0, 1) +// stop() +// sload(0) +// +// Also, storage needs to take branches into account. +// if x { sstore(0, 1) } +// let t := sload(0) +// +// If storage is not changed in a branch, its ssa variable is not updated. +// If all storage writes are to compile-time constant variables, +// then the Evaluator can deal with the branch joins. +// Which means we have to have a mechanism to craete a snapshot of the state (like the SSATracker does) +// and then combine snapshots. +// +// Because of packed storage, the values we store should ideally be byte-wise. +// For now, the following could be OK: +// It's one of the following: +// - unknown +// - a symbolic value in the lower 20 bytes (the rest of the bytes are unknown) +// - a concrete value + +impl Evaluator { + /// Reset all data whose lifetime is tied to a transaction. + /// Keeps storage but resets memory. + /// TODO: Change this interface to "push new call" or something. + /// TODO should also set the current address. + pub fn new_transaction(&mut self, calldata: Vec) { + self.calldata = Some(calldata); + self.memory.clear(); + self.memory_slices.clear(); + self.unknown_memory_is_zero = true; + self.stopped = false; + } + + /// Returns a copy of the state that can later be joined with. + pub fn copy_state(&self) -> EvaluatorState { + EvaluatorState { + storage: self.storage.clone(), + memory: self.memory.clone(), + memory_slices: self.memory_slices.clone(), + unknown_memory_is_zero: self.unknown_memory_is_zero, + stopped: self.stopped, + } + } + /// Joins the state with the given old state. + pub fn join_with_old_state(&mut self, old: EvaluatorState) { + println!( + "===> Join: old st: {}, new st: {}", + self.storage + .get(&BigUint::from(0u32)) + .unwrap_or(&Value::Var("???".to_string())), + old.storage + .get(&BigUint::from(0u32)) + .unwrap_or(&Value::Var("???".to_string())), + ); + if self.stopped { + self.storage = old.storage; + self.memory = old.memory; + self.memory_slices = old.memory_slices; + self.unknown_memory_is_zero = old.unknown_memory_is_zero; + self.stopped = old.stopped; + } else { + assert!(!old.stopped); + self.storage.retain(|k, v| old.storage.get(k) == Some(v)); + self.memory.retain(|k, v| old.memory.get(k) == Some(v)); + self.memory_slices + .retain(|k, v| old.memory_slices.get(k) == Some(v)); + if self.unknown_memory_is_zero { + assert!(old.unknown_memory_is_zero); + } + } + } + /// Returns true if the evaluator can determine that the variable is equal + /// to the given literal value with the previously set restrictions. + pub fn variable_known_equal(&self, var: &SMTVariable, value: &String) -> bool { + println!("Asking if for equal {value}: "); + if let Some(v) = self.ssa_values.get(&var.name) { + println!(" - {v}"); + } + if let Some(Value::Concrete(v)) = self.ssa_values.get(&var.name) { + if let Some(lit) = literal_value(value) { + return *v == lit; + } + } + false + } + pub fn variable_known_unequal(&self, var: &SMTVariable, value: &str) -> bool { + if let Some(Value::Concrete(v)) = self.ssa_values.get(&var.name) { + if let Some(lit) = literal_value(value) { + return *v != lit; + } + } + false + } + + pub fn define_from_literal(&mut self, var: &SMTVariable, literal: &Literal) { + let value = &literal.literal; + //println!("{} := {literal}", var.name); + self.ssa_values.insert( + var.name.clone(), + if let Some(hex) = value.strip_prefix("0x") { + Value::Concrete(BigUint::from_str_radix(hex, 16).unwrap()) + } else if let Some(string) = value.strip_prefix('\"') { + assert!(string.len() >= 2 && string.ends_with('\"')); + // We assume all strings are references to sub-objects, + // which is not true but will not harm correctness. + Value::DataRef(string[1..string.len() - 1].to_string()) + } else { + Value::Concrete(BigUint::from_str_radix(value, 10).unwrap()) + }, + ); + } + pub fn define_from_variable(&mut self, var: &SMTVariable, value: &SMTVariable) { + //println!("{} := {}", var.name, value.name); + if let Some(value) = self.ssa_values.get(&value.name).cloned() { + self.ssa_values.insert(var.name.clone(), value); + } + } + pub fn builtin_call( + &mut self, + builtin: &Builtin, + arguments: &[SMTVariable], + return_vars: &[SMTVariable], + ) { + let arg_values = arguments + .iter() + .map(|arg| { + if let Some(val) = self.ssa_values.get(&arg.name) { + val.clone() + } else { + Value::Var(arg.name.clone()) + } + }) + .collect::>(); + let result = match (builtin.name, &arg_values[..]) { + ( + "add" | "sub" | "mul" | "div" | "shl" | "shr" | "and" | "or" | "datasize" | "dataoffset" | "not" | "iszero" | "lt" | "gt" | "slt" | "sgt" | "eq" | "callvalue", + _ + // TODO fewer clones + ) => Some(Value::Op(builtin.name, arg_values.to_vec())), + ("datacopy", [Value::Concrete(addr), Value::Op("dataoffset", offset), Value::Op("datasize", size)]) => { + assert_eq!(offset, size); + if let Value::DataRef(offset) = &offset[0] { + self.memory_slices.insert(addr.clone(), Value::DataRef(offset.clone())); + } + self.unknown_memory_write_above(addr); + None + } + ("calldatasize", []) => { + self.calldata.as_ref().map(|cd| Value::Concrete(BigUint::from(cd.len()))) + } + ("calldataload", [Value::Concrete(addr)]) => { + self.calldata.as_ref().map(|cd| { + let result = (0..32).map(|i| { + cd.get(addr.to_usize().unwrap() + i).copied().unwrap_or_default() + }).collect::>(); + Value::Concrete(BigUint::from_bytes_be(&result)) + }) + } + ("create", [_ether_value, Value::Concrete(offset), _size /* TODO check size */]) => { + if let Some(Value::DataRef(name)) = self.memory_slices.get(offset) { + Some(Value::KnownContractAddress(name.clone(), 0)) // TODO increment coutner + } else { + None + } + } + // TODO shoudl be part of simplify + ("memoryguard", [value]) => Some(value.clone()), + // TODO unknown mstore? + ("mstore", [Value::Concrete(addr), value]) => { + //println!("mstore({}, {})", addr, value); + self.write_memory(addr.clone(), Some(value.clone())); + None + } + ("mstore", ..) => { + println!("Unknown memory write!"); + self.unknown_memory_write(); + None + } + ("mload", [Value::Concrete(addr)]) => { + //println!("mload({})", addr); + self.read_memory(addr) + } + ("returndatacopy", ..) => { + println!("Unknown memory write!"); + // TODO: Problem: If we have an unknown memory write and join this with another + // branch, we also do need to clear that memory! + self.unknown_memory_write(); + None + } + ("sstore", [Value::Concrete(addr), value]) => { + println!("sstore({addr}, {value})"); + println!( + "===> {}", + self.storage + .get(&BigUint::from(0u32)) + .unwrap_or(&Value::Var("???".to_string())), + ); + self.storage.insert(addr.clone(), value.clone()); + println!( + "===> {}", + self.storage + .get(&BigUint::from(0u32)) + .unwrap_or(&Value::Var("???".to_string())), + ); + None + } + ("sload", [Value::Concrete(addr)]) => { + println!("sload({addr})"); + println!( + "===> {}", + self.storage + .get(&BigUint::from(0u32)) + .unwrap_or(&Value::Var("???".to_string())), + ); + self.storage.get(addr).cloned() + } + ("revert", ..) => { + self.stopped = true; + println!("Reverted!"); + None + } + ("return" | "stop", ..) => { + self.stopped = true; + println!("Returned!"); + None + } + (op, ..) => { + println!("Unhandled opcode: {op}"); + None + } + }; + if let Some(result) = result.map(simplify) { + self.ssa_values.insert(return_vars[0].name.clone(), result); + } + if builtin.name == "call" { + // for i in 0x80..0xc4 { + // println!( + // "{:x}: {:x?}", + // i, + // self.read_memory_byte(&BigUint::from(i as u32)) + // ); + // } + // if let (Some(Value::Concrete(in_offset)), Some(Value::Concrete(in_len))) = (&arg_values[3], &arg_values[4]) { + // println!("{:x?}", &self.get_memory_slice(in_offset.clone(), in_len.clone()).unwrap()); + + // } + } + match builtin.name { + "create" | "sstore" | "sload" | "call" | "datacopy" | "mstore" => { + println!( + "{}{}({})", + if return_vars.is_empty() { + String::new() + } else { + format!( + "{} := ", + return_vars + .iter() + .map(|v| v.name.to_owned()) + .collect::>() + .join(", ") + ) + }, + builtin.name, + arguments + .iter() + .map(|a| { + if let Some(v) = self.ssa_values.get(&a.name) { + format!("{v}") + } else { + format!("${}", a.name) + } + }) + .collect::>() + .join(", ") + ); + // for (name, v) in arguments + // .iter() + // .map(|v| (v.name.clone(), self.ssa_values.get(&v.name))) + // { + // if let Some(v) = v { + // println!(" - {name} = {v}"); + // } + // } + for (name, v) in return_vars + .iter() + .map(|v| (v.name.clone(), self.ssa_values.get(&v.name))) + { + if let Some(v) = v { + println!(" - {name} = {v}"); + } + } + } + _ => {} + } + } + + fn read_memory(&self, offset: &BigUint) -> Option { + let candidate = self.memory.get(offset); + if let Some(ValueByte { + data: candidate, .. + }) = candidate + { + if (0..32u32).all(|i| { + self.memory.get(&(offset.clone() + BigUint::from(i))) + == Some(&ValueByte { + data: candidate.clone(), + byte: i, + }) + }) { + return Some(candidate.clone()); + } + } + + let mut result = vec![0u8; 32]; + for (i, item) in result.iter_mut().enumerate() { + if let Some(v) = self.read_memory_byte(&(offset.clone() + BigUint::from(i))) { + *item = v; + } else { + return None; + } + } + Some(Value::Concrete(BigUint::from_bytes_be(&result))) + } + + fn read_memory_byte(&self, offset: &BigUint) -> Option { + match self.memory.get(offset) { + Some(ValueByte { + data: Value::Concrete(v), + byte: i, + }) => Some( + v.to_bytes_le() + .get((31 - i) as usize) + .copied() + .unwrap_or_default(), + ), + _ => None, + } + } + + fn write_memory(&mut self, offset: BigUint, value: Option) { + match value { + Some(value) => { + for i in 0..32u32 { + self.memory.insert( + offset.clone() + BigUint::from(i), + ValueByte { + data: value.clone(), + byte: i, + }, + ); + } + } + None => { + for i in 0..32u32 { + self.memory.remove(&(offset.clone() + BigUint::from(i))); + } + } + } + } + + fn get_memory_slice(&self, offset: BigUint, len: BigUint) -> Option> { + // TODO aliasing? + (0..(len.to_u64().unwrap())) + .map(|i| self.read_memory_byte(&(offset.clone() + BigUint::from(i)))) + .fold(Some(Vec::::new()), |acc, v| { + if let (Some(mut acc), Some(v)) = (acc, v) { + acc.push(v); + Some(acc) + } else { + None + } + }) + } + + fn unknown_memory_write(&mut self) { + self.memory.clear(); + self.unknown_memory_is_zero = false; + } + fn unknown_memory_write_above(&mut self, offset: &BigUint) { + self.memory.retain(|addr, _| addr < offset); + self.unknown_memory_is_zero = false; + } +} + +fn literal_value(value: &str) -> Option { + if let Some(hex) = value.strip_prefix("0x") { + Some(BigUint::from_str_radix(hex, 16).unwrap()) + } else if value.chars().next().unwrap().is_ascii_digit() { + Some(BigUint::from_str_radix(value, 10).unwrap()) + } else { + None + } +} diff --git a/src/evaluator/mod.rs b/src/evaluator/mod.rs index 071a805..2d4fcd5 100644 --- a/src/evaluator/mod.rs +++ b/src/evaluator/mod.rs @@ -1,9 +1,13 @@ use std::fmt; +use std::fmt::Display; use num_bigint::BigUint; +pub mod engine; pub mod simplifier; +pub use engine::Evaluator; + /// Symbolic or concrete value #[derive(Debug, Clone, PartialEq)] pub enum Value { @@ -20,7 +24,7 @@ pub enum Value { KnownContractAddress(String, u64), } -impl fmt::Display for Value { +impl Display for Value { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Value::Concrete(v) => write!(f, "0x{v:x}"), diff --git a/src/evm_builtins.rs b/src/evm_builtins.rs index fda794f..b25d5c8 100644 --- a/src/evm_builtins.rs +++ b/src/evm_builtins.rs @@ -97,14 +97,17 @@ impl Instructions for EVMInstructions { "calldatasize" => single_return(evm_context::calldatasize(ssa).into()), "calldatacopy" => panic!("Builtin {} not implemented", builtin.name), // TODO "codesize" => single_return(evm_context::codesize(ssa).into()), - "codecopy" => panic!("Builtin {} not implemented", builtin.name), // TODO + "codecopy" => vec![], //panic!("Builtin {} not implemented", builtin.name), // TODO + "datasize" => vec![smt::declare_const(return_vars[0].clone())], // TODO + "dataoffset" => vec![smt::declare_const(return_vars[0].clone())], // TODO + "datacopy" => vec![], //panic!("Builtin {} not implemented", builtin.name), // TODO "gasprice" => single_return(evm_context::gasprice(ssa).into()), - "extcodesize" => panic!("Builtin {} not implemented", builtin.name), // TODO + "extcodesize" => vec![smt::declare_const(return_vars[0].clone())], //panic!("Builtin {} not implemented", builtin.name), // TODO "extcodecopy" => panic!("Builtin {} not implemented", builtin.name), // TODO - "returndatasize" => panic!("Builtin {} not implemented", builtin.name), // TODO - "returndatacopy" => panic!("Builtin {} not implemented", builtin.name), // TODO + "returndatasize" => vec![smt::declare_const(return_vars[0].clone())], //panic!("Builtin {} not implemented", builtin.name), // TODO + "returndatacopy" => vec![], //panic!("Builtin {} not implemented", builtin.name), // TODO "extcodehash" => panic!("Builtin {} not implemented", builtin.name), // TODO - "blockhash" => panic!("Builtin {} not implemented", builtin.name), // TODO + "blockhash" => panic!("Builtin {} not implemented", builtin.name), // TODO "coinbase" => single_return(evm_context::coinbase(ssa).into()), "timestamp" => single_return(evm_context::timestamp(ssa).into()), "number" => single_return(evm_context::number(ssa).into()), @@ -132,12 +135,12 @@ impl Instructions for EVMInstructions { ssa, )], "msize" => panic!("Builtin {} not implemented", builtin.name), // TODO - "gas" => panic!("Builtin {} not implemented", builtin.name), // TODO - "log0" => panic!("Builtin {} not implemented", builtin.name), // TODO - "log1" => panic!("Builtin {} not implemented", builtin.name), // TODO - "log2" => panic!("Builtin {} not implemented", builtin.name), // TODO - "log3" => panic!("Builtin {} not implemented", builtin.name), // TODO - "log4" => panic!("Builtin {} not implemented", builtin.name), // TODO + "gas" => vec![smt::declare_const(return_vars[0].clone())], //panic!("Builtin {} not implemented", builtin.name), // TODO + "log0" => panic!("Builtin {} not implemented", builtin.name), // TODO + "log1" => panic!("Builtin {} not implemented", builtin.name), // TODO + "log2" => panic!("Builtin {} not implemented", builtin.name), // TODO + "log3" => panic!("Builtin {} not implemented", builtin.name), // TODO + "log4" => panic!("Builtin {} not implemented", builtin.name), // TODO "create" => evm_context::create( arg_0.unwrap().into(), MemoryRange::new(arg_1.unwrap(), arg_2.unwrap()), diff --git a/tests/assert_pass/switch_1.yul.smt2 b/tests/assert_pass/switch_1.yul.smt2 index 0a98cfd..55f3239 100644 --- a/tests/assert_pass/switch_1.yul.smt2 +++ b/tests/assert_pass/switch_1.yul.smt2 @@ -38,13 +38,10 @@ (define-const t_4_2 (_ BitVec 256) _5) (define-const r_3_3 (_ BitVec 256) (ite (not (= x_2_1 (_ bv0 256))) r_3_1 r_3_2)) (define-const t_4_3 (_ BitVec 256) (ite (not (= x_2_1 (_ bv0 256))) t_4_1 t_4_2)) -(define-const r_3_4 (_ BitVec 256) t_4_1) -(define-const r_3_5 (_ BitVec 256) (ite (not (= x_2_1 (_ bv1 256))) r_3_3 r_3_4)) -(define-const t_4_4 (_ BitVec 256) (ite (not (= x_2_1 (_ bv1 256))) t_4_3 t_4_1)) (define-const _6 (_ BitVec 256) (_ bv9 256)) -(define-const _7 (_ BitVec 256) (ite (= r_3_5 _6) (_ bv1 256) (_ bv0 256))) +(define-const _7 (_ BitVec 256) (ite (= r_3_3 _6) (_ bv1 256) (_ bv0 256))) (define-const _8 (_ BitVec 256) (_ bv7 256)) -(define-const _9 (_ BitVec 256) (ite (= t_4_4 _8) (_ bv1 256) (_ bv0 256))) +(define-const _9 (_ BitVec 256) (ite (= t_4_3 _8) (_ bv1 256) (_ bv0 256))) (define-const _10 (_ BitVec 256) (bvand _7 _9)) (assert (and (and (= _revert_flag_2070_0 (_ bv0 256)) (= _stop_flag_2069_0 (_ bv0 256))) true (= _10 (_ bv0 256)))) (assert (not (= _revert_flag_2070_0 (_ bv0 256)))) \ No newline at end of file diff --git a/tests/assert_pass/switch_2.yul.smt2 b/tests/assert_pass/switch_2.yul.smt2 index 0d41d18..400b08d 100644 --- a/tests/assert_pass/switch_2.yul.smt2 +++ b/tests/assert_pass/switch_2.yul.smt2 @@ -32,19 +32,12 @@ (define-const r_3_1 (_ BitVec 256) _2) (define-const _3 (_ BitVec 256) (_ bv0 256)) (define-const t_4_1 (_ BitVec 256) _3) -(define-const _4 (_ BitVec 256) (_ bv9 256)) -(define-const r_3_2 (_ BitVec 256) _4) -(define-const _5 (_ BitVec 256) (_ bv7 256)) -(define-const t_4_2 (_ BitVec 256) _5) -(define-const r_3_3 (_ BitVec 256) (ite (not (= x_2_1 (_ bv0 256))) r_3_1 r_3_2)) -(define-const t_4_3 (_ BitVec 256) (ite (not (= x_2_1 (_ bv0 256))) t_4_1 t_4_2)) -(define-const r_3_4 (_ BitVec 256) t_4_1) -(define-const r_3_5 (_ BitVec 256) (ite (not (= x_2_1 (_ bv1 256))) r_3_3 r_3_4)) -(define-const t_4_4 (_ BitVec 256) (ite (not (= x_2_1 (_ bv1 256))) t_4_3 t_4_1)) +(define-const r_3_2 (_ BitVec 256) t_4_1) +(define-const r_3_3 (_ BitVec 256) (ite (not (= x_2_1 (_ bv1 256))) r_3_1 r_3_2)) +(define-const _4 (_ BitVec 256) (_ bv0 256)) +(define-const _5 (_ BitVec 256) (ite (= r_3_3 _4) (_ bv1 256) (_ bv0 256))) (define-const _6 (_ BitVec 256) (_ bv0 256)) -(define-const _7 (_ BitVec 256) (ite (= r_3_5 _6) (_ bv1 256) (_ bv0 256))) -(define-const _8 (_ BitVec 256) (_ bv0 256)) -(define-const _9 (_ BitVec 256) (ite (= t_4_4 _8) (_ bv1 256) (_ bv0 256))) -(define-const _10 (_ BitVec 256) (bvand _7 _9)) -(assert (and (and (= _revert_flag_2070_0 (_ bv0 256)) (= _stop_flag_2069_0 (_ bv0 256))) true (= _10 (_ bv0 256)))) +(define-const _7 (_ BitVec 256) (ite (= t_4_1 _6) (_ bv1 256) (_ bv0 256))) +(define-const _8 (_ BitVec 256) (bvand _5 _7)) +(assert (and (and (= _revert_flag_2070_0 (_ bv0 256)) (= _stop_flag_2069_0 (_ bv0 256))) true (= _8 (_ bv0 256)))) (assert (not (= _revert_flag_2070_0 (_ bv0 256)))) \ No newline at end of file diff --git a/tests/assert_pass/switch_3.yul.smt2 b/tests/assert_pass/switch_3.yul.smt2 index a161c8d..050f074 100644 --- a/tests/assert_pass/switch_3.yul.smt2 +++ b/tests/assert_pass/switch_3.yul.smt2 @@ -32,19 +32,10 @@ (define-const r_3_1 (_ BitVec 256) _2) (define-const _3 (_ BitVec 256) (_ bv0 256)) (define-const t_4_1 (_ BitVec 256) _3) -(define-const _4 (_ BitVec 256) (_ bv9 256)) -(define-const r_3_2 (_ BitVec 256) _4) -(define-const _5 (_ BitVec 256) (_ bv7 256)) -(define-const t_4_2 (_ BitVec 256) _5) -(define-const r_3_3 (_ BitVec 256) (ite (not (= x_2_1 (_ bv0 256))) r_3_1 r_3_2)) -(define-const t_4_3 (_ BitVec 256) (ite (not (= x_2_1 (_ bv0 256))) t_4_1 t_4_2)) -(define-const r_3_4 (_ BitVec 256) t_4_1) -(define-const r_3_5 (_ BitVec 256) (ite (not (= x_2_1 (_ bv1 256))) r_3_3 r_3_4)) -(define-const t_4_4 (_ BitVec 256) (ite (not (= x_2_1 (_ bv1 256))) t_4_3 t_4_1)) -(define-const _6 (_ BitVec 256) (_ bv1 256)) -(define-const _7 (_ BitVec 256) (ite (= r_3_5 _6) (_ bv1 256) (_ bv0 256))) -(define-const _8 (_ BitVec 256) (_ bv0 256)) -(define-const _9 (_ BitVec 256) (ite (= t_4_4 _8) (_ bv1 256) (_ bv0 256))) -(define-const _10 (_ BitVec 256) (bvand _7 _9)) -(assert (and (and (= _revert_flag_2070_0 (_ bv0 256)) (= _stop_flag_2069_0 (_ bv0 256))) true (= _10 (_ bv0 256)))) +(define-const _4 (_ BitVec 256) (_ bv1 256)) +(define-const _5 (_ BitVec 256) (ite (= r_3_1 _4) (_ bv1 256) (_ bv0 256))) +(define-const _6 (_ BitVec 256) (_ bv0 256)) +(define-const _7 (_ BitVec 256) (ite (= t_4_1 _6) (_ bv1 256) (_ bv0 256))) +(define-const _8 (_ BitVec 256) (bvand _5 _7)) +(assert (and (and (= _revert_flag_2070_0 (_ bv0 256)) (= _stop_flag_2069_0 (_ bv0 256))) true (= _8 (_ bv0 256)))) (assert (not (= _revert_flag_2070_0 (_ bv0 256)))) \ No newline at end of file diff --git a/tests/contract_creation_test.yul b/tests/contract_creation_test.yul new file mode 100644 index 0000000..8be6f34 --- /dev/null +++ b/tests/contract_creation_test.yul @@ -0,0 +1,400 @@ +{ + /// @src 0:88:299 "contract Test {..." + mstore(64, memoryguard(128)) + + if iszero(lt(calldatasize(), 4)) + { + let selector := shift_right_224_unsigned(calldataload(0)) + switch selector + + case 0x0a9254e4 + { + // setUp() + + external_fun_setUp_29() + } + + case 0x85632895 + { + // proveA(uint256,uint256) + + external_fun_proveA_63() + } + + default {} + } + + revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74() + + function shift_right_224_unsigned(value) -> newValue { + newValue := + + shr(224, value) + + } + + function allocate_unbounded() -> memPtr { + memPtr := mload(64) + } + + function revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb() { + revert(0, 0) + } + + function revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b() { + revert(0, 0) + } + + function abi_decode_tuple_(headStart, dataEnd) { + if slt(sub(dataEnd, headStart), 0) { revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b() } + + } + + function abi_encode_tuple__to__fromStack(headStart ) -> tail { + tail := add(headStart, 0) + + } + + function external_fun_setUp_29() { + + if callvalue() { revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb() } + abi_decode_tuple_(4, calldatasize()) + fun_setUp_29() + let memPos := allocate_unbounded() + let memEnd := abi_encode_tuple__to__fromStack(memPos ) + return(memPos, sub(memEnd, memPos)) + + } + + function revert_error_c1322bf8034eace5e0b5c7295db60986aa89aae5e0ea0873e4689e076861a5db() { + revert(0, 0) + } + + function cleanup_t_uint256(value) -> cleaned { + cleaned := value + } + + function validator_revert_t_uint256(value) { + if iszero(eq(value, cleanup_t_uint256(value))) { revert(0, 0) } + } + + function abi_decode_t_uint256(offset, end) -> value { + value := calldataload(offset) + validator_revert_t_uint256(value) + } + + function abi_decode_tuple_t_uint256t_uint256(headStart, dataEnd) -> value0, value1 { + if slt(sub(dataEnd, headStart), 64) { revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b() } + + { + + let offset := 0 + + value0 := abi_decode_t_uint256(add(headStart, offset), dataEnd) + } + + { + + let offset := 32 + + value1 := abi_decode_t_uint256(add(headStart, offset), dataEnd) + } + + } + + function external_fun_proveA_63() { + + if callvalue() { revert_error_ca66f745a3ce8ff40e2ccaf1ad45db7774001b90d25810abd9040049be7bf4bb() } + let param_0, param_1 := abi_decode_tuple_t_uint256t_uint256(4, calldatasize()) + fun_proveA_63(param_0, param_1) + let memPos := allocate_unbounded() + let memEnd := abi_encode_tuple__to__fromStack(memPos ) + return(memPos, sub(memEnd, memPos)) + + } + + function revert_error_42b3090547df1d2001c96683413b8cf91c1b902ef5e3cb8d9f6f304cf7446f74() { + revert(0, 0) + } + + function panic_error_0x41() { + mstore(0, 35408467139433450592217433187231851964531694900788300625387963629091585785856) + mstore(4, 0x41) + revert(0, 0x24) + } + + function revert_forward_1() { + let pos := allocate_unbounded() + returndatacopy(pos, 0, returndatasize()) + revert(pos, returndatasize()) + } + + function shift_left_0(value) -> newValue { + newValue := + + shl(0, value) + + } + + function update_byte_slice_20_shift_0(value, toInsert) -> result { + let mask := 0xffffffffffffffffffffffffffffffffffffffff + toInsert := shift_left_0(toInsert) + value := and(value, not(mask)) + result := or(value, and(toInsert, mask)) + } + + function cleanup_t_uint160(value) -> cleaned { + cleaned := and(value, 0xffffffffffffffffffffffffffffffffffffffff) + } + + function identity(value) -> ret { + ret := value + } + + function convert_t_uint160_to_t_uint160(value) -> converted { + converted := cleanup_t_uint160(identity(cleanup_t_uint160(value))) + } + + function convert_t_uint160_to_t_contract$_ToTest_$15(value) -> converted { + converted := convert_t_uint160_to_t_uint160(value) + } + + function convert_t_contract$_ToTest_$15_to_t_contract$_ToTest_$15(value) -> converted { + converted := convert_t_uint160_to_t_contract$_ToTest_$15(value) + } + + function prepare_store_t_contract$_ToTest_$15(value) -> ret { + ret := value + } + + function update_storage_value_offset_0t_contract$_ToTest_$15_to_t_contract$_ToTest_$15(slot, value_0) { + let convertedValue_0 := convert_t_contract$_ToTest_$15_to_t_contract$_ToTest_$15(value_0) + sstore(slot, update_byte_slice_20_shift_0(sload(slot), prepare_store_t_contract$_ToTest_$15(convertedValue_0))) + } + + /// @ast-id 29 + /// @src 0:118:169 "function setUp() public {..." + function fun_setUp_29() { + + /// @src 0:152:164 "new ToTest()" + let _1 := allocate_unbounded() + let _2 := add(_1, datasize("ToTest_15")) + if or(gt(_2, 0xffffffffffffffff), lt(_2, _1)) { panic_error_0x41() } + datacopy(_1, dataoffset("ToTest_15"), datasize("ToTest_15")) + _2 := abi_encode_tuple__to__fromStack(_2) + + let expr_25_address := create(0, _1, sub(_2, _1)) + + if iszero(expr_25_address) { revert_forward_1() } + + /// @src 0:148:164 "t = new ToTest()" + update_storage_value_offset_0t_contract$_ToTest_$15_to_t_contract$_ToTest_$15(0x00, expr_25_address) + let expr_26_address := expr_25_address + + } + /// @src 0:88:299 "contract Test {..." + + function cleanup_t_rational_10_by_1(value) -> cleaned { + cleaned := value + } + + function convert_t_rational_10_by_1_to_t_uint256(value) -> converted { + converted := cleanup_t_uint256(identity(cleanup_t_rational_10_by_1(value))) + } + + function require_helper(condition) { + if iszero(condition) { revert(0, 0) } + } + + function shift_right_0_unsigned(value) -> newValue { + newValue := + + shr(0, value) + + } + + function cleanup_from_storage_t_contract$_ToTest_$15(value) -> cleaned { + cleaned := and(value, 0xffffffffffffffffffffffffffffffffffffffff) + } + + function extract_from_storage_value_offset_0t_contract$_ToTest_$15(slot_value) -> value { + value := cleanup_from_storage_t_contract$_ToTest_$15(shift_right_0_unsigned(slot_value)) + } + + function read_from_storage_split_offset_0_t_contract$_ToTest_$15(slot) -> value { + value := extract_from_storage_value_offset_0t_contract$_ToTest_$15(sload(slot)) + + } + + function convert_t_uint160_to_t_address(value) -> converted { + converted := convert_t_uint160_to_t_uint160(value) + } + + function convert_t_contract$_ToTest_$15_to_t_address(value) -> converted { + converted := convert_t_uint160_to_t_address(value) + } + + function revert_error_0cc013b6b3b6beabea4e3a74a6d380f0df81852ca99887912475e1f66b2a2c20() { + revert(0, 0) + } + + function round_up_to_mul_of_32(value) -> result { + result := and(add(value, 31), not(31)) + } + + function finalize_allocation(memPtr, size) { + let newFreePtr := add(memPtr, round_up_to_mul_of_32(size)) + // protect against overflow + if or(gt(newFreePtr, 0xffffffffffffffff), lt(newFreePtr, memPtr)) { panic_error_0x41() } + mstore(64, newFreePtr) + } + + function shift_left_224(value) -> newValue { + newValue := + + shl(224, value) + + } + + function abi_decode_t_uint256_fromMemory(offset, end) -> value { + value := mload(offset) + validator_revert_t_uint256(value) + } + + function abi_decode_tuple_t_uint256_fromMemory(headStart, dataEnd) -> value0 { + if slt(sub(dataEnd, headStart), 32) { revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b() } + + { + + let offset := 0 + + value0 := abi_decode_t_uint256_fromMemory(add(headStart, offset), dataEnd) + } + + } + + function abi_encode_t_uint256_to_t_uint256_fromStack(value, pos) { + mstore(pos, cleanup_t_uint256(value)) + } + + function abi_encode_tuple_t_uint256_t_uint256__to_t_uint256_t_uint256__fromStack(headStart , value0, value1) -> tail { + tail := add(headStart, 64) + + abi_encode_t_uint256_to_t_uint256_fromStack(value0, add(headStart, 0)) + + abi_encode_t_uint256_to_t_uint256_fromStack(value1, add(headStart, 32)) + + } + + function panic_error_0x11() { + mstore(0, 35408467139433450592217433187231851964531694900788300625387963629091585785856) + mstore(4, 0x11) + revert(0, 0x24) + } + + function checked_add_t_uint256(x, y) -> sum { + x := cleanup_t_uint256(x) + y := cleanup_t_uint256(y) + sum := add(x, y) + + if gt(x, sum) { panic_error_0x11() } + + } + + function panic_error_0x01() { + mstore(0, 35408467139433450592217433187231851964531694900788300625387963629091585785856) + mstore(4, 0x01) + revert(0, 0x24) + } + + function assert_helper(condition) { + if iszero(condition) { panic_error_0x01() } + } + + /// @ast-id 63 + /// @src 0:172:297 "function proveA(uint a, uint b) public {..." + function fun_proveA_63(var_a_31, var_b_33) { + + /// @src 0:225:226 "a" + let _3 := var_a_31 + let expr_37 := _3 + /// @src 0:230:232 "10" + let expr_38 := 0x0a + /// @src 0:225:232 "a <= 10" + let expr_39 := iszero(gt(cleanup_t_uint256(expr_37), convert_t_rational_10_by_1_to_t_uint256(expr_38))) + /// @src 0:225:243 "a <= 10 && b <= 10" + let expr_43 := expr_39 + if expr_43 { + /// @src 0:236:237 "b" + let _4 := var_b_33 + let expr_40 := _4 + /// @src 0:241:243 "10" + let expr_41 := 0x0a + /// @src 0:236:243 "b <= 10" + let expr_42 := iszero(gt(cleanup_t_uint256(expr_40), convert_t_rational_10_by_1_to_t_uint256(expr_41))) + /// @src 0:225:243 "a <= 10 && b <= 10" + expr_43 := expr_42 + } + /// @src 0:217:244 "require(a <= 10 && b <= 10)" + require_helper(expr_43) + /// @src 0:259:260 "t" + let _5_address := read_from_storage_split_offset_0_t_contract$_ToTest_$15(0x00) + let expr_48_address := _5_address + /// @src 0:259:262 "t.f" + let expr_49_address := convert_t_contract$_ToTest_$15_to_t_address(expr_48_address) + let expr_49_functionSelector := 0x13d1aa2e + /// @src 0:263:264 "a" + let _6 := var_a_31 + let expr_50 := _6 + /// @src 0:266:267 "b" + let _7 := var_b_33 + let expr_51 := _7 + /// @src 0:259:268 "t.f(a, b)" + + // storage for arguments and returned data + let _8 := allocate_unbounded() + mstore(_8, shift_left_224(expr_49_functionSelector)) + let _9 := abi_encode_tuple_t_uint256_t_uint256__to_t_uint256_t_uint256__fromStack(add(_8, 4) , expr_50, expr_51) + + let _10 := call(gas(), expr_49_address, 0, _8, sub(_9, _8), _8, 32) + + if iszero(_10) { revert_forward_1() } + + let expr_52 + if _10 { + + let _11 := 32 + + if gt(_11, returndatasize()) { + _11 := returndatasize() + } + + // update freeMemoryPointer according to dynamic return size + finalize_allocation(_8, _11) + + // decode return parameters from external try-call into retVars + expr_52 := abi_decode_tuple_t_uint256_fromMemory(_8, add(_8, _11)) + } + /// @src 0:250:268 "uint r = t.f(a, b)" + let var_r_47 := expr_52 + /// @src 0:281:282 "r" + let _12 := var_r_47 + let expr_55 := _12 + /// @src 0:286:287 "a" + let _13 := var_a_31 + let expr_56 := _13 + /// @src 0:290:291 "b" + let _14 := var_b_33 + let expr_57 := _14 + /// @src 0:286:291 "a + b" + let expr_58 := checked_add_t_uint256(expr_56, expr_57) + + /// @src 0:281:291 "r == a + b" + let expr_59 := eq(cleanup_t_uint256(expr_55), cleanup_t_uint256(expr_58)) + /// @src 0:274:292 "assert(r == a + b)" + assert_helper(expr_59) + + } + /// @src 0:88:299 "contract Test {..." + +} diff --git a/tests/integration.rs b/tests/integration.rs index 7c95d54..362605f 100644 --- a/tests/integration.rs +++ b/tests/integration.rs @@ -2,6 +2,7 @@ use std::{fs, fs::File, path::Path}; use yools::encoder; use yools::encoder::Instructions; +use yools::evaluator::Evaluator; use yools::evm_builtins::EVMInstructions; use yools::evm_context; use yools::smt::{self, SMTExpr, SMTStatement, SMTVariable}; @@ -49,6 +50,37 @@ impl encoder::Instructions for EVMInstructionsWithAssert { } } +#[test] +fn recognize_known_contract() { + let file = "tests/contract_creation_test.yul"; + let content = fs::read_to_string(file).expect("I need to read this file."); + let main_ast = parse_and_resolve::(&content, file); + + println!("=========== SETUP ==================="); + let mut ssa_tracker = SSATracker::default(); + let mut evaluator = Evaluator::default(); + evaluator.new_transaction(b"\x0a\x92\x54\xe4".to_vec()); + // TODO also provide calldata to encoder? + let mut query; + (query, evaluator, ssa_tracker) = encoder::encode_with_evaluator::( + &main_ast, + loop_unroll_default(&content), + evaluator, + ssa_tracker, + ); + println!("=========== CALL ==================="); + evaluator.new_transaction(b"\x85\x63\x28\x95".to_vec()); + let (query2, ..) = encoder::encode_with_evaluator::( + &main_ast, + loop_unroll_default(&content), + evaluator, + ssa_tracker, + ); + query += &query2; + unsat(&query, file); + // TODO the actual test. +} + #[test] fn test_syntax() { test_dir(