From bfeb8c16321488ac18207d996d255b367e5e7ce7 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 23 Mar 2020 13:50:28 +0100
Subject: [PATCH] [typing] avoid removing a block if previous stmt is a
statement contract
or any code annotation that is specifying what the whole next
statement is doing
---
src/kernel_internals/typing/cabs2cil.ml | 159 +++++++++---------
src/kernel_services/ast_queries/file.ml | 26 +--
.../ast_queries/logic_utils.ml | 21 +++
.../ast_queries/logic_utils.mli | 9 +
tests/spec/oracle/stmt_contract.res.oracle | 2 +
tests/spec/stmt_contract.i | 3 +
6 files changed, 120 insertions(+), 100 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 48b894205ee..42b88e95e86 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -2100,82 +2100,89 @@ struct
Cil_printer.pp_stmt s l;
with Found -> ()
- class cleanUnspecified = object(self)
- inherit nopCilVisitor
- val unspecified_stack = Stack.create ()
-
- val mutable replace_table = []
-
- (* we start in a deterministic block. *)
- initializer Stack.push false unspecified_stack
-
- method private push: 'a.bool->'a->'a visitAction =
- fun flag x ->
- Stack.push flag unspecified_stack;
- ChangeDoChildrenPost
- (x,fun x -> ignore(Stack.pop unspecified_stack); x)
-
-
- method! vblock b =
- b.bstmts <-
- List.rev
- (List.fold_left(
- fun res s ->
- match s.skind with
- | Block b when
- (not (Stack.top unspecified_stack)) &&
- b.battrs = [] && b.blocals = [] &&
- s.labels = []
- -> List.rev_append b.bstmts res
- | _ -> s ::res)
- [] b.bstmts);
- DoChildren
-
- method! vstmt s =
- let ghost = s.ghost in
- let change_label_stmt s s' =
- List.iter
- (function
- | Label (x,_,_) -> H.replace labelStmt x s'
- | Case _ | Default _ -> replace_table <- (s, s') :: replace_table
- ) s.labels;
- s'.labels <- s.labels @ s'.labels
- in
- match s.skind with
- | UnspecifiedSequence [s',_,_,_,_] ->
- change_label_stmt s s';
- ChangeDoChildrenPost(s', fun x -> x)
- | UnspecifiedSequence [] ->
- let s' = mkEmptyStmt ~ghost ~valid_sid ~loc:(cabslu "_useq") () in
- change_label_stmt s s';
- ChangeTo s';
- | UnspecifiedSequence _ -> self#push true s
- | Block { battrs = []; blocals = []; bstmts = [s']} ->
- change_label_stmt s s';
- ChangeDoChildrenPost (s', fun x -> x)
- | Block _ | If _ | Loop _
- | TryFinally _ | TryExcept _ | Throw _ | TryCatch _ ->
- self#push false s
- | Switch _ ->
- let change_cases stmt =
- match stmt.skind with
- | Switch(e,body,cases,loc) ->
- let newcases =
- List.map
- (fun s ->
- try List.assq s replace_table
- with Not_found -> s)
- cases
- in
- stmt.skind <- Switch(e,body,newcases,loc);
- ignore (Stack.pop unspecified_stack);
- stmt
- | _ -> assert false
- in Stack.push false unspecified_stack;
- ChangeDoChildrenPost(s,change_cases)
- | Instr _ | Return _ | Goto _ | Break _
- | Continue _ -> DoChildren
- end
+ class cleanUnspecified =
+ let is_annot_next_stmt = function
+ | [] -> false
+ | { skind = Instr (Code_annot (c,_)) } :: _ ->
+ Logic_utils.is_annot_next_stmt c
+ | _ -> false
+ in
+ object(self)
+ inherit nopCilVisitor
+ val unspecified_stack = Stack.create ()
+
+ val mutable replace_table = []
+
+ (* we start in a deterministic block. *)
+ initializer Stack.push false unspecified_stack
+
+ method private push: 'a.bool->'a->'a visitAction =
+ fun flag x ->
+ Stack.push flag unspecified_stack;
+ ChangeDoChildrenPost
+ (x,fun x -> ignore(Stack.pop unspecified_stack); x)
+
+
+ method! vblock b =
+ b.bstmts <-
+ List.rev
+ (List.fold_left(
+ fun res s ->
+ match s.skind with
+ | Block b when
+ (not (Stack.top unspecified_stack)) &&
+ b.battrs = [] && b.blocals = [] &&
+ s.labels = [] && not (is_annot_next_stmt res)
+ -> List.rev_append b.bstmts res
+ | _ -> s ::res)
+ [] b.bstmts);
+ DoChildren
+
+ method! vstmt s =
+ let ghost = s.ghost in
+ let change_label_stmt s s' =
+ List.iter
+ (function
+ | Label (x,_,_) -> H.replace labelStmt x s'
+ | Case _ | Default _ -> replace_table <- (s, s') :: replace_table
+ ) s.labels;
+ s'.labels <- s.labels @ s'.labels
+ in
+ match s.skind with
+ | UnspecifiedSequence [s',_,_,_,_] ->
+ change_label_stmt s s';
+ ChangeDoChildrenPost(s', fun x -> x)
+ | UnspecifiedSequence [] ->
+ let s' = mkEmptyStmt ~ghost ~valid_sid ~loc:(cabslu "_useq") () in
+ change_label_stmt s s';
+ ChangeTo s';
+ | UnspecifiedSequence _ -> self#push true s
+ | Block { battrs = []; blocals = []; bstmts = [s']} ->
+ change_label_stmt s s';
+ ChangeDoChildrenPost (s', fun x -> x)
+ | Block _ | If _ | Loop _
+ | TryFinally _ | TryExcept _ | Throw _ | TryCatch _ ->
+ self#push false s
+ | Switch _ ->
+ let change_cases stmt =
+ match stmt.skind with
+ | Switch(e,body,cases,loc) ->
+ let newcases =
+ List.map
+ (fun s ->
+ try List.assq s replace_table
+ with Not_found -> s)
+ cases
+ in
+ stmt.skind <- Switch(e,body,newcases,loc);
+ ignore (Stack.pop unspecified_stack);
+ stmt
+ | _ -> assert false
+ in Stack.push false unspecified_stack;
+ ChangeDoChildrenPost(s,change_cases)
+ | Instr _ | Return _ | Goto _ | Break _
+ | Continue _ -> DoChildren
+ end
let mkFunctionBody ~ghost (c: chunk) : block =
if c.cases <> [] then
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 49e7e958ce5..a1635dcd9df 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -730,28 +730,6 @@ let synchronize_source_annot has_new_stmt kf =
| Some block, Some stmt_father when block == stmt_father -> true
| _, _ -> false
in
- let is_annot_next annot =
- match annot.annot_content with
- | AStmtSpec _ | APragma (Slice_pragma SPstmt | Impact_pragma IPstmt)
- -> true
- | AExtended(_,is_loop,{ext_name}) ->
- let warn_not_a_code_annot () =
- Kernel.(
- warning ~wkey:wkey_acsl_extension
- "%s is not a code annotation extension" name)
- in
- (match Logic_env.extension_category ext_name with
- | exception Not_found -> warn_not_a_code_annot () ; false
- | Ext_code_annot (Ext_here | Ext_next_loop)-> false
- | Ext_code_annot Ext_next_stmt-> true
- | Ext_code_annot Ext_next_both-> not is_loop
- | Ext_contract | Ext_global -> warn_not_a_code_annot () ; false)
- | AAssert _ | AInvariant _ | AVariant _
- | AAssigns _ | AAllocation _
- | APragma (Slice_pragma (SPctrl | SPexpr _))
- | APragma (Impact_pragma (IPexpr _))
- | APragma (Loop_pragma _) -> false
- in
let synchronize_user_annot a = add_annotation kf st a in
let synchronize_previous_user_annots () =
if !user_annots_for_next_stmt <> [] then begin
@@ -759,7 +737,7 @@ let synchronize_source_annot has_new_stmt kf =
let my_annots = !user_annots_for_next_stmt in
let post_action st =
let treat_annot (has_annot,st) (st_ann, annot) =
- if is_annot_next annot then begin
+ if Logic_utils.is_annot_next_stmt annot then begin
if has_annot || st.labels <> [] || st_ann.labels <> []
then begin
st_ann.skind <- (Block (Cil.mkBlockNonScoping [st]));
@@ -822,7 +800,7 @@ let synchronize_source_annot has_new_stmt kf =
(* Code annotation isn't considered as a real stmt.
So, previous annotations should be relative to the next stmt.
Only this [annot] may be synchronised to that stmt *)
- if is_annot_next annot then
+ if Logic_utils.is_annot_next_stmt annot then
(* Annotation relative to the effect of next statement *)
add_user_annot_for_next_stmt st annot
else
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index bbc4329de6a..41237fee587 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -573,6 +573,27 @@ let is_trivially_true p =
Ptrue -> true
| _ -> false
+let is_annot_next_stmt c =
+ match c.annot_content with
+ | AStmtSpec _ | APragma (Slice_pragma SPstmt | Impact_pragma IPstmt) -> true
+ | AExtended(_,is_loop,{ext_name}) ->
+ let warn_not_a_code_annot () =
+ Kernel.(
+ warning ~wkey:wkey_acsl_extension
+ "%s is not a code annotation extension" ext_name)
+ in
+ (match Logic_env.extension_category ext_name with
+ | exception Not_found -> warn_not_a_code_annot () ; false
+ | Ext_code_annot (Ext_here | Ext_next_loop)-> false
+ | Ext_code_annot Ext_next_stmt-> true
+ | Ext_code_annot Ext_next_both-> not is_loop
+ | Ext_contract | Ext_global -> warn_not_a_code_annot () ; false)
+ | AAssert _ | AInvariant _ | AVariant _
+ | AAssigns _ | AAllocation _
+ | APragma (Slice_pragma (SPctrl | SPexpr _))
+ | APragma (Impact_pragma (IPexpr _))
+ | APragma (Loop_pragma _) -> false
+
let rec add_attribute_glob_annot a g =
match g with
| Dfun_or_pred ({ l_var_info },_) | Dinvariant({ l_var_info }, _)
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index c19683aac4b..b3a51cdf016 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -250,6 +250,15 @@ val is_trivially_true: predicate -> bool
@since Nitrogen-20111001 *)
val is_trivially_false: predicate -> bool
+(** {2 Code annotations} *)
+
+(** Does the annotation apply to the next statement (e.g. a statement
+ contract). Also false for loop-related annotations.
+
+ @since Frama-C+dev
+*)
+val is_annot_next_stmt: code_annotation -> bool
+
(** {2 Global annotations} *)
(** add an attribute to a global annotation
diff --git a/tests/spec/oracle/stmt_contract.res.oracle b/tests/spec/oracle/stmt_contract.res.oracle
index c60dcabab0a..f8723d8fb48 100644
--- a/tests/spec/oracle/stmt_contract.res.oracle
+++ b/tests/spec/oracle/stmt_contract.res.oracle
@@ -38,6 +38,8 @@ int main(int c)
/*@ requires before_label: \true; */
label: /*@ requires after_label: \true; */
y = 8;
+ /*@ ensures x ≡ 0 ∨ x ≡ 7; */
+ if (c >= 3) x = 0; else x = 7;
/*@ requires x ≡ 7; */
/*@ ensures x ≡ 7; */
{
diff --git a/tests/spec/stmt_contract.i b/tests/spec/stmt_contract.i
index ccac6381fcc..80e9690322a 100644
--- a/tests/spec/stmt_contract.i
+++ b/tests/spec/stmt_contract.i
@@ -32,6 +32,9 @@ int main(int c) {
//@ requires after_label: \true;
y=8;
+ /*@ ensures x == 0 || x == 7; */
+ x = (c >= 3) ? 0 : 7;
+
/*@ requires x == 7; */
/*@ ensures x == 7; */
return 0;
--
GitLab