Commit 34f1ba18 authored by David Hauzar's avatar David Hauzar

Merge branch 'counter-examples'

parents c960adbd bf7ec1d7
......@@ -13,7 +13,7 @@ module M
val y "model_projected" "model" "model_trace:y" :ref int
let incr ( x23 "model" "model_trace:x23" : ref int ): unit
ensures { !x23 = old !x23 + 2 + !y }
ensures { "model_vc" "model_func" !x23 = old !x23 + 2 + !y }
=
(*#"/home/cmarche/recherche/why/tests/c/binary_search.c" 62 27 32#*)
y := !y + 1;
......@@ -30,13 +30,13 @@ module M
let test_map (x "model" : ref (map int int)) : unit
ensures { !x[0] <> !x[1] }
=
x := Map.set !x 0 3
x := Map.set !x 0 3
type r = {f:int; g:bool}
let test_record (x "model" "model_trace:x" : ref r) : unit
ensures { !x.g }
=
x := { !x with f = 6}
x := { !x with f = 6}
end
\ No newline at end of file
end
......@@ -144,10 +144,20 @@ module IntMap = Map.Make(struct type t = int let compare = compare end)
module StringMap = Map.Make(String)
type model_file = model_element list IntMap.t
type model = model_file StringMap.t
type model_files = model_file StringMap.t
type model = {
vc_term_loc : Loc.position option;
model_files : model_files;
}
let empty_model = StringMap.empty
let empty_model_file = IntMap.empty
let is_model_empty model =
model.model_files = empty_model
let default_model = {
vc_term_loc = None;
model_files = empty_model;
}
type model_parser = string -> Printer.printer_mapping -> model
......@@ -184,7 +194,7 @@ let print_model
?(me_name_trans = why_name_trans)
fmt
model =
StringMap.iter (print_model_file fmt me_name_trans) model
StringMap.iter (print_model_file fmt me_name_trans) model.model_files
let model_to_string
?(me_name_trans = why_name_trans)
......@@ -204,6 +214,26 @@ let get_elements model_file line_number =
with Not_found ->
[]
let print_model_vc_term
?(me_name_trans = why_name_trans)
?(sep = "\n")
fmt
model =
match model.vc_term_loc with
| None -> ()
| Some pos ->
let (filename, line_number, _, _) = Loc.get pos in
let model_file = get_model_file model.model_files filename in
let model_elements = get_elements model_file line_number in
print_model_elements ~sep me_name_trans fmt model_elements
let model_vc_term_to_string
?(me_name_trans = why_name_trans)
?(sep = "\n")
model =
print_model_vc_term ~me_name_trans ~sep str_formatter model;
flush_str_formatter ()
let get_padding line =
try
let r = Str.regexp " *" in
......@@ -240,7 +270,7 @@ let interleave_with_source
~filename
~source_code =
try
let model_file = StringMap.find filename model in
let model_file = StringMap.find filename model.model_files in
let lines = Str.split (Str.regexp "^") source_code in
let (source_code, _) = List.fold_left
(interleave_line
......@@ -290,7 +320,7 @@ let print_model_json
(fun s -> s)
(print_model_elements_on_lines_json me_name_to_str)
fmt
(StringMap.bindings model)
(StringMap.bindings model.model_files)
let model_to_string_json
?(me_name_trans = why_name_trans)
......@@ -359,9 +389,12 @@ match raw_model with
terms_tail
model
let build_model raw_model printer_mapping =
build_model_rec raw_model printer_mapping.queried_terms empty_model
let model_files = build_model_rec raw_model printer_mapping.queried_terms empty_model in
{
vc_term_loc = printer_mapping.Printer.vc_term_loc;
model_files = model_files;
}
(*
......@@ -399,11 +432,13 @@ let add_first_model_line filename model_file model =
let model_for_positions_and_decls model ~positions =
(* Start with empty model and add locations from model that
are in locations *)
let model_filtered = List.fold_left (add_loc model) empty_model positions in
let model_filtered = List.fold_left (add_loc model.model_files) empty_model positions in
(* For each file add mapping corresponding to the first line of the
counter-example from model to model_filtered.
This corresponds to function declarations *)
StringMap.fold add_first_model_line model model_filtered
let model_filtered = StringMap.fold add_first_model_line model.model_files model_filtered in
{ vc_term_loc = model.vc_term_loc;
model_files = model_filtered }
(*
......
......@@ -101,7 +101,8 @@ val create_model_element :
*)
type model
val empty_model : model
val is_model_empty : model -> bool
val default_model : model
(*
***************************************************************
......@@ -129,6 +130,30 @@ val model_to_string :
string
(** See print_model *)
val print_model_vc_term :
?me_name_trans: ((string * model_element_type) -> string) ->
?sep: string ->
Format.formatter ->
model ->
unit
(** Prints counter-example model elements related to term that
triggers VC.
@param sep separator of counter-example model elements
@param me_name_trans see print_model
@model the counter-example model.
*)
val model_vc_term_to_string :
?me_name_trans: ((string * model_element_type) -> string) ->
?sep: string ->
model ->
string
(** Gets string with counter-example model elements related to term that
triggers VC.
See print_model_vc_term
*)
val print_model_json :
?me_name_trans:((string * model_element_type) -> string) ->
Format.formatter ->
......
......@@ -30,7 +30,7 @@ type 'a pp = Pp.formatter -> 'a -> unit
type printer_mapping = {
lsymbol_m : string -> Term.lsymbol;
vc_line : Loc.position option;
vc_term_loc : Loc.position option;
queried_terms : Term.term list;
}
......@@ -53,7 +53,7 @@ exception UnknownPrinter of string
let get_default_printer_mapping = {
lsymbol_m = (function _ -> raise Not_found);
vc_line = None;
vc_term_loc = None;
queried_terms = [];
}
......
......@@ -28,9 +28,8 @@ type 'a pp = Format.formatter -> 'a -> unit
in the output of the printer to elements of AST in its input. *)
type printer_mapping = {
lsymbol_m : string -> Term.lsymbol;
vc_line : Loc.position option;
(* The position of the term corresponding to the line in the program
for that the VC was made *)
vc_term_loc : Loc.position option;
(* The position of the term that triggers the VC *)
queried_terms : Term.term list;
(* The list of terms that were queried for the counter-example
by the printer *)
......
......@@ -135,7 +135,7 @@ let print_steps fmt s =
let print_prover_result fmt
{pr_answer=ans; pr_status=status; pr_output=out; pr_time=t; pr_steps=s; pr_model=m} =
fprintf fmt "%a (%.2fs%a)" print_prover_answer ans t print_steps s;
if m <> Model_parser.empty_model then begin
if Model_parser.is_model_empty m then begin
fprintf fmt "\nCounter-example model:";
Model_parser.print_model fmt m
end;
......
......@@ -642,7 +642,7 @@ let update_tabs a =
begin
match a.S.proof_state with
| S.Done r ->
if r.Call_provers.pr_model <> Model_parser.empty_model then begin
if Model_parser.is_model_empty r.Call_provers.pr_model then begin
Model_parser.interleave_with_source
r.Call_provers.pr_model
~filename:!current_file
......
......@@ -80,18 +80,18 @@ let ident_printer =
let print_ident fmt id =
fprintf fmt "%s" (id_unique ident_printer id)
(* Information about the line in the program for that the VC was made *)
type vc_line_info = {
(* Information about the term that triggers VC. *)
type vc_term_info = {
mutable vc_inside : bool;
(* true if the term corresponding to VC line is currently processed *)
(* true if the term that triggers VC is currently processed *)
mutable vc_loc : Loc.position option;
(* the position of VC line *)
(* the position of the term that triggers VC *)
mutable vc_func_name : string option;
(* the name of the function. None if VC is not generated for
postcondition or precondition) *)
(* the name of the function for that VC was made. None if VC
is not generated for postcondition or precondition) *)
}
let vc_line_info = { vc_inside = false; vc_loc = None; vc_func_name = None }
let vc_term_info = { vc_inside = false; vc_loc = None; vc_func_name = None }
module TermCmp = struct
type t = term
......@@ -150,7 +150,9 @@ let print_var_list info fmt vsl =
print_list space (print_typed_var info) fmt vsl
let model_label = Ident.create_label "model"
let model_vc_line_label = Ident.create_label "model_vc"
(* 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 collect_model_ls info ls =
if ls.ls_args = [] && Slab.mem model_label ls.ls_name.id_label then
......@@ -160,6 +162,7 @@ let collect_model_ls info ls =
(t_label ?loc:ls.ls_name.id_loc ls.ls_name.id_label t) info.info_model
let model_trace_regexp = Str.regexp "model_trace:"
(* The term labeled with "model_trace:name" will be in counter-example with name "name" *)
let label_starts_with regexp l =
try
......@@ -200,7 +203,7 @@ let model_trace_for_postcondition ~labels =
(* no model_trace label => the term represents the return value *)
Slab.add
(Ident.create_label
("model_trace:" ^ (Opt.get_def "" vc_line_info.vc_func_name) ^ "@result"))
("model_trace:" ^ (Opt.get_def "" vc_term_info.vc_func_name) ^ "@result"))
labels
let get_fun_name name =
......@@ -211,28 +214,29 @@ let get_fun_name name =
| _ ->
""
let check_enter_vc_line t =
(* Check whether the term corresponding to the line of VC is entered.
If it is entered, extract the location of VC line and if the VC is
postcondition or precondition of a function , extract the name of
the function.
let check_enter_vc_term t =
(* Check whether the term that triggers VC is entered.
If it is entered, extract the location of the term and if the VC is
postcondition or precondition of a function, extract the name of
the corresponding function.
*)
if Slab.mem model_vc_line_label t.t_label then begin
vc_line_info.vc_inside <- true;
vc_line_info.vc_loc <- t.t_loc;
if Slab.mem model_vc_term_label t.t_label then begin
vc_term_info.vc_inside <- true;
vc_term_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
vc_line_info.vc_func_name <- Some (get_fun_name fun_label.lab_string);
vc_term_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 *)
()
end
let check_exit_vc_line t =
(* Check whether the term corresponding to the line of VC is exited. *)
if Slab.mem model_vc_line_label t.t_label then begin
vc_line_info.vc_inside <- false;
let check_exit_vc_term t =
(* Check whether the term triggering VC is exited. *)
if Slab.mem model_vc_term_label t.t_label then begin
vc_term_info.vc_inside <- false;
end
(** expr *)
......@@ -242,7 +246,7 @@ let rec print_term info fmt t =
if Slab.mem model_label t.t_label then
info.info_model <- S.add t info.info_model;
check_enter_vc_line t;
check_enter_vc_term t;
let () = match t.t_node with
| Tconst c ->
......@@ -279,11 +283,11 @@ 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 ) *)
| [] ->
if vc_line_info.vc_inside then begin
match vc_line_info.vc_loc with
if vc_term_info.vc_inside then begin
match vc_term_info.vc_loc with
| None -> ()
| Some loc ->
let labels = match vc_line_info.vc_func_name with
let labels = match vc_term_info.vc_func_name with
| None ->
ls.ls_name.id_label
| Some _ ->
......@@ -325,7 +329,7 @@ let rec print_term info fmt t =
| Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
in
check_exit_vc_line t;
check_exit_vc_term t;
and print_fmla info fmt f =
......@@ -333,7 +337,7 @@ and print_fmla info fmt f =
if Slab.mem model_label f.t_label then
info.info_model <- S.add f info.info_model;
check_enter_vc_line f;
check_enter_vc_term f;
let () = match f.t_node with
| Tapp ({ ls_name = id }, []) ->
......@@ -404,7 +408,7 @@ and print_fmla info fmt f =
end
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f) in
check_exit_vc_line f
check_exit_vc_term f
and print_boolean_branches info subject pr fmt bl =
let error () = unsupportedTerm subject
......@@ -530,7 +534,7 @@ let print_prop_decl cntexample args info fmt k pr f = match k with
print_info_model cntexample fmt model_list info;
args.printer_mapping <- { lsymbol_m = args.printer_mapping.lsymbol_m;
vc_line = vc_line_info.vc_loc;
vc_term_loc = vc_term_info.vc_loc;
queried_terms = model_list; }
| Plemma| Pskip -> assert false
......
......@@ -1194,7 +1194,7 @@ let load_result r =
Call_provers.pr_output = "";
Call_provers.pr_status = Unix.WEXITED 0;
Call_provers.pr_steps = steps;
Call_provers.pr_model = Model_parser.empty_model
Call_provers.pr_model = Model_parser.default_model
}
| "undone" -> Interrupted
| "unedited" -> Unedited
......
......@@ -294,7 +294,7 @@ let schedule_edition t command filename callback =
Call_provers.prp_regexps = [];
Call_provers.prp_timeregexps = [];
Call_provers.prp_stepregexps = [];
Call_provers.prp_model_parser = fun _ _ -> Model_parser.empty_model
Call_provers.prp_model_parser = fun _ _ -> Model_parser.default_model
} in
let precall =
Call_provers.call_on_file ~command ~res_parser ~redirect:false filename ~printer_mapping:Printer.get_default_printer_mapping in
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment