1
2open HolKernel boolLib bossLib Parse;
3
4open codegen_x86Lib;
5
6open compilerLib codegen_x86Lib;
7
8val _ = new_theory "compiler_demo";
9
10(* basic loop: mod 10 *)
11
12val (th1,th2,th3) = compile_all ``
13  mod10 (r1:word32) =
14    if r1 <+ 10w then r1 else let r1 = r1 - 10w in mod10 r1``;
15
16(* comparisions *)
17
18val (th1,th2,th3) = compile "ppc" ``
19  test_cmp (r1:word32,r2:word32) =
20    if r1 < r2 then let r2 = 5w:word32 in (r1,r2) else (r1,r2)``;
21
22(* large constants *)
23
24val (th1,th2,th3) = compile_all ``
25  large_constants (r1:word32,r2:word32) =
26    if r1 = 0w then let r2 = 5w:word32 in (r1,r2) else
27      let r1 = r1 + r2 in
28      let r2 = 60000w:word32 in
29      let r2 = 2360000w:word32 in
30        large_constants (r1,r2)``;
31
32(* memory reads *)
33
34val (th1,th2,th3) = compile_all ``
35  read_loop (r1:word32,r2:word32,dm:word32 set,m) =
36    if r1 = 0w then (r1,r2,dm,m) else
37      let r1 = m r1 in
38      let r2 = m r2 in
39        read_loop (r1,r2,dm,m)``;
40
41(* memory writes *)
42
43val (th1,th2,th3) = compile_all ``
44  copy_loop (r1:word32,r2:word32,dg:word32 set,g) =
45    if r1 = 0w then (r1,r2,dg,g) else
46      let r1 = g r1 in
47      let r2 = g r2 in
48      let g = (r2 =+ r1) g in
49        copy_loop (r1,r2,dg,g)``;
50
51(* byte accesses *)
52
53val (th1,th2,th3) = compile_all ``
54  copy_byte_loop (r3:word32,r4:word32,dg:word32 set,g:word32->word8) =
55    if r3 = 0w then (r3,r4,dg,g) else
56      let r3 = w2w (g r3) in
57      let r4 = w2w (g r4) in
58      let g = (r4 =+ w2w r3) g in
59        copy_byte_loop (r3,r4,dg,g)``;
60
61(* shared-tails *)
62
63val (th1,th2,th3) = compile_all ``
64  shared_tails (r1:word32,r2:word32) =
65    if r1 = 0w then
66      let r2 = 23w:word32 in
67      let r1 = 4w:word32 in
68        (r1,r2)
69    else
70      let r2 = 56w:word32 in
71      let r1 = 4w in
72        (r1,r2)``;
73
74(* removal of dead code *)
75
76val (th1,th2,th3) = compile_all ``
77  dead_code (r1:word32,r2:word32) =
78    let r2 = 45w:word32 in
79    if r1 <+ 3w then
80      let r2 = r1 + 67w in
81      let r2 = r1 in (r1,r2)
82    else
83      let r2 = r1 + 6w in (r1,r2)``;
84
85(* subroutines *)
86
87val (th1,th2,th3) = compile_all ``
88  call_mod10 (r1:word32,r2:word32,r3) =
89    let r1 = r1 + r2 in
90    let r1 = r1 + r3 in
91    let r1 = mod10 r1 in
92      r1``;
93
94(* addition *)
95
96val (th1,th2,th3) = compile_all ``
97  addition (r1:word32,r2:word32) =
98    let r1 = r2 + r1 in
99    let r2 = r1 + r2 in
100    let r3 = r1 + 8w in
101    let r4 = r2 + 45w in
102    let r5 = r2 + r3 in
103      (r1,r2,r3,r4,r5)``;
104
105(* string operations *)
106
107val _ = codegen_x86Lib.set_x86_regs
108  [(3,"eax"),(4,"ecx"),(5,"edx"),(6,"ebx"),(7,"edi"),(8,"esi"),(9,"ebp")]
109
110val (thms,arm_str_rev_def,arm_str_rev_pre_def) = compile_all ``
111  arm_string_rev(r3:word32,r6,r7,df:word32 set,f:word32->word8) =
112    if r3 = 0w then (r7,df,f) else
113      let r4 = (w2w (f r6)):word32 in
114      let r5 = (w2w (f r7)):word32 in
115      let f = (r6 =+ w2w r5) f in
116      let f = (r7 =+ w2w r4) f in
117      let r6 = r6 - 1w in
118      let r7 = r7 + 1w in
119      let r3 = r3 - 1w in
120        arm_string_rev(r3,r6,r7,df,f)``
121
122val _ = export_theory();
123
124