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

Rust and VIR-level models
utaal · Aug 23, 2021 · 753ff30 · 753ff30
2 parents d02dead 6870e86
commit 753ff30
Show file tree

Hide file tree

Showing 12 changed files with 366 additions and 32 deletions.
diff --git a/verify/air/src/model.rs b/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> {

diff --git a/verify/air/src/var_to_const.rs b/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)
 }
diff --git a/verify/rust_verify/example/debug.rs b/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
 }
 */
diff --git a/verify/rust_verify/src/lib.rs b/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;

diff --git a/verify/rust_verify/src/model.rs b/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(())
  }
 }
diff --git a/verify/rust_verify/src/verifier.rs b/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),
  );
  }
  }
 

diff --git a/verify/vir/src/def.rs b/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,

diff --git a/verify/vir/src/func_to_air.rs b/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![])),
  }
 }