diff --git a/src/instruction/mod.rs b/src/instruction/mod.rs index 79eb993..1c96746 100644 --- a/src/instruction/mod.rs +++ b/src/instruction/mod.rs @@ -648,7 +648,18 @@ impl<'ctx> MachineInstruction<'ctx, 32> for Instruction { storage: None, } } - Instruction::Address => todo!(), + Instruction::Address => { + let addr = mach.address.as_ref(); + let addr = addr.zero_ext(12 * 8); + MachineRecord { + stack: Some(StackChange::with_ops(vec![StackOp::Push(addr.into())])), + mem: None, + pc: (mach.pc(), mach.pc() + self.byte_size()), + constraints: None, + halt: false, + storage: None, + } + }, Instruction::Balance => { let stack = mach.stack(); let addr = stack.peek().unwrap(); @@ -1082,7 +1093,19 @@ impl<'ctx> MachineInstruction<'ctx, 32> for Instruction { constraints: None, } } - Instruction::Gas => todo!(), + Instruction::Gas => { + let gas_arg: BitVec<256> = random_bv_arg(); + let gas = gas().apply(&[gas_arg.as_ref()]).as_bv().unwrap(); + MachineRecord { + stack: Some(StackChange::with_ops(vec![StackOp::Push(gas.into())])), + pc: (mach.pc(), mach.pc() + self.byte_size()), + mem: None, + halt: false, + storage: None, + constraints: None, + } + + }, Instruction::JumpDest => MachineRecord { stack: None, pc: (mach.pc(), mach.pc() + self.byte_size()), diff --git a/src/state/env.rs b/src/state/env.rs index 364ae3f..21bad1f 100644 --- a/src/state/env.rs +++ b/src/state/env.rs @@ -1,11 +1,49 @@ +use std::collections::HashMap; + use z3_ext::ast::{Array, Ast, AstKind, BV}; use z3_ext::FuncDecl; use z3_ext::Sort; +use crate::parser::Program; use crate::random_bv_arg; use crate::smt::{ctx, BitVec}; - +use crate::storage::Address; + +#[derive(Debug, Clone)] +pub struct ExecutionEnv { + code: HashMap
>, + block: Block, + tx: TransactionContext, + result: Option