1
2open HolKernel boolLib bossLib Parse;
3open wordsTheory bit_listTheory listTheory;
4
5val _ = new_theory "x86_coretypes";
6
7
8(* ---------------------------------------------------------------------------------- *>
9
10  This theory defines the types and operations over these types for the x86 model.
11
12<* ---------------------------------------------------------------------------------- *)
13
14(* used by the AST *)
15
16(* type of address values and of values stored in registers *)
17val _ = type_abbrev("Ximm",``:word32``);
18
19val _ = Hol_datatype `Xreg = EAX | EBX | ECX | EDX | ESP | EBP | ESI | EDI `;
20
21(* used elsewhere *)
22
23val _ = Hol_datatype `
24  Xeflags = X_CF | X_PF | X_AF | X_ZF | X_SF | X_OF `;
25
26val _ = Hol_datatype `
27  Xea =
28      Xea_i of Ximm     (* constant       *)
29    | Xea_r of Xreg     (* register name  *)
30    | Xea_m of word32   (* memory address *) `;
31
32val _ = Hol_datatype   `iiid = <| proc : num ;
33             program_order_index : num |>`;
34
35
36
37val _ = export_theory ();
38