Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly
Appearance settings

Cranelift: VeriISLE: type check terms in isolation, fix over-constraints #13998

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
avanhatt wants to merge 1 commit into
base: main
Choose a base branch
Loading
from
Open

Cranelift: VeriISLE: type check terms in isolation, fix over-constraints #13998

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
76 changes: 19 additions & 57 deletions 76 cranelift/codegen/src/isa/aarch64/spec/mov_from_vec.isle
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,80 +7,42 @@
(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)))))
)
)
((Size64) (= rd (extract 63 0 (as rn (bv 64)))))
((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))))))
(=> (= idx #x00) (= rd (zero_ext 64 (extract 31 0 (as rn (bv 64))))))
(=> (= idx #x01) (= rd (zero_ext 64 (extract 63 32 (as rn (bv 64))))))
)
)
((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))))))
(=> (= idx #x00) (= rd (zero_ext 64 (extract 15 0 (as rn (bv 64))))))
(=> (= idx #x01) (= rd (zero_ext 64 (extract 31 16 (as rn (bv 64))))))
(=> (= idx #x02) (= rd (zero_ext 64 (extract 47 32 (as rn (bv 64))))))
(=> (= idx #x03) (= rd (zero_ext 64 (extract 63 48 (as rn (bv 64))))))
)
)
((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))))))
(=> (= idx #x00) (= rd (zero_ext 64 (extract 7 0 (as rn (bv 64))))))
(=> (= idx #x01) (= rd (zero_ext 64 (extract 15 8 (as rn (bv 64))))))
(=> (= idx #x02) (= rd (zero_ext 64 (extract 23 16 (as rn (bv 64))))))
(=> (= idx #x03) (= rd (zero_ext 64 (extract 31 24 (as rn (bv 64))))))
(=> (= idx #x04) (= rd (zero_ext 64 (extract 39 32 (as rn (bv 64))))))
(=> (= idx #x05) (= rd (zero_ext 64 (extract 47 40 (as rn (bv 64))))))
(=> (= idx #x06) (= rd (zero_ext 64 (extract 55 48 (as rn (bv 64))))))
(=> (= idx #x07) (= rd (zero_ext 64 (extract 63 56 (as rn (bv 64))))))
)
)
)
)
(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)
)
)
((Size64) (= idx #x00))
((Size32) (or (= idx #x00) (= idx #x01)))
((Size16) (or (= idx #x00) (= idx #x01) (= idx #x02) (= idx #x03)))
((Size8) (or (= idx #x00) (= idx #x01) (= idx #x02) (= idx #x03) (= idx #x04) (= idx #x05) (= idx #x06) (= idx #x07)))
)
)
)
3 changes: 2 additions & 1 deletion 3 cranelift/codegen/src/isa/x64/inst.isle
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -379,7 +379,8 @@

(spec (RegMemImm.Imm simm32) (provide
(= result
(bvor (bvshl #b10 62)(zero_ext 64 simm32)))))
(bvor
#x8000000000000000 (zero_ext 64 simm32)))))

(spec (RegMemImm.Mem addr) (provide
(= result
Expand Down
6 changes: 4 additions & 2 deletions 6 cranelift/codegen/src/prelude.isle
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -770,7 +770,9 @@

(spec (i64_neg x) (provide (= result (bvneg x))))
(spec (u64_sub x y) (provide (= result (bvsub x y))))
(spec (u64_shl x y) (provide (= result (bvshl x y))))
(spec (u64_shl x y)
(match (bvult y #x00000040))
(provide (= result (bvshl x (zero_ext 64 y)))))
(spec (u64_eq x y) (provide (= result (= x y))))
(spec (u64_is_odd x) (provide (= result (= (conv_to 1 x) #b1))))
(spec (i64_checked_neg x)
Expand Down Expand Up @@ -801,7 +803,7 @@
(spec (u64_wrapping_shl x y)
(provide (= result
(bvshl x
(zero_ext 32 (bvand y #x0000003f)))))) ; shift by y mod 64
(zero_ext 64 (bvand y #x0000003f)))))) ; shift by y mod 64
(spec (u64_wrapping_sub x y) (provide (= result (bvsub x y))))
(spec (u64_wrapping_add x y) (provide (= result (bvadd x y))))
(spec (u64_gt x y) (provide (bvugt x y)))
Expand Down
14 changes: 12 additions & 2 deletions 14 cranelift/isle/veri/isaspec/src/instructions.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2076,9 +2076,18 @@ fn define_mov_from_vec() -> SpecConfig {
aarch64::gpreg(4),
Mapping::require(spec_var("rd".to_string())),
);
// The source is a 128-bit vector register, but the ISLE `rn` field is
// declared `Reg`, which is modelled as `(bv 64)`. Qualifying it as 128 bits
// contradicts that model, so the spec cannot be type checked; widening it
// instead would need a distinct vector register type, as x64 has for `Xmm`.
//
// Until then this specification covers only the lanes lying within the low
// 64 bits of the register. That is incomplete rather than unsound: reads of
// a higher lane are excluded by the `require` clause, so a lowering that
// needs one will fail to verify.
mappings.reads.insert(
aarch64::vreg(5),
Mapping::require(spec_as_bit_vector_width(spec_var("rn".to_string()), 128)),
Mapping::require(spec_as_bit_vector_width(spec_var("rn".to_string()), 64)),
);

SpecConfig {
Expand All @@ -2091,7 +2100,8 @@ fn define_mov_from_vec() -> SpecConfig {
.iter()
.rev()
.map(|size| {
let lanes = 128 / size.ty().bits();
// Lanes within the low 64 bits only; see above.
let lanes = 64 / size.ty().bits();
Arm {
variant: format!("{size:?}"),
args: Vec::new(),
Expand Down
29 changes: 29 additions & 0 deletions 29 cranelift/isle/veri/veri/filetests/spec_conflict/mismatched_shift_width.isle
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
; Regression test for silently unverified expansions.
;
; The spec below is ill-typed: type inference rejects every candidate
; instantiation, so no query ever reaches the solver.

; 8-bit value type
(type Value (primitive Value))
(model Value (type (bv 8)))

; Top-level test term asserts equality
(decl test (Value) Value)
(spec (test arg) (provide (= result arg)))

; Shift left.
(decl shl (Value Value) Value)
(extern extractor shl shl)
(spec (shl x y) (provide (= result (bvshl x y))))

; Shift left, with the amount widened first.
;
; The width operand of `zero_ext` is the *result* width, so the shift amount
; here is 16 bits wide, while `bvshl` requires it to match the 8-bit value being
; shifted. Both are bit vectors, so this is a width conflict between compatible
; types: type inference reports it as inapplicable rather than a type error.
(decl shl_ext (Value Value) Value)
(extern constructor shl_ext shl_ext)
(spec (shl_ext x y) (provide (= result (bvshl x (zero_ext 16 y)))))

(rule test (test (shl x y)) (shl_ext x y))
1 change: 1 addition & 0 deletions 1 cranelift/isle/veri/veri/src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ pub mod reachability;
pub mod runner;
pub mod solver;
pub mod spec;
pub mod spec_check;
pub mod trie;
pub mod type_inference;
pub mod types;
Expand Down
Loading
Loading
Morty Proxy This is a proxified and sanitized view of the page, visit original site.