[wp] applies function contract

src/plugins/wp/cfgCalculus.ml

@@ -61,6 +61,13 @@ let get_modes kf =
          ) stmt ms
     ) (Kernel_function.get_definition kf).sallstmts []
 
+let get_default_requires mode kf =
+  if Cil.is_default_behavior mode.bhv then [] else
+    try
+      let bhv = List.find Cil.is_default_behavior (Annotations.behaviors kf) in
+      WpAnnot.get_requires kf Kglobal bhv
+    with Not_found -> []
+
 (* -------------------------------------------------------------------------- *)
 (* --- Property Selection by Mode                                         --- *)
 (* -------------------------------------------------------------------------- *)
@@ -127,6 +134,7 @@ struct
     cfg: Cfg.automaton;
     we: M.t_env;
     wp: M.t_prop option Vhash.t; (* None is used for non-dag detection *)
+    mutable wk: M.t_prop; (* end point *)
   }
 
   (* --- Annotation Helpers --- *)
@@ -138,17 +146,17 @@ struct
         let cup = M.merge env.we in
         List.fold_left (fun p y -> cup (f y) p) (f x) xs
 
+  let is_selected ~goal { mode ; props } (pid,_) =
+    (is_selected_property ~goal mode @@ WpPropId.property_of_id pid)
+    && (not goal || props = [] || WpPropId.select_by_name props pid)
+
   let use_assigns env (a : assigns) w =
     match a with
     | NoAssignsInfo -> assert false
     | AssignsAny ad -> M.use_assigns env.we None ad w
     | AssignsLocations(ap,ad) -> M.use_assigns env.we (Some ap) ad w
 
-  let is_selected ~goal { mode ; props } (pid,_) =
-    (is_selected_property ~goal mode @@ WpPropId.property_of_id pid)
-    && (not goal || props = [] || WpPropId.select_by_name props pid)
-
-  let check_assigns env (a : assigns) w =
+  let prove_assigns env (a : assigns) w =
     match a with
     | NoAssignsInfo | AssignsAny _ -> w
     | AssignsLocations ai ->
@@ -224,7 +232,7 @@ struct
       let q =
         M.label env.we None (Clabels.loop_current s) @@
         List.fold_right (prove_property env) lc.loop_preserved @@
-        List.fold_right (check_assigns env) lc.loop_assigns @@
+        List.fold_right (prove_assigns env) lc.loop_assigns @@
         M.empty in
       ( Vhash.replace env.wp a (Some q) ; successors env a )
     end
@@ -256,9 +264,12 @@ struct
         M.use_assigns env.we None (WpPropId.mk_asm_assigns_desc s) p
     | Call _ -> assert false
 
-  let return env (p : M.t_prop) : vertex =
-    Vhash.add env.wp env.cfg.return_point (Some p) ;
-    env.cfg.entry_point
+  let body env ~ensures ~exits w =
+    let rw = List.fold_right (prove_property env) ensures w in
+    let rk = List.fold_right (prove_property env) exits w in
+    Vhash.add env.wp env.cfg.return_point (Some rw) ;
+    env.wk <- rk ;
+    wp env env.cfg.entry_point
 
   (* Putting everything together *)
   let compute ~mode ~props kf =
@@ -267,16 +278,29 @@ struct
       cfg = Cfg.get_automaton kf ;
       we = M.new_env kf ;
       wp = Vhash.create 32 ;
+      wk = M.empty ;
     } in
     let xs = Kernel_function.get_formals kf in
+    let req = get_default_requires mode kf in
+    let bhv = WpAnnot.get_behavior kf Kglobal ~active:[] mode.bhv in
     env.we ,
+    (* global *)
     M.scope env.we [] SC_Global @@
+    (* pre-state *)
     M.label env.we None Clabels.pre @@
