factorize definitions related to CE labels

src/core/ident.ml

@@ -260,13 +260,20 @@ let sanitizer head rest n = sanitizer' head rest rest n
 (** {2 functions for working with counterexample model labels} *)
 
 let model_label = create_label "model"
+let model_projected_label = create_label "model_projected"
+let model_vc_label = create_label "model_vc"
+let model_vc_post_label = create_label "model_vc_post"
 
-let has_model_label id = Slab.mem model_label id.id_label
+let create_model_trace_label s = create_label ("model_trace:" ^ s)
 
-let model_proj_label = create_label "model_projected"
+let is_counterexample_label l =
+  l = model_label || l = model_projected_label
+
+let has_a_model_label id =
+  Slab.exists is_counterexample_label id.id_label
 
 let remove_model_labels ~labels =
-  Slab.filter (fun l -> (l <> model_label) && (l <> model_proj_label) ) labels
+  Slab.filter (fun l -> not (is_counterexample_label l)) labels
 
 let is_model_trace_label label =
   Strings.has_prefix "model_trace:" label.lab_string
@@ -316,6 +323,7 @@ let get_model_trace_string ~labels =
   | [_; t_str] -> t_str
   | _ -> ""
 
+
 (* Functions for working with ITP labels *)
 
 let is_name_label label =

src/core/ident.mli

@@ -143,12 +143,20 @@ val id_unique_label :
 
 (** {2 labels for handling counterexamples} *)
 
-val model_label: label
+val model_label : label
+val model_projected_label : label
+val model_vc_label : label
+val model_vc_post_label : label
 
-val has_model_label: ident -> bool
+val has_a_model_label : ident -> bool
+(** [true] when [ident] has one of the labels above. *)
 
 val remove_model_labels : labels : Slab.t -> Slab.t
-(** Returns a copy of labels without labels ["model"] and ["model_projected"]. *)
+(** Returns a copy of labels without [model_label] and [model_projected_label]. *)
+
+val create_model_trace_label : string -> label
+
+val is_model_trace_label : label -> bool
 
 val append_to_model_trace_label : labels : Slab.t ->
   to_append : string ->

src/parser/parser.mly

@@ -35,63 +35,33 @@ end
     Debug.register_flag ~desc:"When set, model labels are not added during parsing"
       "no_auto_model"
 
-  let model_label = Ident.create_label "model"
-(*  let model_projected = Ident.create_label "model_projected"*)
-
-(*
-  let is_model_label l =
-    match l with
-    | Lpos _ -> false
-    | Lstr lab ->
-      (lab = model_label) || (lab = model_projected)
-
-  let model_lab_present labels =
-    List.exists is_model_label labels
-*)
+  let add_lab id l =
+    { id with id_lab = l }
 
-  let model_trace_regexp = Str.regexp "model_trace:"
-
-  let is_model_trace_label l =
-    match l with
-    | Lpos _ -> false
-    | Lstr lab ->
-      try
-	ignore(Str.search_forward model_trace_regexp lab.Ident.lab_string 0);
-	true
-      with Not_found -> false
-
-  let model_trace_lab_present labels =
-    List.exists is_model_trace_label labels
-
-  let add_model_trace id =
-    if Debug.test_flag debug_auto_model || model_trace_lab_present id.id_lab
-    then
-      id
-    else
+  let add_model_trace_label id =
+    if Debug.test_flag debug_auto_model then id else
+    let is_model_trace_label l =
+      match l with
+      | Lpos _ -> false
+      | Lstr lab -> Ident.is_model_trace_label lab
+    in
+    if List.exists is_model_trace_label id.id_lab then id else
       let l =
-        (Lstr (Ident.create_label ("model_trace:" ^ id.id_str)))
-        ::(Lstr model_label) :: id.id_lab in
+        (Lstr (Ident.create_model_trace_label id.id_str))
+        ::(Lstr Ident.model_label) :: id.id_lab in
       { id with id_lab = l }
 
