Skip to content

Rewrite base pointer refinement by pointee using trick from set #1983

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
sim642 wants to merge 1 commit into
base: master
Choose a base branch
from
+17 −7
Draft

Rewrite base pointer refinement by pointee using trick from set #1983

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 17 additions & 7 deletions src/analyses/baseInvariant.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,13 +117,13 @@ struct
let lvals = eval_lv ~man st (Mem (Lval lv), NoOffset) in
(* Additional offset of value being refined in Addr Offset type *)
let original_offset = convert_offset ~man st off in
let res = AD.fold (fun base_a acc ->
Option.bind acc (fun acc ->
let res = AD.fold (fun base_a st ->
Option.bind st (fun (st, ad) ->
match base_a with
| Addr base_mval ->
let (lval_a:VD.t) = Address (AD.singleton base_a) in
if M.tracing then M.tracel "inv" "Consider case of lval %a = %a" d_lval lv VD.pretty lval_a;
let st = set' lv lval_a st in
(* let st = set' lv lval_a st in *)
let orig = PreValueDomain.Addr.Mval.add_offset base_mval original_offset in
let old_val = get_mval ~man st orig None in
let old_val = VD.cast ~kind:Internal (Cilfacade.typeOfLval x) old_val in (* needed as the type of this pointer may be different *) (* TODO: proper castkind *)
Expand All @@ -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
Comment on lines 120 to 133
Copy link

Copilot AI Apr 8, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copilot uses AI. Check for mistakes.
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)
)
Comment on lines 124 to 139
Copy link

Copilot AI Apr 8, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copilot uses AI. Check for mistakes.
| _ -> None
)
) lvals (Some (D.bot ()))
) lvals (Some (st, AD.empty ()))
in
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
Copy link

Copilot AI Apr 8, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Suggested change
raise Analyses.Deadcode
contra st

Copilot uses AI. Check for mistakes.
else (
let d = set' lv (Address ad) d in
if AD.cardinal ad > 1 then
D.join st d
Copy link

Copilot AI Apr 8, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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).

Suggested change
D.join st d
let d = D.join st d in
set' lv (Address ad) d

Copilot uses AI. Check for mistakes.
else
d
)
) default res
| Var _, _
| Mem _, _ ->
default ()
Expand Down
Loading