Skip to content

Commit

Permalink
lint
Browse files Browse the repository at this point in the history
  • Loading branch information
@brockelmore
brockelmore committed Mar 19, 2024
1 parent a1f2d44 commit ff7bb5f
Show file tree
Hide file tree
Showing 8 changed files with 56 additions and 46 deletions.
24 changes: 12 additions & 12 deletions crates/graph/src/nodes/context/solving.rs
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,4 @@
use crate::elem::Elem;
use crate::FlattenedRange;
use crate::SolcRange;
use crate::{
as_dot_str,
nodes::{ContextNode, ContextVarNode},
Expand All @@ -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)
},
}
}
}

Expand Down Expand Up @@ -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;
}

Expand Down
3 changes: 1 addition & 2 deletions crates/graph/src/nodes/context/var/underlying.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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: {
Expand Down
22 changes: 16 additions & 6 deletions crates/graph/src/nodes/context/var/versioning.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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 {
Expand Down
8 changes: 6 additions & 2 deletions crates/graph/src/nodes/context/variables.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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(())
}
}

Expand All @@ -71,7 +71,11 @@ impl ContextNode {
.copied()
}

pub fn tmp_var_by_name(&self, analyzer: &impl GraphBackend, name: &str) -> Option<ContextVarNode> {
pub fn tmp_var_by_name(
&self,
analyzer: &impl GraphBackend,
name: &str,
) -> Option<ContextVarNode> {
self.underlying(analyzer)
.unwrap()
.cache
Expand Down
2 changes: 1 addition & 1 deletion crates/graph/src/solvers/atoms.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -330,7 +330,7 @@ impl Atomize for Elem<Concrete> {
}
(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)) => {
Expand Down
14 changes: 6 additions & 8 deletions crates/graph/src/solvers/dl.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -496,7 +496,6 @@ impl DLSolver {
);
});


if find_negative_cycle(&self.graph, root_node, analyzer).is_some() {
return Ok(DLSolveResult {
status: SolveStatus::Unsat,
Expand Down Expand Up @@ -619,7 +618,7 @@ impl DLSolver {
})),
}
}
_ => constraint
_ => constraint,
}
} else {
// good
Expand All @@ -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,
Expand All @@ -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 => {
Expand Down Expand Up @@ -820,7 +818,7 @@ impl DLSolver {
},
analyzer,
)
// }
// }
// }
}
_ => panic!("here"),
Expand Down
11 changes: 7 additions & 4 deletions crates/solc-expressions/src/bin_op.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -146,7 +146,7 @@ pub trait BinOp: AnalyzerBackend<Expr = Expression, ExprErr = ExprErr> + Sized {
rhs_cvar: ContextVarNode,
ctx: ContextNode,
op: RangeOp,
mut assign: bool,
assign: bool,
) -> Result<ExprRet, ExprErr> {
tracing::trace!(
"binary op: {} {} {}, assign: {}",
Expand Down Expand Up @@ -183,7 +183,6 @@ pub trait BinOp: AnalyzerBackend<Expr = Expression, ExprErr = ExprErr> + Sized {
// }
// }
// }


let unchecked = match op {
RangeOp::Add(u) | RangeOp::Sub(u) | RangeOp::Mul(u) | RangeOp::Div(u) => u,
Expand All @@ -204,8 +203,12 @@ pub trait BinOp: AnalyzerBackend<Expr = Expression, ExprErr = ExprErr> + 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
Expand Down
18 changes: 7 additions & 11 deletions crates/solc-expressions/src/variable.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -134,12 +134,8 @@ pub trait Variable: AnalyzerBackend<Expr = Expression, ExprErr = ExprErr> + Size
}
}

fn get_tmp_variable(
&mut self,
name: &str,
ctx: ContextNode,
) -> Option<ContextVarNode> {
let cvar = ctx.tmp_var_by_name(self, &name)?;
fn get_tmp_variable(&mut self, name: &str, ctx: ContextNode) -> Option<ContextVarNode> {
let cvar = ctx.tmp_var_by_name(self, name)?;
Some(cvar.latest_version(self))
}

Expand All @@ -149,7 +145,7 @@ pub trait Variable: AnalyzerBackend<Expr = Expression, ExprErr = ExprErr> + Size
ctx: ContextNode,
) -> Result<Option<ContextVarNode>, 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)? {
Expand All @@ -158,12 +154,12 @@ pub trait Variable: AnalyzerBackend<Expr = Expression, ExprErr = ExprErr> + 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);
}
}

Expand All @@ -173,12 +169,12 @@ pub trait Variable: AnalyzerBackend<Expr = Expression, ExprErr = ExprErr> + 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);
}
}
}
Expand Down

0 comments on commit ff7bb5f

Please sign in to comment.