-  let add_lab id l =
-    { id with id_lab = l }
-
   let add_model_labels (b : binder) =
     match b with
     | (loc, Some id, ghost, ty) ->
-      (loc, Some (add_model_trace id), ghost, ty)
+      (loc, Some (add_model_trace_label id), ghost, ty)
     | _ -> b
 
-  let model_vc_label = Ident.create_label "model_vc"
-
-  let model_vc_post_label = Ident.create_label "model_vc_post"
-
   let add_model_vc_label t =
-    {t with term_desc = Tnamed (Lstr model_vc_label, t)}
+    {t with term_desc = Tnamed (Lstr Ident.model_vc_label, t)}
 
   let add_model_vc_post_label t =
-    {t with term_desc = Tnamed (Lstr model_vc_post_label, t)}
-
+    {t with term_desc = Tnamed (Lstr Ident.model_vc_post_label, t)}
 
   let id_anonymous loc = { id_str = "_"; id_lab = []; id_loc = loc }
 
@@ -676,7 +646,7 @@ numeral:
 (* Program declarations *)
 
 pdecl:
-| VAL top_ghost labels(lident_rich) type_v          { Dval (add_model_trace $3, $2, $4) }
+| VAL top_ghost labels(lident_rich) type_v          { Dval (add_model_trace_label $3, $2, $4) }
 | LET top_ghost labels(lident_rich) fun_defn        { Dfun ($3, $2, $4) }
 | LET top_ghost labels(lident_rich) EQUAL fun_expr  { Dfun ($3, $2, $5) }
 | LET REC with_list1(rec_defn)                      { Drec $3 }
@@ -760,13 +730,13 @@ expr_:
 | LET top_ghost pattern EQUAL seq_expr IN seq_expr
     { match $3.pat_desc with
       | Pvar id ->
-          let id = add_model_trace id in
+          let id = add_model_trace_label id in
           Elet (id, $2, $5, $7)
       | Pwild -> Elet (id_anonymous $3.pat_loc, $2, $5, $7)
       | Ptuple [] -> Elet (id_anonymous $3.pat_loc, $2,
           { $5 with expr_desc = Ecast ($5, PTtuple []) }, $7)
       | Pcast ({pat_desc = Pvar id}, ty) ->
-          let id = add_model_trace id in
+          let id = add_model_trace_label id in
           Elet (id, $2, { $5 with expr_desc = Ecast ($5, ty) }, $7)
       | Pcast ({pat_desc = Pwild}, ty) ->
           let id = id_anonymous $3.pat_loc in
@@ -779,7 +749,7 @@ expr_:
             | Gnone -> $5 in
           Ematch (e, [$3, $7]) }
 | LET top_ghost labels(lident_op_id) EQUAL seq_expr IN seq_expr
-    { let id = add_model_trace $3 in
+    { let id = add_model_trace_label $3 in
       Elet (id, $2, $5, $7) }
 | LET top_ghost labels(lident_nq) fun_defn IN seq_expr
     { Efun ($3, $2, $4, $6) }
@@ -802,7 +772,7 @@ expr_:
 | WHILE seq_expr DO loop_annotation seq_expr DONE
     { Ewhile ($2, $4, $5) }
 | FOR lident EQUAL seq_expr for_direction seq_expr DO invariant* seq_expr DONE
-    { let id = add_model_trace $2 in
+    { let id = add_model_trace_label $2 in
       Efor (id, $4, $5, $6, $8, $9) }
 | ABSURD
     { Eabsurd }
@@ -963,13 +933,13 @@ pat_uni_:
 | pat_arg_                              { $1 }
 | uqualid pat_arg+                      { Papp ($1,$2) }
 | mk_pat(pat_uni_) AS labels(lident_nq) {
-  let id = add_model_trace $3 in Pas ($1,id) }
+  let id = add_model_trace_label $3 in Pas ($1,id) }
 | mk_pat(pat_uni_) cast                 { Pcast($1,$2) }
 
 pat_arg_:
 | UNDERSCORE                            { Pwild }
 | labels(lident_nq)                     {
-  let id = add_model_trace $1 in Pvar id }
+  let id = add_model_trace_label $1 in Pvar id }
 | uqualid                               { Papp ($1,[]) }
 | LEFTPAR RIGHTPAR                      { Ptuple [] }
 | LEFTPAR pattern_ RIGHTPAR             { $2 }

