forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
loop_to_wordScript.sml
158 lines (139 loc) · 5.24 KB
/
loop_to_wordScript.sml
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
(*
Compilation from looLang to wordLang.
*)
open preamble loopLangTheory
wordLangTheory
loop_removeTheory
val _ = new_theory "loop_to_word"
val _ = set_grammar_ancestry
["loopLang", "wordLang",
"backend_common"];
Definition find_var_def:
find_var ctxt v =
case lookup v ctxt of
| NONE => 0
| SOME n => (n:num)
End
Definition find_reg_imm_def:
(find_reg_imm ctxt (Imm w) = Imm w) ∧
(find_reg_imm ctxt (Reg n) = Reg (find_var ctxt n))
End
Definition comp_exp_def :
(comp_exp ctxt (loopLang$Const w) = wordLang$Const w) /\
(comp_exp ctxt (Var n) = Var (find_var ctxt n)) /\
(comp_exp ctxt (Lookup m) = Lookup (Temp m)) /\
(comp_exp ctxt (BaseAddr) = Lookup CurrHeap) /\
(comp_exp ctxt (Load exp) = Load (comp_exp ctxt exp)) /\
(comp_exp ctxt (Shift s exp n) = Shift s (comp_exp ctxt exp) n) /\
(comp_exp ctxt (Op op wexps) =
let wexps = MAP (comp_exp ctxt) wexps in
Op op wexps)
Termination
WF_REL_TAC ‘measure (loopLang$exp_size (K 0) o SND)’ >>
rw [] >>
rename [‘MEM x xs’] >>
Induct_on ‘xs’ >> fs [] >>
fs [loopLangTheory.exp_size_def] >>
rw [] >> fs []
End
Definition toNumSet_def:
toNumSet [] = LN ∧
toNumSet (n::ns) = insert n () (toNumSet ns)
End
Definition fromNumSet_def:
fromNumSet t = MAP FST (toAList t)
End
Definition mk_new_cutset_def:
mk_new_cutset ctxt (l:num_set) =
insert 0 () (toNumSet (MAP (find_var ctxt) (fromNumSet l)))
End
Definition comp_def:
(comp ctxt Skip l = (wordLang$Skip,l)) /\
(comp ctxt (Assign n e) l =
(Assign (find_var ctxt n) (comp_exp ctxt e),l)) /\
(comp ctxt (Arith arith) l =
(case arith of
LLongMul r1 r2 r3 r4 =>
(Inst(Arith(LongMul (find_var ctxt r1) (find_var ctxt r2)
(find_var ctxt r3) (find_var ctxt r4))),l)
| LLongDiv r1 r2 r3 r4 r5 =>
(Inst(Arith(LongDiv (find_var ctxt r1) (find_var ctxt r2)
(find_var ctxt r3) (find_var ctxt r4) (find_var ctxt r5))),l)
| LDiv r1 r2 r3 =>
(Inst(Arith(Div (find_var ctxt r1) (find_var ctxt r2) (find_var ctxt r3))),l))) /\
(comp ctxt (Store e v) l =
(Store (comp_exp ctxt e) (find_var ctxt v), l)) /\
(comp ctxt (SetGlobal a e) l =
(Set (Temp a) (comp_exp ctxt e), l)) /\
(comp ctxt (LoadByte a v) l =
(Inst (Mem Load8 (find_var ctxt v)
(Addr (find_var ctxt a) 0w)), l)) /\
(comp ctxt (StoreByte a v) l =
(Inst (Mem Store8 (find_var ctxt v)
(Addr (find_var ctxt a) 0w)), l)) /\
(comp ctxt (Seq p q) l =
let (wp,l) = comp ctxt p l in
let (wq,l) = comp ctxt q l in
(Seq wp wq,l)) /\
(comp ctxt (If c n ri p q l1) l =
let (wp,l) = comp ctxt p l in
let (wq,l) = comp ctxt q l in
(Seq (If c (find_var ctxt n) (find_reg_imm ctxt ri) wp wq) Tick,l)) /\
(comp ctxt (Loop l1 body l2) l = (Skip,l)) /\ (* not present in input *)
(comp ctxt Break l = (Skip,l)) /\ (* not present in input *)
(comp ctxt Continue l = (Skip,l)) /\ (* not present in input *)
(comp ctxt (Raise v) l = (Raise (find_var ctxt v),l)) /\
(comp ctxt (Return v) l = (Return 0 (find_var ctxt v),l)) /\
(comp ctxt Tick l = (Tick,l)) /\
(comp ctxt (Mark p) l = comp ctxt p l) /\
(comp ctxt Fail l = (Skip,l)) /\
(comp ctxt (LocValue n m) l = (LocValue (find_var ctxt n) m,l)) /\
(comp ctxt (Call ret dest args handler) l =
let args = MAP (find_var ctxt) args in
case ret of
| NONE (* tail-call *) => (wordLang$Call NONE dest (0::args) NONE,l)
| SOME (v,live) =>
let v = find_var ctxt v in
let live = mk_new_cutset ctxt live in
let new_l = (FST l, SND l+1) in
case handler of
| NONE => (wordLang$Call (SOME (v,live,Skip,l)) dest args NONE, new_l)
| SOME (n,p1,p2,_) =>
let (p1,l1) = comp ctxt p1 new_l in
let (p2,l1) = comp ctxt p2 l1 in
let new_l = (FST l1, SND l1+1) in
(Seq (Call (SOME (v,live,p2,l)) dest args
(SOME (find_var ctxt n,p1,l1))) Tick, new_l)) /\
(comp ctxt (FFI f ptr1 len1 ptr2 len2 live) l =
let live = mk_new_cutset ctxt live in
(FFI f (find_var ctxt ptr1) (find_var ctxt len1)
(find_var ctxt ptr2) (find_var ctxt len2) live,l)) ∧
(comp ctxt (ShMem memop n e) l =
(ShareInst memop (find_var ctxt n) (comp_exp ctxt e),l))
End
Definition make_ctxt_def:
make_ctxt n [] l = l ∧
make_ctxt n (x::xs) l = make_ctxt (n+2:num) xs (insert x n l)
End
(*
acc_vars body LN: accumulates the assigned variable with the given num_set
The main function below is make_ctxt, we do the difference so that we do not
replicate the parameters (variable names) that we are providing with the
exsiting assigned variables present in the body of the program already
*)
Definition comp_func_def:
comp_func name params body =
let vs = fromNumSet (difference (acc_vars body LN) (toNumSet params)) in
let ctxt = make_ctxt 2 (params ++ vs) LN in
FST (comp ctxt body (name,2))
End
Definition compile_prog_def:
compile_prog p = MAP (λ(name, params, body).
(name, LENGTH params+1, comp_func name params body)) p
End
Definition compile_def:
compile p =
let p = loop_remove$comp_prog p in
compile_prog p
End
val _ = export_theory();