[kernel] first draft or inline-stmt-contracts transformation

src/kernel_services/ast_transformations/inline_stmt_contracts.ml

+open Cil_types
+
+let emitter =
+  Emitter.create
+    "inline_stmt_contract" [Emitter.Code_annot] ~correctness:[] ~tuning:[]
+
+let category = File.register_code_transformation_category "inline_stmt_contract"
+
+let fresh_pred p =
+  let v = new Visitor.frama_c_refresh (Project.current()) in
+  Visitor.visitFramacPredicate v p
+
+let nb_labels = ref 0
+
+let new_label () =
+  let res = Printf.sprintf "__fc_inline_contract_label_%d" !nb_labels in
+  incr nb_labels; res
+
+let treat_behavior for_list stmt acc b =
+  let loc = Cil_datatype.Stmt.loc stmt in
+  let pand p1 p2 = Logic_const.pand ~loc (p1,p2.ip_content.tp_statement) in
+  let assumes = List.fold_left pand Logic_const.ptrue b.b_assumes in
+  let mk_annot p =
+    let p = fresh_pred p in
+    let p = Logic_const.toplevel_predicate p in
+    Logic_const.new_code_annotation (AAssert (for_list,p))
+  in
+  let add_assert p =
+    let p = Logic_const.pimplies ~loc (assumes, p.ip_content.tp_statement) in
+    let annot = mk_annot p in
+    Annotations.add_code_annot emitter stmt annot
+  in
+  let treat_post_cond acc (k,p) =
+    match k with
+    | Normal ->
+      if Logic_utils.is_trivially_true assumes then
+        mk_annot p.ip_content.tp_statement :: acc
+      else begin
+        (match List.filter (fun l -> not (Cil.is_case_label l)) stmt.labels with
+         | [] -> stmt.labels <- Label (new_label(),loc,false) :: stmt.labels
+         | _ -> ());
+        let p =
+          Logic_const.(
+            pimplies ~loc
+              (pat ~loc (assumes,StmtLabel (ref stmt)),
+               p.ip_content.tp_statement))
+        in
+        mk_annot p :: acc
+      end
+    | _ -> acc
+  in
+  List.iter add_assert b.b_requires;
+  List.fold_left treat_post_cond acc b.b_post_cond
+
+class inline_stmt_contract =
+  object(self)
+    inherit Visitor.frama_c_inplace
+    method! vstmt_aux s =
+      let loc = Cil_datatype.Stmt.loc s in
+      match Annotations.code_annot ~filter:Logic_utils.is_contract s with
+      | [ { annot_content = AStmtSpec (l,spec) } ] ->
+        let bhvs = spec.spec_behavior in
+        let posts = List.fold_left (treat_behavior l s) [] bhvs in
+        (match posts with
+         | [] -> Cil.DoChildren
+         | _ ->
+           let nop = Cil.mkStmtOneInstr ~valid_sid:true (Skip loc) in
+           List.iter (Annotations.add_code_annot emitter nop) posts;
+           let b = Cil.mkBlockNonScoping [s; nop] in
+           let b = Cil.transient_block b in
+           let res = Cil.mkStmt ~valid_sid:true (Block b) in
+           File.must_recompute_cfg (Option.get self#current_func);
+           ChangeTo res
+        )
+      | [ _ ] -> Kernel.fatal "code annotation was expected to be a contract"
+      | _ :: _ -> Kernel.fatal "a statement can only have one contract"
+      | [] -> Cil.DoChildren
+
+    method! vfunc _ = nb_labels:= 0; Cil.DoChildren
+
+    method! vexpr _ = Cil.SkipChildren
+    method! vlval _ = Cil.SkipChildren
+    method! vtype _ = Cil.SkipChildren
+    method! vspec _ = Cil.SkipChildren
+    method! vcode_annot _ = Cil.SkipChildren
+    method! vinst _ = Cil.SkipChildren
+
+  end
+
+let inline_stmt_contract ast =
+  if Kernel.InlineStmtContracts.get () then
+    begin
+      let vis = new inline_stmt_contract in
+      Visitor.visitFramacFileSameGlobals vis ast
+    end
+
+let () =
+  let deps = [ (module Kernel.InlineStmtContracts: Parameter_sig.S) ] in
+  File.add_code_transformation_after_cleanup ~deps category inline_stmt_contract

src/kernel_services/ast_transformations/inline_stmt_contracts.mli

+(** transforms requires and ensures of statement contracts into assert.
+    This transformation is done after cleanup
+*)
+
+val emitter : Emitter.t
+val category : File.code_transformation_category

src/kernel_services/plugin_entry_points/kernel.ml

@@ -1379,6 +1379,16 @@ module AsmContractsAutoValidate =
                   (defaults to false)"
     end)
 
+let () = Parameter_customize.set_group normalisation
+module InlineStmtContracts =
+  False
+    (struct
+      let option_name = "-inline-stmt-contracts"
+      let module_name = "InlineStmtContracts"
+      let help = "transforms requires/ensures clauses of statement contracts \
+                  into plain assertions"
+    end)
+
 let () = Parameter_customize.set_group normalisation
 module RemoveExn =
   False

src/kernel_services/plugin_entry_points/kernel.mli

@@ -541,7 +541,10 @@ module AsmContractsInitialized: Parameter_sig.Bool
 (** Behavior of option "-asm-contracts-ensure-init" *)
 
 module AsmContractsAutoValidate: Parameter_sig.Bool
-(** Behavior of option "-asm-contracts-auto-validate." *)
+(** Behavior of option "-asm-contracts-auto-validate" *)
+
+module InlineStmtContracts: Parameter_sig.Bool
+(** Behavior of option "-inline-stmt-contracts" *)
 
 module RemoveExn: Parameter_sig.Bool
 (** Behavior of option "-remove-exn" *)