Loop Invariant Encoding

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

@@ -28,6 +28,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,