smt: eval values atomically to gracefully handle things we cannot

prettyprint

Cargo.toml

@@ -17,7 +17,7 @@ datatype-eureal = ["z3rro/datatype-eureal"]
 datatype-eureal-funcs = ["z3rro/datatype-eureal-funcs"]
 static-link-z3 = ["z3/static-link-z3"]
 # Emit log messages to stderr without timing information. This is useful to diff logs.
-log-print-timeless = [] 
+log-print-timeless = []
 
 [dependencies]
 string-interner = "0.12"
@@ -45,7 +45,7 @@ indexmap = "1.9"
 pretty = "0.11"
 z3rro = { path = "./z3rro" }
 dashmap = "5.4"
-im-rc = "15.1.0"
+im-rc = "15"
 cfg-if = "1.0.0"
 itertools = "0.12.0"
 

src/smt/pretty_model.rs

@@ -112,7 +112,13 @@ fn pretty_var<'smt, 'ctx>(
 ) -> Doc {
     let builder = ExprBuilder::new(Span::dummy_span());
     let symbolic = translate.t_symbolic(&builder.var(ident, translate.ctx.tcx));
-    pretty_eval_result(symbolic.eval(model))
+
+    // atomically evaluate the value in the model, so that if an error occurs
+    // the accessed variables will still show up in the "unaccessed" block later
+    // on.
+    let res = model.atomically(|| symbolic.eval(model));
+
+    pretty_eval_result(res)
 }
 
 fn pretty_eval_result<T>(res: Result<T, SmtEvalError>) -> Doc

z3rro/Cargo.toml

@@ -12,6 +12,7 @@ cfg-if = "1.0"
 tracing = "0.1"
 tempfile = "3.3"
 thiserror = "1.0"
+im-rc = "15"
 
 [features]
 datatype-eureal = []

z3rro/src/model.rs

@@ -2,7 +2,6 @@
 
 use std::{
     cell::RefCell,
-    collections::HashSet,
     fmt::{self, Display},
 };
 
@@ -22,8 +21,8 @@ use z3::{
 pub struct InstrumentedModel<'ctx> {
     model: Model<'ctx>,
     // TODO: turn this into a HashSet of FuncDecls when the type implements Hash
-    accessed_decls: RefCell<HashSet<String>>,
-    accessed_exprs: RefCell<HashSet<Dynamic<'ctx>>>,
+    accessed_decls: RefCell<im_rc::HashSet<String>>,
+    accessed_exprs: RefCell<im_rc::HashSet<Dynamic<'ctx>>>,
 }
 
 impl<'ctx> InstrumentedModel<'ctx> {
@@ -35,6 +34,23 @@ impl<'ctx> InstrumentedModel<'ctx> {
         }
     }
 
+    /// Execute this function "atomically" on this model, rolling back any
+    /// changes to the list of visited decls/exprs if the function fails with an
+    /// error.
+    pub fn atomically<T>(
+        &self,
+        f: impl FnOnce() -> Result<T, SmtEvalError>,
+    ) -> Result<T, SmtEvalError> {
+        let accessed_decls = self.accessed_decls.borrow().clone();
+        let accessed_exprs = self.accessed_exprs.borrow().clone();
+        let res = f();
+        if res.is_err() {
+            *self.accessed_decls.borrow_mut() = accessed_decls;
+            *self.accessed_exprs.borrow_mut() = accessed_exprs;
+        }
+        res
+    }
+
     /// 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.
@@ -60,8 +76,8 @@ impl<'ctx> InstrumentedModel<'ctx> {
                 // 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 {
+                let prev = self.accessed_exprs.borrow_mut().insert(child.clone());
+                if prev.is_some() {
                     continue;
                 }
                 self.add_children_accessed(child);