Display reachable reverts.

Author: chriseth

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;
 
@@ -17,6 +18,7 @@ pub trait Instructions: Default + Dialect {
         return_vars: &[SMTVariable],
         ssa: &mut SSATracker,
         path_conditions: &[SMTExpr],
+        location: &Option<SourceLocation>,
     ) -> Vec<SMTStatement>;
 }
 
@@ -29,6 +31,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 +54,43 @@ 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 struct PanicInfo {
+    pub revert_start: String,
+    pub revert_end: String,
+    pub revert_position: String,
 }
 
 pub fn encode_solc_panic_reachable<T: Instructions>(
     ast: &Block,
     loop_unroll: u64,
     counterexamples: &[Expression],
-) -> (String, Vec<String>) {
+) -> (String, Vec<String>, PanicInfo, ExecutionPositionManager) {
     let mut encoder = Encoder::<T>::default();
     encoder.encode(ast, loop_unroll);
     encoder.encode_solc_panic_reachable();
+    let (revert_start, revert_end) = evm_context::revert_location(&mut encoder.ssa_tracker);
+    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,
+        PanicInfo {
+            revert_start: revert_start.as_smt(),
+            revert_end: revert_end.as_smt(),
+            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 +133,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 +162,7 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
             value: None,
             location: None,
         });
+
         self.encode_block(&function.body);
         self.ssa_tracker.to_smt_variables(&function.returns)
     }
@@ -281,7 +306,26 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
         match expr {
             Expression::Literal(literal) => vec![self.encode_literal(literal)],
             Expression::Identifier(identifier) => vec![self.encode_identifier(identifier)],
-            Expression::FunctionCall(function) => self.encode_function_call(function),
+            Expression::FunctionCall(function) => {
+                self.execution_position.function_called(function);
+                let pos_pre = evm_context::assign_variable_if_executing_regularly(
+                    &mut self.ssa_tracker,
+                    &ExecutionPositionManager::smt_variable(),
+                    self.execution_position.position_id().into(),
+                );
+                self.out(pos_pre);
+
+                let fun_call = self.encode_function_call(function);
+
+                self.execution_position.function_returned();
+                let pos_post = evm_context::assign_variable_if_executing_regularly(
+                    &mut self.ssa_tracker,
+                    &ExecutionPositionManager::smt_variable(),
+                    self.execution_position.position_id().into(),
+                );
+                self.out(pos_post);
+                fun_call
+            }
         }
     }
 
@@ -325,6 +369,7 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
                     &return_vars,
                     &mut self.ssa_tracker,
                     &self.path_conditions,
+                    &call.location,
                 );
                 self.out_vec(result);
                 return_vars

src/evm_builtins.rs

@@ -4,6 +4,7 @@ use crate::evm_context::MemoryRange;
 use crate::smt::{self, SMTExpr, SMTOp, SMTStatement, SMTVariable};
 use crate::ssa_tracker::SSATracker;
 use yultsur::dialect::{Builtin, Dialect, EVMDialect};
+use yultsur::yul::SourceLocation;
 
 #[derive(Default)]
 pub struct EVMInstructions;
@@ -22,6 +23,7 @@ impl Instructions for EVMInstructions {
         return_vars: &[SMTVariable],
         ssa: &mut SSATracker,
         _path_conditions: &[SMTExpr],
+        location: &Option<SourceLocation>,
     ) -> Vec<SMTStatement> {
         let single_return = |value: SMTExpr| {
             assert_eq!(return_vars.len(), 1);
@@ -192,6 +194,9 @@ impl Instructions for EVMInstructions {
                     length: arg_1.unwrap().into(),
                 },
                 ssa,
+                location
+                    .to_owned()
+                    .unwrap_or(SourceLocation { start: 0, end: 0 }),
             ),
             "invalid" => panic!("Builtin {} not implemented", builtin.name), // TODO
             "selfdestruct" => panic!("Builtin {} not implemented", builtin.name), // TODO

src/evm_context.rs

@@ -90,7 +90,9 @@ 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,
+    revert_source_location_start: Type::Default; None,
+    revert_source_location_end: Type::Default; None
 }
 
 // TODO can we make this a global variable?
@@ -112,7 +114,11 @@ impl MemoryRange {
     }
 }
 
-pub fn revert(input: MemoryRange, ssa: &mut SSATracker) -> Vec<SMTStatement> {
+pub fn revert(
+    input: MemoryRange,
+    ssa: &mut SSATracker,
+    location: SourceLocation,
+) -> Vec<SMTStatement> {
     let sig = smt::ite(
         smt::bvuge(input.length.clone(), 4),
         mload4(input.offset.clone(), ssa),
@@ -126,12 +132,29 @@ pub fn revert(input: MemoryRange, ssa: &mut SSATracker) -> Vec<SMTStatement> {
     vec![
         assign_variable_if_executing_regularly(ssa, &context().revert_sig_4, sig),
         assign_variable_if_executing_regularly(ssa, &context().revert_data_32, data),
+        assign_variable_if_executing_regularly(
+            ssa,
+            &context().revert_source_location_start,
+            (location.start as u64).into(),
+        ),
+        assign_variable_if_executing_regularly(
+            ssa,
+            &context().revert_source_location_end,
+            (location.end as u64).into(),
+        ),
         // The order here is important: revert_flag is used to build the two expressions above,
         // so we can only change it after.
         assign_variable_if_executing_regularly(ssa, &context().revert_flag, 1.into()),
     ]
 }
 
+pub fn revert_location(ssa: &mut SSATracker) -> (SMTVariable, SMTVariable) {
+    (
+        context().revert_source_location_start.smt_var(ssa),
+        context().revert_source_location_end.smt_var(ssa),
+    )
+}
+
 pub fn set_stopped(ssa: &mut SSATracker) -> SMTStatement {
     assign_variable_if_executing_regularly(ssa, &context().stop_flag, 1.into())
 }
@@ -422,7 +445,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,79 @@
+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())
+    }
+
+    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;