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
173
174
175
176
177
178
179
180
181
182
183
184
185
|
(* *********************************************************************)
(* *)
(* 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. *)
(* *)
(* *********************************************************************)
Require Import Coqlib.
Require Import Compopts.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.
Require Import Op.
Require Import ValueDomain.
Require Import RTL.
(** Value analysis for IA32 operators *)
Definition eval_static_condition (cond: condition) (vl: list aval): abool :=
match cond, vl with
| Ccomp c, v1 :: v2 :: nil => cmp_bool c v1 v2
| Ccompu c, v1 :: v2 :: nil => cmpu_bool c v1 v2
| Ccompimm c n, v1 :: nil => cmp_bool c v1 (I n)
| Ccompuimm c n, v1 :: nil => cmpu_bool c v1 (I n)
| Ccompf c, v1 :: v2 :: nil => cmpf_bool c v1 v2
| Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2)
| Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2
| Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2)
| Cmaskzero n, v1 :: nil => maskzero v1 n
| Cmasknotzero n, v1 :: nil => cnot (maskzero v1 n)
| _, _ => Bnone
end.
Definition eval_static_addressing (addr: addressing) (vl: list aval): aval :=
match addr, vl with
| Aindexed n, v1::nil => add v1 (I n)
| Aindexed2 n, v1::v2::nil => add (add v1 v2) (I n)
| Ascaled sc ofs, v1::nil => add (mul v1 (I sc)) (I ofs)
| Aindexed2scaled sc ofs, v1::v2::nil => add v1 (add (mul v2 (I sc)) (I ofs))
| Aglobal s ofs, nil => Ptr (Gl s ofs)
| Abased s ofs, v1::nil => add (Ptr (Gl s ofs)) v1
| Abasedscaled sc s ofs, v1::nil => add (Ptr (Gl s ofs)) (mul v1 (I sc))
| Ainstack ofs, nil => Ptr(Stk ofs)
| _, _ => Vbot
end.
Definition eval_static_operation (op: operation) (vl: list aval): aval :=
match op, vl with
| Omove, v1::nil => v1
| Ointconst n, nil => I n
| Ofloatconst n, nil => if propagate_float_constants tt then F n else ftop
| Osingleconst n, nil => if propagate_float_constants tt then FS n else ftop
| Oindirectsymbol id, nil => Ptr (Gl id Int.zero)
| Ocast8signed, v1 :: nil => sign_ext 8 v1
| Ocast8unsigned, v1 :: nil => zero_ext 8 v1
| Ocast16signed, v1 :: nil => sign_ext 16 v1
| Ocast16unsigned, v1 :: nil => zero_ext 16 v1
| Oneg, v1::nil => neg v1
| Osub, v1::v2::nil => sub v1 v2
| Omul, v1::v2::nil => mul v1 v2
| Omulimm n, v1::nil => mul v1 (I n)
| Omulhs, v1::v2::nil => mulhs v1 v2
| Omulhu, v1::v2::nil => mulhu v1 v2
| Odiv, v1::v2::nil => divs v1 v2
| Odivu, v1::v2::nil => divu v1 v2
| Omod, v1::v2::nil => mods v1 v2
| Omodu, v1::v2::nil => modu v1 v2
| Oand, v1::v2::nil => and v1 v2
| Oandimm n, v1::nil => and v1 (I n)
| Oor, v1::v2::nil => or v1 v2
| Oorimm n, v1::nil => or v1 (I n)
| Oxor, v1::v2::nil => xor v1 v2
| Oxorimm n, v1::nil => xor v1 (I n)
| Onot, v1::nil => notint v1
| Oshl, v1::v2::nil => shl v1 v2
| Oshlimm n, v1::nil => shl v1 (I n)
| Oshr, v1::v2::nil => shr v1 v2
| Oshrimm n, v1::nil => shr v1 (I n)
| Oshrximm n, v1::nil => shrx v1 (I n)
| Oshru, v1::v2::nil => shru v1 v2
| Oshruimm n, v1::nil => shru v1 (I n)
| Ororimm n, v1::nil => ror v1 (I n)
| Oshldimm n, v1::v2::nil => or (shl v1 (I n)) (shru v2 (I (Int.sub Int.iwordsize n)))
| Olea addr, _ => eval_static_addressing addr vl
| Onegf, v1::nil => negf v1
| Oabsf, v1::nil => absf v1
| Oaddf, v1::v2::nil => addf v1 v2
| Osubf, v1::v2::nil => subf v1 v2
| Omulf, v1::v2::nil => mulf v1 v2
| Odivf, v1::v2::nil => divf v1 v2
| Onegfs, v1::nil => negfs v1
| Oabsfs, v1::nil => absfs v1
| Oaddfs, v1::v2::nil => addfs v1 v2
| Osubfs, v1::v2::nil => subfs v1 v2
| Omulfs, v1::v2::nil => mulfs v1 v2
| Odivfs, v1::v2::nil => divfs v1 v2
| Osingleoffloat, v1::nil => singleoffloat v1
| Ofloatofsingle, v1::nil => floatofsingle v1
| Ointoffloat, v1::nil => intoffloat v1
| Ofloatofint, v1::nil => floatofint v1
| Ointofsingle, v1::nil => intofsingle v1
| Osingleofint, v1::nil => singleofint v1
| Omakelong, v1::v2::nil => longofwords v1 v2
| Olowlong, v1::nil => loword v1
| Ohighlong, v1::nil => hiword v1
| Ocmp c, _ => of_optbool (eval_static_condition c vl)
| _, _ => Vbot
end.
Section SOUNDNESS.
Variable bc: block_classification.
Variable ge: genv.
Hypothesis GENV: genv_match bc ge.
Variable sp: block.
Hypothesis STACK: bc sp = BCstack.
Theorem eval_static_condition_sound:
forall cond vargs m aargs,
list_forall2 (vmatch bc) vargs aargs ->
cmatch (eval_condition cond vargs m) (eval_static_condition cond aargs).
Proof.
intros until aargs; intros VM.
inv VM.
destruct cond; auto with va.
inv H0.
destruct cond; simpl; eauto with va.
inv H2.
destruct cond; simpl; eauto with va.
destruct cond; auto with va.
Qed.
Lemma symbol_address_sound:
forall id ofs,
vmatch bc (Genv.symbol_address ge id ofs) (Ptr (Gl id ofs)).
Proof.
intros; apply symbol_address_sound; apply GENV.
Qed.
Hint Resolve symbol_address_sound: va.
Ltac InvHyps :=
match goal with
| [H: None = Some _ |- _ ] => discriminate
| [H: Some _ = Some _ |- _] => inv H
| [H1: match ?vl with nil => _ | _ :: _ => _ end = Some _ ,
H2: list_forall2 _ ?vl _ |- _ ] => inv H2; InvHyps
| _ => idtac
end.
Theorem eval_static_addressing_sound:
forall addr vargs vres aargs,
eval_addressing ge (Vptr sp Int.zero) addr vargs = Some vres ->
list_forall2 (vmatch bc) vargs aargs ->
vmatch bc vres (eval_static_addressing addr aargs).
Proof.
unfold eval_addressing, eval_static_addressing; intros;
destruct addr; InvHyps; eauto with va.
rewrite Int.add_zero_l; auto with va.
Qed.
Theorem eval_static_operation_sound:
forall op vargs m vres aargs,
eval_operation ge (Vptr sp Int.zero) op vargs m = Some vres ->
list_forall2 (vmatch bc) vargs aargs ->
vmatch bc vres (eval_static_operation op aargs).
Proof.
unfold eval_operation, eval_static_operation; intros;
destruct op; InvHyps; eauto with va.
destruct (propagate_float_constants tt); constructor.
destruct (propagate_float_constants tt); constructor.
eapply eval_static_addressing_sound; eauto.
apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
Qed.
End SOUNDNESS.
|
