From 08c875099ccbb6ca4a4f088902434e58677e2112 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= Date: Tue, 7 Jan 2025 17:42:44 +0100 Subject: [PATCH] Properly fix issue #63 (#103) --- .../src/analysis/graph/analysis/mod.rs | 16 +- smt-log-parser/src/analysis/graph/disable.rs | 2 +- smt-log-parser/src/analysis/graph/mod.rs | 11 +- smt-log-parser/src/error.rs | 3 +- smt-log-parser/src/items/inst.rs | 8 +- smt-log-parser/src/parsers/z3/bugs.rs | 185 ++++++++++++++++++ smt-log-parser/src/parsers/z3/egraph.rs | 8 +- smt-log-parser/src/parsers/z3/mod.rs | 1 + smt-log-parser/src/parsers/z3/parse.rs | 74 ++----- smt-log-parser/src/parsers/z3/terms.rs | 44 +---- 10 files changed, 235 insertions(+), 117 deletions(-) create mode 100644 smt-log-parser/src/parsers/z3/bugs.rs diff --git a/smt-log-parser/src/analysis/graph/analysis/mod.rs b/smt-log-parser/src/analysis/graph/analysis/mod.rs index bd1a8852..5e44eec9 100644 --- a/smt-log-parser/src/analysis/graph/analysis/mod.rs +++ b/smt-log-parser/src/analysis/graph/analysis/mod.rs @@ -101,15 +101,15 @@ impl Analysis { } impl InstGraph { - pub fn initialise_first(&mut self, parser: &Z3Parser) { + pub fn initialise_first(&mut self, parser: &Z3Parser, n: usize) { self.initialise_collect(ProofInitialiser::, parser); self.initialise_collect(ProofInitialiser::, parser); self.initialise_cdcl(parser); - self.initialise_default(parser); + self.initialise_default(parser, n); } - pub fn initialise_default(&mut self, parser: &Z3Parser) { + pub fn initialise_default(&mut self, parser: &Z3Parser, n: usize) { let mut reach = BwdReachableAnalysis::::default(); self.analysis.reach = self.topo_analysis(&mut reach); @@ -121,16 +121,16 @@ impl InstGraph { self.initialise_transfer(NextInstsInit::, parser); self.initialise_transfer(NextInstsInit::, parser); - self.analyse(); + self.analyse(n); } - pub fn analyse(&mut self) { + pub fn analyse(&mut self, n: usize) { self.analysis.cost.sorted_to = 0; self.analysis.children.sorted_to = 0; self.analysis.fwd_depth_min.sorted_to = 0; - self.analysis.first_n_cost(&self.raw, 10000); - self.analysis.first_n_children(&self.raw, 10000); - self.analysis.first_n_fwd_depth_min(&self.raw, 10000); + self.analysis.first_n_cost(&self.raw, n); + self.analysis.first_n_children(&self.raw, n); + self.analysis.first_n_fwd_depth_min(&self.raw, n); } } diff --git a/smt-log-parser/src/analysis/graph/disable.rs b/smt-log-parser/src/analysis/graph/disable.rs index fcebba64..595f1724 100644 --- a/smt-log-parser/src/analysis/graph/disable.rs +++ b/smt-log-parser/src/analysis/graph/disable.rs @@ -16,7 +16,7 @@ impl InstGraph { ) { let (_, disabled_changed) = self.raw.reset_disabled_to_raw(f); if disabled_changed { - self.initialise_default(parser); + self.initialise_default(parser, super::DEFAULT_N); } } diff --git a/smt-log-parser/src/analysis/graph/mod.rs b/smt-log-parser/src/analysis/graph/mod.rs index 8b4c83df..6c7f6cfc 100644 --- a/smt-log-parser/src/analysis/graph/mod.rs +++ b/smt-log-parser/src/analysis/graph/mod.rs @@ -16,6 +16,8 @@ pub mod visible; pub use raw::{RawEdgeIndex, RawNodeIndex}; pub use visible::{VisibleEdgeIndex, VisibleNodeIndex}; +const DEFAULT_N: usize = 10000; + #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))] #[derive(Debug)] pub struct InstGraph { @@ -26,6 +28,13 @@ pub struct InstGraph { impl InstGraph { pub fn new(parser: &Z3Parser) -> Result { + Self::new_with_analysis(parser, DEFAULT_N) + } + pub fn new_lite(parser: &Z3Parser) -> Result { + Self::new_with_analysis(parser, 0) + } + + fn new_with_analysis(parser: &Z3Parser, n: usize) -> Result { let mut raw = RawInstGraph::new(parser)?; let subgraphs = raw.partition()?; let analysis = Analysis::new(subgraphs.in_subgraphs())?; @@ -34,7 +43,7 @@ impl InstGraph { subgraphs, analysis, }; - self_.initialise_first(parser); + self_.initialise_first(parser, n); Ok(self_) } diff --git a/smt-log-parser/src/error.rs b/smt-log-parser/src/error.rs index 96e94e6e..a8376e46 100644 --- a/smt-log-parser/src/error.rs +++ b/smt-log-parser/src/error.rs @@ -56,8 +56,9 @@ pub enum Error { InvalidQVarInteger(ParseIntError), NewMatchOnLambda(QuantIdx), UnknownPatternIdx(TermIdx), - SubpatTooManyBlame(TermId), SubpatTooFewBlame(usize), + // Z3 BUG: https://github.com/viperproject/axiom-profiler-2/issues/63 + SubpatUnknownBlame(String), // Inst discovered /// theory-solving non-rewrite axiom should blame valid enodes diff --git a/smt-log-parser/src/items/inst.rs b/smt-log-parser/src/items/inst.rs index 7b4f738c..2b1339e1 100644 --- a/smt-log-parser/src/items/inst.rs +++ b/smt-log-parser/src/items/inst.rs @@ -32,6 +32,7 @@ impl Match { .flat_map(|(idx, blame)| matches!(blame, BlameKind::Term { .. }).then(|| idx)) .chain([self.blamed.len()]); let mut last = terms.next().unwrap_or_default(); + debug_assert_eq!(last, 0); terms.map(move |idx| { let slice = &self.blamed[last..idx]; last = idx; @@ -136,10 +137,9 @@ impl MatchKind { #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub enum BlameKind { Term { term: ENodeIdx }, - // See https://github.com/viperproject/axiom-profiler-2/issues/63 - // sometimes we need to ignore a blamed term. - IgnoredTerm { term: ENodeIdx }, Equality { eq: EqTransIdx }, + // Z3 BUG: https://github.com/viperproject/axiom-profiler-2/issues/63 + TermBug { term: ENodeIdx }, } impl BlameKind { pub(crate) fn term(&self) -> Option<&ENodeIdx> { @@ -151,7 +151,7 @@ impl BlameKind { pub(crate) fn equality(&self) -> Option> { match self { Self::Equality { eq } => Some(Ok(eq)), - Self::IgnoredTerm { term } => Some(Err(term)), + Self::TermBug { term } => Some(Err(term)), _ => None, } } diff --git a/smt-log-parser/src/parsers/z3/bugs.rs b/smt-log-parser/src/parsers/z3/bugs.rs new file mode 100644 index 00000000..dbca44b2 --- /dev/null +++ b/smt-log-parser/src/parsers/z3/bugs.rs @@ -0,0 +1,185 @@ +#[cfg(feature = "mem_dbg")] +use mem_dbg::{MemDbg, MemSize}; + +use crate::{ + items::{BlameKind, ENodeIdx, Term, TermId, TermIdx}, + Error as E, FxHashSet, IString, Result, StringTable, +}; + +use super::{terms::Terms, Z3Parser}; + +// Z3 BUG: https://github.com/viperproject/axiom-profiler-2/issues/63 + +impl Z3Parser { + pub(super) fn can_blame_match_subpat(&self, blame: ENodeIdx, subpat: TermIdx) -> bool { + self[self[blame].owner].kind == self[subpat].kind + } + + /// Fixes the blame vector which may be incorrect due the Z3 BUG. + pub(super) fn fix_blamed(&self, blamed: &mut [BlameKind], pattern: &Term) -> Result<()> { + debug_assert!(!pattern.child_ids.is_empty()); + let mut b_roots = blamed.iter().filter_map(|b| b.term()); + let mut no_bug = true; + for (i, subpat) in pattern.child_ids.iter().enumerate() { + let Some(root) = b_roots.next() else { + return Err(E::SubpatTooFewBlame(pattern.child_ids.len() - i)); + }; + no_bug &= self.can_blame_match_subpat(*root, *subpat); + } + let too_many = b_roots.next().is_some(); + if no_bug && !too_many { + debug_assert!(blamed[0].term().is_some()); + return Ok(()); + } + let mut root_count = pattern.child_ids.len() + too_many as usize + b_roots.count(); + debug_assert!(root_count >= pattern.child_ids.len()); + self.disable_obvious_blamed_bugs(blamed, pattern, &mut root_count); + + let b = blamed.iter().enumerate(); + let b_roots: Vec<_> = b + .filter_map(|(i, b)| Some(i).zip(b.term().copied())) + .collect(); + debug_assert_eq!(b_roots.len(), root_count); + + let mut valid_rotation = None; + let mut skipped = Vec::new(); + for offset in 0..b_roots.len() { + if !self.can_blame_match_subpat(b_roots[offset].1, pattern.child_ids[0]) { + continue; + } + let can_skip = b_roots.len() - pattern.child_ids.len(); + let idx = |i| b_roots[(offset + i) % b_roots.len()]; + let mut ok = true; + 'outer: for (i, &sp) in pattern.child_ids.iter().enumerate().skip(1) { + while !self.can_blame_match_subpat(idx(skipped.len() + i).1, sp) { + if skipped.len() == can_skip { + ok = false; + break 'outer; + } + skipped.push(skipped.len() + i); + } + } + if ok { + valid_rotation.replace(offset); + let mut skip = |i| { + let i = idx(i).0; + let b = &mut blamed[i]; + let term = *b.term().unwrap(); + *b = BlameKind::TermBug { term }; + root_count -= 1; + }; + for &i in &skipped { + skip(i); + } + for i in 0..(can_skip - skipped.len()) { + skip(skipped.len() + pattern.child_ids.len() + i); + } + debug_assert_eq!(root_count, pattern.child_ids.len()); + break; + // To error on ambiguous replace the above block with: + // let old = valid_rotation.replace(offset); + // if let Some(old) = old { + // return Err(E::SubpatAmbiguousBlame(old, offset)); + // } + } + skipped.clear(); + } + + let Some(rotation) = valid_rotation else { + let name = |t: TermIdx| &self[self[t].kind.app_name().unwrap()]; + let blamed = blamed.iter().filter_map(|b| match *b { + BlameKind::Term { term } => Some((true, term)), + BlameKind::Equality { .. } => None, + BlameKind::TermBug { term } => Some((false, term)), + }); + let blamed = blamed.map(|(r, t)| format!("{r} {}", name(self[t].owner))); + let pattern = pattern.child_ids.iter().copied(); + let s = format!( + "Blamed: [{}] | Subpats: [{}]", + blamed.collect::>().join(", "), + pattern.map(name).collect::>().join(", "), + ); + return Err(E::SubpatUnknownBlame(s)); + }; + let rotation = b_roots[rotation].0; + blamed.rotate_left(rotation); + debug_assert!(blamed[0].term().is_some()); + Ok(()) + } + + fn disable_obvious_blamed_bugs( + &self, + blamed: &mut [BlameKind], + pattern: &Term, + root_count: &mut usize, + ) { + if pattern.child_ids.len() == *root_count { + return; + } + let roots = pattern + .child_ids + .iter() + .map(|&sp| self[sp].kind.app_name().unwrap()) + .collect::>(); + for b in blamed.iter_mut() { + let BlameKind::Term { term } = *b else { + continue; + }; + let root = self[self[term].owner].kind.app_name().unwrap(); + if roots.contains(&root) { + continue; + } + *b = BlameKind::TermBug { term }; + *root_count -= 1; + } + } +} + +// Z3 BUG: https://github.com/viperproject/axiom-profiler-2/issues/100 + +#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))] +#[derive(Debug, Default)] +pub(super) struct TermsBug { + /// Solve bug by switching to an artificial namespace after a "string" mk_app. + get_model: Option, + get_model_idx: u32, +} + +impl Terms { + /// Normally one would use `app_terms.parse_existing_id`, but here we + /// implement the workaround for `get_model`. + pub fn parse_app_child_id(&self, strings: &mut StringTable, id: &str) -> Result { + let mut term_id = TermId::parse(strings, id)?; + if let Some(namespace) = self.bug.get_model { + debug_assert!(term_id.namespace.is_none()); + term_id.namespace = Some(namespace); + } + self.get_app_term_bug(term_id) + } + + pub fn check_get_model(&mut self, id: &mut TermId, name: &str, strings: &mut StringTable) { + let bug = &mut self.bug; + let get_model = bug.get_model.take(); + if id.namespace.is_some() { + return; + } + // See https://github.com/Z3Prover/z3/blob/z3-4.13.4/src/ast/format.cpp#L45-L52 + let Some(get_model) = get_model else { + // Is a mk_app line with this term the start of a get-model command? + if name == "string" { + let namespace = format!("get-model-{}", bug.get_model_idx); + bug.get_model_idx += 1; + bug.get_model = Some(IString(strings.get_or_intern(namespace))); + id.namespace = bug.get_model; + } + return; + }; + match name { + "string" | "cr" | "compose" | "indent" | "choice" => { + bug.get_model = Some(get_model); + id.namespace = Some(get_model); + } + _ => (), + } + } +} diff --git a/smt-log-parser/src/parsers/z3/egraph.rs b/smt-log-parser/src/parsers/z3/egraph.rs index e4e419e0..f862f190 100644 --- a/smt-log-parser/src/parsers/z3/egraph.rs +++ b/smt-log-parser/src/parsers/z3/egraph.rs @@ -190,12 +190,12 @@ impl EGraph { to: ENodeIdx, stack: &Stack, can_mismatch: impl Fn(&EGraph) -> bool, - ) -> Result> { + ) -> Result> { if from == to { - Ok(None) + Ok(Err(from)) } else { self.construct_trans_equality(from, to, stack, can_mismatch) - .map(Some) + .map(Ok) } } @@ -402,7 +402,7 @@ impl EGraph { let mut use_ = Vec::new(); use_.try_reserve_exact(arg_eqs.len())?; for (from, to) in args { - let Some(trans) = self.new_trans_equality(from, to, stack, |_| false)? else { + let Ok(trans) = self.new_trans_equality(from, to, stack, |_| false)? else { continue; }; use_.push(trans); diff --git a/smt-log-parser/src/parsers/z3/mod.rs b/smt-log-parser/src/parsers/z3/mod.rs index f89c0124..17bb80ad 100644 --- a/smt-log-parser/src/parsers/z3/mod.rs +++ b/smt-log-parser/src/parsers/z3/mod.rs @@ -3,6 +3,7 @@ use std::fmt::Debug; use super::{LogParser, LogParserHelper}; use crate::{Error, FResult, Result}; +mod bugs; pub mod egraph; pub mod inst; pub mod inter_line; diff --git a/smt-log-parser/src/parsers/z3/parse.rs b/smt-log-parser/src/parsers/z3/parse.rs index ffaafb5d..367987a3 100644 --- a/smt-log-parser/src/parsers/z3/parse.rs +++ b/smt-log-parser/src/parsers/z3/parse.rs @@ -175,7 +175,7 @@ impl Z3Parser { fn parse_trans_equality( &mut self, can_mismatch: bool, - ) -> impl FnMut(&str, &str) -> Result> + '_ { + ) -> impl FnMut(&str, &str) -> Result> + '_ { move |from, to| { let from = self.parse_existing_enode(from)?; let to = self.parse_existing_enode(to)?; @@ -203,14 +203,12 @@ impl Z3Parser { &mut self, l: impl Iterator, can_mismatch: bool, - mut f: impl FnMut(EqTransIdx) -> Result<()>, + mut f: impl FnMut(core::result::Result) -> Result<()>, ) -> Result<()> { let mut pte = self.parse_trans_equality(can_mismatch); for t in Self::gobble_tuples::(l) { let (from, to) = t?; - let Some(trans) = pte(from, to)? else { - continue; - }; + let trans = pte(from, to)?; f(trans)?; } Ok(()) @@ -371,10 +369,6 @@ impl Z3Parser { let bool_lit = lit.parse::().map_err(E::InvalidBoolLiteral)?; Ok(Some((Some(bool_lit), value))) } - - fn can_blame_match_subpat(&self, blame: ENodeIdx, subpat: TermIdx) -> bool { - self[self[blame].owner].kind == self[subpat].kind - } } impl Z3LogParser for Z3Parser { @@ -691,40 +685,12 @@ impl Z3LogParser for Z3Parser { bound_terms, } }; - // Z3 BUG: https://github.com/viperproject/axiom-profiler-2/issues/63 - let pat = kind.quant_pat().unwrap(); - let pat = self.get_pattern_term(pat).unwrap(); - // SAFETY: we do not mutate the `terms` field of `self`. - let subpats_slice = unsafe { &*(&*pat.child_ids as *const [TermIdx]) }; - debug_assert!(!subpats_slice.is_empty()); - let mut subpats = subpats_slice.iter(); - let mut last = None; - let mut blamed = Vec::new(); let mut next = l.next(); while let Some(word) = next.take() { let term = self.parse_existing_enode(word)?; blamed.try_reserve(1)?; - // Does `blamed.push(BlameKind::Term { term })` - if let Some(next) = subpats.as_slice().first() { - // If there are still more subpatterns to match, check if this - // blame is valid for the next one. - if self.can_blame_match_subpat(term, *next) { - blamed.push(BlameKind::Term { term }); - last = Some(*subpats.next().unwrap()); - } else { - // Ignore this term, only appears due to the above z3 bug. - blamed.push(BlameKind::IgnoredTerm { term }); - } - } else { - // We have already matched the last subpattern - if let Some(last) = last { - if self.can_blame_match_subpat(term, last) { - return Err(E::SubpatTooManyBlame(self[self[term].owner].id)); - } - } - blamed.push(BlameKind::IgnoredTerm { term }); - } + blamed.push(BlameKind::Term { term }); // `append_trans_equality_tuples` would gobble the next term otherwise, so capture it instead. let l = l.by_ref().take_while(|s| { let cond = s.as_bytes().first().is_some_and(|f| *f == b'(') @@ -735,39 +701,27 @@ impl Z3LogParser for Z3Parser { cond }); self.append_trans_equality_tuples(l, true, |eq| { - blamed.try_reserve(1)?; - blamed.push(BlameKind::Equality { eq }); + if let Ok(eq) = eq { + blamed.try_reserve(1)?; + blamed.push(BlameKind::Equality { eq }); + } Ok(()) })?; } - // Related to the bug. Sometimes z3 lists the last subpat blame first. - // In this case rotate it to the end and set it as valid. - if let [rem_sp] = subpats.as_slice() { - if let Some(BlameKind::IgnoredTerm { term }) = blamed.first().copied() { - if self.can_blame_match_subpat(term, *rem_sp) { - let to_move = blamed.iter().position(|b| b.term().is_some()); - let to_move = to_move.unwrap_or(blamed.len()); - blamed.rotate_left(to_move); - let new_idx = blamed.len() - to_move; - debug_assert_eq!(blamed[new_idx], BlameKind::IgnoredTerm { term }); - blamed[new_idx] = BlameKind::Term { term }; - subpats.next(); - } - } - } - if !subpats.as_slice().is_empty() { - return Err(E::SubpatTooFewBlame(subpats.as_slice().len())); - } + + let pat = kind.quant_pat().unwrap(); + let pat = self.get_pattern_term(pat).unwrap(); + self.fix_blamed(&mut blamed, pat)?; let match_ = Match { kind, blamed: blamed.into(), frame: self.stack.active_frame(), }; - debug_assert_eq!(match_.pattern_matches().count(), subpats_slice.len()); + debug_assert_eq!(match_.pattern_matches().count(), pat.child_ids.len()); debug_assert!(match_ .pattern_matches() - .zip(subpats_slice) + .zip(pat.child_ids.iter()) .all(|(m, s)| self.can_blame_match_subpat(m.enode(), *s))); self.insts.new_match(fingerprint, match_)?; Ok(()) diff --git a/smt-log-parser/src/parsers/z3/terms.rs b/smt-log-parser/src/parsers/z3/terms.rs index e881def9..7883944e 100644 --- a/smt-log-parser/src/parsers/z3/terms.rs +++ b/smt-log-parser/src/parsers/z3/terms.rs @@ -10,9 +10,11 @@ use crate::{ InstProofLink, Instantiation, Meaning, ProofIdx, ProofStep, ProofStepKind, QuantIdx, Term, TermId, TermIdToIdxMap, TermIdx, TermKind, }, - Error, FxHashMap, IString, Result, StringTable, TiVec, + Error, FxHashMap, Result, StringTable, TiVec, }; +use super::bugs::TermsBug; + pub trait HasTermId { fn term_id(&self) -> TermId; } @@ -150,10 +152,7 @@ pub struct Terms { pub(super) proof_terms: TermStorage, meanings: FxHashMap, - /// See https://github.com/viperproject/axiom-profiler-2/issues/100. Solve - /// this by switching to an artificial namespace after a "string" mk_app. - get_model: Option, - get_model_idx: u32, + pub(super) bug: TermsBug, } impl Terms { @@ -257,44 +256,13 @@ impl Terms { self.is_true_const(tidx) || self.is_false_const(tidx) } - /// Normally one would use `app_terms.parse_existing_id`, but here we - /// implement the workaround for `get_model`. - pub fn parse_app_child_id(&self, strings: &mut StringTable, id: &str) -> Result { - let mut term_id = TermId::parse(strings, id)?; - if let Some(namespace) = self.get_model { - debug_assert!(term_id.namespace.is_none()); - term_id.namespace = Some(namespace); - } + /// Used only to give access to the `app_terms` field in `bugs.rs`. + pub(super) fn get_app_term_bug(&self, term_id: TermId) -> Result { self.app_terms .get_term(term_id) .into_result() .map_err(Error::UnknownId) } - - pub fn check_get_model(&mut self, id: &mut TermId, name: &str, strings: &mut StringTable) { - let get_model = self.get_model.take(); - if id.namespace.is_some() { - return; - } - // See https://github.com/Z3Prover/z3/blob/z3-4.13.4/src/ast/format.cpp#L45-L52 - let Some(get_model) = get_model else { - // Is a mk_app line with this term the start of a get-model command? - if name == "string" { - let namespace = format!("get-model-{}", self.get_model_idx); - self.get_model_idx += 1; - self.get_model = Some(IString(strings.get_or_intern(namespace))); - id.namespace = self.get_model; - } - return; - }; - match name { - "string" | "cr" | "compose" | "indent" | "choice" => { - self.get_model = Some(get_model); - id.namespace = Some(get_model); - } - _ => (), - } - } } impl std::ops::Index for Terms {