Merge pull request rust-lang#21 from Chris-Hawblitzel/debugger

Add preliminary support for AIR-level model reconstruction

Author: parno

verify/air/src/ast.rs

@@ -1,3 +1,4 @@
+use std::collections::HashMap;
 use std::rc::Rc;
 
 pub type RawSpan = Rc<dyn std::any::Any>;
@@ -11,15 +12,11 @@ pub type SpanOption = Rc<Option<Span>>;
 
 pub type TypeError = String;
 
-#[derive(Debug)]
-pub enum ValidityResult {
-    Valid,
-    Invalid(SpanOption, SpanOption),
-    TypeError(TypeError),
-}
-
 pub type Ident = Rc<String>;
 
+pub(crate) type Snapshot = HashMap<Ident, u32>;
+pub(crate) type Snapshots = HashMap<Ident, Snapshot>;
+
 pub type Typ = Rc<TypX>;
 pub type Typs = Rc<Vec<Typ>>;
 #[derive(Debug)]

verify/air/src/context.rs

@@ -1,4 +1,5 @@
-use crate::ast::{Command, CommandX, Decl, Ident, Query, SpanOption, TypeError, ValidityResult};
+use crate::ast::{Command, CommandX, Decl, Ident, Query, SpanOption, TypeError};
+use crate::model::Model;
 use crate::print_parse::Logger;
 use crate::typecheck::Typing;
 use std::collections::{HashMap, HashSet};
@@ -13,6 +14,13 @@ pub(crate) struct AssertionInfo {
     pub(crate) decl: Decl,
 }
 
+#[derive(Debug)]
+pub enum ValidityResult<'a> {
+    Valid,
+    Invalid(Model<'a>, SpanOption, SpanOption),
+    TypeError(TypeError),
+}
+
 pub struct Context<'ctx> {
     pub(crate) context: &'ctx z3::Context,
     pub(crate) solver: &'ctx z3::Solver<'ctx>,
@@ -22,6 +30,7 @@ pub struct Context<'ctx> {
     pub(crate) assert_infos: HashMap<Ident, Rc<AssertionInfo>>,
     pub(crate) assert_infos_count: u64,
     pub(crate) typing: Typing,
+    pub(crate) debug: bool,
     pub(crate) rlimit: u32,
     pub(crate) air_initial_log: Logger,
     pub(crate) air_middle_log: Logger,
@@ -47,6 +56,7 @@ impl<'ctx> Context<'ctx> {
                 funs: HashMap::new(),
                 snapshots: HashSet::new(),
             },
+            debug: false,
             rlimit: 0,
             air_initial_log: Logger::new(None),
             air_middle_log: Logger::new(None),
@@ -72,6 +82,14 @@ impl<'ctx> Context<'ctx> {
         self.smt_log = Logger::new(Some(writer));
     }
 
+    pub fn set_debug(&mut self, debug: bool) {
+        self.debug = debug;
+    }
+
+    pub fn get_debug(&self) -> bool {
+        self.debug
+    }
+
     pub fn set_rlimit(&mut self, rlimit: u32) {
         self.rlimit = rlimit;
         self.air_initial_log.log_set_option("rlimit", &rlimit.to_string());
@@ -219,12 +237,12 @@ impl<'ctx> Context<'ctx> {
         if let Err(err) = crate::typecheck::check_query(self, query) {
             return ValidityResult::TypeError(err);
         }
-        let query = 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);
+        let validity = crate::smt_verify::smt_check_query(self, &query, snapshots, local_vars);
 
         validity
     }

verify/air/src/lib.rs

@@ -1,12 +1,14 @@
 pub mod ast;
 pub mod ast_util;
 pub mod context;
+pub mod model;
 
 #[macro_use]
 pub mod print_parse;
 
 mod block_to_assert;
 mod def;
+mod smt_util;
 mod smt_verify;
 mod tests;
 mod typecheck;

verify/air/src/main.rs

