From ddbfd93736af813807b131deea229597f30a8463 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Tue, 28 Oct 2014 18:42:21 +0100
Subject: Refactored the printing functions a little bit more by moving the
 system dependent parts into other modules and some of the functions into a
 util file.

---
 powerpc/PrintDiab.ml | 98 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 98 insertions(+)
 create mode 100644 powerpc/PrintDiab.ml

(limited to 'powerpc/PrintDiab.ml')

diff --git a/powerpc/PrintDiab.ml b/powerpc/PrintDiab.ml
new file mode 100644
index 00000000..2f4da2ee
--- /dev/null
+++ b/powerpc/PrintDiab.ml
@@ -0,0 +1,98 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* The Diab specific printing functions *)
+
+open Printf
+open Datatypes
+open Camlcoq
+open Sections
+open Asm
+open PrintUtil
+
+
+    
+module Diab_System =
+  (struct
+    let comment =  ";"
+        
+    let constant oc cst =
+      match cst with
+      | Cint n ->
+          fprintf oc "%ld" (camlint_of_coqint n)
+      | Csymbol_low(s, n) ->
+          symbol_fragment oc s n "@l"
+      | Csymbol_high(s, n) ->
+          symbol_fragment oc s n "@ha"
+      | Csymbol_sda(s, n) ->
+          symbol_fragment oc s n "@sdarx"
+      | Csymbol_rel_low(s, n) ->
+          symbol_fragment oc s n "@sdax@l"
+      | Csymbol_rel_high(s, n) ->
+          symbol_fragment oc s n "@sdarx@ha"
+ 
+    let ireg oc r =
+      output_char oc 'r';
+      output_string oc (int_reg_name r)
+
+    let freg oc r =
+      output_char oc 'f';
+      output_string oc (float_reg_name r)
+        
+    let creg oc r =
+      fprintf oc "cr%d" r
+        
+    let name_of_section = function
+      | Section_text -> ".text"
+      | Section_data i -> if i then ".data" else ".bss"
+      | Section_small_data i -> if i then ".sdata" else ".sbss"
+      | Section_const -> ".text"
+      | Section_small_const -> ".sdata2"
+      | Section_string -> ".text"
+      | Section_literal -> ".text"
+      | Section_jumptable -> ".text"
+      | Section_user(s, wr, ex) ->
+          sprintf ".section	\"%s\",,%c"
+               s
+            (match wr, ex with
+            | true, true -> 'm'                 (* text+data *)
+            | true, false -> 'd'                (* data *)
+            | false, true -> 'c'                (* text *)
+            | false, false -> 'r')              (* const *)
+
+    let last_file = ref ""
+    let reset_file_line () = last_file := ""
+    let print_file_line oc file line =
+      if !Clflags.option_g && file <> "" then begin
+        if file <> !last_file then begin
+          fprintf oc "	.d1file	%S\n" file;
+          last_file := file
+        end;
+        fprintf oc "	.d1line	%s\n" line
+      end
+
+    (* Emit .cfi directives *)
+    let cfi_startproc oc = ()
+
+    let cfi_endproc oc = ()
+
+    let cfi_adjust oc delta = ()
+
+    let cfi_rel_offset oc reg ofs = ()
+
+        
+    let print_prologue oc =
+      fprintf oc "	.xopt	align-fill-text=0x60000000\n";
+      if !Clflags.option_g then
+        fprintf oc "	.xopt	asm-debug-on\n"
+  
+  end:SYSTEM)
-- 
cgit