src/printer/cntexmp_printer.ml

@@ -71,15 +71,8 @@ let get_label labels regexp =
 let print_label fmt l =
   fprintf fmt "\"%s\"" l.lab_string
 
-(* already in Ident
-let model_label = Ident.create_label "model"
-  (* This label identifies terms that should be in counter-example. *)
- *)
-let model_vc_term_label = Ident.create_label "model_vc"
-  (* This label identifies the term that triggers the VC. *)
 let model_projection = Ident.create_label "model_projection"
 
-
 let add_model_element (el: term) info_model =
 (** Add element el (term) to info_model.
     If an element with the same hash (the same set of labels + the same
@@ -131,8 +124,8 @@ let model_trace_for_postcondition ~labels (info: vc_term_info)  =
   with Not_found ->
     (* no model_trace label => the term represents the return value *)
     Slab.add
-      (Ident.create_label
-	 ("model_trace:" ^ (Opt.get_def "" info.vc_func_name)  ^ "@result"))
+      (Ident.create_model_trace_label
+	 ((Opt.get_def "" info.vc_func_name)  ^ "@result"))
       labels
 
 let get_fun_name name =
@@ -149,7 +142,7 @@ let check_enter_vc_term t in_goal vc_term_info =
      postcondition or precondition of a function, extract the name of
      the corresponding function.
   *)
-  if in_goal && Slab.mem model_vc_term_label t.t_label then begin
+  if in_goal && Slab.mem Ident.model_vc_label t.t_label then begin
     vc_term_info.vc_inside <- true;
     vc_term_info.vc_loc <- t.t_loc;
     try
@@ -164,6 +157,6 @@ let check_enter_vc_term t in_goal vc_term_info =
 
 let check_exit_vc_term t in_goal info =
   (* Check whether the term triggering VC is exited. *)
-  if in_goal && Slab.mem model_vc_term_label t.t_label then begin
+  if in_goal && Slab.mem Ident.model_vc_label t.t_label then begin
     info.vc_inside <- false;
   end

src/printer/cntexmp_printer.mli

@@ -42,8 +42,6 @@ val print_label: Format.formatter -> Ident.label -> unit
 
 val model_projection: Ident.label
 
-val model_vc_term_label: Ident.label
-
 val add_model_element: Term.term -> S.t -> S.t
 
 val add_old: string -> string

src/printer/smtv2.ml

@@ -174,13 +174,11 @@ let print_typed_var info fmt vs =
 let print_var_list info fmt vsl =
   print_list space (print_typed_var info) fmt vsl
 
-let model_projected_label = Ident.create_label "model_projected"
-
 let collect_model_ls info ls =
   if Sls.mem ls info.meta_model_projection then
     info.list_projs <- Stdlib.Sstr.add (sprintf "%a" (print_ident info) ls.ls_name) info.list_projs;
   if ls.ls_args = [] && (Slab.mem model_label ls.ls_name.id_label ||
-  Slab.mem model_projected_label ls.ls_name.id_label) then
+  Slab.mem Ident.model_projected_label ls.ls_name.id_label) then
     let t = t_app ls [] ls.ls_value in
     info.info_model <-
       add_model_element

src/transform/add_name_traceability_labels.ml

