Fix UInt8/UInt16 masking: switch scrutinee, ETernary, ECast#741
Fix UInt8/UInt16 masking: switch scrutinee, ETernary, ECast#741mtzguido wants to merge 1 commit into
Conversation
Three issues: 1- The ESwitch case passed the scrutinee through mk_expr, bypassing mk_arith masking. 2- mk_arith's catch-all marked ETernary as atomic, hiding non-atomic arithmetic branches from consumers (switch, comparisons). 3- ECast applied the cast to the widened uint32 value without masking, leaking overflow bits on widening casts. Fix: for UInt8/UInt16 switch scrutinees, route through mk_arith and mask non-atomic results. Add an ETernary case to mk_arith that recurses into both branches, returning is_atomic only when both are atomic. For ECast, route UInt8/UInt16 sources through mk_arith and mask before casting. Add SmallIntSwitch.fst, SmallIntTernary.fst, SmallIntCast.fst regression tests. Fixes FStarLang#707 Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
protz
left a comment
protz
left a comment
There was a problem hiding this comment.
Makes sense, thanks.
Thinking more about my comment regarding the ternary operator, e.g. (false ? f () : 1) >> 1. I think it should be have like a binary operator and I think w1 || w2 is correct.
| that every subexpression operates over unsigned int until the final | ||
| cast, or until a mask is needed to preserve semantics. *) | ||
| mk_expr env false false e, true, false (* C++: a constant that is wider than the intended type, but in an initializer list, is ok *) | ||
| | ETernary (c, t, f) -> |
There was a problem hiding this comment.
are you expecting things of the form return e1 + e2 ? e3 : e4?
There was a problem hiding this comment.
You mean with an operation in the condition? I don't think so, they must have bool type.
| let c = mk_expr env false false c in | ||
| let t, a1, w1 = mk_arith env t in | ||
| let f, a2, w2 = mk_arith env f in | ||
| CStar.Ternary (c, t, f), a1 && a2, w1 || w2 |
There was a problem hiding this comment.
if one of the branches was widened but not the other, shouldn't we widen both? feels like we should assert that w1 = w2 or do something
There was a problem hiding this comment.
this is a conservative choice so I think it is correct
| CStar.Op (K.op_of_poly_comp c) | ||
| | ECast (e, t) -> | ||
| CStar.Cast (mk_expr env false e, mk_type env t) | ||
| (* When the source is UInt8/UInt16 and contains arithmetic, the widened |
|
I have to say I'm a bit confused about the widening. It's only relevant for C++ initializers if I understand correctly? And it seems like an addition of u8 constants is not considered widened, but the addition would be promoted to int? This generates a bad diff in Eurydice, I'll look into it. I wonder if a different design for all this would be more desirable, actually: keep all casts explicit during AST->C*, and then do a pass to remove the superfluous ones. With enough rules, I think we could remove all the casts in the expression above. |
2 participants
Three issues:
1- The ESwitch case passed the scrutinee through mk_expr, bypassing
mk_arith masking.
2- mk_arith's catch-all marked ETernary as atomic, hiding non-atomic
arithmetic branches from consumers (switch, comparisons).
3- ECast applied the cast to the widened uint32 value without masking,
leaking overflow bits on widening casts.
Fix: for UInt8/UInt16 switch scrutinees, route through mk_arith and mask non-atomic results. Add an ETernary case to mk_arith that recurses into both branches, returning is_atomic only when both are atomic. For ECast, route UInt8/UInt16 sources through mk_arith and mask before casting.
Add SmallIntSwitch.fst, SmallIntTernary.fst, SmallIntCast.fst regression tests.
Fixes #707
--
Hi Jonathan, this is coauthored with Claude. It fixes #707 (which is legit) and a few other variants. The three tests fail before this patch. I'm not sure the style of the patch is that pleasant, since it seems easy to forget about this mk_arith dance and reintroduce variants of this bug later.