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

Handle new caller_location intrinsic the right way #374

Open
adpaco-aws opened this issue Aug 2, 2021 · 5 comments
Open

Handle new caller_location intrinsic the right way #374

adpaco-aws opened this issue Aug 2, 2021 · 5 comments
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] Unsupported Construct Add support to an unsupported construct

Comments

@adpaco-aws
Copy link
Contributor

adpaco-aws commented Aug 2, 2021

Rebase from #346 found a new caller_location intrinsic in the process. In order to unblock, we codegen this intrinsic as:

            "caller_location" => {
                codegen_unimplemented_intrinsic!("https://github.com/model-checking/rmc/issues/374")
            }

But we can probably codegen it the same way Rust does.

@adpaco-aws adpaco-aws added Area: verification [F] Soundness Kani failed to detect an issue labels Aug 2, 2021
@celinval celinval added [C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] Unsupported Construct Add support to an unsupported construct and removed Exp: easy [F] Soundness Kani failed to detect an issue labels Nov 9, 2022
@celinval
Copy link
Contributor

This is a nice explanation on what this does: https://hegdenu.net/posts/track-caller/

@adpaco-aws
Copy link
Contributor Author

Thanks for the update, @celinval !

If adding support for caller_location would allow us to avoid panic messages such as thread 'main' panicked at 'called `Option::unwrap()` on a `None` value', that'd be a major improvement in how we report such failures.

One thing that I don't see mentioned there is the relation to panic strategies. This isn't mentioned in the RFC neither, so I guess it's independent.

@celinval
Copy link
Contributor

celinval commented Mar 3, 2023

I was wondering if it would help with: #1740

@celinval
Copy link
Contributor

celinval commented Jul 3, 2023

For the current Rust implementation, the compiler will add an extra argument to functions that contain #[track_caller]. Unfortunately, this operation is done in the codegen stage, instead of a MIR pass. :(

My guess is that MIR passes can't really change the function signature, so they push it down to the codegen stage. I'm tempted to just encode this as a global variable for now.

@adpaco-aws I don't think CBMC really supports formatting error messages, so I'm not sure implementing this intrinsic will make much of a difference on how we report failures.

In order to fix that, we would have to either inline these functions or generate a different copy per location they are invoked from.

@celinval
Copy link
Contributor

celinval commented Jul 3, 2023

Implementation notes for myself:

  1. To build a constant that represents a location, use query const_caller_location [1].
  2. To get the type of the caller location, use function: pub fn caller_location_ty(self) -> Ty<'tcx> [2]
  3. We can check if a function requires caller location using requires_caller_location [3]
  4. If we are passing the caller location as an argument, we will need to create a ReifyShim for cases that require dynamic dispatch.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] Unsupported Construct Add support to an unsupported construct
Projects
None yet
Development

No branches or pull requests

2 participants