[Termination Plugin] Extend Expr Support

src/main/scala/viper/silver/plugin/standard/termination/transformation/ExpTransformer.scala

@@ -6,7 +6,7 @@
 
 package viper.silver.plugin.standard.termination.transformation
 
-import viper.silver.ast.{Exp, Stmt, _}
+import viper.silver.ast.{And, Exp, Stmt, _}
 import viper.silver.ast.utility.Statements.EmptyStmt
 import viper.silver.ast.utility.ViperStrategy
 import viper.silver.ast.utility.rewriter.{ContextCustom, RepeatedStrategy, Strategy, Traverse}
@@ -15,7 +15,7 @@ import viper.silver.ast.utility.rewriter.{ContextCustom, RepeatedStrategy, Strat
  * A basic interface which helps to rewrite an expression (e.g. a function body) into a stmt (e.g. for a method body).
  * Some default transformations are already implemented.
  */
-trait ExpTransformer extends ErrorReporter {
+trait ExpTransformer extends ProgramManager with ErrorReporter {
 
   /**
    * Transforms an expression into a statement.
@@ -75,6 +75,29 @@ trait ExpTransformer extends ErrorReporter {
           Seqn(Seq(right), Nil)()
       }
       Seqn(Seq(left, rightSCE), Nil)()
+    case (ase: AnySetExp, c) => ase match {
+      case AnySetCardinality(s) => Seqn(Seq(transformExp(s, c)), Nil)(ase.pos)
+      case AnySetUnion(l, r) => Seqn(Seq(transformExp(l, c), transformExp(r, c)), Nil)(ase.pos)
+      case AnySetIntersection(l, r) => Seqn(Seq(transformExp(l, c), transformExp(r, c)), Nil)(ase.pos)
+      case AnySetSubset(l ,r) => Seqn(Seq(transformExp(l, c), transformExp(r, c)), Nil)(ase.pos)
+      case AnySetMinus(l, r) => Seqn(Seq(transformExp(l, c), transformExp(r, c)), Nil)(ase.pos)
+      case AnySetContains(elem, s) => Seqn(Seq(transformExp(elem, c), transformExp(s, c)), Nil)(ase.pos)
+      case MapDomain(base) => Seqn(Seq(transformExp(base, c)), Nil)(ase.pos)
+      case MapRange(base) => Seqn(Seq(transformExp(base, c)), Nil)(ase.pos)
+      case unsupportedExp => transformUnknownExp(unsupportedExp, c)
+    }
+    case (st: SetExp, c) => st match {
+      // note that AnySetExp are handled above
+      case ExplicitSet(elems) => Seqn(elems.map(transformExp(_, c)), Nil)(st.pos)
+      case EmptySet(_) => EmptyStmt
+      case unsupportedExp => transformUnknownExp(unsupportedExp, c)
+    }
+    case (ms: MultisetExp, c) => ms match {
+      // note that AnySetExp are handled above
+      case EmptyMultiset(_) => EmptyStmt
+      case ExplicitMultiset(elems) => Seqn(elems.map(transformExp(_, c)), Nil)(ms.pos)
+      case unsupportedExp => transformUnknownExp(unsupportedExp, c)
+    }
     case (sq: SeqExp, c) => sq match {
       case ExplicitSeq(elems) =>
         Seqn(elems.map(transformExp(_, c)), Nil)(sq.pos)
@@ -104,7 +127,6 @@ trait ExpTransformer extends ErrorReporter {
         Seqn(Seq(transformExp(s, c)), Nil)(sq.pos)
       case EmptySeq(_) => EmptyStmt
       case unsupportedExp => transformUnknownExp(unsupportedExp, c)
-        EmptyStmt
     }
     case (mp: MapExp, c) => mp match {
       case EmptyMap(_, _) => EmptyStmt
@@ -115,16 +137,12 @@ trait ExpTransformer extends ErrorReporter {
       case MapLookup(base, key) => Seqn(Seq(transformExp(base, c), transformExp(key, c)), Nil)(mp.pos)
       case MapUpdate(base, key, value) => Seqn(Seq(transformExp(base, c), transformExp(key, c), transformExp(value, c)), Nil)(mp.pos)
     }
-    case (st: ExplicitSet, c) =>
-      Seqn(st.elems.map(transformExp(_, c)), Nil)(st.pos)
-    case (mst: ExplicitMultiset, c) =>
-      Seqn(mst.elems.map(transformExp(_, c)), Nil)(mst.pos)
-    case (md: MapDomain, c) => Seqn(Seq(transformExp(md.base, c)), Nil)(md.pos)
-    case (mr: MapRange, c) => Seqn(Seq(transformExp(mr.base, c)), Nil)(mr.pos)
     case (u: UnExp, c) => transformExp(u.exp, c)
     case (_: Literal, _) => EmptyStmt
     case (_: AbstractLocalVar, _) => EmptyStmt
     case (_: AbstractConcretePerm, _) => EmptyStmt
+    case (_: WildcardPerm, _) => EmptyStmt
+    case (_: EpsilonPerm, _) => EmptyStmt
     case (_: LocationAccess, _) => EmptyStmt
 
     case (ap: AccessPredicate, c) =>
@@ -133,6 +151,20 @@ trait ExpTransformer extends ErrorReporter {
       val inhale = Inhale(ap)(ap.pos)
 
       Seqn(Seq(check, inhale), Nil)()
+    case (fa: Forall, c) =>
+      // we turn the quantified variables into local variables with arbitrary value and show that the expression holds
+      // for arbitrary values, which is similar to a forall introduction
+      val (freshDecls, transformedExp) = substituteWithFreshVars(fa.variables, fa.exp)
+      val expressionStmt = transformExp(transformedExp, c)
+      Seqn(Seq(expressionStmt), freshDecls)(fa.pos, fa.info, fa.errT)
+    case (ex: Exists, c) =>
+      // we perform existential elimination by retrieving witnesses for the quantified variables
+      val (freshDecls, transformedExp) = substituteWithFreshVars(ex.variables, ex.exp)
+      // we can't use an assume statement at this point because the `assume`s have already been rewritten
+      // furthermore, Viper only allows pure existentially quantified expressions
+      val inhaleWitnesses = Inhale(transformedExp)(ex.pos, ex.info, ex.errT)
+      val expressionStmt = transformExp(transformedExp, c)
+      Seqn(Seq(inhaleWitnesses, expressionStmt), freshDecls)(ex.pos, ex.info, ex.errT)
     case (fa: FuncLikeApp, c) =>
       val argStmts = fa.args.map(transformExp(_, c))
       Seqn(argStmts, Nil)()
@@ -182,6 +214,27 @@ trait ExpTransformer extends ErrorReporter {
     case Forall(_, _, exp) => Seq(exp)
   }
 
+  /**
+    * Turns `vars` into new local variable declarations with a unique name and replaces their occurrences in `exp`.
+    * The new local variables declarations and the transformed expression are returned
+    */
+  protected def substituteWithFreshVars(vars: Seq[LocalVarDecl], exp: Exp): (Seq[LocalVarDecl], Exp) = {
+    val declMapping = vars.map(decl => decl -> uniqueName(decl.name))
+    val freshDecls = declMapping.map {
+      case (oldDecl, freshName) => LocalVarDecl(freshName, oldDecl.typ)(oldDecl.pos, oldDecl.info, oldDecl.errT)
+    }
+    val transformedExp = exp.transform({
+      case v@LocalVar(name, typ) => declMapping
+        // check whether the local variable is in the map of variables that should be replaced:
+        .collectFirst { case (decl, freshName) if decl.name == name => freshName }
+        // replace it by a new local variable:
+        .map(freshName => LocalVar(freshName, typ)(v.pos, v.info, v.errT))
+        // keep the variable unchanged if no replacement should happen:
+        .getOrElse(v)
+    }, Traverse.TopDown)
+    (freshDecls, transformedExp)
+  }
+
 
   /**
    * The simplifyStmts Strategy can be used to simplify statements
@@ -209,6 +262,9 @@ trait ExpTransformer extends ErrorReporter {
       If(Not(c)(c.pos), els, EmptyStmt)(i.pos, i.info, i.errT)
     case i@If(c1, Seqn(Seq(If(c2, thn, EmptyStmt)), Nil), EmptyStmt) => // combine nested if clauses
       If(And(c1, c2)(), thn, EmptyStmt)(i.pos, i.info, i.errT)
+    case If(TrueLit(), thn, _) => thn // remove trivial If conditions (in particular effective together with the next 2 simplifications)
+    case And(TrueLit(), rhs) => rhs // simplify conjunctions
+    case And(lhs, TrueLit()) => lhs // simplify conjunctions
   }, Traverse.BottomUp)
     .repeat
 }

src/test/resources/termination/functions/expressions/exists.vpr

@@ -0,0 +1,51 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import <decreases/declaration.vpr>
+
+field f: Int
+
+function test(x: Ref): Bool
+    decreases
+{
+    //:: ExpectedOutput(termination.failed:termination.condition.false)
+    exists x2: Ref :: x == x2 && nonTerminating(x2)
+}
+
+function test2(): Bool
+    decreases
+{
+    // in general `partiallyTerminating` is non-terminating
+    //:: ExpectedOutput(termination.failed:termination.condition.false)
+    exists x2: Int :: partiallyTerminating(x2)
+}
+
+function test3(x: Int): Bool
+    decreases
+    requires x == 42
+{
+    // `partiallyTerminating` terminates for input `42` so this is fine
+    exists x2: Int :: x == x2 && partiallyTerminating(x2)
+}
+
+function test4(x: Int): Bool
+    decreases
+{
+    // in general `partiallyTerminating` is non-terminating
+    //:: ExpectedOutput(termination.failed:termination.condition.false)
+    (exists x2: Int :: x == x2) && partiallyTerminating(x)
+}
+
+function test5(x: Int): Bool
+    decreases
+{
+    // this is fine due to short-circuiting
+    (exists x2: Int :: x == x2 && x != x2) && partiallyTerminating(x)
+}
+
+function nonTerminating(x: Ref): Bool
+    decreases *
+
+function partiallyTerminating(x: Int): Bool
+    decreases if x == 42
+    decreases *

src/test/resources/termination/functions/expressions/forall.vpr

@@ -0,0 +1,25 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import <decreases/declaration.vpr>
+
+field f: Int
+
+function test(x: Ref): Bool
+    decreases
+    //:: ExpectedOutput(termination.failed:termination.condition.false)
+    requires forall x2: Ref :: x == x2 ==> acc(x2.f) && nonTerminating(x2)
+{
+    true
+}
+
+function test2(x: Ref): Bool
+    decreases
+    // this is fine because `nonTerminating(x2)` is not reachable
+    requires forall x2: Ref :: x == x2 ==> false && nonTerminating(x2)
+{
+    true
+}
+
+function nonTerminating(x: Ref): Bool
+    decreases *

src/test/resources/termination/functions/expressions/wildcard.vpr

@@ -0,0 +1,13 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+import <decreases/declaration.vpr>
+
+field f: Int
+
+function test(x: Ref): Bool
+    decreases
+    requires acc(x.f, wildcard)
+{
+    true
+}