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
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
|
(**************************************************************************)
(* 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. *)
(**************************************************************************)
open Ast
open Ast_defs
open Ast_util
open Type_check
open Rewriter
(* Unroll mutually recursive calls, starting with the functions given as
targets on the command line, by looking for recursive calls with (some)
constant arguments, and creating copies of those functions with the
constants propagated in. This may cause branches with mutually recursively
calls to disappear, breaking the mutually recursive cycle. *)
let targets = ref ([] : id list)
let rec is_const_exp exp = match unaux_exp exp with
| E_lit (L_aux ((L_true | L_false | L_one | L_zero | L_num _), _)) -> true
| E_vector es -> List.for_all is_const_exp es && is_bitvector_typ (typ_of exp)
| E_record fes -> List.for_all is_const_fexp fes
| _ -> false
and is_const_fexp (FE_aux (FE_Fexp (_, e), _)) = is_const_exp e
let recheck_exp exp = check_exp (env_of exp) (strip_exp exp) (typ_of exp)
(* Name function copy by encoding values of constant arguments *)
let generate_fun_id id args =
let rec suffix exp = match unaux_exp exp with
| E_lit (L_aux (L_one, _)) -> "1"
| E_lit (L_aux (L_zero, _)) -> "0"
| E_lit (L_aux (L_true, _)) -> "T"
| E_lit (L_aux (L_false, _)) -> "F"
| E_record fes when is_const_exp exp ->
let fsuffix (FE_aux (FE_Fexp (id, e), _)) = suffix e
in
"struct" ^
Util.zencode_string (string_of_typ (typ_of exp)) ^
"#" ^
String.concat "" (List.map fsuffix fes)
| E_vector es when is_const_exp exp ->
String.concat "" (List.map suffix es)
| _ ->
if is_const_exp exp
then "#" ^ Util.zencode_string (string_of_exp exp)
else "v"
in
append_id id ("#mutrec_" ^ String.concat "" (List.map suffix args))
(* Generate a val spec for a function copy, removing the constant arguments
that will be propagated in *)
let generate_val_spec env id args l annot =
match Env.get_val_spec_orig id env with
| tq, (Typ_aux (Typ_fn (arg_typs, ret_typ, eff), _) as fn_typ) ->
(* Get instantiation of type variables at call site *)
let orig_ksubst (kid, typ_arg) =
match typ_arg with
| A_aux ((A_nexp _ | A_bool _), _) -> (orig_kid kid, typ_arg)
| _ -> raise (Reporting.err_todo l "Propagation of polymorphic arguments not implemented")
in
let ksubsts =
recheck_exp (E_aux (E_app (id, args), (l, annot)))
|> instantiation_of
|> KBindings.bindings
|> List.map orig_ksubst
|> List.fold_left (fun s (v,i) -> KBindings.add v i s) KBindings.empty
in
(* Apply instantiation to original function type. Also collect the
type variables in the new type together their kinds for the new
val spec. *)
let kopts_of_typ env typ =
tyvars_of_typ typ |> KidSet.elements
|> List.map (fun kid -> mk_kopt (Env.get_typ_var kid env) kid)
|> KOptSet.of_list
in
let ret_typ' = KBindings.fold typ_subst ksubsts ret_typ in
let (arg_typs', kopts') =
List.fold_right2 (fun arg typ (arg_typs', kopts') ->
if is_const_exp arg then
(arg_typs', kopts')
else
let typ' = KBindings.fold typ_subst ksubsts typ in
let arg_kopts = kopts_of_typ (env_of arg) typ' in
(typ' :: arg_typs', KOptSet.union arg_kopts kopts'))
args arg_typs ([], kopts_of_typ (env_of_tannot annot) ret_typ')
in
let arg_typs' = if arg_typs' = [] then [unit_typ] else arg_typs' in
let typ' = mk_typ (Typ_fn (arg_typs', ret_typ', eff)) in
(* Construct new val spec *)
let constraints' =
quant_split tq |> snd
|> List.map (KBindings.fold constraint_subst ksubsts)
|> List.filter (fun nc -> KidSet.subset (tyvars_of_constraint nc) (tyvars_of_typ typ'))
in
let quant_items' =
List.map mk_qi_kopt (KOptSet.elements kopts') @
List.map mk_qi_nc constraints'
in
let typschm = mk_typschm (mk_typquant quant_items') typ' in
mk_val_spec (VS_val_spec (typschm, generate_fun_id id args, [], false)),
ksubsts
| _, Typ_aux (_, l) ->
raise (Reporting.err_unreachable l __POS__ "Function val spec is not a function type")
let const_prop target defs substs ksubsts exp =
(* Constant_propagation currently only supports nexps for kid substitutions *)
let nexp_substs =
KBindings.bindings ksubsts
|> List.map (function (kid, A_aux (A_nexp n, _)) -> [(kid, n)] | _ -> [])
|> List.concat
|> List.fold_left (fun s (v,i) -> KBindings.add v i s) KBindings.empty
in
Constant_propagation.const_prop
target
defs
(Constant_propagation.referenced_vars exp)
(substs, nexp_substs)
Bindings.empty
exp
|> fst
(* Propagate constant arguments into function clause pexp *)
let prop_args_pexp target ast ksubsts args pexp =
let pat, guard, exp, annot = destruct_pexp pexp in
let pats = match pat with
| P_aux (P_tup pats, _) -> pats
| _ -> [pat]
in
let match_arg (E_aux (_, (l, _)) as arg) pat (pats, substs) =
if is_const_exp arg then
match pat with
| P_aux (P_id id, _) -> (pats, Bindings.add id arg substs)
| _ ->
raise (Reporting.err_todo l
("Unsupported pattern match in propagation of constant arguments: " ^
string_of_exp arg ^ " and " ^ string_of_pat pat))
else (pat :: pats, substs)
in
let pats, substs = List.fold_right2 match_arg args pats ([], Bindings.empty) in
let exp' = const_prop target ast substs ksubsts exp in
let pat' = match pats with
| [pat] -> pat
| _ -> P_aux (P_tup pats, (Parse_ast.Unknown, empty_tannot))
in
construct_pexp (pat', guard, exp', annot)
let rewrite_ast target env ({ defs; _ } as ast) =
let rec rewrite = function
| [] -> []
| DEF_internal_mutrec mutrecs :: ds ->
let mutrec_ids = IdSet.of_list (List.map id_of_fundef mutrecs) in
let valspecs = ref ([] : unit def list) in
let fundefs = ref ([] : unit def list) in
(* Try to replace mutually recursive calls that have some constant arguments *)
let rec e_app (id, args) (l, annot) =
if IdSet.mem id mutrec_ids && List.exists is_const_exp args then
let id' = generate_fun_id id args in
let args' = match List.filter (fun e -> not (is_const_exp e)) args with
| [] -> [infer_exp env (mk_lit_exp L_unit)]
| args' -> args'
in
if not (IdSet.mem id' (ids_of_defs !valspecs)) then begin
(* Generate copy of function with constant arguments propagated in *)
let (FD_aux (FD_function (_, _, _, fcls), _)) =
List.find (fun fd -> Id.compare id (id_of_fundef fd) = 0) mutrecs
in
let valspec, ksubsts = generate_val_spec env id args l annot in
let const_prop_funcl (FCL_aux (FCL_Funcl (_, pexp), (l, _))) =
let pexp' =
prop_args_pexp target ast ksubsts args pexp
|> rewrite_pexp
|> strip_pexp
in
FCL_aux (FCL_Funcl (id', pexp'), (Parse_ast.Generated l, ()))
in
valspecs := valspec :: !valspecs;
let fundef = mk_fundef (List.map const_prop_funcl fcls) in
fundefs := fundef :: !fundefs
end else ();
E_aux (E_app (id', args'), (l, annot))
else E_aux (E_app (id, args), (l, annot))
and e_aux (e, (l, annot)) =
match e with
| E_app (id, args) -> e_app (id, args) (l, annot)
| _ -> E_aux (e, (l, annot))
and rewrite_pexp pexp = fold_pexp { id_exp_alg with e_aux = e_aux } pexp
and rewrite_funcl (FCL_aux (FCL_Funcl (id, pexp), a) as funcl) =
let pexp' =
if List.exists (fun id' -> Id.compare id id' = 0) !targets then
let pat, guard, body, annot = destruct_pexp pexp in
let body' = const_prop target ast Bindings.empty KBindings.empty body in
rewrite_pexp (construct_pexp (pat, guard, recheck_exp body', annot))
else pexp
in FCL_aux (FCL_Funcl (id, pexp'), a)
and rewrite_fundef (FD_aux (FD_function (ropt, topt, eopt, fcls), a)) =
let fcls' = List.map rewrite_funcl fcls in
FD_aux (FD_function (ropt, topt, eopt, fcls'), a)
in
let mutrecs' = List.map (fun fd -> DEF_fundef (rewrite_fundef fd)) mutrecs in
let fdefs = fst (check_defs env (!valspecs @ !fundefs)) in
mutrecs' @ fdefs @ rewrite ds
| d :: ds ->
d :: rewrite ds
in
Spec_analysis.top_sort_defs { ast with defs = rewrite defs }
|
