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
|
Require Import Integers.
Require Import Op Registers.
Require Import RTLpathSE_theory.
Require Import RTLpathSE_simu_specs.
(* Useful functions for conditions/branches expansion *)
Definition is_inv_cmp_int (cmp: comparison) : bool :=
match cmp with | Cle | Cgt => true | _ => false end.
Definition is_inv_cmp_float (cmp: comparison) : bool :=
match cmp with | Cge | Cgt => true | _ => false end.
Definition make_optR0 (is_x0 is_inv: bool) : option bool :=
if is_x0 then Some is_inv else None.
(* Functions to manage lists of "fake" values *)
Definition make_lhsv_cmp (is_inv: bool) (hv1 hv2: hsval) : list_hsval :=
let (hvfirst, hvsec) := if is_inv then (hv1, hv2) else (hv2, hv1) in
let lhsv := fScons hvfirst fSnil in
fScons hvsec lhsv.
Definition make_lhsv_single (hvs: hsval) : list_hsval :=
fScons hvs fSnil.
(* Expansion functions *)
Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
match cmp with
| Ceq => fSop (OEseqw optR0) lhsv
| Cne => fSop (OEsnew optR0) lhsv
| Clt | Cgt => fSop (OEsltw optR0) lhsv
| Cle | Cge =>
let hvs := (fSop (OEsltw optR0) lhsv) in
let hl := make_lhsv_single hvs in
fSop (OExoriw Int.one) hl
end.
(* Target op simplifications using "fake" values *)
Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval :=
match op, lr with
| Ocmp (Ccomp c), a1 :: a2 :: nil =>
let fv1 := fsi_sreg_get hst a1 in
let fv2 := fsi_sreg_get hst a2 in
let is_inv := is_inv_cmp_int c in
let optR0 := make_optR0 false is_inv in
let lhsv := make_lhsv_cmp is_inv fv1 fv2 in
Some (cond_int32s c lhsv optR0)
(*| Ocmp (Ccompu c), a1 :: a2 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
DO hv2 <~ hsi_sreg_get hst a2;;
let is_inv := is_inv_cmp_int c in
let optR0 := make_optR0 false is_inv in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
cond_int32u c lhsv optR0
| Ocmp (Ccompimm c imm), a1 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
expanse_condimm_int32s c hv1 imm
| Ocmp (Ccompuimm c imm), a1 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
expanse_condimm_int32u c hv1 imm
| Ocmp (Ccompl c), a1 :: a2 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
DO hv2 <~ hsi_sreg_get hst a2;;
let is_inv := is_inv_cmp_int c in
let optR0 := make_optR0 false is_inv in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
cond_int64s c lhsv optR0
| Ocmp (Ccomplu c), a1 :: a2 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
DO hv2 <~ hsi_sreg_get hst a2;;
let is_inv := is_inv_cmp_int c in
let optR0 := make_optR0 false is_inv in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
cond_int64u c lhsv optR0
| Ocmp (Ccomplimm c imm), a1 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
expanse_condimm_int64s c hv1 imm
| Ocmp (Ccompluimm c imm), a1 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
expanse_condimm_int64u c hv1 imm
| Ocmp (Ccompf c), f1 :: f2 :: nil =>
DO hv1 <~ hsi_sreg_get hst f1;;
DO hv2 <~ hsi_sreg_get hst f2;;
let is_inv := is_inv_cmp_float c in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
expanse_cond_fp false cond_float c lhsv
| Ocmp (Cnotcompf c), f1 :: f2 :: nil =>
DO hv1 <~ hsi_sreg_get hst f1;;
DO hv2 <~ hsi_sreg_get hst f2;;
let is_inv := is_inv_cmp_float c in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
expanse_cond_fp true cond_float c lhsv
| Ocmp (Ccompfs c), f1 :: f2 :: nil =>
DO hv1 <~ hsi_sreg_get hst f1;;
DO hv2 <~ hsi_sreg_get hst f2;;
let is_inv := is_inv_cmp_float c in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
expanse_cond_fp false cond_single c lhsv
| Ocmp (Cnotcompfs c), f1 :: f2 :: nil =>
DO hv1 <~ hsi_sreg_get hst f1;;
DO hv2 <~ hsi_sreg_get hst f2;;
let is_inv := is_inv_cmp_float c in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
expanse_cond_fp true cond_single c lhsv*)
| _, _ => None
end.
Lemma target_op_simplify_correct op lr hst fsv ge sp rs0 m0 st args m: forall
(H: target_op_simplify op lr hst = Some fsv)
(REF: hsilocal_refines ge sp rs0 m0 hst st)
(OK0: hsok_local ge sp rs0 m0 hst)
(OK1: seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args)
(OK2: seval_smem ge sp (si_smem st) rs0 m0 = Some m),
seval_sval ge sp (hsval_proj fsv) rs0 m0 = eval_operation ge sp op args m.
Proof. Admitted. (*
unfold target_op_simplify; simpl. congruence.
Qed.*)
Global Opaque target_op_simplify.
|
