Commit 27b053f3 authored by Sylvain Dailler's avatar Sylvain Dailler

P530-020 counterex - Printing quantified variables

We changed the prepare_for_counterexamples transformation to allow
printing of quantified expressions, remove duplications of printed
examples and adding an incomplete function to print universally
quantified variables that are positive but not at head of the term.

* src/transform/intro_projections_counterexmp.ml
(intro_const_equal_to_term): Generating of the preid for a counterex.

* src/transform/intro_projections_counterexmp.mli
(val_intro_const_equal_to_term): Changing signature.

* src/transform/intro_vc_vars_counterexmp.ml
(Hprid): Adding a container for preids.
(do_intro): Adding cases for generation of counterexample in the Tvar
case, factorising the construction of vc_constant in a function
new_counter_example_variable. Adding argument vc_map to avoid
duplication of vc_constants
(new_counter_example_variable): Adding a check to avoid duplication of
vc_constant.
(remove_positive_foralls): New experimental incomplete function that aims
at introducting foralls even when they are under a construct.
"H /\ forall i. P(i)" becomes "i as premisse and H /\ P(i)".
(intros): Added calls to do_intro and removed optimizations.
(do_intro_vc_vars_counterexmp): Concatenate results of intros and
do_intros and create the prop goal.

* src/transform/introduction.ml
(stop_intro): Removed stop_intro.

* src/transform/prepare_for_counterexmp.ml
(prepare_for_counterexmp2): Removed call to introduce_premisses.

