Skip to content

Conversation

@karoliineh
Copy link
Member Author

Decisions from GobCon on 09.07:

What should happen when we write to a pointer that is either known or NullPtr?

  • a) Should we keep the NullPtr and join the known values
  • b) Or should we assume that if it is null, the program crashes anyways, and if it continues, the known value can only be the one that was written
  • Add b) as default behavior, make it configurable (for now), with option called sem.abort-on-null-deref

@sim642
Copy link
Member

sim642 commented Jul 16, 2024

We already have the option sem.null-pointer.dereference (for reading) and I think we decided to reuse that for writing. Its name and values might need to be changed though to match both reading and writing.

@michael-schwarz
Copy link
Member

This seems to have gotten stuck. Are there plans here?

@sim642
Copy link
Member

sim642 commented Mar 3, 2025

There was the matter of naming/describing the option but we discussed it and something seems to have been implemented. Not sure about the test failures though.

I think it makes sense to do this though.

Comment on lines +1825 to +1826
assert (not @@ AD.is_empty lval);
AD.fold (fun addr acc -> D.join (update_one addr st) acc) lval (D.bot ())
Copy link
Member

Choose a reason for hiding this comment

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

[...] Not sure about the test failures though.

The old CI runs seem to be gone, but I now merged master into this and locally at least two malloc_null tests fail.
The path-sensitivity of malloc_null analysis causes a scenario where a path has the malloc-ed pointer as {NULL}. Writing into that pointer, the assert doesn't fail because the points-to set is non-empty, but due to assume_none we end up returning D.bot ().
That bottom is a strange value: it appears live, but has lost all local variables state of base.

I suppose turning a D.bot () result into raise Deadcode could work here.
It does reveal a certain asymmetry with assume_none on NULL pointer reading: the latter doesn't raise Deadcode I think, but just assumes nothing changed.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bug cleanup Refactoring, clean-up

Projects

None yet

4 participants