diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 268a75ba7ac3a2a3e46b6db0999fdaab0ef45fd0..725a619c8beb36678f15ad26c8547dc70cdb929f 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1782,8 +1782,6 @@ src/plugins/wp/Why3Provers.mli: CEA_WP
src/plugins/wp/Wp.mli: .ignore
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
@@ -1798,8 +1796,6 @@ 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
-src/plugins/wp/cil2cfg.mli: CEA_WP
src/plugins/wp/clabels.ml: CEA_WP
src/plugins/wp/clabels.mli: CEA_WP
src/plugins/wp/configure.ac: CEA_WP
@@ -1938,12 +1934,8 @@ src/plugins/wp/share/why3/frama_c_wp/qed.mlw: CEA_WP
src/plugins/wp/share/why3/frama_c_wp/vlist.mlw: CEA_WP
src/plugins/wp/share/why3/frama_c_wp/vset.mlw: CEA_WP
src/plugins/wp/share/wp.driver: CEA_WP
-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
@@ -1952,8 +1944,6 @@ src/plugins/wp/wpReport.ml: CEA_WP
src/plugins/wp/wpReport.mli: CEA_WP
src/plugins/wp/wpRTE.ml: CEA_WP
src/plugins/wp/wpRTE.mli: CEA_WP
-src/plugins/wp/wpStrategy.ml: CEA_WP
-src/plugins/wp/wpStrategy.mli: CEA_WP
src/plugins/wp/wpTarget.ml: CEA_WP
src/plugins/wp/wpTarget.mli: CEA_WP
src/plugins/wp/wp_error.ml: CEA_WP
diff --git a/src/kernel_services/ast_data/globals.ml b/src/kernel_services/ast_data/globals.ml
index 440ea2a0b01a171985775a675ee0be2b3015f255..d4c0e7a40739f78a3d16d0e9c599531f567de6d5 100644
--- a/src/kernel_services/ast_data/globals.ml
+++ b/src/kernel_services/ast_data/globals.ml
@@ -847,6 +847,13 @@ let set_entry_point name lib =
Kernel.LibEntry.unsafe_set lib;
end
+let is_entry_point ?when_lib_entry kf =
+ match when_lib_entry with
+ | Some value when Kernel.LibEntry.get () -> value
+ | _ ->
+ try Cil_datatype.Kf.equal kf @@ fst @@ entry_point ()
+ with No_such_entry_point _ -> false
+
(* ************************************************************************* *)
(** {2 Global Comments} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/ast_data/globals.mli b/src/kernel_services/ast_data/globals.mli
index d5a9e9faf8da86ccabce9e67ed20aa424d04a72c..a4379263ec9991891fc6fc1d144e32af6bfda490 100644
--- a/src/kernel_services/ast_data/globals.mli
+++ b/src/kernel_services/ast_data/globals.mli
@@ -293,6 +293,14 @@ val set_entry_point : string -> bool -> unit
[Kernel.MainFunction] or [Kernel.LibEntry].
@plugin development guide *)
+val is_entry_point : ?when_lib_entry:bool -> kernel_function -> bool
+(** @return [true] iff the given kernel function is the entry point.
+ The optional parameter [when_lib_entry] overrides the result if we are
+ in -lib-entry mode.
+
+ @since Frama-C+dev
+*)
+
(* ************************************************************************* *)
(** {2 Comments} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index e40b51a88db810af67d5bbcdc17dbfe36bf3861d..6c0fad4721f7abdca0b103532ecd9763713e4618 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -3899,6 +3899,10 @@ and typeTermOffset basetyp =
let isConstType typ_lval = typeHasAttributeMemoryBlock "const" typ_lval
+let isGlobalInitConst vi =
+ (* Note: the type must be fully const, not a part of it *)
+ vi.vglob && vi.vstorage <> Extern && typeHasQualifier "const" vi.vtype
+
(**** Check for volatile attribute ****)
let isVolatileType typ_lval = typeHasAttributeMemoryBlock "volatile" typ_lval
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 73ca309ceeec5c8cad167b250cd8066755246508..bb03f8fb2cdf84315404d8dd357e75203c500abb 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1303,6 +1303,14 @@ val isGhostFormalVarinfo: varinfo -> bool
*)
val isGhostFormalVarDecl: (string * typ * attributes) -> bool
+
+(** [true] iff the given variable is a const global variable with non extern
+ storage.
+
+ @since Frama-C+dev
+*)
+val isGlobalInitConst: varinfo -> bool
+
(** Remove attributes whose name appears in the first argument that are
present anywhere in the fully expanded version of the type.
@since Oxygen-20120901
diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index 2661b7572e3ec5d2ce5155fbca313e9155c447ed..36fec2b95781966600bf4d0f6fe2fae24c306611 100644
--- a/src/plugins/wp/Factory.ml
+++ b/src/plugins/wp/Factory.ml
@@ -174,9 +174,9 @@ let is_ptr x = Cil.isPointerType x.Cil_types.vtype
let is_fun_ptr x = Cil.isFunctionType x.Cil_types.vtype
let is_formal_ptr x = x.Cil_types.vformal && is_ptr x
let is_init kf x =
- WpStrategy.is_main_init kf ||
+ Globals.is_entry_point ~when_lib_entry:false kf ||
Wp_parameters.AliasInit.get () ||
- ( WpStrategy.isInitConst () && WpStrategy.isGlobalInitConst x )
+ ( Wp_parameters.Init.get () && Cil.isGlobalInitConst x )
let refusage_param ~byref ~context x =
let kf,init = match WpContext.get_scope () with
diff --git a/src/plugins/wp/Generator.ml b/src/plugins/wp/Generator.ml
index 425a2b4ca9bab6bf6e494abd77b7d5321d3c1a69..0cf4ea60e130dfeb02a125c0dfcf7c77fb246285 100644
--- a/src/plugins/wp/Generator.ml
+++ b/src/plugins/wp/Generator.ml
@@ -70,28 +70,14 @@ let user_setup () : Factory.setup =
(* -------------------------------------------------------------------------- *)
let create
- ?dump ?legacy
+ ?dump
?(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 aead35c64025fcf62bcfaf1a2fee33895da8d4b7..0ed7ad45a6c13c7328f5763a2b190b2adea8da71 100644
--- a/src/plugins/wp/Generator.mli
+++ b/src/plugins/wp/Generator.mli
@@ -29,7 +29,6 @@ val user_setup : unit -> Factory.setup
val create :
?dump:bool ->
- ?legacy:bool ->
?setup:Factory.setup ->
?driver:Factory.driver ->
unit -> Wpo.generator
diff --git a/src/plugins/wp/GuiNavigator.ml b/src/plugins/wp/GuiNavigator.ml
index 890ac610af824bce32e788d3345a17bf97a7755b..49b85d6d68588a439e1069d0f4259f649f18e274 100644
--- a/src/plugins/wp/GuiNavigator.ml
+++ b/src/plugins/wp/GuiNavigator.ml
@@ -414,7 +414,7 @@ let model_varinfo :
| PTermLval(Some kf, _, _, (TVar {lv_origin=Some x},TNoOffset))
when button=1 && RefUsage.is_computed () ->
begin
- let init = WpStrategy.is_main_init kf in
+ let init = Globals.is_entry_point ~when_lib_entry:false kf in
let acc = RefUsage.get ~kf ~init x in
let model = match acc with
| RefUsage.NoAccess -> "any"
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index c45d0439131d37ea213d85f8ace3f15580456644..afc9ef27123cc365fa69e9ac81b39ccb9a6b8468 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -68,7 +68,7 @@ PLUGIN_CMO:= \
LogicUsage RefUsage \
Layout Region \
RegionAnnot RegionAccess RegionDump RegionAnalysis \
- cil2cfg normAtLabels wpPropId wpStrategy \
+ normAtLabels wpPropId \
Lang Repr Matrix Passive Splitter \
LogicBuiltins Definitions \
Cmath Cint Cfloat Vset Vlist Cstring Cvalues \
@@ -82,7 +82,7 @@ PLUGIN_CMO:= \
Sigma MemLoader MemDebug \
MemEmpty MemZeroAlias MemVar \
MemMemory MemTyped MemRegion MemVal \
- wpReached wpRTE wpAnnot wpTarget \
+ wpReached wpRTE wpTarget \
CfgCompiler StmtSemantics \
VCS script proof wpo wpReport \
Footprint Tactical Strategy \
@@ -99,8 +99,8 @@ PLUGIN_CMO:= \
driver prover ProverSearch ProverScript \
Factory \
cfgInit cfgAnnot cfgInfos cfgCalculus \
- calculus cfgDump cfgWP \
- wpGenerator cfgGenerator \
+ cfgDump cfgWP \
+ cfgGenerator \
Generator register VC
PLUGIN_CMI:= \
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 092d9ea11fd3cfee16d9867de035470ccb25e26e..9d845883439b776bee5ede25aea258c3f81e3c0a 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -55,7 +55,8 @@ struct
let hypotheses p =
let kf,init = match WpContext.get_scope () with
| WpContext.Global -> None,false
- | WpContext.Kf f -> Some f, WpStrategy.is_main_init f in
+ | WpContext.Kf f ->
+ Some f, Globals.is_entry_point ~when_lib_entry:false f in
let w = ref p in
V.iter ?kf ~init (fun vi -> w := MemoryContext.set vi (V.param vi) !w) ;
M.hypotheses !w
diff --git a/src/plugins/wp/StmtSemantics.ml b/src/plugins/wp/StmtSemantics.ml
index b068e462498a28251561510c8acd4ff0fe6a0b6e..83b9e66d8605a49169b2b8672953a2df13ea7234 100644
--- a/src/plugins/wp/StmtSemantics.ml
+++ b/src/plugins/wp/StmtSemantics.ml
@@ -666,7 +666,7 @@ struct
let init ~is_pre_main env =
let ninit = (env @: Clabels.init) in
let sinit = Sigma.create () in
- (** todo WpStrategy.is_main_init, need to test that seq.pre is the
+ (** todo Globals.is_entry_point kf, need to test that seq.pre is the
start of the function *)
(** todo warning *)
let cfg_init = Globals.Vars.fold_in_file_order
@@ -690,10 +690,10 @@ struct
let sconst = Sigma.havoc_any ~call:false sinit in
let havoc = Cfg.E.create {pre=sinit; post=sconst} Lang.F.p_true in
let consts =
- if WpStrategy.isInitConst () then
+ if Wp_parameters.Init.get () then
Globals.Vars.fold_in_file_order
(fun var _ cfg ->
- if WpStrategy.isGlobalInitConst var
+ if Cil.isGlobalInitConst var
then
let h = (C.unchanged sconst sinit var) in
let h = Cfg.P.create
@@ -770,7 +770,8 @@ struct
let posts = { pre = Cfg.node (); post = Cfg.node () } in
let env = empty_env kf @* [Clabels.pre,pres.post;Clabels.post,posts.pre] in
(* initialization *)
- let init = init ~is_pre_main:(WpStrategy.is_main_init kf)
+ let init =
+ init ~is_pre_main:(Globals.is_entry_point ~when_lib_entry:false kf)
(env @* [Clabels.here,pres.pre]) in
(* pre-condition *)
let pre =
diff --git a/src/plugins/wp/calculus.ml b/src/plugins/wp/calculus.ml
deleted file mode 100644
index 5cb2133bb68bc2fac5644b88672b91e7e740947e..0000000000000000000000000000000000000000
--- a/src/plugins/wp/calculus.ml
+++ /dev/null
@@ -1,683 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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 computation using the CFG *)
-
-open Cil_types
-open Cil_datatype
-
-module Cfg (W : Mcfg.S) = struct
-
- let dkey = Wp_parameters.register_category "calculus" (* Debugging key *)
- let debug fmt = Wp_parameters.debug ~dkey fmt
-
- (** Before storing something at a program point, we have to process the label
- * at that point. *)
- let do_labels wenv e obj =
- let do_lab s o l = W.label wenv s l o in
- let obj = do_lab None obj Clabels.here in
- let stmt = Cil2cfg.get_edge_stmt e in
- let labels = Cil2cfg.get_edge_labels e in
- List.fold_left (do_lab stmt) obj labels
-
- let add_hyp wenv obj h =
- debug "add hyp %a@." WpPropId.pp_pred_info h;
- W.add_hyp wenv h obj
-
- let add_goal wenv obj g =
- debug "add goal %a@." WpPropId.pp_pred_info g;
- W.add_goal wenv g obj
- (*[LC] Adding scopes for loop invariant preservation: WHY ???? *)
- (*[LC] Nevertheless, if required, this form should be used (BTS #1462)
-
- let open_scope wenv formals blocks =
- List.fold_right
- (fun b obj -> W.scope wenv b.blocals Mcfg.SC_Block_out obj)
- blocks
- (W.scope wenv formals Mcfg.SC_Function_out W.empty)
-
-
- match WpPropId.is_loop_preservation (fst g) with
- | None -> W.add_goal wenv g obj
- | Some stmt ->
- debug "add scope for loop preservation %a@." WpPropId.pp_pred_info g ;
- let blocks = Kernel_function.find_all_enclosing_blocks stmt in
- let kf = Kernel_function.find_englobing_kf stmt in
- let formals = Kernel_function.get_formals kf in
- W.merge wenv (W.add_goal wenv g (open_scope wenv formals blocks)) obj
- *)
-
- let add_assigns_goal wenv obj g_assigns = match g_assigns with
- | WpPropId.AssignsAny _ | WpPropId.NoAssignsInfo -> obj
- | WpPropId.AssignsLocations a ->
- debug "add assign goal (@[%a@])@."
- WpPropId.pretty (WpPropId.assigns_info_id a);
- W.add_assigns wenv a obj
-
- 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 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 None a obj in
- Some a.WpPropId.a_label, obj
- | WpPropId.NoAssignsInfo -> None, obj
-
- (** detect if the computation of the result at [edge] is possible,
- * or if it will loop. If [strategy] are provide,
- * cut are done on edges with cut properties,
- * and if not, cut are done on loop node back edge if any.
- * TODO: maybe this should be done while building the strategy ?
- * *)
- exception Stop of Cil2cfg.edge
- let test_edge_loop_ok cfg strategy edge =
- debug "[test_edge_loop_ok] (%s strategy) for %a"
- (match strategy with None -> "without" | Some _ -> "with")
- Cil2cfg.pp_edge edge;
- let rec collect_edge_preds set e =
- let cut =
- match strategy with None -> Cil2cfg.is_back_edge e
- | Some strategy ->
- let e_annots = WpStrategy.get_annots strategy e in
- (WpStrategy.get_cut e_annots <> [])
- in
- if cut then () (* normal loop cut *)
- else if Cil2cfg.Eset.mem e set
- then (* e is already in set : loop without cut ! *)
- raise (Stop e)
- else (* add e to set and continue with its preds *)
- let set = Cil2cfg.Eset.add e set in
- let preds = Cil2cfg.pred_e cfg (Cil2cfg.edge_src e) in
- List.iter (collect_edge_preds set) preds
- in
- try
- let _ = collect_edge_preds Cil2cfg.Eset.empty edge in
- debug "[test_edge_loop_ok] ok.";
- true
- with Stop e ->
- begin
- debug "[test_edge_loop_ok] loop without cut detected at %a"
- Cil2cfg.pp_edge e;
- false
- end
-
- (** to store the results of computations :
- * we store a result for each edge, and also a list of proof obligations.
- *
- * Be careful that there are two modes of computation :
- * the first one ([Pass1]) is used to prove the establishment of properties
- * while the second (after [change_mode_if_needed]) prove the preservation.
- * See {!R.set} for more details.
- * *)
- module R : sig
- type t
- val empty : Cil2cfg.t -> t
- val is_pass1 : t -> bool
- val change_mode_if_needed : t -> unit
- val find : t -> Cil2cfg.edge -> W.t_prop
- val set : WpStrategy.strategy -> W.t_env ->
- t -> Cil2cfg.edge -> W.t_prop -> W.t_prop
- val add_oblig : t -> Clabels.c_label -> W.t_prop -> unit
- val add_memo : t -> Cil2cfg.edge -> W.t_prop -> unit
- end =
- struct
- type t_mode = Pass1 | Pass2
-
- module HE = Cil2cfg.HE (struct type t = W.t_prop option end)
-
- module LabObligs : sig
- type t
- val empty : t
- val is_empty : t -> bool
- val get_of_label : t -> Clabels.c_label -> W.t_prop list
- val get_of_edge : t -> Cil2cfg.edge -> W.t_prop list
- val add_to_label : t -> Clabels.c_label -> W.t_prop -> t
- val add_to_edge : t -> Cil2cfg.edge -> W.t_prop -> t
- end = struct
-
- type key = Olab of Clabels.c_label | Oedge of Cil2cfg.edge
-
- let cmp_key k1 k2 = match k1, k2 with
- | Olab l1, Olab l2 when Clabels.equal l1 l2 -> true
- | Oedge e1, Oedge e2 when Cil2cfg.same_edge e1 e2 -> true
- | _ -> false
-
- (* TODOopt: could have a sorted list... *)
- type t = (key * W.t_prop list) list
-
- let empty = []
-
- let is_empty obligs = (obligs = [])
-
- let add obligs k obj =
- let rec aux l_obligs = match l_obligs with
- | [] -> (k, [obj])::[]
- | (k', obligs)::tl when cmp_key k k' ->
- (k, obj::obligs)::tl
- | o::tl -> o::(aux tl)
- in aux obligs
-
- let add_to_label obligs label obj = add obligs (Olab label) obj
-
- let add_to_edge obligs e obj = add obligs (Oedge e) obj
-
- let get obligs k =
- let rec aux l_obligs = match l_obligs with
- | [] -> []
- | (k', obligs)::_ when cmp_key k k' -> obligs
- | _::tl -> aux tl
- in aux obligs
-
- let get_of_label obligs label = get obligs (Olab label)
-
- let get_of_edge obligs e = get obligs (Oedge e)
-
- end
-
- type t = {
- mutable mode : t_mode ;
- cfg: Cil2cfg.t;
- tbl : HE.t ;
- mutable memo : LabObligs.t;
- mutable obligs : LabObligs.t;
- }
-
- let empty cfg =
- debug "start computing (pass 1)@.";
- { mode = Pass1; cfg = cfg; tbl = HE.create 97 ;
- obligs = LabObligs.empty ; memo = LabObligs.empty ;}
-
- let is_pass1 res = (res.mode = Pass1)
-
- let add_oblig res label obj =
- debug "add proof obligation at label %a =@. @[<hov2> %a@]@."
- Clabels.pretty label W.pretty obj;
- res.obligs <- LabObligs.add_to_label (res.obligs) label obj
-
- let add_memo res e obj =
- debug "Memo goal for Pass2 at %a=@. @[<hov2> %a@]@."
- Cil2cfg.pp_edge e W.pretty obj;
- res.memo <- LabObligs.add_to_edge (res.memo) e obj
-
- let find res e =
- let obj = HE.find res.tbl e in
- match obj with None ->
- Wp_parameters.warning "find edge annot twice (%a) ?"
- Cil2cfg.pp_edge e;
- raise Not_found
- | Some obj ->
- if (res.mode = Pass2)
- && (List.length
- (Cil2cfg.pred_e res.cfg (Cil2cfg.edge_src e)) < 2) then
- begin
- (* it should be used once only : can free it *)
- HE.replace res.tbl e None;
- debug "clear edge %a@." Cil2cfg.pp_edge e
- end;
- obj
-
- (** If needed, clear wp table to compute Pass2.
- * If nothing has been stored in res.memo, there is nothing to do. *)
- let change_mode_if_needed res =
- if LabObligs.is_empty res.memo then ()
- else
- begin
- debug "change to Pass2 (clear wp table)@.";
- begin try
- let e_start = Cil2cfg.start_edge res.cfg in
- let start_goal = find res e_start in
- add_memo res e_start start_goal
- with Not_found -> ()
- end;
- HE.clear res.tbl;
- (* move memo obligs of Pass1 to obligs for Pass2 *)
- res.obligs <- res.memo;
- res.memo <- LabObligs.empty;
- res.mode <- Pass2
- end
-
- let collect_oblig wenv res e obj =
- let labels = Cil2cfg.get_edge_labels e in
- let add obj obligs =
- List.fold_left (fun obj o -> W.merge wenv o obj) obj obligs
- in
- let obj =
- try
- debug "get proof obligation at edge %a@." Cil2cfg.pp_edge e;
- let obligs = LabObligs.get_of_edge res.obligs e in
- add obj obligs
- with Not_found -> obj
- in
- let add_lab_oblig obj label =
- try
- debug "get proof obligation at label %a@." Clabels.pretty label;
- let obligs = LabObligs.get_of_label res.obligs label in
- add obj obligs
- with Not_found -> obj
- in
- let obj = List.fold_left add_lab_oblig obj labels in
- obj
-
-
- (** We have found some assigns hypothesis in the strategy :
- * it means that we skip the corresponding bloc, ie. we directly compute
- * the result before the block : (forall assigns. P),
- * and continue with empty. *)
- let use_assigns wenv res obj h_assigns =
- let lab, obj = add_assigns_hyp wenv obj h_assigns in
- match lab with
- | None -> obj
- | Some label -> add_oblig res label obj; W.empty
-
- (** store the result p for the computation of the edge e.
- *
- * - In Compute mode :
- if we have some hyps H about this edge, store H => p
- if we have some goal G about this edge, store G /\ p
- if we have annotation B to be used as both H and G, store B /\ B=>P
- We also have to add H and G from HI (invariants computed in Pass1 mode)
- So finally, we build : [ H => [ BG /\ (BH => (G /\ P)) ] ]
- *)
- let set strategy wenv res e obj =
- try
- match (HE.find res.tbl e) with
- | None -> raise Not_found
- | Some obj -> obj
- (* cannot warn here because it can happen with CUT properties.
- * We could check that obj is the same thing than the founded result *)
- (* Wp_parameters.fatal "strange loop at %a ?" Cil2cfg.pp_edge e *)
- with Not_found ->
- begin
- let e_annot = WpStrategy.get_annots strategy e in
- let h_prop = WpStrategy.get_hyp_only e_annot in
- let g_prop = WpStrategy.get_goal_only e_annot in
- let bh_prop, bg_prop = WpStrategy.get_both_hyp_goals e_annot in
- let h_assigns = WpStrategy.get_asgn_hyp e_annot in
- let g_assigns = WpStrategy.get_asgn_goal e_annot in
- (* get_cut is ignored : see get_wp_edge *)
- let obj = collect_oblig wenv res e obj in
- let is_loop_head =
- match Cil2cfg.node_type (Cil2cfg.edge_src e) with
- | Cil2cfg.Vloop (Some _, _) -> true
- | _ -> false
- in
- let compute ~goal obj =
- let local_add_goal obj g =
- if goal then add_goal wenv obj g else obj
- in
- let obj = List.fold_left (local_add_goal) obj g_prop in
- let obj = List.fold_left (add_hyp wenv) obj bh_prop in
- let obj =
- if goal then add_assigns_goal wenv obj g_assigns else obj
- in
- let obj = List.fold_left (local_add_goal) obj bg_prop in
- let obj = List.fold_left (add_hyp wenv) obj h_prop in
- obj
- in
- let obj = match res.mode with
- | Pass1 -> compute ~goal:true obj
- | Pass2 -> compute ~goal:false obj
- in
- let obj = do_labels wenv e obj in
- let obj =
- if is_loop_head then obj (* assigns used in [wp_loop] *)
- else use_assigns wenv res obj h_assigns
- in
- debug "[set_wp_edge] %a@." Cil2cfg.pp_edge e;
- debug " = @[<hov2> %a@]@." W.pretty obj;
- Format.print_flush ();
- HE.replace res.tbl e (Some obj);
- find res e (* this should give back obj, but also do more things *)
- end
-
- end (* module R *)
-
-
- let use_loop_assigns strategy wenv e obj =
- let e_annot = WpStrategy.get_annots strategy e in
- let h_assigns = WpStrategy.get_asgn_hyp e_annot in
- let label, obj = add_assigns_hyp wenv obj h_assigns in
- match label with Some _ -> obj
- | None -> assert false (* we should have assigns hyp for loops !*)
-
- (** Compute the result for edge [e] which goes to the loop node [nloop].
- * So [e] can be either a back_edge or a loop entry edge.
- * Be very careful not to make an infinite loop by calling [get_loop_head]...
- * *)
- let wp_loop ((_, cfg, strategy, _, wenv)) nloop e get_loop_head =
- let loop_with_quantif () =
- if Cil2cfg.is_back_edge e then
- (* Be careful not to use get_only_succ here (infinite loop) *)
- (debug "[wp_loop] cut at back edge";
- W.empty)
- else (* edge going into the loop from outside : quantify *)
- begin
- debug "[wp_loop] quantify";
- let obj = get_loop_head nloop in
- let head = match Cil2cfg.succ_e cfg nloop with
- | [h] -> h
- | _ -> assert false (* already detected in [get_loop_head] *)
- in use_loop_assigns strategy wenv head obj
- end
- in
- (*
- if WpStrategy.new_loop_computation strategy
- && R.is_pass1 res
- && loop_with_cut cfg strategy nloop
- then
- loop_with_cut_pass1 ()
- else (* old mode or no inv or pass2 *)
- *)
- match Cil2cfg.node_type nloop with
- | Cil2cfg.Vloop (Some true, _) -> (* natural loop (has back edges) *)
- loop_with_quantif ()
- | _ -> (* TODO : print info about the loop *)
- Wp_error.unsupported
- "non-natural loop without invariant property."
-
- type callenv = {
- pre_annots : WpStrategy.t_annots ;
- post_annots : WpStrategy.t_annots ;
- exit_annots : WpStrategy.t_annots ;
- }
-
- let callenv cfg strategy v =
- let eb = match Cil2cfg.pred_e cfg v with e::_ -> e | _ -> assert false in
- let en, ee = Cil2cfg.get_call_out_edges cfg v in
- {
- pre_annots = WpStrategy.get_annots strategy eb ;
- post_annots = WpStrategy.get_annots strategy en ;
- exit_annots = WpStrategy.get_annots strategy ee ;
- }
-
- let wp_call_any wenv cenv ~p_post ~p_exit =
- let obj = W.merge wenv p_post p_exit in
- let call_asgn = WpStrategy.get_call_asgn cenv.post_annots None in
- let lab, obj = add_assigns_hyp wenv obj call_asgn in
- match lab with
- | Some _ -> obj
- | None -> assert false
-
- let add_call_post wenv annots kf obj =
- List.fold_left (add_goal wenv) obj (WpStrategy.get_call_post annots kf)
-
- let wp_call_kf wenv cenv stmt lval kf args precond ~p_post ~p_exit =
- let call_asgn = WpStrategy.get_call_asgn cenv.post_annots (Some kf) in
- let assigns = match call_asgn with
- | WpPropId.AssignsLocations (_, asgn_body) ->
- asgn_body.WpPropId.a_assigns
- | WpPropId.AssignsAny _ -> WritesAny
- | WpPropId.NoAssignsInfo -> assert false (* see above *)
- in
- let p_post = add_call_post wenv cenv.post_annots kf p_post in
- let p_exit = add_call_post wenv cenv.exit_annots kf p_exit in
- let pre_hyp, pre_goals = WpStrategy.get_call_pre cenv.pre_annots kf in
- let obj = W.call wenv stmt lval kf args
- ~pre:(pre_hyp)
- ~post:((WpStrategy.get_call_hyp cenv.post_annots kf))
- ~pexit:((WpStrategy.get_call_hyp cenv.exit_annots kf))
- ~assigns ~p_post ~p_exit in
- if precond
- then W.call_goal_precond wenv stmt kf args ~pre:(pre_goals) obj
- else obj
-
- let wp_calls ((_, cfg, strategy, _, wenv)) res v stmt
- lval call args p_post p_exit
- =
- debug "[wp_calls] %a@." Cil2cfg.pp_call_type call;
- let cenv = callenv cfg strategy v in
- match call with
- | Cil2cfg.Static kf ->
- let precond =
- WpStrategy.is_default_behavior strategy && R.is_pass1 res
- in
- wp_call_kf wenv cenv stmt lval kf args precond ~p_post ~p_exit
- | Cil2cfg.Dynamic fct ->
- let bhv = WpStrategy.behavior_name_of_strategy strategy in
- match Dyncall.get ?bhv stmt with
- | None -> wp_call_any wenv cenv ~p_post ~p_exit
- | Some (prop,calls) ->
- let precond = R.is_pass1 res in
- let do_call kf =
- let wp = wp_call_kf wenv cenv stmt lval
- kf args precond ~p_post ~p_exit in
- kf , wp in
- let pid = WpPropId.mk_property prop in
- W.call_dynamic wenv stmt pid fct (List.map do_call calls)
-
- let wp_stmt wenv s obj = match s.skind with
- | Return (r, _) -> W.return wenv s r obj
- | Instr i ->
- begin match i with
- | Local_init (vi, AssignInit i, _) -> W.init wenv vi (Some i) obj
- | Local_init (_, ConsInit _, _) -> assert false
- | (Set (lv, e, _)) -> W.assign wenv s lv e obj
- | (Asm _) ->
- let asm = WpPropId.mk_asm_assigns_desc s in
- W.use_assigns wenv None asm obj
- | (Call _) -> assert false
- | Skip _ | Code_annot _ -> obj
- end
- | Break _ | Continue _ | Goto _ -> obj
- | Loop _-> (* this is not a real loop (exit before looping)
- just ignore it ! *) obj
- | If _ -> assert false
- | Switch _-> assert false
- | Block _-> assert false
- | UnspecifiedSequence _-> assert false
- | TryExcept _ | TryFinally _ | Throw _ | TryCatch _ -> assert false
-
- let wp_scope wenv vars scope obj =
- debug "[wp_scope] %s : %a@."
- (match scope with
- | Mcfg.SC_Global -> "global"
- | Mcfg.SC_Block_in -> "block in"
- | Mcfg.SC_Block_out -> "block out"
- | Mcfg.SC_Frame_in -> "frame in"
- | Mcfg.SC_Frame_out -> "frame out" )
- (Pretty_utils.pp_list ~sep:", " Printer.pp_varinfo) vars;
- match scope with
- | Mcfg.(SC_Block_in | SC_Block_out) when vars = [] -> obj
- | _ -> W.scope wenv vars scope obj
-
- (** @return the WP stored for edge [e]. Compute it if it is not already
- * there and store it. Also handle the Acut annotations. *)
- let rec get_wp_edge ((_kf, cfg, strategy, res, wenv) as env) e =
- Db.yield ();
- let v = Cil2cfg.edge_dst e in
- debug "[get_wp_edge] get wp before %a@." Cil2cfg.pp_node v;
- try
- let res = R.find res e in
- debug "[get_wp_edge] %a already computed@." Cil2cfg.pp_node v;
- res
- with Not_found ->
- (* Notice that other hyp and goal are handled in R.set as usual *)
- let cutp =
- if R.is_pass1 res
- then WpStrategy.get_cut (WpStrategy.get_annots strategy e)
- else []
- in
- match cutp with
- | [] ->
- let wp = compute_wp_edge env e in
- R.set strategy wenv res e wp
- | cutp ->
- debug "[get_wp_edge] cut at node %a@." Cil2cfg.pp_node v;
- let add_cut_goal (g,p) acc =
- if g then add_goal wenv acc p else acc
- in
- let edge_annot = List.fold_right add_cut_goal cutp W.empty in
- (* put cut goal properties as goals in e if any, else true *)
- let edge_annot = R.set strategy wenv res e edge_annot in
- let wp = compute_wp_edge env e in
- let add_cut_hyp (_,p) acc = add_hyp wenv acc p in
- let oblig = List.fold_right add_cut_hyp cutp wp in
- (* TODO : we could add hyp to the oblig if we have some in strategy *)
- let oblig = W.loop_step oblig in
- if test_edge_loop_ok cfg None e
- then R.add_memo res e oblig
- else R.add_oblig res Clabels.pre (W.close wenv oblig);
- edge_annot
-
- and get_only_succ env cfg v = match Cil2cfg.succ_e cfg v with
- | [e'] -> get_wp_edge env e'
- | ls ->
- Wp_parameters.debug "CFG node %a has %d successors instead of 1@."
- Cil2cfg.pp_node v (List.length ls);
- Wp_error.unsupported "strange loop(s)."
-
- and compute_wp_edge ((kf, cfg, _annots, res, wenv) as env) e =
- let v = Cil2cfg.edge_dst e in
- debug "[compute_edge] before %a go...@." Cil2cfg.pp_node v;
- let old_loc = Cil.CurrentLoc.get () in
- let () = match Cil2cfg.node_stmt_opt v with
- | Some s -> Cil.CurrentLoc.set (Stmt.loc s)
- | None -> ()
- in
- let formals = Kernel_function.get_formals kf in
- let res = match Cil2cfg.node_type v with
- | Cil2cfg.Vstart ->
- Wp_parameters.debug "No CFG edge can lead to Vstart";
- Wp_error.unsupported "strange CFGs."
- | Cil2cfg.VfctIn ->
- let obj = get_only_succ env cfg v in
- let obj = wp_scope wenv [] Mcfg.SC_Global obj in
- obj
- | Cil2cfg.VblkIn (Cil2cfg.Bfct, b) ->
- let obj = get_only_succ env cfg v in
- let obj = wp_scope wenv b.blocals Mcfg.SC_Block_in obj in
- let obj = wp_scope wenv formals Mcfg.SC_Frame_in obj in
- obj
- | Cil2cfg.VblkOut (Cil2cfg.Bfct, b) ->
- let obj = get_only_succ env cfg v in
- let obj = wp_scope wenv b.blocals Mcfg.SC_Block_out obj in
- obj
- | Cil2cfg.VblkOut _ | Cil2cfg.VblkIn _ ->
- get_only_succ env cfg v
- | Cil2cfg.Vstmt s ->
- let obj = get_only_succ env cfg v in
- wp_stmt wenv s obj
- | Cil2cfg.Vcall (stmt, lval, fct, args) ->
- let en, ee = Cil2cfg.get_call_out_edges cfg v in
- let objn = get_wp_edge env en in
- let obje = get_wp_edge env ee in
- wp_calls env res v stmt lval fct args objn obje
- | Cil2cfg.Vtest (true, s, c) ->
- let et, ef = Cil2cfg.get_test_edges cfg v in
- let t_obj = get_wp_edge env et in
- let f_obj = get_wp_edge env ef in
- W.test wenv s c t_obj f_obj
- | Cil2cfg.Vtest (false, _, _) ->
- get_only_succ env cfg v
- | Cil2cfg.Vswitch (s, e) ->
- let cases, def_edge = Cil2cfg.get_switch_edges cfg v in
- let cases_obj = List.map (fun (c,e) -> c, get_wp_edge env e) cases in
- let def_obj = get_wp_edge env def_edge in
- W.switch wenv s e cases_obj def_obj
- | Cil2cfg.Vloop _ | Cil2cfg.Vloop2 _ ->
- let get_loop_head = fun n -> get_only_succ env cfg n in
- wp_loop env v e get_loop_head
- | Cil2cfg.VfctOut | Cil2cfg.VfctErr ->
- let obj = get_only_succ env cfg v (* exitpost / postcondition *) in
- wp_scope wenv formals Mcfg.SC_Frame_out obj
- | Cil2cfg.Vend ->
- W.empty
- (* LC : unused entry point...
- let obj = W.empty in
- wp_scope wenv formals Mcfg.SC_Function_after_POST obj
- *)
- in
- let Cil2cfg.{ b_closed ; b_opened } = Cil2cfg.block_scope_for_edge cfg e in
- let do_block sc res b = wp_scope wenv b.blocals sc res in
- let res = List.fold_left (do_block Mcfg.SC_Block_in) res b_opened in
- let res = List.fold_left (do_block Mcfg.SC_Block_out) res b_closed in
- debug "[compute_edge] before %a done@." Cil2cfg.pp_node v;
- Cil.CurrentLoc.set old_loc;
- res
-
- module Init = CfgInit.Make(W)
-
- let get_weakest_precondition cfg ((kf, _g, strategy, res, wenv) as env) =
- debug "[wp-cfg] start Pass1";
- Cil2cfg.iter_edges (fun e -> ignore (get_wp_edge env e)) cfg ;
- debug "[wp-cfg] end of Pass1";
- R.change_mode_if_needed res;
- (* Notice that [get_wp_edge] will start Pass2 if needed,
- * 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 = Init.process_global_init wenv kf obj in
- let obj = match WpStrategy.strategy_kind strategy with
- | WpStrategy.SKannots -> obj
- | WpStrategy.SKfroms info ->
- let pre = info.WpStrategy.get_pre () in
- let pre = WpStrategy.get_hyp_only pre in
- W.build_prop_of_from wenv pre obj
- in
- debug "before close: %a@." W.pretty obj;
- W.close wenv obj
-
- let compute cfg strategy =
- debug "[wp-cfg] start computing with the strategy for %a"
- WpStrategy.pp_info_of_strategy strategy;
- if WpStrategy.strategy_has_prop_goal strategy
- || WpStrategy.strategy_has_asgn_goal strategy then
- try
- let kf = Cil2cfg.cfg_kf cfg in
- if Cil2cfg.strange_loops cfg <> [] then
- Wp_error.unsupported "non natural loop(s)" ;
- let lvars = match WpStrategy.strategy_kind strategy with
- | WpStrategy.SKfroms info -> info.WpStrategy.more_vars
- | _ -> [] in
- let wenv = W.new_env ~lvars kf in
- let res = R.empty cfg in
- let env = (kf, cfg, strategy, res, wenv) in
- List.iter
- (fun (pid,thm) -> W.add_axiom pid thm)
- (WpStrategy.global_axioms strategy) ;
- let goal = get_weakest_precondition cfg env in
- debug "[get_weakest_precondition] %a@." W.pretty goal;
- let pp_cfg_edges_annot res fmt e =
- try W.pretty fmt (R.find res e)
- with Not_found -> Format.fprintf fmt "<released>"
- in
- let annot_cfg = pp_cfg_edges_annot res in
- debug "[wp-cfg] computing done.";
- [goal] , annot_cfg
- with Wp_error.Error (_, msg) ->
- Wp_parameters.warning "@[calculus failed on strategy@ @[for %a@]@ \
- because@ %s (abort)@]"
- WpStrategy.pp_info_of_strategy strategy
- msg;
- let annot_cfg fmt _e = Format.fprintf fmt "" in
- [], annot_cfg
- else
- begin
- debug "[wp-cfg] no goal in this strategy : ignore.";
- let annot_cfg fmt _e = Format.fprintf fmt "" in
- [], annot_cfg
- end
-
-end
diff --git a/src/plugins/wp/calculus.mli b/src/plugins/wp/calculus.mli
deleted file mode 100644
index ad5bc86fb0c85bc7d9f2f2724139e99e3c6f94f0..0000000000000000000000000000000000000000
--- a/src/plugins/wp/calculus.mli
+++ /dev/null
@@ -1,33 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-(** Generic WP calculus *)
-
-module Cfg(W : Mcfg.S) :
-sig
-
- val compute :
- Cil2cfg.t ->
- WpStrategy.strategy ->
- W.t_prop list * (Format.formatter -> Cil2cfg.edge -> unit)
-
-end
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 930f3e439067597fe0408e5a2fd5c98396a940b2..e4663d5fb6710badde9749df7510bc44599f1bae 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -457,6 +457,17 @@ let get_code_assertions ?(smoking=false) kf stmt =
(* --- Loop Invariants --- *)
(* -------------------------------------------------------------------------- *)
+let mk_variant_properties kf s ca v =
+ let vpos_id = WpPropId.mk_var_pos_id kf s ca in
+ let vdecr_id = WpPropId.mk_var_decr_id kf s ca in
+ let loc = v.term_loc in
+ let lcurr = Clabels.to_logic (Clabels.loop_current s) in
+ let vcurr = Logic_const.tat ~loc (v, lcurr) in
+ let zero = Cil.lzero ~loc () in
+ let vpos = Logic_const.prel ~loc (Rle, zero, vcurr) in
+ let vdecr = Logic_const.prel ~loc (Rlt, v, vcurr) in
+ (vpos_id, vpos), (vdecr_id, vdecr)
+
type loop_contract = {
loop_terminates: predicate option;
(* to be verified at loop entry *)
@@ -515,7 +526,7 @@ module LoopContract = WpContext.StaticGenerator(CodeKey)
}
| AVariant(term, None) ->
let vpos , vdec =
- WpStrategy.mk_variant_properties kf stmt ca term in
+ mk_variant_properties kf stmt ca term in
let intro_terminates (pid, v) =
pid,
let t = snd @@ get_terminates_hyp kf in
diff --git a/src/plugins/wp/cfgAnnot.mli b/src/plugins/wp/cfgAnnot.mli
index 294b030675af76c28dd493b4728c972334280dd6..4d246683c330953432587370ff67cf0f8025ddd1 100644
--- a/src/plugins/wp/cfgAnnot.mli
+++ b/src/plugins/wp/cfgAnnot.mli
@@ -95,6 +95,10 @@ type loop_contract = {
val get_loop_contract : ?smoking:bool -> ?terminates:predicate ->
kernel_function -> stmt -> loop_contract
+val mk_variant_properties :
+ kernel_function -> stmt -> code_annotation -> term -> pred_info * pred_info
+
+
(* -------------------------------------------------------------------------- *)
(* --- Property Accessors : Call Contracts --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index e867511bf0c67442688eab50df6a8127497d13e3..1d86603585d87124ecca7353fe0ff08ca1f6736f 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -396,7 +396,7 @@ struct
let do_preconditions env ~formals (b : CfgAnnot.behavior) w =
let kf = env.mode.kf in
- let init = WpStrategy.is_main_init kf in
+ let init = Globals.is_entry_point ~when_lib_entry:false kf in
let side_behaviors =
if init || WpLog.PrecondWeakening.get () then []
else CfgAnnot.get_preconditions ~goal:false kf in
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index 839c3cf03d55e305fa4125b35e9a0559b1f47124..1ff5c4f7a9b5e692fb3b65ff1cc72244eb49ceea 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -303,7 +303,7 @@ let collect_loops_no_variant kf stmt =
| _ -> Extlib.id
in
let props_of_v ca v =
- let (d, _), (p, _) = WpStrategy.mk_variant_properties kf stmt ca v in
+ let (d, _), (p, _) = CfgAnnot.mk_variant_properties kf stmt ca v in
Pset.union
(Pset.singleton @@ WpPropId.property_of_id d)
(Pset.singleton @@ WpPropId.property_of_id p)
@@ -317,6 +317,26 @@ let collect_loops_no_variant kf stmt =
| _ ->
Sset.empty, Pset.empty
+(* -------------------------------------------------------------------------- *)
+(* --- Trivially terminates --- *)
+(* -------------------------------------------------------------------------- *)
+
+let trivial_terminates = ref 0
+
+let wp_trivially_terminates =
+ Emitter.create
+ "Trivial Termination"
+ [Emitter.Property_status]
+ ~correctness:[] (* TBC *)
+ ~tuning:[] (* TBC *)
+
+let set_trivially_terminates p hyps =
+ incr trivial_terminates ;
+ Wp_parameters.result "[CFG] Goal %a : Valid (Trivial)" WpPropId.pp_propid p ;
+ let pid = WpPropId.property_of_id p in
+ let hyps = Property.Set.elements hyps in
+ Property_status.emit wp_trivially_terminates ~hyps pid Property_status.True
+
(* -------------------------------------------------------------------------- *)
(* --- Memoization Key --- *)
(* -------------------------------------------------------------------------- *)
@@ -404,7 +424,7 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
} in
let behaviors = Annotations.behaviors kf in
(* Inits *)
- if WpStrategy.is_main_init kf then
+ if Globals.is_entry_point ~when_lib_entry:false kf then
infos.annots <- List.exists (selected_main_bhv ~bhv ~prop) behaviors ;
(* Function Body *)
Option.iter
@@ -466,7 +486,7 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
end body ;
(* Doomed *)
Bag.iter
- (fun p -> if WpPropId.filter_status p then WpAnnot.set_unreachable p)
+ (fun p -> if WpPropId.filter_status p then WpReached.set_unreachable p)
infos.doomed ;
(* Termination *)
let infos =
@@ -498,7 +518,7 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
end
else if infos.calls = Fset.empty
&& infos.no_variant_loops = Sset.empty then begin
- WpAnnot.set_trivially_terminates id infos.terminates_deps ;
+ set_trivially_terminates id infos.terminates_deps ;
(* Drop dependencies for this terminates, we've used it. *)
{ infos with terminates_deps = Pset.empty }
end
diff --git a/src/plugins/wp/cfgInfos.mli b/src/plugins/wp/cfgInfos.mli
index 45172d3653075c7ba3dd971dd286ab2022ac7bec..ba6256d0099a60679a4f083661cdab56fc8b4761 100644
--- a/src/plugins/wp/cfgInfos.mli
+++ b/src/plugins/wp/cfgInfos.mli
@@ -43,4 +43,6 @@ val terminates_deps : t -> Property.Set.t
val is_recursive : Kernel_function.t -> bool
val get_cluster : Kernel_function.t -> Kernel_function.Set.t option
+val trivial_terminates : int ref
+
(**************************************************************************)
diff --git a/src/plugins/wp/cfgInit.ml b/src/plugins/wp/cfgInit.ml
index 32168850ea40fec1f7095a53a1e4594d5b9d1881..eba644dc7dd4d1fa48b39b5c04e5254444fc64ae 100644
--- a/src/plugins/wp/cfgInit.ml
+++ b/src/plugins/wp/cfgInit.ml
@@ -31,7 +31,7 @@ struct
if var.vstorage = Extern then obj else
let do_init = match filter with
| `All -> true
- | `InitConst -> WpStrategy.isGlobalInitConst var
+ | `InitConst -> Cil.isGlobalInitConst var
in if not do_init then obj
else
let old_loc = Cil.CurrentLoc.get () in
@@ -43,14 +43,14 @@ struct
let process_global_const wenv obj =
Globals.Vars.fold_in_file_order
(fun var _initinfo obj ->
- if WpStrategy.isGlobalInitConst var
+ if Cil.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
+ if Globals.is_entry_point ~when_lib_entry:false kf then
begin
let obj = W.label wenv None Clabels.init obj in
compute_global_init wenv `All obj
@@ -58,14 +58,14 @@ struct
else if W.has_init wenv then
begin
let obj =
- if WpStrategy.isInitConst ()
+ if Wp_parameters.Init.get ()
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 ()
+ if Wp_parameters.Init.get ()
then compute_global_init wenv `InitConst obj
else obj
diff --git a/src/plugins/wp/cil2cfg.ml b/src/plugins/wp/cil2cfg.ml
deleted file mode 100644
index 97e047cd573495d6d055cb161efa44aa7722bc58..0000000000000000000000000000000000000000
--- a/src/plugins/wp/cil2cfg.ml
+++ /dev/null
@@ -1,1453 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-(** Build a CFG of a function keeping some information of the initial structure.
- **)
-
-open Cil_types
-
-let dkey = Wp_parameters.register_category "cil2cfg" (* debugging key *)
-
-let debug fmt = Wp_parameters.debug ~dkey fmt
-let debug2 fmt = Wp_parameters.debug ~dkey ~level:2 fmt
-
-(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-(** {2 Nodes} *)
-
-(** Be careful that only Bstmt are real Block statements *)
-type block_type =
- Bstmt of stmt | Bthen of stmt | Belse of stmt | Bloop of stmt | Bfct
- (* added to identify 2 blocks for tests, else there are mixed up because same
- * sid *)
-
-type call_type =
- | Dynamic of exp
- | Static of kernel_function
-
-let pp_call_type fmt = function
- | Dynamic _ -> Format.pp_print_string fmt "dynamic"
- | Static kf -> Kernel_function.pretty fmt kf
-
-type node_type =
- | Vstart | Vend
- | VfctIn | VfctOut | VfctErr
- | VblkIn of block_type * block
- | VblkOut of block_type * block
- | Vstmt of stmt
- | Vcall of stmt * lval option * call_type * exp list
- | Vtest of bool * stmt * exp (** bool=true for In and false for Out *)
- | Vswitch of stmt * exp
- | Vloop of bool option * stmt
- (** boolean is is_natural. None means the node has not been detected
- * as a loop *)
- | Vloop2 of bool * int
-
-type node_info = { kind : node_type ; mutable reachable : bool }
-
-type node = node_info
-
-let node_type n = n.kind
-
-let bkind_stmt bk = match bk with
- | Bfct -> None
- | Bstmt s | Bthen s | Belse s | Bloop s -> Some s
-
-let _bkind_sid bk = match bk with
- | Bfct -> 0
- | Bstmt s | Bthen s | Belse s | Bloop s -> s.sid
-
-type node_id = int * int
-
-(** gives a identifier to each CFG node in order to hash them *)
-let node_type_id t : node_id = match t with
- | Vstart -> (0, 0)
- | VfctIn -> (0, 1)
- | VfctOut -> (0, 2)
- | VfctErr -> (0, 3)
- | Vend -> (0, 4)
- | Vstmt s | Vtest (true, s, _) | Vswitch (s,_) | Vcall (s, _, _, _) ->
- (1, s.sid)
- | Vloop (_, s) -> (2, s.sid)
- | Vloop2 (_, n) -> (3, n)
- | VblkIn (Bfct, _) -> (4, 0)
- | VblkIn (Bstmt s,_) -> (5, s.sid)
- | VblkIn (Bthen s,_) -> (6, s.sid)
- | VblkIn (Belse s,_) -> (7, s.sid)
- | VblkIn (Bloop s,_) -> (8, s.sid)
- | VblkOut (Bfct, _) -> (9, 0)
- | VblkOut (Bstmt s,_) -> (10, s.sid)
- | VblkOut (Bthen s,_) -> (11, s.sid)
- | VblkOut (Belse s,_) -> (12, s.sid)
- | VblkOut (Bloop s,_) -> (13, s.sid)
- | Vtest (false, s, _) -> (14, s.sid)
-
-let node_id n = node_type_id (node_type n)
-
-let pp_bkind fmt bk = match bk with
- | Bfct -> Format.fprintf fmt "fct"
- | Bstmt s -> Format.fprintf fmt "stmt:%d" s.sid
- | Bthen s -> Format.fprintf fmt "then:%d" s.sid
- | Belse s -> Format.fprintf fmt "else:%d" s.sid
- | Bloop s -> Format.fprintf fmt "loop:%d" s.sid
-
-let pp_node_type fmt n = match n with
- | Vstart -> Format.fprintf fmt "<start>"
- | VfctIn -> Format.fprintf fmt "<fctIn>"
- | VfctOut -> Format.fprintf fmt "<fctOut>"
- | VfctErr -> Format.fprintf fmt "<fctErr>"
- | Vend -> Format.fprintf fmt "<end>"
- | VblkIn (bk,_) -> Format.fprintf fmt "<blkIn-%a>" pp_bkind bk
- | VblkOut (bk,_) -> Format.fprintf fmt "<blkOut-%a>" pp_bkind bk
- | Vcall (s, _, _, _) -> Format.fprintf fmt "<callIn-%d>" s.sid
- | Vstmt s -> Format.fprintf fmt "<stmt-%d>" s.sid
- | Vtest (b, s, _) ->
- Format.fprintf fmt "<test%s-%d>" (if b then "In" else "Out") s.sid
- | Vswitch (s,_) -> Format.fprintf fmt "<switch-%d>" s.sid
- | Vloop (_, s) -> Format.fprintf fmt "<loop-%d>" s.sid
- | Vloop2 (_, n) -> Format.fprintf fmt "<loop-n%d>" n
-
-let same_node v v' =
- (node_id v) = (node_id v')
-
-(** the CFG nodes *)
-module VL =
-struct
- type t = node
-
- let hash v = let (a,b) = (node_id v) in b*17 + a
-
- let equal v v' = same_node v v'
-
- let compare v v' = Extlib.compare_basic (node_id v) (node_id v')
-
- let pretty fmt v = pp_node_type fmt (node_type v)
-end
-
-let pp_node fmt v = VL.pretty fmt v
-
-let start_stmt_of_node v = match node_type v with
- | Vstart | Vtest (false, _, _) | VblkOut _
- | VfctIn | VfctOut | VfctErr | Vend | Vloop2 _ -> None
- | VblkIn (bk, _) -> bkind_stmt bk
- | Vstmt s | Vtest (true, s, _) | Vloop (_, s) | Vswitch (s,_)
- | Vcall (s, _, _, _)
- -> Some s
-
-let node_stmt_opt v = match node_type v with
- | Vstart | Vtest (false, _, _)
- | VfctIn | VfctOut | VfctErr | Vend | Vloop2 _ -> None
- | VblkIn (bk, _) | VblkOut (bk, _) -> bkind_stmt bk
- | Vstmt s | Vtest (true, s, _) | Vloop (_, s) | Vswitch (s,_)
- | Vcall (s, _, _, _)
- -> Some s
-
-let node_stmt_exn v =
- match node_stmt_opt v with None -> raise Not_found | Some s -> s
-
-(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-(** {2 Edge labels} *)
-
-type edge_type =
- | Enone (** normal edge *)
- | Ethen (** then branch : edge source is a Vtest *)
- | Eelse (** else branch : edge source is a Vtest *)
- | Eback (** back edge to a loop : the edge destination is a Vloop *)
- | EbackThen (** Eback + Ethen *)
- | EbackElse (** Eback + Eelse *)
- | Ecase of (exp list) (** switch branch : edge source is a Vswitch.
- Ecase [] for default case *)
- | Enext (** not really a edge : gives the next node of a complex stmt *)
-
-(** the CFG edges *)
-module EL = struct
-
- let compare_edge_type e1 e2 =
- if e1 == e2 then 0
- else match e1, e2 with
- | Enone, Enone | Ethen, Ethen | Eelse, Eelse | Eback, Eback
- | EbackThen, EbackThen | EbackElse, EbackElse | Enext, Enext -> 0
-
- | Ecase l1, Ecase l2 -> Extlib.list_compare Cil_datatype.Exp.compare l1 l2
-
- | Enone, (Ethen | Eelse | Eback | EbackThen | EbackElse | Ecase _ | Enext)
- | Ethen, (Eelse | Eback | EbackThen | EbackElse | Ecase _ | Enext)
- | Eelse, (Eback | EbackThen | EbackElse | Ecase _ | Enext)
- | Eback, (EbackThen | EbackElse | Ecase _ | Enext)
- | EbackThen, (EbackElse | Ecase _ | Enext)
- | EbackElse, (Ecase _ | Enext)
- | Ecase _, Enext
- -> -1
-
- | Enext, (Ecase _ | EbackElse | EbackThen | Eback | Eelse | Ethen | Enone)
- | Ecase _, (EbackElse | EbackThen | Eback | Eelse | Ethen | Enone)
- | EbackElse, (EbackThen | Eback | Eelse | Ethen | Enone)
- | EbackThen, (Eback | Eelse | Ethen | Enone)
- | Eback, (Eelse | Ethen | Enone)
- | Eelse, (Ethen | Enone)
- | Ethen, Enone -> 1
-
- type t = edge_type ref
-
- let compare (e1 : t) (e2 : t) = compare_edge_type !e1 !e2
- let default = ref Enone
- let pretty fmt e =
- let txt = match e with
- | Enone -> "----" | Ethen -> "then" | Eelse -> "else"
- | Eback -> "back" | EbackThen -> "then-back" | EbackElse -> "else-back"
- | Ecase [] -> "default"
- | Ecase l -> Format.asprintf "case(%a)"
- (Pretty_utils.pp_list ~sep:", " Printer.pp_exp) l
- | Enext -> "(next)"
- in Format.fprintf fmt "%s" txt
-end
-
-(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-(** {2 Graph} *)
-
-module PMAP(X: Graph.Sig.COMPARABLE) = struct
-
- module M = Map.Make(X)
- type 'a t = 'a M.t ref
- type key = X.t
- type 'a return = unit
-
- let empty = ()
- (* never called and not visible for the user thanks to signature
- constraints *)
-
- let create ?size () = ignore size ; ref M.empty
-
- let create_from h = ignore h ; ref M.empty
-
- let is_empty h = M.is_empty !h
-
- let clear h = h := M.empty
-
- let add k v h = h := M.add k v !h ; h
- let remove k h = h := M.remove k !h ; h
- let find k h = M.find k !h
- let mem k h = M.mem k !h
-
- let find_and_raise k t s = try find k t with Not_found -> invalid_arg s
-
- let fold f h init = M.fold f !h init
-
- let map f h =
- ref (M.fold (fun k v m -> let (k,v) = f k v in M.add k v m) !h M.empty)
-
- let iter f h = M.iter f !h
-
- let copy h = ref !h
-
-end
-
-(** the CFG is an ocamlgraph, but be careful to use it through the cfg function
- * because some edges don't have the same meaning as some others... *)
-module MyGraph = Graph.Blocks.Make(PMAP)
-module CFG:
- Graph.Sig.I
- with type V.t = VL.t
- and type V.label = VL.t
- and type E.t = VL.t * EL.t * VL.t
- and type E.label = EL.t
-=
-struct
- include MyGraph.Digraph.ConcreteBidirectionalLabeled(VL)(EL)
- let add_vertex g v = ignore (add_vertex g v)
- let add_edge g v1 v2 = ignore (add_edge g v1 v2)
- let remove_edge g v1 v2 = ignore (remove_edge g v1 v2)
- let remove_edge_e g e = ignore (remove_edge_e g e)
- let add_edge_e g e = ignore (add_edge_e g e)
- let remove_vertex g v =
- if HM.mem v g then begin
- ignore (HM.remove v g);
- let remove v = S.filter (fun (v2,_) -> not (V.equal v v2)) in
- HM.iter (fun k (s1, s2) ->
- ignore (HM.add k (remove v s1, remove v s2) g)) g
- end
-end
-
-(** Set of edges. *)
-module Eset = Set.Make (CFG.E)
-
-(** Set of nodes. *)
-module Nset = Set.Make (CFG.V)
-
-(** Hashtbl of node *)
-module Ntbl = Hashtbl.Make (CFG.V)
-
-(** The final CFG is composed of the graph, but also :
- * the function that it represents,
- * an hashtable to find a CFG node knowing its hashcode *)
-type t = {
- kernel_function : kernel_function;
- graph : CFG.t;
- spec_only : bool;
- stmt_node : ((int*int), CFG.V.t) Hashtbl.t;
- unreachables : node_type list;
- loop_nodes : (node list) option;
- mutable loop_cpt : int;
- mutable node_break : node option;
- mutable node_continue : node option;
-}
-
-let new_cfg_env spec_only kf = {
- kernel_function = kf;
- spec_only = spec_only ;
- graph = CFG.create ();
- stmt_node = Hashtbl.create 97;
- unreachables = [];
- loop_nodes = None;
- loop_cpt = 0;
- node_break = None;
- node_continue = None;
-}
-
-let cfg_kf cfg = cfg.kernel_function
-let cfg_graph cfg = cfg.graph
-let cfg_spec_only cfg = cfg.spec_only
-
-let unreachable_nodes cfg = cfg.unreachables
-
-(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-(** {2 CFG edges} *)
-
-type edge = CFG.E.t
-
-let edge_type e = !(CFG.E.label e)
-let edge_src e = CFG.E.src e
-let edge_dst e = CFG.E.dst e
-
-let pp_edge fmt e =
- Format.fprintf fmt "%a -%a-> %a"
- pp_node (CFG.E.src e) EL.pretty (edge_type e) pp_node (CFG.E.dst e)
-
-let is_back_edge e = match (edge_type e) with
- | Eback | EbackThen | EbackElse -> true
- | Enone | Ethen | Eelse | Ecase _ | Enext -> false
-
-let is_next_edge e = match (edge_type e) with
- | Enext -> true
- | Eback | EbackThen | EbackElse | Enone | Ethen | Eelse | Ecase _ -> false
-
-let pred_e cfg n =
- try
- let edges = CFG.pred_e cfg.graph n in
- List.filter (fun e -> not (is_next_edge e)) edges
- with Invalid_argument _ ->
- (Wp_parameters.warning "[cfg.pred_e] pb with node %a" pp_node n; [])
-
-let succ_e cfg n =
- try
- let edges = CFG.succ_e cfg.graph n in
- List.filter (fun e -> not (is_next_edge e)) edges
- with Invalid_argument _ ->
- (Wp_parameters.warning "[cfg.succ_e] pb with node %a" pp_node n; [])
-
-type edge_key = int * int * int * int
-
-let edge_key e : edge_key =
- let a,b = node_id (edge_src e) in
- let c,d = node_id (edge_dst e) in
- a,b,c,d
-
-let same_edge e1 e2 = (edge_key e1 = edge_key e2)
-
-(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-(** {2 Iterators} ignoring the [Enext] edges *)
-
-let iter_nodes f cfg = CFG.iter_vertex f (cfg.graph)
-let fold_nodes f cfg acc = CFG.fold_vertex f (cfg.graph) acc
-
-let iter_edges f cfg =
- let f e = if is_next_edge e then () else f e in
- CFG.iter_edges_e f (cfg.graph)
-
-let iter_succ f cfg n =
- let f e = if is_next_edge e then () else f (CFG.E.dst e)
- in try CFG.iter_succ_e f (cfg.graph) n
- with Invalid_argument _ ->
- (Wp_parameters.warning "[cfg.iter_succ] pb with node %a" pp_node n)
-
-let fold_succ f cfg n acc =
- let f e acc = if is_next_edge e then acc else f (CFG.E.dst e) acc
- in try CFG.fold_succ_e f (cfg.graph) n acc
- with Invalid_argument _ ->
- (Wp_parameters.warning "[cfg.fold_succ] pb with node %a" pp_node n; acc)
-
-let fold_pred f cfg n acc =
- let f e acc = if is_next_edge e then acc else f (CFG.E.src e) acc in
- try CFG.fold_pred_e f (cfg.graph) n acc
- with Invalid_argument s ->
- (Wp_parameters.warning "[cfg.fold_pred] pb with node %a: %s" pp_node n s; acc)
-
-let _iter_succ_e f cfg n =
- let f e = if is_next_edge e then () else f e
- in try CFG.iter_succ_e f (cfg.graph) n
- with Invalid_argument _ ->
- (Wp_parameters.warning "[cfg.iter_succ_e] pb with node %a" pp_node n)
-
-let iter_pred_e f cfg n =
- let f e = if is_next_edge e then () else f e
- in try CFG.iter_pred_e f (cfg.graph) n
- with Invalid_argument _ ->
- (Wp_parameters.warning "[cfg.iter_pred_e] pb with node %a" pp_node n)
-
-let fold_pred_e f cfg n acc =
- let f e acc = if is_next_edge e then acc else f e acc
- in try CFG.fold_pred_e f (cfg.graph) n acc
- with Invalid_argument _ ->
- (Wp_parameters.warning "[cfg.fold_pred_e] pb with node %a" pp_node n; acc)
-
-let fold_succ_e f cfg n acc =
- let f e acc = if is_next_edge e then acc else f e acc
- in try CFG.fold_succ_e f (cfg.graph) n acc
- with Invalid_argument _ ->
- (Wp_parameters.warning "[cfg.fold_succ_e] pb with node %a" pp_node n; acc)
-
-
-(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-(** {2 Getting information} *)
-
-let cfg_start cfg = Hashtbl.find cfg.stmt_node (node_type_id Vstart)
-
-let start_edge cfg = match succ_e cfg (cfg_start cfg) with [e] -> e
- | _ -> Wp_parameters.fatal "[cfg] should have exactly ONE starting edge !"
-
-exception Found of node
-let _find_stmt_node cfg stmt =
- let find n = match node_stmt_opt n with None -> ()
- | Some s -> if s.sid = stmt.sid then raise (Found n)
- in
- try (iter_nodes find cfg; raise Not_found)
- with Found n -> n
-
-(** Get the edges going out a test node with the then branch first *)
-let get_test_edges cfg v =
- match succ_e cfg v with
- | [e1; e2] ->
- begin match (edge_type e1), (edge_type e2) with
- | (Ethen|EbackThen), (Eelse|EbackElse) -> e1, e2
- | (Eelse|EbackElse), (Ethen|EbackThen) -> e2, e1
- | _, (Eelse|EbackElse) ->
- Wp_parameters.fatal "[cfg] test node with invalid edges %a"
- pp_edge e1
- | _, _ ->
- Wp_parameters.fatal "[cfg] test node with invalid edges %a"
- pp_edge e2
- end
- | _ -> raise (Invalid_argument "[cfg:get_test_edges] not a test")
-
-let get_switch_edges cfg v =
- match node_type v with
- | Vswitch _ ->
- begin
- let get_case (cl, dl) e = match (edge_type e) with
- | Ecase [] -> cl, e::dl
- | Ecase c -> (c, e)::cl, dl
- | _ -> Wp_parameters.fatal ("[cfg] switch node with invalid edges")
- in match List.fold_left get_case ([],[]) (succ_e cfg v) with
- | cl, [d] -> cl, d
- | _ ->
- Wp_parameters.fatal ("[cfg] switch node with several 'default' ?")
- end
- | _ -> raise (Invalid_argument "[cfg:get_switch_edges] not a switch")
-
-let get_call_out_edges cfg v =
- let e1, e2 = match succ_e cfg v with
- | [e1;e2] -> e1, e2
- | _ -> assert false
- in
- let en, ee = match node_type (edge_dst e1) ,
- node_type (edge_dst e2) with
- | _, VfctErr -> e1, e2
- | VfctErr, _ -> e2, e1
- | _, _ -> assert false
- in en, ee
-
-let get_edge_stmt e =
- match node_type (edge_dst e) with
- | Vstart | VfctIn | VfctOut | VfctErr -> None
- | VblkIn (Bstmt s, _) | Vstmt s
- | Vcall (s,_,_,_) | Vtest (true, s, _) | Vswitch (s,_) -> Some s
- | Vloop (_,s) -> if is_back_edge e then None else Some s
- | Vtest _ | VblkIn _ | VblkOut _ | Vend | Vloop2 _ -> None
-
-let get_edge_labels e =
- let v_after = edge_dst e in
- let l = match node_type v_after with
- | Vstart -> assert false
- | VfctIn -> []
- | VfctErr | VfctOut -> [Clabels.post]
- | VblkIn (Bstmt s, _)
- | Vcall (s,_,_,_) | Vstmt s | Vtest (true, s, _) | Vswitch (s,_) ->
- [Clabels.stmt s]
- | Vloop (_,s) ->
- if is_back_edge e then []
- else [Clabels.stmt s]
- | Vtest (false, _, _) | VblkIn _ | VblkOut _ | Vend -> []
- | Vloop2 _ -> []
- in
- let v_before = edge_src e in
- match node_type v_before with
- | VfctIn -> Clabels.pre::l
- | Vloop (_, s) -> (Clabels.loop_current s)::l
- | _ -> l
-
-let next_edge cfg n =
- let edges = match node_type n with
- | VblkIn _ | Vswitch _ | Vtest _ | Vloop _ ->
- let edges = CFG.succ_e cfg.graph n in
- List.filter is_next_edge edges
- | Vcall _ ->
- let en, _ee = get_call_out_edges cfg n in [en]
- | Vstmt _ ->
- let edges = match CFG.succ_e cfg.graph n with
- | (([] | _::[]) as edges) -> edges
- | edges -> (* this case may happen in case of a loop
- which is not really a loop : it is then a Vstmt,
- and the Enext is not the succ_e. *)
- List.filter is_next_edge edges
- in edges
- | _ ->
- debug "[next_edge] not found for %a@." pp_node n;
- raise Not_found (* No Enext information on this node *)
- in
- match edges with
- | [] -> (* can append when nodes have been removed *) raise Not_found
- | [e] -> e
- | _ -> Wp_parameters.fatal "several (%d) Enext edges to node %a"
- (List.length edges) pp_node n
-
-(** Find the node that follows the input node statement.
- * The statement postcondition can then be stored to the edges before that node.
- * @raise Not_found when the node after has been removed (unreachable) *)
-let node_after cfg n = edge_dst (next_edge cfg n)
-
-let get_pre_edges cfg n = pred_e cfg n
-
-let get_post_edges cfg v =
- try let v' = node_after cfg v in pred_e cfg v'
- with Not_found -> []
-
-let get_exit_edges cfg src =
- debug "[get_exit_edges] of %a@." pp_node src;
- let do_node n acc =
- debug "[get_exit_edges] look at %a@." pp_node n;
- let add_exit e acc =
- let dst = edge_dst e in
- match node_type dst with
- | VfctErr ->
- debug
- "[get_exit_edges] add %a@." pp_edge e;
- (* (succ_e cfg dst) @ acc *)
- e :: acc
- | _ -> acc
- in match node_type n with
- | Vstart -> (* In it is a problem a domination which is not solved here *)
- Wp_parameters.warning "[cfg] Forget exits clause of node %a" pp_node src;
- raise Exit
- | _ -> fold_succ_e add_exit cfg n acc
- in
- let rec do_node_and_preds n (seen, edges as acc) =
- if Nset.mem n seen then acc (* Don't loop over the same node. *)
- else begin
- let edges = do_node n edges in
- if CFG.V.compare src n = 0 then (seen, edges)
- else do_preds n (Nset.add n seen, edges)
- end
- and do_preds n acc =
- fold_pred do_node_and_preds cfg n acc
- in
- let edges =
- try
- let edge = next_edge cfg src in
- if is_next_edge edge then
- (* needs to look at all node between the next node and the source *)
- snd (do_preds (edge_dst edge) (Nset.empty, []))
- else do_node src []
- with Exit | Not_found -> []
- in
- if edges = [] then
- debug "[get_exit_edges] -> empty";
- edges
-
-let add_edges_before cfg src set e_after =
- let rec add_preds set e =
- let e_src = edge_src e in
- if CFG.V.compare src e_src = 0 then set
- else
- let add_edge_and_preds e set =
- if Eset.mem e set then set
- else add_preds (Eset.add e set) e
- in fold_pred_e add_edge_and_preds cfg e_src set
- in add_preds set e_after
-
-let get_internal_edges cfg n =
- let edges = try pred_e cfg (node_after cfg n) with Not_found -> [] in
- let set = Eset.empty in
- let set = List.fold_left (add_edges_before cfg n) set edges in
- edges, set
-
-let rec get_edge_next_stmt cfg e =
- let v_after = edge_dst e in
- let get_next v = match succ_e cfg v with
- | [e] -> get_edge_next_stmt cfg e
- | [] | _ :: _ -> None (* nodes without statement should have one succ,
- except the last one *)
- in
- match node_type v_after with
- | VblkOut _ | VblkIn ((Bthen _|Belse _|Bloop _|Bfct),_) -> get_next v_after
- | _ ->
- match node_stmt_opt v_after with
- | Some s -> Some s
- | None -> get_next v_after
-
-let get_post_label cfg v =
- match get_post_edges cfg v with
- | [] -> None
- | e::_ -> (* TODO: is this ok to consider only one edge ? *)
- match get_edge_next_stmt cfg e with
- | None -> None
- | Some s -> Some (Clabels.stmt s)
-
-type block_scope = { b_opened : block list ; b_closed : block list }
-
-let no_scope = { b_opened = [] ; b_closed = [] }
-
-let block_scope s s' =
- try
- {
- b_opened = Kernel_function.blocks_opened_by_edge s s' ;
- b_closed = Kernel_function.blocks_closed_by_edge s s' ;
- }
- with Not_found | Invalid_argument _ ->
- debug "[blocks_closed_by_edge] not found sid:%d -> sid:%d@." s.sid s'.sid;
- no_scope
-
-let block_scope_for_edge cfg e =
- debug "[blocks_closed_by_edge] for %a...@." pp_edge e;
- let v_before = edge_src e in
- match node_type v_before with
- | Vstmt s | Vtest (true, s, _) | Vloop (_, s) | Vswitch (s,_) ->
- begin match s.succs with
- | [s'] -> block_scope s s'
- | [] | _ :: _ ->
- let s' = get_edge_next_stmt cfg e in
- match s' with
- | None -> no_scope
- | Some s' -> block_scope s s'
- end
- | VblkIn(Bstmt _,b) -> { b_opened=[b] ; b_closed=[] }
- | Vcall _
- | VblkIn _ | VblkOut _ | Vtest(false,_,_)
- | VfctIn | VfctOut | VfctErr | Vstart | Vend | Vloop2 _ ->
- no_scope
-
-let has_exit cfg =
- try
- let node = Hashtbl.find cfg.stmt_node (node_type_id VfctErr) in
- match pred_e cfg node with
- | [] -> false
- | _ -> true
- with Not_found | Invalid_argument _ -> false
-
-(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-(** {2 Generic table to store things on edges} *)
-
-module type HEsig = sig
- type ti
- type t
- val create : int -> t
- val find : t -> edge -> ti
- val find_all : t -> edge -> ti list
- val add : t -> edge -> ti -> unit
- val replace : t -> edge -> ti -> unit
- val remove : t -> edge -> unit
- val clear : t -> unit
-end
-
-module HE (I : sig type t end) = struct
- type ti = I.t
- type t = (edge_key, ti) Hashtbl.t
- let create n = Hashtbl.create n
- let find info e = Hashtbl.find info (edge_key e)
- let find_all info e = Hashtbl.find_all info (edge_key e)
- let add info e i = Hashtbl.add info (edge_key e) i
- let replace info e i = Hashtbl.replace info (edge_key e) i
- let remove info e = Hashtbl.remove info (edge_key e)
- let clear info = Hashtbl.clear info
-end
-
-(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-(** {2 Building the CFG} *)
-
-let add_node env t =
- let id = node_type_id t in
- let n = {kind = t ; reachable = false } in
- debug "add node : %a@." VL.pretty n;
- let n = CFG.V.create n in
- Hashtbl.add env.stmt_node id n;
- n
-
-let change_node_kind env n t =
- let id = node_id n in
- let id' = node_type_id t in
- let n' = { n with kind = t } in
- debug "change node kind from %a to %a" VL.pretty n VL.pretty n';
- let n' = CFG.V.create n' in
- Hashtbl.remove env.stmt_node id;
- Hashtbl.add env.stmt_node id' n';
- let preds = CFG.fold_pred_e (fun e acc -> e::acc) env.graph n [] in
- let succs = CFG.fold_succ_e (fun e acc -> e::acc) env.graph n [] in
- CFG.remove_vertex env.graph n;
- List.iter
- (fun e ->
- let e' = CFG.E.create (CFG.E.src e) (CFG.E.label e) n' in
- debug "replace edge %a %a %a"
- VL.pretty (CFG.E.src e) EL.pretty !(CFG.E.label e) VL.pretty n';
- CFG.add_edge_e env.graph e') preds;
- List.iter
- (fun e ->
- let e' = CFG.E.create n' (CFG.E.label e) (CFG.E.dst e) in
- debug "replace edge %a %a %a"
- VL.pretty n' EL.pretty !(CFG.E.label e) VL.pretty (CFG.E.dst e) ;
- CFG.add_edge_e env.graph e') succs;
- n'
-
-let add_edge env n1 edge_type n2 =
- let e = CFG.E.create n1 (ref edge_type) n2 in
- debug "add edge : %a@." pp_edge e;
- CFG.add_edge_e env.graph e
-
-let remove_edge env e =
- debug "remove edge : %a@." pp_edge e;
- CFG.remove_edge_e env.graph e
-
-let insert_loop_node env loop_head loop_kind =
- let n_loop = add_node env loop_kind in
- let mv_pred_edge e =
- add_edge env (edge_src e) (edge_type e) n_loop;
- remove_edge env e
- in iter_pred_e mv_pred_edge env loop_head;
- add_edge env n_loop Enone loop_head;
- n_loop
-
-let init_cfg spec_only kf =
- let env = new_cfg_env spec_only kf in
- let start = add_node env (Vstart) in
- let fct_in = add_node env (VfctIn) in
- let _ = add_edge env start Enone fct_in in
- let fct_out = add_node env (VfctOut) in
- let fct_err = add_node env (VfctErr) in
- let nend = add_node env (Vend) in
- let _ = add_edge env fct_out Enone nend in
- let _ = add_edge env fct_err Enone nend in
- env, fct_in, fct_out
-
-let get_node env t =
- let id = node_type_id t in
- debug "get_node: %a --> id:%d,%d"
- pp_node_type t (fst id) (snd id);
- try Hashtbl.find env.stmt_node id
- with Not_found -> add_node env t
-
-(** Setup the preconditions at all the call points of [e_kf], when possible *)
-let setup_preconditions_proxies e_kf =
- match e_kf.enode with
- | Lval (Var vkf, NoOffset) ->
- let kf = Globals.Functions.get vkf in
- Statuses_by_call.setup_all_preconditions_proxies kf
- | _ -> () (* call through function pointer *)
-
-let get_call_type fct =
- match Kernel_function.get_called fct with
- | None -> Dynamic fct
- | Some kf -> Static kf
-
-(** In some cases (goto for instance) we have to create a node before having
- * processed if through [cfg_stmt]. It is important that the created node
- * is the same than while the 'normal' processing ! That is why
- * this pattern matching might seem redundant with the other one. *)
-let get_stmt_node env s =
- let do_call res fct args _loc =
- get_node env (Vcall (s, res, get_call_type fct, args))
- in
- match s.skind with
- | Instr (Call (res, fct, args, loc)) -> do_call res fct args loc
- | Instr (Local_init (v, ConsInit(f, args, kind), loc)) ->
- Cil.treat_constructor_as_func do_call v f args kind loc
- | Block b -> get_node env (VblkIn (Bstmt s,b))
- | UnspecifiedSequence seq ->
- let b = Cil.block_from_unspecified_sequence seq in
- get_node env (VblkIn (Bstmt s,b))
- | If (e, _, _, _) -> get_node env (Vtest (true, s, e))
- | Loop _ -> get_node env (Vloop (None, s))
- | Break _ | Continue _ | Goto _
- | Instr _ | Return _ -> get_node env (Vstmt s)
- | Switch (e, _, _, _) -> get_node env (Vswitch (s, e))
- | TryExcept _ | TryFinally _ | Throw _ | TryCatch _ ->
- Wp_parameters.not_yet_implemented
- ~source:(fst (Cil_datatype.Stmt.loc s)) "[cfg] exception handling"
-
-let cfg_stmt_goto env s next =
- let node = get_node env (Vstmt s) in
- add_edge env node Enone next ; node
-
-let get_succ env s =
- begin match s.succs with
- | [s'] -> get_stmt_node env s'
- | _ -> Wp_parameters.fatal "[cfg] jump with more than one successor ?"
- end
-
-(** build the nodes for the [stmts], connect the last one with [next],
- * and return the node of the first stmt. *)
-let rec cfg_stmts env stmts next = match stmts with
- | [] -> next
- | [s] -> cfg_stmt env s next
- | s::tl ->
- let next = cfg_stmts env tl next in
- let ns = cfg_stmt env s next in
- ns
-
-and cfg_block env bkind b next =
- let in_blk = get_node env (VblkIn (bkind, b)) in
- let out_blk = get_node env (VblkOut (bkind, b)) in
- let _ = add_edge env in_blk Enext out_blk in
- let _ = add_edge env out_blk Enone next in
- let first_in_blk = cfg_stmts env b.bstmts out_blk in
- let _ = add_edge env in_blk Enone first_in_blk in
- in_blk
-
-and cfg_switch env switch_stmt switch_exp blk case_stmts next =
- let n_switch = get_node env (Vswitch (switch_stmt, switch_exp)) in
- add_edge env n_switch Enext next;
- begin
- let s_break = env.node_break in
- try
- env.node_break <- Some next ;
- let _first = cfg_stmts env blk.bstmts next in
- env.node_break <- s_break ;
- with e ->
- env.node_break <- s_break ;
- raise e
- end ;
- let branch with_def s =
- let n = get_stmt_node env s in
- let rec find_case l = match l with
- | [] -> false, []
- | Case (e, _)::tl ->
- let r = match find_case tl with
- | true, [] -> true, []
- | true, _ -> assert false
- | false, l -> false, e::l
- in r
- | Default _ :: _ ->
- (* we don't check if we have several Default because it is impossible:
- * CIL gives an error *)
- true, []
- | _::tl -> find_case tl
- in
- let def, case = find_case s.labels in
- if case = [] && not def then
- Wp_parameters.fatal "[cfg] switch branch without label";
- add_edge env n_switch (Ecase case) n;
- if def then true else with_def
- in
- let with_def = List.fold_left branch false case_stmts in
- let _ = if not with_def then add_edge env n_switch (Ecase []) next in
- n_switch
-
-and cfg_stmt env s next =
- Db.yield ();
- match s.skind with
- | Instr (Call (_, f, _, _)) ->
- setup_preconditions_proxies f;
- let in_call = get_stmt_node env s in
- add_edge env in_call Enone next;
- let exit_node = get_node env VfctErr in
- add_edge env in_call Enone exit_node;
- in_call
- | Instr (Local_init(_,ConsInit (f, _, _), _)) ->
- let kf = Globals.Functions.get f in
- Statuses_by_call.setup_all_preconditions_proxies kf;
- let in_call = get_stmt_node env s in
- add_edge env in_call Enone next;
- let exit_node = get_node env VfctErr in
- add_edge env in_call Enone exit_node;
- in_call
- | Instr _ | Return _ ->
- let n = get_stmt_node env s in
- add_edge env n Enone next;
- n
- | Block b ->
- cfg_block env (Bstmt s) b next
- | UnspecifiedSequence seq ->
- let b = Cil.block_from_unspecified_sequence seq in
- cfg_block env (Bstmt s) b next
- | If (e, b1, b2, _) ->
- begin
- let n_in = get_stmt_node env s (*get_node env (Vtest (true, s, e))*) in
- let n_out = get_node env (Vtest (false, s, e)) in
- (* this node is to ensure that there is only one edge before
- * the [next] node of a if to put post properties about the IF. *)
- add_edge env n_out Enone next;
- let in_b1 = cfg_block env (Bthen s) b1 n_out in
- let in_b2 = cfg_block env (Belse s) b2 n_out in
- add_edge env n_in Ethen in_b1;
- add_edge env n_in Eelse in_b2;
- add_edge env n_in Enext next;
- n_in
- end
- | Loop(_, b, _, _, _) ->
- let s_loop = get_stmt_node env s in
- let b_loop = Bloop s in
- let s_out = get_node env (VblkOut(b_loop,b)) in
- let b_in = cfg_block_with
- ~break:next
- ~continue:s_out
- env b_loop b s_loop in
- add_edge env s_loop Enext next;
- add_edge env s_loop Enone b_in;
- s_loop
- | Break _ ->
- begin match env.node_break with
- | None -> Wp_parameters.fatal "[cfg] missing break successor"
- | Some brk -> cfg_stmt_goto env s brk
- end
- | Continue _ ->
- begin match env.node_continue with
- | None -> Wp_parameters.fatal "[cfg] missing continue successor"
- | Some cnt -> cfg_stmt_goto env s cnt
- end
- | Goto _ -> cfg_stmt_goto env s (get_succ env s)
- | Switch (e, b, lstmts, _) ->
- cfg_switch env s e b lstmts next
- | TryExcept _ | TryFinally _ | Throw _ | TryCatch _ ->
- Wp_parameters.not_yet_implemented
- ~source:(fst (Cil_datatype.Stmt.loc s)) "[cfg] exception handling"
-
-and cfg_block_with ?continue ?break env bkind block next =
- let s_continue = env.node_continue in
- let s_break = env.node_break in
- try
- if continue <> None then env.node_continue <- continue ;
- if break <> None then env.node_break <- break ;
- let head = cfg_block env bkind block next in
- env.node_continue <- s_continue ;
- env.node_break <- s_break ;
- head
- with e ->
- env.node_continue <- s_continue ;
- env.node_break <- s_break ;
- raise e
-
-(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-(** {3 Cleaning} remove node and edges that are unreachable *)
-
-let clean_graph cfg =
- let graph = cfg_graph cfg in
- let rec reach n =
- if n.reachable then ()
- else (n.reachable <- true; iter_succ reach cfg n)
- in reach (cfg_start cfg);
- let clean n acc =
- if n.reachable then acc
- else begin
- debug "remove unreachable node %a@." VL.pretty n;
- let v = node_type n in
- CFG.remove_vertex graph n;
- Hashtbl.remove cfg.stmt_node (node_type_id v);
- v::acc
- end
- in
- let unreach = fold_nodes clean cfg [] in
- { cfg with unreachables = unreach }
-
-
-(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-(** {3 About loops}
- * Let's first remind some definitions about loops :
- * - {b back edge} : edge n->h such that h dominates n.
- * - {b natural loop} : defined by a back edge n->h
- * * h is called the {b loop header},
- * * the body of the loop is the set of nodes n that are "between" h and n,
- * ie all n predecessors until h.
- * Because h dominates n, every backward path from n go through h.
- * Notice that each node in the loop body is dominated by h.
- *
- * A loop is not a natural loop if it has several entries (no loop header),
- * or if it has some irreducible region (no back edge).
- *
- * Below, we use an algorithm from the paper :
- * "A New Algorithm for Identifying Loops in Decompilation"
- * of Tao Wei, Jian Mao, Wei Zou, and Yu Chen,
- * to gather information about the loops in the built CFG.
-*)
-
-module type WeiMaoZouChenInput = sig
- type graph
- type node
- type tenv
-
- (** build a new env from a graph,
- * and also return the entry point of the graph which has to be unique. *)
- val init : graph -> tenv * node
-
- (** apply the function on the node successors *)
- val fold_succ : (tenv -> node -> tenv) -> tenv -> node -> tenv
-
- val eq_nodes : node -> node -> bool
-
- (** store the position for the node and also the fact that the node has
- * been seen *)
- val set_pos : tenv -> node -> int -> tenv
-
- (** reset the position (set the position to 0), but should keep the
- * information that the node has been seen already. *)
- val reset_pos : tenv -> node -> tenv
-
- (** get the previously stored position of the node or 0 if nothing has been
- * stored *)
- val get_pos : tenv -> node -> int
-
- (** get the previously stored position of the node if any, or None
- * if [set_pos] hasn't been called already for this node. *)
- val get_pos_if_traversed : tenv -> node -> int option
-
- (** [set_iloop_header env b h] store h as the innermost loop header for b.
- * Beware that this function can be called several times for the same b
- * with different values of h during the computation. Only the last one
- * will give the correct information.
- * *)
- val set_iloop_header : tenv -> node -> node -> tenv
-
- (** get the node innermost loop header if any *)
- val get_iloop_header : tenv -> node -> node option
-
- (** store the node as a loop header. *)
- val add_loop_header : tenv -> node -> tenv
-
- (** store the node as an irreducible loop header. *)
- val add_irreducible : tenv -> node -> tenv
-
- (** store the edge between the two nodes (n1, n2) as a reentry edge.
- * n2 is the reentry point which means that it is in a loop,
- * but it is not the loop header, and n1 is not in the loop. *)
- val add_reentry_edge : tenv -> node -> node -> tenv
-
- (* val pretty_node : Format.formatter -> node -> unit *)
-end
-
-(** Implementation of
- * "A New Algorithm for Identifying Loops in Decompilation" *)
-module WeiMaoZouChen (G : WeiMaoZouChenInput) : sig
- val identify_loops : G.graph -> G.tenv
-end = struct
-
- let tag_lhead env b h =
- match h with
- | None -> env
- | Some h ->
- if G.eq_nodes h b then (* already done *) env
- else
- let rec do_cur env cur_b cur_h =
- match G.get_iloop_header env cur_b with
- | None -> G.set_iloop_header env cur_b cur_h
- | Some hb when G.eq_nodes hb cur_h -> (* nothing to do *) env
- | Some hb ->
- if (G.get_pos env hb) < (G.get_pos env cur_h) then
- let env = G.set_iloop_header env cur_b cur_h in
- do_cur env cur_h hb
- else do_cur env hb cur_h
- in do_cur env b h
-
- (** @return innermost loop header of b0 (None if b0 is not in a loop) *)
- let rec trav_loops_DFS env b0 pos =
- let env = G.set_pos env b0 pos in
- let do_b env b =
- match G.get_pos_if_traversed env b with
- | None -> (* case A : b is not traversed already *)
- let env, nh = trav_loops_DFS env b (pos + 1) in
- tag_lhead env b0 nh
- | Some b_pos when (b_pos > 0) ->
- begin (* case B : b already in path -> it is a loop *)
- let env = G.add_loop_header env b in
- tag_lhead env b0 (Some b)
- end
- | Some 0 ->
- begin
- match G.get_iloop_header env b with
- | None -> (* case C : do nothing *) env
- | Some h when (G.get_pos env h > 0) ->
- (* case D : b not in path, but h is *)
- tag_lhead env b0 (Some h)
- | Some h -> (* h not in path *)
- begin (* case E : reentry *)
- assert (G.get_pos env h = 0);
- let env = G.add_irreducible env h in
- let env = G.add_reentry_edge env b0 b in
- let rec f env h = match G.get_iloop_header env h with
- | Some h when (G.get_pos env h > 0) ->
- tag_lhead env b0 (Some h)
- | Some h ->
- let env = G.add_irreducible env h in
- f env h
- | None -> env
- in f env h
- end
- end
- | _ -> assert false (* b_pos cannot be < 0 *)
- in
- let env = G.fold_succ do_b env b0 in
- let env = G.reset_pos env b0 in
- let h0 = G.get_iloop_header env b0 in
- env, h0
-
- let identify_loops g =
- let env, start = G.init g in
- let env, _ = trav_loops_DFS env start 1 in
- env
-
-end
-
-(** To use WeiMaoZouChen algorithm,
- * we need to define how to interact with our CFG graph *)
-module LoopInfo = struct
- type node = CFG.V.t
- type graph = t
- type tenv = { graph : t ;
- dfsp : int Ntbl.t;
- iloop_header : node Ntbl.t;
- loop_headers : node list ;
- irreducible : node list ;
- unstruct_coef : int }
-
- let init cfg =
- let env = { graph = cfg ;
- dfsp = Ntbl.create 97; iloop_header = Ntbl.create 7;
- loop_headers = []; irreducible = []; unstruct_coef = 0 } in
- env, cfg_start cfg
-
- let eq_nodes = CFG.V.equal
-
- let set_pos env n pos = Ntbl.add env.dfsp n pos; env
- let reset_pos env n = Ntbl.replace env.dfsp n 0; env
- let get_pos env n = try Ntbl.find env.dfsp n with Not_found -> 0
- let get_pos_if_traversed env n =
- try Some (Ntbl.find env.dfsp n) with Not_found -> None
-
- let set_iloop_header env b h = Ntbl.add env.iloop_header b h; env
- let get_iloop_header env b =
- try Some (Ntbl.find env.iloop_header b) with Not_found -> None
-
- let add_loop_header env h = { env with loop_headers = h :: env.loop_headers}
- let add_irreducible env h = { env with irreducible = h :: env.irreducible}
- let add_reentry_edge env _ _ = (* TODO *) env
-
- let is_irreducible env h = List.exists (eq_nodes h) env.irreducible
-
- let fold_succ f env n = fold_succ (fun v env -> f env v) env.graph n env
-
- let unstructuredness env =
- let k = float_of_int env.unstruct_coef in
- let k = k /. (float_of_int (CFG.nb_edges (cfg_graph env.graph))) in
- let k = 1. +. k in
- k
-
-end
-
-module Mloop = WeiMaoZouChen (LoopInfo)
-
-let set_back_edge e =
- let info = CFG.E.label e in
- match !info with
- | Eback | EbackThen | EbackElse -> ()
- | Enone -> info := Eback
- | Ethen -> info := EbackThen
- | Eelse -> info := EbackElse
- | Ecase _ | Enext -> assert false
-
-let mark_loops cfg =
- let env = Mloop.identify_loops cfg in
- let mark_loop_back_edge h = match node_stmt_opt h with
- | None -> (* Because we use !Db.Dominators that work on statements,
- we don't know how to detect back edge here.
- TODO: compute dominators on our cfg ? *) false
- | Some h_stmt ->
- let mark_back_edge e =
- let n = edge_src e in
- let is_back_edge =
- try
- let n_stmt = node_stmt_exn n in
- Dominators.dominates h_stmt n_stmt
- with Not_found -> false (* pred of h is not a stmt *)
- in
- if is_back_edge then set_back_edge e;
- debug "to loop edge %a@." pp_edge e
- in iter_pred_e mark_back_edge cfg h; true
- in
- let mark_loop loops h =
- debug "loop head in %a@." VL.pretty h;
- let is_natural =
- if (LoopInfo.is_irreducible env h) then
- (debug "irreducible loop detected in %a@." VL.pretty h; false)
- else true
- in let back_edges_ok =
- if is_natural then mark_loop_back_edge h else true
- in
- let loop = match node_type h with
- | Vloop (_, h_stmt) ->
- assert (back_edges_ok);
- change_node_kind cfg h (Vloop (Some is_natural, h_stmt))
- | _ -> match node_stmt_opt h with
- | Some h_stmt when back_edges_ok ->
- insert_loop_node cfg h (Vloop (Some is_natural, h_stmt))
- | None when back_edges_ok ->
- let n = cfg.loop_cpt in cfg.loop_cpt <- n + 1;
- insert_loop_node cfg h (Vloop2 (is_natural, n))
- | _ -> (* consider it has non-natural. *)
- let n = cfg.loop_cpt in cfg.loop_cpt <- n + 1;
- insert_loop_node cfg h (Vloop2 (false, n))
- in loop::loops
- in
- let loops = List.fold_left mark_loop [] env.LoopInfo.loop_headers in
- debug2 "unstructuredness coef = %f@." (LoopInfo.unstructuredness env);
- { cfg with loop_nodes = Some loops }
-
-let loop_nodes cfg = match cfg.loop_nodes with Some l -> l
- | None -> Wp_parameters.fatal
- "Cannot use the loop nodes before having computed them"
-
-let strange_loops cfg =
- let strange n = match node_type n with
- | Vloop (Some is_natural, _) when is_natural -> false
- | _ -> true
- in let loops = loop_nodes cfg in
- let strange_loops = List.filter strange loops in
- debug "%d/%d strange loops"
- (List.length strange_loops) (List.length loops);
- strange_loops
-
-let very_strange_loops cfg =
- let strange n = match node_type n with
- | Vloop (Some _, _) | Vloop2 _ -> false
- | _ -> true
- in let loops = loop_nodes cfg in
- let strange_loops = List.filter strange loops in
- debug "%d/%d very strange loops"
- (List.length strange_loops) (List.length loops);
- strange_loops
-
-(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-(** {3 Create CFG} *)
-
-(*
-Debugging code exporting the CFG in DOT:
-
-let pp_node_type_dot fmt = function
- | Bstmt { sid } -> Format.fprintf fmt "s%d" sid
- | Bthen { sid } -> Format.fprintf fmt "then_s%d" sid
- | Belse { sid } -> Format.fprintf fmt "else_s%d" sid
- | Bloop { sid } -> Format.fprintf fmt "loop_s%d" sid
- | Bfct -> Format.fprintf fmt "fct"
-
-let pp_node_dot fmt { kind } =
- match kind with
- | Vstart -> Format.fprintf fmt "START"
- | Vend -> Format.fprintf fmt "END"
- | Vexit -> Format.fprintf fmt "EXIT"
- | VfctIn -> Format.fprintf fmt "FIN"
- | VfctOut -> Format.fprintf fmt "FOUT"
- | VblkIn (b,_) -> Format.fprintf fmt "IN_%a" pp_node_type_dot b
- | VblkOut (b,_) -> Format.fprintf fmt "OUT_%a" pp_node_type_dot b
- | Vstmt { sid } -> Format.fprintf fmt "STMT_s%d" sid
- | Vloop(_,{ sid }) -> Format.fprintf fmt "LOOP_s%d" sid
- | Vloop2(_,k) -> Format.fprintf fmt "LOOP2_%d" k
- | Vtest(true,{ sid },_) -> Format.fprintf fmt "TEST_IN_s%d" sid
- | Vtest(false,{ sid },_) -> Format.fprintf fmt "TEST_OUT_s%d" sid
- | Vswitch({ sid },_) -> Format.fprintf fmt "SWITCH_s%d" sid
- | Vcall({ sid },_,_,_) -> Format.fprintf fmt "CALL_s%d" sid
-
-let pp_cfg_dot name { kernel_function = kf ; graph } =
- Command.pp_to_file
- (Printf.sprintf "%s-%s.dot" (Kernel_function.get_name kf) name)
- begin fun fmt ->
- Format.fprintf fmt "digraph %s {@\n" name ;
- Format.fprintf fmt " rankdir = TB;@\n" ;
- CFG.iter_edges_e
- (fun (s,i,t) ->
- match !i with
- | Enext -> ()
- | Enone ->
- Format.fprintf fmt " %a -> %a ;@\n" pp_node_dot s pp_node_dot t
- | info ->
- Format.fprintf fmt " %a -> %a [ label=\"%a\" ] ;@\n"
- pp_node_dot s pp_node_dot t EL.pretty info
- ) graph ;
- Format.fprintf fmt "}@." ;
- end
-*)
-
-let cfg_from_definition kf f =
- let kf_name = Kernel_function.get_name kf in
- let cfg, fct_in, fct_out = init_cfg false kf in
- let in_b = cfg_block cfg Bfct f.sbody fct_out in
- let _ = add_edge cfg fct_in Enone in_b in
- let graph = cfg_graph cfg in
- debug "for function '%s': %d vertex - %d edges@."
- kf_name (CFG.nb_edges graph) (CFG.nb_vertex graph);
- debug
- "start removing unreachable in %s@." kf_name;
- Db.yield ();
- let cfg = clean_graph cfg in
- debug "for function '%s': %d vertex - %d edges@."
- kf_name (CFG.nb_edges graph) (CFG.nb_vertex graph);
- Db.yield ();
- debug
- "start loop analysis for %s@." kf_name;
- let cfg = mark_loops cfg in
- cfg
-
-let cfg_from_proto kf =
- let cfg, fct_in, fct_out = init_cfg true kf in
- let _ = add_edge cfg fct_in Enone fct_out in
- let cfg = { cfg with loop_nodes = Some [] } in
- cfg
-
-(* ------------------------------------------------------------------------ *)
-(** {2 CFG management} *)
-
-let create kf =
- let kf_name = Kernel_function.get_name kf in
- debug "create cfg for function '%s'@." kf_name;
- let cfg =
- try
- let f = Kernel_function.get_definition kf in
- cfg_from_definition kf f
- with Kernel_function.No_Definition ->
- cfg_from_proto kf
- in debug "done for %s@." kf_name;
- Db.yield ();
- cfg
-
-module KfCfg =
- Kernel_function.Make_Table
- (Datatype.Make
- (struct
- include Datatype.Undefined
- type tt = t
- type t = tt
- let name = "WpCfg"
- let mem_project = Datatype.never_any_project
- let reprs =
- List.map
- (fun kf ->
- { kernel_function = kf;
- spec_only = true;
- graph = CFG.create ();
- stmt_node = Hashtbl.create 0;
- unreachables = [];
- loop_nodes = None;
- loop_cpt = 0;
- node_break = None;
- node_continue = None;
- }
- )
- Kernel_function.reprs
- let equal t1 t2 =
- Kernel_function.equal t1.kernel_function t2.kernel_function
- let hash t = Kernel_function.hash t.kernel_function
- let compare t1 t2 =
- Kernel_function.compare t1.kernel_function t2.kernel_function
- end))
- (struct let name = "KfCfg"
- let dependencies = [Ast.self]
- let size = 17
- end)
-
-let get kf = KfCfg.memo create kf
-
-(* ------------------------------------------------------------------------ *)
-(** {2 CFG dump} *)
-
-module Dump =
-struct
- type dot = {
- name: string;
- chan: out_channel;
- fmt : 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
deleted file mode 100644
index 97ef821dd4005d62a566c673811065aa68da8edd..0000000000000000000000000000000000000000
--- a/src/plugins/wp/cil2cfg.mli
+++ /dev/null
@@ -1,184 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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 Clabels
-
-(** abstract type of a cfg *)
-type t
-
-(** @raise Log.FeatureRequest for non natural loops and 'exception' stmts.
- * @return the graph and the list of unreachable nodes.
- * *)
-val get : Kernel_function.t -> t
-
-(** abstract type of the cfg nodes *)
-type node
-val pp_node : Format.formatter -> node -> unit
-val same_node : node -> node -> bool
-
-(** abstract type of the cfg edges *)
-type edge
-val pp_edge : Format.formatter -> edge -> unit
-val same_edge : edge -> edge -> bool
-
-(** get the starting edges *)
-val start_edge : t -> edge
-
-(** set of edges *)
-module Eset : Set.S with type elt = edge
-
-(** node and edges relations *)
-val edge_src : edge -> node
-val edge_dst : edge -> node
-val pred_e : t -> node -> edge list
-val succ_e : t -> node -> edge list
-
-(** iterators *)
-val fold_nodes : (node -> 'a -> 'a) -> t -> 'a -> 'a
-val iter_nodes : (node -> unit) -> t -> unit
-val iter_edges : (edge -> unit) -> t -> unit
-
-(** Be careful that only Bstmt are real Block statements *)
-type block_type = private
- | Bstmt of stmt | Bthen of stmt | Belse of stmt | Bloop of stmt | Bfct
-
-type call_type =
- | Dynamic of exp
- | Static of kernel_function
-
-val pp_call_type : Format.formatter -> call_type -> unit
-val get_call_type : exp -> call_type
-
-type node_type = private
- | Vstart | Vend
- | VfctIn | VfctOut | VfctErr
- | VblkIn of block_type * block
- | VblkOut of block_type * block
- | Vstmt of stmt
- | Vcall of stmt * lval option * call_type * exp list
- | Vtest of bool * stmt * exp
- | Vswitch of stmt * exp
- | Vloop of bool option * stmt
- (** boolean is is_natural. None means the node has not been
- * detected as a loop. *)
- | Vloop2 of bool * int
-
-val node_type : node -> node_type
-val pp_node_type : Format.formatter -> node_type -> unit
-
-val node_stmt_opt : node -> stmt option
-val start_stmt_of_node : node -> stmt option
-
-(** @return the nodes that are unreachable from the 'start' node.
- * These nodes have been removed from the cfg already. *)
-val unreachable_nodes : t -> node_type list
-
-(** similar to [succ_e g v]
- * but tests the branch to return (then-edge, else-edge)
- * @raise Invalid_argument if the node is not a test.
- * *)
-val get_test_edges : t -> node -> edge * edge
-
-(** similar to [succ_e g v]
- but give the switch cases and the default edge *)
-val get_switch_edges : t -> node -> (exp list * edge) list * edge
-
-(** similar to [succ_e g v]
- but gives the edge to VcallOut first and the edge to Vexit second. *)
-val get_call_out_edges : t -> node -> edge * edge
-
-type block_scope = { b_opened : block list ; b_closed : block list }
-
-val block_scope_for_edge : t -> edge -> block_scope
-
-val is_back_edge : edge -> bool
-
-(** detect is there are non natural loops or natural loops where we didn't
- * manage to compute back edges (see [mark_loops]). Must be empty in the mode
- * [-wp-no-invariants]. (see also [very_strange_loops]) *)
-val strange_loops : t -> node list
-
-(** detect is there are natural loops where we didn't manage to compute
- * back edges (see [mark_loops]). At the moment, we are not able to handle those
- * loops. *)
-val very_strange_loops : t -> node list
-
-(** @return the (normalized) labels at the program point of the edge. *)
-val get_edge_labels : edge -> Clabels.c_label list
-
-(** Complete get_edge_labels and returns the associated stmt, if any. *)
-val get_edge_stmt : edge -> stmt option
-
-(** @return None when the edge leads to the end of the function. *)
-val get_edge_next_stmt : t -> edge -> stmt option
-
-(** whether an exit edge exists or not *)
-val has_exit : t -> bool
-
-(** Find the edges where the precondition of the node statement have to be
- * checked. *)
-val get_pre_edges : t -> node -> edge list
-
-(** Find the edges where the postconditions of the node statement have to be
- * checked. *)
-val get_post_edges : t -> node -> edge list
-
-(** Get the label to be used for the Post state of the node contract if any. *)
-val get_post_label : t -> node -> c_label option
-
-(** Find the edges [e] that goes to the [Vexit] node inside the statement
- * beginning at node [n] *)
-val get_exit_edges : t -> node -> edge list
-
-(** Find the edges [e] of the statement node [n] postcondition
- * and the set of edges that are inside the statement ([e] excluded).
- * For instance, for a single statement node, [e] is [succ_e n],
- * and the set is empty. For a test node, [e] are the last edges of the 2
- * branches, and the set contains all the edges between [n] and the [e] edges.
- * *)
-val get_internal_edges : t -> node -> edge list * Eset.t
-
-val cfg_kf : t -> Kernel_function.t
-val cfg_spec_only : t -> bool
-(** returns [true] is this CFG is degenerated (no code available) *)
-
-(** signature of a mapping table from cfg edges to some information. *)
-module type HEsig =
-sig
- type ti
- type t
- val create : int -> t
- val find : t -> edge -> ti
- val find_all : t -> edge -> ti list
- val add : t -> edge -> ti -> unit
- val replace : t -> edge -> ti -> unit
- val remove : t -> edge -> unit
- val clear : t -> unit
-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/register.ml b/src/plugins/wp/register.ml
index cd673ad5553ef608a18959dc17135fe8626d4443..a141dbb8301552cde45306ca2832a0b675654a17 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -157,9 +157,9 @@ let clear_scheduled () =
exercised := 0 ;
session := GOALS.empty ;
provers := PM.empty ;
- WpAnnot.trivial_terminates := 0 ;
- WpAnnot.unreachable_proved := 0 ;
- WpAnnot.unreachable_failed := 0 ;
+ CfgInfos.trivial_terminates := 0 ;
+ WpReached.unreachable_proved := 0 ;
+ WpReached.unreachable_failed := 0 ;
end
let get_pstat p =
@@ -439,13 +439,13 @@ let do_report_scheduled () =
else
let total =
!scheduled +
- !WpAnnot.unreachable_failed +
- !WpAnnot.unreachable_proved +
- !WpAnnot.trivial_terminates in
+ !WpReached.unreachable_failed +
+ !WpReached.unreachable_proved +
+ !CfgInfos.trivial_terminates in
if total > 0 then
begin
let passed =
- !WpAnnot.unreachable_proved + !WpAnnot.trivial_terminates
+ !WpReached.unreachable_proved + !CfgInfos.trivial_terminates
in
let passed = GOALS.fold
(fun g n ->
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
deleted file mode 100644
index 7a0dc8f397154c76cfcfc13f8aa029173ab82de8..0000000000000000000000000000000000000000
--- a/src/plugins/wp/wpAnnot.ml
+++ /dev/null
@@ -1,1425 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-let dkey = Wp_parameters.register_category "annot" (* debugging key *)
-let debug fmt = Wp_parameters.debug ~dkey fmt
-
-(* This file groups functions that extract some annotations
- * and associates them with CFG edges. *)
-
-open Cil_types
-open Cil_datatype
-open Logic_utils
-
-(* -------------------------------------------------------------------------- *)
-(* --- Status of Unreachable Annotations --- *)
-(* -------------------------------------------------------------------------- *)
-
-let unreachable_proved = ref 0
-let unreachable_failed = ref 0
-
-let wp_unreachable =
- Emitter.create
- "Unreachable Annotations"
- [ Emitter.Property_status ]
- ~correctness:[] (* TBC *)
- ~tuning:[] (* TBC *)
-
-let set_unreachable pid =
- if WpPropId.is_smoke_test pid then
- begin
- let source = WpPropId.source_of_id pid in
- WpReached.set_doomed wp_unreachable pid ;
- incr unreachable_failed ;
- Wp_parameters.warning ~source "Failed smoke-test"
- end
- else
- let open Property in
- let emit = function
- | IPPredicate {ip_kind = PKAssumes _} -> ()
- | p ->
- debug "unreachable annotation %a@." Property.pretty p;
- Property_status.emit wp_unreachable ~hyps:[] p Property_status.True
- in
- let pids = match WpPropId.property_of_id pid with
- | IPPredicate {ip_kind = PKAssumes _} -> []
- | IPBehavior {ib_kf; ib_kinstr; ib_active; ib_bhv} ->
- let active = Datatype.String.Set.elements ib_active in
- (ip_post_cond_of_behavior ib_kf ib_kinstr active ib_bhv) @
- (ip_requires_of_behavior ib_kf ib_kinstr ib_bhv)
- | IPExtended _ -> []
- (* Extended clauses might concern anything. Don't validate them
- unless we know exactly what is going on. *)
- | p ->
- incr unreachable_proved ;
- Wp_parameters.result "[CFG] Goal %a : Valid (Unreachable)"
- WpPropId.pp_propid pid ; [p]
- in
- List.iter emit pids
-
-(* -------------------------------------------------------------------------- *)
-(* --- Status of Terminates Annotations --- *)
-(* -------------------------------------------------------------------------- *)
-
-let trivial_terminates = ref 0
-
-let wp_trivially_terminates =
- Emitter.create
- "Trivial Termination"
- [Emitter.Property_status]
- ~correctness:[] (* TBC *)
- ~tuning:[] (* TBC *)
-
-let set_trivially_terminates p hyps =
- incr trivial_terminates ;
- Wp_parameters.result "[CFG] Goal %a : Valid (Trivial)" WpPropId.pp_propid p ;
- let pid = WpPropId.property_of_id p in
- let hyps = Property.Set.elements hyps in
- Property_status.emit wp_trivially_terminates ~hyps pid Property_status.True
-
-(* -------------------------------------------------------------------------- *)
-(* --- 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
- let called_pre = WpPropId.property_of_id id in
- let called_pre_p =
- 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 at call-point as WpPropId.t *)
-let preconditions_at_call s = function
- | Cil2cfg.Static kf ->
- let preconds = call_preconditions kf s in
- let aux (pre, pre_call) = WpPropId.mk_call_pre_id kf s pre pre_call in
- List.map aux preconds
- | Cil2cfg.Dynamic _ -> []
-
-(* ########################################################################## *)
-(* ### WARNING: DEPRECATED API BELOW THIS LINE ### *)
-(* ########################################################################## *)
-
-(*----------------------------------------------------------------------------*)
-(* Strategy and annotations *)
-(*----------------------------------------------------------------------------*)
-
-(* This is to code what kind of properties we want to process. *)
-type asked_assigns = NoAssigns | OnlyAssigns | WithAssigns
-
-(* This is to code which behavior the computed strategy refers to. *)
-type asked_bhv =
- | FunBhv of funbehavior option (* None means default behavior
- when the function has no spec. This is useful to process internal
- properties even if the function has no default behavior *)
- | StmtBhv of Cil2cfg.node * stmt * Datatype.String.Set.t * funbehavior
-
-let name_of_asked_bhv = function
- | FunBhv (Some bhv) -> bhv.b_name
- | FunBhv None -> Cil.default_behavior_name
- | StmtBhv (_, _, _, bhv) -> bhv.b_name
-
-let asked_bhv = function
- | FunBhv None -> None
- | FunBhv (Some bhv) | StmtBhv (_,_,_,bhv) -> Some bhv.b_name
-
-(* This is to code what properties the user asked for in a given behavior. *)
-type asked_prop =
- | AllProps
- | NamedProp of string list
- | IdProp of Property.t
- | CallPre of stmt * Property.t option (** No specified property means all *)
-
-(* a table to keep the information about the statement default specification
- * associated with each edge in order to know in which strategy we should put a
- * default annotation on this edge. When an edge has no information in the table,
- * it means that the edge annotations belong to the [FunBhv] default behavior;
- * and when we find a statement [s], it means that they belong to the [StmtBhv s]
- * default behavior. The [int] information is only useful to build the table :
- * when an edge is included in 2 different [StmtBhv] we only keep the one that
- * has the fewer internal edges because it is necessarily included in the other.
-*)
-module HdefAnnotBhv = Cil2cfg.HE (struct type t = (stmt * int) end)
-
-(* Finally, a configuration is associated to a strategy computation to
- * summarize what is to be computed. *)
-type strategy_info = {
- kf : Kernel_function.t;
- cfg : Cil2cfg.t;
- reachability : WpReached.reachability option ;
- cur_bhv : asked_bhv;
- asked_prop : asked_prop;
- assigns_filter : asked_assigns;
- def_annots_info : HdefAnnotBhv.t;
-}
-
-(*----------------------------------------------------------------------------*)
-(* Adding things in the strategy *)
-(*----------------------------------------------------------------------------*)
-
-(* Select annotations to take as Hyp/Goal/... *)
-
-let pp_assigns_mode fmt config =
- let str = match config.assigns_filter with
- | NoAssigns -> "without assigns"
- | OnlyAssigns -> "only with assigns"
- | WithAssigns -> "both assigns or not"
- in Format.fprintf fmt "%s" str
-
-let pp_asked_prop fmt = function
- | AllProps -> Format.fprintf fmt "all properties"
- | NamedProp names -> Format.fprintf fmt "properties %a"
- (Pretty_utils.pp_list ~sep:"," Format.pp_print_string) names
- | IdProp p -> Format.fprintf fmt "property %s" (Property.Names.get_prop_name_id p)
- | CallPre (s, Some p) -> Format.fprintf fmt "pre %s at stmt %a"
- (Property.Names.get_prop_name_id p) Stmt.pretty_sid s
- | CallPre (s, None) -> Format.fprintf fmt "all call preconditions at stmt %a"
- Stmt.pretty_sid s
-
-let pp_strategy_info fmt config =
- Format.fprintf fmt "'%a', " Kernel_function.pretty config.kf;
- let _ = match config.cur_bhv with
- | FunBhv _bhv ->
- Format.fprintf fmt "behavior '%s'" (name_of_asked_bhv config.cur_bhv)
- | StmtBhv (_, s, a, bhv) ->
- Format.fprintf fmt "behavior '%s' of statement %d%a"
- bhv.b_name s.sid
- (Pretty_utils.pp_list
- ~pre:" (for active behaviors " ~sep:"," Format.pp_print_string)
- (Datatype.String.Set.elements a)
- in Format.fprintf fmt ", %a, %a"
- pp_asked_prop config.asked_prop pp_assigns_mode config
-
-let cur_fct_default_bhv config = match config.cur_bhv with
- | FunBhv None -> true
- | FunBhv (Some bhv) -> bhv.b_name = Cil.default_behavior_name
- | _ -> false
-
-let filter_assign config pid =
- match config.assigns_filter, WpPropId.property_of_id pid with
- | NoAssigns, Property.IPAssigns _ -> false
- | (OnlyAssigns | WithAssigns), Property.IPAssigns _ -> true
- | OnlyAssigns, _ -> false
- | (NoAssigns | WithAssigns), _ -> true
-
-let filter_speconly config pid =
- if Cil2cfg.cfg_spec_only config.cfg then
- let open Property in
- match WpPropId.property_of_id pid with
- | IPPredicate {ip_kind = PKRequires _; ip_kinstr = Kglobal} -> true
- | _ -> false
- else true
-
-let filter_configstatus config pid =
- (match config.asked_prop with IdProp _ -> true | _ -> false) ||
- (WpPropId.filter_status pid)
-
-let filter_asked config pid =
- match config.asked_prop with
- | IdProp idp -> Property.equal (WpPropId.property_of_id pid) idp
- | CallPre (s_call, asked_pre) -> WpPropId.select_call_pre s_call asked_pre pid
- | NamedProp names -> WpPropId.select_by_name names pid
- | AllProps -> WpPropId.select_default pid
-
-let rec filter config pid = function
- | [] -> None
- | (f,name)::fs -> if f config pid then filter config pid fs else Some name
-
-let dkey = Wp_parameters.register_category "select"
-let goal_to_select config pid =
- let result =
- filter config pid [
- filter_assign , "assigns/non-assigns pass" ;
- filter_asked , "user selection" ;
- filter_configstatus , "proved status" ;
- filter_speconly , "no code and not main precondition" ;
- ] in
- match result with
- | None ->
- Wp_parameters.debug ~dkey "Goal '%a' selected" WpPropId.pp_propid pid ;
- true
- | Some f ->
- Wp_parameters.debug ~dkey "Goal '%a' skipped (%s)" WpPropId.pp_propid pid f ;
- false
-
-(*----------------------------------------------------------------------------*)
-(* Add properties *)
-
-(* TODO: still have to remove these fonctions... *)
-
-let kind_to_select config kind id = match kind with
- | WpStrategy.Agoal ->
- if goal_to_select config id then Some WpStrategy.Agoal else None
- | WpStrategy.Aboth goal ->
- let goal = goal && goal_to_select config id in
- Some (WpStrategy.Aboth goal)
- | WpStrategy.AcutB goal ->
- let goal = goal && goal_to_select config id in
- Some (WpStrategy.AcutB goal)
- | WpStrategy.AcallPre(goal,fct) ->
- let goal = goal && goal_to_select config id in
- Some (WpStrategy.AcallPre(goal,fct))
- | WpStrategy.AcallCheck(fct) ->
- if goal_to_select config id then Some (WpStrategy.AcallCheck fct)
- else None
- | WpStrategy.AcallPost _ ->
- if goal_to_select config id then Some kind else None
- | WpStrategy.Ahyp | WpStrategy.AcallHyp _ -> Some kind
-
-let add_prop_loop_inv ~established config acc kind s ca p =
- let id = WpPropId.mk_loop_inv_id ~established config.kf s ca in
- match kind_to_select config kind id with
- | None -> acc
- | Some kind -> WpStrategy.add_prop_loop_inv acc kind s id p
-
-let add_prop_inv_fixpoint config acc kind s ca p =
- let id = WpPropId.mk_inv_hyp_id config.kf s ca in
- match kind_to_select config kind id with
- | None -> acc
- | Some kind -> WpStrategy.add_prop_loop_inv acc kind s id p
-
-(*----------------------------------------------------------------------------*)
-(* Add Assigns *)
-
-let add_loop_assigns_goal config s (ca, assigns) acc =
- let id = WpPropId.mk_loop_assigns_id config.kf s ca assigns in
- match id with
- None -> acc
- | Some id ->
- if goal_to_select config id then
- let labels = NormAtLabels.labels_loop s in
- let assigns' = NormAtLabels.preproc_assigns labels assigns in
- let a_desc = WpPropId.mk_loop_assigns_desc s assigns' in
- WpStrategy.add_assigns acc WpStrategy.Agoal id a_desc
- else acc
-
-let add_stmt_assigns_goal config s active acc b l_post = match b.b_assigns with
- | WritesAny -> acc
- | Writes assigns ->
- let id = WpPropId.mk_stmt_assigns_id config.kf s active b assigns in
- match id with
- | None -> acc
- | Some id ->
- if goal_to_select config id then
- let kf = config.kf 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
- else acc
-
-let add_fct_assigns_goal config acc tkind b = match b.b_assigns with
- | WritesAny -> acc
- | Writes assigns ->
- 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 ~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
- else acc
-
-(* ------------------------------------------------------------------------ *)
-(* --- Get annotations according to the behavior --- *)
-(* ------------------------------------------------------------------------ *)
-
-(** find the behavior named [name] in the list *)
-let get_named_bhv name bhv_list =
- try Some (List.find (fun b -> b.b_name = name) bhv_list)
- with Not_found -> None
-
-(** Select in [bhv_list] the behavior that has to be processed
- * according to [config] and [ki] current statement. *)
-let get_behav config ki bh_list = match config.cur_bhv, ki with
- | FunBhv _, Kglobal ->
- get_named_bhv (name_of_asked_bhv config.cur_bhv) bh_list
- | StmtBhv (_, s1, _, b), Kstmt s2 when s1.sid = s2.sid ->
- get_named_bhv b.b_name bh_list
- | _ -> None
-
-(** Tells weather the property belonging to the behaviors in [bhv_name_list]
- * has to be considered according to [config]. *)
-type test_behav_res =
- | TBRno (* [cur_bhv] is not concerned *)
- | TBRhyp (* the property belongs to [default_behavior],
- but not to [cur_bhv] : it doesn't have to be a Goal
- but can be considered as an hypothesis. *)
- | TBRpart (* the property has to be taken as a Goal, but even if it is
- proved for every [asked_bhvs], it will still be a partial proof.
- TODO: use this to generate PKPartial ! *)
- | TBRok (* Select as a Goal *)
-
-(** (see [test_behav_res] above).
- * If the annotation doesn't have "for" names, it is a bit complicated because
- * we have to know if the statement [s] is inside a stmt behavior or not. *)
-let is_annot_for_config config ?(loopassigns=false) node s_annot bhv_name_list =
- let edges_before = Cil2cfg.pred_e config.cfg node in
- debug "[is_annot_for_config] at sid:%d for %a ? @."
- s_annot.sid (Wp_error.pp_string_list ~sep:" " ~empty:"<default>")
- bhv_name_list;
- let hyp_but_not_at_post n = (* don't take assert at post pgpt (see #564) *)
- let s_post = match Cil2cfg.get_post_edges config.cfg n with
- | [] -> None
- | e::_ -> Cil2cfg.get_edge_next_stmt config.cfg e
- in match s_post with
- | Some s_post when s_post.sid = s_annot.sid && not loopassigns -> TBRno
- | _ -> TBRhyp
- in
- let res = match bhv_name_list with
- | [] -> (* no spec 'for' in the property *)
- begin
- let e = match edges_before with
- | e::_ -> e
- | _ -> Wp_parameters.fatal "annot with no edge ?"
- in
- match config.cur_bhv with
- | FunBhv _ when cur_fct_default_bhv config ->
- begin
- try
- let _ = HdefAnnotBhv.find config.def_annots_info e in
- TBRhyp
- with Not_found -> TBRok
- end
- | StmtBhv (n, sb, _, b) when b.b_name = Cil.default_behavior_name ->
- begin
- try
- let s,_ = HdefAnnotBhv.find config.def_annots_info e in
- if s.sid = sb.sid then TBRok
- else raise Not_found
- with Not_found -> hyp_but_not_at_post n
- end
- | FunBhv _ -> TBRhyp
- | StmtBhv (n,_,_,_) -> hyp_but_not_at_post n
- end
- | bhvs -> (* TODOopt : there is surely a better way to do this : *)
- let asked_bhv = name_of_asked_bhv config.cur_bhv in
- let goal = List.exists (fun bl -> bl = asked_bhv) bhvs in
- if goal then
- let full = (* TODO *) true
- (* List.for_all (fun bl -> is_in bl config.asked_bhvs) bhvs *)
- in (if full then TBRok else TBRpart)
- else TBRno
- in debug "[is_annot_for_config] -> %s@."
- (match res with TBRok -> "ok" | TBRhyp -> "hyp" | TBRno -> "no"
- | TBRpart -> "part");
- res
-
-let add_fct_pre config acc spec =
- let kf = config.kf in
- let add_bhv_pre_hyp b acc =
- let kind = WpStrategy.Ahyp in
- WpStrategy.add_prop_fct_bhv_pre acc kind kf b
- in
- let add_def_pre_hyp acc =
- match Cil.find_default_behavior spec with
- | None -> acc
- | Some bdef -> add_bhv_pre_hyp bdef acc
- in
- let acc =
- if WpStrategy.is_main_init kf ||
- Wp_parameters.PrecondWeakening.get () then acc
- else let kind = WpStrategy.Ahyp in
- List.fold_left (fun acc bhv ->
- WpStrategy.add_prop_fct_pre_bhv acc kind kf bhv)
- acc spec.spec_behavior
- in
- let acc = match get_behav config Kglobal spec.spec_behavior with
- | None -> add_def_pre_hyp acc
- | Some b ->
- let acc =
- if not (Cil.is_default_behavior b) then add_def_pre_hyp acc else acc
- in
- let acc =
- if WpStrategy.is_main_init kf then
- let add_both acc p =
- let id = WpPropId.mk_pre_id kf Kglobal b p in
- let goal = goal_to_select config id in
- let kind = WpStrategy.Aboth goal in
- WpStrategy.add_prop_fct_pre acc kind kf b ~assumes:None p
- in
- let acc = List.fold_left add_both acc b.b_requires in
- let add_hyp acc p =
- let kind = WpStrategy.Ahyp in
- WpStrategy.add_prop_fct_pre acc kind kf b ~assumes:None p
- in List.fold_left add_hyp acc b.b_assumes
- else add_bhv_pre_hyp b acc
- in acc
- in
- let acc = match get_behav config Kglobal spec.spec_behavior with
- | Some bhv when Wp_parameters.SmokeTests.get () ->
- WpStrategy.add_prop_fct_smoke acc kf bhv
- | _ -> acc
- in
- acc
-
-
-let add_variant acc spec = (* TODO *)
- let _ = match spec.spec_variant with None -> ()
- | Some v ->
- Wp_parameters.warning ~once:true "Ignored 'decrease' specification:@, %a@."
- Printer.pp_decreases v
- in acc
-
-let add_terminates acc spec = (* TODO *)
- let _ = match spec.spec_terminates with None -> ()
- | Some p ->
- Wp_parameters.warning ~once:true "Ignored 'terminates' specification:@, %a@."
- Printer.pp_predicate
- (Logic_const.pred_of_id_pred p)
- in acc
-
-let add_disjoint_behaviors_props config ki active spec acc =
- match spec.spec_disjoint_behaviors with
- | [] -> acc
- | l ->
- let add_disj acc bhv_names =
- let kf = config.kf in
- let id = WpPropId.mk_disj_bhv_id (kf, ki, active, bhv_names) in
- if goal_to_select config id then
- begin
- let prop = Ast_info.disjoint_behaviors spec bhv_names in
- let labels = match ki with
- | Kglobal -> NormAtLabels.labels_fct_pre
- | Kstmt s -> NormAtLabels.labels_stmt_pre ~kf s in
- let prop = WpStrategy.normalize id labels prop in
- WpStrategy.add_prop acc WpStrategy.Agoal id prop
- end
- else acc
- in List.fold_left add_disj acc l
-
-let add_complete_behaviors_props config ki active spec acc =
- match spec.spec_complete_behaviors with
- | [] -> acc
- | l ->
- let mk_prop acc bhv_names =
- let kf = config.kf in
- let id = WpPropId.mk_compl_bhv_id (kf, ki, active, bhv_names) in
- if goal_to_select config id then
- let prop = Ast_info.complete_behaviors spec bhv_names in
- let labels = match ki with
- | Kglobal -> NormAtLabels.labels_fct_pre
- | Kstmt s -> NormAtLabels.labels_stmt_pre ~kf s in
- let prop = WpStrategy.normalize id labels prop in
- WpStrategy.add_prop acc WpStrategy.Agoal id prop
- else acc
- in List.fold_left mk_prop acc l
-
-let add_behaviors_props config ki active spec acc =
- let add = match config.cur_bhv, ki with
- | FunBhv _, Kglobal when cur_fct_default_bhv config -> true
- | StmtBhv (_, cur_s, cur_a, b), Kstmt s
- when (s.sid = cur_s.sid &&
- b.b_name = Cil.default_behavior_name &&
- Datatype.String.Set.(equal cur_a (of_list active)))
- -> true
- | _ -> false
- in
- if add then
- let acc = add_complete_behaviors_props config ki active spec acc in
- let acc = add_disjoint_behaviors_props config ki active spec acc in
- acc
- else acc
-
-(** Add the post condition of the whole spec as hypothesis.
- * Add [old(assumes) => ensures] for all the behaviors,
- * and also add an upper approximation of the merged assigns information. *)
-let add_stmt_spec_post_as_hyp config v s spec acc =
- let l_post = Cil2cfg.get_post_label config.cfg v in
- let add_bhv_post acc b =
- let assumes = Some (Ast_info.behavior_assumes b) in
- let add tk acc p =
- WpStrategy.add_prop_stmt_post acc WpStrategy.Ahyp config.kf
- s b tk l_post ~assumes p
- in
- let p_acc, e_acc =
- WpStrategy.fold_bhv_post_cond ~warn:false (add Normal) (add Exits) acc b
- in let p_acc =
- WpStrategy.add_stmt_spec_assigns_hyp p_acc config.kf s l_post spec in
- (* let e_acc = TODO, but crach at the moment... why ?
- * add_spec_assigns_hyp config ki l_post e_acc spec in *)
- p_acc, e_acc
- in List.fold_left add_bhv_post acc spec.spec_behavior
-
-(** we want to prove this behavior:
- * - add the requires as preconditions to both prove and use as hyp,
- * - add the assumes as hypotheses,
- * - add the postconditions as goals.
-*)
-let add_stmt_bhv_as_goal config v s active b (b_acc, (p_acc, e_acc)) =
- let l_post = Cil2cfg.get_post_label config.cfg v in
- let assumes = None in (* [assumes] are used as separate hypotheses *)
- let add_pre_hyp acc p =
- WpStrategy.add_prop_stmt_pre acc WpStrategy.Ahyp config.kf s b ~assumes p
- in
- let add_pre_goal acc p =
- let id = WpPropId.mk_pre_id config.kf (Kstmt s) b p in
- let goal = goal_to_select config id in
- let kind = WpStrategy.Aboth goal in
- WpStrategy.add_prop_stmt_pre acc kind config.kf s b ~assumes p
- in
- let add_post tk acc p =
- let id = WpPropId.mk_stmt_post_id config.kf s b (tk, p) in
- let goal = goal_to_select config id in
- let kind = WpStrategy.Aboth goal in
- WpStrategy.add_prop_stmt_post acc kind config.kf s b tk l_post ~assumes p
- in
-
- let b_acc = List.fold_left add_pre_goal b_acc b.b_requires in
- let b_acc = List.fold_left add_pre_hyp b_acc b.b_assumes in
-
- let p_acc, e_acc = WpStrategy.fold_bhv_post_cond ~warn:true
- (add_post Normal) (add_post Exits) (p_acc, e_acc) b
- in
- let p_acc = add_stmt_assigns_goal config s active p_acc b l_post in
- (*let e_acc = TODO, but crash at the moment... why ?
- add_stmt_assigns config s e_acc b l_post in *)
- b_acc, (p_acc, e_acc)
-
-let is_empty_behavior bhv =
- bhv.b_requires = [] &&
- bhv.b_assumes = [] &&
- bhv.b_post_cond = [] &&
- bhv.b_assigns = WritesAny &&
- bhv.b_allocation = FreeAllocAny
-
-let is_empty_spec s =
- s.spec_variant = None &&
- s.spec_terminates = None &&
- List.for_all is_empty_behavior s.spec_behavior
-
-let add_stmt_spec_annots
- config v s active spec ((b_acc, (p_acc, e_acc)) as acc)
- =
- if is_empty_spec spec then acc
- else
- let acc = add_variant acc spec in
- let acc = add_terminates acc spec in
- match config.cur_bhv with
- | StmtBhv (_n, cur_s, cur_a, b)
- when s.sid = cur_s.sid &&
- Datatype.String.Set.(equal cur_a (of_list active))
- ->
- (*
- begin match get_behav config (Kstmt s) spec.spec_behavior with
- | None -> (* in some cases, it seems that we can have several spec
- for the same statement -> not an error *) acc
- | Some b ->
- *)
- let b_acc, a_acc = add_stmt_bhv_as_goal config v s active b acc in
- let b_acc = add_behaviors_props config (Kstmt s) active spec b_acc in
- b_acc, a_acc
- | _ -> (* in all other cases, use the specification as hypothesis *)
- let kind = WpStrategy.Aboth false in
- let b_acc =
- WpStrategy.add_prop_stmt_spec_pre b_acc kind config.kf s spec
- in
- let p_acc, e_acc =
- add_stmt_spec_post_as_hyp config v s spec (p_acc, e_acc)
- in b_acc, (p_acc, e_acc)
-
-(*----------------------------------------------------------------------------*)
-(* Call annotations *)
-(*----------------------------------------------------------------------------*)
-
-let add_called_pre config called_kf s spec acc =
- let add_behav acc b = (* pre for behavior is [assumes => requires] *)
- let assumes = (Ast_info.behavior_assumes b) in
- let add_pre acc pre =
- let id = mk_call_pre_id called_kf b s pre in
- let kind = WpStrategy.AcallPre (goal_to_select config id,called_kf) in
- WpStrategy.add_prop_call_pre acc kind id ~assumes pre
- in List.fold_left add_pre acc b.b_requires
- in
- List.fold_left add_behav acc spec.spec_behavior
-
-let add_called_post called_kf termination_kind acc =
- let spec = Annotations.funspec called_kf in
- let add_behav acc b =
- (* post for behavior is [\old(assumes) => ensures] *)
- let kind = WpStrategy.AcallHyp called_kf in
- let assumes = (Ast_info.behavior_assumes b) in
- let add_post acc (tk, p) =
- if tk = termination_kind && use_predicate p.ip_content.tp_kind
- then WpStrategy.add_prop_call_post acc kind called_kf b tk ~assumes p
- else acc
- in List.fold_left add_post acc b.b_post_cond
- in
- List.fold_left add_behav acc spec.spec_behavior
-
-let add_call_checks config s kf posts exits =
- if cur_fct_default_bhv config
- && Wp_parameters.SmokeTests.get ()
- && Wp_parameters.SmokeDeadcall.get ()
- then
- WpStrategy.add_prop_dead_call kf s posts exits
- else
- posts , exits
-
-let add_call_annots config s kf l_post (before,(posts,exits)) =
- let spec = Annotations.funspec kf in
- let before = add_called_pre config kf s spec before in
- let posts = add_called_post kf Normal posts in
- let posts = WpStrategy.add_call_assigns_hyp posts config.kf s
- ~called_kf:kf l_post (Some spec) in
- let exits = add_called_post kf Exits exits in
- before , add_call_checks config s kf posts exits
-
-let get_call_annots config v s fct =
- let l_post = Cil2cfg.get_post_label config.cfg v in
- let empty = let e = WpStrategy.empty_acc in e,(e,e) in
- match fct with
-
- | Cil2cfg.Static kf -> add_call_annots config s kf l_post empty
-
- | Cil2cfg.Dynamic _ ->
- let bhv = asked_bhv config.cur_bhv in
- match Dyncall.get ?bhv s with
- | None | Some(_,[]) ->
- Wp_parameters.warning ~once:true ~source:(fst (Stmt.loc s))
- "Missing 'calls' for %s"
- (match bhv with
- | None -> "default behavior"
- | Some b -> b) ;
- let annots = WpStrategy.add_call_assigns_any WpStrategy.empty_acc s in
- WpStrategy.empty_acc, (annots , annots)
- | Some(_,calls) ->
- List.fold_left
- (fun acc kf -> add_call_annots config s kf l_post acc)
- empty calls
-
-(*----------------------------------------------------------------------------*)
-
-let add_variant_annot config s ca var_exp loop_entry loop_back =
- let (vpos_id, vpos), (vdecr_id, vdecr) =
- WpStrategy.mk_variant_properties config.kf s ca var_exp
- in
- let add_variant acc kind id p =
- WpStrategy.add_prop_loop_inv acc kind s id p
- in
- let add_hyp acc =
- let acc = add_variant acc WpStrategy.Ahyp vdecr_id vdecr in
- add_variant acc WpStrategy.Ahyp vpos_id vpos
- in
- let add_goal acc =
- let acc =
- if goal_to_select config vdecr_id then
- add_variant acc WpStrategy.Agoal vdecr_id vdecr
- else acc
- in if goal_to_select config vpos_id then
- add_variant acc WpStrategy.Agoal vpos_id vpos
- else acc
- in
- let loop_back =
- if cur_fct_default_bhv config then add_goal loop_back else add_hyp loop_back
- (*TODO: what about variant establishment ??? It seems that [0<v)] is not
- * proved by induction anymore. Why ? *)
- in loop_entry, loop_back
-
-let add_loop_invariant_annot config vloop s ca b_list inv acc =
- let hyp = use_predicate inv.tp_kind in
- let goal = verify_predicate inv.tp_kind in
- let inv = inv.tp_statement in
- let assigns, loop_entry, loop_back , loop_core = acc in
- (* we have to prove that inv is true for each edge that goes
- * in the loop, so we can assume that inv is true for each edge
- * starting from this point. *)
- match is_annot_for_config config vloop s b_list with
- | TBRok
- | TBRpart (* TODO: PKPartial *)
- ->
- begin
- let loop_entry =
- if goal then
- add_prop_loop_inv ~established:true config loop_entry
- WpStrategy.Agoal s ca inv
- else loop_entry in
- let loop_back =
- if goal then
- add_prop_loop_inv ~established:false config loop_back
- WpStrategy.Agoal s ca inv
- else loop_back in
- let loop_core =
- if hyp then
- add_prop_inv_fixpoint config loop_core WpStrategy.Ahyp s ca inv
- else loop_core in
- assigns, loop_entry , loop_back , loop_core
- end
- | TBRhyp ->
- if hyp then
- let kind = WpStrategy.Ahyp in
- let loop_core = add_prop_inv_fixpoint config loop_core kind s ca inv
- in assigns, loop_entry , loop_back , loop_core
- else acc
- | TBRno -> acc
-
-(** Returns the annotations for the three edges of the loop node:
- * - loop_entry : goals for the edge entering in the loop
- * - loop_back : goals for the edge looping to the entry point
- * - loop_core : fix-point hypothesis for the edge starting the loop core
-*)
-let get_loop_annots config vloop s =
- let do_annot _ a (assigns, loop_entry, loop_back , loop_core as acc) =
- match a.annot_content with
- | AInvariant (b_list, true, inv) ->
- add_loop_invariant_annot config vloop s a b_list inv acc
- | AVariant (var_exp, None) ->
- let loop_entry, loop_back =
- add_variant_annot config s a var_exp loop_entry loop_back
- in assigns, loop_entry , loop_back , loop_core
- | AVariant (_v, _rel) ->
- Wp_parameters.warning ~once:true "Ignored 'loop variant' specification with measure : %a"
- Printer.pp_code_annotation a;
- acc
- | AAssigns (_,WritesAny) -> assert false
- | AAssigns (b_list, Writes w) -> (* loop assigns *)
- let h_assigns, g_assigns = assigns in
- let check_assigns old cur =
- match old with
- None -> Some cur
- | Some _ ->
- Wp_parameters.fatal
- "At most one loop assigns can be associated to a behavior"
- in
- let assigns =
- match is_annot_for_config config ~loopassigns:true vloop s b_list with
- | TBRok | TBRpart ->
- check_assigns h_assigns (a,w),
- check_assigns g_assigns (a,w)
- | TBRhyp ->
- check_assigns h_assigns (a,w), g_assigns
- | TBRno -> assigns
- in (assigns, loop_entry , loop_back , loop_core)
- | _ -> acc (* see get_stmt_annots *)
- in
- let loop_core =
- if cur_fct_default_bhv config
- && Wp_parameters.SmokeTests.get ()
- && Wp_parameters.SmokeDeadloop.get ()
- && not (WpReached.is_dead_code s)
- then WpStrategy.add_prop_dead_loop WpStrategy.empty_acc config.kf s
- else WpStrategy.empty_acc in
- let (h_assigns, g_assigns), loop_entry , loop_back , loop_core =
- Annotations.fold_code_annot do_annot s
- ((None,None), WpStrategy.empty_acc, WpStrategy.empty_acc, loop_core)
- in
- let loop_back = match g_assigns with
- | None -> loop_back
- | Some a -> add_loop_assigns_goal config s a loop_back
- in
- let loop_core =
- WpStrategy.add_loop_assigns_hyp loop_core config.kf s h_assigns
- in (loop_entry , loop_back , loop_core)
-
-let add_stmt_deadcode_smoke config acc s =
- if cur_fct_default_bhv config
- then
- match config.reachability with
- | Some r when WpReached.smoking r s ->
- WpStrategy.add_prop_dead_code acc config.kf s
- | _ -> acc
- else
- acc
-
-let get_stmt_annots config v s =
- let do_annot _ a ((b_acc, (a_acc, e_acc)) as acc) =
- match a.annot_content with
- | AInvariant (_blist, loop_inv, _inv) ->
- if loop_inv then (* see get_loop_annots *) acc
- else
- begin
- Wp_parameters.warning ~once:true
- "Unsupported generalized invariant, use loop invariant instead.\n\
- Ignored invariant @[<hov 2>%a@]"
- Printer.pp_code_annotation a;
- acc
- end
- | AAssert (b_list, p) ->
- let kf = config.kf in
- let acc = match is_annot_for_config config v s b_list with
- | TBRno -> acc
- | TBRhyp ->
- if use_predicate p.tp_kind then
- let b_acc =
- WpStrategy.add_prop_assert
- b_acc WpStrategy.Ahyp kf s a p.tp_statement
- in (b_acc, (a_acc, e_acc))
- else acc
- | TBRok | TBRpart ->
- let id = WpPropId.mk_assert_id config.kf s a in
- let goal = goal_to_select config id in
- let add, kind =
- match p.tp_kind with
- | Admit -> true, WpStrategy.Ahyp
- | Assert -> true, Aboth goal
- | Check -> goal, Agoal
- in if add then
- let b_acc =
- WpStrategy.add_prop_assert b_acc kind kf s a p.tp_statement
- in (b_acc, (a_acc, e_acc))
- else acc
- in acc
- | AAllocation (_b_list, _frees_allocates) ->
- (* [PB] TODO *) acc
- | AAssigns (_b_list, _assigns) ->
- (* loop assigns: see get_loop_annots *) acc
- | AVariant (_v, _rel) -> (* see get_loop_annots *) acc
- | APragma _ -> acc
- | AStmtSpec (b_list, spec) ->
- if b_list <> [] then (* TODO ! *)
- Wp_parameters.warning ~once:true
- "Ignored specification 'for %a' (generalize to all behavior)"
- (Pretty_utils.pp_list ~sep:", " Format.pp_print_string)
- b_list;
- add_stmt_spec_annots config v s b_list spec acc
- | AExtended _ -> acc
- in
- let before_acc =
- add_stmt_deadcode_smoke config WpStrategy.empty_acc s in
- let after_acc = WpStrategy.empty_acc in
- let exits_acc = WpStrategy.empty_acc in
- let acc = before_acc, (after_acc, exits_acc) in
- Annotations.fold_code_annot do_annot s acc
-
-let get_fct_pre_annots config spec =
- let acc = WpStrategy.empty_acc in
- let acc = add_fct_pre config acc spec in
- let acc = add_behaviors_props config Kglobal [] spec acc in
- let acc = add_variant acc spec in
- let acc = add_terminates acc spec in
- acc
-
-let get_fct_post_annots config tkind spec =
- let acc = WpStrategy.empty_acc in
- match get_behav config Kglobal spec.spec_behavior with
- | None -> acc
- | Some b ->
- (* add the postconditions *)
- let f_nothing () _ = () in
- let add tk acc p =
- let id = WpPropId.mk_fct_post_id config.kf b (tk, p) in
- if goal_to_select config id then
- WpStrategy.add_prop_fct_post acc WpStrategy.Agoal config.kf b tk p
- else acc
- in
- let acc = match tkind with
- | Normal ->
- let acc, _ =
- WpStrategy.fold_bhv_post_cond ~warn:true (add Normal) f_nothing (acc, ()) b
- in acc
- | Exits ->
- let _, acc =
- WpStrategy.fold_bhv_post_cond ~warn:false f_nothing (add Exits) ((), acc) b
- in acc
- | _ -> assert false
- in (* also add the [assigns] *)
- let acc =
- if Kernel_function.is_definition config.kf
- then add_fct_assigns_goal config acc tkind b
- else WpStrategy.add_fct_bhv_assigns_hyp acc config.kf tkind b
- in acc
-
-(*----------------------------------------------------------------------------*)
-(* Build graph annotation for the strategy *)
-(*----------------------------------------------------------------------------*)
-
-(** Builds tables that give hypotheses and goals relative to [b] behavior
- * for edges of the cfg to consider during wp computation.
- * [b = None] means that we only consider internal properties to select for the
- * default behavior. This is useful when the function doesn't have any
- * specification.
- * @param asked_prop = Some id -> select only this goal (use all hyps).
-*)
-let get_behavior_annots config =
- debug "build strategy for %a@." pp_strategy_info config;
- let cfg = config.cfg in
- let spec = Annotations.funspec config.kf in
- let annots = WpStrategy.create_tbl () in
-
- let get_node_annot v =
- debug "get_node_annot for node %a" Cil2cfg.pp_node v;
- match Cil2cfg.node_type v with
- | Cil2cfg.Vstart | Cil2cfg.Vend -> ()
-
- | Cil2cfg.VfctIn ->
- let pre = get_fct_pre_annots config spec in
- WpStrategy.add_on_edges annots pre (Cil2cfg.succ_e cfg v)
-
- | Cil2cfg.VfctOut ->
- let post = get_fct_post_annots config Normal spec in
- WpStrategy.add_on_edges annots post (Cil2cfg.succ_e cfg v)
-
- | Cil2cfg.VfctErr ->
- let post = get_fct_post_annots config Exits spec in
- WpStrategy.add_on_edges annots post (Cil2cfg.succ_e cfg v)
-
- | Cil2cfg.VblkIn (Cil2cfg.Bstmt s, _)
- | Cil2cfg.Vstmt s
- | Cil2cfg.Vswitch (s,_) | Cil2cfg.Vtest (true, s, _)
- ->
- let stmt_annots = get_stmt_annots config v s in
- WpStrategy.add_node_annots annots cfg v stmt_annots
-
- | Cil2cfg.Vcall (s,_,fct,_) ->
- let stmt_annots = get_stmt_annots config v s in
- WpStrategy.add_node_annots annots cfg v stmt_annots;
- let call_annots = get_call_annots config v s fct in
- WpStrategy.add_node_annots annots cfg v call_annots
-
- | Cil2cfg.Vloop (_, s) ->
- let stmt_annots = get_stmt_annots config v s in
- let before, _after = stmt_annots in
- (* TODO: what about after ? *)
- WpStrategy.add_loop_annots annots cfg v ~entry:before
- ~back:WpStrategy.empty_acc ~core:WpStrategy.empty_acc;
- debug "add_loop_annots stmt ok";
- let (entry , back , core) = get_loop_annots config v s in
- debug "get_loop_annots ok";
- WpStrategy.add_loop_annots annots cfg v ~entry ~back ~core
-
- | Cil2cfg.Vloop2 _ -> (* nothing to do *) ()
- | Cil2cfg.VblkIn (_, _) | Cil2cfg.VblkOut (_, _) -> (* nothing *) ()
- | Cil2cfg.Vtest (false, _s, _) -> (* done in Cil2cfg.Vtest (true) *) ()
- in
- Cil2cfg.iter_nodes get_node_annot cfg;
- annots
-
-(* ------------------------------------------------------------------------ *)
-(* --- Global Properties --- *)
-(* ------------------------------------------------------------------------ *)
-
-module GS = Cil_datatype.Global_annotation.Set
-
-let add_global_annotations annots =
- let rec do_global g =
- let (source,_) = Cil_datatype.Global_annotation.loc g in
- match g with
- | Daxiomatic (_ax_name, globs,_,_) -> do_globals globs
- | Dvolatile _ ->
- (* nothing to do *) ()
- | Dfun_or_pred _ ->
- (* will be processed while translation is needed *) ()
- | Dtype _ ->
- (* will be processed while translation is needed *) ()
- | Dtype_annot (linfo,_) ->
- Wp_parameters.warning ~source ~once:true
- "Type invariant not handled yet ('%s' ignored)"
- linfo.l_var_info.lv_name;
- ()
- | Dmodel_annot (mf,_) ->
- Wp_parameters.warning ~source ~once:true
- "Model fields not handled yet (model field '%s' ignored)"
- mf.mi_name;
- ()
- | Dcustom_annot (_c,_n,_,_) ->
- Wp_parameters.warning ~source ~once:true
- "Custom annotation not handled (ignored)";
- ()
- | Dextended _ -> ()
- (* nothing to do. It's the job of the extension's owner
- to generate the appropriate standard annotations. *)
- | Dinvariant (linfo,_) ->
- Wp_parameters.warning ~source ~once:true
- "Global invariant not handled yet ('%s' ignored)"
- linfo.l_var_info.lv_name;
- ()
- | Dlemma (name,_,_,p,_,_) ->
- if use_predicate p.tp_kind then
- WpStrategy.add_axiom annots (LogicUsage.logic_lemma name)
-
- and do_globals gs = List.iter do_global gs in
- (*[LC]: forcing order of iteration: hash is not the same on 32 and 64 bits *)
- let pool = ref GS.empty in
- Annotations.iter_global (fun _ g -> pool := GS.add g !pool);
- GS.iter do_global !pool;
- annots
-
-(* ------------------------------------------------------------------------ *)
-(* --- Main functions to build the strategies --- *)
-(* ------------------------------------------------------------------------ *)
-
-let string_of_active active =
- Format.asprintf "%a"
- (Pretty_utils.pp_list (fun fmt s -> Format.fprintf fmt "_%s" s))
- (Datatype.String.Set.elements active)
-
-let behavior_name_of_config config =
- match config.cur_bhv with
- | FunBhv None -> None
- | FunBhv (Some b) when b.b_name = Cil.default_behavior_name -> None
- | FunBhv (Some b) -> Some b.b_name
- | StmtBhv (_, s, active, b) when b.b_name = Cil.default_behavior_name ->
- Some(
- "default_for_stmt_"^(string_of_int s.sid)^(string_of_active active))
- (*TODO better name ?*)
- | StmtBhv (_, s, active, b) ->
- Some (b.b_name^"_stmt_"^(string_of_int s.sid)^(string_of_active active))
-
-let build_bhv_strategy config =
- let annots = get_behavior_annots config in
- let annots = add_global_annotations annots in
- let desc = Format.asprintf "%a" pp_strategy_info config in
- WpStrategy.mk_strategy desc config.cfg (behavior_name_of_config config)
- WpStrategy.SKannots annots
-
-(* Visit the CFG to find all the internal statement specifications.
- * (see [HdefAnnotBhv] documentation for information about this table).
-*)
-let internal_function_behaviors cfg =
- let def_annot_bhv = HdefAnnotBhv.create 42 in
- let get_stmt_bhv node stmt acc =
- let add_bhv_info active acc b =
- if is_empty_behavior b then acc else
- begin
- if b.b_name = Cil.default_behavior_name then
- begin
- let _, int_edges = Cil2cfg.get_internal_edges cfg node in
- let n = Cil2cfg.Eset.cardinal int_edges in
- let reg e =
- try
- let (_old_s, old_n) = HdefAnnotBhv.find def_annot_bhv e in
- if n < old_n then
- (* new spec is included in the old one : override. *)
- raise Not_found
- with Not_found ->
- HdefAnnotBhv.replace def_annot_bhv e (stmt, n)
- in
- Cil2cfg.Eset.iter reg int_edges
- end;
- (node, stmt, active, b)::acc
- end
- in
- let spec_bhv_names acc annot = match annot with
- | {annot_content = AStmtSpec (active, spec)} ->
- List.fold_left (add_bhv_info active) acc spec.spec_behavior
- | _ -> Wp_parameters.fatal "filter on is_contract didn't work ?"
- in
- let annots = Annotations.code_annot ~filter:Logic_utils.is_contract stmt in
- List.fold_left spec_bhv_names acc annots
- in
- let get_bhv n ((seen_stmts, bhvs) as l) =
- match Cil2cfg.start_stmt_of_node n with None -> l
- | Some s ->
- if List.mem s.sid seen_stmts then l
- else
- let seen_stmts = s.sid::seen_stmts in
- let bhvs = get_stmt_bhv n s bhvs in
- (seen_stmts, bhvs)
- in
- let _, bhvs = Cil2cfg.fold_nodes get_bhv cfg ([], []) in
- bhvs, def_annot_bhv
-
-
-(** empty [bhv_names] means all (whatever [ki] is) *)
-let find_behaviors kf cfg ki bhv_names =
- let f_bhvs = Annotations.behaviors kf in
- let s_bhvs, def_annot_bhv = internal_function_behaviors cfg in
-
- let add_fct_bhv (def, acc) b =
- let add () =
- let def = if Cil.is_default_behavior b then true else def in
- def, (FunBhv (Some b))::acc
- in
- if bhv_names = [] then add()
- else match ki with
- | None (* not specified ki *) | Some Kglobal ->
- if List.mem b.b_name bhv_names then add () else (def, acc)
- | Some Kstmt _ -> def, acc
- in
-
- let add_stmt_bhv acc (n,s,active,b) =
- let active = Datatype.String.Set.of_list active in
- if bhv_names = [] then (StmtBhv (n,s,active,b))::acc
- else if List.mem b.b_name bhv_names then
- let acc = match ki with
- | None -> (* not specified ki *) (StmtBhv (n, s, active, b))::acc
- | Some (Kstmt stmt) when stmt.sid = s.sid ->
- (StmtBhv (n, s, active, b))::acc
- | _ -> (* specified ki but not this one *) acc
- in acc
- else acc
- in
-
- let f_bhvs = List.rev f_bhvs in (* for compatibility with previous version *)
- let def, bhvs = List.fold_left add_fct_bhv (false, []) f_bhvs in
- let bhvs = List.fold_left add_stmt_bhv bhvs s_bhvs in
- let bhvs =
- if def then (* fct default behavior already in *) bhvs
- else if bhv_names = [] then (FunBhv None)::bhvs
- else match ki with
- | None (* not specified ki *) | Some Kglobal ->
- if List.mem Cil.default_behavior_name bhv_names
- then (FunBhv None)::bhvs
- else bhvs
- | Some Kstmt _ -> bhvs
- in def_annot_bhv, bhvs
-
-(*----------------------------------------------------------------------------*)
-(* Unreachable *)
-(*----------------------------------------------------------------------------*)
-
-class vexit kf acc =
- object
- inherit Visitor.frama_c_inplace
- val mutable ips = acc
- method acc = ips
- method! vstmt_aux stmt =
- Annotations.iter_code_annot
- (fun _e ca ->
- match ca.annot_content with
- | AStmtSpec(_,spec) ->
- List.iter
- (fun bhv ->
- List.iter
- (fun post ->
- if fst post = Exits then
- let ip = WpPropId.mk_stmt_post_id kf stmt bhv post in
- ips <- ip :: ips
- ) bhv.b_post_cond
- ) spec.spec_behavior
- | _ -> ()
- ) stmt ;
- Cil.DoChildren
- end
-
-let process_unreached_annots cfg reachability =
- debug "collecting unreachable annotations@.";
- let unreached = Cil2cfg.unreachable_nodes cfg in
- let kf = Cil2cfg.cfg_kf cfg in
- let spec = Annotations.funspec kf in
- let add_id acc id =
- 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) =
- if tk = termk then add_id acc (WpPropId.mk_fct_post_id kf b p) else acc
- in
- let do_bhv termk acc b = List.fold_left (do_post b termk) acc b.b_post_cond in
- let do_annot s _ a acc =
- List.fold_left add_id acc (WpPropId.mk_code_annot_ids kf s a)
- in
- let do_stmt s acc =
- let acc =
- match reachability with
- | None -> acc
- | Some r ->
- if WpReached.smoking r s then
- WpPropId.mk_smoke kf ~id:"unreachable" ~unreachable:s () :: acc
- else acc
- in Annotations.fold_code_annot (do_annot s) s acc
- in
- let do_node acc n =
- debug
- "process annotations of unreachable node %a@."
- Cil2cfg.pp_node_type n;
- match n with
- | Cil2cfg.Vstart -> Wp_parameters.fatal "Start must be reachable"
- | Cil2cfg.VfctIn -> Wp_parameters.fatal "FctIn must be reachable"
- | Cil2cfg.VfctOut -> List.fold_left (do_bhv Normal) acc spec.spec_behavior
- | Cil2cfg.VfctErr ->
- let acc = List.fold_left (do_bhv Exits) acc spec.spec_behavior in
- let visitor = new vexit kf acc in
- ignore Visitor.(visitFramacKf (visitor :> frama_c_visitor) kf) ;
- visitor#acc
- | Cil2cfg.Vcall (s, _, call, _) ->
- do_stmt s acc @
- preconditions_at_call s call
- | Cil2cfg.Vstmt s
- | Cil2cfg.VblkIn (Cil2cfg.Bstmt s, _)
- | Cil2cfg.VblkOut (Cil2cfg.Bstmt s, _)
- | Cil2cfg.Vtest (true, s, _) | Cil2cfg.Vloop (_, s) | Cil2cfg.Vswitch (s,_)
- -> do_stmt s acc
- | Cil2cfg.Vtest (false, _, _) | Cil2cfg.Vloop2 _
- | Cil2cfg.VblkIn _ | Cil2cfg.VblkOut _ | Cil2cfg.Vend -> acc
- in
- let annots = List.fold_left do_node [] unreached in
- debug "found %d unreachable annotations@." (List.length annots) ;
- List.iter (fun pid -> set_unreachable pid) annots
-
-(*----------------------------------------------------------------------------*)
-(* Everything must go through here. *)
-(*----------------------------------------------------------------------------*)
-
-let build_configs assigns kf model behaviors ki property =
- debug "[get_strategies] for behaviors names: %a@."
- (Wp_error.pp_string_list ~sep:" " ~empty:"<none>")
- (match behaviors with [] -> ["<all>"] | _ :: _ as l -> l) ;
- let _ = match ki with
- | None -> ()
- | Some Kglobal ->
- debug
- "[get_strategies] select in function properties@."
- | Some (Kstmt s) ->
- debug
- "[get_strategies] select stmt %d properties@." s.sid
- in
- if Wp_parameters.RTE.get () then WpRTE.generate model kf ;
- let cfg = Cil2cfg.get kf in
- let reachability =
- if Wp_parameters.SmokeTests.get ()
- && Wp_parameters.SmokeDeadcode.get ()
- then Some (WpReached.reachability kf)
- else None in
- process_unreached_annots cfg reachability ;
- let def_annot_bhv, bhvs = find_behaviors kf cfg ki behaviors in
- if bhvs <> [] then debug "[get_strategies] %d behaviors" (List.length bhvs);
- let mk_bhv_config bhv = {
- kf; reachability; cfg;
- cur_bhv = bhv;
- asked_prop = property;
- assigns_filter = assigns;
- def_annots_info = def_annot_bhv;
- } in List.map mk_bhv_config bhvs
-
-let get_strategies assigns kf model behaviors ki property =
- let configs = build_configs assigns kf model behaviors ki property in
- let rec add_stgs l = match l with [] -> [] | config::tl ->
- let stg = build_bhv_strategy config in
- stg::(add_stgs tl)
- in add_stgs configs
-
-(*----------------------------------------------------------------------------*)
-(* Public functions to build the strategies *)
-(*----------------------------------------------------------------------------*)
-
-let get_precond_strategies ~model p =
- debug "[get_precond_strategies] %s@."
- (Property.Names.get_prop_name_id p);
- let open Property in
- match p with
- | IPPredicate {ip_kind = PKRequires b; ip_kf; ip_kinstr = Kglobal} ->
- let strategies =
- if WpStrategy.is_main_init ip_kf then
- get_strategies NoAssigns ip_kf model [b.b_name] None (IdProp p)
- else []
- in
- let call_sites = Kernel_function.find_syntactic_callsites ip_kf in
- let add_call_pre_strategy acc (kf_caller, stmt) =
- let asked = CallPre (stmt, Some p) in
- get_strategies NoAssigns kf_caller model [] None asked @ acc
- in
- if call_sites = [] then
- (Wp_parameters.warning ~once:true
- "No direct call sites for function '%a': cannot check pre-conditions"
- Kernel_function.pretty ip_kf;
- strategies)
- else List.fold_left add_call_pre_strategy strategies call_sites
- | _ ->
- invalid_arg "[get_precond_strategies] not a function precondition"
-
-let get_call_pre_strategies ~model stmt =
- debug
- "[get_call_pre_strategies] on statement %a@." Stmt.pretty_sid stmt;
- match stmt.skind with
- | Instr(Call(_,f,_,_)) ->
- let strategies = match Kernel_function.get_called f with
- | None ->
- Wp_parameters.warning
- "Call through function pointer not implemented yet: \
- cannot check pre-conditions for statement %a"
- Stmt.pretty_sid stmt;
- []
- | Some _kf_called ->
- let kf_caller = Kernel_function.find_englobing_kf stmt in
- let asked = CallPre (stmt, None) in
- get_strategies NoAssigns kf_caller model [] None asked
- in strategies
- | Instr(Local_init(_, ConsInit _, _)) ->
- let kf_caller = Kernel_function.find_englobing_kf stmt in
- let asked = CallPre(stmt, None) in
- get_strategies NoAssigns kf_caller model [] None asked
- | _ -> Wp_parameters.warning
- "[get_call_pre_strategies] this is not a call statement"; []
-
-let get_id_prop_strategies ~model ?(assigns=WithAssigns) p =
- debug "[get_id_prop_strategies] %s@."
- (Property.Names.get_prop_name_id p);
- let open Property in match p with
- | IPCodeAnnot {ica_kf; ica_ca} ->
- let bhvs = match ica_ca.annot_content with
- | AAssert (l, _) | AInvariant (l, _, _) | AAssigns (l, _) -> l
- | _ -> []
- in get_strategies assigns ica_kf model bhvs None (IdProp p)
- | IPAssigns {ias_kf = kf; ias_bhv = Id_loop _}
- (*loop assigns: belongs to the default behavior *)
- | IPDecrease {id_kf = kf} ->
- (* any variant property is attached to the default behavior of
- * the function, NOT to a statement behavior *)
- let bhvs = [ Cil.default_behavior_name ] in
- get_strategies assigns kf model bhvs None (IdProp p)
- | IPPredicate {ip_kind = PKRequires _; ip_kinstr = Kglobal} ->
- get_precond_strategies model p
- | _ ->
- let strategies = match get_kf p with
- | None -> Wp_parameters.warning
- "WP of property outside functions: ignore %s"
- (Property.Names.get_prop_name_id p); []
- | Some kf ->
- let ki = Some (get_kinstr p) in
- let bhv = match get_behavior p with
- | None -> Cil.default_behavior_name
- | Some fb -> fb.b_name
- in get_strategies assigns kf model [bhv] ki (IdProp p)
- in strategies
-
-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
deleted file mode 100644
index a2b4ebcf85106f1964d12a6273f8296d4ced158e..0000000000000000000000000000000000000000
--- a/src/plugins/wp/wpAnnot.mli
+++ /dev/null
@@ -1,57 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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
-
-(** Every access to annotations have to go through here,
- * so this is the place where we decide what the computation
- * is allowed to use. *)
-
-(* ########################################################################## *)
-(* ### WARNING: DEPRECATED API ### *)
-(* ########################################################################## *)
-
-(*----------------------------------------------------------------------------*)
-
-val unreachable_proved : int ref
-val unreachable_failed : int ref
-val trivial_terminates : int ref
-val set_unreachable : WpPropId.prop_id -> unit
-val set_trivially_terminates : WpPropId.prop_id -> Property.Set.t -> unit
-
-type asked_assigns = NoAssigns | OnlyAssigns | WithAssigns
-
-val get_call_pre_strategies :
- model:WpContext.model ->
- stmt -> WpStrategy.strategy list
-
-val get_function_strategies :
- model:WpContext.model ->
- ?assigns:asked_assigns ->
- ?bhv:string list ->
- ?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/wpGenerator.ml b/src/plugins/wp/wpGenerator.ml
deleted file mode 100644
index 92b9414af253bb28460e95656fb13517a7b16d8c..0000000000000000000000000000000000000000
--- a/src/plugins/wp/wpGenerator.ml
+++ /dev/null
@@ -1,237 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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 () ->
- LogicUsage.iter_lemmas
- (fun (l : LogicUsage.logic_lemma) ->
- if Logic_utils.use_predicate l.lem_predicate.tp_kind
- then VCG.register_lemma l) ;
- 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
deleted file mode 100644
index a2e0cec5c9cfec7b86469cca946fa0b15f2ab38d..0000000000000000000000000000000000000000
--- a/src/plugins/wp/wpGenerator.mli
+++ /dev/null
@@ -1,53 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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/wpReached.ml b/src/plugins/wp/wpReached.ml
index fa15b385d0ef17ea8666aa2e1fc8b969b6d1867b..ec9fb07b03b9cf03eeed070b87f8bcda4ccef40d 100644
--- a/src/plugins/wp/wpReached.ml
+++ b/src/plugins/wp/wpReached.ml
@@ -377,3 +377,52 @@ let set_doomed emitter pid =
| Property.OLGlob _ | Property.OLContract _ -> ()
(* -------------------------------------------------------------------------- *)
+(* --- Status of Unreachable Annotations --- *)
+(* -------------------------------------------------------------------------- *)
+
+let dkey = Wp_parameters.register_category "reach" (* debugging key *)
+let debug fmt = Wp_parameters.debug ~dkey fmt
+
+let unreachable_proved = ref 0
+let unreachable_failed = ref 0
+
+let wp_unreachable =
+ Emitter.create
+ "Unreachable Annotations"
+ [ Emitter.Property_status ]
+ ~correctness:[] (* TBC *)
+ ~tuning:[] (* TBC *)
+
+let set_unreachable pid =
+ if WpPropId.is_smoke_test pid then
+ begin
+ let source = WpPropId.source_of_id pid in
+ set_doomed wp_unreachable pid ;
+ incr unreachable_failed ;
+ Wp_parameters.warning ~source "Failed smoke-test"
+ end
+ else
+ let open Property in
+ let emit = function
+ | IPPredicate {ip_kind = PKAssumes _} -> ()
+ | p ->
+ debug "unreachable annotation %a@." Property.pretty p;
+ Property_status.emit wp_unreachable ~hyps:[] p Property_status.True
+ in
+ let pids = match WpPropId.property_of_id pid with
+ | IPPredicate {ip_kind = PKAssumes _} -> []
+ | IPBehavior {ib_kf; ib_kinstr; ib_active; ib_bhv} ->
+ let active = Datatype.String.Set.elements ib_active in
+ (ip_post_cond_of_behavior ib_kf ib_kinstr active ib_bhv) @
+ (ip_requires_of_behavior ib_kf ib_kinstr ib_bhv)
+ | IPExtended _ -> []
+ (* Extended clauses might concern anything. Don't validate them
+ unless we know exactly what is going on. *)
+ | p ->
+ incr unreachable_proved ;
+ Wp_parameters.result "[CFG] Goal %a : Valid (Unreachable)"
+ WpPropId.pp_propid pid ; [p]
+ in
+ List.iter emit pids
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpReached.mli b/src/plugins/wp/wpReached.mli
index 77a7bfa2297a43d2bb32e73a1ce849d905ef8905..68b6bd23f8b80fb1a2729792fae599bae8002f19 100644
--- a/src/plugins/wp/wpReached.mli
+++ b/src/plugins/wp/wpReached.mli
@@ -51,4 +51,9 @@ val dump : dir:Datatype.Filepath.t -> Kernel_function.t -> reachability -> unit
val set_doomed : Emitter.t -> WpPropId.prop_id -> unit
+val unreachable_proved : int ref
+val unreachable_failed : int ref
+
+val set_unreachable : WpPropId.prop_id -> unit
+
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpStrategy.ml b/src/plugins/wp/wpStrategy.ml
deleted file mode 100644
index b4a4080208a94c700335156e1bf9ff75c49dee55..0000000000000000000000000000000000000000
--- a/src/plugins/wp/wpStrategy.ml
+++ /dev/null
@@ -1,772 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-let dkey = Wp_parameters.register_category "strategy" (* debugging key *)
-let debug fmt = Wp_parameters.debug ~dkey fmt
-
-open Cil_types
-open Logic_utils
-open LogicUsage
-
-(* -------------------------------------------------------------------------- *)
-(** An annotation can be used for different purpose. *)
-type annot_kind =
- | Ahyp (* annotation is an hypothesis,
- but not a goal (see Aboth) : A => ...*)
- | Agoal (* annotation is a goal,
- but not an hypothesis (see Aboth): A /\ ...*)
- | Aboth of bool
- (* annotation can be used as both hypothesis and goal :
- - with true : considered as both : A /\ A=>..
- - with false : we just want to use it as hyp right now. *)
- | AcutB of bool
- (* annotation is use as a cut :
- - with true (A is also a goal) -> A (+ proof obligation A => ...)
- - with false (A is an hyp only) -> True (+ proof obligation A => ...) *)
- | AcallHyp of kernel_function
- (* annotation is a called function property to consider as an Hyp.
- * The pre are not here but in AcallPre since they can also
- * be considered as goals. *)
- | AcallPre of bool * kernel_function
- (* annotation is a called function precondition :
- to be considered as hyp, and goal if bool=true *)
- | AcallCheck of kernel_function
- (* annotation is a called function check-only precondition.
- to be considered as goal only. *)
- | AcallPost of kernel_function
- (* annotation is a called function post check :
- to be considered as goal only *)
-
-type call_pre_kind = CPhyp | CPgoal | CPboth
-
-(* -------------------------------------------------------------------------- *)
-(* --- Annotations for one program point. --- *)
-(* -------------------------------------------------------------------------- *)
-
-module ForCall = Kernel_function.Map
-
-(** Some elements can be used as both Hyp and Goal : because of the selection
- * mechanism, we need to add a boolean [as_goal] to tell if the element is to be
- * considered as a goal. If [false], the element can still be used as hypothesis.
-*)
-type annots = {
- p_hyp : WpPropId.pred_info list;
- p_goal : WpPropId.pred_info list;
- p_both : (bool * WpPropId.pred_info) list;
- p_cut : (bool * WpPropId.pred_info) list;
- call_hyp : WpPropId.pred_info list ForCall.t; (* post and pre *)
- call_pre : (call_pre_kind * WpPropId.pred_info) list ForCall.t;
- call_post : WpPropId.pred_info list ForCall.t; (* post goals only (not hyp) *)
- call_asgn : WpPropId.assigns_full_info ForCall.t;
- a_goal : WpPropId.assigns_full_info;
- a_hyp : WpPropId.assigns_full_info;
- a_call : WpPropId.assigns_full_info; (* dynamic calls *)
-}
-
-type t_annots = { has_asgn_goal : bool; has_prop_goal : bool; info: annots }
-
-(* --- Add annotations --- *)
-
-let empty_acc =
- let a = {
- p_hyp = []; p_goal = []; p_both = []; p_cut = [];
- call_hyp = ForCall.empty;
- call_pre = ForCall.empty;
- call_asgn = ForCall.empty;
- call_post = ForCall.empty;
- a_goal = WpPropId.empty_assigns_info;
- a_hyp = WpPropId.empty_assigns_info;
- a_call = WpPropId.empty_assigns_info;
- } in
- { has_asgn_goal = false; has_prop_goal = false; info = a; }
-
-let normalize id ?assumes labels p =
- try
- let p = NormAtLabels.preproc_annot labels p in
- match assumes with
- | None -> Some p
- | Some a ->
- let a = Logic_const.pat(a,Logic_const.pre_label) in
- let a = NormAtLabels.(preproc_annot labels_fct_pre a) in
- Some(Logic_const.pimplies(a,p))
- with e ->
- let pid = WpPropId.get_propid id in
- NormAtLabels.catch_label_error e pid "annotation" ;
- None
-
-let add_prop acc kind id p =
- let get_p = match p with None -> None
- | Some p -> Some(WpPropId.mk_pred_info id p) in
- let add_hyp l = match get_p with None -> l | Some p -> p::l in
- let add_goal l = match get_p with None -> l | Some p -> p::l in
- let add_both_std goal l =
- match get_p with None -> l | Some p -> (goal,p) :: l
- in
- let add_both goal l =
- match get_p with
- | None -> l
- | Some p ->
- let kind = if goal then CPboth else CPhyp in
- (kind, p)::l
- in
- let add_pre l =
- match get_p with
- | None -> l
- | Some p -> (CPgoal, p) :: l
- in
- let add_for_call fct calls =
- let l = try ForCall.find fct calls with Not_found -> [] in
- ForCall.add fct (add_hyp l) calls in
- let add_both_call fct goal calls =
- let l = try ForCall.find fct calls with Not_found -> [] in
- ForCall.add fct (add_both goal l) calls in
- let add_pre_call fct calls =
- let l = try ForCall.find fct calls with Not_found -> [] in
- ForCall.add fct (add_pre l) calls
- in
- let info = acc.info in
- let goal, info = match kind with
- | Ahyp ->
- false, { info with p_hyp = add_hyp info.p_hyp }
- | Agoal ->
- true, { info with p_goal = add_goal info.p_goal }
- | Aboth goal ->
- goal, { info with p_both = add_both_std goal info.p_both }
- | AcutB goal ->
- goal, { info with p_cut = add_both_std goal info.p_cut }
- | AcallHyp fct ->
- false, { info with call_hyp = add_for_call fct info.call_hyp }
- | AcallPre (goal,fct) ->
- goal, { info with call_pre = add_both_call fct goal info.call_pre }
- | AcallCheck fct ->
- true, { info with call_pre = add_pre_call fct info.call_pre }
- | AcallPost fct ->
- true, { info with call_post = add_for_call fct info.call_post }
- in let acc = { acc with info = info } in
- if goal then { acc with has_prop_goal = true} else acc
-
-(* -------------------------------------------------------------------------- *)
-(* adding some specific properties. *)
-let add_prop_fct_pre_bhv acc kind kf bhv =
- let norm_pred pred =
- let p = Logic_const.pred_of_id_pred pred in
- Logic_const.(pat (p,pre_label))
- in
- let requires =
- List.filter (fun x -> use_predicate x.ip_content.tp_kind) bhv.b_requires
- in
- let requires = Logic_const.pands (List.map norm_pred requires) in
- let assumes = Logic_const.pands (List.map norm_pred bhv.b_assumes) in
- let precond = Logic_const.pimplies (assumes, requires) in
- let precond_id = Logic_const.new_predicate precond in
- let id = WpPropId.mk_pre_id kf Kglobal bhv precond_id in
- let labels = NormAtLabels.labels_fct_pre in
- let p = normalize id labels precond in
- add_prop acc kind id p
-
-let add_prop_fct_pre acc kind kf bhv ~assumes pre =
- if use_predicate pre.ip_content.tp_kind then begin
- let id = WpPropId.mk_pre_id kf Kglobal bhv pre in
- let labels = NormAtLabels.labels_fct_pre in
- let p = Logic_const.pred_of_id_pred pre in
- let p = Logic_const.(pat (p,pre_label)) in
- let p = normalize id ?assumes labels p in
- add_prop acc kind id p
- end else acc
-
-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 ~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
- end else acc
-
-let add_prop_fct_bhv_pre acc kind kf bhv =
- let assumes = None in
- let add acc p = add_prop_fct_pre acc kind kf bhv ~assumes p in
- let acc = List.fold_left add acc bhv.b_requires in
- List.fold_left add acc bhv.b_assumes
-
-let add_prop_stmt_pre acc kind kf s bhv ~assumes pre =
- if use_predicate pre.ip_content.tp_kind then begin
- let id = WpPropId.mk_pre_id kf (Kstmt s) bhv pre in
- let labels = NormAtLabels.labels_stmt_pre ~kf s in
- let p = Logic_const.pred_of_id_pred pre in
- let p = normalize id labels ?assumes p in
- add_prop acc kind id p
- end else acc
-
-let add_prop_stmt_bhv_requires acc kind kf s bhv ~with_assumes =
- let assumes =
- if with_assumes then Some (Ast_info.behavior_assumes bhv) else None
- in let add acc pre =
- add_prop_stmt_pre acc kind kf s bhv ~assumes pre
- in List.fold_left add acc bhv.b_requires
-
-(** Process the stmt spec precondition as an hypothesis for external properties.
- * Add [assumes => requires] for all the behaviors. *)
-let add_prop_stmt_spec_pre acc kind kf s spec =
- let add_bhv_pre acc bhv =
- add_prop_stmt_bhv_requires acc kind kf s bhv ~with_assumes:true
- in List.fold_left add_bhv_pre acc spec.spec_behavior
-
-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_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
- end else acc
-
-let update_kind kind pre =
- if pre.ip_content.tp_kind = Check then begin
- match kind with
- | AcallPre(false,_) -> None
- | AcallPre(true, kf) -> Some (AcallCheck kf)
- | _ -> Some kind
- end else Some kind
-
-let add_prop_call_pre acc kind id ~assumes pre =
- match update_kind kind pre with
- | None -> acc
- | Some kind ->
- let labels = NormAtLabels.labels_fct_pre in
- let p = Logic_const.pred_of_id_pred pre in
- (* assumes can be normalized in the same time *)
- let p = Logic_const.pimplies (assumes, p) in
- let p = normalize id labels p in
- add_prop acc kind id p
-
-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 ~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 ~kf s in
- let p = normalize id labels p in
- add_prop acc kind id p
-
-let add_prop_loop_inv acc kind s id p =
- let labels = NormAtLabels.labels_loop s in
- let p = normalize id labels p in
- add_prop acc kind id p
-
-(** apply [f_normal] on the [Normal] postconditions,
- * [f_exits] on the [Exits] postconditions, and warn on the others. *)
-let fold_bhv_post_cond ~warn f_normal f_exits acc b =
- let add (p_acc, e_acc) ((termination_kind, pe) as e) =
- match termination_kind with
- | Normal -> f_normal p_acc pe, e_acc
- | Exits -> p_acc, f_exits e_acc pe
- | Returns -> p_acc, e_acc (* HANDLED by an ASSERT from CIL *)
- | (Breaks|Continues) -> (* TODO *)
- begin
- if warn then
- Wp_parameters.warning
- "Abrupt statement termination property ignored:@, %a"
- Printer.pp_post_cond e;
- p_acc, e_acc
- end
- in List.fold_left add acc b.b_post_cond
-
-(* -------------------------------------------------------------------------- *)
-(* --- Smoke --- *)
-(* -------------------------------------------------------------------------- *)
-
-let add_smoke acc kf ~id ?doomed ?unreachable () =
- let id = WpPropId.mk_smoke kf ~id ?doomed ?unreachable () in
- add_prop acc Agoal id (Some Logic_const.pfalse)
-
-let add_prop_fct_smoke acc kf bhv =
- if bhv.b_requires = [] then acc else
- 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
- add_smoke acc kf ~id ~doomed ()
-
-let add_prop_dead_loop acc kf stmt =
- add_smoke acc kf ~id:"dead_loop" ~unreachable:stmt ()
-
-let add_prop_dead_code acc kf stmt =
- add_smoke acc kf ~id:"dead_code" ~unreachable:stmt ()
-
-let add_prop_dead_call kf stmt acc_posts acc_exits =
- let id = WpPropId.mk_smoke kf ~id:"dead_call" ~unreachable:stmt () in
- let kind = AcallPost kf in
- let pred = Some Logic_const.pfalse in
- add_prop acc_posts kind id pred , add_prop acc_exits kind id pred
-
-(* -------------------------------------------------------------------------- *)
-
-let from_has_deps = function _, FromAny -> false | _, From _ -> true
-let assigns_has_deps = function
- | WritesAny -> false
- | Writes l -> List.exists from_has_deps l
-
-let add_assigns acc kind id a_desc =
- let take_assigns () =
- debug "take %a %a" WpPropId.pp_propid id WpPropId.pp_assigns_desc a_desc;
- WpPropId.mk_assigns_info id a_desc
- in
- let take_assigns_call fct info =
- let asgn = take_assigns () in
- { info with call_asgn = ForCall.add fct asgn info.call_asgn }
- in
- let info = acc.info in
- let goal, info = match kind with
- | Ahyp -> false, {info with a_hyp = take_assigns ()}
- | AcallHyp fct -> false, take_assigns_call fct info
- | Agoal -> true, {info with a_goal = take_assigns ()}
- | _ -> Wp_parameters.fatal "Assigns prop can only be Hyp or Goal"
- in let acc = { acc with info = info } in
- if goal && assigns_has_deps a_desc.a_assigns then
- Wp_parameters.warning
- ~once: true ~current:false ~wkey:AssignsCompleteness.wkey_pedantic
- "WP uses \\from to generate precise hypotheses, however their proof is \
- not supported yet" ;
- if goal then { acc with has_asgn_goal = true} else acc
-
-let add_assigns_any acc kind asgn =
- let take_call fct asgn info =
- { info with call_asgn = ForCall.add fct asgn info.call_asgn } in
- match kind with
- | Ahyp -> {acc with info = { acc.info with a_hyp = asgn}}
- | AcallHyp fct -> {acc with info = take_call fct asgn acc.info}
- | _ -> Wp_parameters.fatal "Assigns Any prop can only be Hyp"
-
-let assigns_upper_bound spec =
- let bhvs = spec.spec_behavior in
- let upper a b =
- match a, b.b_assigns with
- | None, Writes a when Cil.is_default_behavior b ->
- Some (b,a) (* default behavior always applies. *)
- | None, _ -> None (* WritesAny U X -> WritesAny *)
- | Some (b,_), _ when Cil.is_default_behavior b ->
- a (* default behavior prevails over other behaviors. *)
- | Some _, WritesAny ->
- None (* No default behavior and one behavior assigns everything. *)
- | Some(b,a1), Writes a2 -> Some (b,a1 @ a2)
- (* take the whole list of assigns. *)
- in
- match bhvs with
- | [] -> None
- | bhv::bhvs ->
- (* [VP 2011-02-04] Note that if there is no default and each
- behavior has a proper assigns clause we put dependencies only
- to the assigns of a more or less randomly selected behavior,
- but the datatypes above can't handle anything better. *)
- let acc =
- match bhv.b_assigns with
- WritesAny -> None
- | Writes a -> Some(bhv,a)
- in
- List.fold_left upper acc bhvs
-
-(* [VP 2011-02-04] These two functions below mix all the assigns of
- a function regardless of the behavior. At least now that we take
- WritesAny as soon as at least one behavior has no assigns clause,
- this is correct, but still imprecise. Needs refactoring of t_annots to
- go further, though.
- [AP 2011-03-11] I think that the merge of all assigns properties
- is intended because we are using it as an hypothesis to skip the statement
- or the function call.
-*)
-let add_stmt_spec_assigns_hyp acc kf s l_post spec =
- match assigns_upper_bound spec with
- | None ->
- add_assigns_any acc Ahyp
- (WpPropId.mk_stmt_any_assigns_info s)
- | Some(bhv, assigns) ->
- (* We are always using the spec covering all possible parent behaviors. *)
- let id = WpPropId.mk_stmt_assigns_id kf s [] bhv assigns in
- match id with
- | None -> add_assigns_any acc Ahyp
- (WpPropId.mk_stmt_any_assigns_info s)
- | Some id ->
- 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
-
-let add_call_assigns_any acc s =
- let asgn = WpPropId.mk_stmt_any_assigns_info s in
- {acc with info = { acc.info with a_call = asgn }}
-
-let add_call_assigns_hyp acc kf_caller s ~called_kf l_post spec_opt =
- match spec_opt with
- | None ->
- let pid = WpPropId.mk_stmt_any_assigns_info s in
- add_assigns_any acc (AcallHyp called_kf) pid
- | Some spec ->
- match assigns_upper_bound spec with
- | None ->
- let asgn = WpPropId.mk_stmt_any_assigns_info s in
- add_assigns_any acc (AcallHyp called_kf) asgn
- | Some(bhv, assigns) ->
- (* we're taking assigns from a function contract.
- They're not subject to any active behavior. *)
- let id = WpPropId.mk_stmt_assigns_id kf_caller s [] bhv assigns in
- match id with
- | None ->
- let asgn = WpPropId.mk_stmt_any_assigns_info s in
- add_assigns_any acc (AcallHyp called_kf) asgn
- | Some pid ->
- ignore l_post ;
- (* let kf = kf_caller in *)
- let labels = NormAtLabels.labels_fct_assigns ~exit:false (* ~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
-
-(* [VP 2011-01-28] following old behavior, not sure it is correct:
- why should we give to add_assigns the assigns with unnormalized labels?
- [AP 2011-03-11] to answer VP question, the source assigns are only used to
- build an identifier for the property which is use later to update its status
- and dependencies so we need to have the original one.
-*)
-let add_loop_assigns_hyp acc kf s asgn_opt = match asgn_opt with
- | None ->
- let asgn = WpPropId.mk_loop_any_assigns_info s in
- add_assigns_any acc Ahyp asgn
- | Some (ca, assigns) ->
- let id = WpPropId.mk_loop_assigns_id kf s ca assigns in
- match id with
- | None ->
- let asgn = WpPropId.mk_loop_any_assigns_info s in
- add_assigns_any acc Ahyp asgn
- | Some id ->
- let labels = NormAtLabels.labels_loop s in
- let assigns' = NormAtLabels.preproc_assigns labels assigns in
- let a_desc = WpPropId.mk_loop_assigns_desc s assigns' in
- add_assigns acc Ahyp id a_desc
-
-let add_fct_bhv_assigns_hyp acc kf tkind b = match b.b_assigns with
- | WritesAny ->
- let id = WpPropId.mk_kf_any_assigns_info () in
- add_assigns_any acc Ahyp id
- | Writes assigns ->
- 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 ~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
-
-(* --- Get annotations --- *)
-
-let get_goal_only annots = annots.info.p_goal
-
-let get_hyp_only annots = annots.info.p_hyp
-
-let filter_both l =
- let add (h_acc, g_acc) (goal, p) =
- p::h_acc, if goal then p::g_acc else g_acc
- in List.fold_left add ([], []) l
-
-let filter_both_call l =
- let add (h_acc, g_acc) (goal, p) =
- match goal with
- | CPboth -> p :: h_acc, p :: g_acc
- | CPhyp -> p :: h_acc, g_acc
- | CPgoal -> h_acc, p :: g_acc
- in List.fold_left add ([], []) l
-
-let get_both_hyp_goals annots = filter_both annots.info.p_both
-
-let get_call_hyp annots fct =
- try ForCall.find fct annots.info.call_hyp
- with Not_found -> []
-
-let get_call_pre annots fct =
- try filter_both_call (ForCall.find fct annots.info.call_pre)
- with Not_found -> [],[]
-
-let get_call_post annots fct =
- try ForCall.find fct annots.info.call_post
- with Not_found -> []
-
-let get_call_asgn annots = function
- | None -> annots.info.a_call
- | Some fct ->
- try ForCall.find fct annots.info.call_asgn
- with Not_found -> WpPropId.empty_assigns_info
-
-let get_cut annots = annots.info.p_cut
-
-let get_asgn_hyp annots = annots.info.a_hyp
-
-let get_asgn_goal annots = annots.info.a_goal
-
-(* --- Print annotations --- *)
-
-let pp_annots fmt acc =
- let acc = acc.info in
- let pp_pred k b p =
- Format.fprintf fmt "%s%s: %a@."
- k (if b then "" else " (h)") WpPropId.pp_pred_of_pred_info p
- in
- let pp_pred_c k c p =
- let kind = match c with CPboth -> "(h+g)" | CPgoal -> "g" | CPhyp -> "h" in
- Format.fprintf fmt "%s%s: %a@."
- k kind WpPropId.pp_pred_of_pred_info p
- in
- let pp_pred_list k l = List.iter (fun p -> pp_pred k true p) l in
- let pp_pred_b_list k l = List.iter (fun (b, p) -> pp_pred k b p) l in
- let pp_pred_c_list k l = List.iter (fun (c, p) -> pp_pred_c k c p) l in
- begin
- pp_pred_list "H" acc.p_hyp;
- pp_pred_list "G" acc.p_goal;
- pp_pred_b_list "H+G" acc.p_both;
- pp_pred_b_list "C" acc.p_cut;
- ForCall.iter
- (fun kf hs ->
- let name = "CallHyp:" ^ (Kernel_function.get_name kf) in
- pp_pred_list name hs)
- acc.call_hyp;
- ForCall.iter
- (fun kf bhs ->
- let name = "CallPre:" ^ (Kernel_function.get_name kf) in
- pp_pred_c_list name bhs)
- acc.call_pre;
- ForCall.iter
- (fun kf asgn ->
- let name = "CallAsgn:" ^ (Kernel_function.get_name kf) in
- WpPropId.pp_assign_info name fmt asgn)
- acc.call_asgn;
- WpPropId.pp_assign_info "DC" fmt acc.a_call;
- WpPropId.pp_assign_info "HA" fmt acc.a_hyp;
- WpPropId.pp_assign_info "GA" fmt acc.a_goal;
- end
-
-let merge_calls f call1 call2 =
- ForCall.merge
- (fun _fct a b -> match a,b with
- | None,c | c,None -> c
- | Some a,Some b -> Some (f a b)
- ) call1 call2
-
-(* TODO: it should be possible to do without this, but needs a big refactoring*)
-let merge_acc acc1 acc2 =
- {
- p_hyp = acc1.p_hyp @ acc2.p_hyp;
- p_goal = acc1.p_goal @ acc2.p_goal;
- p_both = acc1.p_both @ acc2.p_both;
- p_cut = acc1.p_cut @ acc2.p_cut;
- call_hyp = merge_calls (@) acc1.call_hyp acc2.call_hyp;
- call_pre = merge_calls (@) acc1.call_pre acc2.call_pre;
- call_post = merge_calls (@) acc1.call_post acc2.call_post;
- call_asgn = merge_calls WpPropId.merge_assign_info acc1.call_asgn acc2.call_asgn;
- a_goal = WpPropId.merge_assign_info acc1.a_goal acc2.a_goal;
- a_hyp = WpPropId.merge_assign_info acc1.a_hyp acc2.a_hyp;
- a_call = WpPropId.merge_assign_info acc1.a_call acc2.a_call;
- }
-
-(* -------------------------------------------------------------------------- *)
-(* --- Annotation table --- *)
-(* -------------------------------------------------------------------------- *)
-
-(** This is an Hashtbl where some predicates are stored on CFG edges.
- * On each edge, we store hypotheses and goals.
-*)
-module Hannots = Cil2cfg.HE (struct type t = annots end)
-
-type annots_tbl = {
- tbl_annots : Hannots.t;
- mutable tbl_axioms : WpPropId.axiom_info list;
- mutable tbl_has_prop_goal : bool;
- mutable tbl_has_asgn_goal : bool;
-}
-
-let create_tbl () = {
- tbl_annots = Hannots.create 7;
- tbl_axioms = [];
- tbl_has_prop_goal = false;
- tbl_has_asgn_goal = false;
-}
-
-let add_on_edges tbl new_acc edges =
- if new_acc.has_prop_goal then tbl.tbl_has_prop_goal <- true;
- if new_acc.has_asgn_goal then tbl.tbl_has_asgn_goal <- true;
- let add_on_edge e =
- let acc =
- try
- let acc = Hannots.find tbl.tbl_annots e in
- merge_acc new_acc.info acc
- with Not_found -> new_acc.info
- in Hannots.replace tbl.tbl_annots e acc;
- in List.iter add_on_edge edges
-
-let add_node_annots tbl cfg v (before, (post, exits)) =
- debug "[add_node_annots] on %a@." Cil2cfg.pp_node v;
- add_on_edges tbl before (Cil2cfg.get_pre_edges cfg v);
- if post <> empty_acc then
- begin
- let edges_after = Cil2cfg.get_post_edges cfg v in
- if edges_after = []
- then (* unreachable (see [process_unreached_annots]) *) ()
- else add_on_edges tbl post edges_after
- end;
- if exits <> empty_acc then
- begin
- let edges_exits = Cil2cfg.get_exit_edges cfg v in
- if edges_exits = []
- then (* unreachable (see [process_unreached_annots]) *) ()
- else add_on_edges tbl exits edges_exits
- end
-
-let add_loop_annots tbl cfg vloop ~entry ~back ~core =
- debug "[add_loop_annots] on %a@."Cil2cfg.pp_node vloop;
- let edges_to_head = Cil2cfg.succ_e cfg vloop in
- debug "[add_loop_annots] %d edges_to_head" (List.length edges_to_head);
- let edges_to_loop = Cil2cfg.pred_e cfg vloop in
- debug "[add_loop_annots] %d edges_to_loop" (List.length edges_to_loop);
- let back_edges, entry_edges =
- List.partition Cil2cfg.is_back_edge edges_to_loop
- in
- debug "[add_loop_annots] %d back_edges + %d entry_edges"
- (List.length back_edges) (List.length entry_edges);
- add_on_edges tbl entry entry_edges;
- debug "[add_loop_annots on entry_edges ok]@.";
- add_on_edges tbl back back_edges;
- debug "[add_loop_annots on back_edges ok]@.";
- add_on_edges tbl core edges_to_head;
- debug "[add_loop_annots on edges_to_head ok]@."
-
-let add_axiom tbl lemma =
- try
- (* Labels does not need normalization *)
- let axiom = WpPropId.mk_axiom_info lemma in
- debug "take %a@." WpPropId.pp_axiom_info axiom;
- tbl.tbl_axioms <- axiom::tbl.tbl_axioms
- with e ->
- NormAtLabels.catch_label_error e ("axiom "^lemma.lem_name) "axiom"
-
-let add_all_axioms tbl =
- let rec do_g g =
- match g with
- | Daxiomatic (_ax_name, globs,_,_) -> do_globs globs
- | Dlemma (name,_,_,_,_,_) ->
- let lem = LogicUsage.logic_lemma name in
- add_axiom tbl lem
- | _ -> ()
- and do_globs globs = List.iter do_g globs in
- Annotations.iter_global (fun _ -> do_g)
-
-let get_annots tbl e =
- try (* TODO clean : this is not very nice ! *)
- let info = Hannots.find tbl.tbl_annots e in { empty_acc with info = info}
- with Not_found -> empty_acc
-
-(* -------------------------------------------------------------------------- *)
-(* --- Strategy --- *)
-(* -------------------------------------------------------------------------- *)
-
-type strategy_for_froms = {
- get_pre : unit -> t_annots;
- more_vars : logic_var list
-}
-
-type strategy_kind =
- | SKannots (* normal mode for annotations *)
- | SKfroms of strategy_for_froms
-
-(* an object of this type is the only access to annotations
- * from the rest of the application.
- * The idea is to be able to tune which properties to use for a computation. *)
-type strategy = {
- desc : string ;
- cfg : Cil2cfg.t;
- behavior_name : string option ;
- strategy_kind : strategy_kind;
- annots : annots_tbl;
-}
-
-
-let get_kf s = Cil2cfg.cfg_kf s.cfg
-let get_bhv s = s.behavior_name
-
-let is_default_behavior s =
- match s.behavior_name with None -> true | Some _ -> false
-
-let mk_strategy desc cfg bhv_name kind tbl = {
- desc = desc; cfg = cfg; behavior_name = bhv_name;
- strategy_kind = kind; annots = tbl;
-}
-
-let cfg_of_strategy strat = strat.cfg
-let behavior_name_of_strategy strat = strat.behavior_name
-let global_axioms strat = strat.annots.tbl_axioms
-let strategy_kind strat = strat.strategy_kind
-let strategy_has_prop_goal strat = strat.annots.tbl_has_prop_goal
-let strategy_has_asgn_goal strat = strat.annots.tbl_has_asgn_goal
-let get_annots strat = get_annots strat.annots
-
-let pp_info_of_strategy fmt strat =
- Format.fprintf fmt "@[%s@]" strat.desc
-
-(* -------------------------------------------------------------------------- *)
-(* --- Helpers --- *)
-(* -------------------------------------------------------------------------- *)
-
-let is_main_init kf =
- if Kernel.LibEntry.get () then false
- else
- let is_main =
- try
- let main, _ = Globals.entry_point () in
- Kernel_function.equal kf main
- with Globals.No_such_entry_point _ -> false
- in
- debug "'%a' is %sthe main entry point@."
- Kernel_function.pretty kf (if is_main then "" else "NOT ");
- is_main
-
-let isInitConst () = Wp_parameters.Init.get ()
-
-let isGlobalInitConst var =
- var.vglob && var.vstorage <> Extern && Cil.typeHasQualifier "const" var.vtype
-
-let mk_variant_properties kf s ca v =
- let vpos_id = WpPropId.mk_var_pos_id kf s ca in
- let vdecr_id = WpPropId.mk_var_decr_id kf s ca in
- let loc = v.term_loc in
- let lcurr = Clabels.to_logic (Clabels.loop_current s) in
- let vcurr = Logic_const.tat ~loc (v, lcurr) in
- let zero = Cil.lzero ~loc () in
- let vpos = Logic_const.prel ~loc (Rle, zero, vcurr) in
- let vdecr = Logic_const.prel ~loc (Rlt, v, vcurr) in
- (vpos_id, vpos), (vdecr_id, vdecr)
-
-(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpStrategy.mli b/src/plugins/wp/wpStrategy.mli
deleted file mode 100644
index d69d701af37f6c607894f7282ee16ec479c7009c..0000000000000000000000000000000000000000
--- a/src/plugins/wp/wpStrategy.mli
+++ /dev/null
@@ -1,302 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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 Clabels
-
-(* -------------------------------------------------------------------------- *)
-(** This file provide all the functions to build a strategy that can then
- * be used by the main generic calculus. *)
-(* -------------------------------------------------------------------------- *)
-
-(* -------------------------------------------------------------------------- *)
-(** {2 Annotations} *)
-(* -------------------------------------------------------------------------- *)
-
-(** a set of annotations to be added to a program point. *)
-type t_annots
-
-val empty_acc : t_annots
-
-(** {3 How to use an annotation} *)
-
-(** An annotation can be used for different purpose. *)
-type annot_kind =
- | Ahyp (** annotation is an hypothesis,
- but not a goal (see Aboth) : A => ...*)
- | Agoal (** annotation is a goal,
- but not an hypothesis (see Aboth): A /\ ...*)
- | Aboth of bool (** annotation can be used as both hypothesis and goal :
- - with true : considered as both : A /\ A=>..
- - with false : we just want to use it as hyp right now. *)
- | AcutB of bool (** annotation is use as a cut :
- - with true (A is also a goal) -> A (+ proof obligation A => ...)
- - with false (A is an hyp only) -> True (+ proof obligation A => ...) *)
- | AcallHyp of kernel_function
- (** annotation is a called function property to consider as an Hyp.
- * The pre are not here but in AcallPre since they can also
- * be considered as goals. *)
- | AcallPre of bool * kernel_function
- (** annotation is a called function precondition :
- to be considered as hyp, and goal if bool=true *)
- | AcallCheck of kernel_function
- (** annotation is check-only called function precondition.
- handled internally by {!add_prop_call_pre} below. *)
- | AcallPost of kernel_function
- (** annotation is a called function post check :
- to be considered as goal only (no hyp) *)
-
-(** {3 Adding properties (predicates)} *)
-
-val normalize : WpPropId.prop_id ->
- ?assumes:predicate ->
- NormAtLabels.label_mapping ->
- predicate -> predicate option
-
-(** generic function to add a predicate property after normalisation.
- * All the [add_prop_xxx] functions below use this one. *)
-val add_prop : t_annots -> annot_kind -> WpPropId.prop_id -> predicate option -> t_annots
-
-val add_prop_fct_pre_bhv :
- t_annots -> annot_kind -> Cil_types.kernel_function ->
- Cil_types.funbehavior -> t_annots
-
-(** Add the predicate as a function precondition.
- * Add [assumes => pre] if [assumes] is given. *)
-val add_prop_fct_pre : t_annots -> annot_kind ->
- kernel_function -> funbehavior ->
- assumes: predicate option -> identified_predicate -> t_annots
-
-(** Add the preconditions of the behavior *)
-val add_prop_fct_bhv_pre : t_annots -> annot_kind ->
- kernel_function -> funbehavior -> t_annots
-
-(** Add Smoke Test behavior *)
-val add_prop_fct_smoke : t_annots -> kernel_function -> funbehavior -> t_annots
-
-(** Add Smoke Test for loop *)
-val add_prop_dead_loop : t_annots -> kernel_function -> stmt -> t_annots
-
-(** Add Smoke Test for possibly dead code *)
-val add_prop_dead_code : t_annots -> kernel_function -> stmt -> t_annots
-
-(** Add Smoke Test for possibly dead call : (posts,exits) *)
-val add_prop_dead_call : kernel_function -> stmt -> t_annots -> t_annots ->
- t_annots * t_annots
-
-val add_prop_fct_post : t_annots -> annot_kind ->
- kernel_function -> funbehavior -> termination_kind -> identified_predicate
- -> t_annots
-
-(** Add the predicate as a stmt precondition.
- * Add [assumes => pre] if [assumes] is given. *)
-val add_prop_stmt_pre : t_annots -> annot_kind ->
- kernel_function -> stmt -> funbehavior ->
- assumes: predicate option -> identified_predicate -> t_annots
-
-(** Add the predicate as a stmt precondition.
- * Add [\old (assumes) => post] if [assumes] is given. *)
-val add_prop_stmt_post :t_annots -> annot_kind ->
- kernel_function -> stmt -> funbehavior -> termination_kind ->
- c_label option -> assumes:predicate option -> identified_predicate
- -> t_annots
-
-(** Add all the [b_requires]. Add [b_assumes => b_requires] if [with_assumes] *)
-val add_prop_stmt_bhv_requires : t_annots -> annot_kind ->
- kernel_function -> stmt -> funbehavior -> with_assumes:bool -> t_annots
-
-(** Process the stmt spec precondition as an hypothesis for external properties.
- * Add [assumes => requires] for all the behaviors. *)
-val add_prop_stmt_spec_pre : t_annots -> annot_kind ->
- kernel_function -> stmt -> funspec -> t_annots
-
-val add_prop_call_pre : t_annots -> annot_kind -> WpPropId.prop_id ->
- assumes:predicate -> identified_predicate -> t_annots
-
-(** Add a postcondition of a called function. Beware that [kf] and [bhv]
- * are the called one. *)
-val add_prop_call_post : t_annots -> annot_kind ->
- kernel_function -> funbehavior -> termination_kind ->
- assumes:predicate -> identified_predicate -> t_annots
-
-val add_prop_assert : t_annots -> annot_kind ->
- kernel_function -> stmt -> code_annotation -> predicate -> t_annots
-
-val add_prop_loop_inv : t_annots -> annot_kind ->
- stmt -> WpPropId.prop_id -> predicate -> t_annots
-
-(** {3 Adding assigns properties} *)
-
-(** generic function to add an assigns property. *)
-val add_assigns : t_annots -> annot_kind ->
- WpPropId.prop_id -> WpPropId.assigns_desc -> t_annots
-
-(** generic function to add a WriteAny assigns property. *)
-val add_assigns_any : t_annots -> annot_kind ->
- WpPropId.assigns_full_info -> t_annots
-
-(** shortcut to add a stmt spec assigns property as an hypothesis. *)
-val add_stmt_spec_assigns_hyp : t_annots -> kernel_function -> stmt ->
- c_label option -> funspec -> t_annots
-
-(** short cut to add a dynamic call *)
-val add_call_assigns_any : t_annots -> stmt -> t_annots
-
-(** shortcut to add a call assigns property as an hypothesis. *)
-val add_call_assigns_hyp : t_annots -> kernel_function -> stmt ->
- called_kf:kernel_function ->
- c_label option -> funspec option -> t_annots
-
-(** shortcut to add a loop assigns property as an hypothesis. *)
-val add_loop_assigns_hyp : t_annots -> kernel_function -> stmt ->
- (code_annotation * from list) option -> t_annots
-
-val add_fct_bhv_assigns_hyp : t_annots -> kernel_function -> termination_kind ->
- funbehavior -> t_annots
-
-val assigns_upper_bound :
- funspec -> (funbehavior * from list) option
-
-(** {3 Getting information from annotations} *)
-
-val get_hyp_only : t_annots -> WpPropId.pred_info list
-val get_goal_only : t_annots -> WpPropId.pred_info list
-val get_both_hyp_goals : t_annots ->
- WpPropId.pred_info list * WpPropId.pred_info list
-
-(** the [bool] in [get_cut] results says if the property has to be
- * considered as a both goal and hyp ([goal=true], or hyp only ([goal=false]) *)
-val get_cut : t_annots -> (bool * WpPropId.pred_info) list
-
-(** To be used as hypotheses around a call, (the pre are in
- * [get_call_pre_goal]) *)
-val get_call_hyp : t_annots -> kernel_function -> WpPropId.pred_info list
-
-(** Preconditions of a called function to be considered as hyp and goal
- * (similar to [get_both_hyp_goals]). *)
-val get_call_pre : t_annots -> kernel_function -> WpPropId.pred_info list * WpPropId.pred_info list
-
-(** Post-checks of a called function to be considered as goal only *)
-val get_call_post : t_annots -> kernel_function -> WpPropId.pred_info list
-
-val get_call_asgn : t_annots -> kernel_function option -> WpPropId.assigns_full_info
-
-
-val get_asgn_hyp : t_annots -> WpPropId.assigns_full_info
-val get_asgn_goal : t_annots -> WpPropId.assigns_full_info
-
-(** {3 Printing} *)
-
-val pp_annots : Format.formatter -> t_annots -> unit
-
-(* -------------------------------------------------------------------------- *)
-(** {2 Annotation table} *)
-(* -------------------------------------------------------------------------- *)
-
-type annots_tbl
-
-val create_tbl : unit -> annots_tbl
-
-val add_on_edges : annots_tbl -> t_annots -> Cil2cfg.edge list -> unit
-
-(** [add_node_annots cfg annots v (before, (after, exits))]
- * add the annotations for the node :
- * @param before preconditions
- * @param after postconditions
- * @param exits \exits properties
-*)
-val add_node_annots : annots_tbl -> Cil2cfg.t -> Cil2cfg.node ->
- (t_annots * (t_annots * t_annots)) -> unit
-
-val add_loop_annots : annots_tbl -> Cil2cfg.t -> Cil2cfg.node ->
- entry:t_annots -> back:t_annots -> core:t_annots -> unit
-
-val add_axiom : annots_tbl -> LogicUsage.logic_lemma -> unit
-
-val add_all_axioms : annots_tbl -> unit
-
-(* -------------------------------------------------------------------------- *)
-(** {2 Strategy} *)
-(* -------------------------------------------------------------------------- *)
-
-type strategy
-
-type strategy_for_froms = {
- get_pre : unit -> t_annots;
- more_vars : logic_var list
-}
-
-type strategy_kind =
- | SKannots (** normal mode for annotations *)
- | SKfroms of strategy_for_froms
-
-val mk_strategy : string -> Cil2cfg.t -> string option ->
- strategy_kind -> annots_tbl -> strategy
-
-val get_annots : strategy -> Cil2cfg.edge -> t_annots
-val strategy_has_asgn_goal : strategy -> bool
-val strategy_has_prop_goal : strategy -> bool
-val strategy_kind : strategy -> strategy_kind
-val global_axioms : strategy -> WpPropId.axiom_info list
-val behavior_name_of_strategy : strategy -> string option
-val is_default_behavior : strategy -> bool
-
-val cfg_of_strategy : strategy -> Cil2cfg.t
-
-val get_kf : strategy -> kernel_function
-val get_bhv : strategy -> string option
-
-val pp_info_of_strategy : Format.formatter -> strategy -> unit
-
-(* -------------------------------------------------------------------------- *)
-(** {2 Other useful things} *)
-(* -------------------------------------------------------------------------- *)
-
-(** The function is the main entry point AND it is not a lib entry *)
-val is_main_init : Cil_types.kernel_function -> bool
-
-
-(** True if both options [-const-readonly] and [-wp-init] are positioned,
- and the variable is global, not extern, with a ["const"] type
- (see [hasConstAttribute]).
- @since Sodium-20150201
-*)
-val isInitConst : unit -> bool
-
-(** True if the variable is global, not extern, with a ["const"] qualifier type.
- {b Should} only apply when [isInitConst] is true.
- @since Sodium-20150201
-*)
-val isGlobalInitConst : varinfo -> bool
-
-(** apply [f_normal] on the [Normal] postconditions,
- * [f_exits] on the [Exits] postconditions, and warn on the others. *)
-val fold_bhv_post_cond : warn:bool ->
- ('n_acc -> Cil_types.identified_predicate -> 'n_acc) ->
- ('e_acc -> Cil_types.identified_predicate -> 'e_acc) ->
- 'n_acc * 'e_acc -> funbehavior -> 'n_acc * 'e_acc
-
-val mk_variant_properties :
- kernel_function -> stmt -> code_annotation -> term ->
- (WpPropId.prop_id * predicate)
- * (WpPropId.prop_id * predicate)
-(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index d037da922d3448206ffcd2da3aea622730a853c8..f822f4567be925a02be6aa29e94a887128522a3c 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -55,13 +55,6 @@ module WP =
end)
let () = on_reset WP.clear
-let () = Parameter_customize.set_group wp_generation
-module Legacy =
- False(struct
- let option_name = "-wp-legacy"
- let help = "Use legacy generator engine."
- end)
-
let () = Parameter_customize.set_group wp_generation
module Dump =
Action(struct
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 9c7961f3df2bda0a0235f294a216c67a41372501..1b2e995888b805f310e22c1cc9a346b314092a96 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -40,7 +40,6 @@ val iter_kf : (Kernel_function.t -> unit) -> unit
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