Change-Id: I836ae9e69b887247eb64196705cc7ad32ba36825
parent 89c3adc3
......@@ -45,16 +45,13 @@ let meta_projection = Theory.register_meta "model_projection" [Theory.MTlsymbol]
let intro_const_equal_to_term
~term
~const_label
~const_loc
~const_name
~id_new
~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
......@@ -98,7 +95,8 @@ let intro_proj_for_ls env map_projs ls_projected =
let const_loc = Opt.get ls_projected.ls_name.id_loc in
let const_name = ls_projected.ls_name.id_string^"_proj_constant_"^proj_name in
let axiom_name = ls_projected.ls_name.id_string^"_proj_axiom_"^proj_name in
intro_const_equal_to_term ~term:t_rhs ~const_label ~const_loc ~const_name ~axiom_name in
let id_new = Ident.id_user ~label:const_label const_name const_loc in
intro_const_equal_to_term ~term:t_rhs ~id_new:id_new ~axiom_name in
let rec projections_for_term term proj_name applied_projs map_projs =
(* Return declarations for projections of the term.
......
......@@ -55,18 +55,14 @@ val intro_projections_counterexmp : Env.env -> Task.task Trans.trans
val intro_const_equal_to_term :
term : Term.term ->
const_label : Ident.Slab.t ->
const_loc : Loc.position ->
const_name : string ->
id_new : Ident.preid ->
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 id_new the preid composed of the name, label and loc 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
*)
......@@ -10,6 +10,7 @@
(********************************************************************)
open Decl
open Ty
open Term
open Ident
......@@ -100,67 +101,200 @@ let model_trace_for_postcondition ~labels =
let is_counterexample_label l = l = model_label || l = model_projected_label
let rec do_intro info vc_loc t =
(* Preid table necessary to avoid duplication of *_vc_constant *)
module Hprid = Exthtbl.Make (struct
type t = preid
let equal x y = x.pre_name = y.pre_name && Slab.equal x.pre_label y.pre_label
let hash p = Exthtbl.hash p
end)
(* Used to generate duplicate vc_constant and axioms for counterex generation.
This function is always called when the term is in negative position or
under a positive term that is not introducible. This means it never change the
goal.
@param info used to know if the current term is under a vc_label
@param vc_loc is the location of the vc_label (returned value)
@param vc_map is a container for generated vc_constant id (used to avoid duplication)
@param t: current subterm of the goal
@return list of declarations added by do_intro
*)
let rec do_intro info vc_loc vc_map t =
let info = check_enter_vc_term t info vc_loc in
let do_intro = do_intro info vc_loc in
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 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 *)
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
let do_intro = do_intro info vc_loc vc_map in
(* Do the necessary machinery to add a printable counterexample when encountered
(variable or function without arguments) *)
let new_counter_example_variable ls info =
if info.vc_inside then begin
match info.vc_loc with
| None -> []
| Some loc ->
(* 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 it for counterexample
and make it equal to the variable *)
if Slab.exists is_counterexample_label ls.id_label then
let const_label = if info.vc_pre_or_post then
model_trace_for_postcondition ~labels:ls.id_label
else
ls.id_label in
let const_name = ls.id_string^"_vc_constant" in
let axiom_name = ls.id_string^"_vc_axiom" in
(* Create a new id here to check the couple name, location. *)
let id_new = Ident.id_user ~label:const_label const_name loc in
(* The following check is used to avoid duplication of
*_vc_constant_n. We keep track of the preids that have already
been duplicated in vc_map. Note that we need to do it before
these preid are casted to lsymbol (by Term.create_lsymbol)
because those integrates a unique hash that would make identical
preid different lsymbol *)
if (Hprid.mem vc_map id_new) then
[]
else
begin
Hprid.add vc_map id_new true;
Intro_projections_counterexmp.intro_const_equal_to_term
~term:t ~const_label ~const_loc:loc ~const_name ~axiom_name
else
[]
end
else []
| _ ->
List.fold_left
~term:t ~id_new:id_new ~axiom_name
end
else
[]
end
else [] in
match t.t_node with
| Tapp (ls, tl) ->
begin
match tl with
| [] ->
new_counter_example_variable ls.ls_name info
| _ ->
List.fold_left
(fun defs term ->
List.append defs (do_intro term))
[]
tl
end;
| Tbinop (_, f1, f2) ->
end
| Tvar v ->
new_counter_example_variable v.vs_name info
| Tbinop (_, f1, f2) ->
List.append (do_intro f1) (do_intro f2)
| Tquant (_, fq) ->
let _, _, f = t_open_quant fq in
do_intro f
| Tlet (t, tb) ->
let _, f = t_open_bound tb in
List.append (do_intro t) (do_intro f)
| Tnot f ->
do_intro f
| Tif (f1, f2, f3) ->
List.append
(List.append (do_intro f1) (do_intro f2))
| Tquant (_, fq) ->
let _, _, f = t_open_quant fq in
do_intro f
| Tlet (t, tb) ->
let _, f = t_open_bound tb in
List.append (do_intro t) (do_intro f)
| Tnot f ->
do_intro f
| Tif (f1, f2, f3) ->
List.append
(List.append (do_intro f1) (do_intro f2))
(do_intro f3)
| Tcase (t, _) ->
do_intro t
(* todo: handle the second argument of Tcase *)
| _ -> [] in
| Tcase (t, _) ->
do_intro t
(* todo: handle the second argument of Tcase *)
| Tconst _ -> []
| Ttrue -> []
| Tfalse -> []
| Teps _ -> []
(* Meant to remove foralls in positive positions (not necessarily in top
position) *)
let rec remove_positive_foralls f =
match f.t_node with
| Tbinop (Timplies,f1,f2) ->
let (decl, fres) = remove_positive_foralls f2 in
(decl, t_implies f1 fres)
| Tbinop (Tand, f1, f2) ->
let (decl1, fres1) = remove_positive_foralls f1 in
let (decl2, fres2) = remove_positive_foralls f2 in
(decl1 @ decl2, t_and fres1 fres2)
| Tquant (Tforall, fq) ->
let vsl,_trl,f_t = t_open_quant fq in
let intro_var subst vs =
let ls = create_lsymbol (id_clone vs.vs_name) [] (Some vs.vs_ty) in
Mvs.add vs (fs_app ls [] vs.vs_ty) subst,
create_param_decl ls
in
let subst, dl = Lists.map_fold_left intro_var Mvs.empty vsl in
let f = t_label_copy f (t_subst subst f_t) in
let decl, goal = remove_positive_foralls f in
(dl @ decl, goal)
| _ -> ([], f)
(* Introduces foralls, lets, and implications at the head of the goal. When
under a vc_label, it can make calls to do_intros which creates new
declarations for counterexample generation. When no more intros are
possible, it calls remove_positive_foralls which do an experimental
introduction of foralls even under another constructs (example: H /\ forall
i. P(i) yields (i, H /\ P(i)). Note that it seems difficult and "unsafe"
to merge these two functions
(* check_exit_vc_term t info; *)
It is adapted from transform/introduce.ml. (we mainly added do_intros calls
and removed split optimizations.
defs
@param info used to know if the current term is under a vc_label
@param vc_loc is the location of the vc_label (returned value)
@param vc_map is a container for generated vc_constant id
(used to avoid duplication)
@param f current goal
@return pair of the declarations introduced and the modified goal. *)
let rec intros info vc_loc vc_map f =
let info = check_enter_vc_term f info vc_loc in
let intros = intros info vc_loc vc_map in
match f.t_node with
| Tbinop (Timplies,f1,f2) ->
let f2 = t_label_copy f f2 in
let l = if info.vc_inside then do_intro info vc_loc vc_map f1 else [] in
let id = create_prsymbol (id_fresh "H") in
let d = create_prop_decl Paxiom id f1 in
let decl, goal = intros f2 in
(d :: l @ decl, goal)
| Tquant (Tforall,fq) ->
let vsl,_trl,f_t = t_open_quant fq in
let intro_var subst vs =
let ls = create_lsymbol (id_clone vs.vs_name) [] (Some vs.vs_ty) in
Mvs.add vs (fs_app ls [] vs.vs_ty) subst,
create_param_decl ls
in
let subst, dl = Lists.map_fold_left intro_var Mvs.empty vsl in
(* if vs is a symbol that is tagged with a model or model_projected
label, we have to allow it to be printed but it wont be available
after its substitution *)
(* preserve labels and location of f *)
let f = t_label_copy f (t_subst subst f_t) in
let decl, goal = intros f in
(dl @ decl, goal)
| Tlet (t,fb) ->
let vs,f = t_open_bound fb in
let ls = create_lsymbol (id_clone vs.vs_name) [] (Some vs.vs_ty) in
let f = t_subst_single vs (fs_app ls [] vs.vs_ty) f in
let d = create_logic_decl [make_ls_defn ls [] t] in
(* If we are not inside a vc we don't want left side of let otherwise we
might want it *)
let decl, goal = intros f in
if info.vc_inside then
let l = do_intro info vc_loc vc_map t in
(d :: l @ decl, goal)
else
(d :: decl, goal)
| _ -> remove_positive_foralls f
let do_intro_vc_vars_counterexmp info vc_loc pr f =
List.append (do_intro info vc_loc f) [(create_prop_decl Pgoal pr f)]
let do_intro_vc_vars_counterexmp info vc_loc pr t =
(* TODO initial guess on number of counter-examples to print *)
let vc_map = Hprid.create 100 in
let tvs = t_ty_freevars Stv.empty t in
let mk_ts tv () = create_tysymbol (id_clone tv.tv_name) [] None in
let tvm = Mtv.mapi mk_ts tvs in
let decls = Mtv.map create_ty_decl tvm in
let subst = Mtv.map (fun ts -> ty_app ts []) tvm in
let (defs_intros, t) =
intros info vc_loc vc_map (t_ty_subst subst Mvs.empty t) in
let defs_do_intro = do_intro info vc_loc vc_map t in
Mtv.values decls @ defs_intros @ defs_do_intro @ [(create_prop_decl Pgoal pr t)]
let intro_vc_vars_counterexmp2 task =
let info = {
......
......@@ -20,14 +20,9 @@ open Ty
open Term
open Decl
(* This label is used to stop the introduction transformation to introduce
variables past it. It is generated by software that uses why3 as a backend
such as SPARK (for counterexamples) *)
let stop_intro = Ident.create_label "stop_intro"
let rec intros pr f =
if Slab.mem stop_intro f.t_label then [create_prop_decl Pgoal pr f] else
match f.t_node with
(* (f2 \/ True) => _ *)
| Tbinop (Timplies,{ t_node = Tbinop (Tor,f2,{ t_node = Ttrue }) },_)
when Slab.mem Term.asym_label f2.t_label ->
[create_prop_decl Pgoal pr f]
......
......@@ -32,11 +32,8 @@ let prepare_for_counterexmp2 env task =
(* Counter-example will be queried, prepare the task *)
Debug.dprintf debug "Get ce@.";
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 env)
)
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