From 2cb5a77fba7ab2748fd73f4f97c756fcd3fc953f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 25 Jan 2019 16:35:41 +0100
Subject: [PATCH] [WP] create better properties for dynamics
---
src/kernel_services/ast_data/property.ml | 11 ++--
.../ast_printing/description.ml | 3 +
src/plugins/wp/calculus.ml | 24 ++++----
src/plugins/wp/dyncall.ml | 58 +++++++++++--------
src/plugins/wp/dyncall.mli | 8 +--
.../tests/wp_plugin/dynamic.i.0.report.json | 9 ++-
.../tests/wp_plugin/oracle/dynamic.res.oracle | 2 +-
.../oracle_qualif/dynamic.res.oracle | 2 +-
src/plugins/wp/wpAnnot.ml | 10 +---
9 files changed, 69 insertions(+), 58 deletions(-)
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index c1b6a0334b9..5a7c62cbe97 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -858,11 +858,15 @@ module Names = struct
Format.asprintf "%sextended%a" (extended_loc_prefix le) pp_names [name]
| IPCodeAnnot (kf,_, ca) ->
let name = match ca.annot_content with
- | AAssert _ -> "assert"
+ | AAssert _ -> "assert"
| AInvariant (_,true,_) -> "loop_inv"
| AInvariant _ -> "inv"
| APragma _ -> "pragma"
- | _ -> assert false
+ | AStmtSpec _ -> "contract"
+ | AAssigns _ -> "assigns"
+ | AVariant _ -> "variant"
+ | AAllocation _ -> "allocates"
+ | AExtended(_,_,(_,clause,_,_)) -> clause
in Format.asprintf "%s%s%a" (kf_prefix kf) name pp_code_annot_names ca
| IPComplete (kf, ki, a, lb) ->
Format.asprintf "%s%s%acomplete%a"
@@ -1125,7 +1129,7 @@ let ip_property_instance kf stmt ipred iprop =
let ip_of_code_annot kf stmt ca =
let ki = Kstmt stmt in
match ca.annot_content with
- | AAssert _ | AInvariant _ -> [ IPCodeAnnot(kf, stmt, ca) ]
+ | AAssert _ | AInvariant _ | AExtended _ -> [ IPCodeAnnot(kf, stmt, ca) ]
| AStmtSpec (active,s) -> ip_of_spec kf ki active s
| AVariant t -> [ IPDecrease (kf,ki,(Some ca),t) ]
| AAllocation _ ->
@@ -1137,7 +1141,6 @@ let ip_of_code_annot kf stmt ca =
| APragma p when Logic_utils.is_property_pragma p ->
[ IPCodeAnnot (kf,stmt,ca) ]
| APragma _ -> []
- | AExtended _ -> []
let ip_of_code_annot_single kf stmt ca = match ip_of_code_annot kf stmt ca with
| [] ->
diff --git a/src/kernel_services/ast_printing/description.ml b/src/kernel_services/ast_printing/description.ml
index a11da2374c6..00b2d7edd66 100644
--- a/src/kernel_services/ast_printing/description.ml
+++ b/src/kernel_services/ast_printing/description.ml
@@ -260,6 +260,9 @@ let rec pp_prop kfopt kiopt kloc fmt = function
pp_for bs
pp_named np
(pp_kloc kloc) np.pred_loc
+ | IPCodeAnnot(_,stmt,{annot_content=AExtended(bs,_,(_,clause,_,_))}) ->
+ Format.fprintf fmt "%a%a%a"
+ pp_capitalize clause pp_for bs (pp_stmt kloc) stmt
| IPCodeAnnot(_,stmt,_) ->
Format.fprintf fmt "Annotation %a" (pp_stmt kloc) stmt
| IPAllocation(kf,Kglobal,Id_contract (_,bhv),(frees,allocates)) ->
diff --git a/src/plugins/wp/calculus.ml b/src/plugins/wp/calculus.ml
index 39dce31afc8..d93b66804f4 100644
--- a/src/plugins/wp/calculus.ml
+++ b/src/plugins/wp/calculus.ml
@@ -438,7 +438,7 @@ module Cfg (W : Mcfg.S) = struct
then W.call_goal_precond wenv stmt kf args ~pre:(pre_goals) obj
else obj
- let wp_calls ((caller_kf, cfg, strategy, _, wenv)) res v stmt
+ let wp_calls ((_, cfg, strategy, _, wenv)) res v stmt
lval call args p_post p_exit
=
debug "[wp_calls] %a@." Cil2cfg.pp_call_type call;
@@ -451,18 +451,16 @@ module Cfg (W : Mcfg.S) = struct
wp_call_kf wenv cenv stmt lval kf args precond ~p_post ~p_exit
| Cil2cfg.Dynamic fct ->
let bhv = WpStrategy.behavior_name_of_strategy strategy in
- let calls = Dyncall.get ?bhv stmt in
- if calls = [] then
- wp_call_any wenv cenv ~p_post ~p_exit
- else
- let precond = R.is_pass1 res in
- let call kf =
- let wp = wp_call_kf wenv cenv stmt lval
- kf args precond ~p_post ~p_exit in
- kf , wp in
- let prop = Dyncall.property ~kf:caller_kf ?bhv ~stmt ~calls in
- let pid = WpPropId.mk_property prop in
- W.call_dynamic wenv stmt pid fct (List.map call calls)
+ match Dyncall.get ?bhv stmt with
+ | None -> wp_call_any wenv cenv ~p_post ~p_exit
+ | Some (prop,calls) ->
+ let precond = R.is_pass1 res in
+ let do_call kf =
+ let wp = wp_call_kf wenv cenv stmt lval
+ kf args precond ~p_post ~p_exit in
+ kf , wp in
+ let pid = WpPropId.mk_property prop in
+ W.call_dynamic wenv stmt pid fct (List.map do_call calls)
let wp_stmt wenv s obj = match s.skind with
| Return (r, _) -> W.return wenv s r obj
diff --git a/src/plugins/wp/dyncall.ml b/src/plugins/wp/dyncall.ml
index a13a06ebc5f..c7e14a68f6f 100644
--- a/src/plugins/wp/dyncall.ml
+++ b/src/plugins/wp/dyncall.ml
@@ -86,7 +86,7 @@ let pp_calls fmt calls =
module PInfo = struct let module_name = "Dyncall.Point" end
module Point = Datatype.Pair_with_collections(Datatype.String)(Stmt)(PInfo)
-module Calls = Datatype.List(Kernel_function)
+module Calls = Datatype.Pair(Property)(Datatype.List(Kernel_function))
module CInfo =
struct
let name = "Dyncall.CallPoints"
@@ -95,10 +95,12 @@ struct
end
module CallPoints = State_builder.Hashtbl(Point.Hashtbl)(Calls)(CInfo)
-let property ~kf ?bhv ~stmt ~calls =
- let fact = match bhv with
- | None -> Format.asprintf "@[<hov 2>calls%a@]" pp_calls calls
- | Some b -> Format.asprintf "@[<hov 2>calls%a for %s@]" pp_calls calls b
+let property ~kf ~bhv ~stmt calls =
+ let fact =
+ if bhv = Cil.default_behavior_name then
+ Format.asprintf "@[<hov 2>calls%a@]" pp_calls calls
+ else
+ Format.asprintf "@[<hov 2>calls%a for %s@]" pp_calls calls bhv
in
Property.(ip_other fact (OLStmt (kf,stmt)))
@@ -116,6 +118,9 @@ class dyncall =
method count = count
+ method private kf =
+ match self#current_kf with None -> assert false | Some kf -> kf
+
method private stmt =
match self#current_stmt with None -> assert false | Some stmt -> stmt
@@ -128,32 +133,39 @@ class dyncall =
| Cil_types.AExtended (bhvs,_,(_, "calls", _,Ext_terms calls)) ->
if calls <> [] && (scope <> [] || not (Stack.is_empty block_calls))
then begin
+ let kf = self#kf in
let bhvs =
match bhvs with
| [] -> [ Cil.default_behavior_name ]
| bhvs -> bhvs
in
+ let debug_calls bhv stmt kfs =
+ if Wp_parameters.has_dkey dkey_calls then
+ let source = snd (Stmt.loc stmt) in
+ if Cil.default_behavior_name = bhv then
+ Wp_parameters.result ~source
+ "@[<hov 2>Calls%a@]" pp_calls kfs
+ else
+ Wp_parameters.result ~source
+ "@[<hov 2>Calls (for %s)%a@]" bhv pp_calls kfs
+ in
+ let pool = ref [] in (* collect emitted properties *)
let add_calls_info stmt =
count <- succ count ;
List.iter
(fun bhv ->
let kfs = List.map get_call calls in
- begin
- if Wp_parameters.has_dkey dkey_calls then
- let source = snd (Stmt.loc stmt) in
- if Cil.default_behavior_name = bhv then
- Wp_parameters.result ~source
- "@[<hov 2>Calls%a@]" pp_calls kfs
- else
- Wp_parameters.result ~source
- "@[<hov 2>Calls (for %s)%a@]" bhv pp_calls kfs
- end;
- CallPoints.add (bhv,stmt) kfs)
+ debug_calls bhv stmt kfs ;
+ let prop = property ~kf ~bhv ~stmt kfs in
+ pool := prop :: !pool ;
+ CallPoints.add (bhv,stmt) (prop,kfs))
bhvs
in
- if scope <> [] then List.iter add_calls_info scope
- else
- List.iter add_calls_info (Stack.top block_calls)
+ let callpoints =
+ if scope <> [] then scope else Stack.top block_calls in
+ List.iter add_calls_info callpoints ;
+ let annot = Property.ip_of_code_annot_single kf self#stmt ca in
+ ignore (annot,!pool) ;
end;
SkipChildren
| _ -> SkipChildren
@@ -216,15 +228,15 @@ let compute =
let get ?bhv stmt =
compute () ;
let get bhv =
- try CallPoints.find (bhv,stmt)
- with Not_found -> []
+ try Some (CallPoints.find (bhv,stmt))
+ with Not_found -> None
in
match bhv with
| None -> get Cil.default_behavior_name
| Some bhv ->
(match get bhv with
- | [] -> get Cil.default_behavior_name
- | l -> l)
+ | None -> get Cil.default_behavior_name
+ | result -> result)
(* -------------------------------------------------------------------------- *)
(* --- Registry --- *)
diff --git a/src/plugins/wp/dyncall.mli b/src/plugins/wp/dyncall.mli
index 823c5c331be..85678b9f73c 100644
--- a/src/plugins/wp/dyncall.mli
+++ b/src/plugins/wp/dyncall.mli
@@ -24,12 +24,8 @@ open Cil_types
val pp_calls : Format.formatter -> kernel_function list -> unit
-val property : kf:kernel_function -> ?bhv:string -> stmt:stmt ->
- calls:kernel_function list -> Property.t
-(** Returns an property identifier for the precondition. *)
-
-val get : ?bhv:string -> stmt -> kernel_function list
-(** Returns empty list if there is no specified dynamic call. *)
+val get : ?bhv:string -> stmt -> (Property.t * kernel_function list) option
+(** Returns [None] if there is no specified dynamic call. *)
val compute : unit -> unit
(** Forces computation of dynamic calls.
diff --git a/src/plugins/wp/tests/wp_plugin/dynamic.i.0.report.json b/src/plugins/wp/tests/wp_plugin/dynamic.i.0.report.json
index 6f08ea23f4e..a092c5cd51e 100644
--- a/src/plugins/wp/tests/wp_plugin/dynamic.i.0.report.json
+++ b/src/plugins/wp/tests/wp_plugin/dynamic.i.0.report.json
@@ -57,9 +57,12 @@
"wp:main": { "total": 5,
"valid": 5,
"rank": 5 } } },
- "behavior": { "behavior_stmt_calls_h1_h2_for_bhv1":
- { "qed": { "total": 1, "valid": 1 },
- "wp:main": { "total": 1, "valid": 1 } },
+ "behavior": { "behavior_stmt_calls_h1_h2": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
"behavior_bhv1_assign": { "qed": { "total": 6,
"valid": 6 },
"wp:main":
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
index a9538e54c89..80192d5d7d4 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
@@ -17,7 +17,7 @@
Function behavior with behavior bhv1
------------------------------------------------------------
-Goal Calls h1 h2 for bhv1 in 'behavior' at instruction (file tests/wp_plugin/dynamic.i, line 65):
+Goal Calls h1 h2 in 'behavior' at instruction (file tests/wp_plugin/dynamic.i, line 65):
Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
index 219867a51e0..38972927867 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
@@ -5,7 +5,7 @@
[wp] tests/wp_plugin/dynamic.i:78: Warning: Missing 'calls' for default behavior
[wp] Warning: Missing RTE guards
[wp] 51 goals scheduled
-[wp] [Qed] Goal typed_behavior_stmt_calls_h1_h2_for_bhv1 : Valid
+[wp] [Qed] Goal typed_behavior_stmt_calls_h1_h2 : Valid
[wp] [Qed] Goal typed_behavior_bhv1_post_part1 : Valid
[wp] [Qed] Goal typed_behavior_bhv1_post_part2 : Valid
[wp] [Qed] Goal typed_behavior_bhv1_assign_exit_part1 : Valid
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 16a29702a4b..3b92a70d828 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -770,9 +770,8 @@ let get_call_annots config v s fct =
| Cil2cfg.Dynamic _ ->
let bhv = asked_bhv config.cur_bhv in
- let calls = Dyncall.get ?bhv s in
- if calls=[] then
- begin
+ match Dyncall.get ?bhv s with
+ | None | Some(_,[]) ->
Wp_parameters.warning ~once:true ~source:(fst (Stmt.loc s))
"Missing 'calls' for %s"
(match bhv with
@@ -780,13 +779,10 @@ let get_call_annots config v s fct =
| Some b -> b) ;
let annots = WpStrategy.add_call_assigns_any WpStrategy.empty_acc s in
WpStrategy.empty_acc, (annots , annots)
- end
- else
- begin
+ | Some(_,calls) ->
List.fold_left
(fun acc kf -> add_call_annots config s kf l_post acc)
empty calls
- end
(*----------------------------------------------------------------------------*)
let add_variant_annot config s ca var_exp loop_entry loop_back =
--
GitLab