From 66f8ac9509e0826f5ad81ca3ccfb235072c0a789 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 12 Jul 2023 18:05:09 +0200
Subject: [PATCH] [Eva] Fixes a bug on goto statement skipping local variable
declarations.
All variables local to a block are now introduced in domain states as soon as
the analysis enters the block. This ensures all variables in scope have always
been introduced in domain states, even when a goto statement jumps to a block
after the declaration of some local variables, skipping their initializations
(these variables would have been introduced in the states, but not initialized).
As a downside, variables explicitly initialized at declaration enter the scope
too early, as they should be introduced on the fly when encountering their
[Local_init] instruction.
---
src/plugins/eva/engine/iterator.ml | 23 ++++++++---------------
1 file changed, 8 insertions(+), 15 deletions(-)
diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index fc546c883cc..6122bee2111 100644
--- a/src/plugins/eva/engine/iterator.ml
+++ b/src/plugins/eva/engine/iterator.ml
@@ -122,12 +122,6 @@ module Make_Dataflow
let active_behaviors = Logic.create AnalysisParam.initial_state kf
- (* Compute the locals that we must enter in scope when we start the analysis
- of [block]. The other ones will be introduced on the fly, when we
- encounter a [Local_init] instruction. *)
- let block_toplevel_locals block =
- List.filter (fun vi -> not vi.vdefined) block.blocals
-
let initial_states =
let state = AnalysisParam.initial_state
and call_kinstr = AnalysisParam.call_kinstr
@@ -267,8 +261,15 @@ module Make_Dataflow
: transfer_function =
lift' (fun s -> Transfer.assign s (Kstmt stmt) dest exp)
+ (* All variables local to a block are introduced in domain states when
+ entering the block. Variables explicitly initialized at declaration time
+ (for which vi.vdefined is true) enter the scope too early, as they should
+ be introduced on the fly when encountering their [Local_init] instruction.
+ However, goto statements can skip their declaration/initialization, so it
+ is safer to always introduce all local variables (without initialize them)
+ when entering a block. *)
let transfer_enter (block : block) : transfer_function =
- let vars = block_toplevel_locals block in
+ let vars = block.blocals in
if vars = [] then id else lift (Transfer.enter_scope kf vars)
let transfer_leave (block : block) : transfer_function =
@@ -289,20 +290,12 @@ module Make_Dataflow
let transfer_instr (stmt : stmt) (instr : instr) : transfer_function =
match instr with
| Local_init (vi, AssignInit exp, _loc) ->
- let kind = Abstract_domain.Local kf in
let transfer state =
- let state = Domain.enter_scope kind [vi] state in
Init.initialize_local_variable stmt vi exp state
in
lift' transfer
| Local_init (vi, ConsInit (f, args, k), loc) ->
- let kind = Abstract_domain.Local kf in
let as_func dest callee args _loc (key, state) =
- (* This variable enters the scope too early, as it should
- be introduced after the call to [f] but before the assignment
- to [v]. This is currently not possible, at least without
- splitting Transfer.call in two. *)
- let state = Domain.enter_scope kind [vi] state in
transfer_call stmt dest callee args (key, state)
in
Cil.treat_constructor_as_func as_func vi f args k loc
--
GitLab