Function with quantification in the precondition crashes with "variable i is not defined"

[viper-admin]

Created by @fpoli on 2019-05-06 13:05
Last updated on 2019-09-16 09:13

The following program crashes with Internal Error: variable i is not defined

predicate P(self: Ref)

function foo(s: Seq[Ref]): Bool 
    requires forall i: Int :: { s[i] } 0 <= i && i < |s| ==> P(s[i])
{
    true
}

‌

Exception:

Exception in thread "main" java.lang.RuntimeException: Internal Error: variable i is not defined.
	at scala.sys.package$.error(package.scala:26)
	at viper.carbon.verifier.Environment.get(Environment.scala:53)
	at viper.carbon.modules.impls.DefaultExpModule.translateLocalVar(DefaultExpModule.scala:285)
	at viper.carbon.modules.impls.DefaultExpModule.translateExp(DefaultExpModule.scala:68)
	at viper.carbon.modules.impls.DefaultSeqModule.t$1(DefaultSeqModule.scala:52)
	at viper.carbon.modules.impls.DefaultSeqModule.translateSeqExp(DefaultSeqModule.scala:73)
	at viper.carbon.modules.impls.DefaultExpModule.translateExp(DefaultExpModule.scala:258)
	at viper.carbon.modules.impls.DefaultHeapModule.$anonfun$translateLocation$1(DefaultHeapModule.scala:418)
	at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:233)
	at scala.collection.mutable.ResizableArray.foreach(ResizableArray.scala:58)
	at scala.collection.mutable.ResizableArray.foreach$(ResizableArray.scala:51)
	at scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:47)
	at scala.collection.TraversableLike.map(TraversableLike.scala:233)
	at scala.collection.TraversableLike.map$(TraversableLike.scala:226)
	at scala.collection.AbstractTraversable.map(Traversable.scala:104)
	at viper.carbon.modules.impls.DefaultHeapModule.translateLocation(DefaultHeapModule.scala:418)
	at viper.carbon.modules.impls.DefaultHeapModule.predicateTrigger(DefaultHeapModule.scala:386)
	at viper.carbon.modules.impls.DefaultFuncPredModule.$anonfun$definitionalAxiom$8(DefaultFuncPredModule.scala:265)
	at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:233)
	at scala.collection.mutable.ResizableArray.foreach(ResizableArray.scala:58)
	at scala.collection.mutable.ResizableArray.foreach$(ResizableArray.scala:51)
	at scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:47)
	at scala.collection.TraversableLike.map(TraversableLike.scala:233)
	at scala.collection.TraversableLike.map$(TraversableLike.scala:226)
	at scala.collection.AbstractTraversable.map(Traversable.scala:104)
	at viper.carbon.modules.impls.DefaultFuncPredModule.definitionalAxiom(DefaultFuncPredModule.scala:265)
	at viper.carbon.modules.impls.DefaultFuncPredModule.translateFunction(DefaultFuncPredModule.scala:198)
	at viper.carbon.modules.impls.DefaultMainModule.$anonfun$translate$3(DefaultMainModule.scala:65)
	at scala.collection.TraversableLike.$anonfun$flatMap$1(TraversableLike.scala:240)
	at scala.collection.mutable.ResizableArray.foreach(ResizableArray.scala:58)
	at scala.collection.mutable.ResizableArray.foreach$(ResizableArray.scala:51)
	at scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:47)
	at scala.collection.TraversableLike.flatMap(TraversableLike.scala:240)
	at scala.collection.TraversableLike.flatMap$(TraversableLike.scala:237)
	at scala.collection.AbstractTraversable.flatMap(Traversable.scala:104)
	at viper.carbon.modules.impls.DefaultMainModule.translate(DefaultMainModule.scala:65)
	at viper.carbon.CarbonVerifier.verify(CarbonVerifier.scala:134)
	at viper.silver.frontend.DefaultFrontend.verification(Frontend.scala:242)
	at viper.silver.frontend.DefaultFrontend.verification$(Frontend.scala:240)
	at viper.carbon.CarbonFrontend.verification(Carbon.scala:26)
	at viper.silver.frontend.DefaultPhases.$anonfun$phases$5(Frontend.scala:98)
	at viper.silver.frontend.Frontend.$anonfun$run$1(Frontend.scala:59)
	at viper.silver.frontend.Frontend.$anonfun$run$1$adapted(Frontend.scala:59)
	at scala.collection.immutable.List.foreach(List.scala:388)
	at viper.silver.frontend.Frontend.run(Frontend.scala:59)
	at viper.silver.frontend.Frontend.run$(Frontend.scala:58)
	at viper.carbon.CarbonFrontend.run(Carbon.scala:26)
	at viper.silver.frontend.SilFrontend.execute(SilFrontend.scala:152)
	at viper.silver.frontend.SilFrontend.execute$(SilFrontend.scala:130)
	at viper.carbon.CarbonFrontend.execute(Carbon.scala:26)
	at viper.carbon.Carbon$.main(Carbon.scala:20)
	at viper.carbon.Carbon.main(Carbon.scala)

