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

Auto-dereference crashes rustboot #112

Closed
jyasskin opened this issue Jul 17, 2010 · 2 comments
Closed

Auto-dereference crashes rustboot #112

jyasskin opened this issue Jul 17, 2010 · 2 comments

Comments

@jyasskin
Copy link
Contributor

Compiling:

obj obT() {
  fn call() {
  }
}
fn foo(@obT o) {
  o.call();
}
fn main() {
}

crashes with:

Fatal error: exception Failure("get_element_ptr 1 on cell [ebp + 0x20]")
Raised at file "pervasives.ml", line 22, characters 22-33
Called from file "boot/me/trans.ml", line 3844, characters 16-64
Called from file "boot/me/trans.ml", line 3887, characters 49-75
Called from file "boot/me/trans.ml", line 3422, characters 38-63
Called from file "boot/me/trans.ml", line 4276, characters 14-92
Called from file "boot/me/trans.ml", line 4055, characters 6-26
Re-raised at file "boot/me/trans.ml", line 4072, characters 11-104
Called from file "array.ml", line 117, characters 31-48
Called from file "boot/me/trans.ml", line 1974, characters 4-36
Called from file "boot/me/trans.ml", line 4604, characters 4-20
Called from file "boot/me/trans.ml", line 4999, characters 4-39
Called from file "boot/me/semant.ml", line 1435, characters 4-17
Called from file "boot/me/semant.ml", line 1561, characters 4-50
Called from file "boot/me/walk.ml", line 134, characters 4-9
Called from file "hashtbl.ml", line 145, characters 8-13
Called from file "hashtbl.ml", line 148, characters 4-19
Called from file "boot/me/walk.ml", line 135, characters 4-15
Called from file "array.ml", line 130, characters 31-51
Called from file "boot/driver/session.ml", line 60, characters 10-17
Called from file "boot/me/semant.ml", line 1861, characters 8-84
Called from file "boot/driver/main.ml", line 322, characters 9-26
Called from file "array.ml", line 117, characters 31-48
Called from file "boot/driver/main.ml", line 320, characters 4-366
Called from file "boot/driver/main.ml", line 404, characters 5-21

Changing foo to use "(*o).call();" avoids the crash.

@graydon
Copy link
Contributor

graydon commented Jul 17, 2010

Yuck. Not sure if this is a bug in the new typechecker (it injects the auto-dereference markers) or an assumption baked into trans based on the old one (it consumes them and is obviously getting upset here). Will investigate, thanks.

@froystig
Copy link
Contributor

Autoderef objects when passing them as implicit (indirect) arg upon vtbl-dispatch. Add testcase and XFAIL it on LLVM. Closed by fde9ca0.

mbrubeck pushed a commit to mbrubeck/rust that referenced this issue Oct 17, 2011
…tbl-dispatch. Add testcase and XFAIL it on LLVM. Closes rust-lang#112.
arielb1 pushed a commit to arielb1/rust that referenced this issue Apr 10, 2015
dlrobertson pushed a commit to dlrobertson/rust that referenced this issue Nov 29, 2018
Inner and outer docs/comments were swapped
flip1995 pushed a commit to flip1995/rust that referenced this issue Dec 20, 2020
Add Redundant else lint

changelog: Add redundant_else lint

It seemed appropriate for "pedantic".

Closes rust-lang#112 \*blows off dust*
djtech-dev pushed a commit to djtech-dev/rust that referenced this issue Dec 9, 2021
Add `atomicrmw` and `cmpxchg` instructions to the builder.
jaisnan pushed a commit to jaisnan/rust-dev that referenced this issue Oct 22, 2024
Towards rust-lang#59 

### Changes
* Added contracts for `wrapping_shl` (located in
`library/core/src/num/int_macros.rs` and `uint_macros.rs`)
* Added a macro for generating wrapping_{shl, shr} harnesses
* Added harnesses for `wrapping_shl` of each integer type
* `i8`, `i16`, `i32`, `i64`, `i128`, `isize`, `u8`, `u16`, `u32`, `u64`,
`u128`, `usize` --- 12 harnesses in total.

### Revalidation
1. Per the discussion in rust-lang#59, we have to **build and run Kani from
`feature/verify-rust-std` branch**.
2. To revalidate the verification results, run the following command.
`<harness_to_run>` can be either `num::verify` to run all harnesses or
`num::verify::<harness_name>` (e.g. `checked_wrapping_shl_i8`) to run a
specific harness.
```
kani verify-std  "path/to/library" \
    --harness <harness_to_run> \
    -Z unstable-options \
    -Z function-contracts \
    -Z mem-predicates
```

All harnesses should pass the default checks (1251 checks where 1
unreachable).
```
SUMMARY:
 ** 0 of 1251 failed (1 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 2.4682913s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.
```
Example of the unreachable check:
```
Check 123: num::<impl i8>::wrapping_shl.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to subtract with overflow"
         - Location: library/core/src/num/int_macros.rs:2172:42 in function num::<impl i8>::wrapping_shl
```

### Questions
1. Should we add `requires` (and `ensures`) for `wrapping_shl` given
that `unchecked_shl` already has a `requires`?

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
This issue was closed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants