package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file Layout.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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         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 licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Pretty_utils
open Cil_datatype
open Cil_types

module Wp = Wp_parameters

module type Data =
sig
  type t
  val equal : t -> t -> bool
  val compare : t -> t -> int
  val pretty : t formatter
end

(* -------------------------------------------------------------------------- *)
(* --- Offsets                                                            --- *)
(* -------------------------------------------------------------------------- *)

type offset =
  | Field of fieldinfo
  | Index of typ * int

module Offset =
struct
  type t = offset
  let compare a b =
    if a == b then 0 else match a,b with
      | Field f, Field g -> Fieldinfo.compare f g
      | Field _ , _ -> (-1)
      | _ , Field _ -> 1
      | Index(ta,n) , Index(tb,m) ->
        let cmp = Typ.compare ta tb in
        if cmp <> 0 then cmp else Stdlib.compare n m

  let equal a b = (compare a b = 0)

  let pretty fmt = function
    | Field fd -> Format.fprintf fmt "{%s}.%a" fd.fcomp.cname Fieldinfo.pretty fd
    | Index(ty,n) -> Format.fprintf fmt "{%a}[%d]" Typ.pretty ty n

  let typeof = function
    | Field f -> f.ftype
    | Index(ty,_) -> ty

  let field fd = Field fd

  let index ty =
    match Cil.unrollType ty with
    | TArray(te,n,_) ->
      begin
        match Option.bind n Ctypes.get_int with
        | None -> failwith "Wp.Layout: unkown array size"
        | Some n -> Index(te,n)
      end
    | _ -> failwith "Wp.Layout: not an array-type"

  let rec typeof_chain ty = function [] -> ty | _::ds -> typeof_chain ty ds

  let rec pp_chain ty fmt = function
    | [] -> ()
    | d::ds ->
      let next =
        Format.pp_print_cut fmt () ;
        match d with
        | Index(t,n) when Typ.equal t ty ->
          Format.fprintf fmt "[%d]" n ; t
        | d -> Format.fprintf fmt "%a" pretty d ; typeof d
      in pp_chain next fmt ds

  module H = Compinfo.Hashtbl

  type cache = typ H.t
  let cache () : cache = H.create 0

  let typ_of_comp cache comp =
    try H.find cache comp with Not_found ->
      let typ = TComp(comp,[]) in
      H.add cache comp typ ; typ

  let field_offset _cache fd =
    Cil.fieldBitsOffset fd

  let range_field cache fd =
    let typ = typ_of_comp cache fd.fcomp in
    Cil.fieldBitsOffset fd, Cil.bitsSizeOf typ

  let range_index typ n =
    let len = Cil.bitsSizeOf typ * n in (0 , len) , len

  let range cache = function
    | Field fd -> range_field cache fd
    | Index(typ,n) -> range_index typ n

  let sizeof = function
    | Field fd -> Cil.bitsSizeOf fd.ftype
    | Index(ty,n) -> Cil.bitsSizeOf ty * n

  let container cache = function
    | Index(ty,n) -> Cil.bitsSizeOf ty * n
    | Field fd -> Cil.bitsSizeOf (typ_of_comp cache fd.fcomp)

end

(* -------------------------------------------------------------------------- *)
(* --- Deref                                                              --- *)
(* -------------------------------------------------------------------------- *)

type alias = NotUsed | NotAliased | Aliased
type usage = Value | Deref | Array
type deref = usage * typ

module Alias =
struct
  let use = function NotUsed | NotAliased -> NotAliased | Aliased -> Aliased
  let is_aliased = function NotUsed | NotAliased -> false | Aliased -> true
  let merge a b =
    match a,b with
    | Aliased,_ | _,Aliased -> Aliased
    | NotAliased,NotAliased -> NotAliased
    | NotUsed,c | c,NotUsed -> c
  let alias a b =
    match a,b with
    | NotUsed,c | c,NotUsed -> c
    | _ -> Aliased
  let to_string = function
    | NotUsed -> "not used"
    | NotAliased -> "not aliased"
    | Aliased -> "aliased"
  let pretty fmt a = Format.pp_print_string fmt (to_string a)
end

module Usage =
struct
  let pretty fmt = function
    | Value -> ()
    | Deref -> Format.pp_print_char fmt '*'
    | Array -> Format.pp_print_string fmt "[]"
  let order = function Value -> 0 | Deref -> 1 | Array -> 2
  let merge a b = if order a < order b then b else a
  let is_aliased = function Value -> false | Deref | Array -> true
  let is_shifted = function Value | Deref -> false | Array -> true
end

