From 97267d51ec1e91ec1100503721139981692e9593 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Sun, 25 Aug 2019 23:02:15 +0200
Subject: [PATCH] [Eva] Apron domains registration.
---
Makefile | 21 +++------
.../value/domains/apron/apron_domain.ko.ml | 44 -------------------
.../{apron_domain.ok.ml => apron_domain.ml} | 42 +++++++++---------
.../value/domains/apron/apron_domain.mli | 27 ------------
src/plugins/value/value_parameters.ml | 17 +++++++
src/plugins/value/value_parameters.mli | 2 +
6 files changed, 47 insertions(+), 106 deletions(-)
delete mode 100644 src/plugins/value/domains/apron/apron_domain.ko.ml
rename src/plugins/value/domains/apron/{apron_domain.ok.ml => apron_domain.ml} (97%)
diff --git a/Makefile b/Makefile
index 334437fc823..c475e1a48da 100644
--- a/Makefile
+++ b/Makefile
@@ -821,21 +821,12 @@ PLUGIN_TESTS_DIRS+=value/traces
# Files for the binding to Apron domains. Only available if Apron is available.
ifeq ($(HAS_APRON),yes)
PLUGIN_REQUIRES+= apron.octMPQ apron.boxMPQ apron.polkaMPQ apron.apron gmp
-src/plugins/value/domains/apron/apron_domain.ml: \
- src/plugins/value/domains/apron/apron_domain.ok.ml \
- share/Makefile.config
- $(CP_IF_DIFF) $< $@
- $(CHMOD_RO) $@
+APRON_CMO:= domains/apron/apron_domain
else
-src/plugins/value/domains/apron/apron_domain.ml: \
- src/plugins/value/domains/apron/apron_domain.ko.ml \
- share/Makefile.config
- $(CP_IF_DIFF) $< $@
- $(CHMOD_RO) $@
-endif
-PLUGIN_GENERATED+= src/plugins/value/domains/apron/apron_domain.ml
+APRON_CMO:=
PLUGIN_DISTRIB_EXTERNAL+= \
- domains/apron/apron_domain.ok.ml domains/apron/apron_domain.ko.ml
+ domains/apron/apron_domain.ml domains/apron/apron_domain.mli
+endif
# Files for the numerors domain. Only available is MPFR is available.
NUMERORS_FILES:= \
@@ -890,7 +881,6 @@ PLUGIN_CMO:= slevel/split_strategy value_parameters \
domains/traces_domain \
domains/simple_memory \
domains/gauges/gauges_domain \
- domains/apron/apron_domain \
domains/hcexprs \
domains/equality/equality domains/equality/equality_domain \
domains/offsm_domain \
@@ -918,7 +908,8 @@ PLUGIN_CMO:= slevel/split_strategy value_parameters \
engine/partition engine/partitioning_parameters engine/trace_partitioning \
engine/iterator \
engine/initialization \
- engine/compute_functions engine/analysis register
+ engine/compute_functions engine/analysis register \
+ $(APRON_CMO)
PLUGIN_CMI:= values/abstract_value values/abstract_location \
domains/abstract_domain domains/simpler_domains
PLUGIN_DEPENDENCIES:=Callgraph LoopAnalysis RteGen
diff --git a/src/plugins/value/domains/apron/apron_domain.ko.ml b/src/plugins/value/domains/apron/apron_domain.ko.ml
deleted file mode 100644
index cde2dc82ad6..00000000000
--- a/src/plugins/value/domains/apron/apron_domain.ko.ml
+++ /dev/null
@@ -1,44 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2019 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-let ok = false
-
-module type S = Abstract_domain.Leaf
- with type value = Main_values.Interval.t
- and type location = Precise_locs.precise_location
-
-module U = struct
- include Unit_domain.Make (Main_values.Interval) (Main_locations.PLoc)
- let key = Structure.Key_Domain.create_key "dummy_apron"
-end
-
-module Octagon = U
-module Box = U
-module Polka_Loose = U
-module Polka_Strict = U
-module Polka_Equalities = U
-
-(*
-Local Variables:
-compile-command: "make -C ../../../.."
-End:
-*)
diff --git a/src/plugins/value/domains/apron/apron_domain.ok.ml b/src/plugins/value/domains/apron/apron_domain.ml
similarity index 97%
rename from src/plugins/value/domains/apron/apron_domain.ok.ml
rename to src/plugins/value/domains/apron/apron_domain.ml
index 160d5ced136..c608d724771 100644
--- a/src/plugins/value/domains/apron/apron_domain.ok.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ml
@@ -20,22 +20,14 @@
(* *)
(**************************************************************************)
-#24 "src/plugins/value/domains/apron/apron_domain.ok.ml"
-
open Cil_types
open Eval
open Apron
let dkey = Value_parameters.register_category "d-apron"
-let ok = true
-
let debug = false
-module type S = Abstract_domain.Leaf
- with type value = Main_values.Interval.t
- and type location = Precise_locs.precise_location
-
let abort exclog =
let open Manager in
Value_parameters.fatal
@@ -357,13 +349,13 @@ let ival_to_interval = function
(* Abstract Domain Functor *)
(* -------------------------------------------------------------------------- *)
-module Make
- (Man: sig
- type t
- val manager: t Manager.t
- val name: string
- end)
-= struct
+module type Input = sig
+ type t
+ val manager: t Manager.t
+ val name: string
+end
+
+module Make (Man : Input) = struct
type state = Man.t Abstract1.t
type value = Main_values.Interval.t
@@ -753,11 +745,21 @@ end
(** Apron manager allocation changes the rounding mode. *)
let () = Floating_point.set_round_nearest_even ()
-module Octagon = Domain_builder.Complete (Make (Apron_Octagon))
-module Box = Domain_builder.Complete (Make (Apron_Box))
-module Polka_Loose = Domain_builder.Complete (Make (Apron_Polka_Loose))
-module Polka_Strict = Domain_builder.Complete (Make (Apron_Polka_Strict))
-module Polka_Equalities = Domain_builder.Complete (Make (Apron_Polka_Equalities))
+let make name enable (module Man: Input) =
+ let module Domain = Domain_builder.Complete (Make (Man)) in
+ let open Abstractions in
+ register ~enable { name;
+ values = Single (module Main_values.Interval);
+ domain = Domain (module Domain); }
+
+let () =
+ let open Value_parameters in
+ make "apron octagons" ApronOctagon.get (module Apron_Octagon);
+ make "apron box" ApronBox.get (module Apron_Box);
+ make "polka loose" PolkaLoose.get (module Apron_Polka_Loose);
+ make "polka strict" PolkaStrict.get (module Apron_Polka_Strict);
+ make "polka equalities" PolkaEqualities.get (module Apron_Polka_Equalities);
+ register_apron ()
(*
diff --git a/src/plugins/value/domains/apron/apron_domain.mli b/src/plugins/value/domains/apron/apron_domain.mli
index b330002eca9..5d86a35d509 100644
--- a/src/plugins/value/domains/apron/apron_domain.mli
+++ b/src/plugins/value/domains/apron/apron_domain.mli
@@ -24,33 +24,6 @@
the APRON library: http://apron.cri.ensmp.fr/library
For now, this binding only processes scalar integer variables. *)
-(** Are apron domains available? *)
-val ok : bool
-
-(** Signature of an Apron domain in Eva. *)
-module type S = Abstract_domain.Leaf
- with type value = Main_values.Interval.t
- and type location = Precise_locs.precise_location
-
-
-(** Apron domains available for Eva. *)
-
-(** Octagons abstract domain. *)
-module Octagon : S
-
-(** Intervals abstract domain. *)
-module Box : S
-
-(** Loose polyhedra of the NewPolka library.
- Cannot have strict inequality constraints. Algorithmically more efficient. *)
-module Polka_Loose : S
-
-(** Strict polyhedra of the NewPolka library. *)
-module Polka_Strict : S
-
-(** Linear equalities. *)
-module Polka_Equalities : S
-
(*
Local Variables:
compile-command: "make -C ../../../.."
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 118115fa8b5..ccd4fa66c36 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -77,6 +77,8 @@ let dkey_incompatible_states = register_category "incompatible-states"
let dkey_iterator = register_category "iterator"
let dkey_callbacks = register_category "callbacks"
let dkey_widening = register_category "widening"
+let dkey_experimental = register_category "experimental-ok"
+
let () =
let activate dkey = add_debug_keys dkey in
@@ -184,12 +186,23 @@ module NumerorsDomain = Domain_Parameter
let apron_help = "Experimental binding of the numerical domains provided \
by the APRON library: http://apron.cri.ensmp.fr/library \n"
+let apron_available = ref false
+let register_apron () = apron_available := true
+
+let apron_hook _ _ =
+ if not !apron_available
+ then
+ abort "an Apron domain is requested but the apron binding is not available."
+ else if not (is_debug_key_enabled dkey_experimental) then
+ warning "The Apron domains binding is experimental.";
+
module ApronOctagon = Domain_Parameter
(struct
let option_name = "-eva-apron-oct"
let help = apron_help ^ "Use the octagon domain of apron."
let default = false
end)
+let () = ApronOctagon.add_set_hook apron_hook
module ApronBox = Domain_Parameter
(struct
@@ -197,6 +210,7 @@ module ApronBox = Domain_Parameter
let help = apron_help ^ "Use the box domain of apron."
let default = false
end)
+let () = ApronBox.add_set_hook apron_hook
module PolkaLoose = Domain_Parameter
(struct
@@ -204,6 +218,7 @@ module PolkaLoose = Domain_Parameter
let help = apron_help ^ "Use the loose polyhedra domain of apron."
let default = false
end)
+let () = PolkaLoose.add_set_hook apron_hook
module PolkaStrict = Domain_Parameter
(struct
@@ -211,6 +226,7 @@ module PolkaStrict = Domain_Parameter
let help = apron_help ^ "Use the strict polyhedra domain of apron."
let default = false
end)
+let () = PolkaStrict.add_set_hook apron_hook
module PolkaEqualities = Domain_Parameter
(struct
@@ -218,6 +234,7 @@ module PolkaEqualities = Domain_Parameter
let help = apron_help ^ "Use the linear equalities domain of apron."
let default = false
end)
+let () = PolkaEqualities.add_set_hook apron_hook
module InoutDomain = Domain_Parameter
(struct
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index dc958517ee4..22a72b258e9 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -234,6 +234,8 @@ val dkey_callbacks : category
val dkey_widening : category
+(** Notifies that the binding to Apron domains is available. *)
+val register_apron: unit -> unit
(*
Local Variables:
--
GitLab