From c237ac8a1ede8d2a803d8fe954517784cc05678b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 30 Jan 2019 15:00:24 +0100
Subject: [PATCH] [stdlib] normalize integer divisions
---
.../abstract_interp/abstract_interp.ml | 2 +-
.../abstract_interp/abstract_interp.mli | 2 +-
src/kernel_services/abstract_interp/base.ml | 4 +-
src/kernel_services/abstract_interp/ival.ml | 86 +++++++++----------
.../abstract_interp/offsetmap.ml | 12 +--
src/kernel_services/analysis/bit_utils.ml | 26 +++---
src/kernel_services/ast_queries/cil.ml | 2 +-
.../ast_queries/logic_utils.ml | 10 +--
src/libraries/stdlib/integer.ml | 60 ++-----------
src/libraries/stdlib/integer.mli | 39 +++++----
src/libraries/utils/floating_point.ml | 5 +-
src/plugins/constant_propagation/api.ml | 5 +-
src/plugins/loop_analysis/loop_analysis.ml | 2 +-
src/plugins/loop_analysis/slevel_analysis.ml | 2 +-
.../value/domains/cvalue/builtins_malloc.ml | 6 +-
.../value/domains/cvalue/builtins_print_c.ml | 10 +--
.../value/domains/cvalue/builtins_string.ml | 6 +-
.../value/domains/gauges/gauges_domain.ml | 8 +-
src/plugins/value/legacy/eval_op.ml | 10 +--
src/plugins/value/legacy/eval_terms.ml | 6 +-
src/plugins/value_types/cvalue.ml | 2 +-
src/plugins/value_types/widen_type.ml | 2 +-
src/plugins/wp/TacCongruence.ml | 8 +-
23 files changed, 134 insertions(+), 181 deletions(-)
diff --git a/src/kernel_services/abstract_interp/abstract_interp.ml b/src/kernel_services/abstract_interp/abstract_interp.ml
index 31bdbd7a924..3d2f1fdd6bf 100644
--- a/src/kernel_services/abstract_interp/abstract_interp.ml
+++ b/src/kernel_services/abstract_interp/abstract_interp.ml
@@ -390,7 +390,7 @@ module Int = struct
let fold f ~inf ~sup ~step acc =
(* Format.printf "Int.fold: inf:%a sup:%a step:%a@\n"
pretty inf pretty sup pretty step; *)
- let nb_loop = div (sub sup inf) step in
+ let nb_loop = e_div (sub sup inf) step in
let rec fold_incr ~counter ~inf acc =
if equal counter onethousand then
Lattice_messages.emit_costly msg_emitter
diff --git a/src/kernel_services/abstract_interp/abstract_interp.mli b/src/kernel_services/abstract_interp/abstract_interp.mli
index 140949d5b25..7a666ccfe69 100644
--- a/src/kernel_services/abstract_interp/abstract_interp.mli
+++ b/src/kernel_services/abstract_interp/abstract_interp.mli
@@ -87,7 +87,7 @@ module Rel : sig
val add_abs : Int.t -> t -> Int.t
val add : t -> t -> t
val sub_abs : Int.t -> Int.t -> t
- val pos_rem: t -> Int.t -> t
+ val e_rem: t -> Int.t -> t
val check: rem:t -> modu:Int.t -> bool
end
diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml
index b6b7af3832f..4ee29fa9fdc 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -292,9 +292,9 @@ let is_aligned_by b alignment =
else
match b with
| Var (v,_) | Allocated(v,_,_) ->
- Int.is_zero (Int.rem (Int.of_int (Cil.bytesAlignOf v.vtype)) alignment)
+ Int.is_zero (Int.e_rem (Int.of_int (Cil.bytesAlignOf v.vtype)) alignment)
| CLogic_Var (_, ty, _) ->
- Int.is_zero (Int.rem (Int.of_int (Cil.bytesAlignOf ty)) alignment)
+ Int.is_zero (Int.e_rem (Int.of_int (Cil.bytesAlignOf ty)) alignment)
| Null -> true
| String _ -> Int.is_one alignment
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index 980c2865415..94ff33306fc 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -230,7 +230,7 @@ let is_safe_modulo r modu =
let is_safe_bound bound r modu = match bound with
| None -> true
- | Some m -> Int.equal (Int.pos_rem m modu) r
+ | Some m -> Int.equal (Int.e_rem m modu) r
(* Sanity check for Top's arguments *)
let check min max r modu =
@@ -328,7 +328,7 @@ let project_float v =
| Top _ | Set _ -> assert false (* by hypothesis that it is a float *)
let in_interval x min max r modu =
- Int.equal (Int.pos_rem x modu) r && min_le_elt min x && max_ge_elt max x
+ Int.equal (Int.e_rem x modu) r && min_le_elt min x && max_ge_elt max x
let array_mem v a =
let l = Array.length a in
@@ -367,7 +367,7 @@ let cardinal v =
match v with
| Top (None,_,_,_) | Top (_,None,_,_) -> None
| Top (Some mn, Some mx,_,m) ->
- Some (Int.succ ((Int.native_div (Int.sub mx mn) m)))
+ Some (Int.succ ((Int.e_div (Int.sub mx mn) m)))
| Set s -> Some (Int.of_int (Array.length s))
| Float f -> if Fval.is_singleton f then Some Int.one else None
@@ -376,7 +376,7 @@ let cardinal_estimate v ~size =
| Set s -> Int.of_int (Array.length s)
| Top (None, _, _, _)
| Top (_, None, _, _) -> Int.two_power size
- | Top (Some mn, Some mx, _, d) -> Int.(succ (div (sub mx mn) d))
+ | Top (Some mn, Some mx, _, d) -> Int.(succ (e_div (sub mx mn) d))
| Float f ->
if Fval.is_singleton f
then Int.one
@@ -397,7 +397,7 @@ let cardinal_less_than v n =
match v with
| Top (None,_,_,_) | Top (_,None,_,_) -> raise Not_less_than
| Top (Some mn, Some mx,_,m) ->
- Int.succ ((Int.native_div (Int.sub mx mn) m))
+ Int.succ ((Int.e_div (Int.sub mx mn) m))
| Set s -> Int.of_int (Array.length s)
| Float f ->
if Fval.is_singleton f then Int.one else raise Not_less_than
@@ -419,7 +419,7 @@ let make ~min ~max ~rem ~modu =
match min, max with
| Some mn, Some mx ->
if Int.gt mx mn then
- let l = Int.succ (Int.div (Int.sub mx mn) modu) in
+ let l = Int.succ (Int.e_div (Int.sub mx mn) modu) in
if Int.le l !small_cardinal_Int
then
let l = Int.to_int l in
@@ -449,7 +449,7 @@ let inject_interval ~min ~max ~rem:r ~modu =
assert (is_safe_modulo r modu);
let fix_bound fix bound = match bound with
| None -> None
- | Some b -> Some (if Int.equal b (Int.pos_rem r modu) then b else fix b)
+ | Some b -> Some (if Int.equal b (Int.e_rem r modu) then b else fix b)
in
let min = fix_bound (fun min -> Int.round_up_to_r ~min ~r ~modu) min
and max = fix_bound (fun max -> Int.round_down_to_r ~max ~r ~modu) max in
@@ -470,7 +470,7 @@ let subdiv_int v =
share_array lo m,
share_array hi lenhi
| Top (Some lo, Some hi, rem, modu) ->
- let mean = Int.native_div (Int.add lo hi) Int.two in
+ let mean = Int.e_div (Int.add lo hi) Int.two in
let succmean = Int.succ mean in
inject_interval ~min:(Some lo) ~max:(Some mean) ~rem ~modu,
inject_interval ~min:(Some succmean) ~max:(Some hi) ~rem ~modu
@@ -503,7 +503,7 @@ let unsafe_make_top_from_set_4 s =
s
Int.zero
in
- let r = Int.pos_rem m modu in
+ let r = Int.e_rem m modu in
let max = O.max_elt s in
let min = m in
(min,max,r,modu)
@@ -521,7 +521,7 @@ let unsafe_make_top_from_array_4 s =
Int.zero
s
in
- let r = Int.pos_rem m modu in
+ let r = Int.e_rem m modu in
let max = Some s.(pred l) in
let min = Some m in
check min max r modu;
@@ -565,7 +565,7 @@ let inject_ps ps =
match ps with
Pre_set(o, s) -> share_set o s
| Pre_top (min, max, modu) ->
- Top(Some min, Some max, Int.pos_rem min modu, modu)
+ Top(Some min, Some max, Int.e_rem min modu, modu)
let min_max_r_mod t =
match t with
@@ -648,7 +648,7 @@ let widen (bitsize,wh) t1 t2 =
let (mn2,mx2,r2,m2) = min_max_r_mod t2 in
let (mn1,mx1,r1,m1) = min_max_r_mod t1 in
let new_mod = Int.pgcd (Int.pgcd m1 m2) (Int.abs (Int.sub r1 r2)) in
- let new_rem = Int.rem r1 new_mod in
+ let new_rem = Int.e_rem r1 new_mod in
let new_min = if bound_compare mn1 mn2 = 0 then mn2 else
match mn2 with
| None -> None
@@ -717,7 +717,7 @@ let extended_euclidian_algorithm a b =
let x = ref Int.zero and lastx = ref Int.one in
let y = ref Int.one and lasty = ref Int.zero in
while not (Int.is_zero !b) do
- let (q,r) = Int.div_rem !a !b in
+ let (q,r) = Int.e_div_rem !a !b in
a := !b;
b := r;
let tmpx = !x in
@@ -746,7 +746,7 @@ let compute_r_common r1 m1 r2 m2 =
<=> \E k1,k2: x = r1 + k1*m1 && x = r2 + k2*m2
<=> \E k1,k2: x = r1 + k1*m1 && k1*m1 - k2*m2 = r2 - r1
- Let c = r2 - r1. The equation (E2): k1*m1 - k2*m2 = c is
+ Let r = r2 - r1. The equation (E2): k1*m1 - k2*m2 = r is
diophantine; there are solutions x to (E1) iff there are
solutions (k1,k2) to (E2).
@@ -754,19 +754,19 @@ let compute_r_common r1 m1 r2 m2 =
divides c (because d divides k1*m1 - k2*m2). Else we raise
[Error_Bottom]. *)
let (x1,_,pgcd) = extended_euclidian_algorithm m1 m2 in
- let c = Int.sub r2 r1 in
- let (c_div_d,c_rem) = Int.div_rem c pgcd in
- if not (Int.equal c_rem Int.zero)
+ let r = Int.sub r2 r1 in
+ let r_div,r_rem = Int.e_div_rem r pgcd in
+ if not (Int.equal r_rem Int.zero)
then raise Error_Bottom
(* The extended euclidian algorithm has provided solutions x1,x2 to
the Bezout identity x1*m1 + x2*m2 = d.
- x1*m1 + x2*m2 = d ==> x1*(c/d)*m1 + x2*(c/d)*m2 = d*(c/d).
+ x1*m1 + x2*m2 = d ==> x1*(c/d)*m1 + x2*(r/d)*m2 = d*(r/d).
- Thus, k1 = x1*(c/d), k2=-x2*(c/d) are solutions to (E2)
- Thus, x = r1 + x1*(c/d)*m1 is a particular solution to (E1). *)
- else let k1 = Int.mul x1 c_div_d in
+ Thus, k1 = x1*(r/d), k2=-x2*(r/d) are solutions to (E2)
+ Thus, x = r1 + x1*(r/d)*m1 is a particular solution to (E1). *)
+ else let k1 = Int.mul x1 r_div in
let x = Int.add r1 (Int.mul k1 m1) in
(* If two solutions x and y exist, they are equal modulo ppcm(m1,m2).
@@ -777,7 +777,7 @@ let compute_r_common r1 m1 r2 m2 =
of ppcm(m1,m2). Thus x = y mod ppcm(m1,m2). *)
let ppcm = Integer.ppcm m1 m2 in
(* x may be bigger than the ppcm, we normalize it. *)
- (Int.rem x ppcm, ppcm)
+ (Int.e_rem x ppcm, ppcm)
;;
let array_truncate r i =
@@ -1021,7 +1021,7 @@ let join v1 v2 =
check mn1 mx1 r1 m1;
check mn2 mx2 r2 m2;
let modu = Int.pgcd (Int.pgcd m1 m2) (Int.abs(Int.sub r1 r2)) in
- let r = Int.rem r1 modu in
+ let r = Int.e_rem r1 modu in
let min = min_min mn1 mn2 in
let max = max_max mx1 mx2 in
let r = inject_top min max r modu in
@@ -1033,7 +1033,7 @@ let join v1 v2 =
else
let f modu elt = Int.pgcd modu (Int.abs(Int.sub r elt)) in
let new_modu = Array.fold_left f modu s in
- let new_r = Int.rem r new_modu in
+ let new_r = Int.e_rem r new_modu in
let new_min = match min with
None -> None
| Some m -> Some (Int.min m s.(0))
@@ -1194,7 +1194,7 @@ let max_is_greater mx1 mx2 =
Int.ge m1 m2
let rem_is_included r1 m1 r2 m2 =
- (Int.is_zero (Int.rem m1 m2)) && (Int.equal (Int.rem r1 m2) r2)
+ (Int.is_zero (Int.e_rem m1 m2)) && (Int.equal (Int.e_rem r1 m2) r2)
let array_for_all f (a : Integer.t array) =
let l = Array.length a in
@@ -1238,7 +1238,7 @@ let is_included t1 t2 =
(* Inclusion of bounds is needed for the entire inclusion *)
min_le_elt min s.(0) && max_ge_elt max s.(Array.length s-1)
&& (Int.equal Int.one modu || (*Top side contains all integers, we're done*)
- array_for_all (fun x -> Int.equal (Int.pos_rem x modu) r) s)
+ array_for_all (fun x -> Int.equal (Int.e_rem x modu) r) s)
| Set s1, Set s2 -> array_subset s1 s2
| Float f1, Float f2 -> Fval.is_included f1 f2
| Float _, _ -> equal t2 top
@@ -1385,7 +1385,7 @@ let add_singleton_int i v = match v with
let incr v = Int.add i v in
let new_mn = opt1 incr mn in
let new_mx = opt1 incr mx in
- let new_r = Int.pos_rem (incr r) m in
+ let new_r = Int.e_rem (incr r) m in
share_top new_mn new_mx new_r m
@@ -1398,7 +1398,7 @@ let rec add_int v1 v2 =
apply2_n Int.add s1 s2
| Top(mn1,mx1,r1,m1), Top(mn2,mx2,r2,m2) ->
let m = Int.pgcd m1 m2 in
- let r = Int.rem (Int.add r1 r2) m in
+ let r = Int.e_rem (Int.add r1 r2) m in
let mn =
try
Some (Int.round_up_to_r (opt2 Int.add mn1 mn2) r m)
@@ -1435,7 +1435,7 @@ let add_int_under v1 v2 = match v1,v2 with
when Int.equal modu1 modu2 ->
(* Note: min1+min2 % modu = max1 + max2 % modu = r1 + r2 % modu;
no need to trim the bounds here. *)
- let r = Int.rem (Int.add r1 r2) modu1 in
+ let r = Int.e_rem (Int.add r1 r2) modu1 in
let min = match min1, min2 with
| Some min1, Some min2 -> Some (Int.add min1 min2)
| _ -> None in
@@ -1473,7 +1473,7 @@ let neg_int v =
share_top
(opt1 Int.neg mx)
(opt1 Int.neg mn)
- (Int.pos_rem (Int.neg r) m)
+ (Int.e_rem (Int.neg r) m)
m
let sub_int v1 v2 = add_int v1 (neg_int v2)
@@ -1544,12 +1544,12 @@ let scale f v =
let modu = incr m1 in
share_top
(opt1 incr mn1) (opt1 incr mx1)
- (Int.pos_rem (incr r1) modu) modu
+ (Int.e_rem (incr r1) modu) modu
else
let modu = Int.neg (incr m1) in
share_top
(opt1 incr mx1) (opt1 incr mn1)
- (Int.pos_rem (incr r1) modu) modu
+ (Int.e_rem (incr r1) modu) modu
| Set s ->
if Int.ge f Int.zero
then apply_bin_1_strict_incr Int.mul f s
@@ -1561,7 +1561,7 @@ let scale_div_common ~pos f v degenerate_ival degenerate_float =
assert (not (Int.is_zero f));
let div_f =
if pos
- then fun a -> Int.pos_div a f
+ then fun a -> Int.e_div a f
else fun a -> Int.c_div a f
in
match v with
@@ -1571,12 +1571,12 @@ let scale_div_common ~pos f v degenerate_ival degenerate_float =
if (negative (* all negative *) ||
pos (* good div *) ||
(min_is_lower (some_zero) mn1) (* all positive *) ||
- (Int.is_zero (Int.rem r1 f)) (* exact *) )
- && (Int.is_zero (Int.rem m1 f))
+ (Int.is_zero (Int.e_rem r1 f)) (* exact *) )
+ && (Int.is_zero (Int.e_rem m1 f))
then
let modu = Int.abs (div_f m1) in
let r = if negative then Int.sub r1 m1 else r1 in
- (Int.pos_rem (div_f r) modu), modu
+ (Int.e_rem (div_f r) modu), modu
else (* degeneration*)
degenerate_ival r1 m1
in
@@ -1692,12 +1692,12 @@ let scale_rem ~pos f v =
else
let f = if Int.lt f Int.zero then Int.neg f else f in
let rem_f a =
- if pos then Int.pos_rem a f else Int.c_rem a f
+ if pos then Int.e_rem a f else Int.c_rem a f
in
match v with
| Top(mn,mx,r,m) ->
let modu = Int.pgcd f m in
- let rr = Int.pos_rem r modu in
+ let rr = Int.e_rem r modu in
let binf,bsup =
if pos
then (Int.round_up_to_r ~min:Int.zero ~r:rr ~modu),
@@ -1716,7 +1716,7 @@ let scale_rem ~pos f v =
match mn,mx with
| Some mn,Some mx ->
let div_f a =
- if pos then Int.pos_div a f else Int.c_div a f
+ if pos then Int.e_div a f else Int.c_div a f
in
(* See if [mn..mx] is included in [k*f..(k+1)*f] for some [k]. In
this case, [%] is monotonic and [mn%f .. mx%f] is a more precise
@@ -1833,7 +1833,7 @@ let cast_int_to_int ~size ~signed value =
let not_p_factor = Int.neg factor in
let best_effort r m =
let modu = Int.pgcd factor m in
- let rr = Int.pos_rem r modu in
+ let rr = Int.e_rem r modu in
let min_val = Some (if signed then
Int.round_up_to_r ~min:(Int.neg mask) ~r:rr ~modu
else
@@ -1863,7 +1863,7 @@ let cast_int_to_int ~size ~signed value =
then value
else
let new_min = rem_f mn in
- let new_r = Int.pos_rem new_min m in
+ let new_r = Int.e_rem new_min m in
inject_top (Some new_min) (Some (rem_f mx)) new_r m
else best_effort r m
| Top (_,_,r,m) ->
@@ -1957,7 +1957,7 @@ let rec mul v1 v2 =
let modu = Int.ppcm modu1 modu2 in *)
let modu = Int.(pgcd (pgcd (mul m1 m2) (mul r1 m2)) (mul r2 m1))
in
- let r = Int.rem (Int.mul r1 r2) modu in
+ let r = Int.e_rem (Int.mul r1 r2) modu in
(* let t = Top (ext_proj min, ext_proj max, r, modu) in
Format.printf "mul. Result: '%a'@\n" pretty t; *)
inject_top (ext_proj min) (ext_proj max) r modu
@@ -2017,7 +2017,7 @@ module Infty = struct
| None -> None
| Some a -> match b with
| None -> Some Int.zero
- | Some b -> Some (Int.div a b)
+ | Some b -> Some (Int.e_div a b)
let neg = function
| Some a -> Some (Int.neg a)
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index 65b75830d44..01dba5d8ede 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -33,8 +33,8 @@ let ( >=~ ) = Integer.ge
let ( +~ ) = Integer.add
let ( -~ ) = Integer.sub
(* let ( *~ ) = Integer.mul *)
-let ( /~ ) = Integer.pos_div
-let ( %~ ) = Integer.pos_rem
+let ( /~ ) = Integer.e_div
+let ( %~ ) = Integer.e_rem
let succ = Integer.succ
let pred = Integer.pred
@@ -90,7 +90,7 @@ type 'a offsetmap =
alignment must be recomputed wrt the offset of the new interval. The new
alignment should be consistent with the size of the value. *)
let realign ~offset ~new_offset rem modu =
- Rel.pos_rem (Rel.add (Rel.sub_abs offset new_offset) rem) modu
+ Rel.e_rem (Rel.add (Rel.sub_abs offset new_offset) rem) modu
(** plevel-related operation: value + hooks to call when the value is modified*)
let plevel = ref 200
@@ -1007,7 +1007,7 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
else
begin (* abs_max1 >~ abs_max2 *)
let min = succ abs_max2 in
- let rem1 = Rel.pos_rem (Rel.add (Rel.sub_abs o1 min) rem1) modu1 in
+ let rem1 = Rel.e_rem (Rel.add (Rel.sub_abs o1 min) rem1) modu1 in
let new_offr1, new_subr1 =
add_node ~min ~max:abs_max1 rem1 modu1 v1 abs_offr1 subr1
in
@@ -1978,7 +1978,7 @@ let update_under ~validity ~exact ~offsets ~size v t =
let lmin = Integer.max imin curr_off in
let lmax = Integer.min imax abs_max in
let lrem =
- Rel.pos_rem (Rel.sub rem (Rel.sub_abs lmin curr_off)) modu
+ Rel.e_rem (Rel.sub rem (Rel.sub_abs lmin curr_off)) modu
in
f (lmin, lmax) (v, modu, lrem) acc
in
@@ -2123,7 +2123,7 @@ let update_under ~validity ~exact ~offsets ~size v t =
(if Int.length bk ek >~ modu then
Format.fprintf fmt " repeated %%%a " pretty_int modu)
else (
- let b_bits = Rel.pos_rem (Rel.sub Rel.zero rel_offs) modu in
+ let b_bits = Rel.e_rem (Rel.sub Rel.zero rel_offs) modu in
let e_bits = Rel.add_abs (ek -~ bk) b_bits in
Format.fprintf fmt "%s%%%a, bits %a to %a "
(if e_bits >~ modu then " repeated " else "")
diff --git a/src/kernel_services/analysis/bit_utils.ml b/src/kernel_services/analysis/bit_utils.ml
index 136e7693700..138752a8060 100644
--- a/src/kernel_services/analysis/bit_utils.ml
+++ b/src/kernel_services/analysis/bit_utils.ml
@@ -191,7 +191,7 @@ let rec pretty_bits_internal env bfinfo typ ~align ~start ~stop =
let raw_bits c start stop =
let cond =
env.use_align
- && ((not (Integer.equal (Integer.pos_rem start env.rh_size) align))
+ && ((not (Integer.equal (Integer.e_rem start env.rh_size) align))
|| (not (Integer.equal req_size env.rh_size)))
in
Format.fprintf env.fmt "[%s%t]%s"
@@ -272,7 +272,7 @@ let rec pretty_bits_internal env bfinfo typ ~align ~start ~stop =
| Some i -> Bitfield (Integer.to_int64 (Integer.of_int i))
in
let new_align =
- Integer.pos_rem (Integer.sub align start_o) env.rh_size
+ Integer.e_rem (Integer.sub align start_o) env.rh_size
in
let name = Format.asprintf "%a" Printer.pp_field field in
NamedField( name ,
@@ -348,13 +348,11 @@ let rec pretty_bits_internal env bfinfo typ ~align ~start ~stop =
if Integer.is_zero size then
raw_bits 'z' start stop
else
- let start_case = Integer.pos_div start size in
- let stop_case = Integer.pos_div stop size in
- let rem_start_size = Integer.pos_rem start size in
- let rem_stop_size = Integer.pos_rem stop size in
+ let start_case,rem_start_size = Integer.e_div_rem start size in
+ let stop_case,rem_stop_size = Integer.e_div_rem stop size in
if Integer.equal start_case stop_case then (** part of one element *)
let new_align =
- Integer.pos_rem
+ Integer.e_rem
(Integer.sub align (Integer.mul start_case size))
env.rh_size
in
@@ -363,8 +361,8 @@ let rec pretty_bits_internal env bfinfo typ ~align ~start ~stop =
~align:new_align
~start:rem_start_size
~stop:rem_stop_size
- else if Integer.equal (Integer.rem start env.rh_size) align
- && (Integer.is_zero (Integer.rem size env.rh_size))
+ else if Integer.equal (Integer.e_rem start env.rh_size) align
+ && (Integer.is_zero (Integer.e_rem size env.rh_size))
then
let pred_size = Integer.pred size in
let start_full_case =
@@ -427,7 +425,7 @@ let pretty_bits typ ~use_align ~align ~rh_size ~start ~stop fmt =
Cil easily gives offset information in terms of offset since the start,
but not easily the offset between two fields (with padding) *)
let align =
- Integer.pos_rem (Abstract_interp.Rel.add_abs start align) rh_size
+ Integer.e_rem (Abstract_interp.Rel.add_abs start align) rh_size
in
assert (Integer.le Integer.zero align
&& Integer.lt align rh_size);
@@ -533,9 +531,9 @@ let rec find_offset typ ~offset om =
Index (minus_one_expr, NoOffset), typ
end
else
- let start = Integer.pos_div offset size_elt in
+ let start = Integer.e_div offset size_elt in
let exp_start = Cil.kinteger64 ~loc start in
- let rem = Integer.pos_rem offset size_elt in
+ let rem = Integer.e_rem offset size_elt in
if offset_match_cell om size_elt then
(* [size] covers at most one cell; we continue in the relevant one *)
let off, typ = find_offset typ_elt rem om in
@@ -545,10 +543,10 @@ let rec find_offset typ ~offset om =
| MatchFirst | MatchType _ -> raise NoMatchingOffset
| MatchSize size ->
if Integer.is_zero rem
- && Integer.is_zero (Integer.rem size size_elt)
+ && Integer.is_zero (Integer.e_rem size size_elt)
then
(* We cover more than one cell, but we are aligned. *)
- let nb = Integer.div size size_elt in
+ let nb = Integer.e_div size size_elt in
let exp_nb = Cil.kinteger64 ~loc nb in
let typ =
TArray (typ_elt, Some exp_nb, Cil.empty_size_cache (),[])
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index a76eabb3b74..027a3758727 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -3995,7 +3995,7 @@ let truncateInteger64 (k: ikind) i =
let i' =
let nrBits = Integer.of_int (8 * (bytesSizeOfInt k)) in
let max_strict_bound = Integer.shift_left Integer.one nrBits in
- let modulo = Integer.pos_rem i max_strict_bound in
+ let modulo = Integer.e_rem i max_strict_bound in
let signed = isSigned k in
if signed then
let max_signed_strict_bound =
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index e43be1ffbcd..9ad4de77133 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -2346,9 +2346,9 @@ and constFoldBinOpToInt ~machdep bop e1 e2 =
| PlusPI | IndexPI | MinusPI | MinusPP -> None
| Mult -> Some (Integer.mul i1 i2)
| Div ->
- if Integer.(equal zero i2) && Integer.(is_zero (rem i1 i2)) then None
- else Some (Integer.div i1 i2)
- | Mod -> if Integer.(equal zero i2) then None else Some (Integer.rem i1 i2)
+ if Integer.(equal zero i2) && Integer.(is_zero (e_rem i1 i2)) then None
+ else Some (Integer.e_div i1 i2)
+ | Mod -> if Integer.(equal zero i2) then None else Some (Integer.e_rem i1 i2)
| BAnd -> Some (Integer.logand i1 i2)
| BOr -> Some (Integer.logor i1 i2)
| BXor -> Some (Integer.logxor i1 i2)
@@ -2377,8 +2377,8 @@ and constFoldToffset t =
try
let start, _width = bitsLogicOffset v.lv_type offset in
let size_char = Integer.eight in
- if Integer.(is_zero (rem start size_char)) then
- Some (Integer.div start size_char)
+ if Integer.(is_zero (e_rem start size_char)) then
+ Some (Integer.e_div start size_char)
else None (* bitfields *)
with Cil.SizeOfError _ -> None
end
diff --git a/src/libraries/stdlib/integer.ml b/src/libraries/stdlib/integer.ml
index e6ac8c03d77..97b5017821d 100644
--- a/src/libraries/stdlib/integer.ml
+++ b/src/libraries/stdlib/integer.ml
@@ -62,10 +62,16 @@ let succ = Z.succ
let pred = Z.pred
let neg = Z.neg
-let rem = Z.erem
-let div = Z.ediv
let mul = Z.mul
+let e_div = Z.ediv
+let e_rem = Z.erem
+let e_div_rem = Z.ediv_rem
+
+let c_div = Z.div
+let c_rem = Z.rem
+let c_div_rem = Z.div_rem
+
let abs = Z.abs
let hash = Z.hash
@@ -191,54 +197,6 @@ let pretty ?(hexa=false) fmt v =
let is_one v = equal one v
-let pos_div = div
-let pos_rem = rem
-let native_div = div
-let divexact = Z.divexact
-let div_rem = Z.div_rem
-
-(*
-let _c_div u v =
- let bad_div = div u v in
- if (lt u zero) && not (is_zero (rem u v))
- then
- if lt v zero
- then pred bad_div
- else succ bad_div
- else bad_div
-
-let _c_div u v =
- let res = _c_div u v in
- let res2 = Z.div u v in
- if not (equal res res2) then
- failwith (Printf.sprintf "division of %a %a c_div %a div %a"
- Z.sprint u
- Z.sprint v
- Z.sprint res
- Z.sprint res2)
- else res2
-*)
-
-let c_div = Z.div
-
-(*
-let _c_rem u v =
- sub u (mul v (c_div u v))
-
-let _c_rem u v =
- let res = _c_rem u v in
- let res2 = Z.rem u v in
- if not (equal res res2) then
- failwith (Printf.sprintf "division of %a %a c_rem %a rem %a"
- Z.sprint u
- Z.sprint v
- Z.sprint res
- Z.sprint res2)
- else res2
-*)
-
-let c_rem = Z.rem
-
let cast ~size ~signed ~value =
if (not signed)
then
@@ -276,7 +234,7 @@ let min = Z.min
let max = Z.max
let round_down_to_zero v modu =
- mul (pos_div v modu) modu
+ mul (e_div v modu) modu
let round_up_to_r ~min:m ~r ~modu =
add (add (round_down_to_zero (pred (sub m r)) modu) r) modu
diff --git a/src/libraries/stdlib/integer.mli b/src/libraries/stdlib/integer.mli
index 1e8202750a9..8f6fffda546 100644
--- a/src/libraries/stdlib/integer.mli
+++ b/src/libraries/stdlib/integer.mli
@@ -54,34 +54,35 @@ val lognot : t -> t
val min : t -> t -> t
val max : t -> t -> t
-val native_div : t -> t -> t
+val e_div : t -> t -> t
+(** Euclidean division (that returns a positive rem).
+ Implemented by [Z.ediv]
-val div : t -> t -> t
-(** Euclidean division (that returns a positive rem) *)
-
-val pos_div : t -> t -> t
-(** Euclidean division. Equivalent to C division if both operands are positive.
+ Equivalent to C division if both operands are positive.
Equivalent to a floored division if b > 0 (rounds downwards),
otherwise rounds upwards.
- Note: it is possible that pos_div (-a) b <> pos_div a (-b). *)
+ Note: it is possible that pos_div (-a) b <> pos_div a (-b).
+*)
-val divexact: t -> t -> t
-(** Faster, but produces correct results only when b evenly divides a. *)
+val e_rem : t -> t -> t
+(** Remainder of the Euclidean division (always positive).
+ Implemented by [Z.erem] *)
-val c_div : t -> t -> t
-(** Truncated division towards 0 (like in C99) *)
+val e_div_rem: t -> t -> (t * t)
+(** [e_div_rem a b] returns [(e_div a b, e_rem a b)].
+ Implemented by [Z.ediv_rem] *)
-val rem : t -> t -> t
-(** Remainder of the Euclidean division (always positive) *)
+val c_div : t -> t -> t
+(** Truncated division towards 0 (like in C99).
+ Implemented by [Z.div] *)
val c_rem : t -> t -> t
-(** Remainder of the truncated division towards 0 (like in C99) *)
-
-val div_rem: t -> t -> (t * t)
-(** [div_rem a b] returns [(pos_div a b, pos_rem a b)] *)
+(** Remainder of the truncated division towards 0 (like in C99).
+ Implemented by [Z.rem] *)
-val pos_rem : t -> t -> t
-(** Remainder of the Euclidean division (always positive) *)
+val c_div_rem : t -> t -> t * t
+(** Remainder of the truncated division towards 0 (like in C99.
+ Implemented by [Z.div_rem] *)
val pgcd : t -> t -> t
(** [pgcd v 0 == pgcd 0 v == abs v]. Result is always positive *)
diff --git a/src/libraries/utils/floating_point.ml b/src/libraries/utils/floating_point.ml
index c8361ffa26a..bc487fe40a9 100644
--- a/src/libraries/utils/floating_point.ml
+++ b/src/libraries/utils/floating_point.ml
@@ -102,10 +102,7 @@ let make_float ~num ~den ~exp ~man_size ~min_exp ~max_exp =
*)
if exp > max_exp - man_size then inf ~man_size ~max_exp
else
- let man = Integer.native_div num den in
- let rem =
- Integer.sub num (Integer.mul den man)
- in
+ let man,rem = Integer.e_div_rem num den in
let rem2 = (* twice the remainder *)
Integer.shift_left rem Integer.one
in
diff --git a/src/plugins/constant_propagation/api.ml b/src/plugins/constant_propagation/api.ml
index 46fcc0277d1..58c9aa199a6 100644
--- a/src/plugins/constant_propagation/api.ml
+++ b/src/plugins/constant_propagation/api.ml
@@ -181,9 +181,8 @@ class propagate project fnames ~cast_intro = object(self)
in
array, Int_Base.project size
in
- array,
- (Integer.pos_div offset sizeof_pointed),
- (Integer.pos_rem offset sizeof_pointed)
+ let div,rem = Integer.e_div_rem offset sizeof_pointed in
+ array,div,rem
in
let expr' =
if array then
diff --git a/src/plugins/loop_analysis/loop_analysis.ml b/src/plugins/loop_analysis/loop_analysis.ml
index 9236b5240a4..a5966da7fa8 100644
--- a/src/plugins/loop_analysis/loop_analysis.ml
+++ b/src/plugins/loop_analysis/loop_analysis.ml
@@ -439,7 +439,7 @@ module Store(* (B:sig *)
may be missed;
2. in '<=' and '>=' loops, to adjust for the last iteration *)
let divident = Integer.sub bound offset in
- let remainder = Integer.rem divident increment in
+ let remainder = Integer.e_rem divident increment in
(* check if induction variable may miss termination condition *)
if binop = Cil_types.Ne && not Integer.(equal remainder zero) then
Options.warning ~current:true
diff --git a/src/plugins/loop_analysis/slevel_analysis.ml b/src/plugins/loop_analysis/slevel_analysis.ml
index 898570e1999..b17e64142f2 100644
--- a/src/plugins/loop_analysis/slevel_analysis.ml
+++ b/src/plugins/loop_analysis/slevel_analysis.ml
@@ -112,7 +112,7 @@ module Specific(KF:sig val kf: Kernel_function.t end) = struct
Integer.power_int_positive_int in_loop_i (max_iteration + 1)
in
let slevel_inside_loop =
- Integer.div (Integer.pred s) (Integer.pred in_loop)
+ Integer.e_div (Integer.pred s) (Integer.pred in_loop)
in
let result = Integer.mul entry slevel_inside_loop in
(* Kernel.feedback "s %a slevel_inside_loop %a result %a" *)
diff --git a/src/plugins/value/domains/cvalue/builtins_malloc.ml b/src/plugins/value/domains/cvalue/builtins_malloc.ml
index ae944aa55f8..b696a031f3c 100644
--- a/src/plugins/value/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/value/domains/cvalue/builtins_malloc.ml
@@ -192,7 +192,7 @@ let guess_intended_malloc_type stack sizev constant_size =
let nb_elems elem_size =
if constant_size && Int.equal size_min size_max
then Some (if Int.(equal elem_size zero) then Int.zero
- else Int.div size_min elem_size)
+ else Int.e_div size_min elem_size)
else None
in
let mk_typed_size t =
@@ -200,8 +200,8 @@ let guess_intended_malloc_type stack sizev constant_size =
| TPtr (t, _) when not (Cil.isVoidType t) ->
let s = Int.of_int (Cil.bytesSizeOf t) in
if Int.(equal s zero) ||
- (Int.equal (Int.rem size_min s) Int.zero &&
- Int.equal (Int.rem size_max s) Int.zero)
+ (Int.equal (Int.e_rem size_min s) Int.zero &&
+ Int.equal (Int.e_rem size_max s) Int.zero)
then
{ min_bytes = size_min; max_bytes = size_max;
elem_typ = t; nb_elems = nb_elems s }
diff --git a/src/plugins/value/domains/cvalue/builtins_print_c.ml b/src/plugins/value/domains/cvalue/builtins_print_c.ml
index dc13b3c198b..7a05b408018 100644
--- a/src/plugins/value/domains/cvalue/builtins_print_c.ml
+++ b/src/plugins/value/domains/cvalue/builtins_print_c.ml
@@ -227,12 +227,12 @@ let value_uninit_pretty cas prampamp lv s fmt = function
let offsetmap_pretty cas name print_ampamp fmt offsm =
let pretty_binding (bk,ek) (v, modu, offset) =
let iso = V_Or_Uninitialized.is_isotropic v in
- if Integer.is_zero (Integer.rem bk Integer.eight)
+ if Integer.is_zero (Integer.e_rem bk Integer.eight)
&& (Rel.is_zero offset)
- && (iso || (Integer.is_zero (Integer.rem modu Integer.eight)))
+ && (iso || (Integer.is_zero (Integer.e_rem modu Integer.eight)))
then
let ek = Integer.succ ek in
- if Integer.is_zero (Integer.rem ek Integer.eight)
+ if Integer.is_zero (Integer.e_rem ek Integer.eight)
then
let step = if iso then 1 else (Integer.to_int modu) / 8 in
let start = ref ((Integer.to_int bk) / 8) in
@@ -302,10 +302,10 @@ let print_declarations_for_malloc_bases fmt =
let dim =
match validity with
| Base.Known (l,u) when (Int.is_zero l)->
- Int.div (Int.succ u) Int.eight
+ Int.e_div (Int.succ u) Int.eight
| Base.Variable { Base.min_alloc; max_alloc } when
Int.(ge min_alloc zero && equal min_alloc max_alloc) ->
- Int.div (Int.succ min_alloc) Int.eight
+ Int.e_div (Int.succ min_alloc) Int.eight
| _ -> Kernel.abort ~current:true "got unexpected validity: %a"
Base.pretty_validity validity
in
diff --git a/src/plugins/value/domains/cvalue/builtins_string.ml b/src/plugins/value/domains/cvalue/builtins_string.ml
index d6c9c6040bd..343dffefba4 100644
--- a/src/plugins/value/domains/cvalue/builtins_string.ml
+++ b/src/plugins/value/domains/cvalue/builtins_string.ml
@@ -170,7 +170,7 @@ let search_range kind ~min ~max (v, v_size, _v_shift) acc =
read_char kind offset v acc
else
(* The value [v] contains [nb_chars] characters: need [nb_chars] reads. *)
- let nb_chars = Integer.div v_size kind.size in
+ let nb_chars = Integer.e_div v_size kind.size in
(* Reads the [count]-nth character in [v]. *)
let rec do_one_char count ~max res =
let start = Integer.mul kind.size count in
@@ -222,9 +222,9 @@ let fold_offsm kind ~validity ~start ~max offsetmap acc =
overlaps between two ranges of the offsetmap.
- and either the value is isotropic, or the reads are aligned with the
repeated values. *)
- if Integer.is_zero (Integer.pos_rem (Integer.succ max) modu) &&
+ if Integer.is_zero (Integer.e_rem (Integer.succ max) modu) &&
(Cvalue.V_Or_Uninitialized.is_isotropic v ||
- Integer.(equal index v_start && is_zero (pos_rem v_size kind.size)))
+ Integer.(equal index v_start && is_zero (e_rem v_size kind.size)))
then search_range kind ~min:index ~max (v, v_size, v_shift) acc
else search_each_index kind ~validity ~index ~max offsetmap acc
in
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index e6845dd9d77..ce361f8068a 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -205,12 +205,12 @@ module G = struct
let div_towards_minus_infty x y =
if Integer.gt y Integer.zero
- then Integer.pos_div x y
- else Integer.(pos_div (neg x) (neg y))
+ then Integer.e_div x y
+ else Integer.(e_div (neg x) (neg y))
let div_towards_plus_infty x y =
if Integer.lt y Integer.zero
- then Integer.pos_div x y
- else Integer.(pos_div (neg x) (neg y))
+ then Integer.e_div x y
+ else Integer.(e_div (neg x) (neg y))
(* Computes the possible [n] such that [(add b)^n = r], when [f^n]
is [f] consecutive applications of [f]. *)
diff --git a/src/plugins/value/legacy/eval_op.ml b/src/plugins/value/legacy/eval_op.ml
index ce1da249d7f..7e919716a71 100644
--- a/src/plugins/value/legacy/eval_op.ml
+++ b/src/plugins/value/legacy/eval_op.ml
@@ -102,7 +102,7 @@ let reduce_by_initialized_defined f loc state =
if v' != v then begin
if V_Or_Uninitialized.is_bottom v' then raise Reduce_to_bottom;
let il = Int.max offl ll and ih = Int.min offh lh in
- let abs_shift = Integer.pos_rem (Rel.add_abs offl shift) modu in
+ let abs_shift = Integer.e_rem (Rel.add_abs offl shift) modu in
(* il and ih are the bounds of the interval to reduce.
We change the initialized flags in the following cases:
- either we overwrite entire values, or the partly overwritten
@@ -110,12 +110,12 @@ let reduce_by_initialized_defined f loc state =
- or we do not lose information on misaligned or partial values:
the result is a singleton *)
if V_Or_Uninitialized.(cardinal_zero_or_one v' || is_isotropic v') ||
- ((Int.equal offl il || Int.equal (Int.pos_rem ll modu) abs_shift) &&
+ ((Int.equal offl il || Int.equal (Int.e_rem ll modu) abs_shift) &&
(Int.equal offh ih ||
- Int.equal (Int.pos_rem (Int.succ lh) modu) abs_shift))
+ Int.equal (Int.e_rem (Int.succ lh) modu) abs_shift))
then
let diff = Rel.sub_abs il offl in
- let shift_il = Rel.pos_rem (Rel.sub shift diff) modu in
+ let shift_il = Rel.e_rem (Rel.sub shift diff) modu in
V_Offsetmap.add (il, ih) (v', modu, shift_il) acc
else acc
end
@@ -234,7 +234,7 @@ let find_offsm_under validity ival size offsm acc =
| Tr_offset.Interval (min, max, modu) ->
let process (start, _stop) (v, v_size, v_offset) acc =
if Rel.(equal v_offset zero) && Int.equal v_size size
- && Int.equal (Int.pos_rem (Int.sub start min) modu) Int.zero
+ && Int.equal (Int.e_rem (Int.sub start min) modu) Int.zero
then add_if_singleton v acc
else acc
in
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 1b237eb589e..bd7d695d456 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -939,11 +939,11 @@ let rec eval_term ~alarm_mode env t =
frontiers are always 0 or 8*k-1 (because validity is in bits and
starts on zero), so we add 1 everywhere, then divide by eight. *)
let convert start_bits end_bits =
- let congr_succ i = Int.(equal zero (rem (succ i) eight)) in
+ let congr_succ i = Int.(equal zero (e_rem (succ i) eight)) in
let congr_or_zero i = Int.(equal zero i || congr_succ i) in
assert (congr_or_zero start_bits || congr_or_zero end_bits);
- let start_bytes = Int.(pos_div (Int.succ start_bits) eight) in
- let end_bytes = Int.(pos_div (Int.succ end_bits) eight) in
+ let start_bytes = Int.(e_div (Int.succ start_bits) eight) in
+ let end_bytes = Int.(e_div (Int.succ end_bits) eight) in
Ival.inject_range (Some start_bytes) (Some end_bytes)
in
match Base.validity b with
diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index 0801bc27aea..f6306e870ba 100644
--- a/src/plugins/value_types/cvalue.ml
+++ b/src/plugins/value_types/cvalue.ml
@@ -979,7 +979,7 @@ module V_Offsetmap = struct
if Integer.is_zero cardinal then Integer.one else cardinal
in
let cardinalf = CardinalEstimate.of_integer cardinal in
- let repeat = Integer.(div (length start stop) size) in
+ let repeat = Integer.(e_div (length start stop) size) in
(* If a value is "cut", we still count it as if it were whole. *)
let repeat = Integer.(max repeat one) in
let cardinalf_repeated = CardinalEstimate.power cardinalf repeat in
diff --git a/src/plugins/value_types/widen_type.ml b/src/plugins/value_types/widen_type.ml
index 7f05346b3e9..ed9929b21d0 100644
--- a/src/plugins/value_types/widen_type.ml
+++ b/src/plugins/value_types/widen_type.ml
@@ -141,7 +141,7 @@ let hints_for_base default_hints hints_by_base b =
(* Try the frontier of the block: further accesses are invalid
anyway. This also works great for constant strings (this computes
the offset of the null terminator). *)
- let bound = Integer.(pred (div (succ m) eight)) in
+ let bound = Integer.(pred (e_div (succ m) eight)) in
Ival.Widen_Hints.add bound widen_zero
| Base.Empty | Base.Invalid -> widen_zero
)
diff --git a/src/plugins/wp/TacCongruence.ml b/src/plugins/wp/TacCongruence.ml
index b59a7a28120..b5d79cedfb2 100644
--- a/src/plugins/wp/TacCongruence.ml
+++ b/src/plugins/wp/TacCongruence.ml
@@ -133,8 +133,8 @@ let rec compare cmp a b =
not Integer.(equal p zero) &&
not Integer.(equal q zero) ->
let g = Integer.pgcd (Integer.abs p) (Integer.abs q) in
- let ka = Integer.div p g in
- let kb = Integer.div q g in
+ let ka = Integer.e_div p g in
+ let kb = Integer.e_div q g in
compare_div cmp (F.e_times ka a) (F.e_times kb b) (F.e_zint g)
| QDIV(a,u) , QDIV(b,v) -> compare_ratio cmp a u b v
@@ -164,8 +164,8 @@ let rec equal eq a b =
not Integer.(equal p zero) &&
not Integer.(equal q zero) ->
let g = Integer.pgcd (Integer.abs p) (Integer.abs q) in
- let ka = Integer.div p g in
- let kb = Integer.div q g in
+ let ka = Integer.e_div p g in
+ let kb = Integer.e_div q g in
compare_div EQ (F.e_times ka a) (F.e_times kb b) (F.e_zint g)
| QDIV(a,u) , QDIV(b,v) -> eq_ratio eq a u b v
--
GitLab