diff --git a/src/kernel_internals/typing/asm_contracts.ml b/src/kernel_internals/typing/asm_contracts.ml
index 0d644c1604bca7cbcd6c9884a42c841783aaff8d..7814244c441c49544c5f306d25c8831af18fcef0 100644
--- a/src/kernel_internals/typing/asm_contracts.ml
+++ b/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
diff --git a/src/kernel_services/ast_transformations/inline_stmt_contracts.ml b/src/kernel_services/ast_transformations/inline_stmt_contracts.ml
new file mode 100644
index 0000000000000000000000000000000000000000..710fe1051385b63769a000dea1fac068a0ffa118
--- /dev/null
+++ b/src/kernel_services/ast_transformations/inline_stmt_contracts.ml
@@ -0,0 +1,156 @@
+(**************************************************************************)
+(* *)
+(* 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
diff --git a/src/kernel_services/ast_transformations/inline_stmt_contracts.mli b/src/kernel_services/ast_transformations/inline_stmt_contracts.mli
new file mode 100644
index 0000000000000000000000000000000000000000..5bb3bdd9fa4fc3ecb2288e18abf275ea4bb12d3b
--- /dev/null
+++ b/src/kernel_services/ast_transformations/inline_stmt_contracts.mli
@@ -0,0 +1,28 @@
+(**************************************************************************)
+(* *)
+(* 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
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 4efe6d0b8ea0372cef138879add02e3d15026285..e704803c577786149f2a0174d9f55535a104dc1b 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/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
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 952d796c3e825e0ac777949d7383b19693174995..8472baa286db098f13eb54ced7bb331744d3f3e5 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/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" *)
diff --git a/tests/misc/asm_initialized.i b/tests/misc/asm_initialized.i
new file mode 100644
index 0000000000000000000000000000000000000000..b0b3d60f4f4820d1157edd9136bf1c29fd26520e
--- /dev/null
+++ b/tests/misc/asm_initialized.i
@@ -0,0 +1,12 @@
+/* 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;
+}
diff --git a/tests/misc/oracle/asm_initialized.res.oracle b/tests/misc/oracle/asm_initialized.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..2d450df9513cfe5447010f99a6c95454dfd27dd3
--- /dev/null
+++ b/tests/misc/oracle/asm_initialized.res.oracle
@@ -0,0 +1,70 @@
+[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;
+}
+
+
diff --git a/tests/syntax/inline_stmt_contract.i b/tests/syntax/inline_stmt_contract.i
new file mode 100644
index 0000000000000000000000000000000000000000..551a6c461a02df52d91495bef90d65cbd08fded5
--- /dev/null
+++ b/tests/syntax/inline_stmt_contract.i
@@ -0,0 +1,44 @@
+/* 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;
+}
diff --git a/tests/syntax/oracle/inline_stmt_contract.res.oracle b/tests/syntax/oracle/inline_stmt_contract.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..39a85c89c69eb63d2706ff0eeb968d2a5ee50f8c
--- /dev/null
+++ b/tests/syntax/oracle/inline_stmt_contract.res.oracle
@@ -0,0 +1,68 @@
+[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;
+}
+
+