Commit cecd6d8c authored by David Hauzar's avatar David Hauzar

Merge branch 'counter-examples'

Conflicts:
	src/printer/smtv2.ml
parents af68079e c9df54e0
......@@ -10,12 +10,12 @@ module M
meta "inline : no" function projf
meta "model_projection" function projf
val y "model_projected" "model_trace:y" :ref int
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 }
=
#"/home/cmarche/recherche/why/tests/c/binary_search.c" 62 27 32#
(*#"/home/cmarche/recherche/why/tests/c/binary_search.c" 62 27 32#*)
y := !y + 1;
x23 := !x23 + 1;
x23 := !x23 + 1
......@@ -27,7 +27,7 @@ module M
while "model" "model_trace:cond" !x > 0 do invariant { !x >= 0 } variant { !x } x := !x - 1 done
use import map.Map
let test_map (x "model" "model_trace:x" : ref (map int int)) : unit
let test_map (x "model" : ref (map int int)) : unit
ensures { !x[0] <> !x[1] }
=
x := Map.set !x 0 3
......
This diff is collapsed.
......@@ -10,14 +10,14 @@
(********************************************************************)
(*
***************************************************************
***************************************************************
** Counter-example model values
****************************************************************
*)
type model_value =
| Integer of string
| Array of model_array
| Other of string
| Unparsed of string
and arr_index = {
arr_index_key : int;
arr_index_value : model_value;
......@@ -27,19 +27,19 @@ and model_array = {
arr_indices : arr_index list;
}
val array_create_constant :
value : model_value ->
val array_create_constant :
value : model_value ->
model_array
(** Creates constant array with all indices equal to the parameter value. *)
val array_add_element :
array : model_array ->
index : model_value ->
value : model_value ->
val array_add_element :
array : model_array ->
index : model_value ->
value : model_value ->
model_array
(** Adds an element to the array.
(** Adds an element to the array.
@param array : the array to that the element will be added
@param index : the index on which the element will be added.
Note that the index must be of value model_value.Integer
......@@ -50,15 +50,26 @@ val print_model_value : Format.formatter -> model_value -> unit
(*
***************************************************************
***************************************************************
** Model elements
***************************************************************
*)
type model_element_type =
| 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
(** Counter-example model elements. Each element represents
a counter-example for a single source-code element.*)
type model_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_value : model_value;
(** Counter-example value for the element. *)
me_location : Loc.position option;
......@@ -67,61 +78,126 @@ type model_element = {
(** Why term corresponding to the element. *)
}
val create_model_element :
name : string ->
value : model_value ->
?location : Loc.position ->
val create_model_element :
name : string ->
value : model_value ->
?location : Loc.position ->
?term : Term.term ->
unit ->
model_element
(** Creates a counter-example model element.
(** Creates a counter-example model element.
@param name : the name of the source-code element
@param value : counter-example value for the element
@param location : source-code location of the element
@param location : source-code location of the element
@param term : why term corresponding to the element *)
(*
***************************************************************
***************************************************************
** Model definitions
***************************************************************
*)
type model
*)
type model
val empty_model : model
(*
***************************************************************
***************************************************************
** Quering the model
***************************************************************
*)
val print_model : Format.formatter -> model -> unit
val print_model :
?me_name_trans:((string * model_element_type) -> 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.
@param model the counter-example model to print
*)
val model_to_string : model -> string
val model_to_string :
?me_name_trans:((string * model_element_type) -> string) ->
model ->
string
(** See print_model *)
val print_model_json : Format.formatter -> model -> unit
val print_model_json :
?me_name_trans:((string * model_element_type) -> string) ->
Format.formatter ->
model ->
unit
(** Prints counter-example model to json format.
val model_to_string_json : model -> string
@param me_name_trans see print_model
@model the counter-example model to print.
*)
val model_to_string_json :
?me_name_trans:((string * model_element_type) -> string) ->
model ->
string
(** See print_model_json *)
val interleave_with_source :
val interleave_with_source :
?start_comment:string ->
?end_comment:string ->
model ->
string ->
string ->
?me_name_trans:((string * model_element_type) -> string) ->
model ->
filename:string ->
source_code:string ->
string
(** Given a source code and a counter-example model interleaves
the source code with information in about the counter-example.
That is, for each location in counter-example trace creates
a comment in the output source code with information about
values of counter-example model elements.
@param start_comment the string that starts a comment
@param end_comment the string that ends a comment
@param me_name_trans see print_model
@param model counter-example model
@param filename the file name of the source
@param source_code the input source code
@return the source code with added comments with information
about counter-example model
*)
(*
***************************************************************
***************************************************************
** Filtering the model
***************************************************************
*)
val model_for_positions_and_decls : model ->
positions: Loc.position list -> model
(** Given a model and a list of source-code positions returns model
that contains only elements from the input model that are on these
positions plus for every file in the model, elements that are
in the positions of function declarations. Elements with other
positions are filtered out.
Assumes that for each file the element on the first line of the model
has position of function declaration.
Only filename and line number is used to identify positions.
*)
(*
***************************************************************
** Registering model parser
***************************************************************
*)
type model_parser = string -> Printer.printer_mapping -> model
(** Parses the input string into model elements, estabilishes
a mapping between these elements and mapping from printer
(** Parses the input string into model elements, estabilishes
a mapping between these elements and mapping from printer
and builds model data structure.
*)
......
......@@ -30,6 +30,7 @@ type 'a pp = Pp.formatter -> 'a -> unit
type printer_mapping = {
lsymbol_m : string -> Term.lsymbol;
vc_line : Loc.position option;
queried_terms : Term.term list;
}
......@@ -38,7 +39,7 @@ type printer_args = {
prelude : prelude;
th_prelude : prelude_map;
blacklist : blacklist;
mutable printer_mapping : printer_mapping;
mutable printer_mapping : printer_mapping;
}
type printer = printer_args -> ?old:in_channel -> task pp
......@@ -52,6 +53,7 @@ exception UnknownPrinter of string
let get_default_printer_mapping = {
lsymbol_m = (function _ -> raise Not_found);
vc_line = None;
queried_terms = [];
}
......
......@@ -28,7 +28,12 @@ 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 *)
queried_terms : Term.term list;
(* The list of terms that were queried for the counter-example
by the printer *)
}
type printer_args = {
......
......@@ -168,8 +168,9 @@ type pre_prover_call = unit -> prover_call
let save f = f ^ ".save"
let debug_print_model model =
Debug.dprintf debug "Call_provers: %s@." (Model_parser.model_to_string model)
let model_str = Model_parser.model_to_string model in
Debug.dprintf debug "Call_provers: %s@." model_str
let parse_prover_run res_parser time out ret on_timelimit timelimit ~printer_mapping =
let ans = match ret with
......
......@@ -23,16 +23,16 @@ output:
pairs:
| possible_space { [] }
| possible_space LPAREN term SPACE value RPAREN pairs
| possible_space LPAREN term SPACE value RPAREN pairs
{ (Model_parser.create_model_element ~name:$3 ~value:$5 ())::$7 }
possible_space:
| { "" }
| SPACE { $1 }
term:
| text { $1 }
| LPAREN term_list RPAREN
| LPAREN term_list RPAREN
{ "(" ^ $2 ^ ")" }
term_list:
......@@ -52,25 +52,25 @@ text_without_int:
value:
| integer { $1 }
| other_val_str { Model_parser.Other $1 }
| other_val_str { Model_parser.Unparsed $1 }
| array { Model_parser.Array $1 }
integer:
| INT_STR { Model_parser.Integer $1 }
| LPAREN possible_space MINUS_INT_STR possible_space RPAREN
| LPAREN possible_space MINUS_INT_STR possible_space RPAREN
{ Model_parser.Integer $3 }
(* Everything that cannot be integer (positive and negative) and array. *)
other_val_str:
| text_without_int { $1 }
| LPAREN possible_space RPAREN { "(" ^ $2 ^ ")" }
| LPAREN possible_space paren_other_val_str RPAREN
| LPAREN possible_space paren_other_val_str RPAREN
{ "(" ^ $3 ^ ")" }
(* Everything that cannot be negative integer and start of an array *)
paren_other_val_str:
| other_than_neg_int_and_array_store term_list { $1 ^ $2 }
| LPAREN possible_space other_than_const_array possible_space RPAREN
| LPAREN possible_space other_than_const_array possible_space RPAREN
{ "(" ^ $3 ^ ")" }
other_than_neg_int_and_array_store:
......@@ -87,19 +87,18 @@ other_than_const_array:
(* Example:
(store (store ((as const (Array Int Int)) 0) 1 2) 3 4) *)
array:
| LPAREN possible_space
LPAREN possible_space
AS SPACE CONST possible_space array_skipped_part possible_space
RPAREN possible_space
integer possible_space
RPAREN
| LPAREN possible_space
LPAREN possible_space
AS SPACE CONST possible_space array_skipped_part possible_space
RPAREN possible_space
integer possible_space
RPAREN
{ Model_parser.array_create_constant ~value:$13 }
| LPAREN possible_space
| LPAREN possible_space
STORE possible_space array possible_space integer SPACE integer
possible_space
RPAREN
possible_space
RPAREN
{ Model_parser.array_add_element ~array:$5 ~index:$7 ~value:$9 }
array_skipped_part:
| LPAREN term_list RPAREN {}
......@@ -175,6 +175,8 @@ type main = {
(* max number of running prover processes *)
plugins : string list;
(* plugins to load, without extension, relative to [libdir]/plugins *)
cntexample : bool;
(* true provers should be asked for counter-example model *)
}
let libdir m =
......@@ -203,6 +205,7 @@ let loadpath m =
let timelimit m = m.timelimit
let memlimit m = m.memlimit
let running_provers_max m = m.running_provers_max
let cntexample m = m.cntexample
exception StepsCommandNotSpecified of string
......@@ -219,6 +222,9 @@ let get_complete_command pc steplimit =
let set_limits m time mem running =
{ m with timelimit = time; memlimit = mem; running_provers_max = running }
let set_cntexample m cntexample =
{ m with cntexample = cntexample }
let plugins m = m.plugins
let set_plugins m pl =
(* TODO : sanitize? *)
......@@ -258,6 +264,7 @@ let empty_main =
memlimit = 1000; (* 1 Mb *)
running_provers_max = 2; (* two provers run in parallel *)
plugins = [];
cntexample = true;
}
let default_main =
......@@ -276,6 +283,7 @@ let set_main rc main =
let section =
set_int section "running_provers_max" main.running_provers_max in
let section = set_stringl section "plugin" main.plugins in
let section = set_bool section "cntexample" main.cntexample in
set_section rc "main" section
exception NonUniqueId
......@@ -509,6 +517,7 @@ let load_main dirname section =
running_provers_max = get_int ~default:default_main.running_provers_max
section "running_provers_max";
plugins = get_stringl ~default:[] section "plugin";
cntexample = get_bool ~default:default_main.cntexample section "cntexample"
}
let read_config_rc conf_file =
......
......@@ -75,7 +75,9 @@ val loadpath: main -> string list
val timelimit: main -> int
val memlimit: main -> int
val running_provers_max: main -> int
val cntexample: main -> bool
val set_limits: main -> int -> int -> int -> main
val set_cntexample: main -> bool -> main
val plugins : main -> string list
val pluginsdir : main -> string
......
......@@ -61,6 +61,7 @@ type t =
mutable session_time_limit : int;
mutable session_mem_limit : int;
mutable session_nb_processes : int;
mutable session_cntexample : bool;
}
......@@ -210,6 +211,7 @@ let load_config config original_config env =
session_time_limit = Whyconf.timelimit main;
session_mem_limit = Whyconf.memlimit main;
session_nb_processes = Whyconf.running_provers_max main;
session_cntexample = Whyconf.cntexample main;
}
let save_config t =
......@@ -222,6 +224,9 @@ let save_config t =
let mem = Whyconf.memlimit new_main in
let nb = Whyconf.running_provers_max new_main in
let config = set_main config (set_limits (get_main config) time mem nb) in
let new_main = Whyconf.get_main t.config in
let cntexample = Whyconf.cntexample new_main in
let config = set_main config (set_cntexample (get_main config) cntexample) in
(* copy also provers section since it may have changed (the editor
can be set via the preferences dialog) *)
let config = set_provers config (get_provers t.config) in
......@@ -628,6 +633,15 @@ let general_settings (c : t) (notebook:GPack.notebook) =
nb_processes_spin#connect#value_changed ~callback:
(fun () -> c.session_nb_processes <- nb_processes_spin#value_as_int)
in
(* counter-example *)
let cntexample_check = GButton.check_button ~label:"get counter-example"
~packing:vb#add ()
~active:c.session_cntexample
in
let (_: GtkSignal.id) =
cntexample_check#connect#toggled ~callback:
(fun () -> c.session_cntexample <- not c.session_cntexample)
in
(* session saving policy *)
let set_saving_policy n () = c.saving_policy <- n in
let saving_policy_frame =
......@@ -1046,6 +1060,9 @@ let preferences (c : t) =
c.config <- Whyconf.set_main c.config
(Whyconf.set_limits (Whyconf.get_main c.config)
c.session_time_limit c.session_mem_limit c.session_nb_processes);
c.config <- Whyconf.set_main c.config
(Whyconf.set_cntexample (Whyconf.get_main c.config)
c.session_cntexample);
save_config ()
| `CLOSE | `DELETE_EVENT -> ()
end;
......
......@@ -40,6 +40,7 @@ type t =
mutable session_time_limit : int;
mutable session_mem_limit : int;
mutable session_nb_processes : int;
mutable session_cntexample : bool;
}
val load_config : Whyconf.config -> Whyconf.config -> Why3.Env.env -> unit
......
......@@ -39,15 +39,12 @@ let debug = Debug.lookup_flag "ide_info"
let files = Queue.create ()
let opt_parser = ref None
let opt_cntexmp = ref false
let spec = Arg.align [
"-F", Arg.String (fun s -> opt_parser := Some s),
"<format> select input format (default: \"why\")";
"--format", Arg.String (fun s -> opt_parser := Some s),
" same as -F";
"--get-ce", Arg.Set opt_cntexmp,
" gets the counter-example model";
(*
"-f",
Arg.String (fun s -> input_files := s :: !input_files),
......@@ -646,12 +643,10 @@ let update_tabs a =
match a.S.proof_state with
| S.Done r ->
if r.Call_provers.pr_model <> Model_parser.empty_model then begin
Model_parser.model_to_string r.Call_provers.pr_model ^ "\n" ^
Model_parser.model_to_string_json r.Call_provers.pr_model ^ "\n\n" ^
(Model_parser.interleave_with_source
r.Call_provers.pr_model
!current_file
(Sysutil.file_contents !current_file))
Model_parser.interleave_with_source
r.Call_provers.pr_model
~filename:!current_file
~source_code:(Sysutil.file_contents !current_file)
end else
""
| _ -> ""
......@@ -994,6 +989,7 @@ let () = Queue.iter (open_file ~start:true) files
let prover_on_selected_goals pr =
let timelimit = gconfig.session_time_limit in
let memlimit = gconfig.session_mem_limit in
let cntexample = Whyconf.cntexample (Whyconf.get_main gconfig.config) in
List.iter
(fun row ->
try
......@@ -1001,7 +997,7 @@ let prover_on_selected_goals pr =
M.run_prover
(env_session()) sched
~context_unproved_goals_only:!context_unproved_goals_only
~cntexample:!opt_cntexmp ~timelimit ~memlimit
~cntexample ~timelimit ~memlimit
pr a
with e ->
eprintf "@[Exception raised while running a prover:@ %a@.@]"
......@@ -1076,6 +1072,7 @@ let bisect_proof_attempt pa =
let timelimit = ref (-1) in
let set_timelimit res =
timelimit := 1 + (int_of_float (floor res.Call_provers.pr_time)) in
let cntexample = Whyconf.cntexample (Whyconf.get_main gconfig.config) in
let rec callback lp pa c = function
| S.Running | S.Scheduled -> ()
| S.Interrupted ->
......@@ -1107,14 +1104,14 @@ let bisect_proof_attempt pa =
let npa = S.copy_external_proof ~notify ~keygen ~obsolete:true
~goal ~env_session:eS pa in
MA.init_any (S.Metas metas);
M.run_external_proof eS sched ~cntexample:!opt_cntexmp npa
M.run_external_proof eS sched ~cntexample npa
with e ->
dprintf debug "Bisecting error:@\n%a@."
Exn_printer.exn_printer e end
| Eliminate_definition.BSstep (t,c) ->
assert (not lp.S.prover_config.C.in_place); (* TODO do this case *)
M.schedule_proof_attempt
~cntexample:!opt_cntexmp
~cntexample
~timelimit:!timelimit
~memlimit:pa.S.proof_memlimit
~steplimit:(-1)
......@@ -1153,7 +1150,7 @@ let bisect_proof_attempt pa =
dprintf debug "Prover can't be loaded.@."
| Some lp ->
M.schedule_proof_attempt
~cntexample:!opt_cntexmp
~cntexample
~timelimit:!timelimit
~memlimit:pa.S.proof_memlimit
~steplimit:(-1)
......@@ -1164,7 +1161,7 @@ let bisect_proof_attempt pa =
~callback:(callback lp pa c) sched t in
dprintf debug "Bisecting with %a started.@."
C.print_prover pa.S.proof_prover;
M.run_external_proof eS sched ~cntexample:!opt_cntexmp ~callback:first_callback pa
M.run_external_proof eS sched ~cntexample ~callback:first_callback pa
let apply_bisect_on_selection () =
List.iter
......@@ -2131,6 +2128,7 @@ let edit_selected_row r =
()
| S.Proof_attempt a ->
let e = env_session () in
let cntexample = Whyconf.cntexample (Whyconf.get_main gconfig.config) in
(*
let coq = { prover_name = "Coq" ; prover_version = "8.3pl3";
prover_altern = "" } in
......@@ -2141,7 +2139,7 @@ let edit_selected_row r =
"[debug] save_config %d: timelimit=%d ; editor for Coq=%s@."
0 time p.editor;
*)
M.edit_proof ~cntexample:!opt_cntexmp e sched ~default_editor:gconfig.default_editor a
M.edit_proof ~cntexample e sched ~default_editor:gconfig.default_editor a
| S.Transf _ -> ()
| S.Metas _ -> ()
......
......@@ -35,7 +35,48 @@ end
let floc s e = Loc.extract (s,e)
let add_lab id l = { id with id_lab = l }
let model_label = Ident.create_label "model"
let is_model_label l =
match l with
| Lpos _ -> false
| Lstr lab ->
lab = model_label
let model_lab_present labels =
try
ignore(List.find is_model_label labels);
true
with Not_found ->
false
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 =
try
ignore(List.find is_model_trace_label labels);
true
with Not_found ->
false
let add_model_trace name labels =
if (model_lab_present labels) && (not (model_trace_lab_present labels)) then
(Lstr (Ident.create_label ("model_trace:" ^ name)))::labels
else
labels
let add_lab id l =
let l = add_model_trace id.id_str l in
{ id with id_lab = l }
let id_anonymous loc = { id_str = "_"; id_lab = []; id_loc = loc }
......
......@@ -80,10 +80,32 @@ 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 = {
mutable vc_inside : bool;
(* true if the term corresponding to VC line is currently processed *)
mutable vc_loc : Loc.position option;
(* the position of VC line *)
mutable vc_func_name : string option;
(* the name of the function. None if VC is not generated for
postcondition or precondition) *)
}
let vc_line_info = { vc_inside = false; vc_loc = None; vc_func_name = None }
module TermCmp = struct
type t = term
let compare a b =
if (a.t_loc = b.t_loc) && (a.t_label = b.t_label)
then 0 else 1
end
module S = Set.Make(TermCmp)
type info = {
info_syn : syntax_map;
info_converters : converter_map;
mutable info_model : term list;
mutable info_model : S.t;
}
let debug_print_term message t =
......@@ -128,21 +150,101 @@ 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"
let collect_model_ls info ls =
if ls.ls_args = [] && Slab.mem model_label ls.ls_name.id_label then
let t = t_app ls [] ls.ls_value in
info.info_model <-