module Deref =
struct
  type t = deref

  let pretty fmt (usage,typ) =
    Format.fprintf fmt "{%a}" Typ.pretty typ ;
    Usage.pretty fmt usage

  let compare ((da,ta):t) ((db,tb):t) =
    let cmp = Stdlib.compare da db in
    if cmp <> 0 then cmp else Typ.compare ta tb

  let equal a b = (compare a b = 0)
end

(* -------------------------------------------------------------------------- *)
(* --- Access                                                             --- *)
(* -------------------------------------------------------------------------- *)

type lvalue =
  | Eval of exp
  | Tval of term
  | Assigned of stmt

module Lvalue =
struct

  type t = lvalue

  let order = function Eval _ -> 0 | Tval _ -> 1 | Assigned _ -> 2

  let compare a b = if a == b then 0 else match a,b with
      | Eval x , Eval y -> Exp.compare x y
      | Tval x , Tval y -> Term.compare x y
      | Assigned a , Assigned b -> Stmt.compare a b
      | _ -> order a - order b

  let equal a b = a == b || match a,b with
    | Eval x , Eval y -> Exp.equal x y
    | Tval x , Tval y -> Term.equal x y
    | Assigned a , Assigned b -> Stmt.equal a b
    | _ -> false

  let pretty fmt = function
    | Eval x -> Exp.pretty fmt x
    | Tval t -> Term.pretty fmt t
    | Assigned { skind = Instr(Set(lv,_,_)) }
    | Assigned { skind = Instr(Call(Some lv,_,_,_)) } -> Lval.pretty fmt lv
    | Assigned { skind = Instr(Local_init(x,_,_)) } -> Varinfo.pretty fmt x
    | Assigned stmt -> Format.fprintf fmt "stmt:s%d" stmt.sid

end


(* -------------------------------------------------------------------------- *)
(* --- Data Layout                                                        --- *)
(* -------------------------------------------------------------------------- *)

type 'a value =
  | Int of Ctypes.c_int
  | Float of Ctypes.c_float
  | Pointer of 'a

module Value =
struct

  let compare phi u v =
    if u == v then 0 else match u,v with
      | Int a , Int b -> Ctypes.compare_c_int a b
      | Int _ , _ -> (-1)
      | _ , Int _ -> 1
      | Float a , Float b -> Ctypes.compare_c_float a b
      | Float _ , _ -> (-1)
      | _ , Float _ -> 1
      | Pointer ra , Pointer rb -> phi ra rb

  let equal phi a b =
    match a,b with
    | Pointer ra , Pointer rb -> phi ra rb
    | Int a , Int b -> a = b
    | Float a , Float b -> a = b
    | _ -> false

  let pretty pp fmt = function
    | Int iota -> Ctypes.pp_int fmt iota
    | Float flt -> Ctypes.pp_float fmt flt
    | Pointer r -> Format.fprintf fmt "ptr(%a)" pp r

  let sizeof = function
    | Int iota -> Ctypes.i_bits iota
    | Float flt -> Ctypes.f_bits flt
    | Pointer _ -> Ctypes.p_bits ()

  let pointed = function
    | Int _ | Float _ -> None
    | Pointer r -> Some r

  let merge mu a b =
    match a,b with
    | Int i , Int j when i = j -> Some a
    | Float f , Float g when f = g -> Some a
    | Pointer r , Pointer r' -> Some(Pointer(mu r r'))
    | _ -> None

end

module Matrix =
struct

  let rec gcd a b = if b = 0 then a else gcd b (a mod b)

  let pretty fmt = function
    | [] -> ()
    | d::ds ->
      Format.fprintf fmt "@[<hov 1>[%d" d ;
      List.iter (fun d -> Format.fprintf fmt ",@,%d" d) ds ;
      Format.fprintf fmt "]@]"

  let rec sizeof n = function [] -> n | d::ds -> sizeof (n*d) ds

  let array ds n = if n = 1 then ds else ds @ [n]

  (* Assumes s divides len *)
  let join_array s len = let n = len / s in if n = 1 then [] else [n]

  (* Assumes s divides len , computes (s,ds) that fits exactly in len
     with ds maximal prefix of da and db *)
  let rec join s da db len =
    match da , db with
    | d::da , d'::db when d = d' ->
      let s' = s * d in
      if len mod s' = 0 then d :: join s' da db len else
        join_array s len
    | _ -> join_array s len

  let rec merge d1 d2 =
    match d1 , d2 with
    | n::d1 , n'::d2 when n=n' -> n :: merge d1 d2
    | _ -> []

end

(* -------------------------------------------------------------------------- *)
(* --- Range & Overlays                                                   --- *)
(* -------------------------------------------------------------------------- *)

