From 37cebaabf65fe3961b9932c6582d15b3b676cefe Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 17 Jun 2019 09:43:34 +0200 Subject: Perform constant propagation and strength reduction on conditional moves A conditional move whose condition is statically known becomes a regular move. Otherwise, the condition can sometimes be simplified by strength reduction. --- powerpc/ConstpropOp.vp | 12 +++++++++++- powerpc/ConstpropOpproof.v | 26 +++++++++++++++++++++++++- 2 files changed, 36 insertions(+), 2 deletions(-) (limited to 'powerpc') diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index 2d492b66..cf1dc6e8 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -16,7 +16,7 @@ Require Import Coqlib Compopts. Require Import AST Integers Floats. Require Import Op Registers. -Require Import ValueDomain. +Require Import ValueDomain ValueAOp. (** * Converting known values to constants *) @@ -95,6 +95,15 @@ Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) := make_cmp_base c args vl end. +Definition make_select (c: condition) (ty: typ) + (r1 r2: reg) (args: list reg) (vl: list aval) := + match resolve_branch (eval_static_condition c vl) with + | Some b => (Omove, (if b then r1 else r2) :: nil) + | None => + let (c', args') := cond_strength_reduction c args vl in + (Osel c' ty, r1 :: r2 :: args') + end. + Definition make_addimm (n: int) (r: reg) := if Int.eq n Int.zero then (Omove, r :: nil) @@ -303,6 +312,7 @@ Nondetfunction op_strength_reduction | Oshrl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrlimm n2 r1 r2 | Oshrlu, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrluimm n2 r1 r2 | Ocmp c, args, vl => make_cmp c args vl + | Osel c ty, r1 :: r2 :: args, v1 :: v2 :: vl => make_select c ty r1 r2 args vl | Omulf, r1 :: r2 :: nil, v1 :: F n2 :: nil => make_mulfimm n2 r1 r1 r2 | Omulf, r1 :: r2 :: nil, F n1 :: v2 :: nil => make_mulfimm n1 r2 r1 r2 | Omulfs, r1 :: r2 :: nil, v1 :: FS n2 :: nil => make_mulfsimm n2 r1 r1 r2 diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index fe061e5b..38daefe4 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -14,7 +14,7 @@ Require Import Coqlib Compopts. Require Import Integers Floats Values Memory Globalenvs Events. -Require Import Op Registers RTL ValueDomain. +Require Import Op Registers RTL ValueDomain ValueAOp ValueAnalysis. Require Import ConstpropOp. Local Transparent Archi.ptr64. @@ -211,6 +211,28 @@ Proof. - apply make_cmp_base_correct; auto. Qed. +Lemma make_select_correct: + forall c ty r1 r2 args vl, + vl = map (fun r => AE.get r ae) args -> + let (op', args') := make_select c ty r1 r2 args vl in + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op' rs##args' m = Some v + /\ Val.lessdef (Val.select (eval_condition c rs##args m) rs#r1 rs#r2 ty) v. +Proof. + unfold make_select; intros. + destruct (resolve_branch (eval_static_condition c vl)) as [b|] eqn:RB. +- exists (if b then rs#r1 else rs#r2); split. ++ simpl. destruct b; auto. ++ destruct (eval_condition c rs##args m) as [b'|] eqn:EC; simpl; auto. + assert (b = b'). + { eapply resolve_branch_sound; eauto. + rewrite <- EC. apply eval_static_condition_sound with bc. + subst vl. exact (aregs_sound _ _ _ args MATCH). } + subst b'. apply Val.lessdef_normalize. +- generalize (cond_strength_reduction_correct c args vl H). + destruct (cond_strength_reduction c args vl) as [cond' args']; intros EQ. + econstructor; split. simpl; eauto. rewrite EQ; auto. +Qed. + Lemma make_addimm_correct: forall n r, let (op, args) := make_addimm n r in @@ -715,6 +737,8 @@ Proof. InvApproxRegs; SimplVM; inv H0. apply make_shrluimm_correct; auto. (* cmp *) inv H0. apply make_cmp_correct; auto. +(* select *) + inv H0. apply make_select_correct; congruence. (* mulf *) InvApproxRegs; SimplVM; inv H0. rewrite <- H2. apply make_mulfimm_correct; auto. InvApproxRegs; SimplVM; inv H0. fold (Val.mulf (Vfloat n1) rs#r2). -- cgit From ed0cfe4b38208f15763f2d1c0372c441a320ea56 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 17 Jun 2019 14:22:22 +0200 Subject: Extended asm: print register names according to their types When printing an extended asm code fragment, placeholders %n are replaced by register names. Currently we ignore the fact that some assemblers use different register names depending on the width of the data that resides in the register. For example, x86_64 uses %rax for a 64-bit quantity and %eax for a 32-bit quantity, but CompCert always prints %rax in extended asm statements. This is problematic if we want to use 32-bit integer instructions in extended asm, e.g. int x, y; asm("addl %1, %0", "=r"(x), "r"(y)); produces addl %rax, %rdx which is syntactically incorrect. Another example is ARM FP registers: D0 is a double-precision float, but S0 is a single-precision float. This commit partially solves this issue by taking into account the Cminor type of the asm parameter when printing the corresponding register. Continuing the previous example, int x, y; asm("addl %1, %0", "=r"(x), "r"(y)); now produces addl %eax, %edx This is not perfect yet: we use Cminor types, because this is all we have at hand, and not source C types, hence "char" and "short" parameters are still printed like "int" parameters, which is not good for x86. (I.e. we produce %eax where GCC might have produced %al or %ax.) We'll leave this issue open. --- powerpc/TargetPrinter.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'powerpc') diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index a1338561..0f608d25 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -340,7 +340,7 @@ module Target (System : SYSTEM):TARGET = let ireg_or_zero oc r = if r = GPR0 then output_string oc "0" else ireg oc r - let preg oc = function + let preg_asm oc ty = function | IR r -> ireg oc r | FR r -> freg oc r | _ -> assert false @@ -863,7 +863,7 @@ module Target (System : SYSTEM):TARGET = (P.to_int kind) (extern_atom txt) args | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; - print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res; + print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res; fprintf oc "%s end inline assembly\n" comment | _ -> assert false -- cgit From 83deaa4b3a164423254008d8594de99edc491c3b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 11 Jul 2019 10:56:23 +0200 Subject: Revised specification of NaN payload behavior When an FP arithmetic instruction produces a NaN result, the payload of this NaN depends on the architecture. Before, the payload behavior was specified by 3 architecture-dependent parameters: `Archi.choose_binop_pl_64` and `Archi.choose_binop_pl_32` and `Archi.fpu_results_default_qNaN`. This was adequate for two-argument operations, but doesn't extend to FMA. In preparation for FMA support, this commit generalizes the `Archi.choose` functions from two arguments to any number of arguments. In passing, `Archi.fpu_results_default_qNaN` is no longer needed. --- powerpc/Archi.v | 30 +++++++++++++++++------------- 1 file changed, 17 insertions(+), 13 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Archi.v b/powerpc/Archi.v index d792e4fe..b99e4812 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -16,7 +16,7 @@ (** Architecture-dependent parameters for PowerPC *) -Require Import ZArith. +Require Import ZArith List. (*From Flocq*) Require Import Binary Bits. @@ -37,24 +37,28 @@ Proof. reflexivity. Qed. -Definition default_nan_64 : { x : binary64 | is_nan _ _ x = true } := - exist _ (B754_nan 53 1024 false (iter_nat 51 _ xO xH) (eq_refl true)) (eq_refl true). +Definition default_nan_64 := (false, iter_nat 51 _ xO xH). +Definition default_nan_32 := (false, iter_nat 22 _ xO xH). -Definition choose_binop_pl_64 (pl1 pl2 : positive) := - false. (**r always choose first NaN *) +(* Always choose the first NaN argument, if any *) -Definition default_nan_32 : { x : binary32 | is_nan _ _ x = true } := - exist _ (B754_nan 24 128 false (iter_nat 22 _ xO xH) (eq_refl true)) (eq_refl true). +Definition choose_nan_64 (l: list (bool * positive)) : bool * positive := + match l with nil => default_nan_64 | n :: _ => n end. -Definition choose_binop_pl_32 (pl1 pl2 : positive) := - false. (**r always choose first NaN *) +Definition choose_nan_32 (l: list (bool * positive)) : bool * positive := + match l with nil => default_nan_32 | n :: _ => n end. -Definition fpu_returns_default_qNaN := false. +Lemma choose_nan_64_idem: forall n, + choose_nan_64 (n :: n :: nil) = choose_nan_64 (n :: nil). +Proof. auto. Qed. + +Lemma choose_nan_32_idem: forall n, + choose_nan_32 (n :: n :: nil) = choose_nan_32 (n :: nil). +Proof. auto. Qed. Definition float_of_single_preserves_sNaN := true. Global Opaque ptr64 big_endian splitlong - default_nan_64 choose_binop_pl_64 - default_nan_32 choose_binop_pl_32 - fpu_returns_default_qNaN + default_nan_64 choose_nan_64 + default_nan_32 choose_nan_32 float_of_single_preserves_sNaN. -- cgit From 8b0de52ffa302298abe8d0d6e3b6ed339a2354ba Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 12 Jul 2019 11:42:25 +0200 Subject: Add floating-point square root and fused multiply-add We just lift the corresponding functions from Flocq and add the computation of NaN payloads. NaN payloads for FMA are described in the ARM and RISC-V specifications, and were determined experimentally for x86 and for Power. --- powerpc/Archi.v | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'powerpc') diff --git a/powerpc/Archi.v b/powerpc/Archi.v index b99e4812..ab348c14 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -56,9 +56,14 @@ Lemma choose_nan_32_idem: forall n, choose_nan_32 (n :: n :: nil) = choose_nan_32 (n :: nil). Proof. auto. Qed. +Definition fma_order {A: Type} (x y z: A) := (x, z, y). + +Definition fma_invalid_mul_is_nan := false. + Definition float_of_single_preserves_sNaN := true. Global Opaque ptr64 big_endian splitlong default_nan_64 choose_nan_64 default_nan_32 choose_nan_32 + fma_order fma_invalid_mul_is_nan float_of_single_preserves_sNaN. -- cgit From fb20aab431a768299118ed30822af59cab13325e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 2 Jul 2019 14:55:31 +0200 Subject: Remove the cparser/Builtins module Move its definitions to modules C (the type `builtins`) and Env (the operations that deal with the initial environment). Reasons for the refactoring: 1- The name "Builtins" will soon be reused for a Coq module 2- `Env.initial()` makes more sense than `Builtins.environment()`. --- powerpc/CBuiltins.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'powerpc') diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 11b7aef9..e29a41f1 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -18,11 +18,11 @@ open C let builtins = { - Builtins.typedefs = [ + builtin_typedefs = [ "__builtin_va_list", TArray(TInt(IUInt, []), Some 3L, []) ]; - Builtins.functions = [ + builtin_functions = [ (* Integer arithmetic *) "__builtin_mulhw", (TInt(IInt, []), [TInt(IInt, []); TInt(IInt, [])], false); -- cgit From d08b080747225160b80c3f04bdfd9cd67550b425 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 2 Jul 2019 16:25:40 +0200 Subject: Give formal semantics to some built-in functions and run-time functions This commit adds mechanisms to - recognize certain built-in and run-time functions by name and signature; - associate semantics to these functions, as a partial function from list of values to values; - interpret external calls to these functions according to this semantics (pure function from values to values, memory unchanged, no observable events in the trace); - external calls to unknown built-in and run-time functions remain interpreted as generating observable events and possibly changing memory, like before. The description of the built-ins is split into a target-independent part (in common/Builtins0.v) and a target-specific part (in $ARCH/Builtins1.v). Instruction selection uses the new mechanism in order to - recognize some built-in functions and turn them into operations of the target processor. Currently, this is done for __builtin_sel and __builtin_fabs; more to come. - remove the axioms about int64 helper functions from the standard library. More precisely, the behavior of these functions is still axiomatized, but now it is specified using the more general machinery introduced in this commit, rather than ad-hoc axioms in backend/SplitLongproof. The only built-ins currently described are __builtin_fsqrt (for all platforms) and __builtin_fmin / __builtin_fmax (for x86). More built-ins will be added later. --- powerpc/Builtins1.v | 33 +++++++++++++++++++++++++++++++++ powerpc/SelectOp.vp | 12 +++++++----- powerpc/SelectOpproof.v | 25 +++++++++++++++---------- 3 files changed, 55 insertions(+), 15 deletions(-) create mode 100644 powerpc/Builtins1.v (limited to 'powerpc') diff --git a/powerpc/Builtins1.v b/powerpc/Builtins1.v new file mode 100644 index 00000000..f6e643d2 --- /dev/null +++ b/powerpc/Builtins1.v @@ -0,0 +1,33 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, Collège de France and Inria Paris *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Platform-specific built-in functions *) + +Require Import String Coqlib. +Require Import AST Integers Floats Values. +Require Import Builtins0. + +Inductive platform_builtin : Type := . + +Local Open Scope string_scope. + +Definition platform_builtin_table : list (string * platform_builtin) := + nil. + +Definition platform_builtin_sig (b: platform_builtin) : signature := + match b with end. + +Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) := + match b with end. diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 24aeb531..ba6612e8 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -38,11 +38,8 @@ Require Import Coqlib. Require Import Compopts. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Op. -Require Import CminorSel. +Require Import AST Integers Floats Builtins. +Require Import Op CminorSel. Require Archi. Local Open Scope cminorsel_scope. @@ -566,3 +563,8 @@ Nondetfunction builtin_arg (e: expr) := | Eop Oadd (e1:::e2:::Enil) => BA_addptr (BA e1) (BA e2) | _ => BA e end. + +(** Platform-specific known builtins *) + +Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr := + None. diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 5d7cd52b..1f23f4bd 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -13,17 +13,10 @@ (** Correctness of instruction selection for operators *) Require Import Coqlib. -Require Import Maps. +Require Import AST Integers Floats. +Require Import Values Memory Builtins Globalenvs. +Require Import Cminor Op CminorSel. Require Import Compopts. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Cminor. -Require Import Op. -Require Import CminorSel. Require Import SelectOp. Local Open Scope cminorsel_scope. @@ -1065,4 +1058,16 @@ Proof. - constructor; auto. Qed. +(** Platform-specific known builtins *) + +Theorem eval_platform_builtin: + forall bf al a vl v le, + platform_builtin bf al = Some a -> + eval_exprlist ge sp e m le al vl -> + platform_builtin_sem bf vl = Some v -> + exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'. +Proof. + intros. discriminate. +Qed. + End CMCONSTR. -- cgit From 4c379d48b35e7c8156f3953fede31d5e47faf8ca Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 19 Jul 2019 18:59:44 +0200 Subject: helpers broke compilation --- powerpc/SelectOp.vp | 15 ++------------- powerpc/SelectOpproof.v | 3 +-- 2 files changed, 3 insertions(+), 15 deletions(-) (limited to 'powerpc') diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 07c325c1..50b1bdd6 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -38,17 +38,8 @@ Require Import Coqlib. Require Import Compopts. -<<<<<<< HEAD -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Op. -Require Import CminorSel. -Require Import OpHelpers. -======= Require Import AST Integers Floats Builtins. -Require Import Op CminorSel. ->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf +Require Import Op OpHelpers CminorSel. Require Archi. Local Open Scope cminorsel_scope. @@ -573,16 +564,14 @@ Nondetfunction builtin_arg (e: expr) := | _ => BA e end. -<<<<<<< HEAD (* floats *) Definition divf_base (e1: expr) (e2: expr) := Eop Odivf (e1 ::: e2 ::: Enil). Definition divfs_base (e1: expr) (e2: expr) := Eop Odivfs (e1 ::: e2 ::: Enil). -======= + (** Platform-specific known builtins *) Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr := None. ->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 3e34244d..63066135 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -1062,7 +1062,6 @@ Proof. - constructor; auto. Qed. -<<<<<<< HEAD (* floating-point division without HELPERS *) Theorem eval_divf_base: forall le a b x y, @@ -1083,7 +1082,7 @@ Proof. intros; unfold divfs_base. TrivialExists. Qed. -======= + (** Platform-specific known builtins *) Theorem eval_platform_builtin: -- cgit From 780ad9d001af651a49d7470e963ed9a49ee11a4c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 19 Jul 2019 19:49:46 +0200 Subject: various fixes --- powerpc/SelectOpproof.v | 1 - 1 file changed, 1 deletion(-) (limited to 'powerpc') diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 63066135..b0cd70a4 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -1095,5 +1095,4 @@ Proof. intros. discriminate. Qed. ->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf End CMCONSTR. -- cgit From 040d9c67942c73d875eec9a2ab131fbae6e8f984 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 12 Aug 2019 16:16:10 +0200 Subject: bswap builtins: give semantics to them, support bswap64 on all targets * Added semantic for byte swap builtins The `__builtin_bswap`, `__builtin_bswap16`, `__builtin_bswap32`, `__builtin_bswap64` builtin function are now standard builtin functions with a defined semantics. The semantics is given in terms of the decode/encode functions used for the memory model. * Added bswap64 expansion to PowerPC 32 bits. * Added bswap64 expansion for ARM. --- powerpc/Asmexpand.ml | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) (limited to 'powerpc') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 415b6651..5ca4c611 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -554,6 +554,26 @@ let expand_builtin_inline name args res = emit (Plabel lbl2) | "__builtin_cmpb", [BA(IR a1); BA(IR a2)], BR(IR res) -> emit (Pcmpb (res,a1,a2)) + | "__builtin_bswap64", [BA_splitlong(BA(IR ah), BA(IR al))], + BR_splitlong(BR(IR rh), BR(IR rl))-> + assert (not Archi.ppc64); + emit (Pstwu(ah, Cint _m8, GPR1)); + emit (Pcfi_adjust _8); + emit (Pstwu(al, Cint _m8, GPR1)); + emit (Pcfi_adjust _8); + emit (Plwbrx(rh, GPR0, GPR1)); + emit (Paddi(GPR1, GPR1, Cint _8)); + emit (Pcfi_adjust _m8); + emit (Plwbrx(rl, GPR0, GPR1)); + emit (Paddi(GPR1, GPR1, Cint _8)); + emit (Pcfi_adjust _m8) + | "__builtin_bswap64", [BA(IR a1)], BR(IR res) -> + assert (Archi.ppc64); + emit (Pstdu(a1, Cint _m8, GPR1)); + emit (Pcfi_adjust _8); + emit (Pldbrx(res, GPR0, GPR1)); + emit (Paddi(GPR1, GPR1, Cint _8)); + emit (Pcfi_adjust _m8) | ("__builtin_bswap" | "__builtin_bswap32"), [BA(IR a1)], BR(IR res) -> emit (Pstwu(a1, Cint _m8, GPR1)); emit (Pcfi_adjust _8); -- cgit From 192bd462233d0284fa3d5f8e8994a514b549713e Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 13 Aug 2019 17:13:46 +0200 Subject: 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. --- powerpc/ConstpropOp.vp | 1 + powerpc/ConstpropOpproof.v | 2 ++ 2 files changed, 3 insertions(+) (limited to 'powerpc') 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 *) -- cgit