diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-01-03 17:09:54 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-01-03 17:09:54 +0000 |
commit | 362f2f36a44fa6ab4fe28264ed572d721adece70 (patch) | |
tree | 2f1b23f88fe906ae554e963acbcde09c54b1b5fb /backend/Allocproof.v | |
parent | 089c6c6dc139a0c32f8566d028702d39d0748077 (diff) | |
download | compcert-kvx-362f2f36a44fa6ab4fe28264ed572d721adece70.tar.gz compcert-kvx-362f2f36a44fa6ab4fe28264ed572d721adece70.zip |
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
Diffstat (limited to 'backend/Allocproof.v')
-rw-r--r-- | backend/Allocproof.v | 29 |
1 files changed, 15 insertions, 14 deletions
diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 1e637f9f..4c39fee4 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. |