Skip to content

Commit

Permalink
dl fix
Browse files Browse the repository at this point in the history
  • Loading branch information
@brockelmore
brockelmore committed Mar 19, 2024
1 parent 7e404bc commit a1f2d44
Show file tree
Hide file tree
Showing 12 changed files with 434 additions and 120 deletions.
2 changes: 2 additions & 0 deletions crates/graph/src/nodes/context/context_tys.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,8 @@ impl ModifierState {
pub struct ContextCache {
/// Variables in this context
pub vars: BTreeMap<String, ContextVarNode>,
/// Temporary variables in this context
pub tmp_vars: BTreeMap<String, ContextVarNode>,
/// Visible functions from this context
pub visible_funcs: Option<Vec<FunctionNode>>,
/// Visible structs from this context
Expand Down
27 changes: 18 additions & 9 deletions crates/graph/src/nodes/context/solving.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,10 +22,16 @@ use std::collections::BTreeMap;
impl ContextNode {
/// Use a Difference Logic solver to see if it is unreachable
pub fn unreachable(&self, analyzer: &impl GraphBackend) -> Result<bool, GraphError> {
// println!("checking unreachable: {}", self.path(analyzer));
let mut solver = self.dl_solver(analyzer)?.clone();
match solver.solve_partial(analyzer)? {
SolveStatus::Unsat => Ok(true),
_ => Ok(false),
SolveStatus::Unsat => {
Ok(true)
},
e => {
// println!("other: {e:?}");
Ok(false)
},
}
}

Expand Down Expand Up @@ -84,7 +90,8 @@ impl ContextNode {
analyzer: &mut impl AnalyzerBackend,
) -> Result<(), GraphError> {
tracing::trace!(
"Adding ctx dependency: {}, is_controllable: {}",
"Adding ctx ({}) dependency: {}, is_controllable: {}",
self.path(analyzer),
dep.display_name(analyzer)?,
dep.is_controllable(analyzer)?
);
Expand All @@ -94,18 +101,20 @@ impl ContextNode {
// dep.cache_flattened_range(analyzer)?;
let mut range = dep.range(analyzer)?.unwrap();
let r = range.flattened_range(analyzer)?.into_owned();
tracing::trace!(
"flattened: {}",
<FlattenedRange as Into<SolcRange>>::into(r.clone()).as_dot_str(analyzer)
);
// add the atomic constraint
if let Some(atom) = Elem::Arena(r.min).atomize(analyzer) {
let mut solver = std::mem::take(&mut self.underlying_mut(analyzer)?.dl_solver);
solver.add_constraints(vec![atom], analyzer);
let constraints = solver.add_constraints(vec![atom], analyzer);
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);
solver.add_constraints(vec![atom], analyzer);
let constraints = solver.add_constraints(vec![atom], analyzer);
constraints.into_iter().for_each(|(constraint, normalized)| {
solver.add_constraint(constraint, normalized);
});
self.underlying_mut(analyzer)?.dl_solver = solver;
}

Expand Down
2 changes: 2 additions & 0 deletions crates/graph/src/nodes/context/underlying.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -206,6 +206,7 @@ impl Context {
number_of_live_edges: 0,
cache: ContextCache {
vars: Default::default(),
tmp_vars: Default::default(),
visible_funcs: if fork_expr.is_some() {
parent_ctx.underlying(analyzer)?.cache.visible_funcs.clone()
} else if let Some(ret_ctx) = returning_ctx {
Expand Down Expand Up @@ -285,6 +286,7 @@ impl Context {
number_of_live_edges: 0,
cache: ContextCache {
vars: parent_ctx.underlying(analyzer)?.cache.vars.clone(),
tmp_vars: Default::default(),
visible_funcs: parent_ctx.underlying(analyzer)?.cache.visible_funcs.clone(),
visible_structs: parent_ctx
.underlying(analyzer)?
Expand Down
38 changes: 38 additions & 0 deletions crates/graph/src/nodes/context/var/underlying.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,44 @@ impl ContextVar {
self.tmp_of
}

pub fn new_bin_op_tmp(
lhs_cvar: ContextVarNode,
op: RangeOp,
rhs_cvar: ContextVarNode,
ctx: ContextNode,
loc: Loc,
analyzer: &mut impl AnalyzerBackend,
) -> Result<Self, GraphError> {
Ok(ContextVar {
loc: Some(loc),
name: format!(
"tmp{}({} {} {})",
ctx.new_tmp(analyzer)?,
lhs_cvar.name(analyzer)?,
op.to_string(),
rhs_cvar.name(analyzer)?
),
display_name: format!(
"({} {} {})",
lhs_cvar.display_name(analyzer)?,
op.to_string(),
rhs_cvar.display_name(analyzer)?
),
storage: None,
is_tmp: true,
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: {
let mut deps = lhs_cvar.dependent_on(analyzer, true)?;
deps.extend(rhs_cvar.dependent_on(analyzer, true)?);
Some(deps)
},
ty: lhs_cvar.underlying(analyzer)?.ty.clone(),
})
}

pub fn new_from_concrete(
loc: Loc,
ctx: ContextNode,
Expand Down
91 changes: 50 additions & 41 deletions crates/graph/src/nodes/context/var/versioning.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,28 +54,32 @@ impl ContextVarNode {
}

pub fn global_first_version(&self, analyzer: &impl GraphBackend) -> Self {
let first = self.first_version(analyzer);
if let Some(inherited_from) = analyzer
.graph()
.edges_directed(first.0.into(), Direction::Outgoing)
.filter(|edge| Edge::Context(ContextEdge::InheritedVariable) == *edge.weight())
.map(|edge| ContextVarNode::from(edge.target()))
.take(1)
.next()
{
inherited_from.global_first_version(analyzer)
} else if let Some(input_from) = analyzer
.graph()
.edges_directed(first.0.into(), Direction::Outgoing)
.filter(|edge| Edge::Context(ContextEdge::InputVariable) == *edge.weight())
.map(|edge| ContextVarNode::from(edge.target()))
.take(1)
.next()
{
input_from.global_first_version(analyzer)
} else {
first
let mut global_first = self.first_version(analyzer);

let mut stack = vec![global_first];

while let Some(current_node) = stack.pop() {
let mut pushed = false;
if let Some(target_node) = analyzer
.graph()
.edges_directed(current_node.0.into(), Direction::Outgoing)
.filter(|edge| {
matches!(edge.weight(), Edge::Context(ContextEdge::InheritedVariable) | Edge::Context(ContextEdge::InputVariable))
})
.map(|edge| ContextVarNode::from(edge.target()))
.take(1)
.next() {
global_first = target_node.first_version(analyzer);
stack.push(global_first);
pushed = true;
}

if !pushed {
continue;
}
}

global_first
}

pub fn first_version(&self, analyzer: &impl GraphBackend) -> Self {
Expand Down Expand Up @@ -110,27 +114,32 @@ impl ContextVarNode {
}

pub fn global_curr_version_num(&self, analyzer: &impl GraphBackend) -> usize {
let mut curr_num = self.curr_version_num(analyzer);
if let Some(inherited_from) = analyzer
.graph()
.edges_directed(self.0.into(), Direction::Outgoing)
.filter(|edge| Edge::Context(ContextEdge::InheritedVariable) == *edge.weight())
.map(|edge| ContextVarNode::from(edge.target()))
.take(1)
.next()
{
curr_num += inherited_from.global_curr_version_num(analyzer);
} else if let Some(input_from) = analyzer
.graph()
.edges_directed(self.0.into(), Direction::Outgoing)
.filter(|edge| Edge::Context(ContextEdge::InputVariable) == *edge.weight())
.map(|edge| ContextVarNode::from(edge.target()))
.take(1)
.next()
{
curr_num += input_from.global_curr_version_num(analyzer);
let mut stack = vec![*self];
let mut total_version_num = 0;

while let Some(current_node) = stack.pop() {
total_version_num += current_node.curr_version_num(analyzer);

let mut pushed = false;
if let Some(target_node) = analyzer
.graph()
.edges_directed(current_node.0.into(), Direction::Outgoing)
.filter(|edge| {
matches!(edge.weight(), Edge::Context(ContextEdge::InheritedVariable) | Edge::Context(ContextEdge::InputVariable))
})
.map(|edge| ContextVarNode::from(edge.target()))
.take(1)
.next() {
stack.push(target_node);
pushed = true;
}

if !pushed {
continue;
}
}
curr_num

total_version_num
}

pub fn all_versions(&self, analyzer: &impl GraphBackend) -> Vec<Self> {
Expand Down
24 changes: 20 additions & 4 deletions crates/graph/src/nodes/context/variables.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,10 +39,17 @@ impl ContextNode {
analyzer: &mut impl AnalyzerBackend,
) -> Result<(), GraphError> {
// var.cache_range(analyzer)?;
let name = var.name(analyzer)?;
let vars = &mut self.underlying_mut(analyzer)?.cache.vars;
vars.insert(name, var);
Ok(())
if var.underlying(analyzer)?.is_tmp {
let name = var.display_name(analyzer)?;
let vars = &mut self.underlying_mut(analyzer)?.cache.tmp_vars;
vars.insert(name, var);
Ok(())
} else {
let name = var.name(analyzer)?;
let vars = &mut self.underlying_mut(analyzer)?.cache.vars;
vars.insert(name, var);
Ok(())
}
}

/// Returns whether the context's cache contains a variable (by name)
Expand All @@ -64,6 +71,15 @@ impl ContextNode {
.copied()
}

pub fn tmp_var_by_name(&self, analyzer: &impl GraphBackend, name: &str) -> Option<ContextVarNode> {
self.underlying(analyzer)
.unwrap()
.cache
.tmp_vars
.get(name)
.copied()
}

/// Gets a variable by name or recurses up the relevant scopes/contexts until it is found
pub fn var_by_name_or_recurse(
&self,
Expand Down
21 changes: 18 additions & 3 deletions crates/graph/src/solvers/atoms.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,14 @@ impl AtomOrPart {
}
}

pub fn expect_part(&self) -> Elem<Concrete> {
if let AtomOrPart::Part(part) = self {
part.clone()
} else {
panic!("Expected part, was atom: {self:?}")
}
}

pub fn dependent_on(&self, analyzer: &impl GraphBackend) -> Vec<ContextVarNode> {
match self {
AtomOrPart::Part(e) => e.dependent_on(analyzer),
Expand Down Expand Up @@ -249,13 +257,14 @@ impl Atomize for Elem<Concrete> {
Elem::Arena(_) => self.dearenaize(analyzer).borrow().atoms_or_part(analyzer),
Elem::Concrete(_) | Elem::Reference(_) => AtomOrPart::Part(self.clone()),
Elem::ConcreteDyn(_) => AtomOrPart::Part(self.clone()),
Elem::Expr(expr) => {
// println!("atoms or part: was expr: {:?} {} {:?}", expr.lhs.atoms_or_part(), expr.op.to_string(), expr.rhs.atoms_or_part());
e @ Elem::Expr(expr) => {
// println!("atoms or part was expr: {e}");
match (
expr.lhs.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");
match (l, r) {
(_, Elem::Arena(_)) => todo!(),
(Elem::Arena(_), _) => todo!(),
Expand Down Expand Up @@ -305,7 +314,7 @@ impl Atomize for Elem<Concrete> {
todo!("here4");
}
(Elem::Concrete(_), Elem::Concrete(_)) => {
expr.clone().arenaize(analyzer);
let _ = expr.clone().arenaize(analyzer);
let res = expr.exec_op(true, analyzer).unwrap();
if res == Elem::Expr(expr.clone()) {
AtomOrPart::Part(res)
Expand All @@ -320,12 +329,16 @@ 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)) => {
// println!("part atom");
AtomOrPart::Atom(r_atom.add_lhs(expr.op, l))
}
(AtomOrPart::Atom(l_atoms), AtomOrPart::Atom(r_atoms)) => {
// println!("atom atom");
AtomOrPart::Atom(r_atoms.add_lhs(expr.op, AtomOrPart::Atom(l_atoms)))
}
}
Expand All @@ -346,6 +359,7 @@ impl Atomize for Elem<Concrete> {
Expr(_) => {
// println!("atomized: was expr");
let AtomOrPart::Atom(mut a) = self.atoms_or_part(analyzer) else {
// println!("returning none");
return None;
};
a.update_max_ty();
Expand All @@ -354,6 +368,7 @@ impl Atomize for Elem<Concrete> {
Arena(_) => match &*self.dearenaize(analyzer).borrow() {
e @ Expr(_) => {
let AtomOrPart::Atom(mut a) = e.atoms_or_part(analyzer) else {
// println!("returning none arena");
return None;
};
a.update_max_ty();
Expand Down
Loading

0 comments on commit a1f2d44

Please sign in to comment.