From fcbebbd16ff304a3e59be6e259bed7286494ad1d Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 10 Feb 2021 11:45:01 +0100
Subject: [PATCH] [wp] Simplifies loop computation

---
 src/plugins/wp/cfgCalculus.ml  | 26 ++++++++++----------------
 src/plugins/wp/normAtLabels.ml |  3 +++
 2 files changed, 13 insertions(+), 16 deletions(-)

diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 1e2f4980d03..8c35871f631 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -232,22 +232,16 @@ struct
 
   (* Compute loops *)
   and loop env a s (lc : CfgAnnot.loop_contract) : W.t_prop =
-    let loop_current = Clabels.loop_current s in
-    let established =
-      W.label env.we None loop_current @@
-      List.fold_right (prove_property env) lc.loop_established W.empty in
-    let presersed =
-      List.fold_right (use_assigns env) lc.loop_assigns @@
-      W.label env.we None loop_current @@
-      List.fold_right (use_property env) lc.loop_invariants @@
-      List.fold_right (prove_property env) lc.loop_smoke @@
-      let q =
-        List.fold_right (prove_property env) lc.loop_preserved @@
-        List.fold_right (prove_assigns env) lc.loop_assigns @@
-        W.empty in
-      ( Vhash.replace env.wp a (Some q) ; successors env a )
-    in
-    W.merge env.we established presersed
+    List.fold_right (prove_property env) lc.loop_established @@
+    List.fold_right (use_assigns env) lc.loop_assigns @@
+    W.label env.we None (Clabels.loop_current s) @@
+    List.fold_right (use_property env) lc.loop_invariants @@
+    List.fold_right (prove_property env) lc.loop_smoke @@
+    let q =
+      List.fold_right (prove_property env) lc.loop_preserved @@
+      List.fold_right (prove_assigns env) lc.loop_assigns @@
+      W.empty in
+    ( Vhash.replace env.wp a (Some q) ; successors env a )
 
   (* Merge transitions *)
   and successors env (a : vertex) = transitions env (env.succ a)
diff --git a/src/plugins/wp/normAtLabels.ml b/src/plugins/wp/normAtLabels.ml
index fb30f63eadd..7a52640077e 100644
--- a/src/plugins/wp/normAtLabels.ml
+++ b/src/plugins/wp/normAtLabels.ml
@@ -121,6 +121,8 @@ let labels_fct ?kf ?at l =
   | BuiltinLabel Pre -> Clabels.pre
   | StmtLabel at -> Clabels.stmt !at
   | BuiltinLabel LoopEntry -> Clabels.loop_entry (enclosing_loop ?kf ?at l)
+  (* Labels fct is not used to label invariant establishment/preservation,
+     thus, contrary to what is done in [labels_loop], Current is not Here. *)
   | BuiltinLabel LoopCurrent -> Clabels.loop_current (enclosing_loop ?kf ?at l)
   | _ -> raise (LabelError l)
 
@@ -189,6 +191,7 @@ let labels_assert_after ~kf s l_post = function
   | l -> labels_fct ~kf ~at:s l
 
 let labels_loop s = function
+  (* In invariant preservation/establishment, LoopCurrent is Here. *)
   | BuiltinLabel (Here | LoopCurrent) -> Clabels.here
   | BuiltinLabel LoopEntry -> Clabels.loop_entry s
   | FormalLabel wplabel -> Clabels.formal wplabel
-- 
GitLab