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

Rust and VIR-level models

Author: parno

verify/air/src/model.rs

@@ -19,7 +19,8 @@ pub struct Model<'a> {
     /// 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>>,
+    /// TODO: Expose via a more abstract interface
+    pub value_snapshots: HashMap<Ident, HashMap<Ident, String>>,
 }
 
 impl<'a> Model<'a> {

verify/air/src/var_to_const.rs

@@ -38,6 +38,7 @@ fn lower_stmt(
     versions: &mut HashMap<Ident, u32>,
     version_decls: &mut HashSet<Ident>,
     snapshots: &mut Snapshots,
+    all_snapshots: &mut Snapshots,
     types: &HashMap<Ident, Typ>,
     stmt: &Stmt,
 ) -> Stmt {
@@ -67,12 +68,21 @@ fn lower_stmt(
         }
         StmtX::Snapshot(snap) => {
             snapshots.insert(snap.clone(), versions.clone());
+            all_snapshots.insert(snap.clone(), versions.clone());
             Arc::new(StmtX::Block(Arc::new(vec![])))
         }
         StmtX::Block(ss) => {
             let mut stmts: Vec<Stmt> = Vec::new();
             for s in ss.iter() {
-                stmts.push(lower_stmt(decls, versions, version_decls, snapshots, types, s));
+                stmts.push(lower_stmt(
+                    decls,
+                    versions,
+                    version_decls,
+                    snapshots,
+                    all_snapshots,
+                    types,
+                    s,
+                ));
             }
             Arc::new(StmtX::Block(Arc::new(stmts)))
         }
@@ -88,10 +98,12 @@ fn lower_stmt(
                     &mut versions_i,
                     version_decls,
                     &mut snapshots_i,
+                    all_snapshots,
                     types,
                     s,
                 ));
                 all_versions.push(versions_i);
+                all_snapshots.extend(snapshots_i);
             }
             for x in all_versions[0].keys() {
                 // For each variable x, the different branches may have different versions[x],
@@ -125,6 +137,7 @@ pub(crate) fn lower_query(query: &Query) -> (Query, Snapshots, Vec<Decl>) {
     let mut versions: HashMap<Ident, u32> = HashMap::new();
     let mut version_decls: HashSet<Ident> = HashSet::new();
     let mut snapshots: Snapshots = HashMap::new();
+    let mut all_snapshots: Snapshots = HashMap::new();
     let mut types: HashMap<Ident, Typ> = HashMap::new();
     let mut local_vars: Vec<Decl> = Vec::new();
 
@@ -151,9 +164,10 @@ pub(crate) fn lower_query(query: &Query) -> (Query, Snapshots, Vec<Decl>) {
         &mut versions,
         &mut version_decls,
         &mut snapshots,
+        &mut all_snapshots,
         &types,
         assertion,
     );
     let local = Arc::new(decls);
-    (Arc::new(QueryX { local, assertion }), snapshots, local_vars)
+    (Arc::new(QueryX { local, assertion }), all_snapshots, local_vars)
 }

verify/rust_verify/example/debug.rs

@@ -5,14 +5,56 @@ use pervasive::*;
 
 fn main() {}
 
-//fn test1(i: int, n: nat, u: u8) {
-//    assert(n >= 5);
-//}
+/*
+fn test_params(i: int, n: nat, u: u8) {
+    assert(n >= 5);
+}
 
-fn test2(i: int, n: nat, u: u8) {
+fn test_mutation(i: int, n: nat, u: u8) {
     let mut x = 5;
     x = x + i;
     x = x + n;
     x = x + u;
     assert(x >= 5);
 }
+*/
+
+fn test_if_else(b:bool, z:int) {
+    let mut x : int = 0;
+    let mut y : int = z;
+    x = x + y;      // 1_mutation
+    if b {
+        x = 2*x;    // 2_mutation
+        y = x + 1;  // 3_mutation
+    } else {
+        x = y + 1;  // 4_mutation
+        y = 7;      // 5_mutation
+    }
+    assert(x + y > 5); // 6_join
+}
+
+/*
+fn test_loop() {
+    let mut i: u64 = 10;
+    let mut b1: u8 = 20;
+    let mut b2: u8 = 200;
+    let mut b3: u8 = 30;  // 0_entry
+    i = i + 1;           // 1_mutation
+    i = i - 1;           // 2_mutation
+
+    while i < 100 {
+        invariant([
+            10 <= i,
+            i <= 100,
+            b1 as u64 == i * 2,
+        ]);
+                      // 3_while_begin
+        assert(b1 == 5);
+        i = i + 1;    // 4_mutation
+        b1 = b1 + 2;  // 5_mutation
+        b2 = b2 + 1;  // 6_mutation
+    } // 5_while_end
+
+    assert(true);   // 7_while_end
+}
+*/

verify/rust_verify/src/lib.rs

@@ -15,6 +15,7 @@ extern crate rustc_typeck;
 
 pub mod config;
 pub mod context;
+pub mod model;
 pub mod rust_to_vir;
 pub mod rust_to_vir_adts;
 pub mod rust_to_vir_base;

verify/rust_verify/src/model.rs

@@ -0,0 +1,104 @@
+use crate::util::from_raw_span;
+use air::ast::Ident;
+use air::ast::Span as ASpan;
+use rustc_span::source_map::SourceMap;
+use rustc_span::Span;
+use std::collections::HashMap;
+use std::fmt;
+use vir::def::SnapPos;
+use vir::model::Model as VModel;
+
+#[derive(Debug)]
+/// Rust-level model of a concrete counterexample
+pub struct Model<'a> {
+    /// Handle to the AIR-level model; only for internal use, e.g., for `eval`
+    vir_model: VModel<'a>,
+    /// Internal mapping from a line in the source file to a snapshot ID
+    line_map: HashMap<usize, Ident>,
+}
+
+impl<'a> Model<'a> {
+    pub fn new(
+        vir_model: VModel<'a>,
+        snap_map: &Vec<(ASpan, SnapPos)>,
+        source_map: &SourceMap,
+    ) -> Model<'a> {
+        let mut line_map = HashMap::new();
+
+        if snap_map.len() > 0 {
+            let (air_span, snap_pos) = &snap_map[0];
+            let span: &Span = &from_raw_span(&air_span.raw_span);
+            let (start, end) =
+                source_map.is_valid_span(*span).expect("internal error: invalid Span");
+
+            let mut min_snap: Ident = match snap_pos {
+                SnapPos::Start(span_id) => span_id.clone(),
+                SnapPos::Full(span_id) => span_id.clone(),
+                SnapPos::End(span_id) => span_id.clone(),
+            };
+            let mut min_line = start.line;
+            let mut max_line = end.line;
+
+            for (air_span, snap_pos) in snap_map {
+                let span: &Span = &from_raw_span(&air_span.raw_span);
+                let (span_start, span_end) =
+                    source_map.is_valid_span(*span).expect("internal error: invalid Span");
+
+                let (start, end, cur_snap) = match snap_pos {
+                    SnapPos::Start(span_id) => (span_start.line, span_start.line + 1, span_id),
+                    SnapPos::Full(span_id) => (span_start.line, span_end.line + 1, span_id),
+                    SnapPos::End(span_id) => (span_end.line, span_end.line + 1, span_id),
+                };
+
+                println!("Apply {} to lines {}..{}", cur_snap, start, end);
+                for line in start..end {
+                    line_map.insert(line, cur_snap.clone());
+                }
+
+                if span_start.line < min_line {
+                    min_line = span_start.line;
+                    min_snap = cur_snap.clone();
+                }
+                max_line = std::cmp::max(max_line, span_end.line);
+            }
+
+            // Fill in any gaps
+            let mut cur_snap = min_snap;
+            for line in min_line..max_line {
+                match line_map.get(&line) {
+                    Some(snap) => cur_snap = snap.clone(),
+                    None => {
+                        let _ = line_map.insert(line, cur_snap.clone());
+                        ()
+                    }
+                }
+            }
+        }
+
+        // Debugging sanity checks
+        for (air_span, snap_pos) in snap_map {
+            let span: &Span = &from_raw_span(&air_span.raw_span);
+            let (start, end) =
+                source_map.is_valid_span(*span).expect("internal error: invalid Span");
+            println!("Span from {} to {} => {:?}", start.line, end.line, snap_pos);
+        }
+        Model { vir_model, line_map }
+    }
+
+    pub fn query_variable(&self, line: usize, name: Ident) -> Option<String> {
+        Some(self.vir_model.query_variable(self.line_map.get(&line)?.clone(), name)?)
+    }
+}
+
+impl<'a> fmt::Display for Model<'a> {
+    /// Dump the contents of the Rust model for debugging purposes
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "\nDisplaying model with {} lines\n", self.line_map.len())?;
+        let mut lines: Vec<_> = self.line_map.iter().collect();
+        lines.sort_by_key(|t| t.0);
+        for (line, snap_id) in lines {
+            write!(f, "Line {}: {}\n", line, snap_id)?;
+        }
+        Ok(())
+    }
+}

