Merge branch 'counter-examples'

examples/tests/cvc4-models.mlw

@@ -11,7 +11,7 @@ module M
   val y "model" "model_trace:y" :ref int
 
   let incr ( x23 "model" "model_trace:x23" : ref int ): unit
-  ensures { "model_vc" "model_func" !x23 = old !x23 + 2 + !y }
+  ensures { "model_vc_post" !x23 = old !x23 + 2 + !y }
   =
   (*#"/home/cmarche/recherche/why/tests/c/binary_search.c" 62 27 32#*)
   y := !y + 1;
@@ -68,7 +68,7 @@ module M
   meta "model_projection" function projf_r_g
 
   let record_match_eval_test1 (x "model" "model_trace:x" : r) : int
-  ensures { "model_vc" "model_func" result = 1 }
+  ensures { "model_vc_post" result = 1 }
   =
   if x.g then
     x.f
@@ -86,7 +86,7 @@ module M
   x := { !x with f = 6}
 
   let record_match_eval_test4 (x "model" "model_trace:x" : ref r) : r
-  ensures { "model_vc" "model_func" result.g }
+  ensures { "model_vc_post" result.g }
   =
   x := { !x with f = 6 };
   !x
@@ -94,7 +94,7 @@ module M
   val re "model_projected" : ref r
 
   let test_record_match_eval_test5 (x "model" "model_trace:x" : ref r) : r
-  ensures { "model_vc" "model_func" result = !re }
+  ensures { "model_vc_post" result = !re }
   =
   x := { !x with f = 6 };
   !x

modules/ref.mlw

@@ -13,7 +13,7 @@
 
 module Ref
 
-  type ref 'a = { mutable contents : 'a }
+  type ref 'a = { mutable contents "model_trace:" : 'a }
 
   function (!) (x: ref 'a) : 'a = x.contents
 

src/core/ident.ml

@@ -85,6 +85,13 @@ let get_model_element_name ~labels =
   | [_] -> ""
   | _ -> assert false
 
+let get_model_trace_string ~labels =
+  let tl = get_model_trace_label ~labels in
+  let splitted = Str.bounded_split (Str.regexp_string ":") tl.lab_string 2 in
+  match splitted with
+  | [_; t_str] -> t_str
+  | _ -> ""
+
 
 (** Identifiers *)
 

src/core/ident.mli

@@ -49,6 +49,12 @@ val get_model_element_name : labels : Slab.t -> string
     Throws Not_found if there is no element name (there is no
     label of the form "model_trace:+". *)
 
+val get_model_trace_string : labels : Slab.t -> string
+(** If labels contain a label of the form "model_trace:mt_string*",
+    return mt_string.
+    Throws Not_found if there is no mt_string (there is no
+    label of the form "model_trace:*". *)
+
 val get_model_trace_label : labels : Slab.t -> Slab.elt
 (** Return label of the for "model_trace:*".
     Throws Not_found if there is no such label.*)

src/core/model_parser.ml

@@ -93,38 +93,45 @@ print_model_value fmt value =
 **  Model elements
 ***************************************************************
 *)
-type model_element_type =
+
+type model_element_kind =
 | Result
 | Old
 | Other
 
+type model_element_name = {
+  men_name   : string;
+  men_kind   : model_element_kind;
+}
+
 type model_element = {
-  me_name     : string;
-  me_type     : model_element_type;
+  me_name     : model_element_name;
   me_value    : model_value;
   me_location : Loc.position option;
   me_term     : Term.term option;
   me_text_info: bool;
 }
 
-let split_me_name name =
-  let splitted = Str.bounded_split (Str.regexp_string "@") name 2 in
+let split_model_trace_name mt_name =
+  (** Mt_name is of the form "name[@type[@*]]". Return (name, type) *)
+  let splitted = Str.bounded_split (Str.regexp_string "@") mt_name 3 in
   match splitted with
   | [first] -> (first, "")
-  | first::[second] ->
-    (first, second)
-  | _ -> (* here, "_" can only stand for [] *)
-    ("", "")
+  | first::second::_ -> (first, second)
+  | [] -> ("", "")
 
 let create_model_element ~name ~value ?location ?term () =
-  let (name, type_s) = split_me_name name in
-  let t = match type_s with
+  let (name, type_s) = split_model_trace_name name in
+  let me_kind = match type_s with
     | "result" -> Result
     | "old" -> Old
     | _ -> Other in
+  let me_name = {
+    men_name = name;
+    men_kind = me_kind;
+  } in
   {
-    me_name = name;
-    me_type = t;
+    me_name = me_name;
     me_value = value;
     me_location = location;
     me_term = term;
@@ -173,9 +180,9 @@ type raw_model_parser =  string -> model_element list
 *)
 let print_model_element me_name_trans fmt m_element =
   if m_element.me_text_info then
-    fprintf fmt "%s" m_element.me_name
+    fprintf fmt "%s" m_element.me_name.men_name
   else
-    let me_name = me_name_trans (m_element.me_name, m_element.me_type) in
+    let me_name = me_name_trans m_element.me_name in
     fprintf fmt  "%s = %a"
       me_name print_model_value m_element.me_value
 
@@ -190,11 +197,11 @@ let print_model_file fmt me_name_trans filename model_file =
       print_model_elements me_name_trans fmt m_elements)
     model_file
 
