2 * 2005 Matthew
Fluet (mfluet@acm
.org
)
7 * The implementation
of the interface that encodes C
's
type system
8 * in ML
. This implementation includes its
"private" extensions
.
10 * (C
) 2001, Lucent Technologies
, Bell Laboratories
12 * author
: Matthias
Blume (blume@research
.bell
-labs
.com
)
15 (* We play some games here
with first calling C_Int simply C
and then
16 * renaming it because they result
in saner printing behavior
. *)
17 structure C
:> C_INT
= struct
19 exception OutOfMemory
= CMemory
.OutOfMemory
21 fun bug m
= raise Fail ("impossible: " ^ m
)
23 type addr
= CMemory
.addr
24 val null
= CMemory
.null
31 | ARR
of { typ
: 'f objt
, n
: word, esz
: word, asz
: word }
33 (* Bitfield
: b bits wide
, l bits from left corner
, r bits from right
.
34 * The
word itself is CMemory
.int_bits wide
and located at address a
.
38 * |
<---l
---> ......... <---r
--->|
39 * |
<----------wordsize
--------->|
41 * 0.......0 1.......1 0.......0 = m
42 * 1.......1 0.......0 1.......1 = im
45 type cword
= MLRep
.Int.Unsigned
.word
46 type bf
= { a
: addr
, l
: word, r
: word, lr
: word, m
: cword
, im
: cword
}
49 fun pair_type_addr (t
: 'f objt
) (a
: addr
) = (a
, t
)
51 fun strip_type (a
: addr
, _
: 'f objt
) = a
52 fun p_strip_type (a
: addr
, _
: 'f objt
) = a
53 fun strip_fun (a
: addr
, _
: 'f
) = a
54 fun addr_type_id (x
: addr
* 'f objt
) = x
55 fun addr_id (x
: addr
) = x
58 val op -- = CMemory
.--
59 val op ++ = CMemory
.++
61 infix << >> ~
>> && || ^^
62 val op << = MLRep
.Int.Unsigned
.<<
63 val op >> = MLRep
.Int.Unsigned
.>>
64 val op ~
>> = MLRep
.Int.Unsigned
.~
>>
65 val op && = MLRep
.Int.Unsigned
.andb
66 val op ||
= MLRep
.Int.Unsigned
.orb
68 val op ^^
= MLRep
.Int.Unsigned
.xorb
70 val ~~
= MLRep
.Int.Unsigned
.notb
73 type ('t
, 'c
) obj
= addr
* 't
objt (* RTTI for stored value
*)
74 type ('t
, 'c
) obj
' = addr
78 type 'o ptr
= addr
* 'o objt (* RTTI for target value
*)
81 type ('t
, 'n
) arr
= 't
83 type 'f fptr
= addr
* 'f
87 type voidptr
= void ptr
'
91 type 'tag enum
= MLRep
.Int.Signed
.int
93 type schar
= MLRep
.Char.Signed
.int
94 type uchar
= MLRep
.Char.Unsigned
.word
95 type sshort
= MLRep
.Short
.Signed
.int
96 type ushort
= MLRep
.Short
.Unsigned
.word
97 type sint
= MLRep
.Int.Signed
.int
98 type uint
= MLRep
.Int.Unsigned
.word
99 type slong
= MLRep
.Long
.Signed
.int
100 type ulong
= MLRep
.Long
.Unsigned
.word
101 type slonglong
= MLRep
.LongLong
.Signed
.int
102 type ulonglong
= MLRep
.LongLong
.Unsigned
.word
103 type float
= MLRep
.Float
.real
104 type double
= MLRep
.Double
.real
106 type 'c schar_obj
= ( schar
, 'c
) obj
107 type 'c uchar_obj
= ( uchar
, 'c
) obj
108 type 'c sshort_obj
= ( sshort
, 'c
) obj
109 type 'c ushort_obj
= ( ushort
, 'c
) obj
110 type 'c sint_obj
= ( sint
, 'c
) obj
111 type 'c uint_obj
= ( uint
, 'c
) obj
112 type 'c slong_obj
= ( slong
, 'c
) obj
113 type 'c ulong_obj
= ( ulong
, 'c
) obj
114 type 'c slonglong_obj
= (slonglong
, 'c
) obj
115 type 'c ulonglong_obj
= (ulonglong
, 'c
) obj
116 type 'c float_obj
= ( float
, 'c
) obj
117 type 'c double_obj
= ( double
, 'c
) obj
118 type 'c voidptr_obj
= ( voidptr
, 'c
) obj
119 type ('e
, 'c
) enum_obj
= ( 'e enum
, 'c
) obj
120 type ('f
, 'c
) fptr_obj
= ( 'f fptr
, 'c
) obj
121 type ('s
, 'c
) su_obj
= ( 's su
, 'c
) obj
123 type 'c schar_obj
' = ( schar
, 'c
) obj
'
124 type 'c uchar_obj
' = ( uchar
, 'c
) obj
'
125 type 'c sshort_obj
' = ( sshort
, 'c
) obj
'
126 type 'c ushort_obj
' = ( ushort
, 'c
) obj
'
127 type 'c sint_obj
' = ( sint
, 'c
) obj
'
128 type 'c uint_obj
' = ( uint
, 'c
) obj
'
129 type 'c slong_obj
' = ( slong
, 'c
) obj
'
130 type 'c ulong_obj
' = ( ulong
, 'c
) obj
'
131 type 'c slonglong_obj
' = (slonglong
, 'c
) obj
'
132 type 'c ulonglong_obj
' = (ulonglong
, 'c
) obj
'
133 type 'c float_obj
' = ( float
, 'c
) obj
'
134 type 'c double_obj
' = ( double
, 'c
) obj
'
135 type 'c voidptr_obj
' = ( voidptr
, 'c
) obj
'
136 type ('e
, 'c
) enum_obj
' = ( 'e enum
, 'c
) obj
'
137 type ('f
, 'c
) fptr_obj
' = ( 'f fptr
, 'c
) obj
'
138 type ('s
, 'c
) su_obj
' = ( 's su
, 'c
) obj
'
144 type ('from
, 'to
) witness
= 'from
-> 'to
146 fun convert (w
: 's
-> 't
) (x
: 's objt
) : 't objt
=
150 | FPTR f
=> FPTR (fn a
=> w (f a
))
151 | ARR
{typ
, n
, esz
, asz
} =>
152 ARR
{typ
= convert w typ
,
153 n
= n
, esz
= esz
, asz
= asz
}
155 val trivial
: ('t
, 't
) witness
=
158 val pointer
: ('from
, 'to
) witness
-> ('from ptr
, 'to ptr
) witness
=
159 fn w
=> fn (a
, t
) => (a
, convert w t
)
160 val object
: ('from
, 'to
) witness
-> (('from
, 'c
) obj
, ('to
, 'c
) obj
) witness
=
161 fn w
=> fn (a
, t
) => (a
, convert w t
)
162 val arr
: ('from
, 'to
) witness
-> (('from
, 'n
) arr
, ('to
, 'n
) arr
) witness
=
164 val ro
: ('from
, 'to
) witness
-> (('from
, 'fc
) obj
, ('to
, ro
) obj
) witness
=
165 fn w
=> fn (a
, t
) => (a
, convert w t
)
166 val rw
: ('from
, 'to
) witness
-> (('from
, 'fc
) obj
, ('to
, 'tc
) obj
) witness
=
167 fn w
=> fn (a
, t
) => (a
, convert w t
)
170 val convert
: (('st
, 'sc
) obj
, ('tt
, 'tc
) obj
) W
.witness
->
171 ('st
, 'sc
) obj
-> ('tt
, 'tc
) obj
=
173 val convert
' : (('st
, 'sc
) obj
, ('tt
, 'tc
) obj
) W
.witness
->
174 ('st
, 'sc
) obj
' -> ('tt
, 'tc
) obj
' =
178 * A family
of types
and corresponding values representing natural numbers
.
179 * (An encoding
in SML without using dependent types
.)
180 * This is the full implementation including an unsafe extension
183 structure Dim
= struct
185 type ('a
, 'z
) dim0
= int
204 type 'a dim
= ('a
, nonzero
) dim0
207 fun dg n d
= 10 * d
+ n
210 val (dg0
', dg1
', dg2
', dg3
', dg4
', dg5
', dg6
', dg7
', dg8
', dg9
') =
211 (dg
0, dg
1, dg
2, dg
3, dg
4, dg
5, dg
6, dg
7, dg
8, dg
9)
214 fun dg0 d k
= k (dg0
' d
)
215 fun dg1 d k
= k (dg1
' d
)
216 fun dg2 d k
= k (dg2
' d
)
217 fun dg3 d k
= k (dg3
' d
)
218 fun dg4 d k
= k (dg4
' d
)
219 fun dg5 d k
= k (dg5
' d
)
220 fun dg6 d k
= k (dg6
' d
)
221 fun dg7 d k
= k (dg7
' d
)
222 fun dg8 d k
= k (dg8
' d
)
223 fun dg9 d k
= k (dg9
' d
)
232 fun toWord (s
: 't size
) = s
234 val schar
= CMemory
.char_size
235 val uchar
= CMemory
.char_size
236 val sint
= CMemory
.int_size
237 val uint
= CMemory
.int_size
238 val sshort
= CMemory
.short_size
239 val ushort
= CMemory
.short_size
240 val slong
= CMemory
.long_size
241 val ulong
= CMemory
.long_size
242 val slonglong
= CMemory
.longlong_size
243 val ulonglong
= CMemory
.longlong_size
244 val float
= CMemory
.float_size
245 val double
= CMemory
.double_size
247 val voidptr
= CMemory
.addr_size
248 val ptr
= CMemory
.addr_size
249 val fptr
= CMemory
.addr_size
250 val enum
= CMemory
.int_size
255 type 't typ
= 't objt
257 val typeof
: ('t
, 'c
) obj
-> 't typ
=
260 val sizeof
: 't typ
-> 't S
.size
=
266 (* use
private (and unsafe
) extension to Dim module here
... *)
267 val dim
: ('t
, 'n
) arr typ
-> 'n Dim
.dim
=
268 fn ARR
{ n
, ... } => Dim
.fromInt (Word.toInt n
)
269 | _
=> bug
"T.dim (non-array type)"
271 val pointer
: 't typ
-> ('t
, rw
) obj ptr typ
=
272 fn t
=> PTR (null
, PTR (null
, t
))
273 val target
: ('t
, 'c
) obj ptr typ
-> 't typ
=
274 fn PTR (_
, PTR (_
, t
)) => t
275 | _
=> bug
"T.target (non-pointer type)"
276 val arr
: 't typ
* 'n Dim
.dim
-> ('t
, 'n
) arr typ
=
279 val n
= Word.fromInt (Dim
.toInt d
)
282 ARR
{ typ
= t
, n
= n
, esz
= s
, asz
= n
* s
}
284 val elem
: ('t
, 'n
) arr typ
-> 't typ
=
286 | _
=> bug
"T.elem (non-array type)"
287 val ro
: ('t
, 'c
) obj ptr typ
-> ('t
, ro
) obj ptr typ
=
290 val schar
: schar typ
= BASE S
.schar
291 val uchar
: uchar typ
= BASE S
.uchar
292 val sshort
: sshort typ
= BASE S
.sshort
293 val ushort
: ushort typ
= BASE S
.ushort
294 val sint
: sint typ
= BASE S
.sint
295 val uint
: uint typ
= BASE S
.uint
296 val slong
: slong typ
= BASE S
.slong
297 val ulong
: ulong typ
= BASE S
.ulong
298 val slonglong
: slonglong typ
= BASE S
.slonglong
299 val ulonglong
: ulonglong typ
= BASE S
.ulonglong
300 val float
: float typ
= BASE S
.float
301 val double
: double typ
= BASE S
.double
303 val voidptr
: voidptr typ
= BASE S
.voidptr
305 val enum
: 'tag enum typ
= BASE S
.sint
308 structure Light
= struct
309 val obj
: ('t
, 'c
) obj
-> ('t
, 'c
) obj
' =
311 val ptr
: 'o ptr
-> 'o ptr
' =
313 val fptr
: 'f fptr
-> 'f fptr
' =
317 structure Heavy
= struct
318 val obj
: 't T
.typ
-> ('t
, 'c
) obj
' -> ('t
, 'c
) obj
=
319 fn t
=> fn a
=> (a
, t
)
320 val ptr
: 'o ptr T
.typ
-> 'o ptr
' -> 'o ptr
=
321 fn PTR (_
, t
) => (fn a
=> (a
, t
))
322 | _
=> bug
"Heavy.ptr (non-object-pointer-type)"
323 val fptr
: 'f fptr T
.typ
-> 'f fptr
' -> 'f fptr
=
324 fn (FPTR mkf
) => (fn a
=> (a
, #
2 (mkf a
)))
325 | _
=> bug
"Heavy.fptr (non-function-pointer-type)"
328 val sizeof
: ('t
, 'c
) obj
-> 't S
.size
=
329 fn (_
, t
) => T
.sizeof t
331 structure Cvt
= struct
332 (* going between abstract
and concrete
; these are all identities
*)
333 fun c_schar (c
: schar
) = c
334 fun c_uchar (c
: uchar
) = c
335 fun c_sshort (s
: sshort
) = s
336 fun c_ushort (s
: ushort
) = s
337 fun c_sint (i
: sint
) = i
338 fun c_uint (i
: uint
) = i
339 fun c_slong (l
: slong
) = l
340 fun c_ulong (l
: ulong
) = l
341 fun c_slonglong (ll
: slonglong
) = ll
342 fun c_ulonglong (ll
: ulonglong
) = ll
343 fun c_float (f
: float
) = f
344 fun c_double (d
: double
) = d
345 fun i2c_enum (e
: 'e enum
) = e
347 val ml_schar
= c_schar
348 val ml_uchar
= c_uchar
349 val ml_sshort
= c_sshort
350 val ml_ushort
= c_ushort
353 val ml_slong
= c_slong
354 val ml_ulong
= c_ulong
355 val ml_slonglong
= c_slonglong
356 val ml_ulonglong
= c_ulonglong
357 val ml_float
= c_float
358 val ml_double
= c_double
359 val c2i_enum
= i2c_enum
362 structure Get
= struct
363 val uchar
' = CMemory
.load_uchar
364 val schar
' = CMemory
.load_schar
365 val uint
' = CMemory
.load_uint
366 val sint
' = CMemory
.load_sint
367 val ushort
' = CMemory
.load_ushort
368 val sshort
' = CMemory
.load_sshort
369 val ulong
' = CMemory
.load_ulong
370 val slong
' = CMemory
.load_slong
371 val ulonglong
' = CMemory
.load_ulonglong
372 val slonglong
' = CMemory
.load_slonglong
373 val float
' = CMemory
.load_float
374 val double
' = CMemory
.load_double
375 val enum
' = CMemory
.load_sint
377 val ptr
' = CMemory
.load_addr
378 val fptr
' = CMemory
.load_addr
379 val voidptr
' = CMemory
.load_addr
381 val uchar
= uchar
' o strip_type
382 val schar
= schar
' o strip_type
383 val uint
= uint
' o strip_type
384 val sint
= sint
' o strip_type
385 val ushort
= ushort
' o strip_type
386 val sshort
= sshort
' o strip_type
387 val ulong
= ulong
' o strip_type
388 val slong
= slong
' o strip_type
389 val ulonglong
= ulonglong
' o strip_type
390 val slonglong
= slonglong
' o strip_type
391 val float
= float
' o strip_type
392 val double
= double
' o strip_type
393 val voidptr
= voidptr
' o strip_type
394 val enum
= enum
' o strip_type
396 val ptr
: ('o ptr
, 'c
) obj
-> 'o ptr
=
397 fn (a
, PTR (_
, t
)) => (ptr
' a
, t
)
398 | _
=> bug
"Get.ptr (non-pointer)"
399 val fptr
: ('f
, 'c
) fptr_obj
-> 'f fptr
=
400 fn (a
, FPTR mkf
) => let val fa
= fptr
' a
in (fa
, #
2 (mkf fa
)) end
401 | _
=> bug
"Get.fptr (non-function-pointer)"
404 val u2s
= MLRep
.Int.Signed
.fromLarge
o MLRep
.Int.Unsigned
.toLargeIntX
406 fun ubf ({ a
, l
, r
=_
, lr
, m
=_
, im
=_
} : bf
) =
407 (CMemory
.load_uint a
<< l
) >> lr
408 fun sbf ({ a
, l
, r
=_
, lr
, m
=_
, im
=_
} : bf
) =
409 u2s ((CMemory
.load_uint a
<< l
) ~
>> lr
)
413 structure Set
= struct
414 val uchar
' = CMemory
.store_uchar
415 val schar
' = CMemory
.store_schar
416 val uint
' = CMemory
.store_uint
417 val sint
' = CMemory
.store_sint
418 val ushort
' = CMemory
.store_ushort
419 val sshort
' = CMemory
.store_sshort
420 val ulong
' = CMemory
.store_ulong
421 val slong
' = CMemory
.store_slong
422 val ulonglong
' = CMemory
.store_ulonglong
423 val slonglong
' = CMemory
.store_slonglong
424 val float
' = CMemory
.store_float
425 val double
' = CMemory
.store_double
426 val enum
' = CMemory
.store_sint
428 val ptr
' = CMemory
.store_addr
429 val fptr
' = CMemory
.store_addr
430 val voidptr
' = CMemory
.store_addr
432 val ptr_voidptr
' = CMemory
.store_addr
436 fun (f $ g
) (x
, y
) = f (g x
, y
)
438 val uchar
= uchar
' $ strip_type
439 val schar
= schar
' $ strip_type
440 val uint
= uint
' $ strip_type
441 val sint
= sint
' $ strip_type
442 val ushort
= ushort
' $ strip_type
443 val sshort
= sshort
' $ strip_type
444 val ulong
= ulong
' $ strip_type
445 val slong
= slong
' $ strip_type
446 val ulonglong
= ulonglong
' $ strip_type
447 val slonglong
= slonglong
' $ strip_type
448 val float
= float
' $ strip_type
449 val double
= double
' $ strip_type
450 val enum
= enum
' $ strip_type
452 val ptr
: ('o ptr
, rw
) obj
* 'o ptr
-> unit
=
453 fn (x
, p
) => ptr
' (p_strip_type x
, p_strip_type p
)
454 val voidptr
= voidptr
' $ strip_type
455 val fptr
: ('f
, rw
) fptr_obj
* 'f fptr
-> unit
=
456 fn (x
, f
) => fptr
' (p_strip_type x
, strip_fun f
)
458 val ptr_voidptr
: ('o ptr
, rw
) obj
* voidptr
-> unit
=
459 fn (x
, p
) => ptr_voidptr
' (p_strip_type x
, p
)
462 fun ubf ({ a
, l
=_
, r
, lr
=_
, m
, im
}, x
) =
463 CMemory
.store_uint (a
, (CMemory
.load_uint a
&& im
) ||
467 val s2u
= MLRep
.Int.Unsigned
.fromLargeInt
o MLRep
.Int.Signed
.toLarge
469 fun sbf (f
, x
) = ubf (f
, s2u x
)
473 fun copy
' bytes
{ from
, to
} =
474 CMemory
.bcopy
{ from
= from
, to
= to
, bytes
= bytes
}
475 fun copy
{ from
= (from
, t
), to
= (to
, _
: 'f objt
) } =
476 copy
' (T
.sizeof t
) { from
= from
, to
= to
}
478 val ro
= addr_type_id
479 val rw
= addr_type_id
484 structure Ptr
= struct
485 val |
&|
: ('t
, 'c
) obj
-> ('t
, 'c
) obj ptr
=
486 fn (a
, t
) => (a
, PTR (null
, t
))
487 val |
*|
: ('t
, 'c
) obj ptr
-> ('t
, 'c
) obj
=
488 fn (a
, PTR (_
, t
)) => (a
, t
)
489 | _
=> bug
"Ptr.* (non-pointer)"
491 val |
&! : ('t
, 'c
) obj
' -> ('t
, 'c
) obj ptr
' =
493 val |
*! : ('t
, 'c
) obj ptr
' -> ('t
, 'c
) obj
' =
496 fun compare (p
, p
') = CMemory
.compare (p_strip_type p
, p_strip_type p
')
498 val compare
' = CMemory
.compare
500 val inject
' = addr_id
503 val inject
: 'o ptr
-> voidptr
= p_strip_type
504 val cast
: 'o ptr T
.typ
-> voidptr
-> 'o ptr
=
505 fn PTR (_
, t
) => (fn p
=> (p
, t
))
506 | _
=> bug
"Ptr.cast (non-pointer-type)"
508 val vnull
: voidptr
= CMemory
.null
509 val null
: 'o ptr T
.typ
-> 'o ptr
=
511 val null
' : 'o ptr
' = vnull
513 val fnull
' : 'f ptr
' = CMemory
.null
514 val fnull
: 'f fptr T
.typ
-> 'f fptr
=
515 fn t
=> Heavy
.fptr t fnull
'
517 val isVNull
: voidptr
-> bool = CMemory
.isNull
518 val isNull
: 'o ptr
-> bool =
519 fn p
=> isVNull (inject p
)
520 val isNull
' = CMemory
.isNull
522 val isFNull
: 'f fptr
-> bool =
523 fn (a
,_
) => CMemory
.isNull a
524 val isFNull
' = CMemory
.isNull
526 fun |
+! s (p
, i
) = p
++ (Word.toInt s
* i
)
527 fun |
-! s (p
, p
') = (p
-- p
') div Word.toInt s
529 val |
+|
: ('t
, 'c
) obj ptr
* int -> ('t
, 'c
) obj ptr
=
530 fn ((p
, t
as PTR (_
, t
')), i
) => (|
+! (T
.sizeof t
') (p
, i
), t
)
531 | _
=> bug
"Ptr.|+| (non-pointer-type)"
532 val |
-|
: ('t
, 'c
) obj ptr
* ('t
, 'c
) obj ptr
-> int =
533 fn ((p
, PTR (_
, t
')), (p
', _
)) => |
-! (T
.sizeof t
') (p
, p
')
534 | _
=> bug
"Ptr.|-| (non-pointer-type"
536 val sub
: ('t
, 'c
) obj ptr
* int -> ('t
, 'c
) obj
=
537 fn (p
, i
) => |
*|
(|
+|
(p
, i
))
539 fun sub
' t (p
, i
) = |
*! (|
+! t (p
, i
))
541 val convert
: (('st
, 'sc
) obj ptr
, ('tt
, 'tc
) obj ptr
) W
.witness
->
542 ('st
, 'sc
) obj ptr
-> ('tt
, 'tc
) obj ptr
=
544 val convert
' : (('st
, 'sc
) obj ptr
, ('tt
, 'tc
) obj ptr
) W
.witness
->
545 ('st
, 'sc
) obj ptr
' -> ('tt
, 'tc
) obj ptr
' =
548 val ro
: ('t
, 'c
) obj ptr
-> ('t
, ro
) obj ptr
=
549 fn x
=> convert (W
.pointer (W
.ro W
.trivial
)) x
550 val rw
: ('t
, 'sc
) obj ptr
-> ('t
, 'tc
) obj ptr
=
551 fn x
=> convert (W
.pointer (W
.rw W
.trivial
)) x
553 val ro
' : ('t
, 'c
) obj ptr
' -> ('t
, ro
) obj ptr
' =
555 val rw
' : ('t
, 'sc
) obj ptr
' -> ('t
, 'tc
) obj ptr
' =
559 structure Arr
= struct
561 fun asub (a
, i
, n
, esz
) =
562 (* take advantage
of wrap
-around to avoid the
>= 0 test
... *)
563 if Word.fromInt i
< n
then a
++ (Word.toIntX esz
* i
)
564 else raise General
.Subscript
566 val sub
: (('t
, 'n
) arr
, 'c
) obj
* int -> ('t
, 'c
) obj
=
567 fn ((a
, ARR
{ typ
, n
, esz
, ... }), i
) => (asub (a
, i
, n
, esz
), typ
)
568 | _
=> bug
"Arr.sub (non-array)"
569 val sub
' : 't S
.size
* 'n Dim
.dim
->
570 (('t
, 'n
) arr
, 'c
) obj
' * int -> ('t
, 'c
) obj
' =
571 fn (s
, d
) => fn (a
, i
) => asub (a
, i
, Word.fromInt (Dim
.toInt d
), s
)
574 val decay
: (('t
, 'n
) arr
, 'c
) obj
-> ('t
, 'c
) obj ptr
=
575 fn (a
, ARR
{ typ
, ... }) => (a
, PTR (null
, typ
))
576 | _
=> bug
"Arr.decay (non-array)"
580 val reconstruct
: ('t
, 'c
) obj ptr
* 'n Dim
.dim
-> (('t
, 'n
) arr
, 'c
) obj
=
581 fn ((a
, PTR (_
, t
)), d
) => (a
, T
.arr (t
, d
))
582 | _
=> bug
"Arr.reconstruct (non-pointer)"
584 fun reconstruct
' (a
: addr
, _
: 'n Dim
.dim
) = a
586 fun dim (_
: addr
, t
) = T
.dim t
589 fun new
' s
= CMemory
.alloc s
590 val new
: 't T
.typ
-> ('t
, 'c
) obj
=
591 fn t
=> (new
' (T
.sizeof t
), t
)
593 val discard
' = CMemory
.free
594 val discard
: ('t
, 'c
) obj
-> unit
=
595 fn x
=> discard
' (p_strip_type x
)
597 fun alloc
' s i
= CMemory
.alloc (s
* i
)
598 val alloc
: 't T
.typ
-> word -> ('t
, 'c
) obj ptr
=
599 fn t
=> fn i
=> (alloc
' (T
.sizeof t
) i
, PTR (null
, t
))
601 val free
' = CMemory
.free
602 val free
: 'o ptr
-> unit
=
603 fn x
=> free
' (p_strip_type x
)
605 val call
: ('a
-> 'b
) fptr
* 'a
-> 'b
=
606 fn ((_
, f
), x
) => f x
608 val call
' : ('a
-> 'b
) fptr T
.typ
-> ('a
-> 'b
) fptr
' * 'a
-> 'b
=
609 fn (FPTR mkf
) => (fn (a
, x
) => (#
2 (mkf a
)) x
)
610 | _
=> bug
"call' (non-function-pointer-type)"
613 fun fcast (f
: 'fa fptr
') : 'fb fptr
' = f
614 fun p2i (a
: 'o ptr
') : ulong
= CMemory
.p2i a
615 fun i2p (a
: ulong
) : 'o ptr
' = CMemory
.i2p a
618 (* ------------- internal stuff
------------- *)
620 fun mk_obj
' (a
: addr
) = a
621 val mk_voidptr
: addr
-> voidptr
= fn a
=> a
624 fun mk_field (t
: 'f objt
, i
, (a
, _
)) = (a
++ i
, t
)
626 val mk_rw_field
: 'm T
.typ
* int * ('s
, 'c
) su_obj
-> ('m
, 'c
) obj
= mk_field
627 val mk_ro_field
: 'm T
.typ
* int * ('s
, 'c
) su_obj
-> ('m
, ro
) obj
= mk_field
628 fun mk_field
' (i
, a
) = a
++ i
632 fun mk_bf
' (offset
, bits
, shift
) a
= let
635 val lr
= CMemory
.int_bits
- bits
637 val m
= (~~
0w0
<< lr
) >> l
640 { a
= a
, l
= l
, r
= r
, lr
= lr
, m
= m
, im
= im
} : bf
642 fun mk_bf
acc (a
, _
) = mk_bf
' acc a
644 val mk_rw_ubf
= mk_bf
645 val mk_ro_ubf
= mk_bf
646 val mk_rw_ubf
' = mk_bf
'
647 val mk_ro_ubf
' = mk_bf
'
649 val mk_rw_sbf
= mk_bf
650 val mk_ro_sbf
= mk_bf
651 val mk_rw_sbf
' = mk_bf
'
652 val mk_ro_sbf
' = mk_bf
'
655 val mk_su_size
: word -> 's S
.size
=
657 val mk_su_typ
: 's su S
.size
-> 's su T
.typ
=
659 val mk_fptr
: (addr
-> 'a
-> 'b
) * addr
-> ('a
-> 'b
) fptr
=
660 fn (mkf
, a
) => (a
, mkf a
)
661 val mk_fptr_typ
: (addr
-> 'a
-> 'b
) -> ('a
-> 'b
) fptr T
.typ
=
662 fn mkf
=> FPTR (fn a
=> (null
, mkf a
))
664 val reveal
: voidptr
-> addr
= addr_id
665 val freveal
: 'f fptr
' -> addr
= addr_id
667 val vcast
: addr
-> voidptr
= addr_id
668 val pcast
: addr
-> 'o ptr
' = addr_id
669 val fcast
: addr
-> 'f fptr
' = addr_id
671 fun unsafe_sub
esz (a
, i
) = a
++ esz
* i