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 /arm/SelectOp.vp | |
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 'arm/SelectOp.vp')
-rw-r--r-- | arm/SelectOp.vp | 34 |
1 files changed, 32 insertions, 2 deletions
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index e4005c92..ad8a9454 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -321,6 +321,12 @@ Definition addf (e1 e2: expr) := Eop Oaddf (e1 ::: e2 ::: Enil). Definition subf (e1 e2: expr) := Eop Osubf (e1 ::: e2 ::: Enil). Definition mulf (e1 e2: expr) := Eop Omulf (e1 ::: e2 ::: Enil). +Definition negfs (e: expr) := Eop Onegfs (e ::: Enil). +Definition absfs (e: expr) := Eop Oabsfs (e ::: Enil). +Definition addfs (e1 e2: expr) := Eop Oaddfs (e1 ::: e2 ::: Enil). +Definition subfs (e1 e2: expr) := Eop Osubfs (e1 ::: e2 ::: Enil). +Definition mulfs (e1 e2: expr) := Eop Omulfs (e1 ::: e2 ::: Enil). + (** ** Comparisons *) Nondetfunction compimm (default: comparison -> int -> condition) @@ -370,6 +376,9 @@ Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) := Definition compf (c: comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). +Definition compfs (c: comparison) (e1: expr) (e2: expr) := + Eop (Ocmp (Ccompfs c)) (e1 ::: e2 ::: Enil). + (** ** Integer conversions *) Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e. @@ -391,21 +400,38 @@ Nondetfunction cast16signed (e: expr) := (** ** Floating-point conversions *) Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil). +Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil). + Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). Definition intuoffloat (e: expr) := Eop Ointuoffloat (e ::: Enil). Nondetfunction floatofint (e: expr) := match e with - | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.floatofint n)) Enil + | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_int n)) Enil | _ => Eop Ofloatofint (e ::: Enil) end. Nondetfunction floatofintu (e: expr) := match e with - | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.floatofintu n)) Enil + | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_intu n)) Enil | _ => Eop Ofloatofintu (e ::: Enil) end. +Definition intofsingle (e: expr) := Eop Ointofsingle (e ::: Enil). +Definition intuofsingle (e: expr) := Eop Ointuofsingle (e ::: Enil). + +Nondetfunction singleofint (e: expr) := + match e with + | Eop (Ointconst n) Enil => Eop (Osingleconst (Float32.of_int n)) Enil + | _ => Eop Osingleofint (e ::: Enil) + end. + +Nondetfunction singleofintu (e: expr) := + match e with + | Eop (Ointconst n) Enil => Eop (Osingleconst (Float32.of_intu n)) Enil + | _ => Eop Osingleofintu (e ::: Enil) + end. + (** ** Recognition of addressing modes for load and store operations *) (** We do not recognize the [Aindexed2] and [Aindexed2shift] modes @@ -424,6 +450,8 @@ Definition can_use_Aindexed2 (chunk: memory_chunk): bool := | Mint64 => false | Mfloat32 => false | Mfloat64 => false + | Many32 => true + | Many64 => false end. Definition can_use_Aindexed2shift (chunk: memory_chunk): bool := @@ -436,6 +464,8 @@ Definition can_use_Aindexed2shift (chunk: memory_chunk): bool := | Mint64 => false | Mfloat32 => false | Mfloat64 => false + | Many32 => true + | Many64 => false end. Nondetfunction addressing (chunk: memory_chunk) (e: expr) := |