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