Add tests to check semantics of pointer primitives

[danpoe]

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[danielsn]

Is this what we want? Or should it be non-det whether this is true?

In particular, is there a doc where all these expectations are laid out?

[thk123]

I think I agree with @danielsn, though I'm not clear what I as a user am trying to get out asserting on this property. But in general, seems safest for it to fail if you assert either way (in my mental model - you're asserting on UB, so whatever you assert, it should be false)

[danpoe]

@thk123 cbmc doesn't necessarily behave like that on UB. In general, one needs the appropriate check flags to be enabled to catch certain cases. For example, signed integer overflow is UB, though one needs to enable --signed-overflow-check to catch that case. Otherwise, the values will just wrap around.

In general though, I think it's a good idea for operations to be nondet in such cases as far as possible. So yes, I've changed the test to check for both the negated and the non-negated condition, and have specified that both should fail in the test.desc file.

[danielsn]

Would it be worth it check that an offset into the object also maintains the same object property?

[danpoe]

Added

[danielsn]

Is that expected? malloc is allowed to (and often does) reuse objects

[thk123]

I think this depends on how you plan to use _same_object? assert(same_object(p1, p2) certainly must fail. I think since this is an internal, it should be more exact, in this case, we know they are not the same object, they are the result of two separate mallocs. However, I would expect assert(p1 != p2) to fail, since is possible they could have the same address since the memory has been freed.

[danpoe]

Yes, assert(p1 != p2) should fail, though currently the way malloc is modelled in cbmc it doesn't reuse addresses.

[danielsn]

My overall question: is there a doc explaining the expected semantics of each primitive? When given a reference to (list not necessarily complete)

1. a global
2. a stack variable
3. a malloced variable
4. an unconstrained variable
5. a freed / out of scope variable
6. an out of bounds access on a valid pointer

[danielsn]

Also, what happens if we semi-constrain a variable? e.g.

int *x;
__CPROVER_assume(x != null); // or __CPROVER_assume(x == null)
assert(__CPROVER_dynamic_object(x));

[thk123]

Looks good - I think we need to check some of them are actually havoicing by adding asserts for either direction

[thk123]

I think I agree with @danielsn, though I'm not clear what I as a user am trying to get out asserting on this property. But in general, seems safest for it to fail if you assert either way (in my mental model - you're asserting on UB, so whatever you assert, it should be false)

[thk123]

I think this depends on how you plan to use _same_object? assert(same_object(p1, p2) certainly must fail. I think since this is an internal, it should be more exact, in this case, we know they are not the same object, they are the result of two separate mallocs. However, I would expect assert(p1 != p2) to fail, since is possible they could have the same address since the memory has been freed.

[thk123]

Thanks seems good (clang-format is complaining on travis)