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
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
|
(**************************************************************************)
(* Sail *)
(* *)
(* Copyright (c) 2013-2017 *)
(* Kathyrn Gray *)
(* Shaked Flur *)
(* Stephen Kell *)
(* Gabriel Kerneis *)
(* Robert Norton-Wright *)
(* Christopher Pulte *)
(* Peter Sewell *)
(* Alasdair Armstrong *)
(* Brian Campbell *)
(* Thomas Bauereiss *)
(* Anthony Fox *)
(* Jon French *)
(* Dominic Mulligan *)
(* Stephen Kell *)
(* Mark Wassell *)
(* *)
(* All rights reserved. *)
(* *)
(* This software was developed by the University of Cambridge Computer *)
(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *)
(* (REMS) project, funded by EPSRC grant EP/K008528/1. *)
(* *)
(* Redistribution and use in source and binary forms, with or without *)
(* modification, are permitted provided that the following conditions *)
(* are met: *)
(* 1. Redistributions of source code must retain the above copyright *)
(* notice, this list of conditions and the following disclaimer. *)
(* 2. Redistributions in binary form must reproduce the above copyright *)
(* notice, this list of conditions and the following disclaimer in *)
(* the documentation and/or other materials provided with the *)
(* distribution. *)
(* *)
(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *)
(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *)
(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *)
(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *)
(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *)
(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *)
(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *)
(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *)
(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *)
(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *)
(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *)
(* SUCH DAMAGE. *)
(**************************************************************************)
(** The A-normal form (ANF) grammar *)
open Ast
open Ast_util
open Jib
open Type_check
(** The first step in compiling Sail is converting the Sail expression
grammar into A-normal form (ANF). Essentially this converts
expressions such as [f(g(x), h(y))] into something like:
[let v0 = g(x) in let v1 = h(x) in f(v0, v1)]
Essentially the arguments to every function must be trivial, and
complex expressions must be let bound to new variables, or used in
a block, assignment, or control flow statement (if, for, and
while/until loops). The aexp datatype represents these expressions,
while aval represents the trivial values.
The convention is that the type of an aexp is given by last
argument to a constructor. It is omitted where it is obvious - for
example all for loops have unit as their type. If some constituent
part of the aexp has an annotation, the it refers to the previous
argument, so in
[AE_let (id, typ1, _, body, typ2)]
[typ1] is the type of the bound identifer, whereas [typ2] is the type
of the whole let expression (and therefore also the body).
See Flanagan et al's {e The Essence of Compiling with Continuations}.
*)
type 'a aexp = AE_aux of 'a aexp_aux * Env.t * l
and 'a aexp_aux =
| AE_val of 'a aval
| AE_app of id * ('a aval) list * 'a
| AE_cast of 'a aexp * 'a
| AE_assign of 'a alexp * 'a aexp
| AE_let of mut * id * 'a * 'a aexp * 'a aexp * 'a
| AE_block of ('a aexp) list * 'a aexp * 'a
| AE_return of 'a aval * 'a
| AE_throw of 'a aval * 'a
| AE_if of 'a aval * 'a aexp * 'a aexp * 'a
| AE_field of 'a aval * id * 'a
| AE_case of 'a aval * ('a apat * 'a aexp * 'a aexp) list * 'a
| AE_try of 'a aexp * ('a apat * 'a aexp * 'a aexp) list * 'a
| AE_record_update of 'a aval * ('a aval) Bindings.t * 'a
| AE_for of id * 'a aexp * 'a aexp * 'a aexp * order * 'a aexp
| AE_loop of loop * 'a aexp * 'a aexp
| AE_short_circuit of sc_op * 'a aval * 'a aexp
and sc_op = SC_and | SC_or
and 'a apat = AP_aux of 'a apat_aux * Env.t * l
and 'a apat_aux =
| AP_tup of ('a apat) list
| AP_id of id * 'a
| AP_global of id * 'a
| AP_app of id * 'a apat * 'a
| AP_cons of 'a apat * 'a apat
| AP_as of 'a apat * id * 'a
| AP_nil of 'a
| AP_wild of 'a
(** We allow ANF->ANF optimization to insert fragments of C code
directly in the ANF grammar via [AV_cval]. Such fragments
must be side-effect free expressions. *)
and 'a aval =
| AV_lit of lit * 'a
| AV_id of id * 'a lvar
| AV_ref of id * 'a lvar
| AV_tuple of ('a aval) list
| AV_list of ('a aval) list * 'a
| AV_vector of ('a aval) list * 'a
| AV_record of ('a aval) Bindings.t * 'a
| AV_cval of cval * 'a
and 'a alexp =
| AL_id of id * 'a
| AL_addr of id * 'a
| AL_field of 'a alexp * id
(** When ANF translation has to introduce new bindings it uses a
counter to ensure uniqueness. This function resets that counter. *)
val reset_anf_counter : unit -> unit
val aexp_loc : 'a aexp -> Parse_ast.l
(** {2 Functions for transforming ANF expressions} *)
val aval_typ : typ aval -> typ
val aexp_typ : typ aexp -> typ
(** Map over all values in an ANF expression *)
val map_aval : (Env.t -> Ast.l -> 'a aval -> 'a aval) -> 'a aexp -> 'a aexp
(** Map over all function calls in an ANF expression *)
val map_functions : (Env.t -> Ast.l -> id -> ('a aval) list -> 'a -> 'a aexp_aux) -> 'a aexp -> 'a aexp
val fold_aexp : ('a aexp -> 'a aexp) -> 'a aexp -> 'a aexp
val aexp_bindings : 'a aexp -> IdSet.t
(** Remove all variable shadowing in an ANF expression *)
val no_shadow : IdSet.t -> 'a aexp -> 'a aexp
val apat_globals : 'a apat -> (id * 'a) list
val apat_types : 'a apat -> 'a Bindings.t
(** Returns true if an ANF expression is dead due to flow typing
implying it is unreachable. Note: This function calls SMT. *)
val is_dead_aexp : 'a aexp -> bool
(** {2 Compiling to ANF expressions} *)
val anf_pat : ?global:bool -> tannot pat -> typ apat
val anf : tannot exp -> typ aexp
(** {2 Pretty printing ANF expressions} *)
val pp_aval : typ aval -> PPrint.document
val pp_aexp : typ aexp -> PPrint.document
|