-(********************************************************************)
-(*                                                                  *)
-(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
-(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
-(*                                                                  *)
-(*  This software is distributed under the terms of the GNU Lesser  *)
-(*  General Public License version 2.1, with the special exception  *)
-(*  on linking described in file LICENSE.                           *)
-(*                                                                  *)
-(********************************************************************)
-
-(*
-The transformation that adds labels with information needed for
-traceability from the names in the Why output to names in the
-Why input (more precisely to the names that are present
-at the time this transformation is run).
-
-This transformation should be called on the AST corresponding to
-the Why input. For each element it adds the label with the information
-about the name of the element.  
-*)
-
-open Term
-open Ident
-open Format
-
-let debug = Debug.register_info_flag "add_name_traceability"
-  ~desc:"Print@ debugging@ messages@ about@ adding@ traceability@ labels."
-
-let term2string_experimental t =
-  (* TODO: Pretty.print_term prints also labels + it generates unique identifiers when printing *)
-  Pretty.print_term str_formatter t;
-  flush_str_formatter ()
-
-(* TODO: should print the term *)
-let term2string t = "term"
-
-let create_traceability_label str =
-  Ident.create_label ("model_trace:"^str)
-
-let create_traceability_identifier ident =
-  id_clone ~label:(Slab.singleton (create_traceability_label ident.id_string))  ident
-
-(*Adds name traceability label to the list of terms. *)
-let rec add_traceability_label_list terms collected_terms =
-  match terms with
-  | [] -> List.rev collected_terms
-  | t::tail ->
-    let t_traceable = add_traceability_label t in
-    add_traceability_label_list tail (t_traceable::collected_terms)
-(* Adds name traceability label to the term. *)
-and  add_traceability_label t = 
-  let term = match t.t_node with
-    |Tvar v ->
-      Debug.dprintf debug "Adding traceability labels: variable@.";
-      let vs_name_t = create_traceability_identifier v.vs_name in
-      Debug.dprintf debug "Creating vsymbol@.";
-      let v_t = create_vsymbol vs_name_t v.vs_ty in
-      Debug.dprintf debug "Creating t_var@.";
-      (* TODO: The following does not work - investigate. *)
-      (* t_var v_t *)
-      t_var v
-    | Tapp (l_symb, terms) ->
-      Debug.dprintf debug "Adding traceability labels: Tapp@.";
-      let l_symb_name = create_traceability_identifier l_symb.ls_name in
-      let l_symb_t = create_lsymbol l_symb_name l_symb.ls_args l_symb.ls_value in
-      let terms_t = add_traceability_label_list terms [] in
-      t_app l_symb terms_t t.t_ty
-    | Tif (t1, t2, t3) ->
-      Debug.dprintf debug "Adding traceability labels: Tif@.";
-      let t1t = add_traceability_label t1 in
-      let t2t = add_traceability_label t2 in
-      let t3t = add_traceability_label t3 in
-      t_if t1t t2t t3t
-    | Tlet (t, t_bound) ->
-      Debug.dprintf debug "Adding traceability labels: Tlet@.";
-      let tt = add_traceability_label t in
-      let vs_bound, term_bound = t_open_bound t_bound in
-      let vs_boundt = vs_bound in (* TODO *)
-      let term_boundt = add_traceability_label term_bound in
-      let t_boundt = t_close_bound vs_boundt term_boundt in
-      t_let tt t_boundt
-    | Tcase (t, tbs) ->
-      (* TODO *)
-      t
-    | Teps tb ->
-      (* TODO *)
-      t
-    | Tquant (q, fq) ->
-      let vl, tl, f = t_open_quant fq in
-      let ft = add_traceability_label f in
-      (* TODO tl, vl *)
-      t_quant_close q vl tl ft
-    | Tbinop (op, f1, f2) -> 
-      Debug.dprintf debug "Adding traceability labels: binary operation@.";
-      let f1_t = add_traceability_label f1 in
-      let f2_t = add_traceability_label f2 in
-      t_binary op f1_t f2_t
-    | Tnot t ->
-      (* TODO *)
-      t
-    | _ ->
-      Debug.dprintf debug "Adding traceability labels: unsupported term@.";
-      t 
-  in
-  let term = t_label_copy t term in
-  Debug.dprintf debug "Adding label to toplevel term@.";
-  t_label_add (create_traceability_label (term2string t)) term
-
-let add_traceability_labels = Trans.rewrite add_traceability_label None
-
-let () =
-  Trans.register_transform "add_name_traceability_labels" add_traceability_labels
-    ~desc:"Add@ labels@ to@ terms@ used@ in@ counterexample@ report@ holding information@ needed@ for@ traceability@ of@ identifiers'@ names.";

src/transform/intro_projections_counterexmp.ml

@@ -62,12 +62,6 @@ let debug_decl decl =
   Debug.dprintf debug "Declaration %s @." s
 *)
 
-(* Label for terms that should be in counterexample *)
-(* already in Ident
-   let model_label = Ident.create_label "model" *)
-(* Label for terms that should be projected in counterexample *)
-let model_proj_label = Ident.create_label "model_projected"
-
 (* Meta to tag projection functions *)
 let meta_projection = Theory.register_meta "model_projection" [Theory.MTlsymbol]
   ~desc:"Declares@ the@ projection."
@@ -194,7 +188,7 @@ let intro_proj_for_ls env map_projs ls_projected =
      @param map_projs maps types to projection function for these types
      @param ls_projected the label symbol that should be projected
   *)
