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.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"

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<Expr>,
     pub span: Span,
+    /// If this declaration was created by cloning another variable declaration,
+    /// we track the original name here.
+    pub created_from: Option<Ident>,
 }
 
 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 {

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<String> {
+        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))
     }

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(", "),

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,

src/front/parser/grammar.lalrpop

@@ -86,7 +86,7 @@ QuantOp: QuantOp = {
 
 QuantVar: QuantVar = {
     <l: @L> <name: Ident> ":" <ty: Ty> <r: @R> 
-        => 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<Stmt> = {
 StmtKind: StmtKind = {
     <block: Block> => StmtKind::Block(block),
     <l: @L> "var" <ident: Ident> ":" <ty: Ty> "=" <rhs: Expr> <r: @R> 
-        => 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 })),
     <l: @L> "var" <ident: Ident> ":" <ty: Ty> <r: @R> 
-        => 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 })),
     <lhs: CommaPlus<Ident>> "=" <rhs: Expr> => StmtKind::Assign(lhs, rhs),
     <call: ExprTier<ExprCall>> => StmtKind::Assign(vec![], call),
     "havoc" <vars: CommaPlus<Ident>> => StmtKind::Havoc(Direction::Down, vars),
@@ -210,14 +210,18 @@ StmtKind: StmtKind = {
     "if" SymCup <block1: Block> "else" <block2: Block> => StmtKind::Angelic(block1, block2),
     "if" <cond: Expr> <block1: Block> "else" <block2: Block> => StmtKind::If(cond, block1, block2),
     "while" <cond: Expr> <block1: Block> => StmtKind::While(cond, block1),
-    "@" <ident: Ident> "(" <inputs: Comma<Expr>> ")" <stmt: Stmt> => StmtKind::Annotation(ident, inputs, Box::new(stmt)),
+    "@" <ident: Ident> <inputs: AnnotationInputs?> <stmt: Stmt> => StmtKind::Annotation(ident, inputs.unwrap_or_default(), Box::new(stmt)),
     "label" <ident: Ident> => StmtKind::Label(ident),
 }
 
 Block: Block = {
     "{" <stmts: Stmts> "}" => stmts,
 }
 
+AnnotationInputs: Vec<Expr> = {
+    "(" <inputs: Comma<Expr>> ")" => inputs,
+}
+
 // ---------------------------------------
 // Declarations
 

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)?;

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) => {