From 8d9081893270f1a0e1c0f117a61b8951f2a5e56a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 17 Sep 2019 14:46:45 +0200
Subject: [PATCH] [Eva] Makes the octagons domain interprocedural. Disabled by
default.
New boolean option -eva-octagons-through-calls to specify whether the octagons
are propagated through function calls.
---
src/plugins/value/domains/octagons.ml | 23 ++++++++++++++++++++---
src/plugins/value/value_parameters.ml | 15 +++++++++++++++
src/plugins/value/value_parameters.mli | 2 ++
3 files changed, 37 insertions(+), 3 deletions(-)
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index d7e9b2bffb1..08661199e82 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -38,6 +38,12 @@ let infer_intervals = true
minimal drop in efficiency. *)
let saturate_octagons = true
+(* Is the domain intraprocedural, according to the -eva-octagons-through-calls
+ option. In this case, the analysis of each function starts with an empty
+ state, and the relations inferred in a function are not propagated back to
+ the caller either. *)
+let intraprocedural () = not (Value_parameters.OctagonsCall.get ())
+
(* -------------------------------------------------------------------------- *)
(* Basic types: pair of variables and Ival.t *)
(* -------------------------------------------------------------------------- *)
@@ -1190,11 +1196,22 @@ module Domain = struct
let assume _stmt _exp _bool = update
- let start_call _stmt _call _valuation _state = `Value (empty ())
+ let start_call _stmt call valuation state =
+ if intraprocedural ()
+ then `Value (empty ())
+ else
+ let state = { state with modified = Locations.Zone.bottom } in
+ let assign_formal state { formal; concrete; avalue } =
+ state >>- assign_variable formal concrete avalue valuation
+ in
+ List.fold_left assign_formal (`Value state) call.arguments
let finalize_call _stmt _call ~pre ~post =
- let written_zone = post.modified in
- `Value (kill written_zone pre)
+ if intraprocedural ()
+ then `Value (kill post.modified pre)
+ else
+ let modified = Locations.Zone.join post.modified pre.modified in
+ `Value { post with modified }
let show_expr _valuation _state _fmt _expr = ()
end
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index dd13a4af2be..f283790bf96 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -319,6 +319,21 @@ module EqualityCallFunction =
end)
let () = add_precision_dep EqualityCallFunction.parameter
+let () = Parameter_customize.set_group domains
+module OctagonsCall =
+ Bool
+ (struct
+ let option_name = "-eva-octagons-through-calls"
+ let help = "Whether the relations inferred by the octagons domain are \
+ propagated through function calls. Disabled by default: \
+ the octagons analysis is intra-procedural, starting \
+ each function with an empty octagons state, \
+ and losing the octagons inferred at the end. \
+ The interprocedural analysis is more precise but slower."
+ let default = false
+ end)
+let () = add_precision_dep OctagonsCall.parameter
+
let () = Parameter_customize.set_group domains
module Numerors_Real_Size =
Int
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index edc7a34b904..84ec6ea9a83 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -51,6 +51,8 @@ module EqualityCallFunction:
Parameter_sig.Map with type key = Cil_types.kernel_function
and type value = string
+module OctagonsCall: Parameter_sig.Bool
+
module TracesUnrollLoop: Parameter_sig.Bool
module TracesUnifyLoop: Parameter_sig.Bool
module TracesDot: Parameter_sig.String
--
GitLab