Compute local variables inside var_to_const, rather than further down

the pipeline.  That way, we don't over include the constants introduced
to disambiguate mutated variables.

Author: parno

verify/air/src/context.rs

@@ -237,12 +237,12 @@ impl<'ctx> Context<'ctx> {
         if let Err(err) = crate::typecheck::check_query(self, query) {
             return ValidityResult::TypeError(err);
         }
-        let (query, snapshots) = crate::var_to_const::lower_query(query);
+        let (query, snapshots, local_vars) = crate::var_to_const::lower_query(query);
         self.air_middle_log.log_query(&query);
         let query = crate::block_to_assert::lower_query(&query);
         self.air_final_log.log_query(&query);
 
-        let validity = crate::smt_verify::smt_check_query(self, &query, snapshots);
+        let validity = crate::smt_verify::smt_check_query(self, &query, snapshots, local_vars);
 
         validity
     }

verify/air/src/model.rs

@@ -59,7 +59,7 @@ impl<'a> Model<'a> {
 
 
     /// Reconstruct an AIR-level model based on the Z3 model
-    pub fn build(&mut self, context: &mut Context, local_vars: &Vec<Decl>) {
+    pub fn build(&mut self, context: &mut Context, local_vars: Vec<Decl>) {
         println!("Building the AIR model"); 
         for (snap_id, id_snapshot) in &self.id_snapshots {
             let mut value_snapshot = HashMap::new();

verify/air/src/smt_verify.rs

@@ -1,5 +1,5 @@
 use crate::ast::{
-    BinaryOp, BindX, Constant, Decl,  DeclX,Expr, ExprX, Ident, MultiOp, Quant, Query, SnapShots, Span, StmtX,
+    BinaryOp, BindX, Constant, Decl, DeclX, Expr, ExprX, Ident, MultiOp, Quant, Query, SnapShots, Span, StmtX,
     Typ, TypX, UnaryOp,
 };
 use crate::context::{AssertionInfo, Context, ValidityResult};
@@ -364,7 +364,7 @@ fn smt_check_assertion<'ctx>(
     context: &mut Context<'ctx>,
     infos: &Vec<AssertionInfo>,
     snapshots: SnapShots,
-    local_vars: &Vec<Decl>,  // Expected to be entirely DeclX::Const
+    local_vars: Vec<Decl>,  // Expected to be entirely DeclX::Const
     expr: &Expr,
 ) -> ValidityResult<'ctx> {
     let mut discovered_span = Rc::new(None);
@@ -435,21 +435,16 @@ fn smt_check_assertion<'ctx>(
     }
 }
 
-pub(crate) fn smt_check_query<'ctx>(context: &mut Context<'ctx>, query: &Query, snapshots: SnapShots) -> ValidityResult<'ctx> {
+pub(crate) fn smt_check_query<'ctx>(context: &mut Context<'ctx>, query: &Query, snapshots: SnapShots, local_vars: Vec<Decl>) -> ValidityResult<'ctx> {
     context.smt_log.log_push();
     context.solver.push();
     context.push_name_scope();
 
-    let mut local_vars = Vec::new();
-
     // add query-local declarations
     for decl in query.local.iter() {
         if let Err(err) = crate::typecheck::add_decl(context, decl, false) {
             return ValidityResult::TypeError(err);
         }
-        if let DeclX::Const(_, _) = **decl {
-            local_vars.push(decl.clone());
-        }
         smt_add_decl(context, decl);
     }
 
@@ -473,7 +468,7 @@ pub(crate) fn smt_check_query<'ctx>(context: &mut Context<'ctx>, query: &Query,
     }
 
     // check assertion
-    let result = smt_check_assertion(context, &infos, snapshots, &local_vars, &labeled_assertion);
+    let result = smt_check_assertion(context, &infos, snapshots, local_vars, &labeled_assertion);
 
     // clean up
     context.pop_name_scope();

verify/air/src/var_to_const.rs

@@ -125,13 +125,15 @@ fn lower_stmt(
     }
 }
 
-pub(crate) fn lower_query(query: &Query) -> (Query, SnapShots) {
+pub(crate) fn lower_query(query: &Query) -> (Query, SnapShots, Vec<Decl>) {
     let QueryX { local, assertion } = &**query;
     let mut decls: Vec<Decl> = Vec::new();
     let mut versions: HashMap<Ident, u32> = HashMap::new();
     let mut version_decls: HashSet<Ident> = HashSet::new();
     let mut snapshots: SnapShots = HashMap::new();
     let mut types: HashMap<Ident, Typ> = HashMap::new();
+    let mut local_vars: Vec<Decl> = Vec::new();
+
     for decl in local.iter() {
         if let DeclX::Axiom(expr) = &**decl {
             let decl_x = DeclX::Axiom(lower_expr(&versions, &snapshots, expr));
@@ -140,12 +142,16 @@ pub(crate) fn lower_query(query: &Query) -> (Query, SnapShots) {
             decls.push(decl.clone());
         }
         if let DeclX::Var(x, t) = &**decl {
+            println!("In var_to_const, lower_query, DeclX::Var of {}", x);
             versions.insert(x.clone(), 0);
             types.insert(x.clone(), t.clone());
             let x = Rc::new(rename_var(x, 0));
             let decl = Rc::new(DeclX::Const(x.clone(), t.clone()));
             decls.push(decl);
         }
+        if let DeclX::Const(_, _) = &**decl {
+            local_vars.push(decl.clone());
+        }
     }
     let assertion = lower_stmt(
         &mut decls,
@@ -156,5 +162,5 @@ pub(crate) fn lower_query(query: &Query) -> (Query, SnapShots) {
         assertion,
     );
     let local = Rc::new(decls);
-    (Rc::new(QueryX { local, assertion }), snapshots)
+    (Rc::new(QueryX { local, assertion }), snapshots, local_vars)
 }