blob: 05fd884285bbea334cf76e23d00fe383838a8aed (
plain)
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
|
Require Import Coqlib.
Require Import Compopts.
Require Import AST Integers Floats.
Require Import Op CminorSel.
Require Import OpHelpers.
Require Import SelectOp SplitLong.
Require Import Values ExtValues.
Require Import DecBoolOps.
Local Open Scope cminorsel_scope.
Local Open Scope string_scope.
Definition e_andl a b := Eop Oandl (a ::: b ::: Enil).
Definition e_addl a b := Eop Oaddl (a ::: b ::: Enil).
Definition e_orl a b := Eop Oorl (a ::: b ::: Enil).
Definition e_constl n := Eop (Olongconst (Int64.repr n)) Enil.
Definition e_float_of_longu a := Eop Ofloatoflongu (a ::: Enil).
Definition e_single_of_float a := Eop Osingleoffloat (a ::: Enil).
Definition e_ite ty c vc v1 v2 := Eop (Osel c ty) (v1 ::: v2 ::: vc ::: Enil).
Definition e_cmpluimm c v n := Eop (Ocmp (Ccompluimm c n)) (v ::: Enil).
Definition a_var := Eletvar 0%nat.
Definition e_single_of_longu a :=
Elet a (e_single_of_float (e_float_of_longu
(e_ite Tlong (Ccompu0 Cne) (e_cmpluimm Cle a_var (Int64.repr (2^53))) a_var
(e_andl (e_orl a_var (e_addl (e_andl a_var (e_constl 2047))
(e_constl 2047)))
(e_constl (-2048))))))%Z.
Theorem e_single_of_longu_correct :
forall (ge : genv) (sp: val) cmenv memenv
(le : letenv) (expr_a : expr) (va : val)
(EVAL_a : eval_expr ge sp cmenv memenv le expr_a va),
eval_expr ge sp cmenv memenv le (e_single_of_longu expr_a)
(Val.maketotal (Val.singleoflongu va)).
Proof.
intros.
unfold e_single_of_longu.
repeat econstructor. eassumption.
cbn.
destruct va; cbn.
all: try reflexivity.
f_equal.
unfold Int64.ltu.
change (Int64.unsigned (Int64.repr 9007199254740992))%Z with 9007199254740992%Z.
destruct zlt as [LT | GE]; cbn.
{ change (Int.eq Int.zero Int.zero) with true. cbn.
f_equal.
symmetry.
apply Float32.of_longu_double_2.
lia.
}
change (Int.eq Int.one Int.zero) with false. cbn.
f_equal.
symmetry.
apply Float32.of_longu_double_1.
lia.
Qed.
|
