Fix empty PVL enums causing verification failure

[wandernauta]

The PVL grammar (but not other front-ends) allows writing enumerations with no constants:

enum Empty { }

However, the toIntRange axiom that the EnumToDomain pass encodes for such an enum doesn't obviously hold, which causes verification of any program with such an enum to fail, for instance:

axiom (\forall Empty i; 0 <= {: empty1(i) :} && empty1(i) < 0);

This change makes it so that this specific axiom is omitted for empty enums.

Also adds a test that a snippet like the above should verify.

Front-ends are unchanged; for example, the Java frontend still rejects empty enums.

Pre-fix crash log for reference

[INFO] Start: VerCors (at 20:19:17)
[WARN] Caching is enabled, but results will be discarded, since there were uncommitted changes at compilation time.
[INFO] Done: VerCors (at 20:19:24, duration: 00:00:07)
vct.col.origin.BlameUnreachable: An error condition was reached, which should be statically unreachable. `requires true` is always satisfiable.. Inner failure:
 > ======================================
 > At classToRef:
 > --------------------------------------
 > The precondition of this contract may be unsatisfiable. If this is intentional, replace it with `requires false`. (https://utwente.nl/vercors#unsatisfiable)
 > ======================================
	at vct.col.origin.PanicBlame.blame(Blame.scala:1415)
	at vct.col.rewrite.CheckContractSatisfiability$AssertPassedNontrivialUnsatisfiable.blame(CheckContractSatisfiability.scala:48)
	at vct.col.rewrite.CheckContractSatisfiability$AssertPassedNontrivialUnsatisfiable.blame(CheckContractSatisfiability.scala:40)
	at vct.col.origin.ExpectedError.signalDone(ExpectedError.scala:32)
	at vct.main.stages.ExpectedErrors.$anonfun$run$1(ExpectedErrors.scala:16)
	at vct.main.stages.ExpectedErrors.$anonfun$run$1$adapted(ExpectedErrors.scala:16)
	at scala.collection.immutable.List.foreach(List.scala:333)
	at vct.main.stages.ExpectedErrors.run(ExpectedErrors.scala:16)
	at vct.main.stages.ExpectedErrors.run(ExpectedErrors.scala:12)
	at hre.stages.Stages.$anonfun$run$3(Stages.scala:104)
	at hre.stages.Stages.$anonfun$run$3$adapted(Stages.scala:101)
	at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576)
	at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:574)
	at scala.collection.AbstractIterable.foreach(Iterable.scala:933)
	at scala.collection.IterableOps$WithFilter.foreach(Iterable.scala:903)
	at hre.stages.Stages.$anonfun$run$1(Stages.scala:101)
	at hre.progress.task.NameSequenceTask.scope(NameSequenceTask.scala:16)
	at hre.progress.Progress$.stages(Progress.scala:47)
	at hre.stages.Stages.run(Stages.scala:98)
	at hre.stages.Stages.run$(Stages.scala:95)
	at hre.stages.StagesPair.run(Stages.scala:145)
	at vct.main.modes.Verify$.verifyWithOptions(Verify.scala:64)
	at vct.main.modes.Verify$.$anonfun$runOptions$3(Verify.scala:99)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.util.Time$.logTime(Time.scala:23)
	at vct.main.modes.Verify$.runOptions(Verify.scala:99)
	at vct.main.Main$.runMode(Main.scala:107)
	at vct.main.Main$.$anonfun$runOptions$3(Main.scala:100)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.middleware.Middleware$.using(Middleware.scala:78)
	at vct.main.Main$.$anonfun$runOptions$2(Main.scala:100)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.io.Watch$.booleanWithWatch(Watch.scala:58)
	at vct.main.Main$.$anonfun$runOptions$1(Main.scala:100)
	at scala.runtime.java8.JFunction0$mcI$sp.apply(JFunction0$mcI$sp.scala:17)
	at hre.middleware.Middleware$.using(Middleware.scala:78)
	at vct.main.Main$.runOptions(Main.scala:95)
	at vct.main.Main$.main(Main.scala:50)
	at vct.main.Main.main(Main.scala)
[ERROR] !*!*!*!*!*!*!*!*!*!*!*!
[ERROR] ! VerCors has crashed !
[ERROR] !*!*!*!*!*!*!*!*!*!*!*!

[bobismijnnaam]

This is a decent hotfix. The only thing I'm wondering about is whether it should actually be stronger, i.e. if you have an instance of EmptyEnum you should be able to prove false:

enum Empty {

}

void (Empty emp) {
  assert false;
}

I'm not sure how to encode that without viper/z3 picking up this fact without even mentioning Empty somewhere else... I'll inquire with the other vercors people and otherwise merge this PR. Of course if you have any ideas please share :)

[bobismijnnaam]

