|
| 1 | +use std::collections::HashMap; |
| 2 | + |
| 3 | +use num_bigint::BigUint; |
| 4 | +use num_traits::{Num, ToPrimitive}; |
| 5 | +use yultsur::{dialect::Builtin, yul::Literal}; |
| 6 | + |
| 7 | +use crate::smt::SMTVariable; |
| 8 | + |
| 9 | +#[derive(Default)] |
| 10 | +pub struct Evaluator { |
| 11 | + ssa_values: HashMap<String, BigUint>, |
| 12 | + storage: HashMap<BigUint, BigUint>, |
| 13 | +} |
| 14 | + |
| 15 | +// TODO |
| 16 | +// As soon as we handle side-effecty things, we might have to include |
| 17 | +// "executing regularly": |
| 18 | +// sstore(0, 1) |
| 19 | +// stop() |
| 20 | +// sload(0) |
| 21 | +// |
| 22 | +// Also, storage needs to take branches into account. |
| 23 | +// if x { sstore(0, 1) } |
| 24 | +// let t := sload(0) |
| 25 | +// |
| 26 | +// If storage is not changed in a branch, its ssa variable is not updated. |
| 27 | +// If all storage writes are to compile-time constant variables, |
| 28 | +// then the Evaluator can deal with the branch joins. |
| 29 | +// Which means we have to have a mechanism to craete a snapshot of the state (like the SSATracker does) |
| 30 | +// and then combine snapshots. |
| 31 | +// |
| 32 | +// Because of packed storage, the values we store should ideally be byte-wise. |
| 33 | +// For now, the following could be OK: |
| 34 | +// It's one of the following: |
| 35 | +// - unknown |
| 36 | +// - a symbolic value in the lower 20 bytes (the rest of the bytes are unknown) |
| 37 | +// - a concrete value |
| 38 | + |
| 39 | +impl Evaluator { |
| 40 | + pub fn define_from_literal(&mut self, var: &SMTVariable, literal: &Literal) { |
| 41 | + let value = &literal.literal; |
| 42 | + //println!("{} := {literal}", var.name); |
| 43 | + self.ssa_values.insert( |
| 44 | + var.name.clone(), |
| 45 | + if let Some(hex) = value.strip_prefix("0x") { |
| 46 | + BigUint::from_str_radix(hex, 16).unwrap() |
| 47 | + } else { |
| 48 | + BigUint::from_str_radix(value, 10).unwrap() |
| 49 | + }, |
| 50 | + ); |
| 51 | + } |
| 52 | + pub fn define_from_variable(&mut self, var: &SMTVariable, value: &SMTVariable) { |
| 53 | + //println!("{} := {}", var.name, value.name); |
| 54 | + if let Some(value) = self.ssa_values.get(&value.name).cloned() { |
| 55 | + self.ssa_values.insert(var.name.clone(), value); |
| 56 | + } |
| 57 | + } |
| 58 | + pub fn builtin_call( |
| 59 | + &mut self, |
| 60 | + builtin: &Builtin, |
| 61 | + arguments: &Vec<SMTVariable>, |
| 62 | + return_vars: &[SMTVariable], |
| 63 | + ) { |
| 64 | + if builtin.name == "create" { |
| 65 | + self.ssa_values |
| 66 | + .insert(return_vars[0].name.clone(), BigUint::from(1234u64)); |
| 67 | + } |
| 68 | + if builtin.name == "sstore" { |
| 69 | + if let (Some(key), Some(value)) = ( |
| 70 | + self.ssa_values.get(&arguments[0].name).cloned(), |
| 71 | + self.ssa_values.get(&arguments[1].name).cloned(), |
| 72 | + ) { |
| 73 | + self.storage.insert(key, value); |
| 74 | + } |
| 75 | + } |
| 76 | + if builtin.name == "sload" { |
| 77 | + if let Some(key) = self.ssa_values.get(&arguments[0].name).cloned() { |
| 78 | + if let Some(value) = self.storage.get(&key).cloned() { |
| 79 | + self.ssa_values.insert(return_vars[0].name.clone(), value); |
| 80 | + } else { |
| 81 | + // TODO assume unknown storage is some weird value - should use unknown bits later |
| 82 | + self.ssa_values.insert( |
| 83 | + return_vars[0].name.clone(), |
| 84 | + BigUint::from(0x1234567812345678u64), |
| 85 | + ); |
| 86 | + } |
| 87 | + } |
| 88 | + } |
| 89 | + if matches!( |
| 90 | + builtin.name, |
| 91 | + "add" | "sub" | "mul" | "div" | "shl" | "shr" | "and" | "or" |
| 92 | + ) { |
| 93 | + if let (Some(left), Some(right)) = ( |
| 94 | + self.ssa_values.get(&arguments[0].name).cloned(), |
| 95 | + self.ssa_values.get(&arguments[1].name).cloned(), |
| 96 | + ) { |
| 97 | + let two256 = BigUint::from(1u64) << 256; |
| 98 | + let result = match builtin.name { |
| 99 | + "add" => wrap(left + right), |
| 100 | + "sub" => wrap(left + two256 - right), |
| 101 | + "shl" => { |
| 102 | + if left >= 256u64.into() { |
| 103 | + BigUint::from(0u64) |
| 104 | + } else { |
| 105 | + wrap(right << left.to_u64().unwrap()) |
| 106 | + } |
| 107 | + } |
| 108 | + "shr" => { |
| 109 | + if left >= 256u64.into() { |
| 110 | + BigUint::from(0u64) |
| 111 | + } else { |
| 112 | + wrap(right >> left.to_u64().unwrap()) |
| 113 | + } |
| 114 | + } |
| 115 | + "and" => left & right, |
| 116 | + "or" => left | right, |
| 117 | + _ => panic!(), |
| 118 | + }; |
| 119 | + self.ssa_values.insert(return_vars[0].name.clone(), result); |
| 120 | + } |
| 121 | + } |
| 122 | + if matches!(builtin.name, "not" | "iszero") { |
| 123 | + if let Some(arg) = self.ssa_values.get(&arguments[0].name).cloned() { |
| 124 | + let mask = (BigUint::from(1u64) << 256) - BigUint::from(1u64); |
| 125 | + let result = match builtin.name { |
| 126 | + "not" => arg ^ mask, |
| 127 | + "iszero" => { |
| 128 | + if arg == BigUint::from(0u64) { |
| 129 | + BigUint::from(1u64) |
| 130 | + } else { |
| 131 | + BigUint::from(0u64) |
| 132 | + } |
| 133 | + } |
| 134 | + _ => panic!(), |
| 135 | + }; |
| 136 | + self.ssa_values.insert(return_vars[0].name.clone(), result); |
| 137 | + } |
| 138 | + } |
| 139 | + match builtin.name { |
| 140 | + "create" | "sstore" | "sload" | "call" => { |
| 141 | + println!( |
| 142 | + "{}{}({})", |
| 143 | + if return_vars.is_empty() { |
| 144 | + String::new() |
| 145 | + } else { |
| 146 | + format!( |
| 147 | + "{} := ", |
| 148 | + return_vars |
| 149 | + .iter() |
| 150 | + .map(|v| v.name.to_owned()) |
| 151 | + .collect::<Vec<_>>() |
| 152 | + .join(", ") |
| 153 | + ) |
| 154 | + }, |
| 155 | + builtin.name, |
| 156 | + arguments |
| 157 | + .iter() |
| 158 | + .map(|v| v.name.to_owned()) |
| 159 | + .collect::<Vec<_>>() |
| 160 | + .join(", ") |
| 161 | + ); |
| 162 | + for (name, v) in arguments |
| 163 | + .iter() |
| 164 | + .map(|v| (v.name.clone(), self.ssa_values.get(&v.name))) |
| 165 | + { |
| 166 | + if let Some(v) = v { |
| 167 | + println!(" - {name} = {v}"); |
| 168 | + } |
| 169 | + } |
| 170 | + for (name, v) in return_vars |
| 171 | + .iter() |
| 172 | + .map(|v| (v.name.clone(), self.ssa_values.get(&v.name))) |
| 173 | + { |
| 174 | + if let Some(v) = v { |
| 175 | + println!(" - {name} = {v}"); |
| 176 | + } |
| 177 | + } |
| 178 | + } |
| 179 | + _ => {} |
| 180 | + } |
| 181 | + } |
| 182 | +} |
| 183 | + |
| 184 | +fn wrap(mut x: BigUint) -> BigUint { |
| 185 | + let mask = (BigUint::from(1u64) << 256) - BigUint::from(1u64); |
| 186 | + // TODO optimization: work directly on limbs |
| 187 | + x & mask |
| 188 | +} |
0 commit comments