Merge branch 'feature/kernel/asm-initialized' into 'master'

Refine contracts inferred from GNU extended asm

See merge request frama-c/frama-c!4738

src/kernel_internals/typing/asm_contracts.ml

@@ -168,6 +168,24 @@ class visit_assembly =
                (fun x -> (to_id_term x, From (List.map to_id_from lv_from)))
                lv_out)
         in
+        let mk_initialized x =
+          let typ = Cil.typeOfTermLval x in
+          if Logic_utils.isLogicVoidType typ then None
+          else begin
+            let t = Logic_utils.mk_logic_AddrOf ~loc x typ in
+            let pred =
+              Logic_const.(
+                new_predicate
+                  (pinitialized ~loc (here_label,t)))
+            in
+            Some (Normal, pred)
+          end
+        in
+        let initialized () =
+          if Kernel.AsmContractsInitialized.get() then begin
+            List.filter_map mk_initialized lv_out
+          end else []
+        in
         let filter ca =
           match ca.annot_content with
           (* search for a statement contract that applies to all cases. *)
@@ -178,7 +196,8 @@ class visit_assembly =
         (match contracts with
          | [] ->
            let assigns = assigns () in
-           let bhv = Cil.mk_behavior ~assigns () in
+           let post_cond = initialized () in
+           let bhv = Cil.mk_behavior ~assigns ~post_cond () in
            let spec = Cil.empty_funspec () in
            spec.spec_behavior <- [ bhv ];
            let ca =
@@ -192,10 +211,12 @@ class visit_assembly =
                Property.ip_assigns_of_behavior kf (Kstmt stmt) ~active bhv in
              let ip_from =
                Property.ip_from_of_behavior kf (Kstmt stmt) ~active bhv in
+             let ip_init =
+               Property.ip_ensures_of_behavior kf (Kstmt stmt) bhv
+             in
              List.iter
-               Property_status.(
-                 fun x -> emit emitter ~hyps:[] x True)
-               (Option.to_list ip_assigns @ ip_from)
+               Property_status.(fun x -> emit emitter ~hyps:[] x True)
+               (Option.to_list ip_assigns @ ip_from @ ip_init)
            end
          | [ { annot_content = AStmtSpec ([], spec) } ] ->
            (* Already existing contracts. Just add assigns clause for
@@ -236,6 +257,8 @@ let transform file =
 let () =
   File.add_code_transformation_after_cleanup
     ~deps:[(module Kernel.AsmContractsGenerate);
+           (module Kernel.AsmContractsInitialized);
            (module Kernel.AsmContractsAutoValidate) ]
+    ~before:[Inline_stmt_contracts.category]
     category
     transform

src/kernel_services/ast_transformations/inline_stmt_contracts.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2024                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Cil_types
+
+let emitter =
+  let open Emitter in
+  create
+    "inline_stmt_contract" [Code_annot; Property_status]
+    ~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 propagate_status p1 p2 =
+  match Property_status.get p1 with
+  | Best (True, _) -> Property_status.emit emitter ~hyps:[p1] p2 True
+  | _ ->
+    begin
+      let open Property_status in
+      let propagate_status_p1 e p s =
+        if Property.equal p p1 && s = True
+           && not (Emitter.(Usable_emitter.equal e.emitter (get emitter)))
+        then
+          Property_status.emit emitter ~hyps:[p1] p2 True
+      in
+      Property_status.register_status_update_hook propagate_status_p1;
+      let propagate_status_assertion e p s =
+        if Property.equal p p2 && s = Property_status.True
+           && not (Emitter.(Usable_emitter.equal e.emitter (get emitter)))
+        then
+          Property_status.emit emitter ~hyps:[p2] p1 True
+      in
+      Property_status.register_status_update_hook propagate_status_assertion
+    end
+
+let treat_behavior for_list kf 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 req =
+    let p = Logic_const.pimplies ~loc (assumes, req.ip_content.tp_statement) in
+    let ip_req = Property.ip_of_requires kf (Kstmt stmt) b req in
+    let annot = mk_annot p in
+    Annotations.add_code_annot emitter stmt annot;
+    let ip_annot = Property.ip_of_code_annot_single kf stmt annot in
+    propagate_status ip_req ip_annot
+  in
+  let treat_post_cond acc (k,p as postcond) =
+    match k with
+    | Normal ->
+      if Logic_utils.is_trivially_true assumes then begin
+        (b, postcond, mk_annot p.ip_content.tp_statement) :: acc
+      end 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
+        (b, postcond, 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
+
+let add_one_postcond kf orig_stmt new_stmt (b, post, assertion) =
+  Annotations.add_code_annot emitter ~kf new_stmt assertion;
+  let post = Property.ip_of_ensures kf (Kstmt orig_stmt) b post in
+  let assertion = Property.ip_of_code_annot_single kf new_stmt assertion in
+  propagate_status post assertion
+
+class inline_stmt_contract =
+  object(self)
+    inherit Visitor.frama_c_inplace
+    method! vstmt_aux s =
+      let loc = Cil_datatype.Stmt.loc s in
+      let kf = Option.get self#current_kf 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 kf s) [] bhvs in
+        (match posts with
+         | [] -> Cil.DoChildren
+         | _ ->
+           let nop = Cil.mkStmtOneInstr ~valid_sid:true (Skip loc) in
+           List.iter (add_one_postcond kf s 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
+           Ast.mark_as_grown ();
+           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

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2024                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** 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

@@ -1358,6 +1358,17 @@ module AsmContractsGenerate =
                   to gcc's extended syntax"
     end)
 
+let () = Parameter_customize.set_group normalisation
+module AsmContractsInitialized =
+  False
+    (struct
+      let option_name = "-asm-contracts-ensure-init"
+      let module_name = "AsmContractsInitialized"
+      let help = "when contracts for assembly code are generated, add \
+                  postconditions stating that the output are initialized."
+    end)
+
+
 let () = Parameter_customize.set_group normalisation
 module AsmContractsAutoValidate =
   False
@@ -1368,6 +1379,17 @@ 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, enabling their verification \
+                  by plug-ins with incomplete support for statement contracts."
+    end)
+
 let () = Parameter_customize.set_group normalisation
 module RemoveExn =
   False

src/kernel_services/plugin_entry_points/kernel.mli

@@ -537,8 +537,14 @@ module AggressiveMerging: Parameter_sig.Bool
 module AsmContractsGenerate: Parameter_sig.Bool
 (** Behavior of option "-asm-contracts" *)
 
+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" *)

tests/misc/asm_initialized.i

+/* run.config*
+PLUGIN: @EVA_PLUGINS@ report
+STDOPT: #"-asm-contracts-ensure-init -asm-contracts-auto-validate -inline-stmt-contracts -absolute-valid-range 0x10000000-0xf00000000 -print -report"
+*/
+
+int main() {
+  int* sp;
+  int x = 2;
+  asm volatile ("mov %%rsp, %0;":"=r"(sp));
+  *(sp - 2) = 3;
+  return x;
+}

tests/misc/oracle/asm_initialized.res.oracle

+[kernel] Parsing asm_initialized.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  NULL[rbits 2147483648 to 515396075527] ∈ [--..--]
+[eva:alarm] asm_initialized.i:9: Warning: 
+  assertion 'inline_stmt_contract' got status unknown.
+[eva:alarm] asm_initialized.i:10: Warning: 
+  out of bounds write. assert \valid(sp - 2);
+[eva] Recording results for main
+[eva] Done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  NULL[rbits 2147483648 to 515396075527] ∈ [--..--]
+  x ∈ {2}
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function main:
+  NULL[268435456..4294967298] FROM \nothing (and SELF)
+  \result FROM \nothing
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main:
+    NULL[268435456..4294967298]; x
+[inout] Inputs for function main:
+    \nothing
+[report] Computing properties status...
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'main'
+--------------------------------------------------------------------------------
+
+[  Valid  ] Post-condition (file asm_initialized.i, line 9) at assembly (file asm_initialized.i, line 9)
+            by asm_contracts.
+[  Valid  ] Assigns (file asm_initialized.i, line 9) at assembly (file asm_initialized.i, line 9)
+            by asm_contracts.
+[  Valid  ] Assertion 'inline_stmt_contract' (file asm_initialized.i, line 9)
+            by inline_stmt_contract.
+[    -    ] Assertion 'Eva,mem_access' (file asm_initialized.i, line 10)
+            tried with Eva.
+[  Valid  ] Froms (file asm_initialized.i, line 9) at assembly (file asm_initialized.i, line 9)
+            by asm_contracts.
+[  Valid  ] Default behavior at assembly (file asm_initialized.i, line 9)
+            by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Status Report Summary
+--------------------------------------------------------------------------------
+     5 Completely validated
+     1 To be validated
+     6 Total
+--------------------------------------------------------------------------------
+/* Generated by Frama-C */
+int main(void)
+{
+  int *sp;
+  int x = 2;
+  /*@ ensures \initialized(&sp);
+      assigns sp;
+      assigns sp \from \nothing; */
+  __asm__ volatile ("mov %%rsp, %0;" : "=r" (sp));
+  /*@ assert inline_stmt_contract: \initialized(&sp); */ ;
+  /*@ assert Eva: mem_access: \valid(sp - 2); */
+  *(sp - 2) = 3;
+  return x;
+}
+
+

tests/syntax/inline_stmt_contract.i

+/* run.config
+OPT: -inline-stmt-contracts -print
+*/
+
+int X;
+
+int f() {
+  /*@ requires X == 0;
+      ensures X == 1;
+  */
+  X++;
+  return X;
+}
+
+int g() {
+
+  /*@ behavior b:
+        assumes X >= 0;
+        requires X > -1;
+        ensures X == 0;
+   */
+  if (X >= 0) { X = 0; } else { X = -1; }
+  return X;
+}
+
+int h() {
+  /*@ ensures \false; */
+  return 1;
+}
+
+int i() {
+  /*@ behavior b0:
+        assumes X == 0;
+        ensures X == 1;
+  */
+  X++;
+
+  /*@ behavior b1:
+        assumes X == 1;
+        ensures X == 2;
+  */
+  X++;
+  return X;
+}

tests/syntax/oracle/inline_stmt_contract.res.oracle

+[kernel] Parsing inline_stmt_contract.i (no preprocessing)
+/* Generated by Frama-C */
+int X;
+int f(void)
+{
+  /*@ assert inline_stmt_contract: X ≡ 0; */
+  /*@ requires X ≡ 0;
+      ensures X ≡ 1; */
+  X ++;
+  /*@ assert inline_stmt_contract: X ≡ 1; */ ;
+  return X;
+}
+
+int g(void)
+{
+  __fc_inline_contract_label_0:
+  /*@ assert inline_stmt_contract: X ≥ 0 ⇒ X > -1; */
+  /*@ behavior b:
+        assumes X ≥ 0;
+        requires X > -1;
+        ensures X ≡ 0; */
+  if (X >= 0) X = 0; else X = -1;
+  /*@
+  assert
+  inline_stmt_contract: \at(X ≥ 0,__fc_inline_contract_label_0) ⇒ X ≡ 0;
+   */
+  ;
+  return X;
+}
+
+int h(void)
+{
+  int __retres;
+  /*@ ensures \false; */
+  {
+    __retres = 1;
+    goto return_label;
+  }
+  /*@ assert inline_stmt_contract: \false; */ ;
+  return_label: return __retres;
+}
+
+int i(void)
+{
+  __fc_inline_contract_label_0:
+  /*@ behavior b0:
+        assumes X ≡ 0;
+        ensures X ≡ 1; */
+  X ++;
+  /*@
+  assert
+  inline_stmt_contract: \at(X ≡ 0,__fc_inline_contract_label_0) ⇒ X ≡ 1;
+   */
+  ;
+  __fc_inline_contract_label_1:
+  /*@ behavior b1:
+        assumes X ≡ 1;
+        ensures X ≡ 2; */
+  X ++;
+  /*@
+  assert
+  inline_stmt_contract: \at(X ≡ 1,__fc_inline_contract_label_1) ⇒ X ≡ 2;
+   */
+  ;
+  return X;
+}
+
+