From 53229c4341e4d69237443694583cc90beed620c1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= Date: Wed, 8 Jan 2025 18:30:19 +0100 Subject: [PATCH] Add z3 mitm mode (#104) --- smt-log-parser/Cargo.toml | 1 + smt-log-parser/src/bin/smt-scope-z3.rs | 152 ++++++++++++++++++ .../src/{ => bin/smt-scope}/cmd/args.rs | 0 .../{ => bin/smt-scope}/cmd/dependencies.rs | 0 .../src/{ => bin/smt-scope}/cmd/mod.rs | 0 .../{ => bin/smt-scope}/cmd/reconstruct.rs | 0 .../src/{ => bin/smt-scope}/cmd/redundancy.rs | 0 .../src/{ => bin/smt-scope}/cmd/stats.rs | 0 .../src/{ => bin/smt-scope}/cmd/test.rs | 0 .../src/{ => bin/smt-scope}/main.rs | 0 smt-log-parser/src/parsers/z3/parse.rs | 15 +- 11 files changed, 158 insertions(+), 10 deletions(-) create mode 100644 smt-log-parser/src/bin/smt-scope-z3.rs rename smt-log-parser/src/{ => bin/smt-scope}/cmd/args.rs (100%) rename smt-log-parser/src/{ => bin/smt-scope}/cmd/dependencies.rs (100%) rename smt-log-parser/src/{ => bin/smt-scope}/cmd/mod.rs (100%) rename smt-log-parser/src/{ => bin/smt-scope}/cmd/reconstruct.rs (100%) rename smt-log-parser/src/{ => bin/smt-scope}/cmd/redundancy.rs (100%) rename smt-log-parser/src/{ => bin/smt-scope}/cmd/stats.rs (100%) rename smt-log-parser/src/{ => bin/smt-scope}/cmd/test.rs (100%) rename smt-log-parser/src/{ => bin/smt-scope}/main.rs (100%) diff --git a/smt-log-parser/Cargo.toml b/smt-log-parser/Cargo.toml index 1783aa73..b6ebe68a 100644 --- a/smt-log-parser/Cargo.toml +++ b/smt-log-parser/Cargo.toml @@ -32,6 +32,7 @@ duplicate = "1.0" strum = { version = "0.26", features = ["derive"] } # For the command line interface clap = { version = "4.5.4", features = ["derive"] } +tempfile = "3" [dev-dependencies] memory-stats = "1.1.0" diff --git a/smt-log-parser/src/bin/smt-scope-z3.rs b/smt-log-parser/src/bin/smt-scope-z3.rs new file mode 100644 index 00000000..a6e5be8a --- /dev/null +++ b/smt-log-parser/src/bin/smt-scope-z3.rs @@ -0,0 +1,152 @@ +use smt_log_parser::{ + analysis::{InstGraph, RedundancyAnalysis}, + display_with::{DisplayCtxt, DisplayWithCtxt}, + formatter::TermDisplayContext, + LogParser, Z3Parser, +}; + +fn main() -> Result<(), String> { + let z3_exe = std::env::var("SCOPE_Z3_EXE").unwrap_or_else(|_| "z3".to_string()); + let logfile = std::env::var("SCOPE_LOGFILE"); + + let tempdir; + let logfile = match logfile { + Ok(logfile) => std::path::PathBuf::from(logfile), + Err(_) => { + tempdir = tempfile::tempdir().unwrap(); + let mut tempdir = tempdir.into_path(); + tempdir.push("z3.log"); + tempdir + } + }; + + let mut passed_args = false; + let args = std::env::args().skip(1); + let args = args.filter(|arg| { + passed_args = true; + !arg.starts_with("trace=") + && !arg.starts_with("proof=") + && !arg.starts_with("trace-file-name=") + }); + + let mut cmd = std::process::Command::new(z3_exe) + .args([ + "trace=true", + "proof=true", + &format!("trace-file-name={}", logfile.display()), + ]) + .args(args) + .stdin(std::process::Stdio::inherit()) + .stdout(std::process::Stdio::inherit()) + .stderr(std::process::Stdio::inherit()) + .spawn() + .expect("failed to execute z3"); + if !passed_args { + eprintln!("smt-scope-z3"); + eprintln!("Runs z3 (either from path or specified by the \"SCOPE_Z3_EXE\" environment variable) and upon exit, analyses the logfile for potential issues."); + eprintln!("The logfile is deleted unless the \"SCOPE_LOGFILE\" environment variable is set with a path for where to store it."); + eprintln!("---"); + } + let output = cmd.wait().expect("command wasn't running"); + if let Some(code) = output.code() { + std::process::exit(code); + } + if !logfile.is_file() { + return Ok(()); + } + analyse(logfile) +} + +fn analyse(logfile: std::path::PathBuf) -> Result<(), String> { + let mut warnings = Vec::new(); + let mut errors = Vec::new(); + + let (_metadata, parser) = Z3Parser::from_file(logfile).map_err(|e| e.to_string())?; + let mut parser = parser.process_all().map_err(|e| e.to_string())?; + + let term_display = &mut None; + fn ctxt<'a>( + parser: &'a Z3Parser, + term_display: &'a mut Option, + ) -> DisplayCtxt<'a> { + let term_display = term_display.get_or_insert_with(TermDisplayContext::basic); + DisplayCtxt { + parser, + term_display, + config: Default::default(), + } + } + + let redundancy = RedundancyAnalysis::new(&parser); + let excess = redundancy + .per_quant + .iter_enumerated() + .filter(|(_, data)| data.input_multiplicativity() > 1.0); + let (error, warning) = + excess.partition::, _>(|(_, data)| data.input_multiplicativity() >= 2.0); + if !warning.is_empty() { + let ctxt = ctxt(&parser, term_display); + let warning = warning + .into_iter() + .map(|(idx, _)| idx.with(&ctxt).to_string()) + .collect::>(); + warnings.push(format!( + "{} quantifiers with multiplicativity 1.0-2.0 {warning:?}", + warning.len() + )); + } + if !error.is_empty() { + let ctxt = ctxt(&parser, term_display); + let error = error + .into_iter() + .map(|(idx, _)| idx.with(&ctxt).to_string()) + .collect::>(); + errors.push(format!( + "{} quantifiers with multiplicativity >= 2.0 {error:?}", + error.len() + )); + } + + let mut graph = InstGraph::new_lite(&parser).map_err(|e| format!("{e:?}"))?; + let mls = graph.search_matching_loops(&mut parser); + if mls.maybe_mls > 0 { + let warning = mls + .matching_loops + .iter() + .filter(|ml| ml.graph.is_none()) + .map(|ml| mls.signatures[ml.sig].qpat); + let ctxt = ctxt(&parser, term_display); + let warning = warning + .map(|idx| idx.with(&ctxt).to_string()) + .collect::>(); + warnings.push(format!( + "{} suspicious long repeating chains {warning:?}", + mls.maybe_mls + )); + } + if mls.sure_mls > 0 { + let error = mls + .matching_loops + .iter() + .filter(|ml| ml.graph.is_some()) + .map(|ml| mls.signatures[ml.sig].qpat); + let ctxt = ctxt(&parser, term_display); + let error = error + .map(|idx| idx.with(&ctxt).to_string()) + .collect::>(); + errors.push(format!("{} matching loops {error:?}", mls.sure_mls)); + } + + for warning in &warnings { + eprintln!("warning: {warning}"); + } + for error in &errors { + eprintln!("error: {error}"); + } + + if errors.is_empty() { + Ok(()) + } else { + Err("errors found".to_string()) + } +} diff --git a/smt-log-parser/src/cmd/args.rs b/smt-log-parser/src/bin/smt-scope/cmd/args.rs similarity index 100% rename from smt-log-parser/src/cmd/args.rs rename to smt-log-parser/src/bin/smt-scope/cmd/args.rs diff --git a/smt-log-parser/src/cmd/dependencies.rs b/smt-log-parser/src/bin/smt-scope/cmd/dependencies.rs similarity index 100% rename from smt-log-parser/src/cmd/dependencies.rs rename to smt-log-parser/src/bin/smt-scope/cmd/dependencies.rs diff --git a/smt-log-parser/src/cmd/mod.rs b/smt-log-parser/src/bin/smt-scope/cmd/mod.rs similarity index 100% rename from smt-log-parser/src/cmd/mod.rs rename to smt-log-parser/src/bin/smt-scope/cmd/mod.rs diff --git a/smt-log-parser/src/cmd/reconstruct.rs b/smt-log-parser/src/bin/smt-scope/cmd/reconstruct.rs similarity index 100% rename from smt-log-parser/src/cmd/reconstruct.rs rename to smt-log-parser/src/bin/smt-scope/cmd/reconstruct.rs diff --git a/smt-log-parser/src/cmd/redundancy.rs b/smt-log-parser/src/bin/smt-scope/cmd/redundancy.rs similarity index 100% rename from smt-log-parser/src/cmd/redundancy.rs rename to smt-log-parser/src/bin/smt-scope/cmd/redundancy.rs diff --git a/smt-log-parser/src/cmd/stats.rs b/smt-log-parser/src/bin/smt-scope/cmd/stats.rs similarity index 100% rename from smt-log-parser/src/cmd/stats.rs rename to smt-log-parser/src/bin/smt-scope/cmd/stats.rs diff --git a/smt-log-parser/src/cmd/test.rs b/smt-log-parser/src/bin/smt-scope/cmd/test.rs similarity index 100% rename from smt-log-parser/src/cmd/test.rs rename to smt-log-parser/src/bin/smt-scope/cmd/test.rs diff --git a/smt-log-parser/src/main.rs b/smt-log-parser/src/bin/smt-scope/main.rs similarity index 100% rename from smt-log-parser/src/main.rs rename to smt-log-parser/src/bin/smt-scope/main.rs diff --git a/smt-log-parser/src/parsers/z3/parse.rs b/smt-log-parser/src/parsers/z3/parse.rs index 367987a3..fb3f322a 100644 --- a/smt-log-parser/src/parsers/z3/parse.rs +++ b/smt-log-parser/src/parsers/z3/parse.rs @@ -499,8 +499,7 @@ impl Z3LogParser for Z3Parser { &self.terms[proof_idx], &self.terms, &self.strings, - )?; - Ok(()) + ) } fn attach_meaning<'a>(&mut self, mut l: impl Iterator) -> Result<()> { @@ -537,8 +536,7 @@ impl Z3LogParser for Z3Parser { let idx = self.parse_existing_app(id)?; let idx = self.terms.new_meaning(idx, meaning)?; let meaning = self.terms.meaning(idx).unwrap(); - self.events.new_meaning(idx, meaning, &self.strings)?; - Ok(()) + self.events.new_meaning(idx, meaning, &self.strings) } fn attach_var_names<'a>(&mut self, mut l: impl Iterator) -> Result<()> { @@ -936,8 +934,7 @@ impl Z3LogParser for Z3Parser { let from_cdcl = matches!(self.comm.prev().last_line_kind, LineKind::DecideAndOr); let from_cdcl = from_cdcl || self.stack.is_speculative(); self.stack.new_frame(scope, from_cdcl)?; - self.events.new_push()?; - Ok(()) + self.events.new_push() } fn pop<'a>(&mut self, mut l: impl Iterator) -> Result<()> { @@ -953,18 +950,16 @@ impl Z3LogParser for Z3Parser { let conflict = matches!(self.comm.prev().last_line_kind, LineKind::Conflict); debug_assert_eq!(conflict, self.cdcl.has_conflict()); let from_cdcl = self.stack.pop_frames(num, scope, conflict)?; - self.events.new_pop(num, from_cdcl)?; if conflict { self.cdcl.backtrack(&self.stack)?; } - Ok(()) + self.events.new_pop(num, from_cdcl) } fn begin_check<'a>(&mut self, mut l: impl Iterator) -> Result<()> { let scope = l.next().ok_or(E::UnexpectedNewline)?; let scope = scope.parse::().map_err(E::InvalidFrameInteger)?; self.stack.ensure_height(scope)?; - self.events.new_begin_check()?; - Ok(()) + self.events.new_begin_check() } }