added loop_invariant (which is true at start and end of loop)

renamed LoopSpecification enum for bodyinvariant! from Invariant to BodyInvariant

Author: paaassscccaaalll

prusti-contracts/prusti-contracts-proc-macros/src/lib.rs

@@ -58,6 +58,12 @@ pub fn body_invariant(_tokens: TokenStream) -> TokenStream {
     TokenStream::new()
 }
 
+#[cfg(not(feature = "prusti"))]
+#[proc_macro]
+pub fn loop_invariant(_tokens: TokenStream) -> TokenStream {
+    TokenStream::new()
+}
+
 #[cfg(not(feature = "prusti"))]
 #[proc_macro]
 pub fn prusti_assert(_tokens: TokenStream) -> TokenStream {
@@ -189,6 +195,12 @@ pub fn body_invariant(tokens: TokenStream) -> TokenStream {
     prusti_specs::body_invariant(tokens.into()).into()
 }
 
+#[cfg(feature = "prusti")]
+#[proc_macro]
+pub fn loop_invariant(tokens: TokenStream) -> TokenStream {
+    prusti_specs::loop_invariant_expr(tokens.into()).into()
+}
+
 #[cfg(feature = "prusti")]
 #[proc_macro]
 pub fn prusti_assert(tokens: TokenStream) -> TokenStream {

prusti-contracts/prusti-contracts/src/lib.rs

@@ -27,6 +27,9 @@ pub use prusti_contracts_proc_macros::invariant;
 /// A macro for writing a loop body invariant.
 pub use prusti_contracts_proc_macros::body_invariant;
 
+/// A macro to annotate loop invariants (Holds at start and end of the loop)
+pub use prusti_contracts_proc_macros::loop_invariant;
+
 /// A macro for writing assertions using the full prusti specifications
 pub use prusti_contracts_proc_macros::prusti_assert;
 

prusti-contracts/prusti-specs/src/lib.rs

@@ -420,6 +420,10 @@ pub fn body_variant(tokens: TokenStream) -> TokenStream {
 }
 
 pub fn body_invariant(tokens: TokenStream) -> TokenStream {
+    generate_expression_closure(&AstRewriter::process_body_invariant, tokens)
+}
+
+pub fn loop_invariant_expr(tokens: TokenStream) -> TokenStream {
     generate_expression_closure(&AstRewriter::process_loop_invariant, tokens)
 }
 

prusti-contracts/prusti-specs/src/rewriter.rs

@@ -240,14 +240,23 @@ impl AstRewriter {
     }
 
     /// Parse a loop invariant into a Rust expression
-    pub fn process_loop_invariant(
+    pub fn process_body_invariant(
         &mut self,
         spec_id: SpecificationId,
         tokens: TokenStream,
     ) -> syn::Result<TokenStream> {
         self.process_prusti_expression(quote! {loop_body_invariant_spec}, spec_id, tokens)
     }
 
+    /// Parse a proper loop invariant into a Rust expression
+    pub fn process_loop_invariant(
+        &mut self,
+        spec_id: SpecificationId,
+        tokens: TokenStream,
+    ) -> syn::Result<TokenStream> {
+        self.process_prusti_expression(quote! {loop_invariant_spec}, spec_id, tokens)
+    }
+
     /// Parse a prusti assertion into a Rust expression
     pub fn process_prusti_assertion(
         &mut self,

prusti-encoder/src/encoders/impure/loop.rs

@@ -312,7 +312,7 @@ impl<'vir, 'enc, E: TaskEncoder> ImpureEncVisitor<'vir, 'enc, E> {
                     {
                         let is_loop_invariant = spec::with_type_spec(|def_spec| {
                             if let Some(loop_spec) = def_spec.get_loop_spec(cl_def_id) {
-                                assert!(!matches!(loop_spec, prusti_interface::specs::typed::LoopSpecification::Invariant(_)), "body_invariant! currently not supported");
+                                assert!(!matches!(loop_spec, prusti_interface::specs::typed::LoopSpecification::BodyInvariant(_)), "body_invariant! currently not supported");
                                 matches!(loop_spec, prusti_interface::specs::typed::LoopSpecification::LoopInvariant(_))
                             } else {
                                 false

prusti-interface/src/specs/mod.rs

@@ -81,6 +81,7 @@ pub struct SpecCollector<'a, 'tcx> {
     /// Map from functions/loops/types to their specifications.
     procedure_specs: FxHashMap<LocalDefId, ProcedureSpecRefs>,
     loop_specs: Vec<LocalDefId>,
+    loop_invariants: Vec<LocalDefId>,
     loop_variants: Vec<LocalDefId>,
     type_specs: FxHashMap<LocalDefId, TypeSpecRefs>,
     prusti_assertions: Vec<LocalDefId>,
@@ -98,6 +99,7 @@ impl<'a, 'tcx> SpecCollector<'a, 'tcx> {
             spec_functions: FxHashMap::default(),
             procedure_specs: FxHashMap::default(),
             loop_specs: vec![],
+            loop_invariants: vec![],
             loop_variants: vec![],
             type_specs: FxHashMap::default(),
             prusti_assertions: vec![],
@@ -220,7 +222,13 @@ impl<'a, 'tcx> SpecCollector<'a, 'tcx> {
         for local_id in self.loop_specs.iter() {
             def_spec.loop_specs.insert(
                 local_id.to_def_id(),
-                typed::LoopSpecification::Invariant(*local_id),
+                typed::LoopSpecification::BodyInvariant(*local_id),
+            );
+        }
+        for local_id in self.loop_invariants.iter() {
+            def_spec.loop_specs.insert(
+                local_id.to_def_id(),
+                typed::LoopSpecification::LoopInvariant(*local_id),
             );
         }
         for local_id in self.loop_variants.iter() {
@@ -487,6 +495,9 @@ impl<'a, 'tcx> intravisit::Visitor<'tcx> for SpecCollector<'a, 'tcx> {
             if has_prusti_attr(attrs, "loop_body_invariant_spec") {
                 self.loop_specs.push(local_id);
             }
+            if has_prusti_attr(attrs, "loop_invariant_spec") {
+                self.loop_invariants.push(local_id);
+            }
             if has_prusti_attr(attrs, "loop_body_variant_spec") {
                 self.loop_variants.push(local_id);
             }

prusti-interface/src/specs/typed.rs

@@ -264,7 +264,8 @@ impl ProcedureSpecificationKind {
 
 #[derive(Debug, Clone)]
 pub enum LoopSpecification {
-    Invariant(LocalDefId),
+    BodyInvariant(LocalDefId),        // body_invariant!() - true at call site in loop body
+    LoopInvariant(LocalDefId),    // invariant!() - true at loop head/start and end of iteration
     Variant(LocalDefId),
 }