-    (*TODO: add function requires *)
+    List.fold_right (use_property env) req @@
+    List.fold_right (use_property env) bhv.bhv_assumes @@
+    List.fold_right (use_property env) bhv.bhv_requires @@
+    (* frame-in *)
     M.scope env.we xs SC_Frame_in @@
-    wp env @@
-    return env @@
+    (* function body *)
+    body env
+      ~ensures:bhv.bhv_ensures
+      ~exits:bhv.bhv_exits @@
+    (* frame-out *)
     M.scope env.we xs SC_Frame_out @@
+    prove_assigns env bhv.bhv_assigns @@
+    (* wp-end *)
     M.empty
 
 end

src/plugins/wp/wpAnnot.ml

@@ -197,36 +197,61 @@ type behavior = {
   bhv_requires: WpPropId.pred_info list ;
   bhv_ensures: WpPropId.pred_info list ;
   bhv_exits: WpPropId.pred_info list ;
-  bhv_assigns: WpPropId.assigns_full_info list ;
+  bhv_assigns: WpPropId.assigns_full_info ;
 }
 
-let get_behavior kf ki bhv =
+let normalize_pre kf ki bhv ip =
   let module L = NormAtLabels in
-  let normalize_pre ip =
-    let labels =
-      match ki with
-      | Kglobal -> L.labels_fct_pre
-      | Kstmt s -> L.labels_stmt_pre kf s in
-    WpPropId.mk_pre_id kf ki bhv ip ,
-    L.preproc_annot labels ip.ip_content.tp_statement
-  in
-  let normalize_post tk ip =
-    let labels =
-      match ki with
-      | Kglobal -> L.labels_fct_pre
-      | Kstmt s -> L.labels_stmt_post kf s in
-    WpPropId.mk_post_id kf ki bhv (tk,ip) ,
-    L.preproc_annot labels ip.ip_content.tp_statement
-  in
-  let post_cond tk = List.filter_map (fun (kind,ip) ->
-      if kind = tk then Some (normalize_post tk ip) else None
-    ) bhv.b_post_cond
-  in {
-    bhv_assumes = List.map normalize_pre bhv.b_assumes;
-    bhv_requires = List.map normalize_pre bhv.b_requires;
-    bhv_ensures = post_cond Normal ;
-    bhv_exits = post_cond Exits ;
-    bhv_assigns = [];
+  let labels =
+    match ki with
+    | Kglobal -> L.labels_fct_pre
+    | Kstmt s -> L.labels_stmt_pre kf s in
+  WpPropId.mk_pre_id kf ki bhv ip ,
+  L.preproc_annot labels ip.ip_content.tp_statement
+
+let normalize_post kf ki bhv tk ip =
+  let module L = NormAtLabels in
+  let labels =
+    match ki with
+    | Kglobal -> L.labels_fct_pre
+    | Kstmt s -> L.labels_stmt_post kf s in
+  WpPropId.mk_post_id kf ki bhv (tk,ip) ,
+  L.preproc_annot labels ip.ip_content.tp_statement
+
+let normalize_assigns kf ki bhv ~active = function
+  | WritesAny -> WpPropId.empty_assigns_info
+  | Writes froms ->
+      let module L = NormAtLabels in
+      let aid = match ki with
+        | Kglobal -> WpPropId.mk_fct_assigns_id kf bhv Normal froms
+        | Kstmt s -> WpPropId.mk_stmt_assigns_id kf s active bhv froms in
+      match aid with
+      | None -> WpPropId.empty_assigns_info
+      | Some id ->
+          let labels =
+            match ki with
+            | Kglobal -> L.labels_fct_assigns
+            | Kstmt s -> L.labels_stmt_assigns kf s in
+          let assigns = L.preproc_assigns labels froms in
+          let desc = match ki with
+            | Kglobal -> WpPropId.mk_kf_assigns_desc assigns
+            | Kstmt s -> WpPropId.mk_stmt_assigns_desc s assigns
+          in  WpPropId.mk_assigns_info id desc
+
+let get_requires kf ki bhv =
+  List.map (normalize_pre kf ki bhv) bhv.b_requires
+
+let get_behavior kf ki ~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 assigns = normalize_assigns kf ki bhv ~active bhv.b_assigns in
+  {
+    bhv_assumes = List.map pre_cond bhv.b_assumes;
+    bhv_requires = List.map pre_cond bhv.b_requires;
+    bhv_ensures = List.filter_map (post_cond Normal) bhv.b_post_cond ;
+    bhv_exits = List.filter_map (post_cond Exits) bhv.b_post_cond ;
+    bhv_assigns = assigns ;
   }
 
 (* -------------------------------------------------------------------------- *)

src/plugins/wp/wpAnnot.mli

@@ -25,16 +25,17 @@
   * is allowed to use. *)
 
 open Cil_types
