package codex

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

Source file bottom.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
(**************************************************************************)
(*  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 Type = struct

  type 'a or_bottom = [ `Value of 'a | `Bottom ]

  (* This monad propagates the `Bottom value if needed. *)
  let (>>-) t f = match t with
    | `Bottom  -> `Bottom
    | `Value t -> f t

  (* Use this monad if the following function returns a simple value. *)
  let (>>-:) t f = match t with
    | `Bottom  -> `Bottom
    | `Value t -> `Value (f t)

end

include Type

let is_bottom = function
  | `Bottom -> true
  | `Value _ -> false

let non_bottom = function
  | `Value v -> v
  | `Bottom  -> assert false

let equal equal x y = match x, y with
  | `Bottom, `Bottom     -> true
  | `Value vx, `Value vy -> equal vx vy
  | _                    -> false

let is_included is_included x y = match x, y with
  | `Bottom, _           -> true
  | _, `Bottom           -> false
  | `Value vx, `Value vy -> is_included vx vy

let join join x y = match x, y with
  | `Value vx, `Value vy    -> `Value (join vx vy)
  | `Bottom, (`Value _ as v)
  | (`Value _ as v), `Bottom
  | (`Bottom as v), `Bottom -> v

let join_list j l = List.fold_left (join j) `Bottom l

let narrow narrow x y = match x, y with
  | `Value vx, `Value vy    -> narrow vx vy
  | `Bottom, `Value _
  | `Value _, `Bottom
  | `Bottom, `Bottom -> `Bottom

let pretty pretty fmt = function
  | `Bottom  -> Format.fprintf fmt "Bottom"
  | `Value v -> pretty fmt v


let counter = ref 0

module Make_Datatype
    (Domain: Datatype_sig.S)
  =
  (* Datatype.Make *) (
  struct
    (* include Datatype.Serializable_undefined *)
    type t = Domain.t or_bottom
    let () = incr counter
    (* let name = Domain.name ^ "+bottom(" ^ string_of_int !counter ^ ")" *)
    (* let reprs = [`Bottom; `Value (List.hd Domain.reprs)]
     * let structural_descr = Structural_descr.t_unknown *)
    (* Structural_descr.t_sum [| [| Domain.packed_descr |] |] *)

    let equal a b = match a, b with
      | `Bottom, `Bottom   -> true
      | `Value v, `Value w -> Domain.equal v w
      | _, _               -> false

    let compare a b = match a, b with
      | `Bottom, `Bottom   -> 0
      | `Bottom, _         -> -1
      | _, `Bottom         -> 1
      | `Value v, `Value w -> Domain.compare v w

    let hash = function
      | `Bottom  -> 0
      | `Value v -> Domain.hash v

    (* let rehash = Datatype.identity
     * 
     * let copy = function
     *   | `Bottom  -> `Bottom
     *   | `Value v -> `Value (Domain.copy v) *)
      
      let pretty fmt = function
        | `Bottom  -> Format.fprintf fmt "Bottom"
        | `Value v -> Domain.pretty fmt v
      
     (* let mem_project = Datatype.never_any_project *)
  end)


module Bound_Lattice
         (Lattice: sig
              include Datatype_sig.S
              val join: t -> t -> t
            end)
= struct
  include Make_Datatype (Lattice)

  let bottom = `Bottom
  let join = join Lattice.join
  (* let is_included = is_included Lattice.is_included *)
end

let to_list = function
  | `Bottom  -> []
  | `Value v -> [v]

let bot_of_list = function
  | [] -> `Bottom
  | l  -> `Value l

let list_of_bot = function
  | `Bottom  -> []
  | `Value l -> l

let add_to_list elt list = match elt with
  | `Bottom    -> list
  | `Value elt -> elt :: list

let all l =
  List.fold_left (fun l elt -> add_to_list elt l) [] l

module Top = struct

  type 'a or_top_bottom = [ 'a or_bottom | `Top ]

  let join vjoin x y = match x, y with
    | `Top, _ | _, `Top -> `Top
    | (#or_bottom as x), (#or_bottom as y) -> join vjoin x y

  let narrow vnarrow x y = match x, y with
    | `Top, v | v, `Top -> v
    | (#or_bottom as x), (#or_bottom as y) ->
      (narrow vnarrow x y :> _ or_top_bottom)

end