[eacsl] Handle variant loop annotations

src/plugins/e-acsl/src/code_generator/injector.ml

@@ -224,8 +224,8 @@ let add_new_block_in_stmt env kf stmt =
         end else
           env
       in
-      (* handle loop invariants *)
-      let new_stmt, env = Loops.preserve_invariant env kf stmt in
+      (* handle loop annotations *)
+      let new_stmt, env = Loops.handle_annotations env kf stmt in
       new_stmt, env
     else
       stmt, env

src/plugins/e-acsl/src/code_generator/loops.ml

@@ -40,17 +40,129 @@ let term_to_exp_ref
   = Extlib.mk_fun "term_to_exp_ref"
 
 (**************************************************************************)
-(************************* Loop invariants ********************************)
+(************************* Loop annotations *******************************)
 (**************************************************************************)
 
-let preserve_invariant env kf stmt = match stmt.skind with
+let handle_annotations env kf stmt =
+  match stmt.skind with
   | Loop(_, ({ bstmts = stmts } as blk), loc, cont, break) ->
-    let rec handle_invariants (stmts, env as acc) = function
-      | [] ->
-        (* empty loop body: no need to verify the invariant twice *)
-        acc
+    (* Loop variant, save the current value of the variant *)
+    let stmts, env, variant =
+      match Env.top_loop_variant env with
+      | Some (t, measure_opt) ->
+        let env = Env.set_annotation_kind env Smart_stmt.Variant in
+        let env = Env.push env in
+        Typing.type_term ~use_gmp_opt:true t;
+        let ty = Typing.get_typ t in
+        let e, env = !term_to_exp_ref kf env t in
+        let vi_old, e_old, env =
+          Env.new_var
+            ~loc
+            ~scope:Varname.Function
+            ~name:"old_variant"
+            env
+            kf
+            (Some t)
+            ty
+            (fun _ _ -> [])
+        in
+        let stmt =
+          Smart_stmt.assigns ~loc ~result:(Cil.var vi_old) e
+        in
+        let blk, env =
+          Env.pop_and_get env stmt ~global_clear:false Env.Middle
+        in
+        Smart_stmt.block_stmt blk :: stmts, env, Some (t, e_old, measure_opt)
+      | None -> stmts, env, None
+    in
+    (* Auxiliary function to generate variant and invariant checks *)
+    let rec aux (stmts, env) = function
+      | [] -> begin
+          (* No statements remaining in the loop: variant check *)
+          let env = Env.set_annotation_kind env Smart_stmt.Variant in
+          match variant with
+          | Some (t, e_old, Some measure) ->
+            let env = Env.push env in
+            let t_old = { t with term_node = t.term_node } in
+            let tapp =
+              { term_node = Tapp(measure, [], [t_old; t]);
+                term_loc = loc;
+                term_name = [];
+                term_type = Linteger;}
+            in
+            Typing.type_term ~use_gmp_opt:true tapp;
+            let e, env = !term_to_exp_ref kf env t in
+            let e_tapp, env =
+              Logic_functions.tapp_to_exp kf env ~eargs:[e_old; e] tapp
+            in
+            let msg =
+              Format.asprintf
+                "%s(old %a, %a)"
+                measure.l_var_info.lv_name
+                Printer.pp_term t_old
+                Printer.pp_term t
+            in
+            let stmt =
+              Smart_stmt.runtime_check_with_msg
+                ~loc
+                msg
+                ~pred_kind:Assert
+                Smart_stmt.Variant
+                kf
+                e_tapp
+            in
+            let blk, env =
+              Env.pop_and_get env stmt ~global_clear:false Env.Middle
+            in
+            let stmts = Smart_stmt.block_stmt blk :: stmts in
+            stmts, env
+          | Some (t, e_old, None) ->
+            let env = Env.push env in
+            Typing.type_term ~use_gmp_opt:true t;
+            let e, env = !term_to_exp_ref kf env t in
+            let msg1 =
+              Format.asprintf
+                "(old %a) %a 0"
+                Printer.pp_term t
+                Printer.pp_relation Rge
+            in
+            let msg2 =
+              Format.asprintf
+                "(old %a) > %a"
+                Printer.pp_term t
+                Printer.pp_term t
+            in
+            let stmt =
+              Smart_stmt.block_from_stmts [
+                Smart_stmt.runtime_check_with_msg
+                  ~loc
+                  msg1
+                  ~pred_kind:Assert
+                  Smart_stmt.Variant
+                  kf
+                  (Cil.mkBinOp ~loc Ge e_old (Cil.zero ~loc));
+                Smart_stmt.runtime_check_with_msg
+                  ~loc
+                  msg2
+                  ~pred_kind:Assert
+                  Smart_stmt.Variant
+                  kf
+                  (Cil.mkBinOp ~loc Gt e_old e)
+              ]
+            in
+            let blk, env =
+              Env.pop_and_get env stmt ~global_clear:false Env.Middle
+            in
+            let stmts = Smart_stmt.block_stmt blk :: stmts in
+            stmts, env
+          | None ->
+            stmts, env
+        end
       | [ last ] ->
