Skip to content
Snippets Groups Projects
Commit e2b2b9c0 authored by David Bühler's avatar David Bühler
Browse files

[Eva] Octagon: do not assume that [reuse] cannot lead to bottom.

When using a previous call from the memexec cache to interpret a new call, if a
relation from the previous output lead to bottom in the new state, emits a
warning and continues the analysis by ignoring this relation.
parent a92dcf1f
No related branches found
No related tags found
No related merge requests found
...@@ -1394,7 +1394,7 @@ module Domain = struct ...@@ -1394,7 +1394,7 @@ module Domain = struct
let join_oct = Octagons.internal_join ~cache ~symmetric ~idempotent ~decide let join_oct = Octagons.internal_join ~cache ~symmetric ~idempotent ~decide
and join_itv = Intervals.internal_join ~cache ~symmetric ~idempotent ~decide and join_itv = Intervals.internal_join ~cache ~symmetric ~idempotent ~decide
and join_rel = Relations.union in and join_rel = Relations.union in
fun ~current_input ~previous_output -> fun kf ~current_input ~previous_output ->
let current_input = kill previous_output.modified current_input in let current_input = kill previous_output.modified current_input in
(* We use [add_diamond] to add each relation from the previous output (* We use [add_diamond] to add each relation from the previous output
into the current input, in order to benefit from the (partial) into the current input, in order to benefit from the (partial)
...@@ -1409,7 +1409,15 @@ module Domain = struct ...@@ -1409,7 +1409,15 @@ module Domain = struct
in in
let state = { current_input with intervals } in let state = { current_input with intervals } in
let add_diamond variables diamond acc = let add_diamond variables diamond acc =
Bottom.non_bottom (add_diamond acc variables diamond) match add_diamond acc variables diamond with
| `Value state -> state
| `Bottom ->
Self.failure ~current:true ~once:true
"Octagon domain: the use of the memexec cache for function %a
unexpectedly led to bottom, which could be a bug. The analysis
continues by ignoring the relations leading to bottom."
Kernel_function.pretty kf;
acc
in in
Octagons.fold add_diamond previous_output.octagons state Octagons.fold add_diamond previous_output.octagons state
else else
...@@ -1418,11 +1426,11 @@ module Domain = struct ...@@ -1418,11 +1426,11 @@ module Domain = struct
relations = join_rel previous_output.relations current_input.relations; relations = join_rel previous_output.relations current_input.relations;
modified = current_input.modified } modified = current_input.modified }
let reuse _kf _bases ~current_input ~previous_output = let reuse kf _bases ~current_input ~previous_output =
if intraprocedural () if intraprocedural ()
then previous_output then previous_output
else else
let t = interprocedural_reuse ~current_input ~previous_output in let t = interprocedural_reuse kf ~current_input ~previous_output in
check "reuse result" t check "reuse result" t
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment