From 584e02429585c366a5361b6dada4fc67d3fa6863 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 28 Feb 2019 19:36:18 +0100
Subject: [PATCH] [Cil] Improved behavior of transient block
---
src/kernel_services/ast_queries/cil.ml | 31 ++++++++---
src/kernel_services/ast_queries/cil.mli | 7 ++-
.../syntax/oracle/transient_block.res.oracle | 31 +++++++++++
tests/syntax/transient_block.i | 14 +++++
tests/syntax/transient_block.ml | 51 +++++++++++++++++++
5 files changed, 124 insertions(+), 10 deletions(-)
create mode 100644 tests/syntax/oracle/transient_block.res.oracle
create mode 100644 tests/syntax/transient_block.i
create mode 100644 tests/syntax/transient_block.ml
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 027a3758727..c7297ce634b 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -2150,10 +2150,25 @@ let assertEmptyQueue vis =
let vis_tmp_attr = "FRAMAC_VIS_TMP_ATTR"
+let wkey_transient = Kernel.register_warn_category "transient-block"
+let () = Kernel.set_warn_status wkey_transient Log.Winactive
+
let transient_block b =
- if b.blocals <> [] then
+ if b.blocals <> [] then begin
+ if List.exists
+ (function
+ | { skind = Instr (Local_init (v,_,_)) } ->
+ not (List.exists (Cil_datatype.Varinfo.equal v) b.blocals)
+ | _ -> false)
+ b.bstmts
+ then
Kernel.fatal
"Attempting to mark as transient a block that declares local variables";
+ Kernel.warning
+ ~wkey:wkey_transient
+ "ignoring request to mark transient a block with local variables:@\n%a"
+ Cil_datatype.Block.pretty b
+ end else
b.battrs <- addAttribute (Attr (vis_tmp_attr,[])) b.battrs; b
let block_of_transient b =
@@ -4546,7 +4561,7 @@ let isCharConstPtrType t =
| Ltype ({lt_name = "typetag"},[]) -> true
| Ltype (tdef,_) as ty when is_unrollable_ltdef tdef ->
isTypeTagType (unroll_ltdef ty)
- | _ -> false
+ | _ -> false
let getReturnType t =
match unrollType t with
@@ -4682,7 +4697,7 @@ let isCharConstPtrType t =
| Ctype typ ->
begin match unrollType typ with
| TPtr (t, _) -> typeTermOffset (Ctype t) off
- | _ ->
+ | _ ->
Kernel.fatal ~current:true
"typeOfTermLval: Mem on a non-pointer"
end
@@ -4690,7 +4705,7 @@ let isCharConstPtrType t =
Kernel.fatal ~current:true "typeOfTermLval: Mem on a logic type"
| Ltype (s,_) as ty when is_unrollable_ltdef s ->
type_of_pointed (unroll_ltdef ty)
- | Ltype (s,_) ->
+ | Ltype (s,_) ->
Kernel.fatal ~current:true
"typeOfTermLval: Mem on a non-C type (%s)" s.lt_name
| Lvar s ->
@@ -4715,7 +4730,7 @@ let isCharConstPtrType t =
"typeTermOffset: Attribute on a logic type"
| Ltype (s,_) as ty when is_unrollable_ltdef s ->
putAttributes (unroll_ltdef ty)
- | Ltype (s,_) ->
+ | Ltype (s,_) ->
Kernel.fatal ~current:true
"typeTermOffset: Attribute on a non-C type (%s)" s.lt_name
| Lvar s ->
@@ -4744,8 +4759,8 @@ let isCharConstPtrType t =
| Linteger | Lreal -> Kernel.fatal ~current:true "typeTermOffset: Index on a logic type"
| Ltype (s,_) as ty when is_unrollable_ltdef s ->
elt_type (unroll_ltdef ty)
- | Ltype (s,_) ->
- Kernel.fatal ~current:true "typeTermOffset: Index on a non-C type (%s)" s.lt_name
+ | Ltype (s,_) ->
+ Kernel.fatal ~current:true "typeTermOffset: Index on a non-C type (%s)" s.lt_name
| Lvar s -> Kernel.fatal ~current:true "typeTermOffset: Index on a non-C type ('%s)" s
| Larrow _ -> Kernel.fatal ~current:true "typeTermOffset: Index on a function type"
in
@@ -4765,7 +4780,7 @@ let isCharConstPtrType t =
| Linteger | Lreal -> Kernel.fatal ~current:true "typeTermOffset: Field on a logic type"
| Ltype (s,_) as ty when is_unrollable_ltdef s ->
elt_type (unroll_ltdef ty)
- | Ltype (s,_) ->
+ | Ltype (s,_) ->
Kernel.fatal ~current:true "typeTermOffset: Field on a non-C type (%s)" s.lt_name
| Lvar s -> Kernel.fatal ~current:true "typeTermOffset: Field on a non-C type ('%s)" s
| Larrow _ -> Kernel.fatal ~current:true "typeTermOffset: Field on a function type"
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 799986722ec..4a48a303c96 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -2045,12 +2045,15 @@ val visitCilBlock: cilVisitor -> block -> block
might prevent it (e.g. if the preceding statement is a statement contract
or a slicing/pragma annotation, or if there are labels involved). Use
that whenever you're creating a block in order to hold multiple statements
- as a result of visiting a single statement.
+ as a result of visiting a single statement. If the block contains local
+ variables, it will not be marked as transient, since removing it will
+ change the scope of those variables.
@raise Fatal error if the given block attempts to declare local variables
- (in which case it can't be marked as transient anyways).
+ and contain definitions of local variables that are not part of the block.
@since Phosphorus-20170501-beta1
+ @modify Frama-C+dev: do not raise fatal as soon as the block has locals
*)
val transient_block: block -> block
diff --git a/tests/syntax/oracle/transient_block.res.oracle b/tests/syntax/oracle/transient_block.res.oracle
new file mode 100644
index 00000000000..0073c7bf559
--- /dev/null
+++ b/tests/syntax/oracle/transient_block.res.oracle
@@ -0,0 +1,31 @@
+[kernel] Parsing tests/syntax/transient_block.i (no preprocessing)
+[kernel] Failure: Attempting to mark as transient a block that declares local variables
+[kernel] transient_block fatal error on int x = 1; as expected
+[kernel:transient-block] Warning:
+ ignoring request to mark transient a block with local variables:
+ {
+ int y;
+ int y = 0;
+ x = 2;
+ }
+/* Generated by Frama-C */
+void f(void)
+{
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ int x = 1;
+ {
+ int y;
+ int y = 0;
+ x = 2;
+ }
+ f();
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/syntax/transient_block.i b/tests/syntax/transient_block.i
new file mode 100644
index 00000000000..bfc8874399c
--- /dev/null
+++ b/tests/syntax/transient_block.i
@@ -0,0 +1,14 @@
+/* run.config
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -kernel-warn-key transient-block=active
+*/
+
+void f(void) { }
+
+int main () {
+
+ int x = 1;
+ x = 2;
+ f();
+
+}
diff --git a/tests/syntax/transient_block.ml b/tests/syntax/transient_block.ml
new file mode 100644
index 00000000000..0bf3ce8e4aa
--- /dev/null
+++ b/tests/syntax/transient_block.ml
@@ -0,0 +1,51 @@
+open Cil_types
+
+class vis prj = object(self)
+ inherit Visitor.frama_c_copy prj
+
+ val mutable my_var = None
+
+ method private create_block create s instr =
+ let s1 = Cil.mkStmtOneInstr ~valid_sid:true instr in
+ let b = Cil.mkBlock [s1] in
+ if create then begin
+ let f = Cil.get_fundec self#behavior (Extlib.the self#current_func) in
+ let y = Cil.makeLocalVar f ~scope:b "y" (TInt(IInt,[])) in
+ my_var <- Some y;
+ let loc = Cil_datatype.Location.unknown in
+ let s2 =
+ Cil.mkStmtOneInstr ~valid_sid:true
+ (Local_init(y,AssignInit(SingleInit(Cil.zero ~loc)),loc))
+ in
+ b.bstmts <- s2 :: b.bstmts;
+ let b = Cil.transient_block b in
+ s.skind <- Block b;
+ end;
+ Cil.JustCopy
+
+ method! vstmt_aux s =
+ match s.skind with
+ | Instr (Local_init _ as instr) ->
+ (try
+ self#create_block true s instr
+ with Log.AbortFatal _ ->
+ Kernel.feedback "transient_block fatal error on %a as expected"
+ Printer.pp_instr instr;
+ let f = Cil.get_fundec self#behavior (Extlib.the self#current_func) in
+ let y = Extlib.the my_var in
+ f.slocals <-
+ List.filter
+ (fun v -> not (Cil_datatype.Varinfo.equal v y)) f.slocals;
+ Cil.DoChildren)
+ | Instr (Set ((Var { vorig_name = "x" }, NoOffset),_,_) as instr) ->
+ self#create_block true s instr
+ | Instr (Call _ as instr) -> self#create_block false s instr
+ | _ -> Cil.DoChildren
+end
+
+let main () =
+ Ast.compute ();
+ let prj = File.create_project_from_visitor "test" (fun prj -> new vis prj) in
+ File.pretty_ast ~prj ()
+
+let () = Db.Main.extend main
--
GitLab