crux-mir: discriminate on MIR type during concretization
#1700
Conversation
Consistently use two-space indentation in `regEval` and put function argument types on separate lines.
NFCI - the argument is currently unused.
RyanGlScott
left a comment
RyanGlScott
left a comment
There was a problem hiding this comment.
This looks plausible at a glance, although it will be hard to truly evaluate this until a solution for #1666 is implemented.
| , Just Refl <- testEquality tpr (cfgReturnType cfg) | ||
| = bindFnHandle (cfgHandle cfg) $ UseOverride $ mkOverride' "concretize" tpr $ concretize symOnline | ||
| = let fns = cs ^. collection . M.functions | ||
| fn = fns Map.! textId name |
There was a problem hiding this comment.
Worth leaving a comment here about why this use of Map.! (a partial function) is expected to succeed. It might also be worth making this panic in the event that the lookup fails, as Map.! won't give a very helpful error message if it does fail.
| -- produce that same `tpr`. The type is in `Maybe` because there are cases | ||
| -- in which it's unknowable/inapplicable - for instance, in `goMirRef`, we | ||
| -- can't recover the `M.Ty` of the reference's `RefRoot`, only its | ||
| -- `TypeRepr`. |
There was a problem hiding this comment.
When we implement a solution for #1666, what will happen in the cases where the Maybe Ty argument is Nothing? Will we not be able to deduce type widths for array elements in such cases? If so, what are the ramifications of not being able to do so?
| go Nothing MirSliceRepr _ = | ||
| throwUnsupported sym "slice-like value of unknown MIR type" |
There was a problem hiding this comment.
Unlike other go Nothing cases, this one actually throws an error outright. Does this mean that concretization of slices can throw this error message in certain cases? Would it be worth adding a test for this?
This refactors
crux-mir'sMir.Overrides.regEvalto give access to the MIRTypeof a value being concretized, in addition to itsTypeRepr.This is largely meant to be a refactoring and functionality-preserving change to help give access to more type information at concretization time, to support work on #1666. However, it does restrict concretization a bit, as
regEvalconducts stricter typechecking of values being concretized. I've included an xfail test demonstrates one such bit of restriction on slices.Note to reviewers: this includes a fair amount of whitespace-only changes, so it's probably easier to review it commit by commit.