package codex

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

Source file bitwise.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
(**************************************************************************)
(*  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 In_bits = Units.In_bits

(* One issue with my tests is that whenever I get through the memory,
   it does not work.  So, the bitwise domain should be beneath
   memory_domain, but above the pointers.

   This raises the questions: why these operable values are not true
   domains?

   Answer: they should. Region separation should just be 2 functor
   domains, one for the binary, one for the memory.

   Or at least, memory_domain should be split into two domains, two
   allow intermediate domains like this one. *)
let pretty_detailed = true

module Quadrivalent = Lattices.Quadrivalent

module Make (Sub : Sig.BASE) = struct

  let name() = "Bitwise(" ^ (Sub.name()) ^ ")";;
  let unique_id() = Sig.Fresh_id.fresh @@ name();;

  (** To represent values, we could use an array where each bit would
      be a bit in another variable, but this would be slow for most
      operation. So, we use a list of "parts" that group these bits,
      and the information is complemented with the known 0 bits and
      known 1 bits informat that we query from Sub. *)
  type binary_part = { size:In_bits.t; index:In_bits.t; oldsize:In_bits.t; value:Sub.binary }
  (* We call this extract even when there is no extraction, in which case index == 0 and size == oldsize. *)


  module Part = struct
    let pretty ctx fmt {size;index;oldsize;value} =
      if index == In_bits.zero && size == oldsize
      then Format.fprintf fmt "(%a)<%d>" (Sub.binary_pretty ~size ctx) value (size:>int)
      else Format.fprintf fmt "(%a)[%d..+%d]" (Sub.binary_pretty ~size ctx) value (index:>int) (size:>int)

    let zero ctx ~size = { size; index=In_bits.zero; oldsize=size;
                           value=Sub.Binary_Forward.biconst ~size Z.zero ctx}

    let ones ctx ~size =
      { size; index=In_bits.zero; oldsize=size;
        value = Sub.Binary_Forward.biconst ~size (Z.extract Z.minus_one 0 (size:>int)) ctx }

    let do_extract ctx {size;index;oldsize;value} =
      if size = oldsize then value
      else Sub.Binary_Forward.bextract ~size ~index ~oldsize ctx value

    let to_singleton ctx {size;index;oldsize;value} =
      let bin = Sub.Binary_Forward.bextract ~size ~index ~oldsize ctx value in
      Sub.Query.binary ~size ctx bin |> Sub.Query.Binary_Lattice.is_singleton ~size

    let from_value ~size value = {size;index=In_bits.zero;oldsize=size;value}

  end

  module Parts = struct

    (* A binary is represented as a list where head is the least significant binary_part
       (this allows for efficient additions, etc). *)
    type t = binary_part list;;

    (* Remove the first ~index bits from the start. *)
    let cut_start ~index p =
      (* Invariant: i <= index. *)
      let rec loop i = function
        | [] -> assert false     (* Index is larger than the size. *)
        | { size; _ }::rest when In_bits.(i + size <= index) -> loop In_bits.(i + size) rest
        | { size=sizee; index=indexe; oldsize; value }::rest as l ->
          if i == index then l
          else
            let removed_size = In_bits.(index - i) in
            { size=In_bits.(sizee-removed_size); index=In_bits.(indexe+removed_size); oldsize; value }::rest
      in loop In_bits.zero p
    ;;

    (* Cut the part so that its size becomes size, which must be smaller than the original size. *)
    let cut_end ~size p =
      let rec loop i = function
        (* | [] when i == size -> [] *)
        | [] -> assert false     (* The parts is too small, cannot cut. *)
        | hd::tl when In_bits.(i + hd.size < size) -> hd::(loop In_bits.(i + hd.size) tl)
        | hd::_ when In_bits.(i + hd.size) = size -> [hd]
        | { size=sizee; index; oldsize; value }::_ ->
          let removed_size = In_bits.(i + sizee - size) in
          [{ size=In_bits.(sizee-removed_size); index; oldsize; value }]
      in loop In_bits.zero p
    ;;

    let extract ~index ~size ~oldsize p =
      (* cut the first bits up to index. *)
      let p =
        if index == In_bits.zero then p
        else cut_start ~index p
      in
      (* cut the size firts bits of p. *)
      let p =
        if In_bits.(index + size) == oldsize then p
        else cut_end ~size p
      in
      p
    ;;

    let append a b = List.append a b;;

    let append ctx a b =
      match b with
      | [] -> assert false
      | hdb::tlb -> begin
          let rec loop = function
            | [] -> b
            | [lasta] -> begin
                (*Codex_log.feedback "lasta = %a" (Part.pretty ctx) lasta;
                  Codex_log.feedback "hdb = %a" (Part.pretty ctx) hdb;*)
                (*let b1 = lasta'.index + lasta'.size == hdb'.index in
                  let b2 = Sub.Binary.equal lasta'.value hdb'.value in
                  Codex_log.feedback "b1 = %B" b1;
                  Codex_log.feedback "b2 = %B" b2;*)
                match lasta,hdb with
                | { size=sizea; index=indexa; oldsize=oldsizea; value=valuea },
                  { size=sizeb; index=indexb; oldsize=oldsizeb; value=valueb }
                  when In_bits.(indexa + sizea == indexb) && Sub.Binary.equal valuea valueb ->
                  (* Stitch together contiguous extractions. *)
                  assert(oldsizea == oldsizeb);
                  { size=In_bits.(sizea+sizeb); index=indexa; oldsize=oldsizea; value=valuea }::tlb
                | { size=sizea; _ },{size=sizeb; _ } -> begin
                    match Part.to_singleton ctx lasta,Part.to_singleton ctx hdb with
                    | Some csta, Some cstb ->
                      let size = In_bits.(sizea + sizeb) in
                      let zvalue = Operator.Concrete.Bitvector_Interp.bconcat ~size1:sizeb ~size2:sizea cstb csta in
                      let value = Sub.Binary_Forward.biconst ~size zvalue ctx in
                      (Part.from_value ~size value)::tlb
                    | _ -> lasta::hdb::tlb
                  end
              end
            | hd::tl -> hd::(loop tl)
          in loop a
        end
    ;;

    (* Preprend (i.e. put in least significant positions) size bits of value 0.  *)
    let prepend_zero ~size ctx p = append ctx [(Part.zero ~size ctx)] p;;

    (* Append (i.e. put in most significant positions) size bits of value 0.  *)
    let append_zero ~size ctx p = append ctx p [(Part.zero ~size ctx)];;

    let chop_last l =
      let rec loop acc = function
        | [] -> assert false
        | [x] -> List.rev acc, x
        | hd :: tl -> loop (hd :: acc) tl
      in loop [] l

    (* Append (i.e. put in most significant positions) size times the most
     * significant bit. If the most significant bit is unknown, use the
     * subdomain to extend the last part. *)
    let signed_extend ~size ~oldsize ctx p =
      let beginning, { size=s_last; value; _ } = chop_last p in
      let zeroes, ones = Sub.Query.(binary ~size:s_last ctx value |> Binary_Lattice.to_known_bits ~size:s_last) in
      if not (Z.testbit zeroes ((s_last:>int)-1)) then
        append_zero ~size:In_bits.(size - oldsize) ctx p
      else if Z.testbit ones ((s_last:>int)-1) then
        append ctx p [Part.ones ~size:In_bits.(size - oldsize) ctx]
      else
        let s = In_bits.(size - oldsize + s_last) in
        append ctx beginning [Part.from_value ~size:s (Sub.Binary_Forward.bsext ~size:s ~oldsize:s_last ctx value)]

    let fold2 ctx f acc pa pb =
      let rec loop acc pa pb = match pa,pb with
        | [],[] -> acc
        | [], _ | _, [] -> acc (* assert false *) (* Different lengths. *)
        | ({size=sizea;index=indexa;oldsize=oldsizea;value=valuea} as pa)::tla,
          ({size=sizeb;index=indexb;oldsize=oldsizeb;value=valueb} as pb)::tlb ->
          (*Codex_log.feedback "fold2 sizea:%d sizeb:%d oldsizea:%d oldsizeb:%d" sizea sizeb oldsizea oldsizeb;*)
          if(sizea == sizeb) then
            let acc = f ~size:sizea acc pa pb in
            loop acc tla tlb
          else if(sizea < sizeb) then
            let bb = {size=sizea; index=indexb; oldsize=oldsizeb; value=valueb} in
            let acc = f ~size:sizea acc pa bb in
            loop acc tla ({size=In_bits.(sizeb-sizea);index=In_bits.(indexb+sizea);oldsize=oldsizeb;value=valueb}::tlb)
          else
            let ba = {size=sizeb; index=indexa; oldsize=oldsizea; value=valuea} in
            let acc = f ~size:sizeb acc ba pb in
            loop acc ({size=In_bits.(sizea-sizeb);index=In_bits.(indexa+sizeb);oldsize=oldsizea;value=valuea}::tla) tlb
      in loop acc pa pb

    type bits =
      | Zeroes of In_bits.t (** size. *)
      | Ones of In_bits.t (** size. *)
      | Unknown of binary_part

    let pretty_bits ctx fmt =
      let open Format in function
        | Zeroes s -> fprintf fmt "00..0<%d>" (s:>int)
        | Ones s -> fprintf fmt "11..1<%d>" (s:>int)
        | Unknown p -> Part.pretty ctx fmt p

    let decompose_using_known_bits ~size ctx part =
      let {size;index;oldsize;value} = part in
      let sub = Part.do_extract ctx part in
      (* Identify groups of known bits *)
      let zeroes, ones = Sub.Query.Binary_Lattice.to_known_bits ~size @@ Sub.Query.binary ~size ctx sub in
      let rec loop acc cur (i:int) =
        if i >= (size:>int) then List.rev (cur :: acc)
        else match Z.testbit zeroes i, Z.testbit ones i, cur with
          | false, true, _ -> raise Sig.Bottom
          | false, _, Zeroes s -> loop acc (Zeroes In_bits.(s+one)) (i+1)
          | false, _, _ -> loop (cur :: acc) (Zeroes In_bits.one) (i+1)
          | _, true, Ones s -> loop acc (Ones In_bits.(s+one)) (i+1)
          | _, true, _ -> loop (cur :: acc) (Ones In_bits.one) (i+1)
          | true, false, Unknown e -> loop acc (Unknown{e with size=In_bits.(e.size+one)}) (i+1)
          | true, false, _ -> loop (cur :: acc) (Unknown{size=In_bits.one;index=In_bits.(index+ of_int i);oldsize;value}) (i+1)
      in
      loop []
        (if not (Z.testbit zeroes 0)
         then Zeroes In_bits.one
         else if Z.testbit ones 0
         then Ones In_bits.one
         else Unknown {size=In_bits.one;index;oldsize;value})
        1

    let fold2_bits ctx f acc pa pb =
      let split size_fst = function
        | Zeroes size -> Zeroes size_fst, Zeroes In_bits.(size - size_fst)
        | Ones size -> Ones size_fst, Ones In_bits.(size - size_fst)
        | Unknown {size;index;oldsize;value} ->
          Unknown {size=size_fst; index; oldsize; value},
          Unknown {size=In_bits.(size-size_fst); index=In_bits.(index+size_fst); oldsize; value}
      in
      let rec loop acc pa pb = match pa,pb with
        | [],[] -> acc
        | [],_ | _,[] -> assert false (* Should not happen (invariant of this function) *)
        | (( Unknown{size=sizea;_}
           | Zeroes sizea
           | Ones sizea) as pa) :: tla,
          (( Unknown{size=sizeb;_}
           | Zeroes sizeb
           | Ones sizeb) as pb) :: tlb ->
          if sizea = sizeb then
            let acc = f ctx ~size:sizea acc pa pb in
            loop acc tla tlb
          else if sizea < sizeb then
            let fst_pb, rest_pb = split sizea pb in
            let acc = f ctx ~size:sizea acc pa fst_pb in
            loop acc tla (rest_pb :: tlb)
          else
            let fst_pa, rest_pa = split sizeb pa in
            let acc = f ctx ~size:sizeb acc fst_pa pb in
            loop acc (rest_pa :: tla) tlb
      in
      loop acc pa pb

    (* Note: can raise Bottom if it discovers bottom. *)
    let fold2_known_bits ctx f acc pa pb =
      fold2 ctx (fun ~size acc pa pb ->
          let bitsa = decompose_using_known_bits ~size ctx pa in
          let bitsb = decompose_using_known_bits ~size ctx pb in
          fold2_bits ctx f acc bitsa bitsb
        ) acc pa pb

  end

  type binary_ = { complete: Sub.binary;
                   parts: Parts.t
                 }

  module Binary = struct
    type t = binary_;;

    (*  We could check for equality of the parts too. *)
    let equal x y = Sub.Binary.equal x.complete y.complete

    let compare x y = Sub.Binary.compare x.complete y.complete
    let hash _ = assert false

    let pretty pp x =
      Sub.Binary.pretty pp x.complete

    (* Lift a constant. *)
    let lift0 ~size x = { complete = x; parts = [{size;oldsize=size;index=In_bits.zero;value=x}]}
    (* Lifts a (bitwise) function over binaries. *)
    let lift1 ~size f x =
      { complete = f ~size x.complete;
        parts = List.map (function
            | x -> { x with value=f ~size:x.oldsize x.value }
            (* | Repeat{repeat;value} -> Repeat{repeat;value=f ~size:1 value} *)
          ) x.parts }

    (* Lift a (non-necessarily bitwise) binary operator. *)
    let lift2 ~size ctx f x y =
      (* If an operand consists in a single part, use it, as it should usually
       * (always?) be more precise than x.complete. *)
      let x = match x.parts with
        | [p] -> Part.do_extract ctx p
        | _ -> x.complete
      in
      let y = match y.parts with
        | [p] -> Part.do_extract ctx p
        | _ -> y.complete
      in
      f ~size ctx x y

    (* TODO: improve this. *)
    let lift2_pred ~size ctx f x y =
      let with_parts = lift2 ~size ctx f x y in
      match Sub.query_boolean ctx with_parts with
      | Quadrivalent.True | Quadrivalent.False | Quadrivalent.Bottom -> with_parts
      | _ -> f ~size ctx x.complete y.complete
    ;;


  end

  module Types = struct
    type binary = Binary.t
    type enum = Sub.enum
    type boolean = Sub.boolean
  end
  include Types

  module Boolean = Sub.Boolean
  module Enum = Sub.Enum
  module Context = Sub.Context
  open Context

  let root_context = Sub.root_context
  let context_pretty = Sub.context_pretty

  (* include Operator.Builtin.Make(Types)(Context) *)

  let mu_context_open = Sub.mu_context_open

  let assume = Sub.assume

  let binary_empty ~size ctx = { parts = []; complete = Sub.binary_empty ~size ctx }
  let boolean_empty = Sub.boolean_empty
  let enum_empty = Sub.enum_empty


  module Boolean_Forward = Sub.Boolean_Forward
  module Enum_Forward = Sub.Enum_Forward
  (* let [@inline always] ar0 ~size f = fun ctx ->
   *   Binary.of_sub ~size @@ f ctx
   * let [@inline always] ar1 ~size f = fun ctx a ->
   *   Binary.of_sub ~size @@ f ctx @@ Binary.to_sub ~size ctx a
   * let [@inline always] ar2 ~size f = fun ctx a b ->
   *   Binary.of_sub ~size @@ f ctx
   *     (Binary.to_sub ~size ctx a) (Binary.to_sub ~size ctx b)
   * let [@inline always] pred2 ~size f = fun ctx a b ->
   *   f ctx (Binary.to_sub ~size ctx a) (Binary.to_sub ~size ctx b)
   * let [@inline always] ar3 f = fun ctx a b c -> match a,b,c with
   *   | Some a, Some b,  Some c -> Some (f ctx a b c)
   *   | _ -> None
   *
   * let to_ival ~signed ~size ctx x =
   *   Binary.to_sub ~size ctx x |> Sub.Query.binary ~size ctx
   *   |> Sub.Query.binary_to_ival ~signed ~size
   *
   * let to_integer ~signed ~size ctx x =
   *   to_ival ~signed ~size ctx x |> Framac_ival.Ival.project_int *)

  let binary_pretty ~size ctx fmt (x : binary) =
    (* match List.rev x.parts with
    | [] -> assert false
    | hd::tl ->
      Sub.binary_pretty ~size ctx fmt x.complete;
      (*
      Format.pp_print_string fmt "(= [";
      Part.pretty ctx fmt hd;
      List.iter (fun p -> Format.fprintf fmt "::%a" (Part.pretty ctx) p) tl;
      Format.pp_print_string fmt "])";
      *)
    *)
    Sub.binary_pretty ~size ctx fmt x.complete

  module Binary_Forward = struct

    module SBF = Sub.Binary_Forward;;

    let bofbool ~size ctx b =
      SBF.bofbool ~size ctx b |> Binary.lift0 ~size

    let bchoose ~size choice ctx x = SBF.bchoose ~size choice ctx x.complete |> Binary.lift0 ~size
    let valid ~size _ = assert false

    (* let valid_ptr_arith ~size _ = assert false
     * let bunknown ~size _ = assert false
     * let baddr ~size _  = assert false
     * let biconst ~size _ = assert false
     * let buninit ~size _ = assert false *)

    let bindex ~size _ = assert false

    let valid_ptr_arith ~size arith ctx a b =
      Sub.Binary_Forward.valid_ptr_arith ~size arith ctx a.complete b.complete

    let biconst ~size ctx k = Binary.lift0 ~size @@ SBF.biconst ~size ctx k;;
    let buninit ~size ctx = Binary.lift0 ~size @@ SBF.buninit ~size ctx;;
    let bisle ~size ctx a b = Binary.lift2_pred ~size ctx SBF.bisle a b
    let biule ~size ctx a b = Binary.lift2_pred ~size ctx SBF.biule a b

    let bisub ~size ~flags ctx a b = Binary.lift0 ~size @@ SBF.bisub ~size ~flags ctx a.complete b.complete
    let bimul ~size ~flags ctx a b = Binary.lift0 ~size @@ SBF.bimul ~size ~flags ctx a.complete b.complete
    let bisdiv ~size ctx a b = Binary.lift0 ~size @@ SBF.bisdiv ~size ctx a.complete b.complete
    let biudiv ~size ctx a b = Binary.lift0 ~size @@ SBF.biudiv ~size ctx a.complete b.complete
    let bismod ~size ctx a b = Binary.lift0 ~size @@ SBF.bismod ~size ctx a.complete b.complete
    let biumod ~size ctx a b = Binary.lift0 ~size @@ SBF.biumod ~size ctx a.complete b.complete

    let bconcat ~size1 ~size2 ctx b1 b2 =
      (*Codex_log.feedback "@[<v 2>BW.bconcat ~size1:%d ~size2:%d@.%a@.%a@]" size1 size2 (binary_pretty ~size:size1 ctx) b1 (binary_pretty ~size:size2 ctx) b2;*)
      let complete = SBF.bconcat ~size1 ~size2 ctx b1.complete b2.complete in
      (* Order of arguments reversed, since b1 should become the most
       * significant part. *)
      let parts = Parts.append ctx b2.parts b1.parts in
      let res = { complete; parts; } in
      (*Codex_log.feedback "result = %a" (binary_pretty ~size:(size1+size2) ctx) res;*)
      res

    let buext ~size ~oldsize ctx x =
      { complete = SBF.buext ~size ~oldsize ctx x.complete;
        (* parts = Parts.append x.parts [Part.zero ~size:(size-oldsize) ctx]; *)
        parts = Parts.append_zero ~size:In_bits.(size-oldsize) ctx x.parts;
      }
    ;;

    let bsext ~size ~oldsize ctx x =
      { complete = SBF.bsext ~size ~oldsize ctx x.complete;
        parts = Parts.signed_extend ~size ~oldsize ctx x.parts }

    let bextract ~size ~index ~oldsize ctx x =
      (*Codex_log.feedback "bextract ~size:%d ~index:%d ~oldsize:%d %a" size index oldsize (binary_pretty ~size:oldsize ctx) x;*)
      let res =
        { parts = Parts.extract ~index ~size ~oldsize x.parts;
          complete = SBF.bextract ~size ~index ~oldsize ctx x.complete
        }
      in
      (*Codex_log.feedback "result = %a" (binary_pretty ~size:oldsize ctx) res;*)
      res

    let bshl ~size ~flags ctx x y =
      let complete = SBF.bshl ~size ~flags ctx x.complete y.complete in
      match Sub.Query.Binary_Lattice.is_singleton ~size @@ Sub.Query.binary ~size ctx y.complete with
      | None -> Binary.lift0 ~size complete
      | Some y ->
        let parts = Parts.prepend_zero ~size:In_bits.(of_int @@ Z.to_int y) ctx x.parts in
        let parts = Parts.cut_end ~size parts in
        { complete; parts }
    ;;

    let blshr ~size ctx x y =
      let complete = SBF.blshr ~size ctx x.complete y.complete in
      match Sub.Query.Binary_Lattice.is_singleton ~size @@ Sub.Query.binary ~size ctx y.complete with
      | None -> Binary.lift0 ~size complete
      | Some y ->
        let yi = Z.to_int y |> In_bits.of_int in
        assert In_bits.(zero <= yi);
        if yi == In_bits.zero then x else
          let parts = Parts.append_zero ~size:yi ctx x.parts in
          let parts = Parts.cut_start ~index:yi parts in
          { complete; parts }

    let bashr ~size ctx x y =
      let complete = SBF.bashr ~size ctx x.complete y.complete in
      match Sub.Query.(Binary_Lattice.is_singleton ~size @@ binary ~size ctx y.complete) with
      | None -> Binary.lift0 ~size complete
      | Some y ->
        let yi = Z.to_int y |> In_bits.of_int in
        let beginning, {size=s_last;value;_} = Parts.chop_last x.parts in
        let zeroes,ones = Sub.Query.(Binary_Lattice.to_known_bits ~size:s_last @@
                                     binary ~size:s_last ctx value) in
        let parts =
          if not (Z.testbit zeroes ((s_last:>int)-1)) then
            let parts = Parts.append_zero ~size:yi ctx x.parts in
            Parts.cut_start ~index:yi parts
          else if Z.testbit ones ((s_last:>int)-1) then
            let parts = Parts.append ctx x.parts [Part.ones ctx ~size:yi] in
            Parts.cut_start ~index:yi parts
          else
            let new_sz_last = In_bits.(s_last+yi) in
            let to_append = SBF.bsext ~size:new_sz_last ~oldsize:s_last ctx value in
            let parts = Parts.append ctx beginning [Part.from_value ~size:new_sz_last to_append] in
            Parts.cut_start ~index:yi parts
        in
        { complete; parts }

    (* TODO: ici, on voudrait faire l'intersection des deux modes de calcul. *)
    let beq ~size ctx a b =
      (*Codex_log.feedback "@[<v 2>beq ~size:%d@.a = %a@.b = %a@]"
        size (binary_pretty ~size ctx) a (binary_pretty ~size ctx) b;*)
      Parts.fold2 ctx (fun ~size acc a b ->
          (*Codex_log.feedback "beq folding: acc = %a, a = %a, b = %a"
            Sub.Boolean.pretty acc (Part.pretty ctx) a (Part.pretty ctx) b;*)
          Sub.Boolean_Forward.(&&) ctx acc @@
          Sub.Binary_Forward.beq ~size ctx (Part.do_extract ctx a) (Part.do_extract ctx b)
        ) (Sub.Boolean_Forward.true_ ctx) a.parts b.parts
    ;;

    (* TODO: Use the other beq only if better. *)
    let beq ~size ctx a b =
      let with_parts = beq ~size ctx a b in
      match Sub.query_boolean ctx with_parts with
      | Quadrivalent.True | Quadrivalent.False | Quadrivalent.Bottom -> with_parts
      | _ -> Sub.Binary_Forward.beq ~size ctx a.complete b.complete;;


    let of_bits ctx = function
      | Parts.Zeroes size -> Part.from_value ~size @@ SBF.biconst ~size Z.zero ctx
      | Parts.Ones size -> Part.from_value ~size @@ SBF.biconst ~size (Z.extract Z.minus_one 0 (size:>int)) ctx
      | Parts.Unknown part -> part

    let or_bits ~size ctx a b = match a,b with
      | Parts.Zeroes _, _ -> of_bits ctx b
      | _, Parts.Zeroes _ -> of_bits ctx a
      | Parts.Ones _, _ -> of_bits ctx a
      | _, Parts.Ones _ -> of_bits ctx b
      | Parts.(Unknown pa, Unknown pb) ->
        Part.from_value ~size @@
        SBF.bor ~size ctx (Part.do_extract ctx pa) (Part.do_extract ctx pb)

    (* The parts is also used by addition in some cases. *)
    let bor' complete ~size ctx a b =
      (*Codex_log.feedback "@[<v 2>BW.bor ~size:%d@.%a@.%a@]" size (binary_pretty ~size:size ctx) a (binary_pretty ~size:size ctx) b;*)
      let res = try
          let parts = Parts.fold2_known_bits ctx (fun ctx ~size acc ba bb ->
              (*Codex_log.feedback "ba = %a, bb = %a" (Parts.pretty_bits ctx) ba (Parts.pretty_bits ctx) bb;*)
              let slice = or_bits ~size ctx ba bb in
              Parts.append ctx acc [slice]
            ) [] a.parts b.parts in
          { parts; complete }
        with Sig.Bottom -> binary_empty ~size ctx in
      (*Codex_log.feedback "result = %a" (binary_pretty ~size ctx) res;*)
      res

    let bor ~size ctx a b =
      let complete = SBF.bor ~size ctx a.complete b.complete in
      bor' complete ~size ctx a b
    ;;

    let and_bits ~size ctx a b = match a,b with
      | Parts.Zeroes _, _ -> of_bits ctx a
      | _, Parts.Zeroes _ -> of_bits ctx b
      | Parts.Ones _, _ -> of_bits ctx b
      | _, Parts.Ones _ -> of_bits ctx a
      | Parts.(Unknown pa, Unknown pb) ->
        Part.from_value ~size @@
        SBF.band ~size ctx (Part.do_extract ctx pa) (Part.do_extract ctx pb)

    let band ~size ctx a b =
      try let parts = Parts.fold2_known_bits ctx (fun ctx ~size acc ba bb ->
          let slice = and_bits ~size ctx ba bb in
          Parts.append ctx acc [slice]
        ) [] a.parts b.parts in
        { parts; complete = SBF.band ~size ctx a.complete b.complete }
      with Sig.Bottom -> binary_empty ~size ctx

    let xor_bits ~size ctx a b = match a,b with
      | Parts.Zeroes _, _ -> of_bits ctx b
      | _, Parts.Zeroes _ -> of_bits ctx a
      | Parts.Ones _, Parts.Ones _ ->
        Part.zero ctx ~size
      | Parts.(Unknown p, Ones _) | Parts.(Ones _, Unknown p) ->
        let pb = Part.ones ctx ~size in
        Part.from_value ~size @@
        SBF.bxor ~size ctx (Part.do_extract ctx p) (Part.do_extract ctx pb)
      | Parts.(Unknown pa, Unknown pb) ->
        Part.from_value ~size @@
        SBF.bxor ~size ctx (Part.do_extract ctx pa) (Part.do_extract ctx pb)

    let bxor ~size ctx a b =
      try let parts = Parts.fold2_known_bits ctx (fun ctx ~size acc ba bb ->
          let slice = xor_bits ~size ctx ba bb in
          Parts.append ctx acc [slice]
        ) [] a.parts b.parts in
        { parts; complete = SBF.bxor ~size ctx a.complete b.complete }
      with Sig.Bottom -> binary_empty ~size ctx

    let biadd ~size ~flags ctx a b =
      (* Codex_log.feedback "@[<v 2>biadd ~size:%d %a %a@]" size (binary_pretty ~size ctx) a (binary_pretty ~size ctx) b; *)
      (* If no face-to-face bits are simultaneously 1, then addition is an OR. *)
      let exception Exit in
      let orable = try Parts.fold2 ctx (fun ~size acc pa pb ->
          let za,oa = Sub.Query.(binary ~size ctx (Part.do_extract ctx pa) |> Binary_Lattice.to_known_bits ~size) in
          let zb,ob = Sub.Query.(binary ~size ctx (Part.do_extract ctx pb) |> Binary_Lattice.to_known_bits ~size) in
          if (Z.equal Z.zero @@ Z.(land) za zb) (* If simultaneously at 0 everywhere *)
          then true
          else raise Exit) true a.parts b.parts
        with Exit -> false
      in
      if orable then
        let complete = SBF.biadd ~size ~flags ctx a.complete b.complete in
        bor' complete ~size ctx a b
      else
        Binary.lift0 ~size @@ SBF.biadd ~size ~flags ctx a.complete b.complete

    let bshift ~size ~offset ~max ctx x =
      let offset = biconst ~size (Z.of_int offset) ctx in
      biadd ~size ~flags:(Operator.Flags.Biadd.pack ~nsw:false ~nuw:false ~nusw:false) ctx x offset
  end

  let binary_unknown ~size ctx = Binary.lift0 ~size @@ Sub.binary_unknown ~size ctx;;
  let binary_unknown_typed ~size ctx typ = Binary.lift0 ~size @@ Sub.binary_unknown_typed ~size ctx typ;;
  let boolean_unknown = Sub.boolean_unknown
  let enum_unknown = Sub.enum_unknown

  let union = Sub.union

  (**************** Serialization, fixpoind and nondet. ****************)

  (* The resulting computation: have we computed something, or should
     we juste take one of the arguments (or none). *)

  (* Higher-ranked polymorphism is required here, and we need a record for that. *)
  type 'elt higher = {subf: 'tl. Sub.Context.t -> 'elt -> Sub.Context.t -> 'elt -> 'tl
                          Sub.Context.in_acc -> ('elt,'tl) Sub.Context.result  } [@@unboxed]

  (* Note: OCaml infers the wrong type (no principal type), we have to help it here. *)
  let serialize (type elt) (type c)
      {subf} ctxa a ctxb b (included, (acc : c in_tuple)) : (elt,c) result =
    let Result (included, in_tup, deserialize) = subf ctxa a ctxb b (included, acc) in
    Result (included, in_tup, deserialize)

  let serialize_boolean ctxa a ctxb b acc = serialize {subf=Sub.serialize_boolean} ctxa a ctxb b acc

  let serialize_enum ctxa a ctxb b acc = serialize {subf=Sub.serialize_enum} ctxa a ctxb b acc

  (* For now we loose everything upon serialization. *)
  let serialize_binary ~widens ~size ctxa a ctxb b (included, acc) =
    let Result (included, in_tup, deserialize) = Sub.serialize_binary ~widens ~size ctxa a.complete ctxb b.complete (included, acc) in
    Result (included, in_tup, (fun ctx out_tup ->
        let res, out_tup = deserialize ctx out_tup in
        Binary.lift0 ~size res,out_tup))
  ;;


  (* Note: OCaml infers the wrong type (no principal type), we have to help it here. *)
  let typed_nondet2 (type c) ctxa ctxb (acc : c in_tuple) =
    Sub.typed_nondet2 ctxa ctxb acc

  let nondet_same_context = Sub.nondet_same_context

  (* Note: OCaml infers the wrong type (no principal type), we have to help it here. *)
  let typed_fixpoint_step (type c) ~iteration ~init ~arg ~body (included, (acc : c in_tuple)) : bool * (close:bool -> (c out_tuple * Context.t)) =
    let bool,continuef = Sub.typed_fixpoint_step ~iteration ~init ~arg ~body (included, acc) in
    bool,fun ~close -> continuef ~close

  let widened_fixpoint_step = Sub.widened_fixpoint_step

  (**************** Queries ****************)

  module Query = struct
    include Sub.Query

    let binary ~size ctx x =
      binary ~size ctx x.complete

  end
  let query_boolean = Sub.query_boolean


 (**************** Pretty printing ****************)


  (* let basis = Query.binary ~size ctx x in
   * Query.Binary_Lattice.pretty ~size pp basis;
   * if pretty_detailed then begin
   *   Format.pp_print_string pp "(= [";
   *   match Imap.to_list ~size ctx x with
   *   | [] -> ()
   *   | (size_fst, fst) :: tl ->
   *       pretty_bits ~size:size_fst ctx pp fst;
   *       List.iter (fun (size,bits) ->
   *         Format.fprintf pp ":%a" (pretty_bits ~size ctx) bits
   *       ) tl;
   *       Format.pp_print_string pp "]"; *)

  let boolean_pretty = Sub.boolean_pretty
  let enum_pretty = Sub.enum_pretty

  let binary_is_empty ~size ctx x = x.parts = []
  let integer_is_empty _ = assert false
  let boolean_is_empty _ = assert false

  let satisfiable = Sub.satisfiable

end