verify/rust_verify/src/verifier.rs

@@ -1,5 +1,6 @@
 use crate::config::Args;
 use crate::context::Context;
+use crate::model::Model;
 use crate::unsupported;
 use crate::util::from_raw_span;
 use air::ast::{Command, CommandX, SpanOption};
@@ -11,6 +12,8 @@ use rustc_span::{CharPos, FileName, MultiSpan, Span};
 use std::fs::File;
 use std::io::Write;
 use vir::ast::{Krate, VirErr, VirErrX};
+use vir::def::SnapPos;
+use vir::model::Model as VModel;
 
 pub struct Verifier {
     pub encountered_vir_error: bool,
@@ -128,6 +131,7 @@ impl Verifier {
     fn check_result_validity(
         &mut self,
         compiler: &Compiler,
+        snap_map: &Vec<(air::ast::Span, SnapPos)>,
         command: &Command,
         result: ValidityResult,
     ) {
@@ -140,7 +144,7 @@ impl Verifier {
             ValidityResult::TypeError(err) => {
                 panic!("internal error: generated ill-typed AIR code: {}", err);
             }
-            ValidityResult::Invalid(m, span1, span2) => {
+            ValidityResult::Invalid(air_model, span1, span2) => {
                 report_verify_error(compiler, &span1, &span2);
                 self.errors.push((
                     span1
@@ -153,7 +157,10 @@ impl Verifier {
                         .map(|x| ErrorSpan::new_from_air_span(compiler.session().source_map(), x)),
                 ));
                 if self.args.debug {
-                    println!("Received model: {}", m);
+                    println!("Received AIR model: {}", air_model);
+                    let vir_model = VModel::new(air_model);
+                    let model = Model::new(vir_model, snap_map, compiler.session().source_map());
+                    println!("Build Rust model: {}", model);
                 }
             }
         }
@@ -231,19 +238,24 @@ impl Verifier {
                 air_context.comment(&("Function-Decl ".to_string() + &function.x.name));
             }
             for command in commands.iter() {
-                self.check_result_validity(compiler, &command, air_context.command(&command));
+                Self::check_internal_result(air_context.command(&command));
             }
         }
 
         // Create queries to check the validity of proof/exec function bodies
         for function in &krate.functions {
-            let commands = vir::func_to_air::func_def_to_air(&ctx, &function)?;
+            let (commands, snap_map) = vir::func_to_air::func_def_to_air(&ctx, &function)?;
             if commands.len() > 0 {
                 air_context.blank_line();
                 air_context.comment(&("Function-Def ".to_string() + &function.x.name));
             }
             for command in commands.iter() {
-                self.check_result_validity(compiler, &command, air_context.command(&command));
+                self.check_result_validity(
+                    compiler,
+                    &snap_map,
+                    &command,
+                    air_context.command(&command),
+                );
             }
         }
 

verify/vir/src/def.rs

@@ -85,6 +85,14 @@ pub fn suffix_local_id(ident: &Ident) -> Ident {
     Arc::new(ident.to_string() + SUFFIX_LOCAL)
 }
 
+pub fn rm_suffix_local_id(ident: &Ident) -> Ident {
+    let mut name = ident.to_string();
+    if name.ends_with(SUFFIX_LOCAL) {
+        name = name[..name.len() - SUFFIX_LOCAL.len()].to_string();
+    }
+    Arc::new(name)
+}
+
 pub fn suffix_typ_param_id(ident: &Ident) -> Ident {
     Arc::new(ident.to_string() + SUFFIX_TYPE_PARAM)
 }
@@ -138,6 +146,15 @@ pub fn variant_positional_field_ident(variant_ident: &Ident, idx: usize) -> Iden
     variant_field_ident(variant_ident, format!("{}", idx).as_str())
 }
 
+/// For a given snapshot, does it represent the state
+/// at the start of the corresponding span, the end, or the full span?
+#[derive(Debug)]
+pub enum SnapPos {
+    Start(Ident),
+    Full(Ident),
+    End(Ident),
+}
+
 pub struct Spanned<X> {
     pub span: Span,
     pub x: X,

verify/vir/src/func_to_air.rs

@@ -2,8 +2,8 @@ use crate::ast::{Function, Ident, Idents, Mode, ParamX, Params, VirErr};
 use crate::context::Ctx;
 use crate::def::{
     prefix_ensures, prefix_fuel_id, prefix_fuel_nat, prefix_recursive, prefix_requires,
-    suffix_global_id, suffix_local_id, suffix_typ_param_id, Spanned, FUEL_BOOL, FUEL_BOOL_DEFAULT,
-    FUEL_LOCAL, FUEL_TYPE, SUCC, ZERO,
+    suffix_global_id, suffix_local_id, suffix_typ_param_id, SnapPos, Spanned, FUEL_BOOL,
+    FUEL_BOOL_DEFAULT, FUEL_LOCAL, FUEL_TYPE, SUCC, ZERO,
 };
 use crate::sst_to_air::{exp_to_expr, typ_invariant, typ_to_air};
 use crate::util::{vec_map, vec_map_result};
@@ -284,7 +284,10 @@ pub fn func_decl_to_air(ctx: &Ctx, function: &Function) -> Result<Commands, VirE
     Ok(Arc::new(commands))
 }
 
-pub fn func_def_to_air(ctx: &Ctx, function: &Function) -> Result<Commands, VirErr> {
+pub fn func_def_to_air(
+    ctx: &Ctx,
+    function: &Function,
+) -> Result<(Commands, Vec<(Span, SnapPos)>), VirErr> {
     match (function.x.mode, function.x.ret.as_ref(), function.x.body.as_ref()) {
         (Mode::Exec, _, Some(body)) | (Mode::Proof, _, Some(body)) => {
             let dest = function.x.ret.as_ref().map(|(x, _, _)| x.clone());
@@ -294,7 +297,7 @@ pub fn func_def_to_air(ctx: &Ctx, function: &Function) -> Result<Commands, VirEr
                 vec_map_result(&*function.x.ensure, |e| crate::ast_to_sst::expr_to_exp(ctx, e))?;
             let stm = crate::ast_to_sst::expr_to_stm(&ctx, &body, &dest)?;
             let stm = crate::recursion::check_termination_stm(ctx, function, &stm)?;
-            let commands = crate::sst_to_air::body_stm_to_air(
+            let (commands, snap_map) = crate::sst_to_air::body_stm_to_air(
                 ctx,
                 &function.x.typ_params,
                 &function.x.params,
@@ -304,8 +307,8 @@ pub fn func_def_to_air(ctx: &Ctx, function: &Function) -> Result<Commands, VirEr
                 &enss,
                 &stm,
             );
-            Ok(commands)
+            Ok((commands, snap_map))
         }
-        _ => Ok(Arc::new(vec![])),
+        _ => Ok((Arc::new(vec![]), vec![])),
     }
 }