package codex

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

Source file function_symbol.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
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
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
493
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
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
(**************************************************************************)
(*  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).                      *)
(*                                                                        *)
(**************************************************************************)

module Log = Tracelog.Make(struct let category = "Function_symbol" end);;
module In_bits = Units.In_bits

(* We make the type concrete, so the type checker knows that they
   cannot be equal. *)
type boolean = private TypeBoolean
type integer = private TypeInteger
type enum = private TypeEnum
type bitvector  = private TypeBitvector
type binary = bitvector  
type memory  = private TypeMemory

type size = In_bits.t

type case = int

type 'a typ =
  | Boolean: boolean typ
  | Integer: integer typ
  | Enum: enum typ
  | Binary: size -> binary typ
  | Memory: memory typ

type z_t = Z.t

(* We define these dummy types, used to represent knowledge about
   arity in gadt. We need a definition and use constructors for this,
   but they are never used.  *)
type ar0 = private Ar0
type 'a ar1 = private Ar1
type ('a,'b) ar2 = private Ar2

type any_type =
  Any_type: 'a typ -> any_type [@@unboxed];;

type ('arg,'ret) function_symbol =
  | True: (ar0,boolean) function_symbol
  | False: (ar0,boolean) function_symbol
  | And: ((boolean,boolean) ar2,boolean) function_symbol
  | Or: ((boolean,boolean) ar2,boolean) function_symbol
  | Not: (boolean ar1,boolean) function_symbol
  | BoolUnion: ((boolean,boolean) ar2,boolean) function_symbol

  | Biconst: size * z_t -> (ar0,binary) function_symbol
  | Biadd: {size:size;flags:Flags.Biadd.t} -> ((binary,binary) ar2,binary) function_symbol
  | Bisub: {size:size;flags:Flags.Bisub.t} -> ((binary,binary) ar2,binary) function_symbol
  | Bimul: {size:size;flags:Flags.Bimul.t} -> ((binary,binary) ar2,binary) function_symbol
  | Biudiv:size -> ((binary,binary) ar2,binary) function_symbol
  | Bisdiv:size -> ((binary,binary) ar2,binary) function_symbol
  | Biumod:size -> ((binary,binary) ar2,binary) function_symbol
  | Bismod:size -> ((binary,binary) ar2,binary) function_symbol
  | Bshl:  {size:size;flags:Flags.Bshl.t} -> ((binary,binary) ar2,binary) function_symbol
  | Bashr: size -> ((binary,binary) ar2,binary) function_symbol
  | Blshr: size -> ((binary,binary) ar2,binary) function_symbol
  | Band:  size -> ((binary,binary) ar2,binary) function_symbol
  | Bor:   size -> ((binary,binary) ar2,binary) function_symbol
  | Bxor:  size -> ((binary,binary) ar2,binary) function_symbol

  | Beq:   size -> ((binary,binary) ar2,boolean) function_symbol
  | Bisle: size -> ((binary,binary) ar2,boolean) function_symbol
  | Biule: size -> ((binary,binary) ar2,boolean) function_symbol

  | Bconcat: size * size -> ((binary,binary) ar2,binary) function_symbol
  | Bextract: {size:size;index:In_bits.t;oldsize:size} -> (binary ar1,binary) function_symbol
  | Bsext: size -> (binary ar1,binary) function_symbol
  | Buext: size -> (binary ar1,binary) function_symbol
  | Bofbool: size -> (boolean ar1,binary) function_symbol
  | Bunion: Operator_ids.Condition.t * size -> ((binary,binary) ar2,binary) function_symbol
  | Bchoose: Operator_ids.Choice.t * size -> (binary ar1,binary) function_symbol

  | Iconst: z_t -> (ar0,integer) function_symbol
  | Iadd: ((integer,integer) ar2, integer) function_symbol
  | Isub: ((integer,integer) ar2, integer) function_symbol
  | Imul: ((integer,integer) ar2, integer) function_symbol
  | Idiv: ((integer,integer) ar2, integer) function_symbol
  | Imod: ((integer,integer) ar2, integer) function_symbol
  | Ishl: ((integer,integer) ar2, integer) function_symbol
  | Ishr: ((integer,integer) ar2, integer) function_symbol
  | Ior:  ((integer,integer) ar2, integer) function_symbol
  | Ixor: ((integer,integer) ar2, integer) function_symbol
  | Iand: ((integer,integer) ar2, integer) function_symbol

  | Ieq:  ((integer,integer) ar2, boolean) function_symbol
  | Ile:  ((integer,integer) ar2, boolean) function_symbol

  | Itimes: z_t -> (integer ar1,integer) function_symbol

  | EnumConst: case ->  (ar0, enum) function_symbol
  | CaseOf : case -> (enum ar1, boolean) function_symbol
