Skip to content

Commit ee1b8d1

Browse files
chrisethchriseth
committed
Concrete evaluator.
1 parent be04d08 commit ee1b8d1

7 files changed

+1159
-33
lines changed

‎src/encoder.rs

+91-17
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,8 @@
1-
use crate::evm_context;
1+
use crate::evaluator::Evaluator;
22
use crate::execution_position::ExecutionPositionManager;
3-
use crate::smt::{self, SMTExpr, SMTFormat, SMTSort, SMTStatement, SMTVariable};
3+
use crate::smt::{SMTExpr, SMTFormat, SMTSort, SMTStatement, SMTVariable};
44
use crate::ssa_tracker::SSATracker;
5+
use crate::{evm_context, smt};
56

67
use yultsur::dialect::{Builtin, Dialect};
78
use yultsur::visitor::ASTVisitor;
@@ -28,6 +29,7 @@ pub struct Encoder<InstructionsType> {
2829
ssa_tracker: SSATracker,
2930
output: Vec<SMTStatement>,
3031
interpreter: InstructionsType,
32+
evaluator: Evaluator,
3133
loop_unroll: u64,
3234
path_conditions: Vec<SMTExpr>,
3335
execution_position: ExecutionPositionManager,
@@ -56,6 +58,25 @@ pub fn encode_revert_reachable<T: Instructions>(
5658
encode_with_counterexamples(&mut encoder, counterexamples)
5759
}
5860

61+
pub fn encode_with_evaluator<T: Instructions>(
62+
ast: &Block,
63+
loop_unroll: u64,
64+
evaluator: Evaluator,
65+
) -> (String, Evaluator) {
66+
let mut encoder = Encoder::<T> {
67+
evaluator,
68+
..Default::default()
69+
};
70+
encoder.encode(ast, loop_unroll);
71+
let query = encoder
72+
.output
73+
.iter()
74+
.map(|s| s.as_smt())
75+
.collect::<Vec<_>>()
76+
.join("\n");
77+
(query, std::mem::take(&mut encoder.evaluator))
78+
}
79+
5980
pub fn encode_solc_panic_reachable<T: Instructions>(
6081
ast: &Block,
6182
loop_unroll: u64,
@@ -133,13 +154,16 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
133154
pub fn encode_function(
134155
&mut self,
135156
function: &FunctionDefinition,
136-
arguments: &[SMTVariable],
157+
arguments: &Vec<SMTVariable>,
137158
) -> Vec<SMTVariable> {
138159
assert_eq!(function.parameters.len(), arguments.len());
139160
for (param, arg) in function.parameters.iter().zip(arguments) {
140161
let var = self.ssa_tracker.introduce_variable(param);
141-
self.out(smt::define_const(var, smt::SMTExpr::from(arg.clone())))
162+
self.out(smt::define_const(var, smt::SMTExpr::from(arg.clone())));
163+
self.evaluator.define_from_variable(&var, arg);
142164
}
165+
166+
let parameters = self.ssa_tracker.to_smt_variables(&function.parameters);
143167
self.encode_variable_declaration(&VariableDeclaration {
144168
variables: function.returns.clone(),
145169
value: None,
@@ -199,7 +223,14 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
199223
fn encode_if(&mut self, expr: &yul::If) {
200224
let cond = self.encode_expression(&expr.condition);
201225
assert!(cond.len() == 1);
226+
if self
227+
.evaluator
228+
.variable_known_equal(&cond[0], &"0".to_string())
229+
{
230+
return;
231+
}
202232
let prev_ssa = self.ssa_tracker.copy_current_ssa();
233+
let prev_eval = self.evaluator.copy_state();
203234

204235
self.push_path_condition(smt::neq(cond[0].clone(), 0));
205236
self.encode_block(&expr.body);
@@ -208,6 +239,7 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
208239
let output = self
209240
.ssa_tracker
210241
.join_branches(smt::eq(cond[0].clone(), 0), prev_ssa);
242+
self.evaluator.join_with_old_state(prev_eval);
211243
self.out_vec(output);
212244
}
213245

@@ -220,6 +252,8 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
220252
let cond = self.encode_expression(&for_loop.condition);
221253
assert!(cond.len() == 1);
222254
let prev_ssa = self.ssa_tracker.copy_current_ssa();
255+
let prev_eval = self.evaluator.copy_state();
256+
// TODO the evaluator does not have path conditions - is that OK?
223257

224258
self.push_path_condition(smt::neq(cond[0].clone(), 0));
225259
self.encode_block(&for_loop.body);
@@ -229,6 +263,7 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
229263
let output = self
230264
.ssa_tracker
231265
.join_branches(smt::eq(cond[0].clone(), 0), prev_ssa);
266+
self.evaluator.join_with_old_state(prev_eval);
232267
self.out_vec(output);
233268
}
234269
}
@@ -238,6 +273,7 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
238273
assert!(discriminator.len() == 1);
239274
let pre_switch_ssa = self.ssa_tracker.copy_current_ssa();
240275
let mut post_switch_ssa = self.ssa_tracker.take_current_ssa();
276+
let prev_eval = self.evaluator.copy_state();
241277

242278
for Case {
243279
literal,
@@ -246,6 +282,15 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
246282
} in &switch.cases
247283
{
248284
let is_default = literal.is_none();
285+
// TODO this will always run the default case.
286+
// We should first go through all case labels and see if we only need to execute a single one.
287+
if !is_default
288+
&& self
289+
.evaluator
290+
.variable_known_unequal(&discriminator[0], &literal.as_ref().unwrap().literal)
291+
{
292+
continue;
293+
}
249294

250295
self.ssa_tracker.set_current_ssa(pre_switch_ssa.clone());
251296

@@ -258,15 +303,17 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
258303
.map(|case| {
259304
smt::eq(
260305
discriminator[0].clone(),
261-
self.encode_literal_value(case.literal.as_ref().unwrap()),
306+
self.encode_literal_value(case.literal.as_ref().unwrap())
307+
.unwrap(),
262308
)
263309
})
264310
.collect::<Vec<_>>(),
265311
)
266312
} else {
267313
smt::neq(
268314
discriminator[0].clone(),
269-
self.encode_literal_value(literal.as_ref().unwrap()),
315+
self.encode_literal_value(literal.as_ref().unwrap())
316+
.unwrap(),
270317
)
271318
};
272319

@@ -278,9 +325,13 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
278325
.ssa_tracker
279326
.join_branches(skip_condition, post_switch_ssa);
280327
self.out_vec(output);
328+
// TODO check if this is correct.
329+
self.evaluator.join_with_old_state(prev_eval.clone());
281330
post_switch_ssa = self.ssa_tracker.take_current_ssa();
282331
post_switch_ssa.retain(|key, _| pre_switch_ssa.contains_key(key));
283332
}
333+
// TODO we should actually reset thet state of the evaluator, because
334+
// we do not know in which branch we ended up
284335

285336
self.ssa_tracker.set_current_ssa(post_switch_ssa);
286337
}
@@ -296,10 +347,12 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
296347
fn encode_literal(&mut self, literal: &Literal) -> SMTVariable {
297348
let sort = SMTSort::BV(256);
298349
let var = self.new_temporary_variable(sort);
299-
self.out(smt::define_const(
300-
var.clone(),
301-
self.encode_literal_value(literal),
302-
));
350+
self.evaluator.define_from_literal(&var, literal);
351+
if let Some(value) = self.encode_literal_value(literal) {
352+
self.out(smt::define_const(var.clone(), value));
353+
} else {
354+
self.out(smt::declare_const(var.clone()))
355+
}
303356
var
304357
}
305358

