-
Notifications
You must be signed in to change notification settings - Fork 13.1k
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.
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
Implement the occurs check for type unification #229
Comments
I think maybe some permutation of the following might trigger it:
I'm not sure if this is exactly right but the idea is to try to write a function that forces the inference algorithm to infer an infinite tower of options. Dave |
This is done now, yes? |
No, not done yet. |
So, I... can't actually reproduce this. For example, I tried Paul's example from #602 and it correctly prints a type error. I tried a version of Dave's example above, and the result is the same. Maybe something with how tags are handled has been changed recently so that this case just never happens in the unifier? I was going to fix it, but with no test case, I'm going to close it instead (reopen if you have a test case!) |
Occurs check is now implemented -- see #768 -- but there may be checks missing in places that should have them. |
linux: Move some MS_flags for mount(2) up These flags are available on Android.
…ferentiation. (rust-lang#229) * Enzyme iter * Temp * Fix indexing * Fix recursive struct accumulation
…st-lang#229) * Add an __VERIFIER_expected_fail() intrinsic, and use it in a test * PR comments
Shard Kani verification workflow across multiple runners by: 1. Running `kani list --format json`, which outputs a JSON file like this: ```json { "kani-version": "0.56.0", "file-version": "0.1", "standard-harnesses": { "src/lib.rs": [ "proof3", "verify::proof2" ], "src/test.rs": [ "test::proof4", "test::proof5" ] }, "contract-harnesses": { "src/lib.rs": [ "proof" ] }, "contracts": [ { "function": "bar", "file": "src/lib.rs", "harnesses": [ "proof" ] } ], "totals": { "standard-harnesses": 4, "contract-harnesses": 1, "functions-under-contract": 1 } } ``` 2. Extracting the harnesses inside `"standard-harnesses"` and `"contract-harnesses"` into an array called `ALL_HARNESSES` and the length of that array into `HARNESS_COUNT`. (So in this example, `ALL_HARNESSES = [proof3, verify::proof2, test::proof4, test::proof5, proof]` and `HARNESS_COUNT=5`). 3. Dividing the harnesses evenly between four workers. For example, if worker 1's harnesses are `proof3` and `verify::proof2`, then we call `kani verify-std --harness proof3 --harness verify::proof2 --exact`. The `--exact` makes Kani look for the exact harness name. This is important so that we don't match on partial patterns, e.g., if there is a harness called "foo" and a harness called "foo_bar", passing `--harness foo` without `--exact` would match against both harnesses, and then `foo_bar` would run twice. 4. Also parallelize verification within a single runner by passing `-j` to Kani. I chose four workers somewhat arbitrarily--it makes each worker take about 45 minutes to an hour to finish. I thought it was good to have a balance between too few workers (which still makes us wait a while) and too many workers (which makes you look through more logs to find where a given harness is being verified). But happy to play with this number if people have opinions. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
This harness takes between 22-25 minutes in CI. Change the harnesses's macro to use kissat solver instead, which brings verification time down to ~7 seconds. As an aside, I noticed this problem because the partition 1 runner in rust-lang#229 is taking ~55 minutes, where the other partitions are taking ~30 minutes. This harness accounts for almost the entire difference. One nice consequence of partitioning verification is that it will make performance issues like this more noticeable. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Fix a typo introduced in rust-lang#229 that prevents `kani-args` from getting passed to the `kani` command. This was discovered by @tengjiang (see model-checking#231). By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
…<try> Bump bootstrap cc to 1.2.14 and cmake to 0.1.54 ## Summary Bump bootstrap's `cc` and `cmake` deps: 1. To make it easier to add new/unofficial targets. In particular, `cc` v1.2.4+ allows using env vars to pass target parameters to the `cc` crate. This was previously attempted in rust-lang#134344 but ran into macos-cross-to-iOS problems with `cmake` (and also rust-lang#136440, rust-lang#136720). See also discussions in rust-lang/cc-rs#1317. 2. Fix some flag inheritance warnings. Fixes rust-lang#136338. ## `cc` changelogs between `1.2.0` and `1.2.14` > ## [1.2.14](rust-lang/cc-rs@cc-v1.2.13...cc-v1.2.14) - 2025-02-14 > > ### Other > > - Regenerate target info ([rust-lang#1398](rust-lang/cc-rs#1398)) > - Add support for setting `-gdwarf-{version}` based on RUSTFLAGS ([rust-lang#1395](rust-lang/cc-rs#1395)) > - Add support for alternative network stack io-sock on QNX 7.1 aarch64 and x86_64 ([rust-lang#1312](rust-lang/cc-rs#1312)) > > ## [1.2.13](rust-lang/cc-rs@cc-v1.2.12...cc-v1.2.13) - 2025-02-08 > > ### Other > > - Fix cross-compiling for Apple platforms ([rust-lang#1389](rust-lang/cc-rs#1389)) > > ## [1.2.12](rust-lang/cc-rs@cc-v1.2.11...cc-v1.2.12) - 2025-02-04 > > ### Other > > - Split impl Build ([rust-lang#1382](rust-lang/cc-rs#1382)) > - Don't specify both `-target` and `-mtargetos=` on Apple targets ([rust-lang#1384](rust-lang/cc-rs#1384)) > > ## [1.2.11](rust-lang/cc-rs@cc-v1.2.10...cc-v1.2.11) - 2025-01-31 > > ### Other > > - Fix more flag inheritance ([rust-lang#1380](rust-lang/cc-rs#1380)) > - Include wrapper args. in `stdout` family heuristics to restore classifying `clang --driver-mode=cl` as `Msvc { clang_cl: true }` ([rust-lang#1378](rust-lang/cc-rs#1378)) > - Constrain `-Clto` and `-Cembed-bitcode` flag inheritance to be `clang`-only ([rust-lang#1379](rust-lang/cc-rs#1379)) > - Pass deployment target with `-m*-version-min=` ([rust-lang#1339](rust-lang/cc-rs#1339)) > - Regenerate target info ([rust-lang#1376](rust-lang/cc-rs#1376)) > > ## [1.2.10](rust-lang/cc-rs@cc-v1.2.9...cc-v1.2.10) - 2025-01-17 > > ### Other > > - Fix CC_FORCE_DISABLE=0 evaluating to true ([rust-lang#1371](rust-lang/cc-rs#1371)) > - Regenerate target info ([rust-lang#1369](rust-lang/cc-rs#1369)) > - Make hidden lifetimes explicit. ([rust-lang#1366](rust-lang/cc-rs#1366)) > > ## [1.2.9](rust-lang/cc-rs@cc-v1.2.8...cc-v1.2.9) - 2025-01-12 > > ### Other > > - Don't pass inherited PGO flags to GNU compilers (rust-lang#1363) > - Adjusted zig cc judgment and avoided zigbuild errors([rust-lang#1360](rust-lang/cc-rs#1360)) ([rust-lang#1361](rust-lang/cc-rs#1361)) > - Fix compilation on macOS using clang and fix compilation using zig-cc ([rust-lang#1364](rust-lang/cc-rs#1364)) > > ## [1.2.8](rust-lang/cc-rs@cc-v1.2.7...cc-v1.2.8) - 2025-01-11 > > ### Other > > - Add `is_like_clang_cl()` getter (rust-lang#1357) > - Fix clippy error in lib.rs ([rust-lang#1356](rust-lang/cc-rs#1356)) > - Regenerate target info ([rust-lang#1352](rust-lang/cc-rs#1352)) > - Fix compiler family detection issue with clang-cl on macOS ([rust-lang#1328](rust-lang/cc-rs#1328)) > - Update `windows-bindgen` dependency ([rust-lang#1347](rust-lang/cc-rs#1347)) > - Fix clippy warnings ([rust-lang#1346](rust-lang/cc-rs#1346)) > > ## [1.2.7](rust-lang/cc-rs@cc-v1.2.6...cc-v1.2.7) - 2025-01-03 > > ### Other > > - Regenerate target info ([rust-lang#1342](rust-lang/cc-rs#1342)) > - Document new supported architecture names in windows::find > - Make is_flag_supported_inner take an &Tool ([rust-lang#1337](rust-lang/cc-rs#1337)) > - Fix is_flag_supported on msvc ([rust-lang#1336](rust-lang/cc-rs#1336)) > - Allow using Visual Studio target names in `find_tool` ([rust-lang#1335](rust-lang/cc-rs#1335)) > > ## [1.2.6](rust-lang/cc-rs@cc-v1.2.5...cc-v1.2.6) - 2024-12-27 > > ### Other > > - Don't inherit the `/Oy` flag for 64-bit targets ([rust-lang#1330](rust-lang/cc-rs#1330)) > > ## [1.2.5](rust-lang/cc-rs@cc-v1.2.4...cc-v1.2.5) - 2024-12-19 > > ### Other > > - Check linking when testing if compiler flags are supported ([rust-lang#1322](rust-lang/cc-rs#1322)) > > ## [1.2.4](rust-lang/cc-rs@cc-v1.2.3...cc-v1.2.4) - 2024-12-13 > > ### Other > > - Add support for C/C++ compiler for Neutrino QNX: `qcc` ([rust-lang#1319](rust-lang/cc-rs#1319)) > - use -maix64 instead of -m64 ([rust-lang#1307](rust-lang/cc-rs#1307)) > > ## [1.2.3](rust-lang/cc-rs@cc-v1.2.2...cc-v1.2.3) - 2024-12-06 > > ### Other > > - Improve detection of environment when compiling from msbuild or msvc ([rust-lang#1310](rust-lang/cc-rs#1310)) > - Better error message when failing on unknown targets ([rust-lang#1313](rust-lang/cc-rs#1313)) > - Optimize RustcCodegenFlags ([rust-lang#1305](rust-lang/cc-rs#1305)) > > ## [1.2.2](rust-lang/cc-rs@cc-v1.2.1...cc-v1.2.2) - 2024-11-29 > > ### Other > > - Inherit flags from rustc ([rust-lang#1279](rust-lang/cc-rs#1279)) > - Add support for using sccache wrapper with cuda/nvcc ([rust-lang#1304](rust-lang/cc-rs#1304)) > - Fix msvc stdout not shown on error ([rust-lang#1303](rust-lang/cc-rs#1303)) > - Regenerate target info ([rust-lang#1301](rust-lang/cc-rs#1301)) > - Fix compilation of C++ code for armv7-unknown-linux-gnueabihf ([rust-lang#1298](rust-lang/cc-rs#1298)) > - Fetch target info from Cargo even if `Build::target` is manually set ([rust-lang#1299](rust-lang/cc-rs#1299)) > - Fix two files with different extensions having the same object name ([rust-lang#1295](rust-lang/cc-rs#1295)) > - Allow disabling cc's ability to compile via env var CC_FORCE_DISABLE ([rust-lang#1292](rust-lang/cc-rs#1292)) > - Regenerate target info ([rust-lang#1293](rust-lang/cc-rs#1293)) > > ## [1.2.1](rust-lang/cc-rs@cc-v1.2.0...cc-v1.2.1) - 2024-11-14 > > ### Other > > - When invoking `cl -?`, set stdin to null ([rust-lang#1288](rust-lang/cc-rs#1288)) ## `cmake` changelogs `0.1.51` to `0.1.54` > ## [0.1.54](rust-lang/cmake-rs@v0.1.53...v0.1.54) - 2025-02-10 > > ### Other > > - Remove workaround for broken `cc-rs` versions ([rust-lang#235](rust-lang/cmake-rs#235)) > - Be more precise in the description of `register_dep` ([rust-lang#238](rust-lang/cmake-rs#238)) > > ## [0.1.53](rust-lang/cmake-rs@v0.1.52...v0.1.53) - 2025-01-27 > > ### Other > > - Disable broken Make jobserver support on OSX to fix parallel builds ([rust-lang#229](rust-lang/cmake-rs#229)) > > ## [0.1.52](rust-lang/cmake-rs@v0.1.51...v0.1.52) - 2024-11-25 > > ### Other > > - Expose cc-rs no_default_flags for hassle-free cross-compilation ([rust-lang#225](rust-lang/cmake-rs#225)) > - Add a `success` job to CI > - Change `--build` to use an absolute path > - Merge pull request [rust-lang#195](rust-lang/cmake-rs#195) from meowtec/feat/improve-fail-hint > - Improve hint for cmake not installed in Linux (code 127) > > ## [0.1.51](rust-lang/cmake-rs@v0.1.50...v0.1.51) - 2024-08-15 > > ### Added > > - Add JOM generator support ([rust-lang#183](rust-lang/cmake-rs#183)) > - Improve visionOS support ([rust-lang#209](rust-lang/cmake-rs#209)) > - Use `Generic` for bare-metal systems ([rust-lang#187](rust-lang/cmake-rs#187)) > > ### Fixed > > - Fix cross compilation on android armv7 and x86 ([rust-lang#186](rust-lang/cmake-rs#186)) try-job: dist-apple-various
We can infinite loop if we try to unify e.g. T with option[T]. Fixing this requires implementing the occurs check. Off the top of my head, I can't think of any cases in which we'd actually trip this, but it's theoretically possible.
Tim thinks this may also be the cause of segfaulting on infinitely interior tags:
The text was updated successfully, but these errors were encountered: