Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat(core): Introduce Graph Invariant checks #87

Merged
merged 13 commits into from
Jul 12, 2024
34 changes: 26 additions & 8 deletions crates/graph/src/graph_elements.rs
Original file line number Diff line number Diff line change
@@ -1,13 +1,24 @@
use crate::elem::Elem;
use crate::{nodes::*, VarType};

use shared::{AnalyzerLike, GraphDot, GraphLike, Heirarchical, NodeIdx, RangeArena};
use shared::{
AnalyzerLike, GraphDot, GraphError, GraphLike, Heirarchical, NodeIdx, RangeArena,
RepresentationErr,
};

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(
&self,
g: &impl GraphBackend,
arena: &RangeArena<Elem<Concrete>>,
) -> Result<Option<RepresentationErr>, GraphError>;
}

pub trait GraphBackend:
GraphLike<Edge = Edge, Node = Node, RangeElem = Elem<Concrete>> + GraphDot
Expand Down Expand Up @@ -391,23 +402,30 @@ 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")
}
}

impl GraphBackend for DummyGraph {}
impl GraphDot for DummyGraph {
type T = Elem<Concrete>;

fn dot_str(&self, _arena: &mut RangeArena<<Self as GraphDot>::T>) -> String {
fn dot_str(&self, _arena: &mut RangeArena<<Self as GraphLike>::RangeElem>) -> String {
// Provide a basic implementation or a placeholder
"digraph DummyGraph {}".to_string()
}

fn cluster_str(
&self,
_arena: &mut RangeArena<Self::T>,
_arena: &mut RangeArena<<Self as GraphLike>::RangeElem>,
_node: NodeIdx,
_cluster_num: &mut usize,
_is_killed: bool,
Expand All @@ -424,14 +442,14 @@ impl GraphDot for DummyGraph {
todo!()
}

fn dot_str_no_tmps(&self, _arena: &mut RangeArena<Self::T>) -> String
fn dot_str_no_tmps(&self, _arena: &mut RangeArena<<Self as GraphLike>::RangeElem>) -> String
where
Self: std::marker::Sized,
{
todo!()
}

fn mermaid_str(&self, _arena: &mut RangeArena<Self::T>) -> String
fn mermaid_str(&self, _arena: &mut RangeArena<<Self as GraphLike>::RangeElem>) -> String
where
Self: std::marker::Sized,
{
Expand Down
2 changes: 2 additions & 0 deletions crates/graph/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,13 @@

mod graph_elements;
mod range;
mod test_command;
mod var_type;

pub mod nodes;
pub mod solvers;

pub use graph_elements::*;
pub use range::*;
pub use test_command::*;
pub use var_type::*;
11 changes: 11 additions & 0 deletions crates/graph/src/nodes/builtin.rs
Original file line number Diff line number Diff line change
Expand Up @@ -110,6 +110,10 @@ impl BuiltInNode {
Ok(self.underlying(analyzer)?.is_indexable())
}

pub fn needs_length(&self, analyzer: &impl GraphBackend) -> Result<bool, GraphError> {
Ok(self.underlying(analyzer)?.needs_length())
}

/// Returns the zero range for this builtin type, i.e. uint256 -> [0, 0]
pub fn zero_range(
&self,
Expand Down Expand Up @@ -353,6 +357,13 @@ impl Builtin {
)
}

pub fn needs_length(&self) -> bool {
matches!(
self,
Builtin::DynamicBytes | Builtin::Array(..) | Builtin::SizedArray(..) | Builtin::String
)
}

/// Checks if self is implicitly castable to another builtin
pub fn implicitly_castable_to(&self, other: &Self) -> bool {
use Builtin::*;
Expand Down
8 changes: 8 additions & 0 deletions crates/graph/src/nodes/concrete.rs
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,10 @@ impl ConcreteNode {
pub fn is_indexable(&self, analyzer: &impl GraphBackend) -> Result<bool, GraphError> {
Ok(self.underlying(analyzer)?.is_indexable())
}

pub fn needs_length(&self, analyzer: &impl GraphBackend) -> Result<bool, GraphError> {
Ok(self.underlying(analyzer)?.needs_length())
}
}

impl From<NodeIdx> for ConcreteNode {
Expand Down Expand Up @@ -284,6 +288,10 @@ impl Concrete {
self.is_dyn() || matches!(self, Concrete::Bytes(..))
}

pub fn needs_length(&self) -> bool {
self.is_dyn()
}

/// Convert a U256 back into it's original type. This is used mostly
/// for range calculations to improve ergonomics. Basically
/// the EVM only operates on U256 words, so most of this should
Expand Down
84 changes: 84 additions & 0 deletions crates/graph/src/nodes/context/invariants.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,84 @@
use std::collections::BTreeSet;

use crate::{
nodes::{Concrete, ContextNode, ContextVarNode},
range::elem::Elem,
ContextEdge, Edge, GraphBackend, RepresentationInvariant,
};
use shared::{ContextReprErr, GraphError, RangeArena, RepresentationErr};

use petgraph::{visit::EdgeRef, Direction};

impl ContextNode {
#[allow(dead_code)]
fn cache_matches_edges(
&self,
g: &impl GraphBackend,
) -> Result<Option<RepresentationErr>, GraphError> {
let mut vars: BTreeSet<_> = self
.underlying(g)?
.cache
.vars
.values()
.cloned()
.collect::<BTreeSet<_>>();
vars.extend(
self.underlying(g)?
.cache
.tmp_vars
.values()
.cloned()
.collect::<BTreeSet<_>>(),
);
let edge_vars: BTreeSet<_> = g
.graph()
.edges_directed(self.0.into(), Direction::Incoming)
.filter(|edge| *edge.weight() == Edge::Context(ContextEdge::Variable))
.map(|e| ContextVarNode::from(e.source()))
.collect::<BTreeSet<_>>();

let diff: Vec<_> = edge_vars.difference(&vars).map(|i| i.0.into()).collect();
if !diff.is_empty() {
Ok(Some(
ContextReprErr::VarCacheErr(self.0.into(), diff).into(),
))
} else {
Ok(None)
}
}

fn variables_invariants(
&self,
g: &impl GraphBackend,
arena: &RangeArena<Elem<Concrete>>,
) -> Result<Vec<RepresentationErr>, GraphError> {
let mut res = vec![];
for var in self.vars(g).values() {
if let Some(err) = var.is_representation_ok(g, arena)? {
res.push(err);
}
}
Ok(res)
}
}

impl RepresentationInvariant for ContextNode {
fn is_representation_ok(
&self,
g: &impl GraphBackend,
arena: &RangeArena<Elem<Concrete>>,
) -> Result<Option<RepresentationErr>, GraphError> {
// if let Some(err) = self.cache_matches_edges(g)? {
// return Ok(Some(err));
// }

let bad_vars = self.variables_invariants(g, arena)?;
if !bad_vars.is_empty() {
return Ok(Some(
ContextReprErr::VarInvariantErr(self.0.into(), bad_vars).into(),
));
}

Ok(None)
}
}
1 change: 1 addition & 0 deletions crates/graph/src/nodes/context/mod.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
mod context_tys;
mod expr_ret;
mod invariants;
mod node;
mod underlying;
mod var;
Expand Down
19 changes: 18 additions & 1 deletion crates/graph/src/nodes/context/node.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
use crate::{
nodes::{Concrete, Context, ContextVarNode, KilledKind},
nodes::{Concrete, Context, ContextVarNode, FunctionNode, KilledKind},
range::elem::Elem,
AnalyzerBackend, AsDotStr, GraphBackend, Node,
};
Expand Down 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 Expand Up @@ -114,6 +115,22 @@ impl ContextNode {
Ok(())
}

/// Propogate that this context has ended up the context graph
pub fn propogate_applied(
&self,
applied: FunctionNode,
analyzer: &mut impl AnalyzerBackend,
) -> Result<(), GraphError> {
let underlying = self.underlying_mut(analyzer)?;
if !underlying.applies.contains(&applied) {
underlying.applies.push(applied);
}
if let Some(parent) = self.underlying(analyzer)?.parent_ctx {
parent.propogate_applied(applied, analyzer)?;
}
Ok(())
}

/// Gets the return nodes for this context
pub fn return_nodes(
&self,
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
Loading
Loading