diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 12f47d738bde8c22fc84e36987e7250514c3f6bb..d1e4b57004ff92cc5829c0968b7b6eeb2f95d182 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1680,8 +1680,18 @@ src/plugins/wp/WpTac.ml: CEA_WP
src/plugins/wp/WpTac.mli: CEA_WP
src/plugins/wp/calculus.ml: CEA_WP
src/plugins/wp/calculus.mli: CEA_WP
+src/plugins/wp/cfgAnnot.ml: CEA_WP
+src/plugins/wp/cfgAnnot.mli: CEA_WP
+src/plugins/wp/cfgInfos.ml: CEA_WP
+src/plugins/wp/cfgInfos.mli: CEA_WP
+src/plugins/wp/cfgCalculus.ml: CEA_WP
+src/plugins/wp/cfgCalculus.mli: CEA_WP
src/plugins/wp/cfgDump.ml: CEA_WP
src/plugins/wp/cfgDump.mli: CEA_WP
+src/plugins/wp/cfgGenerator.ml: CEA_WP
+src/plugins/wp/cfgGenerator.mli: CEA_WP
+src/plugins/wp/cfgInit.ml: CEA_WP
+src/plugins/wp/cfgInit.mli: CEA_WP
src/plugins/wp/cfgWP.ml: CEA_WP
src/plugins/wp/cfgWP.mli: CEA_WP
src/plugins/wp/cil2cfg.ml: CEA_WP
@@ -1827,6 +1837,8 @@ src/plugins/wp/wpAnnot.ml: CEA_WP
src/plugins/wp/wpAnnot.mli: CEA_WP
src/plugins/wp/wpContext.ml: CEA_WP
src/plugins/wp/wpContext.mli: CEA_WP
+src/plugins/wp/wpGenerator.ml: CEA_WP
+src/plugins/wp/wpGenerator.mli: CEA_WP
src/plugins/wp/wpPropId.ml: CEA_WP
src/plugins/wp/wpPropId.mli: CEA_WP
src/plugins/wp/wpReached.ml: CEA_WP
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 0cb64d24a9898703c24e347a8161aec4a942904d..506bb221ee18751fb718f5c3806dc5f243890f31 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -370,6 +370,40 @@ let get_behavior = function
| IPGlobalInvariant _
| IPOther _ -> None
+let get_for_behaviors = function
+ | IPPredicate {ip_kind} ->
+ (match get_pk_behavior ip_kind with None -> [] | Some b -> [b.b_name])
+ | IPBehavior {ib_bhv=b}
+ | IPAllocation {ial_bhv=Id_contract (_, b)}
+ | IPAssigns {ias_bhv=Id_contract (_, b)}
+ | IPFrom {if_bhv=Id_contract (_, b)} -> [b.b_name]
+
+ | IPAllocation {ial_bhv=Id_loop ca}
+ | IPAssigns {ias_bhv=Id_loop ca}
+ | IPFrom {if_bhv=Id_loop ca}
+ | IPCodeAnnot { ica_ca = ca } ->
+ begin
+ match ca.annot_content with
+ | AAssert (bhvs,_)
+ | AInvariant (bhvs,_,_)
+ | AStmtSpec(bhvs,_)
+ | AAssigns(bhvs,_)
+ | AAllocation(bhvs,_) -> bhvs
+ | AVariant _ | APragma _ | AExtended _ -> []
+ end
+
+ | IPAxiomatic _
+ | IPExtended _
+ | IPLemma _
+ | IPComplete _
+ | IPDisjoint _
+ | IPDecrease _
+ | IPReachable _
+ | IPPropertyInstance _
+ | IPTypeInvariant _
+ | IPGlobalInvariant _
+ | IPOther _ -> []
+
(* -------------------------------------------------------------------------- *)
(* --- Property Status --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index 8c26d95abc56c6037c5797147a19a3c947abbb0e..531f38e79aab9956d437243fb4ce703c2d043383 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -520,6 +520,7 @@ val get_kinstr: identified_property -> kinstr
val get_kf: identified_property -> kernel_function option
val get_behavior: identified_property -> funbehavior option
val get_names: identified_property -> string list
+val get_for_behaviors: identified_property -> string list
val location: identified_property -> location
(** returns the location of the property.
diff --git a/src/libraries/utils/bag.mli b/src/libraries/utils/bag.mli
index 2b64c202ecd8b0d7e36e2cd9eff1ccf99b736491..d44fc6263cc4e10c300167608ba7e415b8ea3f79 100644
--- a/src/libraries/utils/bag.mli
+++ b/src/libraries/utils/bag.mli
@@ -36,6 +36,7 @@ val concat : 'a t -> 'a t -> 'a t
val map : ('a -> 'b) -> 'a t -> 'b t
val umap : ('a -> 'b t) -> 'a t -> 'b t
+val umap_list : ('a -> 'b t) -> 'a list -> 'b t
val iter : ('a -> unit) -> 'a t -> unit
val fold_left : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b
diff --git a/src/plugins/wp/Factory.mli b/src/plugins/wp/Factory.mli
index eef3a3a7ed5b5d193dc8c3c7b77b2065a129c10d..07df6d8730678c5a7341340e388aafc76db23630 100644
--- a/src/plugins/wp/Factory.mli
+++ b/src/plugins/wp/Factory.mli
@@ -50,3 +50,5 @@ val parse :
Apply specifications to default setup.
Default setup is [Factory.default].
Default warning is [Wp_parameters.abort]. *)
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Generator.ml b/src/plugins/wp/Generator.ml
index 31c18109ae01aec27ceb2ea4fc9c52291c090a14..4b5d51804c65821460d0d5ee8397f6c39468e130 100644
--- a/src/plugins/wp/Generator.ml
+++ b/src/plugins/wp/Generator.ml
@@ -21,106 +21,67 @@
(**************************************************************************)
(* -------------------------------------------------------------------------- *)
-(* --- WP Computer (main entry points) --- *)
+(* --- Model Setup --- *)
(* -------------------------------------------------------------------------- *)
-class type computer =
- object
- method lemma : bool
- method model : WpContext.model
- method add_strategy : WpStrategy.strategy -> unit
- method add_lemma : LogicUsage.logic_lemma -> unit
- method compute : Wpo.t Bag.t
+let user_setup () : Factory.setup =
+ begin
+ match Wp_parameters.Model.get () with
+ | ["Runtime"] ->
+ Wp_parameters.abort
+ "Model 'Runtime' is no more available.@\nIt will be reintroduced \
+ in a future release."
+ | ["Logic"] ->
+ Wp_parameters.warning ~once:true
+ "Deprecated 'Logic' model.@\nUse 'Typed' with option '-wp-ref' \
+ instead." ;
+ {
+ mheap = Factory.Typed MemTyped.Fits ;
+ mvar = Factory.Ref ;
+ cint = Cint.Natural ;
+ cfloat = Cfloat.Real ;
+ }
+ | ["Store"] ->
+ Wp_parameters.warning ~once:true
+ "Deprecated 'Store' model.@\nUse 'Typed' instead." ;
+ {
+ mheap = Factory.Typed MemTyped.Fits ;
+ mvar = Factory.Var ;
+ cint = Cint.Natural ;
+ cfloat = Cfloat.Real ;
+ }
+ | spec -> Factory.parse spec
end
(* -------------------------------------------------------------------------- *)
-(* --- Property Entry Point --- *)
-(* -------------------------------------------------------------------------- *)
-
-let compute_ip cc ip =
- let open Property in match ip with
- | IPLemma _
- | IPAxiomatic _
- ->
- let rec iter cc = function
- | IPLemma {il_name} -> cc#add_lemma (LogicUsage.logic_lemma il_name)
- | IPAxiomatic {iax_props} -> List.iter (iter cc) iax_props
- | _ -> ()
- in iter cc ip ;
- cc#compute
-
- | IPBehavior {ib_kf; ib_bhv} ->
- let model = cc#model in
- let bhv = [ib_bhv.Cil_types.b_name] in
- let assigns = WpAnnot.WithAssigns in
- List.iter cc#add_strategy
- (WpAnnot.get_function_strategies ~model ~assigns ~bhv ib_kf) ;
- cc#compute
- | IPComplete _
- | IPDisjoint _
- | IPCodeAnnot _
- | IPAllocation _
- | IPAssigns _
- | IPDecrease _
- | IPPredicate _
- ->
- let model = cc#model in
- let assigns = WpAnnot.WithAssigns in
- List.iter cc#add_strategy
- (WpAnnot.get_id_prop_strategies ~model ~assigns ip) ;
- cc#compute
-
- | IPFrom _
- | IPReachable _
- | IPPropertyInstance _
- | IPOther _
- | IPTypeInvariant _
- | IPGlobalInvariant _
- | IPExtended _
- ->
- Wp_parameters.result "Nothing to compute for '%a'" pretty ip ;
- Bag.empty
-
-(* -------------------------------------------------------------------------- *)
-(* --- Annotations Entry Point --- *)
+(* --- WP Computer (main entry points) --- *)
(* -------------------------------------------------------------------------- *)
-let add_kf cc ?bhv ?prop kf =
- let model = cc#model in
- let assigns = WpAnnot.WithAssigns in
- List.iter cc#add_strategy
- (WpAnnot.get_function_strategies ~model ~assigns ?bhv ?prop kf)
-
-let add_lemmas cc = function
- | None | Some[] ->
- LogicUsage.iter_lemmas
- (fun lem ->
- let idp = WpPropId.mk_lemma_id lem in
- if WpAnnot.filter_status idp then cc#add_lemma lem)
- | Some ps ->
- if List.mem "-@lemmas" ps then ()
- else LogicUsage.iter_lemmas
- (fun lem ->
- let idp = WpPropId.mk_lemma_id lem in
- if WpAnnot.filter_status idp && WpPropId.select_by_name ps idp
- then cc#add_lemma lem)
-
-let compute_kf cc ?kf ?bhv ?prop () =
- begin
- Option.iter (add_kf cc ?bhv ?prop) kf ;
- cc#compute
- end
-
-let compute_selection cc ?(fct=Wp_parameters.Fct_all) ?bhv ?prop () =
- begin
- add_lemmas cc prop ;
- Wp_parameters.iter_fct (add_kf cc ?bhv ?prop) fct ;
- cc#compute
- end
-
-let compute_call cc stmt =
- let model = cc#model in
- List.iter cc#add_strategy (WpAnnot.get_call_pre_strategies ~model stmt) ;
- cc#compute
+let create
+ ?dump ?legacy
+ ?(setup: Factory.setup option)
+ ?(driver: Factory.driver option)
+ () : Wpo.generator =
+ let default f = function Some v -> v | None -> f () in
+ let dump = default Wp_parameters.Dump.get dump in
+ let legacy = default Wp_parameters.Legacy.get legacy in
+ let driver = default Driver.load_driver driver in
+ let setup = default user_setup setup in
+ if legacy then
+ let cc =
+ if dump
+ then WpGenerator.dumper ()
+ else WpGenerator.computer setup driver in
+ let the_model = cc#model in
+ object
+ method model = the_model
+ method compute_ip = WpGenerator.compute_ip cc
+ method compute_call = WpGenerator.compute_call cc
+ method compute_main = WpGenerator.compute_selection cc
+ end
+ else
+ if dump
+ then CfgGenerator.dumper setup driver
+ else CfgGenerator.generator setup driver
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Generator.mli b/src/plugins/wp/Generator.mli
index 146436a830a12047d91aac938fcdae84481772c2..aead35c64025fcf62bcfaf1a2fee33895da8d4b7 100644
--- a/src/plugins/wp/Generator.mli
+++ b/src/plugins/wp/Generator.mli
@@ -24,28 +24,14 @@
(* --- WP Computer (main entry points) --- *)
(* -------------------------------------------------------------------------- *)
-class type computer =
- object
- method lemma : bool
- method model : WpContext.model
- method add_strategy : WpStrategy.strategy -> unit
- method add_lemma : LogicUsage.logic_lemma -> unit
- method compute : Wpo.t Bag.t
- end
+(** Compute model setup from command line options. *)
+val user_setup : unit -> Factory.setup
-open Wp_parameters
+val create :
+ ?dump:bool ->
+ ?legacy:bool ->
+ ?setup:Factory.setup ->
+ ?driver:Factory.driver ->
+ unit -> Wpo.generator
-val compute_ip : computer -> Property.t -> Wpo.t Bag.t
-val compute_call : computer -> Cil_types.stmt -> Wpo.t Bag.t
-
-val compute_kf : computer ->
- ?kf:Kernel_function.t ->
- ?bhv:string list ->
- ?prop:string list ->
- unit -> Wpo.t Bag.t
-
-val compute_selection : computer ->
- ?fct:functions ->
- ?bhv:string list ->
- ?prop:string list ->
- unit -> Wpo.t Bag.t
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index 114eb12bfb245431031c90822f57624120627395..d78ac2bd27308ea2531701755545426636c607eb 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -96,9 +96,11 @@ PLUGIN_CMO:= \
ProverTask ProverErgo ProverCoq \
filter_axioms Cache ProverWhy3 \
driver prover ProverSearch ProverScript \
- Generator Factory \
+ Factory \
+ cfgInit cfgAnnot cfgInfos cfgCalculus \
calculus cfgDump cfgWP \
- register VC
+ wpGenerator cfgGenerator \
+ Generator register VC
PLUGIN_CMI:=
diff --git a/src/plugins/wp/StmtSemantics.ml b/src/plugins/wp/StmtSemantics.ml
index b9b9e3afead51dd1acc59c9df87845c3affee4fc..b068e462498a28251561510c8acd4ff0fe6a0b6e 100644
--- a/src/plugins/wp/StmtSemantics.ml
+++ b/src/plugins/wp/StmtSemantics.ml
@@ -98,7 +98,7 @@ struct
subst_formals = Varinfo.Map.empty} in
env @* [
Clabels.init, Cfg.node ();
- Clabels.at_exit, Cfg.node();
+ Clabels.exit, Cfg.node();
]
(* -------------------------------------------------------------------------- *)
@@ -380,7 +380,7 @@ struct
@* [Clabels.init, env @: Clabels.init;
Clabels.pre, pre_node; Clabels.here, pre_node;
Clabels.next, post_node; Clabels.post, post_node;
- Clabels.at_exit, env @: Clabels.at_exit]
+ Clabels.exit, env @: Clabels.exit]
in
(* TODO: Call inlining. *)
@@ -391,7 +391,7 @@ struct
@^ result (env_call @* [(Clabels.here, return_node);
(Clabels.next, next_node)])
@^ exit_status (env_call @* [(Clabels.here, exit_stop);
- (Clabels.next, env @: Clabels.at_exit)])
+ (Clabels.next, env @: Clabels.exit)])
and call
: env -> lval option -> exp -> exp list -> paths
@@ -469,7 +469,7 @@ struct
(fun acc post -> acc @^ post_cond Exits post_at_exit_env post)
nop b.b_post_cond
@^ goto post_normal_behavior (env @: Clabels.post)
- @^ goto post_at_exit_behavior (env @: Clabels.at_exit)
+ @^ goto post_at_exit_behavior (env @: Clabels.exit)
in
let env = env @* [Clabels.here, env @: Clabels.pre; Clabels.next, env @: Clabels.post] in
parallel behavior env spec.spec_behavior
diff --git a/src/plugins/wp/VC.ml b/src/plugins/wp/VC.ml
index b614862c03b25b4d5c331c9d165684b08c53ca68..32355d2fc93dbf0e666f73d1439067e66e63d405 100644
--- a/src/plugins/wp/VC.ml
+++ b/src/plugins/wp/VC.ml
@@ -69,24 +69,21 @@ let () = Property_status.register_property_remove_hook remove
(* --- Generator Interface --- *)
(* -------------------------------------------------------------------------- *)
-let generator ?model () =
+let generator model =
let setup = match model with
- | None -> Register.cmdline ()
- | Some s -> Factory.parse [s] in
- let driver = Driver.load_driver () in
- CfgWP.computer setup driver
+ | None -> None
+ | Some s -> Some (Factory.parse [s]) in
+ Generator.create ~dump:false ?setup ()
let generate_ip ?model ip =
- let gen = generator ?model () in
- Generator.compute_ip gen ip
+ (generator model)#compute_ip ip
-let generate_kf ?model ?(bhv=[]) kf =
- let gen = generator ?model () in
- Generator.compute_kf gen ~bhv ~kf ()
+let generate_kf ?model ?bhv ?prop kf =
+ let kfs = Kernel_function.Set.singleton kf in
+ (generator model)#compute_main ~fct:(Fct_list kfs) ?bhv ?prop ()
let generate_call ?model stmt =
- let gen = generator ?model () in
- Generator.compute_call gen stmt
+ (generator model)#compute_call stmt
(* -------------------------------------------------------------------------- *)
(* --- Prover Interface --- *)
diff --git a/src/plugins/wp/VC.mli b/src/plugins/wp/VC.mli
index 3410ae50f5bdf16c0b03bc3497e9f624ed63938d..cc695838ed463262c37bb9832c09892044b7cb10 100644
--- a/src/plugins/wp/VC.mli
+++ b/src/plugins/wp/VC.mli
@@ -66,7 +66,8 @@ val iter_kf : (t -> unit) -> ?bhv:string list -> Kernel_function.t -> unit
*)
val generate_ip : ?model:string -> Property.t -> t Bag.t
-val generate_kf : ?model:string -> ?bhv:string list -> Kernel_function.t -> t Bag.t
+val generate_kf : ?model:string -> ?bhv:string list -> ?prop:string list ->
+ Kernel_function.t -> t Bag.t
val generate_call : ?model:string -> Cil_types.stmt -> t Bag.t
(** {2 Prover Interface} *)
diff --git a/src/plugins/wp/calculus.ml b/src/plugins/wp/calculus.ml
index ffc8d50d665a0fd2302cbada6f80fb395ce1d2ab..5cb2133bb68bc2fac5644b88672b91e7e740947e 100644
--- a/src/plugins/wp/calculus.ml
+++ b/src/plugins/wp/calculus.ml
@@ -76,12 +76,12 @@ module Cfg (W : Mcfg.S) = struct
let add_assigns_hyp wenv obj h_assigns = match h_assigns with
| WpPropId.AssignsLocations (h_id, a) ->
let hid = Some h_id in
- let obj = W.use_assigns wenv a.WpPropId.a_stmt hid a obj in
+ let obj = W.use_assigns wenv hid a obj in
Some a.WpPropId.a_label, obj
| WpPropId.AssignsAny a ->
Wp_parameters.warning ~current:true ~once:true
"Missing assigns clause (assigns 'everything' instead)" ;
- let obj = W.use_assigns wenv a.WpPropId.a_stmt None a obj in
+ let obj = W.use_assigns wenv None a obj in
Some a.WpPropId.a_label, obj
| WpPropId.NoAssignsInfo -> None, obj
@@ -476,7 +476,7 @@ module Cfg (W : Mcfg.S) = struct
| (Set (lv, e, _)) -> W.assign wenv s lv e obj
| (Asm _) ->
let asm = WpPropId.mk_asm_assigns_desc s in
- W.use_assigns wenv asm.WpPropId.a_stmt None asm obj
+ W.use_assigns wenv None asm obj
| (Call _) -> assert false
| Skip _ | Code_annot _ -> obj
end
@@ -617,49 +617,7 @@ module Cfg (W : Mcfg.S) = struct
Cil.CurrentLoc.set old_loc;
res
- let compute_global_init wenv filter obj =
- Globals.Vars.fold_in_file_order
- (fun var initinfo obj ->
- if var.vstorage = Extern then obj else
- let do_init = match filter with
- | `All -> true
- | `InitConst -> WpStrategy.isGlobalInitConst var
- in if not do_init then obj
- else
- let old_loc = Cil.CurrentLoc.get () in
- Cil.CurrentLoc.set var.vdecl ;
- let obj = W.init wenv var initinfo.init obj in
- Cil.CurrentLoc.set old_loc ; obj
- ) obj
-
- let process_global_const wenv obj =
- Globals.Vars.fold_in_file_order
- (fun var _initinfo obj ->
- if WpStrategy.isGlobalInitConst var
- then W.const wenv var obj
- else obj
- ) obj
-
- (* WP of global initializations. *)
- let process_global_init wenv kf obj =
- if WpStrategy.is_main_init kf then
- begin
- let obj = W.label wenv None Clabels.init obj in
- compute_global_init wenv `All obj
- end
- else if W.has_init wenv then
- begin
- let obj =
- if WpStrategy.isInitConst ()
- then process_global_const wenv obj else obj in
- let obj = W.use_assigns wenv None None WpPropId.mk_init_assigns obj in
- let obj = W.label wenv None Clabels.init obj in
- compute_global_init wenv `All obj
- end
- else
- if WpStrategy.isInitConst ()
- then compute_global_init wenv `InitConst obj
- else obj
+ module Init = CfgInit.Make(W)
let get_weakest_precondition cfg ((kf, _g, strategy, res, wenv) as env) =
debug "[wp-cfg] start Pass1";
@@ -670,7 +628,7 @@ module Cfg (W : Mcfg.S) = struct
* but if not, it will only fetch Pass1 result. *)
let e_start = Cil2cfg.start_edge cfg in
let obj = get_wp_edge env e_start in
- let obj = process_global_init wenv kf obj in
+ let obj = Init.process_global_init wenv kf obj in
let obj = match WpStrategy.strategy_kind strategy with
| WpStrategy.SKannots -> obj
| WpStrategy.SKfroms info ->
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
new file mode 100644
index 0000000000000000000000000000000000000000..c837a3ede6ba819838292be5010ca9f7178ac395
--- /dev/null
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -0,0 +1,467 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+(* -------------------------------------------------------------------------- *)
+(* --- Smoke Tests --- *)
+(* -------------------------------------------------------------------------- *)
+
+let smoke kf ~id ?doomed ?unreachable () =
+ WpPropId.mk_smoke kf ~id ?doomed ?unreachable () , Logic_const.pfalse
+
+let get_unreachable kf stmt =
+ WpPropId.mk_smoke kf ~id:"unreachabled" ~unreachable:stmt ()
+
+(* -------------------------------------------------------------------------- *)
+(* --- Memoization --- *)
+(* -------------------------------------------------------------------------- *)
+
+module CodeKey =
+struct
+ type t = kernel_function * stmt
+ let compare (a:t) (b:t) = Stdlib.compare (snd a).sid (snd b).sid
+ let pretty fmt (a:t) = Format.fprintf fmt "s%d" (snd a).sid
+end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Property Accessors : Behaviors --- *)
+(* -------------------------------------------------------------------------- *)
+
+type behavior = {
+ bhv_assumes: WpPropId.pred_info list ;
+ bhv_requires: WpPropId.pred_info list ;
+ bhv_smokes: WpPropId.pred_info list ;
+ bhv_ensures: WpPropId.pred_info list ;
+ bhv_exits: WpPropId.pred_info list ;
+ bhv_post_assigns: WpPropId.assigns_full_info ;
+ bhv_exit_assigns: WpPropId.assigns_full_info ;
+}
+
+let normalize_assumes h =
+ let module L = NormAtLabels in
+ let labels = L.labels_fct_pre in
+ L.preproc_annot labels h
+
+let implies ?assumes p =
+ match assumes with None -> p | Some h -> Logic_const.pimplies (h,p)
+
+let filter ~goal ip =
+ if goal
+ then Logic_utils.verify_predicate ip.ip_content.tp_kind
+ else Logic_utils.use_predicate ip.ip_content.tp_kind
+
+let normalize_pre ~goal kf bhv ?assumes ip =
+ if filter ~goal ip then
+ let module L = NormAtLabels in
+ let labels = L.labels_fct_pre in
+ let id = WpPropId.mk_pre_id kf Kglobal bhv ip in
+ let p = L.preproc_annot labels ip.ip_content.tp_statement in
+ Some (id, implies ?assumes p)
+ else None
+
+let normalize_post ~goal kf bhv tk ?assumes (itk,ip) =
+ if tk = itk && filter ~goal ip then
+ let module L = NormAtLabels in
+ let labels = L.labels_fct_post ~exit:(tk=Exits) in
+ let id = WpPropId.mk_post_id kf Kglobal bhv (tk,ip) in
+ let p = L.preproc_annot labels ip.ip_content.tp_statement in
+ Some (id , implies ?assumes p)
+ else None
+
+let normalize_froms tk froms =
+ let module L = NormAtLabels in
+ let labels = L.labels_fct_assigns ~exit:(tk=Exits) in
+ L.preproc_assigns labels froms
+
+let normalize_fct_assigns kf ~exits bhv = function
+ | WritesAny ->
+ WpPropId.empty_assigns_info, WpPropId.empty_assigns_info
+ | Writes froms ->
+ let make tk =
+ match WpPropId.mk_fct_assigns_id kf exits bhv tk froms with
+ | None -> WpPropId.empty_assigns_info
+ | Some id ->
+ let assigns = normalize_froms tk froms in
+ let desc = WpPropId.mk_kf_assigns_desc assigns in
+ WpPropId.mk_assigns_info id desc
+ in
+ make Normal,
+ if exits then make Exits else WpPropId.empty_assigns_info
+
+let get_behavior_goals kf ?(smoking=false) ?(exits=false) bhv =
+ let pre_cond = normalize_pre ~goal:false kf bhv in
+ let post_cond = normalize_post ~goal:true kf bhv in
+ let p_asgn, e_asgn = normalize_fct_assigns kf ~exits bhv bhv.b_assigns in
+ let smokes =
+ if smoking && bhv.b_requires <> [] then
+ let bname =
+ if Cil.is_default_behavior bhv then "default" else bhv.b_name in
+ let id = bname ^ "_requires" in
+ let doomed = Property.ip_requires_of_behavior kf Kglobal bhv in
+ [smoke kf ~id ~doomed ()]
+ else []
+ in
+ {
+ bhv_assumes = List.filter_map pre_cond bhv.b_assumes;
+ bhv_requires = List.filter_map pre_cond bhv.b_requires;
+ bhv_ensures = List.filter_map (post_cond Normal) bhv.b_post_cond ;
+ bhv_exits = List.filter_map (post_cond Exits) bhv.b_post_cond ;
+ bhv_post_assigns = p_asgn ;
+ bhv_exit_assigns = e_asgn ;
+ bhv_smokes = smokes;
+ }
+
+(* -------------------------------------------------------------------------- *)
+(* --- Side Behavior Requires --- *)
+(* -------------------------------------------------------------------------- *)
+
+let get_requires ~goal kf bhv =
+ List.filter_map (normalize_pre ~goal kf bhv) bhv.b_requires
+
+let get_preconditions ~goal kf =
+ let module L = NormAtLabels in
+ let mk_pre = L.preproc_annot L.labels_fct_pre in
+ List.map
+ (fun bhv ->
+ let p = Ast_info.behavior_precondition ~goal bhv in
+ let ip = Logic_const.new_predicate p in
+ WpPropId.mk_pre_id kf Kglobal bhv ip, mk_pre p
+ ) (Annotations.behaviors kf)
+
+let get_complete_behaviors kf =
+ let spec = Annotations.funspec kf in
+ let module L = NormAtLabels in
+ List.map
+ (fun bs ->
+ WpPropId.mk_compl_bhv_id (kf,Kglobal,[],bs) ,
+ L.preproc_annot L.labels_fct_pre @@ Ast_info.complete_behaviors spec bs
+ ) spec.spec_complete_behaviors
+
+let get_disjoint_behaviors kf =
+ let spec = Annotations.funspec kf in
+ let module L = NormAtLabels in
+ List.map
+ (fun bs ->
+ WpPropId.mk_disj_bhv_id (kf,Kglobal,[],bs) ,
+ L.preproc_annot L.labels_fct_pre @@ Ast_info.disjoint_behaviors spec bs
+ ) spec.spec_disjoint_behaviors
+
+(* -------------------------------------------------------------------------- *)
+(* --- Contracts --- *)
+(* -------------------------------------------------------------------------- *)
+
+type contract = {
+ contract_cond : WpPropId.pred_info list ;
+ contract_hpre : WpPropId.pred_info list ;
+ contract_post : WpPropId.pred_info list ;
+ contract_exit : WpPropId.pred_info list ;
+ contract_smoke : WpPropId.pred_info list ;
+ contract_assigns : Cil_types.assigns ;
+}
+
+let assigns_upper_bound behaviors =
+ let collect_assigns (def, assigns) bhv =
+ (* Default behavior prevails *)
+ if Cil.is_default_behavior bhv then Some bhv.b_assigns, None
+ else if Option.is_some def then def, None
+ else begin
+ (* Note that here, def is None *)
+ match assigns, bhv.b_assigns with
+ | None, a -> None, Some a
+ | Some WritesAny, _ | Some _, WritesAny -> None, Some WritesAny
+ | Some (Writes a), Writes b -> None, Some (Writes (a @ b))
+ end
+ in
+ match List.fold_left collect_assigns (None, None) behaviors with
+ | Some a, _ -> a (* default behavior first *)
+ | _, Some a -> a (* else combined behaviors *)
+ | _ -> WritesAny
+
+(* -------------------------------------------------------------------------- *)
+(* --- Call Contracts --- *)
+(* -------------------------------------------------------------------------- *)
+
+(*TODO: put it in Status_by_call ? *)
+module AllPrecondStatus =
+ State_builder.Hashtbl(Kernel_function.Hashtbl)(Datatype.Unit)
+ (struct
+ let name = "Wp.CfgAnnot.AllPrecondStatus"
+ let dependencies = [Ast.self]
+ let size = 32
+ end)
+
+let setup_preconditions kf =
+ if not (AllPrecondStatus.mem kf) then
+ begin
+ AllPrecondStatus.add kf () ;
+ Statuses_by_call.setup_all_preconditions_proxies kf ;
+ end
+
+let get_precond_at kf stmt (id,p) =
+ let pi = WpPropId.property_of_id id in
+ let pi_at = Statuses_by_call.precondition_at_call kf pi stmt in
+ let id_at = WpPropId.mk_call_pre_id kf stmt pi pi_at in
+ id_at , p
+
+module CallContract = WpContext.StaticGenerator(Kernel_function)
+ (struct
+ type key = kernel_function
+ type data = contract
+ let name = "Wp.CfgAnnot.CallContract"
+ let compile kf =
+ let wcond : WpPropId.pred_info list ref = ref [] in
+ let whpre : WpPropId.pred_info list ref = ref [] in
+ let wpost : WpPropId.pred_info list ref = ref [] in
+ let wexit : WpPropId.pred_info list ref = ref [] in
+ let add w f x = match f x with Some y -> w := y :: !w | None -> () in
+ let behaviors = Annotations.behaviors kf in
+ setup_preconditions kf ;
+ List.iter
+ begin fun bhv ->
+ let assumes = normalize_assumes (Ast_info.behavior_assumes bhv) in
+ let mk_cond = normalize_pre ~goal:true kf bhv ~assumes in
+ let mk_hpre = normalize_pre ~goal:false kf bhv ~assumes in
+ let mk_post = normalize_post ~goal:false kf bhv ~assumes in
+ List.iter (add wcond @@ mk_cond) bhv.b_requires ;
+ List.iter (add whpre @@ mk_hpre) bhv.b_requires ;
+ List.iter (add wpost @@ mk_post Normal) bhv.b_post_cond ;
+ List.iter (add wexit @@ mk_post Exits) bhv.b_post_cond ;
+ end behaviors ;
+ {
+ contract_cond = List.rev !wcond ;
+ contract_hpre = List.rev !whpre ;
+ contract_post = List.rev !wpost ;
+ contract_exit = List.rev !wexit ;
+ contract_smoke = [] ;
+ contract_assigns = assigns_upper_bound behaviors
+ }
+ end)
+
+let get_call_contract ?smoking kf stmt =
+ let cc = CallContract.get kf in
+ let preconds = List.map (get_precond_at kf stmt) cc.contract_cond in
+ match smoking with
+ | None ->
+ { cc with contract_cond = preconds }
+ | Some s ->
+ let g = smoke kf ~id:"dead_call" ~unreachable:s () in
+ { cc with contract_cond = preconds ; contract_smoke = [ g ] }
+
+(* -------------------------------------------------------------------------- *)
+(* --- Assembly Code --- *)
+(* -------------------------------------------------------------------------- *)
+
+let is_assembly stmt =
+ match stmt.skind with
+ | Instr (Asm _) -> true
+ | _ -> false
+
+let get_stmt_assigns kf stmt =
+ let asgn =
+ Annotations.fold_code_annot
+ begin fun _emitter ca l ->
+ match ca.annot_content with
+ | AStmtSpec(fors,s) ->
+ List.fold_left
+ (fun l bhv ->
+ match bhv.b_assigns with
+ | WritesAny -> l
+ | Writes froms ->
+ let module L = NormAtLabels in
+ let labels = L.labels_stmt_assigns ~kf stmt in
+ match
+ WpPropId.mk_stmt_assigns_id kf stmt fors bhv froms
+ with
+ | None -> l
+ | Some id ->
+ let froms = L.preproc_assigns labels froms in
+ let desc = WpPropId.mk_stmt_assigns_desc stmt froms in
+ WpPropId.mk_assigns_info id desc :: l
+ ) l s.spec_behavior
+ | _ -> l
+ end stmt []
+ in if asgn = [] then [WpPropId.empty_assigns_info] else asgn
+
+(* -------------------------------------------------------------------------- *)
+(* --- Code Assertions --- *)
+(* -------------------------------------------------------------------------- *)
+
+type code_assertions = {
+ code_admitted: WpPropId.pred_info list ;
+ code_verified: WpPropId.pred_info list ;
+}
+
+let reverse_code_assertions a = {
+ code_admitted = List.rev a.code_admitted ;
+ code_verified = List.rev a.code_verified ;
+}
+
+module CodeAssertions = WpContext.StaticGenerator(CodeKey)
+ (struct
+ type key = CodeKey.t
+ type data = code_assertions
+ let name = "Wp.CfgAnnot.CodeAssertions"
+ let compile (kf,stmt) =
+ let labels = NormAtLabels.labels_assert ~kf stmt in
+ let normalize_pred p = NormAtLabels.preproc_annot labels p in
+ reverse_code_assertions @@
+ Annotations.fold_code_annot
+ begin fun _emitter ca l ->
+ match ca.annot_content with
+ | AStmtSpec _ when not @@ is_assembly stmt ->
+ let source = fst (Cil_datatype.Stmt.loc stmt) in
+ Wp_parameters.warning ~once:true ~source
+ "Statement specifications not yet supported (skipped)." ; l
+ | AInvariant(_,false,_) ->
+ let source = fst (Cil_datatype.Stmt.loc stmt) in
+ Wp_parameters.warning ~once:true ~source
+ "Generalized invariant not yet supported (skipped)." ; l
+ | AAssert(_,a) ->
+ let p =
+ WpPropId.mk_assert_id kf stmt ca ,
+ normalize_pred a.tp_statement in
+ let admit = Logic_utils.use_predicate a.tp_kind in
+ let verif = Logic_utils.verify_predicate a.tp_kind in
+ let use flag p ps = if flag then p::ps else ps in
+ {
+ code_admitted = use admit p l.code_admitted ;
+ code_verified = use verif p l.code_verified ;
+ }
+ | _ -> l
+ end stmt {
+ code_admitted = [];
+ code_verified = [];
+ }
+ end)
+
+let get_code_assertions ?(smoking=false) kf stmt =
+ let ca = CodeAssertions.get (kf,stmt) in
+ if smoking then
+ let s = smoke kf ~id:"dead_code" ~unreachable:stmt () in
+ { ca with code_verified = s :: ca.code_verified }
+ else ca
+
+(* -------------------------------------------------------------------------- *)
+(* --- Loop Invariants --- *)
+(* -------------------------------------------------------------------------- *)
+
+type loop_contract = {
+ (* to be verified at loop entry *)
+ loop_established: WpPropId.pred_info list;
+ (* to be assumed for loop current *)
+ loop_invariants: WpPropId.pred_info list;
+ (* to be proved after loop invariants *)
+ loop_smoke: WpPropId.pred_info list;
+ (* to be verified after loop body *)
+ loop_preserved: WpPropId.pred_info list;
+ (* assigned by loop body *)
+ loop_assigns: WpPropId.assigns_full_info list;
+}
+
+let reverse_loop_contract l = {
+ loop_established = List.rev l.loop_established ;
+ loop_invariants = List.rev l.loop_invariants ;
+ loop_preserved = List.rev l.loop_preserved ;
+ loop_assigns = List.rev l.loop_assigns ;
+ loop_smoke = List.rev l.loop_smoke ;
+}
+
+let default_assigns stmt l =
+ { l with
+ loop_assigns =
+ if l.loop_assigns <> [] then l.loop_assigns
+ else [WpPropId.mk_loop_any_assigns_info stmt] }
+
+module LoopContract = WpContext.StaticGenerator(CodeKey)
+ (struct
+ type key = CodeKey.t
+ type data = loop_contract
+ let name = "Wp.CfgAnnot.LoopContract"
+ let compile (kf,stmt) =
+ let labels = NormAtLabels.labels_loop stmt in
+ let normalize_pred p = NormAtLabels.preproc_annot labels p in
+ let normalize_annot (i,p) = i, normalize_pred p in
+ let normalize_assigns w = NormAtLabels.preproc_assigns labels w in
+ default_assigns stmt @@
+ reverse_loop_contract @@
+ Annotations.fold_code_annot
+ begin fun _emitter ca l ->
+ match ca.annot_content with
+ | AInvariant(_,true,inv) ->
+ let p = normalize_pred inv.tp_statement in
+ let g_hyp = WpPropId.mk_inv_hyp_id kf stmt ca in
+ let g_est, g_ind = WpPropId.mk_loop_inv kf stmt ca in
+ let admit = Logic_utils.use_predicate inv.tp_kind in
+ let verif = Logic_utils.verify_predicate inv.tp_kind in
+ let use flag id p ps = if flag then (id,p) :: ps else ps in
+ { l with
+ loop_established = use verif g_est p l.loop_established ;
+ loop_invariants = use admit g_hyp p l.loop_invariants ;
+ loop_preserved = use verif g_ind p l.loop_preserved ;
+ }
+ | AVariant(term, None) ->
+ let vpos , vdec =
+ WpStrategy.mk_variant_properties kf stmt ca term in
+ { l with loop_preserved =
+ normalize_annot vdec ::
+ normalize_annot vpos ::
+ l.loop_preserved }
+ | AAssigns(_,WritesAny) ->
+ let asgn = WpPropId.mk_loop_any_assigns_info stmt in
+ { l with loop_assigns = asgn :: l.loop_assigns }
+ | AAssigns(_,Writes w) ->
+ begin match WpPropId.mk_loop_assigns_id kf stmt ca w with
+ | None -> l (* shall not occur *)
+ | Some id ->
+ let w = normalize_assigns w in
+ let a = WpPropId.mk_loop_assigns_desc stmt w in
+ let asgn = WpPropId.mk_assigns_info id a in
+ { l with loop_assigns = asgn :: l.loop_assigns }
+ end
+ | _ -> l
+ end stmt {
+ loop_established = [] ;
+ loop_invariants = [] ;
+ loop_preserved = [] ;
+ loop_smoke = [] ;
+ loop_assigns = [] ;
+ }
+ end)
+
+let get_loop_contract ?(smoking=false) kf stmt =
+ let lc = LoopContract.get (kf,stmt) in
+ if smoking && not (WpReached.is_dead_code stmt) then
+ let g = smoke kf ~id:"dead_loop" ~unreachable:stmt () in
+ { lc with loop_smoke = g :: lc.loop_smoke }
+ else lc
+
+(* -------------------------------------------------------------------------- *)
+(* --- Clear Tablesnts --- *)
+(* -------------------------------------------------------------------------- *)
+
+let clear () =
+ CallContract.clear () ;
+ LoopContract.clear () ;
+ CodeAssertions.clear ()
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgAnnot.mli b/src/plugins/wp/cfgAnnot.mli
new file mode 100644
index 0000000000000000000000000000000000000000..1ca50e9f0ce2ca26a0462d03491ae619278641dd
--- /dev/null
+++ b/src/plugins/wp/cfgAnnot.mli
@@ -0,0 +1,115 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+open WpPropId
+
+(** Normalization of Annotations.
+
+ Labels are renamed wrt NormAtLabels and reorganized for use/prove
+ dispatching in [CfgCalculus]. *)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Property Accessors : Behaviors --- *)
+(* -------------------------------------------------------------------------- *)
+
+type behavior = {
+ bhv_assumes: pred_info list ;
+ bhv_requires: pred_info list ;
+ bhv_smokes: pred_info list ;
+ bhv_ensures: pred_info list ;
+ bhv_exits: pred_info list ;
+ bhv_post_assigns: assigns_full_info ;
+ bhv_exit_assigns: assigns_full_info ;
+}
+
+val get_requires :
+ goal:bool -> kernel_function -> funbehavior -> pred_info list
+
+val get_preconditions :
+ goal:bool -> kernel_function -> pred_info list
+
+val get_behavior_goals :
+ kernel_function ->
+ ?smoking:bool -> ?exits:bool ->
+ funbehavior -> behavior
+
+val get_complete_behaviors : kernel_function -> pred_info list
+val get_disjoint_behaviors : kernel_function -> pred_info list
+
+(* -------------------------------------------------------------------------- *)
+(* --- Property Accessors : Assertions --- *)
+(* -------------------------------------------------------------------------- *)
+
+type code_assertions = {
+ code_admitted: pred_info list ;
+ code_verified: pred_info list ;
+}
+
+val get_code_assertions :
+ ?smoking:bool -> kernel_function -> stmt -> code_assertions
+
+val get_unreachable : kernel_function -> stmt -> prop_id
+val get_stmt_assigns : kernel_function -> stmt -> assigns_full_info list
+
+(* -------------------------------------------------------------------------- *)
+(* --- Property Accessors : Loop Contracts --- *)
+(* -------------------------------------------------------------------------- *)
+
+type loop_contract = {
+ (** to be verified at loop entry *)
+ loop_established: pred_info list;
+ (** to be assumed for loop current *)
+ loop_invariants: pred_info list;
+ (** to be proved after loop invariants *)
+ loop_smoke: pred_info list;
+ (** to be verified after loop body *)
+ loop_preserved: pred_info list;
+ (** assigned by loop body *)
+ loop_assigns: assigns_full_info list;
+}
+
+val get_loop_contract : ?smoking:bool ->
+ kernel_function -> stmt -> loop_contract
+
+(* -------------------------------------------------------------------------- *)
+(* --- Property Accessors : Call Contracts --- *)
+(* -------------------------------------------------------------------------- *)
+
+type contract = {
+ contract_cond : pred_info list ;
+ contract_hpre : pred_info list ;
+ contract_post : pred_info list ;
+ contract_exit : pred_info list ;
+ contract_smoke : pred_info list ;
+ contract_assigns : assigns ;
+}
+
+val get_call_contract : ?smoking:stmt -> kernel_function -> stmt -> contract
+
+(* -------------------------------------------------------------------------- *)
+(* --- Clear Tablesnts --- *)
+(* -------------------------------------------------------------------------- *)
+
+val clear : unit -> unit
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
new file mode 100644
index 0000000000000000000000000000000000000000..697b3eb75e3b8dd4b7f3aa1ce01b892aa447453c
--- /dev/null
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -0,0 +1,417 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+open Cil_datatype
+
+(* -------------------------------------------------------------------------- *)
+(* --- Automata Helpers --- *)
+(* -------------------------------------------------------------------------- *)
+
+module WpLog = Wp_parameters
+module Kf = Kernel_function
+module Cfg = Interpreted_automata
+module G = Cfg.G
+module V = Cfg.Vertex
+module Vhash = V.Hashtbl
+type vertex = Cfg.vertex
+type assigns = WpPropId.assigns_full_info
+
+(* -------------------------------------------------------------------------- *)
+(* --- Calculus Modes (passes) --- *)
+(* -------------------------------------------------------------------------- *)
+
+type mode = {
+ kf: kernel_function;
+ bhv : funbehavior ;
+ infos : CfgInfos.t ;
+}
+
+type props = [ `All | `Names of string list | `PropId of Property.t ]
+
+let default_requires mode kf =
+ if Cil.is_default_behavior mode.bhv then [] else
+ try
+ let bhv = List.find Cil.is_default_behavior (Annotations.behaviors kf) in
+ CfgAnnot.get_requires ~goal:false kf bhv
+ with Not_found -> []
+
+(* -------------------------------------------------------------------------- *)
+(* --- Property Selection by Mode --- *)
+(* -------------------------------------------------------------------------- *)
+
+let is_default_bhv (m: mode) = Cil.is_default_behavior m.bhv
+
+let is_selected_bhv (m: mode) (bhv: funbehavior) =
+ m.bhv.b_name = bhv.b_name
+
+let is_selected_for (m: mode) ~goal (fors: string list) =
+ (fors=[] && (not goal || is_default_bhv m)) ||
+ List.mem m.bhv.b_name fors
+
+let is_selected_ca (m: mode) ~goal (ca: code_annotation) =
+ match ca.annot_content with
+ | AAssigns(forb,_)
+ | AAllocation(forb,_)
+ | AAssert(forb,_)
+ | AInvariant(forb,_,_)
+ -> is_selected_for m ~goal forb
+ | AVariant _ -> is_default_bhv m
+ | AExtended _ | AStmtSpec _ | APragma _ ->
+ assert false (* n/a *)
+
+let is_active_mode ~mode ~goal (p: Property.t) =
+ let open Property in
+ match p with
+ | IPCodeAnnot { ica_ca } -> is_selected_ca mode ~goal ica_ca
+ | IPPredicate { ip_kind } ->
+ begin match ip_kind with
+ | PKRequires _ | PKAssumes _ -> true
+ | PKEnsures(bhv,_) -> is_selected_bhv mode bhv
+ | PKTerminates -> is_default_bhv mode
+ end
+ | IPAllocation { ial_bhv = bhv } | IPAssigns { ias_bhv = bhv } ->
+ begin match bhv with
+ | Id_loop ca -> is_selected_ca mode ~goal ca
+ | Id_contract(_,bhv) -> is_selected_bhv mode bhv
+ end
+ | IPDecrease { id_ca = None } -> is_default_bhv mode
+ | IPDecrease { id_ca = Some ca } -> is_selected_ca mode ~goal ca
+ | IPComplete _ | IPDisjoint _ -> is_default_bhv mode
+ | IPOther _ -> true
+ | IPFrom _ | IPGlobalInvariant _ | IPTypeInvariant _
+ | IPAxiomatic _ | IPLemma _
+ | IPExtended _ | IPBehavior _
+ | IPReachable _ | IPPropertyInstance _
+ -> assert false (* n/a *)
+
+let is_selected_props (props : props) ?pi pid =
+ WpPropId.filter_status pid &&
+ match props with
+ | `All | `Names [] -> WpPropId.select_default pid
+ | `Names ps -> WpPropId.select_by_name ps pid
+ | `PropId p ->
+ Property.equal p @@ match pi with
+ | Some q -> q
+ | None -> WpPropId.property_of_id pid
+
+let rec factorize ~wdefault = function
+ | (_,w)::wcs when w==wdefault -> factorize ~wdefault wcs
+ | (e,w)::wcs -> collect ~wdefault [e] w wcs
+ | [] -> []
+and collect ~wdefault rs wr = function
+ | (e,w)::wcs when w==wr -> collect ~wdefault (e::rs) wr wcs
+ | wcs -> (List.rev rs,wr) :: factorize ~wdefault wcs
+
+(* -------------------------------------------------------------------------- *)
+(* --- WP Calculus Driver from Interpreted Automata --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Make(W : Mcfg.S) =
+struct
+
+ module I = CfgInit.Make(W)
+
+ (* --- Traversal Environment --- *)
+
+ type env = {
+ mode: mode;
+ props: props;
+ body: Cfg.automaton option;
+ succ: Cfg.vertex -> Cfg.G.edge list;
+ dead: stmt -> bool ;
+ we: W.t_env;
+ wp: W.t_prop option Vhash.t; (* None is used for non-dag detection *)
+ mutable wk: W.t_prop; (* end point *)
+ }
+
+ exception NonNaturalLoop of location
+
+ (* --- Annotation Helpers --- *)
+
+ let fmerge env f = function
+ | [] -> W.empty
+ | [x] -> f x
+ | x::xs ->
+ let cup = W.merge env.we in
+ List.fold_left (fun p y -> cup (f y) p) (f x) xs
+
+ let is_selected ~goal { mode ; props } (pid,_) =
+ let pi = WpPropId.property_of_id pid in
+ is_active_mode ~mode ~goal pi &&
+ ( not goal || is_selected_props props ~pi pid )
+
+ let is_selected_callpre { props } (pid,_) =
+ is_selected_props props pid
+
+ let use_assigns env (a : assigns) w =
+ match a with
+ | NoAssignsInfo -> assert false
+ | AssignsAny ad ->
+ WpLog.warning ~current:true ~once:true
+ "Missing assigns clause (assigns 'everything' instead)" ;
+ W.use_assigns env.we None ad w
+ | AssignsLocations(ap,ad) -> W.use_assigns env.we (Some ap) ad w
+
+ let prove_assigns env (a : assigns) w =
+ match a with
+ | NoAssignsInfo | AssignsAny _ -> w
+ | AssignsLocations ai ->
+ if is_selected ~goal:true env ai
+ then W.add_assigns env.we ai w
+ else w
+
+ let use_property env (p : WpPropId.pred_info) w =
+ if is_selected ~goal:false env p then W.add_hyp env.we p w else w
+
+ let prove_property env (p : WpPropId.pred_info) w =
+ if is_selected ~goal:true env p then W.add_goal env.we p w else w
+
+ (* --- Decomposition of WP Rules --- *)
+
+ let rec wp (env:env) (a:vertex) : W.t_prop =
+ match Vhash.find env.wp a with
+ | None -> raise (NonNaturalLoop (Cil.CurrentLoc.get()));
+ | Some pi -> pi
+ | exception Not_found ->
+ (* cut circularities *)
+ Vhash.add env.wp a None ;
+ let pi = match a.vertex_start_of with
+ | None -> successors env a
+ | Some s -> stmt env a s
+ in Vhash.replace env.wp a (Some pi) ; pi
+
+ (* Compute a stmt node *)
+ and stmt env a (s: stmt) : W.t_prop =
+ let kl = Cil.CurrentLoc.get () in
+ try
+ Cil.CurrentLoc.set (Stmt.loc s) ;
+ let smoking =
+ is_default_bhv env.mode && env.dead s in
+ let ca = CfgAnnot.get_code_assertions ~smoking env.mode.kf s in
+ let pi =
+ W.label env.we (Some s) (Clabels.stmt s) @@
+ List.fold_right (prove_property env) ca.code_verified @@
+ List.fold_right (use_property env) ca.code_admitted @@
+ control env a s
+ in
+ Cil.CurrentLoc.set kl ; pi
+ with err ->
+ Cil.CurrentLoc.set kl ; raise err
+
+ (* Branching wrt control-flow *)
+ and control env a s : W.t_prop =
+ match a.vertex_control with
+ | If { cond ; vthen ; velse } ->
+ let wthen = wp env vthen in
+ let welse = wp env velse in
+ W.test env.we s cond wthen welse
+ | Switch { value ; cases ; default } ->
+ let wcases = List.map (fun (e,v) -> e,wp env v) cases in
+ let wdefault = wp env default in
+ W.switch env.we s value (factorize ~wdefault wcases) wdefault
+ | Loop _ ->
+ let m = env.mode in
+ let smoking =
+ is_default_bhv m &&
+ WpLog.SmokeTests.get () &&
+ WpLog.SmokeDeadloop.get () in
+ loop env a s (CfgAnnot.get_loop_contract ~smoking m.kf s)
+ | Edges -> successors env a
+
+ (* Compute loops *)
+ and loop env a s (lc : CfgAnnot.loop_contract) : W.t_prop =
+ List.fold_right (prove_property env) lc.loop_established @@
+ List.fold_right (use_assigns env) lc.loop_assigns @@
+ W.label env.we None (Clabels.loop_current s) @@
+ List.fold_right (use_property env) lc.loop_invariants @@
+ List.fold_right (prove_property env) lc.loop_smoke @@
+ let q =
+ List.fold_right (prove_property env) lc.loop_preserved @@
+ List.fold_right (prove_assigns env) lc.loop_assigns @@
+ W.empty in
+ ( Vhash.replace env.wp a (Some q) ; successors env a )
+
+ (* Merge transitions *)
+ and successors env (a : vertex) = transitions env (env.succ a)
+ and transitions env (es : G.edge list) = fmerge env (transition env) es
+ and transition env (_,edge,dst) : W.t_prop =
+ let p = wp env dst in
+ match edge.edge_transition with
+ | Skip -> p
+ | Return(r,s) -> W.return env.we s r p
+ | Enter { blocals=[] } | Leave { blocals=[] } -> p
+ | Enter { blocals=xs } -> W.scope env.we xs SC_Block_in p
+ | Leave { blocals=xs } -> W.scope env.we xs SC_Block_out p
+ | Instr (i,s) -> instr env s i p
+ | Prop _ | Guard _ -> (* soundly ignored *) p
+
+ (* Compute a single instruction *)
+ and instr env s instr (w : W.t_prop) : W.t_prop =
+ match instr with
+ | Skip _ | Code_annot _ -> w
+ | Set(lv,e,_) -> W.assign env.we s lv e w
+ | Local_init(x,AssignInit i,_) -> W.init env.we x (Some i) w
+ | Local_init(x,ConsInit (vf, args, kind), loc) ->
+ Cil.treat_constructor_as_func
+ begin fun r fct args _loc ->
+ match Kf.get_called fct with
+ | Some kf -> call env s r kf args w
+ | None ->
+ WpLog.warning ~once:true "No function for constructor '%s'"
+ vf.vname ;
+ let any = WpPropId.mk_stmt_assigns_any_desc s in
+ W.use_assigns env.we None any (W.merge env.we w env.wk)
+ end x vf args kind loc
+ | Call(res,fct,args,_loc) ->
+ begin
+ match Kf.get_called fct with
+ | Some kf -> call env s res kf args w
+ | None ->
+ match Dyncall.get ~bhv:env.mode.bhv.b_name s with
+ | None ->
+ WpLog.warning ~once:true "Missing 'calls' for %s"
+ (if Cil.is_default_behavior env.mode.bhv
+ then "default behavior"
+ else env.mode.bhv.b_name) ;
+ let any = WpPropId.mk_stmt_assigns_any_desc s in
+ W.use_assigns env.we None any (W.merge env.we w env.wk)
+ | Some(prop,kfs) ->
+ let id = WpPropId.mk_property prop in
+ W.call_dynamic env.we s id fct @@
+ List.map (fun kf -> kf, call env s res kf args w) kfs
+ end
+ | Asm _ ->
+ let assigns = CfgAnnot.get_stmt_assigns env.mode.kf s in
+ List.fold_right (use_assigns env) assigns w
+
+ and call env s r kf es wr : W.t_prop =
+ let smoking =
+ if is_default_bhv env.mode &&
+ WpLog.SmokeTests.get () &&
+ WpLog.SmokeDeadcall.get ()
+ then Some s else None in
+ let c = CfgAnnot.get_call_contract ?smoking kf s in
+ let p_post = List.fold_right (prove_property env) c.contract_smoke wr in
+ let p_exit = List.fold_right (prove_property env) c.contract_smoke env.wk in
+ let w_call = W.call env.we s r kf es
+ ~pre:c.contract_hpre
+ ~post:c.contract_post
+ ~pexit:c.contract_exit
+ ~assigns:c.contract_assigns
+ ~p_post ~p_exit in
+ if is_default_bhv env.mode then
+ let pre = List.filter (is_selected_callpre env) c.contract_cond in
+ W.call_goal_precond env.we s kf es ~pre w_call
+ else w_call
+
+ let do_complete_disjoint env w =
+ if not (is_default_bhv env.mode) then w
+ else
+ let kf = env.mode.kf in
+ let complete = CfgAnnot.get_complete_behaviors kf in
+ let disjoint = CfgAnnot.get_disjoint_behaviors kf in
+ List.fold_right (prove_property env) complete @@
+ List.fold_right (prove_property env) disjoint w
+
+ let do_global_init env w =
+ I.process_global_init env.we env.mode.kf @@
+ W.scope env.we [] SC_Global w
+
+ let do_preconditions env ~formals (b : CfgAnnot.behavior) w =
+ let kf = env.mode.kf in
+ let init = WpStrategy.is_main_init kf in
+ let side_behaviors =
+ if init || WpLog.PrecondWeakening.get () then []
+ else CfgAnnot.get_preconditions ~goal:false kf in
+ let requires_init = if init then b.bhv_requires else [] in
+ (* pre-state *)
+ W.label env.we None Clabels.pre @@
+ (* pre-conditions *)
+ List.fold_right (use_property env) (default_requires env.mode kf) @@
+ List.fold_right (use_property env) b.bhv_assumes @@
+ List.fold_right (prove_property env) requires_init @@
+ List.fold_right (use_property env) b.bhv_requires @@
+ List.fold_right (prove_property env) b.bhv_smokes @@
+ List.fold_right (use_property env) side_behaviors @@
+ (* frame-in *)
+ W.scope env.we formals SC_Frame_in w
+
+
+ let do_post env ~formals (b : CfgAnnot.behavior) w =
+ W.label env.we None Clabels.post @@
+ W.scope env.we formals SC_Frame_out @@
+ List.fold_right (prove_property env) b.bhv_ensures @@
+ prove_assigns env b.bhv_post_assigns w
+
+ let do_exit env ~formals (b : CfgAnnot.behavior) w =
+ W.label env.we None Clabels.exit @@
+ W.scope env.we formals SC_Frame_out @@
+ List.fold_right (prove_property env) b.bhv_exits @@
+ prove_assigns env b.bhv_exit_assigns w
+
+ let do_funbehavior env ~formals ~exits (b:CfgAnnot.behavior) w =
+ match env.body with
+ | None -> w
+ | Some cfg ->
+ let wpost = do_post env ~formals b w in
+ Vhash.add env.wp cfg.return_point (Some wpost) ;
+ env.wk <- if exits then do_exit env ~formals b w else w ;
+ wp env cfg.entry_point
+
+ (* Putting everything together *)
+ let compute ~mode ~props =
+ let kf = mode.kf in
+ let infos = mode.infos in
+ let body = CfgInfos.body infos in
+ let succ = match body with
+ | None -> (fun _ -> [])
+ | Some cfg -> Cfg.G.succ_e cfg.graph in
+ let dead =
+ if body <> None &&
+ is_default_bhv mode &&
+ WpLog.SmokeTests.get () &&
+ WpLog.SmokeDeadcode.get ()
+ then CfgInfos.smoking infos else (fun _ -> false) in
+ let env = {
+ mode ; props ; body ;
+ succ ; dead ;
+ we = W.new_env kf ;
+ wp = Vhash.create 32 ;
+ wk = W.empty ;
+ } in
+ let formals = Kf.get_formals kf in
+ let exits = not @@ Kf.Set.is_empty @@ CfgInfos.calls infos in
+ let smoking = WpLog.SmokeTests.get () in
+ let bhv = CfgAnnot.get_behavior_goals kf ~smoking ~exits mode.bhv in
+ begin
+ W.close env.we @@
+ do_global_init env @@
+ do_preconditions env ~formals bhv @@
+ do_complete_disjoint env @@
+ do_funbehavior env ~formals ~exits bhv @@
+ W.empty
+ end
+
+end
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgCalculus.mli b/src/plugins/wp/cfgCalculus.mli
new file mode 100644
index 0000000000000000000000000000000000000000..a43c14feae502803d2963d3de10f4f0b5e70eab9
--- /dev/null
+++ b/src/plugins/wp/cfgCalculus.mli
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+(* -------------------------------------------------------------------------- *)
+(* --- WP Calculus Driver from Interpreted Automata --- *)
+(* -------------------------------------------------------------------------- *)
+
+type mode = {
+ kf : kernel_function ; (* Selected function *)
+ bhv : funbehavior ; (* Selected behavior *)
+ infos : CfgInfos.t ; (* Associated infos *)
+}
+
+type props = [ `All | `Names of string list | `PropId of Property.t ]
+
+module Make(W : Mcfg.S) :
+sig
+ exception NonNaturalLoop of location
+ val compute : mode:mode -> props:props -> W.t_prop
+end
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgDump.ml b/src/plugins/wp/cfgDump.ml
index 84a6852f17d1c188032521f0deba065500c7d11e..798d85ac72a8951197527fa8d11c9672bf87f8b1 100644
--- a/src/plugins/wp/cfgDump.ml
+++ b/src/plugins/wp/cfgDump.ml
@@ -20,283 +20,249 @@
(* *)
(**************************************************************************)
-(* *)
(**************************************************************************)
let _dkey = "cfgdump" (* debugging key *)
-module VC =
-struct
-
- let fc = ref None
- let out = ref Format.std_formatter
- let knode = ref 0
- let node () = incr knode ; !knode
-
- let create kf bhv =
- begin
- let name =
- match bhv with
- | None -> Kernel_function.get_name kf
- | Some bname -> Kernel_function.get_name kf ^ "_" ^ bname
- in
- let file = Filename.concat (Wp_parameters.get_output () :> string) name in
- Wp_parameters.feedback "CFG %a -> %s@." Kernel_function.pretty kf name ;
- let fout = open_out (file ^ ".dot") in
- fc := Some (fout,file) ;
- out := Format.formatter_of_out_channel fout ;
- Format.fprintf !out "digraph %a {@\n" Kernel_function.pretty kf ;
- Format.fprintf !out " rankdir = TB ;@\n" ;
- Format.fprintf !out " node [ style = filled, shape = box ] ;@\n" ;
- Format.fprintf !out " N000 [ color = red, shape = circle, label = \"*\" ] ;@\n" ;
- end
-
- let flush () =
- begin
- Format.fprintf !out "}@." ;
- out := Format.std_formatter ;
- match !fc with
- | None -> ()
- | Some (fout,file) ->
- close_out fout ;
- ignore (Sys.command
- (Printf.sprintf "dot -Tpdf %s.dot > %s.pdf" file file))
- end
-
- (* -------------------------------------------------------------------------- *)
- (* --- MCFG Interface --- *)
- (* -------------------------------------------------------------------------- *)
-
- type t_prop = int (* current node *)
-
- let pretty fmt k = Format.fprintf fmt "N%03d" k
-
- let link a b =
- if b =0
- then Format.fprintf !out " %a -> %a [ style=dotted ];@." pretty a pretty b
- else Format.fprintf !out " %a -> %a ;@." pretty a pretty b
-
- let merge _env k1 k2 =
- if k1=0 then k2 else
- if k2=0 then k1 else
- let u = node () in
- Format.fprintf !out " %a [ label=\"\" , shape=circle ] ;@." pretty u ;
- link u k1 ; link u k2 ; u
-
- let empty = 0
-
- let has_init _ = false
-
- type t_env = Kernel_function.t
-
- let new_env ?lvars kf : t_env = ignore lvars ; kf
-
- let add_axiom _p _l = ()
-
- let add_hyp _env (pid,pred) k =
- let u = node () in
- if Wp_parameters.debug_atleast 1 then
- Format.fprintf !out " %a [ color=green , label=\"Assume %a\" ] ;@." pretty u Printer.pp_predicate pred
- else
- Format.fprintf !out " %a [ color=green , label=\"Assume %a\" ] ;@." pretty u WpPropId.pp_propid pid ;
- link u k ; u
-
- let add_goal env (pid,pred) k =
- let u = node () in
- if Wp_parameters.debug_atleast 1 then
- Format.fprintf !out " %a [ color=red , label=\"Prove %a\" ] ;@." pretty u Printer.pp_predicate pred
- else
- Format.fprintf !out " %a [ color=red , label=\"Prove %a\" ] ;@." pretty u WpPropId.pp_propid pid ;
- Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
- merge env u k
-
- let pp_assigns fmt = function
- | Cil_types.WritesAny -> Format.pp_print_string fmt " \\everything"
- | Cil_types.Writes [] -> Format.pp_print_string fmt " \\nothing"
- | Cil_types.Writes froms ->
- List.iter
- (fun (t,_) -> Format.fprintf fmt "@ %a" Printer.pp_identified_term t)
- froms
-
- let add_assigns env (pid,_) k =
- let u = node () in
- Format.fprintf !out " %a [ color=red , label=\"Assigns %a\" ] ;@." pretty u WpPropId.pp_propid pid ;
- Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
- merge env u k
-
- let use_assigns _env _stmt region d k =
- let u = node () in
- begin match region with
- | None ->
- Format.fprintf !out " %a [ color=orange , label=\"Havoc All\" ] ;@." pretty u
- | Some pid ->
- Format.fprintf !out " %a [ color=orange , label=\"Havoc %a:\n@[<hov 2>assigns%a;@]\" ] ;@."
- pretty u WpPropId.pp_propid pid
- pp_assigns d.WpPropId.a_assigns
- end ;
- link u k ; u
-
- let label _env stmt label k =
- if Clabels.is_here label then k else
- let u = node () in
- ( match stmt with
- | None ->
- Format.fprintf !out " %a [ label=\"Label %a\" ] ;@." pretty u Clabels.pretty label
- | Some s ->
- Format.fprintf !out " %a [ label=\"Label %a (Stmt s%d)\" ] ;@." pretty u Clabels.pretty label s.Cil_types.sid
- ) ;
- link u k ; u
-
- let assign _env _stmt x e k =
- let u = node () in
- Format.fprintf !out " %a [ color=orange , label=\"%a := %a\" ] ;@." pretty u
- Printer.pp_lval x Printer.pp_exp e ;
- link u k ; u
-
- let return _env _stmt r k =
- let u = node () in
- begin
- match r with
- | None ->
- Format.fprintf !out " %a [ color=orange , label=\"Return\" ] ;@." pretty u
- | Some e ->
- Format.fprintf !out " %a [ color=orange , label=\"Return %a\" ] ;@." pretty u
- Printer.pp_exp e
- end ;
- link u k ; u
-
- let test _env _stmt e k1 k2 =
- let u = node () in
- Format.fprintf !out " %a [ color=cyan , label=\"If %a\" ] ;@." pretty u Printer.pp_exp e ;
- link u k1 ; link u k2 ; u
-
- let switch _env _stmt e cases def =
- let u = node () in
- Format.fprintf !out " %a [ color=cyan , label=\"Switch %a\" ] ;@." pretty u Printer.pp_exp e ;
- List.iter (fun (_,k) -> link u k) cases ;
- link u def ; u
-
- let const _ x k =
- let u = node () in
- Format.fprintf !out " %a [ color=orange, label=\"const %a\" ] ;@."
- pretty u Printer.pp_lval (Cil.var x) ;
- link u k ; u
-
- let init _ x init k =
- let u = node () in
- let pp_init fmt = function
- | None -> Format.pp_print_string fmt "<default>"
- | Some init -> Printer.pp_init fmt init
+let fc = ref None
+let out = ref Format.std_formatter
+let knode = ref 0
+let node () = incr knode ; !knode
+
+let fopen kf bhv =
+ begin
+ let name =
+ match bhv with
+ | None -> Kernel_function.get_name kf
+ | Some bname -> Kernel_function.get_name kf ^ "_" ^ bname
in
- Format.fprintf !out " %a [ color=orange, label=\"init %a := %a\" ] ;@."
- pretty u Printer.pp_lval (Cil.var x) pp_init init ;
- link u k ; u
-
- let tag s k =
- let u = node () in
- Format.fprintf !out " %a [ color=cyan , label=\"Tag %s\" ] ;@." pretty u s ;
- link u k ; u
-
- let loop_entry w = tag "BeforeLoop" w
- let loop_step w = tag "InLoop" w
-
- let call_dynamic _env _stmt _pid fct calls =
- let u = node () in
- Format.fprintf !out " %a [ color=red , label \"CallPtr %a\" ];@." pretty u
- Printer.pp_exp fct ;
- List.iter (fun (_,k) -> link u k) calls ; u
-
- let call_goal_precond env _stmt kf _es ~pre k =
- let u = node () in
- Format.fprintf !out " %a [ color=red , label=\"Prove PreCond %a%t\" ] ;@."
- pretty u Kernel_function.pretty kf
- begin fun fmt ->
- if Wp_parameters.debug_atleast 1 then
- List.iter
- (fun (_,p) -> Format.fprintf fmt "\n@[<hov 2>Requires %a ;@]"
- Printer.pp_predicate p) pre
- end ;
- ignore pre ;
- Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
- merge env u k
-
- let call env stmt _r kf _es ~pre ~post ~pexit ~assigns ~p_post ~p_exit =
- let u_post = List.fold_right (add_hyp env) post p_post in
- let u_exit = List.fold_right (add_hyp env) pexit p_exit in
+ let file = Filename.concat (Wp_parameters.get_output () :> string) name in
+ Wp_parameters.feedback "CFG %a -> %s@." Kernel_function.pretty kf name ;
+ let fout = open_out (file ^ ".dot") in
+ fc := Some (fout,file) ;
+ out := Format.formatter_of_out_channel fout ;
+ Format.fprintf !out "digraph %a {@\n" Kernel_function.pretty kf ;
+ Format.fprintf !out " rankdir = TB ;@\n" ;
+ Format.fprintf !out " node [ style = filled, shape = box ] ;@\n" ;
+ Format.fprintf !out " N000 [ color = red, shape = circle, label = \"*\" ] ;@\n" ;
+ end
+
+let flush () =
+ begin
+ Format.fprintf !out "}@." ;
+ out := Format.std_formatter ;
+ match !fc with
+ | None -> ()
+ | Some (fout,file) ->
+ close_out fout ;
+ ignore (Sys.command
+ (Printf.sprintf "dot -Tpdf %s.dot > %s.pdf" file file))
+ end
+
+(* -------------------------------------------------------------------------- *)
+(* --- MCFG Interface --- *)
+(* -------------------------------------------------------------------------- *)
+
+type t_prop = int (* current node *)
+
+let pretty fmt k = Format.fprintf fmt "N%03d" k
+
+let link a b =
+ if b =0
+ then Format.fprintf !out " %a -> %a [ style=dotted ];@." pretty a pretty b
+ else Format.fprintf !out " %a -> %a ;@." pretty a pretty b
+
+let merge _env k1 k2 =
+ if k1=0 then k2 else
+ if k2=0 then k1 else
let u = node () in
- link u u_post ; link u u_exit ;
- Format.fprintf !out
- " %a [ color=orange , label=\"Call %a @[<hov 2>(assigns%a)@]\" ] ;@."
- pretty u Kernel_function.pretty kf pp_assigns assigns ;
- ignore stmt ;
- List.fold_right (add_hyp env) pre u
-
- let pp_scope sc fmt xs =
- let title = match sc with
- | Mcfg.SC_Global -> "Global"
- | Mcfg.SC_Frame_in -> "F-in"
- | Mcfg.SC_Frame_out -> "F-out"
- | Mcfg.SC_Block_in -> "B-in"
- | Mcfg.SC_Block_out -> "B-out"
- in begin
- Format.fprintf fmt "%s {" title ;
- List.iter (fun x -> Format.fprintf fmt " %a" Printer.pp_varinfo x) xs ;
- Format.fprintf fmt " }" ;
- end
-
- let scope _kfenv xs scope k =
- let u = node () in
- Format.fprintf !out " %a [ color=lightblue , label=\"%a\" ] ;@." pretty u
- (pp_scope scope) xs ;
- link u k ; u
+ Format.fprintf !out " %a [ label=\"\" , shape=circle ] ;@." pretty u ;
+ link u k1 ; link u k2 ; u
- let close kfenv k =
+let empty = 0
+
+let has_init _ = false
+
+type t_env = Kernel_function.t
+
+let new_env ?lvars kf : t_env = ignore lvars ; kf
+
+let add_axiom _p _l = ()
+
+let add_hyp _env (pid,pred) k =
+ let u = node () in
+ if Wp_parameters.debug_atleast 1 then
+ Format.fprintf !out " %a [ color=green , label=\"Assume %a\" ] ;@." pretty u Printer.pp_predicate pred
+ else
+ Format.fprintf !out " %a [ color=green , label=\"Assume %a\" ] ;@." pretty u WpPropId.pp_propid pid ;
+ link u k ; u
+
+let add_goal env (pid,pred) k =
+ let u = node () in
+ if Wp_parameters.debug_atleast 1 then
+ Format.fprintf !out " %a [ color=red , label=\"Prove %a\" ] ;@." pretty u Printer.pp_predicate pred
+ else
+ Format.fprintf !out " %a [ color=red , label=\"Prove %a\" ] ;@." pretty u WpPropId.pp_propid pid ;
+ Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
+ merge env u k
+
+let pp_assigns fmt = function
+ | Cil_types.WritesAny -> Format.pp_print_string fmt " \\everything"
+ | Cil_types.Writes [] -> Format.pp_print_string fmt " \\nothing"
+ | Cil_types.Writes froms ->
+ List.iter
+ (fun (t,_) -> Format.fprintf fmt "@ %a" Printer.pp_identified_term t)
+ froms
+
+let add_assigns env (pid,_) k =
+ let u = node () in
+ Format.fprintf !out " %a [ color=red , label=\"Assigns %a\" ] ;@." pretty u WpPropId.pp_propid pid ;
+ Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
+ merge env u k
+
+let use_assigns _env region d k =
+ let u = node () in
+ begin match region with
+ | None ->
+ Format.fprintf !out " %a [ color=orange , label=\"Havoc All\" ] ;@." pretty u
+ | Some pid ->
+ Format.fprintf !out " %a [ color=orange , label=\"Havoc %a:\n@[<hov 2>assigns%a;@]\" ] ;@."
+ pretty u WpPropId.pp_propid pid
+ pp_assigns d.WpPropId.a_assigns
+ end ;
+ link u k ; u
+
+let label _env stmt label k =
+ if Clabels.is_here label then k else
let u = node () in
- Format.fprintf !out " %a [ color=cyan , label=\"Function %a\" ] ;@." pretty u
- Kernel_function.pretty kfenv ;
+ ( match stmt with
+ | None ->
+ Format.fprintf !out " %a [ label=\"Label %a\" ] ;@." pretty u Clabels.pretty label
+ | Some s ->
+ Format.fprintf !out " %a [ label=\"Label %a (Stmt s%d)\" ] ;@." pretty u Clabels.pretty label s.Cil_types.sid
+ ) ;
link u k ; u
- let build_prop_of_from _env _ps _k = 0
-
-end
-
-module WP = Calculus.Cfg(VC)
-
-(* ------------------------------------------------------------------------ *)
-(* --- Proof Obligation Generation --- *)
-(* ------------------------------------------------------------------------ *)
-
-class computer () =
- let driver = Driver.load_driver () in
- let model = Factory.(instance default driver) in
- object
- val mutable wptasks = []
-
- method model = model
- method lemma = true
- method add_lemma (_ : LogicUsage.logic_lemma) = ()
-
- method add_strategy strategy =
- wptasks <- strategy :: wptasks
-
- method compute : Wpo.t Bag.t =
- begin
-
- (* Generates Wpos and accumulate exported goals *)
+let assign _env _stmt x e k =
+ let u = node () in
+ Format.fprintf !out " %a [ color=orange , label=\"%a := %a\" ] ;@." pretty u
+ Printer.pp_lval x Printer.pp_exp e ;
+ link u k ; u
+
+let return _env _stmt r k =
+ let u = node () in
+ begin
+ match r with
+ | None ->
+ Format.fprintf !out " %a [ color=orange , label=\"Return\" ] ;@." pretty u
+ | Some e ->
+ Format.fprintf !out " %a [ color=orange , label=\"Return %a\" ] ;@." pretty u
+ Printer.pp_exp e
+ end ;
+ link u k ; u
+
+let test _env _stmt e k1 k2 =
+ let u = node () in
+ Format.fprintf !out " %a [ color=cyan , label=\"If %a\" ] ;@."
+ pretty u Printer.pp_exp e ;
+ link u k1 ; link u k2 ; u
+
+let switch _env _stmt e cases def =
+ let u = node () in
+ Format.fprintf !out " %a [ color=cyan , label=\"Switch %a\" ] ;@."
+ pretty u Printer.pp_exp e ;
+ List.iter (fun (es,k) ->
+ let c = node () in
+ Format.fprintf !out " %a [ color=orange , label=\"Case %a\" ] ;@."
+ pretty c (Pretty_utils.pp_list ~sep:"," Printer.pp_exp) es ;
+ link u c ;
+ link c k ;
+ ) cases ;
+ let d = node () in
+ Format.fprintf !out " %a [ color=orange , label=\"Default\" ] ;@." pretty d ;
+ link u d ;
+ link d def ; u
+
+let const _ x k =
+ let u = node () in
+ Format.fprintf !out " %a [ color=orange, label=\"const %a\" ] ;@."
+ pretty u Printer.pp_lval (Cil.var x) ;
+ link u k ; u
+
+let init _ x init k =
+ let u = node () in
+ let pp_init fmt = function
+ | None -> Format.pp_print_string fmt "<default>"
+ | Some init -> Printer.pp_init fmt init
+ in
+ Format.fprintf !out " %a [ color=orange, label=\"init %a := %a\" ] ;@."
+ pretty u Printer.pp_lval (Cil.var x) pp_init init ;
+ link u k ; u
+
+let tag s k =
+ let u = node () in
+ Format.fprintf !out " %a [ color=cyan , label=\"Tag %s\" ] ;@." pretty u s ;
+ link u k ; u
+
+let loop_entry w = tag "BeforeLoop" w
+let loop_step w = tag "InLoop" w
+
+let call_dynamic _env _stmt _pid fct calls =
+ let u = node () in
+ Format.fprintf !out " %a [ color=red , label=\"CallPtr %a\" ];@." pretty u
+ Printer.pp_exp fct ;
+ List.iter (fun (_,k) -> link u k) calls ; u
+
+let call_goal_precond env _stmt kf _es ~pre k =
+ let u = node () in
+ Format.fprintf !out " %a [ color=red , label=\"Prove PreCond %a%t\" ] ;@."
+ pretty u Kernel_function.pretty kf
+ begin fun fmt ->
+ if Wp_parameters.debug_atleast 1 then
List.iter
- (fun strategy ->
- let cfg = WpStrategy.cfg_of_strategy strategy in
- let kf = Cil2cfg.cfg_kf cfg in
- let bhv = WpStrategy.behavior_name_of_strategy strategy in
- VC.create kf bhv ;
- try ignore (WP.compute cfg strategy) ; VC.flush ()
- with err -> VC.flush () ; raise err
- ) wptasks ;
- wptasks <- [] ;
- Bag.empty
-
- end (* method compute *)
-
- end (* class computer *)
-
-let create () = (new computer () :> Generator.computer)
+ (fun (_,p) -> Format.fprintf fmt "\n@[<hov 2>Requires %a ;@]"
+ Printer.pp_predicate p) pre
+ end ;
+ ignore pre ;
+ Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
+ merge env u k
+
+let call env stmt _r kf _es ~pre ~post ~pexit ~assigns ~p_post ~p_exit =
+ let u_post = List.fold_right (add_hyp env) post p_post in
+ let u_exit = List.fold_right (add_hyp env) pexit p_exit in
+ let u = node () in
+ link u u_post ; link u u_exit ;
+ Format.fprintf !out
+ " %a [ color=orange , label=\"Call %a @[<hov 2>(assigns%a)@]\" ] ;@."
+ pretty u Kernel_function.pretty kf pp_assigns assigns ;
+ ignore stmt ;
+ List.fold_right (add_hyp env) pre u
+
+let pp_scope sc fmt xs =
+ let title = match sc with
+ | Mcfg.SC_Global -> "Global"
+ | Mcfg.SC_Frame_in -> "F-in"
+ | Mcfg.SC_Frame_out -> "F-out"
+ | Mcfg.SC_Block_in -> "B-in"
+ | Mcfg.SC_Block_out -> "B-out"
+ in begin
+ Format.fprintf fmt "%s {" title ;
+ List.iter (fun x -> Format.fprintf fmt " %a" Printer.pp_varinfo x) xs ;
+ Format.fprintf fmt " }" ;
+ end
+
+let scope _kfenv xs scope k =
+ let u = node () in
+ Format.fprintf !out " %a [ color=lightblue , label=\"%a\" ] ;@." pretty u
+ (pp_scope scope) xs ;
+ link u k ; u
+
+let close kfenv k =
+ let u = node () in
+ Format.fprintf !out " %a [ color=cyan , label=\"Function %a\" ] ;@." pretty u
+ Kernel_function.pretty kfenv ;
+ link u k ; u
+
+let build_prop_of_from _env _ps _k = 0
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgDump.mli b/src/plugins/wp/cfgDump.mli
index 8a56875a65392d30461eaf1f32eef4fc8ef5aa7d..48722048bdd848f86a31476656f5b8b9b42299f2 100644
--- a/src/plugins/wp/cfgDump.mli
+++ b/src/plugins/wp/cfgDump.mli
@@ -20,6 +20,13 @@
(* *)
(**************************************************************************)
-(* Produce a CfgProof.computer that dumps a graph of generated PO *)
+(* Dump calls to Mcfg into DOT graphs *)
-val create : unit -> Generator.computer
+open Cil_types
+
+include Mcfg.S
+
+val fopen : kernel_function -> string option -> unit
+val flush : unit -> unit
+
+(**************************************************************************)
diff --git a/src/plugins/wp/cfgGenerator.ml b/src/plugins/wp/cfgGenerator.ml
new file mode 100644
index 0000000000000000000000000000000000000000..45e5b9c4b347cce18bf5e4e5264fbefcc05872ff
--- /dev/null
+++ b/src/plugins/wp/cfgGenerator.ml
@@ -0,0 +1,330 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+open Wp_parameters
+
+(* -------------------------------------------------------------------------- *)
+(* --- Task Manager --- *)
+(* -------------------------------------------------------------------------- *)
+
+module KFmap = Kernel_function.Map
+
+type pool = {
+ mutable modes: CfgCalculus.mode list KFmap.t ;
+ mutable props: CfgCalculus.props ;
+ mutable lemmas: LogicUsage.logic_lemma list ;
+}
+
+let empty () = {
+ lemmas = [];
+ modes = KFmap.empty;
+ props = `All;
+}
+
+let get_kf_infos model kf ?bhv ?prop () =
+ let missing = WpRTE.missing_guards model kf in
+ if missing && Wp_parameters.RTE.get () then
+ WpRTE.generate model kf ;
+ let smoking =
+ Wp_parameters.SmokeTests.get () &&
+ Wp_parameters.SmokeDeadcode.get () in
+ let infos = CfgInfos.get kf ~smoking ?bhv ?prop () in
+ (*TODO: print warning first *)
+ if missing then
+ Wp_parameters.warning ~current:false ~once:true "Missing RTE guards" ;
+ infos
+
+(* -------------------------------------------------------------------------- *)
+(* --- Behavior Selection --- *)
+(* -------------------------------------------------------------------------- *)
+
+let empty_default_behavior : funbehavior = {
+ b_name = Cil.default_behavior_name ;
+ b_requires = [] ;
+ b_assumes = [] ;
+ b_post_cond = [] ;
+ b_assigns = WritesAny ;
+ b_allocation = FreeAllocAny ;
+ b_extended = [] ;
+}
+
+let default kf =
+ match Annotations.behaviors kf with
+ | [] -> [empty_default_behavior]
+ | bhvs -> List.filter Cil.is_default_behavior bhvs
+
+let select kf bnames =
+ match Annotations.behaviors kf with
+ | [] -> if bnames = [] then [empty_default_behavior] else []
+ | bhvs -> if bnames = [] then bhvs else
+ List.filter
+ (fun b -> List.mem b.b_name bnames)
+ bhvs
+
+(* -------------------------------------------------------------------------- *)
+(* --- Elementary Tasks --- *)
+(* -------------------------------------------------------------------------- *)
+
+let add_lemma_task pool ?(prop=[]) (l : LogicUsage.logic_lemma) =
+ if Logic_utils.verify_predicate l.lem_predicate.tp_kind &&
+ (prop=[] || WpPropId.select_by_name prop (WpPropId.mk_lemma_id l))
+ then pool.lemmas <- l :: pool.lemmas
+
+let add_fun_task model pool ~kf ?infos ?bhvs ?target () =
+ let infos = match infos with
+ | Some infos -> infos
+ | None -> get_kf_infos model kf () in
+ let bhvs = match bhvs with
+ | Some bhvs -> bhvs
+ | None ->
+ let bhvs = Annotations.behaviors kf in
+ if List.exists (Cil.is_default_behavior) bhvs then bhvs
+ else empty_default_behavior :: bhvs in
+ let add_mode kf m =
+ let ms = try KFmap.find kf pool.modes with Not_found -> [] in
+ pool.modes <- KFmap.add kf (m :: ms) pool.modes in
+ begin
+ List.iter (fun bhv -> add_mode kf CfgCalculus.{ infos ; kf ; bhv }) bhvs ;
+ Option.iter (fun ip -> pool.props <- `PropId ip) target ;
+ end
+
+let notyet prop =
+ Wp_parameters.warning ~once:true
+ "Not yet implemented wp for '%a'" Property.pretty prop
+
+(* -------------------------------------------------------------------------- *)
+(* --- Property Tasks --- *)
+(* -------------------------------------------------------------------------- *)
+
+let rec strategy_ip model pool target =
+ let open Property in
+ match target with
+ | IPLemma { il_name } ->
+ add_lemma_task pool (LogicUsage.logic_lemma il_name)
+ | IPAxiomatic { iax_props } ->
+ List.iter (strategy_ip model pool) iax_props
+ | IPBehavior { ib_kf = kf ; ib_bhv = bhv } ->
+ add_fun_task model pool ~kf ~bhvs:[bhv] ()
+ | IPPredicate { ip_kf = kf ; ip_kind ; ip_kinstr = ki } ->
+ begin match ip_kind with
+ | PKAssumes _ -> ()
+ | PKRequires bhv ->
+ begin
+ match ki with
+ | Kglobal -> (*TODO*) notyet target
+ | Kstmt _ -> add_fun_task model pool ~kf ~bhvs:[bhv] ~target ()
+ end
+ | PKEnsures(bhv,_) ->
+ add_fun_task model pool ~kf ~bhvs:[bhv] ~target ()
+ | PKTerminates ->
+ add_fun_task model pool ~kf ~bhvs:(default kf) ~target ()
+ end
+ | IPDecrease { id_kf = kf } ->
+ add_fun_task model pool ~kf ~bhvs:(default kf) ~target ()
+ | IPAssigns { ias_kf=kf ; ias_bhv=Id_loop ca }
+ | IPAllocation { ial_kf=kf ; ial_bhv=Id_loop ca } ->
+ let bhvs = match ca.annot_content with
+ | AAssigns(bhvs,_) | AAllocation(bhvs,_) -> bhvs
+ | _ -> [] in
+ add_fun_task model pool ~kf ~bhvs:(select kf bhvs) ~target ()
+ | IPAssigns { ias_kf=kf ; ias_bhv=Id_contract(_,bhv) }
+ | IPAllocation { ial_kf=kf ; ial_bhv=Id_contract(_,bhv) }
+ -> add_fun_task model pool ~kf ~bhvs:[bhv] ~target ()
+ | IPCodeAnnot { ica_kf = kf ; ica_ca = ca } ->
+ begin match ca.annot_content with
+ | AExtended _ | APragma _ -> ()
+ | AStmtSpec(fors,_) ->
+ (*TODO*) notyet target ;
+ add_fun_task model pool ~kf ~bhvs:(select kf fors) ()
+ | AVariant _ ->
+ add_fun_task model pool ~kf ~target ()
+ | AAssert(fors, _)
+ | AInvariant(fors, _, _)
+ | AAssigns(fors, _)
+ | AAllocation(fors, _) ->
+ add_fun_task model pool ~kf ~bhvs:(select kf fors) ~target ()
+ end
+ | IPComplete _ -> (*TODO*) notyet target
+ | IPDisjoint _ -> (*TODO*) notyet target
+ | IPFrom _ | IPReachable _ | IPTypeInvariant _ | IPGlobalInvariant _
+ | IPPropertyInstance _ -> notyet target (* ? *)
+ | IPExtended _ | IPOther _ -> ()
+
+(* -------------------------------------------------------------------------- *)
+(* --- Function Strategy Tasks --- *)
+(* -------------------------------------------------------------------------- *)
+
+let strategy_main model pool ?(fct=Fct_all) ?(bhv=[]) ?(prop=[]) () =
+ begin
+ if fct = Fct_all && bhv = [] then
+ LogicUsage.iter_lemmas (add_lemma_task pool ~prop) ;
+ Wp_parameters.iter_fct
+ (fun kf ->
+ let infos = get_kf_infos model kf ~bhv ~prop () in
+ if CfgInfos.annots infos then
+ if bhv=[]
+ then add_fun_task model pool ~infos ~kf ()
+ else add_fun_task model pool ~infos ~kf ~bhvs:(select kf bhv) ()
+ ) fct ;
+ pool.props <- (if prop=[] then `All else `Names prop);
+ end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Compute All Tasks --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Make(VCG : CfgWP.VCgen) =
+struct
+
+ module WP = CfgCalculus.Make(VCG)
+
+ let compute model pool =
+ begin
+ let collection = ref Bag.empty in
+ Lang.F.release () ;
+ if pool.lemmas <> [] then
+ WpContext.on_context (model,WpContext.Global)
+ begin fun () ->
+ List.iter
+ (fun (l : LogicUsage.logic_lemma) ->
+ if Logic_utils.verify_predicate l.lem_predicate.tp_kind then
+ let wpo = VCG.compile_lemma l in
+ collection := Bag.add wpo !collection
+ ) pool.lemmas ;
+ end () ;
+ KFmap.iter
+ (fun kf modes ->
+ List.iter
+ begin fun (mode: CfgCalculus.mode) ->
+ WpContext.on_context (model,WpContext.Kf mode.kf)
+ begin fun () ->
+ LogicUsage.iter_lemmas
+ (fun (l : LogicUsage.logic_lemma) ->
+ if Logic_utils.use_predicate l.lem_predicate.tp_kind
+ then VCG.register_lemma l) ;
+ let bhv =
+ if Cil.is_default_behavior mode.bhv then None
+ else Some mode.bhv.b_name in
+ let index = Wpo.Function(mode.kf,bhv) in
+ let props = pool.props in
+ try
+ let wp = WP.compute ~mode ~props in
+ let wcs = VCG.compile_wp index wp in
+ collection := Bag.concat !collection wcs
+ with WP.NonNaturalLoop loc ->
+ Wp_parameters.error
+ ~source:(fst loc)
+ "Non natural loop detected.@\n\
+ WP for function '%a' aborted."
+ Kernel_function.pretty kf
+ end ()
+ end
+ (List.rev modes)
+ ) pool.modes ;
+ CfgAnnot.clear () ;
+ CfgInfos.clear () ;
+ !collection
+ end
+
+ let compute_ip model ip =
+ let pool = empty () in
+ strategy_ip model pool ip ;
+ compute model pool
+
+ let compute_call _model _stmt =
+ Wp_parameters.warning
+ ~once:true "Not yet implemented call preconds" ;
+ Bag.empty
+
+ let compute_main model ?fct ?bhv ?prop () =
+ let pool = empty () in
+ strategy_main model pool ?fct ?bhv ?prop () ;
+ compute model pool
+
+end
+
+(* -------------------------------------------------------------------------- *)
+(* --- New WP Computer (main entry points) --- *)
+(* -------------------------------------------------------------------------- *)
+
+let generators = WpContext.MINDEX.create 1
+
+let generator setup driver =
+ let model = Factory.instance setup driver in
+ try WpContext.MINDEX.find generators model
+ with Not_found ->
+ let module VCG = (val CfgWP.vcgen setup driver) in
+ let module CC = Make(VCG) in
+ let generator : Wpo.generator =
+ object
+ method model = model
+ method compute_ip = CC.compute_ip model
+ method compute_call = CC.compute_call model
+ method compute_main = CC.compute_main model
+ end in
+ WpContext.MINDEX.add generators model generator ;
+ generator
+
+(* -------------------------------------------------------------------------- *)
+(* --- Dumper --- *)
+(* -------------------------------------------------------------------------- *)
+
+let dump pool =
+ let module WP = CfgCalculus.Make(CfgDump) in
+ let props = pool.props in
+ KFmap.iter
+ (fun _ modes ->
+ List.iter
+ begin fun (mode : CfgCalculus.mode) ->
+ let bhv =
+ if Cil.is_default_behavior mode.bhv
+ then None else Some mode.bhv.b_name in
+ try
+ CfgDump.fopen mode.kf bhv ;
+ ignore (WP.compute ~mode ~props) ;
+ CfgDump.flush () ;
+ with err ->
+ CfgDump.flush () ;
+ raise err
+ end
+ (List.rev modes)
+ ) pool.modes
+
+let dumper setup driver =
+ let model = Factory.instance setup driver in
+ let generator : Wpo.generator =
+ object
+ method model = model
+ method compute_ip ip =
+ let pool = empty () in
+ strategy_ip model pool ip ;
+ dump pool ; Bag.empty
+ method compute_call _ = Bag.empty
+ method compute_main ?fct ?bhv ?prop () =
+ let pool = empty () in
+ strategy_main model pool ?fct ?bhv ?prop () ;
+ dump pool ; Bag.empty
+ end
+ in generator
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgGenerator.mli b/src/plugins/wp/cfgGenerator.mli
new file mode 100644
index 0000000000000000000000000000000000000000..ec7f9f9480c0ddfbb449c9559737489179e3b849
--- /dev/null
+++ b/src/plugins/wp/cfgGenerator.mli
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- New WP Computer (main entry points) --- *)
+(* -------------------------------------------------------------------------- *)
+
+val dumper : Factory.setup -> Factory.driver -> Wpo.generator
+val generator : Factory.setup -> Factory.driver -> Wpo.generator
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
new file mode 100644
index 0000000000000000000000000000000000000000..a6e1ad306a00670f622a394c263f237a70d1a515
--- /dev/null
+++ b/src/plugins/wp/cfgInfos.ml
@@ -0,0 +1,318 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+module Cfg = Interpreted_automata
+module Fset = Kernel_function.Set
+module Shash = Cil_datatype.Stmt.Hashtbl
+
+(* -------------------------------------------------------------------------- *)
+(* --- Compute Kernel-Function & CFG Infos for WP --- *)
+(* -------------------------------------------------------------------------- *)
+
+module CheckPath = Graph.Path.Check(Cfg.G)
+
+type t = {
+ body : Cfg.automaton option ;
+ checkpath : CheckPath.path_checker option ;
+ reachability : WpReached.reachability option ;
+ mutable annots : bool; (* has goals to prove *)
+ mutable doomed : WpPropId.prop_id Bag.t;
+ mutable calls : Kernel_function.Set.t;
+}
+
+(* -------------------------------------------------------------------------- *)
+(* --- Getters --- *)
+(* -------------------------------------------------------------------------- *)
+
+let body infos = infos.body
+let calls infos = infos.calls
+let annots infos = infos.annots
+let doomed infos = infos.doomed
+
+let wpreached s = function
+ | None -> false
+ | Some reachability -> WpReached.smoking reachability s
+let smoking infos s = wpreached s infos.reachability
+
+let unreachable infos v =
+ match infos.body, infos.checkpath with
+ | Some cfg , Some checkpath ->
+ not @@ CheckPath.check_path checkpath cfg.entry_point v
+ | _ -> true
+
+(* -------------------------------------------------------------------------- *)
+(* --- Selected Properties --- *)
+(* -------------------------------------------------------------------------- *)
+
+let selected ~bhv ~prop pid =
+ (prop = [] || WpPropId.select_by_name prop pid) &&
+ (bhv = [] || WpPropId.select_for_behaviors bhv pid)
+
+let selected_default ~bhv =
+ bhv=[] || List.mem Cil.default_behavior_name bhv
+
+let selected_name ~prop name =
+ prop=[] || WpPropId.are_selected_names prop [name]
+
+let selected_assigns ~prop = function
+ | Cil_types.WritesAny -> false
+ | Writes _ when prop = [] -> true
+ | Writes l ->
+ let collect_names l (t, _) =
+ WpPropId.ident_names t.Cil_types.it_content.term_name @ l
+ in
+ let names = List.fold_left collect_names ["@assigns"] l in
+ WpPropId.are_selected_names prop names
+
+let selected_allocates ~prop = function
+ | Cil_types.FreeAllocAny -> false
+ | _ -> (selected_name ~prop "@allocates" || selected_name ~prop "@frees")
+
+let selected_precond ~prop ip =
+ prop = [] ||
+ let tk_name = "@requires" in
+ let tp_names = WpPropId.user_pred_names ip.Cil_types.ip_content in
+ WpPropId.are_selected_names prop (tk_name :: tp_names)
+
+let selected_postcond ~prop (tk,ip) =
+ prop = [] ||
+ let tk_name = "@" ^ WpPropId.string_of_termination_kind tk in
+ let tp_names = WpPropId.user_pred_names ip.Cil_types.ip_content in
+ WpPropId.are_selected_names prop (tk_name :: tp_names)
+
+let selected_requires ~prop (b : Cil_types.funbehavior) =
+ List.exists (selected_precond ~prop) b.b_requires
+
+let selected_call ~bhv ~prop kf =
+ bhv = [] && List.exists (selected_requires ~prop) (Annotations.behaviors kf)
+
+let selected_clause ~prop name getter kf =
+ getter kf <> [] && selected_name ~prop name
+
+let selected_disjoint_complete kf ~bhv ~prop =
+ selected_default ~bhv &&
+ ( selected_clause ~prop "@complete_behaviors" Annotations.complete kf ||
+ selected_clause ~prop "@disjoint_behaviors" Annotations.disjoint kf )
+
+let selected_bhv ~smoking ~bhv ~prop (b : Cil_types.funbehavior) =
+ (bhv = [] || List.mem b.b_name bhv) &&
+ begin
+ (selected_assigns ~prop b.b_assigns) ||
+ (selected_allocates ~prop b.b_allocation) ||
+ (smoking && b.b_requires <> []) ||
+ (List.exists (selected_postcond ~prop) b.b_post_cond)
+ end
+
+let selected_main_bhv ~bhv ~prop (b : Cil_types.funbehavior) =
+ (bhv = [] || List.mem b.b_name bhv) && (selected_requires ~prop b)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Calls --- *)
+(* -------------------------------------------------------------------------- *)
+
+let collect_calls ~bhv kf stmt =
+ let open Cil_types in
+ match stmt.skind with
+ | Instr(Call(_,fct,_,_)) ->
+ begin
+ match Kernel_function.get_called fct with
+ | Some kf -> Fset.singleton kf
+ | None ->
+ let bhvs =
+ if bhv = []
+ then List.map (fun b -> b.b_name) (Annotations.behaviors kf)
+ else bhv in
+ List.fold_left
+ (fun fs bhv -> match Dyncall.get ~bhv stmt with
+ | None -> fs
+ | Some(_,kfs) -> List.fold_right Fset.add kfs fs
+ ) Fset.empty bhvs
+ end
+ | Instr(Local_init(x,ConsInit(vf, args, kind), loc)) ->
+ Cil.treat_constructor_as_func
+ (fun _r fct _args _loc ->
+ match Kernel_function.get_called fct with
+ | Some kf -> Fset.singleton kf
+ | None -> Fset.empty)
+ x vf args kind loc
+ | _ -> Fset.empty
+
+(* -------------------------------------------------------------------------- *)
+(* --- Memoization Key --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Key =
+struct
+ type t = {
+ kf: Kernel_function.t ;
+ smoking: bool ;
+ bhv : string list ;
+ prop : string list ;
+ }
+
+ let compare a b =
+ let cmp = Kernel_function.compare a.kf b.kf in
+ if cmp <> 0 then cmp else
+ let cmp = Stdlib.compare a.smoking b.smoking in
+ if cmp <> 0 then cmp else
+ let cmp = Stdlib.compare a.bhv b.bhv in
+ if cmp <> 0 then cmp else
+ Stdlib.compare a.prop b.prop
+
+ let pp_filter kind fmt xs =
+ match xs with
+ | [] -> ()
+ | x::xs ->
+ Format.fprintf fmt "~%s:%s" kind x ;
+ List.iter (Format.fprintf fmt ",%s") xs
+
+ let pretty fmt k =
+ begin
+ Kernel_function.pretty fmt k.kf ;
+ pp_filter "smoking" fmt (if k.smoking then ["true"] else []) ;
+ pp_filter "bhv" fmt k.bhv ;
+ pp_filter "prop" fmt k.prop ;
+ end
+
+end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Main Collection Pass --- *)
+(* -------------------------------------------------------------------------- *)
+
+let dead_posts ~bhv ~prop tk (bhvs : CfgAnnot.behavior list) =
+ let post ~bhv ~prop tk (b: CfgAnnot.behavior) =
+ let assigns, ps = match tk with
+ | Cil_types.Exits -> b.bhv_exit_assigns, b.bhv_exits
+ | _ -> b.bhv_post_assigns, b.bhv_ensures in
+ let ps = List.filter (selected ~prop ~bhv) @@ List.map fst ps in
+ match assigns with
+ | WpPropId.AssignsLocations(id, _) -> Bag.list (id :: ps)
+ | _ -> Bag.list ps
+ in Bag.umap_list (post ~bhv ~prop tk) bhvs
+
+let loop_contract_pids kf stmt =
+ match stmt.Cil_types.skind with
+ | Loop _ ->
+ let invs = CfgAnnot.get_loop_contract kf stmt in
+ let add_assigns assigns l =
+ match assigns with
+ | WpPropId.NoAssignsInfo | AssignsAny _ -> l
+ | AssignsLocations (pid, _) -> pid :: l
+ in
+ List.fold_right (fun (pid,_) l -> pid :: l) invs.loop_established @@
+ List.fold_right (fun (pid,_) l -> pid :: l) invs.loop_preserved @@
+ List.fold_right add_assigns invs.loop_assigns []
+ | _ -> []
+
+let compile Key.{ kf ; smoking ; bhv ; prop } =
+ let body, checkpath, reachability =
+ if Kernel_function.has_definition kf then
+ let cfg = Cfg.get_automaton kf in
+ Some cfg,
+ Some (CheckPath.create cfg.graph),
+ if smoking then Some (WpReached.reachability kf) else None
+ else None, None, None
+ in
+ let infos = {
+ body ; checkpath ; reachability ;
+ annots = false ;
+ doomed = Bag.empty ;
+ calls = Fset.empty ;
+ } in
+ let behaviors = Annotations.behaviors kf in
+ (* Inits *)
+ if WpStrategy.is_main_init kf then
+ infos.annots <- List.exists (selected_main_bhv ~bhv ~prop) behaviors ;
+ (* Function Body *)
+ Option.iter
+ begin fun (cfg : Cfg.automaton) ->
+ (* Spec Iteration *)
+ if selected_disjoint_complete kf ~bhv ~prop ||
+ (List.exists (selected_bhv ~smoking ~bhv ~prop) behaviors)
+ then infos.annots <- true ;
+ (* Stmt Iteration *)
+ Shash.iter
+ (fun stmt (src,_) ->
+ let fs = collect_calls ~bhv kf stmt in
+ let dead = unreachable infos src in
+ let ca = CfgAnnot.get_code_assertions kf stmt in
+ let ca_pids = List.map fst ca.code_verified in
+ let loop_pids = loop_contract_pids kf stmt in
+ if dead then
+ begin
+ if wpreached stmt reachability then
+ (let p = CfgAnnot.get_unreachable kf stmt in
+ infos.doomed <- Bag.append infos.doomed p) ;
+ infos.doomed <- Bag.concat infos.doomed (Bag.list ca_pids) ;
+ infos.doomed <- Bag.concat infos.doomed (Bag.list loop_pids) ;
+ end
+ else
+ begin
+ if not infos.annots &&
+ ( List.exists (selected ~bhv ~prop) ca_pids ||
+ List.exists (selected ~bhv ~prop) loop_pids ||
+ Fset.exists (selected_call ~bhv ~prop) fs )
+ then infos.annots <- true ;
+ infos.calls <- Fset.union fs infos.calls ;
+ end
+ ) cfg.stmt_table ;
+ (* Dead Post Conditions *)
+ let dead_exit = Fset.is_empty infos.calls in
+ let dead_post = unreachable infos cfg.return_point in
+ let bhvs =
+ if dead_exit || dead_post then
+ let exits = not dead_exit in
+ List.map (CfgAnnot.get_behavior_goals kf ~exits) behaviors
+ else [] in
+ if dead_exit then
+ infos.doomed <-
+ Bag.concat infos.doomed (dead_posts ~bhv ~prop Exits bhvs) ;
+ if dead_post then
+ infos.doomed <-
+ Bag.concat infos.doomed (dead_posts ~bhv ~prop Normal bhvs) ;
+ end body ;
+ (* Doomed *)
+ Bag.iter
+ (fun p -> if WpPropId.filter_status p then WpAnnot.set_unreachable p)
+ infos.doomed ;
+ (* Collected Infos *)
+ infos
+
+(* -------------------------------------------------------------------------- *)
+(* --- Memoization Data --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Generator = WpContext.StaticGenerator(Key)
+ (struct
+ type key = Key.t
+ type data = t
+ let name = "Wp.CfgInfos.Generator"
+ let compile = compile
+ end)
+
+let get kf ?(smoking=false) ?(bhv=[]) ?(prop=[]) () =
+ Generator.get { kf ; smoking ; bhv ; prop }
+
+let clear () = Generator.clear ()
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgInfos.mli b/src/plugins/wp/cfgInfos.mli
new file mode 100644
index 0000000000000000000000000000000000000000..472a321933a16e7853b7fd20727ceb0136b27d0f
--- /dev/null
+++ b/src/plugins/wp/cfgInfos.mli
@@ -0,0 +1,42 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* Compute Kernel-Function & CFG Infos for WP *)
+
+type t
+
+module Cfg = Interpreted_automata
+
+(** Memoized *)
+val get : Kernel_function.t ->
+ ?smoking:bool -> ?bhv:string list -> ?prop:string list ->
+ unit -> t
+val clear : unit -> unit
+
+val body : t -> Cfg.automaton option
+val annots : t -> bool
+val doomed : t -> WpPropId.prop_id Bag.t
+val calls : t -> Kernel_function.Set.t
+val smoking : t -> Cil_types.stmt -> bool
+val unreachable : t -> Cfg.vertex -> bool
+
+(**************************************************************************)
diff --git a/src/plugins/wp/cfgInit.ml b/src/plugins/wp/cfgInit.ml
new file mode 100644
index 0000000000000000000000000000000000000000..32168850ea40fec1f7095a53a1e4594d5b9d1881
--- /dev/null
+++ b/src/plugins/wp/cfgInit.ml
@@ -0,0 +1,72 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* Compute Init WP *)
+
+module Make(W : Mcfg.S) =
+struct
+
+ let compute_global_init wenv filter obj =
+ Globals.Vars.fold_in_file_order
+ (fun var initinfo obj ->
+ if var.vstorage = Extern then obj else
+ let do_init = match filter with
+ | `All -> true
+ | `InitConst -> WpStrategy.isGlobalInitConst var
+ in if not do_init then obj
+ else
+ let old_loc = Cil.CurrentLoc.get () in
+ Cil.CurrentLoc.set var.vdecl ;
+ let obj = W.init wenv var initinfo.init obj in
+ Cil.CurrentLoc.set old_loc ; obj
+ ) obj
+
+ let process_global_const wenv obj =
+ Globals.Vars.fold_in_file_order
+ (fun var _initinfo obj ->
+ if WpStrategy.isGlobalInitConst var
+ then W.const wenv var obj
+ else obj
+ ) obj
+
+ (* WP of global initializations. *)
+ let process_global_init wenv kf obj =
+ if WpStrategy.is_main_init kf then
+ begin
+ let obj = W.label wenv None Clabels.init obj in
+ compute_global_init wenv `All obj
+ end
+ else if W.has_init wenv then
+ begin
+ let obj =
+ if WpStrategy.isInitConst ()
+ then process_global_const wenv obj else obj in
+ let obj = W.use_assigns wenv None WpPropId.mk_init_assigns obj in
+ let obj = W.label wenv None Clabels.init obj in
+ compute_global_init wenv `All obj
+ end
+ else
+ if WpStrategy.isInitConst ()
+ then compute_global_init wenv `InitConst obj
+ else obj
+
+end
diff --git a/src/plugins/wp/cfgInit.mli b/src/plugins/wp/cfgInit.mli
new file mode 100644
index 0000000000000000000000000000000000000000..83d3cf130575ff59e361d37b3347dada1bcd92dc
--- /dev/null
+++ b/src/plugins/wp/cfgInit.mli
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+(* Compute Init WP *)
+
+module Make(W : Mcfg.S) :
+sig
+
+ val process_global_init : W.t_env -> kernel_function -> W.t_prop -> W.t_prop
+
+end
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index e8ed36e6a7e14b00cb30e55b2a6256150df7e35b..baa2652d9193dc016225f83dc1b0ee1533b09509 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -35,7 +35,15 @@ open Lang.F
open Sigs
open Wpo
-module VC( C : Sigs.Compiler ) =
+module type VCgen =
+sig
+ include Mcfg.S
+ val register_lemma : logic_lemma -> unit
+ val compile_lemma : logic_lemma -> Wpo.t
+ val compile_wp : Wpo.index -> t_prop -> Wpo.t Bag.t
+end
+
+module VC( C : Sigs.Compiler ) : VCgen =
struct
open C
@@ -598,8 +606,9 @@ struct
let sequence = { pre=s0 ; post=s1 } in
sequence , assigned
- let use_assigns wenv stmt hpid ainfo wp = in_wenv wenv wp
+ let use_assigns wenv hpid ainfo wp = in_wenv wenv wp
begin fun env wp ->
+ let stmt = ainfo.a_stmt in
match ainfo.a_assigns with
| WritesAny ->
@@ -1344,8 +1353,9 @@ struct
else
group.verifs <- Bag.concat group.verifs (make_vcqs target tags vc)
- let compile collection index (wp : t_prop) =
+ let compile_wp index (wp : t_prop) =
let groups = ref PMAP.empty in
+ let collection = ref Bag.empty in
Gmap.iter_sorted
(fun target -> Splitter.iter (group_vc groups target))
wp.vcs ;
@@ -1383,121 +1393,56 @@ struct
end
pid group
- end !groups
+ end !groups ;
+ !collection
+
+ let register_lemma l = ignore (L.lemma l)
- let lemma = L.lemma
+ let compile_lemma l =
+ begin
+ let id = WpPropId.mk_lemma_id l in
+ let def = L.lemma l in
+ let model = WpContext.get_model () in
+ let vca = {
+ Wpo.VC_Lemma.depends = l.lem_depends ;
+ Wpo.VC_Lemma.lemma = def ;
+ Wpo.VC_Lemma.sequent = None ;
+ } in
+ let index = match LogicUsage.section_of_lemma l.lem_name with
+ | LogicUsage.Toplevel _ -> Wpo.Axiomatic None
+ | LogicUsage.Axiomatic a -> Wpo.Axiomatic (Some a.ax_name) in
+ let mid = WpContext.MODEL.id model in
+ let sid = WpPropId.get_propid id in
+ let leg = WpPropId.get_legacy id in
+ let wpo = {
+ Wpo.po_model = model ;
+ Wpo.po_gid = Printf.sprintf "%s_%s" mid sid ;
+ Wpo.po_leg = Printf.sprintf "%s_%s" mid leg ;
+ Wpo.po_sid = sid ;
+ Wpo.po_name = Printf.sprintf "Lemma '%s'" l.lem_name ;
+ Wpo.po_idx = index ;
+ Wpo.po_pid = id ;
+ Wpo.po_formula = Wpo.GoalLemma vca ;
+ } in
+ Wpo.add wpo ; wpo
+ end
end
(* -------------------------------------------------------------------------- *)
-(* --- WPO Computer --- *)
+(* --- VCgen Cache --- *)
(* -------------------------------------------------------------------------- *)
-module KFmap = Kernel_function.Map
-
-module Computer(M : Sigs.Compiler) =
-struct
-
- module VCG = VC(M)
- module WP = Calculus.Cfg(VCG)
-
- let compile_lemma l = ignore (VCG.lemma l)
-
- let prove_lemma collection l =
- if Logic_utils.verify_predicate l.lem_predicate.tp_kind then
- begin
- let id = WpPropId.mk_lemma_id l in
- let def = VCG.lemma l in
- let model = WpContext.get_model () in
- let vca = {
- Wpo.VC_Lemma.depends = l.lem_depends ;
- Wpo.VC_Lemma.lemma = def ;
- Wpo.VC_Lemma.sequent = None ;
- } in
- let index = match LogicUsage.section_of_lemma l.lem_name with
- | LogicUsage.Toplevel _ -> Wpo.Axiomatic None
- | LogicUsage.Axiomatic a -> Wpo.Axiomatic (Some a.ax_name) in
- let mid = WpContext.MODEL.id model in
- let sid = WpPropId.get_propid id in
- let leg = WpPropId.get_legacy id in
- let wpo = {
- Wpo.po_model = model ;
- Wpo.po_gid = Printf.sprintf "%s_%s" mid sid ;
- Wpo.po_leg = Printf.sprintf "%s_%s" mid leg ;
- Wpo.po_sid = sid ;
- Wpo.po_name = Printf.sprintf "Lemma '%s'" l.lem_name ;
- Wpo.po_idx = index ;
- Wpo.po_pid = id ;
- Wpo.po_formula = Wpo.GoalLemma vca ;
- } in
- Wpo.add wpo ;
- collection := Bag.append !collection wpo ;
- end
-
- let prove_strategy collection model kf strategy =
- let cfg = WpStrategy.cfg_of_strategy strategy in
- let bhv = WpStrategy.get_bhv strategy in
- let index = Wpo.Function( kf , bhv ) in
- if WpRTE.missing_guards model kf then
- Wp_parameters.warning ~current:false ~once:true
- "Missing RTE guards" ;
- try
- let (results,_) = WP.compute cfg strategy in
- List.iter (VCG.compile collection index) results
- with Warning.Error(source,reason) ->
- Wp_parameters.failure
- ~current:false "From %s: %s" source reason
-
- class wp (model:WpContext.model) =
- object
- val mutable lemmas : LogicUsage.logic_lemma Bag.t = Bag.empty
- val mutable annots : WpStrategy.strategy Bag.t KFmap.t = KFmap.empty
- method lemma = true
- method model = model
-
- method add_lemma lemma = lemmas <- Bag.append lemmas lemma
-
- method add_strategy strategy =
- let kf = WpStrategy.get_kf strategy in
- let sf = try KFmap.find kf annots with Not_found -> Bag.empty in
- annots <- KFmap.add kf (Bag.append sf strategy) annots
-
- method compute : Wpo.t Bag.t =
- begin
- let collection = ref Bag.empty in
- Lang.F.release () ;
- WpContext.on_context (model,WpContext.Global)
- begin fun () ->
- LogicUsage.iter_lemmas compile_lemma ;
- Bag.iter (prove_lemma collection) lemmas ;
- end () ;
- KFmap.iter
- (fun kf strategies ->
- WpContext.on_context (model,WpContext.Kf kf)
- begin fun () ->
- LogicUsage.iter_lemmas compile_lemma ;
- Bag.iter (prove_strategy collection model kf) strategies ;
- end ()
- ) annots ;
- lemmas <- Bag.empty ;
- annots <- KFmap.empty ;
- Lang.F.release () ;
- !collection
- end
- end
-
-end
-
-(* Cache because computer functors can not be instantiated twice *)
-module COMPUTERS = Hashtbl.Make(WpContext.MODEL)
-let computers = COMPUTERS.create 1
+(* Cache by Model Context *)
+let vcgenerators = WpContext.MINDEX.create 1
-let computer setup driver =
+let vcgen setup driver : (module VCgen) =
let model = Factory.instance setup driver in
- try COMPUTERS.find computers model
+ try WpContext.MINDEX.find vcgenerators model
with Not_found ->
let module M = (val Factory.(compiler setup.mheap setup.mvar)) in
- let module VC = Computer(M) in
- let generator = (new VC.wp model :> Generator.computer) in
- COMPUTERS.add computers model generator ;
- generator
+ let vcgen = (module VC(M) : VCgen) in
+ WpContext.MINDEX.add vcgenerators model vcgen ;
+ vcgen
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgWP.mli b/src/plugins/wp/cfgWP.mli
index ee6bb78f29572ab4dffdaa8ed1841550a14bb2ca..198aa8d6b9eabf7542ede9f170fa7ee9aa766b30 100644
--- a/src/plugins/wp/cfgWP.mli
+++ b/src/plugins/wp/cfgWP.mli
@@ -20,14 +20,20 @@
(* *)
(**************************************************************************)
+open LogicUsage
+
(* -------------------------------------------------------------------------- *)
-(* --- WP Calculus --- *)
+(* --- VC Generator --- *)
(* -------------------------------------------------------------------------- *)
-module VC( M : Sigs.Compiler ) : Mcfg.S
-module Computer( M : Sigs.Compiler ) :
+module type VCgen =
sig
- class wp : WpContext.model -> Generator.computer
+ include Mcfg.S
+ val register_lemma : logic_lemma -> unit
+ val compile_lemma : logic_lemma -> Wpo.t
+ val compile_wp : Wpo.index -> t_prop -> Wpo.t Bag.t
end
-val computer : Factory.setup -> Factory.driver -> Generator.computer
+val vcgen : Factory.setup -> Factory.driver -> (module VCgen)
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cil2cfg.ml b/src/plugins/wp/cil2cfg.ml
index 15d56049af783c14a410b414253f39e95494b2a6..861d41295e4efda49df284417e93b66f98ec434d 100644
--- a/src/plugins/wp/cil2cfg.ml
+++ b/src/plugins/wp/cil2cfg.ml
@@ -1388,3 +1388,66 @@ module KfCfg =
let get kf = KfCfg.memo create kf
(* ------------------------------------------------------------------------ *)
+(** {2 CFG dump} *)
+
+module Dump =
+struct
+ type dot = {
+ name: string;
+ chan: out_channel;
+ fmt : Stdlib__format.formatter;
+ }
+
+ let create kf =
+ let name = Kernel_function.get_name kf in
+ let name =
+ Filename.concat (Wp_parameters.get_output () :> string) ("Cil2CFG_" ^ name)
+ in
+ let chan = open_out (name ^ ".dot") in
+ let fmt = Format.formatter_of_out_channel chan in
+ let out = { name ; chan ; fmt } in
+ Format.fprintf fmt "digraph %a {@\n" Kernel_function.pretty kf ;
+ Format.fprintf fmt " rankdir = TB ;@\n" ;
+ Format.fprintf fmt " node [ style = filled, shape = box ] ;@\n" ;
+ out
+
+ let finalize out =
+ Format.fprintf out.fmt "}@." ;
+ close_out out.chan ;
+ let name = out.name in
+ ignore (Sys.command (Printf.sprintf "dot -Tpdf %s.dot > %s.pdf" name name))
+
+ let pp_id fmt (id, sid) =
+ Format.fprintf fmt "N%03d%03d" sid id
+
+ let pp_content fmt = function
+ | None ->
+ Format.fprintf fmt "label=\"No statement\""
+ | Some s ->
+ Format.fprintf fmt "label=\"wp:sid%d@\n%a\""
+ s.sid Cil_printer.pp_stmt s
+
+ let pp_node fmt n =
+ Format.fprintf fmt " %a [ %a ];@\n"
+ pp_id (node_id n) pp_content (node_stmt_opt n)
+
+ let pp_edge fmt e =
+ Format.fprintf fmt
+ " %a -> %a [ label=\"%a\"];@\n"
+ pp_id (node_id (edge_src e))
+ pp_id (node_id (edge_dst e))
+ EL.pretty (edge_type e)
+
+ let process_kf kf =
+ let cfg = (get kf).graph in
+ let dot = create kf in
+ CFG.iter_vertex (Format.fprintf dot.fmt "%a" pp_node) cfg ;
+ CFG.iter_edges_e (Format.fprintf dot.fmt "%a" pp_edge) cfg ;
+ finalize dot
+
+ let process () =
+ Globals.Functions.iter process_kf
+
+end
+
+(* ------------------------------------------------------------------------ *)
diff --git a/src/plugins/wp/cil2cfg.mli b/src/plugins/wp/cil2cfg.mli
index 087824dfa25a93f43b3502aa5551afb0f98ecf5d..97ef821dd4005d62a566c673811065aa68da8edd 100644
--- a/src/plugins/wp/cil2cfg.mli
+++ b/src/plugins/wp/cil2cfg.mli
@@ -177,3 +177,8 @@ sig
end
module HE (I : sig type t end) : HEsig with type ti = I.t
+
+module Dump :
+sig
+ val process: unit -> unit
+end
diff --git a/src/plugins/wp/clabels.ml b/src/plugins/wp/clabels.ml
index afd2335229e896e83d3b70776636e070834c63d7..8563c5b3fb77262a7c8a6bd6a53a1fc8cc7ac96a 100644
--- a/src/plugins/wp/clabels.ml
+++ b/src/plugins/wp/clabels.ml
@@ -40,11 +40,10 @@ let here = "wp:here"
let next = "wp:next"
let pre = "wp:pre"
let post = "wp:post"
-let old = "wp:old"
+let exit = "wp:exit"
let break = "wp:break"
let continue = "wp:continue"
let default = "wp:default"
-let at_exit = "wp:exit"
let loopcurrent = "wp:loopcurrent"
let loopentry = "wp:loopentry"
@@ -59,6 +58,7 @@ let mem l lbl = List.mem l lbl
let case n = "wp:case" ^ Int64.to_string n
let stmt s = "wp:sid" ^ string_of_int s.sid
+let stmt_post s = "wp:sid:post:" ^ string_of_int s.sid
let loop_entry s = stmt s (* same point *)
let loop_current s = "wp:head" ^ string_of_int s.sid
@@ -69,14 +69,14 @@ let of_logic = function
| BuiltinLabel Pre -> pre
| BuiltinLabel Post -> post
| FormalLabel name -> name
- | BuiltinLabel Old -> old
+ | BuiltinLabel Old -> "wp:old"
| BuiltinLabel LoopCurrent -> loopcurrent
| BuiltinLabel LoopEntry -> loopentry
| StmtLabel s -> stmt !s
let is_post = function
| BuiltinLabel Post -> true
- | FormalLabel a -> a = post
+ | FormalLabel a -> a = post || a = exit
| _ -> false
let name = function FormalLabel a -> a | _ -> ""
diff --git a/src/plugins/wp/clabels.mli b/src/plugins/wp/clabels.mli
index 90e9318ddee025a91e738563c85067b2d3ef6629..dc3ec8d2a5f1f9a01cc9e212a1b4e323da46f987 100644
--- a/src/plugins/wp/clabels.mli
+++ b/src/plugins/wp/clabels.mli
@@ -44,18 +44,18 @@ val here : c_label
val next : c_label
val init : c_label
val post : c_label
+val exit : c_label
val break : c_label
val continue : c_label
val default : c_label
-val at_exit : c_label
val loopentry : c_label
val loopcurrent : c_label
-val old : c_label
val formal : string -> c_label
val case : int64 -> c_label
val stmt : Cil_types.stmt -> c_label
+val stmt_post : Cil_types.stmt -> c_label
val loop_entry : Cil_types.stmt -> c_label
val loop_current : Cil_types.stmt -> c_label
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index c44452f15e11463a5d8e28fa88ae47ce095a7f49..933cd6aa14b0a1b4ccbfb24322588a51c9227e50 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -808,6 +808,11 @@ interface of the programmatic API.
for which the current status is already 'invalid' (default is: \texttt{no}).
\item [\tt -wp-(no)-status-maybe] includes in the goal selection those properties with
an undetermined status (default is: \texttt{yes}).
+\item [\tt -wp-(no)-legacy] use the legacy WP generator, if set to \texttt{no},
+ WP uses a recently developed generator (default is: \texttt{no}).
+\item [\tt -wp-dump] does not prove selected properties, but dumps the control
+ flow graph computed by WP, including code annotations, both DOT files and PDF
+ files into the directory specified by \texttt{-wp-out}.
\end{description}
\textbf{Remark:} options \texttt{-wp-status-xxx} are not taken into account
diff --git a/src/plugins/wp/mcfg.ml b/src/plugins/wp/mcfg.ml
index 0562e0f4b4ca37b7a1ede60bf0a830e2111bc689..568b894770929317b5078add8bfb06d9979f5055 100644
--- a/src/plugins/wp/mcfg.ml
+++ b/src/plugins/wp/mcfg.ml
@@ -73,8 +73,8 @@ module type S = sig
(** [use_assigns env hid kind assgn goal] performs the havoc on the goal.
* [hid] should be [None] iff [assgn] is [WritesAny],
* and tied to the corresponding identified_property otherwise.*)
- val use_assigns : t_env -> stmt option -> WpPropId.prop_id option ->
- WpPropId.assigns_desc -> t_prop -> t_prop
+ val use_assigns : t_env ->
+ WpPropId.prop_id option -> WpPropId.assigns_desc -> t_prop -> t_prop
val label : t_env -> stmt option -> Clabels.c_label -> t_prop -> t_prop
val init : t_env -> varinfo -> init option -> t_prop -> t_prop
diff --git a/src/plugins/wp/normAtLabels.ml b/src/plugins/wp/normAtLabels.ml
index d6d49358da443ad7fa8ef64c6b7b5a41c4c3e1c7..f72ca1ee71a532afb23ce34bb39d34deae742d5b 100644
--- a/src/plugins/wp/normAtLabels.ml
+++ b/src/plugins/wp/normAtLabels.ml
@@ -121,6 +121,8 @@ let labels_fct ?kf ?at l =
| BuiltinLabel Pre -> Clabels.pre
| StmtLabel at -> Clabels.stmt !at
| BuiltinLabel LoopEntry -> Clabels.loop_entry (enclosing_loop ?kf ?at l)
+ (* Labels fct is not used to label invariant establishment/preservation,
+ thus, contrary to what is done in [labels_loop], Current is not Here. *)
| BuiltinLabel LoopCurrent -> Clabels.loop_current (enclosing_loop ?kf ?at l)
| _ -> raise (LabelError l)
@@ -133,16 +135,16 @@ let labels_fct_pre = function
| BuiltinLabel (Pre|Here) -> Clabels.pre
| l -> raise (LabelError l)
-let labels_fct_post = function
+let labels_fct_post ~exit = function
| BuiltinLabel Init -> Clabels.init
| BuiltinLabel (Pre | Old) -> Clabels.pre
- | BuiltinLabel (Post | Here) -> Clabels.post
+ | BuiltinLabel (Post | Here) -> if exit then Clabels.exit else Clabels.post
| l -> raise (LabelError l)
-let labels_fct_assigns = function
+let labels_fct_assigns ~exit = function
| BuiltinLabel Init -> Clabels.init
| BuiltinLabel (Here | Pre | Old) -> Clabels.pre
- | BuiltinLabel Post -> Clabels.post
+ | BuiltinLabel Post -> if exit then Clabels.exit else Clabels.post
| l -> raise (LabelError l)
(* -------------------------------------------------------------------------- *)
@@ -153,12 +155,24 @@ let labels_stmt_pre ~kf s = function
| BuiltinLabel Here -> Clabels.stmt s
| l -> labels_fct ~kf ~at:s l
-let labels_stmt_post ~kf s l_post = function
+let labels_stmt_post ~kf s = function
+ | BuiltinLabel Old -> Clabels.stmt s
+ | BuiltinLabel (Here | Post) -> Clabels.stmt_post s
+ | l -> labels_fct ~kf ~at:s l
+
+let labels_stmt_assigns ~kf s = function
+ | BuiltinLabel (Here | Old) -> Clabels.stmt s
+ | BuiltinLabel Post -> Clabels.stmt_post s
+ | l -> labels_fct ~kf ~at:s l
+
+(* LEGACY *)
+let labels_stmt_post_l ~kf s l_post = function
| BuiltinLabel Old -> Clabels.stmt s
| BuiltinLabel (Here | Post) as l -> option l l_post
| l -> labels_fct ~kf ~at:s l
-let labels_stmt_assigns ~kf s l_post = function
+(* LEGACY *)
+let labels_stmt_assigns_l ~kf s l_post = function
| BuiltinLabel (Here | Old) -> Clabels.stmt s
| BuiltinLabel Post as l -> option l l_post
| l -> labels_fct ~kf ~at:s l
@@ -167,16 +181,12 @@ let labels_stmt_assigns ~kf s l_post = function
(* --- User Assertions in Functions Code --- *)
(* -------------------------------------------------------------------------- *)
-let labels_assert_before ~kf s = function
+let labels_assert ~kf s = function
| BuiltinLabel Here -> Clabels.stmt s
| l -> labels_fct ~kf ~at:s l
-let labels_assert_after ~kf s l_post = function
- | BuiltinLabel Old -> Clabels.stmt s
- | BuiltinLabel Here as l -> option l l_post
- | l -> labels_fct ~kf ~at:s l
-
let labels_loop s = function
+ (* In invariant preservation/establishment, LoopCurrent is Here. *)
| BuiltinLabel (Here | LoopCurrent) -> Clabels.here
| BuiltinLabel LoopEntry -> Clabels.loop_entry s
| FormalLabel wplabel -> Clabels.formal wplabel
diff --git a/src/plugins/wp/normAtLabels.mli b/src/plugins/wp/normAtLabels.mli
index 800b10b7e4d0a4d64cb450943b6335aa183ffd8a..b6b41f04bc428215cb8ae40066755a78bf94f997 100644
--- a/src/plugins/wp/normAtLabels.mli
+++ b/src/plugins/wp/normAtLabels.mli
@@ -30,14 +30,15 @@ type label_mapping
val labels_empty : label_mapping
val labels_fct_pre : label_mapping
-val labels_fct_post : label_mapping
-val labels_fct_assigns : label_mapping
-val labels_assert_before : kf:kernel_function -> stmt -> label_mapping
-val labels_assert_after : kf:kernel_function -> stmt -> c_label option -> label_mapping
+val labels_fct_post : exit:bool -> label_mapping
+val labels_fct_assigns : exit:bool -> label_mapping
+val labels_assert : kf:kernel_function -> stmt -> label_mapping
val labels_loop : stmt -> label_mapping
val labels_stmt_pre : kf:kernel_function -> stmt -> label_mapping
-val labels_stmt_post : kf:kernel_function -> stmt -> c_label option -> label_mapping
-val labels_stmt_assigns : kf:kernel_function -> stmt -> c_label option -> label_mapping
+val labels_stmt_post : kf:kernel_function -> stmt -> label_mapping
+val labels_stmt_assigns : kf:kernel_function -> stmt -> label_mapping
+val labels_stmt_post_l : kf:kernel_function -> stmt -> c_label option -> label_mapping
+val labels_stmt_assigns_l : kf:kernel_function -> stmt -> c_label option -> label_mapping
val labels_predicate : (logic_label * logic_label) list -> label_mapping
val labels_axiom : label_mapping
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index d1528afaf904910ce84500ad8c1ef3e0491e9595..9bff55614bf71b2281a5e671c08bc725efe3aed9 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -20,53 +20,10 @@
(* *)
(**************************************************************************)
-open Factory
-
let dkey_main = Wp_parameters.register_category "main"
let dkey_raised = Wp_parameters.register_category "raised"
let wkey_smoke = Wp_parameters.register_warn_category "smoke"
-(* --------- Command Line ------------------- *)
-
-let cmdline () : setup =
- begin
- match Wp_parameters.Model.get () with
- | ["Runtime"] ->
- Wp_parameters.abort
- "Model 'Runtime' is no more available.@\nIt will be reintroduced \
- in a future release."
- | ["Logic"] ->
- Wp_parameters.warning ~once:true
- "Deprecated 'Logic' model.@\nUse 'Typed' with option '-wp-ref' \
- instead." ;
- {
- mheap = Factory.Typed MemTyped.Fits ;
- mvar = Factory.Ref ;
- cint = Cint.Natural ;
- cfloat = Cfloat.Real ;
- }
- | ["Store"] ->
- Wp_parameters.warning ~once:true
- "Deprecated 'Store' model.@\nUse 'Typed' instead." ;
- {
- mheap = Factory.Typed MemTyped.Fits ;
- mvar = Factory.Var ;
- cint = Cint.Natural ;
- cfloat = Cfloat.Real ;
- }
- | spec -> Factory.parse spec
- end
-
-let set_model (s:setup) =
- Wp_parameters.Model.set [Factory.ident s]
-
-(* --------- WP Computer -------------------- *)
-
-let computer () =
- if Wp_parameters.Model.get () = ["Dump"]
- then CfgDump.create ()
- else CfgWP.computer (cmdline ()) (Driver.load_driver ())
-
(* ------------------------------------------------------------------------ *)
(* --- Memory Model Hypotheses --- *)
(* ------------------------------------------------------------------------ *)
@@ -751,11 +708,12 @@ let cmdline_run () =
if fct <> Wp_parameters.Fct_none then
begin
Wp_parameters.feedback ~ontty:`Feedback "Running WP plugin...";
- let computer = computer () in
+ let generator = Generator.create () in
+ let model = generator#model in
Ast.compute ();
Dyncall.compute ();
if Wp_parameters.RTE.get () then
- WpRTE.generate_all computer#model ;
+ WpRTE.generate_all model ;
if Wp_parameters.has_dkey dkey_logicusage then
begin
LogicUsage.compute ();
@@ -771,14 +729,14 @@ let cmdline_run () =
(** TODO entry point *)
if Wp_parameters.has_dkey dkey_builtins then
begin
- WpContext.on_context (computer#model,WpContext.Global)
+ WpContext.on_context (model,WpContext.Global)
LogicBuiltins.dump ();
end ;
- WpTarget.compute computer#model ;
- wp_compute_memory_context computer#model ;
+ WpTarget.compute model ;
+ wp_compute_memory_context model ;
if Wp_parameters.CheckMemoryContext.get () then
- wp_insert_memory_context computer#model ;
- let goals = Generator.compute_selection computer ~fct ~bhv ~prop () in
+ wp_insert_memory_context model ;
+ let goals = generator#compute_main ~fct ~bhv ~prop () in
do_wp_proofs goals ;
begin
if fct <> Wp_parameters.Fct_all then
@@ -786,7 +744,7 @@ let cmdline_run () =
else
do_wp_print () ;
end ;
- do_wp_report computer#model ;
+ do_wp_report model ;
end
end
@@ -815,10 +773,7 @@ let pp_wp_parameters fmt =
if Wp_parameters.RTE.get () then Format.pp_print_string fmt " -wp-rte" ;
let spec = Wp_parameters.Model.get () in
if spec <> [] && spec <> ["Typed"] then
- ( let descr =
- if spec = ["Dump"] then "Dump"
- else Factory.descr (Factory.parse spec)
- in
+ ( let descr = Factory.descr (Factory.parse spec) in
Format.fprintf fmt " -wp-model '%s'" descr ) ;
if not (Wp_parameters.Let.get ()) then Format.pp_print_string fmt
" -wp-no-let" ;
diff --git a/src/plugins/wp/tests/wp/exit_post_scope.i b/src/plugins/wp/tests/wp/exit_post_scope.i
new file mode 100644
index 0000000000000000000000000000000000000000..4cfdafaf8c5c6de925d1e2abcaab3b51fe57efa6
--- /dev/null
+++ b/src/plugins/wp/tests/wp/exit_post_scope.i
@@ -0,0 +1,9 @@
+void bar(void);
+
+/*@
+ ensures \valid(&f);
+ exits \valid(&f);
+*/
+void foo(int f){
+ bar();
+}
diff --git a/src/plugins/wp/tests/wp/oracle/exit_post_scope.res.oracle b/src/plugins/wp/tests/wp/oracle/exit_post_scope.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..84a6cd87562135b7069d0526bc0a799c8b19db4c
--- /dev/null
+++ b/src/plugins/wp/tests/wp/oracle/exit_post_scope.res.oracle
@@ -0,0 +1,19 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp/exit_post_scope.i (no preprocessing)
+[wp] Running WP plugin...
+[kernel:annot:missing-spec] tests/wp/exit_post_scope.i:7: Warning:
+ Neither code nor specification for function bar, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function foo
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp/exit_post_scope.i, line 4) in 'foo':
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Exit-condition (file tests/wp/exit_post_scope.i, line 5) in 'foo':
+Prove: false.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/exit_post_scope.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/exit_post_scope.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..cd113ca71f9103c32d6e29d58c63237284a54411
--- /dev/null
+++ b/src/plugins/wp/tests/wp/oracle_qualif/exit_post_scope.res.oracle
@@ -0,0 +1,15 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp/exit_post_scope.i (no preprocessing)
+[wp] Running WP plugin...
+[kernel:annot:missing-spec] tests/wp/exit_post_scope.i:7: Warning:
+ Neither code nor specification for function bar, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+[wp] 2 goals scheduled
+[wp] [Alt-Ergo] Goal typed_foo_ensures : Unsuccess
+[wp] [Alt-Ergo] Goal typed_foo_exits : Unsuccess
+[wp] Proved goals: 0 / 2
+ Alt-Ergo: 0 (unsuccess: 2)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ foo - - 2 0.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/cfg.c b/src/plugins/wp/tests/wp_plugin/cfg.c
new file mode 100644
index 0000000000000000000000000000000000000000..0c0a510591c31a3e1074d13742043bd4614be76a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/cfg.c
@@ -0,0 +1,65 @@
+//@ assigns \nothing;
+void foo(void);
+
+/*@ ensures BUG_WP: \false; */
+void f1(void)
+{
+ if (0 == 1)
+ goto return_label;
+ {
+ int t1 = 1;
+ foo();
+ goto return_label;
+ }
+ return_label: return;
+}
+
+/*@ ensures BUG_WP: \false; */
+void f1_simpler(void)
+{
+ if (0 == 1)
+ goto return_label;
+ {
+ int t1 = 1;
+ goto return_label;
+ }
+ return_label: return;
+}
+
+/*@ ensures BUG_WP: \false; */
+void f1_variant(void)
+{
+ if (0 == 1) L: ;
+ else {
+ int t1 = 1;
+ foo();
+ goto return_label;
+ }
+ return_label: return;
+}
+
+/*@ ensures FAILS_AS_EXPECTED: \false; */
+void f1_variant_invert(void)
+{
+ if (! (0 == 1)) {
+ int t1 = 1;
+ foo();
+ goto return_label;
+ }
+ else L: ;
+ return_label: return;
+}
+
+/*@ ensures BUG_WP: \false; */
+void f2(void)
+{
+ if (0 == 1)
+ goto L;
+ if (0 == 0) {
+ int t1 = 1;
+ foo();
+ goto return_label;
+ }
+ else L: ;
+ return_label: return;
+}
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/cfg.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/cfg.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f78e97da034cdcae042c07a28d2fdb21a6fead50
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/cfg.res.oracle
@@ -0,0 +1,44 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/cfg.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function f1
+------------------------------------------------------------
+
+Goal Post-condition 'BUG_WP' in 'f1':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function f1_simpler
+------------------------------------------------------------
+
+Goal Post-condition 'BUG_WP' in 'f1_simpler':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function f1_variant
+------------------------------------------------------------
+
+Goal Post-condition 'BUG_WP' in 'f1_variant':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function f1_variant_invert
+------------------------------------------------------------
+
+Goal Post-condition 'FAILS_AS_EXPECTED' in 'f1_variant_invert':
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function f2
+------------------------------------------------------------
+
+Goal Post-condition 'BUG_WP' in 'f2':
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/cfg.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/cfg.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..65a2d69e16bdb23fa6a41746dccb152924467752
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/cfg.res.oracle
@@ -0,0 +1,21 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/cfg.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 5 goals scheduled
+[wp] [Qed] Goal typed_f1_ensures_BUG_WP : Valid
+[wp] [Qed] Goal typed_f1_simpler_ensures_BUG_WP : Valid
+[wp] [Qed] Goal typed_f1_variant_ensures_BUG_WP : Valid
+[wp] [Alt-Ergo] Goal typed_f1_variant_invert_ensures_FAILS_AS_EXPECTED : Unsuccess
+[wp] [Qed] Goal typed_f2_ensures_BUG_WP : Valid
+[wp] Proved goals: 4 / 5
+ Qed: 4
+ Alt-Ergo: 0 (unsuccess: 1)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ f1 1 - 1 100%
+ f1_simpler 1 - 1 100%
+ f1_variant 1 - 1 100%
+ f1_variant_invert - - 1 0.0%
+ f2 1 - 1 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
index 54fa701c499fd123bd6160f72a022ee8b5fd21de..fc376ede27e35a2ecf8fc9819774ab3bedbdae75 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.log
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-model 'Dump' [...]
+# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/stmt.c (with preprocessing)
[wp] Running WP plugin...
[wp] [CFG] Goal f_exits : Valid (Unreachable)
diff --git a/src/plugins/wp/tests/wp_plugin/stmt.c b/src/plugins/wp/tests/wp_plugin/stmt.c
index df45bff806e6f85034d9af3b89d04427f64516dd..bb82e910c1cc73a606e725ae72c332328f1dd9a4 100644
--- a/src/plugins/wp/tests/wp_plugin/stmt.c
+++ b/src/plugins/wp/tests/wp_plugin/stmt.c
@@ -4,7 +4,7 @@
/* run.config_qualif
OPT: -load-module report -then -report
- EXECNOW: LOG stmt.log LOG f.dot LOG f_default_for_stmt_2.dot LOG g.dot LOG g_default_for_stmt_11.dot @frama-c@ -no-autoload-plugins -load-module wp -wp-precond-weakening -wp -wp-warn-key pedantic-assigns=inactive -wp-model Dump -wp-out tests/wp_plugin/result_qualif -wp-msg-key shell @PTEST_FILE@ 1> tests/wp_plugin/result_qualif/stmt.log
+ EXECNOW: LOG stmt.log LOG f.dot LOG f_default_for_stmt_2.dot LOG g.dot LOG g_default_for_stmt_11.dot @frama-c@ -no-autoload-plugins -load-module wp -wp-precond-weakening -wp -wp-warn-key pedantic-assigns=inactive -wp-dump -wp-out tests/wp_plugin/result_qualif -wp-msg-key shell @PTEST_FILE@ 1> tests/wp_plugin/result_qualif/stmt.log
*/
/*@ ensures a > 0 ==> \result == a + b;
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 3d520317fc0d9c15445a98c8712dc60e0a12eb07..fef919f1502924d6c0a679065c50cccc5ada6697 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -30,41 +30,6 @@ open Cil_types
open Cil_datatype
open Logic_utils
-(* -------------------------------------------------------------------------- *)
-(* --- Selection of relevant assigns and postconditions --- *)
-(* -------------------------------------------------------------------------- *)
-
-(* Properties for kf-conditions of termination-kind 'tkind' *)
-let get_called_postconds (tkind:termination_kind) kf =
- let bhvs = Annotations.behaviors kf in
- List.fold_left
- (fun properties bhv ->
- List.fold_left
- (fun properties postcond ->
- if tkind = fst postcond then
- let pid_spec = Property.ip_of_ensures kf Kglobal bhv postcond in
- pid_spec :: properties
- else properties)
- properties bhv.b_post_cond)
- []
- bhvs
-
-let get_called_post_conditions = get_called_postconds Cil_types.Normal
-let get_called_exit_conditions = get_called_postconds Cil_types.Exits
-
-(** Properties for assigns of kf *)
-let get_called_assigns kf =
- let bhvs = Annotations.behaviors kf in
- List.fold_left
- (fun properties bhv ->
- if Cil.is_default_behavior bhv then
- match Property.ip_assigns_of_behavior kf Kglobal [] bhv with
- | None -> properties
- | Some ip -> ip :: properties
- else properties)
- []
- bhvs
-
(* -------------------------------------------------------------------------- *)
(* --- Status of Unreachable Annotations --- *)
(* -------------------------------------------------------------------------- *)
@@ -111,74 +76,13 @@ let set_unreachable pid =
in
List.iter emit pids
-(*----------------------------------------------------------------------------*)
-(* Proofs *)
-(*----------------------------------------------------------------------------*)
-
-type proof = {
- target : Property.t ;
- proved : proofpart array ;
- mutable invalid : bool ;
- mutable dependencies : Property.Set.t ;
-} and proofpart =
- | Noproof
- | Complete
- | Parts of Bitvector.t
-
-let target p = p.target
-let dependencies p =
- Property.Set.elements (Property.Set.remove p.target p.dependencies)
-
-let create_proof ip =
- let n = WpPropId.subproofs ip in
- {
- target = WpPropId.property_of_id ip ;
- proved = Array.make n Noproof ;
- dependencies = Property.Set.empty ;
- invalid = false ;
- }
-
-let add_proof pf ip hs =
- begin
- if not (Property.equal (WpPropId.property_of_id ip) pf.target)
- then Wp_parameters.fatal "Partial proof inconsistency" ;
- List.iter
- (fun iph ->
- if not (WpPropId.is_requires iph) then
- pf.dependencies <- Property.Set.add iph pf.dependencies
- ) hs ;
- let k = WpPropId.subproof_idx ip in
- match WpPropId.parts_of_id ip with
- | None -> pf.proved.(k) <- Complete
- | Some(p,n) ->
- match pf.proved.(k) with
- | Complete -> ()
- | Noproof ->
- let bv = Bitvector.create n in
- Bitvector.set_range bv 0 (p-1) ;
- Bitvector.set_range bv (p+1) (n-1) ;
- pf.proved.(k) <- Parts bv
- | Parts bv ->
- Bitvector.clear bv p ;
- if Bitvector.is_empty bv
- then pf.proved.(k) <- Complete
- end
-
-let add_invalid_proof pf = pf.invalid <- true
-
-let is_composed pf =
- Array.length pf.proved > 1
-
-let is_proved pf =
- Array.for_all (function Complete -> true | _ -> false) pf.proved
-
-let is_invalid pf =
- pf.invalid && not (is_proved pf)
-
(* -------------------------------------------------------------------------- *)
-(* --- PID for Functions --- *)
+(* --- Preconditions at Callsites --- *)
(* -------------------------------------------------------------------------- *)
+let call_preconditions =
+ Statuses_by_call.all_call_preconditions_at ~warn_missing:true
+
let mk_call_pre_id called_kf bhv s_call called_pre =
(* TODOclean : quite dirty here ! *)
let id = WpPropId.mk_pre_id called_kf Kglobal bhv called_pre in
@@ -187,13 +91,6 @@ let mk_call_pre_id called_kf bhv s_call called_pre =
Statuses_by_call.precondition_at_call called_kf called_pre s_call in
WpPropId.mk_call_pre_id called_kf s_call called_pre called_pre_p
-(* -------------------------------------------------------------------------- *)
-(* --- Preconditions --- *)
-(* -------------------------------------------------------------------------- *)
-
-let call_preconditions =
- Statuses_by_call.all_call_preconditions_at ~warn_missing:true
-
(* Preconditions at call-point as WpPropId.t *)
let preconditions_at_call s = function
| Cil2cfg.Static kf ->
@@ -202,8 +99,9 @@ let preconditions_at_call s = function
List.map aux preconds
| Cil2cfg.Dynamic _ -> []
-let get_called_preconditions_at kf stmt =
- List.map snd (call_preconditions kf stmt)
+(* ########################################################################## *)
+(* ### WARNING: DEPRECATED API BELOW THIS LINE ### *)
+(* ########################################################################## *)
(*----------------------------------------------------------------------------*)
(* Strategy and annotations *)
@@ -316,23 +214,9 @@ let filter_speconly config pid =
| _ -> false
else true
-let filter_status pid =
- Wp_parameters.StatusAll.get () ||
- begin
- let module C = Property_status.Consolidation in
- match C.get (WpPropId.property_of_id pid) with
- | C.Never_tried -> true
- | C.Considered_valid | C.Inconsistent _ -> false
- | C.Valid _ | C.Valid_under_hyp _
- | C.Invalid_but_dead _ | C.Valid_but_dead _ | C.Unknown_but_dead _ ->
- Wp_parameters.StatusTrue.get ()
- | C.Unknown _ -> Wp_parameters.StatusMaybe.get ()
- | C.Invalid _ | C.Invalid_under_hyp _ -> Wp_parameters.StatusFalse.get ()
- end
-
let filter_configstatus config pid =
(match config.asked_prop with IdProp _ -> true | _ -> false) ||
- (filter_status pid)
+ (WpPropId.filter_status pid)
let filter_asked config pid =
match config.asked_prop with
@@ -422,7 +306,7 @@ let add_stmt_assigns_goal config s active acc b l_post = match b.b_assigns with
| Some id ->
if goal_to_select config id then
let kf = config.kf in
- let labels = NormAtLabels.labels_stmt_assigns ~kf s l_post in
+ let labels = NormAtLabels.labels_stmt_assigns_l ~kf s l_post in
let assigns = NormAtLabels.preproc_assigns labels assigns in
let a_desc = WpPropId.mk_stmt_assigns_desc s assigns in
WpStrategy.add_assigns acc WpStrategy.Agoal id a_desc
@@ -431,12 +315,13 @@ let add_stmt_assigns_goal config s active acc b l_post = match b.b_assigns with
let add_fct_assigns_goal config acc tkind b = match b.b_assigns with
| WritesAny -> acc
| Writes assigns ->
- let id = WpPropId.mk_fct_assigns_id config.kf b tkind assigns in
+ let has_exit = Cil2cfg.has_exit (Cil2cfg.get config.kf) in
+ let id = WpPropId.mk_fct_assigns_id config.kf has_exit b tkind assigns in
match id with
| None -> acc
| Some id ->
if goal_to_select config id then
- let labels = NormAtLabels.labels_fct_assigns in
+ let labels = NormAtLabels.labels_fct_assigns ~exit:false in
let assigns' = NormAtLabels.preproc_assigns labels assigns in
let a_desc = WpPropId.mk_kf_assigns_desc assigns' in
WpStrategy.add_assigns acc WpStrategy.Agoal id a_desc
@@ -772,7 +657,7 @@ let add_called_post called_kf termination_kind acc =
let add_call_checks config s kf posts exits =
if cur_fct_default_bhv config
&& Wp_parameters.SmokeTests.get ()
- && Wp_parameters.SmokeDeadcode.get ()
+ && Wp_parameters.SmokeDeadcall.get ()
then
WpStrategy.add_prop_dead_call kf s posts exits
else
@@ -1310,7 +1195,7 @@ let process_unreached_annots cfg reachability =
let kf = Cil2cfg.cfg_kf cfg in
let spec = Annotations.funspec kf in
let add_id acc id =
- if filter_status id then id::acc
+ if WpPropId.filter_status id then id::acc
else (* non-selected property : nothing to do *) acc
in
let do_post b tk acc (termk, _ as p) =
@@ -1489,3 +1374,34 @@ let get_function_strategies ~model
?(assigns=WithAssigns) ?(bhv=[]) ?(prop=[]) kf =
let prop = match prop with [] -> AllProps | _ -> NamedProp prop in
get_strategies assigns kf model bhv None prop
+
+let get_property_strategies ~model ip =
+ let open Property in
+ match ip with
+ | IPBehavior {ib_kf; ib_bhv} ->
+ let bhv = [ib_bhv.Cil_types.b_name] in
+ let assigns = WithAssigns in
+ get_function_strategies ~model ~assigns ~bhv ib_kf
+ | IPComplete _
+ | IPDisjoint _
+ | IPCodeAnnot _
+ | IPAllocation _
+ | IPAssigns _
+ | IPDecrease _
+ | IPPredicate _
+ ->
+ let assigns = WithAssigns in
+ get_id_prop_strategies ~model ~assigns ip
+
+ | IPAxiomatic _
+ | IPLemma _
+ | IPFrom _
+ | IPReachable _
+ | IPPropertyInstance _
+ | IPOther _
+ | IPTypeInvariant _
+ | IPGlobalInvariant _
+ | IPExtended _
+ ->
+ Wp_parameters.result "Nothing to compute for '%a'" pretty ip ;
+ []
diff --git a/src/plugins/wp/wpAnnot.mli b/src/plugins/wp/wpAnnot.mli
index 0fcc0b671b7adee8836ef30666226ca8b2e524a4..a0a268cbc61cd59047db6ca65190568e294b6cca 100644
--- a/src/plugins/wp/wpAnnot.mli
+++ b/src/plugins/wp/wpAnnot.mli
@@ -20,58 +20,24 @@
(* *)
(**************************************************************************)
+open Cil_types
+
(** Every access to annotations have to go through here,
* so this is the place where we decide what the computation
* is allowed to use. *)
-open Cil_types
-
-(*----------------------------------------------------------------------------*)
-
-(** A proof accumulator for a set of related prop_id *)
-type proof
-
-val create_proof : WpPropId.prop_id -> proof
-(** to be used only once for one of the related prop_id *)
-
-val add_proof : proof -> WpPropId.prop_id -> Property.t list -> unit
-(** accumulate in the proof the partial proof for this prop_id *)
-
-val add_invalid_proof : proof -> unit
-(** add an invalid proof result ; can not revert a complete proof *)
-
-val is_composed : proof -> bool
-(** whether a proof needs several lemma to be complete *)
-
-val is_proved : proof -> bool
-(** whether all partial proofs have been accumulated or not *)
-
-val is_invalid : proof -> bool
-(** whether an invalid proof result has been registered or not *)
-
-val target : proof -> Property.t
-val dependencies : proof -> Property.t list
-
-val filter_status : WpPropId.prop_id -> bool
+(* ########################################################################## *)
+(* ### WARNING: DEPRECATED API ### *)
+(* ########################################################################## *)
(*----------------------------------------------------------------------------*)
val unreachable_proved : int ref
val unreachable_failed : int ref
-
-val get_called_preconditions_at : kernel_function -> stmt -> Property.t list
-val get_called_post_conditions : kernel_function -> Property.t list
-val get_called_exit_conditions : kernel_function -> Property.t list
-val get_called_assigns : kernel_function -> Property.t list
-
-(*----------------------------------------------------------------------------*)
+val set_unreachable : WpPropId.prop_id -> unit
type asked_assigns = NoAssigns | OnlyAssigns | WithAssigns
-val get_id_prop_strategies :
- model:WpContext.model ->
- ?assigns:asked_assigns -> Property.t -> WpStrategy.strategy list
-
val get_call_pre_strategies :
model:WpContext.model ->
stmt -> WpStrategy.strategy list
@@ -83,4 +49,7 @@ val get_function_strategies :
?prop:string list ->
Kernel_function.t -> WpStrategy.strategy list
+val get_property_strategies :
+ model:WpContext.model -> Property.t -> WpStrategy.strategy list
+
(*----------------------------------------------------------------------------*)
diff --git a/src/plugins/wp/wpContext.ml b/src/plugins/wp/wpContext.ml
index 0205b6529d5f33c4af4c20ec1d77c1558b7bac73..62b15a0def8506932e938f1fd2bebd995e8ef5e3 100644
--- a/src/plugins/wp/wpContext.ml
+++ b/src/plugins/wp/wpContext.ml
@@ -56,6 +56,8 @@ struct
}
end
+module MINDEX = Hashtbl.Make(MODEL)
+
module MODELS =
struct
diff --git a/src/plugins/wp/wpContext.mli b/src/plugins/wp/wpContext.mli
index cf3576f78470dd4eb1c73f4719c993450864506e..5b3203bc0b2c5522369e8c207c925d25c2ff60a6 100644
--- a/src/plugins/wp/wpContext.mli
+++ b/src/plugins/wp/wpContext.mli
@@ -78,6 +78,8 @@ sig
val compare : t -> t -> int
end
+module MINDEX : Hashtbl.S with type key = model
+
val is_defined : unit -> bool
val on_context : context -> ('a -> 'b) -> 'a -> 'b
val get_model : unit -> model
diff --git a/src/plugins/wp/wpGenerator.ml b/src/plugins/wp/wpGenerator.ml
new file mode 100644
index 0000000000000000000000000000000000000000..8d09a45d599a2d4b85c42bca094bdfb0b296dd27
--- /dev/null
+++ b/src/plugins/wp/wpGenerator.ml
@@ -0,0 +1,233 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- WP Computer (main entry points) --- *)
+(* -------------------------------------------------------------------------- *)
+
+class type computer =
+ object
+ method model : WpContext.model
+ method add_strategy : WpStrategy.strategy -> unit
+ method add_lemma : LogicUsage.logic_lemma -> unit
+ method compute : Wpo.t Bag.t
+ end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Property Entry Point --- *)
+(* -------------------------------------------------------------------------- *)
+
+let compute_ip cc ip =
+ let open Property in match ip with
+ | IPLemma _
+ | IPAxiomatic _
+ ->
+ let rec iter cc = function
+ | IPLemma {il_name} -> cc#add_lemma (LogicUsage.logic_lemma il_name)
+ | IPAxiomatic {iax_props} -> List.iter (iter cc) iax_props
+ | _ -> ()
+ in iter cc ip ;
+ cc#compute
+ | _ ->
+ List.iter cc#add_strategy
+ (WpAnnot.get_property_strategies ~model:cc#model ip) ;
+ cc#compute
+
+(* -------------------------------------------------------------------------- *)
+(* --- Annotations Entry Point --- *)
+(* -------------------------------------------------------------------------- *)
+
+let add_kf cc ?bhv ?prop kf =
+ let model = cc#model in
+ let assigns = WpAnnot.WithAssigns in
+ List.iter cc#add_strategy
+ (WpAnnot.get_function_strategies ~model ~assigns ?bhv ?prop kf)
+
+let add_lemmas cc = function
+ | None | Some[] ->
+ LogicUsage.iter_lemmas
+ (fun lem ->
+ let idp = WpPropId.mk_lemma_id lem in
+ if WpPropId.filter_status idp then cc#add_lemma lem)
+ | Some ps ->
+ if List.mem "-@lemmas" ps then ()
+ else LogicUsage.iter_lemmas
+ (fun lem ->
+ let idp = WpPropId.mk_lemma_id lem in
+ if WpPropId.filter_status idp && WpPropId.select_by_name ps idp
+ then cc#add_lemma lem)
+
+let compute_kf cc ?kf ?bhv ?prop () =
+ begin
+ Option.iter (add_kf cc ?bhv ?prop) kf ;
+ cc#compute
+ end
+
+let compute_selection cc ?(fct=Wp_parameters.Fct_all) ?bhv ?prop () =
+ begin
+ add_lemmas cc prop ;
+ Wp_parameters.iter_fct (add_kf cc ?bhv ?prop) fct ;
+ cc#compute
+ end
+
+let compute_call cc stmt =
+ let model = cc#model in
+ List.iter cc#add_strategy (WpAnnot.get_call_pre_strategies ~model stmt) ;
+ cc#compute
+
+(* -------------------------------------------------------------------------- *)
+(* --- WPO Computer --- *)
+(* -------------------------------------------------------------------------- *)
+
+module KFmap = Kernel_function.Map
+
+module Computer(VCG : CfgWP.VCgen) =
+struct
+
+ open LogicUsage
+ module WP = Calculus.Cfg(VCG)
+
+ let prove_strategy collection model kf strategy =
+ let cfg = WpStrategy.cfg_of_strategy strategy in
+ let bhv = WpStrategy.get_bhv strategy in
+ let index = Wpo.Function( kf , bhv ) in
+ if WpRTE.missing_guards model kf then
+ Wp_parameters.warning ~current:false ~once:true
+ "Missing RTE guards" ;
+ try
+ let (results,_) = WP.compute cfg strategy in
+ List.iter
+ (fun wp ->
+ let wcs = VCG.compile_wp index wp in
+ collection := Bag.concat !collection wcs
+ ) results
+ with Warning.Error(source,reason) ->
+ Wp_parameters.failure
+ ~current:false "From %s: %s" source reason
+
+ class wp (model:WpContext.model) =
+ object
+ val mutable lemmas : LogicUsage.logic_lemma Bag.t = Bag.empty
+ val mutable annots : WpStrategy.strategy Bag.t KFmap.t = KFmap.empty
+
+ method model = model
+
+ method add_lemma lemma =
+ if Logic_utils.verify_predicate lemma.lem_predicate.tp_kind then
+ lemmas <- Bag.append lemmas lemma
+
+ method add_strategy strategy =
+ let kf = WpStrategy.get_kf strategy in
+ let sf = try KFmap.find kf annots with Not_found -> Bag.empty in
+ annots <- KFmap.add kf (Bag.append sf strategy) annots
+
+ method compute : Wpo.t Bag.t =
+ begin
+ let collection = ref Bag.empty in
+ Lang.F.release () ;
+ WpContext.on_context (model,WpContext.Global)
+ begin fun () ->
+ Bag.iter
+ (fun (l : LogicUsage.logic_lemma) ->
+ if Logic_utils.verify_predicate l.lem_predicate.tp_kind then
+ let vc = VCG.compile_lemma l in
+ collection := Bag.append !collection vc
+ ) lemmas ;
+ end () ;
+ KFmap.iter
+ (fun kf strategies ->
+ WpContext.on_context (model,WpContext.Kf kf)
+ begin fun () ->
+ LogicUsage.iter_lemmas
+ (fun (l : LogicUsage.logic_lemma) ->
+ if Logic_utils.use_predicate l.lem_predicate.tp_kind
+ then VCG.register_lemma l) ;
+ LogicUsage.iter_lemmas VCG.register_lemma ;
+ Bag.iter (prove_strategy collection model kf) strategies ;
+ end ()
+ ) annots ;
+ lemmas <- Bag.empty ;
+ annots <- KFmap.empty ;
+ Lang.F.release () ;
+ !collection
+ end
+ end
+
+end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Dump Computer --- *)
+(* -------------------------------------------------------------------------- *)
+
+module DUMPER = Calculus.Cfg(CfgDump)
+
+let dumper () =
+ let driver = Driver.load_driver () in
+ let model = Factory.(instance default driver) in
+ object
+ val mutable wptasks = []
+
+ method model = model
+
+ method add_lemma (_ : LogicUsage.logic_lemma) = ()
+
+ method add_strategy strategy =
+ wptasks <- strategy :: wptasks
+
+ method compute : Wpo.t Bag.t =
+ begin
+ (* Generates Wpos and accumulate exported goals *)
+ List.iter
+ (fun strategy ->
+ let cfg = WpStrategy.cfg_of_strategy strategy in
+ let kf = Cil2cfg.cfg_kf cfg in
+ let bhv = WpStrategy.behavior_name_of_strategy strategy in
+ CfgDump.fopen kf bhv ;
+ try
+ ignore (DUMPER.compute cfg strategy) ;
+ CfgDump.flush ()
+ with err ->
+ CfgDump.flush () ;
+ raise err
+ ) wptasks ;
+ wptasks <- [] ;
+ Bag.empty
+ end
+
+ end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Generators --- *)
+(* -------------------------------------------------------------------------- *)
+
+let generators = WpContext.MINDEX.create 1
+
+let computer setup driver =
+ let model = Factory.instance setup driver in
+ try WpContext.MINDEX.find generators model
+ with Not_found ->
+ let module VCG = (val CfgWP.vcgen setup driver) in
+ let module CC = Computer(VCG) in
+ let computer = (new CC.wp model :> computer) in
+ WpContext.MINDEX.add generators model computer ; computer
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpGenerator.mli b/src/plugins/wp/wpGenerator.mli
new file mode 100644
index 0000000000000000000000000000000000000000..a2e0cec5c9cfec7b86469cca946fa0b15f2ab38d
--- /dev/null
+++ b/src/plugins/wp/wpGenerator.mli
@@ -0,0 +1,53 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- WP Computer (main entry points) --- *)
+(* -------------------------------------------------------------------------- *)
+
+class type computer =
+ object
+ method model : WpContext.model
+ method add_strategy : WpStrategy.strategy -> unit
+ method add_lemma : LogicUsage.logic_lemma -> unit
+ method compute : Wpo.t Bag.t
+ end
+
+open Wp_parameters
+
+val compute_ip : computer -> Property.t -> Wpo.t Bag.t
+val compute_call : computer -> Cil_types.stmt -> Wpo.t Bag.t
+
+val compute_kf : computer ->
+ ?kf:Kernel_function.t ->
+ ?bhv:string list ->
+ ?prop:string list ->
+ unit -> Wpo.t Bag.t
+
+val compute_selection : computer ->
+ ?fct:functions ->
+ ?bhv:string list ->
+ ?prop:string list ->
+ unit -> Wpo.t Bag.t
+
+val dumper : unit -> computer
+val computer : Factory.setup -> Factory.driver -> computer
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 05ca307d17159ba9d542aeccebf2033da84ccdea..c3312d5f84313af0f14bb82cdfc8351ddd311322 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -115,6 +115,11 @@ let mk_assert_id kf s ca = mk_prop PKProp (mk_annot_id kf s ca)
let mk_loop_inv_id kf s ~established ca =
let kind = if established then PKEstablished else PKPreserved in
mk_prop kind (mk_annot_id kf s ca)
+
+let mk_loop_inv kf s ca =
+ mk_loop_inv_id kf s ~established:true ca,
+ mk_loop_inv_id kf s ~established:false ca
+
let mk_inv_hyp_id kf s ca = mk_prop PKPropLoop (mk_annot_id kf s ca)
let mk_var_decr_id kf s ca = mk_prop PKVarDecr (mk_annot_id kf s ca)
let mk_var_pos_id kf s ca = mk_prop PKVarPos (mk_annot_id kf s ca)
@@ -128,16 +133,16 @@ let mk_bhv_from_id kf ki a bhv from =
let id = Property.ip_of_from kf ki (Property.Id_contract (a,bhv)) from in
mk_prop PKProp (Option.get id)
-let get_kind_for_tk kf tkind = match tkind with
+let get_kind_for_tk tkind has_exit = match tkind with
| Normal ->
- if Cil2cfg.has_exit (Cil2cfg.get kf) then PKAFctOut else PKProp
+ if has_exit then PKAFctOut else PKProp
| Exits -> PKAFctExit
| _ -> assert false
-let mk_fct_from_id kf bhv tkind from =
+let mk_fct_from_id kf kf_has_exit bhv tkind from =
let contract_info = Property.Id_contract(Datatype.String.Set.empty,bhv) in
let id = Property.ip_of_from kf Kglobal contract_info from in
- let kind = get_kind_for_tk kf tkind in
+ let kind = get_kind_for_tk tkind kf_has_exit in
mk_prop kind (Option.get id)
let mk_disj_bhv_id (kf,ki,active,disj) =
@@ -160,15 +165,18 @@ let mk_loop_assigns_id kf s ca a =
let p = Property.ip_of_assigns kf (Kstmt s) ca (Writes a) in
Option.map (mk_prop PKPropLoop) p
-let mk_fct_assigns_id kf b tkind a =
+let mk_fct_assigns_id kf kf_has_exit b tkind a =
let b = Property.Id_contract(Datatype.String.Set.empty,b) in
- let kind = get_kind_for_tk kf tkind in
+ let kind = get_kind_for_tk tkind kf_has_exit in
let p = Property.ip_of_assigns kf Kglobal b (Writes a) in
Option.map (mk_prop kind) p
let mk_pre_id kf ki b p =
mk_prop PKProp (Property.ip_of_requires kf ki b p)
+let mk_post_id kf ki b p =
+ mk_prop PKProp (Property.ip_of_ensures kf ki b p)
+
let mk_stmt_post_id kf s b p =
mk_prop PKProp (Property.ip_of_ensures kf (Kstmt s) b p)
@@ -468,13 +476,13 @@ let ident_names names =
List.filter (function "" -> true
| _ as n -> '\"' <> (String.get n 0) ) names
-let pred_names p =
+let user_pred_names p =
let p_names = ident_names p.tp_statement.pred_name in
if p.tp_kind = Check then "@check"::p_names else p_names
let code_annot_names ca = match ca.annot_content with
- | AAssert (_, pred) -> "@assert" :: pred_names pred
- | AInvariant (_,_,pred) -> "@invariant":: pred_names pred
+ | AAssert (_, pred) -> "@assert" :: user_pred_names pred
+ | AInvariant (_,_,pred) -> "@invariant":: user_pred_names pred
| AVariant (term, _) -> "@variant"::(ident_names term.term_name)
| AExtended(_,_,{ext_name}) -> [Printf.sprintf "@%s" ext_name]
| _ -> [] (* TODO : add some more names ? *)
@@ -485,7 +493,7 @@ let user_prop_names p =
let open Property in match p with
| IPPredicate {ip_kind; ip_pred} ->
Format.asprintf "@@%a" Property.pretty_predicate_kind ip_kind ::
- pred_names ip_pred.ip_content
+ user_pred_names ip_pred.ip_content
| IPExtended {ie_ext={ext_name}} -> [ Printf.sprintf "@%s" ext_name ]
| IPCodeAnnot {ica_ca} -> code_annot_names ica_ca
| IPComplete {ic_bhvs} ->
@@ -503,7 +511,7 @@ let user_prop_names p =
| IPDecrease {id_ca=Some ca} -> "@decreases"::code_annot_names ca
| IPDecrease _ -> [ "@decreases" ]
| IPLemma {il_name = a; il_pred = l} ->
- let names = "@lemma"::a::pred_names l in
+ let names = "@lemma"::a::user_pred_names l in
begin
match LogicUsage.section_of_lemma a with
| LogicUsage.Toplevel _ -> names
@@ -537,7 +545,7 @@ let user_bhv_names p =
in Option.fold ~none:fors ~some:(fun b -> b.b_name :: fors) (get_behavior p)
let string_of_termination_kind = function
- Normal -> "post"
+ Normal -> "ensures"
| Exits -> "exits"
| Breaks -> "breaks"
| Continues -> "continues"
@@ -808,11 +816,13 @@ let are_selected_names asked names =
| Some false -> false
| _ -> true
-
let select_by_name asked_names pid =
let names = user_prop_pid pid in
are_selected_names asked_names names
+let select_for_behaviors bhvs pid =
+ let fors = Property.get_for_behaviors @@ property_of_id pid in
+ List.exists (fun b -> List.mem b fors) bhvs
let select_call_pre s_call asked_pre pid =
match pid.p_kind with
@@ -859,6 +869,13 @@ let mk_stmt_assigns_desc s assigns = {
a_assigns = Writes assigns ;
}
+let mk_stmt_assigns_any_desc s = {
+ a_label = Clabels.stmt s ;
+ a_stmt = Some s ;
+ a_kind = StmtAssigns ;
+ a_assigns = WritesAny ;
+}
+
let mk_init_assigns = {
a_label = Clabels.init ;
a_stmt = None ;
@@ -1100,3 +1117,87 @@ let get_induction p =
| PKEstablished|PKVarDecr|PKVarPos|PKPreserved ->
(match get_stmt (property_of_id p) with
| None -> None | Some (_, s) -> Some s)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Filter according to status --- *)
+(* -------------------------------------------------------------------------- *)
+
+let filter_status pid =
+ Wp_parameters.StatusAll.get () ||
+ begin
+ let module C = Property_status.Consolidation in
+ match C.get (property_of_id pid) with
+ | C.Never_tried -> true
+ | C.Considered_valid | C.Inconsistent _ -> false
+ | C.Valid _ | C.Valid_under_hyp _
+ | C.Invalid_but_dead _ | C.Valid_but_dead _ | C.Unknown_but_dead _ ->
+ Wp_parameters.StatusTrue.get ()
+ | C.Unknown _ -> Wp_parameters.StatusMaybe.get ()
+ | C.Invalid _ | C.Invalid_under_hyp _ -> Wp_parameters.StatusFalse.get ()
+ end
+
+(*----------------------------------------------------------------------------*)
+(* Proofs Management *)
+(*----------------------------------------------------------------------------*)
+
+type proof = {
+ target : Property.t ;
+ proved : proofpart array ;
+ mutable invalid : bool ;
+ mutable dependencies : Property.Set.t ;
+} and proofpart =
+ | Noproof
+ | Complete
+ | Parts of Bitvector.t
+
+let target p = p.target
+let dependencies p =
+ Property.Set.elements (Property.Set.remove p.target p.dependencies)
+
+let create_proof ip =
+ let n = subproofs ip in
+ {
+ target = property_of_id ip ;
+ proved = Array.make n Noproof ;
+ dependencies = Property.Set.empty ;
+ invalid = false ;
+ }
+
+let add_proof pf ip hs =
+ begin
+ if not (Property.equal (property_of_id ip) pf.target)
+ then Wp_parameters.fatal "Partial proof inconsistency" ;
+ List.iter
+ (fun iph ->
+ if not (is_requires iph) then
+ pf.dependencies <- Property.Set.add iph pf.dependencies
+ ) hs ;
+ let k = subproof_idx ip in
+ match parts_of_id ip with
+ | None -> pf.proved.(k) <- Complete
+ | Some(p,n) ->
+ match pf.proved.(k) with
+ | Complete -> ()
+ | Noproof ->
+ let bv = Bitvector.create n in
+ Bitvector.set_range bv 0 (p-1) ;
+ Bitvector.set_range bv (p+1) (n-1) ;
+ pf.proved.(k) <- Parts bv
+ | Parts bv ->
+ Bitvector.clear bv p ;
+ if Bitvector.is_empty bv
+ then pf.proved.(k) <- Complete
+ end
+
+let add_invalid_proof pf = pf.invalid <- true
+
+let is_composed pf =
+ Array.length pf.proved > 1
+
+let is_proved pf =
+ Array.for_all (function Complete -> true | _ -> false) pf.proved
+
+let is_invalid pf =
+ pf.invalid && not (is_proved pf)
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpPropId.mli b/src/plugins/wp/wpPropId.mli
index 0d380c5661766e425df4c5c93ecf73634613ca65..20ba4ab98d8f7742b304325fe97835e4e2273322 100644
--- a/src/plugins/wp/wpPropId.mli
+++ b/src/plugins/wp/wpPropId.mli
@@ -62,16 +62,18 @@ val is_smoke_test : prop_id -> bool
(** test if the prop_id does not have a [no_wp:] in its name(s). *)
val select_default : prop_id -> bool
-(** test if the prop_id has to be selected for the asked name.
- Also returns a debug message to explain then answer. Includes
- a test for [no_wp:]. *)
+(** test if the prop_id has to be selected for the asked names. *)
val select_by_name : string list -> prop_id -> bool
-(** test if the prop_id has to be selected when we want to select the call
- * precondition the the [stmt] call (None means all the call preconditions).
- * Also returns a debug message to explain then answer. *)
+(** test if the prop_id has to be selected for the asked behavior names. *)
+val select_for_behaviors : string list -> prop_id -> bool
+
+(** test if the prop_id has to be selected when we want to select the call. *)
val select_call_pre : stmt -> Property.t option -> prop_id -> bool
+(** From a list of names (of an identified terms), returns usable names. *)
+val ident_names : string list -> string list
+
(*----------------------------------------------------------------------------*)
val prop_id_keys : prop_id -> string list * string list (* required , hints *)
@@ -80,6 +82,7 @@ val get_propid : prop_id -> string (** Unique identifier of [prop_id] *)
val get_legacy : prop_id -> string (** Unique legacy identifier of [prop_id] *)
val pp_propid : Format.formatter -> prop_id -> unit (** Print unique id of [prop_id] *)
+val user_pred_names: toplevel_predicate -> string list
val user_bhv_names: Property.identified_property -> string list
val user_prop_names: Property.identified_property -> string list
val are_selected_names: string list -> string list -> bool
@@ -129,6 +132,9 @@ val mk_assert_id : kernel_function -> stmt -> code_annotation -> prop_id
val mk_loop_inv_id : kernel_function -> stmt ->
established:bool -> code_annotation -> prop_id
+(** Invariant establishment and preservation, in this order *)
+val mk_loop_inv : kernel_function -> stmt -> code_annotation -> prop_id * prop_id
+
(** Invariant used as hypothesis *)
val mk_inv_hyp_id : kernel_function -> stmt -> code_annotation -> prop_id
@@ -148,8 +154,10 @@ val mk_bhv_from_id :
kernel_function -> kinstr -> string list -> funbehavior ->
from -> prop_id
-(** \from property of function behavior assigns. Must not be [FromAny]. *)
-val mk_fct_from_id : kernel_function -> funbehavior ->
+(** \from property of function behavior assigns. Must not be [FromAny].
+ The boolean indicate whether the function has exit node or not.
+*)
+val mk_fct_from_id : kernel_function -> bool -> funbehavior ->
termination_kind -> from -> prop_id
(** disjoint behaviors property.
@@ -176,13 +184,18 @@ val mk_stmt_assigns_id :
val mk_loop_assigns_id : kernel_function -> stmt -> code_annotation ->
from list -> prop_id option
-(** function assigns *)
-val mk_fct_assigns_id : kernel_function -> funbehavior ->
+(** function assigns
+ The boolean indicate whether the function has exit node or not.
+*)
+val mk_fct_assigns_id : kernel_function -> bool -> funbehavior ->
termination_kind -> from list -> prop_id option
val mk_pre_id : kernel_function -> kinstr -> funbehavior ->
identified_predicate -> prop_id
+val mk_post_id : kernel_function -> kinstr -> funbehavior ->
+ termination_kind * identified_predicate -> prop_id
+
val mk_stmt_post_id : kernel_function -> stmt -> funbehavior ->
termination_kind * identified_predicate -> prop_id
@@ -231,6 +244,7 @@ val merge_assign_info :
val mk_loop_assigns_desc : stmt -> from list -> assigns_desc
val mk_stmt_assigns_desc : stmt -> from list -> assigns_desc
+val mk_stmt_assigns_any_desc : stmt -> assigns_desc
val mk_asm_assigns_desc : stmt -> assigns_desc
@@ -277,3 +291,33 @@ val subproof_idx : prop_id -> int
val get_induction : prop_id -> stmt option
(*----------------------------------------------------------------------------*)
+
+(*----------------------------------------------------------------------------*)
+
+(** A proof accumulator for a set of related prop_id *)
+type proof
+
+val create_proof : prop_id -> proof
+(** to be used only once for one of the related prop_id *)
+
+val add_proof : proof -> prop_id -> Property.t list -> unit
+(** accumulate in the proof the partial proof for this prop_id *)
+
+val add_invalid_proof : proof -> unit
+(** add an invalid proof result ; can not revert a complete proof *)
+
+val is_composed : proof -> bool
+(** whether a proof needs several lemma to be complete *)
+
+val is_proved : proof -> bool
+(** whether all partial proofs have been accumulated or not *)
+
+val is_invalid : proof -> bool
+(** whether an invalid proof result has been registered or not *)
+
+val target : proof -> Property.t
+val dependencies : proof -> Property.t list
+
+val filter_status : prop_id -> bool
+
+(*----------------------------------------------------------------------------*)
diff --git a/src/plugins/wp/wpStrategy.ml b/src/plugins/wp/wpStrategy.ml
index a3e11ddd1d1e2f26fdc086dc4defd558932575a7..1385c9083189e6c15547c5e1bf5ca864367c5012 100644
--- a/src/plugins/wp/wpStrategy.ml
+++ b/src/plugins/wp/wpStrategy.ml
@@ -196,7 +196,7 @@ let add_prop_fct_pre acc kind kf bhv ~assumes pre =
let add_prop_fct_post acc kind kf bhv tkind post =
if verify_predicate post.ip_content.tp_kind then begin
let id = WpPropId.mk_fct_post_id kf bhv (tkind, post) in
- let labels = NormAtLabels.labels_fct_post in
+ let labels = NormAtLabels.labels_fct_post ~exit:false in
let p = Logic_const.pred_of_id_pred post in
let p = normalize id labels p in
add_prop acc kind id p
@@ -234,7 +234,7 @@ let add_prop_stmt_spec_pre acc kind kf s spec =
let add_prop_stmt_post acc kind kf s bhv tkind l_post ~assumes post =
if verify_predicate post.ip_content.tp_kind then begin
let id = WpPropId.mk_stmt_post_id kf s bhv (tkind, post) in
- let labels = NormAtLabels.labels_stmt_post ~kf s l_post in
+ let labels = NormAtLabels.labels_stmt_post_l ~kf s l_post in
let p = Logic_const.pred_of_id_pred post in
let p = normalize id labels ?assumes p in
add_prop acc kind id p
@@ -261,14 +261,14 @@ let add_prop_call_pre acc kind id ~assumes pre =
let add_prop_call_post acc kind called_kf bhv tkind ~assumes post =
let id = WpPropId.mk_fct_post_id called_kf bhv (tkind, post) in
- let labels = NormAtLabels.labels_fct_post in
+ let labels = NormAtLabels.labels_fct_post ~exit:false in
let p = Logic_const.pred_of_id_pred post in
let p = normalize id labels ~assumes p in
add_prop acc kind id p
let add_prop_assert acc kind kf s ca p =
let id = WpPropId.mk_assert_id kf s ca in
- let labels = NormAtLabels.labels_assert_before ~kf s in
+ let labels = NormAtLabels.labels_assert ~kf s in
let p = normalize id labels p in
add_prop acc kind id p
@@ -410,7 +410,7 @@ let add_stmt_spec_assigns_hyp acc kf s l_post spec =
| None -> add_assigns_any acc Ahyp
(WpPropId.mk_stmt_any_assigns_info s)
| Some id ->
- let labels = NormAtLabels.labels_stmt_assigns ~kf s l_post in
+ let labels = NormAtLabels.labels_stmt_assigns_l ~kf s l_post in
let assigns = NormAtLabels.preproc_assigns labels assigns in
let a_desc = WpPropId.mk_stmt_assigns_desc s assigns in
add_assigns acc Ahyp id a_desc
@@ -439,7 +439,7 @@ let add_call_assigns_hyp acc kf_caller s ~called_kf l_post spec_opt =
add_assigns_any acc (AcallHyp called_kf) asgn
| Some pid ->
let kf = kf_caller in
- let labels = NormAtLabels.labels_stmt_assigns ~kf s l_post in
+ let labels = NormAtLabels.labels_stmt_assigns_l ~kf s l_post in
let assigns = NormAtLabels.preproc_assigns labels assigns in
let a_desc = WpPropId.mk_stmt_assigns_desc s assigns in
add_assigns acc (AcallHyp called_kf) pid a_desc
@@ -471,13 +471,14 @@ let add_fct_bhv_assigns_hyp acc kf tkind b = match b.b_assigns with
let id = WpPropId.mk_kf_any_assigns_info () in
add_assigns_any acc Ahyp id
| Writes assigns ->
- let id = WpPropId.mk_fct_assigns_id kf b tkind assigns in
+ let has_exit = Cil2cfg.has_exit (Cil2cfg.get kf) in
+ let id = WpPropId.mk_fct_assigns_id kf has_exit b tkind assigns in
match id with
| None ->
let id = WpPropId.mk_kf_any_assigns_info () in
add_assigns_any acc Ahyp id
| Some id ->
- let labels = NormAtLabels.labels_fct_assigns in
+ let labels = NormAtLabels.labels_fct_assigns ~exit:false in
let assigns' = NormAtLabels.preproc_assigns labels assigns in
let a_desc = WpPropId.mk_kf_assigns_desc assigns' in
add_assigns acc Ahyp id a_desc
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 96bdd3930df12e2b045c09cd426ed8c8ce5f40c3..38c898654f4ac51b3d37cb85bbe5d1e2c80b11e4 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -44,7 +44,7 @@ let has_dkey (k:category) = is_debug_key_enabled k
(* --- WP Generation --- *)
(* ------------------------------------------------------------------------ *)
-let wp_generation = add_group "Goal Selection"
+let wp_generation = add_group "Goal Generator"
let () = Parameter_customize.set_group wp_generation
let () = Parameter_customize.do_not_save ()
@@ -55,6 +55,21 @@ module WP =
end)
let () = on_reset WP.clear
+let () = Parameter_customize.set_group wp_generation
+module Legacy =
+ True(struct
+ let option_name = "-wp-legacy"
+ let help = "Use legacy generator engine."
+ end)
+
+let () = Parameter_customize.set_group wp_generation
+module Dump =
+ Action(struct
+ let option_name = "-wp-dump"
+ let help = "Dump WP calculus graph."
+ end)
+let () = on_reset Dump.clear
+
let () = Parameter_customize.set_group wp_generation
let () = Parameter_customize.do_not_save ()
module Functions =
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index a7ce251dd60d391185176f047d52420b314c94ba..2bb0a1fea14799a4fc2f5ed9cb40d536343baa8c 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -39,6 +39,8 @@ val iter_kf : (Kernel_function.t -> unit) -> unit
(** {2 Goal Selection} *)
module WP : Parameter_sig.Bool
+module Dump : Parameter_sig.Bool
+module Legacy : Parameter_sig.Bool
module Behaviors : Parameter_sig.String_list
module Properties : Parameter_sig.String_list
module StatusAll : Parameter_sig.Bool
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 1490b3613ebf5b7eac3dc7cb2efd8cbbd6e3ae0c..0d0bf47c4f8059caf2d74312150bcc67f866f3ae 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -578,7 +578,7 @@ type system = {
mutable wpo_ip : WPOset.t Pmap.t ; (* ip -> WPOs *)
mutable age : int WPOmap.t ; (* wpo -> age *)
mutable results : Results.t WPOmap.t ; (* results collector *)
- proofs : WpAnnot.proof Hproof.t ; (* proof collector *)
+ proofs : WpPropId.proof Hproof.t ; (* proof collector *)
}
let create_system () =
@@ -707,11 +707,11 @@ let get_proof g =
try
let proof = Hproof.find system.proofs (proof g target) in
if is_smoke_test g then
- if WpAnnot.is_proved proof then `Failed else
- if WpAnnot.is_invalid proof then `Passed else
+ if WpPropId.is_proved proof then `Failed else
+ if WpPropId.is_invalid proof then `Passed else
`Unknown
else
- if WpAnnot.is_proved proof then `Passed else `Unknown
+ if WpPropId.is_proved proof then `Passed else `Unknown
with Not_found -> `Unknown
in status , target
@@ -719,7 +719,7 @@ let find_proof system g =
let pi = proof g (WpPropId.property_of_id g.po_pid) in
try Hproof.find system.proofs pi
with Not_found ->
- let proof = WpAnnot.create_proof g.po_pid in
+ let proof = WpPropId.create_proof g.po_pid in
Hproof.add system.proofs pi proof ; proof
let clear_results g =
@@ -746,18 +746,18 @@ let set_result g p r =
let smoke = is_smoke_test g in
let proof = find_proof system g in
let emitter = WpContext.get_emitter g.po_model in
- let target = WpAnnot.target proof in
- let unproved = not (WpAnnot.is_proved proof) in
+ let target = WpPropId.target proof in
+ let unproved = not (WpPropId.is_proved proof) in
if VCS.is_valid r then
- WpAnnot.add_proof proof g.po_pid (get_depend g)
+ WpPropId.add_proof proof g.po_pid (get_depend g)
else if smoke then
- WpAnnot.add_invalid_proof proof ;
- let proved = WpAnnot.is_proved proof in
+ WpPropId.add_invalid_proof proof ;
+ let proved = WpPropId.is_proved proof in
let status =
if smoke then
if proved
then Property_status.False_if_reachable (* All goals SAT *)
- else if WpAnnot.is_invalid proof
+ else if WpPropId.is_invalid proof
then Property_status.True (* Some goal is UNSAT *)
else Property_status.Dont_know (* Not finished yet *)
else
@@ -765,7 +765,7 @@ let set_result g p r =
then Property_status.True
else Property_status.Dont_know
in
- let hyps = if smoke then [] else WpAnnot.dependencies proof in
+ let hyps = if smoke then [] else WpPropId.dependencies proof in
Property_status.emit emitter ~hyps target status ;
if smoke && unproved && proved then WpReached.set_doomed emitter g.po_pid ;
end
@@ -988,3 +988,21 @@ let get_files w =
) results []
in
descr_files @ result_files
+
+(* -------------------------------------------------------------------------- *)
+(* --- Generators --- *)
+(* -------------------------------------------------------------------------- *)
+
+class type generator =
+ object
+ method model : WpContext.model
+ method compute_ip : Property.t -> t Bag.t
+ method compute_call : stmt -> t Bag.t
+ method compute_main :
+ ?fct:Wp_parameters.functions ->
+ ?bhv:string list ->
+ ?prop:string list ->
+ unit -> t Bag.t
+ end
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpo.mli b/src/plugins/wp/wpo.mli
index f2c11d5a7917e4ebdc2ded2d1b3deaaec7e582cd..98e14b7efc254befdda2e7a1c6eecfb4942c2f8f 100644
--- a/src/plugins/wp/wpo.mli
+++ b/src/plugins/wp/wpo.mli
@@ -210,3 +210,29 @@ val pp_goal_flow : Format.formatter -> t -> unit
(** Dynamically exported. *)
val prover_of_name : string -> prover option
+
+(* -------------------------------------------------------------------------- *)
+(* --- Generators --- *)
+(* -------------------------------------------------------------------------- *)
+
+(** VC Generator interface. *)
+
+class type generator =
+ object
+ method model : WpContext.model
+ (** Generate VCs for the given Property. *)
+ method compute_ip : Property.t -> t Bag.t
+ (** Generate VCs for call preconditions at the given statement. *)
+ method compute_call : stmt -> t Bag.t
+ (** Generate VCs for all functions
+ matching provided behaviors and property names.
+ For `~bhv` and `~prop` optional arguments,
+ default and empty list means {i all} properties. *)
+ method compute_main :
+ ?fct:Wp_parameters.functions ->
+ ?bhv:string list ->
+ ?prop:string list ->
+ unit -> t Bag.t
+ end
+
+(* -------------------------------------------------------------------------- *)