diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-23 08:54:56 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-23 08:54:56 +0000 |
commit | 2a0168fea37b68ad14e2cb60bf215111e49d4870 (patch) | |
tree | 2f59373790d8ce3a5df66ef7a692271cf0666c6c /backend/CMtypecheck.ml | |
parent | 00805153cf9b88aa07cc6694b17d93f5ba2e7de8 (diff) | |
download | compcert-2a0168fea37b68ad14e2cb60bf215111e49d4870.tar.gz compcert-2a0168fea37b68ad14e2cb60bf215111e49d4870.zip |
Merge of "newspilling" branch:
- Support single-precision floats as first-class values
- Introduce chunks Many32, Many64 and types Tany32, Tany64 to
support saving and restoring registers without knowing
the exact types (int/single/float) of their contents, just
their sizes.
- Memory model: generalize the opaque encoding of pointers to
apply to any value, not just pointers, if chunks Many32/Many64
are selected.
- More properties of FP arithmetic proved.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/CMtypecheck.ml')
-rw-r--r-- | backend/CMtypecheck.ml | 27 |
1 files changed, 24 insertions, 3 deletions
diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml index 5e46d769..02c3f210 100644 --- a/backend/CMtypecheck.ml +++ b/backend/CMtypecheck.ml @@ -34,12 +34,16 @@ let tint = Base Tint let tfloat = Base Tfloat let tlong = Base Tlong let tsingle = Base Tsingle +let tany32 = Base Tany32 +let tany64 = Base Tany64 let ty_of_typ = function | Tint -> tint | Tfloat -> tfloat | Tlong -> tlong - | Tsingle -> tfloat (* should be tsingle when supported *) + | Tsingle -> tsingle + | Tany32 -> tany32 + | Tany64 -> tany64 let ty_of_sig_args tyl = List.map ty_of_typ tyl @@ -88,6 +92,7 @@ let name_of_comparison = function let type_constant = function | Ointconst _ -> tint | Ofloatconst _ -> tfloat + | Osingleconst _ -> tsingle | Olongconst _ -> tlong | Oaddrsymbol _ -> tint | Oaddrstack _ -> tint @@ -101,11 +106,18 @@ let type_unary_operation = function | Onotint -> tint, tint | Onegf -> tfloat, tfloat | Oabsf -> tfloat, tfloat - | Osingleoffloat -> tfloat, tfloat + | Onegfs -> tsingle, tsingle + | Oabsfs -> tsingle, tsingle + | Osingleoffloat -> tfloat, tsingle + | Ofloatofsingle -> tsingle, tfloat | Ointoffloat -> tfloat, tint | Ointuoffloat -> tfloat, tint | Ofloatofint -> tint, tfloat | Ofloatofintu -> tint, tfloat + | Ointofsingle -> tsingle, tint + | Ointuofsingle -> tsingle, tint + | Osingleofint -> tint, tsingle + | Osingleofintu -> tint, tsingle | Onegl -> tlong, tlong | Onotl -> tlong, tlong | Ointoflong -> tlong, tint @@ -115,6 +127,8 @@ let type_unary_operation = function | Olonguoffloat -> tfloat, tlong | Ofloatoflong -> tlong, tfloat | Ofloatoflongu -> tlong, tfloat + | Olongofsingle -> tsingle, tlong + | Olonguofsingle -> tsingle, tlong | Osingleoflong -> tlong, tfloat | Osingleoflongu -> tlong, tfloat @@ -136,6 +150,10 @@ let type_binary_operation = function | Osubf -> tfloat, tfloat, tfloat | Omulf -> tfloat, tfloat, tfloat | Odivf -> tfloat, tfloat, tfloat + | Oaddfs -> tsingle, tsingle, tsingle + | Osubfs -> tsingle, tsingle, tsingle + | Omulfs -> tsingle, tsingle, tsingle + | Odivfs -> tsingle, tsingle, tsingle | Oaddl -> tlong, tlong, tlong | Osubl -> tlong, tlong, tlong | Omull -> tlong, tlong, tlong @@ -152,6 +170,7 @@ let type_binary_operation = function | Ocmp _ -> tint, tint, tint | Ocmpu _ -> tint, tint, tint | Ocmpf _ -> tfloat, tfloat, tint + | Ocmpfs _ -> tsingle, tsingle, tint | Ocmpl _ -> tlong, tlong, tint | Ocmplu _ -> tlong, tlong, tint @@ -166,8 +185,10 @@ let type_chunk = function | Mint16unsigned -> tint | Mint32 -> tint | Mint64 -> tlong - | Mfloat32 -> tfloat + | Mfloat32 -> tsingle | Mfloat64 -> tfloat + | Many32 -> tany32 + | Many64 -> tany64 let name_of_chunk = PrintAST.name_of_chunk |