1
2open HolKernel boolLib bossLib Parse;
3
4open x86_coretypesTheory;
5
6val _ = new_theory "x86_ast";
7
8
9(* ---------------------------------------------------------------------------------- *>
10
11  This theory defines the abstract syntax tree (AST) for x86 instructions. It uses
12
13     Ximm - type of immediate constant
14     Xreg - type of register name
15
16  from x86_coretypesTheory.
17
18  Nearly all instructions operate only over 32-bit data.
19  However, MOV, CMP and DEC are defined also for some 8-bit operations.
20
21<* ---------------------------------------------------------------------------------- *)
22
23
24val _ = Hol_datatype `
25  Xrm = Xr of Xreg                                         (* register *)
26      | Xm of (word2 # Xreg) option => Xreg option => Ximm (* mem[2^{scale} * index + base + displacement] *)`;
27
28(* check whether rm requires a lock, i.e. specifies a memory access *)
29
30val rm_is_memory_access_def = Define `
31  (rm_is_memory_access (Xm i b d) = T) /\
32  (rm_is_memory_access (Xr r) = F)`;
33
34val _ = Hol_datatype `
35  Xdest_src = Xrm_i of Xrm  => Ximm  (* mnemonic r/m32, imm32 or mnemonic r/m32, imm8 (sign-extended) *)
36            | Xrm_r of Xrm  => Xreg  (* mnemonic r/m32, r32 *)
37            | Xr_rm of Xreg => Xrm   (* mnemonic r32, r/m32 *)  `;
38
39val _ = Hol_datatype `
40  Ximm_rm = Xi_rm of Xrm    (* r/m32 *)
41          | Xi    of Ximm   (* imm32 or imm8 (sign-extended) *) `;
42
43val _ = Hol_datatype `Xbinop_name = Xadc | Xadd | Xand | Xcmp | Xor | Xshl | Xshr | Xsar | Xsub | Xsbb | Xtest | Xxor `;
44val _ = Hol_datatype `Xmonop_name = Xdec | Xinc | Xnot | Xneg `;
45
46val _ = Hol_datatype `Xcond = (* this list is not complete *)
47    X_ALWAYS            (* N = not     *)
48  | X_E | X_NE          (* E = equal   *)
49  | X_S | X_NS          (* S = signed  *)
50  | X_A | X_NA          (* A = above   *)
51  | X_B | X_NB          (* B = below   *)`;
52
53val _ = Hol_datatype `
54  Xinstruction = Xbinop     of Xbinop_name => Xdest_src
55               | Xmonop     of Xmonop_name => Xrm
56               | Xcmpxchg   of Xrm => Xreg
57               | Xxadd      of Xrm => Xreg
58               | Xxchg      of Xrm => Xreg
59               | Xmul       of Xrm
60               | Xdiv       of Xrm
61               | Xlea       of Xdest_src
62               | Xpop       of Xrm
63               | Xpush      of Ximm_rm
64               | Xcall      of Ximm_rm
65               | Xret       of Ximm
66               | Xmov       of Xcond => Xdest_src
67               | Xmovzx     of Xdest_src
68               | Xmov_byte  of Xdest_src
69               | Xcmp_byte  of Xdest_src
70               | Xdec_byte  of Xrm
71               | Xjcc       of Xcond => Ximm      (* jcc includes jmp rel, i.e. unconditional relative jumps. *)
72               | Xjmp       of Xrm                (* jmp excludes relative jumps, see jcc. *)
73               | Xloop      of Xcond => Ximm      (* Here Xcond over approximates possibilities. *)
74               | Xpushad
75               | Xpopad     `;
76
77val _ = Hol_datatype `Xpre_g1 = Xlock | Xg1_none `;
78val _ = Hol_datatype `Xpre_g2 = Xbranch_taken | Xbranch_not_taken | Xg2_none `;
79
80val _ = Hol_datatype `Xinst = Xprefix of Xpre_g1 => Xpre_g2 => Xinstruction`;
81
82
83val _ = export_theory ();
84