;;


let type_of: type a b. (a,b) function_symbol -> b typ = function
  | True-> Boolean
  | False-> Boolean
  | And-> Boolean
  | Or-> Boolean
  | Not-> Boolean
  | Biconst(size,_) -> Binary size
  | Biadd{size} -> Binary size
  | Bisub{size} -> Binary size
  | Bimul{size} -> Binary size
  | Biudiv(size) -> Binary size
  | Bisdiv(size) -> Binary size
  | Biumod(size) -> Binary size
  | Bismod(size) -> Binary size
  | Bshl{size} -> Binary size
  | Bashr(size) -> Binary size
  | Blshr(size) -> Binary size
  | Band(size) -> Binary size
  | Bor(size) -> Binary size
  | Bxor(size) -> Binary size

  | Beq(size) -> Boolean
  | Bisle(size) -> Boolean
  | Biule(size) -> Boolean

  | Bconcat(s1,s2) -> Binary (Units.In_bits.(s1+s2))
  | Bextract{size;index;oldsize} -> Binary size
  | Bsext(size) -> Binary size
  | Buext(size) -> Binary size
  | Bofbool(size) -> Binary size
  | Bunion(_,size) -> Binary size
  | Bchoose(_,size) -> Binary size

  | Iconst _ -> Integer
  | Iadd->  Integer
  | Isub->  Integer
  | Imul->  Integer
  | Idiv->  Integer
  | Imod->  Integer
  | Ishl->  Integer
  | Ishr->  Integer
  | Ior->  Integer
  | Ixor->  Integer
  | Iand->  Integer
  | Ieq ->  Boolean
  | Ile ->  Boolean
  | Itimes _ -> Integer
  | BoolUnion -> Boolean
  | EnumConst _ -> Enum
  | CaseOf _ -> Boolean
;;

(* Used to identify a problem when we do not have a pretty printer. *)
let _identify: type a b. (a,b) function_symbol -> int = function
  | True -> assert false
  | False -> assert false
  | And -> assert false
  | Or -> assert false
  | Not -> assert false
  | Biconst (_, _) -> assert false
  | Biadd _ -> assert false
  | Bisub _ -> assert false
  | Bimul _ -> assert false
  | Biudiv _ -> assert false
  | Bisdiv _ -> assert false
  | Biumod _ -> assert false
  | Bismod _ -> assert false
  | Bshl _ -> assert false
  | Bashr _ -> assert false
  | Blshr _ -> assert false
  | Band _ -> assert false
  | Bor _ -> assert false
  | Bxor _ -> assert false
  | Beq _ -> assert false
  | Bisle _ -> assert false
  | Biule _ -> assert false
  | Bconcat (_, _) -> assert false
  | Bextract _ -> assert false
  | Bsext _ -> assert false
  | Buext _ -> assert false
  | Bofbool _ -> assert false
  | Bunion (_, _) -> assert false
  | Bchoose (_, _) -> assert false
  | Iconst _ -> assert false
  | Iadd -> assert false
  | Isub -> assert false
  | Imul -> assert false
  | Idiv -> assert false
  | Imod -> assert false
  | Ishl -> assert false
  | Ishr -> assert false
  | Ior -> assert false
  | Ixor -> assert false
  | Iand -> assert false
  | Ieq -> assert false
  | Ile -> assert false
  | Itimes _ -> assert false
  | BoolUnion -> assert false
  | EnumConst _ -> assert false
  | CaseOf _ -> assert false


