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
|
Require Import Coqlib.
Require Import Integers.
Require Import Values.
Definition is_bitfield stop start :=
(Z.leb start stop)
&& (Z.geb start Z.zero)
&& (Z.ltb stop Int.zwordsize).
Definition extfz stop start v :=
if is_bitfield stop start
then
let stop' := Z.add stop Z.one in
match v with
| Vint w =>
Vint (Int.shru (Int.shl w (Int.repr (Z.sub Int.zwordsize stop'))) (Int.repr (Z.sub Int.zwordsize (Z.sub stop' start))))
| _ => Vundef
end
else Vundef.
Definition extfs stop start v :=
if is_bitfield stop start
then
let stop' := Z.add stop Z.one in
match v with
| Vint w =>
Vint (Int.shr (Int.shl w (Int.repr (Z.sub Int.zwordsize stop'))) (Int.repr (Z.sub Int.zwordsize (Z.sub stop' start))))
| _ => Vundef
end
else Vundef.
Definition zbitfield_mask stop start :=
(Z.shiftl 1 (Z.succ stop)) - (Z.shiftl 1 start).
Definition bitfield_mask stop start :=
Vint(Int.repr (zbitfield_mask stop start)).
Definition bitfield_maskl stop start :=
Vlong(Int64.repr (zbitfield_mask stop start)).
Definition insf stop start prev fld :=
let mask := bitfield_mask stop start in
if is_bitfield stop start
then
Val.or (Val.and prev (Val.notint mask))
(Val.and (Val.shl fld (Vint (Int.repr start))) mask)
else Vundef.
Definition is_bitfieldl stop start :=
(Z.leb start stop)
&& (Z.geb start Z.zero)
&& (Z.ltb stop Int64.zwordsize).
Definition extfzl stop start v :=
if is_bitfieldl stop start
then
let stop' := Z.add stop Z.one in
match v with
| Vlong w =>
Vlong (Int64.shru' (Int64.shl' w (Int.repr (Z.sub Int64.zwordsize stop'))) (Int.repr (Z.sub Int64.zwordsize (Z.sub stop' start))))
| _ => Vundef
end
else Vundef.
Definition extfsl stop start v :=
if is_bitfieldl stop start
then
let stop' := Z.add stop Z.one in
match v with
| Vlong w =>
Vlong (Int64.shr' (Int64.shl' w (Int.repr (Z.sub Int64.zwordsize stop'))) (Int.repr (Z.sub Int64.zwordsize (Z.sub stop' start))))
| _ => Vundef
end
else Vundef.
Definition insfl stop start prev fld :=
let mask := bitfield_maskl stop start in
if is_bitfieldl stop start
then
Val.orl (Val.andl prev (Val.notl mask))
(Val.andl (Val.shll fld (Vint (Int.repr start))) mask)
else Vundef.
Fixpoint highest_bit (x : Z) (n : nat) : Z :=
match n with
| O => 0
| S n1 =>
let n' := Z.of_N (N_of_nat n) in
if Z.testbit x n'
then n'
else highest_bit x n1
end.
Definition int_highest_bit (x : int) : Z :=
highest_bit (Int.unsigned x) (31%nat).
Definition int64_highest_bit (x : int64) : Z :=
highest_bit (Int64.unsigned x) (63%nat).
Definition val_shrx (v1 v2: val): val :=
match v1, v2 with
| Vint n1, Vint n2 =>
if Int.ltu n2 (Int.repr 31)
then Vint(Int.shrx n1 n2)
else Vundef
| _, _ => Vundef
end.
Definition val_shrxl (v1 v2: val): val :=
match v1, v2 with
| Vlong n1, Vint n2 =>
if Int.ltu n2 (Int.repr 63)
then Vlong(Int64.shrx' n1 n2)
else Vundef
| _, _ => Vundef
end.
Remark modulus_fits_64: Int.modulus < Int64.max_unsigned.
Proof.
compute.
trivial.
Qed.
Remark unsigned64_repr :
forall i,
-1 < i < Int.modulus ->
Int64.unsigned (Int64.repr i) = i.
Proof.
intros i H.
destruct H as [Hlow Hhigh].
apply Int64.unsigned_repr.
split. { omega. }
pose proof modulus_fits_64.
omega.
Qed.
Theorem divu_is_divlu: forall v1 v2 : val,
Val.divu v1 v2 =
match Val.divlu (Val.longofintu v1) (Val.longofintu v2) with
| None => None
| Some q => Some (Val.loword q)
end.
Proof.
intros.
destruct v1; simpl; trivial.
destruct v2; simpl; trivial.
destruct i as [i_val i_range].
destruct i0 as [i0_val i0_range].
simpl.
unfold Int.eq, Int64.eq, Int.zero, Int64.zero.
simpl.
rewrite Int.unsigned_repr by (compute; split; discriminate).
rewrite (Int64.unsigned_repr 0) by (compute; split; discriminate).
rewrite (unsigned64_repr i0_val) by assumption.
destruct (zeq i0_val 0) as [ | Hnot0]; simpl; trivial.
f_equal. f_equal.
unfold Int.divu, Int64.divu. simpl.
rewrite (unsigned64_repr i_val) by assumption.
rewrite (unsigned64_repr i0_val) by assumption.
unfold Int64.loword.
rewrite Int64.unsigned_repr.
reflexivity.
destruct (Z.eq_dec i0_val 1).
{subst i0_val.
pose proof modulus_fits_64.
rewrite Zdiv_1_r.
omega.
}
destruct (Z.eq_dec i_val 0).
{ subst i_val. compute.
split;
intro ABSURD;
discriminate ABSURD. }
assert ((i_val / i0_val) < i_val).
{ apply Z_div_lt; omega. }
split.
{ apply Z_div_pos; omega. }
pose proof modulus_fits_64.
omega.
Qed.
|
