Add gas opcode, begin support for configurable execution ctx

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()),

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<Address, Option<Program>>,
+    block: Block,
+    tx: TransactionContext,
+    result: Option<EvmResult>
+}
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum EvmResult {
+    Failed {
+        msg: String
+    },
+    Success {
+        ret_val: BitVec<32>
+    }
+}
+#[derive(Debug, Clone)]
+pub struct TransactionContext {
+    calldata: Option<Vec<BitVec<1>>>,
+    caller: Option<Address>,
+    callvalue: Option<BitVec<32>>,
+}
+
+#[derive(Debug, Clone)]
+pub struct Block {
+    base_fee: Option<BitVec<32>>,
+    chain_id: Option<BitVec<32>>,
+    coinbase: Option<Address>,
+    difficulty: Option<BitVec<32>>,
+    gaslimit: Option<BitVec<32>>,
+    number: Option<BitVec<32>>,
+    timestamp: Option<BitVec<32>>
+}
 /**
     Note: Some of these functions in EVM have no arguments.
     The reason they are passed an argument here is because a zero argument function is

src/state/evm.rs

@@ -23,6 +23,7 @@ pub struct EvmState {
     pub halt: bool,
 }
 
+
 impl MachineComponent for EvmState {
     type Record = MachineRecord<32>;