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
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
|
Require Export Language Conversion QhasmEvalCommon QhasmUtil.
Require Export Pseudo AlmostQhasm State.
Require Export Bedrock.Word NArith NPeano Euclid.
Require Export List Sumbool Vector.
Module PseudoConversion <: Conversion Pseudo AlmostQhasm.
Import QhasmCommon AlmostQhasm EvalUtil Util Pseudo StateCommon.
Import ListNotations.
Definition MMap {w} := NatM.t (Mapping w).
Definition mempty {w} := NatM.empty (Mapping w).
Definition FMap {w} := NatM.t (AlmostProgram * (list (Mapping w))).
Definition fempty {w} := NatM.empty (AlmostProgram * (list (Mapping w))).
Definition getStart {w s n m} (prog: @Pseudo w s n m) :=
let ns := (fix getStart' {n' m'} (p': @Pseudo w s n' m') :=
match p' with
| PVar _ _ i => [proj1_sig i]
| PBin _ _ p => getStart' p
| PDual _ _ p => getStart' p
| PCarry _ _ p => getStart' p
| PShift _ _ _ p => getStart' p
| PIf _ _ _ _ _ l r => (getStart' l) ++ (getStart' r)
| PFunExp _ p _ => getStart' p
| PLet _ k _ a b => (n + k) :: (getStart' a) ++ (getStart' b)
| PComb _ _ _ a b => (getStart' a) ++ (getStart' b)
| PCall _ _ _ p => getStart' p
| _ => []
end) _ _ prog in
maxN (n :: m :: ns).
Definition addMap {T} (a b: NatM.t T): NatM.t T :=
(fix add' (m: NatM.t T) (elts: list (nat * T)%type) :=
match elts with
| [] => m
| (k, v) :: elts' => add' (NatM.add k v m) elts'
end) a (NatM.elements b).
Fixpoint convertProgram' {n m} (prog: Pseudo n m) (start: nat) (M: MMap) (F: FMap):
option (AlmostProgram * (list (Mapping width)) * MMap * FMap) :=
let rM := fun (x: nat) => regM _ (reg width_spec x) in
let sM := fun (x: nat) => stackM _ (stack width_spec x) in
let reg' := reg width_spec in
let stack' := stack width_spec in
let const' := const width_spec in
let G := fun (k: nat) =>
match (NatM.find k M) with
| Some v => v
| _ => rM k (* TODO: more intelligent defaults *)
end in
let madd := fun (k: nat) (f: nat -> Mapping width) => NatM.add k (f k) in
let fadd := fun (k: nat) (f: AlmostProgram) (r: list (Mapping width)) => NatM.add k (f, r) in
match prog with
| PVar n (Some true) i => Some (ASkip, [rM i], madd i rM M, F)
| PVar n (Some false) i => Some (ASkip, [sM i], madd i sM M, F)
| PVar n None i => Some (ASkip, [G i], M, F)
| PConst n c => Some (AAssign (AConstInt (reg' start) (const' c)),
[rM start], madd start rM M, F)
| PMem n m v i => Some (AAssign (ARegMem (reg' start) (mem width_spec v) i),
[rM start], madd start rM M, F)
| PBin n o p =>
match (convertProgram' p start M F) with
| Some (p', [regM (reg _ _ a); regM (reg _ _ b)], M', F') =>
Some (ASeq p' (AOp (IOpReg o (reg' a) (reg' b))),
[rM a], madd a rM (madd b rM M'), F')
| Some (p', [regM (reg _ _ a); constM c], M', F') =>
Some (ASeq p' (AOp (IOpConst o (reg' a) c)),
[rM a], madd a rM M', F')
| Some (p', [regM (reg _ _ a); memM _ b i], M', F') =>
Some (ASeq p' (AOp (IOpMem o (reg' a) b i)),
[rM a], madd a rM M', F')
| Some (p', [regM (reg _ _ a); stackM (stack _ _ b)], M', F') =>
Some (ASeq p' (AOp (IOpStack o (reg' a) (stack' b))),
[rM a], madd a rM (madd b sM M'), F')
| _ => None
end
| PCarry n o p =>
match (convertProgram' p start M F) with
| Some (p', [regM (reg _ _ a); regM (reg _ _ b)], M', F') =>
Some (ASeq p' (AOp (COp o (reg' a) (reg' b))),
[rM a], madd a rM (madd b rM M'), F')
| _ => None
end
| PDual n o p =>
match (convertProgram' p (S start) M F) with
| Some (p', [regM (reg _ _ a); regM (reg _ _ b)], M', F') =>
Some (ASeq p' (AOp (DOp o (reg' a) (reg' b) (Some (reg' start)))),
[rM a; rM start], madd a rM (madd b rM (madd start rM M')), F')
| _ => None
end
| PShift n o x p =>
match (convertProgram' p start M F) with
| Some (p', [regM (reg _ _ a)], M', F') =>
Some (ASeq p' (AOp (ROp o (reg' a) x)),
[rM a], madd a rM M', F')
| _ => None
end
| PLet n k m f g =>
match (convertProgram' f start M F) with
| None => None
| Some (fp, fm, M', F') =>
match (convertProgram' g (start + (length fm)) M' F') with
| None => None
| Some (gp, gm, M'', F'') => Some (ASeq fp gp, gm, M'', F'')
end
end
| PComb n a b f g =>
match (convertProgram' f start M F) with
| None => None
| Some (fp, fm, M', F') =>
match (convertProgram' g (start + (length fm)) M' F') with
| None => None
| Some (gp, gm, M'', F'') => Some (ASeq fp gp, fm ++ gm, M'', F'')
end
end
| PIf n m o i0 i1 l r =>
match (convertProgram' l start M F) with
| None => None
| Some (lp, lr, lM, lF) =>
match (convertProgram' r start lM lF) with
| None => None
| Some (rp, rr, M', F') =>
if (list_eq_dec mapping_dec lr rr)
then
match (G (proj1_sig i0), G (proj1_sig i1)) with
| (regM r0, regM r1) => Some (ACond (CReg _ o r0 r1) lp rp, lr, M', F')
| (regM r, constM c) => Some (ACond (CConst _ o r c) lp rp, lr, M', F')
| _ => None
end
else None
end
end
| PFunExp n f e =>
match (convertProgram' f (S start) M F) with
| Some (fp, fr, M', F') =>
let a := start in
Some (ASeq
(AAssign (AConstInt (reg' a) (const' (natToWord _ O))))
(AWhile (CConst _ TLt (reg' a) (const' (natToWord _ e)))
(ASeq fp (AOp (IOpConst Add (reg' a) (const' (natToWord _ 1)))))),
fr, madd a rM M', F')
| _ => None
end
| PCall n m lbl f =>
match (convertProgram' f start M F) with
| Some (fp, fr, M', F') =>
let F'' := NatM.add lbl (fp, fr) F' in
Some (ACall lbl, fr, M', F'')
| None => None
end
end.
Definition convertProgram (prog: Pseudo inVars outVars): option AlmostProgram :=
match (convertProgram' prog (max inVars outVars) mempty fempty) with
| Some (prog', _, M, F) =>
Some (fold_left
(fun p0 t => match t with | (k, (v, _)) => ADef k v p0 end)
prog'
(of_list (NatM.elements F)))
| _ => None
end.
Fixpoint convertState (st: AlmostQhasm.State): option State :=
let vars := max inVars outVars in
let try_cons := fun {T} (x: option T) (l: list T) =>
match x with | Some x' => x' :: l | _ => l end in
let get := fun i =>
match (FullState.getReg (reg width_spec i) st,
FullState.getStack (stack width_spec i) st) with
| (Some v, _) => Some v
| (_, Some v) => Some v
| _ => None
end in
let varList := (fix cs' (n: nat) :=
try_cons (get (vars - n)) (match n with | O => [] | S m => cs' m end)) vars in
match st with
| FullState.fullState _ _ memState _ carry =>
if (Nat.eq_dec (length varList) vars)
then Some (varList, memState, carry)
else None
end.
Lemma convert_spec: forall a a' b b' prog prog',
convertProgram prog = Some prog' ->
convertState a = Some a' -> convertState b = Some b' ->
AlmostQhasm.evaluatesTo prog' a b <-> evaluatesTo prog a' b'.
Admitted.
End PseudoConversion.
|
