-
Notifications
You must be signed in to change notification settings - Fork 85
/
pan_to_targetScript.sml
74 lines (67 loc) · 3.21 KB
/
pan_to_targetScript.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
(*
Compiler from Pancake to machine code
*)
open preamble
pan_to_wordTheory backendTheory
word_depthTheory word_to_wordTheory;
val _ = new_theory "pan_to_target";
Definition compile_prog_def:
compile_prog c prog =
(* Ensure either user-written main or new main that does nothing is first in func list *)
let prog0 = case SPLITP (\(n,e,p,b). n = «main») prog of
([],ys) => ys
| (xs,[]) => («main»,F,[],Return (Const 0w))::xs
| (xs,y::ys) => y::xs ++ ys in
(* Prevent exported main functions *)
case prog0 of
((_,T,_,_)::xs) => NONE
| _ =>
(* Remove exported information from func list for compiler passes *)
let prog1 = MAP (\(n,e,p,b). (n,p,b)) prog0 in
(* Compiler passes *)
let prog2 = pan_to_word$compile_prog c.lab_conf.asm_conf.ISA prog1 in
let (col,prog3) = word_to_word$compile c.word_to_word_conf c.lab_conf.asm_conf prog2 in
let c = c with
word_to_word_conf updated_by (λc. c with col_oracle := col) in
(* Add user functions to name mapping *)
let names = fromAList (ZIP (QSORT $< (MAP FST prog2), (* func numbers *)
MAP FST prog1 (* func names *)
)) : mlstring$mlstring num_map in
(* Add stubs to name mapping *)
let names = sptree$union (sptree$fromAList $ (word_to_stack$stub_names () ++
stack_alloc$stub_names () ++ stack_remove$stub_names ())) names in
(* Add exported functions to *)
let c = c with exported := MAP FST (FILTER (FST o SND) prog) in
from_word c names prog3
End
(* TODO: evaluate max_depth ... (full_call_graph dest (fromAList prog)) *)
Theorem compile_prog_eq:
compile_prog c prog =
(* Ensure either user-written main or new main that does nothing is first in func list *)
let prog0 = case SPLITP (\(n,e,p,b). n = «main») prog of
([],ys) => ys
| (xs,[]) => («main»,F,[],Return (Const 0w))::xs
| (xs,y::ys) => y::xs ++ ys in
(* Prevent exported main functions *)
if ~NULL prog0 ∧ FST (SND (HD prog0)) then NONE else
(* Remove exported information from func list for compiler passes *)
let prog1 = MAP (\(n,e,p,b). (n,p,b)) prog0 in
(* Compiler passes *)
let prog2 = pan_to_word$compile_prog c.lab_conf.asm_conf.ISA prog1 in
(* Add user functions to name mapping *)
let names = fromAList (ZIP (QSORT $< (MAP FST prog2), (* func numbers *)
MAP FST prog1 (* func names *)
)) : mlstring$mlstring num_map in
(* Add stubs to name mapping *)
let names = sptree$union (sptree$fromAList $ (word_to_stack$stub_names () ++
stack_alloc$stub_names () ++ stack_remove$stub_names ())) names in
let c = c with exported := MAP FST (FILTER (FST o SND) prog) in
from_word_0 c names prog2
Proof
rewrite_tac [compile_prog_def,LET_THM]
\\ AP_THM_TAC \\ gvs [FUN_EQ_THM] \\ rw []
>- (Cases_on ‘prog0’ \\ gvs [] \\ PairCases_on ‘h’ \\ gvs [])
\\ Cases_on ‘prog0’ \\ gvs [from_word_0_def]
\\ PairCases_on ‘h’ \\ gvs []
QED
val _ = export_theory();