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
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
;; GENERATED BY `isaspec`. DO NOT EDIT!!!
(attr MInst.FpuRRR (tag isaspec_generated))
(spec
(MInst.FpuRRR fpu_op size rd rn rm)
(provide
(match
size
((Size64)
(match
fpu_op
((Add)
(with
(t3)
(and
(= t3 (FPAdd! (extract 63 0 (conv_to 128 (as rn (bv 64)))) (extract 63 0 (conv_to 128 (as rm (bv 64)))) fpcr))
(= (conv_to 128 (as rd (bv 64))) (zero_ext 128 t3))
)
)
)
((Sub)
(with
(t3)
(and
(= t3 (FPSub! (extract 63 0 (conv_to 128 (as rn (bv 64)))) (extract 63 0 (conv_to 128 (as rm (bv 64)))) fpcr))
(= (conv_to 128 (as rd (bv 64))) (zero_ext 128 t3))
)
)
)
((Mul)
(with
(t3)
(and
(= t3 (FPMul! (extract 63 0 (conv_to 128 (as rn (bv 64)))) (extract 63 0 (conv_to 128 (as rm (bv 64)))) fpcr))
(= (conv_to 128 (as rd (bv 64))) (zero_ext 128 t3))
)
)
)
((Div)
(with
(t3)
(and
(= t3 (FPDiv! (extract 63 0 (conv_to 128 (as rn (bv 64)))) (extract 63 0 (conv_to 128 (as rm (bv 64)))) fpcr))
(= (conv_to 128 (as rd (bv 64))) (zero_ext 128 t3))
)
)
)
((Min)
(with
(t3)
(and
(= t3 (FPMin! (extract 63 0 (conv_to 128 (as rn (bv 64)))) (extract 63 0 (conv_to 128 (as rm (bv 64)))) fpcr))
(= (conv_to 128 (as rd (bv 64))) (zero_ext 128 t3))
)
)
)
((Max)
(with
(t3)
(and
(= t3 (FPMax! (extract 63 0 (conv_to 128 (as rn (bv 64)))) (extract 63 0 (conv_to 128 (as rm (bv 64)))) fpcr))
(= (conv_to 128 (as rd (bv 64))) (zero_ext 128 t3))
)
)
)
)
)
((Size32)
(match
fpu_op
((Add)
(with
(t3)
(and
(= t3 (FPAdd! (extract 31 0 (conv_to 128 (as rn (bv 64)))) (extract 31 0 (conv_to 128 (as rm (bv 64)))) fpcr))
(= (conv_to 128 (as rd (bv 64))) (zero_ext 128 t3))
)
)
)
((Sub)
(with
(t3)
(and
(= t3 (FPSub! (extract 31 0 (conv_to 128 (as rn (bv 64)))) (extract 31 0 (conv_to 128 (as rm (bv 64)))) fpcr))
(= (conv_to 128 (as rd (bv 64))) (zero_ext 128 t3))
)
)
)
((Mul)
(with
(t3)
(and
(= t3 (FPMul! (extract 31 0 (conv_to 128 (as rn (bv 64)))) (extract 31 0 (conv_to 128 (as rm (bv 64)))) fpcr))
(= (conv_to 128 (as rd (bv 64))) (zero_ext 128 t3))
)
)
)
((Div)
(with
(t3)
(and
(= t3 (FPDiv! (extract 31 0 (conv_to 128 (as rn (bv 64)))) (extract 31 0 (conv_to 128 (as rm (bv 64)))) fpcr))
(= (conv_to 128 (as rd (bv 64))) (zero_ext 128 t3))
)
)
)
((Min)
(with
(t3)
(and
(= t3 (FPMin! (extract 31 0 (conv_to 128 (as rn (bv 64)))) (extract 31 0 (conv_to 128 (as rm (bv 64)))) fpcr))
(= (conv_to 128 (as rd (bv 64))) (zero_ext 128 t3))
)
)
)
((Max)
(with
(t3)
(and
(= t3 (FPMax! (extract 31 0 (conv_to 128 (as rn (bv 64)))) (extract 31 0 (conv_to 128 (as rm (bv 64)))) fpcr))
(= (conv_to 128 (as rd (bv 64))) (zero_ext 128 t3))
)
)
)
)
)
)
)
(require
(match
size
((Size64) (match fpu_op ((Add) true) ((Sub) true) ((Mul) true) ((Div) true) ((Min) true) ((Max) true)))
((Size32) (match fpu_op ((Add) true) ((Sub) true) ((Mul) true) ((Div) true) ((Min) true) ((Max) true)))
)
)
)