Skip to content
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

Closed
pcwalton opened this issue Feb 18, 2011 · 5 comments
Closed

Implement the occurs check for type unification #229

pcwalton opened this issue Feb 18, 2011 · 5 comments
Labels
A-type-system Area: Type system I-crash Issue: The compiler crashes (SIGSEGV, SIGABRT, etc). Use I-ICE instead when the compiler panics.

Comments

@pcwalton
Copy link
Contributor

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:

tag t1 {
    a(int);
    b(@t1);
}
@dherman
Copy link
Contributor

dherman commented Feb 18, 2011

I think maybe some permutation of the following might trigger it:

fn f[T](T x) -> option[T] {
  auto y = f(Some(x));
  ret Some(t);
}

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

@graydon
Copy link
Contributor

graydon commented May 26, 2011

This is done now, yes?

@pcwalton
Copy link
Contributor Author

No, not done yet.

@catamorphism
Copy link
Contributor

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!)

@catamorphism
Copy link
Contributor

Occurs check is now implemented -- see #768 -- but there may be checks missing in places that should have them.

keeperofdakeys pushed a commit to keeperofdakeys/rust that referenced this issue Dec 12, 2017
linux: Move some MS_flags for mount(2) up

These flags are available on Android.
ZuseZ4 pushed a commit to EnzymeAD/rust that referenced this issue Mar 7, 2023
…ferentiation. (rust-lang#229)

* Enzyme iter

* Temp

* Fix indexing

* Fix recursive struct accumulation
matthiaskrgr pushed a commit to matthiaskrgr/rust that referenced this issue Mar 7, 2023
celinval pushed a commit to celinval/rust-dev that referenced this issue Jun 4, 2024
…st-lang#229)

* Add an __VERIFIER_expected_fail() intrinsic, and use it in a test

* PR comments
celinval pushed a commit to celinval/rust-dev that referenced this issue Jan 3, 2025
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.
celinval pushed a commit to celinval/rust-dev that referenced this issue Jan 3, 2025
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.
celinval pushed a commit to celinval/rust-dev that referenced this issue Jan 3, 2025
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.
bors added a commit to rust-lang-ci/rust that referenced this issue Feb 15, 2025
…<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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-type-system Area: Type system I-crash Issue: The compiler crashes (SIGSEGV, SIGABRT, etc). Use I-ICE instead when the compiler panics.
Projects
None yet
Development

No branches or pull requests

4 participants