Commit 004d61b8 authored by David Bühler's avatar David Bühler
Browse files

[Ival] Do not export the ival type.

Exports 4 new functions in ival:
- is_int and is_float
- is_small_set and project_small_set
parent 42748391
......@@ -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
......
......@@ -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. *)
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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]. *)
......
......@@ -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 =
......
......@@ -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,
......
......@@ -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 () =
......
......@@ -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 =
......
......@@ -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
......
......@@ -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
......
......@@ -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 ->
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment