From f39c69684311bb9a80f8b47c7b5adaf02b42b1ac Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Tue, 10 Oct 2023 15:47:08 +0200
Subject: [PATCH] [oneret] Find the original declaration block of retvar.
---
src/kernel_internals/typing/oneret.ml | 61 +++++++++++++++++++--------
1 file changed, 43 insertions(+), 18 deletions(-)
diff --git a/src/kernel_internals/typing/oneret.ml b/src/kernel_internals/typing/oneret.ml
index 881f297878a..5eb2215e207 100644
--- a/src/kernel_internals/typing/oneret.ml
+++ b/src/kernel_internals/typing/oneret.ml
@@ -141,7 +141,7 @@ let encapsulate_local_vars f =
(fun v -> Cil.hasAttribute Cabs2cil.frama_c_destructor v.vattr)
f.sbody.blocals
then begin
- let exception Found of (block * stmt) in
+ let exception Found of (block Stack.t * stmt) in
let vis = object
val sb = Stack.create ()
inherit Cil.nopCilVisitor
@@ -151,24 +151,31 @@ let encapsulate_local_vars f =
method! vstmt s =
match s.skind with
- | Return _ -> raise (Found (Stack.top sb,s));
+ | Return _ -> raise (Found (sb, s));
| _ -> DoChildren
end
in
- let ret_block, ret =
+ let stack_block, ret_stmt =
try
ignore (visitCilBlock vis f.sbody);
Kernel.fatal "No return statement found inside %a"
Cil_printer.pp_varinfo f.svar
with Found res -> res
in
- let ret_block_body =
+ let ret_block = Stack.top stack_block in
+ let ret_block_bstmts =
List.filter
- (fun s -> not (Cil_datatype.Stmt.equal ret s))
+ (fun s -> not (Cil_datatype.Stmt.equal ret_stmt s))
ret_block.bstmts
in
+ ret_block.bstmts <- ret_block_bstmts;
+ let s1 = Cil.mkStmt (Block f.sbody) in
+ let b = Cil.mkBlock [ s1; ret_stmt] in
+ (* As we filtered [ret_stmt] out its original block, we now need to move the
+ declaration of the return variable into [b]. Before doing that, we must
+ remove such a declaration from its original block. *)
let retvar =
- match ret.skind with
+ match ret_stmt.skind with
| Return(None, _) -> None
| Return(Some {enode = Lval (Var v,NoOffset)}, _) -> Some v
| Return _ ->
@@ -176,19 +183,37 @@ let encapsulate_local_vars f =
| _ ->
Kernel.fatal "find_return did not return Return node"
in
- let filter_retvar_vi blocals =
- Option.fold retvar
- ~none:blocals
- ~some:(fun retvar_vi ->
- List.filter
- (fun vi -> not (Cil_datatype.Varinfo.equal retvar_vi vi))
- blocals)
+ (* Retrieve the block declaring [retvar], if any. *)
+ let retvar_decl_block =
+ match retvar with
+ | None -> None
+ | Some retvar ->
+ let contains_retvar =
+ List.exists (Cil_datatype.Varinfo.equal retvar)
+ in
+ let rec find_decl_block stack =
+ let block = Stack.pop_opt stack in
+ match block with
+ | None ->
+ Kernel.fatal "No block found declaring return variable %a"
+ Cil_printer.pp_varinfo retvar
+ | Some block ->
+ if contains_retvar block.blocals
+ then Some block
+ else find_decl_block stack
+ in
+ find_decl_block stack_block
in
- ret_block.bstmts <- ret_block_body;
- ret_block.blocals <- filter_retvar_vi ret_block.blocals;
- f.sbody.blocals <- filter_retvar_vi f.sbody.blocals;
- let s1 = Cil.mkStmt (Block f.sbody) in
- let b = Cil.mkBlock [ s1; ret] in
+ (* Filter [retvar] out its original declaration block [retvar_decl_block],
+ if any, as we will add such declaration to the outermost block [b]. *)
+ Option.fold retvar_decl_block ~none:() ~some:(fun retvar_decl_block ->
+ let retvar = Option.get retvar in
+ retvar_decl_block.blocals <-
+ List.filter
+ (fun vi -> not (Cil_datatype.Varinfo.equal retvar vi))
+ retvar_decl_block.blocals);
+ (* We can now safely add [retvar] into [b]'s declarations, and use [b] as
+ the new function's body block. *)
b.blocals <- Option.to_list retvar;
f.sbody <- b
end
--
GitLab