Skip to content

Handle non returning intrinsics#736

Merged
adpaco merged 5 commits into
model-checking:mainfrom
adpaco:non-ret_intrinsics
Jan 11, 2022
Merged

Handle non returning intrinsics#736
adpaco merged 5 commits into
model-checking:mainfrom
adpaco:non-ret_intrinsics

Conversation

@adpaco

@adpaco adpaco commented Jan 7, 2022

Copy link
Copy Markdown
Contributor

Description of changes:

Adds a specific function for handling of non returning intrinsics, which currently are abort and a special case of transmute.

Resolved issues:

Resolves #734

Call-outs:

Wrote a function for these special intrinsics but they can also be handled within the codegen_intrinsic function. That would require passing p as an option (i.e., not unwrap before call to codegen_intrinsic) and match on it at the beginning of codegen_intrinsic. Let me know if you prefer it that way.

Testing:

  • How is this change tested? Existing regression + new test for transmute.

  • Is this a refactor change? No.

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

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

@adpaco adpaco requested a review from a team as a code owner January 7, 2022 22:27
@adpaco adpaco force-pushed the non-ret_intrinsics branch from 5d128eb to 5079c97 Compare January 7, 2022 22:34
let loc = self.codegen_span_option(span);
debug!("codegen_nonret_intrinsic:\n\tinstance {:?}\n\tspan {:?}", instance, span);
match intrinsic {
"abort" => Stmt::assert_false("reached intrinsic::abort", loc),

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I recommend using GotocCtx::codegen_fatal_error() here. The Stmt::assert_false will not abort the program execution path.


/// Handles codegen for non returning intrinsics
/// Non returning intrinsics are not associated with a destination
pub fn codegen_nonret_intrinsic(

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nit: I would rename it to codegen_never_return_intrinsic()

@celinval celinval left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It looks good. We do need to add either an assume(false) or abort() call after the assert(false) though. In gotoc, an assertion failure does not interrupt the execution flow which may cause some odd behavior.

@adpaco

adpaco commented Jan 10, 2022

Copy link
Copy Markdown
Contributor Author

Thanks @celinval ! Renamed and replaced assert(false) by codegen_fatal_error() in both cases, since they have similar behaviors.

@celinval celinval left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Perfect! Thanks

@adpaco adpaco merged commit 3cc1174 into model-checking:main Jan 11, 2022
@adpaco adpaco mentioned this pull request Jan 12, 2022
tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 26, 2022
* Handle non returning intrinsics

* Newline in comment

* Address comments
tedinski pushed a commit that referenced this pull request Apr 27, 2022
* Handle non returning intrinsics

* Newline in comment

* Address comments
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

Successfully merging this pull request may close these issues.

Non returning instrinsics should be handled properly

2 participants