foundry_evm_symbolic/runtime/
evm.rs

1use super::*;
2
3/// Returns the `failed_slot` EVM semantics helper result.
4pub(crate) fn failed_slot() -> U256 {
5    let mut bytes = [0u8; 32];
6    bytes[..6].copy_from_slice(b"failed");
7    U256::from_be_bytes(bytes)
8}
9
10/// Computes the `pow_mod` EVM semantics helper result.
11pub(crate) fn pow_mod(base: U256, exponent: U256) -> U256 {
12    let mut result = U256::from(1);
13    let mut base = base;
14    let mut exponent = exponent;
15    while !exponent.is_zero() {
16        if exponent & U256::from(1) == U256::from(1) {
17            result = result.wrapping_mul(base);
18        }
19        exponent >>= 1;
20        base = base.wrapping_mul(base);
21    }
22    result
23}
24
25/// Computes the `exp_expr_for_concrete_exponent` EVM semantics helper result.
26pub(crate) fn exp_expr_for_concrete_exponent(base: Expr, exponent: usize) -> Expr {
27    let mut expr = Expr::Const(U256::from(1));
28    for _ in 0..exponent {
29        expr = Expr::op(ExprOp::Mul, expr, base.clone());
30    }
31    expr_const_value(&expr).map(Expr::Const).unwrap_or(expr)
32}
33
34/// Implements the `slt` EVM semantics helper.
35pub(crate) fn slt(left: U256, right: U256) -> bool {
36    let left_negative = (left >> 255) == U256::from(1);
37    let right_negative = (right >> 255) == U256::from(1);
38    match (left_negative, right_negative) {
39        (true, false) => true,
40        (false, true) => false,
41        _ => left < right,
42    }
43}
44
45/// Implements the `signed_abs` EVM semantics helper.
46pub(crate) fn signed_abs(value: U256) -> U256 {
47    if (value >> 255) == U256::from(1) { (!value).wrapping_add(U256::from(1)) } else { value }
48}
49
50/// Implements the `sdiv` EVM semantics helper.
51pub(crate) fn sdiv(left: U256, right: U256) -> U256 {
52    if right.is_zero() {
53        return U256::ZERO;
54    }
55    let left_negative = (left >> 255) == U256::from(1);
56    let right_negative = (right >> 255) == U256::from(1);
57    let quotient = signed_abs(left) / signed_abs(right);
58    if left_negative ^ right_negative { (!quotient).wrapping_add(U256::from(1)) } else { quotient }
59}
60
61/// Implements the `smod` EVM semantics helper.
62pub(crate) fn smod(left: U256, right: U256) -> U256 {
63    if right.is_zero() {
64        return U256::ZERO;
65    }
66    let left_negative = (left >> 255) == U256::from(1);
67    let remainder = signed_abs(left) % signed_abs(right);
68    if left_negative { (!remainder).wrapping_add(U256::from(1)) } else { remainder }
69}
70
71/// Implements the `signextend` EVM semantics helper.
72pub(crate) fn signextend(byte_index: U256, value: U256) -> U256 {
73    if byte_index >= U256::from(32) {
74        return value;
75    }
76    let bit_index = byte_index.to::<usize>() * 8 + 7;
77    let sign_bit = U256::from(1) << bit_index;
78    let mask = sign_bit - U256::from(1);
79    if value & sign_bit == U256::ZERO { value & mask } else { value | !mask }
80}
81
82/// Implements the `signextend_word` EVM semantics helper.
83pub(crate) fn signextend_word(byte_index: U256, value: SymWord) -> SymWord {
84    if byte_index >= U256::from(32) {
85        return value;
86    }
87    match value {
88        SymWord::Concrete(value) => SymWord::Concrete(signextend(byte_index, value)),
89        value => {
90            let bit_index = byte_index.to::<usize>() * 8 + 7;
91            let sign_bit = U256::from(1) << bit_index;
92            let mask = sign_bit - U256::from(1);
93            let value = value.into_expr();
94            SymWord::Expr(Expr::Ite(
95                Box::new(BoolExpr::eq(
96                    Expr::op(ExprOp::And, value.clone(), Expr::Const(sign_bit)),
97                    Expr::Const(U256::ZERO),
98                )),
99                Box::new(Expr::op(ExprOp::And, value.clone(), Expr::Const(mask))),
100                Box::new(Expr::op(ExprOp::Or, value, Expr::Const(!mask))),
101            ))
102        }
103    }
104}
105
106/// Implements the `signextend_word_dynamic` EVM semantics helper.
107pub(crate) fn signextend_word_dynamic(byte_index: SymWord, value: SymWord) -> SymWord {
108    if let SymWord::Concrete(byte_index) = byte_index {
109        return signextend_word(byte_index, value);
110    }
111
112    let byte_index = byte_index.into_expr();
113    let mut result = value.clone().into_expr();
114    for idx in (0..32).rev() {
115        result = Expr::Ite(
116            Box::new(BoolExpr::eq(byte_index.clone(), Expr::Const(U256::from(idx)))),
117            Box::new(signextend_word(U256::from(idx), value.clone()).into_expr()),
118            Box::new(result),
119        );
120    }
121    SymWord::Expr(result)
122}
123
124/// Returns the `byte_word` EVM semantics helper result.
125pub(crate) fn byte_word(index: U256, word: SymWord) -> SymWord {
126    if index >= U256::from(32) {
127        return SymWord::zero();
128    }
129    let index = index.to::<usize>();
130    match word {
131        SymWord::Concrete(word) => SymWord::Concrete(U256::from(word.to_be_bytes::<32>()[index])),
132        word => {
133            let expr = word.into_expr();
134            if let Some(byte) = expr_known_byte(&expr, index) {
135                return SymWord::Concrete(U256::from(byte));
136            }
137            let shift = U256::from((31 - index) * 8);
138            SymWord::Expr(Expr::op(
139                ExprOp::And,
140                Expr::op(ExprOp::Shr, expr, Expr::Const(shift)),
141                Expr::Const(U256::from(0xff)),
142            ))
143        }
144    }
145}
146
147/// Returns the `byte_word_dynamic` EVM semantics helper result.
148pub(crate) fn byte_word_dynamic(index: SymWord, word: SymWord) -> SymWord {
149    if let SymWord::Concrete(index) = index {
150        return byte_word(index, word);
151    }
152
153    let index = index.into_expr();
154    let mut result = Expr::Const(U256::ZERO);
155    for idx in (0..32).rev() {
156        result = Expr::Ite(
157            Box::new(BoolExpr::eq(index.clone(), Expr::Const(U256::from(idx)))),
158            Box::new(byte_word(U256::from(idx), word.clone()).into_expr()),
159            Box::new(result),
160        );
161    }
162    SymWord::Expr(result)
163}
164
165/// Returns the `expr_known_byte` EVM semantics helper result.
166pub(crate) fn expr_known_byte(expr: &Expr, index: usize) -> Option<u8> {
167    debug_assert!(index < 32);
168    match expr {
169        Expr::Const(value) => Some(value.to_be_bytes::<32>()[index]),
170        Expr::Var(_) | Expr::GasLeft(_) | Expr::Keccak { .. } | Expr::Hash { .. } => None,
171        Expr::Not(value) => expr_known_byte(value, index).map(|byte| !byte),
172        Expr::Ite(_, then_expr, else_expr) => {
173            let then_byte = expr_known_byte(then_expr, index)?;
174            let else_byte = expr_known_byte(else_expr, index)?;
175            (then_byte == else_byte).then_some(then_byte)
176        }
177        Expr::Op(op, left, right) => match op {
178            ExprOp::And => match (expr_known_byte(left, index), expr_known_byte(right, index)) {
179                (Some(left), Some(right)) => Some(left & right),
180                (Some(0), _) | (_, Some(0)) => Some(0),
181                _ => None,
182            },
183            ExprOp::Or => Some(expr_known_byte(left, index)? | expr_known_byte(right, index)?),
184            ExprOp::Xor => Some(expr_known_byte(left, index)? ^ expr_known_byte(right, index)?),
185            ExprOp::Shl => {
186                let Expr::Const(shift) = right.as_ref() else { return None };
187                if *shift >= U256::from(256) {
188                    return Some(0);
189                }
190                let shift = shift.to::<usize>();
191                if shift % 8 != 0 {
192                    return None;
193                }
194                let source_index = index + shift / 8;
195                if source_index >= 32 { Some(0) } else { expr_known_byte(left, source_index) }
196            }
197            ExprOp::Shr => {
198                let Expr::Const(shift) = right.as_ref() else { return None };
199                if *shift >= U256::from(256) {
200                    return Some(0);
201                }
202                let shift = shift.to::<usize>();
203                if shift % 8 != 0 {
204                    return None;
205                }
206                let byte_shift = shift / 8;
207                if index < byte_shift { Some(0) } else { expr_known_byte(left, index - byte_shift) }
208            }
209            ExprOp::Add
210            | ExprOp::Sub
211            | ExprOp::Mul
212            | ExprOp::UDiv
213            | ExprOp::URem
214            | ExprOp::SDiv
215            | ExprOp::SRem
216            | ExprOp::Sar => None,
217        },
218    }
219}
220
221/// Returns the `expr_known_word` EVM semantics helper result.
222pub(crate) fn expr_known_word(expr: &Expr) -> Option<U256> {
223    let mut bytes = [0u8; 32];
224    for (idx, byte) in bytes.iter_mut().enumerate() {
225        *byte = expr_known_byte(expr, idx)?;
226    }
227    Some(U256::from_be_bytes(bytes))
228}
229
230/// Implements the `sar` EVM semantics helper.
231pub(crate) fn sar(value: U256, shift: usize) -> U256 {
232    if shift >= 256 {
233        if (value >> 255) == U256::from(1) { U256::MAX } else { U256::ZERO }
234    } else if shift == 0 {
235        value
236    } else if (value >> 255) == U256::from(1) {
237        (value >> shift) | (U256::MAX << (256 - shift))
238    } else {
239        value >> shift
240    }
241}
242
243/// Computes the `shift_left` EVM semantics helper result.
244pub(crate) fn shift_left(value: SymWord, bits: usize) -> SymWord {
245    match value {
246        SymWord::Concrete(value) => SymWord::Concrete(value << bits),
247        value => {
248            SymWord::Expr(Expr::op(ExprOp::Shl, value.into_expr(), Expr::Const(U256::from(bits))))
249        }
250    }
251}
252
253/// Computes the `analyze_jumpdests` EVM semantics helper result.
254pub(crate) fn analyze_jumpdests(code: &SymCode) -> BTreeSet<usize> {
255    let mut jumpdests = BTreeSet::new();
256    let mut pc = 0;
257    while pc < code.len() {
258        let op = code.analysis_opcode(pc).unwrap_or(opcode::STOP);
259        if op == opcode::JUMPDEST {
260            jumpdests.insert(pc);
261            pc += 1;
262        } else if (opcode::PUSH1..=opcode::PUSH32).contains(&op) {
263            pc += 1 + (op - opcode::PUSH1 + 1) as usize;
264        } else {
265            pc += 1;
266        }
267    }
268    jumpdests
269}
270
271/// Computes the `ensure_jumpdest` EVM semantics helper result.
272pub(crate) fn ensure_jumpdest(
273    dest: usize,
274    jumpdests: &BTreeSet<usize>,
275) -> Result<(), SymbolicError> {
276    if jumpdests.contains(&dest) { Ok(()) } else { Err(SymbolicError::InvalidJump(dest)) }
277}
278
279/// Returns whether `is_assertion_revert` holds.
280pub(crate) fn is_assertion_revert(data: &[u8]) -> bool {
281    is_assert_panic(data) || is_revert_assertion_failure(data)
282}
283
284/// Returns whether `is_assert_panic` holds.
285pub(crate) fn is_assert_panic(data: &[u8]) -> bool {
286    data.len() >= ABI_SELECTOR_PLUS_WORD_LEN
287        && data.starts_with(&PANIC_SELECTOR)
288        && abi_word(&data[4..ABI_SELECTOR_PLUS_WORD_LEN])
289            .is_some_and(|code| code == ASSERT_PANIC_CODE)
290}
291
292/// Returns whether `is_revert_assertion_failure` holds.
293pub(crate) fn is_revert_assertion_failure(data: &[u8]) -> bool {
294    if data.len() < ERROR_DATA_MIN_LEN || !data.starts_with(&ERROR_SELECTOR) {
295        return false;
296    }
297
298    let Some(offset) = abi_word_usize(&data[4..ABI_SELECTOR_PLUS_WORD_LEN]) else {
299        return false;
300    };
301    let Some(length_offset) = 4usize.checked_add(offset) else {
302        return false;
303    };
304    let Some(length_end) = length_offset.checked_add(32) else {
305        return false;
306    };
307    if length_end > data.len() {
308        return false;
309    }
310
311    let Some(length) = abi_word_usize(&data[length_offset..length_end]) else {
312        return false;
313    };
314    let Some(message_end) = length_end.checked_add(length) else {
315        return false;
316    };
317    if message_end > data.len() {
318        return false;
319    }
320
321    std::str::from_utf8(&data[length_end..message_end])
322        .is_ok_and(|message| message.contains(ASSERTION_FAILED_PREFIX))
323}
324
325/// Returns the `abi_word_usize` EVM semantics helper result.
326pub(crate) fn abi_word_usize(word: &[u8]) -> Option<usize> {
327    let value = abi_word(word)?;
328    if value > U256::from(usize::MAX) { None } else { Some(value.to::<usize>()) }
329}
330
331/// Returns the `abi_word` EVM semantics helper result.
332pub(crate) const fn abi_word(word: &[u8]) -> Option<U256> {
333    if word.len() != 32 {
334        return None;
335    }
336    let mut bytes = [0u8; 32];
337    bytes.copy_from_slice(word);
338    Some(U256::from_be_bytes(bytes))
339}
foundry_evm_symbolic/runtime/evm.rs

foundry_evm_symbolic/runtime/
evm.rs
