Treat labels attributes for pretty printing of counterexamples at labels

We now use the information inside attributes to correctly associate a
label to each counterexamples. The information is carried inside
attributes which are preserved/collected during ce transformations and
printing to smt2.
The collection filled during the printing of the task is reused during the
printing of counterexamples to add "at label" where needed.

bench/ce/records.mlw

@@ -34,7 +34,7 @@ module M
   =
     x := { !x with f = 6 };
     !x
-    
+
   let record_match_eval_test44 (x : ref r) : r
     ensures { result.g }
   = [@vc:sp]
@@ -85,18 +85,4 @@ module Mutable
     x.f <- 6;
     x
 
-  let record_old_test1 (x : r) : unit
-    ensures { old x.f = x.f}
-  =
-    x.f <- 6
-
-  let record_at_test2 (x : r) : unit
-  =
-    label L in
-    x.f <- 6;
-    label M in
-    x.f <- 12;
-    assert { x at L = x at M} 
-
 end
-

bench/ce/records_label.mlw

+
+
+module Old
+
+  use int.Int
+
+  type r = {mutable f : int; mutable g : bool}
+
+  val y : r
+
+  let record_old_test1 (x : r) : unit
+    ensures { old (x.f + y.f) = x.f }
+  =
+    x.f <- 6
+    
+  let record_at_test2 (x : r) : unit
+  =
+    label L in
+    x.f <- 6;
+    label M in
+    x.f <- 12;
+    assert { x.f at L = ((x.f + x.f + 1) at M + x.f + y.f)}
+
+  let several_hats (x : r): unit
+  = 
+    label L in
+    label M in
+    x.f <- 6;
+    (* Here, the counterexample variable should mention both M and L *)
+    assert { x.f at L  = x.f at M + 1}
+
+end
\ No newline at end of file

src/core/model_parser.ml

@@ -346,7 +346,7 @@ let split_model_trace_name mt_name =
   | first::second::_ -> (first, second)
   | [] -> ("", "")
 
-let create_model_element ~name ~value ?location ?term () =
+let create_model_element ~name ~value ~attrs ?location ?term () =
   let (name, type_s) = split_model_trace_name name in
   let me_kind = match type_s with
     | "result" -> Result
@@ -355,7 +355,7 @@ let create_model_element ~name ~value ?location ?term () =
   let me_name = {
     men_name = name;
     men_kind = me_kind;
-    men_attrs = match term with | None -> Sattr.empty | Some t -> t.t_attrs;
+    men_attrs = match term with | None -> attrs | Some t -> Sattr.union t.t_attrs attrs;
   } in
   {
     me_name = me_name;
@@ -407,19 +407,43 @@ type model_parser =  string -> Printer.printer_mapping -> model
 
 type raw_model_parser =
   Sstr.t -> ((string * string) list) Mstr.t -> string list ->
-    string -> model_element list
+    Ident.Sattr.t Mstr.t -> string -> model_element list
 
 (*
 ***************************************************************
 **  Quering the model
 ***************************************************************
 *)
-let print_model_element ~print_attrs print_model_value me_name_trans fmt m_element =
+
+(* Adapt name of the model to potential labels applying to it: *)
+let apply_location_label ~at_loc ~attrs me_name =
+  let sats =
+    Sattr.filter (fun x -> Strings.has_prefix "at" x.attr_string) attrs
+  in
+  let _labels_added, me_name =
+    Sattr.fold (fun attr_at (labels_added, me_name) ->
+      match Strings.split ':' attr_at.attr_string with
+      | "at" :: label :: "loc" :: loc_file :: loc_line :: [] ->
+          let loc_line = int_of_string loc_line in
+          if at_loc = (Filename.basename loc_file, loc_line) &&
+             not (Sstr.mem label labels_added)
+          then
+            (Sstr.add label labels_added, me_name ^ " at " ^ label)
+          else
+            (labels_added, me_name)
+      | _ -> (labels_added, me_name))
+      sats (Sstr.empty, me_name)
+  in
+  me_name
+
+let print_model_element ~at_loc ~print_attrs print_model_value me_name_trans fmt m_element =
   match m_element.me_name.men_kind with
   | Error_message ->
     fprintf fmt "%s" m_element.me_name.men_name
   | _ ->
     let me_name = me_name_trans m_element.me_name in
+    let attrs = m_element.me_name.men_attrs in
+    let me_name = apply_location_label ~at_loc ~attrs me_name in
     if print_attrs then
       fprintf fmt  "%s, [%a] = %a"
         me_name
@@ -431,10 +455,16 @@ let print_model_element ~print_attrs print_model_value me_name_trans fmt m_eleme
         me_name
         print_model_value m_element.me_value
 
-let print_model_elements ~print_attrs ?(sep = "\n") print_model_value me_name_trans fmt m_elements =
-  Pp.print_list (fun fmt () -> Pp.string fmt sep) (print_model_element ~print_attrs print_model_value me_name_trans) fmt m_elements
+let print_model_elements ~at_loc ~print_attrs ?(sep = "\n")
+    print_model_value me_name_trans fmt m_elements
+  =
+  Pp.print_list (fun fmt () -> Pp.string fmt sep)
+    (print_model_element ~at_loc ~print_attrs print_model_value me_name_trans)
+    fmt m_elements
 
-let print_model_file ~print_attrs ~print_model_value fmt me_name_trans filename model_file =
+let print_model_file ~print_attrs ~print_model_value fmt
+    me_name_trans filename model_file
+  =
   (* Relativize does not work on nighly bench: using basename instead. It
      hides the local paths.  *)
   let filename = Filename.basename filename  in
@@ -442,7 +472,7 @@ let print_model_file ~print_attrs ~print_model_value fmt me_name_trans filename
   IntMap.iter
     (fun line m_elements ->
       fprintf fmt "@\nLine %d:@\n" line;
-      print_model_elements ~print_attrs print_model_value me_name_trans fmt m_elements)
+      print_model_elements ~at_loc:(filename,line) ~print_attrs print_model_value me_name_trans fmt m_elements)
     model_file;
   fprintf fmt "@\n"
 
