Skip to content

MayPointTo is not subset of ReachableFrom #1175

Open
@sim642

Description

@sim642

In #1174 I made pthread_join invalidate its second argument with w instead of the default r_deep; w_deep; s_deep. Surprisingly, this caused test failures due to additional unknown pointer accesses if the pthread_join argument happens to be NULL.
This means that the MayPointTo for w accesses returns more addresses than ReachableFrom for w_deep, although I've always thought the former should be a subset of the latter as the latter is a recursive closure of the former. But apparently not?!

First, ReachableFrom for some reason excludes unknown pointers:

analyzer/src/analyses/base.ml

Lines 1288 to 1290 in 851c6b3

let a' = AD.remove Addr.UnknownPtr a in (* run reachable_vars without unknown just to be safe: TODO why? *)
let addrs = reachable_vars (Analyses.ask_of_ctx ctx) [a'] ctx.global ctx.local in
List.fold_left (AD.join) (AD.empty ()) addrs

Second, reachable_from_value for some reason excludes NULL pointers:
| Address adrs -> AD.remove Addr.NullPtr adrs

This explains why ReachableFrom NULL doesn't yield any accesses, but it doesn't explain why those exclusions are there in the first place.

In a4fb621 reachable_from_value was not just moved around but also the AD.remove Addr.NullPtr was introduced without explanation.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions