From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 20 Apr 2013 07:54:52 +0000
Subject: Big merge of the newregalloc-int64 branch.  Lots of changes in two
 directions: 1- new register allocator (+ live range splitting,
 spilling&reloading, etc)    based on a posteriori validation using the
 Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long
 long").

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 exportclight/Clightdefs.v    |  3 +++
 exportclight/ExportClight.ml | 20 +++++++++++++++++++-
 2 files changed, 22 insertions(+), 1 deletion(-)

(limited to 'exportclight')

diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v
index 4c3c942..1cb93d5 100644
--- a/exportclight/Clightdefs.v
+++ b/exportclight/Clightdefs.v
@@ -32,6 +32,8 @@ Definition tushort := Tint I16 Unsigned noattr.
 Definition tint := Tint I32 Signed noattr.
 Definition tuint := Tint I32 Unsigned noattr.
 Definition tbool := Tint IBool Unsigned noattr.
+Definition tlong := Tlong Signed noattr.
+Definition tulong := Tlong Unsigned noattr.
 Definition tfloat := Tfloat F32 noattr.
 Definition tdouble := Tfloat F64 noattr.
 Definition tptr (t: type) := Tpointer t noattr.
@@ -43,6 +45,7 @@ Definition tvolatile (ty: type) :=
   match ty with
   | Tvoid => Tvoid
   | Tint sz si a => Tint sz si volatile_attr
+  | Tlong si a => Tlong si volatile_attr
   | Tfloat sz a => Tfloat sz volatile_attr
   | Tpointer elt a => Tpointer elt volatile_attr
   | Tarray elt sz a => Tarray elt sz volatile_attr
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index ef00512..04f170d 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -92,6 +92,12 @@ let coqfloat p n =
   then fprintf p "(Float.double_of_bits (Int64.repr %Ld))" n
   else fprintf p "(Float.double_of_bits (Int64.repr (%Ld)))" n
 
+let coqint64 p n =
+  let n = camlint64_of_coqint n in
+  if n >= 0L
+  then fprintf p "(Int64.repr %Ld)" n
+  else fprintf p "(Int64.repr (%Ld))" n
+
 (* Types *)
 
 let use_struct_names = ref true
@@ -114,6 +120,11 @@ and rtyp p = function
         | I32, Signed -> "tint"
         | I32, Unsigned -> "tuint"
         | IBool, _ -> "tbool")
+  | Tlong(sg, _) ->
+      fprintf p "%s" (
+        match sg with
+        | Signed -> "tlong"
+        | Unsigned -> "tulong")
   | Tfloat(sz, _) ->
       fprintf p "%s" (
         match sz with
@@ -151,7 +162,8 @@ and fieldlist p = function
 (* External functions *)
 
 let asttype p t =
-  fprintf p "%s" (match t with AST.Tint -> "AST.Tint" | AST.Tfloat -> "AST.Tfloat")
+  fprintf p "%s"
+     (match t with AST.Tint -> "AST.Tint" | AST.Tfloat -> "AST.Tfloat" | AST.Tlong -> "AST.Tlong")
 
 let name_of_chunk = function
   | Mint8signed -> "Mint8signed"
@@ -159,6 +171,7 @@ let name_of_chunk = function
   | Mint16signed -> "Mint16signed"
   | Mint16unsigned -> "Mint16unsigned"
   | Mint32 -> "Mint32"
+  | Mint64 -> "Mint64"
   | Mfloat32 -> "Mfloat32"
   | Mfloat64 -> "Mfloat64"
   | Mfloat64al32 -> "Mfloat64al32"
@@ -240,6 +253,8 @@ let rec expr p = function
       fprintf p "(Econst_int %a %a)" coqint n typ t
   | Econst_float(n, t) ->
       fprintf p "(Econst_float %a %a)" coqfloat n typ t
+  | Econst_long(n, t) ->
+      fprintf p "(Econst_long %a %a)" coqint64 n typ t
   | Eunop(op, a1, t) ->
       fprintf p "@[<hov 2>(Eunop %s@ %a@ %a)@]"
          (name_unop op) expr a1 typ t
@@ -316,6 +331,7 @@ let init_data p = function
   | Init_int8 n -> fprintf p "Init_int8 %a" coqint n
   | Init_int16 n -> fprintf p "Init_int16 %a" coqint n
   | Init_int32 n -> fprintf p "Init_int32 %a" coqint n
+  | Init_int64 n -> fprintf p "Init_int64 %a" coqint64 n
   | Init_float32 n -> fprintf p "Init_float32 %a" coqfloat n
   | Init_float64 n -> fprintf p "Init_float64 %a" coqfloat n
   | Init_space n -> fprintf p "Init_space %ld" (Z.to_int32 n)
@@ -359,6 +375,7 @@ let register_struct_union ty =
 let rec collect_type = function
   | Tvoid -> ()
   | Tint _ -> ()
+  | Tlong _ -> ()
   | Tfloat _ -> ()
   | Tpointer(t, _) -> collect_type t
   | Tarray(t, _, _) -> collect_type t
@@ -382,6 +399,7 @@ let rec collect_expr e =
   match e with
   | Econst_int _ -> ()
   | Econst_float _ -> ()
+  | Econst_long _ -> ()
   | Evar _ -> ()
   | Etempvar _ -> ()
   | Ederef(r, _) -> collect_expr r
-- 
cgit v1.2.3