1structure codegen_inputLib :> 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->word32`` 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:word32``) 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:word32->word8) a = n2w n`` tm handle e => 100 match_term ``n2w n = (f:word32->word8) a`` tm 101 val addr = dest_address (subst i ``a:word32``) 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 = 129 if not (is_var (car tm) andalso type_of (car tm) = ``:word32->word32``) then fail() else 130 (ACCESS_WORD,dest_address (cdr tm)) 131 fun dest_byte_memory tm = 132 if not (is_const (car tm) andalso type_of (car tm) = ``:word8->word32``) then fail() else 133 (ACCESS_BYTE,dest_address (cdr (cdr tm))) 134 fun dest_lsl tm = 135 if not ((fst o dest_const o car o car) tm = "word_lsl") then fail() else 136 ((dest_x o cdr o car) tm, (Arbnum.toInt o numSyntax.dest_numeral o cdr) tm) 137 fun dest_lsr tm = 138 if not ((fst o dest_const o car o car) tm = "word_lsr") then fail() else 139 ((dest_x o cdr o car) tm, (Arbnum.toInt o numSyntax.dest_numeral o cdr) tm) 140 fun dest_asr tm = 141 if not ((fst o dest_const o car o car) tm = "word_asr") then fail() else 142 ((dest_x o cdr o car) tm, (Arbnum.toInt o numSyntax.dest_numeral o cdr) tm) 143 fun dest_memory_update tm = let 144 val (i,_) = match_term ``(a =+ w) (m:word32->word32)`` tm 145 val addr = dest_address (subst i ``a:word32``) 146 val x = dest_x (subst i ``w:word32``) 147 val _ = if is_var (subst i ``m:word32->word32``) then () else fail() 148 val _ = if is_var (subst i ``w:word32``) then () else fail() 149 in (ACCESS_WORD,addr,x) end handle HOL_ERR _ => let 150 val (i,_) = match_term ``(a =+ w2w (w:word32)) (m:word32->word8)`` tm 151 val addr = dest_address (subst i ``a:word32``) 152 val x = dest_x (subst i ``w:word32``) 153 val _ = if is_var (subst i ``m:word32->word8``) then () else fail() 154 val _ = if is_var (subst i ``w:word32``) then () else fail() 155 in (ACCESS_BYTE,addr,x) end handle HOL_ERR _ => let 156 val (i,_) = match_term ``(a =+ n2w n) (m:word32->word8)`` tm 157 val addr = dest_address (subst i ``a:word32``) 158 val x = dest_n2w_byte (subst i ``(n2w n):word8``) 159 val _ = if is_var (subst i ``m:word32->word8``) then () else fail() 160 in (ACCESS_BYTE,addr,ASSIGN_X_CONST x) end handle HOL_ERR _ => let 161 val (i,_) = match_term ``(a =+ n2w n) (m:word32->word32)`` tm 162 val addr = dest_address (subst i ``a:word32``) 163 val x = dest_n2w (subst i ``(n2w n):word32``) 164 val _ = if is_var (subst i ``m:word32->word32``) then () else fail() 165 in (ACCESS_WORD,addr,ASSIGN_X_CONST x) end 166 in ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_REG (dest_reg t2)) handle e => 167 ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_CONST (dest_n2w t2)) handle e => 168 ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_STACK (dest_stack t2)) handle e => 169 ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_BINOP (dest_binop t2)) handle e => 170 ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_MONOP (dest_monop t2)) handle e => 171 ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_MEMORY (dest_memory t2)) handle e => 172 ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_MEMORY (dest_byte_memory t2)) handle e => 173 ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_SHIFT_LEFT (dest_lsl t2)) handle e => 174 ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_SHIFT_RIGHT (dest_lsr t2)) handle e => 175 ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_SHIFT_ARITHMETIC_RIGHT (dest_asr t2)) handle e => 176 ASSIGN_STACK (dest_stack t1, dest_x t2) handle e => 177 ASSIGN_MEMORY (dest_memory_update t2) handle e => 178 ASSIGN_OTHER (t1,t2) 179 end 180 181fun term2assign t1 t2 = let 182 fun can_eval (ASSIGN_EXP (_, ASSIGN_EXP_BINOP (ASSIGN_X_CONST _,_,ASSIGN_X_CONST _))) = true 183 | can_eval (ASSIGN_EXP (_, ASSIGN_EXP_MONOP (_, ASSIGN_X_CONST _))) = true 184 | can_eval (ASSIGN_EXP (_, ASSIGN_EXP_SHIFT_LEFT (ASSIGN_X_CONST i,n))) = true 185 | can_eval (ASSIGN_EXP (_, ASSIGN_EXP_SHIFT_RIGHT (ASSIGN_X_CONST i,n))) = true 186 | can_eval (ASSIGN_EXP (_, ASSIGN_EXP_SHIFT_ARITHMETIC_RIGHT (ASSIGN_X_CONST i,n))) = true 187 | can_eval _ = false 188 val t = basic_term2assign t1 t2 189 (* fold constants *) 190 val t = if not (can_eval t) then t else basic_term2assign t1 ((cdr o concl o EVAL) t2) 191 in t end 192 193end; 194