-        let invariants, env = Env.pop_loop env in
+        (* Last statement of the loop: invariant check *)
+        (* Optimisation to only verify invariant on a non-empty body loop. *)
+        let invariants = Env.top_loop_invariants env in
+        let env = Env.set_annotation_kind env Smart_stmt.Invariant in
         let env = Env.push env in
         let env =
           let translate_named_predicate = !translate_predicate_ref in
@@ -59,15 +171,15 @@ let preserve_invariant env kf stmt = match stmt.skind with
         let blk, env =
           Env.pop_and_get env last ~global_clear:false Env.Before
         in
-        Smart_stmt.block last blk :: stmts, env
-      | s :: tl ->
-        handle_invariants (s :: stmts, env) tl
+        aux (Smart_stmt.block last blk :: stmts, env) []
+      | hd :: tl -> aux (hd :: stmts, env) tl
     in
-    let env = Env.set_annotation_kind env Smart_stmt.Invariant in
-    let stmts, env = handle_invariants ([], env) stmts in
+    let stmts, env = aux ([], env) stmts in
+    (* The loop annotations have been handled, the loop environment can be
+       popped *)
+    let env = Env.pop_loop env in
     let new_blk = { blk with bstmts = List.rev stmts } in
-    { stmt with skind = Loop([], new_blk, loc, cont, break) },
-    env
+    { stmt with skind = Loop([], new_blk, loc, cont, break) }, env
   | _ ->
     stmt, env
 

src/plugins/e-acsl/src/code_generator/loops.mli

@@ -25,13 +25,14 @@
 open Cil_types
 
 (**************************************************************************)
-(************************* Loop invariants ********************************)
+(************************* Loop annotations *******************************)
 (**************************************************************************)
 
-val preserve_invariant:
+val handle_annotations:
   Env.t -> Kernel_function.t -> stmt -> stmt * Env.t
-(** Modify the given stmt loop to insert the code which preserves its loop
-    invariants. Also return the modified environment. *)
+(** Modify the given stmt loop to insert the code which verifies the loop
+    annotations, ie. preserves its loop invariants and checks the loop variant.
+    Also return the modified environment. *)
 
 (**************************************************************************)
 (**************************** Nested loops ********************************)

src/plugins/e-acsl/src/code_generator/translate_annots.ml

@@ -111,9 +111,9 @@ let pre_code_annotation kf stmt env annot =
         else env
       else
         env
-    | AVariant _ ->
+    | AVariant (t, measure) ->
       if must_translate (Property.ip_of_code_annot_single kf stmt annot)
-      then Env.not_yet env "variant"
+      then Env.set_loop_variant env ?measure t
       else env
     | AAssigns _ ->
       (* TODO: it is not a precondition --> should not be handled here,