1structure x64_Lib :> x64_Lib = 2struct 3 4open HolKernel boolLib bossLib; 5open wordsLib stringLib listSyntax simpLib listTheory wordsTheory; 6open opmonTheory bit_listTheory combinTheory ConseqConv; 7 8open x64_Theory x64_seq_monadTheory x64_opsemTheory x64_astTheory; 9open x64_coretypesTheory x64_icacheTheory; 10 11 12(* decoder *) 13 14val Zreg_distinct = x64_decoderTheory.Zreg_distinct; 15 16fun nTimes n f x = if n = 0 then x else nTimes (n-1) f (f x) 17 18fun eval_term_ss tm_name tm = conv_ss 19 { name = tm_name, trace = 3, key = SOME ([],tm), conv = K (K EVAL) }; 20 21val bytes_LEMMA = SIMP_RULE std_ss [LENGTH] (Q.SPEC `[v1;v2;v3;v4;v5;v6;v7;v8]` bits2num_LESS) 22 23val n2w_SIGN_EXTEND = prove( 24 ``!n. n < 256 ==> (n2w (SIGN_EXTEND 8 32 n):word32 = sw2sw ((n2w n):word8))``, 25 SIMP_TAC (std_ss++SIZES_ss) [sw2sw_def,w2n_n2w]); 26 27fun raw_x64_decode s = let 28 fun mk_bool_list n = 29 if n = 0 then ``[]:bool list`` else 30 mk_cons(mk_var("vvv"^int_to_string n,``:bool``),mk_bool_list (n-1)) 31 val l = length (explode s) div 2 32 val tm = mk_bool_list (8 * (20 - l)) 33 val tm = subst [``s:string`` |-> fromMLstring s, ``t:bool list``|->tm] ``bytebits s ++ t`` 34 val tm = (snd o dest_eq o concl o EVAL) tm 35 val th = EVAL (mk_comb(``x64_decode``,tm)) 36 val _ = computeLib.add_funs [th] 37 val (th,l) = let 38 val x = find_term (can (match_term ``bits2num xs``)) (concl th) 39 val thi = Q.INST [`w`|->`imm32`] w2bits_word32 40 val i = fst (match_term (snd (dest_comb x)) ((snd o dest_eq o concl o SPEC_ALL) thi)) 41 val th = REWRITE_RULE [GSYM thi] (INST i th) 42 val th = REWRITE_RULE [bits2num_w2bits,n2w_w2n] th 43 in (th,l+4) end handle e => (th,l) 44 val (th,l) = let 45 val x = find_term (can (match_term ``bits2num xs``)) (concl th) 46 val th = REWRITE_RULE [bytes_LEMMA, MATCH_MP n2w_SIGN_EXTEND bytes_LEMMA] th 47 val thi = Q.INST [`w`|->`imm8`] w2bits_word8 48 val i = fst (match_term (snd (dest_comb x)) ((snd o dest_eq o concl o SPEC_ALL) thi)) 49 val th = REWRITE_RULE [GSYM thi] (INST i th) 50 val th = REWRITE_RULE [bits2num_w2bits,n2w_w2n] th 51 in (th,l+1) end handle e => (th,l) 52 val tm = (snd o dest_comb o fst o dest_eq o concl) th 53 in (th,tm,l) end; 54 55fun x64_decode s = let 56 val (th,tm,l) = raw_x64_decode s 57 val th = MATCH_MP X64_NEXT_THM th 58 val th = SIMP_RULE std_ss [LENGTH] th 59 val th = nTimes l (SIMP_RULE std_ss [EVERY_DEF] o ONCE_REWRITE_RULE [ZREAD_INSTR_BYTES_def]) th 60 fun assums i n = 61 if i = 0 then [] else 62 subst [``n:num``|->numSyntax.term_of_int n] 63 ``ZREAD_INSTR (ZREAD_RIP s + n2w n) s = SOME (b2w I (TAKE 8 (DROP (8 * n) t)))`` :: assums (i-1) (n+1) 64 val th = foldr (uncurry DISCH) th (assums l 0) 65 val th = SIMP_RULE std_ss [WORD_ADD_0,GSYM WORD_ADD_ASSOC,word_add_n2w] th 66 val th = INST [``t:bool list``|->tm] th 67 val b2w_ss = eval_term_ss "b2w" ``(TAKE n t):bool list`` 68 val w2bits_ss = eval_term_ss "w2bits" ``w2bits ((b2w I x):word8):bool list`` 69 val th = SIMP_RULE (std_ss++b2w_ss) [FOLDR,MAP] th 70 val th = REWRITE_RULE [w2bits_b2w_word32,APPEND,CONS_11,COLLECT_BYTES_n2w_bits2num] th 71 val th = nTimes l UNDISCH th 72 val th = nTimes 20 (SIMP_RULE std_ss [EVERY_DEF,GSYM WORD_ADD_ASSOC,word_add_n2w] o 73 ONCE_REWRITE_RULE [ZREAD_INSTR_BYTES_def]) th 74 val th = SIMP_RULE std_ss [MAP,FOLDR,GSYM WORD_ADD_ASSOC,word_add_n2w,EVERY_DEF] th 75 val th = REWRITE_RULE [GSYM AND_IMP_INTRO,w2bits_EL] th 76 fun inst_one th = let 77 val (x,y) = (dest_eq o fst o dest_imp o concl) th 78 in UNDISCH (INST [y|->x] th) end 79 val th = repeat inst_one th 80 val th = REWRITE_RULE [] (DISCH_ALL th) 81 val th = REWRITE_RULE [GSYM w2bits_word8,COLLECT_BYTES_n2w_bits2num] th 82 val th = REWRITE_RULE [AND_IMP_INTRO,CONJ_ASSOC] th 83 val th = ONCE_REWRITE_RULE [CONJ_COMM] th 84 val th = REWRITE_RULE [GSYM CONJ_ASSOC,GSYM AND_IMP_INTRO] th 85 val any_b2w_ss = eval_term_ss "any_b2w" ``(b2w I xs):'a word`` 86 val th = SIMP_RULE (std_ss++any_b2w_ss) [] th 87 in th end handle e => (print " Decoding failed.\n" ; raise e); 88 89(* one step symbolic simulation *) 90 91val else_none_read_mem_lemma = (UNDISCH o SPEC_ALL) x64_else_none_read_mem_lemma 92val else_none_write_mem_lemma = (UNDISCH o SPEC_ALL) x64_else_none_write_mem_lemma 93val else_none_eflag_lemma = (UNDISCH o SPEC_ALL) x64_else_none_eflag_lemma 94val else_none_assert_lemma = (UNDISCH o SPEC_ALL) option_apply_assertT 95val else_none_conv1 = (fst o dest_eq o concl) else_none_read_mem_lemma 96val else_none_conv2 = (fst o dest_eq o concl) else_none_write_mem_lemma 97val else_none_conv3 = (fst o dest_eq o concl) else_none_eflag_lemma 98val else_none_conv4 = (fst o dest_eq o concl) else_none_assert_lemma 99fun else_none_conv tm = let 100 val ((i,t),th) = (match_term else_none_conv1 tm, else_none_read_mem_lemma) handle HOL_ERR _ => 101 (match_term else_none_conv2 tm, else_none_write_mem_lemma) handle HOL_ERR _ => 102 (match_term else_none_conv3 tm, else_none_eflag_lemma) handle HOL_ERR _ => 103 (match_term else_none_conv4 tm, else_none_assert_lemma) 104 in INST i (INST_TYPE t th) end; 105 106val ss = rewrites [x64_exec_def, ZREAD_REG_def, ZREAD_EFLAG_def, 107 ZREAD_MEM_def, ZREAD_RIP_def, ZWRITE_REG_def, ZWRITE_EFLAG_def, 108 ZWRITE_REG_def, ZWRITE_MEM_def, ZWRITE_RIP_def, bump_rip_def, 109 constT_def, addT_def, lockT_def, failureT_def, seqT_def, parT_def, 110 parT_unit_def, write_reg_def, read_reg_def, write_eflag_def, 111 read_eflag_def, write_rip_def, read_rip_def, write_m32_def, 112 read_m32_def, write_m8_def, read_m8_def, write_m16_def, 113 read_m16_def, write_m64_def, read_m64_def, seq_monad_thm, 114 write_monop_def, ea_Zr_def, ea_Zi_def, ea_Zrm_base_def, 115 ea_Zrm_index_def, ea_Zrm_def, ea_Zdest_def, ea_Zsrc_def, 116 ea_Zimm_rm_def, read_ea_def, read_src_ea_def, read_dest_ea_def, 117 write_ea_def, write_PF_def, write_ZF_def, write_SF_def, 118 write_logical_eflags_def, x64_exec_pop_def, x64_exec_pop_rip_def, 119 write_binop_with_carry_def, write_arith_eflags_except_CF_OF_def, 120 write_arith_eflags_def, add_with_carry_out_def, 121 clear_icache_seq_def, sub_with_borrow_out_def, 122 write_arith_result_def, clear_icache_def, 123 write_arith_result_no_CF_OF_def, write_arith_result_no_write_def, 124 write_logical_result_def, write_logical_result_no_write_def, 125 write_binop_def, write_monop_def, read_cond_def, read_reg_seq_def, 126 read_rip_seq_def, write_rip_seq_def, read_m8_seq_def, 127 write_m8_seq_def, read_m32_seq_def, write_m32_seq_def, 128 read_m16_seq_def, write_m16_seq_def, read_m64_seq_def, 129 write_m64_seq_def, APPLY_UPDATE_THM, WORD_EQ_ADD_LCANCEL, 130 x64_address_lemma, write_reg_seq_def, jump_to_ea_def, 131 x64_exec_push_def, x64_exec_push_rip_def, Zrm_is_memory_access_def, 132 write_eflag_seq_def, if_some_lemma, ZREAD_CLAUSES, 133 call_dest_from_ea_def, Zbinop_name_distinct, get_ea_address_def, 134 erase_eflags_def, write_result_erase_eflags_def,restrict_size_def, 135 word_signed_overflow_add_def, word_signed_overflow_sub_def, w2w_n2w, 136 bitTheory.BITS_THM, value_width_def, word_size_msb_def, 137 EVAL ``dimindex (:8) <= dimindex (:64)``, 138 EVAL ``dimindex (:16) <= dimindex (:64)``, 139 EVAL ``dimindex (:32) <= dimindex (:64)``] 140 141val SCALE_SIMP = LIST_CONJ [EVAL ``w2n (0w:word2)``,EVAL ``w2n (1w:word2)``, 142 EVAL ``w2n (2w:word2)``,EVAL ``w2n (3w:word2)``, 143 prove(``!w. 1w * w = w``,SIMP_TAC std_ss [wordsTheory.WORD_MULT_CLAUSES])] 144 145fun x64_step s = let 146 val th = x64_decode s 147 val tm = (fst o dest_eq o fst o dest_imp o concl) th 148 val th1 = SIMP_CONV (std_ss++ss++wordsLib.SIZES_ss) 149 [x64_execute_def,Zrm_distinct,Zrm_11,Zreg_distinct] tm 150 fun cc th = CONV_RULE (ONCE_DEPTH_CONV else_none_conv) th 151 fun f th = (DISCH_ALL o CONV_RULE (RAND_CONV (SIMP_CONV std_ss [pull_if_lemma])) o 152 UNDISCH_ALL o SIMP_RULE (std_ss++ss) [LET_DEF,Zreg_distinct,Zeflags_distinct] o 153 DISCH_ALL o cc) th 154 fun change f x = let val y = f x in if concl y = concl x then x else change f y end 155 val th1 = change f th1 156 val th1 = SIMP_RULE (std_ss++ss) [Zreg_distinct, Zeflags_distinct] th1 157 val th1 = DISCH_ALL (MATCH_MP th (UNDISCH_ALL th1)) 158 val th1 = REWRITE_RULE [AND_IMP_INTRO,GSYM CONJ_ASSOC] (DISCH_ALL th1) 159 val th1 = REWRITE_RULE [GSYM ZREAD_MEM2_WORD64_def, GSYM ZREAD_MEM2_WORD32_def, 160 GSYM ZREAD_MEM2_WORD16_def, 161 GSYM ZWRITE_MEM2_WORD64_def, GSYM ZWRITE_MEM2_WORD32_def, 162 GSYM ZWRITE_MEM2_WORD16_def] th1 163 val th1 = STRENGTHEN_CONSEQ_CONV_RULE 164 (CONSEQ_REWRITE_CONV ([],[CAN_ZREAD_ZWRITE_THM],[])) th1 165 handle UNCHANGED => th1 166 val th1 = SIMP_RULE bool_ss [GSYM AND_IMP_INTRO,pred_setTheory.IN_INSERT,pred_setTheory.NOT_IN_EMPTY] th1 167 val th1 = SIMP_RULE bool_ss [AND_IMP_INTRO,GSYM CONJ_ASSOC] th1 168 val th1 = SIMP_RULE bool_ss [SIMP_RULE (srw_ss()) [] (INST_TYPE[``:'a``|->``:32``]w2n_lt)] th1 169 val th1 = SIMP_RULE std_ss [SCALE_SIMP] th1 170 in th1 end; 171 172(* 173 174 open x64_encodeLib; 175 176 val th = x64_step (x64_encode "dec eax") 177 val th = x64_step "E9" (* example of partial decoder evaluation with imm32 *) 178 val th = x64_step "83F1" (* example of partial decoder evaluation with imm8 *) 179 val th = x64_step (x64_encode "mov DWORD [rsi],5000") 180 val th = x64_step (x64_encode "mov BYTE [rax],-100") 181 val th = x64_step (x64_encode "mov [rsi],rdx"); 182 val th = x64_step (x64_encode "INC r11"); 183 val th = x64_step (x64_encode "DEC QWORD [rax]"); 184 val th = x64_step (x64_encode "NOT bx"); 185 val th = x64_step (x64_encode "NEG r15"); 186 val th = x64_step (x64_encode "div rsi") 187 val th = x64_step (x64_encode "ADD rax, 4"); 188 val th = x64_step (x64_encode "ADC rbx, rax"); 189 val th = x64_step (x64_encode "AND [rax+r11],rax"); 190 val th = x64_step (x64_encode "XOR WORD [4000],45"); 191 val th = x64_step (x64_encode "OR r12, 50000"); 192 val th = x64_step (x64_encode "SBB eax,[rax]"); 193 val th = x64_step (x64_encode "SUB r11,r12"); 194 val th = x64_step (x64_encode "CMP rax,3"); 195 val th = x64_step (x64_encode "TEST eax,3"); 196 val th = x64_step (x64_encode "xchg [rbx],rax") 197 val th = x64_step (x64_encode "SHL eax,1"); 198 val th = x64_step (x64_encode "SHR rax,3"); 199 val th = x64_step (x64_encode "SAR bx,4"); 200 val th = x64_step (x64_encode "CMOVE rax, [r15+67]"); 201 val th = x64_step (x64_encode "CMOVNE eax, [rsi]"); 202 val th = x64_step (x64_encode "LEA rax, [8*rbx+rcx+5000000]"); 203 val th = x64_step (x64_encode "LOOP -5"); 204 val th = x64_step (x64_encode "LOOPE -15"); 205 val th = x64_step (x64_encode "LOOPNE 50"); 206 val th = x64_step (x64_encode "JB 40"); 207 val th = x64_step (x64_encode "JNB -4000"); 208 val th = x64_step (x64_encode "JMP 400"); 209 val th = x64_step (x64_encode "JMP rax"); 210 val th = x64_step (x64_encode "POP rax"); 211 val th = x64_step (x64_encode "PUSH QWORD [rbx]"); 212 val th = x64_step (x64_encode "DIV r11"); 213 val th = x64_step (x64_encode "MUL r12d"); 214 val th = x64_step (x64_encode "XADD rax,rdx"); 215 val th = x64_step (x64_encode "RET"); 216 val th = x64_step (x64_encode "RET 16"); 217 val th = x64_step (x64_encode "add rsp,80"); 218 val th = x64_step (x64_encode "mov [rsp+80],rax"); 219 val th = x64_step (x64_encode "mov rax,[rsp+80]"); 220 val th = x64_step (x64_encode "CALL r15"); 221 val th = x64_step (x64_encode "CMPXCHG r11,r14"); 222 val th = x64_step (x64_encode "mov rsi,4611686018427844360") 223 val th = x64_step (x64_encode "movzx rdx,BYTE [rax]"); 224 val th = x64_step (x64_encode "movzx rdx,al"); 225 val th = x64_step (x64_encode "movzx rdx,WORD [rax]"); 226 val th = x64_step (x64_encode "movzx rdx,ax"); 227 228*) 229 230val _ = output_words_as_hex(); 231 232fun x64_test_aux i input output = let 233 val rw = x64_step i 234 val old_regs = ["RAX", "RBX", "RCX", "RDX", "RSI", "RDI", "RSP", "RBP"] 235 val new_regs = ["R8", "R9", "R10", "R11", "R12", "R13", "R14", "R15"] 236 fun format state (i,j) = 237 if i = "RIP" 238 then ("ZREAD_RIP "^state^" = 0x"^j^"w") 239 else if mem i new_regs 240 then ("ZREAD_REG z"^i^" "^state^" = 0x"^j^"w") 241 else if mem i old_regs 242 then ("ZREAD_REG "^i^" "^state^" = 0x"^j^"w") 243 else if size i = 2 244 then ("ZREAD_EFLAG Z_"^i^" "^state^" = SOME "^(if j = "1" then "T" else "F")) 245 else ("ZREAD_MEM 0x"^i^"w "^state^" = SOME (0x"^j^"w)") 246 fun p y = Parse.Term [QUOTE y] 247 fun f s = map (p o format s) 248 val th = foldr (fn (x,y) => DISCH x y) rw (f "s" input) 249 val th = SIMP_RULE std_ss [Zrm_distinct,Zrm_11,Zreg_distinct,Zeflags_distinct] th 250 val th = SIMP_RULE std_ss [word_add_n2w,WORD_ADD_0,b2w_def,bits2num_def,GSYM AND_IMP_INTRO] th 251 val th = SIMP_RULE (std_ss++SIZES_ss) [w2n_n2w,word_mul_n2w,word_add_n2w,word_sub_def,word_2comp_n2w] th 252 val ss = eval_term_ss "a" ``(bytes2word (xs:word8 list)):word32`` 253 val th = SIMP_RULE (std_ss++ss++SIZES_ss) [n2w_11] th 254 val th = ONCE_REWRITE_RULE [ZREAD_RIP_ADD_0] th 255 val th = REWRITE_RULE [AND_IMP_INTRO] th 256 val th = REWRITE_RULE [GSYM CONJ_ASSOC] th 257 val xs = find_terms (can (match_term ``ZWRITE_EFLAG x NONE``)) (concl th) 258 val xs = map (implode o tl o tl o explode o fst o dest_const o snd o dest_comb o fst o dest_comb) xs 259 fun distinct [] = [] | distinct (x::xs) = x::distinct (filter (fn y => not (y = x)) xs) 260 val xs = distinct xs 261 val output2 = filter (fn (x,y) => not (mem x xs)) output 262 val output1 = filter (fn (x,y) => mem x xs) output 263 val _ = map (fn (x,y) => print (" ["^x^"]")) output1 264 val tm = list_mk_conj (f "(THE (X64_NEXT s))" output2) 265 val tm2 = (hd o hyp o UNDISCH) th 266 val goal = mk_imp(tm2,tm) 267(* 268 set_goal([],goal) 269*) 270 val result = prove(goal, 271 STRIP_TAC 272 THEN (ASSUME_TAC o UNDISCH_ALL o REWRITE_RULE [GSYM AND_IMP_INTRO]) th 273 THEN ASM_SIMP_TAC std_ss [ZREAD_CLAUSES,optionTheory.THE_DEF,Zreg_distinct,Zeflags_distinct] 274 THEN STRIP_ASSUME_TAC x64_state_EXPAND 275 THEN FULL_SIMP_TAC std_ss [ZREAD_REG_def,ZREAD_EFLAG_def,ZREAD_MEM_def,ZREAD_RIP_def, 276 ZWRITE_MEM_def,ZWRITE_REG_def,ZWRITE_EFLAG_def,ZWRITE_RIP_def, APPLY_UPDATE_THM,Zreg_distinct] 277 THEN EVAL_TAC) 278 val result = REWRITE_RULE [GSYM AND_IMP_INTRO] result 279 in result end; 280 281fun x64_test s diff = let 282 fun get_input (x,y,z) = (x,y) 283 fun get_output (x,y,z) = (x,z) 284 val input = map get_input diff 285 val output = map get_output diff 286 val i = last(String.tokens (fn c => mem c [#" ",#"\t"]) s) 287 val _ = print ("Testing: "^s) 288 val th = SOME (x64_test_aux i input output) handle e => NONE 289 in case th of 290 NONE => (print " --- FAILED!\n"; ()) 291 | SOME th => (print ", ok.\n"; ()) 292 end; 293 294 295 296(* 297 298val _ = x64_test "lea RAX,[R15+4*R13-400] | 4B8D84AF70FEFFFF" 299 [("RAX","dd7685b0d983e708","0f28c87c9005ada0"), 300 ("RBX","6d0dc0863d9fb8a5","6d0dc0863d9fb8a5"), 301 ("RCX","57d4da275d8c867f","57d4da275d8c867f"), 302 ("RDX","04f0600453b21541","04f0600453b21541"), 303 ("RSI","9eab61a9939b06b5","9eab61a9939b06b5"), 304 ("RDI","0f74a94248faaa4a","0f74a94248faaa4a"), 305 ("RSP","00007fff5fbff230","00007fff5fbff230"), 306 ("RBP","00007fff5fbff2a0","00007fff5fbff2a0"), 307 ("R8" ,"2e52646f7adbc694","2e52646f7adbc694"), 308 ("R9" ,"6851092e695571ff","6851092e695571ff"), 309 ("R10","f2593e1dac5dbbce","f2593e1dac5dbbce"), 310 ("R11","940d948eff7cc2b1","940d948eff7cc2b1"), 311 ("R12","147ae1b1548e57c4","147ae1b1548e57c4"), 312 ("R13","03ca121f4c116f1c","03ca121f4c116f1c"), 313 ("R14","d9d91c6175b5684d","d9d91c6175b5684d"), 314 ("R15","00007fff5fbff2c0","00007fff5fbff2c0"), 315 ("RIP","0000000100001b87","0000000100001b8f"), 316 ("CF","0","0"), 317 ("PF","0","0"), 318 ("AF","0","0"), 319 ("ZF","1","1"), 320 ("SF","1","1"), 321 ("OF","1","1"), 322 ("00007fff5fbff3f8","73","73"), 323 ("00007fff5fbff3f9","00","00"), 324 ("00007fff5fbff3fa","e4","e4"), 325 ("00007fff5fbff3fb","6c","6c"), 326 ("00007fff5fbff3fc","d7","d7"), 327 ("00007fff5fbff3fd","f3","f3"), 328 ("00007fff5fbff3fe","fc","fc"), 329 ("00007fff5fbff3ff","64","64")] 330 331*) 332 333end 334