From 4254ffc1e36cf7764d58f56ab97c21b753e7643e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Philipp=20Schro=CC=88er?= Date: Tue, 2 Apr 2024 16:02:08 +0200 Subject: [PATCH] smt: better counter-example printing we now pretty-print values from the smt solver and show their original declaration sites and their declaration kind (e.g. input, mutable, bound, etc.). for the implementation, I also renamed SmtAst to SmtFactory and added an SmtEval trait to z3. --- Cargo.lock | 10 ++ Cargo.toml | 1 + src/ast/decl.rs | 117 ++++++++++++++--------- src/ast/diagnostic.rs | 31 ++++++- src/ast/stmt.rs | 5 +- src/ast/util.rs | 3 +- src/front/parser/grammar.lalrpop | 12 ++- src/front/resolve.rs | 3 +- src/front/tycheck.rs | 13 +-- src/main.rs | 12 ++- src/opt/fuzz_test.rs | 3 +- src/opt/qelim.rs | 6 +- src/opt/unfolder.rs | 10 +- src/procs/spec_call.rs | 2 + src/proof_rules/mciver_ast.rs | 1 + src/proof_rules/omega.rs | 1 + src/proof_rules/util.rs | 4 +- src/smt/mod.rs | 4 +- src/smt/pretty_model.rs | 149 ++++++++++++++++++++++++++++++ src/smt/symbolic.rs | 21 ++++- src/smt/translate_exprs.rs | 4 + src/tyctx.rs | 15 +-- src/vc/subst.rs | 10 +- z3rro/src/eureal/datatype.rs | 31 +++++-- z3rro/src/eureal/mod.rs | 24 +++++ z3rro/src/eureal/pair.rs | 24 ++++- z3rro/src/lib.rs | 19 ++-- z3rro/src/list.rs | 4 +- z3rro/src/model.rs | 153 +++++++++++++++++++++++++++++++ z3rro/src/orders.rs | 6 +- z3rro/src/scope.rs | 8 +- z3rro/src/uint.rs | 18 +++- z3rro/src/ureal.rs | 18 +++- 33 files changed, 622 insertions(+), 120 deletions(-) create mode 100644 src/smt/pretty_model.rs create mode 100644 z3rro/src/model.rs diff --git a/Cargo.lock b/Cargo.lock index fc3726db..94089e3c 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -212,6 +212,7 @@ dependencies = [ "hdrhistogram", "im-rc", "indexmap 1.9.3", + "itertools 0.12.0", "lalrpop", "lalrpop-util", "lit", @@ -837,6 +838,15 @@ dependencies = [ "either", ] +[[package]] +name = "itertools" +version = "0.12.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "25db6b064527c5d482d0423354fcd07a89a2dfe07b67892e62411946db7f07b0" +dependencies = [ + "either", +] + [[package]] name = "itoa" version = "1.0.10" diff --git a/Cargo.toml b/Cargo.toml index e15b2b42..6fe752f8 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -47,6 +47,7 @@ z3rro = { path = "./z3rro" } dashmap = "5.4" im-rc = "15.1.0" cfg-if = "1.0.0" +itertools = "0.12.0" [build-dependencies] lalrpop = "0.19" diff --git a/src/ast/decl.rs b/src/ast/decl.rs index 90534278..ddd7433d 100644 --- a/src/ast/decl.rs +++ b/src/ast/decl.rs @@ -57,7 +57,7 @@ impl DeclKind { impl SimplePretty for DeclKind { fn pretty(&self) -> Doc { match self { - DeclKind::VarDecl(var_decl) => var_decl.pretty(), + DeclKind::VarDecl(var_decl) => var_decl.borrow().pretty_decl(), DeclKind::ProcDecl(proc_decl) => proc_decl.pretty(), DeclKind::DomainDecl(domain_decl) => domain_decl.pretty(), DeclKind::FuncDecl(func_decl) => func_decl.pretty(), @@ -86,9 +86,9 @@ impl SimplePretty for DeclKind { /// Just the name of the [`DeclKind`] to classify different declaration kinds /// and print the name of the kind of declaration to the user. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)] pub enum DeclKindName { - Var, + Var(VarKind), Proc, Domain, Func, @@ -102,7 +102,7 @@ pub enum DeclKindName { impl From<&DeclKind> for DeclKindName { fn from(decl: &DeclKind) -> Self { match decl { - DeclKind::VarDecl(_) => DeclKindName::Var, + DeclKind::VarDecl(decl_ref) => DeclKindName::Var(decl_ref.borrow().kind), DeclKind::ProcDecl(_) => DeclKindName::Proc, DeclKind::DomainDecl(_) => DeclKindName::Domain, DeclKind::FuncDecl(_) => DeclKindName::Func, @@ -142,26 +142,21 @@ impl DeclKindName { pub fn is_proc(self) -> bool { matches!(self, DeclKindName::Proc | DeclKindName::ProcIntrin) } - - /// Print the user-displayable name. - pub fn to_str(self) -> &'static str { - match self { - DeclKindName::Var => "variable", - DeclKindName::Proc => "proc", - DeclKindName::Domain => "domain", - DeclKindName::Func => "func", - DeclKindName::Axiom => "axiom", - DeclKindName::ProcIntrin => "intrinsic proc", - DeclKindName::FuncIntrin => "intrinsic func", - DeclKindName::Label => "label", - DeclKindName::Annotation => "annotation", - } - } } impl Display for DeclKindName { fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { - f.write_str(self.to_str()) + match self { + DeclKindName::Var(kind) => f.write_fmt(format_args!("{} variable", kind)), + DeclKindName::Proc => f.write_str("proc"), + DeclKindName::Domain => f.write_str("domain"), + DeclKindName::Func => f.write_str("func"), + DeclKindName::Axiom => f.write_str("axiom"), + DeclKindName::ProcIntrin => f.write_str("intrinsic proc"), + DeclKindName::FuncIntrin => f.write_str("intrinsic func"), + DeclKindName::Label => f.write_str("label"), + DeclKindName::Annotation => f.write_str("annotation"), + } } } @@ -227,6 +222,9 @@ pub struct VarDecl { pub kind: VarKind, pub init: Option, pub span: Span, + /// If this declaration was created by cloning another variable declaration, + /// we track the original name here. + pub created_from: Option, } impl VarDecl { @@ -238,53 +236,82 @@ impl VarDecl { kind, init: None, span: param.span, + created_from: None, }; DeclRef::new(var_decl) } + + pub fn pretty_stmt(&self) -> Doc { + self.pretty_with_kind("var") + } + + pub fn pretty_decl(&self) -> Doc { + self.pretty_with_kind(self.kind.to_str()) + } + + fn pretty_with_kind(&self, kind: &'static str) -> Doc { + let res = Doc::text(kind) + .append(Doc::space()) + .append(Doc::text(self.name.name.to_string())) + .append(Doc::text(":")) + .append(Doc::space()) + .append(self.ty.pretty()); + if let Some(init) = &self.init { + res.append(Doc::text(" = ")).append(init.pretty()) + } else { + res + } + } + + /// The original name of this declaration, i.e. `created_from` if it is + /// `Some`, else `name`. This is usually the name we want to show to the + /// user. + pub fn original_name(&self) -> Ident { + self.created_from.unwrap_or(self.name) + } } /// What kind of variable is it? -#[derive(Debug, Clone, Copy, PartialEq, Eq)] +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)] pub enum VarKind { - /// Mutable variables - Mut, - /// Constants - Const, - /// Input parameters cannot be modified + /// Input parameters (cannot be modified). Input, - /// Output parameters cannot be accessed in the pre + /// Output parameters (cannot be accessed in the pre). Output, + /// Mutable variables. + Mut, + /// Variables bound by a quantifier. + Quant, + /// Variables from a substitution (cannot be modified). + Subst, + /// Variables for slicing (cannot be modified). + Slice, } impl VarKind { /// Is the user allowed to write this variable? pub fn is_mutable(self) -> bool { - self == VarKind::Mut || self == VarKind::Output + matches!(self, VarKind::Mut | VarKind::Output) } -} -impl SimplePretty for VarDecl { - fn pretty(&self) -> Doc { - let prefix = match self.kind { - VarKind::Mut => "var", - VarKind::Const => "const", + pub fn to_str(&self) -> &'static str { + match self { VarKind::Input => "input", VarKind::Output => "output", - }; - let res = Doc::text(prefix) - .append(Doc::space()) - .append(Doc::text(self.name.name.to_string())) - .append(Doc::text(":")) - .append(Doc::space()) - .append(self.ty.pretty()); - if let Some(init) = &self.init { - res.append(Doc::text(" = ")).append(init.pretty()) - } else { - res + VarKind::Mut => "mutable", + VarKind::Quant => "bound", + VarKind::Subst => "subst", + VarKind::Slice => "slice", } } } +impl Display for VarKind { + fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { + f.write_str(self.to_str()) + } +} + /// A procedure is a callable that has pre- and postconditions. #[derive(Debug, Clone)] pub struct ProcDecl { diff --git a/src/ast/diagnostic.rs b/src/ast/diagnostic.rs index a43bac5c..4c7d504c 100644 --- a/src/ast/diagnostic.rs +++ b/src/ast/diagnostic.rs @@ -116,13 +116,38 @@ impl Files { } pub fn get(&self, file_id: FileId) -> Option<&StoredFile> { - assert_ne!(file_id.0, 0); + assert_ne!(file_id, FileId::DUMMY); self.files.get((file_id.0 - 1) as usize) } pub fn char_span(&self, span: Span) -> CharSpan { self.get(span.file).unwrap().char_span(span) } + + /// Formats the start of the span as a human-readable string. The format is + /// `FILE:LINE:COL`, where `LINE` and `COL` are 1-indexed character offsets + /// into the file. + /// + /// This is the format accepted by e.g. VSCode's terminal to click and jump + /// directly to the location in the file. + /// + /// Returns `None` if the span's file id is [`FileId::DUMMY`]. + pub fn format_span_start(&self, span: Span) -> Option { + if span.file == FileId::DUMMY { + None + } else { + let file = self.get(span.file).unwrap(); + let char_span = file.char_span(span); + let (_line, line_number, col_number) = + file.lines.get_offset_line(char_span.start).unwrap(); + Some(format!( + "{}:{}:{}", + file.path, + line_number + 1, + col_number + 1 + )) + } + } } /// Hacky impl of `Cache` for `Files` so that it only requires a shared reference. @@ -143,11 +168,13 @@ pub enum SpanVariant { Parser, VC, ImplicitCast, + ProcVerify, SpecCall, Encoding, Qelim, Boolify, Subst, + Slicing, } /// A region of source code in some file. @@ -207,11 +234,13 @@ impl fmt::Debug for Span { SpanVariant::Parser => "", SpanVariant::VC => "vc/", SpanVariant::ImplicitCast => "cast/", + SpanVariant::ProcVerify => "verify/", SpanVariant::SpecCall => "spec-call/", SpanVariant::Encoding => "encoding/", SpanVariant::Qelim => "qelim/", SpanVariant::Boolify => "boolify/", SpanVariant::Subst => "subst/", + SpanVariant::Slicing => "slicing/", }; f.write_fmt(format_args!("{}{}-{}", prefix, self.start, self.end)) } diff --git a/src/ast/stmt.rs b/src/ast/stmt.rs index 3313b807..642b6f35 100644 --- a/src/ast/stmt.rs +++ b/src/ast/stmt.rs @@ -101,10 +101,7 @@ impl SimplePretty for StmtKind { let res = match self { StmtKind::Block(stmts) => pretty_block(stmts.pretty()), - StmtKind::Var(decl_ref) => { - let var_decl = decl_ref.borrow(); - var_decl.pretty() - } + StmtKind::Var(decl_ref) => decl_ref.borrow().pretty_stmt(), StmtKind::Assign(lhs, rhs) => Doc::intersperse( lhs.iter().map(|lhs| Doc::as_string(lhs.name)), Doc::text(", "), diff --git a/src/ast/util.rs b/src/ast/util.rs index 37b84a30..616d99fc 100644 --- a/src/ast/util.rs +++ b/src/ast/util.rs @@ -134,9 +134,10 @@ mod test { tcx.declare(crate::ast::DeclKind::VarDecl(DeclRef::new(VarDecl { name: ident, ty: TyKind::Bool, - kind: VarKind::Const, + kind: VarKind::Input, init: None, span: Span::dummy_span(), + created_from: None, }))); let mut expr = builder.binary( BinOpKind::And, diff --git a/src/front/parser/grammar.lalrpop b/src/front/parser/grammar.lalrpop index b040fad8..df408954 100644 --- a/src/front/parser/grammar.lalrpop +++ b/src/front/parser/grammar.lalrpop @@ -86,7 +86,7 @@ QuantOp: QuantOp = { QuantVar: QuantVar = { ":" - => QuantVar::Fresh(DeclRef::new(VarDecl { name, ty: ty, kind: VarKind::Const, init: None, span: span(file, l, r) })) + => QuantVar::Fresh(DeclRef::new(VarDecl { name, ty: ty, kind: VarKind::Quant, init: None, span: span(file, l, r), created_from: None })) } QuantAnn: QuantAnn = { @@ -187,9 +187,9 @@ pub Stmts: Vec = { StmtKind: StmtKind = { => StmtKind::Block(block), "var" ":" "=" - => StmtKind::Var(DeclRef::new(VarDecl { name: ident, ty, kind: VarKind::Mut, init: Some(rhs), span: span(file, l, r) })), + => StmtKind::Var(DeclRef::new(VarDecl { name: ident, ty, kind: VarKind::Mut, init: Some(rhs), span: span(file, l, r), created_from: None })), "var" ":" - => StmtKind::Var(DeclRef::new(VarDecl { name: ident, ty, kind: VarKind::Mut, init: None, span: span(file, l, r) })), + => StmtKind::Var(DeclRef::new(VarDecl { name: ident, ty, kind: VarKind::Mut, init: None, span: span(file, l, r), created_from: None })), > "=" => StmtKind::Assign(lhs, rhs), > => StmtKind::Assign(vec![], call), "havoc" > => StmtKind::Havoc(Direction::Down, vars), @@ -210,7 +210,7 @@ StmtKind: StmtKind = { "if" SymCup "else" => StmtKind::Angelic(block1, block2), "if" "else" => StmtKind::If(cond, block1, block2), "while" => StmtKind::While(cond, block1), - "@" "(" > ")" => StmtKind::Annotation(ident, inputs, Box::new(stmt)), + "@" => StmtKind::Annotation(ident, inputs.unwrap_or_default(), Box::new(stmt)), "label" => StmtKind::Label(ident), } @@ -218,6 +218,10 @@ Block: Block = { "{" "}" => stmts, } +AnnotationInputs: Vec = { + "(" > ")" => inputs, +} + // --------------------------------------- // Declarations diff --git a/src/front/resolve.rs b/src/front/resolve.rs index 33cc11e9..f70c6501 100644 --- a/src/front/resolve.rs +++ b/src/front/resolve.rs @@ -258,9 +258,10 @@ impl<'tcx> VisitorMut for Resolve<'tcx> { let decl = DeclKind::VarDecl(DeclRef::new(VarDecl { name: *ident, ty: TyKind::None, - kind: VarKind::Const, + kind: VarKind::Subst, init: Some(val.clone()), span, + created_from: None, })); self.with_subscope(|this| { this.declare(decl)?; diff --git a/src/front/tycheck.rs b/src/front/tycheck.rs index 5e5b5822..5c92be0f 100644 --- a/src/front/tycheck.rs +++ b/src/front/tycheck.rs @@ -332,15 +332,12 @@ impl TycheckError { TycheckError::CannotAssign { span, lhs_decl } => { let lhs_decl = lhs_decl.borrow(); let lhs = lhs_decl.name; + if lhs_decl.kind.is_mutable() { + unreachable!(); + } Diagnostic::new(ReportKind::Error, *span) .with_message(format!("Cannot assign to variable `{}`", lhs)) - .with_label(Label::new(lhs_decl.span).with_message(match lhs_decl.kind { - VarKind::Mut | VarKind::Output => unreachable!(), - VarKind::Const => format!("`{}` is declared as a constant...", lhs), - VarKind::Input => { - format!("`{}` is declared as an input parameter...", lhs) - } - })) + .with_label(Label::new(lhs_decl.span).with_message(format!("`{}` is declared as {}...", lhs, lhs_decl.kind))) .with_label( Label::new(*span).with_message("... so this assignment is not allowed"), ) @@ -539,7 +536,7 @@ impl<'tcx> VisitorMut for Tycheck<'tcx> { }); }; } - StmtKind::Havoc(_, _) => {} + StmtKind::Havoc(_, _) => {} // TODO: make input vars readable here or throw an error? StmtKind::Assert(_, ref mut expr) => self.try_cast(s.span, self.tcx.spec_ty(), expr)?, StmtKind::Assume(_, ref mut expr) => self.try_cast(s.span, self.tcx.spec_ty(), expr)?, StmtKind::Compare(_, ref mut expr) => { diff --git a/src/main.rs b/src/main.rs index 865c8b9e..d8117b55 100644 --- a/src/main.rs +++ b/src/main.rs @@ -19,7 +19,7 @@ use crate::{ }, front::{resolve::Resolve, tycheck::Tycheck}, opt::{egraph, qelim::Qelim, relational::Relational, unfolder::Unfolder}, - smt::{translate_exprs::TranslateExprs, SmtCtx}, + smt::{pretty_model, translate_exprs::TranslateExprs, SmtCtx}, timing::TimingLayer, tyctx::TyCtx, vc::{subst::apply_subst, vcgen::Vcgen}, @@ -527,7 +527,7 @@ fn verify_files_main( drop(sat_span); // Now let's examine the result. - print_prove_result(result, name, &prover); + print_prove_result(files_mutex, &mut smt_translate, result, name, &prover); write_smtlib(options, smtlib, name, result).unwrap(); @@ -696,13 +696,17 @@ fn expr_eq_infty(vc_expr: Expr) -> Expr { }) } -fn print_prove_result(result: ProveResult, name: &SourceUnitName, prover: &Prover) { +fn print_prove_result<'smt, 'ctx>(files_mutex: &Mutex, smt_translate: &mut TranslateExprs<'smt, 'ctx>, result: ProveResult, name: &SourceUnitName, prover: &Prover<'ctx>) { match result { ProveResult::Proof => println!("{}: Verified.", name), ProveResult::Counterexample => { println!("{}: Counter-example to verification found!", name); if let Some(model) = prover.get_model() { - println!("{:?}", model); + let mut w = Vec::new(); + let files = files_mutex.lock().unwrap(); + let doc = pretty_model(&files, smt_translate, model); + doc.nest(4).render(120, &mut w).unwrap(); + println!(" {}", String::from_utf8(w).unwrap()); }; } ProveResult::Unknown => { diff --git a/src/opt/fuzz_test.rs b/src/opt/fuzz_test.rs index f7b1f51d..980cc465 100644 --- a/src/opt/fuzz_test.rs +++ b/src/opt/fuzz_test.rs @@ -60,9 +60,10 @@ impl ExprGen { tcx.declare(DeclKind::VarDecl(DeclRef::new(VarDecl { name: *name, ty, - kind: VarKind::Const, + kind: VarKind::Input, init: None, span: Span::dummy_span(), + created_from: None, }))) }); } diff --git a/src/opt/qelim.rs b/src/opt/qelim.rs index f6ee2aee..b8f080ff 100644 --- a/src/opt/qelim.rs +++ b/src/opt/qelim.rs @@ -5,7 +5,7 @@ use tracing::debug; use crate::{ ast::{ util::FreeVariableCollector, visit::VisitorMut, BinOpKind, Expr, ExprBuilder, ExprData, - ExprKind, Ident, QuantOpKind, QuantVar, Span, SpanVariant, TyKind, UnOpKind, + ExprKind, Ident, QuantOpKind, QuantVar, Span, SpanVariant, TyKind, UnOpKind, VarKind, }, tyctx::TyCtx, }; @@ -113,6 +113,7 @@ impl<'tcx> Qelim<'tcx> { fn elim_quant(&mut self, span: Span, quant_vars: &[QuantVar], operand: Expr) -> Expr { debug!(span=?span, quant_vars=?quant_vars, "eliminating quantifier"); + let span = span.variant(SpanVariant::Qelim); let idents: Vec = quant_vars .iter() .flat_map(|quant_var| match quant_var { @@ -122,7 +123,8 @@ impl<'tcx> Qelim<'tcx> { .collect(); let builder = ExprBuilder::new(span); builder.subst_by(operand, &idents, |ident| { - let fresh_ident = self.tcx.fresh_var(ident, SpanVariant::Qelim); + let clone_var = self.tcx.clone_var(ident, span, VarKind::Quant); + let fresh_ident = clone_var; builder.var(fresh_ident, self.tcx) }) } diff --git a/src/opt/unfolder.rs b/src/opt/unfolder.rs index d558959c..86dec2cb 100644 --- a/src/opt/unfolder.rs +++ b/src/opt/unfolder.rs @@ -30,7 +30,8 @@ use z3rro::prover::Prover; use crate::{ ast::{ visit::{walk_expr, VisitorMut}, - BinOpKind, Expr, ExprBuilder, ExprData, ExprKind, Shared, Span, Spanned, TyKind, UnOpKind, + BinOpKind, Expr, ExprBuilder, ExprData, ExprKind, Shared, Span, SpanVariant, Spanned, + TyKind, UnOpKind, }, smt::SmtCtx, vc::subst::Subst, @@ -113,6 +114,7 @@ impl<'smt, 'ctx> VisitorMut for Unfolder<'smt, 'ctx> { type Err = (); fn visit_expr(&mut self, e: &mut Expr) -> Result<(), Self::Err> { + let span = e.span; let ty = e.ty.clone().unwrap(); match &mut e.deref_mut().kind { ExprKind::Var(ident) => { @@ -166,7 +168,11 @@ impl<'smt, 'ctx> VisitorMut for Unfolder<'smt, 'ctx> { _ => walk_expr(self, e), }, ExprKind::Quant(_, quant_vars, _, expr) => { - self.subst.push_quant(quant_vars, self.translate.ctx.tcx()); + self.subst.push_quant( + span.variant(SpanVariant::Qelim), + quant_vars, + self.translate.ctx.tcx(), + ); let scope = self.translate.push(); self.prover.push(); diff --git a/src/procs/spec_call.rs b/src/procs/spec_call.rs index 5ca7bb24..7248686e 100644 --- a/src/procs/spec_call.rs +++ b/src/procs/spec_call.rs @@ -154,6 +154,7 @@ impl<'tcx> SpecCall<'tcx> { name: Symbol::intern(&format!("old_{}", param.name)), span, }; + // Reuse an existing declaration if possible. if let Some(_decl) = self.tcx.get(name).as_deref() { let stmt = Spanned::new(span, StmtKind::Assign(vec![name], value)); (stmt, ident_to_expr(self.tcx, span, name)) @@ -172,6 +173,7 @@ impl<'tcx> SpecCall<'tcx> { kind: VarKind::Mut, // we might use the variable again in another proc call init: Some(value), span, + created_from: Some(param.name), }; let decl = DeclRef::new(var_decl); self.tcx.declare(DeclKind::VarDecl(decl.clone())); diff --git a/src/proof_rules/mciver_ast.rs b/src/proof_rules/mciver_ast.rs index cffd6c28..1c7f3ff3 100644 --- a/src/proof_rules/mciver_ast.rs +++ b/src/proof_rules/mciver_ast.rs @@ -97,6 +97,7 @@ impl Encoding for ASTAnnotation { kind: VarKind::Mut, init: None, span: call_span, + created_from: None, }; // Declare the free variable to be used in the omega invariant resolve.declare(DeclKind::VarDecl(DeclRef::new(var_decl)))?; diff --git a/src/proof_rules/omega.rs b/src/proof_rules/omega.rs index e74ee4be..7c30c8f4 100644 --- a/src/proof_rules/omega.rs +++ b/src/proof_rules/omega.rs @@ -86,6 +86,7 @@ impl Encoding for OmegaInvAnnotation { kind: VarKind::Mut, init: None, span: call_span, + created_from: None, }; // Declare the free variable to be used in the omega invariant resolve.declare(DeclKind::VarDecl(DeclRef::new(var_decl)))?; diff --git a/src/proof_rules/util.rs b/src/proof_rules/util.rs index aa0520a0..eeaa1dba 100644 --- a/src/proof_rules/util.rs +++ b/src/proof_rules/util.rs @@ -110,6 +110,7 @@ pub fn new_ident_with_name(tcx: &TyCtx, ty: &TyKind, span: Span, name: &str) -> kind: VarKind::Input, init: None, span, + created_from: None, }; let decl = DeclRef::new(var_decl); tcx.declare(DeclKind::VarDecl(decl)); @@ -142,6 +143,7 @@ pub fn get_init_idents(tcx: &TyCtx, span: Span, idents: &[Ident]) -> Vec kind: VarKind::Input, init: None, span, + created_from: Some(*ident), }; let decl = DeclRef::new(var_decl); tcx.declare(DeclKind::VarDecl(decl.clone())); @@ -207,7 +209,7 @@ pub fn generate_proc( format!("{}_{}", base_proc_ident.name, proc_info.name).as_str(), )); // get a fresh ident to avoid name conflicts - let name = tcx.fresh_ident(ident, SpanVariant::Encoding); + let name = tcx.fresh_ident(ident, ident.span.variant(SpanVariant::Encoding)); let decl = DeclKind::ProcDecl(DeclRef::new(ProcDecl { direction: proc_info.direction, diff --git a/src/smt/mod.rs b/src/smt/mod.rs index 9e3db808..edecf661 100644 --- a/src/smt/mod.rs +++ b/src/smt/mod.rs @@ -3,7 +3,7 @@ use std::{cell::RefCell, collections::HashMap, rc::Rc}; use z3::{ast::Bool, Context, Sort}; -use z3rro::{eureal::EURealSuperFactory, EUReal, Factory, ListFactory}; +use z3rro::{eureal::EURealSuperFactory, EUReal, Factory, ListFactory, SmtInvariant}; use crate::{ ast::{ @@ -15,6 +15,8 @@ use crate::{ use self::{translate_exprs::TranslateExprs, uninterpreted::Uninterpreteds}; +mod pretty_model; +pub use pretty_model::pretty_model; pub mod symbolic; mod symbols; pub mod translate_exprs; diff --git a/src/smt/pretty_model.rs b/src/smt/pretty_model.rs new file mode 100644 index 00000000..e366d60b --- /dev/null +++ b/src/smt/pretty_model.rs @@ -0,0 +1,149 @@ +//! Pretty-printing an SMT model. + +use std::{collections::BTreeMap, rc::Rc}; + +use itertools::Itertools; +use z3::Model; +use z3rro::model::InstrumentedModel; + +use crate::{ + ast::{ + decl::{DeclKind, DeclKindName}, + ExprBuilder, Files, Ident, Span, + }, + pretty::Doc, + smt::translate_exprs::TranslateExprs, +}; + +/// Pretty-print a model. +pub fn pretty_model<'smt, 'ctx>( + files: &Files, + translate: &mut TranslateExprs<'smt, 'ctx>, + model: Model<'ctx>, +) -> Doc { + let mut res: Vec = vec![]; + + let mut model = InstrumentedModel::new(model); + + // objects accessed during vc evaluation do not contribute towards the + // unaccessed list. + model.reset_accessed(); + + // Print the values of the global variables in the model. + pretty_globals(translate, &model, files, &mut res); + + // Print the unaccessed definitions. + res.push(pretty_unaccessed(model)); + + Doc::intersperse(res, Doc::hardline().append(Doc::hardline())) +} + +fn pretty_globals<'smt, 'ctx>( + translate: &mut TranslateExprs<'smt, 'ctx>, + model: &InstrumentedModel<'ctx>, + files: &Files, + res: &mut Vec, +) { + // retrieve the global declarations in the smt translator, sorted by their + // position + // + // TODO: these local idents do not include identifiers for limits such as + // infima and suprema. consequently, those will not be printed in the model. + // we should include those in the future. + let global_decls = translate + .local_idents() + .sorted_by_key(|ident| ident.span.start) + .map(|ident| translate.ctx.tcx.get(ident).unwrap()); + + // now group the declarations by their DeclKindName + let mut decls_by_kind: BTreeMap>> = BTreeMap::new(); + for decl in global_decls { + decls_by_kind + .entry(decl.kind_name()) + .or_default() + .push(decl); + } + + for (kind_name, decls) in decls_by_kind { + let mut lines: Vec = vec![Doc::text(format!("{}s:", kind_name))]; + + for decl_kind in decls { + match &*decl_kind { + DeclKind::VarDecl(decl_ref) => { + let var_decl = decl_ref.borrow(); + let ident = var_decl.name; + + // pretty print the value of this variable + let value = pretty_var(translate, ident, model); + + // pretty print the span of this variable declaration + let span = pretty_span(files, ident); + + lines.push( + Doc::text(format!("{}: ", var_decl.original_name())) + .append(value) + .append(span), + ); + } + _ => {} + } + } + + res.push(Doc::intersperse(lines, Doc::hardline()).nest(4)); + } +} + +fn pretty_var<'smt, 'ctx>( + translate: &mut TranslateExprs<'smt, 'ctx>, + ident: Ident, + model: &InstrumentedModel<'ctx>, +) -> Doc { + let builder = ExprBuilder::new(Span::dummy_span()); + let symbolic = translate.t_symbolic(&builder.var(ident, translate.ctx.tcx)); + let value = match symbolic.eval(model) { + Ok(value) => Doc::text(format!("{}", value)), + Err(err) => Doc::text(format!("({})", err)), + }; + value +} + +fn pretty_span(files: &Files, ident: Ident) -> Doc { + if let Some(text) = files.format_span_start(ident.span) { + let text = format!("({})", text); + let note_len = text.chars().count(); + + // add padding to align the text to the right + let padding = Doc::column(move |col| { + let rest_space = 80_usize + .saturating_sub(4) + .saturating_sub(col) + .saturating_sub(note_len) + .max(4); + Doc::text(" ".repeat(rest_space)) + }); + + padding.append(Doc::text(text)) + } else { + Doc::nil() + } +} + +fn pretty_unaccessed(model: InstrumentedModel<'_>) -> Doc { + let unaccessed: Vec<_> = model.iter_unaccessed().collect(); + if unaccessed.is_empty() { + return Doc::nil(); + } + + let mut lines: Vec = vec![Doc::text("extra definitions:")]; + for decl in unaccessed { + let line = if decl.arity() == 0 { + let value = model.eval(&decl.apply(&[]), true).unwrap(); + format!("{}: {}", decl.name(), value) + } else { + let interp = model.get_func_interp(&decl).unwrap(); + format!("{}: {}", decl.name(), interp) + }; + lines.push(Doc::text(line)); + } + Doc::intersperse(lines, Doc::hardline()).nest(4) +} diff --git a/src/smt/symbolic.rs b/src/smt/symbolic.rs index 844698bc..f1a6900d 100644 --- a/src/smt/symbolic.rs +++ b/src/smt/symbolic.rs @@ -1,11 +1,14 @@ //! Enums to represent all of our supported SMT types. +use std::fmt::Display; + use z3::{ ast::{Bool, Dynamic, Int, Real}, Sort, }; use z3rro::{ eureal, + model::{InstrumentedModel, SmtEval, SmtEvalError}, scope::{SmtFresh, SmtScope}, EUReal, List, SmtInvariant, UInt, UReal, }; @@ -134,8 +137,22 @@ impl<'ctx> Symbolic<'ctx> { } } - /// Call [`SmtInvariant::smt_invariant`] on the underlying value. - pub fn smt_invariant(&self) -> Option> { + pub fn eval(&self, model: &InstrumentedModel<'ctx>) -> Result, SmtEvalError> { + match self { + Symbolic::Bool(v) => v.eval(model).map(|v| Box::new(v) as Box), + Symbolic::Int(v) => v.eval(model).map(|v| Box::new(v) as Box), + Symbolic::UInt(v) => v.eval(model).map(|v| Box::new(v) as Box), + Symbolic::Real(v) => v.eval(model).map(|v| Box::new(v) as Box), + Symbolic::UReal(v) => v.eval(model).map(|v| Box::new(v) as Box), + Symbolic::EUReal(v) => v.eval(model).map(|v| Box::new(v) as Box), + Symbolic::List(_) => Err(SmtEvalError::ParseError), // TODO + Symbolic::Uninterpreted(_) => Err(SmtEvalError::ParseError), // TODO + } + } +} + +impl<'ctx> SmtInvariant<'ctx> for Symbolic<'ctx> { + fn smt_invariant(&self) -> Option> { match self { Symbolic::Bool(v) => v.smt_invariant(), Symbolic::Int(v) => v.smt_invariant(), diff --git a/src/smt/translate_exprs.rs b/src/smt/translate_exprs.rs index ce55fa19..0c48b2af 100644 --- a/src/smt/translate_exprs.rs +++ b/src/smt/translate_exprs.rs @@ -78,6 +78,10 @@ impl<'smt, 'ctx> TranslateExprs<'smt, 'ctx> { scope } + pub fn local_idents<'a>(&'a self) -> impl Iterator + 'a { + self.locals.local_iter().map(|(ident, _)| *ident) + } + pub fn fresh(&mut self, ident: Ident) { self.locals.remove(ident); } diff --git a/src/tyctx.rs b/src/tyctx.rs index 5f54e18a..6110489a 100644 --- a/src/tyctx.rs +++ b/src/tyctx.rs @@ -8,7 +8,7 @@ use std::{ use indexmap::IndexMap; -use crate::ast::{DeclKind, DeclRef, DomainDecl, Ident, LitKind, SpanVariant, Symbol, TyKind}; +use crate::ast::{DeclKind, DeclRef, DomainDecl, Ident, LitKind, Span, Symbol, TyKind, VarKind}; /// This is the central symbol table for the language. It keeps track of all /// definitions, @@ -71,24 +71,25 @@ impl TyCtx { /// Generate a fresh [`Ident`] based on the given [`Ident`]. /// /// Example: Given `x` as input [`Ident`], if `x` already exists than `x_1` is returned as long as `x_1` doesn't exist. - pub fn fresh_ident(&self, ident: Ident, span_variant: SpanVariant) -> Ident { + pub fn fresh_ident(&self, ident: Ident, span: Span) -> Ident { loop { let mut fresh = self.fresh.borrow_mut(); let index = fresh.entry(ident).and_modify(|e| *e += 1).or_insert(0); let new_name = format!("{}_{}", ident.name.to_owned(), index); let new_ident = Ident { name: Symbol::intern(&new_name), - span: ident.span.variant(span_variant), + span, }; if !self.declarations.borrow().contains_key(&new_ident) { return new_ident; } } } - /// Generate a fresh variable declaration from an existing variable declaration. + + /// Generate a fresh variable declaration from an existing variable declaration with the given `var_kind`. /// Uses [`fresh_ident`](fn@fresh_ident) to generate a new name for the variable. - pub fn fresh_var(&self, ident: Ident, span_variant: SpanVariant) -> Ident { - let new_ident = self.fresh_ident(ident, span_variant); + pub fn clone_var(&self, ident: Ident, span: Span, var_kind: VarKind) -> Ident { + let new_ident = self.fresh_ident(ident, span); // now take the old declaration and create a new one with the new name. // this is somewhat involved due to the [`DeclRef`]s everywhere. @@ -98,6 +99,8 @@ impl TyCtx { // clone the underlying struct, _not_ the reference to it! let mut var_decl = var_ref.borrow().clone(); var_decl.name = new_ident; + var_decl.created_from.get_or_insert(ident); + var_decl.kind = var_kind; DeclRef::new(var_decl) } _ => panic!("identifier is not a variable"), diff --git a/src/vc/subst.rs b/src/vc/subst.rs index 87bad250..1f4abbef 100644 --- a/src/vc/subst.rs +++ b/src/vc/subst.rs @@ -13,7 +13,7 @@ use crate::{ ast::{ util::FreeVariableCollector, visit::{walk_expr, VisitorMut}, - Expr, ExprBuilder, ExprKind, Ident, QuantVar, SpanVariant, + Expr, ExprBuilder, ExprKind, Ident, QuantVar, Span, SpanVariant, VarKind, }, tyctx::TyCtx, }; @@ -47,7 +47,7 @@ impl<'a> Subst<'a> { self.cur.substs.insert(ident, expr); } - pub fn push_quant(&mut self, vars: &mut [QuantVar], tcx: &TyCtx) { + pub fn push_quant(&mut self, span: Span, vars: &mut [QuantVar], tcx: &TyCtx) { self.stack.push(self.cur.clone()); for var in vars { let ident = var.name(); @@ -61,7 +61,8 @@ impl<'a> Subst<'a> { // renamed. if self.cur.free_vars.contains(&ident) { - let new_ident = tcx.fresh_var(ident, SpanVariant::Subst); + let new_ident = + tcx.clone_var(ident, span.variant(SpanVariant::Subst), VarKind::Subst); *var = QuantVar::Shadow(new_ident); let builder = ExprBuilder::new(new_ident.span); self.cur.substs.insert(ident, builder.var(new_ident, tcx)); @@ -82,6 +83,7 @@ impl<'a> VisitorMut for Subst<'a> { type Err = (); fn visit_expr(&mut self, e: &mut Expr) -> Result<(), Self::Err> { + let span = e.span; match &mut e.deref_mut().kind { ExprKind::Var(ident) => { if let Some(subst) = self.lookup_var(*ident) { @@ -90,7 +92,7 @@ impl<'a> VisitorMut for Subst<'a> { Ok(()) } ExprKind::Quant(_, ref mut vars, _, ref mut expr) => { - self.push_quant(vars, self.tcx); + self.push_quant(span, vars, self.tcx); self.visit_expr(expr)?; self.pop(); Ok(()) diff --git a/z3rro/src/eureal/datatype.rs b/z3rro/src/eureal/datatype.rs index e7764594..70369110 100644 --- a/z3rro/src/eureal/datatype.rs +++ b/z3rro/src/eureal/datatype.rs @@ -9,21 +9,20 @@ use std::{ use once_cell::unsync; use z3::{ ast::{Ast, Bool, Datatype, Dynamic}, - Context, DatatypeAccessor, DatatypeBuilder, FuncDecl, RecFuncDecl, Sort, -}; - -use crate::{ - forward_binary_op, interpreted::FuncDef, scope::SmtAlloc, Factory, SmtAst, SmtEq, SmtInvariant, - UReal, + Context, DatatypeAccessor, DatatypeBuilder, FuncDecl, Model, RecFuncDecl, Sort, }; use crate::{ + eureal::ConcreteEUReal, + forward_binary_op, + interpreted::FuncDef, + model::{InstrumentedModel, SmtEval, SmtEvalError}, orders::{ smt_max, smt_min, SmtCompleteLattice, SmtGodel, SmtLattice, SmtOrdering, SmtPartialOrd, }, - scope::SmtFresh, + scope::{SmtAlloc, SmtFresh}, uint::UInt, - SmtBranch, + Factory, SmtBranch, SmtEq, SmtFactory, SmtInvariant, UReal, }; /// This structure saves the necessary Z3 objects to construct and work with @@ -174,7 +173,7 @@ impl<'ctx> EUReal<'ctx> { } } -impl<'ctx> SmtAst<'ctx> for EUReal<'ctx> { +impl<'ctx> SmtFactory<'ctx> for EUReal<'ctx> { type FactoryType = Rc>; fn factory(&self) -> Factory<'ctx, Self> { @@ -218,6 +217,20 @@ impl<'ctx> SmtBranch<'ctx> for EUReal<'ctx> { } } +impl<'ctx> SmtEval<'ctx> for EUReal<'ctx> { + type Value = ConcreteEUReal; + + fn eval(&self, model: &InstrumentedModel<'ctx>) -> Result { + let is_infinite = self.is_infinity().eval(model)?; + if is_infinite { + Ok(ConcreteEUReal::Infinity) + } else { + let real = self.get_ureal().eval(model)?; + Ok(ConcreteEUReal::Real(real)) + } + } +} + #[derive(Debug)] struct EURealLateDefs<'ctx> { rplus_le: FuncDef<'ctx>, diff --git a/z3rro/src/eureal/mod.rs b/z3rro/src/eureal/mod.rs index f1a3f6a1..89c6104e 100644 --- a/z3rro/src/eureal/mod.rs +++ b/z3rro/src/eureal/mod.rs @@ -5,6 +5,9 @@ //! everywhere. However, the [`datatype`] representation can be enabled with the //! `datatype-eureal` feature. +use std::fmt::{Display, Formatter}; + +use num::BigRational; use z3::Context; use crate::{Factory, SmtBranch}; @@ -18,6 +21,27 @@ pub type EUReal<'ctx> = pair::EUReal<'ctx>; #[cfg(feature = "datatype-eureal")] pub type EUReal<'ctx> = datatype::EUReal<'ctx>; +/// A concrete extended unsigned real. If it's finite, then it's represented as +/// a [`BigRational`]. Thus, this representation cannot represent all reals, but +/// only the rationals. +/// +/// These values can be created using [`EUReal`]s implementation of the +/// [`z3rro::eval::SmtEval`] trait. +#[derive(Debug)] +pub enum ConcreteEUReal { + Infinity, + Real(BigRational), +} + +impl Display for ConcreteEUReal { + fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { + match self { + ConcreteEUReal::Infinity => f.write_str("∞"), + ConcreteEUReal::Real(rational) => write!(f, "{}", rational), + } + } +} + /// This is just a factory that supports both EUReal types and supports /// retrieval of the factory for the default [`EUReal`] type. pub struct EURealSuperFactory<'ctx> { diff --git a/z3rro/src/eureal/pair.rs b/z3rro/src/eureal/pair.rs index 81fd65eb..cb245312 100644 --- a/z3rro/src/eureal/pair.rs +++ b/z3rro/src/eureal/pair.rs @@ -6,7 +6,8 @@ use std::ops::{Add, Mul, Sub}; use z3::{ast::Bool, Context}; -use crate::{forward_binary_op, scope::SmtAlloc, Factory, SmtAst, SmtEq, SmtInvariant, UReal}; +use crate::model::{InstrumentedModel, SmtEval, SmtEvalError}; +use crate::{forward_binary_op, scope::SmtAlloc, Factory, SmtEq, SmtFactory, SmtInvariant, UReal}; use crate::{ orders::{ @@ -17,6 +18,8 @@ use crate::{ SmtBranch, }; +use super::ConcreteEUReal; + #[derive(Debug, Clone)] pub struct EURealFactory<'ctx> { ctx: &'ctx Context, @@ -79,7 +82,7 @@ impl<'ctx> EUReal<'ctx> { } } -impl<'ctx> SmtAst<'ctx> for EUReal<'ctx> { +impl<'ctx> SmtFactory<'ctx> for EUReal<'ctx> { type FactoryType = EURealFactory<'ctx>; fn factory(&self) -> Factory<'ctx, Self> { @@ -123,6 +126,23 @@ impl<'ctx> SmtBranch<'ctx> for EUReal<'ctx> { } } +impl<'ctx> SmtEval<'ctx> for EUReal<'ctx> { + type Value = ConcreteEUReal; + + fn eval(&self, model: &InstrumentedModel<'ctx>) -> Result { + let is_infinite = self.is_infinite.eval(model)?; + // we evaluate the number even if the value is infinite. this is so the + // instrumented model tracks the access and we don't have a (logically + // falsely) unaccessed value left over in the model. + let real = self.number.eval(model)?; + if is_infinite { + Ok(ConcreteEUReal::Infinity) + } else { + Ok(ConcreteEUReal::Real(real)) + } + } +} + impl<'a, 'ctx> Add<&'a EUReal<'ctx>> for &'a EUReal<'ctx> { type Output = EUReal<'ctx>; diff --git a/z3rro/src/lib.rs b/z3rro/src/lib.rs index ca54e819..f4916304 100644 --- a/z3rro/src/lib.rs +++ b/z3rro/src/lib.rs @@ -19,6 +19,7 @@ pub mod interpreted; pub mod orders; pub mod scope; +pub mod model; pub mod pretty; pub mod prover; mod uint; @@ -39,7 +40,7 @@ use z3::{ }; /// SMT values who have an associated factory to create new values of its type. -pub trait SmtAst<'ctx> { +pub trait SmtFactory<'ctx> { /// The value of the factory type. You'll probably use [`Factory`] most of the time. type FactoryType; @@ -48,12 +49,12 @@ pub trait SmtAst<'ctx> { } /// Type alias for a reference to the the factory type of an [`SmtAst`] type. -pub type Factory<'ctx, T> = >::FactoryType; +pub type Factory<'ctx, T> = >::FactoryType; // Many built-in Z3 AST object trivially implement [`SmtAst`]. macro_rules! z3_smt_ast { ($ty:ident) => { - impl<'ctx> SmtAst<'ctx> for $ty<'ctx> { + impl<'ctx> SmtFactory<'ctx> for $ty<'ctx> { type FactoryType = &'ctx Context; fn factory(&self) -> &'ctx Context { @@ -68,29 +69,25 @@ z3_smt_ast!(Bool); z3_smt_ast!(Int); z3_smt_ast!(Real); -/* -TODO: the following code does not compile because there's a lifetime bug in z3.rs at the moment - #[derive(Debug, Clone)] pub struct ArrayFactory<'ctx> { pub domain: Sort<'ctx>, pub range: Sort<'ctx>, } -impl<'ctx> SmtAst<'ctx> for Array<'ctx> { +impl<'ctx> SmtFactory<'ctx> for Array<'ctx> { type FactoryType = ArrayFactory<'ctx>; fn factory(&self) -> Factory<'ctx, Self> { let sort = self.get_sort(); - ArrayFactory{ + ArrayFactory { domain: sort.array_domain().unwrap(), range: sort.array_range().unwrap(), } } } - */ -impl<'ctx> SmtAst<'ctx> for Dynamic<'ctx> { +impl<'ctx> SmtFactory<'ctx> for Dynamic<'ctx> { type FactoryType = (&'ctx Context, Sort<'ctx>); fn factory(&self) -> Factory<'ctx, Self> { @@ -98,7 +95,7 @@ impl<'ctx> SmtAst<'ctx> for Dynamic<'ctx> { } } -impl<'ctx> SmtAst<'ctx> for Datatype<'ctx> { +impl<'ctx> SmtFactory<'ctx> for Datatype<'ctx> { type FactoryType = (&'ctx Context, Sort<'ctx>); fn factory(&self) -> Factory<'ctx, Self> { diff --git a/z3rro/src/list.rs b/z3rro/src/list.rs index 09911309..11ad0baf 100644 --- a/z3rro/src/list.rs +++ b/z3rro/src/list.rs @@ -10,7 +10,7 @@ use z3::{ use crate::{ orders::SmtPartialOrd, scope::{SmtAlloc, SmtFresh, SmtScope}, - Factory, SmtAst, SmtBranch, SmtEq, SmtInvariant, UInt, + Factory, SmtBranch, SmtEq, SmtFactory, SmtInvariant, UInt, }; #[derive(Debug)] @@ -140,7 +140,7 @@ impl<'ctx> List<'ctx> { } } -impl<'ctx> SmtAst<'ctx> for List<'ctx> { +impl<'ctx> SmtFactory<'ctx> for List<'ctx> { type FactoryType = Rc>; fn factory(&self) -> Factory<'ctx, Self> { diff --git a/z3rro/src/model.rs b/z3rro/src/model.rs new file mode 100644 index 00000000..7126f4b3 --- /dev/null +++ b/z3rro/src/model.rs @@ -0,0 +1,153 @@ +//! SMT objects that can be evaluated in a model to return a concrete SMT type. + +use std::{ + cell::RefCell, + collections::HashSet, + fmt::{self, Display}, +}; + +use num::{BigInt, BigRational}; +use thiserror::Error; +use z3::{ + ast::{Ast, Bool, Dynamic, Int, Real}, + FuncDecl, FuncInterp, Model, +}; + +/// A [`z3::Model`] which keeps track of the accessed constants. This is useful +/// to later print those constants which were not accessed by any of the +/// [`SmtEval`] implementations (e.g. stuff generated by Z3 we don't know +/// about). This way, we can print the whole model and pretty-print everything +/// we know, and then print the rest of the assignments in the model as well. +#[derive(Debug)] +pub struct InstrumentedModel<'ctx> { + model: Model<'ctx>, + // TODO: turn this into a HashSet of FuncDecls when the type implements Hash + accessed_decls: RefCell>, + accessed_exprs: RefCell>>, +} + +impl<'ctx> InstrumentedModel<'ctx> { + pub fn new(model: Model<'ctx>) -> Self { + InstrumentedModel { + model, + accessed_decls: Default::default(), + accessed_exprs: Default::default(), + } + } + + /// Evaluate the given ast node in this model. `model_completion` indicates + /// whether the node should be assigned a value even if it is not present in + /// the model. + pub fn eval>(&self, ast: &T, model_completion: bool) -> Option { + self.add_children_accessed(Dynamic::from_ast(ast)); + let res = self.model.eval(ast, model_completion)?; + Some(res) + } + + /// Get the function interpretation for this `f`. + pub fn get_func_interp(&self, f: &FuncDecl<'ctx>) -> Option> { + self.accessed_decls.borrow_mut().insert(f.name()); + self.model.get_func_interp(f) + } + + /// Add this ast node and all its children to the accessed set. + fn add_children_accessed(&self, ast: Dynamic<'ctx>) { + if ast.is_const() { + self.accessed_decls.borrow_mut().insert(ast.decl().name()); + } else if ast.is_app() { + for child in ast.children() { + // some Z3 expressions might be extremely big because they + // contain big expressions repeatedly. so the following check is + // necessary to avoid walking through these expressions for a + // very long time. + let is_new = self.accessed_exprs.borrow_mut().insert(child.clone()); + if !is_new { + continue; + } + self.add_children_accessed(child); + } + } + } + + /// Iterate over all function declarations that were not accessed using + /// `eval` so far. + pub fn iter_unaccessed(&self) -> impl Iterator> + '_ { + self.model + .iter() + .filter(|decl| !self.accessed_decls.borrow().contains(&decl.name())) + } + + /// Reset the internally tracked accessed declarations and expressions. + pub fn reset_accessed(&mut self) { + self.accessed_decls.borrow_mut().clear(); + self.accessed_exprs.borrow_mut().clear(); + } + + pub fn into_model(self) -> Model<'ctx> { + self.model + } +} + +/// The [`Display`] implementation simply defers to the underlying +/// [`z3::Model`]'s implementation. +impl<'ctx> Display for InstrumentedModel<'ctx> { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + f.write_fmt(format_args!("{}", &self.model)) + } +} + +#[derive(Error, Debug)] +pub enum SmtEvalError { + #[error("solver failed to evaluate a value")] + EvalError, + #[error("could not parse value from solver")] + ParseError, +} + +/// SMT objects that can be evaluated to a concrete value given a model. +pub trait SmtEval<'ctx> { + type Value; + + // TODO: pass a model completion option? + fn eval(&self, model: &InstrumentedModel<'ctx>) -> Result; +} + +impl<'ctx> SmtEval<'ctx> for Bool<'ctx> { + type Value = bool; + + fn eval(&self, model: &InstrumentedModel<'ctx>) -> Result { + model + .eval(self, true) + .ok_or(SmtEvalError::EvalError)? + .as_bool() + .ok_or(SmtEvalError::ParseError) + } +} + +impl<'ctx> SmtEval<'ctx> for Int<'ctx> { + type Value = BigInt; + + fn eval(&self, model: &InstrumentedModel<'ctx>) -> Result { + // TODO: Z3's as_i64 only returns an i64 value. is there something more complete? + let value = model + .eval(self, true) + .ok_or(SmtEvalError::EvalError)? + .as_i64() + .ok_or(SmtEvalError::ParseError)?; + Ok(BigInt::from(value)) + } +} + +impl<'ctx> SmtEval<'ctx> for Real<'ctx> { + type Value = BigRational; + + fn eval(&self, model: &InstrumentedModel<'ctx>) -> Result { + // TODO: Z3's as_real only returns a pair of i64 values. is there something more complete? + let (num, den) = model + .eval(self, false) // TODO + .ok_or(SmtEvalError::EvalError)? + .as_real() + .ok_or(SmtEvalError::ParseError)?; + Ok(BigRational::new(num.into(), den.into())) + } +} diff --git a/z3rro/src/orders.rs b/z3rro/src/orders.rs index c21d6540..ff4b4366 100644 --- a/z3rro/src/orders.rs +++ b/z3rro/src/orders.rs @@ -14,7 +14,7 @@ use z3::{ Pattern, }; -use crate::{scope::SmtAlloc, Factory, SmtAst, SmtInvariant}; +use crate::{scope::SmtAlloc, Factory, SmtFactory, SmtInvariant}; use super::{ scope::{SmtFresh, SmtScope}, @@ -112,7 +112,7 @@ impl<'ctx> SmtPartialOrd<'ctx> for Bool<'ctx> { /// A bounded lattice with top and bottom elements and binary infimum and /// supremum. -pub trait SmtLattice<'ctx>: SmtAst<'ctx> + SmtPartialOrd<'ctx> { +pub trait SmtLattice<'ctx>: SmtFactory<'ctx> + SmtPartialOrd<'ctx> { fn bot(factory: &Factory<'ctx, Self>) -> Self; fn top(factory: &Factory<'ctx, Self>) -> Self; @@ -263,7 +263,7 @@ impl Opp { } } -impl<'ctx, L: SmtAst<'ctx>> SmtAst<'ctx> for Opp { +impl<'ctx, L: SmtFactory<'ctx>> SmtFactory<'ctx> for Opp { type FactoryType = L::FactoryType; fn factory(&self) -> Factory<'ctx, Self> { diff --git a/z3rro/src/scope.rs b/z3rro/src/scope.rs index dd6154c0..1cef6ae1 100644 --- a/z3rro/src/scope.rs +++ b/z3rro/src/scope.rs @@ -7,7 +7,7 @@ use z3::{ Context, Pattern, }; -use crate::{prover::Prover, Factory, SmtAst, SmtInvariant}; +use crate::{prover::Prover, Factory, SmtFactory, SmtInvariant}; /// An SmtScope can be used to construct a quantifier like `forall` or `exists`. /// The scope has a list of bound expressions (usually just variables) and a @@ -87,6 +87,10 @@ impl<'ctx> SmtScope<'ctx> { ) } + pub fn get_bounds(&self) -> impl Iterator> { + self.bounds.iter() + } + /// The Z3 Rust API needs the bounds as a vector of `&dyn Ast<'ctx>` and /// does not accept a vector of [`Dynamic`] references, so we convert that /// here. @@ -144,7 +148,7 @@ impl<'ctx, 'a> SmtAlloc<'ctx, 'a> { /// /// Implementors of this trait should only implement [`SmtFresh::allocate`] and /// users should only use [`SmtFresh::fresh`]. -pub trait SmtFresh<'ctx>: Sized + SmtAst<'ctx> + SmtInvariant<'ctx> { +pub trait SmtFresh<'ctx>: Sized + SmtFactory<'ctx> + SmtInvariant<'ctx> { /// Create a new instance of this type and prefix the created Z3 variable(s) /// with `prefix`. All created Z3 variables must be registered with the /// allocator so that quantification works correctly. diff --git a/z3rro/src/uint.rs b/z3rro/src/uint.rs index 6adb5744..6d477fb2 100644 --- a/z3rro/src/uint.rs +++ b/z3rro/src/uint.rs @@ -1,11 +1,17 @@ use std::ops::{Add, Mul, Sub}; +use num::BigInt; use z3::{ ast::{Ast, Bool, Int}, Context, }; -use crate::{forward_binary_op, scope::SmtAlloc, Factory, SmtAst, SmtInvariant}; +use crate::{ + forward_binary_op, + model::{InstrumentedModel, SmtEval, SmtEvalError}, + scope::SmtAlloc, + Factory, SmtFactory, SmtInvariant, +}; use super::{ orders::{SmtOrdering, SmtPartialOrd}, @@ -39,7 +45,7 @@ impl<'ctx> UInt<'ctx> { } } -impl<'ctx> SmtAst<'ctx> for UInt<'ctx> { +impl<'ctx> SmtFactory<'ctx> for UInt<'ctx> { type FactoryType = &'ctx Context; fn factory(&self) -> Factory<'ctx, Self> { @@ -84,6 +90,14 @@ impl<'ctx> SmtPartialOrd<'ctx> for UInt<'ctx> { } } +impl<'ctx> SmtEval<'ctx> for UInt<'ctx> { + type Value = BigInt; + + fn eval(&self, model: &InstrumentedModel<'ctx>) -> Result { + self.0.eval(model) + } +} + impl<'a, 'ctx> Add<&'a UInt<'ctx>> for &'a UInt<'ctx> { type Output = UInt<'ctx>; diff --git a/z3rro/src/ureal.rs b/z3rro/src/ureal.rs index f8c823f5..68dc144c 100644 --- a/z3rro/src/ureal.rs +++ b/z3rro/src/ureal.rs @@ -1,11 +1,17 @@ use std::ops::{Add, Div, Mul, Sub}; +use num::BigRational; use z3::{ ast::{Ast, Bool, Real}, Context, }; -use crate::{forward_binary_op, scope::SmtAlloc, Factory, SmtAst, SmtInvariant, UInt}; +use crate::{ + forward_binary_op, + model::{InstrumentedModel, SmtEval, SmtEvalError}, + scope::SmtAlloc, + Factory, SmtFactory, SmtInvariant, UInt, +}; use super::{ orders::{SmtOrdering, SmtPartialOrd}, @@ -43,7 +49,7 @@ impl<'ctx> UReal<'ctx> { } } -impl<'ctx> SmtAst<'ctx> for UReal<'ctx> { +impl<'ctx> SmtFactory<'ctx> for UReal<'ctx> { type FactoryType = &'ctx Context; fn factory(&self) -> Factory<'ctx, Self> { @@ -88,6 +94,14 @@ impl<'ctx> SmtPartialOrd<'ctx> for UReal<'ctx> { } } +impl<'ctx> SmtEval<'ctx> for UReal<'ctx> { + type Value = BigRational; + + fn eval(&self, model: &InstrumentedModel<'ctx>) -> Result { + self.0.eval(model) + } +} + impl<'a, 'ctx> Add<&'a UReal<'ctx>> for &'a UReal<'ctx> { type Output = UReal<'ctx>;