From 271db6912a6187c0b231c035e1ccd17a78bd735d Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Fri, 23 Aug 2024 10:02:08 +0200
Subject: [PATCH] [kernel] Fix Kernel_function.var_is_in_scope
Fix a bug where `Kernel_function.var_is_in_scope vi stmt` would return
true if `stmt` was the defining statement for `vi` and the first
statement of a block.
---
.../ast_data/kernel_function.ml | 50 +++++++++++--------
.../ast_data/kernel_function.mli | 6 +--
2 files changed, 31 insertions(+), 25 deletions(-)
diff --git a/src/kernel_services/ast_data/kernel_function.ml b/src/kernel_services/ast_data/kernel_function.ml
index dc8bad23a4..ed5b97a739 100644
--- a/src/kernel_services/ast_data/kernel_function.ml
+++ b/src/kernel_services/ast_data/kernel_function.ml
@@ -519,31 +519,36 @@ let find_syntactic_callsites kf =
try CallSites.find table kf
with Not_found -> []
-let local_definition kf vi =
+let local_definition_opt kf vi =
let locals = get_locals kf in
- if not vi.vdefined ||
- not (List.exists (fun vi' -> Cil_datatype.Varinfo.equal vi vi') locals)
- then
- Kernel.fatal
- "%a is not a defined local variable of %a"
+ if not vi.vdefined || not (List.exists (Cil_datatype.Varinfo.equal vi) locals)
+ then None
+ else
+ try
+ List.find (fun s ->
+ match s.skind with
+ | Instr (Local_init (vi', _, _)) -> Cil_datatype.Varinfo.equal vi vi'
+ | _ -> false
+ ) (get_definition kf).sallstmts
+ |> Option.some
+ with Not_found -> assert false (* cannot occur on well-formed AST. *)
+
+let local_definition kf vi =
+ match local_definition_opt kf vi with
+ | None ->
+ Kernel.fatal "%a is not a defined local variable of %a"
Cil_datatype.Varinfo.pretty vi pretty kf;
- try
- List.find
- (fun s ->
- match s.skind with
- | Instr (Local_init (vi', _, _)) -> Cil_datatype.Varinfo.equal vi vi'
- | _ -> false)
- (get_definition kf).sallstmts
- with Not_found -> assert false (* cannot occur on well-formed AST. *)
+ | Some sdef -> sdef
let var_is_in_scope stmt vi =
let blocks = find_all_enclosing_blocks stmt in
+ let sdef = local_definition_opt (find_englobing_kf stmt) vi in
let is_def_above b =
- let sdef = local_definition (find_englobing_kf stmt) vi in
- (* If sdef == stmt, vi is in the scope. *)
- Cil_datatype.Stmt.equal sdef stmt ||
+ (* sdef cannot be None in this context because vi is defined and in b locals
+ (so in kf locals as well) when we call is_def_above. *)
+ let sdef = Option.get sdef in
match b.bstmts with
- | [] -> assert false (* at least contains stmt *)
+ | [] -> assert false (* b should at least contains stmt. *)
| sfst :: _ ->
(* if sfst is sdef (or an unspecified sequence containing sdef), it
is necessarily above stmt. Otherwise, we can rely on is_between to
@@ -551,10 +556,11 @@ let var_is_in_scope stmt vi =
Cil_datatype.Stmt.equal sfst (find_enclosing_stmt_in_block b sdef) ||
is_between b sfst sdef stmt
in
- List.exists
- (fun b ->
- List.exists (Cil_datatype.Varinfo.equal vi) b.blocals &&
- (not vi.vdefined || is_def_above b)
+ (* If sdef is equal to stmt, vi is not in the scope yet. *)
+ Option.equal Cil_datatype.Stmt.equal sdef (Some stmt) ||
+ List.exists (fun b ->
+ List.exists (Cil_datatype.Varinfo.equal vi) b.blocals &&
+ (not vi.vdefined || is_def_above b)
)
blocks
diff --git a/src/kernel_services/ast_data/kernel_function.mli b/src/kernel_services/ast_data/kernel_function.mli
index 529072770f..2144f87a9f 100644
--- a/src/kernel_services/ast_data/kernel_function.mli
+++ b/src/kernel_services/ast_data/kernel_function.mli
@@ -144,9 +144,9 @@ val local_definition: t -> varinfo -> stmt
val var_is_in_scope: stmt -> varinfo -> bool
(** [var_is_in_scope stmt vi] returns [true] iff the local variable [vi]
- is syntactically visible from statement [stmt] in function [kf]. Note
- that on the contrary to {!Globals.Syntactic_search.find_in_scope}, the
- variable is searched according to its [vid], not its [vorig_name].
+ is syntactically visible from statement [stmt]. Note that on the contrary to
+ {!Globals.Syntactic_search.find_in_scope}, the variable is searched
+ according to its [vid], not its [vorig_name].
@since 19.0-Potassium *)
--
GitLab