#
# The implementation of the interface that encodes C's type system
# in Mythryl. This implementation includes its "private" extensions.
#
# (C) 2001, Lucent Technologies, Bell Laboratories
#
# author: Matthias Blume (blume@research.bell-labs.com)
# Compiled by:
# src/lib/c-glue-lib/internals/c-internals.libstipulate
# We play some games here with first calling c_internals simply c and then
# renaming it because they result in saner printing behavior.
package c : Ckit_Internal { # Ckit_Internal is from src/lib/c-glue-lib/internals/ckit-internal.api exception OUT_OF_MEMORY = cmemory::OUT_OF_MEMORY;
fun bug m
=
raise exception DIE ("impossible: " + m);
Addr = cmemory::Addr;
stipulate
Chunkt = BASE Unt
| PTR Chunkt
| FPTR unsafe::unsafe_chunk::Chunk # == address -> $f
| ARR { type: Chunkt,
n: Unt,
esz: Unt, # "esz" == "element size".
asz: Unt # "asz" == "array size".
};
# Bitfield: b bits wide, l bits from left corner, r bits from right.
# The word itself is c_memory::int_bits wide and located at address a.
#
# MSB LSB
# V |<---b--->| V
# |<---l---> ......... <---r--->|
# |<----------wordsize--------->|
#
# 0.......0 1.......1 0.......0 = m
# 1.......1 0.......0 1.......1 = im
#
# l + r = lr
Cword = mlrep::unsigned::Unt;
Bf = { a: Addr, # "Bf" == "bitfield", probably.
l: Unt,
r: Unt,
lr: Unt,
m: Cword,
im: Cword
};
fun pair_type_addr (t: Chunkt) (a: Addr) = (a, t);
fun strip_type (a: Addr, _: Chunkt) = a;
fun p_strip_type (a: Addr, _: Chunkt) = a;
fun strip_fun (a: Addr, _: F ) = a;
fun address_type_id (x: (Addr, Chunkt)) = x;
fun addr_id (x: Addr ) = x;
infix my --- +++ ;
my (---) = cmemory::(---);
my (+++) = cmemory::(+++);
infix my << >> >>> &&& ||| ^^^;
my (<<) = mlrep::unsigned::(<<);
my (>>) = mlrep::unsigned::(>>);
my (>>>) = mlrep::unsigned::(>>>);
my (&&&) = mlrep::unsigned::bitwise_and;
my (|||) = mlrep::unsigned::bitwise_or;
my (^^^) = mlrep::unsigned::bitwise_xor;
my (~~~) = mlrep::unsigned::bitwise_not;
herein
Chunk (T, C) = (Addr, Chunkt); # RTTI for stored value
Chunk' (T, C) = Addr;
Ro = Void;
Rw = Void;
Ptr O = (Addr, Chunkt); # RTTI for target value
Ptr' O = Addr;
Arr (T, N) = Void;
Fptr( F ) = (Addr, F);
Fptr'( F ) = Addr; # Lightweight variant does not carry function around
Void = Void;
Voidptr = Ptr'( Void );
Su( A_tag ) = Void;
An_Enum( A_tag ) = mlrep::signed::Int;
Schar = mlrep::signed::Int;
Uchar = mlrep::unsigned::Unt;
Sint = mlrep::signed::Int;
Uint = mlrep::unsigned::Unt;
Sshort = mlrep::signed::Int;
Ushort = mlrep::unsigned::Unt;
Slong = mlrep::signed::Int;
Ulong = mlrep::unsigned::Unt;
Slonglong = mlrep::long_long_signed::Int;
Ulonglong = mlrep::long_long_unsigned::Unt;
Float = mlrep::float::Float;
Double = mlrep::float::Float;
Schar_Chunk( C ) = Chunk( Schar, C );
Uchar_Chunk( C ) = Chunk( Uchar, C );
Sint_Chunk( C ) = Chunk (Sint, C);
Uint_Chunk( C ) = Chunk (Uint, C);
Sshort_Chunk( C ) = Chunk (Sshort, C);
Ushort_Chunk( C ) = Chunk (Ushort, C);
Slong_Chunk( C ) = Chunk (Slong, C);
Ulong_Chunk( C ) = Chunk (Ulong, C);
Slonglong_Chunk( C ) = Chunk (Slonglong, C);
Ulonglong_Chunk( C ) = Chunk (Ulonglong, C);
Float_Chunk( C ) = Chunk (Float, C);
Double_Chunk( C ) = Chunk (Double, C);
Voidptr_Chunk( C ) = Chunk (Voidptr, C);
Enum_Chunk (E, C ) = Chunk (An_Enum( E ), C);
Fptr_Chunk (F, C ) = Chunk (Fptr( F ), C);
Su_Chunk (S, C ) = Chunk (Su( S ), C);
Schar_Chunk'( C ) = Chunk' (Schar, C);
Uchar_Chunk'( C ) = Chunk' (Uchar, C);
Sint_Chunk'( C ) = Chunk' (Sint, C);
Uint_Chunk'( C ) = Chunk' (Uint, C);
Sshort_Chunk'( C ) = Chunk' (Sshort, C);
Ushort_Chunk'( C ) = Chunk' (Ushort, C);
Slong_Chunk'( C ) = Chunk' (Slong, C);
Ulong_Chunk'( C ) = Chunk' (Ulong, C);
Slonglong_Chunk'( C ) = Chunk' (Slonglong, C);
Ulonglong_Chunk'( C ) = Chunk' (Ulonglong, C);
Float_Chunk'( C ) = Chunk' (Float, C);
Double_Chunk'( C ) = Chunk' (Double, C);
Voidptr_Chunk'( C ) = Chunk' (Voidptr, C);
Enum_Chunk' (E, C ) = Chunk' (An_Enum( E ), C);
Fptr_Chunk' (F, C ) = Chunk' (Fptr( F), C);
Su_Chunk' (S, C ) = Chunk' (Su (S ), C);
Ubf( C ) = Bf;
Sbf( C ) = Bf;
package w {
Witness (A_from, A_to) = Void;
trivial = ();
fun pointer () = ();
fun chunk () = ();
fun arr () = ();
fun ro () = ();
fun rw () = ();
};
fun convert w x = x;
fun convert' w x = x;
# A family of types and corresponding values representing natural numbers.
# (An encoding in Mythryl without using dependent types.)
# This is the full implementation including an unsafe extension
# ("from_int").
package dim {
Dim0 (X, Z) = Int;
fun to_int d = d;
fun from_int d = d;
Dec = Void;
Dg0(X) = Void;
Dg1(X) = Void;
Dg2(X) = Void;
Dg3(X) = Void;
Dg4(X) = Void;
Dg5(X) = Void;
Dg6(X) = Void;
Dg7(X) = Void;
Dg8(X) = Void;
Dg9(X) = Void;
Zero = Void;
Nonzero = Void;
Dim(X) = Dim0(X, Nonzero);
stipulate
fun dg n d
=
10 * d + n;
herein
dec' = 0;
my (dg0', dg1', dg2', dg3', dg4', dg5', dg6', dg7', dg8', dg9') =
(dg 0, dg 1, dg 2, dg 3, dg 4, dg 5, dg 6, dg 7, dg 8, dg 9);
fun dec k = k dec';
fun dg0 d k = k (dg0' d);
fun dg1 d k = k (dg1' d);
fun dg2 d k = k (dg2' d);
fun dg3 d k = k (dg3' d);
fun dg4 d k = k (dg4' d);
fun dg5 d k = k (dg5' d);
fun dg6 d k = k (dg6' d);
fun dg7 d k = k (dg7' d);
fun dg8 d k = k (dg8' d);
fun dg9 d k = k (dg9' d);
fun dim d = d;
end;
};
package s {
Size( T ) = Unt;
fun to_word (s: Size( T ))
=
s;
schar = cmemory::char_size;
uchar = cmemory::char_size;
sint = cmemory::int_size;
uint = cmemory::int_size;
sshort = cmemory::short_size;
ushort = cmemory::short_size;
slong = cmemory::long_size;
ulong = cmemory::long_size;
slonglong = cmemory::longlong_size;
ulonglong = cmemory::longlong_size;
float = cmemory::float_size;
double = cmemory::double_size;
voidptr = cmemory::addr_size;
ptr = cmemory::addr_size;
fptr = cmemory::addr_size;
an_enum = cmemory::int_size;
};
package t {
Type( T ) = Chunkt;
fun typeof (_: Addr, t: Chunkt)
=
t;
fun sizeof (BASE b) => b;
sizeof (PTR _) => s::ptr;
sizeof (FPTR _) => s::fptr;
sizeof (ARR a) => a.asz;
end;
# Use private (and unsafe) extension to Dim module here...
fun dim (ARR { n, ... } ) => dim::from_int (unt::to_int n);
dim _ => bug "t::dim (non-rw_vector type)";
end;
fun pointer t = PTR t;
fun target (PTR t) => t;
target _ => bug "t::target (non-pointer type)";
end;
fun arr (t, d)
=
{ n = unt::from_int (dim::to_int d);
s = sizeof t;
ARR { type => t, n, esz => s, asz => n * s };
};
fun element (ARR a) => a.type;
element _ => bug "t::element (non-rw_vector type)";
end;
fun ro (t: Chunkt) = t;
schar = BASE s::schar;
uchar = BASE s::uchar;
sint = BASE s::sint;
uint = BASE s::uint;
sshort = BASE s::sshort;
ushort = BASE s::ushort;
slong = BASE s::slong;
ulong = BASE s::ulong;
slonglong = BASE s::slonglong;
ulonglong = BASE s::ulonglong;
float = BASE s::float;
double = BASE s::double;
voidptr = BASE s::voidptr;
an_enum = BASE s::sint;
};
package light {
chunk = p_strip_type;
ptr = p_strip_type;
fptr = strip_fun;
};
package heavy {
chunk = pair_type_addr;
fun ptr (PTR t) p => (p, t);
ptr _ _ => bug "Heavy::ptr (non-chunk-pointer-type)";
end;
fun fptr (FPTR makef) p => (p, unsafe::cast makef p);
fptr _ _ => bug "Heavy::fptr (non-function-pointer-type)";
end;
};
fun sizeof (_: Addr, t) = t::sizeof t;
package convert {
# Going between abstract and concrete; these are all identities
fun c_schar (c: Schar) = c;
fun c_uchar (c: Uchar) = c;
fun c_sint (i: Sint) = i;
fun c_uint (i: Uint) = i;
fun c_sshort (s: Sshort) = s;
fun c_ushort (s: Ushort) = s;
fun c_slong (l: Slong) = l;
fun c_ulong (l: Ulong) = l;
fun c_slonglong (l: Slonglong) = l;
fun c_ulonglong (l: Ulonglong) = l;
fun c_float (f: Float) = f;
fun c_double (d: Double) = d;
fun i2c_enum (e: An_Enum( E )) = e;
ml_schar = c_schar;
ml_uchar = c_uchar;
ml_sint = c_sint;
ml_uint = c_uint;
ml_sshort = c_sshort;
ml_ushort = c_ushort;
ml_slong = c_slong;
ml_ulong = c_ulong;
ml_slonglong = c_slonglong;
ml_ulonglong = c_ulonglong;
ml_float = c_float;
ml_double = c_double;
c2i_enum = i2c_enum;
};
package get {
uchar' = cmemory::load_uchar;
schar' = cmemory::load_schar;
uint' = cmemory::load_uint;
sint' = cmemory::load_sint;
ushort' = cmemory::load_ushort;
sshort' = cmemory::load_sshort;
ulong' = cmemory::load_ulong;
slong' = cmemory::load_slong;
ulonglong' = cmemory::load_ulonglong;
slonglong' = cmemory::load_slonglong;
float' = cmemory::load_float;
double' = cmemory::load_double;
an_enum' = cmemory::load_sint;
ptr' = cmemory::load_addr;
fptr' = cmemory::load_addr;
voidptr' = cmemory::load_addr;
uchar = uchar' o strip_type;
schar = schar' o strip_type;
uint = uint' o strip_type;
sint = sint' o strip_type;
ushort = ushort' o strip_type;
sshort = sshort' o strip_type;
ulong = ulong' o strip_type;
slong = slong' o strip_type;
ulonglong = ulonglong' o strip_type;
slonglong = slonglong' o strip_type;
float = float' o strip_type;
double = double' o strip_type;
voidptr = voidptr' o strip_type;
an_enum = an_enum' o strip_type;
fun ptr (a, PTR t) => (cmemory::load_addr a, t);
ptr _ => bug "get::ptr (non-pointer)";
end;
fun fptr (a, FPTR makef) => { fa = cmemory::load_addr a; (fa, unsafe::cast makef fa); };
fptr _ => bug "get::fptr (non-function-pointer)";
end;
stipulate
u2s = mlrep::signed::from_multiword_int o mlrep::unsigned::to_multiword_int_x;
herein
fun ubf ( { a, l, r, lr, m, im } : Bf)
=
(cmemory::load_uint a << l) >> lr;
fun sbf ( { a, l, r, lr, m, im } : Bf)
=
u2s ((cmemory::load_uint a << l) >>> lr);
end;
};
package set {
uchar' = cmemory::store_uchar;
schar' = cmemory::store_schar;
uint' = cmemory::store_uint;
sint' = cmemory::store_sint;
ushort' = cmemory::store_ushort;
sshort' = cmemory::store_sshort;
ulong' = cmemory::store_ulong;
slong' = cmemory::store_slong;
ulonglong' = cmemory::store_ulonglong;
slonglong' = cmemory::store_slonglong;
float' = cmemory::store_float;
double' = cmemory::store_double;
an_enum' = cmemory::store_sint;
ptr' = cmemory::store_addr;
fptr' = cmemory::store_addr;
voidptr' = cmemory::store_addr;
ptr_voidptr' = cmemory::store_addr;
stipulate
infix my @@@;
fun (f @@@ g) (x, y)
=
f (g x, y);
herein
uchar = uchar' @@@ strip_type;
schar = schar' @@@ strip_type;
uint = uint' @@@ strip_type;
sint = sint' @@@ strip_type;
ushort = ushort' @@@ strip_type;
sshort = sshort' @@@ strip_type;
ulong = ulong' @@@ strip_type;
slong = slong' @@@ strip_type;
ulonglong = ulonglong' @@@ strip_type;
slonglong = slonglong' @@@ strip_type;
float = float' @@@ strip_type;
double = double' @@@ strip_type;
voidptr = voidptr' @@@ strip_type;
an_enum = an_enum' @@@ strip_type;
fun ptr_voidptr (x, p) = ptr_voidptr' (p_strip_type x, p);
fun ptr (x, p) = ptr' (p_strip_type x, p_strip_type p);
fun fptr (x, f) = fptr' (p_strip_type x, strip_fun f);
end;
fun ubf ( { a, l, r, lr, m, im }, x)
=
cmemory::store_uint (a, (cmemory::load_uint a &&& im) |||
((x << r) &&& m));
stipulate
s2u = mlrep::unsigned::from_multiword_int
o
mlrep::signed::to_multiword_int;
herein
fun sbf (f, x)
=
ubf (f, s2u x);
end;
};
fun copy' bytes { from, to }
=
cmemory::bcopy { from, to, bytes };
fun copy { from => (from, t), to => (to, _: Chunkt) }
=
copy' (t::sizeof t) { from, to };
ro = address_type_id;
rw = address_type_id;
ro' = addr_id;
rw' = addr_id;
package ptr {
my enref = address_type_id; # Same as C '&' addres-of op.
my deref = address_type_id; # Save as C '*' fetch-via-pointer op.
my enref' = addr_id; # Lightweight version of above (no implicit run-time type info).
my deref' = addr_id; # Lightweight version of above (no implicit run-time type info).
fun compare (p, p')
=
cmemory::compare (p_strip_type p, p_strip_type p');
compare' = cmemory::compare;
inject' = addr_id;
cast' = addr_id;
inject = p_strip_type;
fun cast (PTR t) (p: Voidptr) => (p, t);
cast _ _ => bug "Ptr::cast (non-pointer-type)";
end;
v_null = cmemory::null;
fun null t = cast t v_null;
null' = cmemory::null;
fnull' = cmemory::null;
fun fnull t = heavy::fptr t fnull';
v_is_null = cmemory::is_null;
fun is_null p = v_is_null (inject p);
is_null' = cmemory::is_null;
fun is_fnull (p, _)
=
cmemory::is_null p;
is_fnull' = cmemory::is_null;
fun plus' s (p, i) = p +++ (unt::to_int s * i);
fun diff' s (p, p') = (p --- p') / unt::to_int s;
fun plus ((p, t), i) = (plus' (t::sizeof t) (p, i), t);
fun diff ((p, t), (p', _: Chunkt)) = diff' (t::sizeof t) (p, p');
fun sub (p, i)
=
deref (plus (p, i));
fun sub' t (p, i)
=
deref' (plus' t (p, i));
ro = address_type_id;
rw = address_type_id;
ro' = addr_id;
rw' = addr_id;
fun convert w x = x;
fun convert' w x = x;
};
package arr {
stipulate
fun asub (a, i, n, esz)
=
# Take advantage of wrap-around to avoid the >= 0 test...
if (unt::from_int i < n)
a +++ (unt::to_int_x esz * i);
else
raise exception exceptions::INDEX_OUT_OF_BOUNDS;
fi;
herein
fun sub ((a, ARR { type, n, esz, ... } ), i)
=>
(asub (a, i, n, esz), type);
sub _
=>
bug "Arr::sub (non-rw_vector)";
end;
fun sub' (s, d) (a, i)
=
asub (a, i, unt::from_int (dim::to_int d), s);
end;
fun decay (a, ARR { type, ... } )
=>
(a, type);
decay _
=>
bug "Arr::decay (non-rw_vector)";
end;
decay' = addr_id;
fun reconstruct ((a: Addr, t), d)
=
(a, t::arr (t, d));
fun reconstruct' (a: Addr, d: dim::Dim( N ))
=
a;
fun dim (_: Addr, t)
=
t::dim t;
};
fun new' s = cmemory::allot s;
fun new t = (new' (t::sizeof t), t);
discard' = cmemory::free;
fun discard x
=
discard' (p_strip_type x);
fun allot' s i = cmemory::allot (s * i);
fun allot t i = (allot' (t::sizeof t) i, t);
free' = cmemory::free;
fun free x = free' (p_strip_type x);
fun call ((_: Addr, f), x) = f x;
fun call' (FPTR makef) (a, x)
=>
unsafe::cast makef a x;
call' _ _
=>
bug "call' (non-function-pointer-type)";
end;
package u {
fun fcast (f: Fptr'(X)) : Fptr'(Y) = f;
fun p2i (a: Ptr'( O )) : Ulong = cmemory::p2i a;
fun i2p (a: Ulong) : Ptr'( O ) = cmemory::i2p a;
};
# ------------- internal stuff -------------
fun make_chunk' (a: Addr) = a;
fun make_voidptr (a: Addr) = a;
fun make_fptr (makef, a)
=
(a, makef a);
stipulate
fun make_field (t: Chunkt, i, (a, _: Chunkt)) = (a +++ i, t);
herein
make_rw_field = make_field;
make_ro_field = make_field;
fun make_field' (i, a)
=
a +++ i;
end;
stipulate
fun make_bf' (offset, bits, shift) a
=
{
a = a +++ offset;
l = shift;
lr = cmemory::int_bits - bits;
r = lr - l;
m = (~~~0u0 << lr) >> l;
im = ~~~ m;
{ a, l, r, lr, m, im } : Bf;
};
fun make_bf acc (a, _: Chunkt)
=
make_bf' acc a;
herein
make_rw_ubf = make_bf;
make_ro_ubf = make_bf;
make_rw_ubf' = make_bf';
make_ro_ubf' = make_bf';
make_rw_sbf = make_bf;
make_ro_sbf = make_bf;
make_rw_sbf' = make_bf';
make_ro_sbf' = make_bf';
end;
fun make_su_size size = size;
fun make_su_type size = BASE size;
fun make_fptr_type (makef: Addr -> X -> Y)
=
FPTR (unsafe::cast makef);
reveal = addr_id;
freveal = addr_id;
vcast = addr_id;
pcast = addr_id;
fcast = addr_id;
fun unsafe_sub esz (a, i)
=
a +++ esz * i;
end; # local
};
herein
package c_internals= c; # c is from src/lib/c-glue-lib/internals/c.pkgend;