Display reachable reverts.

Cargo.toml

@@ -11,3 +11,5 @@ num-bigint = "^0.4.3"
 tempfile = "3"
 clap = "^3.2"
 num-traits = "^0.2.15"
+colored = "^2"
+codespan-reporting = "^0.11.1"

src/encoder.rs

@@ -1,4 +1,5 @@
 use crate::evm_context;
+use crate::execution_position::ExecutionPositionManager;
 use crate::smt::{self, SMTExpr, SMTFormat, SMTSort, SMTStatement, SMTVariable};
 use crate::ssa_tracker::SSATracker;
 
@@ -29,6 +30,7 @@ pub struct Encoder<InstructionsType> {
     interpreter: InstructionsType,
     loop_unroll: u64,
     path_conditions: Vec<SMTExpr>,
+    execution_position: ExecutionPositionManager,
 }
 
 pub fn encode<T: Instructions>(ast: &Block, loop_unroll: u64) -> String {
@@ -51,23 +53,27 @@ pub fn encode_revert_reachable<T: Instructions>(
     encoder.encode(ast, loop_unroll);
     encoder.encode_revert_reachable();
 
-    encode_with_counterexamples(encoder, counterexamples)
+    encode_with_counterexamples(&mut encoder, counterexamples)
 }
 
 pub fn encode_solc_panic_reachable<T: Instructions>(
     ast: &Block,
     loop_unroll: u64,
     counterexamples: &[Expression],
-) -> (String, Vec<String>) {
+) -> (String, Vec<String>, String, ExecutionPositionManager) {
     let mut encoder = Encoder::<T>::default();
     encoder.encode(ast, loop_unroll);
     encoder.encode_solc_panic_reachable();
+    let revert_position = ExecutionPositionManager::smt_variable()
+        .smt_var(&mut encoder.ssa_tracker)
+        .as_smt();
 
-    encode_with_counterexamples(encoder, counterexamples)
+    let (enc, cex) = encode_with_counterexamples(&mut encoder, counterexamples);
+    (enc, cex, revert_position, encoder.execution_position)
 }
 
 fn encode_with_counterexamples<T: Instructions>(
-    mut encoder: Encoder<T>,
+    encoder: &mut Encoder<T>,
     counterexamples: &[Expression],
 ) -> (String, Vec<String>) {
     let encoded_counterexamples = counterexamples
@@ -110,7 +116,8 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
     }
 
     fn encode_context_init(&mut self) {
-        let output = evm_context::init(&mut self.ssa_tracker);
+        let mut output = evm_context::init(&mut self.ssa_tracker);
+        output.push(ExecutionPositionManager::init(&mut self.ssa_tracker));
         self.out_vec(output);
     }
 
@@ -138,6 +145,7 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
             value: None,
             location: None,
         });
+
         self.encode_block(&function.body);
         self.ssa_tracker.to_smt_variables(&function.returns)
     }
@@ -312,7 +320,23 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
             .rev()
             .collect();
 
-        match call.function.id {
+        let record_location = match call.function.id {
+            IdentifierID::Reference(_) => true,
+            IdentifierID::BuiltinReference => call.function.name == "revert", // TODO more flexibility about which builtins to record.
+            _ => false,
+        };
+
+        if record_location {
+            self.execution_position.function_called(call);
+            let record_pos = evm_context::assign_variable_if_executing_regularly(
+                &mut self.ssa_tracker,
+                &ExecutionPositionManager::smt_variable(),
+                self.execution_position.position_id().into(),
+            );
+            self.out(record_pos);
+        }
+
+        let return_vars = match call.function.id {
             IdentifierID::BuiltinReference => {
                 let builtin = &InstructionsType::builtin(&call.function.name).unwrap();
                 let return_vars: Vec<SMTVariable> = (0..builtin.returns)
@@ -337,7 +361,18 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
                 "Unexpected reference in function call: {:?}",
                 call.function.id
             ),
+        };
+
+        if record_location {
+            self.execution_position.function_returned();
+            let record_pos = evm_context::assign_variable_if_executing_regularly(
+                &mut self.ssa_tracker,
+                &ExecutionPositionManager::smt_variable(),
+                self.execution_position.position_id().into(),
+            );
+            self.out(record_pos);
         }
+        return_vars
     }
 }
 