@@ -549,6 +579,7 @@ let add_offset off (loc, a) =
   (Loc.user_position f (l + off) fc lc, a)
 
 let interleave_line
+    ~filename
     ~print_attrs
     start_comment
     end_comment
@@ -566,7 +597,7 @@ let interleave_line
       asprintf "%s%s%a%s"
         (get_padding line)
         start_comment
-        (print_model_elements ~print_attrs ~sep:"; " print_model_value_human me_name_trans) model_elements
+        (print_model_elements ~at_loc:(filename,line_number) ~print_attrs ~sep:"; " print_model_value_human me_name_trans) model_elements
         end_comment in
 
     (* We need to know how many lines will be taken by the counterexample. This
@@ -598,8 +629,9 @@ let interleave_with_source
        the file because they contain extra ".." which cannot be reliably removed
        (because of potential symbolic link). So, we use the basename.
     *)
+    let rel_filename = Filename.basename rel_filename in
     let model_files =
-      StringMap.filter (fun k _ -> Filename.basename k = Filename.basename rel_filename)
+      StringMap.filter (fun k _ -> Filename.basename k = rel_filename)
         model.model_files
     in
     let model_file = snd (StringMap.choose model_files) in
@@ -609,7 +641,7 @@ let interleave_with_source
     in
     let (source_code, _, _, _, gen_loc) =
       List.fold_left