let garbled_key = Wp.register_category "garbled"

type dim = Raw of int | Dim of int * int list

type 'a range = {
  ofs : int ; (* in bits, start from 0 *)
  len : int ;
  reg : 'a ;
  dim : dim ;
}

type 'a overlay = 'a range list

type 'a merger = raw:bool -> 'a -> 'a -> 'a

module Range =
struct

  let pp_dim fmt = function
    | Raw _ -> Format.pp_print_string fmt "raw"
    | Dim(s,ds) -> Format.fprintf fmt "{%d}%a" s Matrix.pretty ds

  let pretty pp fmt { ofs ; len ; reg ; dim } =
    Format.fprintf fmt "%d..%d: %a#%a" ofs (ofs+len-1) pp reg pp_dim dim

  let overlap (type a) (_ : a formatter) (mu : a merger) ra rb =
    let aligned = ref None in
    let ofs = min ra.ofs rb.ofs in
    let len = max (ra.ofs + ra.len) (rb.ofs + rb.len) - ofs in
    begin match ra.dim , rb.dim with
      | Dim(s,da) , Dim(s',db) when s = s' ->
        if len mod s = 0 then
          let ta = abs (ra.ofs - rb.ofs) in
          let tb = abs (ra.ofs + ra.len - rb.ofs - rb.len) in
          if ta mod s = 0 && tb mod s = 0 then
            let reg = mu ~raw:false ra.reg rb.reg in
            let ds = Matrix.join s da db len in
            let dim = Dim(s,ds) in
            aligned := Some { ofs ; len ; reg ; dim }
      | _ -> ()
    end ;
    match !aligned with
    | Some rg -> rg
    | None -> { ofs ; len ; reg = mu ~raw:true ra.reg rb.reg ; dim = Raw len }

  let shift ofs rg = { rg with ofs = rg.ofs + ofs }

  let flatten rg = match rg.dim with
    | Dim(s,ds) when ds <> [] ->
      let n = Matrix.sizeof 1 ds in
      { rg with dim = Dim(s,Matrix.array [] n) }
    | _ -> rg

  let included p n { ofs ; len } =
    ofs <= p && p + n <= ofs + len

end

module Overlay =
struct

  let pretty ?title pp fmt rs =
    begin
      Format.fprintf fmt "@[<hv 0>" ;
      Option.iter (fun pp -> pp fmt) title ;
      Format.fprintf fmt "@[<hov 2>{" ;
      List.iter
        (fun rg ->
           Format.fprintf fmt "@ @[<hov 2>%a@];" (Range.pretty pp) rg
        ) rs ;
      Format.fprintf fmt "@]@ }@]" ;
    end

  let rec merge (pp : 'a formatter) (mu : _ merger) ova ovb =
    match ova , ovb with
    | [],ovc | ovc,[] -> ovc
    | ra::wa , rb::wb ->
      let sa = ra.ofs + ra.len in
      let sb = rb.ofs + rb.len in
      if sa <= rb.ofs then ra :: merge pp mu wa ovb else
      if sb <= ra.ofs then rb :: merge pp mu ova wb else
      if sa < sb then
        merge pp mu wa (Range.overlap pp mu ra rb :: wb)
      else
        merge pp mu (Range.overlap pp mu ra rb :: wa) wb

  let rec pack eq = function
    | ({ dim = Dim(s ,da) } as ra ) ::
      ({ dim = Dim(s',db) } as rb ) ::
      ovl when eq ra.reg rb.reg && s = s' && ra.ofs + ra.len = rb.ofs ->
      let len = ra.len + rb.len in
      let ds = Matrix.join s da db len in
      pack eq ({ ofs = ra.ofs ; len ; reg = ra.reg ; dim = Dim(s,ds) } :: ovl)
    | rg :: ovl ->
      rg :: pack eq ovl
    | [] -> []

  let flatten ovl = List.map Range.flatten ovl

  let once reg overlay =
    match List.filter (fun rg -> rg.reg == reg) overlay with
    | [] | [_] -> true | _ -> false

end

(* -------------------------------------------------------------------------- *)
(* --- Layout                                                             --- *)
(* -------------------------------------------------------------------------- *)

type 'a layout = {
  sizeof : int ;
  layout : 'a overlay ;
}

module Compound =
struct

  let garbled cache offset reg =
    let (ofs,len),sizeof = Offset.range cache offset in
    { sizeof ; layout = [ { ofs ; len ; reg ; dim = Raw len } ] }

  let field cache fd reg dim =
    let (ofs,len),sizeof = Offset.range_field cache fd in
    { sizeof ; layout = [ { ofs ; len ; reg ; dim } ] }

  let index te n reg dim =
    let len = Cil.bitsSizeOf te * n in
    { sizeof = len ; layout = [ { ofs = 0 ; len ; reg ; dim } ] }

  let reshape ~eq ~flat ~pack { sizeof ; layout } =
    let ovl = if flat then Overlay.flatten layout else layout in
    let ovl = if pack then Overlay.pack eq ovl else ovl in
    { sizeof ; layout = ovl }

end

(* -------------------------------------------------------------------------- *)
(* --- Clustering                                                         --- *)
(* -------------------------------------------------------------------------- *)

type 'a cluster =
  | Empty
  | Garbled
  | Chunk of 'a value
  | Layout of 'a layout

module Cluster =
struct

  let is_empty = function Empty -> true | _ -> false
  let is_garbled = function Garbled -> true | _ -> false

  let pretty pp fmt = function
    | Empty -> Format.pp_print_string fmt "empty"
    | Garbled -> Format.pp_print_string fmt "garbled"
    | Chunk v -> Value.pretty pp fmt v
    | Layout { sizeof ; layout } ->
      Overlay.pretty
        ~title:(fun fmt -> Format.fprintf fmt "sizeof:%d" sizeof)
        pp fmt layout

  let deref ~pointed (_,typ) =
    match Cil.unrollType typ with
    | TInt(ti,_) | TEnum({ ekind = ti },_) -> Chunk (Int (Ctypes.c_int ti))
    | TFloat(tf,_) -> Chunk (Float (Ctypes.c_float tf))
    | TPtr _ | TFun _ -> Chunk(Pointer(Lazy.force pointed))
    | TVoid _ | TNamed _ | TComp _ | TArray _ | TBuiltin_va_list _ -> Empty

  let rec get_dim s rds typ =
    if s = Cil.bitsSizeOf typ then Some (List.rev rds) else
      match Cil.unrollType typ with
      | TArray( te , Some e , _ ) ->
        begin match Ctypes.get_int e with
          | None -> None
          | Some n -> get_dim s (if n = 1 then rds else n::rds) te
        end
      | _ -> None

  let shift_may cache pp offset reg ~inline cluster =
    match offset , cluster with
    | _ , Garbled -> None
    | _ , Empty ->
      let sizeof = Offset.container cache offset in
      Some { sizeof ; layout = [] }
    | Field fd , Chunk v ->
      begin
        let s = Value.sizeof v in
        match get_dim s [] fd.ftype with
        | None -> None
        | Some ds ->
          let dim = Dim(s,ds) in
          Some (Compound.field cache fd reg dim)
      end
    | Index(te,n) , Chunk v ->
      begin
        let s = Value.sizeof v in
        match get_dim s (Matrix.array [] n) te with
        | None -> None
        | Some ds ->
          let dim = Dim(s,ds) in
          Some (Compound.index te n reg dim)
      end
    | Field fd , Layout d ->
      let (ofs,len),sizeof = Offset.range_field cache fd in
      if d.sizeof = len then
        let layout =
          if inline then
            List.map (Range.shift ofs) d.layout
          else
            [ { ofs ; len ; reg ; dim=Dim(len,[]) } ]
        in Some { sizeof ; layout }
      else None
    | Index(te,n) , Layout {
        sizeof = s ;
        layout = [ { ofs=0 ; len ; reg ; dim = Dim(se,dse) } ]
      }
      when inline && s = len && Cil.bitsSizeOf te = len ->
      let dim = Dim(se,Matrix.array dse n) in
      Some (Compound.index te n reg dim)
    | Index(te,n) , Layout { sizeof } ->
      let size = Cil.bitsSizeOf te in
      if sizeof = size then
        let dim = Dim(size,Matrix.array [] n) in
        Some (Compound.index te n reg dim)
      else
        ( if Wp.has_dkey garbled_key then
            Wp.debug ~dkey:garbled_key
              "@[<hv 0>Garbled Offset:@ Index= {%a}[%d];@ Cluster= %a;@]"
              Cil_datatype.Typ.pretty te n (pretty pp) cluster ;
          None )

  let shift cache pp offset reg ~inline cluster =
    match shift_may cache pp offset reg ~inline cluster
    with Some ovl -> ovl
       | None -> Compound.garbled cache offset reg

  let do_merge pp (mu : 'a merger) (a : 'a cluster) (b : 'a cluster) =
    match a,b with
    | Empty , c | c , Empty -> c
    | Chunk va , Chunk vb ->
      begin match Value.merge (mu ~raw:false) va vb with
        | None -> Garbled
        | Some v -> Chunk v
      end
    | Layout { layout = [ { ofs=0 ; len=la ; reg=ra ; dim=Dim(s,da) } ] } ,
      Layout { layout = [ { ofs=0 ; len=lb ; reg=rb ; dim=Dim(s',db) } ] }
      when s = s' ->
      let reg = mu ~raw:false ra rb in
      let len = max la lb in
      let ds = Matrix.join s da db len in
      let layout = [ { ofs=0 ; len ; reg ; dim=Dim(s,ds) } ] in
      Layout { sizeof = len ; layout }
    | Layout { sizeof ; layout = la } ,
      Layout { sizeof = s ; layout = lb }
      when s = sizeof ->
      let layout = Overlay.merge pp mu la lb in
      Layout { sizeof ;  layout }
    | _ -> Garbled

  let merge pp mu a b =
    let result = do_merge pp mu a b in
    if result = Garbled && Wp.has_dkey garbled_key then
      Wp.debug ~dkey:garbled_key
        "@[<hv 0>Garbled Clusters:@ A=%a@ B=%a@]"
        (pretty pp) a (pretty pp) b ;
    result

  let reshape ~eq ~flat ~pack = function
    | Layout layout when flat || pack ->
      Layout (Compound.reshape ~eq ~flat ~pack layout)
    | cluster -> cluster

end

(* -------------------------------------------------------------------------- *)
(* --- Roots                                                              --- *)
(* -------------------------------------------------------------------------- *)

type 'a from =
  | Fvar of varinfo
  | Ffield of 'a * int
  | Findex of 'a
  | Fderef of 'a
  | Farray of 'a

type root =
  | Rnone
  | Rfield of varinfo * int (* static offset *)
  | Rindex of varinfo (* any offset rooted at var *)
  | Rtop

module Root =
struct

  let pretty fmt = function
    | Rtop -> Format.pp_print_string fmt "*"
    | Rnone -> Format.pp_print_string fmt "-"
    | Rfield(x,0) -> Format.fprintf fmt "&%a" Varinfo.pretty x
    | Rfield(x,ofs) -> Format.fprintf fmt "&%a+%d" Varinfo.pretty x ofs
    | Rindex(x) -> Format.fprintf fmt "&%a+(..)" Varinfo.pretty x

  let field ofs = function
    | Rfield(x,p) -> Rfield(x,p+ofs)
    | (Rindex _ | Rnone | Rtop) as r -> r

  let index = function
    | Rfield(x,_) -> Rindex x
    | (Rindex _ | Rnone | Rtop) as r -> r

  let from ~root = function
    | Fvar x -> Rfield(x,0)
    | Ffield(r,ofs) -> field ofs (root r)
    | Findex r -> index (root r)
    | Fderef r -> root r
    | Farray _ -> Rtop

  let merge_var a b = match a,b with
    | (Rfield(x,_) | Rindex x) ,
      (Rfield(y,_) | Rindex y)
      when Varinfo.equal x y -> Some x
    | _ -> None

  let merge_field x a b = match a,b with
    | Rfield(_,p) , Rfield(_,q) when p = q -> a
    | _ -> Rindex x

  let merge a b =
    if a == b then a else
      match a,b with
      | Rnone,s | s,Rnone -> s
      | Rtop,_ | _,Rtop -> Rtop
      | _ ->
        match merge_var a b with
        | Some x -> merge_field x a b
        | None -> Rtop

  let indexed = function
    | Rnone | Rfield _ -> false
    | Rindex _ | Rtop -> true

  let framed = function
    | Rfield(x,_) | Rindex x -> not x.vglob && not x.vaddrof (* Cf. MemVar *)
    | Rnone -> true
    | Rtop -> false

end

(* -------------------------------------------------------------------------- *)
(* --- Chunks                                                             --- *)
(* -------------------------------------------------------------------------- *)

module R = Qed.Intset

type chunks = R.t

type 'a chunk =
  | Mref of 'a
  | Mmem of root * 'a value
  | Mraw of root * 'a option
  | Mcomp of chunks * 'a overlay

module Chunk =
struct
  let mem = R.mem
  let empty = R.empty
  let singleton = R.singleton
  let union = R.union
  let union_map f es = List.fold_left (fun w e -> R.union w @@ f e) R.empty es
  let disjoint a b = not (R.intersect a b)
  let pretty pp fmt es =
    begin
      Format.fprintf fmt "@[<hov 2>{" ;
      R.iter (fun e -> Format.fprintf fmt "@ %a" pp e) es ;
      Format.fprintf fmt " }@]" ;
    end
end

(* -------------------------------------------------------------------------- *)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct