Skip to content

Commit

Permalink
Update mem_dbg and fix related bugs
Browse files Browse the repository at this point in the history
  • Loading branch information
JonasAlaif committed Nov 15, 2024
1 parent 21fb204 commit 44f3e85
Show file tree
Hide file tree
Showing 25 changed files with 130 additions and 68 deletions.
2 changes: 1 addition & 1 deletion axiom-profiler-GUI/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ wasm-timer = "0.2"
gloo-timers = { version = "0.3.0", features = ["futures"] }
semver = "1.0"
nucleo-matcher = "0.3.1"
mem_dbg = { version = "0.1.8", features = ["std", "derive"], default-features = false }
mem_dbg = { version = "0.2.4", features = ["std", "derive"], default-features = false }
duplicate = "1.0"

# For random colour generation
Expand Down
2 changes: 1 addition & 1 deletion smt-log-parser/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ num = "0.4"
futures = "0.3"
semver = "1.0"
wasm-timer = "0.2"
mem_dbg = { version = "0.1.8", features = ["std", "derive"], default-features = false, optional = true }
mem_dbg = { version = "0.2.4", features = ["std", "derive"], default-features = false, optional = true }
# Analysis
petgraph = "0.6.4"
roaring = "0.10"
Expand Down
2 changes: 1 addition & 1 deletion smt-log-parser/src/analysis/dependencies.rs
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ impl QuantifierAnalysis {
let qinfo = &mut self_.0[qidx];
let ginst = &inst_graph.raw[iidx];
qinfo.costs += ginst.cost;
for &parent_iidx in &ginst.inst_parents.nodes {
for &parent_iidx in ginst.inst_parents.nodes.iter() {
let parent_inst = &parser.insts[parent_iidx];
let parent_match_ = &parser.insts[parent_inst.match_];
let Some(parent_qidx) = parent_match_.kind.quant_idx() else {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ pub use signature::*;
#[cfg(feature = "mem_dbg")]
use mem_dbg::{MemDbg, MemSize};

use crate::{idx, items::InstIdx, Graph, TiVec};
use crate::{idx, items::InstIdx, BoxSlice, Graph, TiVec};

pub const MIN_MATCHING_LOOP_LENGTH: u32 = 6;

Expand All @@ -29,7 +29,7 @@ pub struct MlData {
pub struct MatchingLoop {
pub sig: MlSigIdx,
pub leaves: MlLeaves,
pub members: Box<[InstIdx]>,
pub members: BoxSlice<InstIdx>,
pub graph: Option<(GenIdx, Option<MlExplanation>)>,
}
pub type MlExplanation = Graph<MLGraphNode, MLGraphEdge>;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,10 @@ use crate::{items::TermIdx, parsers::z3::synthetic::SynthIdx};

use super::MlSignature;

#[cfg(feature = "mem_dbg")]
use mem_dbg::{MemDbg, MemSize};

#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[derive(Debug, Clone, Eq, Hash, PartialEq)]
pub enum MLGraphNode {
QI(MlSignature),
Expand All @@ -11,6 +15,7 @@ pub enum MLGraphNode {
RecurringEquality(SynthIdx, SynthIdx, Option<bool>),
}

#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[derive(Debug, Clone, Eq, Hash, PartialEq)]
pub enum MLGraphEdge {
Blame(usize),
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ impl InstGraph {
let mls = ml_data.matching_loops.len();
for (i, ml) in ml_data.matching_loops.iter().enumerate() {
let mut last = None;
for &member in &ml.members {
for &member in ml.members.iter() {
self.raw[member].part_of_ml.insert(i);
if let Some(last) = last.replace(member) {
for between in MlOutput::others_between(&topo, member, last) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,8 @@ pub struct MlSignature {
/// Instantiation chains which all depend on a single term will have the same
/// `InstParent`.
#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[derive(Clone, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)]
#[cfg_attr(feature = "mem_dbg", copy_type)]
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum InstParent {
Quant(QuantIdx),
Const(ENodeIdx),
Expand Down
11 changes: 8 additions & 3 deletions smt-log-parser/src/analysis/graph/raw.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@ use std::{
ops::{Index, IndexMut},
};

use fxhash::FxHashSet;
#[cfg(feature = "mem_dbg")]
use mem_dbg::{MemDbg, MemSize};
use petgraph::{
Expand All @@ -18,7 +17,7 @@ use crate::{
ENodeIdx, EqGivenIdx, EqTransIdx, EqualityExpl, GraphIdx, InstIdx, StackIdx,
TransitiveExplSegmentKind,
},
DiGraph, FxHashMap, NonMaxU32, Result, Z3Parser,
DiGraph, FxHashMap, FxHashSet, NonMaxU32, Result, Z3Parser,
};

graph_idx!(raw_idx, RawNodeIndex, RawEdgeIndex, RawIx);
Expand Down Expand Up @@ -250,6 +249,7 @@ impl GraphStats {
}
}

#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[derive(Debug, Clone)]
pub struct Node {
state: NodeState,
Expand All @@ -260,16 +260,18 @@ pub struct Node {
kind: NodeKind,
pub inst_parents: NextInsts,
pub inst_children: NextInsts,
pub part_of_ml: fxhash::FxHashSet<usize>,
pub part_of_ml: FxHashSet<usize>,
}

#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum NodeState {
Disabled,
Hidden,
Visible,
}

#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[derive(Debug, Clone, Copy, Default)]
pub struct Depth {
/// What is the shortest path to a root/leaf
Expand All @@ -278,6 +280,7 @@ pub struct Depth {
pub max: u32,
}

#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[derive(Debug, Clone, Default)]
pub struct NextInsts {
/// What are the immediate next instantiation nodes
Expand Down Expand Up @@ -327,6 +330,7 @@ impl Node {
}
}

#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[derive(Debug, Clone, Copy)]
pub enum NodeKind {
/// Corresponds to `ENodeIdx`.
Expand Down Expand Up @@ -401,6 +405,7 @@ impl NodeKind {
}
}

#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[derive(Debug, Clone, Copy)]
pub enum EdgeKind {
/// Instantiation -> ENode
Expand Down
2 changes: 1 addition & 1 deletion smt-log-parser/src/analysis/graph/visible.rs
Original file line number Diff line number Diff line change
Expand Up @@ -180,7 +180,7 @@ impl InstGraph {
if from == NodeIndex::end() {
continue;
}
for &next_inst in &node.inst_children.nodes {
for &next_inst in node.inst_children.nodes.iter() {
let next_inst = next_inst.index(&self.raw);
let to = node_index_map[next_inst.0.index()];
if to == NodeIndex::end() {
Expand Down
8 changes: 7 additions & 1 deletion smt-log-parser/src/display_with.rs
Original file line number Diff line number Diff line change
Expand Up @@ -166,6 +166,12 @@ impl DisplayConfiguration {
#[cfg(not(feature = "display_html"))]
return false;
}
pub fn font_tag(&self) -> bool {
#[cfg(feature = "display_html")]
return self.font_tag;
#[cfg(not(feature = "display_html"))]
return false;
}

pub fn with_html_italic(
&self,
Expand All @@ -180,7 +186,7 @@ impl DisplayConfiguration {
colour: &str,
rest: impl FnMut(&mut fmt::Formatter<'_>) -> fmt::Result,
) -> fmt::Result {
let (tag, attribute) = if self.font_tag {
let (tag, attribute) = if self.font_tag() {
("font", format!("color=\"{colour}\""))
} else {
("span", format!("style=\"color:{colour}\""))
Expand Down
3 changes: 2 additions & 1 deletion smt-log-parser/src/items/enode.rs
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,8 @@ pub struct ENode {
}

#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[derive(Debug)]
#[cfg_attr(feature = "mem_dbg", copy_type)]
#[derive(Debug, Clone, Copy)]
pub struct Equality {
pub(crate) _frame: StackIdx,
pub to: ENodeIdx,
Expand Down
2 changes: 2 additions & 0 deletions smt-log-parser/src/items/equality.rs
Original file line number Diff line number Diff line change
Expand Up @@ -159,6 +159,7 @@ impl TransitiveExpl {
}

#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[cfg_attr(feature = "mem_dbg", copy_type)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
#[derive(Debug, Clone, Copy)]
pub struct TransitiveExplSegment {
Expand All @@ -182,6 +183,7 @@ impl TransitiveExplSegment {
pub type EqGivenUse = (EqGivenIdx, Option<NonMaxU32>);

#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[cfg_attr(feature = "mem_dbg", copy_type)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
#[derive(Debug, Clone, Copy)]
pub enum TransitiveExplSegmentKind {
Expand Down
1 change: 1 addition & 0 deletions smt-log-parser/src/items/idx.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ use mem_dbg::{MemDbg, MemSize};
macro_rules! idx {
($struct:ident, $prefix:tt) => {
#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[cfg_attr(feature = "mem_dbg", copy_type)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
#[derive(Clone, Copy, Eq, PartialEq, PartialOrd, Ord, Hash)]
// Note: we use `u32` since this the file would need to be > ~100GB to
Expand Down
5 changes: 4 additions & 1 deletion smt-log-parser/src/items/inst.rs
Original file line number Diff line number Diff line change
Expand Up @@ -120,8 +120,9 @@ impl MatchKind {
/// - Term: one instantiation produced a term that the other triggered on
/// - Equality: dependency based on an equality.
#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[cfg_attr(feature = "mem_dbg", copy_type)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
#[derive(Debug, Clone)]
#[derive(Debug, Clone, Copy)]
pub enum BlameKind {
Term { term: ENodeIdx },
Equality { eq: EqTransIdx },
Expand Down Expand Up @@ -170,6 +171,7 @@ impl Index<usize> for Blame<'_> {
/// An identifier for a Z3 quantifier instantiation (called "fingerprint" in the original Axiom Profiler).
/// Represented as a 16-digit hexadecimal number in log files.
#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[cfg_attr(feature = "mem_dbg", copy_type)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub struct Fingerprint(pub u64);
Expand Down Expand Up @@ -213,6 +215,7 @@ pub struct Instantiation {

/// A Z3 instantiation.
#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[cfg_attr(feature = "mem_dbg", copy_type)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
#[derive(Debug, Clone, Copy)]
pub enum InstProofLink {
Expand Down
1 change: 1 addition & 0 deletions smt-log-parser/src/items/proof.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ pub struct ProofStep {

#[allow(non_camel_case_types)]
#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[cfg_attr(feature = "mem_dbg", copy_type)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
#[derive(Debug, Clone, Copy, EnumIter)]
/// Taken from
Expand Down
2 changes: 2 additions & 0 deletions smt-log-parser/src/items/stack.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ use core::fmt;
use mem_dbg::{MemDbg, MemSize};

#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[cfg_attr(feature = "mem_dbg", copy_type)]
#[derive(Debug, Clone, Copy)]
pub struct StackFrame {
/// Is this frame definitely from CDCL? If this is false then it may still
Expand All @@ -26,6 +27,7 @@ impl StackFrame {
}

#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[cfg_attr(feature = "mem_dbg", copy_type)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)]
pub struct TimeRange {
start: u32,
Expand Down
2 changes: 2 additions & 0 deletions smt-log-parser/src/items/term.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ pub struct Term {
}

#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[cfg_attr(feature = "mem_dbg", copy_type)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
#[repr(u8)]
Expand Down Expand Up @@ -135,6 +136,7 @@ impl VarNames {

/// Represents an ID string of the form `name#id` or `name#`.
#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[cfg_attr(feature = "mem_dbg", copy_type)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
#[derive(Debug, Clone, Copy, Default, Hash, PartialEq, Eq)]
pub struct TermId {
Expand Down
4 changes: 2 additions & 2 deletions smt-log-parser/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,8 +18,8 @@ mod mem_dbg;

pub use error::{Error, FResult, FatalError, Result};
pub use mem_dbg::{
BigRational, BoxSlice, DiGraph, FxHashMap, Graph, IString, NonMaxU32, NonMaxUsize, StringTable,
TiVec, UnGraph,
BigRational, BoxSlice, DiGraph, FxHashMap, FxHashSet, Graph, IString, NonMaxU32, NonMaxUsize,
StringTable, TiVec, UnGraph,
};
pub use parsers::z3::z3parser::Z3Parser;
pub use parsers::LogParser;
Loading

0 comments on commit 44f3e85

Please sign in to comment.