@@ -308,7 +361,7 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
308361
}
309362

310363
fn encode_function_call(&mut self, call: &FunctionCall) -> Vec<SMTVariable> {
311-
let arguments = call
364+
let arguments: Vec<SMTVariable> = call
312365
.arguments
313366
.iter()
314367
.rev()
@@ -343,6 +396,15 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
343396
.map(|_i| self.new_temporary_variable(SMTSort::BV(256)))
344397
.collect();
345398

399+
// TODO call evaluator first or interpreter first?
400+
self.evaluator
401+
.builtin_call(builtin, &arguments, &return_vars);
402+
if builtin.name == "call" {
403+
// if let Some((ast, calldata)) = self.evaluator.is_call_to_knon_contract(arguments) {
404+
405+
// // TODO
406+
// }
407+
}
346408
let result = self.interpreter.encode_builtin_call(
347409
builtin,
348410
arguments,
@@ -355,7 +417,13 @@ impl<InstructionsType: Instructions> Encoder<InstructionsType> {
355417
}
356418
IdentifierID::Reference(id) => {
357419
let fun_def = self.function_definitions[&id].clone();
358-
self.encode_function(&fun_def, &arguments)
420+
let function_vars = self.encode_function(&fun_def, &arguments);
421+
assert!(arguments.len() == function_vars.parameters.len());
422+
arguments
423+
.into_iter()
424+
.zip(function_vars.parameters)
425+
.for_each(|(arg, param)| self.out(smt::assert(smt::eq(arg, param))));
426+
function_vars.returns
359427
}
360428
_ => panic!(
361429
"Unexpected reference in function call: {:?}",
@@ -393,21 +461,27 @@ impl<T> Encoder<T> {
393461

394462
for (v, val) in variables.iter().zip(values.into_iter()) {
395463
let var = self.ssa_tracker.allocate_new_ssa_index(v);
464+
self.evaluator.define_from_variable(&var, &val);
396465
self.out(smt::define_const(var, val.into()));
397466
}
398467
}
399468

400-
fn encode_literal_value(&self, literal: &Literal) -> SMTExpr {
401-
if literal.literal.starts_with("0x") {
402-
smt::literal(format!("{:0>64}", &literal.literal[2..]), SMTSort::BV(256))
469+
fn encode_literal_value(&self, literal: &Literal) -> Option<SMTExpr> {
470+
if let Some(hex) = literal.literal.strip_prefix("0x") {
471+
Some(smt::literal(format!("{:0>64}", hex), SMTSort::BV(256)))
472+
} else if let Some(string) = literal.literal.strip_prefix("\"") {
473+
assert!(string.len() >= 2 && string.chars().last().unwrap() == '"');
474+
// This is usually only used for references to data objects,
475+
// so we do not encode it.
476+
None
403477
} else {
404-
smt::literal(
478+
Some(smt::literal(
405479
format!(
406480
"{:064X}",
407481
literal.literal.parse::<num_bigint::BigUint>().unwrap()
408482
),
409483
SMTSort::BV(256),
410-
)
484+
))
411485
}
412486
}
413487

0 commit comments

Comments
 (0)