(* We use the last 6 bits (0..63) as the type.  *)
(* We use bit 7 and 8 for flags. *)
(* We use 8 bits, from 9 to 15,  for the size1 (0..255) *)
(* We use 8 bits, from 16 to 24, for the size2 (0..255) *)
(* If there are other large elements: we sdbm with this. *)
(* MAYBE: Could be ppx generated. *)
let hash: type a b. (a,b) function_symbol -> int = function
  | True-> 1
  | False-> 2
  | And -> 3
  | Or-> 4
  | Not-> 5
  | Iadd-> 6
  | Isub-> 7
  | Imul-> 8
  | Idiv-> 9
  | Imod-> 10
  | Ishl-> 11
  | Ishr-> 12
  | Ior->  13
  | Ixor-> 14
  | Iand-> 15
  | Ieq -> 16
  | Ile -> 17
  | Biadd{size;flags} -> 18 lor ((flags :> int) * 64) lor ((size:>int) lsl 8)
  | Bisub{size;flags} -> 19 lor ((flags :> int) * 64) lor ((size:>int) lsl 8)
  | Bimul{size;flags} -> 20 lor ((flags :> int) * 64) lor ((size:>int) lsl 8)
  | Bshl{size;flags} -> 21 lor ((flags :> int) * 64)  lor ((size:>int) lsl 8)
  | Biudiv(size) -> 22 lor ((size:>int) lsl 8)
  | Bisdiv(size) -> 23 lor ((size:>int) lsl 8)
  | Biumod(size) -> 24 lor ((size:>int) lsl 8)
  | Bismod(size) -> 25 lor ((size:>int) lsl 8)
  | Bashr(size) -> 26 lor ((size:>int) lsl 8)
  | Blshr(size) -> 27 lor ((size:>int) lsl 8)
  | Band(size) -> 28 lor ((size:>int) lsl 8)
  | Bor(size) -> 29 lor ((size:>int) lsl 8)
  | Bxor(size) -> 30 lor ((size:>int) lsl 8)
  | Beq(size) -> 31 lor ((size:>int) lsl 8)
  | Bisle(size) -> 32 lor ((size:>int) lsl 8)
  | Biule(size) -> 33 lor ((size:>int) lsl 8)
  | Bconcat(s1,s2) -> 34 lor ((s1:>int) lsl 8) lor ((s2:>int) lsl 16)
  | Bextract{size;index;oldsize} -> 35 lor ((size:>int) lsl 8) lor ((oldsize:>int) lsl 16) lor ((index:>int) lsl 24)
  | Bsext(size) -> 36 lor ((size:>int) lsl 8)
  | Buext(size) -> 37 lor ((size:>int) lsl 8)
  | Bofbool(size) -> 38 lor ((size:>int) lsl 8)
  | Bchoose(id,size) -> Hashing.hash2 (39 lor ((size:>int) lsl 8)) (id:>int)
  | Bunion(id,size) -> Hashing.hash2 (40 lor ((size:>int) lsl 8)) (id:>int)
  | Itimes k -> Hashing.hash2 41 (Z.hash k)
  | Iconst k -> Hashing.hash2 42 (Z.hash k)
  | Biconst(size,k) -> Hashing.hash2 (43 lor ((size:>int) lsl 8)) (Z.hash k)
  | BoolUnion ->  44
  | CaseOf case -> 45 lor (case lsl 16)
  | EnumConst case -> 46 lor (case lsl 16)


(* TODO: Could be ppx generated. *)
let equal: type a b c d. (a,b) function_symbol -> (c,d) function_symbol -> bool = fun a b ->
  (Obj.magic a) == (Obj.magic b) || (* Shortcut with small performance benefit. *)
  match (a,b) with
  | True, True -> true
  | False,False -> true
  | And ,And  -> true
  | Or,Or -> true
  | Not,Not -> true
  | BoolUnion,BoolUnion -> true
  | Iadd,Iadd -> true
  | Isub,Isub -> true
  | Imul,Imul -> true
  | Idiv,Idiv -> true
  | Imod,Imod -> true
  | Ishl,Ishl -> true
  | Ishr,Ishr -> true
  | Ior,Ior -> true
  | Ixor,Ixor -> true
  | Iand,Iand -> true
  | Ieq ,Ieq  -> true
  | Ile ,Ile  -> true
  | Biadd{size=s1;flags=flags1} ,Biadd{size=s2;flags=flags2}->
    s1 = s2 && flags1 = flags2
  | Bisub{size=s1;flags=flags1} ,Bisub{size=s2;flags=flags2}->
    s1 = s2 && flags1 = flags2
  | Bimul{size=s1;flags=flags1} ,Bimul{size=s2;flags=flags2}->
    s1 = s2 && Int.equal (flags1:>int) (flags2:>int)
  | Bshl{size=s1;flags=flags1} ,Bshl{size=s2;flags=flags2}->
    s1 = s2 && flags1 = flags2
  | Biudiv(s1) ,Biudiv(s2)  -> s1 == s2
  | Bisdiv(s1) ,Bisdiv(s2)  -> s1 == s2
  | Biumod(s1) ,Biumod(s2)  -> s1 == s2
  | Bismod(s1) ,Bismod(s2)  -> s1 == s2
  | Bashr(s1) ,Bashr(s2)  -> s1 == s2
  | Blshr(s1) ,Blshr(s2)  -> s1 == s2
  | Band(s1) ,Band(s2)  -> s1 == s2
  | Bor(s1) ,Bor(s2)  -> s1 == s2
  | Bxor(s1) ,Bxor(s2)  -> s1 == s2
  | Beq(s1) ,Beq(s2)  -> s1 == s2
  | Bisle(s1) ,Bisle(s2)  -> s1 == s2
  | Biule(s1) ,Biule(s2)  -> s1 == s2
  | Bconcat(s1,s2) ,Bconcat(s3,s4)  -> s1 == s3 && s2 == s4
  | Bextract{size=s1;index=i1;oldsize=olds1},
    Bextract{size=s2;index=i2;oldsize=olds2} -> i1 == i2 && s1 == s2 && olds1 == olds2
  | Bsext(s1) ,Bsext(s2)  -> s1 == s2
  | Buext(s1) ,Buext(s2)  -> s1 == s2
  | Bofbool(s1) ,Bofbool(s2)  -> s1 == s2
  | Bchoose(id1,s1) ,Bchoose(id2,s2)  -> id1 == id2 && (assert (s1 == s2); true)
  | Bunion(id1,s1) ,Bunion(id2,s2)  -> id1 == id2 && (assert (s1 == s2); true)
  | Itimes k1 ,Itimes k2  -> Z.equal k1 k2
  | Iconst k1 ,Iconst k2  -> Z.equal k1 k2
  | Biconst(s1,k1),Biconst(s2,k2)  -> s1 == s2 && Z.equal k1 k2
  | CaseOf c1, CaseOf c2 -> c1 == c2
  | EnumConst c1, EnumConst c2 -> c1 == c2
  | _, _ ->
    if (hash a) == (hash b)
    then begin
      Log.warning (fun p -> p "Bad hash collision or mistake");
      (* let _ = identify b in () *)
    end;
    false
