Blame | Last modification | View Log | RSS feed
/*
Crown Copyright (c) 1997
This TenDRA(r) Computer Program is subject to Copyright
owned by the United Kingdom Secretary of State for Defence
acting through the Defence Evaluation and Research Agency
(DERA). It is made available to Recipients with a
royalty-free licence for its use, reproduction, transfer
to other parties and amendment for any purpose not excluding
product development provided that any such use et cetera
shall be deemed to be acceptance of the following conditions:-
(1) Its Recipients shall ensure that this Notice is
reproduced upon any copies or amended versions of it;
(2) Any amended version of it shall be clearly marked to
show both the nature of and the organisation responsible
for the relevant amendment or amendments;
(3) Its onward transfer from a recipient to another
party shall be deemed to be that party's acceptance of
these conditions;
(4) DERA gives no warranty or assurance as to its
quality or suitability for any purpose and DERA accepts
no liability whatsoever in relation to any use to which
it may be put.
*/
/* **************************************************** */
/* */
/* Generic pl_tdf source for sys.j */
/* */
/* **************************************************** */
Tokdef ~toks_major_v = [] NAT 3;
Tokdef ~toks_minor_v = [] NAT 1;
/* Target dependency tokens declarations */
Tokdec .~rep_var_width : [NAT] NAT;
Tokdec .~rep_atomic_width : [] NAT;
Tokdec .~rep_fv : [NAT] FLOATING_VARIETY;
Tokdec .~rep_fv_width : [NAT] NAT;
Tokdec .~rep_fv_radix : [NAT] NAT;
Tokdec .~rep_fv_mant : [NAT] NAT;
Tokdec .~rep_fv_min_exp : [NAT] NAT;
Tokdec .~rep_fv_max_exp : [NAT] NAT;
Tokdec .~rep_fv_epsilon : [NAT] EXP;
Tokdec .~rep_fv_min_val : [NAT] EXP;
Tokdec .~rep_fv_max_val : [NAT] EXP;
Tokdec .~ptr_width : [] NAT;
Tokdec .~best_div : [] NAT;
Tokdec .~little_endian : [] BOOL;
Tokdec .~ptr_to_ptr : [ALIGNMENT, ALIGNMENT, EXP] EXP;
Tokdec .~ptr_to_int : [ALIGNMENT, VARIETY, EXP] EXP;
Tokdec .~int_to_ptr : [VARIETY, ALIGNMENT, EXP] EXP;
Tokdec .~f_to_ptr : [ALIGNMENT, EXP] EXP;
Tokdec .~ptr_to_f : [ALIGNMENT, EXP] EXP;
/* C mapping token declarations */
Tokdec .~char_width : [] NAT;
Tokdec .~short_width : [] NAT;
Tokdec .~int_width : [] NAT;
Tokdec .~long_width : [] NAT;
Tokdec .~longlong_width : [] NAT;
Tokdec .~size_t_width : [] NAT;
Tokdec .~fl_rep : [] NAT;
Tokdec .~dbl_rep : [] NAT;
Tokdec .~ldbl_rep : [] NAT;
Tokdec .~pv_align : [] ALIGNMENT;
Tokdec .~min_struct_rep : [] NAT;
Tokdec .~char_is_signed : [] BOOL;
Tokdec .~bitfield_is_signed : [] BOOL;
/* Variety encoding constants for representing integer */
/* types in conversion, promotion rules etc */
Tokdef t_char = [] SIGNED_NAT 0;
Tokdef t_short = [] SIGNED_NAT 1;
Tokdef t_int = [] SIGNED_NAT 2;
Tokdef t_long = [] SIGNED_NAT 3;
Tokdef t_signed = [] SIGNED_NAT 4;
Tokdef t_unsigned = [] SIGNED_NAT 8;
Tokdef t_longlong = [] SIGNED_NAT 16;
Tokdef t_vmask = [] SIGNED_NAT 19;
Tokdef t_smask = [] SIGNED_NAT 12;
Tokdef t_vty = [] VARIETY /* variety for above constants */
var_width(false,8);
/* Constants derived from the above */
Tokdef t_s_char = [] SIGNED_NAT
computed_signed_nat (t_char(t_vty) Or t_signed(t_vty));
Tokdef t_u_char = [] SIGNED_NAT
computed_signed_nat (t_char(t_vty) Or t_unsigned(t_vty));
Tokdef t_s_short = [] SIGNED_NAT
computed_signed_nat (t_short(t_vty) Or t_signed(t_vty));
Tokdef t_u_short = [] SIGNED_NAT
computed_signed_nat (t_short(t_vty) Or t_unsigned(t_vty));
Tokdef t_s_int = [] SIGNED_NAT
computed_signed_nat (t_int(t_vty) Or t_signed(t_vty));
Tokdef t_u_int = [] SIGNED_NAT
computed_signed_nat (t_int(t_vty) Or t_unsigned(t_vty));
Tokdef t_s_long = [] SIGNED_NAT
computed_signed_nat (t_long(t_vty) Or t_signed(t_vty));
Tokdef t_u_long = [] SIGNED_NAT
computed_signed_nat (t_long(t_vty) Or t_unsigned(t_vty));
Tokdef t_s_longlong = [] SIGNED_NAT
computed_signed_nat (t_longlong(t_vty) Or t_s_long(t_vty));
Tokdef t_u_longlong = [] SIGNED_NAT
computed_signed_nat (t_longlong(t_vty) Or t_u_long(t_vty));
/* C integer and float varieties */
Tokdef ~char = [] VARIETY
var_width (.~char_is_signed, .~char_width);
Tokdef ~signed_char = [] VARIETY
var_width (true, .~char_width);
Tokdef ~unsigned_char = [] VARIETY
var_width (false, .~char_width);
Tokdef ~signed_short = [] VARIETY
var_width (true, .~short_width);
Tokdef ~unsigned_short = [] VARIETY
var_width (false, .~short_width);
Tokdef ~signed_int = [] VARIETY
var_width (true, .~int_width);
Tokdef ~unsigned_int = [] VARIETY
var_width (false, .~int_width);
Tokdef ~signed_long = [] VARIETY
var_width (true, .~long_width);
Tokdef ~unsigned_long = [] VARIETY
var_width (false, .~long_width);
Tokdef ~signed_longlong = [] VARIETY
var_width (true, .~longlong_width);
Tokdef ~unsigned_longlong = [] VARIETY
var_width (false, .~longlong_width);
Tokdef ~float = [] FLOATING_VARIETY
.~rep_fv [.~fl_rep];
Tokdef ~double = [] FLOATING_VARIETY
.~rep_fv [.~dbl_rep];
Tokdef ~long_double = [] FLOATING_VARIETY
.~rep_fv [.~ldbl_rep];
/* max values needed to determine types of literals */
Tokdef max_signed_int = [] SIGNED_NAT
computed_signed_nat (
(1(~unsigned_int) <<
(snat_from_nat(false,.~int_width)(~unsigned_int) - 1(~unsigned_int)))
- 1(~unsigned_int)
);
Tokdef max_unsigned_int = [] SIGNED_NAT
computed_signed_nat (
(0(~unsigned_int) - 1(~unsigned_int))
);
Tokdef max_signed_long = [] SIGNED_NAT
computed_signed_nat (
(1(~unsigned_long) <<
(snat_from_nat(false,.~long_width)(~unsigned_long) - 1(~unsigned_long)))
- 1(~unsigned_long)
);
Tokdef max_signed_longlong = [] SIGNED_NAT
computed_signed_nat (
(1(~unsigned_longlong) <<
(snat_from_nat(false,.~longlong_width)(~unsigned_long) - 1(~unsigned_long)))
- 1(~unsigned_longlong)
);
/* Shorthand tests producing EXP boolean */
/* for use in constant evaluation constructions */
Tokdef ITEST = [a:EXP, comp:NTEST, b:EXP] EXP /* exp integer test */
? { ?(a comp b); 1(~unsigned_int) | 0(~unsigned_int) };
Tokdef OTEST = [a:EXP, comp:NTEST, b:EXP] EXP /* exp offset test */
? { .?(a comp b); 1(~unsigned_int) | 0(~unsigned_int) };
Tokdef SNTEST = [a:SIGNED_NAT, comp:NTEST, b:SIGNED_NAT] EXP /* s_nat test */
ITEST [a(~unsigned_long), comp, b(~unsigned_long)];
Tokdef SNLLTEST = [a:SIGNED_NAT, comp:NTEST, b:SIGNED_NAT] EXP /* s_nat test */
ITEST [a(~unsigned_longlong), comp, b(~unsigned_longlong)];
Tokdef NATTEST = [a:NAT, comp:NTEST, b:NAT] EXP /* nat test */
SNTEST [snat_from_nat(false,a), comp, snat_from_nat(false,b)];
Tokdef TV_SNTEST = [a:SIGNED_NAT, comp:NTEST, b:SIGNED_NAT] EXP /* s_nat test */
ITEST [a(t_vty), comp, b(t_vty)];
Tokdef BOOLTEST = [b:BOOL] EXP
ITEST [snat_from_nat(b,1)(~signed_int), <, 0(~signed_int)];
Tokdef ~div = [arg1:EXP, arg2:EXP] EXP
div0 (impossible, wrap, arg1, arg2);
Tokdef ~rem = [arg1:EXP, arg2:EXP] EXP
rem0 (impossible, wrap, arg1, arg2);
Tokdef ~assign = [ptr:EXP, val:EXP, sh:SHAPE] EXP
Let desttag = ptr {
desttag = val ;
*(sh) desttag
};
Tokdef ~assign_vol = [ptr:EXP, val:EXP, sh:SHAPE] EXP
Let assigned_val = val {
assign_with_mode (volatile, ptr, assigned_val) ;
assigned_val
};
Tokdef ~ptr_add = [ptr:EXP, n:EXP, sh:SHAPE] EXP
( ptr *+. ( Sizeof(sh) .* n ) );
Tokdef ~ptr_sub = [ptr:EXP, n:EXP, sh:SHAPE] EXP
( ptr *+. offset_negate(( Sizeof(sh) .* n )) );
Tokdef ~sizeof = [sh:SHAPE] EXP
offset_div (
var_width (false, .~size_t_width),
Sizeof (sh),
Sizeof (integer(~unsigned_char))
);
Tokdef ~comp_off = [sz:EXP] EXP
offset_pad (
alignment (integer (var_width (false, .~min_struct_rep))),
offset_pad (alignment(compound(sz)), sz)
);
Tokdef ~convert = [which_v:SIGNED_NAT] VARIETY
VARIETY ? ( TV_SNTEST [which_v, ==, t_char],
~char,
VARIETY ? ( TV_SNTEST [which_v, ==, t_s_char],
~signed_char,
VARIETY ? ( TV_SNTEST [which_v, ==, t_u_char],
~unsigned_char,
VARIETY ? ( TV_SNTEST [which_v, ==, t_s_short],
~signed_short,
VARIETY ? ( TV_SNTEST [which_v, ==, t_u_short],
~unsigned_short,
VARIETY ? ( TV_SNTEST [which_v, ==, t_s_int],
~signed_int,
VARIETY ? ( TV_SNTEST [which_v, ==, t_u_int],
~unsigned_int,
VARIETY ? ( TV_SNTEST [which_v, ==, t_s_long],
~signed_long,
VARIETY ? ( TV_SNTEST [which_v, ==, t_u_long],
~unsigned_long,
VARIETY ? ( TV_SNTEST [which_v, ==, t_s_longlong],
~signed_longlong,
~unsigned_longlong
)
)
)
)
)
)
)
)
)
);
Tokdef OLDarith_type = [arg1:SIGNED_NAT, arg2:SIGNED_NAT] SIGNED_NAT
SIGNED_NAT ? ( TV_SNTEST [arg1, ==, t_u_long],
t_u_long,
SIGNED_NAT ? ( TV_SNTEST [arg2, ==, t_u_long],
t_u_long,
SIGNED_NAT ? ( TV_SNTEST [arg1, ==, t_s_long],
SIGNED_NAT ? ( NATTEST [.~long_width, >, .~int_width],
t_s_long,
SIGNED_NAT ? ( TV_SNTEST [arg2, ==, t_u_int],
t_u_long,
t_s_long
)
),
SIGNED_NAT ? ( TV_SNTEST [arg2, ==, t_s_long],
SIGNED_NAT ? ( NATTEST [.~long_width, >, .~int_width],
t_s_long,
SIGNED_NAT ? ( TV_SNTEST [arg1, ==, t_u_int],
t_u_long,
t_s_long
)
),
SIGNED_NAT ? ( TV_SNTEST [arg1, ==, t_u_int],
t_u_int,
SIGNED_NAT ? ( TV_SNTEST [arg2, ==, t_u_int],
t_u_int,
t_s_int
)
)
)
)
)
);
Tokdef ~arith_type = [arg1:SIGNED_NAT, arg2:SIGNED_NAT] SIGNED_NAT
SIGNED_NAT ? ( TV_SNTEST [arg1, ==, t_u_longlong],
t_u_longlong,
SIGNED_NAT ? ( TV_SNTEST [arg2, ==, t_u_longlong],
t_u_longlong,
SIGNED_NAT ? ( TV_SNTEST [arg1, ==, t_s_longlong],
SIGNED_NAT ? ( NATTEST [.~longlong_width, >, .~long_width],
t_s_longlong,
SIGNED_NAT ? ( TV_SNTEST [arg2, ==, t_u_long],
t_u_longlong,
SIGNED_NAT ? ( NATTEST [.~longlong_width, >, .~int_width],
t_s_longlong,
SIGNED_NAT ? ( TV_SNTEST [arg2, ==, t_u_int],
t_u_longlong,
t_s_longlong
)
)
)
),
SIGNED_NAT ? ( TV_SNTEST [arg2, ==, t_s_longlong],
SIGNED_NAT ? ( NATTEST [.~longlong_width, >, .~long_width],
t_s_longlong,
SIGNED_NAT ? ( TV_SNTEST [arg1, ==, t_u_long],
t_u_longlong,
SIGNED_NAT ? ( NATTEST [.~longlong_width, >, .~int_width],
t_s_longlong,
SIGNED_NAT ? ( TV_SNTEST [arg2, ==, t_u_int],
t_u_longlong,
t_s_longlong
)
)
)
),
OLDarith_type [arg1, arg2]
)
)
)
);
Tokdef ~int_promot = [] SIGNED_NAT
SIGNED_NAT ? ( NATTEST [.~int_width, >, .~short_width],
t_s_int,
t_u_int
);
Tokdef ~promote = [arg:SIGNED_NAT] SIGNED_NAT
computed_signed_nat(
EXP ? ( TV_SNTEST [arg, ==, t_u_short],
~int_promot(t_vty),
? { ?( (arg(t_vty) And t_vmask(t_vty)) < t_int(t_vty));
t_s_int(t_vty)
| arg(t_vty)
}
)
);
Tokdef ~sign_promote = [arg:SIGNED_NAT] SIGNED_NAT
computed_signed_nat(
? { ?( (arg(t_vty) And t_vmask(t_vty)) < t_int(t_vty));
? { ?( (arg(t_vty) And t_smask(t_vty)) == t_unsigned(t_vty));
t_u_int(t_vty)
| t_s_int(t_vty)
}
| arg(t_vty)
}
);
Tokdef ~lit_int = [arg:SIGNED_NAT] SIGNED_NAT
SIGNED_NAT ? ( SNTEST [arg, <=, max_signed_int],
t_s_int,
SIGNED_NAT ? ( SNTEST [arg, <=, max_signed_long],
t_s_long,
t_u_long
)
);
Tokdef ~lit_hex = [arg:SIGNED_NAT] SIGNED_NAT
SIGNED_NAT ? ( SNTEST [arg, <=, max_signed_int],
t_s_int,
SIGNED_NAT ? ( SNTEST [arg, <=, max_unsigned_int],
t_u_int,
SIGNED_NAT ? ( SNTEST [arg, <=, max_signed_long],
t_s_long,
t_u_long
)
)
);
Tokdef ~lit_unsigned = [arg:SIGNED_NAT] SIGNED_NAT
SIGNED_NAT ? ( SNTEST [arg, <=, max_unsigned_int],
t_u_int,
t_u_long
);
Tokdef ~lit_long = [arg:SIGNED_NAT] SIGNED_NAT
SIGNED_NAT ? ( SNTEST [arg, <=, max_signed_long],
t_s_long,
t_u_long
);
Tokdef ~lit_ulong = [arg:SIGNED_NAT] SIGNED_NAT
t_u_long;
Tokdef ~lit_longlong = [arg:SIGNED_NAT] SIGNED_NAT
SIGNED_NAT ? ( SNLLTEST [arg, <=, max_signed_longlong],
t_s_longlong,
t_u_longlong
);
Tokdef ~lit_ulonglong = [arg:SIGNED_NAT] SIGNED_NAT
t_u_longlong;
Tokdef ~char_lit = [chars:EXP, length:SIGNED_NAT, v:VARIETY] EXP
EXP ? ( SNTEST [length, ==, 1],
Var char_val = chars {
[ v ] * (integer(~char)) char_val
},
#"Too many characters in char literal"
);
Tokdef ~wchar_lit = [chars:EXP, length:SIGNED_NAT, v:VARIETY] EXP
~char_lit [ chars, length, v ];
Tokdef ~string_lit = [string:EXP, length:SIGNED_NAT, v:VARIETY] EXP
(string);
Tokdef ~checked_plus = [arg1:EXP, arg2:EXP] EXP
EXP ? ( ITEST [arg1, >, (max_signed_int(~unsigned_long) - arg2)],
#"Constant out of range for its type",
arg1 + arg2
);
/* pointer conversions, simple for byte-addressed architectures */
Tokdef ~ptr_void = [] SHAPE
pointer (.~pv_align);
Tokdef ~pun = [from_sh:SHAPE, to_sh:SHAPE, val:EXP] EXP
component (
to_sh,
Cons [ shape_offset(from_sh) .max. shape_offset(to_sh) ] (
offset_zero(alignment(from_sh)) : val
),
offset_zero(alignment(to_sh))
);
Tokdef ~ptr_to_ptr = [from_al:ALIGNMENT, to_al:ALIGNMENT, ptr:EXP] EXP
~pun [ pointer(from_al), pointer(to_al), ptr ];
Tokdef ~to_ptr_void = [al:ALIGNMENT, ptr:EXP] EXP
~ptr_to_ptr [ al, .~pv_align, ptr ];
Tokdef ~from_ptr_void = [al:ALIGNMENT, ptr:EXP] EXP
~ptr_to_ptr [ .~pv_align, al, ptr ];
Tokdef ~i_to_p = [v:VARIETY, al:ALIGNMENT, val:EXP] EXP
~pun [
integer (var_width (true, .~ptr_width)),
pointer (al),
[var_width (true, .~ptr_width)] val
];
Tokdef ~p_to_i = [al:ALIGNMENT, v:VARIETY, val:EXP] EXP
([v] ~pun [
pointer (al),
integer (var_width (true,.~ptr_width)),
val
]);
Tokdef ~null_pv = [] EXP
make_null_ptr(.~pv_align);
Tokdef ~pv_test = [ptr:EXP, escape:LABEL, comparison:NTEST] EXP
*?(ptr comparison ~null_pv | escape);
Tokdef ~cpp.pv_compare = [ptr1:EXP, ptr2:EXP, escape:LABEL, comparison:NTEST] EXP
*?(ptr1 comparison ptr2 | escape);
Tokdef ~pad = [off:EXP, sh1:SHAPE, sh2:SHAPE] EXP
EXP ? ( OTEST [offset_pad(alignment(sh1), (off .+. shape_offset(sh2))),
>,
offset_pad(alignment(sh1), off)],
offset_pad(alignment(sh1), off),
offset_pad(alignment(sh2), off)
);
Tokdef ~i_to_pv = [v:VARIETY, val:EXP] EXP
~i_to_p [ v, .~pv_align, val ];
Tokdef ~pv_to_i = [v:VARIETY, val:EXP] EXP
~p_to_i [ .~pv_align, v, val ];
Tokdef ~f_to_pv = [fn:EXP] EXP
.~f_to_ptr [ .~pv_align, fn ];
Tokdef ~pv_to_f = [ptr:EXP] EXP
.~ptr_to_f [ .~pv_align, ptr ];
Tokdef ~debug_exp = [diagi:NAT, body:EXP] EXP
(body);
Tokdef ~debug_scope = [starti:NAT, endi:NAT, body:EXP] EXP
(body);
Tokdef ~fn_scope = [body:EXP, starti:NAT, endi:NAT] EXP
(body);
Tokdef ~little_endian = [] EXP
EXP ? ( BOOLTEST [.~little_endian],
1(~signed_int),
0(~signed_int)
);
Tokdef ~cpp.empty.offset = [] EXP
~comp_off [
offset_add (
offset_zero(alignment(integer(~char))),
shape_offset(integer(~char)))
];
Tokdef ~cpp.empty.shape = [] SHAPE
compound(~cpp.empty.offset);
Tokdef ~cpp.empty.align = [] ALIGNMENT
alignment(floating(~long_double));
Tokdef ~cpp.bitf_sign = [which_v: SIGNED_NAT] BOOL
BOOL ? ( BOOLTEST [.~bitfield_is_signed],
BOOL ? ( which_v(t_vty) And t_unsigned(t_vty),
false,
true
),
false
);
Tokdef ~cpp.ptr_rep = [] SIGNED_NAT
SIGNED_NAT ? ( NATTEST [.~ptr_width, ==, .~int_width],
t_s_int,
t_s_long
);
Keep (
~toks_major_v, ~toks_minor_v,
~div, ~rem, ~ptr_add, ~ptr_sub, ~char, ~unsigned_char, ~signed_char,
~unsigned_short, ~signed_short, ~unsigned_int, ~signed_int,
~unsigned_long, ~signed_long, ~unsigned_longlong, ~signed_longlong,
~float, ~double, ~long_double,
~ptr_void, ~assign, ~assign_vol, ~convert, ~arith_type, ~int_promot,
~debug_exp, ~debug_scope, ~fn_scope, ~promote, ~sign_promote,
~lit_int, ~lit_hex, ~lit_unsigned, ~lit_long, ~lit_ulong, ~lit_longlong,
~lit_ulonglong, ~char_lit, ~wchar_lit,
~string_lit, ~checked_plus, ~to_ptr_void, ~from_ptr_void, ~ptr_to_ptr,
~sizeof, ~i_to_p, ~p_to_i, ~null_pv, ~pv_test, ~cpp.pv_compare, ~pad,
~i_to_pv, ~pv_to_i, ~f_to_pv, ~pv_to_f, ~comp_off, ~little_endian,
~cpp.empty.offset, ~cpp.empty.shape, ~cpp.empty.align,
~cpp.bitf_sign, ~cpp.ptr_rep
)
Generated by GNU Enscript 1.6.6.