Skip to content

Commit b57985c

Browse files
chrisethchriseth
committed
Use evaluator to eliminate if and switch branches.
1 parent c318ba3 commit b57985c

File tree

3 files changed

+97
-53
lines changed

3 files changed

+97
-53
lines changed

‎src/encoder.rs

+6
Original file line numberDiff line numberDiff line change
@@ -256,6 +256,9 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
256256
fn encode_if(&mut self, expr: &yul::If) {
257257
let cond = self.encode_expression(&expr.condition);
258258
assert!(cond.len() == 1);
259+
if self.evaluator.variable_known_equal(&cond[0], &"0".to_string()) {
260+
return;
261+
}
259262
let prev_ssa = self.ssa_tracker.copy_current_ssa();
260263

261264
self.push_path_condition(smt::neq(cond[0].clone(), 0));
@@ -303,6 +306,9 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
303306
} in &switch.cases
304307
{
305308
let is_default = literal.is_none();
309+
if !is_default && self.evaluator.variable_known_unequal(&discriminator[0], &literal.as_ref().unwrap().literal) {
310+
continue;
311+
}
306312

307313
self.ssa_tracker.set_current_ssa(pre_switch_ssa.clone());
308314

‎src/evaluator.rs

+89-53
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ enum Value {
3636
struct ValueByte {
3737
data: Value,
3838
/// Byte of the data, 0 is most significant byte.
39-
byte: u32
39+
byte: u32,
4040
}
4141

4242
impl Display for Value {
@@ -82,8 +82,29 @@ impl Evaluator {
8282
/// TODO should also set the current address.
8383
pub fn new_transaction(&mut self, calldata: Vec<u8>) {
8484
self.calldata = Some(calldata);
85+
self.memory.clear();
86+
self.memory_slices.clear();
8587
self.unknown_memory_is_zero = true;
8688
}
89+
/// Returns true if the evaluator can determine that the variable is equal
90+
/// to the given literal value with the previously set restrictions.
91+
pub fn variable_known_equal(&self, var: &SMTVariable, value: &String) -> bool {
92+
if let Some(Value::Concrete(v)) = self.ssa_values.get(&var.name) {
93+
if let Some(lit) = literal_value(value) {
94+
return *v == lit;
95+
}
96+
}
97+
false
98+
}
99+
pub fn variable_known_unequal(&self, var: &SMTVariable, value: &String) -> bool {
100+
if let Some(Value::Concrete(v)) = self.ssa_values.get(&var.name) {
101+
if let Some(lit) = literal_value(value) {
102+
return *v != lit;
103+
}
104+
}
105+
false
106+
}
107+
87108
pub fn define_from_literal(&mut self, var: &SMTVariable, literal: &Literal) {
88109
let value = &literal.literal;
89110
//println!("{} := {literal}", var.name);
@@ -113,37 +134,6 @@ impl Evaluator {
113134
arguments: &Vec<SMTVariable>,
114135
return_vars: &[SMTVariable],
115136
) {
116-
if builtin.name == "create" {
117-
println!(
118-
"Create: {:?} {:?} {:?}",
119-
arguments[0], arguments[1], arguments[2]
120-
);
121-
122-
// self.ssa_values
123-
// .insert(return_vars[0].name.clone(), BigUint::from(1234u64));
124-
}
125-
// if builtin.name == "sstore" {
126-
// if let (Some(key), Some(value)) = (
127-
// self.ssa_values.get(&arguments[0].name).cloned(),
128-
// self.ssa_values.get(&arguments[1].name).cloned(),
129-
// ) {
130-
// self.storage.insert(key, value);
131-
// }
132-
// }
133-
// if builtin.name == "sload" {
134-
// if let Some(key) = self.ssa_values.get(&arguments[0].name).cloned() {
135-
// if let Some(value) = self.storage.get(&key).cloned() {
136-
// self.ssa_values.insert(return_vars[0].name.clone(), value);
137-
// } else {
138-
// // TODO assume unknown storage is some weird value - should use unknown bits later
139-
// self.ssa_values.insert(
140-
// return_vars[0].name.clone(),
141-
// BigUint::from(0x1234567812345678u64),
142-
// );
143-
// }
144-
// }
145-
// }
146-
147137
let mask = (BigUint::from(1u64) << 256) - BigUint::from(1u64);
148138
let two256 = BigUint::from(1u64) << 256;
149139
let address_mask = (BigUint::from(1u64) << 160) - BigUint::from(1u64);
@@ -200,6 +190,18 @@ impl Evaluator {
200190
self.memory_slices.insert(addr.clone(), Value::DataRef(offset.clone()));
201191
None
202192
}
193+
("calldatasize", []) => {
194+
self.calldata.as_ref().map(|cd| Value::Concrete(BigUint::from(cd.len())))
195+
}
196+
("calldataload", [Some(Value::Concrete(addr))]) => {
197+
self.calldata.as_ref().map(|cd| {
198+
let mut result = vec![0u8; 32];
199+
for i in 0..32usize {
200+
result[i] = cd.get(addr.to_usize().unwrap() + i).copied().unwrap_or_default();
201+
}
202+
Value::Concrete(BigUint::from_bytes_be(&result))
203+
})
204+
}
203205
("create", [_ether_value, Some(Value::Concrete(offset)), _size /* TODO check size */]) => {
204206
if let Some(Value::DataRef(name)) = self.memory_slices.get(offset) {
205207
Some(Value::KnownContractAddress(name.clone(), 0)) // TODO increment coutner
@@ -233,14 +235,17 @@ impl Evaluator {
233235
self.ssa_values.insert(return_vars[0].name.clone(), result);
234236
}
235237
if builtin.name == "call" {
236-
for i in 0x80..0xc4 {
237-
println!("{:x}: {:x?}", i,self.read_memory_byte(&BigUint::from(i as u32)));
238-
}
238+
// for i in 0x80..0xc4 {
239+
// println!(
240+
// "{:x}: {:x?}",
241+
// i,
242+
// self.read_memory_byte(&BigUint::from(i as u32))
243+
// );
244+
// }
239245
// if let (Some(Value::Concrete(in_offset)), Some(Value::Concrete(in_len))) = (&arg_values[3], &arg_values[4]) {
240246
// println!("{:x?}", &self.get_memory_slice(in_offset.clone(), in_len.clone()).unwrap());
241247

242248
// }
243-
244249
}
245250
match builtin.name {
246251
"create" | "sstore" | "sload" | "call" | "datacopy" | "mstore" => {
@@ -294,8 +299,17 @@ impl Evaluator {
294299

295300
fn read_memory(&self, offset: &BigUint) -> Option<Value> {
296301
let candidate = self.memory.get(offset);
297-
if let Some(ValueByte{data: candidate, ..}) = candidate {
298-
if (0..32u32).all(|i| self.memory.get(&(offset.clone() + BigUint::from(i))) == Some(&ValueByte{data: candidate.clone(), byte: i}) ) {
302+
if let Some(ValueByte {
303+
data: candidate, ..
304+
}) = candidate
305+
{
306+
if (0..32u32).all(|i| {
307+
self.memory.get(&(offset.clone() + BigUint::from(i)))
308+
== Some(&ValueByte {
309+
data: candidate.clone(),
310+
byte: i,
311+
})
312+
}) {
299313
return Some(candidate.clone());
300314
}
301315
}
@@ -313,18 +327,30 @@ impl Evaluator {
313327

314328
fn read_memory_byte(&self, offset: &BigUint) -> Option<u8> {
315329
match self.memory.get(offset) {
316-
Some(ValueByte{data: Value::Concrete(v), byte: i}) => {
317-
Some(v.to_bytes_le().get((31 - i) as usize).copied().unwrap_or_default())
318-
}
319-
_ => None
330+
Some(ValueByte {
331+
data: Value::Concrete(v),
332+
byte: i,
333+
}) => Some(
334+
v.to_bytes_le()
335+
.get((31 - i) as usize)
336+
.copied()
337+
.unwrap_or_default(),
338+
),
339+
_ => None,
320340
}
321341
}
322342

323343
fn write_memory(&mut self, offset: BigUint, value: Option<Value>) {
324344
match value {
325345
Some(value) => {
326346
for i in 0..32u32 {
327-
self.memory.insert(offset.clone() + BigUint::from(i), ValueByte{data: value.clone(), byte: i});
347+
self.memory.insert(
348+
offset.clone() + BigUint::from(i),
349+
ValueByte {
350+
data: value.clone(),
351+
byte: i,
352+
},
353+
);
328354
}
329355
}
330356
None => {
@@ -337,16 +363,16 @@ impl Evaluator {
337363

338364
fn get_memory_slice(&self, offset: BigUint, len: BigUint) -> Option<Vec<u8>> {
339365
// TODO aliasing?
340-
(0..(len.to_u64().unwrap())).map(|i| {
341-
self.read_memory_byte(&(offset.clone() + BigUint::from(i)))
342-
}).fold(Some(Vec::<u8>::new()), |acc, v| {
343-
if let (Some(mut acc), Some(v)) = (acc, v) {
344-
acc.push(v);
345-
Some(acc)
346-
} else {
347-
None
348-
}
349-
})
366+
(0..(len.to_u64().unwrap()))
367+
.map(|i| self.read_memory_byte(&(offset.clone() + BigUint::from(i))))
368+
.fold(Some(Vec::<u8>::new()), |acc, v| {
369+
if let (Some(mut acc), Some(v)) = (acc, v) {
370+
acc.push(v);
371+
Some(acc)
372+
} else {
373+
None
374+
}
375+
})
350376
}
351377
}
352378

@@ -355,3 +381,13 @@ fn wrap(mut x: BigUint) -> BigUint {
355381
// TODO optimization: work directly on limbs
356382
x & mask
357383
}
384+
385+
fn literal_value(value: &String) -> Option<BigUint> {
386+
if let Some(hex) = value.strip_prefix("0x") {
387+
Some(BigUint::from_str_radix(hex, 16).unwrap())
388+
} else if matches!(value.chars().next().unwrap(), '0'..='9') {
389+
Some(BigUint::from_str_radix(value, 10).unwrap())
390+
} else {
391+
None
392+
}
393+
}

‎tests/integration.rs

+2
Original file line numberDiff line numberDiff line change
@@ -62,6 +62,7 @@ fn recognize_known_contract() {
6262
let content = fs::read_to_string(file).expect("I need to read this file.");
6363
let main_ast = parse_and_resolve::<EVMInstructionsWithAssert>(&content, file);
6464

65+
println!("=========== SETUP ===================");
6566
let mut evaluator = Evaluator::default();
6667
evaluator.new_transaction(b"\x0a\x92\x54\xe4".to_vec());
6768
// TODO also provide calldata to encoder?
@@ -71,6 +72,7 @@ fn recognize_known_contract() {
7172
loop_unroll_default(&content),
7273
evaluator,
7374
);
75+
println!("=========== CALL ===================");
7476
evaluator.new_transaction(b"\x85\x63\x28\x95".to_vec());
7577
encoder::encode_with_evaluator::<EVMInstructionsWithAssert>(
7678
&main_ast,

0 commit comments

Comments
 (0)