Source file coreIdent.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
(* ------------------------------------------------------------------------ *)
open Utils
open Wsize

module L = Location

module Name = struct
  type t = string
end

type uid = Uint63.t
let string_of_uid = Uint63.to_string

(* ------------------------------------------------------------------------ *)
type base_ty =
  | Bool
  | Int              (* Unbounded integer for pexpr *)
  | U   of wsize (* U(n): unsigned n-bit integer *)
  [@@deriving compare,sexp]

type 'len gty =
  | Bty of base_ty
  | Arr of wsize * 'len (* Arr(n,de): array of n-bit integers with dim. *)
           (* invariant only Const variable can be used in expression *)
           (* the type of the expression is [Int] *)


type 'len gety =
  | ETbool
  | ETint
  | ETword of signedness option * wsize
  | ETarr  of wsize * 'len (* Arr(n,de): array of n-bit integers with dim. *)
           (* invariant only Const variable can be used in expression *)
           (* the type of the expression is [Int] *)

let u8   = Bty (U U8)
let u16  = Bty (U U16)
let u32  = Bty (U U32)
let u64  = Bty (U U64)
let u128 = Bty (U U128)
let u256 = Bty (U U256)
let tu ws = Bty (U ws)
let tbool = Bty Bool
let tint  = Bty Int

let etw ws = ETword (None, ws)
let etwi s ws = ETword(Some s, ws)
let etbool = ETbool
let etint = ETint

let gty_of_gety (t: 'len gety) : 'len gty =
  match t with
  | ETbool -> tbool
  | ETint  -> tint
  | ETword(_, ws) -> tu ws
  | ETarr(ws, len) -> Arr(ws, len)

let gety_of_gty (t : 'len gty) : 'len gety =
  match t with
  | Arr(ws, len) -> ETarr(ws, len)
  | Bty t ->
    match t with
    | Bool -> etbool
    | Int  -> etint
    | U ws -> etw ws


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

type 'len gvar = {
  v_name : Name.t;
  v_id   : uid;
  v_kind : v_kind;
  v_ty   : 'len gty;
  v_dloc : L.t;   (* location where declared *)
  v_annot : Annotations.annotations;
}



(* ------------------------------------------------------------------------ *)
module GV = struct
  let mk v_name v_kind v_ty v_dloc v_annot =
    let v_id = Uint63.of_int (Uniq.gen ()) in
    { v_name; v_id; v_kind; v_ty; v_dloc; v_annot }

  let clone ?dloc v =
    mk v.v_name v.v_kind v.v_ty (Option.default v.v_dloc dloc) v.v_annot

  let compare v1 v2 = Uint63.compares v1.v_id v2.v_id

  let equal v1 v2 = Uint63.equal v1.v_id v2.v_id

  let hash v = Uint63.hash v.v_id

  let is_glob v = v.v_kind = Const

  let is_local v = not (is_glob v)
end

(* ------------------------------------------------------------------------ *)
(* Non parametrized variable                                                *)

type ty    = int gty
type var   = int gvar

module V = struct
  type t = var
  include GV
end

(* Cident *)

module Cident = struct
  type t = var

  let tag (x:t) = x.v_id

  let id_name (x: t) : Name.t = x.v_name
  let id_kind (x: t) : v_kind = x.v_kind

  let spill_to_mmx (x:t) =
    match Annot.ensure_uniq1 "spill_to_mmx" Annot.none x.v_annot with
    | Some () -> true
    | None    -> false

end

(* ------------------------------------------------------------------------ *)
(* Function name                                                            *)

type funname = {
  fn_name : Name.t;
  fn_id   : uid;
}

let funname_tag (f:funname) = f.fn_id

module F = struct
  let mk fn_name =
    { fn_name; fn_id = Uint63.of_int (Uniq.gen ()); }

  type t = funname

  let compare f1 f2 = Uint63.compares f1.fn_id f2.fn_id

  let equal f1 f2 = Uint63.equal f1.fn_id f2.fn_id

  let hash f = Uint63.hash f.fn_id
end

module Sf = Set.Make (F)
module Mf = Map.Make (F)
module Hf = Hash.Make(F)