Commit a5d0aa0b authored by Sylvain Dailler's avatar Sylvain Dailler

Why3 altergo counterex - Allowing values to be printed for Altergo

We added the generation of identifiers for counterex values inside the
printer of altergo.
Also added a file to factorize counterex printing functions that are used
for both altergo and smtv2.

* Makefile.in
(cntexmp_printer): Factorization file added to Makefile.

* src/driver/parse_smtv2_model_lexer.mll
(MODEL): Adding model keyword.

* src/driver/parse_smtv2_model_parser.mly
(output): Added parsing when keyword model is at beginning of the
 output of the prover.

* src/printer/alt_ergo.ml
Adding info mimicking smtv2.ml inside most printing functions for counterex
generation.

* src/printer/cntexmp_printer.ml
Common functions to alt_ergo.ml and smtv2.ml

* src/printer/smtv2.ml
Removed functions that are factorized into cntexmp_printer.ml
parent 219c8bb3
......@@ -195,7 +195,7 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \
eval_match instantiate_predicate smoke_detector \
induction_pr prop_curry
LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs isabelle \
LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 coq pvs isabelle \
simplify gappa cvc3 yices mathematica
LIB_WHYML = mlw_ty mlw_expr mlw_decl mlw_pretty mlw_wp mlw_module \
......
......@@ -27,6 +27,7 @@ rule token = parse
| "mk_t__ref"(num*) { MK_T_REF }
| "store" { STORE }
| "const" { CONST }
| "model" {MODEL}
| "as" { AS }
| '('
{ LPAREN }
......
......@@ -15,6 +15,7 @@
%start <Model_parser.model_element list> output
%token <string> SPACE
%token <string> ATOM
%token MODEL
%token STORE
%token CONST
%token AS
......@@ -29,6 +30,10 @@
%%
output:
| possible_space LPAREN MODEL output1 RPAREN {$4}
| output1 {$1}
output1:
| EOF { [] }
| possible_space text { [] }
| possible_space LPAREN text { [] }
......
......@@ -18,6 +18,7 @@ open Ty
open Term
open Decl
open Printer
open Cntexmp_printer
let meta_ac = Theory.register_meta "AC" [Theory.MTlsymbol]
~desc:"Specify@ that@ a@ symbol@ is@ associative@ and@ commutative."
......@@ -40,7 +41,10 @@ type info = {
info_axs : Spr.t;
info_inv_trig : Sls.t;
info_printer : ident_printer;
}
mutable info_model: S.t;
info_vc_term: vc_term_info;
mutable info_in_goal: bool;
}
let ident_printer () =
let bls = [
......@@ -59,9 +63,6 @@ let ident_printer () =
let print_ident info fmt id =
fprintf fmt "%s" (id_unique info.info_printer id)
let print_label fmt l =
fprintf fmt "\"%s\"" l.lab_string
let print_ident_label info fmt id =
if info.info_show_labels then
fprintf fmt "%s %a"
......@@ -72,6 +73,13 @@ let print_ident_label info fmt id =
let forget_var info v = forget_id info.info_printer v.vs_name
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 <-
add_model_element
(t_label ?loc:ls.ls_name.id_loc ls.ls_name.id_label t) info.info_model
(*
let tv_printer =
let san = sanitizer char_to_lalpha char_to_alnumus in
......@@ -120,7 +128,13 @@ let unambig_fs fs =
in
inspect (Opt.get fs.ls_value)
let rec print_term info fmt t = match t.t_node with
let rec print_term info fmt t =
if Slab.mem model_label t.t_label then
info.info_model <- add_model_element t info.info_model;
check_enter_vc_term t info.info_in_goal info.info_vc_term;
let () = match t.t_node with
| Tconst c ->
let number_format = {
Number.long_int_support = true;
......@@ -138,21 +152,51 @@ let rec print_term info fmt t = match t.t_node with
Number.print number_format fmt c
| Tvar { vs_name = id } ->
print_ident info fmt id
| Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
| Tapp (ls, tl) -> begin
(match query_syntax info.info_syn ls.ls_name with
| Some s -> syntax_arguments s (print_term info) fmt tl
| None when Mls.mem ls info.info_csm ->
| None ->
begin
if (tl = []) then
begin
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 labels = match vc_term_info.vc_func_name with
| None ->
ls.ls_name.id_label
| Some _ ->
model_trace_for_postcondition ~labels:ls.ls_name.id_label info.info_vc_term in
let _t_check_pos = t_label ~loc labels t in
(* TODO: temporarily disable collecting variables inside the term triggering VC *)
(*info.info_model <- add_model_element t_check_pos info.info_model;*)
()
end
end;
end;
if (Mls.mem ls info.info_csm) then
begin
let print_field fmt ({ls_name = id},t) =
fprintf fmt "%a =@ %a" (print_ident info) id (print_term info) t in
fprintf fmt "{@ %a@ }" (print_list semi print_field)
(List.combine (Mls.find ls info.info_csm) tl)
| None when Sls.mem ls info.info_pjs ->
end
else if (Sls.mem ls info.info_pjs) then
begin
fprintf fmt "%a.%a" (print_tapp info) tl (print_ident info) ls.ls_name
| None when unambig_fs ls || not info.info_type_casts ->
end
else if (unambig_fs ls || not info.info_type_casts) then
begin
fprintf fmt "%a%a" (print_ident info) ls.ls_name (print_tapp info) tl
| None ->
end
else
begin
fprintf fmt "(%a%a : %a)" (print_ident info) ls.ls_name
(print_tapp info) tl (print_type info) (t_type t)
end
) end
| Tlet _ -> unsupportedTerm t
"alt-ergo : you must eliminate let in term"
| Tif _ -> unsupportedTerm t
......@@ -162,13 +206,21 @@ let rec print_term info fmt t = match t.t_node with
| Teps _ -> unsupportedTerm t
"alt-ergo : you must eliminate epsilon"
| Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
in
check_exit_vc_term t info.info_in_goal info.info_vc_term;
and print_tapp info fmt = function
| [] -> ()
| tl -> fprintf fmt "(%a)" (print_list comma (print_term info)) tl
let rec print_fmla info fmt f =
if info.info_show_labels then
if Slab.mem model_label f.t_label then
info.info_model <- add_model_element f info.info_model;
check_enter_vc_term f info.info_in_goal info.info_vc_term;
let () = if info.info_show_labels then
match Slab.elements f.t_label with
| [] -> print_fmla_node info fmt f
| l ->
......@@ -177,6 +229,8 @@ let rec print_fmla info fmt f =
(print_fmla_node info) f
else
print_fmla_node info fmt f
in
check_exit_vc_term f info.info_in_goal info.info_vc_term
and print_fmla_node info fmt f = match f.t_node with
| Tapp ({ ls_name = id }, []) ->
......@@ -289,6 +343,7 @@ let print_param_decl info fmt ls =
then () else (print_param_decl info fmt ls; forget_tvs info)
let print_logic_decl info fmt ls ld =
collect_model_ls info ls;
let vl,e = open_ls_defn ld in
begin match e.t_ty with
| Some _ ->
......@@ -310,31 +365,58 @@ let print_logic_decl info fmt (ls,ld) =
if Mid.mem ls.ls_name info.info_syn || Sls.mem ls info.info_pjs
then () else (print_logic_decl info fmt ls ld; forget_tvs info)
let print_prop_decl info fmt k pr f = match k with
let print_info_model cntexample info =
(* Prints the content of info.info_model *)
let info_model = info.info_model in
if not (S.is_empty info_model) && cntexample then
begin
let model_map =
S.fold (fun f acc ->
fprintf str_formatter "%a" (print_fmla info) f;
let s = flush_str_formatter () in
Stdlib.Mstr.add s f acc)
info_model
Stdlib.Mstr.empty in ();
(* Printing model has modification of info.info_model as undesirable
side-effect. Revert it back. *)
info.info_model <- info_model;
model_map
end
else
Stdlib.Mstr.empty
let print_prop_decl vc_loc cntexample args info fmt k pr f =
match k with
| Paxiom ->
fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n@\n"
(print_ident info) pr.pr_name (print_fmla info) f
| Pgoal ->
let model_list = print_info_model cntexample info in
args.printer_mapping <- { lsymbol_m = args.printer_mapping.lsymbol_m;
vc_term_loc = vc_loc;
queried_terms = model_list; };
fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n"
(print_ident info) pr.pr_name (print_fmla info) f
| Plemma| Pskip -> assert false
let print_prop_decl info fmt k pr f =
let print_prop_decl vc_loc cntexample args info fmt k pr f =
if Mid.mem pr.pr_name info.info_syn || Spr.mem pr info.info_axs
then () else (print_prop_decl info fmt k pr f; forget_tvs info)
then () else (print_prop_decl vc_loc cntexample args info fmt k pr f; forget_tvs info)
let print_decl info fmt d = match d.d_node with
let print_decl vc_loc cntexample args info fmt d = match d.d_node with
| Dtype ts ->
print_ty_decl info fmt ts
| Ddata dl ->
print_list nothing (print_data_decl info) fmt dl
| Dparam ls ->
collect_model_ls info ls;
print_param_decl info fmt ls
| Dlogic dl ->
print_list nothing (print_logic_decl info) fmt dl
| Dind _ -> unsupportedDecl d
"alt-ergo: inductive definitions are not supported"
| Dprop (k,pr,f) -> print_prop_decl info fmt k pr f
| Dprop (k,pr,f) -> print_prop_decl vc_loc cntexample args info fmt k pr f
let add_projection (csm,pjs,axs) = function
| [Theory.MAls ls; Theory.MAls cs; Theory.MAint ind; Theory.MApr pr] ->
......@@ -351,13 +433,14 @@ let check_options ((show,cast) as acc) = function
| _ -> assert false
let print_task args ?old:_ fmt task =
print_prelude fmt args.prelude;
print_th_prelude task fmt args.th_prelude;
let csm,pjs,axs = Task.on_meta Eliminate_algebraic.meta_proj
add_projection (Mls.empty,Sls.empty,Spr.empty) task in
let inv_trig = Task.on_tagged_ls meta_invalid_trigger task in
let show,cast = Task.on_meta meta_printer_option
check_options (false,true) task in
let cntexample = Prepare_for_counterexmp.get_counterexmp task in
let vc_loc = Intro_vc_vars_counterexmp.get_location_of_vc task in
let vc_info = {vc_inside = false; vc_loc = None; vc_func_name = None} in
let info = {
info_syn = Discriminate.get_syntax_map task;
info_ac = Task.on_tagged_ls meta_ac task;
......@@ -367,13 +450,18 @@ let print_task args ?old:_ fmt task =
info_pjs = pjs;
info_axs = axs;
info_inv_trig = Sls.add ps_equ inv_trig;
info_printer = ident_printer () } in
info_printer = ident_printer ();
info_model = S.empty;
info_vc_term = vc_info;
info_in_goal = false;} in
print_prelude fmt args.prelude;
print_th_prelude task fmt args.th_prelude;
let rec print_decls = function
| Some t ->
print_decls t.Task.task_prev;
begin match t.Task.task_decl.Theory.td_node with
| Theory.Decl d ->
begin try print_decl info fmt d
begin try print_decl vc_loc cntexample args info fmt d
with Unsupported s -> raise (UnsupportedDecl (d,s)) end
| _ -> () end
| None -> () in
......
open Format
open Ident
open Term
(* Information about the term that triggers VC. *)
type vc_term_info = {
mutable vc_inside : bool;
(* 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) *)
}
module TermCmp = struct
type t = term
let before loc1 loc2 =
(* Return true if loc1 is strictly before loc2 *)
match loc1 with
| None -> false
| Some loc1 ->
match loc2 with
| None -> false
| Some loc2 ->
let (_, line1, col1, _) = Loc.get loc1 in
let (_, line2, col2, _) = Loc.get loc2 in
if line1 <> line2 then
if line1 < line2 then true
else false
else
if col1 < col2 then true
else false
let compare a b =
if (a.t_loc = b.t_loc) && (a.t_label = b.t_label)
then 0 else
(* Order the terms accoridng to their source code locations *)
if before a.t_loc b.t_loc then 1
else -1
end
module S = Set.Make(TermCmp)
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
ignore(Str.search_forward regexp l.lab_string 0);
true
with Not_found -> false
let get_label labels regexp =
Slab.choose (Slab.filter (label_starts_with regexp) labels)
let print_label fmt l =
fprintf fmt "\"%s\"" l.lab_string
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 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
location) as the element el already exists in info_model, replace it with el.
The reason is that we do not want to display two model elements with the same
name in the same location and usually it is better to display the last one.
Note that two model elements can have the same name and location if why is used
as an intemediate language and the locations are locations in the source language.
Then, more why constructs (terms) can represent a single construct in the source
language and more terms have thus the same model name and location. This happens,
e.g., if why code is generated from SPARK. There, the first iteration of while
cycle is unrolled in some cases. If the task contains both a term representing a
variable in the first iteration of unrolled loop and a term representing the variable
in the subsequent loop iterations, only the latter is relevant for the counterexample
and it is the one that comes after the former one (and that is why we always keep the
last term).
*)
let info_model = S.remove el info_model in
S.add el info_model
let add_old lab_str =
try
let pos = Str.search_forward (Str.regexp "@") lab_str 0 in
let after = String.sub lab_str pos ((String.length lab_str)-pos) in
if after = "@init" then
(String.sub lab_str 0 pos) ^ "@old"
else lab_str
with Not_found -> lab_str ^ "@old"
let model_trace_for_postcondition ~labels (info: vc_term_info) =
(* 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
*)
try
let trace_label = get_label labels model_trace_regexp in
let lab_str = add_old trace_label.lab_string in
if lab_str = trace_label.lab_string then
labels
else
let other_labels = Slab.remove trace_label labels in
Slab.add
(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
let get_fun_name name =
let splitted = Strings.bounded_split ':' name 2 in
match splitted with
| _::[second] ->
second
| _ ->
""
let check_enter_vc_term t in_goal vc_term_info =
(* 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 in_goal && 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_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_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
info.vc_inside <- false;
end
open Term
(* Information about the term that triggers VC. *)
type vc_term_info = {
mutable vc_inside : bool;
(* 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) *)
}
module TermCmp : sig
type t = term
val before: Loc.position option -> Loc.position option -> bool
val compare: term -> term -> int
end
module S : Set.S with type elt = term and type t = Set.Make(TermCmp).t
val model_trace_regexp: Str.regexp
val label_starts_with: Str.regexp -> Ident.label -> bool
val get_label: unit Ident.Mlab.t -> Str.regexp -> Ident.label
val print_label: Format.formatter -> Ident.label -> unit
val model_label: Ident.label
val model_vc_term_label: Ident.label
val add_model_element: Term.term -> S.t -> S.t
val add_old: string -> string
val model_trace_for_postcondition: labels: unit Ident.Mlab.t -> vc_term_info -> unit Ident.Mlab.t
val get_fun_name: string -> string
val check_enter_vc_term: Term.term -> bool -> vc_term_info -> unit
val check_exit_vc_term: Term.term -> bool -> vc_term_info -> unit
......@@ -18,6 +18,7 @@ open Ty
open Term
open Decl
open Printer
open Cntexmp_printer
let debug = Debug.register_info_flag "smtv2_printer"
~desc:"Print@ debugging@ messages@ about@ printing@ \
......@@ -77,48 +78,6 @@ let ident_printer () =
let san = sanitizer char_to_alpha char_to_alnumus in
create_ident_printer bls ~sanitizer:san
(* Information about the term that triggers VC. *)
type vc_term_info = {
mutable vc_inside : bool;
(* 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) *)
}
module TermCmp = struct
type t = term
let before loc1 loc2 =
(* Return true if loc1 is strictly before loc2 *)
match loc1 with
| None -> false
| Some loc1 ->
match loc2 with
| None -> false
| Some loc2 ->
let (_, line1, col1, _) = Loc.get loc1 in
let (_, line2, col2, _) = Loc.get loc2 in
if line1 <> line2 then
if line1 < line2 then true
else false
else
if col1 < col2 then true
else false
let compare a b =
if (a.t_loc = b.t_loc) && (a.t_label = b.t_label)
then 0 else
(* Order the terms accoridng to their source code locations *)
if before a.t_loc b.t_loc then 1
else -1
end
module S = Set.Make(TermCmp)
type info = {
info_syn : syntax_map;
info_converters : converter_map;
......@@ -172,33 +131,6 @@ 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_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 add_model_element el info_model =
(** Add element el (term) to info_model.
If an element with the same hash (the same set of labels + the same
location) as the element el already exists in info_model, replace it with el.
The reason is that we do not want to display two model elements with the same
name in the same location and usually it is better to display the last one.
Note that two model elements can have the same name and location if why is used
as an intemediate language and the locations are locations in the source language.
Then, more why constructs (terms) can represent a single construct in the source
language and more terms have thus the same model name and location. This happens,
e.g., if why code is generated from SPARK. There, the first iteration of while
cycle is unrolled in some cases. If the task contains both a term representing a
variable in the first iteration of unrolled loop and a term representing the variable
in the subsequent loop iterations, only the latter is relevant for the counterexample
and it is the one that comes after the former one (and that is why we always keep the
last term).
*)
let info_model = S.remove el info_model in
S.add el info_model
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
......@@ -206,85 +138,6 @@ let collect_model_ls info ls =
add_model_element
(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
ignore(Str.search_forward regexp l.lab_string 0);
true
with Not_found -> false
let get_label labels regexp =
Slab.choose (Slab.filter (label_starts_with regexp) labels)
let add_old lab_str =
try
let pos = Str.search_forward (Str.regexp "@") lab_str 0 in
let after = String.sub lab_str pos ((String.length lab_str)-pos) in
if after = "@init" then
(String.sub lab_str 0 pos) ^ "@old"
else lab_str
with Not_found -> lab_str ^ "@old"
let model_trace_for_postcondition ~labels info =
(* 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
*)
try
let trace_label = get_label labels model_trace_regexp in
let lab_str = add_old trace_label.lab_string in
if lab_str = trace_label.lab_string then
labels
else
let other_labels = Slab.remove trace_label labels in
Slab.add
(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.info_vc_term.vc_func_name) ^ "@result"))
labels
let get_fun_name name =
let splitted = Strings.bounded_split ':' name 2 in
match splitted with
| _::[second] ->
second
| _ ->
""
let check_enter_vc_term t info =
(* Check whether the term that triggers VC is entered.