diff options
author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2015-08-17 13:43:02 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2015-08-17 13:43:02 +0200 |
commit | 2c2fca9756e38535db7697c6f53126003b624c6c (patch) | |
tree | 2ecde0a9f5720b8a3bc3bb70eaa80caa37fca37e /backend | |
parent | 4d70c9820f5b840cfd7870395673723a3151e525 (diff) | |
parent | cc8d02d23cc70c42612a37f4cac8452514e9d873 (diff) | |
download | compcert-2c2fca9756e38535db7697c6f53126003b624c6c.tar.gz compcert-2c2fca9756e38535db7697c6f53126003b624c6c.zip |
Merge pull request #46 from AbsInt/asmexpand
Merge branch 'asmexpand' of github.com:AbsInt/CompCert
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Asmexpandaux.ml | 57 |
1 files changed, 57 insertions, 0 deletions
diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml new file mode 100644 index 00000000..6ce6c005 --- /dev/null +++ b/backend/Asmexpandaux.ml @@ -0,0 +1,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} |