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.

Sign up for GitHub

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

Jump to bottom

Standard library function panicking::take_hook does not codegen #208

Closed
danielsn opened this issue Jun 16, 2021 · 5 comments
Closed

Standard library function panicking::take_hook does not codegen #208

danielsn opened this issue Jun 16, 2021 · 5 comments
Assignees
@celinval
Labels
[C] Bug This is a bug. Something isn't working.
Milestone
Maintenance

Comments

@danielsn
Copy link
Contributor 

            // [compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs:885] self.current_fn().readable_name() = "panicking::take_hook"
            // error: internal compiler error: compiler/rustc_middle/src/ty/fold.rs:829:17: Trying to collect bound vars with a bound region: DebruijnIndex(0) BoundRegion { var: 0, kind: BrAnon(0) }

related #109
@avanhatt avanhatt mentioned this issue Aug 25, 2021
Merged
4 tasks
zhassan-aws added a commit to zhassan-aws/kani that referenced this issue Mar 15, 2022
@zhassan-aws
Add test for model-checking#208
c93890b
@zhassan-aws
Copy link
Contributor

This doesn't fail as of 4fe8370a2a8 on the following example:

use std::panic;

fn main() {
    panic::set_hook(Box::new(|_| {
        println!("Custom panic hook");
    }));

    let _ = panic::take_hook();

    panic!("Normal panic");
}

zhassan-aws added a commit to zhassan-aws/kani that referenced this issue Mar 15, 2022
@zhassan-aws
Add test for model-checking#208
80715f5
@zhassan-aws zhassan-aws mentioned this issue Mar 15, 2022
Closed
4 tasks
@zhassan-aws
Copy link
Contributor

This stopped working at some point (possibly due to the switch to using assert-false-assume-false for missing functions). It seems that the set_hook/take_hook functions need the standard library to be linked as their definition is missing. The example above now fails with:

Check 9: _ZN3std9panicking8set_hook17hd9797ff1f60891f8E.assertion.1
	 - Status: FAILURE
	 - Description: "assertion false"
	 - Location: Unknown File in function _ZN3std9panicking8set_hook17hd9797ff1f60891f8E

which suggests that the definition of set_hook is missing. If I remove set_hook:

fn main() {
    let _ = panic::take_hook();

    panic!("Normal panic");
}

I get a different failure due to a missing take_hook function:

Check 4: _ZN3std9panicking9take_hook17h69295202e6d47881E.assertion.1
	 - Status: FAILURE
	 - Description: "assertion false"
	 - Location: Unknown File in function _ZN3std9panicking9take_hook17h69295202e6d47881E

@tedinski tedinski mentioned this issue May 23, 2022
Closed
@celinval celinval self-assigned this Oct 26, 2022
@celinval celinval mentioned this issue Oct 26, 2022
Merged
4 tasks
@celinval
Copy link
Contributor

There seems to still be an issue with this test even after we fixed the linking issue. The new failure has to do with pthread handling. With an unwind of 2, this test now fails with the following error:

: function call: parameter "pthread_key_create::destructor" type mismatch:
got struct_tag
  * identifier: tag-_18057172096210256107
expected pointer
  * #source_location:
    * file: <builtin-library-pthread_key_create>
    * line: 11
    * function: pthread_key_create
    * working_directory: /tmp/StdLink
  * width: 64
  * #failed_symbol: pthread_key_create::destructor$object
  0: code
      * #source_location:
        * file: <builtin-library-pthread_key_create>
        * line: 11
        * function: pthread_key_create
        * working_directory: /tmp/StdLink
      * return_type: empty
          * #source_location:
            * file: <builtin-library-pthread_key_create>
            * line: 11
            * function: pthread_key_create
            * working_directory: /tmp/StdLink
      * parameters:
        0: parameter
            * type: pointer
                * #source_location:
                  * file: <builtin-library-pthread_key_create>
                  * line: 11
                  * function: pthread_key_create
                  * working_directory: /tmp/StdLink
                * width: 64
                0: empty
                    * #source_location:
                      * file: <builtin-library-pthread_key_create>
                      * line: 11
                      * function: pthread_key_create
                      * working_directory: /tmp/StdLink
            * #source_location:
              * file: <builtin-library-pthread_key_create>
              * line: 11
              * function: pthread_key_create
              * working_directory: /tmp/StdLink

CBMC failed with status 6

@adpaco-aws
Copy link
Contributor

That's the same error reported in #1781

celinval added a commit that referenced this issue Oct 26, 2022
@celinval
Add tests for issues related to std linking (#1801)
f306a44 
Add tests for #564, #208 and #87.

Unfortunately, it looks like there are still issues with with how we are
encoding panic threads and dynamic objects which are causing two of the
test cases to fail.
@celinval celinval mentioned this issue Nov 3, 2022
Merged
4 tasks
@tedinski tedinski added the [C] Bug This is a bug. Something isn't working. label Nov 14, 2022
@celinval
Copy link
Contributor

The original issue described here has been fixed.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@celinval celinval

Labels
[C] Bug This is a bug. Something isn't working.
Projects
None yet
Milestone
Maintenance
Development

Successfully merging a pull request may close this issue.

Add test for #208 zhassan-aws/kani
5 participants
@tedinski @danielsn @celinval @adpaco-aws @zhassan-aws