Skip to content

Commit

Permalink
fix ands
Browse files Browse the repository at this point in the history
  • Loading branch information
brockelmore committed Jul 22, 2024
1 parent 2c8e918 commit 26ae57a
Show file tree
Hide file tree
Showing 3 changed files with 59 additions and 37 deletions.
1 change: 1 addition & 0 deletions crates/graph/src/range/elem/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -244,6 +244,7 @@ impl RangeOp {
Gt => Lt,
Lt => Gt,
other => {
tracing::trace!("Require rhs other: {other:?}");
return None;
}
};
Expand Down
18 changes: 9 additions & 9 deletions crates/shared/src/flattened.rs
Original file line number Diff line number Diff line change
Expand Up @@ -302,15 +302,15 @@ impl FlatExpr {
}
pub fn try_inv_cmp(&self) -> Option<Self> {
use FlatExpr::*;
Some(match self {
Less(loc) => MoreEqual(*loc),
More(loc) => LessEqual(*loc),
LessEqual(loc) => More(*loc),
MoreEqual(loc) => Less(*loc),
Equal(loc) => NotEqual(*loc),
NotEqual(loc) => Equal(*loc),
_ => Not(self.try_loc()?),
})
match self {
Less(loc) => Some(MoreEqual(*loc)),
More(loc) => Some(LessEqual(*loc)),
LessEqual(loc) => Some(More(*loc)),
MoreEqual(loc) => Some(Less(*loc)),
Equal(loc) => Some(NotEqual(*loc)),
NotEqual(loc) => Some(Equal(*loc)),
_ => None,
}
}
pub fn try_loc(&self) -> Option<Loc> {
use FlatExpr::*;
Expand Down
77 changes: 49 additions & 28 deletions crates/solc-expressions/src/context_builder/flattened.rs
Original file line number Diff line number Diff line change
Expand Up @@ -106,16 +106,35 @@ pub trait Flatten:
// based on their size
let start_len = self.expr_stack_mut().len();
self.traverse_expression(if_expr, unchecked);
let mut false_cond = self.expr_stack()[start_len..].to_vec();
let cmp = self.expr_stack_mut().pop().unwrap();
// have it be a require statement
self.push_expr(FlatExpr::Requirement(*loc));
self.push_expr(cmp);
self.traverse_requirement(cmp, if_expr.loc());
let true_cond = self.expr_stack_mut().drain(start_len..).collect::<Vec<_>>();

// the false condition is the same as the true, but with the comparator inverted
let mut false_cond = true_cond.clone();
if let Some(last) = false_cond.pop() {
false_cond.push(last.try_inv_cmp().unwrap_or(FlatExpr::Not(*loc)));
match last {
FlatExpr::And(loc, ..) => {
let lhs = false_cond.pop().unwrap();
let rhs = false_cond.pop().unwrap();
false_cond.push(lhs);
false_cond.push(FlatExpr::Not(loc));
false_cond.push(rhs);
false_cond.push(FlatExpr::Not(loc));
false_cond.push(FlatExpr::Requirement(loc));
false_cond.push(FlatExpr::Or(loc));
}
_ => {
if let Some(inv) = last.try_inv_cmp() {
false_cond.push(inv)
} else {
false_cond.push(last);
false_cond.push(FlatExpr::Requirement(*loc));
false_cond.push(FlatExpr::Not(*loc));
}
}
}
}

let true_cond_delta = true_cond.len();
Expand Down Expand Up @@ -163,8 +182,7 @@ pub trait Flatten:
let start_len = self.expr_stack_mut().len();
self.traverse_expression(if_expr, unchecked);
let cmp = self.expr_stack_mut().pop().unwrap();
self.push_expr(FlatExpr::Requirement(*loc));
self.push_expr(cmp);
self.traverse_requirement(cmp, if_expr.loc());
let cond_exprs = self.expr_stack_mut().drain(start_len..).collect::<Vec<_>>();
let condition = cond_exprs.len();

Expand Down Expand Up @@ -195,8 +213,7 @@ pub trait Flatten:
let for_cond_exprs = if let Some(cond) = maybe_for_cond {
self.traverse_expression(cond, unchecked);
let cmp = self.expr_stack_mut().pop().unwrap();
self.push_expr(FlatExpr::Requirement(*loc));
self.push_expr(cmp);
self.traverse_requirement(cmp, cond.loc());
self.expr_stack_mut().drain(start_len..).collect::<Vec<_>>()
} else {
vec![]
Expand Down Expand Up @@ -315,6 +332,29 @@ pub trait Flatten:
}
}

fn traverse_requirement(&mut self, cmp: FlatExpr, loc: Loc) {
match cmp {
FlatExpr::And(..) => {
// Its better to just break up And into its component
// parts now as opposed to trying to do it later
// i.e.:
// require(x && y) ==>
// require(x);
// require(y);
let rhs = self.expr_stack_mut().pop().unwrap();
let lhs = self.expr_stack_mut().pop().unwrap();
self.push_expr(FlatExpr::Requirement(loc));
self.push_expr(rhs);
self.push_expr(FlatExpr::Requirement(loc));
self.push_expr(lhs);
}
_ => {
self.push_expr(FlatExpr::Requirement(loc));
self.push_expr(cmp);
}
}
}

fn traverse_yul_statement(&mut self, stmt: &YulStatement) {
use YulStatement::*;
match stmt {
Expand Down Expand Up @@ -801,26 +841,7 @@ pub trait Flatten:
self.traverse_expression(expr, unchecked);
});
let cmp = self.expr_stack_mut().pop().unwrap();
match cmp {
FlatExpr::And(..) => {
// Its better to just break up And into its component
// parts now as opposed to trying to do it later
// i.e.:
// require(x && y) ==>
// require(x);
// require(y);
let rhs = self.expr_stack_mut().pop().unwrap();
let lhs = self.expr_stack_mut().pop().unwrap();
self.push_expr(FlatExpr::Requirement(*loc));
self.push_expr(rhs);
self.push_expr(FlatExpr::Requirement(*loc));
self.push_expr(lhs);
}
_ => {
self.push_expr(FlatExpr::Requirement(*loc));
self.push_expr(cmp);
}
}
self.traverse_requirement(cmp, *loc);
}
_ => {
// func(inputs)
Expand Down

0 comments on commit 26ae57a

Please sign in to comment.