diff --git a/case_studies/tests/src/lib.rs b/case_studies/tests/src/lib.rs
index 041a9e336e9cdaba0352aa350483e18fa50cd84d..225e603f824808938cd9b715c98f258d1625fd53 100644
--- a/case_studies/tests/src/lib.rs
+++ b/case_studies/tests/src/lib.rs
@@ -12,7 +12,7 @@ mod traits;
mod statics;
-//mod vec_client;
+mod vec_client;
mod mixed;
mod closures;
@@ -23,3 +23,5 @@ mod consts;
mod generics;
mod rectypes;
+
+mod loops;
diff --git a/case_studies/tests/src/loops.rs b/case_studies/tests/src/loops.rs
new file mode 100644
index 0000000000000000000000000000000000000000..4f8f685ad529251cb51e083c8ea82870ecfa3cc6
--- /dev/null
+++ b/case_studies/tests/src/loops.rs
@@ -0,0 +1,61 @@
+
+// TODO write some simple test cases
+
+
+#[rr::verify]
+fn loop1() {
+
+ let mut x = 0;
+
+ while x < 5 {
+ let _ = #[rr::exists("i")]
+ #[rr::inv_var("x": "#i")]
+ #[rr::inv("(0 ≤ i ≤ 5)%Z")]
+ #[rr::ignore] ||{};
+
+ x += 1;
+ }
+
+ assert!(x == 5);
+}
+
+
+// Basic infinite loop test
+#[rr::verify]
+#[allow(unreachable_code)]
+#[allow(clippy::self_assignment)]
+fn loop2() {
+ let mut x = 0;
+
+ loop {
+ let _ =
+ #[rr::inv_var("x": "#0%Z")]
+ #[rr::ignore] ||{};
+
+ x = x;
+ }
+
+ unreachable!();
+}
+
+
+// Demonstrates that we need definitely-initialized analysis.
+// (interestingly, this still partially works without, because we just do one loop unfolding
+// without an invariant if it's not initialized yet...)
+#[rr::verify]
+fn loop3() {
+ let mut x = 0;
+
+ while x < 5 {
+ let _ = #[rr::exists("i")]
+ #[rr::inv_var("x": "#i")]
+ #[rr::inv("(0 ≤ i ≤ 5)%Z")]
+ #[rr::ignore] ||{};
+
+ let y = 0;
+
+ x += 1 + y;
+ }
+
+ assert!(x == 5);
+}
diff --git a/rr_frontend/radium/src/code.rs b/rr_frontend/radium/src/code.rs
index a1c9c9f6a1a6be68da67cc8661118424f13848fd..c179b399b9c7a09eddc8220389851b97fc703277 100644
--- a/rr_frontend/radium/src/code.rs
+++ b/rr_frontend/radium/src/code.rs
@@ -761,9 +761,32 @@ impl FunctionCodeBuilder {
}
}
+/// Classifies the kind of a local variable similar to `mir::LocalKind`,
+/// but distinguishes user-specified locals from compiler-generated temporaries.
+#[derive(PartialEq, Eq, Debug, Clone)]
+pub enum LocalKind {
+ Arg,
+ Local,
+ CompilerTemp,
+}
+
+impl LocalKind {
+ #[must_use]
+ pub fn mk_local_name(&self, name: &str) -> String {
+ match self {
+ Self::Arg => {
+ format!("arg_{name}")
+ },
+ Self::CompilerTemp | Self::Local => {
+ format!("local_{name}")
+ },
+ }
+ }
+}
+
#[derive(Clone, Debug, Display)]
#[display("({}PolyNil)", display_list!(_0, "",
- |(bb, spec)| format!("PolyCons (\"_bb{}\", wrap_inv ({})) $ ", bb, spec.func_predicate))
+ |(bb, spec)| format!("PolyCons (\"_bb{}\", {}) $ ", bb, spec))
)]
struct InvariantMap(HashMap<usize, LoopSpec>);
@@ -1019,21 +1042,23 @@ impl<'def> Function<'def> {
}
write!(f, " );\n")?;
- write!(f, "set (loop_map := BB_INV_MAP {});\n", self.loop_invariants)?;
-
// intro stack locations
write!(f, "intros")?;
for Variable((arg, _)) in &self.code.stack_layout.args {
- write!(f, " arg_{}", arg)?;
+ write!(f, " arg_{}", LocalKind::Arg.mk_local_name(arg))?;
}
for Variable((local, _)) in &self.code.stack_layout.locals {
- write!(f, " local_{}", local)?;
+ write!(f, " {}", LocalKind::Local.mk_local_name(local))?;
}
-
write!(f, ";\n")?;
+ write!(f, "let π := get_π in\n")?;
+ write!(f, "let Σ := get_Σ in\n")?;
+
+ write!(f, "set (loop_map := BB_INV_MAP {});\n", self.loop_invariants)?;
+
// destruct specification-level parameters
/*
if let Some(params) = params {
diff --git a/rr_frontend/radium/src/specs.rs b/rr_frontend/radium/src/specs.rs
index 72a0e4ac25360ff35dad2d8109587278c0456a0a..3e40423cda0bf18e641c1cfc11a6a5c68c3d3329 100644
--- a/rr_frontend/radium/src/specs.rs
+++ b/rr_frontend/radium/src/specs.rs
@@ -2737,8 +2737,11 @@ impl Display for IProp {
Self::Conj(v) => fmt_with_op(v, "∧", f),
Self::Wand(l, r) => write!(f, "({l}) -∗ {r}"),
Self::Exists(b, p) => {
- fmt_binders(b, "∃", f)?;
- write!(f, ", {p}")
+ if !b.is_empty() {
+ fmt_binders(b, "∃", f)?;
+ write!(f, ", ")?;
+ }
+ write!(f, "{p}")
},
Self::All(b, p) => {
fmt_binders(b, "∀", f)?;
@@ -2770,14 +2773,24 @@ impl Display for IPropPredicate {
}
/// Representation of a loop invariant
-#[derive(Clone, Debug)]
+#[derive(Clone, Constructor, Debug)]
pub struct LoopSpec {
/// the functional invariant as a predicate on the refinement of local variables.
- pub func_predicate: IPropPredicate,
+ func_predicate: IPropPredicate,
+ inv_locals: Vec<String>,
+ preserved_locals: Vec<String>,
+ uninit_locals: Vec<String>,
}
impl Display for LoopSpec {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
- write!(f, "(wrap_inv ({}), wrap_inv (λ (L : llctx), True%I : iProp Σ))", self.func_predicate)?;
+ write!(
+ f,
+ "([{}], [{}], [{}], wrap_inv ({}), wrap_inv (λ (L : llctx), True%I : iProp Σ))",
+ self.inv_locals.join("; "),
+ self.preserved_locals.join("; "),
+ self.uninit_locals.join("; "),
+ self.func_predicate
+ )?;
Ok(())
}
diff --git a/rr_frontend/translation/src/base.rs b/rr_frontend/translation/src/base.rs
index ab77ee4d0ba8d1a860c1ef01f82792b58c587356..52a72b3f9a874e0dcde55ab18f2d3c2f1df8bbc7 100644
--- a/rr_frontend/translation/src/base.rs
+++ b/rr_frontend/translation/src/base.rs
@@ -79,6 +79,8 @@ pub enum TranslationError<'tcx> {
ProcedureRegistry(String),
#[display("Lookup in a dummy scope: {}", _0)]
DummyScope(String),
+ #[display("Could not parse loop spec: {}", _0)]
+ LoopSpec(String),
}
impl<'tcx> From<traits::Error<'tcx>> for TranslationError<'tcx> {
diff --git a/rr_frontend/translation/src/body/checked_op_analysis.rs b/rr_frontend/translation/src/body/checked_op_analysis.rs
index 093aa630b188e2993fe88334baf5801cbfbb77f6..f523e8a5932df3cd1e5f9d766d393ca952b6f71e 100644
--- a/rr_frontend/translation/src/body/checked_op_analysis.rs
+++ b/rr_frontend/translation/src/body/checked_op_analysis.rs
@@ -5,8 +5,8 @@
// file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
use std::collections::{HashMap, HashSet};
-use log::{info, trace};
+use log::{info, trace};
use rr_rustc_interface::middle::mir::tcx::PlaceTy;
use rr_rustc_interface::middle::mir::{
BasicBlock, BasicBlockData, Body, Local, Place, Rvalue, StatementKind, TerminatorKind,
diff --git a/rr_frontend/translation/src/body/mod.rs b/rr_frontend/translation/src/body/mod.rs
index 2a994f905309f2b50148dedc347ac0370db03cf7..327c26c1a27e9924c3fa4c746cf2f2c7f0f24d45 100644
--- a/rr_frontend/translation/src/body/mod.rs
+++ b/rr_frontend/translation/src/body/mod.rs
@@ -14,9 +14,9 @@ use rr_rustc_interface::hir::def_id::DefId;
use rr_rustc_interface::middle::mir::interpret::{ConstValue, ErrorHandled, Scalar};
use rr_rustc_interface::middle::mir::tcx::PlaceTy;
use rr_rustc_interface::middle::mir::{
- BasicBlock, BasicBlockData, BinOp, Body, BorrowKind, Constant, ConstantKind, Local, Location,
- Mutability, NonDivergingIntrinsic, Operand, Place, ProjectionElem, Rvalue, StatementKind, Terminator,
- TerminatorKind, UnOp, VarDebugInfoContents,
+ BasicBlock, BasicBlockData, BinOp, Body, BorrowKind, Constant, ConstantKind, Local, Location, Mutability,
+ NonDivergingIntrinsic, Operand, Place, ProjectionElem, Rvalue, StatementKind, Terminator, TerminatorKind,
+ UnOp, VarDebugInfoContents,
};
use rr_rustc_interface::middle::ty::fold::TypeFolder;
use rr_rustc_interface::middle::ty::{ConstKind, Ty, TyKind};
@@ -39,16 +39,6 @@ use crate::{base, consts, procedures, regions, search, traits, types};
pub mod signature;
mod translation;
-/// Classifies the kind of a local variable similar to `mir::LocalKind`,
-/// but distinguishes user-specified locals from compiler-generated temporaries.
-#[derive(PartialEq, Eq, Debug, Clone)]
-pub enum LocalKind {
- Arg,
- Local,
- CompilerTemp,
- Return,
-}
-
/// Get the syntypes of function arguments for a procedure call.
pub fn get_arg_syntypes_for_procedure_call<'tcx, 'def>(
tcx: ty::TyCtxt<'tcx>,
diff --git a/rr_frontend/translation/src/body/translation/loops.rs b/rr_frontend/translation/src/body/translation/loops.rs
index eafba15fde34de1c14c270b76ba5dfcbdd7c59a3..4ce86fa691e6c430168d2d0979de75b0946f7fbb 100644
--- a/rr_frontend/translation/src/body/translation/loops.rs
+++ b/rr_frontend/translation/src/body/translation/loops.rs
@@ -10,9 +10,9 @@ use rr_rustc_interface::hir::def_id::DefId;
use rr_rustc_interface::middle::mir::interpret::{ConstValue, ErrorHandled, Scalar};
use rr_rustc_interface::middle::mir::tcx::PlaceTy;
use rr_rustc_interface::middle::mir::{
- BasicBlock, BasicBlockData, BinOp, Body, BorrowKind, Constant, ConstantKind, Local, LocalKind, Location,
- Mutability, NonDivergingIntrinsic, Operand, Place, ProjectionElem, Rvalue, StatementKind, Terminator,
- TerminatorKind, UnOp, VarDebugInfoContents,
+ BasicBlock, BasicBlockData, BinOp, Body, BorrowKind, Constant, ConstantKind, Local, Location, Mutability,
+ NonDivergingIntrinsic, Operand, Place, ProjectionElem, Rvalue, StatementKind, Terminator, TerminatorKind,
+ UnOp, VarDebugInfoContents,
};
use rr_rustc_interface::middle::ty::fold::TypeFolder;
use rr_rustc_interface::middle::ty::{ConstKind, Ty, TyKind};
@@ -20,7 +20,10 @@ use rr_rustc_interface::middle::{mir, ty};
use rr_rustc_interface::{abi, ast, middle};
use super::TX;
+use crate::attrs;
use crate::base::*;
+use crate::environment::mir_analyses::initialization;
+use crate::spec_parsers::loop_attr_parser::{LoopAttrParser, VerboseLoopAttrParser};
impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
/// Parse the attributes on spec closure `did` as loop annotations and add it as an invariant
@@ -29,22 +32,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
&self,
loop_head: BasicBlock,
did: Option<DefId>,
- ) -> radium::LoopSpec {
- // for now: just make invariants True.
-
- // need to do:
- // - find out the locals in the right order, make parameter names for them. based on their type and
- // initialization status, get the refinement type.
- // - output/pretty-print this map when generating the typing proof of each function. [done]
- // + should not be a separate definition, but rather a "set (.. := ...)" with a marker type so
- // automation can find it.
-
- // representation of loop invariants:
- // - introduce parameters for them.
-
- let mut rfn_binders = Vec::new();
- let prop_body = radium::IProp::True;
-
+ ) -> Result<radium::LoopSpec, TranslationError<'tcx>> {
// determine invariant on initialization:
// - we need this both for the refinement invariant (though this could be removed if we make uninit
// generic over the refinement)
@@ -61,34 +49,34 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
// - this does not cause issues with posing a too strong loop invariant,
// - but this poses an issue for annotations
//
- //
- // get locals
- for (_, kind, name, ty) in &self.fn_locals {
- // get the refinement type
- let mut rfn_ty = ty.get_rfn_type();
- // wrap it in place_rfn, since we reason about places
- rfn_ty = coq::term::Type::PlaceRfn(Box::new(rfn_ty));
+ let init_result = initialization::compute_definitely_initialized(
+ self.proc.get_id(),
+ self.proc.get_mir(),
+ self.env.tcx(),
+ );
+ let init_places = init_result.get_before_block(loop_head);
- // determine their initialization status
- //let initialized = true; // TODO
- // determine the actual refinement type for the current initialization status.
+ // get locals
+ let mut locals_with_initialization: Vec<(String, radium::LocalKind, bool, radium::Type<'def>)> =
+ Vec::new();
+ for (local, kind, name, ty) in &self.fn_locals {
+ let place = mir::Place::from(*local);
+ let initialized = init_places.contains(place);
- let rfn_name = format!("r_{}", name);
- rfn_binders.push(coq::binder::Binder::new(Some(rfn_name), rfn_ty));
+ locals_with_initialization.push((name.to_owned(), kind.to_owned(), initialized, ty.to_owned()));
}
- // TODO what do we do about stuff connecting borrows?
+ let scope = self.ty_translator.scope.borrow();
+ let mut parser = VerboseLoopAttrParser::new(locals_with_initialization, &*scope);
+
if let Some(did) = did {
let attrs = self.env.get_attributes(did);
+ let attrs = attrs::filter_for_tool(attrs);
info!("attrs for loop {:?}: {:?}", loop_head, attrs);
+ parser.parse_loop_attrs(&attrs).map_err(TranslationError::LoopSpec)
} else {
- info!("no attrs for loop {:?}", loop_head);
- }
-
- let pred = radium::IPropPredicate::new(rfn_binders, prop_body);
- radium::LoopSpec {
- func_predicate: pred,
+ parser.parse_loop_attrs(&[]).map_err(TranslationError::LoopSpec)
}
}
diff --git a/rr_frontend/translation/src/body/translation/mod.rs b/rr_frontend/translation/src/body/translation/mod.rs
index b09cea37c8c9caf82f593115d04b73296f0679f8..b5db74a5c21c1fa650dc9b6d5a65fdcb8bbf8e12 100644
--- a/rr_frontend/translation/src/body/translation/mod.rs
+++ b/rr_frontend/translation/src/body/translation/mod.rs
@@ -14,14 +14,14 @@ mod terminator;
use std::collections::{HashMap, HashSet};
-use log::{trace, info};
+use log::{info, trace};
use rr_rustc_interface::hir::def_id::DefId;
use rr_rustc_interface::middle::mir::interpret::{ConstValue, ErrorHandled, Scalar};
use rr_rustc_interface::middle::mir::tcx::PlaceTy;
use rr_rustc_interface::middle::mir::{
- BasicBlock, BasicBlockData, BinOp, Body, BorrowKind, Constant, ConstantKind, Local, Location,
- Mutability, NonDivergingIntrinsic, Operand, Place, ProjectionElem, Rvalue, StatementKind, Terminator,
- TerminatorKind, UnOp, VarDebugInfoContents,
+ BasicBlock, BasicBlockData, BinOp, Body, BorrowKind, Constant, ConstantKind, Local, Location, Mutability,
+ NonDivergingIntrinsic, Operand, Place, ProjectionElem, Rvalue, StatementKind, Terminator, TerminatorKind,
+ UnOp, VarDebugInfoContents,
};
use rr_rustc_interface::middle::ty::fold::TypeFolder;
use rr_rustc_interface::middle::ty::{ConstKind, Ty, TyKind};
@@ -38,8 +38,6 @@ use crate::environment::{polonius_info, Environment};
use crate::regions::inclusion_tracker::InclusionTracker;
use crate::traits::registry;
use crate::{base, consts, procedures, regions, types};
-use crate::body::LocalKind;
-
/// Struct that keeps track of all information necessary to translate a MIR Body to a `radium::Function`.
/// `'a` is the lifetime of the translator and ends after translation has finished.
@@ -94,7 +92,7 @@ pub struct TX<'a, 'def, 'tcx> {
loop_specs: HashMap<BasicBlock, Option<DefId>>,
/// relevant locals: (local, name, type)
- fn_locals: Vec<(Local, LocalKind, String, radium::Type<'def>)>,
+ fn_locals: Vec<(Local, radium::LocalKind, String, radium::Type<'def>)>,
/// result temporaries of checked ops that we rewrite
/// we assume that this place is typed at (result_type, bool)
@@ -292,7 +290,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
// definition)
// - have a function that takes the def_id and then parses the attributes into a loop invariant
for (head, did) in &self.loop_specs {
- let spec = self.parse_attributes_on_loop_spec_closure(*head, *did);
+ let spec = self.parse_attributes_on_loop_spec_closure(*head, *did)?;
self.translated_fn.register_loop_invariant(head.as_usize(), spec);
}
@@ -328,24 +326,18 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
}
/// Classify the kind of a local.
- fn get_local_kind(mir_body: &Body<'tcx>, local: Local) -> LocalKind {
+ fn get_local_kind(mir_body: &Body<'tcx>, local: Local) -> radium::LocalKind {
let kind = mir_body.local_kind(local);
match kind {
- mir::LocalKind::Arg => {
- LocalKind::Arg
- },
- mir::LocalKind::Temp => {
- let used_names = HashSet::new();
+ mir::LocalKind::Arg => radium::LocalKind::Arg,
+ mir::LocalKind::Temp | mir::LocalKind::ReturnPointer => {
+ let used_names = HashSet::new();
if Self::find_name_for_local(mir_body, local, &used_names).is_some() {
- LocalKind::Local
- }
- else {
- LocalKind::CompilerTemp
+ radium::LocalKind::Local
+ } else {
+ radium::LocalKind::CompilerTemp
}
},
- mir::LocalKind::ReturnPointer => {
- LocalKind::Return
- },
}
}
@@ -513,11 +505,9 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
return Ok(None);
};
- let mode = self
- .procedure_registry
- .lookup_function_mode(*did);
+ let mode = self.procedure_registry.lookup_function_mode(*did);
let res = mode.and_then(|m| m.is_ignore().then_some(*did));
-
+
trace!("is_spec_closure_local: found closure {res:?} with mode {mode:?}");
Ok(res)
diff --git a/rr_frontend/translation/src/spec_parsers/loop_attr_parser.rs b/rr_frontend/translation/src/spec_parsers/loop_attr_parser.rs
index a5c3c0a4d8c7c8593481f510cc9f13905303aa9b..9f7a35ac73dcf357436d026daa5668025f4f7021 100644
--- a/rr_frontend/translation/src/spec_parsers/loop_attr_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/loop_attr_parser.rs
@@ -4,23 +4,19 @@
// If a copy of the BSD-3-clause license was not distributed with this
// file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
-use rr_rustc_interface::ast::ast::AttrItem;
-use rr_rustc_interface::hir::def_id::LocalDefId;
use attribute_parse::{parse, MToken};
use parse::{Parse, Peek};
-
use radium::{coq, specs};
+use rr_rustc_interface::ast::ast::AttrItem;
+use rr_rustc_interface::hir::def_id::LocalDefId;
+
use crate::spec_parsers::parse_utils::*;
-use crate::body::LocalKind;
/// Parse attributes on a const.
/// Permitted attributes:
/// TODO
pub trait LoopAttrParser {
- fn parse_loop_attrs<'a>(
- &'a mut self,
- attrs: &'a [&'a AttrItem],
- ) -> Result<radium::LoopSpec, String>;
+ fn parse_loop_attrs<'a>(&'a mut self, attrs: &'a [&'a AttrItem]) -> Result<radium::LoopSpec, String>;
}
/// Representation of the `IProps` that can appear in a requires or ensures clause.
@@ -106,7 +102,6 @@ impl From<MetaIProp> for specs::IProp {
}
}
-
/// Invariant variable refinement declaration
struct InvVar {
local: String,
@@ -129,29 +124,26 @@ impl<'def, T: ParamLookup<'def>> parse::Parse<T> for InvVar {
}
}
-
#[allow(clippy::module_name_repetitions)]
pub struct VerboseLoopAttrParser<'def, 'a, T> {
- locals: Vec<(String, LocalKind, radium::Type<'def>)>,
+ locals: Vec<(String, radium::LocalKind, bool, radium::Type<'def>)>,
scope: &'a T,
}
impl<'def, 'a, T: ParamLookup<'def>> VerboseLoopAttrParser<'def, 'a, T> {
- pub const fn new(locals: Vec<(String, LocalKind, radium::Type<'def>)>, scope: &'a T) -> Self {
- Self {
- locals,
- scope,
- }
+ pub const fn new(
+ locals: Vec<(String, radium::LocalKind, bool, radium::Type<'def>)>,
+ scope: &'a T,
+ ) -> Self {
+ Self { locals, scope }
}
}
impl<'def, 'a, T: ParamLookup<'def>> LoopAttrParser for VerboseLoopAttrParser<'def, 'a, T> {
- fn parse_loop_attrs<'b>(
- &'b mut self,
- attrs: &'b [&'b AttrItem],
- ) -> Result<radium::LoopSpec, String> {
+ fn parse_loop_attrs<'b>(&'b mut self, attrs: &'b [&'b AttrItem]) -> Result<radium::LoopSpec, String> {
let mut invariant: Vec<specs::IProp> = Vec::new();
let mut inv_vars: Vec<InvVar> = Vec::new();
+ let mut existentials: Vec<coq::binder::Binder> = Vec::new();
for &it in attrs {
let path_segs = &it.path.segments;
@@ -164,6 +156,12 @@ impl<'def, 'a, T: ParamLookup<'def>> LoopAttrParser for VerboseLoopAttrParser<'d
let buffer = parse::Buffer::new(&it.args.inner_tokens());
match seg.ident.name.as_str() {
+ "exists" => {
+ let params = RRParams::parse(&buffer, self.scope).map_err(str_err)?;
+ for param in params.params {
+ existentials.push(param.into());
+ }
+ },
"inv" => {
let parsed_iprop: MetaIProp = buffer.parse(self.scope).map_err(str_err)?;
invariant.push(parsed_iprop.into());
@@ -172,6 +170,9 @@ impl<'def, 'a, T: ParamLookup<'def>> LoopAttrParser for VerboseLoopAttrParser<'d
let parsed_inv_var: InvVar = buffer.parse(self.scope).map_err(str_err)?;
inv_vars.push(parsed_inv_var);
},
+ "ignore" => {
+ // ignore, this is the spec closure annotation
+ },
_ => {
return Err(format!("unknown attribute for loop specification: {:?}", args));
},
@@ -179,30 +180,62 @@ impl<'def, 'a, T: ParamLookup<'def>> LoopAttrParser for VerboseLoopAttrParser<'d
}
// now assemble the actual invariant
+ // we split the local variables into three sets:
+ // - named and definitely initialized variables, which we can use in the invariant
+ // - named and maybe uninitialized variables, which we can not use in the invariant. Their type is
+ // preserved across the loop.
+ // - compiler temporaries, which are required to be uninitialized. (NOTE: if we have mutable
+ // references around, this means that we need to extract observations and properly use their
+ // equalities)
+
+ // binders that the invariant is parametric in
let mut rfn_binders = Vec::new();
+ // proposition for unknown locals
+ let mut uninit_locals_prop: Vec<specs::IProp> = Vec::new();
+
+ // track locals
+ let mut inv_locals: Vec<String> = Vec::new();
+ let mut uninit_locals: Vec<String> = Vec::new();
+ let mut preserved_locals: Vec<String> = Vec::new();
+
// get locals
- for (name, kind, ty) in &self.locals {
+ for (name, kind, initialized, ty) in &self.locals {
// get the refinement type
let mut rfn_ty = ty.get_rfn_type();
+ let ty_st: specs::SynType = ty.into();
// wrap it in place_rfn, since we reason about places
rfn_ty = coq::term::Type::PlaceRfn(Box::new(rfn_ty));
- // determine their initialization status
- //let initialized = true; // TODO
-
- // TODO: if we use the argnames here too, then we cannot use the original value of the
- // arg anymore..
+ let local_name = kind.mk_local_name(name);
+
+ if *kind == radium::LocalKind::CompilerTemp {
+ let pred = format!("{local_name} â—â‚—[Ï€, Owned false] .@ (â— uninit {ty_st})");
+ uninit_locals_prop.push(specs::IProp::Atom(pred));
+
+ uninit_locals.push(local_name);
+ } else if *initialized {
+ inv_locals.push(local_name);
+
+ rfn_binders.push(coq::binder::Binder::new(Some(name.to_owned()), rfn_ty));
+ } else {
+ preserved_locals.push(local_name);
+ }
+ }
- let rfn_name = format!("r_{}", name);
- rfn_binders.push(coq::binder::Binder::new(Some(rfn_name), rfn_ty));
+ // add constraints on refinements
+ let mut var_invariants = Vec::new();
+ for inv_var in inv_vars {
+ var_invariants.push(specs::IProp::Pure(format!("{} = {}", inv_var.local, inv_var.rfn)));
}
- let prop_body = specs::IProp::Sep(invariant);
+ var_invariants.extend(invariant);
+ var_invariants.extend(uninit_locals_prop);
+
+ let prop_body = specs::IProp::Sep(var_invariants);
+ let prop_body = specs::IProp::Exists(existentials, Box::new(prop_body));
let pred = radium::IPropPredicate::new(rfn_binders, prop_body);
- Ok(radium::LoopSpec {
- func_predicate: pred,
- })
+ Ok(radium::LoopSpec::new(pred, inv_locals, preserved_locals, uninit_locals))
}
}
diff --git a/rr_frontend/translation/src/spec_parsers/mod.rs b/rr_frontend/translation/src/spec_parsers/mod.rs
index 38ccf61dc02933cc258a7489304108afb08c1e41..bb574fd73470d52f7475fcd3c6c2b7960919be13 100644
--- a/rr_frontend/translation/src/spec_parsers/mod.rs
+++ b/rr_frontend/translation/src/spec_parsers/mod.rs
@@ -1,13 +1,13 @@
pub mod const_attr_parser;
pub mod crate_attr_parser;
pub mod enum_spec_parser;
+pub mod loop_attr_parser;
pub mod module_attr_parser;
pub mod parse_utils;
pub mod struct_spec_parser;
pub mod trait_attr_parser;
pub mod trait_impl_attr_parser;
pub mod verbose_function_spec_parser;
-pub mod loop_attr_parser;
use attribute_parse::{parse, MToken};
use parse::Parse;
diff --git a/theories/rust_typing/automation.v b/theories/rust_typing/automation.v
index c9274cf75c87ba3fd59a11a0a757762f86b20784..f0e41e33eb4256f25f8d39d12e809ce609716059 100644
--- a/theories/rust_typing/automation.v
+++ b/theories/rust_typing/automation.v
@@ -183,8 +183,13 @@ Arguments PolySome {_}.
(* Wrapper to store predicates of arbitrary arity. *)
Definition wrap_inv {T} (x : T) := existT (P := id) _ x.
-(* Type of loop invariants: a predicate on the refinements, and a predicate on the lifetime contexts *)
-Definition bb_inv_t := (sigT (@id Type) * sigT (@id Type))%type.
+(* Type of loop invariants:
+ - list of variables the invariant is over
+ - list of variables whose type is preserved
+ - list of uninit variables
+ - a predicate on the refinements,
+ - and a predicate on the lifetime contexts *)
+Definition bb_inv_t := (list loc * list loc * list loc * sigT (@id Type) * sigT (@id Type))%type.
(* Type of the loop invariant map we keep in the context *)
Definition bb_inv_map_t := poly_list (var_name * bb_inv_t)%type.
Inductive bb_inv_map_marker : bb_inv_map_t → Type :=
@@ -247,11 +252,11 @@ Proof.
Defined.
(** Generates [count] successive fresh identifiers as Coq strings with prefix [prefix].
- Returns a Coq list [list string]. *)
+ Poses the result as a hypothesis [out]. *)
(* TODO: potentially take a list of suffix strings, so that we can we also get the variable names for the refinements, e.g. x, y? *)
Ltac get_idents_rec' prefix count acc out :=
match count with
- | 0%nat =>
+ | 0%nat =>
set (out := acc)
| (S ?n)%nat =>
(* need to prefix with some symbol because just a number is not a valid ident *)
@@ -303,18 +308,23 @@ Ltac build_local_sepconj local_locs spatial_env ex_names base base_app :=
end
end.
+Ltac get_Σ :=
+ let tgs := constr:(_ : typeGS _) in
+ match type of tgs with
+ | typeGS ?Σ => Σ
+ end.
+Ltac get_Ï€ :=
+ match goal with
+ | π : thread_id |- _ => π
+ end.
+
(** Composes the loop invariant from the invariant [inv : bb_inv_t] (a constr),
the runtime function [FN : runtime_function], the current Iris environment [env : env],
and the current contexts [current_E : elctx], [current_L : llctx],
and poses it with the identifier [Hinv]. *)
Ltac pose_loop_invariant Hinv FN inv envs current_E current_L :=
(* find Σ *)
- let Σ :=
- let tgs := constr:(_ : typeGS _) in
- match type of tgs with
- | typeGS ?Σ => Σ
- end
- in
+ let Σ := get_Σ in
(* get spatial env *)
let envs := eval hnf in envs in
let spatial_env :=
@@ -325,20 +335,25 @@ Ltac pose_loop_invariant Hinv FN inv envs current_E current_L :=
in
(* extract the invariants *)
+ let inv_locals :=
+ match inv with
+ | (?inv_locals, _, _, _, _) => constr:(inv_locals)
+ end in
+ let preserved_locals :=
+ match inv with
+ | (_, ?pres_locals, _, _, _) => constr:(pres_locals)
+ end in
let functional_inv := match inv with
- | (wrap_inv ?inv, _) => uconstr:(inv)
+ | (_, _, _, wrap_inv ?inv, _) => uconstr:(inv)
end
in
let llctx_inv := match inv with
- | (_, wrap_inv ?inv) => uconstr:(inv)
+ | (_, _, _, _, wrap_inv ?inv) => uconstr:(inv)
end
in
- (* find the locals in the context *)
- let FN := eval hnf in FN in
- let local_locs := gather_locals FN in
(* generate names for the existentially abstracted refinements *)
- let num_locs := eval cbv in (length local_locs) in
+ let num_locs := eval cbv in (length inv_locals) in
let names_ident := fresh "tmp" in
get_idents_rec ident:(r) constr:(num_locs) ident:(names_ident);
let names := eval cbv in names_ident in
@@ -359,7 +374,7 @@ Ltac pose_loop_invariant Hinv FN inv envs current_E current_L :=
let Ha := fresh "Hinv" in
pose (Ha := functional_inv);
- build_local_sepconj local_locs spatial_env names constr:(((True ∗ ⌜HELâŒ)%I: iProp Σ)) Ha
+ build_local_sepconj inv_locals spatial_env names constr:(((True ∗ ⌜HELâŒ)%I: iProp Σ)) Ha
));
(* get rid of all the lets we introduced *)
simpl in Hinv.
@@ -464,7 +479,7 @@ Ltac liRGoto goto_bb :=
pose_loop_invariant Hinv fn inv Δ E L;
(* finally initiate Löb *)
notypeclasses refine (tac_fast_apply (typed_goto_acc _ _ _ _ _ Hinv goto_bb _ _ _) _);
- [unfold_code_marker_and_compute_map_lookup| ]
+ [unfold_code_marker_and_compute_map_lookup| unfold Hinv; clear Hinv ]
)
end
| (* do a direct jump *)
@@ -817,7 +832,7 @@ Tactic Notation "prepare_parameters" "(" ident_list(i) ")" :=
(* IMPORTANT: We need to make sure to never call simpl while the code
(fn) is part of the goal, because simpl seems to take exponential time
-in the number of blocks!
+in the number of blocks!
TODO: does this still hold? we've since started doing this...
*)
@@ -841,13 +856,13 @@ Tactic Notation "start_function" constr(fnname) ident(Ï) "(" simple_intropatter
let lsa := fresh "lsa" in let lsv := fresh "lsv" in
iIntros (lsa lsv);
simpl in lsa;
- revert params;
+ revert params;
repeat liForall;
prepare_initial_coq_context;
iExists _; iSplitR;
[iPureIntro; solve [preprocess_elctx] | ];
inv_vec lsv; inv_vec lsa;
- simpl;
+ simpl;
unfold typarams_wf, typaram_wf;
init_cache
end
diff --git a/theories/rust_typing/program_rules.v b/theories/rust_typing/program_rules.v
index 924dcacdc15d07fff6692ceae511aac1287a0e8e..941aeffa6335eeaf4b0a48c3ca4d99f890b34567 100644
--- a/theories/rust_typing/program_rules.v
+++ b/theories/rust_typing/program_rules.v
@@ -3212,13 +3212,22 @@ Section typing.
(* TODO maybe also stratify? *)
prove_with_subtype E L false ProveDirect (P E L) (λ L' _ R2, R2 -∗
⌜L' = L⌠∗ (* TODO maybe relax if we have a separate condition on lifetime contexts *)
- â–¡ (∀ E L, (â–¡ typed_block Ï€ P b fn R Ï) -∗ P E L -∗ typed_stmt Ï€ E L s fn R Ï))
+ (* gather up the remaining ownership *)
+ accu (λ Q,
+ (∀ E L, (â–¡ typed_block Ï€ (λ E L, P E L ∗ Q) b fn R Ï) -∗
+ P E L ∗ Q -∗
+ typed_stmt Ï€ E L s fn R Ï)))
⊢ typed_stmt Ï€ E L (Goto b) fn R Ï.
Proof.
iIntros (Hlook) "Hsubt". iIntros (?) "#CTX #HE HL Hna Hcont".
iMod ("Hsubt" with "[] [] CTX HE HL") as "(%L' & % & %R2 & >(Hinv &HR2) & HL & HT)"; [done.. | ].
iDestruct ("HT" with "HR2") as "(-> & Hrec)".
- iApply (typed_block_rec with "Hrec CTX HE HL Hna Hinv"); done.
+ rewrite /accu.
+ iDestruct "Hrec" as "(%Q & HQ & #Hrec)".
+ iApply (typed_block_rec with "Hrec CTX HE HL Hna [Hinv HQ]").
+ - done.
+ - iFrame.
+ - done.
Qed.
Lemma type_assert E L e s fn Ï€ R Ï :