diff --git a/verify/air/src/model.rs b/verify/air/src/model.rs index 3bc0ea7b51af4..ff3b9aa5fa497 100644 --- 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>, + /// TODO: Expose via a more abstract interface + pub value_snapshots: HashMap>, } impl<'a> Model<'a> { diff --git a/verify/air/src/var_to_const.rs b/verify/air/src/var_to_const.rs index 8c9e615182c23..8a72d61847e97 100644 --- 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, version_decls: &mut HashSet, snapshots: &mut Snapshots, + all_snapshots: &mut Snapshots, types: &HashMap, 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 = 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) { let mut versions: HashMap = HashMap::new(); let mut version_decls: HashSet = HashSet::new(); let mut snapshots: Snapshots = HashMap::new(); + let mut all_snapshots: Snapshots = HashMap::new(); let mut types: HashMap = HashMap::new(); let mut local_vars: Vec = Vec::new(); @@ -151,9 +164,10 @@ pub(crate) fn lower_query(query: &Query) -> (Query, Snapshots, Vec) { &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 index b0f94dd9e63e9..63055ec02417a 100644 --- 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 index b282a64a3e575..9ac945793f08e 100644 --- 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 new file mode 100644 index 0000000000000..c0018c42b4a3a --- /dev/null +++ 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, +} + +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 { + 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 index 7f6983aaa1d19..bcb21f53878b5 100644 --- 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 index b54a096732143..b436347e1b54c 100644 --- 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 { pub span: Span, pub x: X, diff --git a/verify/vir/src/func_to_air.rs b/verify/vir/src/func_to_air.rs index c43ec70fc61f0..e053e9215fbd5 100644 --- 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 Result { +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 Result Ok(Arc::new(vec![])), + _ => Ok((Arc::new(vec![]), vec![])), } } diff --git a/verify/vir/src/lib.rs b/verify/vir/src/lib.rs index f3d54a3fde57b..0bd8048e09460 100644 --- a/verify/vir/src/lib.rs +++ b/verify/vir/src/lib.rs @@ -9,6 +9,7 @@ pub mod datatype_to_air; pub mod def; pub mod func_to_air; pub mod headers; +pub mod model; pub mod modes; mod prelude; mod recursion; diff --git a/verify/vir/src/model.rs b/verify/vir/src/model.rs new file mode 100644 index 0000000000000..7e9e36a5d1a27 --- /dev/null +++ b/verify/vir/src/model.rs @@ -0,0 +1,35 @@ +use crate::ast::Ident; +use crate::def::rm_suffix_local_id; +use air::model::Model as AModel; +use std::collections::HashMap; + +#[derive(Debug)] +/// VIR-level model of a concrete counterexample +pub struct Model<'a> { + /// Handle to the AIR-level model; only for internal use, e.g., for `eval` + air_model: AModel<'a>, + /// Internal mapping from snapshot IDs to snapshots that map VIR variables to values + /// TODO: Upgrade to a semantics-preserving value type, instead of String. + vir_snapshots: HashMap>, +} + +impl<'a> Model<'a> { + pub fn new(air_model: AModel<'a>) -> Model<'a> { + let mut vir_snapshots = HashMap::new(); + + for (snap_id, value_snapshot) in &air_model.value_snapshots { + let mut vir_snapshot = HashMap::new(); + for (var_name, value) in &*value_snapshot { + vir_snapshot.insert(rm_suffix_local_id(&var_name), value.clone()); + } + vir_snapshots.insert(snap_id.clone(), vir_snapshot); + } + + Model { air_model, vir_snapshots } + } + + /// Look up the value of a VIR variable `name` in a given `snapshot` + pub fn query_variable(&self, snapshot: Ident, name: Ident) -> Option { + Some(self.vir_snapshots.get(&snapshot)?.get(&name)?.to_string()) + } +} diff --git a/verify/vir/src/recursion.rs b/verify/vir/src/recursion.rs index f989f85362895..d6fc1239e60ac 100644 --- a/verify/vir/src/recursion.rs +++ b/verify/vir/src/recursion.rs @@ -266,7 +266,9 @@ pub(crate) fn check_termination_exp( StmX::Block(Arc::new(vec![stm_decl, stm_assign, stm_assert])), ); - let commands = crate::sst_to_air::body_stm_to_air( + // TODO: If we decide to support debugging decreases failures, we should plumb _snap_map + // up to the VIR model + let (commands, _snap_map) = crate::sst_to_air::body_stm_to_air( ctx, &function.x.typ_params, &function.x.params, diff --git a/verify/vir/src/sst_to_air.rs b/verify/vir/src/sst_to_air.rs index a9e7ae269cb6d..7a410c7ffe082 100644 --- a/verify/vir/src/sst_to_air.rs +++ b/verify/vir/src/sst_to_air.rs @@ -5,8 +5,8 @@ use crate::ast_util::path_to_string; use crate::context::Ctx; use crate::def::{ prefix_ensures, prefix_fuel_id, prefix_requires, prefix_type_id, suffix_global_id, - suffix_local_id, suffix_typ_param_id, Spanned, FUEL_BOOL, FUEL_BOOL_DEFAULT, FUEL_DEFAULTS, - FUEL_ID, FUEL_PARAM, FUEL_TYPE, POLY, SNAPSHOT_CALL, SUCC, + suffix_local_id, suffix_typ_param_id, SnapPos, Spanned, FUEL_BOOL, FUEL_BOOL_DEFAULT, + FUEL_DEFAULTS, FUEL_ID, FUEL_PARAM, FUEL_TYPE, POLY, SNAPSHOT_CALL, SUCC, }; use crate::sst::{BndX, Dest, Exp, ExpX, Stm, StmX}; use crate::util::vec_map; @@ -270,7 +270,9 @@ pub(crate) fn exp_to_expr(ctx: &Ctx, exp: &Exp) -> Expr { struct State { local_shared: Vec, // shared between all queries for a single function commands: Vec, - snapshot_count: u32, + snapshot_count: u32, // Used to ensure unique Idents for each snapshot + latest_snapshot: Ident, // The ID of the closest snapshot that dominates the current position in the AST + snap_map: Vec<(Span, SnapPos)>, // Maps each statement's span to the closest dominating snapshot's ID } fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Vec { @@ -295,6 +297,11 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Vec { for arg in args.iter() { ens_args.push(exp_to_expr(ctx, arg)); } + if ctx.debug { + state + .snap_map + .push((stm.span.clone(), SnapPos::Full(state.latest_snapshot.clone()))); + } } Some(Dest { var, mutable }) => { let x = suffix_local_id(&var.clone()); @@ -323,9 +330,15 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Vec { if ctx.debug { // Add a snapshot after we modify the destination state.snapshot_count += 1; - let name = format!("Mutation_{}", state.snapshot_count); - let snapshot = Arc::new(StmtX::Snapshot(Arc::new(name))); + let name = format!("{}_mutation", state.snapshot_count); + let snapshot = Arc::new(StmtX::Snapshot(Arc::new(name.clone()))); stmts.push(snapshot); + state.latest_snapshot = Arc::new(name); + // Update the snap_map so that it reflects the state _after_ the + // statement takes effect. + state + .snap_map + .push((stm.span.clone(), SnapPos::Full(state.latest_snapshot.clone()))); } } } @@ -339,15 +352,32 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Vec { StmX::Assert(expr) => { let air_expr = exp_to_expr(ctx, &expr); let option_span = Arc::new(Some(stm.span.clone())); + if ctx.debug { + state + .snap_map + .push((stm.span.clone(), SnapPos::Full(state.latest_snapshot.clone()))); + } vec![Arc::new(StmtX::Assert(option_span, air_expr))] } - StmX::Assume(expr) => vec![Arc::new(StmtX::Assume(exp_to_expr(ctx, &expr)))], + StmX::Assume(expr) => { + if ctx.debug { + state + .snap_map + .push((stm.span.clone(), SnapPos::Full(state.latest_snapshot.clone()))); + } + vec![Arc::new(StmtX::Assume(exp_to_expr(ctx, &expr)))] + } StmX::Decl { ident, typ, mutable, init: _ } => { state.local_shared.push(if *mutable { Arc::new(DeclX::Var(suffix_local_id(&ident), typ_to_air(&typ))) } else { Arc::new(DeclX::Const(suffix_local_id(&ident), typ_to_air(&typ))) }); + if ctx.debug { + state + .snap_map + .push((stm.span.clone(), SnapPos::Full(state.latest_snapshot.clone()))); + } vec![] } StmX::Assign(lhs, rhs) => { @@ -360,9 +390,15 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Vec { if ctx.debug { // Add a snapshot after we modify the destination state.snapshot_count += 1; - let name = format!("Mutation_{}", state.snapshot_count); - let snapshot = Arc::new(StmtX::Snapshot(Arc::new(name))); + let name = format!("{}_mutation", state.snapshot_count); + let snapshot = Arc::new(StmtX::Snapshot(Arc::new(name.clone()))); stmts.push(snapshot); + state.latest_snapshot = Arc::new(name); + // Update the snap_map so that it reflects the state _after_ the + // statement takes effect. + state + .snap_map + .push((stm.span.clone(), SnapPos::Full(state.latest_snapshot.clone()))); } stmts } @@ -380,7 +416,21 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Vec { rhss.insert(0, neg_assume); let lblock = Arc::new(StmtX::Block(Arc::new(lhss))); let rblock = Arc::new(StmtX::Block(Arc::new(rhss))); - vec![Arc::new(StmtX::Switch(Arc::new(vec![lblock, rblock])))] + let mut stmts = vec![Arc::new(StmtX::Switch(Arc::new(vec![lblock, rblock])))]; + if ctx.debug { + // Add a snapshot for the state after we join the lhs and rhs back together + state.snapshot_count += 1; + let name = format!("{}_join", state.snapshot_count); + let snapshot = Arc::new(StmtX::Snapshot(Arc::new(name.clone()))); + stmts.push(snapshot); + state.latest_snapshot = Arc::new(name); + // Update the snap_map so that it reflects the state _after_ the + // statement takes effect. + state + .snap_map + .push((stm.span.clone(), SnapPos::End(state.latest_snapshot.clone()))); + } + stmts } StmX::While { cond, body, invs, typ_inv_vars, modified_vars } => { let pos_cond = exp_to_expr(ctx, &cond); @@ -389,6 +439,19 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Vec { let neg_assume = Arc::new(StmtX::Assume(neg_cond)); let invs: Vec<(Span, Expr)> = invs.iter().map(|e| (e.span.clone(), exp_to_expr(ctx, e))).collect(); + + let entry_snap_id = if ctx.debug { + // Add a snapshot to capture the start of the while loop + // We add the snapshot via Block to avoid copying the entire AST of the loop body + state.snapshot_count += 1; + let name = format!("{}_while_begin", state.snapshot_count); + let entry_snap = Arc::new(name); + state.latest_snapshot = entry_snap.clone(); + Some(entry_snap) + } else { + None + }; + let mut air_body = stm_to_stmts(ctx, state, body); /* @@ -430,6 +493,19 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Vec { } else { Arc::new(StmtX::Block(Arc::new(air_body))) }; + + let assertion = if !ctx.debug { + assertion + } else { + // Update the snap_map to associate the start of the while loop with the new snapshot + let entry_snap_id = entry_snap_id.unwrap(); // Always Some if ctx.debug + let snapshot: Stmt = Arc::new(StmtX::Snapshot(Arc::new(entry_snap_id.to_string()))); + state.snap_map.push((body.span.clone(), SnapPos::Start(entry_snap_id.clone()))); + let block_contents: Vec = vec![snapshot, assertion]; + let new_block: Stmt = Arc::new(StmtX::Block(Arc::new(block_contents))); + new_block + }; + let query = Arc::new(QueryX { local: Arc::new(local), assertion }); state.commands.push(Arc::new(CommandX::CheckValid(query))); @@ -457,6 +533,19 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Vec { stmts.push(Arc::new(inv_stmt)); } stmts.push(neg_assume); + if ctx.debug { + // Add a snapshot for the state after we emerge from the while loop + state.snapshot_count += 1; + let name = format!("{}_while_end", state.snapshot_count); + let snapshot = Arc::new(StmtX::Snapshot(Arc::new(name.clone()))); + stmts.push(snapshot); + // Update the snap_map so that it reflects the state _after_ the + // statement takes effect. + state.latest_snapshot = Arc::new(name); + state + .snap_map + .push((stm.span.clone(), SnapPos::End(state.latest_snapshot.clone()))); + } stmts } StmX::Fuel(x, fuel) => { @@ -477,6 +566,11 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Vec { let binder = ident_binder(&str_ident(FUEL_PARAM), &str_typ(FUEL_TYPE)); stmts.push(Arc::new(StmtX::Assume(mk_exists(&vec![binder], &vec![], &eq)))); } + if ctx.debug { + state + .snap_map + .push((stm.span.clone(), SnapPos::Full(state.latest_snapshot.clone()))); + } stmts } StmX::Block(stms) => stms.iter().map(|s| stm_to_stmts(ctx, state, s)).flatten().collect(), @@ -523,7 +617,7 @@ pub fn body_stm_to_air( reqs: &Vec, enss: &Vec, stm: &Stm, -) -> Commands { +) -> (Commands, Vec<(Span, SnapPos)>) { // Verifying a single function can generate multiple SMT queries. // Some declarations (local_shared) are shared among the queries. // Others are private to each query. @@ -552,13 +646,21 @@ pub fn body_stm_to_air( assigned.insert(param.x.name.clone()); } - let mut state = State { local_shared, commands: Vec::new(), snapshot_count: 0 }; + let initial_snapshot_name = Arc::new("0_entry".to_string()); + + let mut state = State { + local_shared, + commands: Vec::new(), + snapshot_count: 0, + latest_snapshot: initial_snapshot_name.clone(), + snap_map: Vec::new(), + }; let stm = crate::sst_vars::stm_assign(&mut declared, &mut assigned, &mut HashSet::new(), stm); let mut stmts = stm_to_stmts(ctx, &mut state, &stm); if ctx.debug { - let snapshot = Arc::new(StmtX::Snapshot(Arc::new("Entry".to_string()))); + let snapshot = Arc::new(StmtX::Snapshot(initial_snapshot_name)); let mut new_stmts = vec![snapshot]; new_stmts.append(&mut stmts); stmts = new_stmts; @@ -589,5 +691,5 @@ pub fn body_stm_to_air( let query = Arc::new(QueryX { local: Arc::new(local), assertion }); state.commands.push(Arc::new(CommandX::CheckValid(query))); - Arc::new(state.commands) + (Arc::new(state.commands), state.snap_map) }