[viper-admin]

@fpoli commented on 2019-05-20 08:31

Another program that causes a similar error:

domain Array {
    function loc(a : Array, i : Int) : Ref
}

field val : Int

method foo(s : Array)
    requires forall j: Int ::
        forall k: Int ::
            acc(loc(s, k).val)

java.lang.RuntimeException: Internal Error: variable k is not defined.
 trace:
  scala.sys.package$.error(package.scala:26)
  viper.carbon.verifier.Environment.get(Environment.scala:53)
  viper.carbon.modules.impls.DefaultExpModule.translateLocalVar(DefaultExpModule.scala:285)
  viper.carbon.modules.impls.DefaultExpModule.translateExp(DefaultExpModule.scala:68)
  viper.carbon.modules.impls.DefaultDomainModule.$anonfun$translateDomainFuncApp$1(DefaultDomainModule.scala:70)
  scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:233)
  scala.collection.mutable.ResizableArray.foreach(ResizableArray.scala:58)
  scala.collection.mutable.ResizableArray.foreach$(ResizableArray.scala:51)
  scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:47)
  scala.collection.TraversableLike.map(TraversableLike.scala:233)
  scala.collection.TraversableLike.map$(TraversableLike.scala:226)
  scala.collection.AbstractTraversable.map(Traversable.scala:104)
  viper.carbon.modules.impls.DefaultDomainModule.translateDomainFuncApp(DefaultDomainModule.scala:70)
  viper.carbon.modules.impls.DefaultExpModule.translateExp(DefaultExpModule.scala:247)
  viper.carbon.modules.impls.QuantifiedPermModule.translateInhale(QuantifiedPermModule.scala:885)
  viper.carbon.modules.impls.QuantifiedPermModule.inhaleAux(QuantifiedPermModule.scala:775)
  viper.carbon.modules.impls.QuantifiedPermModule.inhaleExp(QuantifiedPermModule.scala:726)
  viper.carbon.modules.impls.DefaultInhaleModule.$anonfun$inhaleConnective$1(DefaultInhaleModule.scala:87)
  scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:233)
  scala.collection.immutable.List.foreach(List.scala:388)
  scala.collection.generic.TraversableForwarder.foreach(TraversableForwarder.scala:34)
  scala.collection.generic.TraversableForwarder.foreach$(TraversableForwarder.scala:34)
  scala.collection.mutable.ListBuffer.foreach(ListBuffer.scala:43)
  scala.collection.TraversableLike.map(TraversableLike.scala:233)
  scala.collection.TraversableLike.map$(TraversableLike.scala:226)
  scala.collection.AbstractTraversable.map(Traversable.scala:104)
  viper.carbon.modules.impls.DefaultInhaleModule.inhaleConnective(DefaultInhaleModule.scala:87)
  viper.carbon.modules.impls.DefaultInhaleModule.$anonfun$inhale$1(DefaultInhaleModule.scala:40)
  scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:233)
  scala.collection.immutable.List.foreach(List.scala:388)
  scala.collection.TraversableLike.map(TraversableLike.scala:233)
  scala.collection.TraversableLike.map$(TraversableLike.scala:226)
  scala.collection.immutable.List.map(List.scala:294)
  viper.carbon.modules.impls.DefaultInhaleModule.inhale(DefaultInhaleModule.scala:40)
  viper.carbon.modules.impls.DefaultExpModule.checkDefinednessOfSpecAndInhale(DefaultExpModule.scala:511)
  viper.carbon.modules.ExpModule.$anonfun$checkDefinednessOfInhaleSpecAndInhale$1(ExpModule.scala:77)
  scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:233)
  scala.collection.mutable.ResizableArray.foreach(ResizableArray.scala:58)
  scala.collection.mutable.ResizableArray.foreach$(ResizableArray.scala:51)
  scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:47)
  scala.collection.TraversableLike.map(TraversableLike.scala:233)
  scala.collection.TraversableLike.map$(TraversableLike.scala:226)
  scala.collection.AbstractTraversable.map(Traversable.scala:104)
  viper.carbon.modules.ExpModule.checkDefinednessOfInhaleSpecAndInhale(ExpModule.scala:76)
  viper.carbon.modules.ExpModule.checkDefinednessOfInhaleSpecAndInhale$(ExpModule.scala:74)
  viper.carbon.modules.impls.DefaultExpModule.checkDefinednessOfInhaleSpecAndInhale(DefaultExpModule.scala:22)
  viper.carbon.modules.impls.DefaultMainModule.translateMethodDeclPre(DefaultMainModule.scala:189)
  viper.carbon.modules.impls.DefaultMainModule.translateMethodDecl(DefaultMainModule.scala:104)
  viper.carbon.modules.impls.DefaultMainModule.$anonfun$translate$5(DefaultMainModule.scala:67)
  scala.collection.TraversableLike.$anonfun$flatMap$1(TraversableLike.scala:240)
  scala.collection.mutable.ResizableArray.foreach(ResizableArray.scala:58)
  scala.collection.mutable.ResizableArray.foreach$(ResizableArray.scala:51)
  scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:47)
  scala.collection.TraversableLike.flatMap(TraversableLike.scala:240)
  scala.collection.TraversableLike.flatMap$(TraversableLike.scala:237)
  scala.collection.AbstractTraversable.flatMap(Traversable.scala:104)
  viper.carbon.modules.impls.DefaultMainModule.translate(DefaultMainModule.scala:67)
  viper.carbon.CarbonVerifier.verify(CarbonVerifier.scala:134)
  viper.silver.frontend.DefaultFrontend.verification(Frontend.scala:242)
  viper.silver.frontend.DefaultFrontend.verification$(Frontend.scala:240)
  viper.carbon.CarbonFrontend.verification(Carbon.scala:26)
  viper.server.ViperBackend.execute(VerificationWorker.scala:262)
  viper.server.VerificationWorker.run(VerificationWorker.scala:86)
  java.lang.Thread.run(Thread.java:748)

