Skip to content

Cranelift verifier: run in CI, using an SMT query caching setup. #13929

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
cfallin wants to merge 12 commits into
base: main
Choose a base branch
from
+1,663 −10
Open

Cranelift verifier: run in CI, using an SMT query caching setup. #13929

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
a2b68b0
veri-isle verifier: add SMT query cache.
cfallin Jul 21, 2026
afbed88
Add SMT cache for aarch64-fast verification.
cfallin Jul 21, 2026
24476f9
Add SMT cache entries for aarch64 and x64-iadd-base-case.
cfallin Jul 21, 2026
987c70c
Add to CI, and add a better error message.
cfallin Jul 21, 2026
5cbfb8f
clippy cleanups.
cfallin Jul 22, 2026
c5543a2
Refactoring (review feedback):
cfallin Jul 22, 2026
efd2fbd
Review feedback: refactor to a simpler cache format.
cfallin Jul 23, 2026
a4441fb
Update cache.
cfallin Jul 23, 2026
0657306
Delete in-tree cache.
cfallin Jul 23, 2026
17b197f
Rework to layer caching on top of easy-smt in an API-compatible layer…
cfallin Jul 23, 2026
112ed15
rustfmt
cfallin Jul 23, 2026
04c5997
fix tests
cfallin Jul 23, 2026
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
2 changes: 2 additions & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,3 +35,5 @@ testcase*.json
perf.data*
miri-wast/
report/
# Local SMT query cache for the ISLE verifier (see cranelift/isle/veri/verify.sh).
cranelift/isle/veri/cache/
13 changes: 13 additions & 0 deletions Cargo.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -186,6 +186,7 @@ members = [
"cranelift/isle/islec",
"cranelift/isle/veri/aslp",
"cranelift/isle/veri/isaspec",
"cranelift/isle/veri/caching",
"cranelift/isle/veri/test-macros",
"cranelift/isle/veri/veri",
"cranelift/serde",
Expand Down
16 changes: 16 additions & 0 deletions cranelift/isle/veri/caching/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
[package]
name = "cranelift-isle-veri-caching"
version = "0.1.0"
edition.workspace = true
publish = false
description = "Transparent caching layer over easy-smt for the ISLE verifier"

[dependencies]
easy-smt = "0.3.2"
log = { workspace = true }
serde = { workspace = true, features = ['derive'] }
serde_json = { workspace = true }
sha2 = "0.10"

[dev-dependencies]
tempfile = { workspace = true }
Loading
Loading