Actually, you can also assign null to enum-typed variables. So empty enums only allow you to prove false if you have a non-null reference to one. The axiom can instead be something like:

\forall EnumType e; e != null ==> ... e is in range ...

Would you mind trying this change out? It's especially important that it doesn't make (false) asserts in unrelated methods suddenly pass, but with the null check in place that should be fine.

[wandernauta]

Thanks for taking a look!

It looks like the fact that enums can be null is encoded as an Option, so e.g. the argument emp gets type Option<Empty>. So on the axioms for the adt Empty itself, it's already certain that we are not in the null case, right? So e != null would always be true, and true ==> ... e is in range ..., which is the axiom from before.

Indeed it would be nice if VerCors could prove no instances of Empty can exist, that feels neater. Perhaps it can be stated that Option<Empty> can only ever be none?

With the suggested change, a number of tests break (both Java and PVL). If I try to verify the program from above, the axiom becomes:

    axiom (\forall Empty i; asAny1(i) != asAny2(TNull.vNull()) ==> 0 <= Empty.empty1(i) && Empty.empty1(i) < 0);

I get:

[WARN] Possible viper bug: silver AST does not reparse when printing as text
[WARN] Cannot use function asAny1, which has preconditions, inside axiom ([email protected])
[WARN] Cannot use function asAny2, which has preconditions, inside axiom ([email protected])

I can find asAny1 and asAny2 in the COL, they don't look like they have preconditions, but they do have a signature; it feels like a type error, basically.

[superaxander]

Thanks for taking a look!

It looks like the fact that enums can be null is encoded as an Option, so e.g. the argument emp gets type Option<Empty>. So on the axioms for the adt Empty itself, it's already certain that we are not in the null case, right? So e != null would always be true, and true ==> ... e is in range ..., which is the axiom from before.

Indeed it would be nice if VerCors could prove no instances of Empty can exist, that feels neater. Perhaps it can be stated that Option<Empty> can only ever be none?

With the suggested change, a number of tests break (both Java and PVL). If I try to verify the program from above, the axiom becomes:

    axiom (\forall Empty i; asAny1(i) != asAny2(TNull.vNull()) ==> 0 <= Empty.empty1(i) && Empty.empty1(i) < 0);

I get:

[WARN] Possible viper bug: silver AST does not reparse when printing as text
[WARN] Cannot use function asAny1, which has preconditions, inside axiom ([email protected])
[WARN] Cannot use function asAny2, which has preconditions, inside axiom ([email protected])

I can find asAny1 and asAny2 in the COL, they don't look like they have preconditions, but they do have a signature; it feels like a type error, basically.

You can still refer to another type (i.e. Option[Empty]) in an ADT's axiom.

That warning comes from the decreases clauses on these functions. Recently those were changed to no longer count as preconditions for this check but we haven't changed to that viper version yet but it's fine to ignore those warnings for now.

[bobismijnnaam]

I think this requires a little bit more design work. Initially I intended for the COL enum type to be more of a mathematical enum type, meaning you can have an empty enum, and having an instance of that would allow you to prove false. Obviously I never got that far :) In addition, the implementation encodes enums as a domain, and (correct me if I'm wrong) in silicon/z3 domains are assumed to be inhabited. So that makes it a bit difficult to get the behaviour we want with a small fix. Or at least, in terms of design, it's not really clear to me what needs to change. In addition, Java allows empty enums, so that's actually a shortcoming of the frontend.

Writing the enum axioms over the type Option[Enum] instead of over just Enum is an interesting idea, but feels a bit fishy as well. Not sure if that's what we want. Maybe it is?

@wandernauta If you have time to redesign the enum implementation more thoroughly you are welcome to do so. It would be nice to have an internal enum type that is a bit more well founded. But otherwise, if we just want VerCors to behave sane without too much effort, I think it may be best do just disallow empty enums in PVL for now, like we do in the Java frontend. AFIAK I don't think anyone really depends on it. If you could change your PR to reflect that that'd be nice.

In addition, we should probably fix the SatCheck pass/default constructor generation code to generate a sane error message when a false axiom is added. (#1255)

[wandernauta]

I think it may be best do just disallow empty enums in PVL for now, like we do in the Java frontend.

This sounds good to me, especially since it doesn't hinder making enum Foo { } valid syntax at some later stage, to represent something that cannot exist.

Would it be sufficient to do this at the grammar level (so an empty enum would error saw }, expected IDENTIFIER, right here), or would you like to see a specific failure message, exactly like the Java frontend?

If you could change your PR to reflect that that'd be nice.

Will do!

[bobismijnnaam]

Probably the best place to do this is in PVLToCol.scala. You can find examples that use the fail method to reject unsupported syntaxes.

[bobismijnnaam]

Looks finished. Please confirm, then I'll merge it.

[wandernauta]

Yep! I think this should do it.

Thanks for your help!