Commit a6b1d368 authored by David Hauzar's avatar David Hauzar
Browse files

Merge branch 'counter-examples'

parents 510a24ec 048d5150
......@@ -35,7 +35,7 @@ transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
(* Prepare for counter-example query: get rid of some quantifiers (makes it
(* Prepare for counter-example query: get rid of some quantifiers (makes it
possible to query model values of the variables in premises) and introduce
counter-example projections *)
transformation "prepare_for_counterexmp"
......
......@@ -5,45 +5,10 @@ module M
type int_type = Integer int
function projfi "model_trace:.projfi" (l : int) : int
meta "inline : no" function projfi
meta "model_projection" function projfi
function projfl "model_trace:.projfl" (l : list int_type) : int
=
match l with
| Nil -> 0
| Cons (Integer n) _ -> n
| _ -> 0
end
function projf1 "model_trace:.projf1" (l : int) : bool
=
l > 0
function projf2 "model_trace:.projf2" (l : int) : bool
=
l <= 0
meta "inline : no" function projfl
meta "model_projection" function projfl
meta "inline : no" function projf1
meta "model_projection" function projf1
meta "inline : no" function projf2
meta "model_projection" function projf2
val y "model_projected" "model" "model_trace:y" :ref int
let proj_test ( l "model_projected" : list int_type) : int
ensures { result > 0 }
=
match l with
| Nil -> 1
| Cons (Integer n) _ -> n
| _ -> 1
end
(**********************************************************
** Getting counterexamples for terms of primitive types **
**********************************************************)
val y "model" "model_trace:y" :ref int
let incr ( x23 "model" "model_trace:x23" : ref int ): unit
ensures { "model_vc" "model_func" !x23 = old !x23 + 2 + !y }
......@@ -59,20 +24,50 @@ module M
incr x;
while "model" "model_trace:cond" !x > 0 do invariant { !x >= 0 } variant { !x } x := !x - 1 done
(**************************************
** Getting counterexamples for maps **
**************************************)
use import map.Map
let test_map (x "model" : ref (map int int)) : unit
ensures { !x[0] <> !x[1] }
ensures { "model_vc" !x[0] <> !x[1] }
=
x := Map.set !x 0 3
(* Multi-dimensional maps *)
let test_map2 (x "model" : ref (map int (map int int))) : unit
ensures { !x[0][0] <> !x[1][1] }
let test_map_multidim1 (x "model" : ref (map int (map int int))) : unit
ensures { "model_vc" !x[0][0] <> !x[1][1] }
=
x := Map.set !x 0 (Map.get !x 1)
type r = {f:int; g:bool}
let test_record1 (x "model" "model_trace:x" : r) : int
let test_map_multidim2 (x "model" : ref (map int (map int int))) : unit
ensures { "model_vc" !x[0][0] <> !x[1][1] }
=
let x0 = Map.get !x 0 in
let x0 = Map.set x0 0 3 in
x := Map.set !x 0 x0
(*****************************************
** Getting counterexamples for records **
*****************************************)
(*** In all cases, records are decomposed using match eval ***)
type r = {f "field_f" :int; g:bool}
(* Projection functions *)
function projf_r_f "model_trace:.f" (x : r) : int
=
x.f
function projf_r_g "model_trace:.g" (x : r) : bool
=
x.g
meta "inline : no" function projf_r_f
meta "model_projection" function projf_r_f
meta "inline : no" function projf_r_g
meta "model_projection" function projf_r_g
let record_match_eval_test1 (x "model" "model_trace:x" : r) : int
ensures { "model_vc" "model_func" result = 1 }
=
if x.g then
......@@ -80,23 +75,131 @@ module M
else
1
let test_record2 (x "model" "model_trace:x" : ref r) : unit
let record_match_eval_test2 (x "model_projected" : r ) : int
ensures { result = 1 }
=
x.f
let record_match_eval_test3 (x "model" "model_trace:x" : ref r) : unit
ensures { !x.g }
=
x := { !x with f = 6}
let test_record3 (x "model" "model_trace:x" : ref r) : r
let record_match_eval_test4 (x "model" "model_trace:x" : ref r) : r
ensures { "model_vc" "model_func" result.g }
=
x := { !x with f = 6 };
!x
val re "model" : ref r
val re "model_projected" : ref r
let test_record4 (x "model" "model_trace:x" : ref r) : r
let test_record_match_eval_test5 (x "model" "model_trace:x" : ref r) : r
ensures { "model_vc" "model_func" result = !re }
=
x := { !x with f = 6 };
!x
(***********************************************************
** Getting counterexamples for records and maps together **
***********************************************************)
(*** Records and maps together ***)
type r_map = {f_map:map bool int; g_bool:bool}
function projf_r_map_f_map "model_trace:.f_map" (rec_map : r_map) : map bool int
=
rec_map.f_map
function projf_r_map_g "model_trace:.g_map" (rec_map : r_map) : bool
=
rec_map.g_bool
meta "inline : no" function projf_r_map_f_map
meta "model_projection" function projf_r_map_f_map
meta "inline : no" function projf_r_map_g
meta "model_projection" function projf_r_map_g
(* Tests *)
(* Warning: does not terminate *)
let map_record_proj_test1 (map_rec "model_projected" : map bool r)
ensures { result = 0 }
=
map_rec[true].f
let record_map_proj_test2 (rec_map "model_projected" : r_map)
ensures { result = 0 }
=
rec_map.f_map[true]
val re_rec_map "model_projected" : r_map
let record_map_proj_test3 (rec_map "model_projected" : r_map)
ensures { result = re_rec_map }
=
rec_map
(*******************************************
** Definitions of projections used below **
*******************************************)
function projfi "model_trace:.projfi" (l : int) : int
= l
meta "inline : no" function projfi
meta "model_projection" function projfi
function projf1 "model_trace:.projf1" (l : int) : bool
=
l > 0
function projf2 "model_trace:.projf2" (l : int) : bool
=
l <= 0
meta "inline : no" function projf1
meta "model_projection" function projf1
meta "inline : no" function projf2
meta "model_projection" function projf2
(*******************************************************
** Getting counterexamples for maps with projections **
******************************************************)
(* Both indices and range of map will be projected using
projfi, projf1, and projf2
Warning: cvc4 is not able to handle projections there *)
let proj_map_test1 (x "model_projected" : ref (map int int)) : unit
ensures { "model_vc" !x[0] <> !x[1] }
=
x := Map.set !x 0 3
(* No projection function for bool -> the array should be
present in counterexample as it is. *)
let proj_map_test2 (x "model_projected" : ref (map int bool)) : unit
ensures { "model_vc" !x[0] <> !x[1] }
=
x := Map.set !x 0 true
(*********************************
** Non-terminating projections **
*********************************)
(* Warning: if definition of the following projections are present,
the proof of everything below will not terminate. *)
function projfl "model_trace:.projfl" (l : list int_type) : int
=
match l with
| Nil -> 0
| Cons (Integer n) _ -> n
| _ -> 0
end
meta "inline : no" function projfl
meta "model_projection" function projfl
(* list int_type will be projected using projfl to int,
int will be projected using projfi, projf1, and projf2
Warning: does not terminate. *)
let proj_test ( l "model_projected" : list int_type) : int
ensures { result > 0 }
=
match l with
| Nil -> 1
| Cons (Integer n) _ -> n
| _ -> 1
end
end
......@@ -33,7 +33,7 @@ type model_value =
| Bitvector of int
| Unparsed of string
and arr_index = {
arr_index_key : int;
arr_index_key : model_value;
arr_index_value : model_value;
}
and model_array = {
......@@ -51,11 +51,8 @@ let array_add_element ~array ~index ~value =
(*
Adds the element value to the array on specified index.
*)
let int_index = match index with
| Integer s -> int_of_string s
| _ -> raise Not_found in
let arr_index = {
arr_index_key = int_index;
arr_index_key = index;
arr_index_value = value
} in
{
......@@ -67,7 +64,7 @@ let rec print_indices sanit_print fmt indices =
match indices with
| [] -> ()
| index::tail ->
fprintf fmt "; %d -> " index.arr_index_key;
fprintf fmt "; %a -> " (print_model_value_sanit sanit_print) index.arr_index_key;
print_model_value_sanit sanit_print fmt index.arr_index_value;
print_indices sanit_print fmt tail
and
......
......@@ -20,7 +20,7 @@ type model_value =
| Bitvector of int
| Unparsed of string
and arr_index = {
arr_index_key : int;
arr_index_key : model_value;
arr_index_value : model_value;
}
and model_array = {
......
......@@ -85,9 +85,16 @@ other_than_const_array:
| INT_STR { $1 }
| CONST { "const" }
(* Example:
(store (store ((as const (Array Int Int)) 0) 1 2) 3 4)
(store (store ((as const (Array Int Int)) false) 1 true) 3 true) *)
(* Examples:
(1) Map from int to int:
(store (store ((as const (Array Int Int)) 0) 1 2) 3 4)
(2) Map from int to bool:
(store (store ((as const (Array Int Int)) false) 1 true) 3 true)
(3) Map from int to map from int to int (all elemets are 0):
((as const (Array Int (Array Int Int))) ((as const (Array Int Int)) 0))
(4) Map from int to map from int to int (element [1][1] is 3, all others are 0)
(store (store ((as const (Array Int (Array Int Int))) ((as const (Array Int Int)) 0)) 0 (store ((as const (Array Int Int)) 0) 0 3)) 1 (store ((as const (Array Int Int)) 0) 1 3))
*)
array:
| LPAREN possible_space
LPAREN possible_space
......@@ -97,16 +104,16 @@ array:
RPAREN
{ Model_parser.array_create_constant ~value:$13 }
| LPAREN possible_space
STORE possible_space array possible_space value SPACE integer
STORE possible_space array possible_space value SPACE value
possible_space
RPAREN
{ Model_parser.array_add_element ~array:$5 ~index:$7 ~value:$9 }
array_skipped_part:
| LPAREN term_list RPAREN {}
(* Example:
(_ bv2048 16) *)
bitvector:
| BITVECTOR_VALUE
{ $1 }
array_skipped_part:
| LPAREN term_list RPAREN {}
......@@ -12,13 +12,15 @@
open Ident
open Term
open Decl
open Theory
open Ty
(*
(* Debugging functions *)
let debug = Debug.register_info_flag "intro_projections_counterexmp"
~desc:"Print@ debugging@ messages@ about@ introducing@ projections@ for@ counterexamples."
let rec debug_print_terms terms =
vlet rec debug_print_terms terms =
match terms with
| [] -> ()
| term::tail ->
......@@ -65,7 +67,7 @@ let intro_const_equal_to_term
(* Return the declaration of new constant and the axiom *)
decl_new_constant::decl_axiom::[]
let intro_proj_for_ls map_projs ls_projected =
let intro_proj_for_ls env map_projs ls_projected =
(* Returns list of declarations for projection of ls_projected
if it has a label "model_projected", otherwise returns [].
......@@ -101,36 +103,124 @@ let intro_proj_for_ls map_projs ls_projected =
let rec projections_for_term term proj_name applied_projs map_projs =
(* Return declarations for projections of the term.
Parameter proj_name is the name of the projection
Parameter applied_proj_f is a set of projection functions already applied to term*)
try
(* Find all projection functions for the term *)
let pfs = Ty.Mty.find (Opt.get term.t_ty) map_projs in
(* Collect declarations for projections f of the form
f = pf_n .. pf_1 where pf_1 is an element of pfs *)
List.fold_left
(fun l pf_1 ->
if Term.Sls.mem pf_1 applied_projs then
(* Do not apply the same projection twice *)
introduce_constant term proj_name
else
let t_applied = Term.t_app pf_1 [term] pf_1.ls_value in
let pf_1_name =
try
get_model_element_name ~labels:pf_1.ls_name.id_label
with Not_found -> "" in
let proj_name = proj_name^pf_1_name in
let applied_projs = Term.Sls.add pf_1 applied_projs in
(* Return declarations for projections of t_applied = pf_1 term *)
let t_applied_projs = projections_for_term t_applied proj_name applied_projs map_projs in
List.append l t_applied_projs
)
[]
pfs
with Not_found ->
(* There is no projection function for the term
-> the projection consists of definition of constant c and axiom c = p
Parameter applied_proj_f is a set of projection functions already applied to the term *)
match (Opt.get term.t_ty).ty_node with
| Tyapp (ts, [t_from; t_to]) when ts.ts_name.id_string = "map" -> begin
(* If the term is of map type, check whether t_to (and t_from - to be done later) can be projected.
If it is so, for each projection pf_1 from t_to to t_res introduce new map with the elemements
equal to projections of the source map:
const proj_map: map t_from t_res
axiom proj_axiom :
(forall i : t_from. proj_map[i] = pf_1(term[i]))
-> continue recursively with m2 as a term (see comments for non-map case)
Problem: this introduces too many new constants => TODO: do either:
(1)
val proj_map_func (term: map t_from t_to) : map t_from t_res
ensures { forall i: t_from. pf_1(term[i]) = result[i] }
-> apply proj_map_func to term and continue the same way as in the non-map case
or
(2)
NOT: this does not work
function proj_map_func (term : map t_from t_to) : map t_from t_res
=
let proj_map = ref (Const.const 0) in
problem, cannot do for cycle through all the map proj_map
*)
introduce_constant term proj_name
try
let pfs = Ty.Mty.find t_to map_projs in
List.fold_left
(fun l pf_1 ->
if Term.Sls.mem pf_1 applied_projs then
(* Do not apply the same projection twice *)
introduce_constant term proj_name
else
(* Newly introduced map with projected indices *)
let proj_map_name = ls_projected.ls_name.id_string^"_proj_arr_constant"^proj_name in
let proj_map_id = Ident.id_fresh proj_map_name in
let proj_map_ty = Some (ty_app ts [t_from; Opt.get pf_1.ls_value]) in
let proj_map_ls = Term.create_lsymbol proj_map_id [] proj_map_ty in
let proj_map_decl = Decl.create_param_decl proj_map_ls in
let proj_map_t = Term.t_app proj_map_ls [] proj_map_ty in
(* The quantified variable i *)
let var_i : Term.vsymbol = Term.create_vsymbol (Ident.id_fresh "x") t_from in
let i : Term.term = Term.t_var var_i in
let map_theory = Env.read_theory env ["map"] "Map" in
let select = (ns_find_ls map_theory.th_export ["get"]) in
(* Indices: proj_map[i], term[i] *)
let proj_map_idx_t = Term.t_app_infer select [proj_map_t;i] in
let term_idx_t = Term.t_app_infer select [term;i] in
(* Formula f: forall i : t_from. proj_map[i] = pf_1(term[i]) *)
let term_idx_projected_t = Term.t_app pf_1 [term_idx_t] pf_1.ls_value in
let fla_to_be_quant = Term.t_equ proj_map_idx_t term_idx_projected_t in
let fla_axiom = Term.t_forall_close [var_i] [] fla_to_be_quant in
(* Axiom about projection: axiom f*)
let proj_axiom_name = ls_projected.ls_name.id_string^"_proj_arr_axiom"^proj_name in
let proj_axiom_id = Decl.create_prsymbol (Ident.id_fresh proj_axiom_name) in
let proj_axiom = Decl.create_prop_decl Decl.Paxiom proj_axiom_id fla_axiom in
(* Recursively call projecting of the term proj_map -> proj_map_projections *)
let pf_1_name =
try
get_model_element_name ~labels:pf_1.ls_name.id_label
with Not_found -> "" in
let proj_name = proj_name^pf_1_name in
let applied_projs = Term.Sls.add pf_1 applied_projs in
let proj_map_projections_defs = projections_for_term proj_map_t proj_name applied_projs map_projs in
List.append l (List.append [proj_map_decl;proj_axiom] proj_map_projections_defs)
)
[]
pfs
with Not_found ->
(* There is no projection function for the term
-> the projection consists of definition of constant c and axiom c = p
*)
introduce_constant term proj_name
end
| _ ->
(* Non-map case *)
try
(* Find all projection functions for the term *)
let pfs = Ty.Mty.find (Opt.get term.t_ty) map_projs in
(* Collect declarations for projections f of the form
f = pf_n .. pf_1 where pf_1 is an element of pfs *)
List.fold_left
(fun l pf_1 ->
if Term.Sls.mem pf_1 applied_projs then
(* Do not apply the same projection twice *)
introduce_constant term proj_name
else
let t_applied = Term.t_app pf_1 [term] pf_1.ls_value in
let pf_1_name =
try
get_model_element_name ~labels:pf_1.ls_name.id_label
with Not_found -> "" in
let proj_name = proj_name^pf_1_name in
let applied_projs = Term.Sls.add pf_1 applied_projs in
(* Return declarations for projections of t_applied = pf_1 term *)
let t_applied_projs = projections_for_term t_applied proj_name applied_projs map_projs in
List.append l t_applied_projs
)
[]
pfs
with Not_found ->
(* There is no projection function for the term
-> the projection consists of definition of constant c and axiom c = p
*)
introduce_constant term proj_name
in
......@@ -139,11 +229,11 @@ let intro_proj_for_ls map_projs ls_projected =
projections_for_term t_projected "" Term.Sls.empty map_projs
let introduce_projs map_projs decl =
let introduce_projs env map_projs decl =
match decl.d_node with
| Dparam ls_projected ->
(* Create declarations for a projections of ls_projected *)
let projection_decls = intro_proj_for_ls map_projs ls_projected in
let projection_decls = intro_proj_for_ls env map_projs ls_projected in
decl::projection_decls
(* TODO
......@@ -175,15 +265,15 @@ let build_projections_map projs =
in
Sls.fold build_map projs Ty.Mty.empty
let meta_transform2 projs =
let meta_transform2 env projs =
let map_projs = build_projections_map projs in
Trans.decl (introduce_projs map_projs) None
Trans.decl (introduce_projs env map_projs) None
let intro_projections_counterexmp =
Trans.on_tagged_ls meta_projection meta_transform2
let intro_projections_counterexmp env =
Trans.on_tagged_ls meta_projection (meta_transform2 env)
let () = Trans.register_transform "intro_projections_counterexmp" intro_projections_counterexmp
let () = Trans.register_env_transform "intro_projections_counterexmp" intro_projections_counterexmp
~desc:"For@ each@ declared@ abstract@ function@ and@ predicate@ p@ with@ label@ model_projected@ \
and@ projectin@ f@ for@ p@ creates@ declaration@ of@ new@ constant@ c@ with@ label@ model@ and@ an@ axiom@ \
c = f p."
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
val intro_projections_counterexmp : Task.task Trans.trans
val intro_projections_counterexmp : Env.env -> Task.task Trans.trans
(**
Transformation that for each declared abstract function or predicate
p labeled with label "model_projected" creates a declaration of new
......
......@@ -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 env task =
if not (get_counterexmp task) then begin
(* Counter-example will not be queried, do nothing *)
Debug.dprintf debug "Not get ce@.";
......@@ -24,15 +24,15 @@ let prepare_for_counterexmp2 task =
(Trans.goal Introduction.intros)
(Trans.compose
Intro_vc_vars_counterexmp.intro_vc_vars_counterexmp
Intro_projections_counterexmp.intro_projections_counterexmp
(Intro_projections_counterexmp.intro_projections_counterexmp env)
)
in
(Trans.apply comp_trans) task
end
let prepare_for_counterexmp = Trans.store prepare_for_counterexmp2
let prepare_for_counterexmp env = Trans.store (prepare_for_counterexmp2 env)
let () = Trans.register_transform "prepare_for_counterexmp" prepare_for_counterexmp
let () = Trans.register_env_transform "prepare_for_counterexmp" prepare_for_counterexmp
~desc:"Transformation@ that@ prepares@ the@ task@ for@ quering@ for@ \
the@ counter-example@ model.@ This@ transformation@ does@ so@ only@ \
when@ the@ solver@ will@ be@ asked@ for@ the@ counter-example."
......
......@@ -14,9 +14,9 @@ val get_counterexmp : Task.task -> bool
Returns true if counter-example should be get for the task.
*)
val prepare_for_counterexmp : Task.task Trans.trans
val prepare_for_counterexmp : Env.env -> Task.task Trans.trans
(**
Transformation that prepares the task for quering for
Transformation that prepares the task for quering for
the counter-example model.
This transformation does so only when the solver will be asked
for the counter-example.
......
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