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