[wp] compute modes for new calculus

src/libraries/utils/bag.mli

@@ -36,6 +36,7 @@ val concat : 'a t -> 'a t -> 'a t
 
 val map : ('a -> 'b) -> 'a t -> 'b t
 val umap : ('a -> 'b t) -> 'a t -> 'b t
+val umap_list : ('a -> 'b t) -> 'a list -> 'b t
 
 val iter : ('a -> unit) -> 'a t -> unit
 val fold_left : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b

src/plugins/wp/Generator.ml

@@ -67,17 +67,19 @@ let create
   let legacy = default Wp_parameters.Dump.get legacy in
   let driver = default Driver.load_driver driver in
   let setup = default user_setup setup in
-  ignore legacy ;
-  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
+  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
+    CfgGenerator.generator setup driver
 
 (* -------------------------------------------------------------------------- *)

src/plugins/wp/cfgCalculus.ml

@@ -40,37 +40,12 @@ type assigns = WpPropId.assigns_full_info
 (* -------------------------------------------------------------------------- *)
 
 type mode = {
+  kf: kernel_function;
   bhv : funbehavior ; (* Selected behavior (None is default) *)
-  stmt : stmt option ;  (* Stmt contract under proof *)
 }
 
 type props = [ `All | `Names of string list | `PropId of Property.t ]
 
-module MODES = WpContext.StaticGenerator(Kernel_function)
-    (struct
-      type key = kernel_function
-      type data = mode list
-      let name = "Wp.CfgCalculus.Modes"
-      let compile kf =
-        Annotations.fold_behaviors
-          (fun _emitter bhv ms -> { bhv ; stmt = None } :: ms)
-          kf @@
-        List.fold_right
-          (fun stmt ms ->
-             Annotations.fold_code_annot (fun _emitter ca ms ->
-                 match ca.annot_content with
-                 | AStmtSpec(_, { spec_behavior = bs } ) ->
-                     List.fold_right (fun bhv ms -> {
-                           bhv ;
-                           stmt = Some stmt ;
-                         }::ms) bs ms
-                 | _ -> ms
-               ) stmt ms
-          ) (Kernel_function.get_definition kf).sallstmts []
-    end)
-
-let modes = MODES.get
-
 let default_requires mode kf =
   if Cil.is_default_behavior mode.bhv then [] else
     try
@@ -139,10 +114,8 @@ struct
   (* --- Traversal Environment --- *)
 
   type env = {
-    kf: kernel_function;
     mode: mode;
     props: props;
-    mutable ki: kinstr; (* Current localisation *)
     cfg: Cfg.automaton;
     we: W.t_env;
     wp: W.t_prop option Vhash.t; (* None is used for non-dag detection *)
@@ -189,13 +162,13 @@ struct
 
   (* --- Decomposition of WP Rules --- *)
 
-  exception NonNaturalLoop of kernel_function * kinstr
+  exception NonNaturalLoop
 
   let succ env a = G.succ_e env.cfg.graph a
 
   let rec wp (env:env) (a:vertex) : W.t_prop =
     match Vhash.find env.wp a with
-    | None -> raise (NonNaturalLoop(env.kf,env.ki))
+    | None -> raise NonNaturalLoop
     | Some pi -> pi
     | exception Not_found ->
         (* cut circularities *)
@@ -207,23 +180,19 @@ struct
 
   (* Compute a stmt node *)
   and stmt env a (s: stmt) : W.t_prop =
-    let ki = env.ki in
     let kl = Cil.CurrentLoc.get () in
     try
-      env.ki <- Kstmt s ;
       Cil.CurrentLoc.set (Stmt.loc s) ;
-      let ca = CfgAnnot.get_code_assertions env.kf s in
+      let ca = CfgAnnot.get_code_assertions env.mode.kf s in
       let pi =
         W.label env.we (Some s) (Clabels.stmt s) @@
         List.fold_right (prove_property env) ca.code_verified @@
         List.fold_right (use_property env) ca.code_admitted @@
         control env a s
       in
-      Cil.CurrentLoc.set kl ;
-      env.ki <- ki ; pi
+      Cil.CurrentLoc.set kl ; pi
     with err ->
-      Cil.CurrentLoc.set kl ;
-      env.ki <- ki ; raise err
+      Cil.CurrentLoc.set kl ; raise err
 
   (* Branching wrt control-flow *)
   and control env a s : W.t_prop =
@@ -234,7 +203,7 @@ struct
         W.switch env.we s value
           (List.map (fun (e,v) -> [e], wp env v) cases)
           (wp env default)
-    | Loop _ -> loop env a s (CfgAnnot.get_loop_contract env.kf s)
+    | Loop _ -> loop env a s (CfgAnnot.get_loop_contract env.mode.kf s)
     | Edges -> successors env a
 
   (* Compute loops *)
@@ -322,21 +291,21 @@ struct
     wp env env.cfg.entry_point
 
   (* Putting everything together *)
-  let compute ~mode ~props kf =
+  let compute ~mode ~props =
     let env = {
-      kf ; ki = Kglobal ; mode ; props ;
-      cfg = Cfg.get_automaton kf ;
-      we = W.new_env kf ;
+      mode ; props ;
+      cfg = Cfg.get_automaton mode.kf ;
+      we = W.new_env mode.kf ;
       wp = Vhash.create 32 ;
       wk = W.empty ;
     } in
-    let xs = Kernel_function.get_formals kf in
-    let req = default_requires mode kf in
-    let bhv = CfgAnnot.get_behavior kf Kglobal ~active:[] mode.bhv in
+    let xs = Kernel_function.get_formals mode.kf in
+    let req = default_requires mode mode.kf in
+    let bhv = CfgAnnot.get_behavior mode.kf Kglobal ~active:[] mode.bhv in
     env.we ,
     (* global init *)
     W.close env.we @@
-    I.process_global_init env.we kf @@
+    I.process_global_init env.we mode.kf @@
     W.scope env.we [] SC_Global @@
     (* pre-state *)
     W.label env.we None Clabels.pre @@

src/plugins/wp/cfgCalculus.mli

@@ -27,20 +27,16 @@ open Cil_types
 (* -------------------------------------------------------------------------- *)
 
 type mode = {
-  bhv : funbehavior ; (* Selected behavior (None is default) *)
-  stmt : stmt option ;  (* Stmt contract under proof *)
+  kf : kernel_function ; (* Selected function *)
+  bhv : funbehavior ; (* Selected behavior *)
 }
 
 type props = [ `All | `Names of string list | `PropId of Property.t ]
 
-(* Memoized *)
-val modes : kernel_function -> mode list
-
 module Make(W : Mcfg.S) :
 sig
 
-  val compute : mode:mode -> props:props -> kernel_function ->
-    W.t_env * W.t_prop
+  val compute : mode:mode -> props:props -> W.t_env * W.t_prop
 
 end
 

src/plugins/wp/cfgGenerator.ml

@@ -20,6 +20,170 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Cil_types
+open Wp_parameters
+
+(* -------------------------------------------------------------------------- *)
+(* --- Task Manager                                                       --- *)
+(* -------------------------------------------------------------------------- *)
+
+type task = {
+  mutable lemmas: LogicUsage.logic_lemma list ;
+  mutable modes: CfgCalculus.mode list ;
+  mutable props: CfgCalculus.props ;
+}
+
+let empty () = {
+  lemmas = [];
+  modes = [];
+  props = `All ;
+}
+
+(* -------------------------------------------------------------------------- *)
+(* --- Property Guided Selection                                          --- *)
+(* -------------------------------------------------------------------------- *)
+
+let default kf =
+  List.filter
+    Cil.is_default_behavior
+    (Annotations.behaviors kf)
+
+let select kf bnames =
+  List.filter
+    (fun b -> List.mem b.b_name bnames)
+    (Annotations.behaviors kf)
+
+let apply task ~kf ?bhvs ?prop () =
+  begin
+    let bhvs = match bhvs with
+      | None -> Annotations.behaviors kf
+      | Some bhvs -> bhvs in
+    List.iter (fun bhv ->
+        task.modes <- { kf ; bhv } :: task.modes
+      ) bhvs ;
+    Extlib.may (fun ip -> task.props <- `PropId ip) prop ;
+  end
+
+let notyet prop =
+  Wp_parameters.warning ~once:true
+    "Not yet implemented wp for '%a'" Property.pretty prop
+
+let rec strategy task prop =
+  let open Property in
+  match prop with
+  | IPLemma { il_name } ->
+      let l = LogicUsage.logic_lemma il_name in
+      task.lemmas <- l :: task.lemmas
+  | IPAxiomatic { iax_props } ->
+      List.iter (strategy task) iax_props
+  | IPBehavior { ib_kf = kf ; ib_bhv = bhv } ->
+      apply task ~kf ~bhvs:[bhv] ()
+  | IPPredicate { ip_kf = kf ; ip_kind ; ip_kinstr = ki } ->
+      begin match ip_kind with
+        | PKAssumes _ -> ()
+        | PKRequires bhv ->
+            begin
+              match ki with
+              | Kglobal -> (*TODO*) notyet prop
+              | Kstmt _ -> apply task ~kf ~bhvs:[bhv] ~prop ()
+            end
+        | PKEnsures(bhv,_) ->
+            apply task ~kf ~bhvs:[bhv] ~prop ()
+        | PKTerminates ->
+            apply task ~kf ~bhvs:(default kf) ~prop ()
+      end
+  | IPDecrease { id_kf = kf } ->
+      apply task ~kf ~bhvs:(default kf) ~prop ()
+  | 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 ()
+  | IPAssigns { ias_kf=kf ; ias_bhv=Id_contract(_,bhv) }
+  | IPAllocation { ial_kf=kf ; ial_bhv=Id_contract(_,bhv) }
+    -> apply task ~kf ~bhvs:[bhv] ~prop ()
+  | IPCodeAnnot { ica_kf = kf ; ica_ca = ca } ->
+      begin match ca.annot_content with
+        | AExtended _ | APragma _ -> ()
+        | AStmtSpec(fors,_) ->
+            (*TODO*) notyet prop ;
+            apply task ~kf ~bhvs:(select kf fors) ()
+        | AVariant _ ->
+            apply task ~kf ~prop ()
+        | AAssert(fors, _)
+        | AInvariant(fors, _, _)
+        | AAssigns(fors, _)
+        | AAllocation(fors, _) ->
+            apply task ~kf ~bhvs:(select kf fors) ~prop ()
+      end
+  | IPComplete _ -> (*TODO*) notyet prop
+  | IPDisjoint _ -> (*TODO*) notyet prop
+  | IPFrom _ | IPReachable _ | IPTypeInvariant _ | IPGlobalInvariant _
+  | IPPropertyInstance _ -> notyet prop (* ? *)
+  | IPExtended _ | IPAxiom _ | IPOther _ -> ()
+
+(* -------------------------------------------------------------------------- *)
+(* --- Compute All Tasks                                                  --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Make(VCG : CfgWP.VCgen) =
+struct
+
+  module WP = CfgCalculus.Make(VCG)
+
+  let compute model task =
+    begin
+      let collection = ref Bag.empty in
+      Lang.F.release () ;
+      if task.lemmas <> [] then
+        WpContext.on_context (model,WpContext.Global)
+          begin fun () ->
+            LogicUsage.iter_lemmas VCG.register_lemma ;
+            List.iter (fun l ->
+               let wpo = VCG.compile_lemma l in
+               collection := Bag.add wpo !collection
+              ) task.lemmas ;
+          end () ;
+      List.iter
+        (fun (mode : CfgCalculus.mode) ->
+           WpContext.on_context (model,WpContext.Kf mode.kf)
+             begin fun () ->
+               let wp = snd @@ WP.compute ~mode ~props:task.props in
+               let bhv =
+                 if Cil.is_default_behavior mode.bhv then None
+                 else Some mode.bhv.b_name in
+               let index = Wpo.Function(mode.kf,bhv) in
+               let wcs = VCG.compile_wp index wp in
+               collection := Bag.concat !collection wcs
+             end ()
+        ) task.modes ;
+      !collection
+    end
+
+  let compute_ip model ip =
+    let task = empty () in
+    strategy task ip ;
+    compute model task
+
+  let compute_call _model _stmt =
+    Wp_parameters.warning
+      ~once:true "Not yet implemented call preconds" ;
+    Bag.empty
+
+  let compute_main model ?(fct=Fct_all) ?bhv ?prop () =
+    let task = empty () in
+    Wp_parameters.iter_fct
+      (fun kf ->
+         match bhv with
+         | None -> apply task ~kf ()
+         | Some bs -> apply task ~kf ~bhvs:(select kf bs) ()
+      ) fct ;
+    task.props <- (match prop with None -> `All | Some ps -> `Names ps) ;
+    compute model task
+
+end
+
 (* -------------------------------------------------------------------------- *)
 (* --- New WP Computer (main entry points)                                --- *)
 (* -------------------------------------------------------------------------- *)
@@ -31,17 +195,13 @@ let generator setup driver =
   try WpContext.MINDEX.find generators model
   with Not_found ->
     let module VCG = (val CfgWP.vcgen setup driver) in
-    let module WP = CfgCalculus.Make(VCG) in
+    let module CC = Make(VCG) in
     let generator : Wpo.generator =
       object
         method model = model
-        method compute_ip _ = Bag.empty
-        method compute_call _ = Bag.empty
-        method compute_main ?fct ?bhv ?prop () =
-          ignore fct ;
-          ignore bhv ;
-          ignore prop ;
-          Bag.empty
+        method compute_ip = CC.compute_ip model
+        method compute_call = CC.compute_call model
+        method compute_main = CC.compute_main model
       end in
     WpContext.MINDEX.add generators model generator ;
     generator