From a2a09b382ee24cbc6c9a51993550384aa1b2ba26 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 29 Mar 2023 10:28:34 +0200
Subject: [PATCH] [wp] fix polymorphic definitions compilation - LogicCompiler:
make sure that return type is computed in the frame - Lang: tau_of_return ->
tau_of_li_type
---
src/plugins/wp/Lang.ml | 6 +-
src/plugins/wp/Lang.mli | 2 +-
src/plugins/wp/LogicCompiler.ml | 89 ++++++++++---------
.../wp/tests/wp_acsl/oracle/poly.res.oracle | 61 +++++++++++++
.../wp_acsl/oracle_qualif/poly.res.oracle | 25 ++++++
src/plugins/wp/tests/wp_acsl/poly.c | 59 ++++++++++++
6 files changed, 198 insertions(+), 44 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle/poly.res.oracle
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/poly.res.oracle
create mode 100644 src/plugins/wp/tests/wp_acsl/poly.c
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index c647b8120ca..91272859fed 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -225,8 +225,8 @@ let rec tau_of_ltype t =
| Ltype _ as b when Logic_const.is_boolean_type b -> Logic.Bool
| Ltype(lt,lts) -> atype lt (List.map tau_of_ltype lts)
-let tau_of_return l =
- match l.l_type with
+let tau_of_li_type ltype =
+ match ltype with
| None -> Logic.Prop
| Some t -> tau_of_ltype t
@@ -420,7 +420,7 @@ and source =
let tau_of_lfun phi ts =
match phi with
- | ACSL f -> tau_of_return f
+ | ACSL f -> tau_of_li_type f.l_type
| CTOR c ->
if c.ctor_type.lt_params = [] then Logic.Data(Atype c.ctor_type,[])
else raise Not_found
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index f39c4ae1d63..4c196d1fa5e 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -158,7 +158,7 @@ val extern_t:
val tau_of_object : c_object -> tau
val tau_of_ctype : typ -> tau
val tau_of_ltype : logic_type -> tau
-val tau_of_return : logic_info -> tau
+val tau_of_li_type : logic_type option -> tau
val tau_of_lfun : lfun -> tau option list -> tau
val tau_of_field : field -> tau
val tau_of_record : field -> tau
diff --git a/src/plugins/wp/LogicCompiler.ml b/src/plugins/wp/LogicCompiler.ml
index 72eaba5ea25..34148ea3695 100644
--- a/src/plugins/wp/LogicCompiler.ml
+++ b/src/plugins/wp/LogicCompiler.ml
@@ -428,6 +428,7 @@ struct
let occurs_ps x ps = List.exists (F.occursp x) ps
let compile_step
+ (tres: logic_type option)
(name:string)
(types:string list)
(profile:logic_var list)
@@ -435,10 +436,11 @@ struct
(cc : env -> 'a -> 'b)
(filter : 'b -> var -> bool)
(data : 'a)
- : var list * trigger list * pred list * 'b * sig_param list =
+ : tau * var list * trigger list * pred list * 'b * sig_param list =
let frame = logic_frame name types in
in_frame frame
begin fun () ->
+ let tres = Lang.tau_of_li_type tres in
let env,domain,sigv = profile_env Logic_var.Map.empty [] [] profile in
let env = default_label env labels in
let result = cc env data in
@@ -464,7 +466,7 @@ struct
(Sigma.domain sigma) acc)
frame.labels (parp,sigp)
in
- parm , frame.triggers , domain , result , sigm
+ tres, parm , frame.triggers , domain , result , sigm
end ()
let cc_term : (env -> Cil_types.term -> term) ref
@@ -505,9 +507,9 @@ struct
let compile_lemma cluster name ~kind types labels lemma =
let qs,prop = strip_forall [] lemma in
- let xs,tgs,domain,prop,_ =
+ let _,xs,tgs,domain,prop,_ =
let cc_pred = pred `Positive in
- compile_step name types qs labels cc_pred in_pred prop in
+ compile_step None name types qs labels cc_pred in_pred prop in
let weak = Wp_parameters.WeakIntModel.get () in
let lemma = if weak then prop else F.p_hyps domain prop in
{
@@ -557,37 +559,45 @@ struct
(* -------------------------------------------------------------------------- *)
let compile_lbpure cluster l =
- let lfun = ACSL l in
- let tau = Lang.tau_of_return l in
- let parp,sigp = Lang.local profile_sig l.l_profile in
- let ldef = {
- d_lfun = lfun ;
- d_types = List.length l.l_tparams ;
- d_params = parp ;
- d_cluster = cluster ;
- d_definition = Logic tau ;
- } in
- Definitions.update_symbol ldef ;
- Signature.update l (SIG sigp) ;
- parp,sigp
+ let frame = logic_frame l.l_var_info.lv_name l.l_tparams in
+ in_frame frame
+ begin fun () ->
+ let lfun = ACSL l in
+ let tau = Lang.tau_of_li_type l.l_type in
+ let parp,sigp = Lang.local profile_sig l.l_profile in
+ let ldef = {
+ d_lfun = lfun ;
+ d_types = List.length l.l_tparams ;
+ d_params = parp ;
+ d_cluster = cluster ;
+ d_definition = Logic tau ;
+ } in
+ Definitions.update_symbol ldef ;
+ Signature.update l (SIG sigp) ;
+ parp,sigp
+ end ()
(* -------------------------------------------------------------------------- *)
(* --- Compiling Abstract Logic Function (in axiomatic with no reads) --- *)
(* -------------------------------------------------------------------------- *)
let compile_lbnone cluster l vars =
- let lfun = ACSL l in
- let tau = Lang.tau_of_return l in
- let parm,sigm = Lang.local (profile_mem l) vars in
- let ldef = {
- d_lfun = lfun ;
- d_types = List.length l.l_tparams ;
- d_params = parm ;
- d_cluster = cluster ;
- d_definition = Logic tau ;
- } in
- Definitions.define_symbol ldef ;
- type_for_signature l ldef sigm ; SIG sigm
+ let frame = logic_frame l.l_var_info.lv_name l.l_tparams in
+ in_frame frame
+ begin fun () ->
+ let lfun = ACSL l in
+ let tau = Lang.tau_of_li_type l.l_type in
+ let parm,sigm = Lang.local (profile_mem l) vars in
+ let ldef = {
+ d_lfun = lfun ;
+ d_types = List.length l.l_tparams ;
+ d_params = parm ;
+ d_cluster = cluster ;
+ d_definition = Logic tau ;
+ } in
+ Definitions.define_symbol ldef ;
+ type_for_signature l ldef sigm ; SIG sigm
+ end ()
(* -------------------------------------------------------------------------- *)
(* --- Compiling Logic Function with Reads --- *)
@@ -596,9 +606,8 @@ struct
let compile_lbreads cluster l ts =
let lfun = ACSL l in
let name = l.l_var_info.lv_name in
- let tau = Lang.tau_of_return l in
- let xs,_,_,(),s =
- compile_step name l.l_tparams l.l_profile l.l_labels
+ let tau,xs,_,_,(),s =
+ compile_step l.l_type name l.l_tparams l.l_profile l.l_labels
reads in_reads ts
in
let ldef = {
@@ -616,15 +625,16 @@ struct
(* -------------------------------------------------------------------------- *)
let compile_rec name l cc filter data =
+ let tau = l.l_type in
let types = l.l_tparams in
let profile = l.l_profile in
let labels = l.l_labels in
- let result = compile_step name types profile labels cc filter data in
+ let result = compile_step tau name types profile labels cc filter data in
if LogicUsage.is_recursive l then
begin
- let (_,_,_,_,s) = result in
+ let (_,_,_,_,_,s) = result in
Signature.update l (SIG s) ;
- compile_step name types profile labels cc filter data
+ compile_step tau name types profile labels cc filter data
end
else result
@@ -634,8 +644,7 @@ struct
let compile_lbterm cluster l t =
let name = l.l_var_info.lv_name in
- let tau = Lang.tau_of_return l in
- let xs,_,_,r,s = compile_rec name l term in_term t in
+ let tau,xs,_,_,r,s = compile_rec name l term in_term t in
match F.repr r with
| Qed.Logic.Kint c -> CST c
| _ ->
@@ -657,7 +666,7 @@ struct
let lfun = ACSL l in
let name = l.l_var_info.lv_name in
let cc_pred = pred `Positive in
- let xs,_,_,r,s = compile_rec name l cc_pred in_pred p in
+ let _,xs,_,_,r,s = compile_rec name l cc_pred in_pred p in
let ldef = {
d_lfun = lfun ;
d_types = List.length l.l_tparams ;
@@ -690,9 +699,9 @@ struct
(* Compile cases with default definition and collect used chunks *)
let support = List.fold_left
(fun support (case,labels,types,lemma) ->
- let _,_,_,_,s =
+ let _,_,_,_,_,s =
let cc_pred = pred `Positive in
- compile_step case types [] labels cc_pred in_pred lemma in
+ compile_step l.l_type case types [] labels cc_pred in_pred lemma in
let labels_used = LogicUsage.get_induction_labels l case in
List.fold_left (heap_case labels_used) support s)
Heap.Map.empty cases in
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/poly.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/poly.res.oracle
new file mode 100644
index 00000000000..57483d894cb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/poly.res.oracle
@@ -0,0 +1,61 @@
+# frama-c -wp [...]
+[kernel] Parsing poly.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Global
+------------------------------------------------------------
+
+Lemma test2_ko:
+Prove: (L_x_bar i_0 s_0)!=(concat (elt i_0) s_0)
+
+------------------------------------------------------------
+
+Lemma test2_ok:
+Prove: (L_x_bar i_0 s_0)=(concat (elt i_0) s_0)
+
+------------------------------------------------------------
+
+Lemma test_ko:
+Prove: (L_bar i_0 s_0)!=(concat (elt i_0) s_0)
+
+------------------------------------------------------------
+
+Lemma test_ok:
+Prove: (L_bar i_0 s_0)=(concat (elt i_0) s_0)
+
+------------------------------------------------------------
+
+Lemma testp2_ko:
+Prove: (L_x_foo a_0 s_0)!=(concat (elt a_0) s_0)
+
+------------------------------------------------------------
+
+Lemma testp2_ok:
+Prove: (L_x_foo a_0 s_0)=(concat (elt a_0) s_0)
+
+------------------------------------------------------------
+
+Lemma testp_ko:
+Prove: (L_foo a_0 s_0)!=(concat (elt a_0) s_0)
+
+------------------------------------------------------------
+
+Lemma testp_ok:
+Prove: (L_foo a_0 s_0)=(concat (elt a_0) s_0)
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function main
+------------------------------------------------------------
+
+Goal Assertion (file poly.c, line 57):
+Prove: P_P(1, [ 1 ]).
+
+------------------------------------------------------------
+
+Goal Assertion (file poly.c, line 58):
+Assume { (* Assertion *) Have: P_P(1, [ 1 ]). }
+Prove: P_Y(1, [ 1 ]).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/poly.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/poly.res.oracle
new file mode 100644
index 00000000000..a807b4a2348
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/poly.res.oracle
@@ -0,0 +1,25 @@
+# frama-c -wp [...]
+[kernel] Parsing poly.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 10 goals scheduled
+[wp] [Unsuccess] typed_check_lemma_test2_ko (Alt-Ergo) (Cached)
+[wp] [Valid] typed_check_lemma_test2_ok (Alt-Ergo) (Cached)
+[wp] [Unsuccess] typed_check_lemma_test_ko (Alt-Ergo) (Cached)
+[wp] [Valid] typed_check_lemma_test_ok (Alt-Ergo) (Cached)
+[wp] [Unsuccess] typed_check_lemma_testp2_ko (Alt-Ergo) (Cached)
+[wp] [Valid] typed_check_lemma_testp2_ok (Alt-Ergo) (Cached)
+[wp] [Unsuccess] typed_check_lemma_testp_ko (Alt-Ergo) (Cached)
+[wp] [Valid] typed_check_lemma_testp_ok (Alt-Ergo) (Cached)
+[wp] [Unsuccess] typed_main_assert (Alt-Ergo) (Cached)
+[wp] [Valid] typed_main_assert_2 (Alt-Ergo) (Cached)
+[wp] Proved goals: 5 / 10
+ Alt-Ergo: 5
+ Unsuccess: 5
+------------------------------------------------------------
+ Axiomatics WP Alt-Ergo Total Success
+ Lemma - 4 8 50.0%
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ main - 1 2 50.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/poly.c b/src/plugins/wp/tests/wp_acsl/poly.c
new file mode 100644
index 00000000000..9ab4bf54c90
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/poly.c
@@ -0,0 +1,59 @@
+/*@ logic \list<A> foo<A> (A i, \list<A> s) = \Cons (i, s);
+
+ logic \list<integer> bar (integer i, \list<integer> s) =
+ foo(i, s);
+
+ check lemma test_ok: \forall integer i; \forall \list<integer> s;
+ bar (i, s) == \Cons (i, s);
+
+ check lemma test_ko: \forall integer i; \forall \list<integer> s;
+ bar (i, s) != \Cons (i, s);
+
+ check lemma testp_ok <A>: \forall A a; \forall \list<A> s;
+ foo (a, s) == \Cons (a, s);
+
+ check lemma testp_ko <A>: \forall A a; \forall \list<A> s;
+ foo (a, s) != \Cons (a, s);
+*/
+
+/*@ axiomatic X {
+ logic \list<A> x_foo<A>(A i, \list<A> s) reads \nothing ;
+ logic \list<integer> x_bar (integer i, \list<integer> s) reads \nothing ;
+
+ axiom x_foo_value<A>:
+ \forall A i, \list<A> s ;
+ x_foo(i, s) == \Cons(i, s) ;
+
+ axiom x_bar_value:
+ \forall integer i, \list<integer> s ;
+ x_bar(i, s) == x_foo(i, s) ;
+ }
+
+ check lemma test2_ok: \forall integer i; \forall \list<integer> s;
+ x_bar (i, s) == \Cons (i, s);
+
+ check lemma test2_ko: \forall integer i; \forall \list<integer> s;
+ x_bar (i, s) != \Cons (i, s);
+
+ check lemma testp2_ok <A>: \forall A a; \forall \list<A> s;
+ x_foo (a, s) == \Cons (a, s);
+
+ check lemma testp2_ko <A>: \forall A a; \forall \list<A> s;
+ x_foo (a, s) != \Cons (a, s);
+*/
+
+/*@ inductive P<A>(A i, \list<A> s){
+ case one<B>:
+ \forall B b, \list<B> s ; \Cons(b, s) == [| b |] ==> P(b, s);
+ }
+*/
+
+/*@ axiomatic Y {
+ predicate Y<A>(A i, \list<A> s);
+ }
+*/
+
+int main(void){
+ //@ assert P(1, [| 1 |]) ;
+ //@ assert Y(1, [| 1 |]) ;
+}
--
GitLab