From 20e12ca5c416a9c0887d059b69924ce5ab2c7782 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Wed, 3 Nov 2021 19:54:59 +0100
Subject: [PATCH] [LoopAnalysis] Use the new EVA API
---
src/plugins/loop_analysis/Makefile.in | 1 +
src/plugins/loop_analysis/loop_analysis.ml | 35 +++++--------------
.../oracle/with_value.res.oracle | 4 +++
3 files changed, 13 insertions(+), 27 deletions(-)
diff --git a/src/plugins/loop_analysis/Makefile.in b/src/plugins/loop_analysis/Makefile.in
index 4cb7ceebdc7..a4aee4ac5c0 100644
--- a/src/plugins/loop_analysis/Makefile.in
+++ b/src/plugins/loop_analysis/Makefile.in
@@ -33,6 +33,7 @@ PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
PLUGIN_NAME:= LoopAnalysis
PLUGIN_CMO:= options region_analysis region_analysis_stmt loop_analysis register
PLUGIN_CMI:= region_analysis_sig
+PLUGIN_DEPENDENCIES:= Eva
PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure test.c test.oracle README.org
PLUGIN_TESTS_DIRS:=loop_analysis
diff --git a/src/plugins/loop_analysis/loop_analysis.ml b/src/plugins/loop_analysis/loop_analysis.ml
index 39a8827dd6a..a37f5ec6586 100644
--- a/src/plugins/loop_analysis/loop_analysis.ml
+++ b/src/plugins/loop_analysis/loop_analysis.ml
@@ -340,37 +340,18 @@ module Store(* (B:sig *)
Printer.pp_stmt stmt
let value_min_max stmt vi =
- if (Db.Value.is_computed ()) then
+ if (Eva.Analysis.is_computed ()) then
begin
Options.feedback ~dkey ~once:true
"value analysis computed, trying results";
- if Db.Value.is_reachable_stmt stmt then
- let state = Db.Value.get_stmt_state stmt in
- try
- let loc = Locations.loc_of_varinfo vi in
- let v = Db.Value.find state loc in
- let ival = Cvalue.V.project_ival v in
- let omin, omax = Ival.min_and_max ival in
- omin, omax
- with
- | Not_found ->
- Options.feedback ~dkey "value_min_max: not found: %a@.\
- function: %a, stmt: %a"
- Printer.pp_varinfo vi Kernel_function.pretty
- (Kernel_function.find_englobing_kf stmt) Printer.pp_stmt stmt;
- None, None
- | Cvalue.V.Not_based_on_null ->
- Options.feedback ~dkey "value_min_max: not based on null: %a@.\
- function: %a, stmt: %a"
- Printer.pp_varinfo vi Kernel_function.pretty
- (Kernel_function.find_englobing_kf stmt) Printer.pp_stmt stmt;
- None, None
- else
- begin
+ let value = Eva.Results.(before stmt |> eval_var vi |> as_ival) in
+ match value with
+ | Result.Ok ival -> Ival.min_and_max ival
+ | Error e ->
+ if e = Eva.Results.Bottom then
Options.feedback ~dkey "skipping unreachable stmt (function: %a)"
Kernel_function.pretty (Kernel_function.find_englobing_kf stmt);
- None, None
- end
+ None, None
end
else
begin
@@ -490,7 +471,7 @@ module Store(* (B:sig *)
with Not_found -> ()
end
| c ->
- if (Db.Value.is_computed ()) then
+ if (Eva.Analysis.is_computed ()) then
begin
let min_max_int = value_min_max stmt in
match c with
diff --git a/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle b/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle
index f2851d8cb74..b7db69d0c82 100644
--- a/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle
+++ b/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle
@@ -433,6 +433,10 @@
with_value.i:26: 5
with_value.i:30: 5
with_value.i:34: 4
+ with_value.i:38: 2147483648
+ with_value.i:42: 2147483649
+ with_value.i:46: 2147483649
+ with_value.i:50: 2147483648
with_value.i:54: 2147483646
with_value.i:58: 2147483647
with_value.i:62: 2147483647
--
GitLab