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