[wp] use cfg-infos

src/plugins/wp/cfgAnnot.ml

@@ -110,12 +110,12 @@ let normalize_assigns kf ki has_exit bhv ~active = function
 let get_requires kf ki bhv =
   List.map (normalize_pre kf ki bhv) bhv.b_requires
 
-let get_behavior kf ki has_exit ~active bhv =
+let get_behavior kf ki ~exits ~active bhv =
   let pre_cond = normalize_pre kf ki bhv in
   let post_cond tk (kind,ip) =
     if kind = tk then Some (normalize_post kf ki bhv tk ip) else None in
   let p_asgn, e_asgn =
-    normalize_assigns kf ki has_exit bhv ~active bhv.b_assigns
+    normalize_assigns kf ki exits bhv ~active bhv.b_assigns
   in
   {
     bhv_assumes = List.map pre_cond bhv.b_assumes;

src/plugins/wp/cfgAnnot.mli

@@ -43,8 +43,8 @@ type behavior = {
 
 val get_requires : kernel_function -> kinstr -> funbehavior -> pred_info list
 val get_behavior :
-  kernel_function -> kinstr -> bool -> active:string list -> funbehavior ->
-  behavior
+  kernel_function -> kinstr -> exits:bool -> active:string list ->
+  funbehavior -> behavior
 
 val get_preconditions : goal:bool ->kernel_function -> pred_info list
 val get_complete_behaviors : kernel_function -> pred_info list

src/plugins/wp/cfgCalculus.ml

@@ -28,6 +28,7 @@ open Cil_datatype
 (* -------------------------------------------------------------------------- *)
 
 module WpLog = Wp_parameters
+module Kf = Kernel_function
 module Cfg = Interpreted_automata
 module G = Cfg.G
 module V = Cfg.Vertex
@@ -42,6 +43,7 @@ type assigns = WpPropId.assigns_full_info
 type mode = {
   kf: kernel_function;
   bhv : funbehavior ;
+  infos : CfgInfos.t ;
 }
 
 type props = [ `All | `Names of string list | `PropId of Property.t ]
@@ -122,37 +124,6 @@ struct
 
   module I = CfgInit.Make(W)
 
-  module Reachable_call : sig
-    val has_reachable_call: Cfg.automaton -> vertex -> bool
-  end
-  =
-  struct
-    exception Found_call
-
-    type reachability_env = {
-      table: unit Vhash.t ;
-      cfg: Cfg.automaton ;
-    }
-
-    let rec reachable_call_by_cfg env a =
-      try Vhash.find env.table a
-      with Not_found ->
-        Vhash.add env.table a () ;
-        List.iter (transition env) (G.succ_e env.cfg.graph a)
-
-    and transition env (_,edge,dst) =
-      reachable_call_by_cfg env dst ;
-      match edge.edge_transition with
-      | Instr ((Local_init(_,ConsInit _, _)| Call _), _) -> raise Found_call
-      | _ -> ()
-
-    let has_reachable_call cfg v =
-      let env = { table = Vhash.create 32 ; cfg } in
-      try reachable_call_by_cfg env v ; false
-      with Found_call -> true
-
-  end
-
   (* --- Traversal Environment --- *)
 
   type env = {
@@ -291,7 +262,7 @@ struct
     | Local_init(x,ConsInit (vf, args, kind), loc) ->
         Cil.treat_constructor_as_func
           begin fun r fct args _loc ->
-            match Kernel_function.get_called fct with
+            match Kf.get_called fct with
             | Some kf -> call env s r kf args w
             | None ->
                 WpLog.warning ~once:true "No function for constructor '%s'"
@@ -301,7 +272,7 @@ struct
           end x vf args kind loc
     | Call(res,fct,args,_loc) ->
         begin
-          match Kernel_function.get_called fct with
+          match Kf.get_called fct with
           | Some kf -> call env s res kf args w
           | None ->
               match Dyncall.get ~bhv:env.mode.bhv.b_name s with
@@ -335,27 +306,28 @@ struct
       in W.call_goal_precond env.we s kf es ~pre w_call
     else w_call
 
-  let complete mode kf =
-    if not (is_default_bhv mode) then []
-    else CfgAnnot.get_complete_behaviors kf
-
-  let disjoint mode kf =
-    if not (is_default_bhv mode) then []
-    else CfgAnnot.get_disjoint_behaviors kf
+  let do_complete_disjoint env w =
+    if not (is_default_bhv env.mode) then w
+    else
+      let kf = env.mode.kf in
+      let complete = CfgAnnot.get_complete_behaviors kf in
+      let disjoint = CfgAnnot.get_disjoint_behaviors kf in
+      List.fold_right (prove_property env) complete @@
+      List.fold_right (prove_property env) disjoint w
 
   let do_global_init env w =
     I.process_global_init env.we env.mode.kf @@
     W.scope env.we [] SC_Global w
 
-  let do_preconditions env ~main ~formals bhvs w =
+  let do_preconditions env ~formals bhvs w =
     let kf = env.mode.kf in
-    let prove_if_main ps w =
-      if main then List.fold_right (prove_property env) ps w else w in
+    let init = WpStrategy.is_main_init kf in
     let behaviors =
-      if main || WpLog.PrecondWeakening.get () then []
+      if init || WpLog.PrecondWeakening.get () then []
       else CfgAnnot.get_preconditions ~goal:false kf in
     let defaults = default_requires env.mode kf in
     let requires = bhvs.CfgAnnot.bhv_requires in
+    let initreqs = if init then requires else [] in
     let assumes = bhvs.CfgAnnot.bhv_assumes in
     (* pre-state *)
     W.label env.we None Clabels.pre @@
@@ -364,14 +336,10 @@ struct
     (* pre-conditions *)
     List.fold_right (use_property env) defaults @@
     List.fold_right (use_property env) assumes @@
-    prove_if_main requires @@
+    List.fold_right (prove_property env) initreqs @@
     List.fold_right (use_property env) requires @@
     List.fold_right (use_property env) behaviors w
 
-  let do_complete_disjoint env ~complete ~disjoint w =
-    List.fold_right (prove_property env) complete @@
-    List.fold_right (prove_property env) disjoint w
-
   let do_post env ~formals (b : CfgAnnot.behavior) w =
     W.scope env.we formals SC_Frame_out @@
     W.label env.we None Clabels.post @@
@@ -384,7 +352,7 @@ struct
     List.fold_right (prove_property env) b.bhv_exits @@
     prove_assigns env b.bhv_exit_assigns w
 
-  let do_body env ~formals (b : CfgAnnot.behavior) w =
+  let do_funbehavior env ~formals (b : CfgAnnot.behavior) w =
     let wpost = do_post env ~formals b w in
     let wexit = do_exit env ~formals b w in
     Vhash.add env.wp env.cfg.return_point (Some wpost) ;
@@ -394,27 +362,25 @@ struct
   (* Putting everything together *)
   let compute ~mode ~props =
     let kf = mode.kf in
-    let cfg = Cfg.get_automaton kf in
+    let infos = mode.infos in
+    let cfg = CfgInfos.cfg infos in
     let env = {
-      mode ; props ;
-      cfg ;
+      mode ; props ; cfg ;
       we = W.new_env kf ;
       wp = Vhash.create 32 ;
       wk = W.empty ;
     } in
-    let main = WpStrategy.is_main_init kf in
-    let formals = Kernel_function.get_formals kf in
-    let complete = complete mode kf in
-    let disjoint = disjoint mode kf in
-    let has_exit = Reachable_call.has_reachable_call cfg (cfg.entry_point) in
-    let bhv = CfgAnnot.get_behavior kf Kglobal has_exit ~active:[] mode.bhv in
-    env.we ,
-    W.close env.we @@
-    do_global_init env @@
-    do_preconditions env ~main ~formals bhv @@
-    do_complete_disjoint env ~complete ~disjoint @@
-    do_body env ~formals bhv @@
-    W.empty
+    let formals = Kf.get_formals kf in
+    let exits = not @@ Kf.Set.is_empty @@ CfgInfos.calls infos in
+    let bhv = CfgAnnot.get_behavior kf Kglobal ~exits ~active:[] mode.bhv in
+    begin
+      W.close env.we @@
+      do_global_init env @@
+      do_preconditions env ~formals bhv @@
+      do_complete_disjoint env @@
+      do_funbehavior env ~formals bhv @@
+      W.empty
+    end
 
 end
 

src/plugins/wp/cfgCalculus.mli

@@ -29,15 +29,14 @@ open Cil_types
 type mode = {
   kf : kernel_function ; (* Selected function *)
   bhv : funbehavior ; (* Selected behavior *)
+  infos : CfgInfos.t ; (* Associated infos *)
 }
 
 type props = [ `All | `Names of string list | `PropId of Property.t ]
 
 module Make(W : Mcfg.S) :
 sig
-
-  val compute : mode:mode -> props:props -> W.t_env * W.t_prop
-
+  val compute : mode:mode -> props:props -> W.t_prop
 end
 
 (* -------------------------------------------------------------------------- *)

src/plugins/wp/cfgGenerator.ml

@@ -30,15 +30,15 @@ open Wp_parameters
 module KFmap = Kernel_function.Map
 
 type task = {
-  mutable lemmas: LogicUsage.logic_lemma list ;
-  mutable modes: CfgCalculus.mode list KFmap.t ; (** TODO: when New CFG is validated, use list *)
+  mutable modes: CfgCalculus.mode list KFmap.t ;
   mutable props: CfgCalculus.props ;
+  mutable lemmas: LogicUsage.logic_lemma list ;
 }
 
 let empty () = {
   lemmas = [];
   modes = KFmap.empty;
-  props = `All ;
+  props = `All;
 }
 
 (* -------------------------------------------------------------------------- *)
@@ -73,34 +73,31 @@ let lemma task ?(prop=[]) l =
      (prop=[] || WpPropId.select_by_name prop (WpPropId.mk_lemma_id l))
   then task.lemmas <- l :: task.lemmas
 
-let apply task ~kf ?bhvs ?prop () =
+let apply task ~kf ?infos ?bhvs ?target () =
+  let infos = match infos with
+    | Some infos -> infos
+    | None -> CfgInfos.get kf () in
+  let bhvs = match bhvs with
+    | Some bhvs -> bhvs
+    | None ->
+        let bhvs = Annotations.behaviors kf in
+        if List.exists (Cil.is_default_behavior) bhvs then bhvs
+        else empty_default_behavior :: bhvs in
+  let add_mode kf m =
+    let ms = try KFmap.find kf task.modes with Not_found -> [] in
+    task.modes <- KFmap.add kf (m :: ms) task.modes in
   begin
-    let bhvs = match bhvs with
-      | Some bhvs -> bhvs
-      | None ->
-          let bhvs = Annotations.behaviors kf in
-          if List.exists (Cil.is_default_behavior) bhvs then bhvs
-          else empty_default_behavior :: bhvs
-    in
-    let add_mode kf m =
-      let modes =
-        match KFmap.find_opt kf task.modes with
-        | None -> []
-        | Some modes -> modes
-      in
-      task.modes <- KFmap.add kf (m :: modes) task.modes
-    in
-    List.iter (fun bhv -> add_mode kf { CfgCalculus.kf ; bhv }) bhvs ;
-    Option.iter (fun ip -> task.props <- `PropId ip) prop ;
+    List.iter (fun bhv -> add_mode kf CfgCalculus.{ infos ; kf ; bhv }) bhvs ;
+    Option.iter (fun ip -> task.props <- `PropId ip) target ;
   end
 
 let notyet prop =
   Wp_parameters.warning ~once:true
     "Not yet implemented wp for '%a'" Property.pretty prop
 
-let rec strategy_ip task prop =
+let rec strategy_ip task target =
   let open Property in
-  match prop with
+  match target with
   | IPLemma { il_name } ->
       lemma task (LogicUsage.logic_lemma il_name)
   | IPAxiomatic { iax_props } ->
@@ -113,43 +110,43 @@ let rec strategy_ip task prop =
         | PKRequires bhv ->
             begin
               match ki with
-              | Kglobal -> (*TODO*) notyet prop
-              | Kstmt _ -> apply task ~kf ~bhvs:[bhv] ~prop ()
+              | Kglobal -> (*TODO*) notyet target
+              | Kstmt _ -> apply task ~kf ~bhvs:[bhv] ~target ()
             end
         | PKEnsures(bhv,_) ->
-            apply task ~kf ~bhvs:[bhv] ~prop ()
+            apply task ~kf ~bhvs:[bhv] ~target ()
         | PKTerminates ->
-            apply task ~kf ~bhvs:(default kf) ~prop ()
+            apply task ~kf ~bhvs:(default kf) ~target ()
       end
   | IPDecrease { id_kf = kf } ->
-      apply task ~kf ~bhvs:(default kf) ~prop ()
+      apply task ~kf ~bhvs:(default kf) ~target ()
   | IPAssigns { ias_kf=kf ; ias_bhv=Id_loop ca }
   | IPAllocation { ial_kf=kf ; ial_bhv=Id_loop ca } ->
       let bhvs = match ca.annot_content with
         | AAssigns(bhvs,_) | AAllocation(bhvs,_) -> bhvs
         | _ -> [] in
-      apply task ~kf ~bhvs:(select kf bhvs) ~prop ()
+      apply task ~kf ~bhvs:(select kf bhvs) ~target ()
   | IPAssigns { ias_kf=kf ; ias_bhv=Id_contract(_,bhv) }
   | IPAllocation { ial_kf=kf ; ial_bhv=Id_contract(_,bhv) }
-    -> apply task ~kf ~bhvs:[bhv] ~prop ()
+    -> apply task ~kf ~bhvs:[bhv] ~target ()
   | IPCodeAnnot { ica_kf = kf ; ica_ca = ca } ->
       begin match ca.annot_content with
         | AExtended _ | APragma _ -> ()
         | AStmtSpec(fors,_) ->
-            (*TODO*) notyet prop ;
+            (*TODO*) notyet target ;
             apply task ~kf ~bhvs:(select kf fors) ()
         | AVariant _ ->
-            apply task ~kf ~prop ()
+            apply task ~kf ~target ()
         | AAssert(fors, _)
         | AInvariant(fors, _, _)
         | AAssigns(fors, _)
         | AAllocation(fors, _) ->
-            apply task ~kf ~bhvs:(select kf fors) ~prop ()
+            apply task ~kf ~bhvs:(select kf fors) ~target ()
       end
-  | IPComplete _ -> (*TODO*) notyet prop
-  | IPDisjoint _ -> (*TODO*) notyet prop
+  | IPComplete _ -> (*TODO*) notyet target
+  | IPDisjoint _ -> (*TODO*) notyet target
   | IPFrom _ | IPReachable _ | IPTypeInvariant _ | IPGlobalInvariant _
-  | IPPropertyInstance _ -> notyet prop (* ? *)
+  | IPPropertyInstance _ -> notyet target (* ? *)
   | IPExtended _ | IPAxiom _ | IPOther _ -> ()
 
 let strategy_main task ?(fct=Fct_all) ?(bhv=[]) ?(prop=[]) () =
@@ -159,9 +156,11 @@ let strategy_main task ?(fct=Fct_all) ?(bhv=[]) ?(prop=[]) () =
     Wp_parameters.iter_fct
       (fun kf ->
          if Kernel_function.has_definition kf then
-           if bhv=[]
-           then apply task ~kf ()
-           else apply task ~kf ~bhvs:(select kf bhv) ()
+           let infos = CfgInfos.get kf ~bhv ~prop () in
+           if CfgInfos.annots infos then
+             if bhv=[]
+             then apply task ~infos ~kf ()
+             else apply task ~infos ~kf ~bhvs:(select kf bhv) ()
       ) fct ;
     task.props <- (if prop=[] then `All else `Names prop);
   end
@@ -202,7 +201,8 @@ struct
                      if Cil.is_default_behavior mode.bhv then None
                      else Some mode.bhv.b_name in
                    let index = Wpo.Function(mode.kf,bhv) in
-                   let wp = snd @@ WP.compute ~mode ~props:task.props in
+                   let props = task.props in
+                   let wp = WP.compute ~mode ~props in
                    let wcs = VCG.compile_wp index wp in
                    collection := Bag.concat !collection wcs
                  end ()

src/plugins/wp/cfgInfos.ml

@@ -41,6 +41,7 @@ type t = {
 (* --- Getters                                                            --- *)
 (* -------------------------------------------------------------------------- *)
 
+let cfg infos = infos.cfg
 let calls infos = infos.calls
 let annots infos = infos.annots
 let doomed infos = infos.doomed
@@ -173,7 +174,6 @@ module Generator = WpContext.StaticGenerator(Key)
       let compile = compile
     end)
 
-let collect kf ?(bhv=[]) ?(prop=[]) () =
-  Generator.get { kf ; bhv ; prop }
+let get kf ?(bhv=[]) ?(prop=[]) () = Generator.get { kf ; bhv ; prop }
 
 (* -------------------------------------------------------------------------- *)

src/plugins/wp/cfgInfos.mli

@@ -27,9 +27,10 @@ type t
 module Cfg = Interpreted_automata
 
 (** Memoized *)
-val collect :
-  Kernel_function.t -> ?bhv:string list -> ?prop:string list -> unit -> t
+val get : Kernel_function.t -> ?bhv:string list -> ?prop:string list ->
+  unit -> t
 
+val cfg : t -> Cfg.automaton
 val annots : t -> bool
 val doomed : t -> WpPropId.prop_id Bag.t
 val calls : t -> Kernel_function.Set.t