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

Cannot call tag value constructors for tag type imported from another crate. #150

Closed
froystig opened this issue Aug 19, 2010 · 5 comments
Closed

Comments

@froystig
Copy link
Contributor

Suppose foo.rc is compiled as a shared (library) crate, and looks like:

mod bar;

and that bar.rs looks like:

type baz = tag(a(), b(), c());

When we compile a file that looks like:

use foo;
import foo.bar;

fn main() {
    let bar.baz x = bar.a();   // alternatively bar.b() or bar.c()
}

we are told

Fatal error: exception Failure("internal_check_ext_lval: ident a not found in mod item")

in response to our use of bar.a().

Fix whatever is wrong with tags imported from an external crate.

@froystig
Copy link
Contributor Author

Here's the post-parse AST for the main file:

import bar = foo.bar
export *;
fn main() -> () {
    let mutable bar.baz x;
    x = bar.a();
}
mod foo {
    export *;
    mod bar {
        export *;
        type baz = rec(uint tag);
    }
}

Looks like DWARF for tag types is emitted incorrectly or parsed incorrectly.

@pcwalton
Copy link
Contributor

In fact, DWARF for tag types isn't parsed at all (see the handling of DW_TAG_structure_type at boot/me/dwarf.ml line 2954).

@pcwalton
Copy link
Contributor

The DWARF is parsed as of commit 88c9759, but the tag constructors still aren't created.

@pcwalton
Copy link
Contributor

pcwalton commented Sep 2, 2010

This will be fixed when tag types become fully nominal. graydon is working on this right now.

@graydon
Copy link
Contributor

graydon commented Jan 27, 2011

Fixed ages ago.

keeperofdakeys pushed a commit to keeperofdakeys/rust that referenced this issue Dec 12, 2017
Add SOCK_NONBLOCK & SOCK_CLOEXEC
kazcw pushed a commit to kazcw/rust that referenced this issue Oct 23, 2018
* x86: fixed testing equality of floating point numbers

* x86: removed unused macro branch

* x86: marked assert_approx_eq as used only in tests
dlrobertson pushed a commit to dlrobertson/rust that referenced this issue Nov 29, 2018
Merge Notation subsections into Notation.md
djtech-dev pushed a commit to djtech-dev/rust that referenced this issue Dec 9, 2021
antoyo added a commit to antoyo/rust that referenced this issue Jun 7, 2022
…_intrinsics

Add missing vendor intrinsics
celinval pushed a commit to celinval/rust-dev that referenced this issue Nov 29, 2024
…ng#180)

Towards rust-lang#150 

### Changes
* Added a `CStr` Safety Invariant
* Added a harness for `from_bytes_until_nul`, the harness covers:
    * The input slice contains a single null byte at the end;
    * The input slice contains no null bytes;
    * The input slice contains intermediate null bytes

### Discussion
* [Safety invariant
implementation](model-checking#150 (comment))
* [Input array
generation](model-checking#181)

### Verification Result
`./scripts/run-kani.sh --kani-args --harness ffi::c_str::verify`

```
// array size 16
Checking harness ffi::c_str::verify::check_from_bytes_until_nul...

VERIFICATION RESULT:
 ** 0 of 140 failed (5 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 7.3023376s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.
```

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 Nov 29, 2024
Towards rust-lang#150 

Changes
Added harnesses for count_bytes

Verification Result
```
Checking harness ffi::c_str::verify::check_count_bytes...

VERIFICATION RESULT:
 ** 0 of 241 failed (5 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 5.377671s
```
celinval pushed a commit to celinval/rust-dev that referenced this issue Nov 29, 2024
Towards rust-lang#150 

### Changes
* Added harnesses for `to_bytes` and `to_bytes_with_nul`
* Added a small fix to `count_bytes`

Verification Result:
```
Checking harness ffi::c_str::verify::check_to_bytes_with_nul...

VERIFICATION RESULT:
 ** 0 of 179 failed (5 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 88.397385s

Checking harness ffi::c_str::verify::check_to_bytes...

VERIFICATION RESULT:
 ** 0 of 180 failed (5 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 79.66312s

Checking harness ffi::c_str::verify::check_from_bytes_until_nul...

VERIFICATION RESULT:
 ** 0 of 132 failed (5 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 28.593569s

Complete - 3 successfully verified harnesses, 0 failures, 3 total.
```
celinval pushed a commit to celinval/rust-dev that referenced this issue Dec 6, 2024
Towards rust-lang#150 

### Changes
* Added a harness for `is_empty`
* Added a small optimization for `arbitray_cstr`

### Verification Result
```
SUMMARY:
 ** 0 of 193 failed (5 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 51.462265s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.
```
celinval pushed a commit to celinval/rust-dev that referenced this issue Dec 6, 2024
Towards rust-lang#150 

Verifies that the CStr safety invariant holds after calling :

from_bytes_with_nul --> core::ffi::c_str module
celinval pushed a commit to celinval/rust-dev that referenced this issue Dec 6, 2024
Towards rust-lang#150 

Verifies that the CStr safety invariant holds after calling :

`bytes	core::ffi::c_str`
`to_str	core::ffi::c_str`
`as_ptr	core::ffi::c_str`

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Yenyun035 <yew005eng@gmail.com>
Co-authored-by: Yenyun035 <57857379+Yenyun035@users.noreply.github.com>
carolynzech pushed a commit to celinval/rust-dev that referenced this issue Dec 13, 2024
Towards rust-lang#150

Similar PR Ref : rust-lang#193 

Annotates and verifies the safety contracts for the unsafe function :
`from_ptr` - `core::ffi::c_str`

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Yenyun035 <57857379+Yenyun035@users.noreply.github.com>
Co-authored-by: Yenyun035 <yew005eng@gmail.com>
carolynzech added a commit to celinval/rust-dev that referenced this issue Dec 13, 2024
…ith_nul_unchecked (rust-lang#193)

Towards rust-lang#150

Annotates and verifies the safety contracts for the following unsafe
functions:

`from_bytes_with_nul_uncheked` `core::ffi::c_str`
`strlen` `core::ffi::c_str`

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Yenyun035 <yew005eng@gmail.com>
Co-authored-by: Yenyun035 <57857379+Yenyun035@users.noreply.github.com>
Co-authored-by: Carolyn Zech <cmzech@amazon.com>
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