AutoCorres abstraction allows me to prove an invalid Hoare triple

[sdconsta]

Using AutoCorres 1.2 to abstract some C code, I discovered that I was able to prove some invalid Hoare triples. But I was not able to prove those same Hoare triples on the C-SIMPL output, which leads me to believe that this is specifically an AutoCorres issue. In brief, it seems that reading/writing from/to heap memory using a pointer, automatically asserts that the pointer is properly aligned and non-null.

I have provided code which demonstrates the issue. The function bar() increments a static pointer, which should not preserve the invariant c_guard on the pointer. Indeed, the invariant is unprovable. The function foo() also increments the pointer, but additionally writes to the pointed-to memory. This somehow makes the c_guard invariant provable.

Any assistance would be much appreciated. If this isn't the right place to post an AutoCorres issue, please let me know.

Scott Constable

Test.zip

[lsf37]

Hi Scott,

in the test file you're using the partial correctness Hoare triples that assume guards and asserts (which pointer validity is translated to).

To get the ones you want, you'd either prove "no_fail P f" independently, or you'd use the total correctness triples (validNF, i.e. the "\ .. \ f \ .. \!" syntax -- note the "!" at the end).

Cheers, Gerwin

[lsf37]

Just to explain why this strange division (we recently had a discussion about this internally as well): in our refinement proofs, no_fail is implied by the refinement we're proving, so it'd be wasted effort to prove it twice -- that's why there is a version of Hoare triples that assume them instead of asserting them, and it's also the reason that version is the default syntax.

[talsewell]

Um, on that issue, there's another aspect.

One useful but unusual feature of the "wp" proof approach is the way we've approached specialisation.

So, if you need to prove {P} f {Q and R}, you can build this out of proofs {P1} f {Q}, {P2} f {R}, etc.

These smaller proof fragments might seem overspecialised, but once you get down to the building blocks of your invariants, the fragments may actually be quite reusable.

Anyway, for that approach to work, it has to be partial validity. Otherwise every one of these proof fragments would need to establish the same correctness properties.

Cheers, Thomas.

On 22/03/17 10:30, Gerwin Klein wrote:

Just to explain why this strange division (we recently had a discussion about this internally as well): in our refinement proofs, no_fail is implied by the refinement we're proving, so it'd be wasted effort to prove it twice -- that's why there is a version of Hoare triples that assume them instead of asserting them, and it's also the reason that version is the default syntax.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://github.com/seL4/l4v/issues/18#issuecomment-288251859, or mute the threadhttps://github.com/notifications/unsubscribe-auth/ANQQ8BQK7t_A7nGQnDxnScsQNULdajxxks5roF2hgaJpZM4MkJB1.

[sdconsta]

Excellent explanations from both of you. This fully explains the behavior I was witnessing. Thanks!

Scott