T0b1/wasmtime
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

peepmatic: update z3 dependency to version 0.7.0

Browse Source
This commit is contained in:
Nick Fitzgerald
2020-10-29 10:58:05 -07:00
parent b73b831892
commit 5a09e47e38
3 changed files with 13 additions and 13 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
Cargo.lock generated
View File

@@ -2791,9 +2791,9 @@ dependencies = [
[[package]] [[package]]
name = "z3" name = "z3"
version = "0.6.0" version = "0.7.0"
source = "registry+https://github.com/rust-lang/crates.io-index" source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "f0354c65dfe00e08c4ab30581732906874f97156f424bfb390cf0cca2cb6ac29" checksum = "dbb8ef9d11f50b64327c8a5906b53d3f7f792cb0e849909d476ac0aa16117d61"
dependencies = [ dependencies = [
"lazy_static", "lazy_static",
"log", "log",
@@ -2802,9 +2802,9 @@ dependencies = [
[[package]] [[package]]
name = "z3-sys" name = "z3-sys"
version = "0.6.2" version = "0.6.3"
source = "registry+https://github.com/rust-lang/crates.io-index" source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e1863cafae8eb86dd7d69c9218421b288594e8836346e93d4f36ade427195a21" checksum = "afa18ba5fbd4933e41ffb440c3fd91f91fe9cdb7310cce3ddfb6648563811de0"
dependencies = [ dependencies = [
"cmake", "cmake",
] ]

2
cranelift/peepmatic/Cargo.toml
View File

@@ -16,7 +16,7 @@ peepmatic-runtime = { version = "0.67.0", path = "crates/runtime", features = ["
peepmatic-traits = { version = "0.67.0", path = "crates/traits" } peepmatic-traits = { version = "0.67.0", path = "crates/traits" }
serde = { version = "1.0.105", features = ["derive"] } serde = { version = "1.0.105", features = ["derive"] }
wast = "25.0.0" wast = "25.0.0"
z3 = { version = "0.6.0", features = ["static-link-z3"] } z3 = { version = "0.7.0", features = ["static-link-z3"] }
[dev-dependencies] [dev-dependencies]
peepmatic-test-operator = { version = "0.67.0", path = "crates/test-operator" } peepmatic-test-operator = { version = "0.67.0", path = "crates/test-operator" }

16
cranelift/peepmatic/src/verify.rs
View File

@@ -237,13 +237,13 @@ struct TypingContext<'a, TOperator> {
impl<'a, TOperator> TypingContext<'a, TOperator> { impl<'a, TOperator> TypingContext<'a, TOperator> {
fn new(z3: &'a z3::Context) -> Self { fn new(z3: &'a z3::Context) -> Self {
let type_kind_sort = z3::DatatypeBuilder::new(z3) let type_kind_sort = z3::DatatypeBuilder::new(z3, "TypeKind")
.variant("int", &[]) .variant("int", vec![])
.variant("bool", &[]) .variant("bool", vec![])
.variant("cpu_flags", &[]) .variant("cpu_flags", vec![])
.variant("cc", &[]) .variant("cc", vec![])
.variant("void", &[]) .variant("void", vec![])
.finish("TypeKind"); .finish();
TypingContext { TypingContext {
z3, z3,
solver: z3::Solver::new(z3), solver: z3::Solver::new(z3),
@@ -576,7 +576,7 @@ impl<'a, TOperator> TypingContext<'a, TOperator> {
// Check if there is more than one satisfying assignment to // Check if there is more than one satisfying assignment to
// `ty_var`'s width variable. If so, then it must be polymorphic. If // `ty_var`'s width variable. If so, then it must be polymorphic. If
// not, then it must have a fixed value. // not, then it must have a fixed value.
let model = self.solver.get_model(); let model = self.solver.get_model().unwrap();
let width_var = model.eval(&ty_var.width).unwrap(); let width_var = model.eval(&ty_var.width).unwrap();
let bit_width: u8 = width_var.as_u64().unwrap().try_into().unwrap(); let bit_width: u8 = width_var.as_u64().unwrap().try_into().unwrap();