1structure x64_codegen_inputLib :> x64_codegen_inputLib = 2struct 3 4open HolKernel boolLib bossLib Parse; 5open helperLib wordsTheory; 6 7 8(* core code generator input syntax *) 9 10datatype access_type = 11 ACCESS_WORD 12 | ACCESS_BYTE; 13 14datatype assign_address_type = 15 ASSIGN_ADDRESS_REG of int 16 | ASSIGN_ADDRESS_OFFSET_ADD of int * Arbnum.num 17 | ASSIGN_ADDRESS_OFFSET_SUB of int * Arbnum.num; 18 19datatype assign_monop_type = 20 ASSIGN_MONOP_NOT 21 | ASSIGN_MONOP_NEG; 22 23datatype assign_binop_type = 24 ASSIGN_BINOP_ADD 25 | ASSIGN_BINOP_SUB 26 | ASSIGN_BINOP_MUL 27 | ASSIGN_BINOP_MOD 28 | ASSIGN_BINOP_DIV 29 | ASSIGN_BINOP_AND 30 | ASSIGN_BINOP_XOR 31 | ASSIGN_BINOP_OR; 32 33datatype assign_x_type = 34 ASSIGN_X_REG of int (* register number *) 35 | ASSIGN_X_CONST of Arbnum.num (* constant *); 36 37datatype assign_exp_type = 38 ASSIGN_EXP_REG of int 39 | ASSIGN_EXP_CONST of Arbnum.num (* constant *) 40 | ASSIGN_EXP_STACK of int (* stack[offset] *) 41 | ASSIGN_EXP_BINOP of assign_x_type * assign_binop_type * assign_x_type 42 | ASSIGN_EXP_MONOP of assign_monop_type * assign_x_type 43 | ASSIGN_EXP_MEMORY of access_type * assign_address_type 44 | ASSIGN_EXP_SHIFT_LEFT of assign_x_type * int 45 | ASSIGN_EXP_SHIFT_RIGHT of assign_x_type * int 46 | ASSIGN_EXP_SHIFT_ARITHMETIC_RIGHT of assign_x_type * int 47 48datatype assign_type = 49 ASSIGN_EXP of int * assign_exp_type (* register := expression *) 50 | ASSIGN_STACK of int * assign_x_type (* stack[offset] := x *) 51 | ASSIGN_MEMORY of access_type * assign_address_type * assign_x_type 52 (* mem[address] := x *) 53 | ASSIGN_OTHER of term * term (* lhs := rhs *); 54 55datatype guard_compare_type = 56 GUARD_COMPARE_LESS of bool (* true: signed, false: unsigned *) 57 | GUARD_COMPARE_LESS_EQUAL of bool (* true: signed, false: unsigned *) 58 | GUARD_COMPARE_EQUAL; 59 60datatype guard_type = 61 GUARD_NOT of guard_type 62 | GUARD_COMPARE of int * guard_compare_type * assign_x_type (* reg, cmp, reg/const *) 63 | GUARD_EQUAL_BYTE of assign_address_type * Arbnum.num 64 | GUARD_TEST of int * assign_x_type 65 | GUARD_OTHER of term; 66 67 68(* term2guard, term2assign *) 69 70fun dest_var_char c tm = 71 if not ((hd o explode o fst o dest_var) tm = c) then fail() else 72 (string_to_int o implode o tl o explode o fst o dest_var) tm 73val dest_reg = dest_var_char #"r" 74val dest_stack = dest_var_char #"s" 75fun dest_n2w tm = if car tm = ``n2w:num->word64`` then numSyntax.dest_numeral (cdr tm) else fail() 76fun dest_n2w_byte tm = if car tm = ``n2w:num->word8`` then numSyntax.dest_numeral (cdr tm) else fail() 77fun dest_x tm = ASSIGN_X_REG (dest_reg tm) handle e => ASSIGN_X_CONST (dest_n2w tm) 78fun dest_address tm = ASSIGN_ADDRESS_REG (dest_reg tm) handle e => 79 (if not ((fst o dest_const o car o car) tm = "word_add") then fail() else 80 ASSIGN_ADDRESS_OFFSET_ADD ((dest_reg o cdr o car) tm, dest_n2w (cdr tm))) handle e => 81 if not ((fst o dest_const o car o car) tm = "word_sub") then fail() else 82 ASSIGN_ADDRESS_OFFSET_SUB ((dest_reg o cdr o car) tm, dest_n2w (cdr tm)) 83 84fun basic_term2guard tm = (* expects input to use "~", "<+", "<" and "=" only *) 85 if can dest_neg tm then GUARD_NOT (basic_term2guard (dest_neg tm)) else let 86 val cmps = [("word_lo", (GUARD_COMPARE_LESS false, GUARD_COMPARE_LESS_EQUAL false)), 87 ("word_lt", (GUARD_COMPARE_LESS true, GUARD_COMPARE_LESS_EQUAL true)), 88 ("=", (GUARD_COMPARE_EQUAL, GUARD_COMPARE_EQUAL))] 89 val (d1,d2) = (snd o hd o filter (fn x => fst x = (fst o dest_const o car o car) tm)) cmps 90 val x1 = (cdr o car) tm 91 val x2 = cdr tm 92 in if can (match_term ``(x && y) = 0w:word64``) tm then 93 GUARD_TEST ((dest_reg o cdr o car o cdr o car) tm, (dest_x o cdr o cdr o car) tm) 94 else if can dest_n2w x1 then 95 GUARD_NOT (GUARD_COMPARE (dest_reg x2, d2, dest_x x1)) 96 else 97 GUARD_COMPARE (dest_reg x1, d1, dest_x x2) 98 handle e => let 99 val (i,_) = match_term ``(f:word64->word8) a = n2w n`` tm handle e => 100 match_term ``n2w n = (f:word64->word8) a`` tm 101 val addr = dest_address (subst i ``a:word64``) 102 val imm = dest_n2w_byte (subst i ``(n2w n):word8``) 103 in GUARD_EQUAL_BYTE (addr,imm) end 104 handle e => 105 GUARD_OTHER tm 106 end; 107 108fun term2guard tm = let 109 fun f (GUARD_NOT (GUARD_NOT x)) = x | f x = x 110 val c = REWRITE_CONV [WORD_HIGHER,WORD_GREATER,WORD_HIGHER_EQ, 111 WORD_GREATER_EQ,GSYM WORD_NOT_LOWER,GSYM WORD_NOT_LESS] 112 val tm = ((snd o dest_eq o concl o c) tm) handle e => tm 113 in f (basic_term2guard tm) end; 114 115fun basic_term2assign t1 t2 = let 116 val binops = [("word_add",ASSIGN_BINOP_ADD), ("word_sub",ASSIGN_BINOP_SUB), 117 ("word_mul",ASSIGN_BINOP_MUL), ("word_and",ASSIGN_BINOP_AND), 118 ("word_div",ASSIGN_BINOP_DIV), ("word_mod",ASSIGN_BINOP_MOD), 119 ("word_xor",ASSIGN_BINOP_XOR), ("word_or",ASSIGN_BINOP_OR)] 120 val monops = [("word_1comp",ASSIGN_MONOP_NOT), ("word_2comp",ASSIGN_MONOP_NEG)] 121 fun dest_binop tm = 122 ((dest_x o cdr o car) tm, 123 (snd o hd o filter (fn x => fst x = (fst o dest_const o car o car) tm)) binops, 124 (dest_x o cdr) tm) 125 fun dest_monop tm = 126 ((snd o hd o filter (fn x => fst x = (fst o dest_const o car) tm)) monops, 127 (dest_x o cdr) tm) 128 fun dest_memory tm = let 129 val (i,_) = match_term ``((m:word64->word64) a)`` tm 130 val addr = dest_address (subst i ``a:word64``) 131 in (ACCESS_WORD,addr) end handle HOL_ERR _ => fail() 132 fun dest_byte_memory tm = let 133 val (i,_) = match_term ``w2w ((m:word64->word8) a)`` tm 134 val addr = dest_address (subst i ``a:word64``) 135 in (ACCESS_BYTE,addr) end handle HOL_ERR _ => fail() 136 fun dest_lsl tm = 137 if not ((fst o dest_const o car o car) tm = "word_lsl") then fail() else 138 ((dest_x o cdr o car) tm, (Arbnum.toInt o numSyntax.dest_numeral o cdr) tm) 139 fun dest_lsr tm = 140 if not ((fst o dest_const o car o car) tm = "word_lsr") then fail() else 141 ((dest_x o cdr o car) tm, (Arbnum.toInt o numSyntax.dest_numeral o cdr) tm) 142 fun dest_asr tm = 143 if not ((fst o dest_const o car o car) tm = "word_asr") then fail() else 144 ((dest_x o cdr o car) tm, (Arbnum.toInt o numSyntax.dest_numeral o cdr) tm) 145 fun dest_memory_update tm = let 146 val (i,_) = match_term ``(a =+ w) (m:word64->word64)`` tm 147 val addr = dest_address (subst i ``a:word64``) 148 val x = dest_x (subst i ``w:word64``) 149 val _ = if is_var (subst i ``m:word64->word64``) then () else fail() 150 val _ = if is_var (subst i ``w:word64``) then () else fail() 151 in (ACCESS_WORD,addr,x) end handle HOL_ERR _ => let 152 val (i,_) = match_term ``(a =+ n2w n) (m:word64->word64)`` tm 153 val addr = dest_address (subst i ``a:word64``) 154 val x = dest_n2w (subst i ``(n2w n):word64``) 155 val _ = if is_var (subst i ``m:word64->word64``) then () else fail() 156 in (ACCESS_WORD,addr,ASSIGN_X_CONST x) end 157 in ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_REG (dest_reg t2)) handle e => 158 ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_CONST (dest_n2w t2)) handle e => 159 ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_STACK (dest_stack t2)) handle e => 160 ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_BINOP (dest_binop t2)) handle e => 161 ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_MONOP (dest_monop t2)) handle e => 162 ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_MEMORY (dest_memory t2)) handle e => 163 ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_MEMORY (dest_byte_memory t2)) handle e => 164 ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_SHIFT_LEFT (dest_lsl t2)) handle e => 165 ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_SHIFT_RIGHT (dest_lsr t2)) handle e => 166 ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_SHIFT_ARITHMETIC_RIGHT (dest_asr t2)) handle e => 167 ASSIGN_STACK (dest_stack t1, dest_x t2) handle e => 168 ASSIGN_MEMORY (dest_memory_update t2) handle e => 169 ASSIGN_OTHER (t1,t2) 170 end 171 172fun term2assign t1 t2 = let 173 fun can_eval (ASSIGN_EXP (_, ASSIGN_EXP_BINOP (ASSIGN_X_CONST _,_,ASSIGN_X_CONST _))) = true 174 | can_eval (ASSIGN_EXP (_, ASSIGN_EXP_MONOP (_, ASSIGN_X_CONST _))) = true 175 | can_eval (ASSIGN_EXP (_, ASSIGN_EXP_SHIFT_LEFT (ASSIGN_X_CONST i,n))) = true 176 | can_eval (ASSIGN_EXP (_, ASSIGN_EXP_SHIFT_RIGHT (ASSIGN_X_CONST i,n))) = true 177 | can_eval (ASSIGN_EXP (_, ASSIGN_EXP_SHIFT_ARITHMETIC_RIGHT (ASSIGN_X_CONST i,n))) = true 178 | can_eval _ = false 179 val t = basic_term2assign t1 t2 180 (* fold constants *) 181 val t = if not (can_eval t) then t else basic_term2assign t1 ((cdr o concl o EVAL) t2) 182 in t end 183 184end; 185