viperproject/silicon

Viper command line not giving termination error

BenjaminFrei opened this issue · 2 comments

BenjaminFrei commented

While trying to verify the Viper code with the command line, an error occurs in the newest version. In older version the code verifies, for example in the silicon commit 3b3b4be the code verifies. This does also not work with the new carbon version.

code:

import <decreases/all.vpr>

domain ListWellFoundedOrder[T] {

 
  axiom {
    forall y : List[T] :: {bounded(y)} bounded(y) 
  }


  axiom {
    forall xs : List[T] , y : T :: 
      decreasing(xs, Cons(y, xs)) 
  }

  axiom {
    forall xs : List[T], ys : List[T], zs : List[T] :: {decreasing(xs, ys), decreasing(ys, zs)}
      decreasing(xs, ys) && decreasing(ys, zs) ==> decreasing(xs, zs)
  }
}

adt List[T] {
  Nil()
  Cons(value : T, tail : List[T])
}

Output:
with the newest version of silicon, it gives this error message:

$ java -jar /home/benjamin_frei/Desktop/ETH/Bachelor_Thesis/silicon/target/scala-2.13/silicon.jar --z3Exe /usr/bin/z3 /home/benjamin_frei/Desktop/ETH/Bachelor_Thesis/Viper_examples/BachelorThesis/Book_Part1/ch6/chapter6viperhelp.vpr
Silicon 1.1-SNAPSHOT (8e3190bc)
Verification aborted exceptionally: scala.MatchError: List[T] (of class viper.silver.plugin.standard.adt.PAdtType)
scala.MatchError: List[T] (of class viper.silver.plugin.standard.adt.PAdtType)
	at viper.silver.plugin.standard.termination.TerminationPlugin.viper$silver$plugin$standard$termination$TerminationPlugin$$isNotExpectedConstrainedType$1(TerminationPlugin.scala:134)
	at viper.silver.plugin.standard.termination.TerminationPlugin$$anonfun$constrainsWellfoundednessUnexpectedly$2.applyOrElse(TerminationPlugin.scala:150)
	at viper.silver.plugin.standard.termination.TerminationPlugin$$anonfun$constrainsWellfoundednessUnexpectedly$2.applyOrElse(TerminationPlugin.scala:147)
	at scala.PartialFunction$Lifted.apply(PartialFunction.scala:338)
	at scala.PartialFunction$Lifted.apply(PartialFunction.scala:334)
	at viper.silver.ast.utility.Visitor$.$anonfun$shallowCollect$1(Visitor.scala:175)
	at scala.collection.immutable.List.flatMap(List.scala:293)
	at scala.collection.immutable.List.flatMap(List.scala:79)
	at viper.silver.ast.utility.Visitor$.shallowCollect$1(Visitor.scala:174)
	at viper.silver.ast.utility.Visitor$.$anonfun$shallowCollect$2(Visitor.scala:175)
	at scala.Option.fold(Option.scala:263)
	at viper.silver.ast.utility.Visitor$.$anonfun$shallowCollect$1(Visitor.scala:175)
	at scala.collection.immutable.List.flatMap(List.scala:293)
	at scala.collection.immutable.List.flatMap(List.scala:79)
	at viper.silver.ast.utility.Visitor$.shallowCollect$1(Visitor.scala:174)
	at viper.silver.ast.utility.Visitor$.$anonfun$shallowCollect$2(Visitor.scala:175)
	at scala.Option.fold(Option.scala:263)
	at viper.silver.ast.utility.Visitor$.$anonfun$shallowCollect$1(Visitor.scala:175)
	at scala.collection.immutable.List.flatMap(List.scala:293)
	at scala.collection.immutable.List.flatMap(List.scala:79)
	at viper.silver.ast.utility.Visitor$.shallowCollect$1(Visitor.scala:174)
	at viper.silver.ast.utility.Visitor$.shallowCollect(Visitor.scala:178)
	at viper.silver.parser.PNode.shallowCollect(ParseAst.scala:76)
	at viper.silver.parser.PNode.shallowCollect$(ParseAst.scala:75)
	at viper.silver.parser.PForall.shallowCollect(ParseAst.scala:914)
	at viper.silver.plugin.standard.termination.TerminationPlugin.constrainsWellfoundednessUnexpectedly(TerminationPlugin.scala:147)
	at viper.silver.plugin.standard.termination.TerminationPlugin.$anonfun$beforeTranslate$5(TerminationPlugin.scala:173)
	at scala.collection.immutable.List.flatMap(List.scala:293)
	at scala.collection.immutable.List.flatMap(List.scala:79)
	at viper.silver.plugin.standard.termination.TerminationPlugin.$anonfun$beforeTranslate$4(TerminationPlugin.scala:173)
	at viper.silver.plugin.standard.termination.TerminationPlugin.$anonfun$beforeTranslate$4$adapted(TerminationPlugin.scala:167)
	at scala.collection.immutable.List.foreach(List.scala:333)
	at viper.silver.plugin.standard.termination.TerminationPlugin.beforeTranslate(TerminationPlugin.scala:167)
	at viper.silver.plugin.SilverPluginManager.$anonfun$beforeTranslate$1(SilverPluginManager.scala:49)
	at viper.silver.plugin.SilverPluginManager.$anonfun$foldWithError$1(SilverPluginManager.scala:30)
	at scala.collection.immutable.ArraySeq.foldLeft(ArraySeq.scala:222)
	at viper.silver.plugin.SilverPluginManager.foldWithError(SilverPluginManager.scala:28)
	at viper.silver.plugin.SilverPluginManager.beforeTranslate(SilverPluginManager.scala:49)
	at viper.silver.frontend.SilFrontend.doTranslation(SilFrontend.scala:304)
	at viper.silver.frontend.SilFrontend.doTranslation$(SilFrontend.scala:302)
	at viper.silicon.SiliconFrontend.doTranslation(Silicon.scala:338)
	at viper.silicon.SiliconFrontend.doTranslation(Silicon.scala:338)
	at viper.silver.frontend.DefaultFrontend.translation(Frontend.scala:247)
	at viper.silver.frontend.DefaultFrontend.translation$(Frontend.scala:245)
	at viper.silicon.SiliconFrontend.translation(Silicon.scala:338)
	at viper.silver.frontend.DefaultPhases.$anonfun$Translation$1(Frontend.scala:115)
	at viper.silver.frontend.Frontend.$anonfun$runAllPhases$1(Frontend.scala:62)
	at viper.silver.frontend.Frontend.$anonfun$runAllPhases$1$adapted(Frontend.scala:60)
	at scala.collection.immutable.List.foreach(List.scala:333)
	at viper.silver.frontend.Frontend.runAllPhases(Frontend.scala:60)
	at viper.silver.frontend.Frontend.runAllPhases$(Frontend.scala:59)
	at viper.silicon.SiliconFrontend.runAllPhases(Silicon.scala:338)
	at viper.silver.frontend.SilFrontend.execute(SilFrontend.scala:173)
	at viper.silver.frontend.SilFrontend.execute$(SilFrontend.scala:150)
	at viper.silicon.SiliconFrontend.execute(Silicon.scala:338)
	at viper.silicon.SiliconRunnerInstance.runMain(Silicon.scala:391)
	at viper.silicon.SiliconRunner$.main(Silicon.scala:382)
	at viper.silicon.SiliconRunner.main(Silicon.scala)
jcp19 commented

The fact that this fails in both Silicon and Carbon may indicate that this is a Silver issue