1structure ppc_Lib :> ppc_Lib = 2struct 3 4open HolKernel boolLib bossLib; 5open wordsLib stringLib listSyntax simpLib listTheory wordsTheory; 6open opmonTheory bit_listTheory combinTheory; 7 8open ppc_Theory ppc_seq_monadTheory ppc_opsemTheory ppc_astTheory ppc_coretypesTheory; 9 10 11(* decoder *) 12 13fun ppc_decode s = let 14 val tm = Parse.Term [QUOTE ("w2bits (0x"^s^"w:word32)")] 15 val bits = (snd o dest_eq o concl o EVAL) tm 16 val th = EVAL (mk_comb(``ppc_decode``,bits)) 17 in th end; 18 19fun ppc_decode_next s = let 20 fun fill s = if length (explode s) < 8 then fill ("0" ^ s) else s 21 val s = fill s 22 val th = ppc_decode s 23 val th = MATCH_MP PPC_NEXT_THM th 24 val th = Q.SPEC [QUOTE ("(0x"^(substring(s,0,2))^"w:word8)")] th 25 val th = Q.SPEC [QUOTE ("(0x"^(substring(s,2,2))^"w:word8)")] th 26 val th = Q.SPEC [QUOTE ("(0x"^(substring(s,4,2))^"w:word8)")] th 27 val th = Q.SPEC [QUOTE ("(0x"^(substring(s,6,2))^"w:word8)")] th 28 val th = CONV_RULE (RATOR_CONV EVAL THENC BETA_CONV) th 29 in th end; 30 31 32(* one step symbolic simulation *) 33 34val else_none_mem_lemma = (UNDISCH o SPEC_ALL) ppc_else_none_mem_lemma 35val else_none_status_lemma = (UNDISCH o SPEC_ALL) ppc_else_none_status_lemma 36val assertT_lemma = (UNDISCH o SPEC_ALL) ppc_assertT_lemma 37val else_none_conv1 = (fst o dest_eq o concl) else_none_mem_lemma 38val else_none_conv2 = (fst o dest_eq o concl) else_none_status_lemma 39val else_none_conv3 = (fst o dest_eq o concl) assertT_lemma 40fun else_none_conv tm = let 41 val ((i,t),th) = (match_term else_none_conv1 tm, else_none_mem_lemma) handle HOL_ERR _ => 42 (match_term else_none_conv2 tm, else_none_status_lemma) handle HOL_ERR _ => 43 (match_term else_none_conv3 tm, assertT_lemma) 44 in INST i (INST_TYPE t th) end; 45 46val w2bytes1 = SIMP_CONV std_ss [Ntimes word2bytes_def 7,ASR_ADD] ``word2bytes 1 (w:word32)`` 47val w2bytes2 = SIMP_CONV std_ss [Ntimes word2bytes_def 7,ASR_ADD] ``word2bytes 2 (w:word32)`` 48val w2bytes4 = SIMP_CONV std_ss [Ntimes word2bytes_def 7,ASR_ADD] ``word2bytes 4 (w:word32)`` 49 50val lemma1 = REWRITE_RULE [WORD_ADD_0] (Q.SPECL [`v`,`0w`,`x`] WORD_EQ_ADD_LCANCEL) 51val lemma2 = REWRITE_RULE [WORD_ADD_0] (Q.SPECL [`v`,`x`,`0w`] WORD_EQ_ADD_LCANCEL) 52val address_lemma = prove( 53 ``~(0w = 1w:word32) /\ ~(0w = 2w:word32) /\ ~(0w = 3w:word32) /\ 54 ~(1w = 2w:word32) /\ ~(1w = 3w:word32) /\ ~(2w = 3w:word32)``,EVAL_TAC); 55 56val w_conv = SIMP_CONV std_ss [ppc_write_mem_aux_def,GSYM WORD_ADD_ASSOC, word_add_n2w] 57val ppc_write_mem_aux_lemma1 = w_conv ``ppc_write_mem_aux ii addr [x0]`` 58val ppc_write_mem_aux_lemma2 = w_conv ``ppc_write_mem_aux ii addr [x0;x1]`` 59val ppc_write_mem_aux_lemma3 = w_conv ``ppc_write_mem_aux ii addr [x0;x1;x2;x3]`` 60 61val if_SOME = prove( 62 ``(if b then SOME((),x:ppc_state) else SOME((),y)) = SOME ((),if b then x else y)``, 63 Cases_on `b` THEN SIMP_TAC std_ss []); 64 65val ss = rewrites [OK_nextinstr_def, PWRITE_M_LIST_def, 66 bit_update_def, const_high_def, const_low_def, const_high_s_def, 67 const_low_s_def, effective_address_def, goto_label_def, 68 gpr_or_zero_def, load_word_def, no_carry_def, ppc_sint_cmp_def, 69 ppc_uint_cmp_def, read_bit_word_def, read_ireg_def, 70 read_mem_aux_def, reg_load_def, reg_store_def, reg_update_def, 71 sint_compare_def, sint_reg_update_def, uint_compare_def, 72 uint_reg_update_def, seq_monad_thm, write_reg_def, read_reg_def, 73 ppc_write_mem_aux_lemma1, ppc_write_mem_aux_lemma2, 74 ppc_write_mem_aux_lemma3, write_mem_def, read_mem_def, 75 read_status_def, write_status_def, write_reg_seq_def, 76 read_reg_seq_def, write_status_seq_def, constT_def, seqT_def, 77 parT_def, parT_unit_def, failureT_def, PREAD_CLAUSES, 78 ppc_clear_CR0_def, ppc_reg_distinct, ppc_bit_distinct, w2w_def, 79 w2n_n2w, WORD_ADD_0, n2w_w2n, w2bytes1, w2bytes2, w2bytes4, n2w_11, 80 address_aligned_def, rich_listTheory.REVERSE, 81 WORD_EQ_ADD_LCANCEL,ppc_branch_condition_def, 82 rich_listTheory.SNOC_APPEND, APPEND, lemma1, lemma2, address_lemma] 83 84fun EVAL_sw2sw th = let 85 val tm = find_term (can (match_term ``(sw2sw:'a word -> 'b word) (n2w n)``)) (concl th) 86 in EVAL_sw2sw (REWRITE_RULE [EVAL tm] th) end handle e => th; 87 88fun EVAL_word_and_eq th = let 89 val tm = find_term (can (match_term ``(n2w n) && (n2w m) = (n2w k):'a word``)) (concl th) 90 in EVAL_word_and_eq (REWRITE_RULE [EVAL tm] th) end handle e => th; 91 92fun ppc_step s = let 93 val th = ppc_decode_next s 94 val tm = (fst o dest_eq o fst o dest_imp o concl) th 95 val th1 = SIMP_CONV (std_ss++ss++wordsLib.SIZES_ss) [ppc_exec_instr_def] tm 96 fun cc th = CONV_RULE (ONCE_DEPTH_CONV else_none_conv) th 97 fun f th = (DISCH_ALL o CONV_RULE (RAND_CONV (SIMP_CONV std_ss [pull_if_lemma])) o 98 UNDISCH_ALL o SIMP_RULE (std_ss++ss) [LET_DEF] o 99 DISCH_ALL o cc) th 100 fun change f x = let val y = f x in if concl y = concl x then x else change f y end 101 val th1 = change f th1 102 val th1 = EVAL_word_and_eq th1 103 val th1 = DISCH_ALL (MATCH_MP th (UNDISCH_ALL (REWRITE_RULE [if_SOME] th1))) 104 val th1 = (REWRITE_RULE [pull_if_lemma] o UNDISCH_ALL) th1 105 val th1 = REWRITE_RULE [AND_IMP_INTRO,GSYM CONJ_ASSOC,conditional_def] (DISCH_ALL th1) 106 val th1 = EVAL_sw2sw th1 107 in th1 end; 108 109 110(* 111 test cases: 112 113 val th = ppc_step "7C640194"; (* addze 3,4 *) 114 val th = ppc_step "7C221A14"; (* add 1,2,3 *) 115 val th = ppc_step "7E6802A6"; (* mflr 19 *) 116 val th = ppc_step "7C4903A6"; (* mtctr 2 *) 117 val th = ppc_step "7C4803A6"; (* mtlr 2 *) 118 val th = ppc_step "7C032040"; (* cmplw 3,4 *) 119 val th = ppc_step "28070320"; (* cmplwi 7,800 *) 120 val th = ppc_step "7C119000"; (* cmpw 17,18 *) 121 val th = ppc_step "2C070258"; (* cmpwi 7,600 *) 122 val th = ppc_step "7E7A21D6"; (* mullw 19, 26, 4 *) 123 val th = ppc_step "7E7A2010"; (* subfc 19, 26, 4 *) 124 val th = ppc_step "38221388"; (* addi 1,2,5000 *) 125 val th = ppc_step "3C22FFCE"; (* addis 1,2,-50 *) 126 val th = ppc_step "7C812839"; (* and. 1,4,5 *) 127 val th = ppc_step "7C812878"; (* andc 1,4,5 *) 128 val th = ppc_step "70E60050"; (* andi. 6,7,80 *) 129 val th = ppc_step "76300007"; (* andis. 16,17,7 *) 130 val th = ppc_step "4C221B82"; (* cror 1,2,3 *) 131 val th = ppc_step "7C411A38"; (* eqv 1,2,3 *) 132 val th = ppc_step "7E300774"; (* extsb 16,17 *) 133 val th = ppc_step "7CA40734"; (* extsh 4,5 *) 134 val th = ppc_step "8A7A00EA"; (* lbz 19, 234(26) *) 135 val th = ppc_step "7E7A20AE"; (* lbzx 19, 26, 4 *) 136 val th = ppc_step "7E7A22AE"; (* lhax 19, 26, 4 *) 137 val th = ppc_step "7E7A222E"; (* lhzx 19, 26, 4 *) 138 val th = ppc_step "827A00EA"; (* lwz 19, 234(26) *) 139 val th = ppc_step "7E7A202E"; (* lwzx 19, 26, 4 *) 140 val th = ppc_step "7C5A1378"; (* mr 26, 2 *) 141 val th = ppc_step "1E7AFFFE"; (* mulli 19, 26, -2 *) 142 val th = ppc_step "7C5A23B8"; (* nand 26, 2, 4 *) 143 val th = ppc_step "7C5A20F8"; (* nor 26, 2, 4 *) 144 val th = ppc_step "7C5A2378"; (* or 26, 2, 4 *) 145 val th = ppc_step "7C5A2338"; (* orc 26, 2, 4 *) 146 val th = ppc_step "605A0237"; (* ori 26, 2, 567 *) 147 val th = ppc_step "645A0237"; (* oris 26, 2, 567 *) 148 val th = ppc_step "7C5A2030"; (* slw 26, 2, 4 *) 149 val th = ppc_step "7C5A2630"; (* sraw 26, 2, 4 *) 150 val th = ppc_step "7C5A1E70"; (* srawi 26, 2, 3 *) 151 val th = ppc_step "7C5A2430"; (* srw 26, 2, 4 *) 152 val th = ppc_step "7C5A2278"; (* xor 26, 2, 4 *) 153 val th = ppc_step "685A0237"; (* xori 26, 2, 567 *) 154 val th = ppc_step "6C5A0237"; (* xoris 26, 2, 567 *) 155 val th = ppc_step "227AFFFE"; (* subfic 19, 26, -2 *) 156 val th = ppc_step "985A00EA"; (* stb 2, 234(26) *) 157 val th = ppc_step "7C44D1AE"; (* stbx 2, 4, 26 *) 158 val th = ppc_step "7C5A232E"; (* sthx 2, 26, 4 *) 159 val th = ppc_step "905A00EA"; (* stw 2, 234(26) *) 160 val th = ppc_step "7C5A212E"; (* stwx 2, 26, 4 *) 161 val th = ppc_step "4BFFFFFC"; (* b L1 *) 162 val th = ppc_step "4180FFF8"; (* bc 12,0,L1 *) 163 val th = ppc_step "4181FFF4"; (* bc 12,1,L1 *) 164 val th = ppc_step "4082FFF0"; (* bc 4,2,L1 *) 165 val th = ppc_step "4083FFEC"; (* bc 4,3,L1 *) 166 val th = ppc_step "7C858396"; (* divwu 4,5,16 *) 167 168 (* these are not modelled *) 169 170 val th = ppc_step "545A188A"; (* rlwinm 26, 2, 3, 2, 5 *) 171 val th = ppc_step "7C221BD6"; (* divw 1,2,3 *) 172 173*) 174 175val _ = output_words_as_hex(); 176 177fun ppc_test_aux inst input output = let 178 val rw = ppc_step inst 179 fun format state (i,j) = 180 if mem i ["PC","CTR","LR"] 181 then ("PREAD_R PPC_"^i^" "^state^" = 0x"^j^"w") 182 else if substring(i,0,3) = "GPR" 183 then ("PREAD_R (PPC_IR "^substring(i,3,size(i)-3)^"w) "^state^" = 0x"^j^"w") 184 else if i = "CARRY" 185 then ("PREAD_S PPC_CARRY "^state^" = SOME "^j) 186 else if substring(i,0,3) = "CR0" 187 then ("PREAD_S (PPC_CR0 "^substring(i,3,size(i)-3)^"w) "^state^" = SOME "^j) 188 else ("PREAD_M 0x"^i^"w "^state^" = SOME (0x"^j^"w)") 189 fun p y = Parse.Term [QUOTE y] 190 fun f s = map (p o format s) 191 val th = foldr (fn (x,y) => DISCH x y) rw (f "s" input) 192 val th = SIMP_RULE std_ss [ppc_reg_distinct,ppc_reg_11,ppc_bit_distinct,ppc_bit_11] th 193 val th = SIMP_RULE std_ss [word_add_n2w,WORD_ADD_0,b2w_def,bits2num_def,GSYM AND_IMP_INTRO] th 194 val th = SIMP_RULE (std_ss++SIZES_ss) [w2n_n2w,word_mul_n2w,word_add_n2w,word_sub_def,word_2comp_n2w] th 195 val th = SIMP_RULE (std_ss++ss++SIZES_ss) [n2w_11] th 196 fun find_and_delete_cond th = let 197 val tm = find_term (can (match_term ``n2w n && (n2w m):word32 = n2w k``)) (concl th) 198 in REWRITE_RULE [prove(tm,EVAL_TAC)] th end 199 val th = repeat find_and_delete_cond th 200 val th = REWRITE_RULE [AND_IMP_INTRO] th 201 val th = REWRITE_RULE [GSYM CONJ_ASSOC] th 202 val xs = find_terms (can (match_term ``PWRITE_S x NONE``)) (concl th) 203 val xs = map (snd o dest_comb o fst o dest_comb) xs 204 val output1 = f "(THE (PPC_NEXT s))" output 205 val output2 = Lib.zip (map (snd o dest_comb o fst o dest_comb o fst o dest_eq) output1) output1 206 val output3 = filter (fn (x,y) => not (mem x xs)) output2 207 val tm = list_mk_conj (map snd output3) 208 val tm2 = (hd o hyp o UNDISCH) th 209 val goal = mk_imp(tm2,tm) 210(* 211 set_goal([],goal) 212*) 213 val result = prove(goal, 214 STRIP_TAC 215 THEN (ASSUME_TAC o UNDISCH_ALL o REWRITE_RULE [GSYM AND_IMP_INTRO]) th 216 THEN ASM_SIMP_TAC std_ss [PREAD_CLAUSES,optionTheory.THE_DEF,ppc_reg_distinct,ppc_reg_11,ppc_bit_distinct,ppc_bit_11] 217 THEN EVAL_TAC) 218 val result = REWRITE_RULE [GSYM AND_IMP_INTRO] result 219 in result end; 220 221fun ppc_test inst input output = let 222 fun p s = if length (explode s) < 6 then s else "["^s^"]" 223 val _ = print ("\nTesting:\n instruction = "^inst^"\n") 224 val _ = print ("Input:\n") 225 val _ = map (fn (x,y) => print (" "^(p x)^" = "^y^"\n")) input 226 val _ = print ("Output:\n") 227 val _ = map (fn (x,y) => print (" "^(p x)^" = "^y^"\n")) output 228 val _ = print ("Result:\n") 229 val th = SOME (ppc_test_aux inst input output) handle e => NONE 230 in case th of 231 NONE => (print " Test failed.\n"; TRUTH) 232 | SOME th => (print " Test successful.\n\n"; print_thm th; print "\n\n"; th) 233 end; 234 235 236end 237