search

viperproject / carbon

Verification-condition-generation-based verifier for the Viper intermediate verification language.
Mozilla Public License 2.0
30 stars 21 forks source link

Crash: cannot translate wildcard at an arbitrary position #169

Open viper-admin opened 7 years ago

viper-admin commented 7 years ago

Created by @vakaras on 2016-12-19 14:04 Last updated on 2017-06-19 10:02

For this program:

#!silver
field f1: Ref

field f2: Int

function foo(this: Ref): Ref
  requires this != null
{
  (unfolding acc(P2(this), wildcard) in this.f1)
}

predicate P1(this: Ref) {
  true
}

predicate P2(this: Ref) {
  acc(P1(this.f1), this.f2 / 100)
}

Carbon gives a stack trace:

#!console
> carbon --useNailgun /tmp/c2s.sil
carbon 1.0
(c) 2013 ETH Zurich

java.lang.RuntimeException: cannot translate wildcard at an arbitrary position (should only occur directly in an accessibility predicate)
        at scala.sys.package$.error(package.scala:27)
        at viper.carbon.modules.impls.QuantifiedPermModule.translatePerm(QuantifiedPermModule.scala:1180)
        at viper.carbon.modules.impls.QuantifiedPermModule.translatePerm(QuantifiedPermModule.scala:1194)
        at viper.carbon.modules.impls.QuantifiedPermModule.inhaleAux(QuantifiedPermModule.scala:734)
        at viper.carbon.modules.impls.QuantifiedPermModule.inhaleExp(QuantifiedPermModule.scala:715)
        at viper.carbon.modules.impls.DefaultInhaleModule$$anonfun$1.apply(DefaultInhaleModule.scala:61)
        at viper.carbon.modules.impls.DefaultInhaleModule$$anonfun$1.apply(DefaultInhaleModule.scala:61)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:245)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:245)
        at scala.collection.immutable.List.foreach(List.scala:381)
        at scala.collection.TraversableLike$class.map(TraversableLike.scala:245)
        at scala.collection.immutable.List.map(List.scala:285)
        at viper.carbon.modules.impls.DefaultInhaleModule.viper$carbon$modules$impls$DefaultInhaleModule$$inhaleConnective(DefaultInhaleModule.scala:61)
        at viper.carbon.modules.impls.DefaultInhaleModule$$anonfun$inhale$1.apply(DefaultInhaleModule.scala:32)
        at viper.carbon.modules.impls.DefaultInhaleModule$$anonfun$inhale$1.apply(DefaultInhaleModule.scala:32)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:245)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:245)
        at scala.collection.immutable.List.foreach(List.scala:381)
        at scala.collection.TraversableLike$class.map(TraversableLike.scala:245)
        at scala.collection.immutable.List.map(List.scala:285)
        at viper.carbon.modules.impls.DefaultInhaleModule.inhale(DefaultInhaleModule.scala:32)
        at viper.carbon.modules.impls.DefaultFuncPredModule.unfoldPredicate(DefaultFuncPredModule.scala:707)
        at viper.carbon.modules.impls.DefaultFuncPredModule.viper$carbon$modules$impls$DefaultFuncPredModule$$before$1(DefaultFuncPredModule.scala:626)
        at viper.carbon.modules.impls.DefaultFuncPredModule$$anonfun$partialCheckDefinedness$1.apply(DefaultFuncPredModule.scala:633)
        at viper.carbon.modules.impls.DefaultFuncPredModule$$anonfun$partialCheckDefinedness$1.apply(DefaultFuncPredModule.scala:633)
        at viper.carbon.modules.impls.DefaultExpModule$$anonfun$13.apply(DefaultExpModule.scala:299)
        at viper.carbon.modules.impls.DefaultExpModule$$anonfun$13.apply(DefaultExpModule.scala:299)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:245)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:245)
        at scala.collection.immutable.List.foreach(List.scala:381)
        at scala.collection.TraversableLike$class.map(TraversableLike.scala:245)
        at scala.collection.immutable.List.map(List.scala:285)
        at viper.carbon.modules.impls.DefaultExpModule.translate$1(DefaultExpModule.scala:299)
        at viper.carbon.modules.impls.DefaultExpModule.viper$carbon$modules$impls$DefaultExpModule$$checkDefinednessImpl(DefaultExpModule.scala:349)
        at viper.carbon.modules.impls.DefaultExpModule.checkDefinedness(DefaultExpModule.scala:268)
        at viper.carbon.modules.impls.DefaultFuncPredModule.checkFunctionDefinedness(DefaultFuncPredModule.scala:499)
        at viper.carbon.modules.impls.DefaultFuncPredModule.translateFunction(DefaultFuncPredModule.scala:196)
        at viper.carbon.modules.impls.DefaultMainModule$$anonfun$5.apply(DefaultMainModule.scala:64)
        at viper.carbon.modules.impls.DefaultMainModule$$anonfun$5.apply(DefaultMainModule.scala:64)
        at scala.collection.TraversableLike$$anonfun$flatMap$1.apply(TraversableLike.scala:252)
        at scala.collection.TraversableLike$$anonfun$flatMap$1.apply(TraversableLike.scala:252)
        at scala.collection.mutable.ResizableArray$class.foreach(ResizableArray.scala:59)
        at scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:48)
        at scala.collection.TraversableLike$class.flatMap(TraversableLike.scala:252)
        at scala.collection.AbstractTraversable.flatMap(Traversable.scala:104)
        at viper.carbon.modules.impls.DefaultMainModule.translate(DefaultMainModule.scala:64)
        at viper.carbon.CarbonVerifier.verify(CarbonVerifier.scala:128)
        at viper.silver.frontend.DefaultFrontend$class.verify(Frontend.scala:198)
        at viper.carbon.CarbonFrontend.verify(Carbon.scala:26)
        at viper.silver.frontend.SilFrontend$class.execute(SilFrontend.scala:115)
        at viper.carbon.CarbonFrontend.execute(Carbon.scala:26)
        at viper.carbon.Carbon$.main(Carbon.scala:17)
        at viper.carbon.Carbon.main(Carbon.scala)
        at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
        at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:57)
        at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
        at java.lang.reflect.Method.invoke(Method.java:606)
        at com.martiansoftware.nailgun.NGSession.run(Unknown Source)
viper-admin commented 7 years ago

@mschwerhoff commented on 2017-06-19 10:02

Also affects all/issues/silicon/0292.sil