diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-01 17:26:46 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-01 17:26:46 +0200 |
| commit | 3bef0962079cf971673b4267b0142bd5fe092509 (patch) | |
| tree | 6dd283fa6b8305d960fd08938fbbd09e0940c139 /powerpc/SelectOp.vp | |
| parent | e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c (diff) | |
| download | compcert-kvx-3bef0962079cf971673b4267b0142bd5fe092509.tar.gz compcert-kvx-3bef0962079cf971673b4267b0142bd5fe092509.zip | |
Support for 64-bit architectures: update the PowerPC port
The PowerPC port remains 32-bit only, no support is added for PPC 64.
This shows how much work is needed to update an existing port a minima.
Diffstat (limited to 'powerpc/SelectOp.vp')
| -rw-r--r-- | powerpc/SelectOp.vp | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index a1fcecc7..79f05295 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -48,10 +48,10 @@ Open Local Scope cminorsel_scope. (** ** Constants **) -Definition addrsymbol (id: ident) (ofs: int) := +Definition addrsymbol (id: ident) (ofs: ptrofs) := Eop (Oaddrsymbol id ofs) Enil. -Definition addrstack (ofs: int) := +Definition addrstack (ofs: ptrofs) := Eop (Oaddrstack ofs) Enil. (** ** Integer logical negation *) @@ -78,17 +78,17 @@ Nondetfunction addimm (n: int) (e: expr) := if Int.eq n Int.zero then e else match e with | Eop (Ointconst m) Enil => Eop (Ointconst(Int.add n m)) Enil - | Eop (Oaddrsymbol s m) Enil => Eop (Oaddrsymbol s (Int.add n m)) Enil - | Eop (Oaddrstack m) Enil => Eop (Oaddrstack (Int.add n m)) Enil + | Eop (Oaddrsymbol s m) Enil => Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int n) m)) Enil + | Eop (Oaddrstack m) Enil => Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n) m)) Enil | Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil) - | Eop (Oaddsymbol s m) (t ::: Enil) => Eop (Oaddsymbol s (Int.add n m)) (t ::: Enil) + | Eop (Oaddsymbol s m) (t ::: Enil) => Eop (Oaddsymbol s (Ptrofs.add (Ptrofs.of_int n) m)) (t ::: Enil) | _ => Eop (Oaddimm n) (e ::: Enil) end. -Nondetfunction addsymbol (s: ident) (ofs: int) (e: expr) := +Nondetfunction addsymbol (s: ident) (ofs: ptrofs) (e: expr) := match e with - | Eop (Ointconst n) Enil => Eop (Oaddrsymbol s (Int.add ofs n)) Enil - | Eop (Oaddimm n) (t ::: Enil) => Eop (Oaddsymbol s (Int.add ofs n)) (t ::: Enil) + | Eop (Ointconst n) Enil => Eop (Oaddrsymbol s (Ptrofs.add ofs (Ptrofs.of_int n))) Enil + | Eop (Oaddimm n) (t ::: Enil) => Eop (Oaddsymbol s (Ptrofs.add ofs (Ptrofs.of_int n))) (t ::: Enil) | _ => Eop (Oaddsymbol s ofs) (e ::: Enil) end. @@ -107,9 +107,9 @@ Nondetfunction add (e1: expr) (e2: expr) := | Eop (Oaddimm n1) (t1:::Enil), t2 => addimm n1 (Eop Oadd (t1:::t2:::Enil)) | Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) => - Eop Oadd (Eop (Oaddrstack (Int.add n1 n2)) Enil ::: t2 ::: Enil) + Eop Oadd (Eop (Oaddrstack (Ptrofs.add n1 (Ptrofs.of_int n2))) Enil ::: t2 ::: Enil) | Eop (Oaddsymbol s ofs) (t1:::Enil), Eop (Oaddimm n) (t2:::Enil) => - addsymbol s (Int.add ofs n) (Eop Oadd (t1:::t2:::Enil)) + addsymbol s (Ptrofs.add ofs (Ptrofs.of_int n)) (Eop Oadd (t1:::t2:::Enil)) | Eop (Oaddsymbol s ofs) (t1:::Enil), t2 => addsymbol s ofs (Eop Oadd (t1:::t2:::Enil)) | t1, Eop (Oaddimm n2) (t2:::Enil) => |