@@ -1,5 +1,5 @@
-use air::ast::{CommandX, Span, ValidityResult};
-use air::context::Context;
+use air::ast::{CommandX, Span};
+use air::context::{Context, ValidityResult};
 use getopts::Options;
 use sise::Node;
 use std::fs::File;
@@ -14,6 +14,7 @@ pub fn main() {
     opts.optopt("", "log-air-middle", "Log AIR queries in middle form", "FILENAME");
     opts.optopt("", "log-air-final", "Log AIR queries in final form", "FILENAME");
     opts.optopt("", "log-smt", "Log SMT queries", "FILENAME");
+    opts.optflag("d", "debug", "Debug verification failures");
     opts.optflag("h", "help", "print this help menu");
 
     let print_usage = || {
@@ -77,6 +78,8 @@ pub fn main() {
     let z3_context = z3::Context::new(&z3_config);
     let z3_solver = z3::Solver::new(&z3_context);
     let mut air_context = Context::new(&z3_context, &z3_solver);
+    let debug = matches.opt_present("debug");
+    air_context.set_debug(debug);
 
     // Start logging
     if let Some(filename) = matches.opt_str("log-air-middle") {
@@ -106,7 +109,7 @@ pub fn main() {
             ValidityResult::TypeError(err) => {
                 panic!("Type error: {}", err);
             }
-            ValidityResult::Invalid(span1, span2) => {
+            ValidityResult::Invalid(m, span1, span2) => {
                 count_errors += 1;
                 match &*span1 {
                     None => {
@@ -124,6 +127,9 @@ pub fn main() {
                         println!("Additional error detail at {}", as_string);
                     }
                 }
+                if debug {
+                    println!("Model: {}", m);
+                }
             }
         }
     }

verify/air/src/model.rs

@@ -0,0 +1,109 @@
+//! Provides an AIR-level interface to the model returned by the SMT solver
+//! when it reaches a SAT conclusion
+
+use crate::ast::{Decl, DeclX, Ident, Snapshots};
+use crate::context::Context;
+use crate::smt_util::new_const;
+use std::collections::HashMap;
+use std::fmt;
+use z3::ast::Dynamic;
+
+#[derive(Debug)]
+/// AIR-level model of a concrete counterexample
+pub struct Model<'a> {
+    /// Handle to the original Z3 model; only for internal use, e.g., for `eval`
+    z3_model: z3::Model<'a>,
+    /// Internal mapping of snapshot IDs to snapshots that map AIR variables to usage counts.
+    /// Generated when converting mutable variables to Z3-level constants.
+    id_snapshots: Snapshots,
+    /// Externally facing mapping from snapshot IDs to snapshots that map AIR variables
+    /// to their concrete values.
+    /// TODO: Upgrade to a semantics-preserving value type, instead of String.
+    value_snapshots: HashMap<Ident, HashMap<Ident, String>>,
+}
+
+impl<'a> Model<'a> {
+    /// Returns an (unpopulated) AIR model object.  Must call [build()] to fully populate.
+    /// # Arguments
+    /// * `model` - The model that Z3 returns
+    /// * `snapshots` - Internal mapping of snapshot IDs to snapshots that map AIR variables to usage counts.
+    pub fn new(model: z3::Model<'a>, snapshots: Snapshots) -> Model<'a> {
+        // println!("Creating a new model with {} snapshots", snapshots.len());
+        Model { z3_model: model, id_snapshots: snapshots, value_snapshots: HashMap::new() }
+    }
+
+    /// Convert a Z3 AST variable `var_stmt` into a String value
+    /// Uses `var_name` only for error reporting.
+    fn lookup_z3_var(&self, var_name: &String, var_smt: &Dynamic) -> String {
+        if let Some(x) = self.z3_model.eval(var_smt) {
+            if let Some(b) = x.as_bool() {
+                format!("{}", b)
+            } else if let Some(i) = x.as_int() {
+                format!("{}", i)
+            } else {
+                println!("Unexpected type returned from model eval for {}", var_name);
+                "".to_string()
+            }
+        } else {
+            println!("Failed to extract evaluation of var {} from Z3's model", var_name);
+            "".to_string()
+        }
+    }
+
+    /// Populate the AIR-level model based on the Z3 model
+    /// `local_vars` should be a list of [DeclX::Const] values
+    /// representing the function's local non-mutable variables
+    /// (e.g., function parameters)
+    /// This is decoupled from the Model's constructor so that
+    /// we only do this expensive work when called in debug mode.
+    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();
+            println!("Snapshot {} has {} variables", snap_id, id_snapshot.len());
+            for (var_id, var_count) in &*id_snapshot {
+                let var_name = crate::var_to_const::rename_var(&*var_id, *var_count);
+                println!("\t{}", var_name);
+                let var_smt = context
+                    .vars
+                    .get(&var_name)
+                    .unwrap_or_else(|| panic!("internal error: variable {} not found", var_name));
+                let val = self.lookup_z3_var(&var_name, var_smt);
+                value_snapshot.insert(var_id.clone(), val);
+            }
+            // Add the local variables to every snapshot for uniformity
+            println!("local_vars has {} variables", local_vars.len());
+            for decl in local_vars.iter() {
+                if let DeclX::Const(var_name, typ) = &**decl {
+                    println!("\t{}", var_name);
+                    let var_smt = new_const(context, &var_name, &typ);
+                    let val = self.lookup_z3_var(&var_name, &var_smt);
+                    value_snapshot.insert(var_name.clone(), val);
+                    //value_snapshot.insert(Rc::new((*var_name).clone()), val);
+                } else {
+                    panic!("Expected local vars to all be constants at this point");
+                }
+            }
+            self.value_snapshots.insert(snap_id.clone(), value_snapshot);
+        }
+    }
+
+    /// Look up the value of an AIR variable `name` in a given `snapshot`
+    pub fn query_variable(&self, snapshot: Ident, name: Ident) -> Option<String> {
+        Some(self.value_snapshots.get(&snapshot)?.get(&name)?.to_string())
+    }
+}
+
+impl<'a> fmt::Display for Model<'a> {
+    /// Dump the contents of the AIR model for debugging purposes
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "\nDisplaying model with {} snapshots\n", self.value_snapshots.len())?;
+        for (snap_id, value_snapshot) in &self.value_snapshots {
+            write!(f, "Snapshot <{}>:\n", snap_id)?;
+            for (var_name, value) in &*value_snapshot {
+                write!(f, "\t{} -> {}\n", var_name, value)?;
+            }
+        }
+        Ok(())
+    }
+}

verify/air/src/smt_util.rs

@@ -0,0 +1,19 @@
+use crate::ast::{Typ, TypX};
+use crate::context::Context;
+use z3::ast::{Bool, Dynamic, Int};
+
+pub(crate) fn new_const<'ctx>(
+    context: &mut Context<'ctx>,
+    name: &String,
+    typ: &Typ,
+) -> Dynamic<'ctx> {
+    match &**typ {
+        TypX::Bool => Bool::new_const(context.context, name.clone()).into(),
+        TypX::Int => Int::new_const(context.context, name.clone()).into(),
+        TypX::Named(x) => {
+            let sort = &context.typs[x];
+            let fdecl = z3::FuncDecl::new(context.context, name.clone(), &[], sort);
+            fdecl.apply(&[])
+        }
+    }
+}

