diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index 82ac648b952..01a64ef660c 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -16,7 +16,7 @@ use rustc_middle::ty::subst::{Subst, SubstsRef}; use rustc_trait_selection::infer::{InferCtxtExt, TyCtxtInferExt}; use std::path::PathBuf; -use rustc_errors::MultiSpan; +use rustc_errors::{DiagnosticBuilder, EmissionGuarantee, MultiSpan}; use rustc_span::{Span, symbol::Symbol}; use std::collections::HashSet; use log::{debug, trace}; @@ -76,6 +76,7 @@ pub struct Environment<'tcx> { bodies: RefCell>>, external_bodies: RefCell>>, tcx: TyCtxt<'tcx>, + warn_buffer: RefCell>, } impl<'tcx> Environment<'tcx> { @@ -85,6 +86,7 @@ impl<'tcx> Environment<'tcx> { tcx, bodies: RefCell::new(HashMap::new()), external_bodies: RefCell::new(HashMap::new()), + warn_buffer: RefCell::new(Vec::new()), } } @@ -142,15 +144,12 @@ impl<'tcx> Environment<'tcx> { // self.state.session.span_err(sp, msg); // } - /// Emits an error message. - pub fn span_err_with_help_and_notes + Clone>( - &self, + fn configure_diagnostic + Clone, T: EmissionGuarantee>( + diagnostic: &mut DiagnosticBuilder, sp: S, - msg: &str, help: &Option, - notes: &[(String, Option)], + notes: &[(String, Option)] ) { - let mut diagnostic = self.tcx.sess.struct_err(msg); diagnostic.set_span(sp); if let Some(help_msg) = help { diagnostic.help(help_msg); @@ -162,10 +161,25 @@ impl<'tcx> Environment<'tcx> { diagnostic.note(note_msg); } } - diagnostic.emit(); } /// Emits an error message. + pub fn span_err_with_help_and_notes + Clone>( + &self, + sp: S, + msg: &str, + help: &Option, + notes: &[(String, Option)], + ) { + let mut diagnostic = self.tcx.sess.struct_err(msg); + Self::configure_diagnostic(&mut diagnostic, sp, help, notes); + for warn in self.warn_buffer.borrow_mut().iter_mut() { + self.tcx.sess.diagnostic().emit_diagnostic(warn); + } + diagnostic.emit(); + } + + /// Emits a warning message. pub fn span_warn_with_help_and_notes + Clone>( &self, sp: S, @@ -174,20 +188,23 @@ impl<'tcx> Environment<'tcx> { notes: &[(String, Option)], ) { let mut diagnostic = self.tcx.sess.struct_warn(msg); - diagnostic.set_span(sp); - if let Some(help_msg) = help { - diagnostic.help(help_msg); - } - for (note_msg, opt_note_sp) in notes { - if let Some(note_sp) = opt_note_sp { - diagnostic.span_note(note_sp.clone(), note_msg); - } else { - diagnostic.note(note_msg); - } - } + Self::configure_diagnostic(&mut diagnostic, sp, help, notes); diagnostic.emit(); } + /// Buffers a warning message, to be emitted on error. + pub fn span_warn_on_err_with_help_and_notes + Clone>( + &self, + sp: S, + msg: &str, + help: &Option, + notes: &[(String, Option)], + ) { + let mut diagnostic = self.tcx.sess.struct_warn(msg); + Self::configure_diagnostic(&mut diagnostic, sp, help, notes); + diagnostic.buffer(&mut self.warn_buffer.borrow_mut()); + } + /// Returns true if an error has been emitted pub fn has_errors(&self) -> bool { self.tcx.sess.has_errors().is_some() diff --git a/prusti-interface/src/prusti_error.rs b/prusti-interface/src/prusti_error.rs index 66991af4ab4..6367f04193b 100644 --- a/prusti-interface/src/prusti_error.rs +++ b/prusti-interface/src/prusti_error.rs @@ -21,7 +21,7 @@ use ::log::warn; /// `SpannedEncodingError` and similar types to something less confusing.) #[derive(Clone, Debug, PartialEq, Eq)] pub struct PrustiError { - is_error: bool, + kind: PrustiErrorKind, /// If `true`, it should not be reported to the user. We need this in cases /// when the same error could be reported twice. /// @@ -34,6 +34,13 @@ pub struct PrustiError { help: Option, notes: Vec<(String, Option)>, } +/// Determines how a `PrustiError` is reported. +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum PrustiErrorKind { + Error, Warning, + /// A warning which is only shown if at least one error is emitted. + WarningOnError, +} impl PartialOrd for PrustiError { fn partial_cmp(&self, other: &Self) -> Option { @@ -51,7 +58,7 @@ impl PrustiError { /// Private constructor. Use one of the following methods. fn new(message: String, span: MultiSpan) -> Self { PrustiError { - is_error: true, + kind: PrustiErrorKind::Error, is_disabled: false, message, span, @@ -101,6 +108,29 @@ impl PrustiError { ) } + /// Report a non-fatal issue + pub fn warning(message: S, span: MultiSpan) -> Self { + check_message(message.to_string()); + let mut err = PrustiError::new( + format!("[Prusti: warning] {}", message.to_string()), + span + ); + err.kind = PrustiErrorKind::Warning; + err + } + + /// Report a non-fatal issue only if there are errors + /// (e.g. cannot automatically include loop guard as an invariant) + pub fn warning_on_error(message: S, span: MultiSpan) -> Self { + check_message(message.to_string()); + let mut err = PrustiError::new( + format!("[Prusti: warning] {}", message.to_string()), + span + ); + err.kind = PrustiErrorKind::WarningOnError; + err + } + /// Report an internal error of Prusti (e.g. failure of the fold-unfold) pub fn internal(message: S, span: MultiSpan) -> Self { check_message(message.to_string()); @@ -122,11 +152,11 @@ impl PrustiError { /// Set that this Prusti error should be reported as a warning to the user pub fn set_warning(&mut self) { - self.is_error = false; + self.kind = PrustiErrorKind::Warning; } pub fn is_error(&self) -> bool { - self.is_error + matches!(self.kind, PrustiErrorKind::Error) } // FIXME: This flag is a temporary workaround for having duplicate errors @@ -152,24 +182,31 @@ impl PrustiError { self.notes.push((message.to_string(), opt_span)); } - /// Report the encoding error using the compiler's interface + /// Report the encoding error using the compiler's interface. + /// Warnings are not immediately emitted, but buffered and only shown + /// if an error is emitted (i.e. verification failure) pub fn emit(self, env: &Environment) { assert!(!self.is_disabled); - if self.is_error { - env.span_err_with_help_and_notes( + match self.kind { + PrustiErrorKind::Error => env.span_err_with_help_and_notes( self.span, &self.message, &self.help, &self.notes, - ); - } else { - env.span_warn_with_help_and_notes( + ), + PrustiErrorKind::Warning => env.span_warn_with_help_and_notes( self.span, &self.message, &self.help, &self.notes, - ); - } + ), + PrustiErrorKind::WarningOnError => env.span_warn_on_err_with_help_and_notes( + self.span, + &self.message, + &self.help, + &self.notes, + ), + }; } /// Cancel the error. diff --git a/prusti-tests/tests/verify_overflow/fail/optimizations/purification/test1.rs b/prusti-tests/tests/verify_overflow/fail/optimizations/purification/test1.rs index 6ffbc8f1879..bd358569c12 100644 --- a/prusti-tests/tests/verify_overflow/fail/optimizations/purification/test1.rs +++ b/prusti-tests/tests/verify_overflow/fail/optimizations/purification/test1.rs @@ -5,20 +5,20 @@ use prusti_contracts::*; fn test1() { let mut i = 0; while i < 5 { - i += 1; //~ ERROR: attempt to add with overflow + i += 1; } let mut j = 0; - assert!(i == j); + assert!(i == j); //~ ERROR: the asserted expression might not hold } fn test2() { let mut i = 0; while i < 5 { - assert!(i < 5); //~ ERROR: the asserted expression might not hold + assert!(i < 5); i += 1; } let mut j = 0; - assert!(i == j); + assert!(i == j); //~ ERROR: the asserted expression might not hold } fn test3() { @@ -35,7 +35,7 @@ fn test4(v: &mut[i32]) { let mut zero_num_start = 0; let mut i = 0; while i < v.len() { - assert!(i < v.len()); //~ ERROR: the asserted expression might not hold + assert!(i < v.len()); i += 1; } } @@ -44,8 +44,8 @@ fn test5(v: &mut[i32]) { let mut zero_num_start = 0; let mut i = 0; while i < v.len() { - if v[i] == 0 { //~ ERROR: the array or slice index may be out of bounds - zero_num_start += 1; + if v[i] == 0 { + zero_num_start += 1; //~ ERROR: attempt to add with overflow } i += 1; } diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index f0ceea48318..d1c046837cc 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -28,6 +28,7 @@ use prusti_common::{ use vir_crate::{ polymorphic::{ self as vir, + compute_identifier, borrows::Borrow, collect_assigned_vars, CfgBlockIndex, ExprIterator, Successor, Type}, @@ -42,6 +43,7 @@ use prusti_interface::{ }, BasicBlockIndex, PermissionKind, Procedure, }, + PrustiError, }; use prusti_interface::utils; use rustc_middle::mir::Mutability; @@ -519,6 +521,126 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { Ok(still_unresolved_edges) } + fn stmt_preconditions(&self, stmt: &vir::Stmt) -> Vec<(Option, vir::Expr)> { + use vir::{ExprFolder, StmtWalker}; + struct FindFnApps<'a, 'b, 'c> { + recurse: bool, + preconds: Vec<(Option, vir::Expr)>, + encoder: &'a Encoder<'b, 'c>, + } + fn is_const_true(expr: &vir::Expr) -> bool { + matches!( + expr, + vir::Expr::Const(vir::ConstExpr { + value: vir::Const::Bool(true), .. + }) + ) + } + impl<'a, 'b, 'c> FindFnApps<'a, 'b, 'c> { + fn push_precond(&mut self, expr: vir::Expr, fn_name: Option) { + let expr = self.fold(expr); + if !is_const_true(&expr) { + self.preconds.push((fn_name, expr)); + } + } + } + impl<'a, 'b, 'c> StmtWalker for FindFnApps<'a, 'b, 'c> { + fn walk_exhale(&mut self, statement: &vir::Exhale) { + self.push_precond(statement.expr.clone(), None); + } + fn walk_expr(&mut self, expr: &vir::Expr) { + self.fold(expr.clone()); + } + } + impl<'a, 'b, 'c> ExprFolder for FindFnApps<'a, 'b, 'c> { + fn fold_func_app(&mut self, expr: vir::FuncApp) -> vir::Expr { + let vir::FuncApp { function_name, type_arguments, arguments, formal_arguments, return_type, .. } = expr; + if self.recurse { + let identifier: vir::FunctionIdentifier = + compute_identifier(&function_name, &type_arguments, &formal_arguments, &return_type).into(); + let pres = self.encoder.get_function(&identifier).unwrap().pres.clone(); + // Avoid recursively collecting preconditions: they should be self-framing anyway + self.recurse = false; + let pres: vir::Expr = pres.into_iter().fold(true.into(), |acc, expr| vir_expr! { [acc] && [expr] }); + self.push_precond(pres, Some(function_name)); + self.recurse = true; + + for arg in arguments { + self.fold(arg); + } + } + true.into() + } + fn fold_inhale_exhale(&mut self, expr: vir::InhaleExhale) -> vir::Expr { + // We only care about the exhale part (e.g. for `walk_exhale`) + self.fold(*expr.exhale_expr) + } + fn fold_predicate_access_predicate(&mut self, expr: vir::PredicateAccessPredicate) -> vir::Expr { + self.fold(*expr.argument); + true.into() + } + fn fold_field_access_predicate(&mut self, expr: vir::FieldAccessPredicate) -> vir::Expr { + self.fold(*expr.base); + true.into() + } + fn fold_bin_op(&mut self, expr: vir::BinOp) -> vir::Expr { + let vir::BinOp { op_kind, left, right, position } = expr; + let left = self.fold_boxed(left); + let right = self.fold_boxed(right); + match op_kind { + vir::BinaryOpKind::And if is_const_true(&*left) => *right, + vir::BinaryOpKind::And if is_const_true(&*right) => *left, + vir::BinaryOpKind::Or if is_const_true(&*left) => *left, + vir::BinaryOpKind::Or if is_const_true(&*right) => *right, + _ => vir::Expr::BinOp(vir::BinOp { + op_kind, left, right, position, + }), + } + } + } + let mut walker = FindFnApps { + recurse: true, preconds: Vec::new(), encoder: self.encoder + }; + walker.walk(stmt); + walker.preconds + } + fn block_preconditions(&self, block: &CfgBlockIndex) -> Vec<(Option, vir::Expr)> { + let bb = &self.cfg_method.basic_blocks[block.block_index]; + let mut preconds: Vec<_> = bb.stmts.iter().flat_map(|stmt| self.stmt_preconditions(stmt)).collect(); + match &bb.successor { + Successor::Undefined => (), + Successor::Return => (), + Successor::Goto(cbi) => preconds.extend(self.block_preconditions(cbi)), + Successor::GotoSwitch(succs, def) => { + preconds.extend( + succs.iter().flat_map(|cond_bb| self.block_preconditions(&cond_bb.1)) + ); + preconds.extend(self.block_preconditions(def)); + } + } + preconds + } + fn block_assert_to_assume(&mut self, block: &CfgBlockIndex) { + let bb = &mut self.cfg_method.basic_blocks[block.block_index]; + for stmt in &mut bb.stmts { + if let vir::Stmt::Assert(assert) = stmt { + let expr = assert.expr.clone(); + *stmt = vir::Stmt::Inhale(vir::Inhale { expr }); + } + } + match bb.successor.clone() { + Successor::Undefined => (), + Successor::Return => (), + Successor::Goto(cbi) => self.block_assert_to_assume(&cbi), + Successor::GotoSwitch(succs, def) => { + for (_, succ) in succs { + self.block_assert_to_assume(&succ); + } + self.block_assert_to_assume(&def) + } + } + } + /// Encodes a loop. /// /// Returns: @@ -660,6 +782,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { )?; heads.push(first_b1_head); + // Calculate if `G` and `B1` are safe to include as the first `body_invariant!(...)` + let mut preconds = first_g_head.map(|cbi| self.block_preconditions(&cbi)).unwrap_or_default(); + preconds.extend(first_b1_head.map(|cbi| self.block_preconditions(&cbi)).unwrap_or_default()); + // Build the "invariant" CFG block (start - G - B1 - *invariant* - B2 - G - B1 - end) // (1) checks the loop invariant on entry // (2) havocs the invariant and the local variables. @@ -670,28 +796,89 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { loop_label_prefix ))], ); - let inv_post_block = self.cfg_method.add_block( - &format!("{}_inv_post", loop_label_prefix), + let inv_post_block_perms = self.cfg_method.add_block( + &format!("{}_inv_post_perm", loop_label_prefix), + vec![vir::Stmt::comment(format!( + "========== {}_inv_post_perm ==========", + loop_label_prefix + ))], + ); + let inv_post_block_fnspc = self.cfg_method.add_block( + &format!("{}_inv_post_fnspc", loop_label_prefix), vec![vir::Stmt::comment(format!( - "========== {}_inv_post ==========", + "========== {}_inv_post_fnspc ==========", loop_label_prefix ))], ); heads.push(Some(inv_pre_block)); self.cfg_method - .set_successor(inv_pre_block, vir::Successor::Goto(inv_post_block)); + .set_successor(inv_pre_block, vir::Successor::Goto(inv_post_block_perms)); { let stmts = self.encode_loop_invariant_exhale_stmts(loop_head, before_invariant_block, false)?; self.cfg_method.add_stmts(inv_pre_block, stmts); } // We'll add later more statements at the end of inv_pre_block, to havoc local variables + let fnspec_span = { + let (stmts, fnspec_span) = + self.encode_loop_invariant_inhale_fnspec_stmts(loop_head, before_invariant_block, false)?; + self.cfg_method.add_stmts(inv_post_block_fnspc, stmts); fnspec_span + }; { let stmts = - self.encode_loop_invariant_inhale_stmts(loop_head, before_invariant_block, false)?; - self.cfg_method.add_stmts(inv_post_block, stmts); + self.encode_loop_invariant_inhale_perm_stmts(loop_head, before_invariant_block, false).with_span(fnspec_span)?; + self.cfg_method.add_stmts(inv_post_block_perms, stmts); } + let mid_groups = if preconds.is_empty() { + // Encode the mid G group (start - G - B1 - invariant_perm - *G* - B1 - invariant_fnspec - B2 - G - B1 - end) + let mid_g = self.encode_blocks_group( + &format!("{}_group2a_", loop_label_prefix), + loop_guard_evaluation, + loop_depth, + return_block, + )?; + if let Some(mid_g_head) = &mid_g.0 { + self.block_assert_to_assume(mid_g_head); + } + + // Encode the mid B1 group (start - G - B1 - invariant_perm - G - *B1* - invariant_fnspec - B2 - G - B1 - end) + let mid_b1 = self.encode_blocks_group( + &format!("{}_group2b_", loop_label_prefix), + loop_body_before_inv, + loop_depth, + return_block, + )?; + if let Some(mid_b1_head) = &mid_b1.0 { + self.block_assert_to_assume(mid_b1_head); + } + // Save for later linking up + Some((mid_g, mid_b1)) + } else { + // Cannot add loop guard to loop invariant + let fn_names: Vec<_> = preconds.iter().filter_map(|(name, _)| name.as_ref()).map(|name| { + name.strip_prefix("m_").unwrap_or(name) + }).collect(); + let warning_msg = if fn_names.is_empty() { + "the loop guard was not automatically added as a `body_invariant!(...)`, consider doing this manually".to_string() + } else { + "the loop guard was not automatically added as a `body_invariant!(...)`, \ + due to the following pure functions with preconditions: [".to_string() + &fn_names.join(", ") + "]" + }; + // Span of loop guard + let span_lg = loop_guard_evaluation.last().map(|bb| self.mir_encoder.get_span_of_basic_block(*bb)); + // Span of entire loop body before inv; the last elem (if any) will be the `body_invariant!(...)` bb + let span_lb = loop_body_before_inv.iter().rev().skip(1).map(|bb| self.mir_encoder.get_span_of_basic_block(*bb)) + .fold(None, |acc: Option, span| Some(acc.map(|other| + if span.ctxt() == other.ctxt() { span.to(other) } else { other } + ).unwrap_or(span)) ); + // Multispan to highlight both + let span = MultiSpan::from_spans(vec![span_lg, span_lb].into_iter().flatten().collect()); + // It's only a warning so we might as well emit it straight away + PrustiError::warning(warning_msg, span).emit(self.encoder.env()); + None + }; + // Encode the last B2 group (start - G - B1 - invariant - *B2* - G - B1 - end) let (last_b2_head, last_b2_edges) = self.encode_blocks_group( &format!("{}_group3_", loop_label_prefix), @@ -771,10 +958,60 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { } })?); + if let Some(((mid_g_head, mid_g_edges), (mid_b1_head, mid_b1_edges))) = mid_groups { + let mid_b1_block = mid_b1_head.unwrap_or(inv_post_block_fnspc); + // Link edges of "invariant_perm" (start - G - B1 - *invariant_perm* - G - B1 - invariant_fnspec - B2 - G - B1 - end) + self.cfg_method + .set_successor(inv_post_block_perms, vir::Successor::Goto(mid_g_head.unwrap_or(mid_b1_block))); + + // We know that there is at least one loop iteration of B2, thus it is safe to assume + // that anything beforehand couldn't have exited the loop. Here we use + // `self.cfg_method.set_successor(..., Successor::Return)` as the same as `assume false` + for (curr_block, target) in &mid_g_edges { + if self.loop_encoder.get_loop_depth(*target) < loop_depth { + self.cfg_method.set_successor(*curr_block, Successor::Return); + } + } + let mid_g_edges = mid_g_edges.into_iter().filter(|(_, target)| + self.loop_encoder.get_loop_depth(*target) >= loop_depth + ).collect::>(); + // Link edges from the mid G group (start - G - B1 - invariant_perm - *G* - B1 - invariant_fnspec - B2 - G - B1 - end) + still_unresolved_edges.extend(self.encode_unresolved_edges(mid_g_edges, |bb| { + if bb == after_guard_block { + Some(mid_b1_block) + } else { + None + } + })?); + + // We know that there is at least one loop iteration of B2, thus it is safe to assume + // that anything beforehand couldn't have exited the loop. + for (curr_block, target) in &mid_b1_edges { + if self.loop_encoder.get_loop_depth(*target) < loop_depth { + self.cfg_method.set_successor(*curr_block, Successor::Return); + } + } + let mid_b1_edges = mid_b1_edges.into_iter().filter(|(_, target)| + self.loop_encoder.get_loop_depth(*target) >= loop_depth + ).collect::>(); + // Link edges from the mid B1 group (start - G - B1 - invariant_perm - G - *B1* - invariant_fnspec - B2 - G - B1 - end) + still_unresolved_edges.extend(self.encode_unresolved_edges(mid_b1_edges, |bb| { + if bb == after_inv_block { + Some(inv_post_block_fnspc) + } else { + None + } + })?); + } else { + // Link edges of "invariant_perm" (start - G - B1 - *invariant_perm* - invariant_fnspec - B2 - G - B1 - end) + self.cfg_method + .set_successor(inv_post_block_perms, vir::Successor::Goto(inv_post_block_fnspc)); + } + // Link edges of "invariant" (start - G - B1 - *invariant* - B2 - G - B1 - end) let following_block = heads[4..].iter().find(|x| x.is_some()).unwrap().unwrap(); self.cfg_method - .set_successor(inv_post_block, vir::Successor::Goto(following_block)); + .set_successor(inv_post_block_fnspc, vir::Successor::Goto(following_block)); // Link edges from the last B2 group (start - G - B1 - invariant - *B2* - G - B1 - end) let following_block = heads[5..].iter().find(|x| x.is_some()).unwrap().unwrap(); @@ -836,7 +1073,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { // Done. Phew! Ok((start_block, still_unresolved_edges)) -} + } /// Encode a block. /// @@ -4887,28 +5124,25 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { Ok(stmts) } - fn encode_loop_invariant_inhale_stmts( + fn encode_loop_invariant_inhale_perm_stmts( &mut self, loop_head: BasicBlockIndex, loop_inv_block: BasicBlockIndex, after_loop: bool, - ) -> SpannedEncodingResult> { + ) -> EncodingResult> { trace!( - "[enter] encode_loop_invariant_inhale_stmts loop_head={:?} after_loop={}", + "[enter] encode_loop_invariant_inhale_perm_stmts loop_head={:?} after_loop={}", loop_head, after_loop ); - let (func_spec, func_spec_span) = - self.encode_loop_invariant_specs(loop_head, loop_inv_block)?; let (permissions, equalities, invs_spec) = - self.encode_loop_invariant_permissions(loop_head, loop_inv_block, true) - .with_span(func_spec_span)?; + self.encode_loop_invariant_permissions(loop_head, loop_inv_block, true)?; let permission_expr = permissions.into_iter().conjoin(); let equality_expr = equalities.into_iter().conjoin(); let mut stmts = vec![vir::Stmt::comment(format!( - "Inhale the loop invariant of block {:?}", + "Inhale the loop permissions invariant of block {:?}", loop_head ))]; stmts.push(vir::Stmt::Inhale( vir::Inhale { @@ -4920,10 +5154,31 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { stmts.push(vir::Stmt::Inhale( vir::Inhale { expr: invs_spec.into_iter().conjoin(), })); + Ok(stmts) + } + + fn encode_loop_invariant_inhale_fnspec_stmts( + &mut self, + loop_head: BasicBlockIndex, + loop_inv_block: BasicBlockIndex, + after_loop: bool, + ) -> SpannedEncodingResult<(Vec, MultiSpan)> { + trace!( + "[enter] encode_loop_invariant_inhale_fnspec_stmts loop_head={:?} after_loop={}", + loop_head, + after_loop + ); + let (func_spec, func_spec_span) = + self.encode_loop_invariant_specs(loop_head, loop_inv_block)?; + + let mut stmts = vec![vir::Stmt::comment(format!( + "Inhale the loop fnspec invariant of block {:?}", + loop_head + ))]; stmts.push(vir::Stmt::Inhale( vir::Inhale { expr: func_spec.into_iter().conjoin(), })); - Ok(stmts) + Ok((stmts, func_spec_span)) } fn encode_prusti_local(&self, local: Local) -> vir::LocalVar { diff --git a/vir/defs/polymorphic/ast/expr_transformers.rs b/vir/defs/polymorphic/ast/expr_transformers.rs index 5ecf3e2b20e..c6fe744b85f 100644 --- a/vir/defs/polymorphic/ast/expr_transformers.rs +++ b/vir/defs/polymorphic/ast/expr_transformers.rs @@ -483,85 +483,85 @@ pub trait ExprWalker: Sized { self.walk_type(&var.typ); } - fn walk_local(&mut self, statement: &Local) { - let Local { variable, .. } = statement; + fn walk_local(&mut self, expr: &Local) { + let Local { variable, .. } = expr; self.walk_local_var(variable); } - fn walk_variant(&mut self, statement: &Variant) { + fn walk_variant(&mut self, expr: &Variant) { let Variant { base, variant_index, .. - } = statement; + } = expr; self.walk(base); self.walk_type(&variant_index.typ); } - fn walk_field(&mut self, statement: &FieldExpr) { - let FieldExpr { base, field, .. } = statement; + fn walk_field(&mut self, expr: &FieldExpr) { + let FieldExpr { base, field, .. } = expr; self.walk(base); self.walk_type(&field.typ); } - fn walk_addr_of(&mut self, statement: &AddrOf) { + fn walk_addr_of(&mut self, expr: &AddrOf) { let AddrOf { base, addr_type, .. - } = statement; + } = expr; self.walk(base); self.walk_type(addr_type); } fn walk_const(&mut self, _const_expr: &ConstExpr) {} - fn walk_labelled_old(&mut self, statement: &LabelledOld) { - let LabelledOld { base, .. } = statement; + fn walk_labelled_old(&mut self, expr: &LabelledOld) { + let LabelledOld { base, .. } = expr; self.walk(base); } - fn walk_magic_wand(&mut self, statement: &MagicWand) { - let MagicWand { left, right, .. } = statement; + fn walk_magic_wand(&mut self, expr: &MagicWand) { + let MagicWand { left, right, .. } = expr; self.walk(left); self.walk(right); } - fn walk_predicate_access_predicate(&mut self, statement: &PredicateAccessPredicate) { - let PredicateAccessPredicate { argument, .. } = statement; + fn walk_predicate_access_predicate(&mut self, expr: &PredicateAccessPredicate) { + let PredicateAccessPredicate { argument, .. } = expr; self.walk(argument); } - fn walk_field_access_predicate(&mut self, statement: &FieldAccessPredicate) { - let FieldAccessPredicate { base, .. } = statement; + fn walk_field_access_predicate(&mut self, expr: &FieldAccessPredicate) { + let FieldAccessPredicate { base, .. } = expr; self.walk(base); } - fn walk_unary_op(&mut self, statement: &UnaryOp) { - let UnaryOp { argument, .. } = statement; + fn walk_unary_op(&mut self, expr: &UnaryOp) { + let UnaryOp { argument, .. } = expr; self.walk(argument) } - fn walk_bin_op(&mut self, statement: &BinOp) { - let BinOp { left, right, .. } = statement; + fn walk_bin_op(&mut self, expr: &BinOp) { + let BinOp { left, right, .. } = expr; self.walk(left); self.walk(right); } - fn walk_unfolding(&mut self, statement: &Unfolding) { + fn walk_unfolding(&mut self, expr: &Unfolding) { let Unfolding { arguments, base, .. - } = statement; + } = expr; for arg in arguments { self.walk(arg); } self.walk(base); } - fn walk_cond(&mut self, statement: &Cond) { + fn walk_cond(&mut self, expr: &Cond) { let Cond { guard, then_expr, else_expr, .. - } = statement; + } = expr; self.walk(guard); self.walk(then_expr); self.walk(else_expr); } - fn walk_forall(&mut self, statement: &ForAll) { + fn walk_forall(&mut self, expr: &ForAll) { let ForAll { variables, triggers, body, .. - } = statement; + } = expr; for set in triggers { for expr in set.elements() { self.walk(expr); @@ -572,13 +572,13 @@ pub trait ExprWalker: Sized { } self.walk(body); } - fn walk_exists(&mut self, statement: &Exists) { + fn walk_exists(&mut self, expr: &Exists) { let Exists { variables, triggers, body, .. - } = statement; + } = expr; for set in triggers { for expr in set.elements() { self.walk(expr); @@ -589,24 +589,24 @@ pub trait ExprWalker: Sized { } self.walk(body); } - fn walk_let_expr(&mut self, statement: &LetExpr) { + fn walk_let_expr(&mut self, expr: &LetExpr) { let LetExpr { variable, def, body, .. - } = statement; + } = expr; self.walk_local_var(variable); self.walk(def); self.walk(body); } - fn walk_func_app(&mut self, statement: &FuncApp) { + fn walk_func_app(&mut self, expr: &FuncApp) { let FuncApp { arguments, formal_arguments, return_type, .. - } = statement; + } = expr; for arg in arguments { self.walk(arg) } @@ -615,12 +615,12 @@ pub trait ExprWalker: Sized { } self.walk_type(return_type); } - fn walk_domain_func_app(&mut self, statement: &DomainFuncApp) { + fn walk_domain_func_app(&mut self, expr: &DomainFuncApp) { let DomainFuncApp { domain_function, arguments, .. - } = statement; + } = expr; for arg in arguments { self.walk(arg) } @@ -646,52 +646,52 @@ pub trait ExprWalker: Sized { } } */ - fn walk_inhale_exhale(&mut self, statement: &InhaleExhale) { + fn walk_inhale_exhale(&mut self, expr: &InhaleExhale) { let InhaleExhale { inhale_expr, exhale_expr, .. - } = statement; + } = expr; self.walk(inhale_expr); self.walk(exhale_expr); } - fn walk_downcast(&mut self, statement: &DowncastExpr) { + fn walk_downcast(&mut self, expr: &DowncastExpr) { let DowncastExpr { base, enum_place, .. - } = statement; + } = expr; self.walk(base); self.walk(enum_place); } - fn walk_snap_app(&mut self, statement: &SnapApp) { - let SnapApp { base, .. } = statement; + fn walk_snap_app(&mut self, expr: &SnapApp) { + let SnapApp { base, .. } = expr; self.walk(base); } - fn walk_container_op(&mut self, statement: &ContainerOp) { - let ContainerOp { left, right, .. } = statement; + fn walk_container_op(&mut self, expr: &ContainerOp) { + let ContainerOp { left, right, .. } = expr; self.walk(left); self.walk(right); } - fn walk_seq(&mut self, statement: &Seq) { - let Seq { typ, elements, .. } = statement; + fn walk_seq(&mut self, expr: &Seq) { + let Seq { typ, elements, .. } = expr; for elem in elements { self.walk(elem); } self.walk_type(typ); } - fn walk_map(&mut self, statement: &Map) { - let Map { typ, elements, .. } = statement; + fn walk_map(&mut self, expr: &Map) { + let Map { typ, elements, .. } = expr; for elem in elements { self.walk(elem); } self.walk_type(typ); } - fn walk_cast(&mut self, statement: &Cast) { - let Cast { base, .. } = statement; + fn walk_cast(&mut self, expr: &Cast) { + let Cast { base, .. } = expr; self.walk(base); } } @@ -1189,96 +1189,96 @@ pub trait FallibleExprWalker: Sized { self.fallible_walk_type(&var.typ) } - fn fallible_walk_local(&mut self, statement: &Local) -> Result<(), Self::Error> { - let Local { variable, .. } = statement; + fn fallible_walk_local(&mut self, expr: &Local) -> Result<(), Self::Error> { + let Local { variable, .. } = expr; self.fallible_walk_local_var(variable) } - fn fallible_walk_variant(&mut self, statement: &Variant) -> Result<(), Self::Error> { + fn fallible_walk_variant(&mut self, expr: &Variant) -> Result<(), Self::Error> { let Variant { base, variant_index, .. - } = statement; + } = expr; self.fallible_walk(base)?; self.fallible_walk_type(&variant_index.typ) } - fn fallible_walk_field(&mut self, statement: &FieldExpr) -> Result<(), Self::Error> { - let FieldExpr { base, field, .. } = statement; + fn fallible_walk_field(&mut self, expr: &FieldExpr) -> Result<(), Self::Error> { + let FieldExpr { base, field, .. } = expr; self.fallible_walk(base)?; self.fallible_walk_type(&field.typ) } - fn fallible_walk_addr_of(&mut self, statement: &AddrOf) -> Result<(), Self::Error> { + fn fallible_walk_addr_of(&mut self, expr: &AddrOf) -> Result<(), Self::Error> { let AddrOf { base, addr_type, .. - } = statement; + } = expr; self.fallible_walk(base)?; self.fallible_walk_type(addr_type) } fn fallible_walk_const(&mut self, _const_expr: &ConstExpr) -> Result<(), Self::Error> { Ok(()) } - fn fallible_walk_labelled_old(&mut self, statement: &LabelledOld) -> Result<(), Self::Error> { - let LabelledOld { base, .. } = statement; + fn fallible_walk_labelled_old(&mut self, expr: &LabelledOld) -> Result<(), Self::Error> { + let LabelledOld { base, .. } = expr; self.fallible_walk(base) } - fn fallible_walk_magic_wand(&mut self, statement: &MagicWand) -> Result<(), Self::Error> { - let MagicWand { left, right, .. } = statement; + fn fallible_walk_magic_wand(&mut self, expr: &MagicWand) -> Result<(), Self::Error> { + let MagicWand { left, right, .. } = expr; self.fallible_walk(left)?; self.fallible_walk(right)?; Ok(()) } fn fallible_walk_predicate_access_predicate( &mut self, - statement: &PredicateAccessPredicate, + expr: &PredicateAccessPredicate, ) -> Result<(), Self::Error> { - let PredicateAccessPredicate { argument, .. } = statement; + let PredicateAccessPredicate { argument, .. } = expr; self.fallible_walk(argument) } fn fallible_walk_field_access_predicate( &mut self, - statement: &FieldAccessPredicate, + expr: &FieldAccessPredicate, ) -> Result<(), Self::Error> { - let FieldAccessPredicate { base, .. } = statement; + let FieldAccessPredicate { base, .. } = expr; self.fallible_walk(base) } - fn fallible_walk_unary_op(&mut self, statement: &UnaryOp) -> Result<(), Self::Error> { - let UnaryOp { argument, .. } = statement; + fn fallible_walk_unary_op(&mut self, expr: &UnaryOp) -> Result<(), Self::Error> { + let UnaryOp { argument, .. } = expr; self.fallible_walk(argument) } - fn fallible_walk_bin_op(&mut self, statement: &BinOp) -> Result<(), Self::Error> { - let BinOp { left, right, .. } = statement; + fn fallible_walk_bin_op(&mut self, expr: &BinOp) -> Result<(), Self::Error> { + let BinOp { left, right, .. } = expr; self.fallible_walk(left)?; self.fallible_walk(right)?; Ok(()) } - fn fallible_walk_unfolding(&mut self, statement: &Unfolding) -> Result<(), Self::Error> { + fn fallible_walk_unfolding(&mut self, expr: &Unfolding) -> Result<(), Self::Error> { let Unfolding { arguments, base, .. - } = statement; + } = expr; for arg in arguments { self.fallible_walk(arg)?; } self.fallible_walk(base) } - fn fallible_walk_cond(&mut self, statement: &Cond) -> Result<(), Self::Error> { + fn fallible_walk_cond(&mut self, expr: &Cond) -> Result<(), Self::Error> { let Cond { guard, then_expr, else_expr, .. - } = statement; + } = expr; self.fallible_walk(guard)?; self.fallible_walk(then_expr)?; self.fallible_walk(else_expr)?; Ok(()) } - fn fallible_walk_forall(&mut self, statement: &ForAll) -> Result<(), Self::Error> { + fn fallible_walk_forall(&mut self, expr: &ForAll) -> Result<(), Self::Error> { let ForAll { variables, triggers, body, .. - } = statement; + } = expr; for var in variables { self.fallible_walk_local_var(var)?; } @@ -1289,13 +1289,13 @@ pub trait FallibleExprWalker: Sized { } self.fallible_walk(body) } - fn fallible_walk_exists(&mut self, statement: &Exists) -> Result<(), Self::Error> { + fn fallible_walk_exists(&mut self, expr: &Exists) -> Result<(), Self::Error> { let Exists { variables, triggers, body, .. - } = statement; + } = expr; for var in variables { self.fallible_walk_local_var(var)?; } @@ -1306,25 +1306,25 @@ pub trait FallibleExprWalker: Sized { } self.fallible_walk(body) } - fn fallible_walk_let_expr(&mut self, statement: &LetExpr) -> Result<(), Self::Error> { + fn fallible_walk_let_expr(&mut self, expr: &LetExpr) -> Result<(), Self::Error> { let LetExpr { variable, def, body, .. - } = statement; + } = expr; self.fallible_walk_local_var(variable)?; self.fallible_walk(def)?; self.fallible_walk(body)?; Ok(()) } - fn fallible_walk_func_app(&mut self, statement: &FuncApp) -> Result<(), Self::Error> { + fn fallible_walk_func_app(&mut self, expr: &FuncApp) -> Result<(), Self::Error> { let FuncApp { arguments, formal_arguments, return_type, .. - } = statement; + } = expr; for arg in arguments { self.fallible_walk(arg)?; } @@ -1333,15 +1333,12 @@ pub trait FallibleExprWalker: Sized { } self.fallible_walk_type(return_type) } - fn fallible_walk_domain_func_app( - &mut self, - statement: &DomainFuncApp, - ) -> Result<(), Self::Error> { + fn fallible_walk_domain_func_app(&mut self, expr: &DomainFuncApp) -> Result<(), Self::Error> { let DomainFuncApp { domain_function, arguments, .. - } = statement; + } = expr; for arg in arguments { self.fallible_walk(arg)?; } @@ -1367,56 +1364,56 @@ pub trait FallibleExprWalker: Sized { } } */ - fn fallible_walk_inhale_exhale(&mut self, statement: &InhaleExhale) -> Result<(), Self::Error> { + fn fallible_walk_inhale_exhale(&mut self, expr: &InhaleExhale) -> Result<(), Self::Error> { let InhaleExhale { inhale_expr, exhale_expr, .. - } = statement; + } = expr; self.fallible_walk(inhale_expr)?; self.fallible_walk(exhale_expr)?; Ok(()) } - fn fallible_walk_downcast(&mut self, statement: &DowncastExpr) -> Result<(), Self::Error> { + fn fallible_walk_downcast(&mut self, expr: &DowncastExpr) -> Result<(), Self::Error> { let DowncastExpr { base, enum_place, .. - } = statement; + } = expr; self.fallible_walk(base)?; self.fallible_walk(enum_place)?; Ok(()) } - fn fallible_walk_snap_app(&mut self, statement: &SnapApp) -> Result<(), Self::Error> { - let SnapApp { base, .. } = statement; + fn fallible_walk_snap_app(&mut self, expr: &SnapApp) -> Result<(), Self::Error> { + let SnapApp { base, .. } = expr; self.fallible_walk(base) } - fn fallible_walk_container_op(&mut self, statement: &ContainerOp) -> Result<(), Self::Error> { - let ContainerOp { left, right, .. } = statement; + fn fallible_walk_container_op(&mut self, expr: &ContainerOp) -> Result<(), Self::Error> { + let ContainerOp { left, right, .. } = expr; self.fallible_walk(left)?; self.fallible_walk(right)?; Ok(()) } - fn fallible_walk_seq(&mut self, statement: &Seq) -> Result<(), Self::Error> { - let Seq { typ, elements, .. } = statement; + fn fallible_walk_seq(&mut self, expr: &Seq) -> Result<(), Self::Error> { + let Seq { typ, elements, .. } = expr; for elem in elements { self.fallible_walk(elem)?; } self.fallible_walk_type(typ) } - fn fallible_walk_map(&mut self, statement: &Map) -> Result<(), Self::Error> { - let Map { typ, elements, .. } = statement; + fn fallible_walk_map(&mut self, expr: &Map) -> Result<(), Self::Error> { + let Map { typ, elements, .. } = expr; for elem in elements { self.fallible_walk(elem)?; } self.fallible_walk_type(typ) } - fn fallible_walk_cast(&mut self, statement: &Cast) -> Result<(), Self::Error> { - let Cast { base, .. } = statement; + fn fallible_walk_cast(&mut self, expr: &Cast) -> Result<(), Self::Error> { + let Cast { base, .. } = expr; self.fallible_walk(base) } } diff --git a/vir/defs/polymorphic/ast/function.rs b/vir/defs/polymorphic/ast/function.rs index 057ba7f4c33..25e336afc8f 100644 --- a/vir/defs/polymorphic/ast/function.rs +++ b/vir/defs/polymorphic/ast/function.rs @@ -105,7 +105,9 @@ pub fn compute_identifier( ) -> String { let mut identifier = name.to_string(); // Include the signature of the function in the function name - identifier.push_str("__$TY$__"); + if !type_arguments.is_empty() { + identifier.push_str("__$TY$__"); + } fn type_name(typ: &Type) -> String { match typ { Type::Int => "$int$".to_string(),