diff --git a/crates/graph/src/nodes/context/solving.rs b/crates/graph/src/nodes/context/solving.rs index 8e1fc2c8..c66aef3d 100644 --- a/crates/graph/src/nodes/context/solving.rs +++ b/crates/graph/src/nodes/context/solving.rs @@ -1,6 +1,4 @@ use crate::elem::Elem; -use crate::FlattenedRange; -use crate::SolcRange; use crate::{ as_dot_str, nodes::{ContextNode, ContextVarNode}, @@ -25,13 +23,11 @@ impl ContextNode { // println!("checking unreachable: {}", self.path(analyzer)); let mut solver = self.dl_solver(analyzer)?.clone(); match solver.solve_partial(analyzer)? { - SolveStatus::Unsat => { - Ok(true) - }, + SolveStatus::Unsat => Ok(true), e => { // println!("other: {e:?}"); Ok(false) - }, + } } } @@ -105,16 +101,20 @@ impl ContextNode { if let Some(atom) = Elem::Arena(r.min).atomize(analyzer) { let mut solver = std::mem::take(&mut self.underlying_mut(analyzer)?.dl_solver); let constraints = solver.add_constraints(vec![atom], analyzer); - constraints.into_iter().for_each(|(constraint, normalized)| { - solver.add_constraint(constraint, normalized); - }); + constraints + .into_iter() + .for_each(|(constraint, normalized)| { + solver.add_constraint(constraint, normalized); + }); self.underlying_mut(analyzer)?.dl_solver = solver; } else if let Some(atom) = Elem::Arena(r.max).atomize(analyzer) { let mut solver = std::mem::take(&mut self.underlying_mut(analyzer)?.dl_solver); let constraints = solver.add_constraints(vec![atom], analyzer); - constraints.into_iter().for_each(|(constraint, normalized)| { - solver.add_constraint(constraint, normalized); - }); + constraints + .into_iter() + .for_each(|(constraint, normalized)| { + solver.add_constraint(constraint, normalized); + }); self.underlying_mut(analyzer)?.dl_solver = solver; } diff --git a/crates/graph/src/nodes/context/var/underlying.rs b/crates/graph/src/nodes/context/var/underlying.rs index a35c32be..ac799221 100644 --- a/crates/graph/src/nodes/context/var/underlying.rs +++ b/crates/graph/src/nodes/context/var/underlying.rs @@ -84,8 +84,7 @@ impl ContextVar { ), storage: None, is_tmp: true, - is_symbolic: lhs_cvar.is_symbolic(analyzer)? - || rhs_cvar.is_symbolic(analyzer)?, + is_symbolic: lhs_cvar.is_symbolic(analyzer)? || rhs_cvar.is_symbolic(analyzer)?, is_return: false, tmp_of: Some(TmpConstruction::new(lhs_cvar, op, Some(rhs_cvar))), dep_on: { diff --git a/crates/graph/src/nodes/context/var/versioning.rs b/crates/graph/src/nodes/context/var/versioning.rs index caf3d91e..594dfa90 100644 --- a/crates/graph/src/nodes/context/var/versioning.rs +++ b/crates/graph/src/nodes/context/var/versioning.rs @@ -64,14 +64,19 @@ impl ContextVarNode { .graph() .edges_directed(current_node.0.into(), Direction::Outgoing) .filter(|edge| { - matches!(edge.weight(), Edge::Context(ContextEdge::InheritedVariable) | Edge::Context(ContextEdge::InputVariable)) + matches!( + edge.weight(), + Edge::Context(ContextEdge::InheritedVariable) + | Edge::Context(ContextEdge::InputVariable) + ) }) .map(|edge| ContextVarNode::from(edge.target())) .take(1) - .next() { + .next() + { global_first = target_node.first_version(analyzer); stack.push(global_first); - pushed = true; + pushed = true; } if !pushed { @@ -125,13 +130,18 @@ impl ContextVarNode { .graph() .edges_directed(current_node.0.into(), Direction::Outgoing) .filter(|edge| { - matches!(edge.weight(), Edge::Context(ContextEdge::InheritedVariable) | Edge::Context(ContextEdge::InputVariable)) + matches!( + edge.weight(), + Edge::Context(ContextEdge::InheritedVariable) + | Edge::Context(ContextEdge::InputVariable) + ) }) .map(|edge| ContextVarNode::from(edge.target())) .take(1) - .next() { + .next() + { stack.push(target_node); - pushed = true; + pushed = true; } if !pushed { diff --git a/crates/graph/src/nodes/context/variables.rs b/crates/graph/src/nodes/context/variables.rs index 6061da17..20ccb24e 100644 --- a/crates/graph/src/nodes/context/variables.rs +++ b/crates/graph/src/nodes/context/variables.rs @@ -48,7 +48,7 @@ impl ContextNode { let name = var.name(analyzer)?; let vars = &mut self.underlying_mut(analyzer)?.cache.vars; vars.insert(name, var); - Ok(()) + Ok(()) } } @@ -71,7 +71,11 @@ impl ContextNode { .copied() } - pub fn tmp_var_by_name(&self, analyzer: &impl GraphBackend, name: &str) -> Option { + pub fn tmp_var_by_name( + &self, + analyzer: &impl GraphBackend, + name: &str, + ) -> Option { self.underlying(analyzer) .unwrap() .cache diff --git a/crates/graph/src/solvers/atoms.rs b/crates/graph/src/solvers/atoms.rs index 87ab7eda..9fe1dd39 100644 --- a/crates/graph/src/solvers/atoms.rs +++ b/crates/graph/src/solvers/atoms.rs @@ -330,7 +330,7 @@ impl Atomize for Elem { } (AtomOrPart::Atom(l_atom), r @ AtomOrPart::Part(_)) => { // println!("atom part"); - + AtomOrPart::Atom(l_atom.add_rhs(expr.op, r)) } (l @ AtomOrPart::Part(_), AtomOrPart::Atom(r_atom)) => { diff --git a/crates/graph/src/solvers/dl.rs b/crates/graph/src/solvers/dl.rs index 2b2b39b8..dcaf5978 100644 --- a/crates/graph/src/solvers/dl.rs +++ b/crates/graph/src/solvers/dl.rs @@ -496,7 +496,6 @@ impl DLSolver { ); }); - if find_negative_cycle(&self.graph, root_node, analyzer).is_some() { return Ok(DLSolveResult { status: SolveStatus::Unsat, @@ -619,7 +618,7 @@ impl DLSolver { })), } } - _ => constraint + _ => constraint, } } else { // good @@ -640,7 +639,7 @@ impl DLSolver { ty: OpType::DL, lhs: constraint.lhs, op: RangeOp::Add(true), - rhs: rhs.rhs + rhs: rhs.rhs, })), op: constraint.op, rhs: rhs.lhs, @@ -654,23 +653,22 @@ impl DLSolver { ty: OpType::DL, lhs: constraint.lhs, op: RangeOp::Sub(true), - rhs: rhs.rhs + rhs: rhs.rhs, })), op: constraint.op, rhs: rhs.lhs, } } - _ => constraint + _ => constraint, } } else { // good constraint } } - _ => constraint + _ => constraint, }; - println!("normalizing: {}", constraint.into_expr_elem()); match constraint.op { RangeOp::Eq => { @@ -820,7 +818,7 @@ impl DLSolver { }, analyzer, ) - // } + // } // } } _ => panic!("here"), diff --git a/crates/solc-expressions/src/bin_op.rs b/crates/solc-expressions/src/bin_op.rs index a512e4ca..a9c45591 100644 --- a/crates/solc-expressions/src/bin_op.rs +++ b/crates/solc-expressions/src/bin_op.rs @@ -146,7 +146,7 @@ pub trait BinOp: AnalyzerBackend + Sized { rhs_cvar: ContextVarNode, ctx: ContextNode, op: RangeOp, - mut assign: bool, + assign: bool, ) -> Result { tracing::trace!( "binary op: {} {} {}, assign: {}", @@ -183,7 +183,6 @@ pub trait BinOp: AnalyzerBackend + Sized { // } // } // } - let unchecked = match op { RangeOp::Add(u) | RangeOp::Sub(u) | RangeOp::Mul(u) | RangeOp::Div(u) => u, @@ -204,8 +203,12 @@ pub trait BinOp: AnalyzerBackend + Sized { new } else { // TODO: simplify the expression such that we match an existing tmp if possible - let mut new_lhs_underlying = ContextVar::new_bin_op_tmp(lhs_cvar, op, rhs_cvar, ctx, loc, self).into_expr_err(loc)?; - if let Ok(Some(existing)) = self.get_unchanged_tmp_variable(&new_lhs_underlying.display_name, ctx) { + let mut new_lhs_underlying = + ContextVar::new_bin_op_tmp(lhs_cvar, op, rhs_cvar, ctx, loc, self) + .into_expr_err(loc)?; + if let Ok(Some(existing)) = + self.get_unchanged_tmp_variable(&new_lhs_underlying.display_name, ctx) + { self.advance_var_in_ctx_forcible(existing, loc, ctx, true)? } else { // will potentially mutate the ty from concrete to builtin with a concrete range diff --git a/crates/solc-expressions/src/variable.rs b/crates/solc-expressions/src/variable.rs index a7d16293..18d0956b 100644 --- a/crates/solc-expressions/src/variable.rs +++ b/crates/solc-expressions/src/variable.rs @@ -134,12 +134,8 @@ pub trait Variable: AnalyzerBackend + Size } } - fn get_tmp_variable( - &mut self, - name: &str, - ctx: ContextNode, - ) -> Option { - let cvar = ctx.tmp_var_by_name(self, &name)?; + fn get_tmp_variable(&mut self, name: &str, ctx: ContextNode) -> Option { + let cvar = ctx.tmp_var_by_name(self, name)?; Some(cvar.latest_version(self)) } @@ -149,7 +145,7 @@ pub trait Variable: AnalyzerBackend + Size ctx: ContextNode, ) -> Result, GraphError> { let Some(var) = self.get_tmp_variable(name, ctx) else { - return Ok(None) + return Ok(None); }; if let Some(tmp) = var.tmp_of(self)? { @@ -158,12 +154,12 @@ pub trait Variable: AnalyzerBackend + Size let newest_min = latest.evaled_range_min(self)?; let curr_min = tmp.lhs.evaled_range_min(self)?; if newest_min != curr_min { - return Ok(None) + return Ok(None); } let newest_max = latest.evaled_range_max(self)?; let curr_max = tmp.lhs.evaled_range_max(self)?; if newest_max != curr_max { - return Ok(None) + return Ok(None); } } @@ -173,12 +169,12 @@ pub trait Variable: AnalyzerBackend + Size let newest_min = latest.evaled_range_min(self)?; let curr_min = rhs.evaled_range_min(self)?; if newest_min != curr_min { - return Ok(None) + return Ok(None); } let newest_max = latest.evaled_range_max(self)?; let curr_max = rhs.evaled_range_max(self)?; if newest_max != curr_max { - return Ok(None) + return Ok(None); } } }