verify/air/src/smt_verify.rs

@@ -1,26 +1,16 @@
 use crate::ast::{
-    BinaryOp, BindX, Constant, Decl, DeclX, Expr, ExprX, Ident, MultiOp, Quant, Query, Span, StmtX,
-    Typ, TypX, UnaryOp, ValidityResult,
+    BinaryOp, BindX, Constant, Decl, DeclX, Expr, ExprX, Ident, MultiOp, Quant, Query, Snapshots,
+    Span, StmtX, Typ, TypX, UnaryOp,
 };
-use crate::context::{AssertionInfo, Context};
+use crate::context::{AssertionInfo, Context, ValidityResult};
 use crate::def::{GLOBAL_PREFIX_LABEL, PREFIX_LABEL};
+pub use crate::model::Model;
+use crate::smt_util::new_const;
 use std::collections::{HashMap, HashSet};
 use std::rc::Rc;
 use z3::ast::{Ast, Bool, Dynamic, Int};
 use z3::{Pattern, SatResult, Sort, Symbol};
 
-fn new_const<'ctx>(context: &mut Context<'ctx>, name: &String, typ: &Typ) -> Dynamic<'ctx> {
-    match &**typ {
-        TypX::Bool => Bool::new_const(context.context, name.clone()).into(),
-        TypX::Int => Int::new_const(context.context, name.clone()).into(),
-        TypX::Named(x) => {
-            let sort = &context.typs[x];
-            let fdecl = z3::FuncDecl::new(context.context, name.clone(), &[], sort);
-            fdecl.apply(&[])
-        }
-    }
-}
-
 fn expr_to_smt<'ctx>(context: &mut Context<'ctx>, expr: &Expr) -> Dynamic<'ctx> {
     match &**expr {
         ExprX::Const(Constant::Bool(b)) => Bool::from_bool(&context.context, *b).into(),
@@ -353,8 +343,10 @@ pub(crate) fn smt_add_decl<'ctx>(context: &mut Context<'ctx>, decl: &Decl) {
 fn smt_check_assertion<'ctx>(
     context: &mut Context<'ctx>,
     infos: &Vec<AssertionInfo>,
+    snapshots: Snapshots,
+    local_vars: Vec<Decl>, // Expected to be entirely DeclX::Const
     expr: &Expr,
-) -> ValidityResult {
+) -> ValidityResult<'ctx> {
     let mut discovered_span = Rc::new(None);
     let mut discovered_global_span = Rc::new(None);
     let not_expr = Rc::new(ExprX::Unary(UnaryOp::Not, expr.clone()));
