From f6e6f575fd90cbee7ff7eb784e704ceb546b9be6 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@cea.fr>
Date: Thu, 26 Sep 2024 18:09:52 +0200
Subject: [PATCH] [inline-contracts] preparing propagation of statuses
---
src/kernel_internals/typing/asm_contracts.ml | 8 ++-
.../inline_stmt_contracts.ml | 61 ++++++++++++++-----
tests/misc/asm_initialized.i | 4 +-
tests/misc/oracle/asm_initialized.res.oracle | 38 ++++++++++++
4 files changed, 92 insertions(+), 19 deletions(-)
diff --git a/src/kernel_internals/typing/asm_contracts.ml b/src/kernel_internals/typing/asm_contracts.ml
index 29123aa017..7814244c44 100644
--- a/src/kernel_internals/typing/asm_contracts.ml
+++ b/src/kernel_internals/typing/asm_contracts.ml
@@ -211,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
diff --git a/src/kernel_services/ast_transformations/inline_stmt_contracts.ml b/src/kernel_services/ast_transformations/inline_stmt_contracts.ml
index 4cd772eb9d..aa0b2711ac 100644
--- a/src/kernel_services/ast_transformations/inline_stmt_contracts.ml
+++ b/src/kernel_services/ast_transformations/inline_stmt_contracts.ml
@@ -23,8 +23,10 @@
open Cil_types
let emitter =
- Emitter.create
- "inline_stmt_contract" [Emitter.Code_annot] ~correctness:[] ~tuning:[]
+ let open Emitter in
+ create
+ "inline_stmt_contract" [Code_annot; Property_status]
+ ~correctness:[] ~tuning:[]
let category = File.register_code_transformation_category "inline_stmt_contract"
@@ -38,7 +40,29 @@ 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 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
@@ -47,17 +71,20 @@ let treat_behavior for_list stmt acc b =
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 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
+ 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) =
+ let treat_post_cond acc (k,p as postcond) =
match k with
| Normal ->
- if Logic_utils.is_trivially_true assumes then
- mk_annot p.ip_content.tp_statement :: acc
- else begin
+ 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
| _ -> ());
@@ -67,28 +94,34 @@ let treat_behavior for_list stmt acc b =
(pat ~loc (assumes,StmtLabel (ref stmt)),
p.ip_content.tp_statement))
in
- mk_annot p :: acc
+ (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 s) [] bhvs 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
- let kf = Option.get self#current_kf in
- List.iter (Annotations.add_code_annot emitter ~kf nop) posts;
+ 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
diff --git a/tests/misc/asm_initialized.i b/tests/misc/asm_initialized.i
index fdf22cba97..d0be761ab1 100644
--- a/tests/misc/asm_initialized.i
+++ b/tests/misc/asm_initialized.i
@@ -1,6 +1,6 @@
/* run.config*
-PLUGIN: @EVA_PLUGINS@
-STDOPT: #"-asm-contracts-ensure-init -inline-stmt-contracts -absolute-valid-range 0x10000000-0xf00000000 -print"
+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() {
diff --git a/tests/misc/oracle/asm_initialized.res.oracle b/tests/misc/oracle/asm_initialized.res.oracle
index 1cdc82f26b..2c96f18db6 100644
--- a/tests/misc/oracle/asm_initialized.res.oracle
+++ b/tests/misc/oracle/asm_initialized.res.oracle
@@ -46,3 +46,41 @@ int main(void)
}
+[report] Computing properties status...
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'main'
+--------------------------------------------------------------------------------
+
+[ - ] Assertion 'inline_stmt_contract' (file asm_initialized.i, line 9)
+ tried with Eva.
+[ - ] Assertion 'Eva,mem_access' (file asm_initialized.i, line 10)
+ tried with Eva.
+[ Alarm ] Assertion 'Eva,initialization' (file asm_initialized.i, line 11)
+ By Eva, with pending:
+ - Unreachable return (file asm_initialized.i, line 11)
+
+--------------------------------------------------------------------------------
+--- Status Report Summary
+--------------------------------------------------------------------------------
+ 2 To be validated
+ 1 Alarm emitted
+ 3 Total
+--------------------------------------------------------------------------------
+/* Generated by Frama-C */
+int main(void)
+{
+ int *sp;
+ int x;
+ /*@ 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;
+ /*@ assert Eva: initialization: \initialized(&x); */
+ return x;
+}
+
+
--
GitLab