-        (interleave_line ~print_attrs
+        (interleave_line ~filename:rel_filename ~print_attrs
            start_comment end_comment me_name_trans model_file)
         ("", 1, 0, locations, [])
         (src_lines_up_to_last_cntexmp_el source_code model_file)
@@ -766,12 +798,17 @@ and replace_projection_array const_function a =
 let build_model_rec (raw_model: model_element list) (term_map: Term.term Mstr.t) (model: model_files) =
   List.fold_left (fun model raw_element ->
     let raw_element_name = raw_element.me_name.men_name in
-    let raw_element_value = replace_projection (fun x -> (recover_name term_map x).men_name) raw_element.me_value in
+    let raw_element_value =
+      replace_projection
+        (fun x -> (recover_name term_map x).men_name)
+        raw_element.me_value
+    in
     try
       (
        let t = Mstr.find raw_element_name term_map in
+       let attrs = Sattr.union raw_element.me_name.men_attrs t.t_attrs in
        let model_element = {
-         me_name = construct_name (get_model_trace_string ~attrs:t.t_attrs) t.t_attrs;
+         me_name = construct_name (get_model_trace_string ~attrs:t.t_attrs) attrs;
          me_value = raw_element_value;
          me_location = t.t_loc;
          me_term = Some t;
@@ -887,7 +924,8 @@ let make_mp_from_raw (raw_mp:raw_model_parser) =
     let list_proj = printer_mapping.list_projections in
     let list_records = printer_mapping.list_records in
     let noarg_cons = printer_mapping.noarg_constructors in
-    let raw_model = raw_mp list_proj list_records noarg_cons input in
+    let set_str = printer_mapping.set_str in
+    let raw_model = raw_mp list_proj list_records noarg_cons set_str input in
     build_model raw_model printer_mapping
 
 let register_model_parser ~desc s p =
@@ -906,4 +944,4 @@ let list_model_parsers () =
 
 let () = register_model_parser
   ~desc:"Model@ parser@ with@ no@ output@ (used@ if@ the@ solver@ does@ not@ support@ models." "no_model"
-  (fun _ _ _ _ -> [])
+  (fun _ _ _ _ _ -> [])

src/core/model_parser.mli

@@ -114,6 +114,7 @@ type model_element = {
 val create_model_element :
   name      : string ->
   value     : model_value ->
+  attrs     : Ident.Sattr.t ->
   ?location : Loc.position ->
   ?term     : Term.term ->
   unit ->
@@ -333,7 +334,7 @@ type model_parser =  string -> Printer.printer_mapping -> model
 
 type raw_model_parser =
   Wstdlib.Sstr.t -> ((string * string) list) Wstdlib.Mstr.t ->
-    string list -> string -> model_element list
+    string list -> Ident.Sattr.t Wstdlib.Mstr.t -> string -> model_element list
 (** Parses the input string into model elements.
     [raw_model_parser: proj->record_map->noarg_cons->s->mel]
     [proj]: is the list of projections

src/core/printer.ml

@@ -37,6 +37,7 @@ type printer_mapping = {
   list_projections: Sstr.t;
   list_records: ((string * string) list) Mstr.t;
   noarg_constructors: string list;
+  set_str: Sattr.t Mstr.t
 }
 
 type printer_args = {
@@ -63,6 +64,7 @@ let get_default_printer_mapping = {
   list_projections = Sstr.empty;
   list_records = Mstr.empty;
   noarg_constructors = [];
+  set_str = Mstr.empty
 }
 
 let register_printer ~desc s p =

src/core/printer.mli

@@ -39,7 +39,11 @@ type printer_mapping = {
   list_records: ((string * string) list) Mstr.t;
   (* List of constructors with no arguments that can be confused for variables
      during parsing. *)
-  noarg_constructors: string list
+  noarg_constructors: string list;
+  (* List of attributes corresponding to a printed constants (that was on the
+     immediate term, not inside the ident) *)
+  set_str: Sattr.t Mstr.t
+
 }
 
 type printer_args = {

src/driver/collect_data_model.ml

@@ -447,9 +447,14 @@ and convert_z3_array (t: term) : array =
 and convert_record l =
   List.map (fun (f, v) -> f, convert_to_model_value v) l
 
-let convert_to_model_element name (t: term) =
+let convert_to_model_element ~set_str name (t: term) =
   let value = convert_to_model_value t in
-  Model_parser.create_model_element ~name ~value ()
+  let attrs =
+    match Mstr.find name set_str with
+    | exception Not_found -> Ident.Sattr.empty
+    | attrs -> attrs
+  in
+  Model_parser.create_model_element ~name ~value ~attrs ()
 
 let default_apply_to_record (list_records: (string list) Mstr.t)
     (noarg_constructors: string list) (t: term) =
@@ -586,7 +591,7 @@ and convert_tarray_to_array a =
   | TStore (a, t1, t2) -> Store (convert_tarray_to_array a, convert_tterm_to_term t1, convert_tterm_to_term t2)
 
 let create_list (projections_list: Sstr.t) (list_records: ((string * string) list) Mstr.t)
-    (noarg_constructors: string list) (table: definition Mstr.t) =
+    (noarg_constructors: string list) (set_str: Ident.Sattr.t Mstr.t) (table: definition Mstr.t) =
 
   (* Convert list_records to take replace fields with model_trace when
      necessary. *)
@@ -657,7 +662,7 @@ let create_list (projections_list: Sstr.t) (list_records: ((string * string) lis
   (* Then converts all variables to raw_model_element *)
   Mstr.fold
     (fun key value list_acc ->
-      try (convert_to_model_element key value :: list_acc)
+      try (convert_to_model_element ~set_str key value :: list_acc)
       with Not_value when not (Debug.test_flag Debug.stack_trace) -> list_acc
       | e -> raise e)
     table

src/driver/collect_data_model.mli

@@ -26,4 +26,5 @@ val register_apply_to_records:
 (* From the table generated by the parser, build a list of model_element *)
 val create_list:
     Sstr.t -> ((string * string) list) Mstr.t -> string list ->
+    Ident.Sattr.t Mstr.t ->
       Smt2_model_defs.definition Mstr.t -> Model_parser.model_element list

src/driver/parse_smtv2_model.ml

@@ -57,9 +57,9 @@ let do_parsing model =
        l;
      Wstdlib.Mstr.empty
 
-let do_parsing list_proj list_records noarg_constructors model =
+let do_parsing list_proj list_records noarg_constructors set_str model =
   let m = do_parsing model in
-  Collect_data_model.create_list list_proj list_records noarg_constructors m
+  Collect_data_model.create_list list_proj list_records noarg_constructors set_str m
 
 (* Parses the model returned by CVC4, Z3 or Alt-ergo.
    Returns the list of pairs term - value *)
@@ -67,7 +67,7 @@ let do_parsing list_proj list_records noarg_constructors model =
    match on "I don't know". But we also need to begin
    parsing on a fresh new line ".*" ensures it *)
 let parse : raw_model_parser =
-  fun list_proj list_records noarg_constructors input ->
+  fun list_proj list_records noarg_constructors set_str input ->
   try
 (*    let r = Str.regexp "unknown\\|sat\\|\\(I don't know.*\\)" in
     ignore (Str.search_forward r input 0);
@@ -75,7 +75,7 @@ let parse : raw_model_parser =
     let nr = Str.regexp "^)+" in
     let res = Str.search_backward nr input (String.length input) in
     let model_string = String.sub input 0 (res + String.length (Str.matched_string input)) in
-    do_parsing list_proj list_records noarg_constructors model_string
+    do_parsing list_proj list_records noarg_constructors set_str model_string
   with
   | Not_found -> []
 

src/printer/alt_ergo.ml

@@ -422,7 +422,8 @@ let print_prop_decl vc_loc args info fmt k pr f =
 				queried_terms = model_list;
                                 list_projections = info.list_projs;
                                 list_records = Mstr.empty;
-                                noarg_constructors = []};
+                                noarg_constructors = [];
+                                set_str = Mstr.empty};
       fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n"
         (print_ident info) pr.pr_name (print_fmla info) f
   | Plemma -> assert false

src/printer/cntexmp_printer.ml

@@ -9,6 +9,7 @@
 (*                                                                  *)
 (********************************************************************)
 
+open Wstdlib
 open Ident
 open Term
 
@@ -93,3 +94,31 @@ let check_exit_vc_term t in_goal info =
   if in_goal && Sattr.mem Ident.model_vc_attr t.t_attrs then begin
     info.vc_inside <- false;
   end
+
+(* This is used to update info_labels of info in the printer. This takes the
+   label informations present in the term and add a location to help pretty
+   printing the counterexamples.
+*)
+let update_info_labels lsname cur_attrs t ls =
+  let cur_l =
+    match Mstr.find lsname cur_attrs with
+    | exception Not_found -> Sattr.empty
+    | s -> s
+  in
+  let updated_attr_labels =
+    (* Change attributes labels with "at:" to located
+       "at:[label]:loc:filename:line" *)
+    Sattr.fold (fun attr acc ->
+        if Strings.has_prefix "at:" attr.attr_string then
+          let (f, l, _, _) =
+            match t.t_loc with
+            | None -> Loc.get (Opt.get_def Loc.dummy_position ls.ls_name.id_loc)
+            | Some loc -> Loc.get loc
+          in
+          let attr = create_attribute (attr.attr_string ^ ":loc:" ^ f ^ ":" ^ (string_of_int l)) in
+          Sattr.add attr acc
+        else
+          acc
+      ) (Sattr.union t.t_attrs ls.ls_name.id_attrs) cur_l
+  in
+  Mstr.add lsname updated_attr_labels cur_attrs

src/printer/cntexmp_printer.mli

@@ -9,6 +9,8 @@
 (*                                                                  *)
 (********************************************************************)
 
+open Wstdlib
+open Ident
 open Term
 
 (* Information about the term that triggers VC.  *)
@@ -42,3 +44,6 @@ val model_trace_for_postcondition:
 val check_enter_vc_term: Term.term -> bool -> vc_term_info -> unit
 
 val check_exit_vc_term: Term.term -> bool -> vc_term_info -> unit
+
+val update_info_labels: string -> Sattr.t Mstr.t -> Term.term ->
+  Term.lsymbol -> Sattr.t Mstr.t

src/printer/smtv2.ml

@@ -142,6 +142,7 @@ type info = {
   info_cntexample: bool;
   info_incremental: bool;
   info_set_incremental: bool;
+  mutable info_labels: Sattr.t Mstr.t;
   mutable incr_list: (prsymbol * term) list;
 }
 
@@ -256,18 +257,23 @@ let rec print_term info fmt t =
         (print_type info) t fmt tl
       | None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
           | [] ->
-	    let vc_term_info = info.info_vc_term in
-	    if vc_term_info.vc_inside then begin
-	      match vc_term_info.vc_loc with
-	      | None -> ()
-	      | Some loc ->
+
+            let str_ls = sprintf "%a" (print_ident info) ls.ls_name in
+            let cur_var = info.info_labels in
+            let new_var = update_info_labels  str_ls cur_var t ls in
+            let () = info.info_labels <- new_var in
+            let vc_term_info = info.info_vc_term in
+            if vc_term_info.vc_inside then begin
+              match vc_term_info.vc_loc with
+              | None -> ()
+              | Some loc ->
                 let attrs = (* match vc_term_info.vc_func_name with
                   | None -> *)
                     ls.ls_name.id_attrs
                   (* | Some _ ->
                     model_trace_for_postcondition ~attrs:ls.ls_name.id_attrs info.info_vc_term
                    *)
-in
+                in
 		let _t_check_pos = t_attr_set ~loc attrs t in
 		(* TODO: temporarily disable collecting variables inside the term triggering VC *)
 		(*info.info_model <- add_model_element t_check_pos info.info_model;*)
@@ -325,7 +331,8 @@ and print_fmla info fmt f =
       | Some s -> syntax_arguments_typed s (print_term info)
         (print_type info) f fmt tl
       | None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
-          | [] -> print_ident info fmt ls.ls_name
+          | [] ->
+              print_ident info fmt ls.ls_name
           | _ -> fprintf fmt "(%a@ %a)"
               (print_ident info) ls.ls_name
               (print_list space (print_term info)) tl
@@ -572,7 +579,9 @@ let print_prop_decl vc_loc args info fmt k pr f = match k with
                                 queried_terms = model_list;
                                 list_projections = info.list_projs;
                                 Printer.list_records = info.list_records;
-                                noarg_constructors = info.noarg_constructors}
+                                noarg_constructors = info.noarg_constructors;
+                                set_str = info.info_labels;
+                              }
   | Plemma -> assert false
 
 let print_constructor_decl info fmt (ls,args) =
@@ -712,6 +721,7 @@ let print_task version args ?old:_ fmt task =
     (* info_set_incremental add the incremental option to the header. It is not
        needed for some provers
     *)
+    info_labels = Mstr.empty;
     info_set_incremental = not need_push && incremental;
     incr_list = [];
     }

src/transform/intro_vc_vars_counterexmp.ml

@@ -130,6 +130,12 @@ let rec do_intro info vc_loc vc_map vc_var t =
               in
               let const_name = ls.id_string^"_vc_constant" in
               let axiom_name = ls.id_string^"_vc_axiom" in
+              let labels_attr =
+                Sattr.filter (fun x ->
+                    Strings.has_prefix "at:" x.attr_string)
+                  t.t_attrs
+              in
+              let const_attr = Sattr.union const_attr labels_attr in
               (* Create a new id here to check the couple name, location. *)
               let id_new = Ident.id_user ~attrs:const_attr const_name loc in
               (* The following check is used to avoid duplication of

src/transform/prepare_for_counterexmp.ml

@@ -34,7 +34,8 @@ let prepare_for_counterexmp2 env task =
     Debug.dprintf debug "Get ce@.";
     let comp_trans = Trans.seq [
       Intro_vc_vars_counterexmp.intro_vc_vars_counterexmp;
-      Intro_projections_counterexmp.intro_projections_counterexmp env ] in
+      Intro_projections_counterexmp.intro_projections_counterexmp env
+    ] in
     Trans.apply comp_trans task
   end