[herd][AArch64] Fix GCS fault propagation - #1950
Draft
murzinv wants to merge 3 commits into
Draft
Conversation
The AArch64 CAS monad helpers currently force the write_rs callback and the overall operation to return unit. This prevents callers whose register-update step determines instruction control flow from propagating that result; in particular, a GCS CAS must retain either its normal Next result or a Fault result instead of discarding it and advancing unconditionally. Generalise only the callback result from unit to an arbitrary type and carry that value through the existing event structure. The generated events, constraints, dependencies, and all other callbacks are unchanged. Existing callers continue to instantiate the result as unit, making this a backward-compatible and safe relaxation of the helper interface. Signed-off-by: Vladimir Murzin <vladimir.murzin@arm.com>
The generic lift_memop wrapper always discards the memory operation result and returns B.Next. That is correct for ordinary loads and stores, but not for GCS operations whose memory callbacks decide control flow. It caused GCS faults to be replaced by unconditional fall-through, and likewise prevented successful callbacks from carrying their own Next or branch state. Switch to direc use of do_lift_memop for GCSPOPM and GCSSS2 so their selected Fault or Next result is propagated. For GCSSS1, retain the result of both the successful register update and the fault assertion rather than mapping them to unit. GCSSS1 shares the CAS success/failure machinery with architectural CAS, so parameterise the common helper over its lifting function. Ordinary CAS continues through the existing lift_memop adapter and therefore keeps its established unconditional-next behaviour; GCSSS1 supplies a local adapter and can propagate its control flow result. Signed-off-by: Vladimir Murzin <vladimir.murzin@arm.com>
lift_shadow_stack duplicated an older subset of the AArch64 memory lifting path solely so BL, BLR, and RET could return their own control-flow result. Now that do_lift_memop accepts an explicit result transformer, the duplicate is unnecessary and risks diverging from future update in memory lifting path. Switch to do_lift_memop for GCS branch shadow-stack accesses. This retains their Jump or Fault result while reusing the common translation and permission checking machinery. Signed-off-by: Vladimir Murzin <vladimir.murzin@arm.com>
Collaborator
|
Thanks @murzinv , I'll take a look |
fsestini
reviewed
Aug 4, 2026
| in | ||
| let mv = read_reg_data rA ii in | ||
| do_cas quad Annot.N r ma mv mop_success mop_fail_with_wb mop_fail_no_wb false ii) | ||
| let lift_memop ?(tag = "") rA dir updatedb checked mop perms ma mv an ii = |
Collaborator
There was a problem hiding this comment.
This function always receives a ~tag parameter, so making it optional is not needed.
Suggested change
| let lift_memop ?(tag = "") rA dir updatedb checked mop perms ma mv an ii = | |
| let lift_memop ~tag rA dir updatedb checked mop perms ma mv an ii = |
| do_cas quad Annot.N r ma mv mop_success mop_fail_with_wb mop_fail_no_wb false ii) | ||
| let lift_memop ?(tag = "") rA dir updatedb checked mop perms ma mv an ii = | ||
| do_lift_memop ~tag rA dir updatedb checked mop perms ma mv an ii Fun.id DISide.Data in | ||
| do_cas_with (fun ~tag -> lift_memop ~tag) quad Annot.N r ma mv mop_success mop_fail_with_wb mop_fail_no_wb false ii) |
Collaborator
There was a problem hiding this comment.
Perhaps we could format this line so that it fits within 80-ish columns.
| (read_reg_ord r ii) | ||
| an | ||
| ii | ||
| Fun.id |
Collaborator
There was a problem hiding this comment.
Codex pointed out that using do_lift_memop here may not be sufficient if PAC is enabled (-variant pauth1 or -variant pauth2). Indeed the pac path of do_lift_memop ignores the branch argument, and lift_pac_virt discards the memory operation's result.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Opening it as a draft since: