diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-20 07:54:52 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-20 07:54:52 +0000 |
commit | 255cee09b71255051c2b40eae0c88bffce1f6f32 (patch) | |
tree | 7951b1b13e8fd5e525b9223e8be0580e83550f55 /backend/CMtypecheck.ml | |
parent | 6e5041958df01c56762e90770abd704b95a36e5d (diff) | |
download | compcert-255cee09b71255051c2b40eae0c88bffce1f6f32.tar.gz compcert-255cee09b71255051c2b40eae0c88bffce1f6f32.zip |
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
Diffstat (limited to 'backend/CMtypecheck.ml')
-rw-r--r-- | backend/CMtypecheck.ml | 84 |
1 files changed, 32 insertions, 52 deletions
diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml index 39e8c517..1a19f710 100644 --- a/backend/CMtypecheck.ml +++ b/backend/CMtypecheck.ml @@ -24,15 +24,16 @@ open Cminor exception Error of string -let name_of_typ = function Tint -> "int" | Tfloat -> "float" +let name_of_typ = function Tint -> "int" | Tfloat -> "float" | Tlong -> "long" type ty = Base of typ | Var of ty option ref let newvar () = Var (ref None) let tint = Base Tint let tfloat = Base Tfloat +let tlong = Base Tlong -let ty_of_typ = function Tint -> tint | Tfloat -> tfloat +let ty_of_typ = function Tint -> tint | Tfloat -> tfloat | Tlong -> tlong let ty_of_sig_args tyl = List.map ty_of_typ tyl @@ -81,6 +82,7 @@ let name_of_comparison = function let type_constant = function | Ointconst _ -> tint | Ofloatconst _ -> tfloat + | Olongconst _ -> tlong | Oaddrsymbol _ -> tint | Oaddrstack _ -> tint @@ -98,6 +100,15 @@ let type_unary_operation = function | Ointuoffloat -> tfloat, tint | Ofloatofint -> tint, tfloat | Ofloatofintu -> tint, tfloat + | Onegl -> tlong, tlong + | Onotl -> tlong, tlong + | Ointoflong -> tlong, tint + | Olongofint -> tint, tlong + | Olongofintu -> tint, tlong + | Olongoffloat -> tfloat, tlong + | Olonguoffloat -> tfloat, tlong + | Ofloatoflong -> tlong, tfloat + | Ofloatoflongu -> tlong, tfloat let type_binary_operation = function | Oadd -> tint, tint, tint @@ -117,52 +128,28 @@ let type_binary_operation = function | Osubf -> tfloat, tfloat, tfloat | Omulf -> tfloat, tfloat, tfloat | Odivf -> tfloat, tfloat, tfloat + | Oaddl -> tlong, tlong, tlong + | Osubl -> tlong, tlong, tlong + | Omull -> tlong, tlong, tlong + | Odivl -> tlong, tlong, tlong + | Odivlu -> tlong, tlong, tlong + | Omodl -> tlong, tlong, tlong + | Omodlu -> tlong, tlong, tlong + | Oandl -> tlong, tlong, tlong + | Oorl -> tlong, tlong, tlong + | Oxorl -> tlong, tlong, tlong + | Oshll -> tlong, tint, tlong + | Oshrl -> tlong, tint, tlong + | Oshrlu -> tlong, tint, tlong | Ocmp _ -> tint, tint, tint | Ocmpu _ -> tint, tint, tint | Ocmpf _ -> tfloat, tfloat, tint + | Ocmpl _ -> tlong, tlong, tint + | Ocmplu _ -> tlong, tlong, tint -let name_of_constant = function - | Ointconst n -> sprintf "intconst %ld" (camlint_of_coqint n) - | Ofloatconst n -> sprintf "floatconst %g" (camlfloat_of_coqfloat n) - | Oaddrsymbol (s, ofs) -> sprintf "addrsymbol %s %ld" (extern_atom s) (camlint_of_coqint ofs) - | Oaddrstack n -> sprintf "addrstack %ld" (camlint_of_coqint n) +let name_of_unary_operation = PrintCminor.name_of_unop -let name_of_unary_operation = function - | Ocast8signed -> "cast8signed" - | Ocast16signed -> "cast16signed" - | Ocast8unsigned -> "cast8unsigned" - | Ocast16unsigned -> "cast16unsigned" - | Onegint -> "negint" - | Onotint -> "notint" - | Onegf -> "negf" - | Oabsf -> "absf" - | Osingleoffloat -> "singleoffloat" - | Ointoffloat -> "intoffloat" - | Ointuoffloat -> "intuoffloat" - | Ofloatofint -> "floatofint" - | Ofloatofintu -> "floatofintu" - -let name_of_binary_operation = function - | Oadd -> "add" - | Osub -> "sub" - | Omul -> "mul" - | Odiv -> "div" - | Odivu -> "divu" - | Omod -> "mod" - | Omodu -> "modu" - | Oand -> "and" - | Oor -> "or" - | Oxor -> "xor" - | Oshl -> "shl" - | Oshr -> "shr" - | Oshru -> "shru" - | Oaddf -> "addf" - | Osubf -> "subf" - | Omulf -> "mulf" - | Odivf -> "divf" - | Ocmp c -> sprintf "cmp %s" (name_of_comparison c) - | Ocmpu c -> sprintf "cmpu %s" (name_of_comparison c) - | Ocmpf c -> sprintf "cmpf %s" (name_of_comparison c) +let name_of_binary_operation = PrintCminor.name_of_binop let type_chunk = function | Mint8signed -> tint @@ -170,19 +157,12 @@ let type_chunk = function | Mint16signed -> tint | Mint16unsigned -> tint | Mint32 -> tint + | Mint64 -> tlong | Mfloat32 -> tfloat | Mfloat64 -> tfloat | Mfloat64al32 -> tfloat -let name_of_chunk = function - | Mint8signed -> "int8signed" - | Mint8unsigned -> "int8unsigned" - | Mint16signed -> "int16signed" - | Mint16unsigned -> "int16unsigned" - | Mint32 -> "int32" - | Mfloat32 -> "float32" - | Mfloat64 -> "float64" - | Mfloat64al32 -> "float64al32" +let name_of_chunk = PrintAST.name_of_chunk let rec type_expr env lenv e = match e with |