(rewrite) const_prop: soundness & case support - #1006
Open
dc-mak wants to merge 3 commits into
Open
Conversation
kmemarian
reviewed
May 29, 2026
| | PEcatch_exceptional_condition _ (* may raise UB *) | ||
| | PEconv_int _ (* may raise impl-defined error *) | ||
| | PEcfunction _ (* function pointer lookup may fail *) | ||
| | PEcall _ (* may not terminate *) -> |
Collaborator
There was a problem hiding this comment.
I dont see how DeriveCap can UB, it's not in the memory monad and the reduction in Core_eval simply returns the integer value.
Other than that, I double checked the rest and I think you have it all covered. Just some nitpick if we care about the comments being more precise:
PEcallmay even also UB out.- for
PEcfunction, looking atCore_evalI think all thefail $ Illformed_program ...should be UBs (there are also already a UB, and there will still remain anerrorfor an illtyped expression, but that's irrelevant here). I'll make a PR to fix that in parallel.
Collaborator
Author
There was a problem hiding this comment.
So is it CapAssignValue that may UB here?
type pure_memop =
(* CHERI *) (* (integer, integer) -> integer *)
| DeriveCap of derivecap_op * bool (* is_signed *)
(* CHERI*) (* (integer, integer) -> integer (may result in UB) *)
| CapAssignValue
(* CHERI *) (* integer -> integer *)
| Ptr_tIntValue
(* Bytes *)
| ByteFromInt (* integer -> byte *)
| IntFromByte (* byte -> integer *)
Collaborator
|
The CI failure is weird, I thought it was because the opam cache had an old cmdliner that might not do the argument shortening but it's using |
dc-mak
force-pushed
the
copy-prop-sound
branch
2 times, most recently
from
May 29, 2026 18:51
2876c3b to
8eb270f
Compare
The previous analysis of which pexpr can be propagated was poorly explained and also unsound: values which could potentially not terminate, error, or cause UB in Core's strict setting should be left alone. This shouldn't affect the upcoming mem2reg because that only relies on symbols being propagated correctly.
This commit modifies the copy-prop to also propagate under case branches. It does so by adding a new switch to analyze_pat_pexpr so that it _doesn't_ change the type of the pattern to unit, and replace the scrutinee with Unit, to maintain consitency across branches. Woohoo! Might be nice to simplify the pattern but this could affect source location and annotations.
It started off as a copy-propagation pass just for symbols but it's long passed that now so it's been renamed as such to minimise further confusion.
dc-mak
changed the title
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.
The previous analysis of which pexpr can be propagated was poorly explained and also unsound: values which could potentially not terminate, error, or cause UB, or depend on the memory model, in Core's strict setting should be left alone.
This shouldn't affect the upcoming mem2reg because that only relies on symbols being propagated correctly.
The PR also adds support for const-prop across case branches.