feat: add symbolic stack backend path#85
Conversation
# Conflicts: # Cargo.lock # Cargo.toml # crates/jet_ir/src/types.rs
Add symbolic block-state handling for static jumps and joins, share non-jump opcode dispatch between stack backends, and document the current lowering model. Also add targeted JUMPI join tests and jumpdest indexing so symbolic target lookup stays explicit and cheap.
Lower symbolic dynamic JUMP and taken JUMPI through site-local switches over known JUMPDEST targets, carrying the post-pop symbolic stack to each conservative successor. Add ROM coverage for computed JUMP and JUMPI targets in both runtime and symbolic modes, and update the symbolic stack design note.
![gemini-code-assist[bot]](https://avatars.githubusercontent.com/in/956858?s=60&v=4){kind=small}
There was a problem hiding this comment.
Code Review
This pull request introduces a symbolic stack lowering path to the Jet EVM JIT compiler, enabling compile-time tracking of stack values and more efficient IR generation. It refactors opcode implementations to use a generic StackBackend trait, supporting both runtime and symbolic modes, and upgrades the project to LLVM 22. A new jetdbg CLI tool is also included for contract debugging. Review feedback identifies a bug in the symbolic handling of PUSH data where bytes are incorrectly reversed, and recommends using safe Inkwell methods to replace unnecessary unsafe blocks in the stack backend implementation.
| IterItem::PushData(_, _, data) => { | ||
| let mut new_data = [0u8; 32]; | ||
| new_data[..data.len()].copy_from_slice(data); | ||
| new_data[..data.len()].reverse(); |
There was a problem hiding this comment.
The reverse() call here appears to be a bug. According to the architecture documentation and the instructions::Iter implementation, PUSH data is already converted to little-endian (bytes reversed) by the iterator. Since ops::push expects little-endian bytes to construct its i256 limbs, reversing them again here will turn them back into big-endian, leading to incorrect values for multi-byte PUSH opcodes.
ops::push(bctx, new_data)?;| let loaded = bctx | ||
| .builder | ||
| .build_load(bctx.env.types().i256, ptr, "load_int")?; | ||
| let word = unsafe { IntValue::new(loaded.as_value_ref()) }; |
There was a problem hiding this comment.
The use of unsafe and as_value_ref() here is unnecessary. Since loaded is a BasicValueEnum resulting from an i256 load, you can use the safe into_int_value() method provided by Inkwell.
| let word = unsafe { IntValue::new(loaded.as_value_ref()) }; | |
| let word = loaded.into_int_value(); |
| &[bctx.registers.exec_ctx.into(), index_value.into()], | ||
| "stack_peek_word_result", | ||
| )?; | ||
| let ptr = unsafe { PointerValue::new(ret.as_value_ref()) }; |
There was a problem hiding this comment.
The use of unsafe and as_value_ref() can be avoided here by using into_pointer_value() on the result of the peek call.
| let ptr = unsafe { PointerValue::new(ret.as_value_ref()) }; | |
| let ptr = ret.try_as_basic_value().left().unwrap().into_pointer_value(); |
Build symbolic-mode control flow from a fixed-point abstract stack pass before IR emission. Pre-create entry phis for planned block variants, specialize bytecode blocks by incoming stack height, and lower dynamic jumps through variants without falling back to runtime stack traffic. Preserve known-u64 metadata through symbolic DUP so planned static jump edges and emitted symbolic state agree. Add ROM coverage for backward-only targets, duplicate-carried jump targets, and differing-height joins.
1 participant
Summary
Verification