number.ml 17.6 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5
6
7
8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
11
12

open Format
13
14
15

(** Construction *)

16
type integer_literal =
17
18
19
20
21
  | IConstDec of string
  | IConstHex of string
  | IConstOct of string
  | IConstBin of string

22
23
24
25
26
27
type integer_constant = {
    ic_negative : bool;
    ic_abs : integer_literal;
  }

type real_literal =
28
29
30
  | RConstDec of string * string * string option (* int / frac / exp *)
  | RConstHex of string * string * string option

31
32
33
34
35
type real_constant = {
    rc_negative : bool;
    rc_abs : real_literal;
  }

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
type constant =
  | ConstInt  of integer_constant
  | ConstReal of real_constant

exception InvalidConstantLiteral of int * string
let invalid_constant_literal n s = raise (InvalidConstantLiteral(n,s))

let check_integer_literal n f s =
  let l = String.length s in
  if l = 0 then invalid_constant_literal n s;
  for i = 0 to l-1 do
    if not (f s.[i]) then invalid_constant_literal n s;
  done

let is_hex = function '0'..'9' | 'A'..'F' | 'a'..'f' -> true | _ -> false
let is_dec = function '0'..'9' -> true | _ -> false
let is_oct = function '0'..'7' -> true | _ -> false
let is_bin = function '0'..'1' -> true | _ -> false

let int_const_dec s =
  check_integer_literal 10 is_dec s;
  IConstDec s

let int_const_hex s =
  check_integer_literal 16 is_hex s;
  IConstHex s

let int_const_oct s =
  check_integer_literal 8 is_oct s;
  IConstOct s

let int_const_bin s =
  check_integer_literal 2 is_bin s;
  IConstBin s

71
72
73
74
75
76
77
78
79
80
let const_of_big_int n =
  let neg,a =
    if BigInt.ge n BigInt.zero then
      false,n
    else
      true,BigInt.minus n
  in
  let a = int_const_dec (BigInt.to_string a) in
  ConstInt {ic_negative = neg ;ic_abs = a}

81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
let check_exp e =
  let e = if e.[0] = '-' then String.sub e 1 (String.length e - 1) else e in
  check_integer_literal 10 is_dec e

let real_const_dec i f e =
  if i <> "" then check_integer_literal 10 is_dec i;
  if f <> "" then check_integer_literal 10 is_dec f;
  Opt.iter check_exp e;
  RConstDec (i,f,e)

let real_const_hex i f e =
  if i <> "" then check_integer_literal 16 is_hex i;
  if f <> "" then check_integer_literal 16 is_hex f;
  Opt.iter check_exp e;
  RConstHex (i,f,e)

97
let compute_any radix s =
98
99
100
101
102
103
104
105
106
107
108
  let n = String.length s in
  let rec compute acc i =
    if i = n then
      acc
    else begin
      let v = match s.[i] with
        | '0'..'9' as c -> Char.code c - Char.code '0'
        | 'A'..'Z' as c -> 10 + Char.code c - Char.code 'A'
        | 'a'..'z' as c -> 10 + Char.code c - Char.code 'a'
        | _ -> assert false in
      assert (v < radix);
109
      compute (BigInt.add_int v (BigInt.mul_int radix acc)) (i + 1)
110
    end in
111
  (compute BigInt.zero 0)
112

Clément Fumex's avatar
Clément Fumex committed
113
114
(** Printing *)

115
let compute_int_literal c =
116
117
118
119
120
121
  match c with
  | IConstDec s -> compute_any 10 s
  | IConstHex s -> compute_any 16 s
  | IConstOct s -> compute_any 8 s
  | IConstBin s -> compute_any 2 s

122
123
124
125
126
127
128
129
130
131
132
133
let compute_int_constant c =
  let a = compute_int_literal c.ic_abs in
  if c.ic_negative then BigInt.minus a else a

let to_small_integer i =
  match i with
  | IConstDec s -> int_of_string s
  | IConstHex s -> int_of_string ("0x"^s)
  | IConstOct s -> int_of_string ("0o"^s)
  | IConstBin s -> int_of_string ("0b"^s)


134
let any_to_dec radix s =
135
  BigInt.to_string (compute_any radix s)
136
137

let power2 n =
138
  BigInt.to_string (BigInt.pow_int_pos 2 n)
139

140
141
142
143
144
145
146
147
148
type integer_format =
  (string -> unit, Format.formatter, unit) format

type real_format =
  (string -> string -> string -> unit, Format.formatter, unit) format

type part_real_format =
  (string -> string -> unit, Format.formatter, unit) format

149
150
type dec_real_format =
  | PrintDecReal of part_real_format * real_format
151

152
153
154
155
156
157
158
159
160
161
type frac_real_format =
  | PrintFracReal of integer_format * part_real_format * part_real_format

type 'a number_support_kind =
  | Number_unsupported
  | Number_default
  | Number_custom of 'a

type integer_support_kind = integer_format number_support_kind

162
163
164
type 'a negative_format =
  ((Format.formatter->'a->unit)->'a->unit,Format.formatter,unit) format

165
type number_support = {
166
  long_int_support  : bool;
167
  extra_leading_zeros_support : bool;
168
  negative_int_support  : (integer_literal negative_format) number_support_kind;
169
170
171
172
173
  dec_int_support   : integer_support_kind;
  hex_int_support   : integer_support_kind;
  oct_int_support   : integer_support_kind;
  bin_int_support   : integer_support_kind;
  def_int_support   : integer_support_kind;
174
  negative_real_support  : (real_literal negative_format) number_support_kind;
175
176
  dec_real_support  : dec_real_format number_support_kind;
  hex_real_support  : real_format number_support_kind;
177
  frac_real_support : frac_real_format number_support_kind;
178
  def_real_support  : integer_support_kind;
179
180
181
182
183
}

let check_support support default do_it try_next v =
  match support with
  | Number_unsupported -> try_next v
184
  | Number_default -> do_it (Opt.get default) v
185
186
187
188
189
190
191
192
  | Number_custom f -> do_it f v

let force_support support do_it v =
  match support with
  | Number_unsupported -> assert false
  | Number_default -> assert false
  | Number_custom f -> do_it f v

193
let simplify_max_int = BigInt.of_string "2147483646"
194
195
196

let remove_minus e =
  if e.[0] = '-' then
197
    (let e' = Strings.copy e in Strings.set e' 0 'm'; e')
198
199
200
201
202
203
  else e

let print_dec_int support fmt i =
  let fallback i =
    force_support support.def_int_support (fprintf fmt) i in
  if not support.long_int_support &&
204
     (BigInt.compare (BigInt.of_string i) simplify_max_int > 0) then
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
    fallback i
  else
    check_support support.dec_int_support (Some "%s") (fprintf fmt)
    fallback i

let print_hex_int support fmt =
  check_support support.hex_int_support (Some "0x%s")
    (fun s i -> assert support.long_int_support; fprintf fmt s i)
  (fun i -> print_dec_int support fmt (any_to_dec 16 i))

let print_oct_int support fmt =
  check_support support.oct_int_support (Some "0o%s")
    (fun s i -> assert support.long_int_support; fprintf fmt s i)
  (fun i -> print_dec_int support fmt (any_to_dec 8 i))

let print_bin_int support fmt =
  check_support support.bin_int_support (Some "0b%s")
    (fun s i -> assert support.long_int_support; fprintf fmt s i)
  (fun i -> print_dec_int support fmt (any_to_dec 2 i))

225
226
227
228
229
230
231
232
233
let remove_leading_zeros support s =
  if support.extra_leading_zeros_support then s else
  let len = String.length s in
  let rec aux i =
    if i+1 < len && s.[i] = '0' then aux (i+1) else i
  in
  let i = aux 0 in
  String.sub s i (len - i)

234
235
236
237
238
let print_dec_real support fmt =
  check_support support.dec_real_support
    (Some (PrintDecReal ("%s.%s", "%s.%se%s")))
    (fun (PrintDecReal (noexp,full)) i f e ->
      match e with
239
240
241
      | None -> fprintf fmt noexp
          (remove_leading_zeros support i)
          (if f = "" then "0" else f)
242
      | Some e -> fprintf fmt full
243
244
245
          (remove_leading_zeros support i)
          (if f = "" then "0" else f)
          (remove_leading_zeros support e))
246
    (check_support support.frac_real_support None
247
248
    (fun (PrintFracReal (exp_zero, exp_pos, exp_neg)) i f e ->
      let f = if f = "0" then "" else f in
249
250
      let e = Opt.fold (fun _ -> int_of_string) 0 e in
      let e = e - String.length f in
251
      if e = 0 then
252
        fprintf fmt exp_zero (remove_leading_zeros support (i ^ f))
253
      else if e > 0 then
254
        fprintf fmt exp_pos (remove_leading_zeros support (i ^ f))
255
          ("1" ^ String.make e '0')
256
      else
257
        fprintf fmt exp_neg (remove_leading_zeros support (i ^ f))
258
          ("1" ^ String.make (-e) '0'))
259
260
261
262
263
264
265
266
  (force_support support.def_real_support
    (fun def i f e -> fprintf fmt def (sprintf "%s_%s_e%s" i f
      (match e with None -> "0" | Some e -> remove_minus e)))
  ))

let print_hex_real support fmt =
  check_support support.hex_real_support
    (Some "0x%s.%sp%s")
267
268
269
    (fun s i f e -> fprintf fmt s i
      (if f = "" then "0" else f)
      (Opt.get_def "0" e))
270
271
272
273
274
  (* TODO: add support for decay to decimal floats *)
  (check_support support.frac_real_support None
    (fun (PrintFracReal (exp_zero, exp_pos, exp_neg)) i f e ->
      let f = if f = "0" then "" else f in
      let dec = any_to_dec 16 (i ^ f) in
275
276
      let e = Opt.fold (fun _ -> int_of_string) 0 e in
      let e = e - 4 * String.length f in
277
278
279
280
281
282
283
      if e = 0 then
        fprintf fmt exp_zero dec
      else if e > 0 then
        fprintf fmt exp_pos dec (power2 e)
      else
        fprintf fmt exp_neg dec (power2 (-e)))
  (force_support support.def_real_support
284
285
    (fun def i f e -> fprintf fmt def (sprintf "0x%s_%s_p%s" i f
      (match e with None -> "0" | Some e -> remove_minus e)))
286
287
  ))

288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
let print_int_literal support fmt = function
  | IConstDec i -> print_dec_int support fmt i
  | IConstHex i -> print_hex_int support fmt i
  | IConstOct i -> print_oct_int support fmt i
  | IConstBin i -> print_bin_int support fmt i

let print_real_literal support fmt = function
  | RConstDec (i, f, e) -> print_dec_real support fmt i f e
  | RConstHex (i, f, e) -> print_hex_real support fmt i f e

let print_int_constant support fmt i =
  if i.ic_negative then
    check_support support.negative_int_support (Some "(- %a)")
                  (fun def n -> fprintf fmt def (print_int_literal support) n)
                  (fun _ -> assert false)
                  i.ic_abs
  else
    fprintf fmt "%a" (print_int_literal support) i.ic_abs

let print_real_constant support fmt r =
  if r.rc_negative then
309
    check_support support.negative_real_support (Some "(- %a)")
310
311
312
313
314
315
316
                  (fun def n -> fprintf fmt def (print_real_literal support) n)
                  (fun _ -> assert false)
                  r.rc_abs
  else
    fprintf fmt "%a" (print_real_literal support) r.rc_abs


317
let print support fmt = function
318
319
320
321
322
323
324
325
  | ConstInt i -> print_int_constant support fmt i
  | ConstReal r -> print_real_constant support fmt r






326

Clément Fumex's avatar
Clément Fumex committed
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
let char_of_int i =
  if i < 10 then
    Char.chr (i + Char.code '0')
  else
    Char.chr (i + Char.code 'A' - 10)

open BigInt

let print_zeros fmt n =
  for _i = 0 to n - 1 do
    pp_print_char fmt '0'
  done

let rec print_in_base_aux radix digits fmt i =
  if lt i radix then begin
    begin match digits with
      | Some n -> print_zeros fmt (n - 1)
      | None -> ()
    end;
    fprintf fmt "%c" (char_of_int (to_int i))
347
  end
Clément Fumex's avatar
Clément Fumex committed
348
349
350
351
352
353
354
355
356
357
358
359
  else
    let d,m = computer_div_mod i radix in
    let digits = Opt.map ((+) (-1)) digits in
    print_in_base_aux radix digits fmt d;
    fprintf fmt "%c" (char_of_int (to_int m))

let print_in_base radix digits fmt i =
  print_in_base_aux (of_int radix) digits fmt i

(** Range checks *)

type int_range = {
360
361
362
363
364
365
366
367
368
369
370
  ir_lower : integer_constant;
  ir_upper : integer_constant;
  ir_lower_val : BigInt.t;
  ir_upper_val : BigInt.t;
}

let create_range lo hi =
  { ir_lower = lo;
    ir_upper = hi;
    ir_lower_val = compute_int_constant lo;
    ir_upper_val = compute_int_constant hi;
Clément Fumex's avatar
Clément Fumex committed
371
372
373
}

exception OutOfRange of integer_constant
374

375
376
377
let check_range c {ir_lower_val = lo; ir_upper_val = hi} =
  let cval = compute_int_literal c.ic_abs in
  let cval = if c.ic_negative then BigInt.minus cval else cval in
Clément Fumex's avatar
Clément Fumex committed
378
379
380
381
382
383
384
385
386
  if BigInt.lt cval lo || BigInt.gt cval hi then raise (OutOfRange c)

(** Float checks *)

type float_format = {
  fp_exponent_digits    : int;
  fp_significand_digits : int; (* counting the hidden bit *)
}

387
exception NonRepresentableFloat of real_literal
Clément Fumex's avatar
Clément Fumex committed
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492

let debug_float = Debug.register_info_flag "float"
  ~desc:"Avoid@ catching@ exceptions@ in@ order@ to@ get@ \
         float@ literal@ checks@ messages."

let float_parser c =
  let exp_parser e = match e.[0] with
    | '-' -> minus (compute_any 10 (String.sub e 1 (String.length e - 1)))
    | _   -> compute_any 10 e
  in

  (* get the value s and e such that c = s * 2 ^ e *)
  let s, e =
    match c with
    (* c = a.b * 10 ^ e *)
    | RConstDec (a,b,e) ->
      let b_length = String.length b in
      let s = ref (compute_any 10 (a ^ b)) in
      let e = sub (match e with
          | None -> Debug.dprintf debug_float "c = %s.%s" a b;
            zero
          | Some e -> Debug.dprintf debug_float "c = %s.%se%s" a b e;
            exp_parser e)
          (of_int b_length)
      in
      (* transform c = s * 10 ^ i into c = s' * 2 ^ i' *)
      let s =
        if lt e zero then begin
          let efive = pow_int_pos_bigint 5 (minus e) in
          let dv, rem = euclidean_div_mod !s efive in
          if not (eq rem zero) then begin
            raise (NonRepresentableFloat c);
          end else
            dv
        end else
          mul !s (pow_int_pos_bigint 5 e)
      in
      Debug.dprintf debug_float " = %s * 2 ^ %s" (to_string s) (to_string e);
      ref s, ref e

    (* c = a.b * 2 ^ e *)
    | RConstHex (a,b,e) ->
      let b_length = String.length b in
      ref (compute_any 16 (a ^ b)),
      ref (sub (match e with
          | None -> Debug.dprintf debug_float "c = %s.%s" a b;
            zero
          | Some e -> Debug.dprintf debug_float "c = %s.%sp%s" a b e;
            exp_parser e)
          (of_int (b_length * 4)))
  in
  s, e

let compute_float c fp =
  let eb = BigInt.of_int fp.fp_exponent_digits in
  let sb = BigInt.of_int fp.fp_significand_digits in
  (* 2 ^ (sb - 1)    min representable normalized significand*)
  let smin = pow_int_pos_bigint 2 (sub sb one) in
  (* (2 ^ sb) - 1    max representable normalized significand*)
  let smax = sub (pow_int_pos_bigint 2 sb) one in
  (* 2 ^ (eb - 1)    exponent of the infinities *)
  let emax = pow_int_pos_bigint 2 (sub eb one) in
  (* 1 - emax        exponent of the denormalized *)
  let eden = sub one emax in
  (* 3 - emax - sb   smallest denormalized' exponent *)
  let emin = sub (add (of_int 2) eden) sb in

  (* get [s] and [e] such that "c = s * 2 ^ e" *)
  let s, e = float_parser c in

  (* if s = 0 stop now *)
  if eq !s zero then
    zero, zero

  else begin

    (* if s is too big or e is too small, try to remove trailing zeros
       in s and incr e *)
    while gt !s smax || lt !e emin do
      let new_s, rem = euclidean_div_mod !s (of_int 2) in
      if not (eq rem zero) then begin
        Debug.dprintf debug_float "Too many digits in significand.";
        raise (NonRepresentableFloat c);
      end else begin
        s := new_s;
        e := succ !e
      end
    done;

    (* if s is too small and e is too big, add trailing zeros in s and
       decr e *)
    while lt !s smin && gt !e emin do
      s := mul_int 2 !s;
      e := pred !e
    done;

    Debug.dprintf debug_float " = %s * 2 ^ %s@." (to_string !s) (to_string !e);

    if lt !s smin then begin
      (* denormal case *)

      Debug.dprintf debug_float "final: c = 0.[%s] * 2 ^ ([0] - bias + 1); bias=%s, i.e, 0[%a][%a]@."
        (to_string !s) (to_string (sub emax one)) (print_in_base 2 (Some (to_int eb))) zero
      (print_in_base 2 (Some (to_int (sub sb one)))) !s;

493
      zero, !s
Clément Fumex's avatar
Clément Fumex committed
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524

    end else begin
      (* normal case *)

      (* normalize the exponent *)
      let fe = add !e (sub sb one) in

      (* now that s and e are in shape, check that e is not too big *)
      if ge fe emax then begin
        Debug.dprintf debug_float "Exponent too big.";
        raise (NonRepresentableFloat c)
      end;

      (* add the exponent bia to e *)
      let fe = add fe (sub emax one) in
      let fs = sub !s smin in

      Debug.dprintf debug_float "final: c = 1.[%s] * 2 ^ ([%s] - bias); bias=%s, i.e, 0[%a][%a]@."
        (to_string fs) (to_string fe) (to_string (sub emax one))
        (print_in_base 2 (Some (to_int eb))) fe
        (print_in_base 2 (Some (to_int (sub sb one)))) fs;

      assert (le zero fs && lt fs (pow_int_pos_bigint 2 (sub sb one))
              && le zero fe && lt fe (sub (pow_int_pos_bigint 2 eb) one));

      fe, fs
    end
  end

let check_float c fp = ignore (compute_float c fp)

525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545

let full_support =
  {
    long_int_support = true;
    extra_leading_zeros_support = true;
    negative_int_support = Number_default;
    dec_int_support = Number_default;
    hex_int_support = Number_default;
    oct_int_support = Number_default;
    bin_int_support = Number_default;
    def_int_support = Number_default;
    negative_real_support = Number_default;
    dec_real_support = Number_default;
    hex_real_support = Number_default;
    frac_real_support = Number_default;
    def_real_support = Number_default;
  }

(*

let print_integer_literal fmt = function
Clément Fumex's avatar
Clément Fumex committed
546
547
548
549
550
  | IConstDec s -> fprintf fmt "%s" s
  | IConstHex s -> fprintf fmt "0x%s" s
  | IConstOct s -> fprintf fmt "0o%s" s
  | IConstBin s -> fprintf fmt "0b%s" s

551
let print_real_literal fmt = function
Clément Fumex's avatar
Clément Fumex committed
552
553
554
555
556
  | RConstDec (i,f,None)   -> fprintf fmt "%s.%s" i f
  | RConstDec (i,f,Some e) -> fprintf fmt "%s.%se%s" i f e
  | RConstHex (i,f,Some e) -> fprintf fmt "0x%s.%sp%s" i f e
  | RConstHex (i,f,None)   -> fprintf fmt "0x%s.%s" i f

557
558
559
560
561
562
563
564
let print_unsigned_constant fmt = function
  | ConstInt c  -> print_integer_literal fmt c
  | ConstReal c -> print_real_literal fmt c

let print_constant fmt c =
  if c.is_positive then print_unsigned_constant fmt c.abs_value
  else fprintf fmt "-%a" print_unsigned_constant c.abs_value
 *)
Clément Fumex's avatar
Clément Fumex committed
565
566
567
568
569
570

let () = Exn_printer.register (fun fmt exn -> match exn with
  | InvalidConstantLiteral (n,s) ->
      fprintf fmt "Invalid integer literal in base %d: '%s'" n s
  | NonRepresentableFloat c ->
      fprintf fmt "Invalid floating point literal: '%a'"
571
        (print_real_literal full_support) c
Clément Fumex's avatar
Clément Fumex committed
572
  | OutOfRange c ->
573
574
      fprintf fmt "Integer literal %a is out of range"
              (print_int_constant full_support) c
Clément Fumex's avatar
Clément Fumex committed
575
  | _ -> raise exn)
576
577

let print_constant = print full_support