[viper-admin]

@gauravpartha on 2019-09-16 09:13:

• changed the assignee from (none) to @gauravpartha

[gauravpartha]

This issue has been fixed in commit 6598ba2.

Carbon adds triggers for function axioms using predicate accesses that appear in the function precondition or for predicate accesses that are unfolded in the function definition (when there is a recursive call to the function in the body of the unfolding expression). However, in cases where these predicate accesses contain bound variables, the trigger refers to variables that are not in scope and hence Carbon crashed.

In the fix, these triggers are only added if the corresponding predicate accesses do not refer to bound variables.

Side remark: The example posted in #271 (comment) was already ok before the commit and is orthogonal to what I described.

Here are some other examples that used to crash, but do not crash anymore.

Predicate access refers to a variable defined introduced by a let expression:

predicate P(self: Ref)

function foo(s: Seq[Ref]): Bool 
    requires let i == (5) in 0 <= i && i < |s| ==> P(s[i])
{
    true
}

Predicate being unfolded inside function definition refers to bound variable:

field elem: Int
field next: Ref

predicate list2(this: Ref, i: Int) {
  acc(this.elem) && acc(this.next) &&
  (this.next != null ==> list2(this.next, i))
}

function listLength2(l:Ref, i: Int) : Bool
  requires list2(l, i)
{ 
  forall j:Int ::
        i == j ==> unfolding list2(l,j) in l.next == null ? true :  listLength2(l.next, j) 
}