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 --- backend/Allocation.v | 5 +++-- backend/Allocproof.v | 29 +++++++++++++++-------------- backend/Regalloc.ml | 8 ++++---- 3 files changed, 22 insertions(+), 20 deletions(-) (limited to 'backend') 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] -- cgit v1.2.3