From 929c0ea6f02713f59c0862fa0c3a53e0cb89c334 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 10 Jun 2015 10:07:02 +0200 Subject: Moved the printing of the builtin functions etc. into Asmexpand for ARM in the same way as it is done for PPC. --- backend/Asmexpandaux.ml | 57 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) create mode 100644 backend/Asmexpandaux.ml (limited to 'backend/Asmexpandaux.ml') 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} -- cgit