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

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

(attr MInst.Extend (tag isaspec_generated))

(spec
    (MInst.Extend rd rn signed from_bits to_bits)
    (provide
        (=> (and (not signed) (= from_bits #x08) (= to_bits #x08)) (= rd (zero_ext 64 (extract 7 0 (as rn (bv 64))))))
        (=> (and signed (= from_bits #x08) (= to_bits #x08)) (= rd (zero_ext 64 (sign_ext 32 (extract 7 0 (as rn (bv 64)))))))
        (=> (and (not signed) (= from_bits #x08) (= to_bits #x10)) (= rd (zero_ext 64 (extract 7 0 (as rn (bv 64))))))
        (=> (and signed (= from_bits #x08) (= to_bits #x10)) (= rd (zero_ext 64 (sign_ext 32 (extract 7 0 (as rn (bv 64)))))))
        (=> (and (not signed) (= from_bits #x08) (= to_bits #x20)) (= rd (zero_ext 64 (extract 7 0 (as rn (bv 64))))))
        (=> (and signed (= from_bits #x08) (= to_bits #x20)) (= rd (zero_ext 64 (sign_ext 32 (extract 7 0 (as rn (bv 64)))))))
        (=> (and (not signed) (= from_bits #x08) (= to_bits #x40)) (= rd (zero_ext 64 (extract 7 0 (as rn (bv 64))))))
        (=> (and signed (= from_bits #x08) (= to_bits #x40)) (= rd (sign_ext 64 (extract 7 0 (as rn (bv 64))))))
        (=> (and (not signed) (= from_bits #x10) (= to_bits #x10)) (= rd (zero_ext 64 (extract 15 0 (as rn (bv 64))))))
        (=> (and signed (= from_bits #x10) (= to_bits #x10)) (= rd (zero_ext 64 (sign_ext 32 (extract 15 0 (as rn (bv 64)))))))
        (=> (and (not signed) (= from_bits #x10) (= to_bits #x20)) (= rd (zero_ext 64 (extract 15 0 (as rn (bv 64))))))
        (=> (and signed (= from_bits #x10) (= to_bits #x20)) (= rd (zero_ext 64 (sign_ext 32 (extract 15 0 (as rn (bv 64)))))))
        (=> (and (not signed) (= from_bits #x10) (= to_bits #x40)) (= rd (zero_ext 64 (extract 15 0 (as rn (bv 64))))))
        (=> (and signed (= from_bits #x10) (= to_bits #x40)) (= rd (sign_ext 64 (extract 15 0 (as rn (bv 64))))))
        (=> (and (not signed) (= from_bits #x20) (= to_bits #x20)) (= rd (zero_ext 64 (extract 31 0 (as rn (bv 64))))))
        (=> (and signed (= from_bits #x20) (= to_bits #x20)) (= rd (zero_ext 64 (extract 31 0 (as rn (bv 64))))))
        (=> (and (not signed) (= from_bits #x20) (= to_bits #x40)) (= rd (zero_ext 64 (extract 31 0 (as rn (bv 64))))))
        (=> (and signed (= from_bits #x20) (= to_bits #x40)) (= rd (sign_ext 64 (extract 31 0 (as rn (bv 64))))))
    )
    (require
        (or
            (and (not signed) (= from_bits #x08) (= to_bits #x08))
            (and signed (= from_bits #x08) (= to_bits #x08))
            (and (not signed) (= from_bits #x08) (= to_bits #x10))
            (and signed (= from_bits #x08) (= to_bits #x10))
            (and (not signed) (= from_bits #x08) (= to_bits #x20))
            (and signed (= from_bits #x08) (= to_bits #x20))
            (and (not signed) (= from_bits #x08) (= to_bits #x40))
            (and signed (= from_bits #x08) (= to_bits #x40))
            (and (not signed) (= from_bits #x10) (= to_bits #x10))
            (and signed (= from_bits #x10) (= to_bits #x10))
            (and (not signed) (= from_bits #x10) (= to_bits #x20))
            (and signed (= from_bits #x10) (= to_bits #x20))
            (and (not signed) (= from_bits #x10) (= to_bits #x40))
            (and signed (= from_bits #x10) (= to_bits #x40))
            (and (not signed) (= from_bits #x20) (= to_bits #x20))
            (and signed (= from_bits #x20) (= to_bits #x20))
            (and (not signed) (= from_bits #x20) (= to_bits #x40))
            (and signed (= from_bits #x20) (= to_bits #x40))
        )
    )
)