1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
|
(* *********************************************************************)
(* *)
(* 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.
Lemma combine_compimm_eq_1_sound:
forall x cond args,
combine_compimm_eq_1 get x = Some(cond, args) ->
eval_condition cond (map valu args) m = Val.cmp_bool Ceq (valu x) (Vint Int.one) /\
eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Ceq (valu x) (Vint Int.one).
Proof.
intros until args. functional induction (combine_compimm_eq_1 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_ne_1_sound:
forall x cond args,
combine_compimm_ne_1 get x = Some(cond, args) ->
eval_condition cond (map valu args) m = Val.cmp_bool Cne (valu x) (Vint Int.one) /\
eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Cne (valu x) (Vint Int.one).
Proof.
intros until args. functional induction (combine_compimm_ne_1 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 ne one *)
simpl; eapply combine_compimm_ne_1_sound; eauto.
(* compimm eq zero *)
simpl; eapply combine_compimm_eq_0_sound; eauto.
(* compimm eq one *)
simpl; eapply combine_compimm_eq_1_sound; eauto.
(* compuimm ne zero *)
simpl; eapply combine_compimm_ne_0_sound; eauto.
(* compuimm ne one *)
simpl; eapply combine_compimm_ne_1_sound; eauto.
(* compuimm eq zero *)
simpl; eapply combine_compimm_eq_0_sound; eauto.
(* compuimm eq one *)
simpl; eapply combine_compimm_eq_1_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.
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.
|
