cranelift-codegen 0.134.0

Low-level code generator library
Documentation 
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

;; GENERATED BY `isaspec`. DO NOT EDIT!!!

(attr MInst.MovFromVec (tag isaspec_generated))

(spec
    (MInst.MovFromVec rd rn idx size)
    (provide
        (match
            size
            ((Size64)
                (and
                    (=> (= idx #x00) (= rd (extract 63 0 (as rn (bv 128)))))
                    (=> (= idx #x01) (= rd (extract 127 64 (as rn (bv 128)))))
                )
            )
            ((Size32)
                (and
                    (=> (= idx #x00) (= rd (zero_ext 64 (extract 31 0 (as rn (bv 128))))))
                    (=> (= idx #x01) (= rd (zero_ext 64 (extract 63 32 (as rn (bv 128))))))
                    (=> (= idx #x02) (= rd (zero_ext 64 (extract 95 64 (as rn (bv 128))))))
                    (=> (= idx #x03) (= rd (zero_ext 64 (extract 127 96 (as rn (bv 128))))))
                )
            )
            ((Size16)
                (and
                    (=> (= idx #x00) (= rd (zero_ext 64 (extract 15 0 (as rn (bv 128))))))
                    (=> (= idx #x01) (= rd (zero_ext 64 (extract 31 16 (as rn (bv 128))))))
                    (=> (= idx #x02) (= rd (zero_ext 64 (extract 47 32 (as rn (bv 128))))))
                    (=> (= idx #x03) (= rd (zero_ext 64 (extract 63 48 (as rn (bv 128))))))
                    (=> (= idx #x04) (= rd (zero_ext 64 (extract 79 64 (as rn (bv 128))))))
                    (=> (= idx #x05) (= rd (zero_ext 64 (extract 95 80 (as rn (bv 128))))))
                    (=> (= idx #x06) (= rd (zero_ext 64 (extract 111 96 (as rn (bv 128))))))
                    (=> (= idx #x07) (= rd (zero_ext 64 (extract 127 112 (as rn (bv 128))))))
                )
            )
            ((Size8)
                (and
                    (=> (= idx #x00) (= rd (zero_ext 64 (extract 7 0 (as rn (bv 128))))))
                    (=> (= idx #x01) (= rd (zero_ext 64 (extract 15 8 (as rn (bv 128))))))
                    (=> (= idx #x02) (= rd (zero_ext 64 (extract 23 16 (as rn (bv 128))))))
                    (=> (= idx #x03) (= rd (zero_ext 64 (extract 31 24 (as rn (bv 128))))))
                    (=> (= idx #x04) (= rd (zero_ext 64 (extract 39 32 (as rn (bv 128))))))
                    (=> (= idx #x05) (= rd (zero_ext 64 (extract 47 40 (as rn (bv 128))))))
                    (=> (= idx #x06) (= rd (zero_ext 64 (extract 55 48 (as rn (bv 128))))))
                    (=> (= idx #x07) (= rd (zero_ext 64 (extract 63 56 (as rn (bv 128))))))
                    (=> (= idx #x08) (= rd (zero_ext 64 (extract 71 64 (as rn (bv 128))))))
                    (=> (= idx #x09) (= rd (zero_ext 64 (extract 79 72 (as rn (bv 128))))))
                    (=> (= idx #x0a) (= rd (zero_ext 64 (extract 87 80 (as rn (bv 128))))))
                    (=> (= idx #x0b) (= rd (zero_ext 64 (extract 95 88 (as rn (bv 128))))))
                    (=> (= idx #x0c) (= rd (zero_ext 64 (extract 103 96 (as rn (bv 128))))))
                    (=> (= idx #x0d) (= rd (zero_ext 64 (extract 111 104 (as rn (bv 128))))))
                    (=> (= idx #x0e) (= rd (zero_ext 64 (extract 119 112 (as rn (bv 128))))))
                    (=> (= idx #x0f) (= rd (zero_ext 64 (extract 127 120 (as rn (bv 128))))))
                )
            )
        )
    )
    (require
        (match
            size
            ((Size64) (or (= idx #x00) (= idx #x01)))
            ((Size32) (or (= idx #x00) (= idx #x01) (= idx #x02) (= idx #x03)))
            ((Size16) (or (= idx #x00) (= idx #x01) (= idx #x02) (= idx #x03) (= idx #x04) (= idx #x05) (= idx #x06) (= idx #x07)))
            ((Size8)
                (or
                    (= idx #x00)
                    (= idx #x01)
                    (= idx #x02)
                    (= idx #x03)
                    (= idx #x04)
                    (= idx #x05)
                    (= idx #x06)
                    (= idx #x07)
                    (= idx #x08)
                    (= idx #x09)
                    (= idx #x0a)
                    (= idx #x0b)
                    (= idx #x0c)
                    (= idx #x0d)
                    (= idx #x0e)
                    (= idx #x0f)
                )
            )
        )
    )
)