diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index b9f8d8529c95358a14b00b53f6ee29139f433a23..2a04b50f4619a3a3570669a9371e1ff65dc18e92 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -92,6 +92,12 @@ type pre_set =
type t =
| Set of Int.t array
| Float of Fval.t
+ (* [Top(min, max, rem, modulo)] represents the interval between
+ [min] and [max], congruent to [rem] modulo [modulo]. A value of
+ [None] for [min] (resp. [max]) represents -infinity
+ (resp. +infinity). [modulo] is > 0, and [0 <= rem < modulo].
+
+ Actual [Top] is thus represented by Top(None,None,Int.zero,Int.one) *)
| Top of Int.t option * Int.t option * Int.t * Int.t
(* Binary abstract operations do not model precisely float/integer operations.
It is the responsibility of the callers to have two operands of the same
@@ -326,6 +332,15 @@ let project_float v =
| Float f -> f
| Top _ | Set _ -> assert false (* by hypothesis that it is a float *)
+let is_float = function
+ | Float _ -> true
+ | Top _ -> false
+ | Set _ as i -> equal zero i || equal bottom i
+
+let is_int = function
+ | Top _ | Set _ -> true
+ | Float _ -> false
+
let in_interval x min max r modu =
Int.equal (Int.e_rem x modu) r && min_le_elt min x && max_ge_elt max x
@@ -362,6 +377,14 @@ let project_int v = match v with
| Set [| e |] -> e
| _ -> raise Not_Singleton_Int
+let is_small_set = function
+ | Set _ -> true
+ | _ -> false
+
+let project_small_set = function
+ | Set a -> Some (Array.to_list a)
+ | _ -> None
+
let cardinal v =
match v with
| Top (None,_,_,_) | Top (_,None,_,_) -> None
@@ -590,12 +613,8 @@ let min_and_max_float t =
| Float f -> Fval.min_and_max f
| _ -> assert false
-let is_float = function
- | Float _ -> true
- | Set _ | Top _ -> false
-
let has_greater_min_bound t1 t2 =
- if is_float t1 || is_float t2
+ if is_float t1 && is_float t2
then Fval.has_greater_min_bound (project_float t1) (project_float t2)
else
let m1, _ = min_and_max t1 in
@@ -607,7 +626,7 @@ let has_greater_min_bound t1 t2 =
| Some m1, Some m2 -> Int.compare m1 m2
let has_smaller_max_bound t1 t2 =
- if is_float t1 || is_float t2
+ if is_float t1 && is_float t2
then Fval.has_smaller_max_bound (project_float t1) (project_float t2)
else
let _, m1 = min_and_max t1 in
diff --git a/src/kernel_services/abstract_interp/ival.mli b/src/kernel_services/abstract_interp/ival.mli
index a94f2aa8f8c32356edcef3dd7c3c67add75b029c..628066eea2104421a4fe3fe347b50e8c606b5055 100644
--- a/src/kernel_services/abstract_interp/ival.mli
+++ b/src/kernel_services/abstract_interp/ival.mli
@@ -26,16 +26,7 @@
open Abstract_interp
-type t = private
- | Set of Int.t array
- | Float of Fval.t
- (** [Top(min, max, rem, modulo)] represents the interval between
- [min] and [max], congruent to [rem] modulo [modulo]. A value of
- [None] for [min] (resp. [max]) represents -infinity
- (resp. +infinity). [modulo] is > 0, and [0 <= rem < modulo].
-
- Actual [Top] is thus represented by Top(None,None,Int.zero,Int.one) *)
- | Top of Int.t option * Int.t option * Int.t * Int.t
+type t
(** {2 General guidelines of this module}
@@ -68,6 +59,9 @@ include Lattice_type.Full_AI_Lattice_with_cardinality
val is_bottom : t -> bool
val overlaps: partial:bool -> size:Integer.t -> t -> t -> bool
+val is_float: t -> bool
+val is_int: t -> bool
+
val add_int : t -> t -> t
(** Addition of two integer (ie. not [Float]) ivals. *)
val add_int_under : t -> t -> t
@@ -175,6 +169,10 @@ val project_int : t -> Integer.t
(** @raise Not_Singleton_Int when the cardinal of the argument is not 1,
or if it is not an integer. *)
+val is_small_set: t -> bool
+
+val project_small_set: t -> Integer.t list option
+
val cardinal: t -> Integer.t option
(** [cardinal v] returns [n] if [v] has finite cardinal [n], or [None] if
the cardinal is not finite. *)
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index 506f4f18d86809dbf22a77df367a7c1aea3f7625..c6257bfd3d4398c06b6561cad8929c3e034f7ca2 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -2061,14 +2061,17 @@ let update_under ~validity ~exact ~offsets ~size v t =
let paste_slice ~validity ~exact ~from:src ~size ~offsets dst =
if Int.(equal size zero) then (* nothing to do *) `Value dst
else
- match offsets, src with
+ let size_ok =
+ Ival.is_singleton_int offsets
+ || let _, _, _, modu = Ival.min_max_r_mod offsets in size =~ modu
+ in
+ match src with
(*Special case: [from] contains a single (aligned) binding [v], and [size]
matches the periodicity of [offsets] and the size of [v]. In this case,
it is more efficient to perform an interval update instead of an
offsetmap copy. *)
- | Ival.Top (_,_,_, offperiod), Node(_,_, Empty,_, Empty, vrem, vsize, v,_)
- when Rel.is_zero vrem && size =~ offperiod &&
- (size =~ vsize || V.is_isotropic v)
+ | Node (_,_, Empty,_, Empty, vrem, vsize, v,_)
+ when Rel.is_zero vrem && size_ok && (size =~ vsize || V.is_isotropic v)
->
update ~validity ~exact ~offsets ~size v dst
| _ ->
@@ -2708,15 +2711,11 @@ module Int_Intervals = struct
in
Intervals (curr_off', i, min, max)
in
- match ival with
- | Ival.Top(None, _, _, _) | Ival.Top(_, None, _, _) | Ival.Float _ -> top
- | Ival.Top(Some mn, Some mx, _r, _m) ->
- aux_min_max mn mx
- | Ival.Set(s) ->
- if Array.length s > 0 then
- aux_min_max s.(0) s.(Array.length s - 1)
- else
- bottom
+ try
+ match Ival.min_and_max ival with
+ | None, _ | _, None -> top
+ | Some min, Some max -> aux_min_max min max
+ with Error_Bottom -> bottom
in
Cache.merge from_ival_size_aux
@@ -2735,18 +2734,19 @@ module Int_Intervals = struct
match size with
| Int_Base.Top -> Bottom (* imprecise *)
| Int_Base.Value size ->
- match ival with
- | Ival.Top(None, _, _, _) | Ival.Top(_, None, _, _) | Ival.Float _ ->
- Bottom (* imprecise *)
- | Ival.Set _ -> from_ival_size_over_cached ival size (* precise *)
- | Ival.Top (Some min, Some start_max, _, _) ->
- (* See if using [from_ival_size] would cause an approximation *)
- let max = pred (start_max +~ size) in
- let validity = Base.Known (min, max) in
- let offsets = Tr_offset.trim_by_validity ival size validity in
- if Int_Intervals_Map.update_aux_tr_offsets_approximates offsets size
- then bottom (* imprecise *)
- else from_ival_size_over_cached ival size (* precise *)
+ if Ival.is_small_set ival
+ then from_ival_size_over_cached ival size (* precise *)
+ else
+ match Ival.min_and_max ival with
+ | None, _ | _, None -> Bottom (* imprecise *)
+ | Some min, Some start_max ->
+ (* See if using [from_ival_size] would cause an approximation *)
+ let max = pred (start_max +~ size) in
+ let validity = Base.Known (min, max) in
+ let offsets = Tr_offset.trim_by_validity ival size validity in
+ if Int_Intervals_Map.update_aux_tr_offsets_approximates offsets size
+ then bottom (* imprecise *)
+ else from_ival_size_over_cached ival size (* precise *)
let range_covers_whole_type typ itvs =
match project_singleton itvs with
diff --git a/src/kernel_services/abstract_interp/tr_offset.ml b/src/kernel_services/abstract_interp/tr_offset.ml
index 1dff8c7d48b1c8cbcd94653452626b4025e4e7ed..379aa9ac52016c64693f87cad91e4739f801b7a6 100644
--- a/src/kernel_services/abstract_interp/tr_offset.ml
+++ b/src/kernel_services/abstract_interp/tr_offset.ml
@@ -47,10 +47,10 @@ let reduce_offset_by_validity origin ival size validity =
let max_valid = Int.sub max (Int.pred size) in
let valid_range = Ival.inject_range (Some min) (Some max_valid) in
let reduced_ival = Ival.narrow ival valid_range in
- match reduced_ival with
- | Ival.Float _ -> assert false
- | Ival.Set s -> if s = [||] then Invalid else Set (Array.to_list s)
- | Ival.Top (min, max, _r, modu) ->
+ match Ival.project_small_set reduced_ival with
+ | Some l -> if l = [] then Invalid else Set l
+ | None ->
+ let min, max, _r, modu = Ival.min_max_r_mod reduced_ival in
(* The bounds are finite thanks to the narrow with the valid range. *)
let min = Extlib.the min and max = Extlib.the max in
if Int.lt modu size
diff --git a/src/plugins/value/domains/cvalue/builtins_memory.ml b/src/plugins/value/domains/cvalue/builtins_memory.ml
index dac35d94de1cac889b51d9b42b3a004d8b712724..3039c1f9bbe17e922bb3f80b5a507fcba6211900 100644
--- a/src/plugins/value/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/value/domains/cvalue/builtins_memory.ml
@@ -37,11 +37,11 @@ let frama_C_is_base_aligned state actuals =
match actuals with
| [_,x,_; _,y,_] ->
let i = Cvalue.V.project_ival y in
- begin match i with
- | Ival.Set si ->
+ begin match Ival.project_small_set i with
+ | Some si ->
Location_Bytes.fold_i
(fun b _o () ->
- Array.iter
+ List.iter
(fun int ->
if not (Base.is_aligned_by b int)
then raise Found_misaligned_base)
@@ -54,7 +54,7 @@ let frama_C_is_base_aligned state actuals =
c_from = None;
c_cacheable = Value_types.Cacheable;
}
- | _ -> raise Found_misaligned_base
+ | None -> raise Found_misaligned_base
end
| _ -> raise (Builtins.Invalid_nb_of_args 2)
end
diff --git a/src/plugins/value/domains/cvalue/builtins_string.ml b/src/plugins/value/domains/cvalue/builtins_string.ml
index 3298ae3d4d48f3a32c20dcf44b40b49ba881d07c..e3ed961c845dea79c3c09c708f103da5d218ebb4 100644
--- a/src/plugins/value/domains/cvalue/builtins_string.ml
+++ b/src/plugins/value/domains/cvalue/builtins_string.ml
@@ -80,13 +80,14 @@ let read_exact_char ~offset ~from =
let min = Integer.max (the_max_int from) (pos_min_int offset) in
let offset = backward_comp_left Comp.Le offset min in
let length = Ival.sub_int offset from in
- match offset with
- | Ival.Top (_min, _max, _rem, modu) ->
+ if not (Ival.is_singleton_int offset)
+ then
+ let _, _, _, modu = Ival.min_max_r_mod offset in
let start_length = Integer.sub (pos_min_int offset) (pos_min_int from) in
let max_length = Integer.max start_length modu in
let length = backward_comp_left Comp.Lt length max_length in
offset, length
- | _ -> offset, length
+ else offset, length
(* Checks if some limits are reached after a read at [offset]. In this case,
adds these limits as possible lengths in [t], and adds null to [t]. *)
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index e45fc726212b250492260e4c551bc5c1bed3dea4..62ce07b51b98ab311330f1f79b1e12ba6348d26e 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -846,6 +846,11 @@ module G = struct
with Cvalue.V.Not_based_on_null | Ival.Not_Singleton_Int ->
raise Untranslatable
+ let has_variable_validity b =
+ match Base.validity b with
+ | Base.Variable _ -> true
+ | _ -> false
+
(* Check that [v] is an integer, or a single pointer (invariant 2 of MV).
Pointers to a single base with variable validity are also ruled out, as
the base may become weak, making the pointer imprecise and thus breaking
@@ -853,11 +858,8 @@ module G = struct
let sanitize_v v =
try
let b, i = Cvalue.V.find_lonely_key v in
- let validity = Base.validity b in
- match validity, i with
- | Base.Variable _, _
- | _, Ival.Float _ -> raise Untranslatable
- | _, _ -> ()
+ if not (Ival.is_int i) || has_variable_validity b
+ then raise Untranslatable
with Not_found -> raise Untranslatable
let add (ct1, l1: t) (ct2, l2: t) : t =
diff --git a/src/plugins/value/domains/numerors/numerors_domain.ml b/src/plugins/value/domains/numerors/numerors_domain.ml
index 6295adc0eed64e7d4495b8c1dc62ed8aba6ec0cf..65fd9d13c246ced41dd04e82ecd8afa4bb67da8b 100644
--- a/src/plugins/value/domains/numerors/numerors_domain.ml
+++ b/src/plugins/value/domains/numerors/numerors_domain.ml
@@ -100,14 +100,13 @@ end
let reduce_error cvalue error =
try
let ival = Cvalue.V.project_ival cvalue in
- match ival with
- | Ival.Float fval ->
- begin
- match Numerors_value.reduce fval error with
- | `Value error -> cvalue, error
- | `Bottom -> cvalue, error (* TODO: we should be able to reduce to bottom. *)
- end
- | _ -> cvalue, error
+ if Ival.is_float ival
+ then
+ let fval = Ival.project_float ival in
+ match Numerors_value.reduce fval error with
+ | `Value error -> cvalue, error
+ | `Bottom -> cvalue, error (* TODO: we should be able to reduce to bottom. *)
+ else cvalue, error
with Cvalue.V.Not_based_on_null -> cvalue, error
(* Reduction of the numerors value resulting from a cast from int to float type,
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index 4261513ad85956b5344086030abbb39c7cef4759..5e73c7d1374b9b9d76a5b9db7c43b7bd43eb2a60 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -337,12 +337,12 @@ let reduce_apron_itv cvalue ival =
| Some ival ->
try
let ival' = Cvalue.V.project_ival cvalue in
- (match ival' with
- | Ival.Float _ -> raise Cvalue.V.Not_based_on_null
- | _ -> ());
- let reduced_ival = Ival.narrow ival ival' in
- let cvalue = Cvalue.V.inject_ival reduced_ival in
- cvalue, Some reduced_ival
+ if Ival.is_int ival'
+ then
+ let reduced_ival = Ival.narrow ival ival' in
+ let cvalue = Cvalue.V.inject_ival reduced_ival in
+ cvalue, Some reduced_ival
+ else cvalue, Some ival
with Cvalue.V.Not_based_on_null -> cvalue, Some ival
let () =
diff --git a/src/plugins/value/legacy/eval_op.ml b/src/plugins/value/legacy/eval_op.ml
index 03b3185c5769643921278386c05c1da5c31775e6..6fb7f3dc9fef2e5aa0c4d8e37aa62a70c3b87a43 100644
--- a/src/plugins/value/legacy/eval_op.ml
+++ b/src/plugins/value/legacy/eval_op.ml
@@ -161,14 +161,17 @@ let make_loc_contiguous loc =
let base, offset =
Locations.Location_Bits.find_lonely_key loc.Locations.loc
in
- match offset, loc.Locations.size with
- | Ival.Top (Some min, Some max, _rem, modu), Int_Base.Value size
- when Int.equal modu size ->
- let size' = Int.add (Int.sub max min) modu in
- let i = Ival.inject_singleton min in
- let loc_bits = Locations.Location_Bits.inject base i in
- Locations.make_loc loc_bits (Int_Base.inject size')
- | _ -> loc
+ if Ival.is_small_set offset
+ then loc
+ else
+ let min, max, _rem, modu = Ival.min_max_r_mod offset in
+ match min, max, loc.Locations.size with
+ | Some min, Some max, Int_Base.Value size when Int.equal modu size ->
+ let size' = Int.add (Int.sub max min) modu in
+ let i = Ival.inject_singleton min in
+ let loc_bits = Locations.Location_Bits.inject base i in
+ Locations.make_loc loc_bits (Int_Base.inject size')
+ | _ -> loc
with Not_found -> loc
let apply_on_all_locs f loc state =
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 089f3c93a5eadaca570d79802bec072a5d689b64..291139e5ccded4f527783880668e75e5d550b7ed 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -1145,7 +1145,7 @@ and eval_toffset ~alarm_mode env typ toffset =
(* Note: scale_int_base would overapproximate when given a
Float. Should never happen. *)
| Int_Base.Value f ->
- (match offset with | Ival.Float _ -> assert false | _ -> ());
+ assert (Ival.is_int offset);
Ival.scale f offset
in
Ival.add_int_under offset offsrem.eunder
diff --git a/src/plugins/value/utils/eval_typ.ml b/src/plugins/value/utils/eval_typ.ml
index d749568e9f5bb57c6b531f14ef9d693a76856e19..1b3c82b59e958d818386eea2880e65ba93811faf 100644
--- a/src/plugins/value/utils/eval_typ.ml
+++ b/src/plugins/value/utils/eval_typ.ml
@@ -52,18 +52,9 @@ let offsetmap_matches_type typ_lv o =
try typ_matches (V.project_ival_bottom v)
with V.Not_based_on_null -> true (* Do not mess with pointers *)
in
- let is_float = function
- | Ival.Float _ -> true
- | Ival.Top _ -> false
- | Ival.Set _ as i -> Ival.(equal zero i || equal bottom i)
- in
- let is_int = function
- | Ival.Top _ | Ival.Set _ -> true
- | Ival.Float _ -> false
- in
match Cil.unrollType typ_lv with
- | TFloat _ -> aux is_float
- | TInt _ | TEnum _ | TPtr _ -> aux is_int
+ | TFloat _ -> aux Ival.is_float
+ | TInt _ | TEnum _ | TPtr _ -> aux Ival.is_int
| _ -> true
diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index 56124a5079b644189247e11c29afd8807e7ae581..66e5958a6e40179fc91c9fee4684a1366b319d8b 100644
--- a/src/plugins/value_types/cvalue.ml
+++ b/src/plugins/value_types/cvalue.ml
@@ -173,8 +173,8 @@ module V = struct
type. Find a matching offset with potentially the wrong type *)
find_match Bit_utils.MatchFirst, false
in
- match i with
- | Ival.Set [|o|] ->
+ match Ival.project_small_set i with
+ | Some [o] ->
(* One single offset. Use a short notation, and an even shorter one
if we represent [&b] *)
let o, ok = conv_offset o in
@@ -183,7 +183,7 @@ module V = struct
else
Format.fprintf fmt "@[%a%a%a@]"
pretty_cast ok Base.pretty_addr b Printer.pp_offset o
- | Ival.Set a -> (* Multiple offsets. We use a set notation *)
+ | Some a -> (* Multiple offsets. We use a set notation *)
(* Catch NoOffset, which we would be printed as '{, [1], [2]}. Instead,
we find a slightly deeper offset. We should never be in a different
case from array/comp, as the other types cannot have multiple
@@ -199,7 +199,7 @@ module V = struct
else o, ok
in
let arr_off, ok =
- Array.fold_right
+ List.fold_right
(fun o (l, ok)-> let o', ok' = conv_offset' o in o' :: l, ok && ok')
a ([], true)
in
@@ -208,10 +208,9 @@ module V = struct
Base.pretty_addr b
(Pretty_utils.pp_iter
~sep:",@ " List.iter Printer.pp_offset) arr_off
- | Ival.Top _ ->
+ | None ->
(* Too many offsets. Currently, we use the basic notation. *)
pretty_base_offsets_default fmt b i
- | Ival.Float _ -> assert false
with
(* Strange looking base, or no offset found. Use default printing *)
| Base.Not_a_C_variable | Bit_utils.NoMatchingOffset ->