Skip to content

Commit 9bdbd42

Browse files
avanhattavanhatt
authored
Type check term specs in isolation, and fix the over-constrained specs it finds. (#13998)
Adds a check that builds verification conditions for one term at a time, against nothing but its own declared types, so that a genuine type conflict is distinct from an expansion that shouldn't be reached for a specific type. Fixes the conflicts it reports.
1 parent 6d8e923 commit 9bdbd42

11 files changed

Lines changed: 560 additions & 101 deletions

File tree

‎cranelift/codegen/src/isa/aarch64/spec/mov_from_vec.isle‎

Lines changed: 19 additions & 57 deletions
Original file line numberDiff line numberDiff line change
@@ -7,80 +7,42 @@
77
(provide
88
(match
99
size
10-
((Size64)
11-
(and
12-
(=> (= idx #x00) (= rd (extract 63 0 (as rn (bv 128)))))
13-
(=> (= idx #x01) (= rd (extract 127 64 (as rn (bv 128)))))
14-
)
15-
)
10+
((Size64) (= rd (extract 63 0 (as rn (bv 64)))))
1611
((Size32)
1712
(and
18-
(=> (= idx #x00) (= rd (zero_ext 64 (extract 31 0 (as rn (bv 128))))))
19-
(=> (= idx #x01) (= rd (zero_ext 64 (extract 63 32 (as rn (bv 128))))))
20-
(=> (= idx #x02) (= rd (zero_ext 64 (extract 95 64 (as rn (bv 128))))))
21-
(=> (= idx #x03) (= rd (zero_ext 64 (extract 127 96 (as rn (bv 128))))))
13+
(=> (= idx #x00) (= rd (zero_ext 64 (extract 31 0 (as rn (bv 64))))))
14+
(=> (= idx #x01) (= rd (zero_ext 64 (extract 63 32 (as rn (bv 64))))))
2215
)
2316
)
2417
((Size16)
2518
(and
26-
(=> (= idx #x00) (= rd (zero_ext 64 (extract 15 0 (as rn (bv 128))))))
27-
(=> (= idx #x01) (= rd (zero_ext 64 (extract 31 16 (as rn (bv 128))))))
28-
(=> (= idx #x02) (= rd (zero_ext 64 (extract 47 32 (as rn (bv 128))))))
29-
(=> (= idx #x03) (= rd (zero_ext 64 (extract 63 48 (as rn (bv 128))))))
30-
(=> (= idx #x04) (= rd (zero_ext 64 (extract 79 64 (as rn (bv 128))))))
31-
(=> (= idx #x05) (= rd (zero_ext 64 (extract 95 80 (as rn (bv 128))))))
32-
(=> (= idx #x06) (= rd (zero_ext 64 (extract 111 96 (as rn (bv 128))))))
33-
(=> (= idx #x07) (= rd (zero_ext 64 (extract 127 112 (as rn (bv 128))))))
19+
(=> (= idx #x00) (= rd (zero_ext 64 (extract 15 0 (as rn (bv 64))))))
20+
(=> (= idx #x01) (= rd (zero_ext 64 (extract 31 16 (as rn (bv 64))))))
21+
(=> (= idx #x02) (= rd (zero_ext 64 (extract 47 32 (as rn (bv 64))))))
22+
(=> (= idx #x03) (= rd (zero_ext 64 (extract 63 48 (as rn (bv 64))))))
3423
)
3524
)
3625
((Size8)
3726
(and
38-
(=> (= idx #x00) (= rd (zero_ext 64 (extract 7 0 (as rn (bv 128))))))
39-
(=> (= idx #x01) (= rd (zero_ext 64 (extract 15 8 (as rn (bv 128))))))
40-
(=> (= idx #x02) (= rd (zero_ext 64 (extract 23 16 (as rn (bv 128))))))
41-
(=> (= idx #x03) (= rd (zero_ext 64 (extract 31 24 (as rn (bv 128))))))
42-
(=> (= idx #x04) (= rd (zero_ext 64 (extract 39 32 (as rn (bv 128))))))
43-
(=> (= idx #x05) (= rd (zero_ext 64 (extract 47 40 (as rn (bv 128))))))
44-
(=> (= idx #x06) (= rd (zero_ext 64 (extract 55 48 (as rn (bv 128))))))
45-
(=> (= idx #x07) (= rd (zero_ext 64 (extract 63 56 (as rn (bv 128))))))
46-
(=> (= idx #x08) (= rd (zero_ext 64 (extract 71 64 (as rn (bv 128))))))
47-
(=> (= idx #x09) (= rd (zero_ext 64 (extract 79 72 (as rn (bv 128))))))
48-
(=> (= idx #x0a) (= rd (zero_ext 64 (extract 87 80 (as rn (bv 128))))))
49-
(=> (= idx #x0b) (= rd (zero_ext 64 (extract 95 88 (as rn (bv 128))))))
50-
(=> (= idx #x0c) (= rd (zero_ext 64 (extract 103 96 (as rn (bv 128))))))
51-
(=> (= idx #x0d) (= rd (zero_ext 64 (extract 111 104 (as rn (bv 128))))))
52-
(=> (= idx #x0e) (= rd (zero_ext 64 (extract 119 112 (as rn (bv 128))))))
53-
(=> (= idx #x0f) (= rd (zero_ext 64 (extract 127 120 (as rn (bv 128))))))
27+
(=> (= idx #x00) (= rd (zero_ext 64 (extract 7 0 (as rn (bv 64))))))
28+
(=> (= idx #x01) (= rd (zero_ext 64 (extract 15 8 (as rn (bv 64))))))
29+
(=> (= idx #x02) (= rd (zero_ext 64 (extract 23 16 (as rn (bv 64))))))
30+
(=> (= idx #x03) (= rd (zero_ext 64 (extract 31 24 (as rn (bv 64))))))
31+
(=> (= idx #x04) (= rd (zero_ext 64 (extract 39 32 (as rn (bv 64))))))
32+
(=> (= idx #x05) (= rd (zero_ext 64 (extract 47 40 (as rn (bv 64))))))
33+
(=> (= idx #x06) (= rd (zero_ext 64 (extract 55 48 (as rn (bv 64))))))
34+
(=> (= idx #x07) (= rd (zero_ext 64 (extract 63 56 (as rn (bv 64))))))
5435
)
5536
)
5637
)
5738
)
5839
(require
5940
(match
6041
size
61-
((Size64) (or (= idx #x00) (= idx #x01)))
62-
((Size32) (or (= idx #x00) (= idx #x01) (= idx #x02) (= idx #x03)))
63-
((Size16) (or (= idx #x00) (= idx #x01) (= idx #x02) (= idx #x03) (= idx #x04) (= idx #x05) (= idx #x06) (= idx #x07)))
64-
((Size8)
65-
(or
66-
(= idx #x00)
67-
(= idx #x01)
68-
(= idx #x02)
69-
(= idx #x03)
70-
(= idx #x04)
71-
(= idx #x05)
72-
(= idx #x06)
73-
(= idx #x07)
74-
(= idx #x08)
75-
(= idx #x09)
76-
(= idx #x0a)
77-
(= idx #x0b)
78-
(= idx #x0c)
79-
(= idx #x0d)
80-
(= idx #x0e)
81-
(= idx #x0f)
82-
)
83-
)
42+
((Size64) (= idx #x00))
43+
((Size32) (or (= idx #x00) (= idx #x01)))
44+
((Size16) (or (= idx #x00) (= idx #x01) (= idx #x02) (= idx #x03)))
45+
((Size8) (or (= idx #x00) (= idx #x01) (= idx #x02) (= idx #x03) (= idx #x04) (= idx #x05) (= idx #x06) (= idx #x07)))
8446
)
8547
)
8648
)

‎cranelift/codegen/src/isa/x64/inst.isle‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -379,7 +379,8 @@
379379

380380
(spec (RegMemImm.Imm simm32) (provide
381381
(= result
382-
(bvor (bvshl #b10 62)(zero_ext 64 simm32)))))
382+
(bvor
383+
#x8000000000000000 (zero_ext 64 simm32)))))
383384

384385
(spec (RegMemImm.Mem addr) (provide
385386
(= result

‎cranelift/codegen/src/prelude.isle‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -770,7 +770,9 @@
770770

771771
(spec (i64_neg x) (provide (= result (bvneg x))))
772772
(spec (u64_sub x y) (provide (= result (bvsub x y))))
773-
(spec (u64_shl x y) (provide (= result (bvshl x y))))
773+
(spec (u64_shl x y)
774+
(match (bvult y #x00000040))
775+
(provide (= result (bvshl x (zero_ext 64 y)))))
774776
(spec (u64_eq x y) (provide (= result (= x y))))
775777
(spec (u64_is_odd x) (provide (= result (= (conv_to 1 x) #b1))))
776778
(spec (i64_checked_neg x)
@@ -801,7 +803,7 @@
801803
(spec (u64_wrapping_shl x y)
802804
(provide (= result
803805
(bvshl x
804-
(zero_ext 32 (bvand y #x0000003f)))))) ; shift by y mod 64
806+
(zero_ext 64 (bvand y #x0000003f)))))) ; shift by y mod 64
805807
(spec (u64_wrapping_sub x y) (provide (= result (bvsub x y))))
806808
(spec (u64_wrapping_add x y) (provide (= result (bvadd x y))))
807809
(spec (u64_gt x y) (provide (bvugt x y)))

‎cranelift/isle/veri/isaspec/src/instructions.rs‎

Lines changed: 12 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2076,9 +2076,18 @@ fn define_mov_from_vec() -> SpecConfig {
20762076
aarch64::gpreg(4),
20772077
Mapping::require(spec_var("rd".to_string())),
20782078
);
2079+
// The source is a 128-bit vector register, but the ISLE `rn` field is
2080+
// declared `Reg`, which is modelled as `(bv 64)`. Qualifying it as 128 bits
2081+
// contradicts that model, so the spec cannot be type checked; widening it
2082+
// instead would need a distinct vector register type, as x64 has for `Xmm`.
2083+
//
2084+
// Until then this specification covers only the lanes lying within the low
2085+
// 64 bits of the register. That is incomplete rather than unsound: reads of
2086+
// a higher lane are excluded by the `require` clause, so a lowering that
2087+
// needs one will fail to verify.
20792088
mappings.reads.insert(
20802089
aarch64::vreg(5),
2081-
Mapping::require(spec_as_bit_vector_width(spec_var("rn".to_string()), 128)),
2090+
Mapping::require(spec_as_bit_vector_width(spec_var("rn".to_string()), 64)),
20822091
);
20832092

20842093
SpecConfig {
@@ -2091,7 +2100,8 @@ fn define_mov_from_vec() -> SpecConfig {
20912100
.iter()
20922101
.rev()
20932102
.map(|size| {
2094-
let lanes = 128 / size.ty().bits();
2103+
// Lanes within the low 64 bits only; see above.
2104+
let lanes = 64 / size.ty().bits();
20952105
Arm {
20962106
variant: format!("{size:?}"),
20972107
args: Vec::new(),

‎cranelift/isle/veri/veri/filetests/spec_conflict/mismatched_shift_width.isle‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
; Regression test for silently unverified expansions.
2+
;
3+
; The spec below is ill-typed: type inference rejects every candidate
4+
; instantiation, so no query ever reaches the solver.
5+
6+
; 8-bit value type
7+
(type Value (primitive Value))
8+
(model Value (type (bv 8)))
9+
10+
; Top-level test term asserts equality
11+
(decl test (Value) Value)
12+
(spec (test arg) (provide (= result arg)))
13+
14+
; Shift left.
15+
(decl shl (Value Value) Value)
16+
(extern extractor shl shl)
17+
(spec (shl x y) (provide (= result (bvshl x y))))
18+
19+
; Shift left, with the amount widened first.
20+
;
21+
; The width operand of `zero_ext` is the *result* width, so the shift amount
22+
; here is 16 bits wide, while `bvshl` requires it to match the 8-bit value being
23+
; shifted. Both are bit vectors, so this is a width conflict between compatible
24+
; types: type inference reports it as inapplicable rather than a type error.
25+
(decl shl_ext (Value Value) Value)
26+
(extern constructor shl_ext shl_ext)
27+
(spec (shl_ext x y) (provide (= result (bvshl x (zero_ext 16 y)))))
28+
29+
(rule test (test (shl x y)) (shl_ext x y))

‎cranelift/isle/veri/veri/src/lib.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ pub mod reachability;
2525
pub mod runner;
2626
pub mod solver;
2727
pub mod spec;
28+
pub mod spec_check;
2829
pub mod trie;
2930
pub mod type_inference;
3031
pub mod types;

0 commit comments

Comments
 (0)