From 4e1853048e81e6c105313c2b14afa88d1ddbf5d3 Mon Sep 17 00:00:00 2001 From: Vytautas Astrauskas <vastrauskas@gmail.com> Date: Thu, 19 Jan 2023 17:20:43 +0100 Subject: [PATCH] Ugly commit. --- .../symbolic_execution/heap/mod.rs | 3 +- .../heap/predicate_snapshots.rs | 39 +++++++++++++++---- .../transformations/symbolic_execution/mod.rs | 9 +++-- .../symbolic_execution/trace_builder/mod.rs | 3 -- 4 files changed, 38 insertions(+), 16 deletions(-) diff --git a/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/heap/mod.rs b/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/heap/mod.rs index b34efc747e2..98f1c7c1a14 100644 --- a/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/heap/mod.rs +++ b/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/heap/mod.rs @@ -12,6 +12,7 @@ use super::{ trace_builder::{ExecutionTraceBuilder, ExecutionTraceHeapView}, VerificationResult, }; +use log::debug; use rustc_hash::FxHashMap; use std::collections::BTreeMap; use vir_crate::{ @@ -144,7 +145,7 @@ impl ExecutionTraceBuilder { &self, program: &ProgramContext, ) -> VerificationResult<Trace> { - eprintln!("Finalizing trace"); + debug!("Finalizing trace"); let (state, solver) = self.current_heap_and_egraph_state(); let view = self.heap_view(); let last_block_id = view.last_block_id(); diff --git a/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/heap/predicate_snapshots.rs b/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/heap/predicate_snapshots.rs index eb9747c651e..f1978ad4fe7 100644 --- a/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/heap/predicate_snapshots.rs +++ b/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/heap/predicate_snapshots.rs @@ -20,12 +20,16 @@ impl PredicateSnapshots { let predicate_snapshots = self.snapshots.entry(predicate.name.clone()).or_default(); let snapshot_variable_name = format!("snapshot${}${}", predicate.name, predicate_snapshots.len()); - let ty = program_context.get_snapshot_type(&predicate.name).unwrap(); - let snapshot = vir_low::VariableDecl::new(snapshot_variable_name, ty); - self.variables.push(snapshot.clone()); + let snapshot = if let Some(ty) = program_context.get_snapshot_type(&predicate.name) { + let snapshot = vir_low::VariableDecl::new(snapshot_variable_name, ty); + self.variables.push(snapshot.clone()); + PredicateSnapshotState::Inhaled(snapshot) + } else { + PredicateSnapshotState::NoSnapshot + }; predicate_snapshots.push(PredicateSnapshot { arguments: predicate.arguments.clone(), - snapshot: Some(snapshot), + snapshot, }); } @@ -36,10 +40,10 @@ impl PredicateSnapshots { ) -> VerificationResult<()> { let predicate_snapshots = self.snapshots.get_mut(&predicate.name).unwrap(); for predicate_snapshot in predicate_snapshots { - if predicate_snapshot.snapshot.is_some() + if predicate_snapshot.snapshot.is_not_exhaled() && predicate_snapshot.matches(predicate, solver)? { - predicate_snapshot.snapshot = None; + predicate_snapshot.snapshot = PredicateSnapshotState::Exhaled; } } Ok(()) @@ -53,7 +57,7 @@ impl PredicateSnapshots { ) -> VerificationResult<Option<vir_low::VariableDecl>> { if let Some(predicate_snapshots) = self.snapshots.get(predicate_name) { for predicate_snapshot in predicate_snapshots { - if let Some(snapshot) = &predicate_snapshot.snapshot { + if let PredicateSnapshotState::Inhaled(snapshot) = &predicate_snapshot.snapshot { if predicate_snapshot.matches_arguments(arguments, solver)? { return Ok(Some(snapshot.clone())); } @@ -68,12 +72,31 @@ impl PredicateSnapshots { } } +#[derive(Clone)] +enum PredicateSnapshotState { + /// The snapshot is valid. + Inhaled(vir_low::VariableDecl), + /// The snapshot was exhaled and no longer valid. + Exhaled, + /// The predicate does not have a snapshot. + NoSnapshot, +} + +impl PredicateSnapshotState { + pub(super) fn is_not_exhaled(&self) -> bool { + matches!( + self, + PredicateSnapshotState::Inhaled(_) | PredicateSnapshotState::NoSnapshot + ) + } +} + #[derive(Clone)] pub(super) struct PredicateSnapshot { /// Predicate arguments. arguments: Vec<vir_low::Expression>, /// None means that the corresponding predicate was exhaled. - snapshot: Option<vir_low::VariableDecl>, + snapshot: PredicateSnapshotState, } impl PredicateSnapshot { diff --git a/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/mod.rs b/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/mod.rs index 2aff3502d91..fed74605550 100644 --- a/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/mod.rs +++ b/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/mod.rs @@ -16,6 +16,7 @@ use self::{egg::EGraphState, program_context::ProgramContext}; use crate::encoder::{ errors::SpannedEncodingResult, middle::core_proof::predicates::PredicateInfo, }; +use log::debug; use prusti_common::config; use rustc_hash::FxHashMap; use std::collections::BTreeMap; @@ -137,7 +138,7 @@ impl<'a> ProcedureExecutor<'a> { procedure: vir_low::ProcedureDecl, new_procedures: &mut Vec<vir_low::ProcedureDecl>, ) -> VerificationResult<()> { - eprintln!("Executing procedure {}", procedure.name); + debug!("Executing procedure {}", procedure.name); let mut current_block = procedure.entry.clone(); loop { let block = procedure.basic_blocks.get(¤t_block).unwrap(); @@ -248,7 +249,7 @@ impl<'a> ProcedureExecutor<'a> { default_position: vir_low::Position, ) -> VerificationResult<Option<vir_low::Label>> { while let Some(continuation) = self.continuations.pop() { - eprintln!("Rolling back to {}", continuation.parent_block_label); + debug!("Rolling back to {}", continuation.parent_block_label); self.execution_trace_builder .rollback_to_split_point(continuation.parent_block_label)?; self.assume_condition(continuation.condition, default_position)?; @@ -257,7 +258,7 @@ impl<'a> ProcedureExecutor<'a> { .current_egraph_state() .is_inconsistent()? { - eprintln!("Inconsistent after rollback"); + debug!("Inconsistent after rollback"); self.execution_trace_builder.remove_last_block()?; } else { return Ok(Some(continuation.next_block_label)); @@ -286,7 +287,7 @@ impl<'a> ProcedureExecutor<'a> { current_block: &vir_low::Label, block: &vir_low::BasicBlock, ) -> VerificationResult<()> { - eprintln!("Executing block {}", current_block); + debug!("Executing block {}", current_block); for statement in &block.statements { self.execute_statement(current_block, statement)?; } diff --git a/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/trace_builder/mod.rs b/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/trace_builder/mod.rs index 61a88cd1ea6..58e4dab542f 100644 --- a/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/trace_builder/mod.rs +++ b/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/trace_builder/mod.rs @@ -149,9 +149,6 @@ impl ExecutionTraceBuilder { }; self.finalize_original_trace_for_block(&mut original_trace, self.blocks.len() - 1)?; let final_trace = self.heap_finalize_trace(program)?; - for v in &final_trace.variables { - eprintln!("final trace variable: {}", v); - } Ok((original_trace, final_trace)) }