1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
|
(X86ISA::PRECONDITIONS)
(X86ISA::PROGRAM-EFFECTS-1
(101 52 (:REWRITE DEFAULT-+-2))
(93 3 (:REWRITE X86ISA::GET-PREFIXES-OPENER-LEMMA-GROUP-2-PREFIX))
(65 52 (:REWRITE DEFAULT-+-1))
(65 3 (:REWRITE X86ISA::GET-PREFIXES-OPENER-LEMMA-GROUP-4-PREFIX))
(65 3 (:REWRITE X86ISA::GET-PREFIXES-OPENER-LEMMA-GROUP-3-PREFIX))
(61 3 (:REWRITE X86ISA::GET-PREFIXES-OPENER-LEMMA-NO-LEGACY-PREFIX-BUT-REX-PREFIX))
(20 10 (:REWRITE DEFAULT-UNARY-MINUS))
(17 17 (:REWRITE X86ISA::RME08-WHEN-64-BIT-MODEP-AND-FS/GS))
(16 16 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
(12 12 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
(12 12 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
(5 3 (:REWRITE X86ISA::RB-RETURNS-X86-IN-NON-MARKING-VIEW-IF-NO-ERROR))
(4 4 (:TYPE-PRESCRIPTION BITOPS::ASH-NATP-TYPE))
(4 4 (:REWRITE X86ISA::XR-OF-XW-INTER-FIELD))
(3 3 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-2))
(3 3 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-1))
(2 2 (:REWRITE-QUOTED-CONSTANT BFIX-UNDER-BIT-EQUIV))
(2 1 (:DEFINITION X86ISA::MARKING-VIEW))
(1 1 (:DEFINITION X86ISA::MARKING-VIEW$A))
)
(X86ISA::PROGRAM-EFFECTS-2
(284 145 (:REWRITE DEFAULT-+-2))
(276 6 (:REWRITE X86ISA::GET-PREFIXES-OPENER-LEMMA-GROUP-2-PREFIX))
(201 145 (:REWRITE DEFAULT-+-1))
(200 6 (:REWRITE X86ISA::GET-PREFIXES-OPENER-LEMMA-GROUP-4-PREFIX))
(198 6 (:REWRITE X86ISA::GET-PREFIXES-OPENER-LEMMA-GROUP-3-PREFIX))
(183 6 (:REWRITE X86ISA::GET-PREFIXES-OPENER-LEMMA-NO-LEGACY-PREFIX-BUT-REX-PREFIX))
(158 1 (:REWRITE X86ISA::PROGRAM-EFFECTS-1))
(114 19 (:REWRITE BFIX-WHEN-NOT-1))
(76 76 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-3))
(67 67 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-2))
(67 67 (:REWRITE X86ISA::CANONICAL-ADDRESS-P-LIMITS-THM-1))
(40 20 (:REWRITE DEFAULT-UNARY-MINUS))
(38 38 (:TYPE-PRESCRIPTION BIT->BOOL$INLINE))
(38 19 (:REWRITE BFIX-WHEN-NOT-BITP))
(38 19 (:REWRITE BFIX-WHEN-NOT-BIT->BOOL))
(38 19 (:REWRITE BFIX-WHEN-BIT->BOOL))
(34 34 (:REWRITE X86ISA::RME08-WHEN-64-BIT-MODEP-AND-FS/GS))
(24 24 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
(24 3 (:REWRITE BITOPS::BASIC-SIGNED-BYTE-P-OF-+))
(16 16 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
(12 12 (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
(10 8 (:REWRITE X86ISA::RB-XW-RFLAGS-NOT-AC-VALUES-IN-SYS-VIEW))
(8 8 (:TYPE-PRESCRIPTION BITOPS::ASH-NATP-TYPE))
(8 6 (:REWRITE X86ISA::RB-RETURNS-X86-IN-NON-MARKING-VIEW-IF-NO-ERROR))
(8 4 (:REWRITE IFIX-WHEN-NOT-INTEGERP))
(8 1 (:REWRITE X86ISA::UNSIGNED-BYTE-P-WHEN-CR0BITS-P))
(6 6 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-UNSIGNED-BYTE-P-SMALLER))
(6 6 (:REWRITE BITOPS::SIGNED-BYTE-P-WHEN-SIGNED-BYTE-P-SMALLER))
(6 6 (:REWRITE BITOPS::SIGNED-BYTE-P-MONOTONICITY))
(6 6 (:REWRITE BITOPS::SIGNED-BYTE-P-INCR))
(5 3 (:REWRITE X86ISA::RB-XW-RFLAGS-NOT-AC-STATE-IN-SYS-VIEW))
(3 3 (:REWRITE X86ISA::SIGNED-BYTE-P-LIMITS-THM))
(3 3 (:REWRITE X86ISA::RFLAGSBITS->ZF-OF-WRITE-WITH-MASK))
(3 3 (:REWRITE X86ISA::RFLAGSBITS->VM-OF-WRITE-WITH-MASK))
(3 3 (:REWRITE X86ISA::RFLAGSBITS->VIP-OF-WRITE-WITH-MASK))
(3 3 (:REWRITE X86ISA::RFLAGSBITS->VIF-OF-WRITE-WITH-MASK))
(3 3 (:REWRITE X86ISA::RFLAGSBITS->TF-OF-WRITE-WITH-MASK))
(3 3 (:REWRITE X86ISA::RFLAGSBITS->SF-OF-WRITE-WITH-MASK))
(3 3 (:REWRITE X86ISA::RFLAGSBITS->RF-OF-WRITE-WITH-MASK))
(3 3 (:REWRITE X86ISA::RFLAGSBITS->RES5-OF-WRITE-WITH-MASK))
(3 3 (:REWRITE X86ISA::RFLAGSBITS->RES4-OF-WRITE-WITH-MASK))
(3 3 (:REWRITE X86ISA::RFLAGSBITS->RES3-OF-WRITE-WITH-MASK))
(3 3 (:REWRITE X86ISA::RFLAGSBITS->RES2-OF-WRITE-WITH-MASK))
(3 3 (:REWRITE X86ISA::RFLAGSBITS->RES1-OF-WRITE-WITH-MASK))
(3 3 (:REWRITE X86ISA::RFLAGSBITS->PF-OF-WRITE-WITH-MASK))
(3 3 (:REWRITE X86ISA::RFLAGSBITS->OF-OF-WRITE-WITH-MASK))
(3 3 (:REWRITE X86ISA::RFLAGSBITS->NT-OF-WRITE-WITH-MASK))
(3 3 (:REWRITE X86ISA::RFLAGSBITS->IOPL-OF-WRITE-WITH-MASK))
(3 3 (:REWRITE X86ISA::RFLAGSBITS->INTF-OF-WRITE-WITH-MASK))
(3 3 (:REWRITE X86ISA::RFLAGSBITS->ID-OF-WRITE-WITH-MASK))
(3 3 (:REWRITE X86ISA::RFLAGSBITS->DF-OF-WRITE-WITH-MASK))
(3 3 (:REWRITE X86ISA::RFLAGSBITS->AF-OF-WRITE-WITH-MASK))
(3 3 (:REWRITE X86ISA::RFLAGSBITS->AC-OF-WRITE-WITH-MASK))
(3 2 (:REWRITE X86ISA::64-BIT-MODEP-OF-XW))
(2 2 (:TYPE-PRESCRIPTION X86ISA::CR0BITS-P$INLINE))
(2 2 (:REWRITE-QUOTED-CONSTANT BFIX-UNDER-BIT-EQUIV))
(2 1 (:REWRITE X86ISA::CR0BITS-P-WHEN-UNSIGNED-BYTE-P))
(2 1 (:DEFINITION X86ISA::MARKING-VIEW))
(1 1 (:REWRITE BITOPS::UNSIGNED-BYTE-P-INCR))
(1 1 (:DEFINITION X86ISA::MARKING-VIEW$A))
)
|
