diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-01 17:38:24 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-01 17:38:24 +0200 |
commit | a14b9578ee5297d954103e05d7b2d322816ddd8f (patch) | |
tree | 93b7c2b6bd7de8a4dedaf399088257e0660959b8 /ia32/SelectLongproof.v | |
parent | 3bef0962079cf971673b4267b0142bd5fe092509 (diff) | |
download | compcert-a14b9578ee5297d954103e05d7b2d322816ddd8f.tar.gz compcert-a14b9578ee5297d954103e05d7b2d322816ddd8f.zip |
Support for 64-bit architectures: x86 in 64-bit mode
This commit enriches the IA32 port so that it supports x86 processors in 64-bit mode as well as in 32-bit mode, depending on the value of Archi.ptr64, which itself is set from the configuration model.
To activate x86-64 bit support, configure with "x86_64-linux".
Main steps:
- Enrich Op.v and Asm.v with 64-bit operations
- SelectLong: in 64-bit mode, use 64-bit operations directly; in 32-bit mode, fall back on the old implementation based on pairs of 32-bit integers
- Conventions1: support x86-64 ABI in addition to the 32-bit ABI.
- Add support for the new 64-bit operations everywhere.
- runtime/x86_64: implementation of the supporting library appropriate for x86 in 64-bit mode
To do:
- More optimizations are possible on 64-bit integer arithmetic operations.
- Could add new chunks to load, say, an unsigned byte into a 64-bit long
(currently we load as a 32-bit int then zero-extend).
- Implements the wrong ABI for struct passing.
Diffstat (limited to 'ia32/SelectLongproof.v')
-rw-r--r-- | ia32/SelectLongproof.v | 304 |
1 files changed, 304 insertions, 0 deletions
diff --git a/ia32/SelectLongproof.v b/ia32/SelectLongproof.v new file mode 100644 index 00000000..634da83a --- /dev/null +++ b/ia32/SelectLongproof.v @@ -0,0 +1,304 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Correctness of instruction selection for 64-bit integer operations *) + +Require Import String Coqlib Maps Integers Floats Errors. +Require Archi. +Require Import AST Values Memory Globalenvs Events. +Require Import Cminor Op CminorSel. +Require Import SelectOp SelectOpproof SplitLong SplitLongproof. +Require Import SelectLong. + +Open Local Scope cminorsel_scope. +Open Local Scope string_scope. + +(** * Correctness of the instruction selection functions for 64-bit operators *) + +Section CMCONSTR. + +Variable prog: program. +Variable hf: helper_functions. +Hypothesis HELPERS: helper_functions_declared prog hf. +Let ge := Genv.globalenv prog. +Variable sp: val. +Variable e: env. +Variable m: mem. + +Definition unary_constructor_sound (cstr: expr -> expr) (sem: val -> val) : Prop := + forall le a x, + eval_expr ge sp e m le a x -> + exists v, eval_expr ge sp e m le (cstr a) v /\ Val.lessdef (sem x) v. + +Definition binary_constructor_sound (cstr: expr -> expr -> expr) (sem: val -> val -> val) : Prop := + forall le a x b y, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + exists v, eval_expr ge sp e m le (cstr a b) v /\ Val.lessdef (sem x y) v. + +Definition partial_unary_constructor_sound (cstr: expr -> expr) (sem: val -> option val) : Prop := + forall le a x y, + eval_expr ge sp e m le a x -> + sem x = Some y -> + exists v, eval_expr ge sp e m le (cstr a) v /\ Val.lessdef y v. + +Definition partial_binary_constructor_sound (cstr: expr -> expr -> expr) (sem: val -> val -> option val) : Prop := + forall le a x b y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + sem x y = Some z -> + exists v, eval_expr ge sp e m le (cstr a b) v /\ Val.lessdef z v. + +Theorem eval_longconst: + forall le n, eval_expr ge sp e m le (longconst n) (Vlong n). +Proof. + unfold longconst; intros; destruct Archi.splitlong. + apply SplitLongproof.eval_longconst. + EvalOp. +Qed. + +Lemma is_longconst_sound: + forall a n, is_longconst a = Some n -> a = Eop (Olongconst n) Enil. +Proof with (try discriminate). + unfold is_longconst; intros. destruct a... destruct o... destruct e0... congruence. +Qed. + +Lemma is_longconst_inv: + forall v a n le, + is_longconst a = Some n -> eval_expr ge sp e m le a v -> v = Vlong n. +Proof. + intros. rewrite (is_longconst_sound _ _ H) in H0. InvEval. auto. +Qed. + +Theorem eval_intoflong: unary_constructor_sound intoflong Val.loword. +Proof. + unfold intoflong; destruct Archi.splitlong. apply SplitLongproof.eval_intoflong. + red; intros. destruct (is_longconst a) as [n|] eqn:C. +- TrivialExists. simpl. erewrite (is_longconst_inv x) by eauto. auto. +- TrivialExists. +Qed. + +Theorem eval_longofintu: unary_constructor_sound longofintu Val.longofintu. +Proof. + unfold longofintu; destruct Archi.splitlong. apply SplitLongproof.eval_longofintu. + red; intros. destruct (is_intconst a) as [n|] eqn:C. +- econstructor; split. apply eval_longconst. + exploit is_intconst_sound; eauto. intros; subst x. auto. +- TrivialExists. +Qed. + +Theorem eval_longofint: unary_constructor_sound longofint Val.longofint. +Proof. + unfold longofint; destruct Archi.splitlong. apply SplitLongproof.eval_longofint. + red; intros. destruct (is_intconst a) as [n|] eqn:C. +- econstructor; split. apply eval_longconst. + exploit is_intconst_sound; eauto. intros; subst x. auto. +- TrivialExists. +Qed. + +Theorem eval_notl: unary_constructor_sound notl Val.notl. +Proof. + unfold notl; destruct Archi.splitlong. apply SplitLongproof.eval_notl. + red; intros. destruct (notl_match a). +- InvEval. econstructor; split. apply eval_longconst. auto. +- InvEval. subst. exists v1; split; auto. destruct v1; simpl; auto. rewrite Int64.not_involutive; auto. +- TrivialExists. +Qed. + +Theorem eval_andlimm: forall n, unary_constructor_sound (andlimm n) (fun v => Val.andl v (Vlong n)). +Proof. + unfold andlimm; intros; red; intros. + predSpec Int64.eq Int64.eq_spec n Int64.zero. + exists (Vlong Int64.zero); split. apply eval_longconst. + subst. destruct x; simpl; auto. rewrite Int64.and_zero; auto. + predSpec Int64.eq Int64.eq_spec n Int64.mone. + exists x; split. assumption. + subst. destruct x; simpl; auto. rewrite Int64.and_mone; auto. + destruct (andlimm_match a); InvEval; subst. +- econstructor; split. apply eval_longconst. simpl. rewrite Int64.and_commut; auto. +- TrivialExists. simpl. rewrite Val.andl_assoc. rewrite Int64.and_commut; auto. +- TrivialExists. +Qed. + +Theorem eval_andl: binary_constructor_sound andl Val.andl. +Admitted. + +Theorem eval_orlimm: forall n, unary_constructor_sound (orlimm n) (fun v => Val.orl v (Vlong n)). +Admitted. + +Theorem eval_orl: binary_constructor_sound orl Val.orl. +Admitted. + +Theorem eval_xorlimm: forall n, unary_constructor_sound (xorlimm n) (fun v => Val.xorl v (Vlong n)). +Admitted. + +Theorem eval_xorl: binary_constructor_sound xorl Val.xorl. +Admitted. + +Theorem eval_shllimm: forall n, unary_constructor_sound (fun e => shllimm e n) (fun v => Val.shll v (Vint n)). +Admitted. + +Theorem eval_shrluimm: forall n, unary_constructor_sound (fun e => shrluimm e n) (fun v => Val.shrlu v (Vint n)). +Admitted. + +Theorem eval_shrlimm: forall n, unary_constructor_sound (fun e => shrlimm e n) (fun v => Val.shrl v (Vint n)). +Admitted. + +Theorem eval_shll: binary_constructor_sound shll Val.shll. +Admitted. + +Theorem eval_shrlu: binary_constructor_sound shrlu Val.shrlu. +Admitted. + +Theorem eval_shrl: binary_constructor_sound shrl Val.shrl. +Admitted. + +Theorem eval_negl: unary_constructor_sound negl Val.negl. +Admitted. + +Theorem eval_addlimm: forall n, unary_constructor_sound (addlimm n) (fun v => Val.addl v (Vlong n)). +Proof. + unfold addlimm; intros; red; intros. + predSpec Int64.eq Int64.eq_spec n Int64.zero. + subst. exists x; split; auto. + destruct x; simpl; auto. + rewrite Int64.add_zero; auto. + destruct Archi.ptr64; auto. rewrite Ptrofs.add_zero; auto. + destruct (addlimm_match a); InvEval. +- econstructor; split. apply eval_longconst. rewrite Int64.add_commut; auto. +- inv H. simpl in H6. TrivialExists. simpl. + erewrite eval_offset_addressing_total_64 by eauto. rewrite Int64.repr_signed; auto. +- TrivialExists. simpl. rewrite Int64.repr_signed; auto. +Qed. + +Theorem eval_addl: binary_constructor_sound addl Val.addl. +Proof. + assert (A: forall x y, Int64.repr (x + y) = Int64.add (Int64.repr x) (Int64.repr y)). + { intros; apply Int64.eqm_samerepr; auto with ints. } + assert (B: forall id ofs n, Archi.ptr64 = true -> + Genv.symbol_address ge id (Ptrofs.add ofs (Ptrofs.repr n)) = + Val.addl (Genv.symbol_address ge id ofs) (Vlong (Int64.repr n))). + { intros. replace (Ptrofs.repr n) with (Ptrofs.of_int64 (Int64.repr n)) by auto with ptrofs. + apply Genv.shift_symbol_address_64; auto. } + unfold addl. destruct Archi.splitlong eqn:SL. + apply SplitLongproof.eval_addl. apply Archi.splitlong_ptr32; auto. + red; intros; destruct (addl_match a b); InvEval. +- rewrite Val.addl_commut. apply eval_addlimm; auto. +- apply eval_addlimm; auto. +- subst. TrivialExists. simpl. rewrite A, Val.addl_permut_4. auto. +- subst. TrivialExists. simpl. rewrite A, Val.addl_assoc. decEq; decEq. rewrite Val.addl_permut. auto. +- subst. TrivialExists. simpl. rewrite A, Val.addl_permut_4. rewrite <- Val.addl_permut. rewrite <- Val.addl_assoc. auto. +- subst. TrivialExists. simpl. rewrite Val.addl_commut; auto. +- subst. TrivialExists. +- subst. TrivialExists. simpl. rewrite ! Val.addl_assoc. rewrite (Val.addl_commut y). auto. +- subst. TrivialExists. simpl. rewrite ! Val.addl_assoc. auto. +- TrivialExists. simpl. destruct x; destruct y; simpl; auto. + rewrite Int64.add_zero; auto. + destruct Archi.ptr64 eqn:SF; simpl; auto. rewrite SF. rewrite Ptrofs.add_assoc, Ptrofs.add_zero. auto. + destruct Archi.ptr64 eqn:SF; simpl; auto. rewrite SF. rewrite Ptrofs.add_assoc, Ptrofs.add_zero. auto. +Qed. + +Theorem eval_subl: binary_constructor_sound subl Val.subl. +Proof. + unfold subl. destruct Archi.splitlong eqn:SL. + apply SplitLongproof.eval_subl. apply Archi.splitlong_ptr32; auto. + red; intros; destruct (subl_match a b); InvEval. +- rewrite Val.subl_addl_opp. apply eval_addlimm; auto. +- subst. rewrite Val.subl_addl_l. rewrite Val.subl_addl_r. + rewrite Val.addl_assoc. simpl. rewrite Int64.add_commut. rewrite <- Int64.sub_add_opp. + replace (Int64.repr (n1 - n2)) with (Int64.sub (Int64.repr n1) (Int64.repr n2)). + apply eval_addlimm; EvalOp. + apply Int64.eqm_samerepr; auto with ints. +- subst. rewrite Val.subl_addl_l. apply eval_addlimm; EvalOp. +- subst. rewrite Val.subl_addl_r. + replace (Int64.repr (-n2)) with (Int64.neg (Int64.repr n2)). + apply eval_addlimm; EvalOp. + apply Int64.eqm_samerepr; auto with ints. +- TrivialExists. +Qed. + +Theorem eval_mullimm_base: forall n, unary_constructor_sound (mullimm_base n) (fun v => Val.mull v (Vlong n)). +Admitted. + +Theorem eval_mullimm: forall n, unary_constructor_sound (mullimm n) (fun v => Val.mull v (Vlong n)). +Admitted. + +Theorem eval_mull: binary_constructor_sound mull Val.mull. +Admitted. + +Theorem eval_divl: partial_binary_constructor_sound divl Val.divls. +Admitted. + +Theorem eval_modl: partial_binary_constructor_sound modl Val.modls. +Admitted. + +Theorem eval_divlu: partial_binary_constructor_sound divlu Val.divlu. +Admitted. + +Theorem eval_modlu: partial_binary_constructor_sound modlu Val.modlu. +Admitted. + +Theorem eval_cmplu: + forall c le a x b y v, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.cmplu (Mem.valid_pointer m) c x y = Some v -> + eval_expr ge sp e m le (cmplu c a b) v. +Proof. + unfold cmplu; intros. destruct Archi.splitlong eqn:SL. + eapply SplitLongproof.eval_cmplu; eauto. apply Archi.splitlong_ptr32; auto. + unfold Val.cmplu in H1. + destruct (Val.cmplu_bool (Mem.valid_pointer m) c x y) as [vb|] eqn:C; simpl in H1; inv H1. + destruct (is_longconst a) as [n1|] eqn:LC1; destruct (is_longconst b) as [n2|] eqn:LC2; + try (assert (x = Vlong n1) by (eapply is_longconst_inv; eauto)); + try (assert (y = Vlong n2) by (eapply is_longconst_inv; eauto)); + subst. +- simpl in C; inv C. EvalOp. destruct (Int64.cmpu c n1 n2); reflexivity. +- EvalOp. simpl. rewrite Val.swap_cmplu_bool. rewrite C; auto. +- EvalOp. simpl; rewrite C; auto. +- EvalOp. simpl; rewrite C; auto. +Qed. + +Theorem eval_cmpl: + forall c le a x b y v, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.cmpl c x y = Some v -> + eval_expr ge sp e m le (cmpl c a b) v. +Proof. + unfold cmpl; intros. destruct Archi.splitlong eqn:SL. + eapply SplitLongproof.eval_cmpl; eauto. + unfold Val.cmpl in H1. + destruct (Val.cmpl_bool c x y) as [vb|] eqn:C; simpl in H1; inv H1. + destruct (is_longconst a) as [n1|] eqn:LC1; destruct (is_longconst b) as [n2|] eqn:LC2; + try (assert (x = Vlong n1) by (eapply is_longconst_inv; eauto)); + try (assert (y = Vlong n2) by (eapply is_longconst_inv; eauto)); + subst. +- simpl in C; inv C. EvalOp. destruct (Int64.cmp c n1 n2); reflexivity. +- EvalOp. simpl. rewrite Val.swap_cmpl_bool. rewrite C; auto. +- EvalOp. simpl; rewrite C; auto. +- EvalOp. simpl; rewrite C; auto. +Qed. + +Theorem eval_longoffloat: partial_unary_constructor_sound longoffloat Val.longoffloat. +Admitted. + +Theorem eval_floatoflong: partial_unary_constructor_sound floatoflong Val.floatoflong. +Admitted. + +Theorem eval_longofsingle: partial_unary_constructor_sound longofsingle Val.longofsingle. +Admitted. + +Theorem eval_singleoflong: partial_unary_constructor_sound singleoflong Val.singleoflong. +Admitted. + +End CMCONSTR. |