forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
loopLangScript.sml
145 lines (133 loc) · 4.8 KB
/
loopLangScript.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
(*
loopLang intermediate language
*)
open preamble
asmTheory (* for importing binop and cmp *)
backend_commonTheory (* for overloading shift operation *);
val _ = new_theory "loopLang";
Type shift = ``:ast$shift``
Datatype:
exp = Const ('a word)
| Var num
| Lookup (5 word)
| Load exp
| Op binop (exp list)
| Shift shift exp num
| BaseAddr
End
Datatype:
loop_arith = LLongMul num num num num | LLongDiv num num num num num | LDiv num num num
End
Datatype:
prog = Skip
| Assign num ('a exp) (* dest, source *)
| Arith loop_arith
| Store ('a exp) num (* dest, source *)
| SetGlobal (5 word) ('a exp) (* dest, source *)
| LoadByte num num (* TODISC: have removed imm, why num num? *)
| StoreByte num num
| Seq prog prog
| If cmp num ('a reg_imm) prog prog num_set
| Loop num_set prog num_set (* names in, body, names out *)
| Break
| Continue
| Raise num
| Return num
| ShMem memop num ('a exp)
| Tick
| Mark prog
| Fail
| LocValue num num (* assign v1 := Loc v2 0 *)
| Call ((num # num_set) option) (* return var *)
(num option) (* target of call *)
(num list) (* arguments *)
((num # prog # prog # num_set) option) (* var to store exception,
exception-handler code,
normal-return handler code,
live vars after call *)
| FFI string num num num num num_set
(* FFI name, conf_ptr, conf_len, array_ptr, array_len, cut-set *)
End
Theorem MEM_IMP_exp_size:
!xs a. MEM a xs ==> (exp_size l a < exp1_size l xs)
Proof
Induct \\ FULL_SIMP_TAC (srw_ss()) []
\\ REPEAT STRIP_TAC \\ SRW_TAC [] [definition"exp_size_def"]
\\ RES_TAC \\ DECIDE_TAC
QED
Definition nested_seq_def:
(nested_seq [] = Skip) /\
(nested_seq (e::es) = Seq e (nested_seq es))
End
Definition locals_touched_def:
(locals_touched (Const w) = []) /\
(locals_touched (Var v) = [v]) /\
(locals_touched (Lookup name) = []) /\
(locals_touched (Load addr) = locals_touched addr) /\
(locals_touched (Op op wexps) = FLAT (MAP locals_touched wexps)) /\
(locals_touched (Shift sh wexp n) = locals_touched wexp) ∧
(locals_touched BaseAddr = [])
Termination
wf_rel_tac `measure (\e. exp_size ARB e)` >>
rpt strip_tac >>
imp_res_tac MEM_IMP_exp_size >>
TRY (first_x_assum (assume_tac o Q.SPEC `ARB`)) >>
decide_tac
End
Definition assigned_vars_def:
(assigned_vars Skip = []) ∧
(assigned_vars (Assign n e) = [n]) ∧
(assigned_vars (Arith arith) =
case arith of
LLongMul v1 v2 v3 v4 => [v1;v2]
| LLongDiv v1 v2 v3 v4 v5 => [v1;v2]
| LDiv v1 v2 v3 => [v1]) ∧
(assigned_vars (LoadByte n m) = [m]) ∧
(assigned_vars (Seq p q) = assigned_vars p ++ assigned_vars q) ∧
(assigned_vars (If cmp n r p q ns) = assigned_vars p ++ assigned_vars q) ∧
(assigned_vars (LocValue n m) = [n]) ∧
(assigned_vars (ShMem op n e) = [n]) ∧
(assigned_vars (Mark p) = assigned_vars p) ∧
(assigned_vars (Loop _ p _) = assigned_vars p) ∧
(assigned_vars (Call NONE _ _ _) = []) ∧
(assigned_vars (Call (SOME (n,_)) _ _ NONE) = [n]) ∧
(assigned_vars (Call (SOME (n,_)) _ _ (SOME (m,p,q, _))) =
n::m::assigned_vars p ++ assigned_vars q) ∧
(assigned_vars _ = [])
End
Definition acc_vars_def:
(acc_vars (Seq p1 p2) l = acc_vars p1 (acc_vars p2 l)) ∧
(acc_vars Break l = (l:num_set)) ∧
(acc_vars Continue l = l) ∧
(acc_vars (Loop l1 body l2) l = acc_vars body l) ∧
(acc_vars (If x1 x2 x3 p1 p2 l1) l = acc_vars p1 (acc_vars p2 l)) ∧
(acc_vars (Arith arith) l =
case arith of
LLongMul v1 v2 v3 v4 => insert v1 () $ insert v2 () l
| LLongDiv v1 v2 v3 v4 v5 => insert v1 () $ insert v2 () l
| LDiv v1 v2 v3 => insert v1 () l) ∧
(acc_vars (Mark p1) l = acc_vars p1 l) /\
(acc_vars Tick l = l) /\
(acc_vars Skip l = l) /\
(acc_vars Fail l = l) /\
(acc_vars (Raise v) l = l) /\
(acc_vars (Return v) l = l) /\
(acc_vars (Call ret dest args handler) l =
case ret of
| NONE => l
| SOME (v,live) =>
let l = insert v () l in
case handler of
| NONE => l
| SOME (n,p1,p2,l1) =>
acc_vars p1 (acc_vars p2 (insert n () l))) /\
(acc_vars (LocValue n m) l = insert n () l) /\
(acc_vars (Assign n exp) l = insert n () l) /\
(acc_vars (ShMem op n exp) l = insert n () l) /\
(acc_vars (Store exp n) l = l) /\
(acc_vars (SetGlobal w exp) l = l) /\
(acc_vars (LoadByte n m) l = insert m () l) /\
(acc_vars (StoreByte n m) l = l) /\
(acc_vars (FFI name n1 n2 n3 n4 live) l = l)
End
val _ = export_theory();