[wp] refactor function-body

src/plugins/wp/cfgCalculus.ml

@@ -129,7 +129,8 @@ struct
   type env = {
     mode: mode;
     props: props;
-    cfg: Cfg.automaton option;
+    body: Cfg.automaton option;
+    succ: Cfg.vertex -> Cfg.G.edge list;
     we: W.t_env;
     wp: W.t_prop option Vhash.t; (* None is used for non-dag detection *)
     mutable wk: W.t_prop; (* end point *)
@@ -179,8 +180,6 @@ struct
 
   exception NonNaturalLoop
 
-  let succ env a = G.succ_e (Option.get env.cfg).graph a
-
   let rec wp (env:env) (a:vertex) : W.t_prop =
     match Vhash.find env.wp a with
     | None -> raise NonNaturalLoop
@@ -240,7 +239,7 @@ struct
     W.merge env.we established presersed
 
   (* Merge transitions *)
-  and successors env (a : vertex) = transitions env (succ env a)
+  and successors env (a : vertex) = transitions env (env.succ a)
   and transitions env (es : G.edge list) = fmerge env (transition env) es
   and transition env (_,edge,dst) : W.t_prop =
     let p = wp env dst in
@@ -355,21 +354,26 @@ struct
     List.fold_right (prove_property env) b.bhv_exits @@
     prove_assigns env b.bhv_exit_assigns w
 
-  let do_funbehavior env ~formals (b : CfgAnnot.behavior) w =
-    let cfg = Option.get env.cfg in
-    let wpost = do_post env ~formals b w in
-    let wexit = do_exit env ~formals b w in
-    Vhash.add env.wp cfg.return_point (Some wpost) ;
-    env.wk <- wexit ;
-    wp env cfg.entry_point
+  let do_funbehavior env ~formals (b:CfgAnnot.behavior) w =
+    match env.body with
+    | None -> w
+    | Some cfg ->
+        let wpost = do_post env ~formals b w in
+        let wexit = do_exit env ~formals b w in
+        Vhash.add env.wp cfg.return_point (Some wpost) ;
+        env.wk <- wexit ;
+        wp env cfg.entry_point
 
   (* Putting everything together *)
   let compute ~mode ~props =
     let kf = mode.kf in
     let infos = mode.infos in
-    let cfg = CfgInfos.cfg infos in
+    let body = CfgInfos.body infos in
+    let succ = match body with
+      | None -> (fun _ -> [])
+      | Some cfg -> Cfg.G.succ_e cfg.graph in
     let env = {
-      mode ; props ; cfg ;
+      mode ; props ; body ; succ ;
       we = W.new_env kf ;
       wp = Vhash.create 32 ;
       wk = W.empty ;
@@ -382,9 +386,7 @@ struct
       do_global_init env @@
       do_preconditions env ~formals bhv @@
       do_complete_disjoint env @@
-      (if Kernel_function.has_definition kf
-       then do_funbehavior env ~formals bhv
-       else Extlib.id) @@
+      do_funbehavior env ~formals bhv @@
       W.empty
     end
 

src/plugins/wp/cfgInfos.ml

@@ -31,7 +31,7 @@ module Shash = Cil_datatype.Stmt.Hashtbl
 module Reachability = Graph.Path.Check(Cfg.G)
 
 type t = {
-  cfg : Cfg.automaton option ;
+  body : Cfg.automaton option ;
   reachability : Reachability.path_checker option ;
   mutable annots : bool; (* has goals to prove *)
   mutable doomed : WpPropId.prop_id Bag.t;
@@ -42,15 +42,17 @@ type t = {
 (* --- Getters                                                            --- *)
 (* -------------------------------------------------------------------------- *)
 
-let cfg infos = infos.cfg
+let body infos = infos.body
 let calls infos = infos.calls
 let annots infos = infos.annots
 let doomed infos = infos.doomed
 
 let unreachable infos v =
-  let reachability = Option.get infos.reachability in
-  let entry = (Option.get infos.cfg).entry_point in
-  not @@ Reachability.check_path reachability entry v
+  match infos.body, infos.reachability with
+  | Some cfg , Some reach ->
+      let entry = cfg.entry_point in
+      not @@ Reachability.check_path reach entry v
+  | _ -> true
 
 (* -------------------------------------------------------------------------- *)
 (* --- Selected Properties                                                --- *)
@@ -191,51 +193,52 @@ let loop_contract_pids kf stmt =
   | _ -> []
 
 let compile Key.{ kf ; bhv ; prop } =
-  let cfg, reachability =
+  let body, reachability =
     if Kernel_function.has_definition kf then
       let cfg = Cfg.get_automaton kf in
       Some cfg, Some (Reachability.create cfg.graph)
     else None, None
   in
   let infos = {
-    cfg ;
+    body ;
     annots = false ;
     doomed = Bag.empty ;
     calls = Fset.empty ;
-    reachability
+    reachability ;
   } in
   let behaviors = Annotations.behaviors kf in
+  (* Inits *)
   if WpStrategy.is_main_init kf then
     infos.annots <- List.exists (selected_main_bhv ~bhv ~prop) behaviors ;
-
-  if Kernel_function.has_definition kf then begin
-    let cfg = Option.get cfg in
-    (* Spec Iteration *)
-    if selected_disjoint_complete kf ~bhv ~prop ||
-       (List.exists (selected_bhv ~bhv ~prop) behaviors)
-    then infos.annots <- true ;
-    (* Stmt Iteration *)
-    Shash.iter
-      (fun stmt (src,_) ->
-         let fs = collect_calls ~bhv stmt in
-         let dead = unreachable infos src in
-         let ca = CfgAnnot.get_code_assertions kf stmt in
-         let ca_pids = List.map fst ca.code_verified in
-         let loop_pids = loop_contract_pids kf stmt in
-         if dead then begin
-           infos.doomed <- Bag.concat infos.doomed (Bag.list ca_pids) ;
-           infos.doomed <- Bag.concat infos.doomed (Bag.list loop_pids) ;
-         end else
-           begin
-             if not infos.annots &&
-                ( List.exists (selected ~bhv ~prop) ca_pids ||
-                  List.exists (selected ~bhv ~prop) loop_pids ||
-                  Fset.exists (selected_call ~bhv ~prop) fs )
-             then infos.annots <- true ;
-             infos.calls <- Fset.union fs infos.calls ;
-           end
-      ) cfg.stmt_table ;
-  end ;
+  (* Function Body *)
+  Option.iter
+    begin fun (cfg : Cfg.automaton) ->
+      (* Spec Iteration *)
+      if selected_disjoint_complete kf ~bhv ~prop ||
+         (List.exists (selected_bhv ~bhv ~prop) behaviors)
+      then infos.annots <- true ;
+      (* Stmt Iteration *)
+      Shash.iter
+        (fun stmt (src,_) ->
+           let fs = collect_calls ~bhv stmt in
+           let dead = unreachable infos src in
+           let ca = CfgAnnot.get_code_assertions kf stmt in
+           let ca_pids = List.map fst ca.code_verified in
+           let loop_pids = loop_contract_pids kf stmt in
+           if dead then begin
+             infos.doomed <- Bag.concat infos.doomed (Bag.list ca_pids) ;
+             infos.doomed <- Bag.concat infos.doomed (Bag.list loop_pids) ;
+           end else
+             begin
+               if not infos.annots &&
+                  ( List.exists (selected ~bhv ~prop) ca_pids ||
+                    List.exists (selected ~bhv ~prop) loop_pids ||
+                    Fset.exists (selected_call ~bhv ~prop) fs )
+               then infos.annots <- true ;
+               infos.calls <- Fset.union fs infos.calls ;
+             end
+        ) cfg.stmt_table ;
+    end body ;
   (* Collected Infos *)
   infos
 

src/plugins/wp/cfgInfos.mli

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