-let why_name_trans (me_name, me_type) =
-  match me_type with
+let why_name_trans me_name =
+  match me_name.men_kind with
   | Result -> "result"
-  | Old -> "old" ^ " " ^ me_name
-  | Other -> me_name
+  | Old    -> "old" ^ " " ^ me_name.men_name
+  | Other  -> me_name.men_name
 
 let print_model
     ?(me_name_trans = why_name_trans)
@@ -322,7 +329,7 @@ let print_model_json
     fmt
     model =
   let me_name_to_str = fun me ->
-    me_name_trans (me.me_name, me.me_type) in
+    me_name_trans me.me_name in
   Json.map_bindings
     (fun s -> s)
     (print_model_elements_on_lines_json me_name_to_str)
@@ -353,35 +360,19 @@ let add_to_model model model_element =
     let model_file = IntMap.add line_number elements model_file in
     StringMap.add filename model_file model
 
-(* Estabilish mapping to why3 code *)
-let rec extract_element_name labels raw_string regexp =
-  match labels with
-  | [] -> raw_string
-  | label::labels_tail ->
-    let l_string = label.lab_string in
-    begin
-      try
-	ignore(Str.search_forward regexp l_string 0);
-	let end_pos = Str.match_end () in
-	String.sub l_string end_pos ((String.length l_string) - end_pos)
-      with Not_found -> extract_element_name labels_tail raw_string regexp
-    end
-
-let get_element_name term raw_string  =
-  let labels = Slab.elements term.t_label in
-  let regexp = Str.regexp "model_trace:" in
-  extract_element_name labels raw_string regexp
-
-
 let rec build_model_rec raw_model terms model =
 match raw_model with
   | [] -> model
   | model_element::raw_strings_tail ->
     let (element_name, element_location, element_term, terms_tail) =
       match terms with
-      | [] -> (model_element.me_name, None, None, [])
+      | [] -> (model_element.me_name.men_name, None, None, [])
       | term::t_tail ->
-        ((get_element_name term model_element.me_name),
+	let get_element_name term raw_string  =
+	  try
+	    get_model_trace_string ~labels:term.t_label
+	  with Not_found -> raw_string in
+        ((get_element_name term model_element.me_name.men_name),
          term.t_loc,
          Some term, t_tail) in
     let new_model_element = create_model_element
@@ -415,9 +406,12 @@ let handle_contradictory_vc model_files vc_term_loc =
       let model_elements = get_elements model_file line_number in
       if model_elements = [] then
       (* The vc is contradictory, add special model element  *)
+	let me_name = {
+	  men_name = "the check fails with all inputs";
+	  men_kind = Other;
+	} in
 	let me = {
-	  me_name = "the check fails with all inputs";
-	  me_type = Other;
+	  me_name = me_name;
 	  me_value = Unparsed "";
 	  me_location = Some pos;
 	  me_term = None;

src/core/model_parser.mli

@@ -56,21 +56,26 @@ val print_model_value : Format.formatter -> model_value -> unit
 ***************************************************************
 *)
 
-type model_element_type =
+type model_element_kind =
 | Result
   (* Result of a function call (if the counter-example is for postcondition)  *)
 | Old
   (* Old value of function argument (if the counter-example is for postcondition)  *)
 | Other
 
+(** Information about the name of the model element *)
+type model_element_name = {
+  men_name   : string;
+    (** The name of the source-code element.  *)
+  men_kind   : model_element_kind;
+    (** The kind of model element. *)
+}
 
 (** Counter-example model elements. Each element represents
     a counter-example for a single source-code element.*)
 type model_element = {
-  me_name     : string;
-    (** The name of the source-code element.  *)
-  me_type     : model_element_type;
-    (** The type of model element. *)
+  me_name     : model_element_name;
+    (** Information about the name of the model element  *)
   me_value    : model_value;
     (** Counter-example value for the element. *)
   me_location : Loc.position option;
@@ -116,27 +121,26 @@ val default_model : model
 *)
 
 val print_model :
-  ?me_name_trans:((string * model_element_type) -> string) ->
+  ?me_name_trans:(model_element_name -> string) ->
   Format.formatter ->
   model ->
   unit
 (** Prints the counter-example model
 
     @param me_name_trans the transformation of the model elements
-      names. The input is a pair consisting of the name of model
-      element and type of the model element. The output is the
-      name of the model element that should be displayed.
+      names. The input is information about model element name. The
+      output is the name of the model element that should be displayed.
     @param model the counter-example model to print
 *)
 
 val model_to_string :
-  ?me_name_trans:((string * model_element_type) -> string) ->
+  ?me_name_trans:(model_element_name -> string) ->
   model ->
   string
 (** See print_model  *)
 
 val print_model_vc_term :
-  ?me_name_trans: ((string * model_element_type) -> string) ->
+  ?me_name_trans: (model_element_name -> string) ->
   ?sep: string ->
   Format.formatter ->
   model ->
@@ -150,7 +154,7 @@ val print_model_vc_term :
 *)
 
 val model_vc_term_to_string :
