1 2open HolKernel boolLib bossLib Parse; val _ = new_theory "x86_"; 3 4open wordsTheory bit_listTheory; 5 6open x86_coretypesTheory x86_astTheory x86_opsemTheory; 7open x86_seq_monadTheory x86_decoderTheory x86_icacheTheory; 8 9 10(* ---------------------------------------------------------------------------------- *> 11 12 Here the decoder from x86_decoderTheory is put together with x86_execute 13 from x86_opsemTheory and the sequential monad from x86_seq_monadTheory. 14 15<* ---------------------------------------------------------------------------------- *) 16 17val iiid_dummy_def = Define `iiid_dummy = <| proc:=0; program_order_index:=0 |>`; 18 19val x86_decode_bytes_def = Define ` 20 x86_decode_bytes b = x86_decode (FOLDR APPEND [] (MAP w2bits b))`; 21 22val x86_execute_some_def = Define ` 23 x86_execute_some i w s = option_apply (x86_execute iiid_dummy i w s) (\t. SOME (SND t))`; 24 25val X86_NEXT_def = Define ` 26 X86_NEXT s = 27 let e = XREAD_EIP s in (* read eip *) 28 let xs = MAP THE (XREAD_INSTR_BYTES 20 e s) in (* read next 20 bytes *) 29 let m = x86_decode_bytes xs in (* attempt to decode *) 30 if m = NONE then NONE else (* if decoded fail, return NONE *) 31 let (i,w) = THE m in (* otherwise extract content *) 32 let n = 20 - (LENGTH w DIV 8) in (* calc length of instruction *) 33 if EVERY (\x. ~(x = NONE)) (XREAD_INSTR_BYTES n e s) (* check that the memory is there *) 34 then x86_execute_some i (n2w n) s else NONE (* execute the instruction *)`; 35 36val X86_NEXT_REL_def = Define ` 37 X86_NEXT_REL s t = ?u. X86_ICACHE s u /\ (X86_NEXT u = SOME t)`; 38 39 40(* help to evaluate X86_NEXT *) 41 42val X86_NEXT_THM = store_thm("X86_NEXT_THM", 43 ``(x86_decode xs = SOME (i,w)) ==> 44 (FOLDR APPEND [] (MAP w2bits (MAP THE (XREAD_INSTR_BYTES 20 (XREAD_EIP s) s))) = xs) ==> 45 (EVERY (\x. ~(x = NONE)) (XREAD_INSTR_BYTES (20 - (LENGTH w DIV 8)) (XREAD_EIP s) s)) ==> 46 (x86_execute iiid_dummy i (n2w (20 - (LENGTH w DIV 8))) s = SOME (tt,s')) ==> 47 (X86_NEXT s = SOME s')``, 48 SIMP_TAC std_ss [X86_NEXT_def,LET_DEF,XREAD_REG_def,x86_decode_bytes_def, 49 x86_execute_some_def,option_apply_def]); 50 51 52(* test whether decoding works, if this is slow then something's wrong *) 53 54val t1 = Time.now(); 55val th = EVAL ``x86_decode(bytebits "D1F8")``; (* sar eax, 1 *) 56val t2 = Time.now(); 57val elapsed_time = Time.toReal t2 - Time.toReal t1 58val _ = elapsed_time < 5.0 orelse failwith("Decoding failed to use compset properly.") 59 60val _ = export_theory (); 61