From 40bff4dc1dbe50874e380d02c75ed81cc0a95250 Mon Sep 17 00:00:00 2001 From: hermanventer Date: Sun, 22 Oct 2023 16:26:23 -0700 Subject: [PATCH] Make simplification with TOP more aggressive --- .github/workflows/rust.yml | 83 +++++----------------------- Cargo.lock | 57 ++++++++----------- binaries/summary_store.tar | Bin 2999296 -> 2991104 bytes checker/Cargo.toml | 2 +- checker/src/abstract_value.rs | 6 +- checker/src/body_visitor.rs | 3 +- checker/src/path.rs | 7 +++ checker/src/type_visitor.rs | 1 + checker/tests/run-pass/transmute.rs | 2 +- 9 files changed, 52 insertions(+), 109 deletions(-) diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml index 3eba341f..a04f9222 100644 --- a/.github/workflows/rust.yml +++ b/.github/workflows/rust.yml @@ -7,82 +7,25 @@ on: branches: [ main ] jobs: - clippy: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v3.5.2 - - - name: Run Clippy - run: | - cargo clippy --no-default-features --all-targets -- -D warnings - - tests: - runs-on: macos-latest - - steps: - - uses: actions/checkout@v3.5.2 - - - name: Execute tests - run: | - cargo test --all -- --test-threads=1 - env: - CARGO_INCREMENTAL: 0 - RUSTFLAGS: "-Zprofile -Ccodegen-units=1 -Copt-level=0 -Clink-dead-code -Coverflow-checks=off -Zpanic_abort_tests" - - - name: Setup grcov - run: | - cargo install grcov - - - name: Run grcov - run: | - zip -0 cov.zip $(find . -name "mirai*.gc*" -print) - grcov cov.zip -s . -t lcov --llvm --ignore-not-existing --ignore "/*" -o lcov.info - - - name: Upload coverage data to codecov.io - uses: codecov/codecov-action@v3 - with: - token: ${{ secrets.CODECOV_TOKEN }} - files: "lcov.info" - - mirai_on_mirai_macos: - runs-on: macos-latest - - steps: - - uses: actions/checkout@v3.5.2 - - - name: Install MIRAI - run: | - cargo install --force --path ./checker --no-default-features - - - name: Run MIRAI on MIRAI - run: | - cargo mirai --no-default-features - - mirai_on_mirai_ubuntu: - runs-on: ubuntu-latest - - steps: - - uses: actions/checkout@v3.5.2 - - - name: Install MIRAI - run: | - cargo install --force --path ./checker - - - name: Run MIRAI on MIRAI - run: | - cargo mirai --no-default-features - mirai_on_mirai_windows: runs-on: windows-latest steps: - uses: actions/checkout@v3.5.2 + - uses: lukka/get-cmake@latest + - name: List $RUNNER_WORKSPACE before vcpkg is setup + run: find $RUNNER_WORKSPACE + shell: bash + + - name: Setup vcpkg + uses: lukka/run-vcpkg@main + id: runvcpkg + with: + # This one is not needed, as it is the default value anyway. + # vcpkgDirectory: '${{ github.workspace }}/vcpkg' + vcpkgJsonGlob: '**/cmakepresets/vcpkg.json' + vcpkgCommitId: 'c9f906558f9bb12ee9811d6edc98ec9255c6cda5' - name: Install MIRAI run: | cargo install --force --path ./checker - - - name: Run MIRAI on MIRAI - run: | - cargo mirai --no-default-features - diff --git a/Cargo.lock b/Cargo.lock index 437233f3..f1fa55e9 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -153,15 +153,6 @@ dependencies = [ "thiserror", ] -[[package]] -name = "cc" -version = "1.0.83" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f1174fb0b6ec23863f8b971027804a42614e347eafb0a95bf0b12cdae21fc4d0" -dependencies = [ - "libc", -] - [[package]] name = "cexpr" version = "0.6.0" @@ -215,15 +206,6 @@ version = "0.5.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "cd7cc57abe963c6d3b9d8be5b06ba7c8957a930305ca90304f24ef040aa6f961" -[[package]] -name = "cmake" -version = "0.1.50" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a31c789563b815f77f4250caee12365734369f942439b7defd71e18a48197130" -dependencies = [ - "cc", -] - [[package]] name = "colorchoice" version = "1.0.0" @@ -421,9 +403,9 @@ checksum = "d2fabcfbdc87f4758337ca535fb41a6d701b65693ce38287d856d1674551ec9b" [[package]] name = "hashbrown" -version = "0.14.1" +version = "0.14.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7dfda62a12f55daeae5015f81b0baea145391cb4520f86c248fc615d72640d12" +checksum = "f93e7192158dbcda357bdec5fb5788eebf8bbac027f3f33e719d29135ae84156" [[package]] name = "hermit-abi" @@ -524,9 +506,9 @@ checksum = "da2479e8c062e40bf0066ffa0bc823de0a9368974af99c9f6df941d2c231e03f" [[package]] name = "lock_api" -version = "0.4.10" +version = "0.4.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c1cc9717a20b1bb222f333e6a92fd32f7d8a18ddc5a3191a11af45dcbf4dcd16" +checksum = "3c168f8615b12bc01f9c17e2eb0cc07dcae1940121185446edc3744920e8ef45" dependencies = [ "autocfg", "scopeguard", @@ -758,9 +740,9 @@ dependencies = [ [[package]] name = "regex" -version = "1.10.1" +version = "1.10.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "aaac441002f822bc9705a681810a4dd2963094b9ca0ddc41cb963a4c189189ea" +checksum = "380b951a9c5e80ddfd6136919eef32310721aa4aacd4889a8d39124b026ab343" dependencies = [ "aho-corasick", "memchr", @@ -770,9 +752,9 @@ dependencies = [ [[package]] name = "regex-automata" -version = "0.4.2" +version = "0.4.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5011c7e263a695dc8ca064cddb722af1be54e517a280b12a5356f98366899e5d" +checksum = "5f804c7828047e88b2d32e2d7fe5a105da8ee3264f01902f796c8e067dc2483f" dependencies = [ "aho-corasick", "memchr", @@ -809,9 +791,9 @@ checksum = "8ba09476327c4b70ccefb6180f046ef588c26a24cf5d269a9feba316eb4f029f" [[package]] name = "rustix" -version = "0.38.19" +version = "0.38.20" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "745ecfa778e66b2b63c88a61cb36e0eea109e803b0b86bf9879fbc77c70e86ed" +checksum = "67ce50cb2e16c2903e30d1cbccfd8387a74b9d4c938b6a4c5ec6cc7556f7a8a0" dependencies = [ "bitflags 2.4.1", "errno", @@ -1016,18 +998,18 @@ dependencies = [ [[package]] name = "thiserror" -version = "1.0.49" +version = "1.0.50" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1177e8c6d7ede7afde3585fd2513e611227efd6481bd78d2e82ba1ce16557ed4" +checksum = "f9a7210f5c9a7156bb50aa36aed4c95afb51df0df00713949448cf9e97d382d2" dependencies = [ "thiserror-impl", ] [[package]] name = "thiserror-impl" -version = "1.0.49" +version = "1.0.50" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "10712f02019e9288794769fba95cd6847df9874d49d871d062172f9dd41bc4cc" +checksum = "266b2e40bc00e5a6c09c3584011e08b06f123c00362c92b975ba9843aaaa14b8" dependencies = [ "proc-macro2", "quote", @@ -1068,6 +1050,12 @@ version = "0.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "711b9620af191e0cdc7468a8d14e709c3dcdb115b36f838e601583af800a370a" +[[package]] +name = "vcpkg" +version = "0.2.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "accd4ea62f7bb7a82fe23066fb0957d48ef677f6eeb8215f372f52e48bb32426" + [[package]] name = "verification_status" version = "0.1.0" @@ -1200,9 +1188,8 @@ dependencies = [ [[package]] name = "z3-sys" version = "0.8.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d7cf70fdbc0de3f42b404f49b0d4686a82562254ea29ff0a155eef2f5430f4b0" +source = "git+https://github.com/prove-rs/z3.rs.git#d49d3564ceccdb887be62f32dd9d6c852b583dae" dependencies = [ "bindgen", - "cmake", + "vcpkg", ] diff --git a/binaries/summary_store.tar b/binaries/summary_store.tar index f0aa724ecb4f93ad397f1b96b86c27b685e9dedd..33538f78c06ceb4f3f5a96a6411b11fcc940980d 100644 GIT binary patch delta 342 zcmZ9|%TB^j5XNyw3l;?{rQT_6z2BO&wukcoz7ugLgas_zpox7D6T8u!3*W-<4(^YC zVj#pxe!DN5-ljv1yEqV6b`-Onkx%wYy z&jL9OI@JV{zlMSML-7U6Sb>EKs#t}M8rHCmIvUu3gH1Hyq6H6I*v1Zav4?#eppEIy z0EdP6p>ZbNPs^BZ!#wnVCPOC(5#b2OIKe5-aE=RH;tJQeDV-p$ycFJhJUeyzEUi*K LKed#P*i?T3o()oy delta 1994 zcmd7T%T5zf90u^2+D>gj3Q~$F=&2XPOONNAnK?rjEDBK}!6=t_SvAvkOo+6Fwwme& zq6=K;qLKg$T=57d@(ONz0}~TpK;NK#ofcb6CGO~?zhpY;r1SOrpVRd(pVjrZ`|1Eq z(&F=M)-JqE7EAepLyOB!rV^d1ua&|85D5^*K8t(nMq(yS>Hyah!`ihJ^u*=hqopB1c{*}k;=Hcvc9>Gju zDx}=Zv!*kWEiGl82`=N7!MPN1D!D0i5w~Q}w8-qtWMY15dgkG6TDD820&Vxm6N$N* z#H;zaIZHgddnaoIjW}7rO|wsqx(PW02SJ1FlJXCpa3x&sYbiwP2w>I&d{WhZ)lZYD z<$S8>UeemuC>Up~^J+x6P_xNKh(!D1(2M-9;+PQ9;2luhyO!20OUKim#^cA|nfIVG z_vhyloi(<;H>z(#^{L>26X1o~H4Xf55&{r}F6f3+&;udpg+4e9{Sbx$h`=D6fgv~x z=U^B{;5=N|R(+%zdQ^J+4%M$!g{*KxDv1jx&$FH7ZvJv6X03w3mhJk;tBL}d)+w=Ii bWXHd0Z0*JlCeUrbtgWBM1n#RJV^!@p4x9uY diff --git a/checker/Cargo.toml b/checker/Cargo.toml index 270bd1a8..f1d08a65 100644 --- a/checker/Cargo.toml +++ b/checker/Cargo.toml @@ -49,7 +49,7 @@ shellwords = "*" sled = "*" tar = "0.4.38" tempfile = "*" -z3-sys = { version = "*", features = ["static-link-z3"], optional = true } +z3-sys = { version = "*", git="https://github.com/prove-rs/z3.rs.git", features = ["vcpkg"], optional = true } [dev-dependencies] walkdir = "*" diff --git a/checker/src/abstract_value.rs b/checker/src/abstract_value.rs index 854ca428..8037a9f5 100644 --- a/checker/src/abstract_value.rs +++ b/checker/src/abstract_value.rs @@ -3416,7 +3416,11 @@ impl AbstractValueTrait for Rc { /// True if all possible concrete values are elements of the set corresponding to this domain. #[logfn_inputs(TRACE)] fn is_top(&self) -> bool { - matches!(&self.expression, Expression::Top) + match &self.expression { + Expression::Top => true, + Expression::Variable { path, .. } => path.is_top(), + _ => false, + } } /// True if this value is an empty tuple, which is the sole value of the unit type. diff --git a/checker/src/body_visitor.rs b/checker/src/body_visitor.rs index 2febdab9..e19facc6 100644 --- a/checker/src/body_visitor.rs +++ b/checker/src/body_visitor.rs @@ -835,6 +835,7 @@ impl<'analysis, 'compilation, 'tcx> BodyVisitor<'analysis, 'compilation, 'tcx> { return environment; } trace!("def_id {:?}", self.tcx.def_kind(self.def_id)); + let saved_type_visitor = self.type_visitor.clone(); let saved_mir = self.mir; let saved_def_id = self.def_id; for (ordinal, constant_mir) in self.tcx.promoted_mir(self.def_id).iter().enumerate() { @@ -917,7 +918,7 @@ impl<'analysis, 'compilation, 'tcx> BodyVisitor<'analysis, 'compilation, 'tcx> { } self.def_id = saved_def_id; self.mir = saved_mir; - self.type_visitor_mut().mir = saved_mir; + *self.type_visitor_mut() = saved_type_visitor; environment } diff --git a/checker/src/path.rs b/checker/src/path.rs index cdbc9510..ab3b6819 100644 --- a/checker/src/path.rs +++ b/checker/src/path.rs @@ -506,6 +506,13 @@ impl Path { } } + pub fn is_top(&self) -> bool { + match &self.value { + PathEnum::Computed { value } => value.is_top(), + _ => false, + } + } + // Returns the length of the path. #[logfn_inputs(TRACE)] pub fn path_length(&self) -> usize { diff --git a/checker/src/type_visitor.rs b/checker/src/type_visitor.rs index b6624f43..4a67d9ca 100644 --- a/checker/src/type_visitor.rs +++ b/checker/src/type_visitor.rs @@ -73,6 +73,7 @@ impl<'tcx> TypeCache<'tcx> { } } +#[derive(Clone)] pub struct TypeVisitor<'tcx> { pub actual_argument_types: Vec>, pub closures_being_specialized: RefCell>, diff --git a/checker/tests/run-pass/transmute.rs b/checker/tests/run-pass/transmute.rs index d0d27ac1..72fb9ebf 100644 --- a/checker/tests/run-pass/transmute.rs +++ b/checker/tests/run-pass/transmute.rs @@ -120,7 +120,7 @@ pub unsafe fn t6() { let arr_ptr = std::mem::transmute::<&[i32], *const [i32]>(arr_ref); let fat_ptr = std::mem::transmute::<*const [i32], FatPtr>(arr_ptr); verify!(fat_ptr.fat == 3); - verify!(*fat_ptr.ptr == 1); + verify!(*fat_ptr.ptr == 1); //~ possible false verification condition } pub unsafe fn t7() {