This partial spec for list: error_with_none.txt, is crashing with the following error:
scala.MatchError: None (of class scala.None$)
at viper.silicon.rules.consumer$.evalAndAssert(Consumer.scala:947)
at viper.silicon.rules.consumer$.consumeTlc(Consumer.scala:853)
at viper.silicon.rules.consumer$.wrappedConsumeTlc(Consumer.scala:226)
at viper.silicon.rules.consumer$.consumeTlcs(Consumer.scala:181)
at viper.silicon.rules.consumer$.consumeR(Consumer.scala:196)
at viper.silicon.rules.consumer$.$anonfun$consumeTlc$5(Consumer.scala:326)
...
This is happening when statically verifying the appendLemmaAfterLoopBody function in the a == b case. One of the branches in this case should and does correctly statically fail when consuming a->val >= prev in the fold of sortedSegHelper. Consume calls evalAndAssert and then evalAndAssert calls evalpc to actually evaluate a->val >= prev. When failure happens in evalpc, the rest of the continuation is not evaluated and evalpc returns a failure verification result. This is fine, but the code in evalAndAssert in consume does not account for this case. It assumes execution always proceeds from evalpc and into the continuation, which creates a Some case for the return value match at the end of evalAndAssert. The return value is left as None for this match case if evalpc fails. Therefore, the solution here is to add an additional match case for the return value of evalAndAssert that handles the None (and thus failure) case of evalpc. When evalpc fails, evalAndAssert should return the failure verification result and None run-time checks.
jennalwise
commented
2 years ago
This partial spec for list: error_with_none.txt, is crashing with the following error:
This is happening when statically verifying the
appendLemmaAfterLoopBodyfunction in thea == bcase. One of the branches in this case should and does correctly statically fail when consuminga->val >= previn the fold ofsortedSegHelper.ConsumecallsevalAndAssertand thenevalAndAssertcallsevalpcto actually evaluatea->val >= prev. When failure happens inevalpc, the rest of the continuation is not evaluated andevalpcreturns a failure verification result. This is fine, but the code inevalAndAssertin consume does not account for this case. It assumes execution always proceeds fromevalpcand into the continuation, which creates aSomecase for the return value match at the end ofevalAndAssert. The return value is left asNonefor this match case ifevalpcfails. Therefore, the solution here is to add an additional match case for the return value ofevalAndAssertthat handles theNone(and thus failure) case ofevalpc. Whenevalpcfails,evalAndAssertshould return the failure verification result andNonerun-time checks.