[C-Semantics] Fixed important bug in r812

[John Regehr]

Pascal, out of curiosity, did this come up in real code or is it some 
sort of torture test?

John



On 6/9/11 9:38 AM, Chucky Ellison wrote:
> Grigore & Derek,
>
> First to address Grigore's question.  The standard says that it's okay
> to create a pointer +1 past the end of an array.  This is what &a[1] is
> doing when a[0] is the highest element in the array.  Since it's a valid
> pointer, I am allowed to compare it using == or != to other valid
> pointers. &a[1] == &b is essentially asking if the addresses are
> adjacent in memory.  There is a footnote in the standard (6.5.9) that
> says, "Two objects may be adjacent in memory because they are adjacent
> elements of a larger array or adjacent members of a structure with no
> padding between them, or because the implementation chose to place them
> so, even though they are unrelated."  So, on one implementation this
> could return true, on another, false.  In either case, the program is
> "correct", but it relies on unspecified behavior.
>
> About Derek's point.  We handle unspecified behavior in a number of
> ways, but the main goal is to handle it symbolically or
> nondeterministically.  Personally, I want to give this program
> nondeterministic behavior.  I feel like that would best capture what the
> standard is saying.  Obviously, two comparisons of the same objects
> would always result in the same thing, but there's no requirement this
> be consistent across all two objects declared similarly (that's my
> understanding).  If this weren't main and were a normal function, two
> separate calls to that function in a single implementation could return
> two different things (on a perverse implementation).
>
> This is difficult to do consistently.  Imagine searching the state space
> where one path returns true, and another returns false.  This "choice"
> needs to be remembered in a smart way, so that subsequent comparisons
> using the same objects are consistent.  We could do this, but it seems
> likely to me that there are examples with more subtlety where a complex
> logical conclusion needs to be drawn based on these equality choices.
> If it really were as simple as remembering these decisions, it would be
> easy for us to do.  I'm just not sure it's enough.
>
> So with all that, it makes sense to me to just have this be not-defined
> by my semantics than to try to capture that fidelity.  Still... if the
> program were this instead:
> int main(){
>       int a[1], b;
> &a[1] ==&b;
>      return 0;
>   }
> I don't think this is considered unspecified; it is a correct program
> with a single meaning.  My current semantics would still complain.
>
> -Chucky
>
>
> On Thu, Jun 9, 2011 at 10:54 AM, Derek M Jones <derek at knosof.co.uk
> <mailto:derek at knosof.co.uk>> wrote:
>
>     Chucky,
>
>      > int main(){
>      >    int a[1], b;
>      >    return&a[1] ==&b;
>      > }
>      >
>      > The program above was being given semantics, and would always
>     return false.
>      > However, it is possible for certain correct implementations to
>     return true,
>      > but we were missing this.
>     ...
>      > This means we no longer give semantics to possibly correct
>     programs like the
>      > one above (i.e., two live objects where a pointer is +1 OOB an
>     array), but
>
>     The behavior is unspecified and you should give the same behavior as
>     for other constructs having unspecified behavior.
>
>     --
>     Derek M. Jones                         tel: +44 (0) 1252 520 667
>     <tel:%2B44%20%280%29%201252%20520%20667>
>     Knowledge Software Ltd                 mailto:derek at knosof.co.uk
>     <mailto:derek at knosof.co.uk>
>     Source code analysis http://www.knosof.co.uk
>     _______________________________________________
>     c-semantics mailing list
>     c-semantics at cs.illinois.edu <mailto:c-semantics at cs.illinois.edu>
>     http://lists.cs.uiuc.edu/mailman/listinfo/c-semantics
>
>
>
>
> _______________________________________________
> c-semantics mailing list
> c-semantics at cs.illinois.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/c-semantics