Skip to content

Commit

Permalink
Merge pull request #121 from leonardoalt/refactor_for_eval
Browse files Browse the repository at this point in the history 
Refactor function call to prepare for evaluator.
  • Loading branch information
@chriseth
chriseth authored Nov 1, 2022
2 parents cde2f6e + 3c2c2b1 commit 03946ad
Show file tree
Hide file tree
Showing 5 changed files with 20 additions and 46 deletions.
39 changes: 11 additions & 28 deletions src/encoder.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -85,14 +85,6 @@ fn encode_with_counterexamples<T: Instructions>(
)
}

#[derive(Debug, PartialEq, Eq)]
pub struct FunctionVariables {
/// smtlib2 names of the initial values of the function parameters
pub parameters: Vec<SMTVariable>,
/// smtlib2 names of the final values of the function return variables
pub returns: Vec<SMTVariable>,
}

#[derive(Default)]
struct FunctionDefinitionCollector {
function_definitions: BTreeMap<u64, yul::FunctionDefinition>,
Expand Down Expand Up @@ -130,24 +122,24 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {

/// Encodes the given function, potentially re-creating copies of all local variables
/// if called multiple times.
/// @returns the names of the function parameters and return variables.
pub fn encode_function(&mut self, function: &FunctionDefinition) -> FunctionVariables {
for param in &function.parameters {
/// @returns the names of the return variables.
pub fn encode_function(
&mut self,
function: &FunctionDefinition,
arguments: &[SMTVariable],
) -> Vec<SMTVariable> {
assert_eq!(function.parameters.len(), arguments.len());
for (param, arg) in function.parameters.iter().zip(arguments) {
let var = self.ssa_tracker.introduce_variable(param);
self.out(smt::declare_const(var))
self.out(smt::define_const(var, smt::SMTExpr::from(arg.clone())))
}
let parameters = self.ssa_tracker.to_smt_variables(&function.parameters);
self.encode_variable_declaration(&VariableDeclaration {
variables: function.returns.clone(),
value: None,
location: None,
});
self.encode_block(&function.body);
let returns = self.ssa_tracker.to_smt_variables(&function.returns);
FunctionVariables {
parameters,
returns,
}
self.ssa_tracker.to_smt_variables(&function.returns)
}

fn encode_variable_declaration(&mut self, var: &VariableDeclaration) {
Expand Down Expand Up @@ -179,16 +171,13 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
.for_each(|st| self.encode_statement(st));
}

fn encode_function_def(&mut self, _fun: &yul::FunctionDefinition) {}

fn encode_statement(&mut self, st: &yul::Statement) {
match st {
yul::Statement::VariableDeclaration(var_decl) => {
self.encode_variable_declaration(var_decl)
}
yul::Statement::Assignment(assignment) => self.encode_assignment(assignment),
yul::Statement::Block(block) => self.encode_block(block),
yul::Statement::FunctionDefinition(fun) => self.encode_function_def(fun),
yul::Statement::If(if_st) => self.encode_if(if_st),
yul::Statement::Switch(switch) => self.encode_switch(switch),
yul::Statement::ForLoop(for_loop) => self.encode_for(for_loop),
Expand Down Expand Up @@ -342,13 +331,7 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
}
IdentifierID::Reference(id) => {
let fun_def = self.function_definitions[&id].clone();
let function_vars = self.encode_function(&fun_def);
assert!(arguments.len() == function_vars.parameters.len());
arguments
.into_iter()
.zip(function_vars.parameters)
.for_each(|(arg, param)| self.out(smt::assert(smt::eq(arg, param))));
function_vars.returns
self.encode_function(&fun_def, &arguments)
}
_ => panic!(
"Unexpected reference in function call: {:?}",
Expand Down
3 changes: 1 addition & 2 deletions tests/assert_pass/function_call_1.yul.smt2
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,11 +27,10 @@
(assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff))
(define-const _1 (_ BitVec 256) _address_2048_0)
(define-const x_5_1 (_ BitVec 256) _1)
(declare-const a_3_0 (_ BitVec 256))
(define-const a_3_0 (_ BitVec 256) x_5_1)
(define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000)
(define-const b_4_1 (_ BitVec 256) _2)
(define-const b_4_2 (_ BitVec 256) a_3_0)
(assert (= x_5_1 a_3_0))
(define-const _3 (_ BitVec 256) (ite (= x_5_1 b_4_2) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000000000))
(assert (and (and (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) true (= _3 #x0000000000000000000000000000000000000000000000000000000000000000)))
(assert (not (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000)))
6 changes: 2 additions & 4 deletions tests/assert_pass/function_call_add_1.yul.smt2
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,8 +29,8 @@
(define-const x_6_1 (_ BitVec 256) _1)
(define-const _2 (_ BitVec 256) _address_2048_0)
(define-const y_7_1 (_ BitVec 256) _2)
(declare-const a_3_0 (_ BitVec 256))
(declare-const b_4_0 (_ BitVec 256))
(define-const a_3_0 (_ BitVec 256) x_6_1)
(define-const b_4_0 (_ BitVec 256) y_7_1)
(define-const _3 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000)
(define-const c_5_1 (_ BitVec 256) _3)
(define-const _4 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000064)
Expand All @@ -55,8 +55,6 @@
(define-const _revert_data_32_2072_4 (_ BitVec 256) (ite (= _9 #x0000000000000000000000000000000000000000000000000000000000000000) _revert_data_32_2072_2 _revert_data_32_2072_3))
(define-const _12 (_ BitVec 256) (bvadd a_3_0 b_4_0))
(define-const c_5_2 (_ BitVec 256) _12)
(assert (= x_6_1 a_3_0))
(assert (= y_7_1 b_4_0))
(define-const _13 (_ BitVec 256) (ite (bvugt x_6_1 c_5_2) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000000000))
(define-const _14 (_ BitVec 256) (ite (= _13 #x0000000000000000000000000000000000000000000000000000000000000000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000000000))
(assert (and (and (= _revert_flag_2070_4 #x0000000000000000000000000000000000000000000000000000000000000000) (= _stop_flag_2069_0 #x0000000000000000000000000000000000000000000000000000000000000000)) true (= _14 #x0000000000000000000000000000000000000000000000000000000000000000)))
Expand Down
6 changes: 2 additions & 4 deletions tests/syntax/function_call_1.yul.smt2
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,15 +26,13 @@
(assert (= ((_ extract 255 160) _address_2048_0) #x000000000000000000000000))
(assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff))
(define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000002)
(declare-const a_3_0 (_ BitVec 256))
(define-const a_3_0 (_ BitVec 256) _1)
(define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000)
(define-const b_4_1 (_ BitVec 256) _2)
(define-const b_4_2 (_ BitVec 256) a_3_0)
(assert (= _1 a_3_0))
(declare-const a_3_1 (_ BitVec 256))
(define-const a_3_1 (_ BitVec 256) b_4_2)
(define-const _3 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000)
(define-const b_4_4 (_ BitVec 256) _3)
(define-const b_4_5 (_ BitVec 256) a_3_1)
(assert (= b_4_2 a_3_1))
(define-const x_5_1 (_ BitVec 256) b_4_5)
(assert (not (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000)))
12 changes: 4 additions & 8 deletions tests/syntax/function_call_2.yul.smt2
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,26 +27,22 @@
(assert (bvule _calldatasize_2050_0 #x000000000000000000000000000000000000000000000000ffffffffffffffff))
(define-const _1 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000001)
(define-const _2 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000002)
(declare-const a_3_0 (_ BitVec 256))
(declare-const b_4_0 (_ BitVec 256))
(define-const a_3_0 (_ BitVec 256) _1)
(define-const b_4_0 (_ BitVec 256) _2)
(define-const _3 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000)
(define-const c_5_1 (_ BitVec 256) _3)
(define-const d_6_1 (_ BitVec 256) _3)
(define-const c_5_2 (_ BitVec 256) a_3_0)
(define-const d_6_2 (_ BitVec 256) b_4_0)
(assert (= _1 a_3_0))
(assert (= _2 b_4_0))
(define-const x_7_1 (_ BitVec 256) c_5_2)
(define-const y_8_1 (_ BitVec 256) d_6_2)
(declare-const a_3_1 (_ BitVec 256))
(declare-const b_4_1 (_ BitVec 256))
(define-const a_3_1 (_ BitVec 256) x_7_1)
(define-const b_4_1 (_ BitVec 256) y_8_1)
(define-const _4 (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000)
(define-const c_5_4 (_ BitVec 256) _4)
(define-const d_6_4 (_ BitVec 256) _4)
(define-const c_5_5 (_ BitVec 256) a_3_1)
(define-const d_6_5 (_ BitVec 256) b_4_1)
(assert (= x_7_1 a_3_1))
(assert (= y_8_1 b_4_1))
(define-const t_9_1 (_ BitVec 256) c_5_5)
(define-const s_10_1 (_ BitVec 256) d_6_5)
(assert (not (= _revert_flag_2070_0 #x0000000000000000000000000000000000000000000000000000000000000000)))

0 comments on commit 03946ad

Please sign in to comment.