-  ?me_name_trans: ((string * model_element_type) -> string) ->
+  ?me_name_trans: (model_element_name -> string) ->
   ?sep: string ->
   model ->
   string
@@ -160,7 +164,7 @@ val model_vc_term_to_string :
 *)
 
 val print_model_json :
-  ?me_name_trans:((string * model_element_type) -> string) ->
+  ?me_name_trans:(model_element_name -> string) ->
   Format.formatter ->
   model ->
   unit
@@ -171,7 +175,7 @@ val print_model_json :
 *)
 
 val model_to_string_json :
-  ?me_name_trans:((string * model_element_type) -> string) ->
+  ?me_name_trans:(model_element_name -> string) ->
   model ->
   string
 (** See print_model_json *)
@@ -179,7 +183,7 @@ val model_to_string_json :
 val interleave_with_source :
   ?start_comment:string ->
   ?end_comment:string ->
-  ?me_name_trans:((string * model_element_type) -> string) ->
+  ?me_name_trans:(model_element_name -> string) ->
   model ->
   filename:string ->
   source_code:string ->

src/transform/eval_match.ml

@@ -70,17 +70,15 @@ let rec add_quant kn (vl,tl,f) v =
 	    | Some pj_ls ->
 	      begin
 		try
-		  Ident.get_model_element_name ~labels:pj_ls.ls_name.id_label
+		  Ident.get_model_trace_string ~labels:pj_ls.ls_name.id_label
 		with Not_found -> pj_ls.ls_name.id_string
 	      end
 	    | _ -> ""
 	  ) in
-	  let field_str = if field_name <> "" then "." ^ field_name
-	    else "" in
+	  let field_str = if field_name = "" then "" else "." ^ field_name in
 	  let label = Ident.append_to_model_element_name
 	    ~labels:v.vs_name.id_label ~to_append:(field_str) in
 	  create_vsymbol (id_lab label v.vs_name) (ty_inst s ty) in
-
         let nvl = List.map2 mk_v ls.ls_args pjl in
         let t = fs_app ls (List.map t_var nvl) ty in
         let f = t_let_close_simp v t f in

src/transform/intro_vc_vars_counterexmp.ml

@@ -24,8 +24,10 @@ let model_label = Ident.create_label "model"
   (* 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_term_label = Ident.create_label "model_vc"
+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. *)
 let model_trace_regexp = Str.regexp "model_trace:"
   (* The term labeled with "model_trace:name" will be in counterexample with name "name" *)
 
@@ -35,9 +37,8 @@ type vc_term_info = {
   (* true if the term that triggers VC is currently processed *)
   mutable vc_loc : Loc.position option;
   (* the position of the term that triggers VC *)
-  mutable vc_func_name : string option;
-  (* the name of the function for that VC was made. None if VC
-     is not generated for postcondition or precondition) *)
+  mutable vc_pre_or_post : bool;
+  (* true if VC was generated for precondition or postcondition *)
 }
 
 let label_starts_with regexp l =
@@ -49,13 +50,8 @@ let label_starts_with regexp l =
 let get_label labels regexp =
   Slab.choose (Slab.filter (label_starts_with regexp) labels)
 
