Can prove nil-ness and non-nilness from struct predicate

[felixlinker]

Heya!

I'm currently teaching myself how to prove programs memory safe. In that pursuit, I wrote a little struct and tried to phrase a predicate expressing general memory-safety for a pointer to that struct. While testing, I noticed that I could prove the pointer to be non-nil from that predicate, which contradicted my intuition. After digging a bit further, I managed to create the following little example where I can prove both s == nil and s != nil when assuming the invariant. I would expect to not be able to prove either as I wanted my predicate to apply to both pointers that are nil and that are non-nil.

Either, there is a soundness error or (I guess?) my predicate is contradictory. I don't think, though, that my specification is contradictory, because h() does not verify and raises an error as expected.

Here the example:

type S struct {
	arr *[1]int
}

/*@
pred (s *S) Inv() {
	(s != nil ==> acc(&s.arr)) &&
	(s != nil && s.arr != nil ==> acc(s.arr))
}
@*/

func mk() (s *S) {
	return nil
}

// verifies (unexpected)
func f() {
	s := mk()
	// @ assume s.Inv()
	// @ unfold s.Inv()
	// @ assert s != nil
	return
}

// verifies (unexpected)
func g() {
	s := mk()
	// @ assume s.Inv()
	// @ unfold s.Inv()
	// @ assert s == nil
	return
}

// does not verify (expected)
func h() {
	var s *S = nil
	// @ assert s == nil
	// @ fold s.Inv()
	// @ unfold s.Inv()
	// @ assert s != nil
	return
}

[felixlinker]

When using inhale s.Inv() instead of assume s.Inv(), Gobra behaves as expected. I leave this issue open in case you decide to address it in documentation, but feel free to ignore and close.

[jcp19]

Hi Felix, good point. This is not a soundness problem, but I agree the semantics of impure assumes is confusing.

When you write assume P(x), where P(x) is a resource (i.e., either a predicate instance or a an access permission like acc(x)), Gobra interprets this as assume I already have permission to this resource. Thus, at the points you assume s.Inv(), Gobra simultaneously assumes it has permission to s.Inv(), and, at the same time, that it does not have permissions to anything (as no resources were transferred to the function via the precondition and no resources were obtained the assumption), leading to a contradiction (you can try this by asserting false right after the assumption). The inhale has a different reading: inhale s.Inv() means "add s.Inv() to the resources I already have. Doing so does not immediately lead to a contradiction, and thus, you get the expected behaviour.

On a side note, I feel like the impure assumes kind of contradict the monotonic view we have of the heap everywhere else in Viper/Gobra. This semantics for impure statements only makes sense to me in classical separation logics, where the assertions describe exactly what resources we currently have.

[jcp19]

Given how easy it is too misuse impure assumes, and how rarely they are useful, I would be happy to downgrade it to an experimental feature, i.e., one that is only enabled when a specific flag is passed to the gobra command. @bruggerl would that be fine by you?

[ArquintL]

I was having a similar thought (emit a warning or remove it altogether) as I don't think I've ever used it

[jcp19]

I was having a similar thought (emit a warning or remove it altogether) as I don't think I've ever used it

I think @bruggerl uses this feature in some of her experiments.