blob: c8959d10d3ffaa9950501aac0a5ab2401771d14d (
plain)
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
|
(* generated by Ott 0.29 from: ../language/jib.ott *)
open import Pervasives
open import Ast
open import Value2
type name =
| Name of id * nat
| Have_exception of nat
| Current_exception of nat
| Return of nat
type ctyp = (* C type *)
| CT_lint
| CT_fint of nat
| CT_constant of integer
| CT_lbits of bool
| CT_sbits of nat * bool
| CT_fbits of nat * bool
| CT_unit
| CT_bool
| CT_bit
| CT_string
| CT_real
| CT_tup of list ctyp
| CT_enum of id * list id
| CT_struct of id * list (uid * ctyp)
| CT_variant of id * list (uid * ctyp)
| CT_vector of bool * ctyp
| CT_list of ctyp
| CT_ref of ctyp
| CT_poly
and uid = id * list ctyp
type op =
| Bnot
| Bor
| Band
| List_hd
| List_tl
| Bit_to_bool
| Eq
| Neq
| Ilt
| Ilteq
| Igt
| Igteq
| Iadd
| Isub
| Unsigned of nat
| Signed of nat
| Bvnot
| Bvor
| Bvand
| Bvxor
| Bvadd
| Bvsub
| Bvaccess
| Concat
| Zero_extend of nat
| Sign_extend of nat
| Slice of nat
| Sslice of nat
| Set_slice
| Replicate of nat
type clexp =
| CL_id of name * ctyp
| CL_rmw of name * name * ctyp
| CL_field of clexp * uid
| CL_addr of clexp
| CL_tuple of clexp * nat
| CL_void
type cval =
| V_id of name * ctyp
| V_ref of name * ctyp
| V_lit of vl * ctyp
| V_struct of list (uid * cval) * ctyp
| V_ctor_kind of cval * id * list ctyp * ctyp
| V_ctor_unwrap of id * cval * list ctyp * ctyp
| V_tuple_member of cval * nat * nat
| V_call of op * list cval
| V_field of cval * uid
| V_poly of cval * ctyp
type iannot = nat * nat * nat
type instr_aux =
| I_decl of ctyp * name
| I_init of ctyp * name * cval
| I_jump of cval * string
| I_goto of string
| I_label of string
| I_funcall of clexp * bool * uid * list cval
| I_copy of clexp * cval
| I_clear of ctyp * name
| I_undefined of ctyp
| I_match_failure
| I_end of name
| I_if of cval * list instr * list instr * ctyp
| I_block of list instr
| I_try_block of list instr
| I_throw of cval
| I_comment of string
| I_raw of string
| I_return of cval
| I_reset of ctyp * name
| I_reinit of ctyp * name * cval
and instr =
| I_aux of instr_aux * iannot
type ctype_def = (* C type definition *)
| CTD_enum of id * list id
| CTD_struct of id * list (uid * ctyp)
| CTD_variant of id * list (uid * ctyp)
type cdef =
| CDEF_reg_dec of id * ctyp * list instr
| CDEF_type of ctype_def
| CDEF_let of nat * list (id * ctyp) * list instr
| CDEF_spec of id * list ctyp * ctyp
| CDEF_fundef of id * maybe id * list id * list instr
| CDEF_startup of id * list instr
| CDEF_finish of id * list instr
|
