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
;; GENERATED BY `isaspec`. DO NOT EDIT!!!
(attr MInst.FpuMoveFPImm (tag isaspec_generated))
(spec
(MInst.FpuMoveFPImm rd imm size)
(provide
(match
size
((Size64)
(=
rd
(zero_ext
128
(concat
(concat
(extract 7 7 (:imm imm))
(concat (concat (bvnot (extract 6 6 (:imm imm))) (replicate (extract 6 6 (:imm imm)) 8)) (extract 5 4 (:imm imm)))
)
(concat (extract 3 0 (:imm imm)) #x000000000000)
)
)
)
)
((Size32)
(=
rd
(zero_ext
128
(concat
(concat
(extract 7 7 (:imm imm))
(concat (concat (bvnot (extract 6 6 (:imm imm))) (replicate (extract 6 6 (:imm imm)) 5)) (extract 5 4 (:imm imm)))
)
(concat (extract 3 0 (:imm imm)) #b0000000000000000000)
)
)
)
)
)
)
(require (match size ((Size64) true) ((Size32) true)))
)