blob: 6ce6c0056eae4ed3c940e6d0ad0dcb29100f15b2 (
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
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(* Util functions used for the expansion of built-ins and some
pseudo-instructions *)
open Asm
open AST
open Camlcoq
(* Buffering the expanded code *)
let current_code = ref ([]: instruction list)
let emit i = current_code := i :: !current_code
(* Generation of fresh labels *)
let dummy_function = { fn_code = []; fn_sig = signature_main }
let current_function = ref dummy_function
let next_label = ref (None: label option)
let new_label () =
let lbl =
match !next_label with
| Some l -> l
| None ->
(* on-demand computation of the next available label *)
List.fold_left
(fun next instr ->
match instr with
| Plabel l -> if P.lt l next then next else P.succ l
| _ -> next)
P.one (!current_function).fn_code
in
next_label := Some (P.succ lbl);
lbl
let set_current_function f =
current_function := f; next_label := None; current_code := []
let get_current_function () =
let c = List.rev !current_code in
let fn = !current_function in
set_current_function dummy_function;
{fn with fn_code = c}
|