-  if not (Slab.mem model_proj_label ls_projected.ls_name.id_label)
+  if not (Slab.mem Ident.model_projected_label ls_projected.ls_name.id_label)
   then
     (* ls_projected has not a label "model_projected" *)
     []

src/transform/intro_vc_vars_counterexmp.ml

@@ -22,17 +22,6 @@ let meta_vc_location =
   Theory.register_meta_excl "vc_location" [Theory.MTstring]
   ~desc:"Location@ of@ the@ term@ that@ triggers@ vc@ in@ the@ form@ file:line:col."
 
-(* let model_label = Ident.create_label "model"
-  already in Ident
-  (* Identifies terms that should be in counterexample and should not be projected. *)
- *)
-let model_projected_label = Ident.create_label "model_projected"
-  (* Identifies terms that should be in counterexample and should be projected. *)
-let model_vc_label = Ident.create_label "model_vc"
-  (* Identifies the term that triggers the VC. *)
-let model_vc_post_label = Ident.create_label "model_vc_post"
-(* Identifies the postcondition that triggers the VC. *)
-
 (* Information about the term that triggers VC.  *)
 type vc_term_info = {
   vc_inside : bool;
@@ -91,9 +80,6 @@ let model_trace_for_postcondition ~labels =
   with Not_found ->
     labels
 
-let is_counterexample_label l =
-  l = model_label || l = model_projected_label
-
 
 (* Preid table necessary to avoid duplication of *_vc_constant *)
 module Hprid = Exthtbl.Make (struct
@@ -131,7 +117,7 @@ let rec do_intro info vc_loc vc_map vc_var t =
 	     should be in counterexample, introduce new constant in location
 	     loc with all labels necessary for collecting it for counterexample
 	     and make it equal to the variable *)
-          if Slab.exists is_counterexample_label ls.id_label then
+          if Ident.has_a_model_label ls then
 	    let const_label = if info.vc_pre_or_post then
 	      model_trace_for_postcondition ~labels:ls.id_label
 	    else

src/transform/simplify_formula.ml

@@ -112,7 +112,7 @@ let rec fmla_quant ~keep_model_vars sign f = function
   | [] -> [], f
   | vs::l ->
      let vsl, f = fmla_quant ~keep_model_vars sign f l in
-     if keep_model_vars && has_model_label vs.vs_name then
+     if keep_model_vars && has_a_model_label vs.vs_name then
        vs::vsl, f
      else
       try