Commit 0b53e050 authored by David Hauzar's avatar David Hauzar

Introducting constants with model labels for variables in the term

triggering VC.

- Transformation intro_vc_vars_counterexamp introduces new constant with
model labels for every variable in the term that trigger VC and axiom
that this constant is equal to the variable, finds the position of the
term that trigger VC, and saves this position in meta (for smtv2
printer).

- Transformation prepare_for_counterexmp additionally performs the
transformation intro_vc_vars_counterexamp

- smtv2 printer no longer collects the location of the term that
triggers VC and does not collect variables in this term in a special
way. Note that this functionality was not yet completely removed from
the printer. It will be done so after the transformation
intro_vc_vars_counterexmp will be tested.

The rationale:
Variables that should be displayed in counterexample are marked
by model labels ("model", "model_projected", "model_trace:*").

Variables inside the term that triggers VC should be displayed in
counterexample for that VC. However, many VCs (tasks) can be generated
for  a signle *.mlw file and only variables in the term that trigger
the VC (task) that is currently proven should be displayed. That means
that the process of selecting variables inside the term that triggers
VC for counterexample must be done while processing the task. It is
done by transformation intro_vc_vars_counterexmp. This means that smtv2
printer no longer has to find the position of the term that triggers
VC and no longer has to collect variables in this term in a special
way.
parent 4b9104a7
......@@ -162,7 +162,7 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \
encoding_sort simplify_array filter_trigger \
introduction abstraction close_epsilon lift_epsilon \
eliminate_epsilon intro_projections_counterexmp \
prepare_for_counterexmp \
intro_vc_vars_counterexmp prepare_for_counterexmp \
eval_match instantiate_predicate smoke_detector \
induction_pr prop_curry
......
......@@ -317,7 +317,9 @@ let rec print_term info fmt t =
| Some _ ->
model_trace_for_postcondition ~labels:ls.ls_name.id_label info in
let t_check_pos = t_label ~loc labels t in
info.info_model <- S.add t_check_pos info.info_model;
(* TODO: temporarily disable collecting variables inside the term triggering VC *)
(*info.info_model <- S.add t_check_pos info.info_model;*)
()
end;
fprintf fmt "@[%a@]" print_ident ls.ls_name
| _ ->
......@@ -540,7 +542,7 @@ let print_info_model cntexample fmt model_list info =
info.info_model <- info_model
end
let print_prop_decl cntexample args info fmt k pr f = match k with
let print_prop_decl vc_loc cntexample args info fmt k pr f = match k with
| Paxiom ->
fprintf fmt "@[<hov 2>;; %s@\n(assert@ %a)@]@\n@\n"
pr.pr_name.id_string (* FIXME? collisions *)
......@@ -560,7 +562,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_term_loc = info.info_vc_term.vc_loc;
vc_term_loc = vc_loc;
queried_terms = model_list; }
| Plemma| Pskip -> assert false
......@@ -587,7 +589,7 @@ let print_data_decl info fmt (ts,cl) =
print_ident ts.ts_name
(print_list space (print_constructor_decl info)) cl
let print_decl cntexample args 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_type_decl info fmt ts
| Ddata [(ts,_)] when query_syntax info.info_syn ts.ts_name <> None -> ()
......@@ -603,9 +605,9 @@ let print_decl cntexample args info fmt d = match d.d_node with
"smtv2 : inductive definition are not supported"
| Dprop (k,pr,f) ->
if Mid.mem pr.pr_name info.info_syn then () else
print_prop_decl cntexample args info fmt k pr f
print_prop_decl vc_loc cntexample args info fmt k pr f
let print_decls cntexample args =
let print_decls vc_loc cntexample args =
let print_decl (sm, cm, model) fmt d =
try
let vc_term_info = { vc_inside = false; vc_loc = None; vc_func_name = None } in
......@@ -615,7 +617,7 @@ let print_decls cntexample args =
info_model = model;
info_in_goal = false;
info_vc_term = vc_term_info} in
print_decl cntexample args info fmt d; (sm, cm, info.info_model), []
print_decl vc_loc cntexample args info fmt d; (sm, cm, info.info_model), []
with Unsupported s -> raise (UnsupportedDecl (d,s)) in
let print_decl = Printer.sprint_decl print_decl in
let print_decl task acc = print_decl task.Task.task_decl acc in
......@@ -632,6 +634,7 @@ let print_task args ?old:_ fmt task =
(* forget_all ident_printer; *)
let cntexample = Prepare_for_counterexmp.get_counterexmp task in
let vc_loc = Intro_vc_vars_counterexmp.get_location_of_vc task in
print_prelude fmt args.prelude;
set_produce_models fmt cntexample;
......@@ -639,7 +642,7 @@ let print_task args ?old:_ fmt task =
let rec print = function
| x :: r -> print r; Pp.string fmt x
| [] -> () in
print (snd (Trans.apply (print_decls cntexample args) task));
print (snd (Trans.apply (print_decls vc_loc cntexample args) task));
pp_print_flush fmt ()
let () = register_printer "smtv2" print_task
......
......@@ -33,14 +33,38 @@ let debug_decl decl =
*)
(* Label for terms that should be in counterexample *)
let label_model = Ident.create_label "model"
let model_label = Ident.create_label "model"
(* Label for terms that should be projected in counterexample *)
let label_model_proj = Ident.create_label "model_projected"
let model_proj_label = Ident.create_label "model_projected"
(* Meta to tag projection functions *)
let meta_projection = Theory.register_meta "model_projection" [Theory.MTlsymbol]
~desc:"Declares@ the@ projection."
let intro_const_equal_to_term
~term
~const_label
~const_loc
~const_name
~axiom_name
=
(** See documentation of the function in file intro_projections_counterexmp.mli. *)
(* Create declaration of new constant *)
(*let lab_new = Slab.add model_label labels in*)
let id_new = Ident.id_user ~label:const_label const_name const_loc in
let ls_new_constant = Term.create_lsymbol id_new [] term.t_ty in
let decl_new_constant = Decl.create_param_decl ls_new_constant in
let t_new_constant = Term.t_app ls_new_constant [] term.t_ty in
(* Create declaration of the axiom about the constant: t_new_constant = t_rhs *)
let id_axiom = Decl.create_prsymbol (Ident.id_fresh axiom_name) in
let fla_axiom = Term.t_equ t_new_constant term in
let decl_axiom = Decl.create_prop_decl Decl.Paxiom id_axiom fla_axiom in
(* Return the declaration of new constant and the axiom *)
decl_new_constant::decl_axiom::[]
let intro_proj_for_ls map_projs ls_projected =
(* Returns list of declarations for projection of ls_projected
if it has a label "model_projected", otherwise returns [].
......@@ -57,48 +81,31 @@ let intro_proj_for_ls map_projs ls_projected =
@param map_projs maps types to projection function for these types
@param ls_projected the label symbol that should be projected
*)
if not (Slab.mem label_model_proj ls_projected.ls_name.id_label) then
if not (Slab.mem model_proj_label ls_projected.ls_name.id_label) then
(* ls_projected has not a label "model_projected" *)
[]
else
match ls_projected.ls_value with
| None -> []
| Some ty_projected ->
let create_proj_decls t_rhs =
(* Creates projection declarations. That is:
- declaration for new constant t_new_constant
- declaration for axiom stating that t_new_constant = t_rhs. *)
(* Create declaration of new constant *)
let name_new_constant = ls_projected.ls_name.id_string^"_proj_constant" in
let lab_new = Slab.add label_model Slab.empty in
let id_new = Ident.id_derive ~label:lab_new name_new_constant ls_projected.ls_name in
let ls_new_constant = Term.create_lsymbol id_new [] t_rhs.t_ty in
let decl_new_constant = Decl.create_param_decl ls_new_constant in
let t_new_constant = Term.t_app ls_new_constant [] t_rhs.t_ty in
(* Create the declaration of the axiom about the constant: t_new_constant = t_rhs *)
let name_axiom = ls_projected.ls_name.id_string^"_proj_axiom" in
let id_axiom = Decl.create_prsymbol (Ident.id_fresh name_axiom) in
let fla_axiom = Term.t_equ t_new_constant t_rhs in
let decl_axiom = Decl.create_prop_decl Decl.Paxiom id_axiom fla_axiom in
(* Add the declaration of new constant and the axiom *)
decl_new_constant::decl_axiom::[]
in
(* t_rhs is a term corresponding to
(* t_proj is a term corresponding to
- ls_projected (the label symbol being projected) - if there is no
projection function for its type
- application of projection function f to ls_projected *)
let t_rhs =
let t_proj =
let t_projected = Term.t_app ls_projected [] ls_projected.ls_value in
try
let f = Ty.Mty.find ty_projected map_projs in
Term.t_app f [t_projected] f.ls_value
with Not_found -> t_projected in
create_proj_decls t_rhs
(* introduce new constant c and axiom stating c = t_proj *)
let const_label = Slab.add model_label ls_projected.ls_name.id_label in
let const_loc = Opt.get ls_projected.ls_name.id_loc in
let const_name = ls_projected.ls_name.id_string^"_proj_constant" in
let axiom_name = ls_projected.ls_name.id_string^"_proj_axiom" in
intro_const_equal_to_term ~term:t_proj ~const_label ~const_loc ~const_name ~axiom_name
let introduce_projs map_projs decl =
match decl.d_node with
......
......@@ -36,3 +36,21 @@ val intro_projections_counterexmp : Task.task Trans.trans
the projection.
Also, it means that this transformation must be executed before this renaming.
*)
val intro_const_equal_to_term :
term : Term.term ->
const_label : Ident.Slab.t ->
const_loc : Loc.position ->
const_name : string ->
axiom_name : string ->
Decl.decl list
(** Creates declaration of new constant and declaration of axiom
stating that the constant is equal to given term.
@param term the term to which the new constant will be equal
@param const_label the label of the constant
@param const_loc the location of the constant
@param const_name the name of the constant
@param axiom_name the name of the axiom about the constant
@return the definition of the constant and axiom about the constant
*)
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
open Decl
open Term
open Ident
(** For see intro_vc_vars_counterexmp.mli for detailed description
of this transformation. *)
let meta_vc_location =
Theory.register_meta_excl "vc_location" [Theory.MTstring]
~desc:"Location@ of@ the@ term@ that@ triggers@ vc@ in@ the@ form@ file:line:col."
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"
(* Identifies the term 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" *)
(* 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) *)
}
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 get_fun_name name =
let splitted = Str.bounded_split (Str.regexp_string ":") name 2 in
match splitted with
| _::[second] ->
second
| _ ->
""
let check_enter_vc_term t 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 Slab.mem model_vc_term_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 *)
()
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
info.vc_inside <- false;
end
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.vc_func_name) ^ "@result"))
labels
let rec do_intro info t =
check_enter_vc_term t info;
let defs = match t.t_node with
| Tapp (ls, tl) ->
begin
match tl with
| [] ->
if info.vc_inside then begin
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
end
else []
| _ ->
List.fold_left
(fun defs term ->
List.append defs (do_intro info term))
[]
tl
end;
| Tbinop (_, f1, f2) ->
List.append (do_intro info f1) (do_intro info f2)
| Tquant (_, fq) ->
let _, _, f = t_open_quant fq in
do_intro info f
| Tlet (t, tb) ->
let _, f = t_open_bound tb in
List.append (do_intro info t) (do_intro info f)
| Tnot f ->
do_intro info f
| Tif (f1, f2, f3) ->
List.append
(List.append (do_intro info f1) (do_intro info f2))
(do_intro info f3)
| Tcase (t, _) ->
do_intro info t
(* todo: handle the second argument of Tcase *)
| _ -> [] in
check_exit_vc_term t info;
defs
let do_intro_vc_vars_counterexmp info pr f =
List.append (do_intro info f) [(create_prop_decl Pgoal pr f)]
let intro_vc_vars_counterexmp2 task =
let info = {
vc_inside = false;
vc_loc = None;
vc_func_name = None;
} in
(* Do introduction and find location of term triggering VC *)
let do_intro_trans = Trans.goal (do_intro_vc_vars_counterexmp info) in
let task = (Trans.apply do_intro_trans) task in
(* Pass meta with location of the term triggering VC to printer *)
let vc_loc_meta = Theory.lookup_meta "vc_location" in
let g,task = Task.task_separate_goal task in
let pos_str = match info.vc_loc with
| None -> ""
| Some loc ->
let (file, line, col1, col2) = Loc.get loc in
file ^ ":" ^ (string_of_int line) ^ ":" ^ (string_of_int col1) ^ ":" ^ (string_of_int col2)
in
let task = Task.add_meta task vc_loc_meta [Theory.MAstr pos_str] in
Task.add_tdecl task g
let intro_vc_vars_counterexmp = Trans.store intro_vc_vars_counterexmp2
let () = Trans.register_transform "intro_vc_vars_counterexmp"
intro_vc_vars_counterexmp
~desc:"Introduce."
let get_location_of_vc task =
let meta_args = Task.on_meta_excl meta_vc_location task in
match meta_args with
| Some [Theory.MAstr loc_str] ->
let splitted = Str.bounded_split (Str.regexp_string ":") loc_str 4 in
let loc = match splitted with
| [filename; line; col1; col2] ->
let line = int_of_string line in
let col1 = int_of_string col1 in
let col2 = int_of_string col2 in
Some (Loc.user_position filename line col1 col2)
| _ -> None in
loc
| _ -> None
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
val intro_vc_vars_counterexmp : Task.task Trans.trans
(** Finds the position of the term t_vc that trigger VC and saves this
position in meta (for smtv2 printer). For every variable v inside
the term t_vc that triggers VC introduces constant c equal to the
variable v with the location of t_vc, label "model_trace:*", and
either label "model" or "model_projected".
This means that all variables that should be collected for
counterexample will marked by model labels.
If the term triggering VC is postcondition of a function, appends to
the label "model_trace:*" string "@old" for variables corresponding
to old values of input arguments and string "@return" for the variable
corresponding to the return value of the function.
------------------------------------------------------------------
The rationale of this transformation:
Variables that should be displayed in counterexample are marked
by model labels ("model", "model_projected", "model_trace").
Variables inside the term that triggers VC should be displayed in
counterexample for that VC. However, many VCs (tasks) can be generated
for a signle *.mlw file and only variables in the term that trigger
the VC (task) that is currently proven should be displayed. That means
that the process of selecting variables inside the term that triggers
VC for counterexample cannot be done before the task is processed.
It is done by this transformation.
*)
val get_location_of_vc : Task.task -> Loc.position option
(** Gets the location of the term that triggers vc.
This location is collected by transformation intro_vc_vars_counterexmp. *)
......@@ -23,7 +23,7 @@ open Decl
let rec intros pr f = match f.t_node with
| Tbinop (Timplies,f1,f2) ->
(* split f1 *)
(* f is going to be removed, preserve its labels (and possibly also location) *)
(* f is going to be removed, preserve its labels (and possibly also location) in f2 *)
let f2 = t_label_copy f f2 in
let l = Split_goal.split_pos_intro f1 in
List.fold_right
......
......@@ -11,7 +11,7 @@ let get_counterexmp task =
let ce_meta = Task.find_meta_tds task meta_get_counterexmp in
not (Theory.Stdecl.is_empty ce_meta.tds_set)
let prepare_for_counterexmp2 task =
let prepare_for_counterexmp2 task =
if not (get_counterexmp task) then begin
(* Counter-example will not be queried, do nothing *)
Debug.dprintf debug "Not get ce@.";
......@@ -20,9 +20,12 @@ let prepare_for_counterexmp2 task =
else begin
(* Counter-example will be queried, prepare the task *)
Debug.dprintf debug "Get ce@.";
let comp_trans = Trans.compose
(Trans.goal Introduction.intros)
Intro_projections_counterexmp.intro_projections_counterexmp
let comp_trans = Trans.compose
(Trans.goal Introduction.intros)
(Trans.compose
Intro_vc_vars_counterexmp.intro_vc_vars_counterexmp
Intro_projections_counterexmp.intro_projections_counterexmp
)
in
(Trans.apply comp_trans) task
end
......
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