+open WpPropId
 
 (*----------------------------------------------------------------------------*)
 
 (** A proof accumulator for a set of related prop_id *)
 type proof
 
-val create_proof : WpPropId.prop_id -> proof
+val create_proof : prop_id -> proof
 (** to be used only once for one of the related prop_id *)
 
-val add_proof : proof -> WpPropId.prop_id -> Property.t list -> unit
+val add_proof : proof -> prop_id -> Property.t list -> unit
 (** accumulate in the proof the partial proof for this prop_id *)
 
 val add_invalid_proof : proof -> unit
@@ -52,7 +53,7 @@ val is_invalid : proof -> bool
 val target : proof -> Property.t
 val dependencies : proof -> Property.t list
 
-val filter_status : WpPropId.prop_id -> bool
+val filter_status : prop_id -> bool
 
 (* -------------------------------------------------------------------------- *)
 (* --- Property Accessors : Function Calls                                --- *)
@@ -68,22 +69,24 @@ val get_called_assigns : kernel_function -> Property.t list
 (* -------------------------------------------------------------------------- *)
 
 type behavior = {
-  bhv_assumes: WpPropId.pred_info list ;
-  bhv_requires: WpPropId.pred_info list ;
-  bhv_ensures: WpPropId.pred_info list ;
-  bhv_exits: WpPropId.pred_info list ;
-  bhv_assigns: WpPropId.assigns_full_info list;
+  bhv_assumes: pred_info list ;
+  bhv_requires: pred_info list ;
+  bhv_ensures: pred_info list ;
+  bhv_exits: pred_info list ;
+  bhv_assigns: assigns_full_info ;
 }
 
-val get_behavior : kernel_function -> kinstr -> funbehavior -> behavior
+val get_requires : kernel_function -> kinstr -> funbehavior -> pred_info list
+val get_behavior : kernel_function -> kinstr -> active:string list ->
+  funbehavior -> behavior
 
 (* -------------------------------------------------------------------------- *)
 (* --- Property Accessors : Assertions                                    --- *)
 (* -------------------------------------------------------------------------- *)
 
 type code_assertions = {
-  code_admitted: WpPropId.pred_info list ;
-  code_verified: WpPropId.pred_info list ;
+  code_admitted: pred_info list ;
+  code_verified: pred_info list ;
 }
 
 val get_code_assertions : kernel_function -> stmt -> code_assertions
@@ -94,13 +97,13 @@ val get_code_assertions : kernel_function -> stmt -> code_assertions
 
 type loop_contract = {
   (** to be verified at loop entry *)
-  loop_established: WpPropId.pred_info list;
+  loop_established: pred_info list;
   (** to be assumed for loop current *)
-  loop_invariants: WpPropId.pred_info list;
+  loop_invariants: pred_info list;
   (** to be verified after loop body *)
-  loop_preserved: WpPropId.pred_info list;
+  loop_preserved: pred_info list;
   (** assigned by loop body *)
-  loop_assigns: WpPropId.assigns_full_info list;
+  loop_assigns: assigns_full_info list;
 }
 
 val get_loop_contract : kernel_function -> stmt -> loop_contract