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