add support for z3 probes

Author: Philipp15b

Cargo.lock

@@ -76,8 +76,6 @@ libtest-mimic = "0.8.1"
 name = "integration"
 path = "tests/integration.rs"
 harness = false
-
-[profile.release]
 # Unfortunately, adding debug information to release binaries incurs
 # an unacceptable overhead of about 450 megabytes. So we disable it.
 # debug = "line-tables-only"

Cargo.toml

@@ -60,9 +60,10 @@ use ariadne::ReportKind;
 use itertools::Itertools;
 use z3::{
     ast::{Ast, Bool},
-    Config, Context,
+    Config, Context, Goal,
 };
 use z3rro::{
+    probes::ProbeSummary,
     prover::{ProveResult, Prover},
     smtlib::Smtlib,
     util::{PrefixWriter, ReasonUnknown},
@@ -696,6 +697,18 @@ impl<'ctx> SmtVcUnit<'ctx> {
 
         let prover = mk_valid_query_prover(limits_ref, ctx, translate, &self.vc);
 
+        if options.debug_options.probe {
+            let goal = Goal::new(ctx, false, false, false);
+            for assertion in prover.solver().get_assertions() {
+                goal.assert(&assertion);
+            }
+            eprintln!(
+                "Probe results for {}:\n{}",
+                name,
+                ProbeSummary::probe(ctx, &goal)
+            );
+        }
+
         let smtlib = get_smtlib(options, &prover);
         if let Some(smtlib) = &smtlib {
             write_smtlib(&options.debug_options, name, smtlib, None)?;

src/driver.rs

@@ -370,6 +370,10 @@ pub struct DebugOptions {
     /// Enable Z3 tracing for the final SAT check.
     #[arg(long)]
     pub z3_trace: bool,
+
+    /// Run a bunch of probes on the SMT solver.
+    #[arg(long)]
+    pub probe: bool,
 }
 
 #[derive(Debug, Default, Args)]
@@ -815,9 +819,10 @@ fn verify_files_main(
     // If `--no-verify` is set and we don't need to print SMT-LIB or explain the
     // core VC, we can return early.
     if options.debug_options.no_verify
+        && !options.lsp_options.explain_core_vc
+        && !options.debug_options.probe
         && !options.debug_options.print_smt
         && options.debug_options.smt_dir.is_none()
-        && !options.lsp_options.explain_core_vc
     {
         return Ok(true);
     }

src/main.rs

@@ -120,7 +120,7 @@ impl<'a> VisitorMut for Subst<'a> {
 ///
 /// As said in the module description [`crate::vc::subst`], this is the "strict"
 /// and simpler version of the [`crate::opt::unfolder`].
-#[instrument(skip(tcx, e))]
+#[instrument(skip_all)]
 pub fn apply_subst(tcx: &TyCtx, e: &mut Expr, limits_ref: &LimitsRef) -> Result<(), LimitError> {
     let mut subst = Subst::new(tcx, limits_ref);
     subst.visit_expr(e)

src/vc/subst.rs

@@ -44,6 +44,7 @@ Set a memory limit of 16000 megabytes with `--mem 16000`.
 * With the `--print-theorem` flag, Caesar prints the theorem that is encoded into SMT.
 * With the `--print-smt` flag, Caesar prints the SMT-LIB query for each verification task. You can also use `--smt-dir DIR` with a directory `DIR` to have Caesar write the SMT-LIB queries to files in `DIR`.
   * If [`raco read`](https://docs.racket-lang.org/raco/read.html) is installed, Caesar will auto-format the SMT-LIB code with it. This is very useful as Z3's default formatting is really confusing sometimes.
+* With the `--probe` flag, [Caesar will print information from Z3 probes](./debugging.md#z3-probes) to standard error.
 
 ## More Topics
 

website/docs/caesar/README.md

@@ -1,5 +1,5 @@
 ---
-sidebar_position: 4
+sidebar_position: 5
 ---
 
 # Benchmarks

website/docs/caesar/benchmarks.md

@@ -1,7 +1,60 @@
 ---
-sidebar_position: 5
+sidebar_position: 1
 ---
 
 # Debugging
 
-TODO.
+Follow this guide if you are debugging verification with Caesar.
+
+
+## SMT Theories and Incompleteness {#incompleteness}
+
+[Expressions](../heyvl/expressions.md) are the main reason for *incompleteness* of Caesar, i.e. instances Caesar is unable to decide whether a given HeyVL program verifies or not.
+Caesar's incompleteness comes from incompleteness of the underlying SMT solver which is used to prove or disprove verification.
+
+At the moment, Caesar's translation of HeyVL verification problems is rather direct: most expressions are translated as one would intuitively expect.
+If operators have a direct correspondence in [SMT-LIB](https://smt-lib.org/), then we translate directly to those.
+Otherwise, usually only additional simple case distinctions are introduced.
+We have some more explanations in [Section 5 of our paper on HeyVL](https://arxiv.org/pdf/2309.07781#page=23).
+
+As a consequence, it is usually pretty simple to predict which [SMT-LIB theories](https://smt-lib.org/theories.shtml) will be used for the SMT query done by Caesar.
+[Caesar supports Z3 probes](#z3-probes) to help you check in which theory your problem falls.
+Also refer to the [Z3 documentation on arithmetic theories](https://microsoft.github.io/z3guide/docs/theories/Arithmetic/), since a lot of Caesar's reasoning will need arithmetic.
+
+Here are some rules of thumb for (in-)completeness:
+ * Linear integer and real arithmetic (QF_LRA, QF_LIRA) is decidable.
+ * Nonlinear integer arithmetic (QF_NIA) is undecidable.
+ * Nonlinear real arithmetic (QF_NRA) is decidable for algebraic reals.
+ * Quantifiers usually introduce undecidability, although there are [a bunch of strategies and fragments in Z3 that allow decidability](https://microsoft.github.io/z3guide/docs/logic/Quantifiers#model-based-quantifier-instantiation).
+   * In particular, restrictive [quantifier triggers](../heyvl/expressions.md#triggers) can help e-matching prove many instances.
+ * HeyVL's [quantitative quantifiers](../heyvl/expressions.md#quantifiers) (`inf` and `sup`) currently have a very naive default encoding that is problematic for Z3.  If the quantitative quantifiers cannot be eliminated by Caesar's quantifier elimination (QE) procedure, then they are often a cause of nontermination of Caesar.
+   * Quantitative quantifiers also come from the semantics of [`havoc` and `cohavoc`](../heyvl/statements.md#havoc). However, for e.g. the [induction-based proof rules](../proof-rules/induction.md), the HeyVL encodings fall into a fragment where Caesar's QE applies and the generated quantifiers are eliminated.
+ * In practice, the SMT solver can often *prove* correctness, but it often has problems with *refutations* (i.e. providing counter-examples).
+
+
+### Z3 Probes
+
+Caesar supports the use of [Z3's *probes*](https://microsoft.github.io/z3guide/docs/strategies/probes/) to quickly help you determine performance-relevant properties about the SMT query, such as the presence of quantifiers or the theoretical complexity of the problem.
+
+Run Caesar with the `--probe` flag to enable probes.
+Caesar will print an output of the following form to standard error:
+
+```
+Probe results for test.heyvl::test:
+Has quantifiers: false
+Detected theories: NIRA
+ - complexity: Undecidable
+ - rejected theories: LRA, LIA, LIRA, NRA, NIA
+Number of arithmetic constants: 1
+Number of Boolean constants: 4
+Number of bit-vector constants: 0
+Number of constants: 1
+Number of expressions: 71
+```
+
+The tool also tries to compute the complexity class of the problem to help you determine whether a problem is "easy".
+
+## Further Reading
+
+ * [Dafny's guidelines for verification](https://dafny.org/dafny/DafnyRef/DafnyRef.html#sec-verification) can be helpful.
+   Many of the ideas translate pretty much directly to Caesar.

website/docs/caesar/debugging.md

@@ -1,5 +1,5 @@
 ---
-sidebar_position: 3
+sidebar_position: 4
 ---
 
 # Optimizations & Alternative Implementations

website/docs/caesar/optimizations.md

@@ -1,5 +1,5 @@
 ---
-sidebar_position: 2
+sidebar_position: 3
 description: Caesar supports program slicing on the HeyVL intermediate verification language.
 ---