From c4920777e358e44740efff32be01ea3cd19f999f Mon Sep 17 00:00:00 2001 From: Vytautas Astrauskas Date: Tue, 21 Mar 2023 13:48:47 +0100 Subject: [PATCH] Ugly commit 1. --- prusti-utils/src/config.rs | 14 +++- .../symbolic_execution/heap/finalizer.rs | 8 +++ .../symbolic_execution/heap/mod.rs | 3 + .../transformations/symbolic_execution/mod.rs | 14 +++- .../trace_builder/heap_view.rs | 15 ++++ .../symbolic_execution/trace_builder/mod.rs | 70 ++++++++++++++++++- 6 files changed, 120 insertions(+), 4 deletions(-) diff --git a/prusti-utils/src/config.rs b/prusti-utils/src/config.rs index 85ac688f5eb..df4bc701f8b 100644 --- a/prusti-utils/src/config.rs +++ b/prusti-utils/src/config.rs @@ -122,6 +122,7 @@ lazy_static::lazy_static! { settings.set_default("custom_heap_encoding", false).unwrap(); settings.set_default("trace_with_symbolic_execution", false).unwrap(); settings.set_default("purify_with_symbolic_execution", false).unwrap(); + settings.set_default("symbolic_execution_single_method", false).unwrap(); settings.set_default("expand_quantifiers", false).unwrap(); settings.set_default("report_symbolic_execution_failures", false).unwrap(); settings.set_default("report_symbolic_execution_purification", false).unwrap(); @@ -922,7 +923,18 @@ pub fn trace_with_symbolic_execution() -> bool { /// **Note:** This option automatically enables /// `trace_with_symbolic_execution`. pub fn purify_with_symbolic_execution() -> bool { - read_setting("purify_with_symbolic_execution") + read_setting("purify_with_symbolic_execution") || symbolic_execution_single_method() +} + +/// Puts all symbolic execution traces into a single method. +/// +/// **Note:** This option is taken into account only when `unsafe_core_proof` is +/// true. +/// +/// **Note:** This option automatically enables +/// `purify_with_symbolic_execution`. +pub fn symbolic_execution_single_method() -> bool { + read_setting("symbolic_execution_single_method") } /// Whether to expand the asserted quantifiers (skolemize them out). diff --git a/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/heap/finalizer.rs b/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/heap/finalizer.rs index 805d41703c0..dfbf0e3f41f 100644 --- a/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/heap/finalizer.rs +++ b/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/heap/finalizer.rs @@ -71,6 +71,14 @@ impl<'a, EC: EncoderContext> TraceFinalizer<'a, EC> { } } + pub(super) fn trace_len(&self) -> usize { + self.trace.len() + } + + pub(super) fn trace_suffix(&self, checkpoint: usize) -> &[vir_low::Statement] { + self.trace[checkpoint..].as_ref() + } + pub(super) fn add_variables( &mut self, new_variables: &[vir_low::VariableDecl], 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 9afcbb35da1..ea0f85fcfc7 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 @@ -192,9 +192,12 @@ impl<'a> ExecutionTraceBuilder<'a> { } trace_finalizer.add_variables(block.get_new_variables())?; trace_finalizer.add_labels(block.get_new_labels())?; + let trace_checkpoint = trace_finalizer.trace_len(); for (entry_id, entry) in block.iter_entries().enumerate() { trace_finalizer.add_entry(Location { block_id, entry_id }, entry)?; } + let finalized_statements = trace_finalizer.trace_suffix(trace_checkpoint); + block.set_finalized_statements(finalized_statements); Ok(()) } } 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 144b326bfb1..33b9be49efe 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 @@ -300,9 +300,19 @@ impl<'a, 'c, EC: EncoderContext> ProcedureExecutor<'a, 'c, EC> { } } if config::purify_with_symbolic_execution() { - for (i, trace) in self.final_traces.into_iter().enumerate() { - let new_procedure = trace.into_procedure(i, &procedure); + if config::symbolic_execution_single_method() { + let new_procedure = self.execution_trace_builder.into_procedure(&procedure); + prusti_common::report::log::report_with_writer( + "graphviz_method_vir_low_symbex_single_method", + format!("{}.{}.dot", self.source_filename, new_procedure.name), + |writer| new_procedure.to_graphviz(writer).unwrap(), + ); new_procedures.push(new_procedure); + } else { + for (i, trace) in self.final_traces.into_iter().enumerate() { + let new_procedure = trace.into_procedure(i, &procedure); + new_procedures.push(new_procedure); + } } } else { for (i, trace) in self.original_traces.into_iter().enumerate() { diff --git a/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/trace_builder/heap_view.rs b/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/trace_builder/heap_view.rs index 971b1a8bc50..26d79bbbdc4 100644 --- a/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/trace_builder/heap_view.rs +++ b/prusti-viper/src/encoder/middle/core_proof/transformations/symbolic_execution/trace_builder/heap_view.rs @@ -50,4 +50,19 @@ impl<'a> BlockView<'a> { pub(in super::super) fn get_new_labels(&self) -> &[vir_low::Label] { &self.block.new_labels } + + pub(crate) fn set_finalized_statements(&self, new_statements: &[vir_low::Statement]) { + let mut borrow = self.block.finalized_statements.borrow_mut(); + if let Some(statements) = borrow.as_ref() { + // FIXME: This does not work because whether an inhale is purified + // out depends on whether a matching exhale is found, which depends + // on the executed trace. + for (old, new) in statements.iter().zip(new_statements.iter()) { + assert_eq!(old, new); + } + assert_eq!(statements.len(), new_statements.len()); + } else { + *borrow = Some(new_statements.to_vec()); + } + } } 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 291f8cb4c3b..3951d5a4d1e 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 @@ -16,7 +16,7 @@ use crate::encoder::{ use rustc_hash::FxHashMap; use std::collections::BTreeMap; use vir_crate::{ - common::graphviz::ToGraphviz, + common::{expression::BinaryOperationHelpers, graphviz::ToGraphviz}, low::{self as vir_low}, }; @@ -227,6 +227,70 @@ impl<'a> ExecutionTraceBuilder<'a> { assert_eq!(last_block.heap_statements.len(), 1); Ok(()) } + + pub(super) fn into_procedure( + mut self, + original_procedure: &vir_low::ProcedureDecl, + ) -> vir_low::ProcedureDecl { + let entry = vir_low::Label::new("trace_start"); + let exit = vir_low::Label::new("trace_end"); + let mut jump_targets = vec![Vec::new(); self.blocks.len()]; + for (i, block) in self.blocks.iter().enumerate() { + if let Some(parent) = block.parent { + jump_targets[parent].push(i); + } + } + let mut locals = original_procedure.locals.clone(); + let mut custom_labels = original_procedure.custom_labels.clone(); + let mut basic_blocks = BTreeMap::new(); + for (i, block) in std::mem::take(&mut self.blocks).into_iter().enumerate() { + let mut statements = block.finalized_statements.borrow_mut().take().unwrap(); + let successor = match jump_targets[i].len() { + 0 => vir_low::Successor::Goto(exit.clone()), + 1 => vir_low::Successor::Goto(vir_low::Label::new(format!( + "trace_block_{}", + jump_targets[i][0] + ))), + _ => { + let mut targets = Vec::new(); + let variable = vir_low::VariableDecl::new( + format!("trace_block_{}_guard", i), + vir_low::Type::Int, + ); + for (j, target) in jump_targets[i].iter().enumerate() { + let guard = vir_low::Expression::equals(variable.clone().into(), j.into()); + let label = vir_low::Label::new(format!("trace_block_{}", target)); + targets.push((guard, label)); + } + statements.push(vir_low::Statement::assume( + vir_low::Expression::and( + vir_low::Expression::greater_equals(0.into(), variable.clone().into()), + vir_low::Expression::less_than( + variable.into(), + jump_targets[i].len().into(), + ), + ), + original_procedure.position, + )); + vir_low::Successor::GotoSwitch(targets) + } + }; + let basic_block = vir_low::BasicBlock::new(statements, successor); + basic_blocks.insert( + vir_low::Label::new(format!("trace_block_{}", i)), + basic_block, + ); + } + vir_low::ProcedureDecl::new_with_pos( + format!("{}$trace", original_procedure.name), + locals, + custom_labels, + entry, + exit, + basic_blocks, + original_procedure.position, + ) + } } struct ExecutionTraceBlock { @@ -240,6 +304,8 @@ struct ExecutionTraceBlock { original_statements: Vec, /// Statements that make the heap operations more explicit. heap_statements: Vec, + /// Statements after all the transformations. + finalized_statements: std::cell::RefCell>>, /// The last heap state. If the block is fully executed, it is the state /// after the last statement. heap_state: HeapState, @@ -260,6 +326,7 @@ impl ExecutionTraceBlock { new_labels: Vec::new(), original_statements: Vec::new(), heap_statements: Vec::new(), + finalized_statements: std::cell::RefCell::new(None), heap_state: HeapState::default(), egraph_state: Some(EGraphState::new(domains, bool_type, bool_domain_info)?), }) @@ -272,6 +339,7 @@ impl ExecutionTraceBlock { new_labels: Vec::new(), original_statements: Vec::new(), heap_statements: Vec::new(), + finalized_statements: std::cell::RefCell::new(None), heap_state: parent.heap_state.clone(), egraph_state: parent.egraph_state.clone(), }