Skip to content

Commit

Permalink
dl fix2
Browse files Browse the repository at this point in the history
  • Loading branch information
@brockelmore
brockelmore committed Mar 19, 2024
1 parent ff7bb5f commit 6c51283
Show file tree
Hide file tree
Showing 4 changed files with 150 additions and 142 deletions.
26 changes: 26 additions & 0 deletions crates/graph/src/range/elem/expr.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,32 @@ impl Hash for RangeExpr<Concrete> {
}

impl RangeExpr<Concrete> {
pub fn is_noop(&self) -> (bool, usize) {
let one = Elem::from(Concrete::from(U256::one()));
let zero = Elem::from(Concrete::from(U256::zero()));
match self.op {
RangeOp::Mul(_) | RangeOp::Div(_) => {
if *self.lhs == one {
(true, 0)
} else if *self.rhs == one {
(true, 1)
} else {
(false, 0)
}
}
RangeOp::Add(_) | RangeOp::Sub(_) => {
if *self.lhs == zero {
(true, 0)
} else if *self.rhs == zero {
(true, 1)
} else {
(false, 0)
}
}
_ => (false, 0),
}
}

pub fn inverse_if_boolean(&self) -> Option<Self> {
if EQ_OPS.contains(&self.op) {
if SINGLETON_EQ_OPS.contains(&self.op) {
Expand Down
18 changes: 15 additions & 3 deletions crates/graph/src/solvers/atoms.rs
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
use crate::elem::{collapse, MaybeCollapsed};
use crate::range::exec_traits::ExecOp;
use crate::{
nodes::{Concrete, ContextVarNode},
Expand Down Expand Up @@ -253,15 +254,26 @@ pub trait Atomize {
impl Atomize for Elem<Concrete> {
#[tracing::instrument(level = "trace", skip_all)]
fn atoms_or_part(&self, analyzer: &mut impl GraphBackend) -> AtomOrPart {

match self {
Elem::Arena(_) => self.dearenaize(analyzer).borrow().atoms_or_part(analyzer),
Elem::Concrete(_) | Elem::Reference(_) => AtomOrPart::Part(self.clone()),
Elem::ConcreteDyn(_) => AtomOrPart::Part(self.clone()),
e @ Elem::Expr(expr) => {
// println!("atoms or part was expr: {e}");
Elem::Expr(expr) => {
match collapse(&expr.lhs, expr.op, &expr.rhs, analyzer) {
MaybeCollapsed::Concretes(_l, _r) => {
let exec_res = expr.exec_op(true, analyzer).unwrap();
return exec_res.atoms_or_part(analyzer);
}
MaybeCollapsed::Collapsed(elem) => {
return elem.atoms_or_part(analyzer);
}
MaybeCollapsed::Not(..) => {}
}

match (
expr.lhs.atoms_or_part(analyzer),
expr.rhs.atoms_or_part(analyzer),
expr.rhs.atoms_or_part(analyzer)
) {
(ref lp @ AtomOrPart::Part(ref l), ref rp @ AtomOrPart::Part(ref r)) => {
// println!("part part");
Expand Down
240 changes: 105 additions & 135 deletions crates/graph/src/solvers/dl.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -308,11 +308,26 @@ impl DLSolver {

let dl_solvable = self.dl_solvable_constraints();
// println!("dl solvable: {dl_solvable:#?}");
// constraints -> paths -> constraint

// constraints -> variable -> paths

// [
// var1: [
// constraint1: [path1, path2],
// constraint2: [path1],
// ]
// ]
let basic: Vec<SolverAtom> = dl_solvable
.iter()
.filter_map(|c| if c.len() == 1 { Some(c.clone()) } else { None })
.filter_map(|var| {
let res: Vec<_> = var.iter().filter_map(|constraint| {
if constraint.len() == 1 { Some(constraint.clone()) } else { None }
}).collect();
if res.len() == 1 {
Some(res)
} else {
None
}
})
.flatten()
.flatten()
.collect();
Expand All @@ -321,17 +336,28 @@ impl DLSolver {
// so its truly unsat
// println!("basic: {basic:#?}");
let basic_solve = self.dl_solve(basic.clone(), analyzer)?;
if matches!(basic_solve.status, SolveStatus::Unsat) {
return Ok(SolveStatus::Unsat);
}
// if matches!(basic_solve.status, SolveStatus::Unsat) {
// return Ok(SolveStatus::Unsat);
// }

// println!("basic solve: {basic_solve:?}");

let multi: Vec<_> = dl_solvable
.iter()
.filter_map(|c| if c.len() > 1 { Some(c.clone()) } else { None })
.filter_map(|var| {
let res: Vec<_> = var.iter().filter_map(|constraint| {
if constraint.len() > 1 { Some(constraint.clone()) } else { None }
}).collect();
if res.len() > 1 {
Some(res)
} else {
None
}
})
.collect();

// println!("multi: {multi:?}");

if multi.is_empty() {
// we had no branches, just use the basic solve
return match basic_solve.status {
Expand All @@ -345,6 +371,7 @@ impl DLSolver {
}
};
} else if !basic.is_empty() {
// println!("was multi");
let mut cnt = 0;
let mut unsat = 0;
for permutation in multi.iter().multi_cartesian_product() {
Expand Down Expand Up @@ -669,7 +696,7 @@ impl DLSolver {
_ => constraint,
};

println!("normalizing: {}", constraint.into_expr_elem());
// println!("normalizing: {}", constraint.into_expr_elem());
match constraint.op {
RangeOp::Eq => {
// convert `x == y` into `x <= y - 0 || y <= x - 0`
Expand Down Expand Up @@ -751,78 +778,47 @@ impl DLSolver {
res
}
RangeOp::Lt => {
let lhs_symb = !constraint.lhs.dependent_on(analyzer).is_empty();
let rhs_symb = !constraint.rhs.dependent_on(analyzer).is_empty();
match (lhs_symb, rhs_symb) {
(true, true) => {
// x < y
// ==> x - y <= -1
let new_lhs = AtomOrPart::Atom(
constraint
.lhs
.into_elem()
.wrapping_sub(constraint.rhs.into_elem())
.atomize(analyzer)
.expect("unable to atomize?"),
);
Self::dl_atom_normalize(
SolverAtom {
ty: OpType::DL,
lhs: Rc::new(new_lhs),
op: RangeOp::Lte,
rhs: Rc::new(AtomOrPart::Part(Elem::from(Concrete::from(
I256::from(-1),
)))),
},
analyzer,
)
}
(true, false) => {
// x < k
// ==> x - 0 <= k
let new_lhs = AtomOrPart::Atom(
constraint
.lhs
.into_elem()
.wrapping_sub(Elem::from(Concrete::from(U256::zero())))
.atomize(analyzer)
.expect("unable to atomize?"),
);

Self::dl_atom_normalize(
SolverAtom {
ty: OpType::DL,
lhs: Rc::new(new_lhs),
op: RangeOp::Lte,
rhs: constraint.rhs,
},
analyzer,
)
}
(false, true) => {
// k < x ==> k < (x - y)
// k < x
// ==> 0 - x <= k
let new_lhs = AtomOrPart::Atom(
Elem::from(Concrete::from(U256::zero()))
.wrapping_sub(constraint.rhs.into_elem())
.atomize(analyzer)
.expect("unable to atomize?"),
);
Self::dl_atom_normalize(
SolverAtom {
ty: OpType::DL,
lhs: Rc::new(new_lhs),
op: RangeOp::Lte,
rhs: constraint.lhs,
},
analyzer,
)
// }
// }
}
_ => panic!("here"),
}
// x < y
// x <= y - 1
let new_rhs = constraint.rhs
.into_elem()
.wrapping_sub(Elem::from(Concrete::from(U256::one())))
.atoms_or_part(analyzer);
Self::dl_atom_normalize(
SolverAtom {
ty: OpType::DL,
lhs: constraint.lhs,
op: RangeOp::Lte,
rhs: Rc::new(new_rhs),
},
analyzer,
)
}
RangeOp::Gte => Self::dl_atom_normalize(
SolverAtom {
ty: OpType::DL,
lhs: constraint.rhs,
op: RangeOp::Lte,
rhs: constraint.lhs,
},
analyzer,
),
RangeOp::Gt => Self::dl_atom_normalize(
SolverAtom {
ty: OpType::DL,
lhs: constraint.rhs,
op: RangeOp::Lt,
rhs: constraint.lhs,
},
analyzer,
),
RangeOp::Or => {
let mut res = Self::dl_atom_normalize(constraint.lhs.as_solver_atom(), analyzer);
res.extend(Self::dl_atom_normalize(
constraint.rhs.as_solver_atom(),
analyzer,
));
res
}
RangeOp::Lte => {
if constraint.lhs.is_atom() {
Expand Down Expand Up @@ -953,37 +949,37 @@ impl DLSolver {
}
}
// RangeOp::Eq => {
// // (atom.lhs == atom.rhs) <= rhs
// // try just swapping
// // rhs >=
// let new_lhs_atom = SolverAtom {
// ty: constraint.ty,
// lhs: lhs_atom.lhs,
// op: RangeOp::Sub(true),
// rhs: lhs_atom.rhs
// };
// Self::dl_atom_normalize(SolverAtom {
// ty: constraint.ty,
// lhs: Box::new(AtomOrPart::Atom(new_lhs_atom)),
// op: constraint.op,
// rhs: constraint.rhs.clone(),
// })
// // (atom.lhs == atom.rhs) <= rhs
// // try just swapping
// // rhs >=
// let new_lhs_atom = SolverAtom {
// ty: constraint.ty,
// lhs: lhs_atom.lhs,
// op: RangeOp::Sub(true),
// rhs: lhs_atom.rhs
// };
// Self::dl_atom_normalize(SolverAtom {
// ty: constraint.ty,
// lhs: Box::new(AtomOrPart::Atom(new_lhs_atom)),
// op: constraint.op,
// rhs: constraint.rhs.clone(),
// })
// }
// RangeOp::Neq => {
// // (atom.lhs != atom.rhs) <= rhs
// // (atom.lhs - atom.rhs) <= rhs
// let new_lhs_atom = SolverAtom {
// ty: constraint.ty,
// lhs: lhs_atom.lhs,
// op: RangeOp::Sub(true),
// rhs: lhs_atom.rhs
// };
// Self::dl_atom_normalize(SolverAtom {
// ty: constraint.ty,
// lhs: Box::new(AtomOrPart::Atom(new_lhs_atom)),
// op: constraint.op,
// rhs: constraint.rhs.clone(),
// })
// // (atom.lhs != atom.rhs) <= rhs
// // (atom.lhs - atom.rhs) <= rhs
// let new_lhs_atom = SolverAtom {
// ty: constraint.ty,
// lhs: lhs_atom.lhs,
// op: RangeOp::Sub(true),
// rhs: lhs_atom.rhs
// };
// Self::dl_atom_normalize(SolverAtom {
// ty: constraint.ty,
// lhs: Box::new(AtomOrPart::Atom(new_lhs_atom)),
// op: constraint.op,
// rhs: constraint.rhs.clone(),
// })
// }
other => panic!("other op: {}, {constraint:#?}", other.to_string()),
}
Expand All @@ -1008,32 +1004,6 @@ impl DLSolver {
vec![vec![constraint]]
}
}
RangeOp::Gte => Self::dl_atom_normalize(
SolverAtom {
ty: OpType::DL,
lhs: constraint.rhs,
op: RangeOp::Lte,
rhs: constraint.lhs,
},
analyzer,
),
RangeOp::Gt => Self::dl_atom_normalize(
SolverAtom {
ty: OpType::DL,
lhs: constraint.rhs,
op: RangeOp::Lt,
rhs: constraint.lhs,
},
analyzer,
),
RangeOp::Or => {
let mut res = Self::dl_atom_normalize(constraint.lhs.as_solver_atom(), analyzer);
res.extend(Self::dl_atom_normalize(
constraint.rhs.as_solver_atom(),
analyzer,
));
res
}
_other => {
// println!("other: {}, {}", other.to_string(), constraint.into_expr_elem());
Self::dl_atom_normalize(constraint, analyzer)
Expand Down
8 changes: 4 additions & 4 deletions crates/solc-expressions/src/cond_op.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -82,11 +82,11 @@ pub trait CondOp: AnalyzerBackend<Expr = Expression, ExprErr = ExprErr> + Requir
match (true_killed, false_killed) {
(true, true) => {
// both have been killed, delete the child and dont process the bodies
println!("BOTH KILLED");
// println!("BOTH KILLED");
ctx.delete_child(analyzer).into_expr_err(loc)?;
}
(true, false) => {
println!("TRUE KILLED");
// println!("TRUE KILLED");
// the true context has been killed, delete child, process the false fork expression
// in the parent context and parse the false body
ctx.delete_child(analyzer).into_expr_err(loc)?;
Expand All @@ -99,7 +99,7 @@ pub trait CondOp: AnalyzerBackend<Expr = Expression, ExprErr = ExprErr> + Requir
}
}
(false, true) => {
println!("FALSE KILLED");
// println!("FALSE KILLED");
// the false context has been killed, delete child, process the true fork expression
// in the parent context and parse the true body
ctx.delete_child(analyzer).into_expr_err(loc)?;
Expand All @@ -114,7 +114,7 @@ pub trait CondOp: AnalyzerBackend<Expr = Expression, ExprErr = ExprErr> + Requir
})?;
}
(false, false) => {
println!("NEITHER KILLED");
// println!("NEITHER KILLED");
// both branches are reachable. process each body
analyzer.apply_to_edges(true_subctx, loc, &|analyzer, ctx, _loc| {
analyzer.parse_ctx_statement(
Expand Down

0 comments on commit 6c51283

Please sign in to comment.