package codex

  1. Overview
  2. Docs
package codex
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file integer.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
(**************************************************************************)
(*  This file is part of the Codex semantics library.                     *)
(*                                                                        *)
(*  Copyright (C) 2013-2025                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file LICENSE).                      *)
(*                                                                        *)
(**************************************************************************)

type t = Z.t

let equal = Z.equal

let compare = Z.compare

let two_power_of_int k =
  Z.shift_left Z.one k

let two_power n =
  let k = Z.to_int n in
  if k > 1024 then
    raise Z.Overflow
  else
    two_power_of_int k

let power_int_positive_int = Big_int_Z.power_int_positive_int

let popcount = Z.popcount

let zero = Z.zero
let one = Z.one
let minus_one = Z.minus_one
let two = Z.of_int 2
let four = Z.of_int 4
let eight = Z.of_int 8
let sixteen = Z.of_int 16
let thirtytwo = Z.of_int 32
let onethousand = Z.of_int 1000
let billion_one = Z.of_int 1_000_000_001
let two_power_32 = two_power_of_int 32
let two_power_60 = two_power_of_int 60
let two_power_64 = two_power_of_int 64

let is_zero v = Z.equal v Z.zero

let add = Z.add
let sub = Z.sub
let succ = Z.succ
let pred = Z.pred
let neg = Z.neg

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

let shift_left x y = Z.shift_left x (Z.to_int y)
let shift_right x y = Z.shift_right x (Z.to_int y)
let shift_right_logical x y = (* no meaning for negative value of x *)
  if (Z.lt x Z.zero)
  then raise (Invalid_argument "Integer.shift_right_logical")
  else Z.shift_right x (Z.to_int y)

let logand = Z.logand
let lognot = Z.lognot
let logor = Z.logor
let logxor = Z.logxor

let le a b = Z.compare a b <= 0
let ge a b = Z.compare a b >= 0
let lt a b = Z.compare a b < 0
let gt a b = Z.compare a b > 0

let of_int = Z.of_int
let of_int64 = Z.of_int64
let of_int32 = Z.of_int32

let to_int = Z.to_int
let to_int64 = Z.to_int64
let to_int32 = Z.to_int32

let of_string = Z.of_string
let to_string = Z.to_string

let of_float = Z.of_float
let to_float = Z.to_float
let max_int64 = of_int64 Int64.max_int
let min_int64 = of_int64 Int64.min_int


let bdigits = [|
  "0000" ; (* 0 *)
  "0001" ; (* 1 *)
  "0010" ; (* 2 *)
  "0011" ; (* 3 *)
  "0100" ; (* 4 *)
  "0101" ; (* 5 *)
  "0110" ; (* 6 *)
  "0111" ; (* 7 *)
  "1000" ; (* 8 *)
  "1001" ; (* 9 *)
  "1010" ; (* 10 *)
  "1011" ; (* 11 *)
  "1100" ; (* 12 *)
  "1101" ; (* 13 *)
  "1110" ; (* 14 *)
  "1111" ; (* 15 *)
|]

let pp_bin_pos fmt r = Format.pp_print_string fmt bdigits.(r)
let pp_bin_neg fmt r = Format.pp_print_string fmt bdigits.(15-r)

let pp_hex_pos fmt r = Format.fprintf fmt "%04X" r
let pp_hex_neg fmt r = Format.fprintf fmt "%04X" (0xFFFF-r)

let bmask_bin = Z.of_int 0xF     (* 4 bits mask *)
let bmask_hex = Z.of_int 0xFFFF (* 64 bits mask *)

type digits = {
  nbits : int ; (* max number of bits *)
  bsize : int ; (* bits in each bloc *)
  bmask : Z.t ; (* block mask, must be (1 << bsize) - 1 *)
  sep : string ;
  pp : Format.formatter -> int -> unit ; (* print one block *)
}

let rec pp_digits d fmt n v =
  if gt v zero || n < d.nbits then
    begin
      let r = Z.to_int (Z.logand v d.bmask) in
      let k = d.bsize in
      pp_digits d fmt (n + k) (Z.shift_right_trunc v k) ;
      if gt v d.bmask || (n + k) < d.nbits
      then Format.pp_print_string fmt d.sep ;
      d.pp fmt r ;
    end

let pp_bin ?(nbits=1) ?(sep="") fmt v =
  let nbits = if nbits <= 0 then 1 else nbits in
  if le zero v then
    ( Format.pp_print_string fmt "0b" ;
      pp_digits { nbits ; sep ; bsize=4 ;
                  bmask = bmask_bin ; pp = pp_bin_pos } fmt 0 v )
  else
    ( Format.pp_print_string fmt "1b" ;
      pp_digits { nbits ; sep ; bsize=4 ;
                  bmask = bmask_bin ; pp = pp_bin_neg } fmt 0 (Z.lognot v) )

let pp_hex ?(nbits=1) ?(sep="") fmt v =
  let nbits = if nbits <= 0 then 1 else nbits in
  if le zero v then
    ( Format.pp_print_string fmt "0x" ;
      pp_digits { nbits ; sep ; bsize=16 ;
                  bmask = bmask_hex ; pp = pp_hex_pos } fmt 0 v )

  else
    ( Format.pp_print_string fmt "1x" ;
      pp_digits { nbits ; sep ; bsize=16 ;
                  bmask = bmask_hex ; pp = pp_hex_neg } fmt 0 (Z.lognot v) )
let pretty ?(hexa=false) fmt v =
  let rec aux v =
    if gt v two_power_60 then
      let quo, rem = Z.ediv_rem v two_power_60 in
      aux quo;
      Format.fprintf fmt "%015LX" (to_int64 rem)
    else
      Format.fprintf fmt "%LX" (to_int64 v)
  in
  if hexa then
    if equal v zero then Format.pp_print_string fmt "0"
    else if gt v zero then (Format.pp_print_string fmt "0x"; aux v)
    else (Format.pp_print_string fmt "-0x"; aux (Z.neg v))
  else
    Format.pp_print_string fmt (to_string v)

let is_one v = equal one v

let cast ~size ~signed ~value =
  if (not signed)
  then
    let factor = two_power size in logand value (pred factor)
  else
    let mask = two_power (sub size one) in
    let p_mask = pred mask in
    if equal (logand mask value) zero
    then logand value p_mask
    else
      logor (lognot p_mask) value

let length u v = succ (sub v u)

let extract_bits ~start ~stop v =
  assert (ge start zero && ge stop start);
  (*Format.printf "%a[%a..%a]@\n" pretty v pretty start pretty stop;*)
  let r = Z.extract v (to_int start) (to_int (length start stop)) in
  (*Format.printf "%a[%a..%a]=%a@\n" pretty v pretty start pretty stop pretty r;*)
  r

let is_even v = is_zero (logand one v)

let pgcd u v =
  if is_zero v then abs u (* Zarith raises an exception on zero arguments *)
  else if is_zero u then abs v
  else Z.gcd u v

let ppcm u v =
  if u = zero || v = zero
  then zero
  else Z.lcm u v

let min = Z.min
let max = Z.max

let round_down_to_zero v 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

let round_down_to_r ~max:m ~r ~modu =
  add (round_down_to_zero (sub m r) modu) r