From 996ee48041ec49b305738f8c32fa4d83b2aa1e4d Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@cea.fr>
Date: Thu, 29 Jul 2021 11:03:05 +0200
Subject: [PATCH] [e-acsl] move the extra guard computation in typing
---
.../e-acsl/src/analyses/bound_variables.ml | 60 -------------------
src/plugins/e-acsl/src/analyses/typing.ml | 56 +++++++++++++++++
2 files changed, 56 insertions(+), 60 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index 44a2194bfaa..88e38a22e72 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.ml
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -627,66 +627,6 @@ let compute_quantif_guards ~is_forall quantif bounded_vars p =
let goal = Option.get goal in
guards, goal
-(******************************************************************************)
-(** Type intersection *)
-(******************************************************************************)
-
-(* It could happen that the bounds provided for a quantifier [lv] are bigger
- than its type. [bounds_for_small_type] handles such cases
- and provides smaller bounds whenever possible.
- Let B be the inferred interval and R the range of [lv.typ]
- - Case 1: B \subseteq R
- Example: [\forall unsigned char c; 4 <= c <= 100 ==> 0 <= c <= 255]
- Return: B
- - Case 2: B \not\subseteq R and the bounds of B are inferred exactly
- Example: [\forall unsigned char c; 4 <= c <= 300 ==> 0 <= c <= 255]
- Return: B \intersect R
- - Case 3: B \not\subseteq R and the bounds of B are NOT inferred exactly
- Example: [\let m = n > 0 ? 4 : 341; \forall char u; 1 < u < m ==> u > 0]
- Return: R with a guard guaranteeing that [lv] does not overflow *)
-let bounds_for_small_types ~loc (t1, lv, t2) =
- match lv.lv_type with
- | Ltype _ | Lvar _ | Lreal | Larrow _ ->
- Error.not_yet "quantification over non-integer type"
- | Linteger ->
- t1, t2, None
- | Ctype ty ->
- let iv1 = Interval.(extract_ival (infer t1)) in
- let iv2 = Interval.(extract_ival (infer t2)) in
- (* Ival.join is NOT correct here:
- Eg: (Ival.join [-3..-3] [300..300]) gives {-3, 300}
- but NOT [-3..300] *)
- let iv = Ival.inject_range (Ival.min_int iv1) (Ival.max_int iv2) in
- let ity = Interval.extract_ival (Interval.extended_interv_of_typ ty) in
- if Ival.is_included iv ity then
- (* case 1 *)
- t1, t2, None
- else if Ival.is_singleton_int iv1 && Ival.is_singleton_int iv2 then begin
- (* case 2 *)
- let i = Ival.meet iv ity in
- (* now we potentially have a better interval for [lv]
- ==> update the binding *)
- Interval.Env.replace lv (Interval.Ival i);
- (* the smaller bounds *)
- let min, max = Misc.finite_min_and_max i in
- let t1 = Logic_const.tint ~loc min in
- let t2 = Logic_const.tint ~loc max in
- let ctx = Typing.number_ty_of_typ ~post:false ty in
- (* we are assured that we will not have a GMP,
- once again because we intersected with [ity] *)
- Typing.type_term ~use_gmp_opt:false ~ctx t1;
- Typing.type_term ~use_gmp_opt:false ~ctx t2;
- t1, t2, None
- end else
- (* case 3 *)
- let min, max = Misc.finite_min_and_max ity in
- let guard_lower = Logic_const.tint ~loc min in
- let guard_upper = Logic_const.tint ~loc max in
- let lv_term = Logic_const.tvar ~loc lv in
- let guard_lower = Logic_const.prel ~loc (Rle, guard_lower, lv_term) in
- let guard_upper = Logic_const.prel ~loc (Rlt, lv_term, guard_upper) in
- let guard = Logic_const.pand ~loc (guard_lower, guard_upper) in
- t1, t2, Some guard
let () = Typing.compute_quantif_guards_ref := compute_quantif_guards
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index d49de2da589..0f1094d579d 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -595,6 +595,62 @@ and type_term_offset = function
let ctx = type_offset t in
ignore (type_term ~use_gmp_opt:false ~ctx t);
type_term_offset toff
+(* It could happen that the bounds provided for a quantifier [lv] are bigger
+ than its type. [bounds_for_small_type] handles such cases
+ and provides smaller bounds whenever possible.
+ Let B be the inferred interval and R the range of [lv.typ]
+ - Case 1: B \subseteq R
+ Example: [\forall unsigned char c; 4 <= c <= 100 ==> 0 <= c <= 255]
+ Return: B
+ - Case 2: B \not\subseteq R and the bounds of B are inferred exactly
+ Example: [\forall unsigned char c; 4 <= c <= 300 ==> 0 <= c <= 255]
+ Return: B \intersect R
+ - Case 3: B \not\subseteq R and the bounds of B are NOT inferred exactly
+ Example: [\let m = n > 0 ? 4 : 341; \forall char u; 1 < u < m ==> u > 0]
+ Return: R with a guard guaranteeing that [lv] does not overflow *)
+let bounds_for_small_types ~loc (t1, lv, t2) =
+ match lv.lv_type with
+ | Ltype _ | Lvar _ | Lreal | Larrow _ ->
+ Error.not_yet "quantification over non-integer type"
+ | Linteger ->
+ t1, t2, None
+ | Ctype ty ->
+ let iv1 = Interval.(extract_ival (infer t1)) in
+ let iv2 = Interval.(extract_ival (infer t2)) in
+ (* Ival.join is NOT correct here:
+ Eg: (Ival.join [-3..-3] [300..300]) gives {-3, 300}
+ but NOT [-3..300] *)
+ let iv = Ival.inject_range (Ival.min_int iv1) (Ival.max_int iv2) in
+ let ity = Interval.extract_ival (Interval.extended_interv_of_typ ty) in
+ if Ival.is_included iv ity then
+ (* case 1 *)
+ t1, t2, None
+ else if Ival.is_singleton_int iv1 && Ival.is_singleton_int iv2 then begin
+ (* case 2 *)
+ let i = Ival.meet iv ity in
+ (* now we potentially have a better interval for [lv]
+ ==> update the binding *)
+ Interval.Env.replace lv (Interval.Ival i);
+ (* the smaller bounds *)
+ let min, max = Misc.finite_min_and_max i in
+ let t1 = Logic_const.tint ~loc min in
+ let t2 = Logic_const.tint ~loc max in
+ let ctx = Typing.number_ty_of_typ ~post:false ty in
+ (* we are assured that we will not have a GMP,
+ once again because we intersected with [ity] *)
+ Typing.type_term ~use_gmp_opt:false ~ctx t1;
+ Typing.type_term ~use_gmp_opt:false ~ctx t2;
+ t1, t2, None
+ end else
+ (* case 3 *)
+ let min, max = Misc.finite_min_and_max ity in
+ let guard_lower = Logic_const.tint ~loc min in
+ let guard_upper = Logic_const.tint ~loc max in
+ let lv_term = Logic_const.tvar ~loc lv in
+ let guard_lower = Logic_const.prel ~loc (Rle, guard_lower, lv_term) in
+ let guard_upper = Logic_const.prel ~loc (Rlt, lv_term, guard_upper) in
+ let guard = Logic_const.pand ~loc (guard_lower, guard_upper) in
+ t1, t2, Some guard
let rec type_predicate p =
Cil.CurrentLoc.set p.pred_loc;
--
GitLab