-let get_fun_name name =
-  let splitted = Str.bounded_split (Str.regexp_string ":") name 2 in
-  match splitted with
-  | _::[second] ->
-    second
-  | _ ->
-    ""
+let is_model_vc_label l = if l = model_vc_label || l = model_vc_post_label then true
+  else false
 
 let check_enter_vc_term t info =
   (* Check whether the term that triggers VC is entered.
@@ -63,22 +59,15 @@ let check_enter_vc_term t info =
      postcondition or precondition of a function, extract the name of
      the corresponding function.
   *)
-  if Slab.mem model_vc_term_label t.t_label then begin
+  if Slab.exists is_model_vc_label t.t_label then begin
     info.vc_inside <- true;
     info.vc_loc <- t.t_loc;
-    try
-      (* Label "model_func" => the VC is postcondition or precondition *)
-      (* Extract the function name from "model_func" label *)
-      let fun_label = get_label t.t_label (Str.regexp "model_func") in
-      info.vc_func_name <- Some (get_fun_name fun_label.lab_string);
-    with Not_found ->
-      (* No label "model_func" => the VC is not postcondition or precondition *)
-      ()
+    info.vc_pre_or_post <- Slab.mem model_vc_post_label t.t_label;
   end
 
 let check_exit_vc_term t info =
   (* Check whether the term triggering VC is exited. *)
-  if Slab.mem model_vc_term_label t.t_label then begin
+  if Slab.exists is_model_vc_label t.t_label then begin
     info.vc_inside <- false;
   end
 
@@ -91,12 +80,14 @@ let add_old lab_str =
     else lab_str
   with Not_found -> lab_str ^ "@old"
 
-let model_trace_for_postcondition ~labels info =
+let model_trace_for_postcondition ~labels =
   (* Modifies the  model_trace label of a term in the postcondition:
      - if term corresponds to the initial value of a function
      parameter, model_trace label will have postfix @old
      - if term corresponds to the return value of a function, add
      model_trace label in a form function_name@result
+     Returns labels with model_trace label modified if there
+     exist model_trace label in labels, labels otherwise.
   *)
   try
     let trace_label = get_label labels model_trace_regexp in
@@ -109,11 +100,7 @@ let model_trace_for_postcondition ~labels info =
 	(Ident.create_label lab_str)
 	other_labels
   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"))
-      labels
+    labels
 
 let rec do_intro info t =
   check_enter_vc_term t info;
@@ -127,20 +114,23 @@ let rec do_intro info t =
 	    match info.vc_loc with
 	    | None -> []
 	    | Some loc ->
-	      (* variable inside the term that triggers VC.
-		 Introduce new constant equal to this variable that contains
-	         all labels necessary for collecting it for counterexample*)
-	      let const_label = match info.vc_func_name with
-		| None ->
-		  ls.ls_name.id_label
-		| Some _ ->
-		  model_trace_for_postcondition ~labels:ls.ls_name.id_label info in
-	      let const_label = if (Slab.mem model_label const_label) then const_label
-		else Slab.add model_projected_label const_label in
-	      let const_name = ls.ls_name.id_string^"_vc_constant" in
-	      let axiom_name = ls.ls_name.id_string^"_vc_axiom" in
-	      Intro_projections_counterexmp.intro_const_equal_to_term
-		~term:t ~const_label ~const_loc:loc ~const_name ~axiom_name
+	      (* variable inside the term T that triggers VC.
+		 If the variable should be in counterexample, introduce new constant
+		 in location loc with all labels necessary for collecting the it for
+		 counterexample and make it equal to the variable *)
+	      let is_counterexample_label l = if
+		  l = model_label || l = model_projected_label then true else false in
+	      if Slab.exists is_counterexample_label ls.ls_name.id_label then
+		let const_label = if info.vc_pre_or_post then
+		    model_trace_for_postcondition ~labels:ls.ls_name.id_label
+		  else
+		    ls.ls_name.id_label in
+		let const_name = ls.ls_name.id_string^"_vc_constant" in
+		let axiom_name = ls.ls_name.id_string^"_vc_axiom" in
+		Intro_projections_counterexmp.intro_const_equal_to_term
+		  ~term:t ~const_label ~const_loc:loc ~const_name ~axiom_name
+	      else
+		[]
 	  end
 	  else []
 	| _ ->
@@ -180,7 +170,7 @@ let intro_vc_vars_counterexmp2 task =
   let info = {
     vc_inside = false;
     vc_loc = None;
-    vc_func_name = None;
+    vc_pre_or_post = false;
   } in
   (* Do introduction and find location of term triggering VC *)
   let do_intro_trans = Trans.goal (do_intro_vc_vars_counterexmp info) in