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

Improve the tail call identification logic to prefer local jumps unless the target is a known function entry #296

Merged
merged 2 commits into from
Jun 27, 2022

Conversation

travitch
Copy link
Contributor

@travitch travitch commented Jun 24, 2022

It turns out that we have to be more conservative with tail call identification, as incorrectly identifying a block as the target of a tail call (instead of a branch) can cause other branch classifiers to fail if that block is the target of another jump.

The tradeoff is that we will recognize fewer tail calls, but we will also encounter fewer situations where intra-procedural jumps are not resolved. Ultimately, we will need to give up some tail call recognition (since they are in general indistinguishable from jumps), and instead only identify known call targets as tail call candidates.

With additional global analysis we could do better.

Fixes #294

It turns out that we have to be more conservative with tail call identification,
as incorrectly identifying a block as the target of a tail call (instead of a
branch) can cause other branch classifiers to fail if that block is the target
of another jump.

Ultimately, we will need to give up some tail call recognition (since they are
in general indistinguishable from jumps), and instead only identify known call
targets as tail call candidates.

With additional global analysis we could do better.

Fixes #294
@travitch travitch marked this pull request as ready for review June 24, 2022 23:51
@travitch travitch changed the title Tr/fix 294 Improve the tail call identification logic to prefer local jumps unless the target is a known function entry Jun 25, 2022
@RyanGlScott
Copy link
Contributor

With additional global analysis we could do better.

Is there an issue tracking this idea?

@RyanGlScott
Copy link
Contributor

Is there an issue tracking this idea?

For posterity's sake, this is now tracked in #298.

RyanGlScott added a commit to GaloisInc/ambient-verifier that referenced this pull request Mar 1, 2023
This is an alternative fix for GaloisInc/macaw#285
(i.e., allowing tail calls into PLT stubs) without needing to rearrange the
order in which `macaw`'s classifiers run (the culprit behind
GaloisInc/macaw#294). Our new approach is to mark
all PLT stub addresses as trusted function entry points so that code discovery
will be more likely to analyze them. See the comments on the new
`lbpTrustedPltEntryPoints` function for the full details.

This bumps the `macaw` submodule to bring in the changes from
GaloisInc/macaw#296, which prompted the need for
changing the behavior on the `ambient-verifier` side in the first place.
@Ptival Ptival deleted the tr/fix-294 branch August 14, 2023 15:29
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.

BLST SAW x86 proofs fail after commit 8e10643 (Fix tail call classification)
2 participants