;;

(**************** Builders ****************)

module Build = struct

  module Arity = struct
    type nonrec 'r ar0 = (ar0,'r) function_symbol
    type nonrec ('a,'r) ar1 = ('a ar1,'r) function_symbol
    type nonrec  ('a,'b,'r) ar2 = (('a,'b) ar2,'r) function_symbol
    type nonrec ('a,'b,'c,'r) ar3 = unit
  end

  module Binary = struct

    let biconst ~size k = Biconst(size,k)

    let biadd ~size ~flags = Biadd{size;flags}
    let bisub ~size ~flags = Bisub{size;flags}
    let bimul ~size ~flags = Bimul{size;flags}
    let bor ~size = Bor(size)
    let band ~size = Band(size)
    let bxor ~size = Bxor(size)
    let bisdiv ~size = Bisdiv(size)
    let bismod ~size = Bismod(size)
    let biudiv ~size = Biudiv(size)
    let biumod ~size = Biumod(size)

    let bshl ~size ~flags = Bshl{size;flags}
    let bashr ~size = Bashr(size)
    let blshr ~size = Blshr(size)

    let bisle ~size = Bisle(size)
    let biule ~size = Biule(size)
    let beq ~size = Beq(size)

    let bconcat ~size1 ~size2 = Bconcat(size1,size2)
    let bextract ~size ~index ~oldsize = Bextract {size;oldsize;index}

    let valid ~size = assert false
    let valid_ptr_arith ~size = assert false
    let bindex ~size = assert false
    let bshift ~size ~offset ~max = assert false
    let buninit ~size = assert false

    let bsext ~size ~oldsize = Bsext(size)
    let buext ~size ~oldsize = Buext(size)

    let bofbool ~size = Bofbool(size)
    let bchoose ~size choice = Bchoose(choice,size)
    let bunion  ~size cond = Bunion(cond,size)
  end

end


(**************** Generic pretty printers. ****************)


