Skip to content

Commit

Permalink
comptroller runs in ~9s
Browse files Browse the repository at this point in the history
  • Loading branch information
brockelmore committed Jul 12, 2024
1 parent 0fbf88a commit b4855ed
Show file tree
Hide file tree
Showing 27 changed files with 507 additions and 238 deletions.
11 changes: 10 additions & 1 deletion crates/graph/src/graph_elements.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ use lazy_static::lazy_static;
use petgraph::{Directed, Graph};
use solang_parser::pt::{Identifier, Loc};

use std::collections::HashMap;
use std::collections::{BTreeSet, HashMap};

pub trait RepresentationInvariant {
fn is_representation_ok(
Expand Down Expand Up @@ -402,6 +402,15 @@ impl GraphLike for DummyGraph {
panic!("Dummy Graph")
}

fn mark_dirty(&mut self, _node: NodeIdx) {}
fn dirty_nodes(&self) -> &BTreeSet<NodeIdx> {
todo!()
}

fn dirty_nodes_mut(&mut self) -> &mut BTreeSet<NodeIdx> {
todo!()
}

fn graph(&self) -> &Graph<Node, Edge, Directed, usize> {
panic!("Dummy Graph")
}
Expand Down
1 change: 1 addition & 0 deletions crates/graph/src/nodes/context/node.rs
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,7 @@ impl ContextNode {
&self,
analyzer: &'a mut impl AnalyzerBackend<Node = Node>,
) -> Result<&'a mut Context, GraphError> {
analyzer.mark_dirty(self.0.into());
match analyzer.node_mut(*self) {
Node::Context(c) => Ok(c),
Node::Unresolved(ident) => Err(GraphError::UnknownVariable(format!(
Expand Down
8 changes: 4 additions & 4 deletions crates/graph/src/nodes/context/solving.rs
Original file line number Diff line number Diff line change
Expand Up @@ -54,10 +54,10 @@ impl ContextNode {
Ok(ranges
.iter()
.filter_map(|(_dep, range)| {
if let Some(atom) = Elem::Arena(range.min).atomize(analyzer, arena) {
if let Some(atom) = range.min.atomize(analyzer, arena) {
Some(atom)
} else {
Elem::Arena(range.max).atomize(analyzer, arena)
range.max.atomize(analyzer, arena)
}
})
.collect::<Vec<SolverAtom>>())
Expand Down Expand Up @@ -131,7 +131,7 @@ impl ContextNode {
let r = range.flattened_range(analyzer, arena)?.into_owned();

// add the atomic constraint
if let Some(atom) = Elem::Arena(r.min).atomize(analyzer, arena) {
if let Some(atom) = r.min.atomize(analyzer, arena) {
let mut solver = std::mem::take(&mut self.underlying_mut(analyzer)?.dl_solver);
let constraints = solver.add_constraints(vec![atom], analyzer, arena);
constraints
Expand All @@ -140,7 +140,7 @@ impl ContextNode {
solver.add_constraint(constraint, normalized);
});
self.underlying_mut(analyzer)?.dl_solver = solver;
} else if let Some(atom) = Elem::Arena(r.max).atomize(analyzer, arena) {
} else if let Some(atom) = r.max.atomize(analyzer, arena) {
let mut solver = std::mem::take(&mut self.underlying_mut(analyzer)?.dl_solver);
let constraints = solver.add_constraints(vec![atom], analyzer, arena);
constraints
Expand Down
1 change: 1 addition & 0 deletions crates/graph/src/nodes/context/var/node.rs
Original file line number Diff line number Diff line change
Expand Up @@ -81,6 +81,7 @@ impl ContextVarNode {
&self,
analyzer: &'a mut impl GraphBackend,
) -> Result<&'a mut ContextVar, GraphError> {
analyzer.mark_dirty(self.0.into());
match analyzer.node_mut(*self) {
Node::ContextVar(c) => Ok(c),
Node::Unresolved(ident) => Err(GraphError::UnknownVariable(format!(
Expand Down
4 changes: 2 additions & 2 deletions crates/graph/src/nodes/context/var/ranging.rs
Original file line number Diff line number Diff line change
Expand Up @@ -309,7 +309,7 @@ impl ContextVarNode {
pub fn set_range_exclusions(
&self,
analyzer: &mut impl GraphBackend,
new_exclusions: Vec<usize>,
new_exclusions: Vec<Elem<Concrete>>,
) -> Result<(), GraphError> {
tracing::trace!(
"setting range exclusions for {}",
Expand Down Expand Up @@ -405,7 +405,7 @@ impl ContextVarNode {
pub fn try_set_range_exclusions(
&self,
analyzer: &mut impl GraphBackend,
new_exclusions: Vec<usize>,
new_exclusions: Vec<Elem<Concrete>>,
) -> Result<bool, GraphError> {
tracing::trace!(
"setting range exclusions for: {}",
Expand Down
4 changes: 2 additions & 2 deletions crates/graph/src/nodes/context/var/underlying.rs
Original file line number Diff line number Diff line change
Expand Up @@ -400,7 +400,7 @@ impl ContextVar {

pub fn set_range_exclusions(
&mut self,
new_exclusions: Vec<usize>,
new_exclusions: Vec<Elem<Concrete>>,
fallback_range: Option<SolcRange>,
) -> Result<(), GraphError> {
match &mut self.ty {
Expand Down Expand Up @@ -457,7 +457,7 @@ impl ContextVar {

pub fn try_set_range_exclusions(
&mut self,
new_exclusions: Vec<usize>,
new_exclusions: Vec<Elem<Concrete>>,
fallback_range: Option<SolcRange>,
) -> bool {
match &mut self.ty {
Expand Down
29 changes: 26 additions & 3 deletions crates/graph/src/nodes/context/variables.rs
Original file line number Diff line number Diff line change
Expand Up @@ -402,6 +402,30 @@ impl ContextNode {
}
}

pub fn recursive_move_struct_field(
&self,
parent: ContextVarNode,
field: ContextVarNode,
loc: Loc,
analyzer: &mut impl AnalyzerBackend,
) -> Result<(), GraphError> {
let mut new_cvar = field.latest_version(analyzer).underlying(analyzer)?.clone();
new_cvar.loc = Some(loc);

let new_cvarnode = ContextVarNode::from(analyzer.add_node(Node::ContextVar(new_cvar)));

analyzer.add_edge(
new_cvarnode.0,
parent.0,
Edge::Context(ContextEdge::AttrAccess("field")),
);

let sub_fields = field.struct_to_fields(analyzer)?;
sub_fields.iter().try_for_each(|sub_field| {
self.recursive_move_struct_field(new_cvarnode, *sub_field, loc, analyzer)
})
}

/// May move the variable from an old context to this context
pub fn maybe_move_var(
&self,
Expand Down Expand Up @@ -442,10 +466,9 @@ impl ContextNode {
Edge::Context(ContextEdge::InheritedVariable),
);

let fields = new_cvarnode.struct_to_fields(analyzer)?;
let fields = var.struct_to_fields(analyzer)?;
fields.iter().try_for_each(|field| {
let _ = self.maybe_move_var(*field, loc, analyzer)?;
Ok(())
self.recursive_move_struct_field(new_cvarnode, *field, loc, analyzer)
})?;
Ok(new_cvarnode.into())
} else {
Expand Down
4 changes: 4 additions & 0 deletions crates/graph/src/nodes/debug_reconstruction.rs
Original file line number Diff line number Diff line change
Expand Up @@ -502,6 +502,10 @@ impl FunctionNode {
&self,
analyzer: &mut impl AnalyzerBackend,
) -> FuncReconstructionReqs {
println!(
"reconstruction requirements for: {}",
self.name(analyzer).unwrap()
);
FuncReconstructionReqs {
storage: self.maybe_used_storage(analyzer).unwrap_or_default(),
usertypes: self.maybe_used_usertypes(analyzer).unwrap_or_default(),
Expand Down
4 changes: 4 additions & 0 deletions crates/graph/src/nodes/struct_ty.rs
Original file line number Diff line number Diff line change
Expand Up @@ -104,6 +104,10 @@ impl StructNode {
cvar,
Edge::Context(ContextEdge::AttrAccess("field")),
);
// do so recursively
if let Some(field_struct) = ContextVarNode::from(fc_node).ty(analyzer)?.maybe_struct() {
field_struct.add_fields_to_cvar(analyzer, loc, ContextVarNode::from(fc_node))?;
}
Ok(())
})
}
Expand Down
13 changes: 9 additions & 4 deletions crates/graph/src/range/elem/elem_enum/range_elem.rs
Original file line number Diff line number Diff line change
Expand Up @@ -482,7 +482,6 @@ impl RangeElem<Concrete> for Elem<Concrete> {
return Ok(*min.clone());
}
}
Null => return Ok(Elem::Null),
_ => {}
}
}
Expand Down Expand Up @@ -513,15 +512,21 @@ impl RangeElem<Concrete> for Elem<Concrete> {

match arena.ranges.get_mut(idx) {
Some(Self::Reference(ref mut d)) => {
tracing::trace!("simplify minimize cache MISS: {self}");
tracing::trace!(
"simplify minimize cache MISS: {self}, new simp min: {min}"
);
d.flattened_min = Some(Box::new(min.clone()));
}
Some(Self::Expr(ref mut expr)) => {
tracing::trace!("simplify minimize cache MISS: {self}");
tracing::trace!(
"simplify minimize cache MISS: {self}, new simp min: {min}"
);
expr.flattened_min = Some(Box::new(min.clone()));
}
Some(Self::ConcreteDyn(ref mut d)) => {
tracing::trace!("simplify minimize cache MISS: {self}");
tracing::trace!(
"simplify minimize cache MISS: {self}, new simp min: {min}"
);
d.flattened_min = Some(Box::new(min.clone()));
}
_ => {}
Expand Down
4 changes: 2 additions & 2 deletions crates/graph/src/range/range_trait.rs
Original file line number Diff line number Diff line change
Expand Up @@ -61,11 +61,11 @@ pub trait Range<T: Ord + Hash> {
/// Set the range maximum
fn set_range_max(&mut self, new: Self::ElemTy);
/// Set the range exclusions
fn set_range_exclusions(&mut self, new: Vec<usize>)
fn set_range_exclusions(&mut self, new: Vec<Self::ElemTy>)
where
Self: std::marker::Sized;
/// Add an exclusion value to the range
fn add_range_exclusion(&mut self, new: usize)
fn add_range_exclusion(&mut self, new: Self::ElemTy)
where
Self: std::marker::Sized;
/// Replace a potential recursion causing node index with a new index
Expand Down
75 changes: 33 additions & 42 deletions crates/graph/src/range/solc_range.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,18 +13,14 @@ use std::{borrow::Cow, collections::BTreeMap};

#[derive(Clone, Debug, PartialEq, Eq, Ord, PartialOrd, Hash)]
pub struct FlattenedRange {
pub min: usize,
pub max: usize,
pub exclusions: Vec<usize>,
pub min: Elem<Concrete>,
pub max: Elem<Concrete>,
pub exclusions: Vec<Elem<Concrete>>,
}

impl From<FlattenedRange> for SolcRange {
fn from(range: FlattenedRange) -> Self {
SolcRange::new(
Elem::Arena(range.min),
Elem::Arena(range.max),
range.exclusions,
)
SolcRange::new(range.min, range.max, range.exclusions)
}
}

Expand All @@ -34,7 +30,7 @@ pub struct SolcRange {
pub min_cached: Option<usize>,
pub max: Elem<Concrete>,
pub max_cached: Option<usize>,
pub exclusions: Vec<usize>,
pub exclusions: Vec<Elem<Concrete>>,
pub flattened: Option<FlattenedRange>,
}

Expand All @@ -56,7 +52,7 @@ impl AsDotStr for SolcRange {
.s,
self.exclusions
.iter()
.map(|excl| Elem::Arena(*excl).to_range_string(false, analyzer, arena).s)
.map(|excl| excl.to_range_string(false, analyzer, arena).s)
.collect::<Vec<_>>()
.join(", ")
)
Expand Down Expand Up @@ -102,7 +98,7 @@ impl SolcRange {
Ok(deps)
}

pub fn new(min: Elem<Concrete>, max: Elem<Concrete>, exclusions: Vec<usize>) -> Self {
pub fn new(min: Elem<Concrete>, max: Elem<Concrete>, exclusions: Vec<Elem<Concrete>>) -> Self {
Self {
min,
min_cached: None,
Expand All @@ -121,18 +117,12 @@ impl SolcRange {
arena: &mut RangeArena<Elem<Concrete>>,
) {
if let Some(ref mut flattened) = &mut self.flattened {
Elem::Arena(flattened.min).replace_dep(
to_replace,
replacement.clone(),
analyzer,
arena,
);
Elem::Arena(flattened.max).replace_dep(
to_replace,
replacement.clone(),
analyzer,
arena,
);
flattened
.min
.replace_dep(to_replace, replacement.clone(), analyzer, arena);
flattened
.max
.replace_dep(to_replace, replacement.clone(), analyzer, arena);
}
self.min
.replace_dep(to_replace, replacement.clone(), analyzer, arena);
Expand Down Expand Up @@ -538,22 +528,24 @@ impl SolcRange {
return Ok(cached.clone());
}

let mut min = Elem::Arena(arena.idx_or_upsert(self.min.clone(), analyzer));
let mut max = Elem::Arena(arena.idx_or_upsert(self.max.clone(), analyzer));
let mut min = self.min.clone();
min.arenaize(analyzer, arena)?;
min.cache_flatten(analyzer, arena)?;
let mut max = self.max.clone();
max.arenaize(analyzer, arena)?;
max.cache_flatten(analyzer, arena)?;

self.min = min.clone();
self.max = max.clone();

let simp_min = min.simplify_minimize(analyzer, arena)?;
let simp_max = max.simplify_maximize(analyzer, arena)?;
let min = arena.idx_or_upsert(simp_min, analyzer);
let max = arena.idx_or_upsert(simp_max, analyzer);
let mut simp_min = min.simplify_minimize(analyzer, arena)?;
simp_min.arenaize(analyzer, arena)?;
let mut simp_max = max.simplify_maximize(analyzer, arena)?;
simp_max.arenaize(analyzer, arena)?;

let flat_range = FlattenedRange {
min,
max,
min: simp_min,
max: simp_max,
exclusions: self.exclusions.clone(),
};
self.flattened = Some(flat_range.clone());
Expand Down Expand Up @@ -583,10 +575,12 @@ impl Range<Concrete> for SolcRange {
analyzer: &mut impl GraphBackend,
arena: &mut RangeArena<Elem<Concrete>>,
) -> Result<(), GraphError> {
let min = std::mem::take(&mut self.min);
let max = std::mem::take(&mut self.max);
self.min = Elem::Arena(arena.idx_or_upsert(min, analyzer));
self.max = Elem::Arena(arena.idx_or_upsert(max, analyzer));
let mut min = std::mem::take(&mut self.min);
let mut max = std::mem::take(&mut self.max);
min.arenaize(analyzer, arena)?;
max.arenaize(analyzer, arena)?;
self.min = min;
self.max = max;
if self.max_cached.is_none() {
let max = self.range_max_mut();
max.cache_maximize(analyzer, arena)?;
Expand Down Expand Up @@ -646,11 +640,7 @@ impl Range<Concrete> for SolcRange {
}

fn range_exclusions(&self) -> Vec<Self::ElemTy> {
self.exclusions
.clone()
.into_iter()
.map(Elem::Arena)
.collect()
self.exclusions.clone().into_iter().collect()
}
fn set_range_min(&mut self, new: Self::ElemTy) {
self.min_cached = None;
Expand All @@ -663,14 +653,15 @@ impl Range<Concrete> for SolcRange {
self.max = new;
}

fn add_range_exclusion(&mut self, new: usize) {
fn add_range_exclusion(&mut self, new: Elem<Concrete>) {
if !self.exclusions.contains(&new) {
self.exclusions.push(new);
}
}
fn set_range_exclusions(&mut self, new: Vec<usize>) {
fn set_range_exclusions(&mut self, new: Vec<Elem<Concrete>>) {
self.exclusions = new;
}

fn filter_min_recursion(
&mut self,
self_idx: NodeIdx,
Expand Down
2 changes: 1 addition & 1 deletion crates/graph/src/solvers/dl.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1059,7 +1059,7 @@ impl DLSolver {
};
Some(res)
}
other => panic!("other op: {}, {constraint:#?}", other.to_string()),
_other => return None,
}
} else if constraint.rhs.is_part() {
let new_rhs = AtomOrPart::Atom(SolverAtom {
Expand Down
Loading

0 comments on commit b4855ed

Please sign in to comment.