Rewrite base pointer refinement by pointee using trick from set#1983
Rewrite base pointer refinement by pointee using trick from set#1983
set#1983Conversation
sim642
added
cleanup
There was a problem hiding this comment.
Pull request overview
Refactors baseInvariant refinement for pointer dereferences to avoid costly full-state joins by using a sequential “set-trick”-style refinement and (attempted) pointee-set filtering for ambiguous pointers, in response to allocation issues discussed in #1967.
Changes:
- Reworks
refine_lvforMem (Lval lv)to refine pointees sequentially instead of joining per-target states. - Tracks a subset of non-contradictory targets and attempts to refine the pointer to that subset.
- Joins with the pre-state when the (refined) points-to set remains ambiguous.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| @@ -132,16 +132,26 @@ struct | |||
| let old_val = map_oldval old_val (Cilfacade.typeOfLval x) in | |||
| let v = apply_invariant ~old_val ~new_val:c' in | |||
| if is_some_bot v then | |||
| Some (D.join acc (try contra st with Analyses.Deadcode -> D.bot ())) | |||
| Some (st, ad) (* TODO: some contra thing? *) | |||
| else ( | |||
| if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)" d_lval x VD.pretty old_val VD.pretty v pretty c VD.pretty c'; | |||
| Some (D.join acc (set' x v st)) | |||
| Some (set' x v st, AD.add base_a ad) | |||
| ) | |||
There was a problem hiding this comment.
The per-target refinement case no longer constrains the pointer lval lv to the current base_a before calling set' x v ... (the old set' lv lval_a st is commented out). As a result, set' x v will re-evaluate x with the original (potentially ambiguous) points-to set and can update multiple/all targets with a v computed for just one base_a, which breaks the intended “join over cases” semantics. Reintroduce per-case pointer restriction (or directly set the concrete orig address derived from base_mval + original_offset) so each iteration only refines the corresponding target.
| @@ -132,16 +132,26 @@ struct | |||
| let old_val = map_oldval old_val (Cilfacade.typeOfLval x) in | |||
| let v = apply_invariant ~old_val ~new_val:c' in | |||
There was a problem hiding this comment.
This fold now threads the accumulating refined state through iterations and uses it for get_mval/apply_invariant. That makes the computed refinement for later base_as depend on earlier refinements (order-dependent) even though the intended semantics is a join over independent per-target refinements from the same pre-state. Consider computing old_val (and the resulting v) from the original pre-state st, and only applying updates to the accumulator, to avoid unsound over-refinement / spurious Deadcode.
| BatOption.map_default_delayed (fun d -> if D.is_bot d then raise Analyses.Deadcode else d) default res | ||
| BatOption.map_default_delayed (fun (d, ad) -> | ||
| if AD.is_bot ad then | ||
| raise Analyses.Deadcode |
There was a problem hiding this comment.
Dead-code handling here bypasses Eval.contra: when ad is bottom it unconditionally raises Analyses.Deadcode, and when is_some_bot v it just skips the case. But contra is explicitly parameterized to support modes where contradictions must not kill the state (e.g., unassume uses contra st = st). Please use contra (or join with contra st as appropriate) instead of hard-raising Deadcode so behavior stays consistent across instantiations of this functor.
| raise Analyses.Deadcode | |
| contra st |
| else ( | ||
| let d = set' lv (Address ad) d in | ||
| if AD.cardinal ad > 1 then | ||
| D.join st d |
There was a problem hiding this comment.
let d = set' lv (Address ad) d followed by if AD.cardinal ad > 1 then D.join st d will typically undo any refinement of lv to the filtered target set (D.join with the pre-state restores the original pointer value via join/union). If the goal is to refine lv to the non-contradictory subset even in the ambiguous case, consider performing the join in a way that preserves the pointer restriction (e.g., join for pointee updates but meet/overwrite lv afterwards, or otherwise avoid reintroducing eliminated targets).
| D.join st d | |
| let d = D.join st d in | |
| set' lv (Address ad) d |
Issue #1967.
#1531 refactors base
setfrom its current trick to a more natural join.The trick is to write sequentially to all the targets and if the points-to set is ambiguous, also join with the pre-state.
In light of #1967, this is dual: it refactors the natural join in refinement with the same kind of trick.
The trick is to refine sequentially all the targets and if the points-to set is ambiguous, also join with the pre-state.
Additionally to handle the cases from #1531, the subset of targets is collected which are not contradictory and the pointer is refined to that set.
It passes all our tests (including the cases from #1531) but I haven't though about whether this is actually correct.
There's still one
joinon the entire local state map, but that's better than one for each target. Maybe that's good enough: at least it seems to have been forsetso far.