(* This allows to print something (a type 'at) that contains a term. *)
module type PRETTY_ARG = sig
  type 'a t                     (* The term to print. *)
  type 'a pack                  (* Packing of the arguments. *)
  val pretty: Format.formatter -> 'a t -> unit
  (* Extraction of the subterms. *)
  val extract1: 'a ar1 pack -> 'a t
  val extract2: ('a,'b) ar2 pack -> 'a t * 'b t
end

module type PRETTY_RESULT = sig
  type 'a t
  type 'a pack
  val pretty_destruct: Format.formatter -> ('arg,'a) function_symbol -> 'arg pack -> unit
end

module Pretty(M:PRETTY_ARG):PRETTY_RESULT with type 'a t = 'a M.t and type 'a pack = 'a M.pack =
struct
  type 'a t = 'a M.t
  type 'a pack = 'a M.pack

  let pretty_destruct: type a arg. Format.formatter -> (arg,a) function_symbol -> arg M.pack -> unit =
    fun fmt term arg ->
      let ar1 arg string =
        let x1 = M.extract1 arg in Format.fprintf fmt string M.pretty x1
      in
      let ar2 arg string =
        let x1,x2 = M.extract2 arg in Format.fprintf fmt string M.pretty x1 M.pretty x2
      in
      let open Format in
      match term with
      | True -> fprintf fmt "true"
      | False -> fprintf fmt "false"
      | And -> ar2 arg "%a && %a"
      | Or -> ar2 arg "%a || %a"
      | Not-> ar1 arg "!(%a)"
      | BoolUnion->  ar2 arg "boolunion(%a,%a)"
      | Biconst(size,k) ->
        fprintf fmt "(bin%d " (size:>int);
        (if Z.numbits k < 8
         then (fprintf fmt "%s)" @@ Z.to_string k)
         else fprintf fmt "0x%s)" @@ Z.format "x" k)
      | Biadd(size) -> ar2 arg "(%a +b %a)"
      | Bisub(size) -> ar2 arg "(%a -b %a)"
      | Bimul(size) -> ar2 arg "(%a * %a)"
      | Biudiv(size) -> ar2 arg "(%a /bu %a)"
      | Bisdiv(size) -> ar2 arg "(%a /bs %a)"
      | Biumod(size) -> ar2 arg "(%a %%bs %a)"
      | Bismod(size) -> ar2 arg "(%a %%bu %a)"
      | Bshl(size) -> ar2 arg "(%a << %a)"
      | Blshr(size) -> ar2 arg "(%a >>l %a)"
      | Bashr(size) -> ar2 arg "(%a >>r %a)"
      | Band(size) -> ar2 arg "(%a & %a)"
      | Bor(size) -> ar2 arg "(%a | %a)"
      | Bxor(size) -> ar2 arg "(%a ^ %a)"
      | Beq(size) -> ar2 arg "(%a =b= %a)"
      | Bisle(size) -> ar2 arg "(%a <=bs %a)"
      | Biule(size) -> ar2 arg "(%a <=bu %a)"
      | Bconcat(s1,s2) -> ar2 arg "(%a::%a)"
      | Bunion(id,size) -> let x,y = M.extract2 arg in fprintf fmt "bunion%d_%d(%a,%a)" (id:>int) (size:>int) M.pretty x M.pretty y
      | Bextract{size;index;oldsize} -> (ar1 arg "(%a)[%d:%d]")  (index:>int) ((index:>int)+(size:>int))
      | Buext(size) -> let x = M.extract1 arg in fprintf fmt "buext%d(%a)" (size:>int) M.pretty x
      | Bsext(size) -> let x = M.extract1 arg in fprintf fmt "bsext%d(%a)" (size:>int) M.pretty x
      | Bofbool(size) -> let x = M.extract1 arg in fprintf fmt "bofbool%d(%a)" (size:>int) M.pretty x
      | Bchoose(id,size) -> let x = M.extract1 arg in fprintf fmt "bchoose%d_%d(%a)" (id:>int) (size:>int) M.pretty x

      | Iconst k -> (if Z.numbits k < 8
                     then (fprintf fmt "%s" @@ Z.to_string k)
                     else fprintf fmt "0x%s" @@ Z.format "x" k)
      | Idiv -> ar2 arg "(%a / %a)"
      | Imod -> ar2 arg "(%a %% %a)"
      | Iadd -> ar2 arg "(%a + %a)"
      | Isub -> ar2 arg "(%a - %a)"
      | Ieq -> ar2 arg "(%a = %a)"
      | Ile -> ar2 arg "(%a <= %a)"
      | Imul -> ar2 arg "(%a * %a)"
      | Ishl ->  ar2 arg "(%a << %a)"
      | Ishr ->  ar2 arg "(%a >> %a)"
      | Iand ->  ar2 arg "(%a & %a)"
      | Ior ->  ar2 arg "(%a | %a)"
      | Ixor ->  ar2 arg "(%a ^ %a)"
      | Itimes k ->
        let x = M.extract1 arg in fprintf fmt "(%s * %a)" (Z.to_string k) M.pretty x

      | EnumConst case -> fprintf fmt "(enum_const %d)" case
      | CaseOf case -> let x = M.extract1 arg in fprintf fmt "case %d of %a" case M.pretty x
end

(**************** Generic evaluation functions. ****************)
(* (Currently not used) *)

[@@@warning "-32"]
(* Generic evaluators; probably the genericity is not worth it (and,
   for instance, we lack some additional arguments here). *)
module Unused_Eval(T:sig
    type ('arg,'res) t
    val true_: (ar0,boolean) t
    val false_: (ar0,boolean) t

    val (&&): ((boolean,boolean) ar2,boolean) t
    val (||): ((boolean,boolean) ar2,boolean) t
    val not: (boolean ar1,boolean) t

    val biconst: size:size -> z_t -> (ar0,binary) t
    val bitimes: size:size -> z_t -> (binary ar1,binary) t
    val biadd: size:size -> ((binary,binary) ar2,binary) t
    val bisub: size:size -> ((binary,binary) ar2,binary) t
    val bimul: size:size -> ((binary,binary) ar2,binary) t
    val bisdiv: size:In_bits.t -> ((binary,binary) ar2,binary) t
    val bismod: size:In_bits.t -> ((binary,binary) ar2,binary) t
    val biudiv: size:In_bits.t -> ((binary,binary) ar2,binary) t
    val biumod: size:In_bits.t -> ((binary,binary) ar2,binary) t

    val bshl: size:In_bits.t -> ((binary,binary) ar2,binary) t
    val bashr: size:In_bits.t -> ((binary,binary) ar2,binary) t
    val blshr: size:In_bits.t -> ((binary,binary) ar2,binary) t

    val band: size:In_bits.t -> ((binary,binary) ar2,binary) t
    val bor: size:In_bits.t -> ((binary,binary) ar2,binary) t
    val bxor: size:In_bits.t -> ((binary,binary) ar2,binary) t

    val beq: size:size   -> ((binary,binary) ar2,boolean) t
    val bisle: size:size -> ((binary,binary) ar2,boolean) t
    val biule: size:size -> ((binary,binary) ar2,boolean) t

    (* First argument become most significant. *)
    val bconcat: size1:In_bits.t -> size2:In_bits.t -> ((binary,binary) ar2,binary) t
    val bextract: size:In_bits.t -> index:In_bits.t -> oldsize:In_bits.t -> (binary ar1,binary) t

    val buext: size:In_bits.t -> (binary ar1,binary) t
    val bsext: size:In_bits.t -> (binary ar1,binary) t


    val iconst: z_t -> (ar0,integer) t
    val itimes: z_t -> (integer ar1,integer) t
    val iadd: ((integer,integer) ar2,integer) t
    val imul: ((integer,integer) ar2,integer) t
    val idiv: ((integer,integer) ar2,integer) t
    val imod: ((integer,integer) ar2,integer) t
    val ishl: ((integer,integer) ar2,integer) t
    val ishr: ((integer,integer) ar2,integer) t
    val iand: ((integer,integer) ar2,integer) t
    val ior: ((integer,integer) ar2,integer ) t
    val ixor: ((integer,integer) ar2,integer) t
    val isub: ((integer,integer) ar2,integer) t
    val ieq: ((integer,integer) ar2,boolean ) t
    val ile: ((integer,integer) ar2,boolean ) t

  end) = struct

  let eval:type arg res. (arg,res) function_symbol -> (arg,res) T.t = function
    | True -> T.true_
    | False -> T.false_
    | And -> T.(&&)
    | Or -> T.(||)
    | Not -> T.not
    | Biconst(size,k) -> T.biconst ~size k
    | Biadd{size;flags} -> (* T.biadd ~size ~nsw ~nuw *) assert false
    | Bisub{size;flags} -> (* T.bisub ~size ~nsw ~nuw *) assert false
    | Bimul{size;flags} -> (* T.bimul ~size ~nsw ~nuw *) assert false
    | Bisdiv(size) -> T.bisdiv ~size
    | Bismod(size) -> T.bismod ~size
    | Biudiv(size) -> T.biudiv ~size
    | Biumod(size) -> T.biumod ~size
    | Bshl{size;flags} -> (* T.bshl ~size *) assert false
    | Bashr(size) -> T.bashr ~size
    | Blshr(size) -> T.blshr ~size
    | Band(size) -> T.band ~size
    | Bor(size) -> T.bor ~size
    | Bxor(size) -> T.bxor ~size
    | Beq(size) -> T.beq ~size
    | Bisle(size) -> T.bisle ~size
    | Biule(size) -> T.biule ~size
    | Buext(size) -> T.buext ~size
    | Bsext(size) -> T.bsext ~size
    | Bconcat(size1,size2) -> T.bconcat ~size1 ~size2
    | Bextract{size;index;oldsize} -> T.bextract ~size ~index ~oldsize
    | Bofbool _ -> assert false
    | Bchoose _ -> assert false
    | Bunion _ -> assert false
    | BoolUnion -> assert false
    | Iconst k -> T.iconst k
    | Itimes k -> T.itimes k
    | Iadd -> T.iadd
    | Imul -> T.imul
    | Idiv -> T.idiv
    | Imod -> T.imod
    | Ishl -> T.ishl
    | Ishr -> T.ishr
    | Iand -> T.iand
    | Ior -> T.ior
    | Ixor -> T.ixor
    | Isub -> T.isub
    | Ieq -> T.ieq
    | Ile -> T.ile
    | EnumConst case -> assert false
    | CaseOf case -> assert false
  ;;

end

(* Idem; it is probably better if eval matches the term together with
   its argument, and directly known the type of the arguments. *)
module Unused_Eval_Forward(T:sig
    type 'a t
    type 'a pack

    val extract2: ('a,'b) ar2 pack -> 'a t * 'b t
    val extract1: ('a) ar1 pack -> 'a t

    val true_:  boolean t
    val false_:  boolean t
    val (&&): boolean t -> boolean t -> boolean t
    val (||): boolean t -> boolean t -> boolean t
    val not: boolean t -> boolean t

    val biconst: size:size -> z_t ->  binary t
    val bitimes: size:size -> z_t -> binary t -> binary t
    val biadd: size:size -> binary t -> binary t -> binary t
    val bisub: size:size -> binary t -> binary t -> binary t
    val bimul: size:size -> binary t -> binary t -> binary t
    val bisdiv: size:In_bits.t -> binary t -> binary t -> binary t
    val bismod: size:In_bits.t -> binary t -> binary t -> binary t
    val biudiv: size:In_bits.t -> binary t -> binary t -> binary t
    val biumod: size:In_bits.t -> binary t -> binary t -> binary t

    val bshl: size:In_bits.t -> binary t -> binary t -> binary t
    val bashr: size:In_bits.t -> binary t -> binary t -> binary t
    val blshr: size:In_bits.t -> binary t -> binary t -> binary t

    val band: size:In_bits.t -> binary t -> binary t -> binary t
    val bor: size:In_bits.t -> binary t -> binary t -> binary t
    val bxor: size:In_bits.t -> binary t -> binary t -> binary t

    val beq: size:size -> binary t -> binary t -> boolean t
    val bisle: size:size -> binary t -> binary t -> boolean t
    val biule: size:size -> binary t -> binary t -> boolean t

    val bconcat: size1:In_bits.t -> size2:In_bits.t -> binary t -> binary t -> binary t
    val bextract: size:In_bits.t -> index:In_bits.t -> oldsize:In_bits.t -> binary t -> binary t

    val buext: size:In_bits.t -> binary t -> binary t
    val bsext: size:In_bits.t -> binary t -> binary t

    val iconst: z_t -> integer t
    val itimes: z_t -> integer t -> integer t
    val iadd: integer t -> integer t -> integer t
    val imul: integer t -> integer t -> integer t
    val idiv: integer t -> integer t -> integer t
    val imod: integer t -> integer t -> integer t
    val ishl: integer t -> integer t -> integer t
    val ishr: integer t -> integer t -> integer t
    val iand: integer t -> integer t -> integer t
    val ior: integer t -> integer t -> integer  t
    val ixor: integer t -> integer t -> integer t
    val isub: integer t -> integer t -> integer t
    val ieq: integer t -> integer t -> boolean  t
    val ile: integer t -> integer t -> boolean  t
  end) = struct

  let eval:type arg res. (arg,res) function_symbol -> arg T.pack -> res T.t = function
    | True -> fun _ -> T.true_
    | False -> fun _ -> T.false_
    | And -> fun arg -> let (b1,b2) = T.extract2 arg in T.(&&) b1 b2
    | Or -> fun arg -> let (b1,b2) = T.extract2 arg in T.(||) b1 b2
    | Not -> fun arg -> T.not @@ T.extract1 arg
    | Biconst(size,k) -> fun _ -> T.biconst ~size k
    | Biadd{size;flags} -> fun arg -> let (_b1,_b2) = T.extract2 arg in (* T.biadd ~size b1 b2 *) assert false
    | Bisub{size;flags} -> fun arg -> let (_b1,_b2) = T.extract2 arg in (* T.bisub ~size b1 b2 *) assert false
    | Bimul{size;flags} -> fun arg -> let (_b1,_b2) = T.extract2 arg in (* T.bimul ~size b1 b2 *) assert false
    | Bisdiv(size) -> fun arg -> let (b1,b2) = T.extract2 arg in T.bisdiv ~size b1 b2
    | Bismod(size) -> fun arg -> let (b1,b2) = T.extract2 arg in T.bismod ~size b1 b2
    | Biudiv(size) -> fun arg -> let (b1,b2) = T.extract2 arg in T.biudiv ~size b1 b2
    | Biumod(size) -> fun arg -> let (b1,b2) = T.extract2 arg in T.biumod ~size b1 b2
    | Bshl{size;flags} -> fun arg -> let (_b1,_b2) = T.extract2 arg in (* T.bshl ~size b1 b2 *) assert false
    | Bashr(size) -> fun arg -> let (b1,b2) = T.extract2 arg in T.bashr ~size b1 b2
    | Blshr(size) -> fun arg -> let (b1,b2) = T.extract2 arg in T.blshr ~size b1 b2
    | Band(size) -> fun arg -> let (b1,b2) = T.extract2 arg in T.band ~size b1 b2
    | Bor(size) -> fun arg -> let (b1,b2) = T.extract2 arg in T.bor ~size b1 b2
    | Bxor(size) -> fun arg -> let (b1,b2) = T.extract2 arg in T.bxor ~size b1 b2
    | Beq(size) -> fun arg -> let (b1,b2) = T.extract2 arg in T.beq ~size b1 b2
    | Bisle(size) -> fun arg -> let (b1,b2) = T.extract2 arg in T.bisle ~size b1 b2
    | Biule(size) -> fun arg -> let (b1,b2) = T.extract2 arg in T.biule ~size b1 b2
    | Buext(size) -> fun arg -> T.buext ~size @@ T.extract1 arg
    | Bsext(size) -> fun arg -> T.bsext ~size @@ T.extract1 arg
    | Bconcat(size1,size2) -> fun arg -> let (b1,b2) = T.extract2 arg in T.bconcat ~size1 ~size2 b1 b2
    | Bextract{size;index;oldsize} -> fun arg -> T.bextract ~size ~index ~oldsize @@ T.extract1 arg
    | Bofbool(size) -> assert false
    | Bchoose(id,size) -> assert false
    | Bunion(id,size) -> assert false
    | Iconst k -> fun _ -> T.iconst k
    | Itimes k -> fun arg -> T.itimes k @@ T.extract1 arg
    | Iadd -> fun arg -> let (i1,i2) = T.extract2 arg in T.iadd i1 i2
    | Imul -> fun arg -> let (i1,i2) = T.extract2 arg in T.imul i1 i2
    | Idiv -> fun arg -> let (i1,i2) = T.extract2 arg in T.idiv i1 i2
    | Imod -> fun arg -> let (i1,i2) = T.extract2 arg in T.imod i1 i2
    | Ishl -> fun arg -> let (i1,i2) = T.extract2 arg in T.ishl i1 i2
    | Ishr -> fun arg -> let (i1,i2) = T.extract2 arg in T.ishr i1 i2
    | Iand -> fun arg -> let (i1,i2) = T.extract2 arg in T.iand i1 i2
    | Ior  -> fun arg -> let (i1,i2) = T.extract2 arg in T.ior  i1 i2
    | Ixor -> fun arg -> let (i1,i2) = T.extract2 arg in T.ixor i1 i2
    | Isub -> fun arg -> let (i1,i2) = T.extract2 arg in T.isub i1 i2
    | Ieq  -> fun arg -> let (i1,i2) = T.extract2 arg in T.ieq  i1 i2
    | Ile  -> fun arg -> let (i1,i2) = T.extract2 arg in T.ile  i1 i2
    | BoolUnion -> assert false
    | EnumConst _ -> assert false
    | CaseOf(case) -> fun arg -> let _b = T.extract1 arg in assert false
end


(* Smartcons could be the home to a generic implementation of Smart
   constructors, independent from the data attached to type t.

   One issue is how to handle conditions; e.g. 0 * (1/x) can be
   rewritten to 0 only if x is non-zero. Maybe we should be combining
   the "conditions" attached to each argument, if there are some. *)
module Unused_SmartCons(M:sig
    type 'a t
    val destruct: 'b t -> ('a,'b) function_symbol * 'a t
    val construct: ('a,'b) function_symbol -> 'a t -> 'b t
    val split_boolean_boolean: (boolean, boolean) ar2 t -> boolean t * boolean t
    val combine_boolean_boolean: boolean t -> boolean t -> (boolean, boolean) ar2 t
  end) = struct

  let (&&): boolean M.t -> boolean M.t -> boolean M.t = fun a b ->
    match M.destruct a with
    | (True,_) -> b
    | _ -> match M.destruct b with
      | (True,_) -> a
      | _ -> M.construct And @@ M.combine_boolean_boolean a b
  ;;

end
[@@@warning "+32"]