From 362f2f36a44fa6ab4fe28264ed572d721adece70 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 3 Jan 2014 17:09:54 +0000 Subject: Introduce and use the platform-specific Archi module giving: - endianness - alignment constraints for 8-byte types (which is 4 for x86 ABI and 8 for other ABIs) - NaN handling options (superceding the Nan module, removed). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2402 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- .depend | 14 +++++++------- Makefile | 2 +- arm/Archi.v | 36 ++++++++++++++++++++++++++++++++++++ arm/Nan.v | 29 ----------------------------- backend/Allocation.v | 5 +++-- backend/Allocproof.v | 29 +++++++++++++++-------------- backend/Regalloc.ml | 8 ++++---- cfrontend/Ctypes.v | 19 ++++++++++++------- common/Memdata.v | 27 +++++++++++++-------------- common/Memory.v | 25 +++++++++++++------------ extraction/extraction.v | 11 +---------- ia32/Archi.v | 34 ++++++++++++++++++++++++++++++++++ ia32/Nan.v | 26 -------------------------- lib/Floats.v | 13 ++++++------- powerpc/Archi.v | 34 ++++++++++++++++++++++++++++++++++ powerpc/Nan.v | 26 -------------------------- 16 files changed, 179 insertions(+), 159 deletions(-) create mode 100644 arm/Archi.v delete mode 100644 arm/Nan.v create mode 100644 ia32/Archi.v delete mode 100644 ia32/Nan.v create mode 100644 powerpc/Archi.v delete mode 100644 powerpc/Nan.v diff --git a/.depend b/.depend index d79e968..2b18734 100644 --- a/.depend +++ b/.depend @@ -7,8 +7,8 @@ lib/Lattice.vo lib/Lattice.glob lib/Lattice.v.beautified: lib/Lattice.v lib/Coql lib/Ordered.vo lib/Ordered.glob lib/Ordered.v.beautified: lib/Ordered.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Iteration.vo lib/Iteration.glob lib/Iteration.v.beautified: lib/Iteration.v lib/Axioms.vo lib/Coqlib.vo lib/Wfsimpl.vo lib/Integers.vo lib/Integers.glob lib/Integers.v.beautified: lib/Integers.v lib/Coqlib.vo -lib/Floats.vo lib/Floats.glob lib/Floats.v.beautified: lib/Floats.v lib/Axioms.vo lib/Coqlib.vo lib/Integers.vo flocq/Appli/Fappli_IEEE.vo flocq/Appli/Fappli_IEEE_bits.vo flocq/Core/Fcore.vo flocq/Calc/Fcalc_round.vo flocq/Calc/Fcalc_bracket.vo flocq/Prop/Fprop_Sterbenz.vo -$(ARCH)/Nan.vo $(ARCH)/Nan.glob $(ARCH)/Nan.v.beautified: $(ARCH)/Nan.v flocq/Appli/Fappli_IEEE.vo flocq/Appli/Fappli_IEEE_bits.vo lib/Floats.vo lib/Integers.vo +$(ARCH)/Archi.vo $(ARCH)/Archi.glob $(ARCH)/Archi.v.beautified: $(ARCH)/Archi.v flocq/Appli/Fappli_IEEE.vo flocq/Appli/Fappli_IEEE_bits.vo +lib/Floats.vo lib/Floats.glob lib/Floats.v.beautified: lib/Floats.v lib/Axioms.vo lib/Coqlib.vo lib/Integers.vo flocq/Appli/Fappli_IEEE.vo flocq/Appli/Fappli_IEEE_bits.vo flocq/Core/Fcore.vo flocq/Calc/Fcalc_round.vo flocq/Calc/Fcalc_bracket.vo flocq/Prop/Fprop_Sterbenz.vo $(ARCH)/Archi.vo lib/Parmov.vo lib/Parmov.glob lib/Parmov.v.beautified: lib/Parmov.v lib/Axioms.vo lib/Coqlib.vo lib/UnionFind.vo lib/UnionFind.glob lib/UnionFind.v.beautified: lib/UnionFind.v lib/Coqlib.vo lib/Wfsimpl.vo lib/Wfsimpl.glob lib/Wfsimpl.v.beautified: lib/Wfsimpl.v lib/Axioms.vo @@ -19,9 +19,9 @@ common/Errors.vo common/Errors.glob common/Errors.v.beautified: common/Errors.v common/AST.vo common/AST.glob common/AST.v.beautified: common/AST.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Events.vo common/Events.glob common/Events.v.beautified: common/Events.v lib/Coqlib.vo lib/Intv.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Errors.vo common/Globalenvs.vo common/Globalenvs.glob common/Globalenvs.v.beautified: common/Globalenvs.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo -common/Memdata.vo common/Memdata.glob common/Memdata.v.beautified: common/Memdata.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo +common/Memdata.vo common/Memdata.glob common/Memdata.v.beautified: common/Memdata.v lib/Coqlib.vo $(ARCH)/Archi.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memtype.vo common/Memtype.glob common/Memtype.v.beautified: common/Memtype.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo -common/Memory.vo common/Memory.glob common/Memory.v.beautified: common/Memory.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memtype.vo lib/Intv.vo +common/Memory.vo common/Memory.glob common/Memory.v.beautified: common/Memory.v lib/Axioms.vo lib/Coqlib.vo lib/Intv.vo lib/Maps.vo $(ARCH)/Archi.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memtype.vo common/Values.vo common/Values.glob common/Values.v.beautified: common/Values.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Smallstep.vo common/Smallstep.glob common/Smallstep.v.beautified: common/Smallstep.v lib/Coqlib.vo common/Events.vo common/Globalenvs.vo lib/Integers.vo common/Behaviors.vo common/Behaviors.glob common/Behaviors.v.beautified: common/Behaviors.v lib/Coqlib.vo common/Events.vo common/Globalenvs.vo lib/Integers.vo common/Smallstep.vo @@ -75,8 +75,8 @@ backend/Locations.vo backend/Locations.glob backend/Locations.v.beautified: back $(ARCH)/$(VARIANT)/Conventions1.vo $(ARCH)/$(VARIANT)/Conventions1.glob $(ARCH)/$(VARIANT)/Conventions1.v.beautified: $(ARCH)/$(VARIANT)/Conventions1.v lib/Coqlib.vo common/AST.vo backend/Locations.vo backend/Conventions.vo backend/Conventions.glob backend/Conventions.v.beautified: backend/Conventions.v lib/Coqlib.vo common/AST.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions1.vo backend/LTL.vo backend/LTL.glob backend/LTL.v.beautified: backend/LTL.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo -backend/Allocation.vo backend/Allocation.glob backend/Allocation.v.beautified: backend/Allocation.v lib/FSetAVLplus.vo lib/Coqlib.vo lib/Ordered.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.vo common/Memdata.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/RTLtyping.vo backend/LTL.vo -backend/Allocproof.vo backend/Allocproof.glob backend/Allocproof.v.beautified: backend/Allocproof.v lib/Coqlib.vo lib/Ordered.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/LTL.vo backend/Allocation.vo +backend/Allocation.vo backend/Allocation.glob backend/Allocation.v.beautified: backend/Allocation.v lib/FSetAVLplus.vo $(ARCH)/Archi.vo lib/Coqlib.vo lib/Ordered.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.vo common/Memdata.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/RTLtyping.vo backend/LTL.vo +backend/Allocproof.vo backend/Allocproof.glob backend/Allocproof.v.beautified: backend/Allocproof.v $(ARCH)/Archi.vo lib/Coqlib.vo lib/Ordered.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/LTL.vo backend/Allocation.vo backend/Tunneling.vo backend/Tunneling.glob backend/Tunneling.v.beautified: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo backend/LTL.vo backend/Tunnelingproof.vo backend/Tunnelingproof.glob backend/Tunnelingproof.v.beautified: backend/Tunnelingproof.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Tunneling.vo backend/Linear.vo backend/Linear.glob backend/Linear.v.beautified: backend/Linear.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo @@ -95,7 +95,7 @@ $(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob $(ARCH)/Asmgen.v.beautified: $(ARCH)/Asmge backend/Asmgenproof0.vo backend/Asmgenproof0.glob backend/Asmgenproof0.v.beautified: backend/Asmgenproof0.v lib/Coqlib.vo lib/Intv.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo $(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob $(ARCH)/Asmgenproof1.v.beautified: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo backend/Conventions.vo $(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob $(ARCH)/Asmgenproof.v.beautified: $(ARCH)/Asmgenproof.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo $(ARCH)/Asmgenproof1.vo -cfrontend/Ctypes.vo cfrontend/Ctypes.glob cfrontend/Ctypes.v.beautified: cfrontend/Ctypes.v lib/Coqlib.vo common/AST.vo common/Errors.vo +cfrontend/Ctypes.vo cfrontend/Ctypes.glob cfrontend/Ctypes.v.beautified: cfrontend/Ctypes.v lib/Coqlib.vo common/AST.vo common/Errors.vo $(ARCH)/Archi.vo cfrontend/Cop.vo cfrontend/Cop.glob cfrontend/Cop.v.beautified: cfrontend/Cop.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo cfrontend/Ctypes.vo cfrontend/Csyntax.vo cfrontend/Csyntax.glob cfrontend/Csyntax.v.beautified: cfrontend/Csyntax.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csem.vo cfrontend/Csem.glob cfrontend/Csem.v.beautified: cfrontend/Csem.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo common/Smallstep.vo diff --git a/Makefile b/Makefile index 28e945f..b527a8c 100644 --- a/Makefile +++ b/Makefile @@ -65,7 +65,7 @@ FLOCQ=\ # General-purpose libraries (in lib/) LIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \ - Iteration.v Integers.v Floats.v Nan.v Parmov.v UnionFind.v Wfsimpl.v \ + Iteration.v Integers.v Archi.v Floats.v Parmov.v UnionFind.v Wfsimpl.v \ Postorder.v FSetAVLplus.v IntvSets.v # Parts common to the front-ends and the back-end (in common/) diff --git a/arm/Archi.v b/arm/Archi.v new file mode 100644 index 0000000..e693541 --- /dev/null +++ b/arm/Archi.v @@ -0,0 +1,36 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Architecture-dependent parameters for ARM *) + +Require Import ZArith. +Require Import Fappli_IEEE. +Require Import Fappli_IEEE_bits. + +Definition big_endian := false. + +Notation align_int64 := 8%Z (only parsing). +Notation align_float64 := 8%Z (only parsing). + +Program Definition default_pl : bool * nan_pl 53 := (false, nat_iter 51 xO xH). + +Definition choose_binop_pl (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) := + (** Choose second NaN if pl2 is sNaN but pl1 is qNan. + In all other cases, choose first NaN *) + (Pos.testbit (proj1_sig pl1) 51 && + negb (Pos.testbit (proj1_sig pl2) 51))%bool. + +Global Opaque big_endian default_pl choose_binop_pl. diff --git a/arm/Nan.v b/arm/Nan.v deleted file mode 100644 index e2bddf6..0000000 --- a/arm/Nan.v +++ /dev/null @@ -1,29 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) -(* *) -(* 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. *) -(* *) -(* *********************************************************************) - -Require Import Fappli_IEEE. -Require Import Fappli_IEEE_bits. -Require Import Floats. -Require Import ZArith. -Require Import Integers. - -Program Definition default_pl : bool * nan_pl 53 := (false, nat_iter 51 xO xH). - -Definition choose_binop_pl (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) := - (** Choose second NaN if pl2 is sNaN but pl1 is qNan. - In all other cases, choose first NaN *) - (Pos.testbit (proj1_sig pl1) 51 && - negb (Pos.testbit (proj1_sig pl2) 51))%bool. diff --git a/backend/Allocation.v b/backend/Allocation.v index 0851b77..f830d79 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -14,6 +14,7 @@ Require Import FSets. Require FSetAVLplus. +Require Archi. Require Import Coqlib. Require Import Ordered. Require Import Errors. @@ -814,8 +815,8 @@ Definition transfer_use_def (args: list reg) (res: reg) (args': list mreg) (res' assertion (can_undef undefs e1); add_equations args args' e1. -Definition kind_first_word := if big_endian then High else Low. -Definition kind_second_word := if big_endian then Low else High. +Definition kind_first_word := if Archi.big_endian then High else Low. +Definition kind_second_word := if Archi.big_endian then Low else High. (** The core transfer function. It takes a set [e] of equations that must hold "after" and a block shape [shape] representing a matching pair diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 1e637f9..4c39fee 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -14,6 +14,7 @@ RTL to LTL). *) Require Import FSets. +Require Archi. Require Import Coqlib. Require Import Ordered. Require Import Errors. @@ -1745,8 +1746,8 @@ Proof. (* load pair *) - generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12). - set (v2' := if big_endian then v2 else v1) in *. - set (v1' := if big_endian then v1 else v2) in *. + set (v2' := if Archi.big_endian then v2 else v1) in *. + set (v1' := if Archi.big_endian then v1 else v2) in *. exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. assert (LD1: Val.lessdef_list rs##args (reglist ls1 args1')). { eapply add_equations_lessdef; eauto. } @@ -1759,7 +1760,7 @@ Proof. eapply add_equations_satisf; eauto. assumption. rewrite Regmap.gss. apply Val.lessdef_trans with v1'; auto. subst v. unfold v1', kind_first_word. - destruct big_endian; apply val_hiword_longofwords || apply val_loword_longofwords. + destruct Archi.big_endian; apply val_hiword_longofwords || apply val_loword_longofwords. } exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. assert (LD3: Val.lessdef_list rs##args (reglist ls3 args2')). @@ -1777,7 +1778,7 @@ Proof. eapply add_equations_satisf; eauto. assumption. apply Val.lessdef_trans with v2'; auto. rewrite Regmap.gss. subst v. unfold v2', kind_second_word. - destruct big_endian; apply val_hiword_longofwords || apply val_loword_longofwords. + destruct Archi.big_endian; apply val_hiword_longofwords || apply val_loword_longofwords. } exploit (exec_moves mv3); eauto. intros [ls5 [A5 B5]]. econstructor; split. @@ -1799,8 +1800,8 @@ Proof. (* load first word of a pair *) - generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12). - set (v2' := if big_endian then v2 else v1) in *. - set (v1' := if big_endian then v1 else v2) in *. + set (v2' := if Archi.big_endian then v2 else v1) in *. + set (v1' := if Archi.big_endian then v1 else v2) in *. exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. assert (LD1: Val.lessdef_list rs##args (reglist ls1 args')). { eapply add_equations_lessdef; eauto. } @@ -1811,7 +1812,7 @@ Proof. { eapply parallel_assignment_satisf; eauto. apply Val.lessdef_trans with v1'; auto. subst v. unfold v1', kind_first_word. - destruct big_endian; apply val_hiword_longofwords || apply val_loword_longofwords. + destruct Archi.big_endian; apply val_hiword_longofwords || apply val_loword_longofwords. eapply can_undef_satisf. eauto. eapply add_equations_satisf; eauto. } exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. @@ -1830,8 +1831,8 @@ Proof. (* load second word of a pair *) - generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. exploit Mem.loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V12). - set (v2' := if big_endian then v2 else v1) in *. - set (v1' := if big_endian then v1 else v2) in *. + set (v2' := if Archi.big_endian then v2 else v1) in *. + set (v1' := if Archi.big_endian then v1 else v2) in *. exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. assert (LD1: Val.lessdef_list rs##args (reglist ls1 args')). { eapply add_equations_lessdef; eauto. } @@ -1843,7 +1844,7 @@ Proof. { eapply parallel_assignment_satisf; eauto. apply Val.lessdef_trans with v2'; auto. subst v. unfold v2', kind_second_word. - destruct big_endian; apply val_hiword_longofwords || apply val_loword_longofwords. + destruct Archi.big_endian; apply val_hiword_longofwords || apply val_loword_longofwords. eapply can_undef_satisf. eauto. eapply add_equations_satisf; eauto. } exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. @@ -1888,12 +1889,12 @@ Proof. (* store 2 *) - exploit Mem.storev_int64_split; eauto. - replace (if big_endian then Val.hiword rs#src else Val.loword rs#src) + replace (if Archi.big_endian then Val.hiword rs#src else Val.loword rs#src) with (sel_val kind_first_word rs#src) - by (unfold kind_first_word; destruct big_endian; reflexivity). - replace (if big_endian then Val.loword rs#src else Val.hiword rs#src) + by (unfold kind_first_word; destruct Archi.big_endian; reflexivity). + replace (if Archi.big_endian then Val.loword rs#src else Val.hiword rs#src) with (sel_val kind_second_word rs#src) - by (unfold kind_second_word; destruct big_endian; reflexivity). + by (unfold kind_second_word; destruct Archi.big_endian; reflexivity). intros [m1 [STORE1 STORE2]]. exploit (exec_moves mv1); eauto. intros [ls1 [X Y]]. exploit add_equations_lessdef. eexact Heqo1. eexact Y. intros LD1. diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index 5c68602..b21eeb0 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -150,9 +150,9 @@ let block_of_RTL_instr funsig tyenv = function | None -> assert false | Some addr' -> [Xload(Mint32, addr, vregs tyenv args, - V((if big_endian then dst else twin_reg dst), Tint)); + V((if Archi.big_endian then dst else twin_reg dst), Tint)); Xload(Mint32, addr', vregs tyenv args, - V((if big_endian then twin_reg dst else dst), Tint)); + V((if Archi.big_endian then twin_reg dst else dst), Tint)); Xbranch s] end else [Xload(chunk, addr, vregs tyenv args, vreg tyenv dst); Xbranch s] @@ -162,9 +162,9 @@ let block_of_RTL_instr funsig tyenv = function | None -> assert false | Some addr' -> [Xstore(Mint32, addr, vregs tyenv args, - V((if big_endian then src else twin_reg src), Tint)); + V((if Archi.big_endian then src else twin_reg src), Tint)); Xstore(Mint32, addr', vregs tyenv args, - V((if big_endian then twin_reg src else src), Tint)); + V((if Archi.big_endian then twin_reg src else src), Tint)); Xbranch s] end else [Xstore(chunk, addr, vregs tyenv args, vreg tyenv src); Xbranch s] diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index ec4780e..5cd032d 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -18,6 +18,7 @@ Require Import Coqlib. Require Import AST. Require Import Errors. +Require Archi. (** * Syntax of types *) @@ -172,9 +173,9 @@ Fixpoint alignof (t: type) : Z := | Tint I16 _ _ => 2 | Tint I32 _ _ => 4 | Tint IBool _ _ => 1 - | Tlong _ _ => 8 + | Tlong _ _ => Archi.align_int64 | Tfloat F32 _ => 4 - | Tfloat F64 _ => 8 + | Tfloat F64 _ => Archi.align_float64 | Tpointer _ _ => 4 | Tarray t' _ _ => alignof t' | Tfunction _ _ _ => 1 @@ -214,10 +215,14 @@ Proof. induction t; apply X; simpl; auto. exists 0%nat; auto. destruct i. - exists 0%nat; auto. exists 1%nat; auto. exists 2%nat; auto. - exists 0%nat; auto. exists 3%nat; auto. + exists 0%nat; auto. + exists 1%nat; auto. + exists 2%nat; auto. + exists 0%nat; auto. + (exists 2%nat; reflexivity) || (exists 3%nat; reflexivity). destruct f. - exists 2%nat; auto. exists 3%nat; auto. + exists 2%nat; auto. + (exists 2%nat; reflexivity) || (exists 3%nat; reflexivity). exists 2%nat; auto. exists 0%nat; auto. exists 2%nat; auto. @@ -311,8 +316,8 @@ Local Transparent alignof. induction t; simpl; intros. - apply Zdivide_refl. - rewrite H. destruct i; apply Zdivide_refl. -- rewrite H; apply Zdivide_refl. -- rewrite H. destruct f; apply Zdivide_refl. +- rewrite H. exists (8 / Archi.align_int64); reflexivity. +- rewrite H. destruct f. apply Zdivide_refl. exists (8 / Archi.align_float64); reflexivity. - rewrite H; apply Zdivide_refl. - destruct H. rewrite H. apply Z.divide_mul_l; auto. - apply Zdivide_refl. diff --git a/common/Memdata.v b/common/Memdata.v index 47f8471..d8d347e 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -17,6 +17,7 @@ (** In-memory representation of values. *) Require Import Coqlib. +Require Archi. Require Import AST. Require Import Integers. Require Import Floats. @@ -146,10 +147,8 @@ Fixpoint int_of_bytes (l: list byte): Z := | b :: l' => Byte.unsigned b + int_of_bytes l' * 256 end. -Parameter big_endian: bool. - Definition rev_if_be (l: list byte) : list byte := - if big_endian then List.rev l else l. + if Archi.big_endian then List.rev l else l. Definition encode_int (sz: nat) (x: Z) : list byte := rev_if_be (bytes_of_int sz x). @@ -168,7 +167,7 @@ Qed. Lemma rev_if_be_length: forall l, length (rev_if_be l) = length l. Proof. - intros; unfold rev_if_be; destruct big_endian. + intros; unfold rev_if_be; destruct Archi.big_endian. apply List.rev_length. auto. Qed. @@ -200,7 +199,7 @@ Qed. Lemma rev_if_be_involutive: forall l, rev_if_be (rev_if_be l) = l. Proof. - intros; unfold rev_if_be; destruct big_endian. + intros; unfold rev_if_be; destruct Archi.big_endian. apply List.rev_involutive. auto. Qed. @@ -914,8 +913,8 @@ Lemma decode_val_int64: forall l1 l2, length l1 = 4%nat -> length l2 = 4%nat -> decode_val Mint64 (l1 ++ l2) = - Val.longofwords (decode_val Mint32 (if big_endian then l1 else l2)) - (decode_val Mint32 (if big_endian then l2 else l1)). + Val.longofwords (decode_val Mint32 (if Archi.big_endian then l1 else l2)) + (decode_val Mint32 (if Archi.big_endian then l2 else l1)). Proof. intros. unfold decode_val. assert (PP: forall vl, match proj_pointer vl with Vundef => True | Vptr _ _ => True | _ => False end). @@ -935,7 +934,7 @@ Proof. generalize (int_of_bytes_range l). rewrite H1. change (two_p (Z.of_nat 4 * 8)) with (Int.max_unsigned + 1). omega. - unfold decode_int, rev_if_be. destruct big_endian; rewrite B1; rewrite B2. + unfold decode_int, rev_if_be. destruct Archi.big_endian; rewrite B1; rewrite B2. + rewrite <- (rev_length b1) in L1. rewrite <- (rev_length b2) in L2. rewrite rev_app_distr. @@ -946,9 +945,9 @@ Proof. + unfold Val.longofwords. f_equal. rewrite Int64.ofwords_add. f_equal. rewrite !UR by auto. rewrite int_of_bytes_append. rewrite L1. change (Z.of_nat 4 * 8) with 32. ring. -- destruct big_endian; rewrite B1; rewrite B2; auto. -- destruct big_endian; rewrite B1; rewrite B2; auto. -- destruct big_endian; rewrite B1; rewrite B2; auto. +- destruct Archi.big_endian; rewrite B1; rewrite B2; auto. +- destruct Archi.big_endian; rewrite B1; rewrite B2; auto. +- destruct Archi.big_endian; rewrite B1; rewrite B2; auto. Qed. Lemma bytes_of_int_append: @@ -987,10 +986,10 @@ Qed. Lemma encode_val_int64: forall v, encode_val Mint64 v = - encode_val Mint32 (if big_endian then Val.hiword v else Val.loword v) - ++ encode_val Mint32 (if big_endian then Val.loword v else Val.hiword v). + encode_val Mint32 (if Archi.big_endian then Val.hiword v else Val.loword v) + ++ encode_val Mint32 (if Archi.big_endian then Val.loword v else Val.hiword v). Proof. - intros. destruct v; destruct big_endian eqn:BI; try reflexivity; + intros. destruct v; destruct Archi.big_endian eqn:BI; try reflexivity; unfold Val.loword, Val.hiword, encode_val. unfold inj_bytes. rewrite <- map_app. f_equal. unfold encode_int, rev_if_be. rewrite BI. rewrite <- rev_app_distr. f_equal. diff --git a/common/Memory.v b/common/Memory.v index 79fc8a0..0260a89 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -31,6 +31,7 @@ Require Import Axioms. Require Import Coqlib. Require Intv. Require Import Maps. +Require Archi. Require Import AST. Require Import Integers. Require Import Floats. @@ -891,8 +892,8 @@ Theorem load_int64_split: forall m b ofs v, load Mint64 m b ofs = Some v -> exists v1 v2, - load Mint32 m b ofs = Some (if big_endian then v1 else v2) - /\ load Mint32 m b (ofs + 4) = Some (if big_endian then v2 else v1) + load Mint32 m b ofs = Some (if Archi.big_endian then v1 else v2) + /\ load Mint32 m b (ofs + 4) = Some (if Archi.big_endian then v2 else v1) /\ v = Val.longofwords v1 v2. Proof. intros. @@ -909,10 +910,10 @@ Proof. exploit loadbytes_load. eexact LB2. simpl. apply Zdivide_plus_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto. intros L2. - exists (decode_val Mint32 (if big_endian then bytes1 else bytes2)); - exists (decode_val Mint32 (if big_endian then bytes2 else bytes1)). - split. destruct big_endian; auto. - split. destruct big_endian; auto. + exists (decode_val Mint32 (if Archi.big_endian then bytes1 else bytes2)); + exists (decode_val Mint32 (if Archi.big_endian then bytes2 else bytes1)). + split. destruct Archi.big_endian; auto. + split. destruct Archi.big_endian; auto. rewrite EQ. rewrite APP. apply decode_val_int64. erewrite loadbytes_length; eauto. reflexivity. erewrite loadbytes_length; eauto. reflexivity. @@ -922,8 +923,8 @@ Theorem loadv_int64_split: forall m a v, loadv Mint64 m a = Some v -> exists v1 v2, - loadv Mint32 m a = Some (if big_endian then v1 else v2) - /\ loadv Mint32 m (Val.add a (Vint (Int.repr 4))) = Some (if big_endian then v2 else v1) + loadv Mint32 m a = Some (if Archi.big_endian then v1 else v2) + /\ loadv Mint32 m (Val.add a (Vint (Int.repr 4))) = Some (if Archi.big_endian then v2 else v1) /\ v = Val.longofwords v1 v2. Proof. intros. destruct a; simpl in H; try discriminate. @@ -1674,8 +1675,8 @@ Theorem store_int64_split: forall m b ofs v m', store Mint64 m b ofs v = Some m' -> exists m1, - store Mint32 m b ofs (if big_endian then Val.hiword v else Val.loword v) = Some m1 - /\ store Mint32 m1 b (ofs + 4) (if big_endian then Val.loword v else Val.hiword v) = Some m'. + store Mint32 m b ofs (if Archi.big_endian then Val.hiword v else Val.loword v) = Some m1 + /\ store Mint32 m1 b (ofs + 4) (if Archi.big_endian then Val.loword v else Val.hiword v) = Some m'. Proof. intros. exploit store_valid_access_3; eauto. intros [A B]. simpl in *. @@ -1694,8 +1695,8 @@ Theorem storev_int64_split: forall m a v m', storev Mint64 m a v = Some m' -> exists m1, - storev Mint32 m a (if big_endian then Val.hiword v else Val.loword v) = Some m1 - /\ storev Mint32 m1 (Val.add a (Vint (Int.repr 4))) (if big_endian then Val.loword v else Val.hiword v) = Some m'. + storev Mint32 m a (if Archi.big_endian then Val.hiword v else Val.loword v) = Some m1 + /\ storev Mint32 m1 (Val.add a (Vint (Int.repr 4))) (if Archi.big_endian then Val.loword v else Val.hiword v) = Some m'. Proof. intros. destruct a; simpl in H; try discriminate. exploit store_int64_split; eauto. intros [m1 [A B]]. diff --git a/extraction/extraction.v b/extraction/extraction.v index b1cd8fd..6556c87 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -12,7 +12,6 @@ Require Coqlib. Require Wfsimpl. -Require Nan. Require AST. Require Iteration. Require Floats. @@ -34,17 +33,10 @@ Extract Inlined Constant Coqlib.proj_sumbool => "(fun x -> x)". (* Wfsimpl *) Extraction Inline Wfsimpl.Fix Wfsimpl.Fixm. -(* Floats *) -Extract Constant Floats.Float.default_pl => "Nan.default_pl". -Extract Constant Floats.Float.choose_binop_pl => "Nan.choose_binop_pl". - (* AST *) Extract Constant AST.ident_of_string => "fun s -> Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s)". -(* Memdata *) -Extract Constant Memdata.big_endian => "Memdataaux.big_endian". - (* Memory - work around an extraction bug. *) Extraction NoInline Memory.Mem.valid_pointer. @@ -140,5 +132,4 @@ Separate Extraction Conventions1.dummy_int_reg Conventions1.dummy_float_reg RTL.instr_defs RTL.instr_uses Machregs.mregs_for_operation Machregs.mregs_for_builtin - Machregs.two_address_op - Nan.default_pl Nan.choose_binop_pl. + Machregs.two_address_op. diff --git a/ia32/Archi.v b/ia32/Archi.v new file mode 100644 index 0000000..a2e136c --- /dev/null +++ b/ia32/Archi.v @@ -0,0 +1,34 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Architecture-dependent parameters for IA32 *) + +Require Import ZArith. +Require Import Fappli_IEEE. +Require Import Fappli_IEEE_bits. + +Definition big_endian := false. + +Notation align_int64 := 4%Z (only parsing). +Notation align_float64 := 4%Z (only parsing). + +Program Definition default_pl : bool * nan_pl 53 := + (true, nat_iter 51 xO xH). + +Definition choose_binop_pl (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) := + false. (**r always choose first NaN *) + +Global Opaque big_endian default_pl choose_binop_pl. diff --git a/ia32/Nan.v b/ia32/Nan.v deleted file mode 100644 index f3e777e..0000000 --- a/ia32/Nan.v +++ /dev/null @@ -1,26 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) -(* *) -(* 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. *) -(* *) -(* *********************************************************************) - -Require Import Fappli_IEEE. -Require Import Fappli_IEEE_bits. -Require Import Floats. -Require Import ZArith. -Require Import Integers. - -Program Definition default_pl : bool * nan_pl 53 := (true, nat_iter 51 xO xH). - -Definition choose_binop_pl (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) := - false. (** always choose first NaN *) diff --git a/lib/Floats.v b/lib/Floats.v index 0a30836..5502927 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -26,6 +26,7 @@ Require Import Fcalc_round. Require Import Fcalc_bracket. Require Import Fprop_Sterbenz. Require Import Program. +Require Archi. Close Scope R_scope. @@ -268,18 +269,15 @@ Definition singleoflongu (n:int64): float:= (**r conversion from unsigned 64-bit - a choice function determining which of the payload arguments to choose, when an operation is given two NaN arguments. *) -Parameter default_pl : bool*nan_pl 53. -Parameter choose_binop_pl : bool -> nan_pl 53 -> bool -> nan_pl 53 -> bool. - Definition binop_pl (x y: binary64) : bool*nan_pl 53 := match x, y with | B754_nan s1 pl1, B754_nan s2 pl2 => - if choose_binop_pl s1 pl1 s2 pl2 + if Archi.choose_binop_pl s1 pl1 s2 pl2 then (s2, transform_quiet_pl pl2) else (s1, transform_quiet_pl pl1) | B754_nan s1 pl1, _ => (s1, transform_quiet_pl pl1) | _, B754_nan s2 pl2 => (s2, transform_quiet_pl pl2) - | _, _ => default_pl + | _, _ => Archi.default_pl end. Definition add: float -> float -> float := b64_plus binop_pl mode_NE. (**r addition *) @@ -1235,8 +1233,9 @@ Proof. etransitivity. apply H. symmetry. etransitivity. apply H0. f_equal. destruct Bsign; reflexivity. - - destruct f as [[]|[]| |]; try discriminate; try reflexivity. - simpl. destruct (choose_binop_pl b n b n); auto. + - destruct f as [[]|[]| |]; try discriminate; simpl. + auto. auto. auto. auto. + destruct (Archi.choose_binop_pl b n b n); auto. Qed. Program Definition pow2_float (b:bool) (e:Z) (H:-1023 < e < 1023) : float := diff --git a/powerpc/Archi.v b/powerpc/Archi.v new file mode 100644 index 0000000..0672dce --- /dev/null +++ b/powerpc/Archi.v @@ -0,0 +1,34 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Architecture-dependent parameters for PowerPC *) + +Require Import ZArith. +Require Import Fappli_IEEE. +Require Import Fappli_IEEE_bits. + +Definition big_endian := false. + +Notation align_int64 := 8%Z (only parsing). +Notation align_float64 := 8%Z (only parsing). + +Program Definition default_pl : bool * nan_pl 53 := + (true, nat_iter 51 xO xH). + +Definition choose_binop_pl (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) := + false. (**r always choose first NaN *) + +Global Opaque big_endian default_pl choose_binop_pl. diff --git a/powerpc/Nan.v b/powerpc/Nan.v deleted file mode 100644 index c230789..0000000 --- a/powerpc/Nan.v +++ /dev/null @@ -1,26 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) -(* *) -(* 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. *) -(* *) -(* *********************************************************************) - -Require Import Fappli_IEEE. -Require Import Fappli_IEEE_bits. -Require Import Floats. -Require Import ZArith. -Require Import Integers. - -Program Definition default_pl : bool * nan_pl 53 := (false, nat_iter 51 xO xH). - -Definition choose_binop_pl (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) := - false. -- cgit v1.2.3