From 132e36fa0be63eb5672eda9168403d3fb74af2fa Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 26 May 2012 07:32:01 +0000 Subject: CSE: add recognition of some combined operators, conditions, and addressing modes (cf. CombineOp.v) Memory model: cleaning up Memdata Inlining and new Constprop: updated for ARM. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1902 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- .depend | 10 +- Makefile | 2 +- arm/CombineOp.v | 107 +++++++++++ arm/CombineOpproof.v | 127 +++++++++++++ arm/Op.v | 28 ++- arm/SelectOp.vp | 2 +- arm/SelectOpproof.v | 12 +- arm/Unusedglob1.ml | 2 +- backend/CSE.v | 97 ++++++++-- backend/CSEproof.v | 175 ++++++++++++------ backend/Inliningproof.v | 10 +- backend/Linearizeproof.v | 4 +- backend/Renumberproof.v | 6 +- backend/Selectionproof.v | 4 +- cfrontend/Cminorgenproof.v | 4 +- common/Globalenvs.v | 13 +- common/Memdata.v | 447 +++++++++++++++------------------------------ common/Memory.v | 26 ++- common/Memtype.v | 1 - ia32/CombineOp.v | 101 ++++++++++ ia32/CombineOpproof.v | 130 +++++++++++++ ia32/Op.v | 24 ++- ia32/SelectOpproof.v | 10 +- powerpc/CombineOp.v | 119 ++++++++++++ powerpc/CombineOpproof.v | 142 ++++++++++++++ powerpc/Op.v | 24 ++- powerpc/SelectOp.vp | 4 +- powerpc/SelectOpproof.v | 12 +- 28 files changed, 1172 insertions(+), 471 deletions(-) create mode 100644 arm/CombineOp.v create mode 100644 arm/CombineOpproof.v create mode 100644 ia32/CombineOp.v create mode 100644 ia32/CombineOpproof.v create mode 100644 powerpc/CombineOp.v create mode 100644 powerpc/CombineOpproof.v diff --git a/.depend b/.depend index 1b504277..5cc392f7 100644 --- a/.depend +++ b/.depend @@ -49,7 +49,9 @@ $(ARCH)/ConstpropOp.vo $(ARCH)/ConstpropOp.glob: $(ARCH)/ConstpropOp.v lib/Coqli backend/Constprop.vo backend/Constprop.glob: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo $(ARCH)/ConstpropOp.vo $(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo backend/Constpropproof.vo backend/Constpropproof.glob: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo $(ARCH)/ConstpropOpproof.vo -backend/CSE.vo backend/CSE.glob: backend/CSE.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo +$(ARCH)/CombineOp.vo $(ARCH)/CombineOp.glob: $(ARCH)/CombineOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo $(ARCH)/SelectOp.vo +backend/CSE.vo backend/CSE.glob: backend/CSE.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo $(ARCH)/CombineOp.vo +$(ARCH)/CombineOpproof.vo $(ARCH)/CombineOpproof.glob: $(ARCH)/CombineOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo $(ARCH)/CombineOp.vo backend/CSE.vo backend/CSEproof.vo backend/CSEproof.glob: backend/CSEproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.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/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo backend/CSE.vo $(ARCH)/Machregs.vo $(ARCH)/Machregs.glob: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Locations.vo backend/Locations.glob: backend/Locations.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo $(ARCH)/Machregs.vo @@ -93,9 +95,9 @@ backend/Stackingtyping.vo backend/Stackingtyping.glob: backend/Stackingtyping.v backend/Machsem.vo backend/Machsem.glob: backend/Machsem.v lib/Coqlib.vo lib/Maps.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/Conventions.vo backend/Mach.vo $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asm.vo $(ARCH)/Asm.glob: $(ARCH)/Asm.v lib/Coqlib.vo lib/Maps.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 backend/Locations.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Conventions.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob: $(ARCH)/Asmgen.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.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)/Asmgenretaddr.vo $(ARCH)/Asmgenretaddr.glob: $(ARCH)/Asmgenretaddr.v lib/Coqlib.vo lib/Maps.vo common/AST.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 -$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo lib/Maps.vo common/AST.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 backend/Machsem.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo -$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.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/Conventions.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenproof1.vo +$(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenretaddr.glob: $(ARCH)/Asmgenretaddr.v lib/Coqlib.vo lib/Maps.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 +$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo lib/Maps.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 backend/Machsem.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo +$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.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/Machsem.vo backend/Machtyping.vo backend/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenproof1.vo cfrontend/Csyntax.vo cfrontend/Csyntax.glob: cfrontend/Csyntax.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Csem.vo cfrontend/Csem.glob: 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/Csyntax.vo common/Smallstep.vo cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob: cfrontend/Cstrategy.v lib/Axioms.vo 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 common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo diff --git a/Makefile b/Makefile index 8c737983..793a4d47 100644 --- a/Makefile +++ b/Makefile @@ -60,7 +60,7 @@ BACKEND=\ RTLtyping.v \ Kildall.v \ ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \ - CSE.v CSEproof.v \ + CombineOp.v CSE.v CombineOpproof.v CSEproof.v \ Machregs.v Locations.v Conventions1.v Conventions.v LTL.v LTLtyping.v \ InterfGraph.v Coloring.v Coloringproof.v \ Allocation.v Allocproof.v Alloctyping.v \ diff --git a/arm/CombineOp.v b/arm/CombineOp.v new file mode 100644 index 00000000..80486537 --- /dev/null +++ b/arm/CombineOp.v @@ -0,0 +1,107 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, 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 INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Recognition of combined operations, addressing modes and conditions + during the [CSE] phase. *) + +Require Import Coqlib. +Require Import AST. +Require Import Integers. +Require Import Op. +Require SelectOp. + +Definition valnum := positive. + +Inductive rhs : Type := + | Op: operation -> list valnum -> rhs + | Load: memory_chunk -> addressing -> list valnum -> rhs. + +Section COMBINE. + +Variable get: valnum -> option rhs. + +Function combine_compimm_ne_0 (x: valnum) : option(condition * list valnum) := + match get x with + | Some(Op (Ocmp c) ys) => Some (c, ys) + | _ => None + end. + +Function combine_compimm_eq_0 (x: valnum) : option(condition * list valnum) := + match get x with + | Some(Op (Ocmp c) ys) => Some (negate_condition c, ys) + | _ => None + end. + +Function combine_cond (cond: condition) (args: list valnum) : option(condition * list valnum) := + match cond, args with + | Ccompimm Cne n, x::nil => + if Int.eq_dec n Int.zero then combine_compimm_ne_0 x else None + | Ccompimm Ceq n, x::nil => + if Int.eq_dec n Int.zero then combine_compimm_eq_0 x else None + | Ccompuimm Cne n, x::nil => + if Int.eq_dec n Int.zero then combine_compimm_ne_0 x else None + | Ccompuimm Ceq n, x::nil => + if Int.eq_dec n Int.zero then combine_compimm_eq_0 x else None + | _, _ => None + end. + +Function combine_addr (addr: addressing) (args: list valnum) : option(addressing * list valnum) := + match addr, args with + | Aindexed n, x::nil => + match get x with + | Some(Op (Oaddimm m) ys) => Some(Aindexed (Int.add m n), ys) + | Some(Op Oadd ys) => if Int.eq_dec n Int.zero then Some(Aindexed2, ys) else None + | Some(Op (Oaddshift s) ys) => if Int.eq_dec n Int.zero then Some(Aindexed2shift s, ys) else None + | _ => None + end + | _, _ => None + end. + +Function combine_op (op: operation) (args: list valnum) : option(operation * list valnum) := + match op, args with + | Oaddimm n, x :: nil => + match get x with + | Some(Op (Oaddimm m) ys) => Some(Oaddimm (Int.add m n), ys) + | Some(Op (Orsubimm m) ys) => Some(Orsubimm (Int.add m n), ys) + | _ => None + end + | Orsubimm n, x :: nil => + match get x with + | Some(Op (Oaddimm m) ys) => Some(Orsubimm (Int.sub n m), ys) + | _ => None + end + | Oandimm n, x :: nil => + match get x with + | Some(Op (Oandimm m) ys) => Some(Oandimm (Int.and m n), ys) + | _ => None + end + | Oorimm n, x :: nil => + match get x with + | Some(Op (Oorimm m) ys) => Some(Oorimm (Int.or m n), ys) + | _ => None + end + | Oxorimm n, x :: nil => + match get x with + | Some(Op (Oxorimm m) ys) => Some(Oxorimm (Int.xor m n), ys) + | _ => None + end + | Ocmp cond, _ => + match combine_cond cond args with + | Some(cond', args') => Some(Ocmp cond', args') + | None => None + end + | _, _ => None + end. + +End COMBINE. + + diff --git a/arm/CombineOpproof.v b/arm/CombineOpproof.v new file mode 100644 index 00000000..9d297ace --- /dev/null +++ b/arm/CombineOpproof.v @@ -0,0 +1,127 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, 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 INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Recognition of combined operations, addressing modes and conditions + during the [CSE] phase. *) + +Require Import Coqlib. +Require Import AST. +Require Import Integers. +Require Import Values. +Require Import Memory. +Require Import Op. +Require Import Registers. +Require Import RTL. +Require Import CombineOp. +Require Import CSE. + +Section COMBINE. + +Variable ge: genv. +Variable sp: val. +Variable m: mem. +Variable get: valnum -> option rhs. +Variable valu: valnum -> val. +Hypothesis get_sound: forall v rhs, get v = Some rhs -> equation_holds valu ge sp m v rhs. + +Lemma combine_compimm_ne_0_sound: + forall x cond args, + combine_compimm_ne_0 get x = Some(cond, args) -> + eval_condition cond (map valu args) m = Val.cmp_bool Cne (valu x) (Vint Int.zero) /\ + eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Cne (valu x) (Vint Int.zero). +Proof. + intros until args. functional induction (combine_compimm_ne_0 get x); intros EQ; inv EQ. + (* of cmp *) + exploit get_sound; eauto. unfold equation_holds. simpl. intro EQ; inv EQ. + destruct (eval_condition cond (map valu args) m); simpl; auto. destruct b; auto. +Qed. + +Lemma combine_compimm_eq_0_sound: + forall x cond args, + combine_compimm_eq_0 get x = Some(cond, args) -> + eval_condition cond (map valu args) m = Val.cmp_bool Ceq (valu x) (Vint Int.zero) /\ + eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Ceq (valu x) (Vint Int.zero). +Proof. + intros until args. functional induction (combine_compimm_eq_0 get x); intros EQ; inv EQ. + (* of cmp *) + exploit get_sound; eauto. unfold equation_holds. simpl. intro EQ; inv EQ. + rewrite eval_negate_condition. + destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto. +Qed. + +Theorem combine_cond_sound: + forall cond args cond' args', + combine_cond get cond args = Some(cond', args') -> + eval_condition cond' (map valu args') m = eval_condition cond (map valu args) m. +Proof. + intros. functional inversion H; subst. + (* compimm ne zero *) + simpl; eapply combine_compimm_ne_0_sound; eauto. + (* compimm eq zero *) + simpl; eapply combine_compimm_eq_0_sound; eauto. + (* compuimm ne zero *) + simpl; eapply combine_compimm_ne_0_sound; eauto. + (* compuimm eq zero *) + simpl; eapply combine_compimm_eq_0_sound; eauto. +Qed. + +Theorem combine_addr_sound: + forall addr args addr' args', + combine_addr get addr args = Some(addr', args') -> + eval_addressing ge sp addr' (map valu args') = eval_addressing ge sp addr (map valu args). +Proof. + intros. functional inversion H; subst. + (* indexed - addimm *) + exploit get_sound; eauto. unfold equation_holds; simpl; intro EQ. FuncInv. + rewrite <- H0. rewrite Val.add_assoc. auto. + (* indexed 0 - add *) + exploit get_sound; eauto. unfold equation_holds; simpl; intro EQ. FuncInv. + rewrite <- H0. destruct v; destruct v0; simpl; auto; rewrite Int.add_zero; auto. + (* indexed 0 - addshift *) + exploit get_sound; eauto. unfold equation_holds; simpl; intro EQ. FuncInv. + rewrite <- H0. destruct v; destruct (eval_shift s v0); simpl; auto; rewrite Int.add_zero; auto. +Qed. + +Theorem combine_op_sound: + forall op args op' args', + combine_op get op args = Some(op', args') -> + eval_operation ge sp op' (map valu args') m = eval_operation ge sp op (map valu args) m. +Proof. + intros. functional inversion H; subst. +(* addimm - addimm *) + exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. + rewrite <- H1. rewrite Val.add_assoc. auto. +(* addimm - subimm *) +Opaque Val.sub. + exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. + rewrite <- H1. change (Vint (Int.add m0 n)) with (Val.add (Vint m0) (Vint n)). + rewrite Val.sub_add_l. auto. +(* subimm - addimm *) + exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. + rewrite <- H1. +Transparent Val.sub. + destruct v; simpl; auto. repeat rewrite Int.sub_add_opp. rewrite Int.add_assoc. + rewrite Int.neg_add_distr. decEq. decEq. decEq. apply Int.add_commut. +(* andimm - andimm *) + exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. + rewrite <- H1. rewrite Val.and_assoc. auto. +(* orimm - orimm *) + exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. + rewrite <- H1. rewrite Val.or_assoc. auto. +(* xorimm - xorimm *) + exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. + rewrite <- H1. rewrite Val.xor_assoc. auto. +(* cmp *) + simpl. decEq; decEq. eapply combine_cond_sound; eauto. +Qed. + +End COMBINE. diff --git a/arm/Op.v b/arm/Op.v index a5502c01..3353416f 100644 --- a/arm/Op.v +++ b/arm/Op.v @@ -492,22 +492,20 @@ Definition negate_condition (cond: condition): condition := end. Lemma eval_negate_condition: - forall (cond: condition) (vl: list val) (b: bool) (m: mem), - eval_condition cond vl m = Some b -> - eval_condition (negate_condition cond) vl m = Some (negb b). + forall cond vl m, + eval_condition (negate_condition cond) vl m = option_map negb (eval_condition cond vl m). Proof. - intros. - destruct cond; simpl in H; FuncInv; simpl. - rewrite Val.negate_cmp_bool; rewrite H; auto. - rewrite Val.negate_cmpu_bool; rewrite H; auto. - rewrite Val.negate_cmp_bool; rewrite H; auto. - rewrite Val.negate_cmpu_bool; rewrite H; auto. - rewrite Val.negate_cmp_bool; rewrite H; auto. - rewrite Val.negate_cmpu_bool; rewrite H; auto. - rewrite H; auto. - destruct (Val.cmpf_bool c v v0); simpl in H; inv H. rewrite negb_elim; auto. - rewrite H; auto. - destruct (Val.cmpf_bool c v (Vfloat Float.zero)); simpl in H; inv H. rewrite negb_elim; auto. + intros. destruct cond; simpl. + repeat (destruct vl; auto). apply Val.negate_cmp_bool. + repeat (destruct vl; auto). apply Val.negate_cmpu_bool. + repeat (destruct vl; auto). apply Val.negate_cmp_bool. + repeat (destruct vl; auto). apply Val.negate_cmpu_bool. + repeat (destruct vl; auto). apply Val.negate_cmp_bool. + repeat (destruct vl; auto). apply Val.negate_cmpu_bool. + repeat (destruct vl; auto). + repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0); auto. destruct b; auto. + repeat (destruct vl; auto). + repeat (destruct vl; auto). destruct (Val.cmpf_bool c v (Vfloat Float.zero)); auto. destruct b; auto. Qed. (** Shifting stack-relative references. This is used in [Stacking]. *) diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index 27b5f536..6049017c 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -111,10 +111,10 @@ Nondetfunction addimm (n: int) (e: expr) := Nondetfunction add (e1: expr) (e2: expr) := match e1, e2 with | Eop (Ointconst n1) Enil, t2 => addimm n1 t2 + | t1, Eop (Ointconst n2) Enil => addimm n2 t1 | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil)) | Eop(Oaddimm n1) (t1:::Enil), t2 => addimm n1 (Eop Oadd (t1:::t2:::Enil)) - | t1, Eop (Ointconst n2) Enil => addimm n2 t1 | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil)) | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oaddshift s) (t2:::t1:::Enil) | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oaddshift s) (t1:::t2:::Enil) diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index 1a2f5606..dc4fb54d 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -179,13 +179,9 @@ Proof. (* intconst *) destruct e0; eauto. InvEval. TrivialExists. simpl. destruct (Int.eq i Int.zero); auto. (* cmp *) - inv H. simpl in H5. - destruct (eval_condition c vl m) as []_eqn. - TrivialExists. simpl. rewrite (eval_negate_condition _ _ _ Heqo). destruct b; inv H5; auto. - inv H5. simpl. - destruct (eval_condition (negate_condition c) vl m) as []_eqn. - destruct b; [exists Vtrue | exists Vfalse]; split; auto; EvalOp; simpl. rewrite Heqo0; auto. rewrite Heqo0; auto. - exists Vundef; split; auto; EvalOp; simpl. rewrite Heqo0; auto. + inv H. simpl in H5. inv H5. + TrivialExists. simpl. rewrite eval_negate_condition. + destruct (eval_condition c vl m); auto. destruct b; auto. (* condition *) inv H. destruct v1. exploit IHa1; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. @@ -211,6 +207,7 @@ Proof. red; intros until y. unfold add; case (add_match a b); intros; InvEval. rewrite Val.add_commut. apply eval_addimm; auto. + apply eval_addimm; auto. subst. replace (Val.add (Val.add v1 (Vint n1)) (Val.add v0 (Vint n2))) with (Val.add (Val.add v1 v0) (Val.add (Vint n1) (Vint n2))). @@ -221,7 +218,6 @@ Proof. with (Val.add (Val.add v1 y) (Vint n1)). apply eval_addimm. EvalOp. repeat rewrite Val.add_assoc. decEq. apply Val.add_commut. - apply eval_addimm; auto. subst. rewrite <- Val.add_assoc. apply eval_addimm. EvalOp. subst. rewrite Val.add_commut. TrivialExists. subst. TrivialExists. diff --git a/arm/Unusedglob1.ml b/arm/Unusedglob1.ml index 04ef89a6..33a9bf8d 100644 --- a/arm/Unusedglob1.ml +++ b/arm/Unusedglob1.ml @@ -26,7 +26,7 @@ let referenced_instr = function | Pbsymb(s, _) -> [s] | Pblsymb(s, _) -> [s] | Ploadsymbol(_, s, _) -> [s] - | Pbuiltin ef -> referenced_builtin ef + | Pbuiltin(ef, _, _) -> referenced_builtin ef | _ -> [] let code_of_function f = f.fn_code diff --git a/backend/CSE.v b/backend/CSE.v index d46afdce..e9613c92 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -27,6 +27,7 @@ Require Import Registers. Require Import RTL. Require Import RTLtyping. Require Import Kildall. +Require Import CombineOp. (** * Value numbering *) @@ -49,11 +50,13 @@ Require Import Kildall. Equations are of the form [valnum = rhs], where the right-hand sides [rhs] are either arithmetic operations or memory loads. *) +(* Definition valnum := positive. Inductive rhs : Type := | Op: operation -> list valnum -> rhs | Load: memory_chunk -> addressing -> list valnum -> rhs. +*) Definition eq_valnum: forall (x y: valnum), {x=y}+{x<>y} := peq. @@ -272,8 +275,8 @@ Definition add_store (n: numbering) (chunk: memory_chunk) (addr: addressing) | _ => n2 end. -(* [reg_valnum n vn] returns a register that is mapped to value number - [vn], or [None] if no such register exists. *) +(** [reg_valnum n vn] returns a register that is mapped to value number + [vn], or [None] if no such register exists. *) Definition reg_valnum (n: numbering) (vn: valnum) : option reg := match PMap.get vn n.(num_val) with @@ -281,10 +284,19 @@ Definition reg_valnum (n: numbering) (vn: valnum) : option reg := | r :: rs => Some r end. -(* [find_rhs] and its specializations [find_op] and [find_load] - return a register that already holds the result of the given arithmetic - operation or memory load, according to the given numbering. - [None] is returned if no such register exists. *) +Fixpoint regs_valnums (n: numbering) (vl: list valnum) : option (list reg) := + match vl with + | nil => Some nil + | v1 :: vs => + match reg_valnum n v1, regs_valnums n vs with + | Some r1, Some rs => Some (r1 :: rs) + | _, _ => None + end + end. + +(** [find_rhs] return a register that already holds the result of the given arithmetic + operation or memory load, according to the given numbering. + [None] is returned if no such register exists. *) Definition find_rhs (n: numbering) (rh: rhs) : option reg := match find_valnum_rhs rh n.(num_eqs) with @@ -292,15 +304,44 @@ Definition find_rhs (n: numbering) (rh: rhs) : option reg := | Some vres => reg_valnum n vres end. -Definition find_op - (n: numbering) (op: operation) (rs: list reg) : option reg := - let (n1, vl) := valnum_regs n rs in - find_rhs n1 (Op op vl). +(** Experimental: take advantage of known equations to select more efficient + forms of operations, addressing modes, and conditions. *) + +Section REDUCE. + +Variable A: Type. +Variable f: (valnum -> option rhs) -> A -> list valnum -> option (A * list valnum). +Variable n: numbering. + +Fixpoint reduce_rec (niter: nat) (op: A) (args: list valnum) : option(A * list reg) := + match niter with + | O => None + | S niter' => + match f (fun v => find_valnum_num v n.(num_eqs)) op args with + | None => None + | Some(op', args') => + match reduce_rec niter' op' args' with + | None => + match regs_valnums n args' with Some rl => Some(op', rl) | None => None end + | Some _ as res => + res + end + end + end. + +Definition reduce (op: A) (rl: list reg) (vl: list valnum) : A * list reg := + match reduce_rec 4%nat op vl with + | None => (op, rl) + | Some res => res + end. + +End REDUCE. -Definition find_load - (n: numbering) (chunk: memory_chunk) (addr: addressing) (rs: list reg) : option reg := - let (n1, vl) := valnum_regs n rs in - find_rhs n1 (Load chunk addr vl). +(* +Parameter combine_cond: (valnum -> option rhs) -> condition -> list valnum -> option (condition * list valnum). +Parameter combine_addr: (valnum -> option rhs) -> addressing -> list valnum -> option (addressing * list valnum). +Parameter combine_op: (valnum -> option rhs) -> operation -> list valnum -> option (operation * list valnum). +*) (** * The static analysis *) @@ -442,15 +483,31 @@ Definition transf_instr (n: numbering) (instr: instruction) := match instr with | Iop op args res s => if is_trivial_op op then instr else - match find_op n op args with - | None => instr - | Some r => Iop Omove (r :: nil) res s + let (n1, vl) := valnum_regs n args in + match find_rhs n1 (Op op vl) with + | Some r => + Iop Omove (r :: nil) res s + | None => + let (op', args') := reduce _ combine_op n1 op args vl in + Iop op' args' res s end | Iload chunk addr args dst s => - match find_load n chunk addr args with - | None => instr - | Some r => Iop Omove (r :: nil) dst s + let (n1, vl) := valnum_regs n args in + match find_rhs n1 (Load chunk addr vl) with + | Some r => + Iop Omove (r :: nil) dst s + | None => + let (addr', args') := reduce _ combine_addr n1 addr args vl in + Iload chunk addr' args' dst s end + | Istore chunk addr args src s => + let (n1, vl) := valnum_regs n args in + let (addr', args') := reduce _ combine_addr n1 addr args vl in + Istore chunk addr' args' src s + | Icond cond args s1 s2 => + let (n1, vl) := valnum_regs n args in + let (cond', args') := reduce _ combine_cond n1 cond args vl in + Icond cond' args' s1 s2 | _ => instr end. diff --git a/backend/CSEproof.v b/backend/CSEproof.v index fa077161..49b213bd 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -28,6 +28,8 @@ Require Import Registers. Require Import RTL. Require Import RTLtyping. Require Import Kildall. +Require Import CombineOp. +Require Import CombineOpproof. Require Import CSE. (** * Semantic properties of value numberings *) @@ -708,7 +710,7 @@ Proof. eapply VAL. rewrite Heql. auto with coqlib. Qed. -(** Correctness of [find_op] and [find_load]: if successful and in a +(** Correctness of [find_rhs]: if successful and in a satisfiable numbering, the returned register does contain the result value of the operation or memory load. *) @@ -730,42 +732,73 @@ Proof. discriminate. Qed. -Lemma find_op_correct: - forall rs m n op args r, - wf_numbering n -> - numbering_satisfiable ge sp rs m n -> - find_op n op args = Some r -> - eval_operation ge sp op rs##args m = Some rs#r. +(** Correctness of operator reduction *) + +Section REDUCE. + +Variable A: Type. +Variable f: (valnum -> option rhs) -> A -> list valnum -> option (A * list valnum). +Variable V: Type. +Variable rs: regset. +Variable m: mem. +Variable sem: A -> list val -> option V. +Hypothesis f_sound: + forall eqs valu op args op' args', + (forall v rhs, eqs v = Some rhs -> equation_holds valu ge sp m v rhs) -> + f eqs op args = Some(op', args') -> + sem op' (map valu args') = sem op (map valu args). +Variable n: numbering. +Variable valu: valnum -> val. +Hypothesis n_holds: numbering_holds valu ge sp rs m n. +Hypothesis n_wf: wf_numbering n. + +Lemma regs_valnums_correct: + forall vl rl, regs_valnums n vl = Some rl -> rs##rl = map valu vl. Proof. - intros until r. intros WF [valu NH]. - unfold find_op. caseEq (valnum_regs n args). intros n' vl VR FIND. - assert (WF': wf_numbering n') by (eapply wf_valnum_regs; eauto). - generalize (valnum_regs_holds _ _ _ _ _ _ _ WF NH VR). - intros [valu2 [NH2 [EQ AG]]]. - rewrite <- EQ. - change (rhs_evals_to valu2 (Op op vl) m rs#r). - eapply find_rhs_correct; eauto. + induction vl; simpl; intros. + inv H. auto. + destruct (reg_valnum n a) as [r1|]_eqn; try discriminate. + destruct (regs_valnums n vl) as [rx|]_eqn; try discriminate. + inv H. simpl; decEq; auto. + eapply (proj2 n_holds); eauto. eapply reg_valnum_correct; eauto. Qed. -Lemma find_load_correct: - forall rs m n chunk addr args r, - wf_numbering n -> - numbering_satisfiable ge sp rs m n -> - find_load n chunk addr args = Some r -> - exists a, - eval_addressing ge sp addr rs##args = Some a /\ - Mem.loadv chunk m a = Some rs#r. +Lemma reduce_rec_sound: + forall niter op args op' rl' res, + reduce_rec A f n niter op args = Some(op', rl') -> + sem op (map valu args) = Some res -> + sem op' (rs##rl') = Some res. Proof. - intros until r. intros WF [valu NH]. - unfold find_load. caseEq (valnum_regs n args). intros n' vl VR FIND. - assert (WF': wf_numbering n') by (eapply wf_valnum_regs; eauto). - generalize (valnum_regs_holds _ _ _ _ _ _ _ WF NH VR). - intros [valu2 [NH2 [EQ AG]]]. - rewrite <- EQ. - change (rhs_evals_to valu2 (Load chunk addr vl) m rs#r). - eapply find_rhs_correct; eauto. + induction niter; simpl; intros. + discriminate. + destruct (f (fun v : valnum => find_valnum_num v (num_eqs n)) op args) + as [[op1 args1] | ]_eqn. + assert (sem op1 (map valu args1) = Some res). + rewrite <- H0. eapply f_sound; eauto. + simpl; intros. apply (proj1 n_holds). eapply find_valnum_num_correct; eauto. + destruct (reduce_rec A f n niter op1 args1) as [[op2 rl2] | ]_eqn. + inv H. eapply IHniter; eauto. + destruct (regs_valnums n args1) as [rl|]_eqn. + inv H. erewrite regs_valnums_correct; eauto. + discriminate. + discriminate. Qed. +Lemma reduce_sound: + forall op rl vl op' rl' res, + reduce A f n op rl vl = (op', rl') -> + map valu vl = rs##rl -> + sem op rs##rl = Some res -> + sem op' rs##rl' = Some res. +Proof. + unfold reduce; intros. + destruct (reduce_rec A f n 4%nat op vl) as [[op1 rl1] | ]_eqn; inv H. + eapply reduce_rec_sound; eauto. congruence. + auto. +Qed. + +End REDUCE. + End SATISFIABILITY. (** The numberings associated to each instruction by the static analysis @@ -942,17 +975,27 @@ Proof. (* Iop *) exists (State s' (transf_function' f approx) sp pc' (rs#res <- v) m); split. - assert (eval_operation tge sp op rs##args m = Some v). - rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. destruct (is_trivial_op op) as []_eqn. - eapply exec_Iop'; eauto. - destruct (find_op approx!!pc op args) as [r|]_eqn. - eapply exec_Iop'; eauto. simpl. - assert (eval_operation ge sp op rs##args m = Some rs#r). - eapply find_op_correct; eauto. - eapply wf_analyze; eauto. - congruence. eapply exec_Iop'; eauto. + rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. + destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn. + assert (wf_numbering approx!!pc). eapply wf_analyze; eauto. + destruct SAT as [valu1 NH1]. + exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. + assert (wf_numbering n1). eapply wf_valnum_regs; eauto. + destruct (find_rhs n1 (Op op vl)) as [r|]_eqn. + (* replaced by move *) + assert (EV: rhs_evals_to ge sp valu2 (Op op vl) m rs#r). eapply find_rhs_correct; eauto. + assert (RES: rs#r = v). red in EV. congruence. + eapply exec_Iop'; eauto. simpl. congruence. + (* possibly simplified *) + destruct (reduce operation combine_op n1 op args vl) as [op' args']_eqn. + assert (RES: eval_operation ge sp op' rs##args' m = Some v). + eapply reduce_sound with (sem := fun op vl => eval_operation ge sp op vl m); eauto. + intros; eapply combine_op_sound; eauto. + eapply exec_Iop'; eauto. + rewrite <- RES. apply eval_operation_preserved. exact symbols_preserved. + (* state matching *) econstructor; eauto. apply wt_regset_assign; auto. generalize (wt_instrs _ _ WTF pc _ H); intro WTI; inv WTI. @@ -966,17 +1009,25 @@ Proof. (* Iload *) exists (State s' (transf_function' f approx) sp pc' (rs#dst <- v) m); split. - assert (eval_addressing tge sp addr rs##args = Some a). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - destruct (find_load approx!!pc chunk addr args) as [r|]_eqn. - eapply exec_Iop'; eauto. simpl. - assert (exists a, eval_addressing ge sp addr rs##args = Some a - /\ Mem.loadv chunk m a = Some rs#r). - eapply find_load_correct; eauto. - eapply wf_analyze; eauto. - destruct H3 as [a' [A B]]. - congruence. - eapply exec_Iload'; eauto. + destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn. + assert (wf_numbering approx!!pc). eapply wf_analyze; eauto. + destruct SAT as [valu1 NH1]. + exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. + assert (wf_numbering n1). eapply wf_valnum_regs; eauto. + destruct (find_rhs n1 (Load chunk addr vl)) as [r|]_eqn. + (* replaced by move *) + assert (EV: rhs_evals_to ge sp valu2 (Load chunk addr vl) m rs#r). eapply find_rhs_correct; eauto. + assert (RES: rs#r = v). red in EV. destruct EV as [a' [EQ1 EQ2]]. congruence. + eapply exec_Iop'; eauto. simpl. congruence. + (* possibly simplified *) + destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args']_eqn. + assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a). + eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. + intros; eapply combine_addr_sound; eauto. + assert (ADDR': eval_addressing tge sp addr' rs##args' = Some a). + rewrite <- ADDR. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload; eauto. + (* state matching *) econstructor; eauto. generalize (wt_instrs _ _ WTF pc _ H); intro WTI; inv WTI. apply wt_regset_assign. auto. rewrite H8. eapply type_of_chunk_correct; eauto. @@ -986,8 +1037,17 @@ Proof. (* Istore *) exists (State s' (transf_function' f approx) sp pc' rs m'); split. - assert (eval_addressing tge sp addr rs##args = Some a). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn. + assert (wf_numbering approx!!pc). eapply wf_analyze; eauto. + destruct SAT as [valu1 NH1]. + exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. + assert (wf_numbering n1). eapply wf_valnum_regs; eauto. + destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args']_eqn. + assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a). + eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. + intros; eapply combine_addr_sound; eauto. + assert (ADDR': eval_addressing tge sp addr' rs##args' = Some a). + rewrite <- ADDR. apply eval_addressing_preserved. exact symbols_preserved. eapply exec_Istore; eauto. econstructor; eauto. eapply analysis_correct_1; eauto. simpl; auto. @@ -1035,6 +1095,15 @@ Proof. eapply kill_loads_satisfiable; eauto. (* Icond *) + destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn. + assert (wf_numbering approx!!pc). eapply wf_analyze; eauto. + elim SAT; intros valu1 NH1. + exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. + assert (wf_numbering n1). eapply wf_valnum_regs; eauto. + destruct (reduce condition combine_cond n1 cond args vl) as [cond' args']_eqn. + assert (RES: eval_condition cond' rs##args' m = Some b). + eapply reduce_sound with (sem := fun cond vl => eval_condition cond vl m); eauto. + intros; eapply combine_cond_sound; eauto. econstructor; split. eapply exec_Icond; eauto. econstructor; eauto. diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index c62e173a..f88ca81e 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -868,9 +868,10 @@ Proof. eauto. fold (saddr ctx addr). intros [a' [P Q]]. exploit Mem.loadv_inject; eauto. intros [v' [U V]]. + assert (eval_addressing tge (Vptr sp' Int.zero) (saddr ctx addr) rs' ## (sregs ctx args) = Some a'). + rewrite <- P. apply eval_addressing_preserved. exact symbols_preserved. left; econstructor; split. - eapply plus_one. eapply exec_Iload; eauto. erewrite eval_addressing_preserved; eauto. - exact symbols_preserved. + eapply plus_one. eapply exec_Iload; eauto. econstructor; eauto. apply match_stacks_inside_set_reg; auto. apply agree_set_reg; auto. @@ -885,9 +886,10 @@ Proof. fold saddr. intros [a' [P Q]]. exploit Mem.storev_mapped_inject; eauto. eapply agree_val_reg; eauto. intros [m1' [U V]]. + assert (eval_addressing tge (Vptr sp' Int.zero) (saddr ctx addr) rs' ## (sregs ctx args) = Some a'). + rewrite <- P. apply eval_addressing_preserved. exact symbols_preserved. left; econstructor; split. - eapply plus_one. eapply exec_Istore; eauto. erewrite eval_addressing_preserved; eauto. - exact symbols_preserved. + eapply plus_one. eapply exec_Istore; eauto. destruct a; simpl in H1; try discriminate. destruct a'; simpl in U; try discriminate. econstructor; eauto. diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index 50db0c65..b72268a6 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -641,7 +641,7 @@ Proof. econstructor; split. eapply plus_left'. eapply exec_Lcond_false; eauto. - change false with (negb true). apply eval_negate_condition; auto. + rewrite eval_negate_condition; rewrite H0; auto. eapply add_branch_correct; eauto. eapply is_tail_add_branch. eapply is_tail_cons_left. eapply is_tail_find_label. eauto. @@ -657,7 +657,7 @@ Proof. destruct (starts_with ifso c'). econstructor; split. apply plus_one. eapply exec_Lcond_true; eauto. - change true with (negb false). apply eval_negate_condition; auto. + rewrite eval_negate_condition; rewrite H0; auto. econstructor; eauto. econstructor; split. eapply plus_left'. diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v index a1b32b8f..5ec29e25 100644 --- a/backend/Renumberproof.v +++ b/backend/Renumberproof.v @@ -171,13 +171,15 @@ Proof. constructor; auto. eapply reach_succ; eauto. simpl; auto. (* load *) econstructor; split. - eapply exec_Iload; eauto. + assert (eval_addressing tge sp addr rs ## args = Some a). rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload; eauto. constructor; auto. eapply reach_succ; eauto. simpl; auto. (* store *) econstructor; split. - eapply exec_Istore; eauto. + assert (eval_addressing tge sp addr rs ## args = Some a). rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Istore; eauto. constructor; auto. eapply reach_succ; eauto. simpl; auto. (* call *) econstructor; split. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 4e67181a..0aa2b6bf 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -50,7 +50,7 @@ Proof. induction 1; simpl. constructor. constructor. - econstructor. eauto. apply eval_negate_condition. auto. + econstructor. eauto. rewrite eval_negate_condition. rewrite H0. auto. econstructor. eauto. destruct vb1; auto. Qed. @@ -124,7 +124,7 @@ Proof. intros. apply is_compare_neq_zero_correct with (negate_condition c). destruct c; simpl in H; simpl; try discriminate; destruct c; simpl; try discriminate; auto. - apply eval_negate_condition; auto. + rewrite eval_negate_condition. rewrite H0. auto. Qed. Lemma eval_condition_of_expr: diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index f94e0815..f7256624 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -373,9 +373,9 @@ Proof. assert (b0 = b) by congruence. subst. assert (chunk0 = chunk) by congruence. subst. econstructor. eauto. - eapply Mem.load_store_same; eauto. apply val_normalized_has_type; auto. auto. + eapply Mem.load_store_same; eauto. auto. rewrite PTree.gss. reflexivity. - red in H0. rewrite H0. auto. + red in H0. rewrite H0. auto. (* a different variable *) econstructor; eauto. rewrite <- H6. eapply Mem.load_store_other; eauto. diff --git a/common/Globalenvs.v b/common/Globalenvs.v index d7449f9b..ba038f88 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -897,7 +897,6 @@ Proof. assert (A: forall chunk v m b p m1 il m', Mem.store chunk m b p v = Some m1 -> store_init_data_list m1 b (p + size_chunk chunk) il = Some m' -> - Val.has_type v (type_of_chunk chunk) -> Mem.load chunk m' b p = Some(Val.load_result chunk v)). intros. transitivity (Mem.load chunk m1 b p). eapply store_init_data_list_outside; eauto. right. omega. @@ -909,13 +908,13 @@ Proof. intros m1 B C. exploit IHil; eauto. intro D. destruct a; simpl in B; intuition. - eapply (A Mint8unsigned (Vint i)); eauto. simpl; auto. - eapply (A Mint16unsigned (Vint i)); eauto. simpl; auto. - eapply (A Mint32 (Vint i)); eauto. simpl; auto. - eapply (A Mfloat32 (Vfloat f)); eauto. simpl; auto. - eapply (A Mfloat64 (Vfloat f)); eauto. simpl; auto. + eapply (A Mint8unsigned (Vint i)); eauto. + eapply (A Mint16unsigned (Vint i)); eauto. + eapply (A Mint32 (Vint i)); eauto. + eapply (A Mfloat32 (Vfloat f)); eauto. + eapply (A Mfloat64 (Vfloat f)); eauto. destruct (find_symbol ge i); try congruence. exists b0; split; auto. - eapply (A Mint32 (Vptr b0 i0)); eauto. simpl; auto. + eapply (A Mint32 (Vptr b0 i0)); eauto. Qed. Remark load_alloc_variables: diff --git a/common/Memdata.v b/common/Memdata.v index 47ed79e9..fd776386 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -122,7 +122,7 @@ Inductive memval: Type := (** * Encoding and decoding integers *) (** We define functions to convert between integers and lists of bytes - according to a given memory chunk. *) + of a given length *) Fixpoint bytes_of_int (n: nat) (x: Z) {struct n}: list byte := match n with @@ -208,201 +208,88 @@ Proof. auto. Qed. -Definition encode_int (c: memory_chunk) (x: int) : list byte := - let n := Int.unsigned x in - rev_if_be (match c with - | Mint8signed | Mint8unsigned => bytes_of_int 1%nat n - | Mint16signed | Mint16unsigned => bytes_of_int 2%nat n - | Mint32 => bytes_of_int 4%nat n - | Mfloat32 => bytes_of_int 4%nat 0 - | Mfloat64 => bytes_of_int 8%nat 0 - end). - -Definition decode_int (c: memory_chunk) (b: list byte) : int := - let b' := rev_if_be b in - match c with - | Mint8signed => Int.sign_ext 8 (Int.repr (int_of_bytes b')) - | Mint8unsigned => Int.zero_ext 8 (Int.repr (int_of_bytes b')) - | Mint16signed => Int.sign_ext 16 (Int.repr (int_of_bytes b')) - | Mint16unsigned => Int.zero_ext 16 (Int.repr (int_of_bytes b')) - | Mint32 => Int.repr (int_of_bytes b') - | Mfloat32 => Int.zero - | Mfloat64 => Int.zero - end. +Definition encode_int (sz: nat) (x: int) : list byte := + rev_if_be (bytes_of_int sz (Int.unsigned x)). -Lemma encode_int_length: - forall chunk n, length(encode_int chunk n) = size_chunk_nat chunk. -Proof. - intros. unfold encode_int. rewrite rev_if_be_length. - destruct chunk; rewrite length_bytes_of_int; reflexivity. -Qed. +Definition decode_int (b: list byte) : int := + Int.repr (int_of_bytes (rev_if_be b)). -Lemma decode_encode_int: - forall c x, - decode_int c (encode_int c x) = - match c with - | Mint8signed => Int.sign_ext 8 x - | Mint8unsigned => Int.zero_ext 8 x - | Mint16signed => Int.sign_ext 16 x - | Mint16unsigned => Int.zero_ext 16 x - | Mint32 => x - | Mfloat32 => Int.zero - | Mfloat64 => Int.zero - end. -Proof. - intros. unfold decode_int, encode_int; destruct c; auto; - rewrite rev_if_be_involutive. - rewrite int_of_bytes_of_int_2; auto. - apply Int.sign_ext_zero_ext. compute; auto. - rewrite int_of_bytes_of_int_2; auto. - apply Int.zero_ext_idem. compute; auto. - rewrite int_of_bytes_of_int_2; auto. - apply Int.sign_ext_zero_ext. compute; auto. - rewrite int_of_bytes_of_int_2; auto. - apply Int.zero_ext_idem. compute; auto. - rewrite int_of_bytes_of_int. - transitivity (Int.repr (Int.unsigned x)). - apply Int.eqm_samerepr. apply Int.eqm_sym. apply Int.eqmod_mod. apply two_p_gt_ZERO. omega. - apply Int.repr_unsigned. -Qed. - -Lemma encode_int8_signed_unsigned: forall n, - encode_int Mint8signed n = encode_int Mint8unsigned n. +Lemma encode_int_length: + forall sz x, length(encode_int sz x) = sz. Proof. - intros; reflexivity. + intros. unfold encode_int. rewrite rev_if_be_length. apply length_bytes_of_int. Qed. -Remark encode_8_mod: - forall x y, - Int.eqmod (two_p 8) (Int.unsigned x) (Int.unsigned y) -> - encode_int Mint8unsigned x = encode_int Mint8unsigned y. +Lemma decode_encode_int_1: + forall x, decode_int (encode_int 1%nat x) = Int.zero_ext 8 x. Proof. - intros. unfold encode_int. decEq. apply bytes_of_int_mod. auto. + intros; unfold decode_int, encode_int. rewrite rev_if_be_involutive. + rewrite int_of_bytes_of_int_2. reflexivity. auto. Qed. -Lemma encode_int8_zero_ext: - forall x, - encode_int Mint8unsigned (Int.zero_ext 8 x) = encode_int Mint8unsigned x. +Lemma decode_encode_int_2: + forall x, decode_int (encode_int 2%nat x) = Int.zero_ext 16 x. Proof. - intros. apply encode_8_mod. apply Int.eqmod_zero_ext. compute; auto. + intros; unfold decode_int, encode_int. rewrite rev_if_be_involutive. + rewrite int_of_bytes_of_int_2. reflexivity. auto. Qed. -Lemma encode_int8_sign_ext: - forall x, - encode_int Mint8signed (Int.sign_ext 8 x) = encode_int Mint8signed x. +Lemma decode_encode_int_4: + forall x, decode_int (encode_int 4%nat x) = x. Proof. - intros. repeat rewrite encode_int8_signed_unsigned. - apply encode_8_mod. eapply Int.eqmod_trans. - apply Int.eqm_eqmod_two_p. compute; auto. - apply Int.eqm_sym. apply Int.eqm_signed_unsigned. - apply Int.eqmod_sign_ext. compute; auto. + intros; unfold decode_int, encode_int. rewrite rev_if_be_involutive. + rewrite int_of_bytes_of_int. + transitivity (Int.repr (Int.unsigned x)). + apply Int.eqm_samerepr. apply Int.eqm_sym. apply Int.eqmod_mod. apply two_p_gt_ZERO. omega. + apply Int.repr_unsigned. Qed. -Lemma encode_int16_signed_unsigned: forall n, - encode_int Mint16signed n = encode_int Mint16unsigned n. +Lemma encode_int_8_mod: + forall x y, + Int.eqmod (two_p 8) (Int.unsigned x) (Int.unsigned y) -> + encode_int 1%nat x = encode_int 1%nat y. Proof. - intros; reflexivity. + intros. unfold encode_int. decEq. apply bytes_of_int_mod. auto. Qed. -Remark encode_16_mod: +Lemma encode_16_mod: forall x y, Int.eqmod (two_p 16) (Int.unsigned x) (Int.unsigned y) -> - encode_int Mint16unsigned x = encode_int Mint16unsigned y. + encode_int 2%nat x = encode_int 2%nat y. Proof. intros. unfold encode_int. decEq. apply bytes_of_int_mod. auto. Qed. -Lemma encode_int16_zero_ext: - forall x, - encode_int Mint16unsigned (Int.zero_ext 16 x) = encode_int Mint16unsigned x. -Proof. - intros. apply encode_16_mod. apply Int.eqmod_zero_ext. compute; auto. -Qed. - -Lemma encode_int16_sign_ext: - forall x, - encode_int Mint16signed (Int.sign_ext 16 x) = encode_int Mint16signed x. -Proof. - intros. repeat rewrite encode_int16_signed_unsigned. - apply encode_16_mod. eapply Int.eqmod_trans. - apply Int.eqm_eqmod_two_p. compute; auto. - apply Int.eqm_sym. apply Int.eqm_signed_unsigned. - apply Int.eqmod_sign_ext. compute; auto. -Qed. - -Lemma decode_int8_zero_ext: - forall l, - Int.zero_ext 8 (decode_int Mint8unsigned l) = decode_int Mint8unsigned l. -Proof. - intros; simpl. apply Int.zero_ext_idem. vm_compute; auto. -Qed. +(** * Encoding and decoding floats *) -Lemma decode_int8_sign_ext: - forall l, - Int.sign_ext 8 (decode_int Mint8signed l) = decode_int Mint8signed l. -Proof. - intros; simpl. apply Int.sign_ext_idem. vm_compute; auto. -Qed. +Definition encode_float_32 (f: float) : list byte := + rev_if_be (bytes_of_int 4%nat (Int.unsigned (Float.bits_of_single f))). -Lemma decode_int16_zero_ext: - forall l, - Int.zero_ext 16 (decode_int Mint16unsigned l) = decode_int Mint16unsigned l. -Proof. - intros; simpl. apply Int.zero_ext_idem. vm_compute; auto. -Qed. +Definition encode_float_64 (f: float) : list byte := + rev_if_be (bytes_of_int 8%nat (Int64.unsigned (Float.bits_of_double f))). -Lemma decode_int16_sign_ext: - forall l, - Int.sign_ext 16 (decode_int Mint16signed l) = decode_int Mint16signed l. -Proof. - intros; simpl. apply Int.sign_ext_idem. vm_compute; auto. -Qed. +Definition decode_float_32 (b: list byte) : float := + Float.single_of_bits (Int.repr (int_of_bytes (rev_if_be b))). -Lemma decode_int8_signed_unsigned: - forall l, - decode_int Mint8signed l = Int.sign_ext 8 (decode_int Mint8unsigned l). -Proof. - intros; simpl. rewrite Int.sign_ext_zero_ext; auto. vm_compute; auto. -Qed. +Definition decode_float_64 (b: list byte) : float := + Float.double_of_bits (Int64.repr (int_of_bytes (rev_if_be b))). -Lemma decode_int16_signed_unsigned: - forall l, - decode_int Mint16signed l = Int.sign_ext 16 (decode_int Mint16unsigned l). +Lemma encode_float_32_length: + forall n, length(encode_float_32 n) = 4%nat. Proof. - intros; simpl. rewrite Int.sign_ext_zero_ext; auto. vm_compute; auto. + unfold encode_float_32; intros. rewrite rev_if_be_length. apply length_bytes_of_int. Qed. -(** * Encoding and decoding floats *) - -Definition encode_float (c: memory_chunk) (f: float) : list byte := - rev_if_be (match c with - | Mint8signed | Mint8unsigned => bytes_of_int 1%nat 0 - | Mint16signed | Mint16unsigned => bytes_of_int 2%nat 0 - | Mint32 => bytes_of_int 4%nat 0 - | Mfloat32 => bytes_of_int 4%nat (Int.unsigned (Float.bits_of_single f)) - | Mfloat64 => bytes_of_int 8%nat (Int64.unsigned (Float.bits_of_double f)) - end). - -Definition decode_float (c: memory_chunk) (b: list byte) : float := - let b' := rev_if_be b in - match c with - | Mfloat32 => Float.single_of_bits (Int.repr (int_of_bytes b')) - | Mfloat64 => Float.double_of_bits (Int64.repr (int_of_bytes b')) - | _ => Float.zero - end. - -Lemma encode_float_length: - forall chunk n, length(encode_float chunk n) = size_chunk_nat chunk. +Lemma encode_float_64_length: + forall n, length(encode_float_64 n) = 8%nat. Proof. - unfold encode_float; intros. - rewrite rev_if_be_length. - destruct chunk; apply length_bytes_of_int. + unfold encode_float_64; intros. rewrite rev_if_be_length. apply length_bytes_of_int. Qed. Lemma decode_encode_float32: forall n, - decode_float Mfloat32 (encode_float Mfloat32 n) = Float.singleoffloat n. + decode_float_32 (encode_float_32 n) = Float.singleoffloat n. Proof. - intros; unfold decode_float, encode_float. + intros; unfold decode_float_32, encode_float_32. rewrite rev_if_be_involutive. rewrite int_of_bytes_of_int. rewrite <- Float.single_of_bits_of_single. decEq. @@ -412,9 +299,9 @@ Proof. Qed. Lemma decode_encode_float64: forall n, - decode_float Mfloat64 (encode_float Mfloat64 n) = n. + decode_float_64 (encode_float_64 n) = n. Proof. - intros; unfold decode_float, encode_float. + intros; unfold decode_float_64, encode_float_64. rewrite rev_if_be_involutive. rewrite int_of_bytes_of_int. set (x := Float.bits_of_double n). @@ -424,32 +311,34 @@ Proof. rewrite Int64.repr_unsigned. apply Float.double_of_bits_of_double. Qed. -Lemma encode_float8_signed_unsigned: forall n, - encode_float Mint8signed n = encode_float Mint8unsigned n. +Lemma encode_float32_eq: + forall f, encode_float_32 f = encode_int 4%nat (Float.bits_of_single f). Proof. - intros. reflexivity. + auto. Qed. -Lemma encode_float16_signed_unsigned: forall n, - encode_float Mint16signed n = encode_float Mint16unsigned n. +Lemma decode_float32_eq: + forall bl, decode_float_32 bl = Float.single_of_bits (decode_int bl). Proof. - intros. reflexivity. + auto. Qed. +(* Lemma encode_float32_cast: forall f, - encode_float Mfloat32 (Float.singleoffloat f) = encode_float Mfloat32 f. + encode_float_32 (Float.singleoffloat f) = encode_float_32 f. Proof. - intros; unfold encode_float. decEq. decEq. decEq. + intros; unfold encode_float_32. decEq. decEq. decEq. apply Float.bits_of_singleoffloat. Qed. Lemma decode_float32_cast: forall l, - Float.singleoffloat (decode_float Mfloat32 l) = decode_float Mfloat32 l. + Float.singleoffloat (decode_float_32 l) = decode_float_32 l. Proof. - intros; unfold decode_float. rewrite Float.singleoffloat_of_bits. auto. + intros; unfold decode_float_32. rewrite Float.singleoffloat_of_bits. auto. Qed. +*) (** * Encoding and decoding values *) @@ -503,17 +392,18 @@ Fixpoint check_pointer (n: nat) (b: block) (ofs: int) (vl: list memval) Definition proj_pointer (vl: list memval) : val := match vl with | Pointer b ofs n :: vl' => - if check_pointer (size_chunk_nat Mint32) b ofs vl - then Vptr b ofs - else Vundef + if check_pointer 4%nat b ofs vl then Vptr b ofs else Vundef | _ => Vundef end. Definition encode_val (chunk: memory_chunk) (v: val) : list memval := match v, chunk with - | Vptr b ofs, Mint32 => inj_pointer (size_chunk_nat Mint32) b ofs - | Vint n, _ => inj_bytes (encode_int chunk n) - | Vfloat f, _ => inj_bytes (encode_float chunk f) + | Vint n, (Mint8signed | Mint8unsigned) => inj_bytes (encode_int 1%nat n) + | Vint n, (Mint16signed | Mint16unsigned) => inj_bytes (encode_int 2%nat n) + | Vint n, Mint32 => inj_bytes (encode_int 4%nat n) + | Vptr b ofs, Mint32 => inj_pointer 4%nat b ofs + | Vfloat n, Mfloat32 => inj_bytes (encode_float_32 n) + | Vfloat n, Mfloat64 => inj_bytes (encode_float_64 n) | _, _ => list_repeat (size_chunk_nat chunk) Undef end. @@ -521,11 +411,13 @@ Definition decode_val (chunk: memory_chunk) (vl: list memval) : val := match proj_bytes vl with | Some bl => match chunk with - | Mint8signed | Mint8unsigned - | Mint16signed | Mint16unsigned | Mint32 => - Vint(decode_int chunk bl) - | Mfloat32 | Mfloat64 => - Vfloat(decode_float chunk bl) + | Mint8signed => Vint(Int.sign_ext 8 (decode_int bl)) + | Mint8unsigned => Vint(Int.zero_ext 8 (decode_int bl)) + | Mint16signed => Vint(Int.sign_ext 16 (decode_int bl)) + | Mint16unsigned => Vint(Int.zero_ext 16 (decode_int bl)) + | Mint32 => Vint(decode_int bl) + | Mfloat32 => Vfloat(decode_float_32 bl) + | Mfloat64 => Vfloat(decode_float_64 bl) end | None => match chunk with @@ -537,11 +429,8 @@ Definition decode_val (chunk: memory_chunk) (vl: list memval) : val := Lemma encode_val_length: forall chunk v, length(encode_val chunk v) = size_chunk_nat chunk. Proof. - intros. destruct v; simpl. - apply length_list_repeat. - rewrite length_inj_bytes. apply encode_int_length. - rewrite length_inj_bytes. apply encode_float_length. - destruct chunk; try (apply length_list_repeat). reflexivity. + intros. destruct v; simpl; destruct chunk; try (apply length_list_repeat); auto; + rewrite length_inj_bytes; try (apply encode_int_length). apply encode_float_64_length. Qed. Lemma check_inj_pointer: @@ -564,73 +453,62 @@ Definition decode_encode_val (v1: val) (chunk1 chunk2: memory_chunk) (v2: val) : | Vint n, Mint16signed, Mint16unsigned => v2 = Vint(Int.zero_ext 16 n) | Vint n, Mint16unsigned, Mint16unsigned => v2 = Vint(Int.zero_ext 16 n) | Vint n, Mint32, Mint32 => v2 = Vint n - | Vint n, Mint32, Mfloat32 => v2 = Vfloat(decode_float Mfloat32 (encode_int Mint32 n)) - | Vint n, _, _ => True (* nothing interesting to say about v2 *) + | Vint n, Mint32, Mfloat32 => v2 = Vfloat(Float.single_of_bits n) + | Vint n, (Mfloat32 | Mfloat64), _ => v2 = Vundef + | Vint n, _, _ => True (**r nothing meaningful to say about v2 *) | Vptr b ofs, Mint32, Mint32 => v2 = Vptr b ofs | Vptr b ofs, _, _ => v2 = Vundef | Vfloat f, Mfloat32, Mfloat32 => v2 = Vfloat(Float.singleoffloat f) - | Vfloat f, Mfloat32, Mint32 => v2 = Vint(decode_int Mint32 (encode_float Mfloat32 f)) + | Vfloat f, Mfloat32, Mint32 => v2 = Vint(Float.bits_of_single f) | Vfloat f, Mfloat64, Mfloat64 => v2 = Vfloat f + | Vfloat f, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32), _ => v2 = Vundef | Vfloat f, _, _ => True (* nothing interesting to say about v2 *) end. +Remark decode_val_undef: + forall bl chunk, decode_val chunk (Undef :: bl) = Vundef. +Proof. + intros. unfold decode_val. simpl. destruct chunk; auto. +Qed. + Lemma decode_encode_val_general: forall v chunk1 chunk2, decode_encode_val v chunk1 chunk2 (decode_val chunk2 (encode_val chunk1 v)). Proof. - intros. destruct v. -(* Vundef *) - simpl. destruct (size_chunk_nat_pos chunk1) as [psz EQ]. - rewrite EQ. simpl. - unfold decode_val. simpl. destruct chunk2; auto. -(* Vint *) - simpl. - destruct chunk1; auto; destruct chunk2; auto; unfold decode_val; - rewrite proj_inj_bytes. - rewrite decode_encode_int. auto. - rewrite encode_int8_signed_unsigned. rewrite decode_encode_int. auto. - rewrite <- encode_int8_signed_unsigned. rewrite decode_encode_int. auto. - rewrite decode_encode_int. auto. - rewrite decode_encode_int. auto. - rewrite encode_int16_signed_unsigned. rewrite decode_encode_int. auto. - rewrite <- encode_int16_signed_unsigned. rewrite decode_encode_int. auto. - rewrite decode_encode_int. auto. - rewrite decode_encode_int. auto. - reflexivity. -(* Vfloat *) - unfold decode_val, encode_val, decode_encode_val; - destruct chunk1; auto; destruct chunk2; auto; unfold decode_val; - rewrite proj_inj_bytes. - auto. +Opaque inj_pointer. + intros. + destruct v; destruct chunk1; simpl; try (apply decode_val_undef); + destruct chunk2; unfold decode_val; auto; try (rewrite proj_inj_bytes). + (* int-int *) + rewrite decode_encode_int_1. decEq. apply Int.sign_ext_zero_ext. compute; auto. + rewrite decode_encode_int_1. decEq. apply Int.zero_ext_idem. compute; auto. + rewrite decode_encode_int_1. decEq. apply Int.sign_ext_zero_ext. compute; auto. + rewrite decode_encode_int_1. decEq. apply Int.zero_ext_idem. compute; auto. + rewrite decode_encode_int_2. decEq. apply Int.sign_ext_zero_ext. compute; auto. + rewrite decode_encode_int_2. decEq. apply Int.zero_ext_idem. compute; auto. + rewrite decode_encode_int_2. decEq. apply Int.sign_ext_zero_ext. compute; auto. + rewrite decode_encode_int_2. decEq. apply Int.zero_ext_idem. compute; auto. + rewrite decode_encode_int_4. auto. + rewrite decode_float32_eq. rewrite decode_encode_int_4. auto. + rewrite encode_float32_eq. rewrite decode_encode_int_4. auto. rewrite decode_encode_float32. auto. rewrite decode_encode_float64. auto. -(* Vptr *) - unfold decode_val, encode_val, decode_encode_val; - destruct chunk1; auto; destruct chunk2; auto. - simpl. generalize (check_inj_pointer b i (size_chunk_nat Mint32)). - simpl. intro. rewrite H. auto. + change (proj_bytes (inj_pointer 4 b i)) with (@None (list byte)). simpl. + unfold proj_pointer. generalize (check_inj_pointer b i 4%nat). +Transparent inj_pointer. + simpl. intros EQ; rewrite EQ; auto. Qed. Lemma decode_encode_val_similar: forall v1 chunk1 chunk2 v2, type_of_chunk chunk1 = type_of_chunk chunk2 -> size_chunk chunk1 = size_chunk chunk2 -> - Val.has_type v1 (type_of_chunk chunk1) -> decode_encode_val v1 chunk1 chunk2 v2 -> v2 = Val.load_result chunk2 v1. Proof. - intros. - destruct v1. - simpl in *. destruct chunk2; simpl; auto. - red in H1. - destruct chunk1; simpl in H1; try contradiction; - destruct chunk2; simpl in *; discriminate || auto. - red in H1. - destruct chunk1; simpl in H1; try contradiction; - destruct chunk2; simpl in *; discriminate || auto. - red in H1. - destruct chunk1; simpl in H1; try contradiction; - destruct chunk2; simpl in *; discriminate || auto. + intros until v2; intros TY SZ DE. + destruct chunk1; destruct chunk2; simpl in TY; try discriminate; simpl in SZ; try omegaContradiction; + destruct v1; auto. Qed. Lemma decode_val_type: @@ -643,7 +521,7 @@ Proof. destruct chunk; simpl; auto. unfold proj_pointer. destruct cl; try (exact I). destruct m; try (exact I). - destruct (check_pointer (size_chunk_nat Mint32) b i (Pointer b i n :: cl)); + destruct (check_pointer 4%nat b i (Pointer b i n :: cl)); exact I. Qed. @@ -662,54 +540,25 @@ Qed. Lemma encode_val_int8_zero_ext: forall n, encode_val Mint8unsigned (Vint (Int.zero_ext 8 n)) = encode_val Mint8unsigned (Vint n). Proof. - intros; unfold encode_val. rewrite encode_int8_zero_ext. auto. + intros; unfold encode_val. decEq. apply encode_int_8_mod. apply Int.eqmod_zero_ext. compute; auto. Qed. Lemma encode_val_int8_sign_ext: forall n, encode_val Mint8signed (Vint (Int.sign_ext 8 n)) = encode_val Mint8signed (Vint n). Proof. - intros; unfold encode_val. rewrite encode_int8_sign_ext. auto. + intros; unfold encode_val. decEq. apply encode_int_8_mod. apply Int.eqmod_sign_ext'. compute; auto. Qed. Lemma encode_val_int16_zero_ext: forall n, encode_val Mint16unsigned (Vint (Int.zero_ext 16 n)) = encode_val Mint16unsigned (Vint n). Proof. - intros; unfold encode_val. rewrite encode_int16_zero_ext. auto. + intros; unfold encode_val. decEq. apply encode_16_mod. apply Int.eqmod_zero_ext. compute; auto. Qed. Lemma encode_val_int16_sign_ext: forall n, encode_val Mint16signed (Vint (Int.sign_ext 16 n)) = encode_val Mint16signed (Vint n). Proof. - intros; unfold encode_val. rewrite encode_int16_sign_ext. auto. -Qed. - -Lemma decode_val_int_inv: - forall chunk cl n, - decode_val chunk cl = Vint n -> - type_of_chunk chunk = Tint /\ - exists bytes, proj_bytes cl = Some bytes /\ n = decode_int chunk bytes. -Proof. - intros until n. unfold decode_val. destruct (proj_bytes cl). -Opaque decode_int. - destruct chunk; intro EQ; inv EQ; split; auto; exists l; auto. - destruct chunk; try congruence. unfold proj_pointer. - destruct cl; try congruence. destruct m; try congruence. - destruct (check_pointer (size_chunk_nat Mint32) b i (Pointer b i n0 :: cl)); - congruence. -Qed. - -Lemma decode_val_float_inv: - forall chunk cl f, - decode_val chunk cl = Vfloat f -> - type_of_chunk chunk = Tfloat /\ - exists bytes, proj_bytes cl = Some bytes /\ f = decode_float chunk bytes. -Proof. - intros until f. unfold decode_val. destruct (proj_bytes cl). - destruct chunk; intro EQ; inv EQ; split; auto; exists l; auto. - destruct chunk; try congruence. unfold proj_pointer. - destruct cl; try congruence. destruct m; try congruence. - destruct (check_pointer (size_chunk_nat Mint32) b i (Pointer b i n :: cl)); - congruence. + intros; unfold encode_val. decEq. apply encode_16_mod. apply Int.eqmod_sign_ext'. compute; auto. Qed. Lemma decode_val_cast: @@ -725,24 +574,24 @@ Lemma decode_val_cast: end. Proof. unfold decode_val; intros; destruct chunk; auto; destruct (proj_bytes l); auto. - unfold Val.sign_ext. decEq. symmetry. apply decode_int8_sign_ext. - unfold Val.zero_ext. decEq. symmetry. apply decode_int8_zero_ext. - unfold Val.sign_ext. decEq. symmetry. apply decode_int16_sign_ext. - unfold Val.zero_ext. decEq. symmetry. apply decode_int16_zero_ext. - unfold Val.singleoffloat. decEq. symmetry. apply decode_float32_cast. + unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. compute; auto. + unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. compute; auto. + unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. compute; auto. + unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. compute; auto. + simpl. rewrite decode_float32_eq. rewrite Float.singleoffloat_of_bits. auto. Qed. (** Pointers cannot be forged. *) Definition memval_valid_first (mv: memval) : Prop := match mv with - | Pointer b ofs n => n = pred (size_chunk_nat Mint32) + | Pointer b ofs n => n = 3%nat | _ => True end. Definition memval_valid_cont (mv: memval) : Prop := match mv with - | Pointer b ofs n => n <> pred (size_chunk_nat Mint32) + | Pointer b ofs n => n <> 3%nat | _ => True end. @@ -765,11 +614,8 @@ Proof. intros. destruct bl; simpl in *. congruence. constructor. exact I. unfold inj_bytes. intros. exploit list_in_map_inv; eauto. intros [x [A B]]. subst mv. exact I. - destruct v; simpl. - auto. - apply H0. apply encode_int_length. - apply H0. apply encode_float_length. - destruct chunk; auto. + destruct v; auto; destruct chunk; simpl; auto; try (apply H0); try (apply encode_int_length). + apply encode_float_64_length. constructor. red. auto. simpl; intros. intuition; subst mv; red; simpl; congruence. Qed. @@ -812,7 +658,7 @@ Proof. subst mv. split. red; auto. congruence. intros. destruct chunk; auto. unfold proj_pointer. destruct mvl; auto. destruct m; auto. - caseEq (check_pointer (size_chunk_nat Mint32) b i (Pointer b i n :: mvl)); auto. + caseEq (check_pointer 4%nat b i (Pointer b i n :: mvl)); auto. intros. right. exploit check_pointer_inv; eauto. simpl; intros; inv H2. constructor. red. auto. congruence. simpl; intros. intuition; subst mv; simpl; congruence. @@ -821,29 +667,34 @@ Qed. Lemma encode_val_pointer_inv: forall chunk v b ofs n mvl, encode_val chunk v = Pointer b ofs n :: mvl -> - chunk = Mint32 /\ v = Vptr b ofs /\ mvl = inj_pointer (pred (size_chunk_nat Mint32)) b ofs. -Proof. - intros until mvl. - destruct (size_chunk_nat_pos chunk) as [sz SZ]. - unfold encode_val. rewrite SZ. destruct v. - simpl. congruence. - generalize (encode_int_length chunk i). destruct (encode_int chunk i); simpl; congruence. - generalize (encode_float_length chunk f). destruct (encode_float chunk f); simpl; congruence. - destruct chunk; try (simpl; congruence). - simpl. intuition congruence. + chunk = Mint32 /\ v = Vptr b ofs /\ mvl = inj_pointer 3%nat b ofs. +Proof. + intros until mvl. + assert (A: list_repeat (size_chunk_nat chunk) Undef = Pointer b ofs n :: mvl -> + chunk = Mint32 /\ v = Vptr b ofs /\ mvl = inj_pointer 3 b ofs). + intros. destruct (size_chunk_nat_pos chunk) as [sz SZ]. rewrite SZ in H. simpl in H. discriminate. + assert (B: forall bl, length bl <> 0%nat -> inj_bytes bl = Pointer b ofs n :: mvl -> + chunk = Mint32 /\ v = Vptr b ofs /\ mvl = inj_pointer 3 b ofs). + intros. destruct bl; simpl in *; congruence. + unfold encode_val; destruct v; destruct chunk; + (apply A; assumption) || + (apply B; try (rewrite encode_int_length; congruence)) || idtac. + rewrite encode_float_32_length; congruence. + rewrite encode_float_64_length; congruence. + simpl. intros EQ; inv EQ; auto. Qed. Lemma decode_val_pointer_inv: forall chunk mvl b ofs, decode_val chunk mvl = Vptr b ofs -> - chunk = Mint32 /\ mvl = inj_pointer (size_chunk_nat Mint32) b ofs. + chunk = Mint32 /\ mvl = inj_pointer 4%nat b ofs. Proof. intros until ofs; unfold decode_val. destruct (proj_bytes mvl). destruct chunk; congruence. destruct chunk; try congruence. unfold proj_pointer. destruct mvl. congruence. destruct m; try congruence. - case_eq (check_pointer (size_chunk_nat Mint32) b0 i (Pointer b0 i n :: mvl)); intros. + case_eq (check_pointer 4%nat b0 i (Pointer b0 i n :: mvl)); intros. inv H0. split; auto. apply check_pointer_inv; auto. congruence. Qed. @@ -937,7 +788,7 @@ Lemma proj_pointer_inject: Proof. intros. unfold proj_pointer. inversion H; subst. auto. inversion H0; subst; auto. - case_eq (check_pointer (size_chunk_nat Mint32) b0 ofs1 (Pointer b0 ofs1 n :: al)); intros. + case_eq (check_pointer 4%nat b0 ofs1 (Pointer b0 ofs1 n :: al)); intros. exploit check_pointer_inject. eexact H. eauto. eauto. intro. rewrite H4. econstructor; eauto. constructor. @@ -1021,10 +872,10 @@ Theorem encode_val_inject: list_forall2 (memval_inject f) (encode_val chunk v1) (encode_val chunk v2). Proof. intros. inv H; simpl. - apply inj_bytes_inject. - apply inj_bytes_inject. - destruct chunk; try apply repeat_Undef_inject_self. - unfold inj_pointer; simpl; repeat econstructor; auto. + destruct chunk; apply inj_bytes_inject || apply repeat_Undef_inject_self. + destruct chunk; apply inj_bytes_inject || apply repeat_Undef_inject_self. + destruct chunk; try (apply repeat_Undef_inject_self). + repeat econstructor; eauto. replace (size_chunk_nat chunk) with (length (encode_val chunk v2)). apply repeat_Undef_inject_any. apply encode_val_length. Qed. @@ -1037,4 +888,4 @@ Proof. red. destruct mv; econstructor. unfold inject_id; reflexivity. rewrite Int.add_zero; auto. Qed. - + diff --git a/common/Memory.v b/common/Memory.v index 0fc663f2..49dcd7b7 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -659,7 +659,8 @@ Proof. set (cl := getN (size_chunk_nat Mint8unsigned) ofs m.(mem_contents)#b). destruct (valid_access_dec m Mint8signed b ofs Readable). rewrite pred_dec_true; auto. unfold decode_val. - destruct (proj_bytes cl); auto. rewrite decode_int8_signed_unsigned. auto. + destruct (proj_bytes cl); auto. + simpl. decEq. decEq. rewrite Int.sign_ext_zero_ext. auto. compute; auto. rewrite pred_dec_false; auto. Qed. @@ -672,7 +673,8 @@ Proof. set (cl := getN (size_chunk_nat Mint16unsigned) ofs m.(mem_contents)#b). destruct (valid_access_dec m Mint16signed b ofs Readable). rewrite pred_dec_true; auto. unfold decode_val. - destruct (proj_bytes cl); auto. rewrite decode_int16_signed_unsigned. auto. + destruct (proj_bytes cl); auto. + simpl. decEq. decEq. rewrite Int.sign_ext_zero_ext. auto. compute; auto. rewrite pred_dec_false; auto. Qed. @@ -939,13 +941,20 @@ Proof. apply inj_eq_rev; auto. Qed. +Theorem load_store_similar_2: + forall chunk', + size_chunk chunk' = size_chunk chunk -> + type_of_chunk chunk' = type_of_chunk chunk -> + load chunk' m2 b ofs = Some (Val.load_result chunk' v). +Proof. + intros. destruct (load_store_similar chunk') as [v' [A B]]. auto. + rewrite A. decEq. eapply decode_encode_val_similar with (chunk1 := chunk); eauto. +Qed. + Theorem load_store_same: - Val.has_type v (type_of_chunk chunk) -> load chunk m2 b ofs = Some (Val.load_result chunk v). Proof. - intros. - destruct (load_store_similar chunk) as [v' [A B]]. auto. - rewrite A. decEq. eapply decode_encode_val_similar; eauto. + apply load_store_similar_2; auto. Qed. Theorem load_store_other: @@ -1276,7 +1285,10 @@ Theorem store_float32_truncate: forall m b ofs n, store Mfloat32 m b ofs (Vfloat (Float.singleoffloat n)) = store Mfloat32 m b ofs (Vfloat n). -Proof. intros. apply store_similar_chunks. simpl. decEq. apply encode_float32_cast. Qed. +Proof. + intros. apply store_similar_chunks. simpl. decEq. + repeat rewrite encode_float32_eq. rewrite Float.bits_of_singleoffloat. auto. +Qed. (** ** Properties related to [storebytes]. *) diff --git a/common/Memtype.v b/common/Memtype.v index a13e8614..b7d953fc 100644 --- a/common/Memtype.v +++ b/common/Memtype.v @@ -418,7 +418,6 @@ Axiom load_store_similar: Axiom load_store_same: forall chunk m1 b ofs v m2, store chunk m1 b ofs v = Some m2 -> - Val.has_type v (type_of_chunk chunk) -> load chunk m2 b ofs = Some (Val.load_result chunk v). Axiom load_store_other: diff --git a/ia32/CombineOp.v b/ia32/CombineOp.v new file mode 100644 index 00000000..61f26e77 --- /dev/null +++ b/ia32/CombineOp.v @@ -0,0 +1,101 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, 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 INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Recognition of combined operations, addressing modes and conditions + during the [CSE] phase. *) + +Require Import Coqlib. +Require Import AST. +Require Import Integers. +Require Import Op. +Require SelectOp. + +Definition valnum := positive. + +Inductive rhs : Type := + | Op: operation -> list valnum -> rhs + | Load: memory_chunk -> addressing -> list valnum -> rhs. + +Section COMBINE. + +Variable get: valnum -> option rhs. + +Function combine_compimm_ne_0 (x: valnum) : option(condition * list valnum) := + match get x with + | Some(Op (Ocmp c) ys) => Some (c, ys) + | Some(Op (Oandimm n) ys) => Some (Cmasknotzero n, ys) + | _ => None + end. + +Function combine_compimm_eq_0 (x: valnum) : option(condition * list valnum) := + match get x with + | Some(Op (Ocmp c) ys) => Some (negate_condition c, ys) + | Some(Op (Oandimm n) ys) => Some (Cmaskzero n, ys) + | _ => None + end. + +Function combine_cond (cond: condition) (args: list valnum) : option(condition * list valnum) := + match cond, args with + | Ccompimm Cne n, x::nil => + if Int.eq_dec n Int.zero then combine_compimm_ne_0 x else None + | Ccompimm Ceq n, x::nil => + if Int.eq_dec n Int.zero then combine_compimm_eq_0 x else None + | Ccompuimm Cne n, x::nil => + if Int.eq_dec n Int.zero then combine_compimm_ne_0 x else None + | Ccompuimm Ceq n, x::nil => + if Int.eq_dec n Int.zero then combine_compimm_eq_0 x else None + | _, _ => None + end. + +Function combine_addr (addr: addressing) (args: list valnum) : option(addressing * list valnum) := + match addr, args with + | Aindexed n, x::nil => + match get x with + | Some(Op (Olea a) ys) => Some(SelectOp.offset_addressing a n, ys) + | _ => None + end + | _, _ => None + end. + +Function combine_op (op: operation) (args: list valnum) : option(operation * list valnum) := + match op, args with + | Oandimm n, x :: nil => + match get x with + | Some(Op (Oandimm m) ys) => Some(Oandimm (Int.and m n), ys) + | _ => None + end + | Oorimm n, x :: nil => + match get x with + | Some(Op (Oorimm m) ys) => Some(Oorimm (Int.or m n), ys) + | _ => None + end + | Oxorimm n, x :: nil => + match get x with + | Some(Op (Oxorimm m) ys) => Some(Oxorimm (Int.xor m n), ys) + | _ => None + end + | Olea addr, _ => + match combine_addr addr args with + | Some(addr', args') => Some(Olea addr', args') + | None => None + end + | Ocmp cond, _ => + match combine_cond cond args with + | Some(cond', args') => Some(Ocmp cond', args') + | None => None + end + | _, _ => None + end. + +End COMBINE. + + diff --git a/ia32/CombineOpproof.v b/ia32/CombineOpproof.v new file mode 100644 index 00000000..c6d25093 --- /dev/null +++ b/ia32/CombineOpproof.v @@ -0,0 +1,130 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, 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 INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Recognition of combined operations, addressing modes and conditions + during the [CSE] phase. *) + +Require Import Coqlib. +Require Import AST. +Require Import Integers. +Require Import Values. +Require Import Memory. +Require Import Op. +Require Import Registers. +Require Import RTL. +Require Import CombineOp. +Require Import CSE. + +Section COMBINE. + +Variable ge: genv. +Variable sp: val. +Variable m: mem. +Variable get: valnum -> option rhs. +Variable valu: valnum -> val. +Hypothesis get_sound: forall v rhs, get v = Some rhs -> equation_holds valu ge sp m v rhs. + +Lemma combine_compimm_ne_0_sound: + forall x cond args, + combine_compimm_ne_0 get x = Some(cond, args) -> + eval_condition cond (map valu args) m = Val.cmp_bool Cne (valu x) (Vint Int.zero) /\ + eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Cne (valu x) (Vint Int.zero). +Proof. + intros until args. functional induction (combine_compimm_ne_0 get x); intros EQ; inv EQ. + (* of cmp *) + exploit get_sound; eauto. unfold equation_holds. simpl. intro EQ; inv EQ. + destruct (eval_condition cond (map valu args) m); simpl; auto. destruct b; auto. + (* of and *) + exploit get_sound; eauto. unfold equation_holds; simpl. + destruct args; try discriminate. destruct args; try discriminate. simpl. + intros EQ; inv EQ. destruct (valu v); simpl; auto. +Qed. + +Lemma combine_compimm_eq_0_sound: + forall x cond args, + combine_compimm_eq_0 get x = Some(cond, args) -> + eval_condition cond (map valu args) m = Val.cmp_bool Ceq (valu x) (Vint Int.zero) /\ + eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Ceq (valu x) (Vint Int.zero). +Proof. + intros until args. functional induction (combine_compimm_eq_0 get x); intros EQ; inv EQ. + (* of cmp *) + exploit get_sound; eauto. unfold equation_holds. simpl. intro EQ; inv EQ. + rewrite eval_negate_condition. + destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto. + (* of and *) + exploit get_sound; eauto. unfold equation_holds; simpl. + destruct args; try discriminate. destruct args; try discriminate. simpl. + intros EQ; inv EQ. destruct (valu v); simpl; auto. +Qed. + +Theorem combine_cond_sound: + forall cond args cond' args', + combine_cond get cond args = Some(cond', args') -> + eval_condition cond' (map valu args') m = eval_condition cond (map valu args) m. +Proof. + intros. functional inversion H; subst. + (* compimm ne zero *) + simpl; eapply combine_compimm_ne_0_sound; eauto. + (* compimm eq zero *) + simpl; eapply combine_compimm_eq_0_sound; eauto. + (* compuimm ne zero *) + simpl; eapply combine_compimm_ne_0_sound; eauto. + (* compuimm eq zero *) + simpl; eapply combine_compimm_eq_0_sound; eauto. +Qed. + +Theorem combine_addr_sound: + forall addr args addr' args', + combine_addr get addr args = Some(addr', args') -> + eval_addressing ge sp addr' (map valu args') = eval_addressing ge sp addr (map valu args). +Proof. + intros. functional inversion H; subst. + exploit get_sound; eauto. unfold equation_holds; simpl; intro EQ. + assert (forall vl, + eval_addressing ge sp (SelectOp.offset_addressing a n) vl = + option_map (fun v => Val.add v (Vint n)) (eval_addressing ge sp a vl)). + intros. destruct a; simpl; repeat (destruct vl; auto); simpl. + rewrite Val.add_assoc. auto. + repeat rewrite Val.add_assoc. auto. + rewrite Val.add_assoc. auto. + repeat rewrite Val.add_assoc. auto. + unfold symbol_address. destruct (Globalenvs.Genv.find_symbol ge i); auto. + unfold symbol_address. destruct (Globalenvs.Genv.find_symbol ge i); auto. + repeat rewrite <- (Val.add_commut v). rewrite Val.add_assoc. auto. + unfold symbol_address. destruct (Globalenvs.Genv.find_symbol ge i0); auto. + repeat rewrite <- (Val.add_commut (Val.mul v (Vint i))). rewrite Val.add_assoc. auto. + rewrite Val.add_assoc; auto. + rewrite H0. rewrite EQ. auto. +Qed. + +Theorem combine_op_sound: + forall op args op' args', + combine_op get op args = Some(op', args') -> + eval_operation ge sp op' (map valu args') m = eval_operation ge sp op (map valu args) m. +Proof. + intros. functional inversion H; subst. +(* andimm *) + exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. + rewrite <- H1. rewrite Val.and_assoc. auto. +(* orimm *) + exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. + rewrite <- H1. rewrite Val.or_assoc. auto. +(* xorimm *) + exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. + rewrite <- H1. rewrite Val.xor_assoc. auto. +(* lea *) + simpl. eapply combine_addr_sound; eauto. +(* cmp *) + simpl. decEq; decEq. eapply combine_cond_sound; eauto. +Qed. + +End COMBINE. diff --git a/ia32/Op.v b/ia32/Op.v index 896badf2..0b32b88e 100644 --- a/ia32/Op.v +++ b/ia32/Op.v @@ -446,20 +446,18 @@ Definition negate_condition (cond: condition): condition := end. Lemma eval_negate_condition: - forall cond vl m b, - eval_condition cond vl m = Some b -> - eval_condition (negate_condition cond) vl m = Some (negb b). + forall cond vl m, + eval_condition (negate_condition cond) vl m = option_map negb (eval_condition cond vl m). Proof. - intros. - destruct cond; simpl in H; FuncInv; simpl. - rewrite Val.negate_cmp_bool; rewrite H; auto. - rewrite Val.negate_cmpu_bool; rewrite H; auto. - rewrite Val.negate_cmp_bool; rewrite H; auto. - rewrite Val.negate_cmpu_bool; rewrite H; auto. - rewrite H; auto. - destruct (Val.cmpf_bool c v v0); simpl in H; inv H. rewrite negb_elim; auto. - rewrite H0; auto. - rewrite <- H0. rewrite negb_elim; auto. + intros. destruct cond; simpl. + repeat (destruct vl; auto). apply Val.negate_cmp_bool. + repeat (destruct vl; auto). apply Val.negate_cmpu_bool. + repeat (destruct vl; auto). apply Val.negate_cmp_bool. + repeat (destruct vl; auto). apply Val.negate_cmpu_bool. + repeat (destruct vl; auto). + repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0); auto. destruct b; auto. + destruct vl; auto. destruct v; auto. destruct vl; auto. + destruct vl; auto. destruct v; auto. destruct vl; auto. simpl. rewrite negb_involutive. auto. Qed. (** Shifting stack-relative references. This is used in [Stacking]. *) diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v index 658a7550..9b1cd899 100644 --- a/ia32/SelectOpproof.v +++ b/ia32/SelectOpproof.v @@ -176,13 +176,9 @@ Proof. (* intconst *) destruct e0; eauto. InvEval. TrivialExists. simpl. destruct (Int.eq i Int.zero); auto. (* cmp *) - inv H. simpl in H5. - destruct (eval_condition c vl m) as []_eqn. - TrivialExists. simpl. rewrite (eval_negate_condition _ _ _ Heqo). destruct b; inv H5; auto. - inv H5. simpl. - destruct (eval_condition (negate_condition c) vl m) as []_eqn. - destruct b; [exists Vtrue | exists Vfalse]; split; auto; EvalOp; simpl. rewrite Heqo0; auto. rewrite Heqo0; auto. - exists Vundef; split; auto; EvalOp; simpl. rewrite Heqo0; auto. + inv H. simpl in H5. inv H5. + TrivialExists. simpl. rewrite eval_negate_condition. + destruct (eval_condition c vl m); auto. destruct b; auto. (* condition *) inv H. destruct v1. exploit IHa1; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. diff --git a/powerpc/CombineOp.v b/powerpc/CombineOp.v new file mode 100644 index 00000000..243da4ef --- /dev/null +++ b/powerpc/CombineOp.v @@ -0,0 +1,119 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, 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 INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Recognition of combined operations, addressing modes and conditions + during the [CSE] phase. *) + +Require Import Coqlib. +Require Import AST. +Require Import Integers. +Require Import Op. +Require SelectOp. + +Definition valnum := positive. + +Inductive rhs : Type := + | Op: operation -> list valnum -> rhs + | Load: memory_chunk -> addressing -> list valnum -> rhs. + +Section COMBINE. + +Variable get: valnum -> option rhs. + +Function combine_compimm_ne_0 (x: valnum) : option(condition * list valnum) := + match get x with + | Some(Op (Ocmp c) ys) => Some (c, ys) + | Some(Op (Oandimm n) ys) => Some (Cmasknotzero n, ys) + | _ => None + end. + +Function combine_compimm_eq_0 (x: valnum) : option(condition * list valnum) := + match get x with + | Some(Op (Ocmp c) ys) => Some (negate_condition c, ys) + | Some(Op (Oandimm n) ys) => Some (Cmaskzero n, ys) + | _ => None + end. + +Function combine_cond (cond: condition) (args: list valnum) : option(condition * list valnum) := + match cond, args with + | Ccompimm Cne n, x::nil => + if Int.eq_dec n Int.zero then combine_compimm_ne_0 x else None + | Ccompimm Ceq n, x::nil => + if Int.eq_dec n Int.zero then combine_compimm_eq_0 x else None + | Ccompuimm Cne n, x::nil => + if Int.eq_dec n Int.zero then combine_compimm_ne_0 x else None + | Ccompuimm Ceq n, x::nil => + if Int.eq_dec n Int.zero then combine_compimm_eq_0 x else None + | _, _ => None + end. + +Function combine_addr (addr: addressing) (args: list valnum) : option(addressing * list valnum) := + match addr, args with + | Aindexed n, x::nil => + match get x with + | Some(Op (Oaddimm m) ys) => Some(Aindexed (Int.add m n), ys) + | Some(Op Oadd ys) => if Int.eq_dec n Int.zero then Some(Aindexed2, ys) else None + | _ => None + end + | _, _ => None + end. + +Function combine_op (op: operation) (args: list valnum) : option(operation * list valnum) := + match op, args with + | Oaddimm n, x :: nil => + match get x with + | Some(Op (Oaddimm m) ys) => Some(Oaddimm (Int.add m n), ys) + | Some(Op (Osubimm m) ys) => Some(Osubimm (Int.add m n), ys) + | _ => None + end + | Osubimm n, x :: nil => + match get x with + | Some(Op (Oaddimm m) ys) => Some(Osubimm (Int.sub n m), ys) + | _ => None + end + | Oandimm n, x :: nil => + match get x with + | Some(Op (Oandimm m) ys) => Some(Oandimm (Int.and m n), ys) + | Some(Op (Orolm amount m) ys) => Some(Orolm amount (Int.and m n), ys) + | _ => None + end + | Oorimm n, x :: nil => + match get x with + | Some(Op (Oorimm m) ys) => Some(Oorimm (Int.or m n), ys) + | _ => None + end + | Oxorimm n, x :: nil => + match get x with + | Some(Op (Oxorimm m) ys) => Some(Oxorimm (Int.xor m n), ys) + | _ => None + end + | Orolm amount2 mask2, x :: nil => + match get x with + | Some(Op (Oandimm mask1) ys) => + Some(Orolm (Int.modu amount2 Int.iwordsize) + (Int.and (Int.rol mask1 amount2) mask2), ys) + | Some(Op (Orolm amount1 mask1) ys) => + Some(Orolm (Int.modu (Int.add amount1 amount2) Int.iwordsize) + (Int.and (Int.rol mask1 amount2) mask2), ys) + | _ => None + end + | Ocmp cond, _ => + match combine_cond cond args with + | Some(cond', args') => Some(Ocmp cond', args') + | None => None + end + | _, _ => None + end. + +End COMBINE. + + diff --git a/powerpc/CombineOpproof.v b/powerpc/CombineOpproof.v new file mode 100644 index 00000000..f493c169 --- /dev/null +++ b/powerpc/CombineOpproof.v @@ -0,0 +1,142 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, 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 INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Recognition of combined operations, addressing modes and conditions + during the [CSE] phase. *) + +Require Import Coqlib. +Require Import AST. +Require Import Integers. +Require Import Values. +Require Import Memory. +Require Import Op. +Require Import Registers. +Require Import RTL. +Require Import CombineOp. +Require Import CSE. + +Section COMBINE. + +Variable ge: genv. +Variable sp: val. +Variable m: mem. +Variable get: valnum -> option rhs. +Variable valu: valnum -> val. +Hypothesis get_sound: forall v rhs, get v = Some rhs -> equation_holds valu ge sp m v rhs. + +Lemma combine_compimm_ne_0_sound: + forall x cond args, + combine_compimm_ne_0 get x = Some(cond, args) -> + eval_condition cond (map valu args) m = Val.cmp_bool Cne (valu x) (Vint Int.zero) /\ + eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Cne (valu x) (Vint Int.zero). +Proof. + intros until args. functional induction (combine_compimm_ne_0 get x); intros EQ; inv EQ. + (* of cmp *) + exploit get_sound; eauto. unfold equation_holds. simpl. intro EQ; inv EQ. + destruct (eval_condition cond (map valu args) m); simpl; auto. destruct b; auto. + (* of and *) + exploit get_sound; eauto. unfold equation_holds; simpl. + destruct args; try discriminate. destruct args; try discriminate. simpl. + intros EQ; inv EQ. destruct (valu v); simpl; auto. +Qed. + +Lemma combine_compimm_eq_0_sound: + forall x cond args, + combine_compimm_eq_0 get x = Some(cond, args) -> + eval_condition cond (map valu args) m = Val.cmp_bool Ceq (valu x) (Vint Int.zero) /\ + eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Ceq (valu x) (Vint Int.zero). +Proof. + intros until args. functional induction (combine_compimm_eq_0 get x); intros EQ; inv EQ. + (* of cmp *) + exploit get_sound; eauto. unfold equation_holds. simpl. intro EQ; inv EQ. + rewrite eval_negate_condition. + destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto. + (* of and *) + exploit get_sound; eauto. unfold equation_holds; simpl. + destruct args; try discriminate. destruct args; try discriminate. simpl. + intros EQ; inv EQ. destruct (valu v); simpl; auto. +Qed. + +Theorem combine_cond_sound: + forall cond args cond' args', + combine_cond get cond args = Some(cond', args') -> + eval_condition cond' (map valu args') m = eval_condition cond (map valu args) m. +Proof. + intros. functional inversion H; subst. + (* compimm ne zero *) + simpl; eapply combine_compimm_ne_0_sound; eauto. + (* compimm eq zero *) + simpl; eapply combine_compimm_eq_0_sound; eauto. + (* compuimm ne zero *) + simpl; eapply combine_compimm_ne_0_sound; eauto. + (* compuimm eq zero *) + simpl; eapply combine_compimm_eq_0_sound; eauto. +Qed. + +Theorem combine_addr_sound: + forall addr args addr' args', + combine_addr get addr args = Some(addr', args') -> + eval_addressing ge sp addr' (map valu args') = eval_addressing ge sp addr (map valu args). +Proof. + intros. functional inversion H; subst. + (* indexed - addimm *) + exploit get_sound; eauto. unfold equation_holds; simpl; intro EQ. FuncInv. + rewrite <- H0. rewrite Val.add_assoc. auto. + (* indexed 0 - add *) + exploit get_sound; eauto. unfold equation_holds; simpl; intro EQ. FuncInv. + rewrite <- H0. destruct v; destruct v0; simpl; auto; rewrite Int.add_zero; auto. +Qed. + +Theorem combine_op_sound: + forall op args op' args', + combine_op get op args = Some(op', args') -> + eval_operation ge sp op' (map valu args') m = eval_operation ge sp op (map valu args) m. +Proof. + intros. functional inversion H; subst. +(* addimm - addimm *) + exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. + rewrite <- H1. rewrite Val.add_assoc. auto. +(* addimm - subimm *) +Opaque Val.sub. + exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. + rewrite <- H1. change (Vint (Int.add m0 n)) with (Val.add (Vint m0) (Vint n)). + rewrite Val.sub_add_l. auto. +(* subimm - addimm *) + exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. + rewrite <- H1. +Transparent Val.sub. + destruct v; simpl; auto. repeat rewrite Int.sub_add_opp. rewrite Int.add_assoc. + rewrite Int.neg_add_distr. decEq. decEq. decEq. apply Int.add_commut. +(* andimm - andimm *) + exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. + rewrite <- H1. rewrite Val.and_assoc. auto. +(* andimm - rolm *) + exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. + rewrite <- H1. destruct v; simpl; auto. unfold Int.rolm. rewrite Int.and_assoc. auto. +(* orimm *) + exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. + rewrite <- H1. rewrite Val.or_assoc. auto. +(* xorimm *) + exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. + rewrite <- H1. rewrite Val.xor_assoc. auto. +(* rolm - andimm *) + exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. + rewrite <- H1. rewrite <- Val.rolm_zero. rewrite Val.rolm_rolm. + rewrite (Int.add_commut Int.zero). rewrite Int.add_zero. auto. +(* rolm - rolm *) + exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. + rewrite <- H1. rewrite Val.rolm_rolm. auto. +(* cmp *) + simpl. decEq; decEq. eapply combine_cond_sound; eauto. +Qed. + +End COMBINE. diff --git a/powerpc/Op.v b/powerpc/Op.v index 76c426bd..986ea8c4 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -420,20 +420,18 @@ Definition negate_condition (cond: condition): condition := end. Lemma eval_negate_condition: - forall cond vl m b, - eval_condition cond vl m = Some b -> - eval_condition (negate_condition cond) vl m = Some (negb b). + forall cond vl m, + eval_condition (negate_condition cond) vl m = option_map negb (eval_condition cond vl m). Proof. - intros. - destruct cond; simpl in H; FuncInv; simpl. - rewrite Val.negate_cmp_bool; rewrite H; auto. - rewrite Val.negate_cmpu_bool; rewrite H; auto. - rewrite Val.negate_cmp_bool; rewrite H; auto. - rewrite Val.negate_cmpu_bool; rewrite H; auto. - rewrite H; auto. - destruct (Val.cmpf_bool c v v0); simpl in H; inv H. rewrite negb_elim; auto. - rewrite H0; auto. - rewrite <- H0. rewrite negb_elim; auto. + intros. destruct cond; simpl. + repeat (destruct vl; auto). apply Val.negate_cmp_bool. + repeat (destruct vl; auto). apply Val.negate_cmpu_bool. + repeat (destruct vl; auto). apply Val.negate_cmp_bool. + repeat (destruct vl; auto). apply Val.negate_cmpu_bool. + repeat (destruct vl; auto). + repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0); auto. destruct b; auto. + destruct vl; auto. destruct v; auto. destruct vl; auto. + destruct vl; auto. destruct v; auto. destruct vl; auto. simpl. rewrite negb_involutive. auto. Qed. (** Shifting stack-relative references. This is used in [Stacking]. *) diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index c54beed3..6c83ab76 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -119,6 +119,8 @@ Nondetfunction add (e1: expr) (e2: expr) := match e1, e2 with | Eop (Ointconst n1) Enil, t2 => addimm n1 t2 + | t1, Eop (Ointconst n2) Enil => + addimm n2 t1 | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil)) | Eop (Oaddimm n1) (t1:::Enil), t2 => @@ -127,8 +129,6 @@ Nondetfunction add (e1: expr) (e2: expr) := Eop Oadd (Eop (Oaddrsymbol s (Int.add n1 n2)) Enil ::: t2 ::: Enil) | Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) => Eop Oadd (Eop (Oaddrstack (Int.add n1 n2)) Enil ::: t2 ::: Enil) - | t1, Eop (Ointconst n2) Enil => - addimm n2 t1 | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil)) | _, _ => diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index b42503f8..e4f981d1 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -192,13 +192,9 @@ Proof. (* intconst *) destruct e0; eauto. InvEval. TrivialExists. simpl. destruct (Int.eq i Int.zero); auto. (* cmp *) - inv H. simpl in H5. - destruct (eval_condition c vl m) as []_eqn. - TrivialExists. simpl. rewrite (eval_negate_condition _ _ _ Heqo). destruct b; inv H5; auto. - inv H5. simpl. - destruct (eval_condition (negate_condition c) vl m) as []_eqn. - destruct b; [exists Vtrue | exists Vfalse]; split; auto; EvalOp; simpl. rewrite Heqo0; auto. rewrite Heqo0; auto. - exists Vundef; split; auto; EvalOp; simpl. rewrite Heqo0; auto. + inv H. simpl in H5. inv H5. + TrivialExists. simpl. rewrite eval_negate_condition. + destruct (eval_condition c vl m); auto. destruct b; auto. (* condition *) inv H. destruct v1. exploit IHa1; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. @@ -224,6 +220,7 @@ Proof. red; intros until y. unfold add; case (add_match a b); intros; InvEval. rewrite Val.add_commut. apply eval_addimm; auto. + apply eval_addimm; auto. subst. replace (Val.add (Val.add v1 (Vint n1)) (Val.add v0 (Vint n2))) with (Val.add (Val.add v1 v0) (Val.add (Vint n1) (Vint n2))). @@ -242,7 +239,6 @@ Proof. econstructor. EvalOp. simpl. reflexivity. econstructor. eauto. constructor. simpl. repeat rewrite Val.add_assoc. decEq; decEq. rewrite Val.add_commut. rewrite Val.add_permut. auto. - apply eval_addimm; auto. subst. rewrite <- Val.add_assoc. apply eval_addimm. EvalOp. TrivialExists. Qed. -- cgit