src/evm_context.rs

@@ -90,7 +90,7 @@ context_variables! {
     stop_flag: Type::Default; Some(0.into()),
     revert_flag: Type::Default; Some(0.into()),
     revert_sig_4: Type::Constant(smt::bv(32)); None,
-    revert_data_32: Type::Constant(smt::bv(256)); None
+    revert_data_32: Type::Default; None
 }
 
 // TODO can we make this a global variable?
@@ -422,7 +422,7 @@ pub fn encode_solc_panic_reachable(ssa: &mut SSATracker) -> SMTStatement {
 
 /// Assigns to the variable if we neither stopped nor reverted. Otherwise, the variable keeps
 /// its value. Increases the SSA index in any case.
-fn assign_variable_if_executing_regularly(
+pub fn assign_variable_if_executing_regularly(
     ssa: &mut SSATracker,
     variable: &SystemVariable,
     new_value: SMTExpr,

src/execution_position.rs

@@ -0,0 +1,80 @@
+use yultsur::yul::{FunctionCall, Identifier, IdentifierID, SourceLocation};
+
+use crate::smt::{self, SMTExpr};
+use crate::ssa_tracker::SSATracker;
+use crate::variables::SystemVariable;
+
+/**
+ * Stores the current call stack encoded in a single number that can be used
+ * during the SMT encoding.
+ *
+ * Can be extended in the future with other information like loop iterations.
+ */
+#[derive(Default)]
+pub struct ExecutionPositionManager {
+    positions: Vec<ExecutionPosition>,
+}
+
+pub struct PositionID(pub usize);
+
+impl From<PositionID> for SMTExpr {
+    fn from(pos: PositionID) -> Self {
+        (pos.0 as u64).into()
+    }
+}
+
+struct ExecutionPosition {
+    call_stack: Vec<Option<SourceLocation>>,
+}
+
+impl ExecutionPositionManager {
+    pub fn init(ssa_tracker: &mut SSATracker) -> smt::SMTStatement {
+        Self::smt_variable().generate_definition(ssa_tracker)
+    }
+
+    /// @returns the SystemVariable that encodes the position.
+    pub fn smt_variable() -> SystemVariable {
+        SystemVariable {
+            identifier: Identifier {
+                id: IdentifierID::Reference(8128),
+                name: "_exe_pos".to_string(),
+                location: None,
+            },
+            domain: vec![],
+            codomain: smt::bv(256),
+            default_value: Some(0.into()),
+        }
+    }
+
+    pub fn function_called(&mut self, fun: &FunctionCall) {
+        self.append_position(ExecutionPosition {
+            call_stack: [self.current_call_stack(), vec![fun.location.clone()]].concat(),
+        });
+    }
+
+    pub fn function_returned(&mut self) {
+        let mut call_stack = self.current_call_stack();
+        call_stack.pop().unwrap();
+        self.append_position(ExecutionPosition { call_stack })
+    }
+
+    /// Returns the current position ID that can later
+    /// be translated into e.g. a call stack.
+    pub fn position_id(&self) -> PositionID {
+        PositionID(self.positions.len() - 1)
+    }
+
+    pub fn call_stack_at_position(&self, pos: PositionID) -> &Vec<Option<SourceLocation>> {
+        &self.positions[pos.0].call_stack
+    }
+
+    fn append_position(&mut self, pos: ExecutionPosition) {
+        self.positions.push(pos)
+    }
+    fn current_call_stack(&self) -> Vec<Option<SourceLocation>> {
+        match self.positions.iter().last() {
+            Some(p) => p.call_stack.clone(),
+            None => vec![],
+        }
+    }
+}

src/lib.rs

@@ -2,6 +2,7 @@ pub mod cfg;
 pub mod encoder;
 pub mod evm_builtins;
 pub mod evm_context;
+pub mod execution_position;
 pub mod sexpr;
 pub mod smt;
 pub mod solver;