Skip to content

Add __builtin_trap to x86 - #357

Open
Aurel300 wants to merge 1 commit into
AbsInt:masterfrom
Aurel300:feature/x86-trap
Open

Aurel300 wants to merge 1 commit into
AbsInt:masterfrom
Aurel300:feature/x86-trap

Conversation

@Aurel300

Copy link
Copy Markdown

This PR adds support for __builtin_trap on x86, mapped to the ud2 instruction. I copied how this was done for PowerPC.

Should I instead add a case for the Pbuiltin pseudo-instruction?

@remix7531

Copy link
Copy Markdown

I know this PR is quite dated but I would also like to have this feature. Willing to rebase.

@xavierleroy

Copy link
Copy Markdown
Contributor

Noted! Can you tell us a bit more how you'd use this feature? When the PR was first discussed, we weren't sure of the intended usage. In the meantime, you can always use inline assembly:

   asm volatile ("ub2");

@remix7531

Copy link
Copy Markdown

I am formally verifying libsecp256k1 and SHRINCS with CompCert and VST. SHRINCS uses __builtin_trap in its panic function, but currently falls back to an infinite loop under CompCert. The proofs establish that panic is unreachable under the specified preconditions, while the trap provides runtime failure handling outside them.

Builtin support would avoid architecture-specific inline assembly and let the CompCert build trap too. For precision, secp256k1 currently uses abort.

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.

3 participants