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

Non returning instrinsics should be handled properly #734

Closed
adpaco-aws opened this issue Jan 6, 2022 · 1 comment · Fixed by #736
Closed

Non returning instrinsics should be handled properly #734

adpaco-aws opened this issue Jan 6, 2022 · 1 comment · Fixed by #736
Assignees
Labels
[I] Refactoring / Clean Up Refactoring or cleaning up of existing code

Comments

@adpaco-aws
Copy link
Contributor

The hooks.rs file handles the abort intrinsic before even calling codegen_intrinsic in this piece of code:

    fn handle(
        &self,
        tcx: &mut GotocCtx<'tcx>,
        instance: Instance<'tcx>,
        fargs: Vec<Expr>,
        assign_to: Option<Place<'tcx>>,
        target: Option<BasicBlock>,
        span: Option<Span>,
    ) -> Stmt {
        let loc = tcx.codegen_span_option(span);
        if tcx.symbol_name(instance) == "abort" {
            Stmt::assert_false("abort intrinsic reached", loc)
        } else {
            let p = assign_to.unwrap();
            let target = target.unwrap();
            Stmt::block(
                vec![
                    tcx.codegen_intrinsic(instance, fargs, &p, span),
                    Stmt::goto(tcx.current_fn().find_label(&target), loc.clone()),
                ],
                loc,
            )
        }
    }
}

This special case should be removed to handle abort in codegen_intrinsic

@adpaco-aws adpaco-aws added Area: verification [I] Refactoring / Clean Up Refactoring or cleaning up of existing code labels Jan 6, 2022
@adpaco-aws adpaco-aws self-assigned this Jan 6, 2022
This was referenced Jan 6, 2022
@adpaco-aws adpaco-aws changed the title Abort intrinsic handled before call to codegen_intrinsic Non returning instrinsics should be handled before call to codegen_intrinsic Jan 7, 2022
@adpaco-aws adpaco-aws changed the title Non returning instrinsics should be handled before call to codegen_intrinsic Non returning instrinsics should be handled properly Jan 7, 2022
@adpaco-aws
Copy link
Contributor Author

Renaming since handling abort before or at the beginning of codegen_intrinsic is the right thing to do. But we should not always expect a destination (p or place in the code above) since non returning intrinsics will not have one.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[I] Refactoring / Clean Up Refactoring or cleaning up of existing code
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant