1 2open HolKernel boolLib bossLib Parse; 3 4open x64_coretypesTheory; 5 6val _ = new_theory "x64_ast"; 7 8 9(* ---------------------------------------------------------------------------------- *> 10 11 This theory defines the abstract syntax tree (AST) for x64 instructions. It uses 12 13 word64 - type of immediate constant 14 Zreg - type of register name 15 16 from x64_coretypesTheory. 17 18<* ---------------------------------------------------------------------------------- *) 19 20 21val _ = Hol_datatype ` 22 Zrm = Zr of Zreg (* register *) 23 | Zm of (word2 # Zreg) option => Zreg option => word64 (* mem[2^{scale} * index + base + displacement] *)`; 24 25(* check whether rm requires a lock, i.e. specifies a memory access *) 26 27val Zrm_is_memory_access_def = Define ` 28 (Zrm_is_memory_access (Zm i b d) = T) /\ 29 (Zrm_is_memory_access (Zr r) = F)`; 30 31val _ = Hol_datatype ` (* Here XX is one of 8, 16, 32, 64. *) 32 Zdest_src = Zrm_i of Zrm => word64 (* mnemonic r/mXX, immXX (sign-extended) *) 33 | Zrm_r of Zrm => Zreg (* mnemonic r/mXX, rXX *) 34 | Zr_rm of Zreg => Zrm (* mnemonic rXX, r/mXX *) `; 35 36val _ = Hol_datatype ` 37 Zimm_rm = Zi_rm of Zrm (* r/mXX *) 38 | Zi of word64 (* sign-extended immediate *) `; 39 40val _ = Hol_datatype `Zbinop_name = Zadc | Zadd | Zand | Zcmp | Zor | Zshl | Zshr | Zsar | Zsub | Zsbb | Ztest | Zxor `; 41val _ = Hol_datatype `Zmonop_name = Zdec | Zinc | Znot | Zneg `; 42 43val _ = Hol_datatype `Zcond = (* this list is not complete *) 44 Z_ALWAYS (* N = not *) 45 | Z_E | Z_NE (* E = equal *) 46 | Z_S | Z_NS (* S = signed *) 47 | Z_A | Z_NA (* A = above *) 48 | Z_B | Z_NB (* B = below *)`; 49 50val _ = Hol_datatype ` 51 Zinstruction = Zbinop of Zbinop_name => Zsize => Zdest_src 52 | Zmonop of Zmonop_name => Zsize => Zrm 53 | Zcmpxchg of Zsize => Zrm => Zreg 54 | Zxadd of Zsize => Zrm => Zreg 55 | Zxchg of Zsize => Zrm => Zreg 56 | Zmul of Zsize => Zrm 57 | Zdiv of Zsize => Zrm 58 | Zlea of Zsize => Zdest_src 59 | Zpop of Zrm 60 | Zpush of Zimm_rm 61 | Zcall of Zimm_rm 62 | Zret of word64 63 | Zcpuid 64 | Zmov of Zcond => Zsize => Zdest_src 65 | Zmovzx of Zsize => Zdest_src => Zsize 66 | Zjcc of Zcond => word64 (* jcc includes jmp rel, i.e. unconditional relative jumps. *) 67 | Zjmp of Zrm (* jmp excludes relative jumps, see jcc. *) 68 | Zloop of Zcond => word64 (* Here Zcond over approximates possibilities. *)`; 69 70(* This semantics understands the following prefixes in addition to the REX prefix. *) 71val _ = Hol_datatype `Zprefix = Zlock 72 | Zbranch_taken 73 | Zbranch_not_taken 74 | Zoperand_size_override `; 75 76val Zprefix_group_def = Define ` 77 (Zprefix_group Zlock = 1) /\ 78 (Zprefix_group Zbranch_taken = 2) /\ 79 (Zprefix_group Zbranch_not_taken = 2) /\ 80 (Zprefix_group Zoperand_size_override = 3)`; 81 82val _ = Hol_datatype `Zinst = Zfull_inst of Zprefix list => Zinstruction`; 83 84 85val _ = export_theory (); 86