From 92314417d9a4cdc6928ba5e374e50015ebf6c783 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 1 Mar 2019 15:14:13 +0100
Subject: [PATCH] rename Fixpoint into Interval_system_solver
---
src/plugins/e-acsl/Makefile.in | 2 +-
src/plugins/e-acsl/headers/header_spec.txt | 4 +-
src/plugins/e-acsl/interval.ml | 51 ++++++++++---------
...{fixpoint.ml => interval_system_solver.ml} | 0
...ixpoint.mli => interval_system_solver.mli} | 0
5 files changed, 31 insertions(+), 26 deletions(-)
rename src/plugins/e-acsl/{fixpoint.ml => interval_system_solver.ml} (100%)
rename src/plugins/e-acsl/{fixpoint.mli => interval_system_solver.mli} (100%)
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index c7bfa9ea27a..2ac47809eb4 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -73,7 +73,7 @@ PLUGIN_CMO:= local_config \
env \
keep_status \
dup_functions \
- fixpoint \
+ interval_system_solver \
interval \
typing \
loops \
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index 99ef606045b..dd4e5417bb0 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -21,14 +21,14 @@ error.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
error.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
exit_points.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
exit_points.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-fixpoint.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-fixpoint.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
functions.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
functions.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
gmpz.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
gmpz.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
interval.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
interval.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+interval_system_solver.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+interval_system_solver.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
keep_status.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
keep_status.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
label.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index 03083cf1602..ea2e4c951f6 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -222,25 +222,30 @@ let rec infer t =
(* 1) Build a system of interval equations that constrain the
solution: do so by returning a variable when encoutering a call
of a recursive function instead of performing the usual interval
- inference BEWARE: we might be tempted to memoize the solution
- for a given function signature HOWEVER: it cannot be done in a
- straightforward manner due to the cases of functions that use C
- (global) variables in their definition (as the values of those
- variables can change between two function calls). *)
- let ieqs = Fixpoint.Ieqs.empty in
+ inference.
+
+ BEWARE: we might be tempted to memoize the solution for a given
+ function signature HOWEVER: it cannot be done in a straightforward
+ manner due to the cases of functions that use C (global) variables
+ in their definition (as the values of those variables can change
+ between two function calls).
+
+ TODO: I do not understand the remark above. The interval of a C
+ global variable is computed from its type. *)
+ let ieqs = Interval_system_solver.Ieqs.empty in
let ivar, ieqs, _ = build_ieqs t ieqs [] in
(* 2) Solve it:
The problem is probably undecidable in the general case.
Thus we just look for reasonably precise approximations
without being too computationally expensive:
simply iterate over a finite set of pre-defined intervals.
- See [Fixpoint.solve] for details. *)
+ See [Interval_system_solver.solve] for details. *)
let chain_of_ivalmax =
[| Integer.one; Integer.billion_one; Integer.max_int64 |]
(* This set can be changed based on experimental evidences,
but it works fine for now. *)
in
- Fixpoint.solve ieqs ivar chain_of_ivalmax
+ Interval_system_solver.solve ieqs ivar chain_of_ivalmax
else begin (* non-recursive case *)
(* add the arguments to the context *)
List.iter2
@@ -359,51 +364,51 @@ and build_ieqs t ieqs ivars =
args
in
(* x *)
- let ivar = Fixpoint.Ivar(li.l_var_info.lv_name, args_lty) in
+ let ivar = Interval_system_solver.Ivar(li.l_var_info.lv_name, args_lty) in
(* Adding x = g(x) if it is not yet in the system of equations.
Without this check, the algorithm would not terminate. *)
let ieqs, ivars =
- if Fixpoint.ivars_contains_ivar ivars ivar then ieqs, ivars
+ if Interval_system_solver.ivars_contains_ivar ivars ivar then ieqs, ivars
else
let iexp, ieqs, ivars =
build_ieqs (Misc.term_of_li li) ieqs (ivar :: ivars)
in
- let ieqs = Fixpoint.Ieqs.add ivar iexp ieqs in (* Adding x = g(x) *)
+ let ieqs = Interval_system_solver.Ieqs.add ivar iexp ieqs in (* Adding x = g(x) *)
ieqs, ivars
in
List.iter (fun lv -> Env.remove lv) li.l_profile;
ivar, ieqs, ivars
end else
- (try Fixpoint.Iconst(infer t), ieqs, ivars
- with Not_an_integer -> Fixpoint.Iunsupported, ieqs, ivars)
+ (try Interval_system_solver.Iconst(infer t), ieqs, ivars
+ with Not_an_integer -> Interval_system_solver.Iunsupported, ieqs, ivars)
| TConst _ ->
- (try Fixpoint.Iconst(infer t), ieqs, ivars
- with Not_an_integer -> Fixpoint.Iunsupported, ieqs, ivars)
+ (try Interval_system_solver.Iconst(infer t), ieqs, ivars
+ with Not_an_integer -> Interval_system_solver.Iunsupported, ieqs, ivars)
| TLval(TVar _, _) ->
- (try Fixpoint.Iconst(infer t), ieqs, ivars
- with Not_an_integer -> Fixpoint.Iunsupported, ieqs, ivars)
+ (try Interval_system_solver.Iconst(infer t), ieqs, ivars
+ with Not_an_integer -> Interval_system_solver.Iunsupported, ieqs, ivars)
| TBinOp (PlusA, t1, t2) ->
let iexp1, ieqs, ivars = build_ieqs t1 ieqs ivars in
let iexp2, ieqs, ivars = build_ieqs t2 ieqs ivars in
- Fixpoint.Ibinop(Fixpoint.Ival_add, iexp1, iexp2), ieqs, ivars
+ Interval_system_solver.Ibinop(Interval_system_solver.Ival_add, iexp1, iexp2), ieqs, ivars
| TBinOp (MinusA, t1, t2) ->
let iexp1, ieqs, ivars = build_ieqs t1 ieqs ivars in
let iexp2, ieqs, ivars = build_ieqs t2 ieqs ivars in
- Fixpoint.Ibinop(Fixpoint.Ival_min, iexp1, iexp2), ieqs, ivars
+ Interval_system_solver.Ibinop(Interval_system_solver.Ival_min, iexp1, iexp2), ieqs, ivars
| TBinOp (Mult, t1, t2) ->
let iexp1, ieqs, ivars = build_ieqs t1 ieqs ivars in
let iexp2, ieqs, ivars = build_ieqs t2 ieqs ivars in
- Fixpoint.Ibinop(Fixpoint.Ival_mul, iexp1, iexp2), ieqs, ivars
+ Interval_system_solver.Ibinop(Interval_system_solver.Ival_mul, iexp1, iexp2), ieqs, ivars
| TBinOp (Div, t1, t2) ->
let iexp1, ieqs, ivars = build_ieqs t1 ieqs ivars in
let iexp2, ieqs, ivars = build_ieqs t2 ieqs ivars in
- Fixpoint.Ibinop(Fixpoint.Ival_div, iexp1, iexp2), ieqs, ivars
+ Interval_system_solver.Ibinop(Interval_system_solver.Ival_div, iexp1, iexp2), ieqs, ivars
| Tif(_, t1, t2) ->
let iexp1, ieqs, ivars = build_ieqs t1 ieqs ivars in
let iexp2, ieqs, ivars = build_ieqs t2 ieqs ivars in
- Fixpoint.Ibinop(Fixpoint.Ival_union, iexp1, iexp2), ieqs, ivars
+ Interval_system_solver.Ibinop(Interval_system_solver.Ival_union, iexp1, iexp2), ieqs, ivars
| _ ->
- Fixpoint.Iunsupported, ieqs, ivars
+ Interval_system_solver.Iunsupported, ieqs, ivars
(*
Local Variables:
diff --git a/src/plugins/e-acsl/fixpoint.ml b/src/plugins/e-acsl/interval_system_solver.ml
similarity index 100%
rename from src/plugins/e-acsl/fixpoint.ml
rename to src/plugins/e-acsl/interval_system_solver.ml
diff --git a/src/plugins/e-acsl/fixpoint.mli b/src/plugins/e-acsl/interval_system_solver.mli
similarity index 100%
rename from src/plugins/e-acsl/fixpoint.mli
rename to src/plugins/e-acsl/interval_system_solver.mli
--
GitLab