diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2019-08-13 17:13:46 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-13 17:13:46 +0200 |
| commit | 192bd462233d0284fa3d5f8e8994a514b549713e (patch) | |
| tree | 73d6ee96c12f2850e6e46222171c95a83ff75e61 /powerpc | |
| parent | 040d9c67942c73d875eec9a2ab131fbae6e8f984 (diff) | |
| download | compcert-kvx-192bd462233d0284fa3d5f8e8994a514b549713e.tar.gz compcert-kvx-192bd462233d0284fa3d5f8e8994a514b549713e.zip | |
Allow Long as const result for ppc64 variant.
Since the ppc64 has 64 bit registers it is okay to have a 64 bit
constant result.
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/ConstpropOp.vp | 1 | ||||
| -rw-r--r-- | powerpc/ConstpropOpproof.v | 2 |
2 files changed, 3 insertions, 0 deletions
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index cf1dc6e8..8e90a849 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -23,6 +23,7 @@ Require Import ValueDomain ValueAOp. Definition const_for_result (a: aval) : option operation := match a with | I n => Some(Ointconst n) + | L n => if Archi.ppc64 then Some (Olongconst n) else None | F n => if Compopts.generate_float_constants tt then Some(Ofloatconst n) else None | FS n => if Compopts.generate_float_constants tt then Some(Osingleconst n) else None | Ptr(Gl id ofs) => Some (Oaddrsymbol id ofs) diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index 38daefe4..8687b056 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -101,6 +101,8 @@ Proof. destruct a; inv H; SimplVM. - (* integer *) exists (Vint n); auto. +- (* long *) + destruct (Archi.ppc64); inv H2. exists (Vlong n); auto. - (* float *) destruct (generate_float_constants tt); inv H2. exists (Vfloat f); auto. - (* single *) |