fixup! [eacsl] Create an analysis to compute translation location of labeled pred and terms

src/plugins/e-acsl/Makefile.in

@@ -61,9 +61,9 @@ ANALYSES_CMI:= \
 ANALYSES_CMI:=$(addprefix src/analyses/, $(ANALYSES_CMI))
 
 SRC_ANALYSES:= \
+	lscope \
 	analyses_datatype \
 	rte \
-	lscope \
 	e_acsl_visitor \
 	logic_normalizer \
 	bound_variables \

src/plugins/e-acsl/src/analyses/analyses_datatype.ml

@@ -22,6 +22,7 @@
 
 (** Datatypes for analyses types *)
 
+open Cil_types
 open Cil_datatype
 open Analyses_types
 
@@ -83,3 +84,165 @@ module PredOrTerm =
 
       let varname _ = "pred_or_term"
     end)
+
+(** Extended logic label module to associate a statement to a label when
+    necessary. For instance, the label `Old` is associated with its contract
+    statement to be able to distinguish two `Old` annotations in the same
+    function. On the contrary the `Pre` label does not have an associated
+    statement because this label designate the same location for all contracts
+    in the same function. *)
+module ExtLogicLabel: sig
+  include Datatype.S_with_collections with type t = logic_label * stmt option
+
+  val from: kinstr -> logic_label -> logic_label * stmt option
+  (** @return an extended logic label from a [kinstr] and a [logic_label]. *)
+end = struct
+  include Datatype.Pair_with_collections
+      (Logic_label)
+      (Datatype.Option_with_collections
+         (Stmt)
+         (struct
+           let module_name = "E_ACSL.Labels.ExtLogicLabel.StmtOption"
+         end))
+      (struct let module_name = "E_ACSL.Labels.ExtLogicLabel" end)
+
+  (* Override [pretty] to print a more compact representation of [ExtLogicLabel]
+     for debugging purposes. *)
+  let pretty fmt (label, from_stmt_opt) =
+    match from_stmt_opt with
+    | Some from_stmt ->
+      Format.fprintf fmt "%a from stmt %d at %a"
+        Logic_label.pretty label
+        from_stmt.sid
+        Printer.pp_location (Stmt.loc from_stmt)
+    | None ->
+      Format.fprintf fmt "%a"
+        Logic_label.pretty label
+
+  let from kinstr label =
+    let from_stmt_opt =
+      match kinstr, label with
+      | Kglobal, _
+      | Kstmt _, (BuiltinLabel (Pre | Here | Init)
+                 | FormalLabel _ | StmtLabel _) ->
+        None
+      | Kstmt _, BuiltinLabel (LoopCurrent | LoopEntry) ->
+        (* [None] for now because these labels are unsupported, but the
+           statement before the loop and the first statement of the loop should
+           probably be used once they are supported. *)
+        Error.print_not_yet
+          (Format.asprintf "label %a" Printer.pp_logic_label label);
+        None
+      | Kstmt s, BuiltinLabel (Old | Post) -> Some s
+    in
+    label, from_stmt_opt
+end
+
+(** Basic printer for a [kinstr]. Contrary to [Cil_datatype.Kinstr.pretty], the
+    stmt of [Kstmt] is not printed. *)
+let basic_pp_kinstr fmt kinstr =
+  Format.fprintf fmt "%s"
+    (match kinstr with
+     | Kglobal -> "Kglobal"
+     | Kstmt _ -> "Kstmt")
+
+(** Basic comparison for two [kinstr], i.e. two [Kstmt] are always equal
+    regardless of the statement value (contrary to [Cil_datatype.Kinstr.compare]
+    where two [Kstmt] are compared with their included statement's [sid]). *)
+let basic_kinstr_compare kinstr1 kinstr2 =
+  match kinstr1, kinstr2 with
+  | Kglobal, Kglobal | Kstmt _, Kstmt _ -> 0
+  | Kglobal, _ -> 1
+  | _, Kglobal -> -1
+
+(** Basic hash function for a [kinstr], i.e. contrary to
+    [Cil_datatype.Kinstr.hash] the statement of the [Kstmt] is not considered
+    for the hash. *)
+let basic_kinstr_hash kinstr =
+  match kinstr with
+  | Kglobal -> 1 lsl 29
+  | Kstmt _ -> 1 lsl 31
+
+module AtData = struct
+  let create ?error kf kinstr lscope pot label =
+    { kf; kinstr; lscope; pot; label; error }
+
+  include Datatype.Make_with_collections
+      (struct
+        type t = at_data
+        let name = "E_ACSL.AtData"
+
+        let reprs =
+          List.fold_left
+            (fun acc kf ->
+               List.fold_left
+                 (fun acc kinstr ->
+                    List.fold_left
+                      (fun acc pot ->
+                         List.fold_left
+                           (fun acc label ->
+                              create kf kinstr Lscope.empty pot label :: acc)
+                           acc
+                           Logic_label.reprs)
+                      acc
+                      PredOrTerm.reprs)
+                 acc
+                 Kinstr.reprs)
+            []
+            Kf.reprs
+
+        include Datatype.Undefined
+
+        let compare
+            { kf = kf1;
+              kinstr = kinstr1;
+              lscope = lscope1;
+              pot = pot1;
+              label = label1 }
+            { kf = kf2;
+              kinstr = kinstr2;
+              lscope = lscope2;
+              pot = pot2;
+              label = label2 }
+          =
+          let cmp = Kf.compare kf1 kf2 in
+          let cmp =
+            if cmp = 0 then
+              basic_kinstr_compare kinstr1 kinstr2
+            else cmp
+          in
+          let cmp =
+            if cmp = 0 then Lscope.D.compare lscope1 lscope2
+            else cmp
+          in
+          let cmp =
+            if cmp = 0 then PredOrTerm.compare pot1 pot2
+            else cmp
+          in
+          if cmp = 0 then
+            let extlabel1 = ExtLogicLabel.from kinstr1 label1 in
+            let extlabel2 = ExtLogicLabel.from kinstr2 label2 in
+            ExtLogicLabel.compare extlabel1 extlabel2
+          else cmp
+
+        let equal = Datatype.from_compare
+
+        let hash { kf; kinstr; lscope; pot; label } =
+          let extlabel = ExtLogicLabel.from kinstr label in
+          Hashtbl.hash
+            (Kf.hash kf,
+             basic_kinstr_hash kinstr,
+             Lscope.D.hash lscope,
+             PredOrTerm.hash pot,
+             ExtLogicLabel.hash extlabel)
+
+        let pretty fmt { kf; kinstr; lscope; pot; label } =
+          let extlabel = ExtLogicLabel.from kinstr label in
+          Format.fprintf fmt "@[(%a, %a, %a, %a, %a)@]"
+            Kf.pretty kf
+            basic_pp_kinstr kinstr
+            Lscope.D.pretty lscope
+            PredOrTerm.pretty pot
+            ExtLogicLabel.pretty extlabel
+      end)
+end

src/plugins/e-acsl/src/analyses/analyses_datatype.mli

@@ -22,8 +22,24 @@
 
 (** Datatypes for analyses types *)
 
+open Cil_types
 open Analyses_types
 
 module Annotation_kind: Datatype.S with type t = annotation_kind
 
 module PredOrTerm: Datatype.S_with_collections with type t = pred_or_term
+
+module AtData: sig
+  include Datatype.S_with_collections with type t = at_data
+
+  val create:
+    ?error:exn ->
+    kernel_function ->
+    kinstr ->
+    lscope ->
+    pred_or_term ->
+    logic_label ->
+    at_data
+    (** [create ?error kf kinstr lscope pot label] creates an [at_data] from the
+        given arguments. *)
+end

src/plugins/e-acsl/src/analyses/analyses_types.mli

@@ -36,7 +36,29 @@ type pred_or_term =
   | PoT_pred of predicate
   | PoT_term of term
 
-type at_data = kernel_function * kinstr * lscope * pred_or_term * logic_label
+(** Type uniquely representing a [predicate] or [term] with an associated
+    [label], and all the information necessary for its translation. *)
+type at_data = {
+  (** [kernel_function] englobing the [pred_or_term]. *)
+  kf: kernel_function;
+
+  (** [kinstr] where the [pred_or_term] is used. *)
+  kinstr: kinstr;
+
+  (** Current state of the [lscope] for the [pred_or_term]. *)
+  lscope: lscope;
+
+  (** [pred_or_term] to translate. *)
+  pot: pred_or_term;
+
+  (** Label of the [pred_or_term]. *)
+  label: logic_label;
+
+  (** Error raised during the pre-analysis.
+      This field does not contribute to the equality and comparison between two
+      [at_data]. *)
+  error: exn option
+}
 
 type annotation_kind =
   | Assertion

src/plugins/e-acsl/src/analyses/labels.mli

@@ -20,51 +20,25 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** Labeled term and predicates pre-analysis *)
+(** Labeled term and predicates pre-analysis.
+
+    This pre-analysis records, for each labeled term or predicate, the place
+    where the translation must happen.
+
+    The list of labeled term or predicates to be translated for a given
+    statement is provided by [Labels.at_for_stmt]. *)
 
 open Cil_types
-open Analyses_types
+open Analyses_datatype
 
 val get_first_inner_stmt: stmt -> stmt
 (** If the given statement has a label, return the first statement of the block.
     Otherwise return the given statement. *)
 
-(** Manage labeled terms and predicates translation *)
-module Translation : sig
-  (** Represents a labeled translation *)
-  type t =
-    | Done of exp
-    (** The translation is done and the result is the expression [e] *)
-    | Queued
-    (** The translation needs to be done in a statement preceding the statement
-        where the labeled term or predicate is used. *)
-    | Inplace
-    (** The translation can be done when translating the statement where the
-        labeled term or predicate is used. *)
-
-  val at_for_stmt: stmt -> at_data list Error.result
-  (** @return the list of labeled predicates and terms to be translated on the
-      given statement. *)
-
-  val set: ?force:bool -> at_data -> t Error.result -> unit
-  (** Sets the translation for the given labeled term or predicate.
-
-      If a translation already exists, then the behavior depend on the existing
-      translation and the new translation:
-      - If the new translation is an error, keep the old translation except if
-        [force] is true;
-      - If the existing translation is an error and the new translation is a result,
-        always keep the new translation;
-      - If both translation are results:
-        -- if the old is Queued and the new one is Queued or Done, then keep the
-           new one;
-        -- if one is Queued and the other is Inplace, then store Queued;
-        -- if both are Inplace then keep Inplace
-        -- other combinations are errors. *)
-
-  val get: at_data -> t Error.result
-  (** @return the translation for the given labeled term or predicate. *)
-end
+val at_for_stmt: stmt -> AtData.Set.t Error.result
+(** @return the set of labeled predicates and terms to be translated on the
+    given statement.
+    @raise Not_memoized if the labels pre-analysis was not run. *)
 
 val preprocess: file -> unit
 (** Analyse sources to find the statements where a labeled predicate or term
@@ -73,9 +47,6 @@ val preprocess: file -> unit
 val reset: unit -> unit
 (** Reset the results of the pre-anlaysis. *)
 
-val pp_at_data: Format.formatter -> at_data -> unit
-(** Printer for [at_data]. *)
-
 val _debug: unit -> unit
 (** Print internal state of labels translation. *)
 
@@ -83,10 +54,6 @@ val _debug: unit -> unit
 (********************** Forward references ********************************)
 (**************************************************************************)
 
-val must_translate_ppt_ref: (Property.t -> bool) ref
-
-val must_translate_ppt_opt_ref: (Property.t option -> bool) ref
-
 val has_empty_quantif_ref: ((term * logic_var * term) list -> bool) ref
 
 (*

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

@@ -75,9 +75,7 @@ let must_translate_opt = function
 
 let () =
   E_acsl_visitor.must_translate_ppt_ref := must_translate;
-  E_acsl_visitor.must_translate_ppt_opt_ref := must_translate_opt;
-  Labels.must_translate_ppt_ref := must_translate;
-  Labels.must_translate_ppt_opt_ref := must_translate_opt
+  E_acsl_visitor.must_translate_ppt_opt_ref := must_translate_opt
 
 let gmp_to_sizet ~adata ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
   let lenv = Env.Local_vars.get env in