From 1e2be64f3d90246deca580a19071583a4a19280b Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Fri, 1 Mar 2024 18:03:35 +0100
Subject: [PATCH] [alias] render more robust in case of cyclic graphs
Cyclic graphs may occur in the presence of unsafe casts.
Instead of crashing with an exception we continue with a warning.
Fixes #1299
Move tests/known_bugs/reduce_by_valid.c -> tests/fixed_bugs/reduce_by_valid.c
---
src/plugins/alias/src/abstract_state.ml | 12 +++++--
src/plugins/alias/src/options.ml | 1 +
src/plugins/alias/src/options.mli | 1 +
.../oracle/reduce_by_valid.res.oracle | 35 +++++++++++++++++++
.../reduce_by_valid.c | 0
5 files changed, 47 insertions(+), 2 deletions(-)
create mode 100644 src/plugins/alias/tests/fixed_bugs/oracle/reduce_by_valid.res.oracle
rename src/plugins/alias/tests/{known_bugs => fixed_bugs}/reduce_by_valid.c (100%)
diff --git a/src/plugins/alias/src/abstract_state.ml b/src/plugins/alias/src/abstract_state.ml
index 7e07ea865f4..25308698c08 100644
--- a/src/plugins/alias/src/abstract_state.ml
+++ b/src/plugins/alias/src/abstract_state.ml
@@ -159,7 +159,13 @@ module Readout = struct
assert (G.mem_vertex s.graph v);
(* cycles can occur with unsafe casts such as: x->f = (int* ) x; *)
let rec checking_for_cycles s visited v =
- if VSet.mem v visited then LSet.empty else
+ if VSet.mem v visited then
+ let () =
+ Options.warning ~once:true ~wkey:Options.Warn.incoherent
+ "cycle during readout of vertex %d, \
+ (following unsafe cast?); analysis may be unsound" v
+ in LSet.empty
+ else
let visited = VSet.add v visited in
let modified_predecessors = List.map
(fun e ->
@@ -290,7 +296,9 @@ let assert_invariants s : unit =
G.iter_vertex assert_vertex s.graph;
let assert_edge v1 v2 =
Options.debug ~level:11 "checking coherence of edge %d → %d" v1 v2;
- assert (v1 <> v2);
+ if v1 = v2 then
+ Options.warning ~once:true ~wkey:Options.Warn.incoherent
+ "loop on vertex %d (following unsafe cast?); analysis may be unsound" v1;
assert (G.mem_vertex s.graph v1);
assert (G.mem_vertex s.graph v2)
in
diff --git a/src/plugins/alias/src/options.ml b/src/plugins/alias/src/options.ml
index 7c57801673f..ef9f63fa946 100644
--- a/src/plugins/alias/src/options.ml
+++ b/src/plugins/alias/src/options.ml
@@ -72,6 +72,7 @@ module Warn = struct
let unsupported_asm = register_warn_category "unsupported:asm"
let unsupported_function = register_warn_category "unsupported:fn"
let unsafe_cast = register_warn_category "unsafe-cast"
+ let incoherent = register_warn_category "incoherent"
end
module DebugKeys = struct
diff --git a/src/plugins/alias/src/options.mli b/src/plugins/alias/src/options.mli
index bfe5800b537..603c67bcb21 100644
--- a/src/plugins/alias/src/options.mli
+++ b/src/plugins/alias/src/options.mli
@@ -48,6 +48,7 @@ module Warn : sig
val unsupported_asm : warn_category
val unsupported_function : warn_category
val unsafe_cast : warn_category
+ val incoherent : warn_category
end
module DebugKeys : sig
diff --git a/src/plugins/alias/tests/fixed_bugs/oracle/reduce_by_valid.res.oracle b/src/plugins/alias/tests/fixed_bugs/oracle/reduce_by_valid.res.oracle
new file mode 100644
index 00000000000..290c2dbe3ec
--- /dev/null
+++ b/src/plugins/alias/tests/fixed_bugs/oracle/reduce_by_valid.res.oracle
@@ -0,0 +1,35 @@
+[kernel] Parsing reduce_by_valid.c (with preprocessing)
+[kernel:typing:incompatible-pointer-types] reduce_by_valid.c:5: Warning:
+ casting function to int *
+[kernel:typing:incompatible-pointer-types] reduce_by_valid.c:5: Warning:
+ casting function to int *
+[alias] analysing function: f
+[alias] analysing instruction: int *q = (int *)(& f);
+[alias:unsafe-cast] reduce_by_valid.c:5: Warning:
+ unsafe cast from void (*)(void) to int *
+[alias] May-aliases after instruction int *q = (int *)(& f); are <none>
+[alias] May-alias graph after instruction int *q = (int *)(& f); is
+ 0:{ q } → 1:{ f }
+[alias] analysing instruction: int *p = (int *)(& f);
+[alias:unsafe-cast] reduce_by_valid.c:5: Warning:
+ unsafe cast from void (*)(void) to int *
+[alias] May-aliases after instruction int *p = (int *)(& f); are { q; p }
+[alias] May-alias graph after instruction int *p = (int *)(& f); is
+ 0:{ q } → 5:{ f } 4:{ p } → 5:{ f }
+[alias] analysing instruction: p = (int *)(& q);
+[alias:unsafe-cast] reduce_by_valid.c:6: Warning:
+ unsafe cast from int ** to int *
+[alias:incoherent] Warning:
+ loop on vertex 5 (following unsafe cast?); analysis may be unsound
+[alias:incoherent] Warning:
+ cycle during readout of vertex 5, (following unsafe cast?); analysis may be unsound
+[alias] May-aliases after instruction p = (int *)(& q); are { *p; f; q; p }
+[alias] May-alias graph after instruction p = (int *)(& q); is
+ 4:{ p } → 5:{ f; q } 5:{ f; q } → 5:{ f; q }
+[alias] May-aliases at the end of function f: { *p; f; q; p }
+[alias] May-alias graph at the end of function f:
+ 4:{ p } → 5:{ f; q } 5:{ f; q } → 5:{ f; q }
+[alias] Summary of function f:
+ formals: locals: q→{ f; q } p→{ f; q } returns: <none>
+ state: { *p; f; q; p }
+[alias] Analysis complete
diff --git a/src/plugins/alias/tests/known_bugs/reduce_by_valid.c b/src/plugins/alias/tests/fixed_bugs/reduce_by_valid.c
similarity index 100%
rename from src/plugins/alias/tests/known_bugs/reduce_by_valid.c
rename to src/plugins/alias/tests/fixed_bugs/reduce_by_valid.c
--
GitLab