@@ -375,7 +367,7 @@ fn smt_check_assertion<'ctx>(
         SatResult::Sat | SatResult::Unknown => {
             context.smt_log.log_word("get-model");
             let model = context.solver.get_model();
-            match model {
+            let mut air_model = match model {
                 None => {
                     panic!("SMT solver did not generate a model");
                 }
@@ -411,14 +403,26 @@ fn smt_check_assertion<'ctx>(
                             }
                         }
                     }
+                    if context.debug {
+                        println!("Z3 model: {}", model);
+                    }
+                    Model::new(model, snapshots)
                 }
+            };
+            if context.debug {
+                air_model.build(context, local_vars);
             }
-            ValidityResult::Invalid(discovered_span, discovered_global_span)
+            ValidityResult::Invalid(air_model, discovered_span, discovered_global_span)
         }
     }
 }
 
-pub(crate) fn smt_check_query<'ctx>(context: &mut Context<'ctx>, query: &Query) -> ValidityResult {
+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();
@@ -451,7 +455,7 @@ pub(crate) fn smt_check_query<'ctx>(context: &mut Context<'ctx>, query: &Query)
     }
 
     // check assertion
-    let result = smt_check_assertion(context, &infos, &labeled_assertion);
+    let result = smt_check_assertion(context, &infos, snapshots, local_vars, &labeled_assertion);
 
     // clean up
     context.pop_name_scope();

verify/air/src/tests.rs

@@ -1,4 +1,5 @@
-use crate::ast::{CommandX, ValidityResult};
+use crate::ast::CommandX;
+use crate::context::ValidityResult;
 #[allow(unused_imports)]
 use crate::print_parse::{macro_push_node, nodes_to_commands};
 #[allow(unused_imports)]
@@ -22,7 +23,7 @@ fn run_nodes_as_test(should_typecheck: bool, should_be_valid: bool, nodes: &[Nod
                         panic!("type error: {}", s);
                     }
                     (_, _, true, ValidityResult::Valid) => {}
-                    (_, _, false, ValidityResult::Invalid(_, _)) => {}
+                    (_, _, false, ValidityResult::Invalid(_, _, _)) => {}
                     (CommandX::CheckValid(_), _, _, _) => {
                         panic!("unexpected result");
                     }