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