1structure x64_compilerLib :> x64_compilerLib =
2struct
3
4open HolKernel boolLib bossLib Parse;
5open decompilerLib;
6open x64_codegenLib;
7open x64_codegen_x64Lib;
8
9open prog_x64Lib;
10open prog_x64_extraTheory;
11open wordsTheory wordsLib addressTheory;
12open helperLib;
13open tailrecLib;
14
15
16fun AUTO_ALPHA_CONV () = let
17  val counter = ref (Arbnum.zero)
18  fun inc () = let val v = !counter in (counter := Arbnum.+(v,Arbnum.one); v) end
19  fun counter_genvar ty = mk_var("auto_"^ Arbnum.toString (inc()),ty)
20  fun doit tm =
21    if is_abs tm then
22      (ALPHA_CONV (counter_genvar (type_of (fst (dest_abs tm)))) THENC
23       ABS_CONV doit) tm
24    else if is_comb tm then
25      (RATOR_CONV doit THENC RAND_CONV doit) tm
26    else ALL_CONV tm
27  in doit end
28
29val COMPILER_TAC_LEMMA = prove(
30  ``!a b:bool. (a /\ a /\ b <=> a /\ b) /\ (a \/ a \/ b <=> a \/ b)``,
31  REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC std_ss []);
32
33val COMPILER_TAC =
34    SIMP_TAC bool_ss [LET_DEF,word_div_def,word_mod_def,w2w_CLAUSES]
35    THEN SIMP_TAC std_ss [WORD_OR_CLAUSES,GUARD_def]
36    THEN REWRITE_TAC [WORD_CMP_NORMALISE]
37    THEN REWRITE_TAC [WORD_HIGHER,WORD_GREATER,WORD_HIGHER_EQ,
38           WORD_GREATER_EQ,GSYM WORD_NOT_LOWER,GSYM WORD_NOT_LESS]
39    THEN SIMP_TAC std_ss [WORD_MUL_LSL,word_mul_n2w,word_add_n2w,NOT_IF,
40           WORD_OR_CLAUSES]
41    THEN CONV_TAC (EVAL_ANY_MATCH_CONV word_patterns)
42    THEN SIMP_TAC std_ss [WORD_SUB_RZERO, WORD_ADD_0, IF_IF,
43                          AC WORD_ADD_COMM WORD_ADD_ASSOC,
44                          AC WORD_MULT_COMM WORD_MULT_ASSOC,
45                          AC WORD_AND_COMM WORD_AND_ASSOC,
46                          AC WORD_OR_COMM WORD_OR_ASSOC,
47                          AC WORD_XOR_COMM WORD_XOR_ASSOC,
48                          AC CONJ_COMM CONJ_ASSOC,
49                          AC DISJ_COMM DISJ_ASSOC,
50                          IMP_DISJ_THM, WORD_MULT_CLAUSES]
51    THEN REPEAT STRIP_TAC
52    THEN CONV_TAC (RAND_CONV (AUTO_ALPHA_CONV ()))
53    THEN CONV_TAC ((RATOR_CONV o RAND_CONV) (AUTO_ALPHA_CONV ()))
54    THEN SIMP_TAC std_ss [AC CONJ_ASSOC CONJ_COMM, AC DISJ_COMM DISJ_ASSOC,
55                          COMPILER_TAC_LEMMA]
56    THEN SIMP_TAC std_ss [WORD_SUB_RZERO, WORD_ADD_0, IF_IF,
57                          AC WORD_ADD_COMM WORD_ADD_ASSOC,
58                          AC WORD_MULT_COMM WORD_MULT_ASSOC,
59                          AC WORD_AND_COMM WORD_AND_ASSOC,
60                          AC WORD_OR_COMM WORD_OR_ASSOC,
61                          AC WORD_XOR_COMM WORD_XOR_ASSOC,
62                          AC CONJ_COMM CONJ_ASSOC,
63                          AC DISJ_COMM DISJ_ASSOC,
64                          IMP_DISJ_THM, WORD_MULT_CLAUSES]
65    THEN EQ_TAC
66    THEN ONCE_REWRITE_TAC [GSYM DUMMY_EQ_def]
67    THEN REWRITE_TAC [FLATTEN_IF]
68    THEN REPEAT STRIP_TAC
69    THEN ASM_SIMP_TAC std_ss [];
70
71fun x64_basic_compile tm = let
72  val target = "x64"
73  val (tools,target,model_name,s) = (x64_tools_64,"x64","X64_MODEL",[])
74  val x = fst (dest_eq tm)
75  val name = fst (dest_const (repeat car x)) handle e => fst (dest_var (repeat car x))
76  val _ = echo 1 ("\nCompiling " ^ name ^ " into "^ target ^ "...\n")
77  val (code,len) = generate_code model_name true tm
78  fun append' [] = "" | append' (x::xs) = x ^ "\n" ^ append' xs
79  val qcode = [QUOTE (append' code)] : term quotation
80  val in_tm = cdr x
81  fun ends (FUN_IF (_,c1,c2)) = ends c1 @ ends c2
82    | ends (FUN_LET (_,_,c)) = ends c
83    | ends (FUN_COND (_,c)) = ends c
84    | ends (FUN_VAL t) = if is_var t orelse pairSyntax.is_pair t then [t] else []
85  val out_tm2 = hd (ends (tm2ftree (cdr tm)))
86  val (in_tm,out_tm) = (subst s in_tm, subst s out_tm2)
87  val function_in_out = SOME (in_tm,out_tm)
88  val qcode = ([QUOTE (append' code)]) : term Lib.frag list
89  val (th1,th2) = basic_decompile tools name function_in_out qcode
90  val _ = print "Proving equivalence, "
91  val const = (repeat car o fst o dest_eq o concl o hd o CONJUNCTS) th2
92  val tm = subst [ repeat car x |-> const ] tm
93  val pre = if is_conj (concl th2) then (last o CONJUNCTS) th2 else TRUTH
94  val pre = RW [IF_IF,WORD_TIMES2] pre
95  val th3 = auto_prove "compile" (tm,
96    REPEAT STRIP_TAC
97    THEN CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [th2]))
98    THEN COMPILER_TAC)
99    handle HOL_ERR e => let
100      val _ = (show_types := true)
101      val _ = print ("\n\nval tm = ``"^ term_to_string tm ^"``;\n\n")
102      val _ = (show_types := false)
103      in raise HOL_ERR e end;
104  val _ = add_compiler_assignment out_tm2 (fst (dest_eq tm)) name len model_name
105  val _ = print "done.\n"
106  in (th1,th3,pre) end;
107
108fun x64_compile t = let
109  val tm = Parse.Term t
110  val _ = set_abbreviate_code true
111  fun compile_each [] = []
112    | compile_each (tm::tms) = let
113    val (th,def,pre) = x64_basic_compile tm
114    in (th,def,pre) :: compile_each tms end
115  val tms = list_dest dest_conj tm
116  val xs = compile_each tms
117  val defs = map (fn (x,y,z) => y) xs
118  val pres = map (fn (x,y,z) => z) xs
119  val def = RW [] (foldr (uncurry CONJ) TRUTH defs)
120  val pre = RW [] (foldr (uncurry CONJ) TRUTH pres)
121  val (th,_,_) = last xs
122  val _ = set_abbreviate_code false
123  val th = UNABBREV_CODE_RULE th
124  in (th,def,pre) end;
125
126val _ = add_compiled (map (SIMP_RULE std_ss [LET_DEF] o Q.INST [`rip`|->`p`])
127    [x64_push_r0, x64_push_r1, x64_push_r2, x64_push_r3, x64_push_r6,
128     x64_push_r7, x64_push_r8, x64_push_r9, x64_push_r10,
129     x64_push_r11, x64_push_r12, x64_push_r13, x64_push_r14,
130     x64_push_r15, x64_pop_r0, x64_pop_r1, x64_pop_r2, x64_pop_r3,
131     x64_pop_r6, x64_pop_r7, x64_pop_r8, x64_pop_r9, x64_pop_r10,
132     x64_pop_r11, x64_pop_r12, x64_pop_r13, x64_pop_r14, x64_pop_r15]);
133
134end;
135