Make simplifier preserve (lack of) well-definedness

src/main/scala/viper/silver/ast/utility/Simplifier.scala

@@ -14,12 +14,21 @@ import viper.silver.ast.utility.rewriter._
  */
 object Simplifier {
 
+  def guaranteedToBeWellFormed(exp: Exp): Boolean = {
+    exp match {
+      case _: Mod | _: Div | _: FuncApp | _: MapLookup | _: SeqIndex => false
+      case _ => exp.subExps.forall(guaranteedToBeWellFormed)
+    }
+  }
+
   /**
-   * Simplify `expression`, in particular by making use of literals. For
-   * example, `!true` is replaced by `false`. Division and modulo with divisor
-   * 0 are not treated. Note that an expression with non-terminating evaluation due to endless recursion
-   * might be transformed to terminating expression.
-   */
+    * Simplify `expression`, in particular by making use of literals. For
+    * example, `!true` is replaced by `false`.
+    * The simplifier will not simplify parts of expressions that may not be well-defined.
+    * For example the expression `s[1] == s[1]` will not be simplified to `true`, because `s[1]` may not be defined.
+    * Note that an expression with non-terminating evaluation due to endless recursion
+    * might be transformed to terminating expression.
+    */
   def simplify(expression: Exp): Exp = {
     /* Always simplify children first, then treat parent. */
     StrategyBuilder.Slim[Node]({
@@ -29,21 +38,21 @@ object Simplifier {
 
       case And(TrueLit(), right) => right
       case And(left, TrueLit()) => left
-      case root @ And(FalseLit(), _) => FalseLit()(root.pos, root.info)
-      case root @ And(_, FalseLit()) => FalseLit()(root.pos, root.info)
+      case root @ And(FalseLit(), exp) if guaranteedToBeWellFormed(exp) => FalseLit()(root.pos, root.info)
+      case root @ And(exp, FalseLit()) if guaranteedToBeWellFormed(exp) => FalseLit()(root.pos, root.info)
 
       case Or(FalseLit(), right) => right
       case Or(left, FalseLit()) => left
-      case root @ Or(TrueLit(), _) => TrueLit()(root.pos, root.info)
-      case root @ Or(_, TrueLit()) => TrueLit()(root.pos, root.info)
+      case root @ Or(TrueLit(), exp) if guaranteedToBeWellFormed(exp) => TrueLit()(root.pos, root.info)
+      case root @ Or(exp, TrueLit()) if guaranteedToBeWellFormed(exp) => TrueLit()(root.pos, root.info)
 
-      case root @ Implies(FalseLit(), _) => TrueLit()(root.pos, root.info)
-      case root @ Implies(_, TrueLit()) => TrueLit()(root.pos, root.info)
+      case root @ Implies(FalseLit(), exp) if guaranteedToBeWellFormed(exp) => TrueLit()(root.pos, root.info)
+      case root @ Implies(exp, TrueLit()) if guaranteedToBeWellFormed(exp) => TrueLit()(root.pos, root.info)
       case root @ Implies(TrueLit(), FalseLit()) =>
         FalseLit()(root.pos, root.info)
       case Implies(TrueLit(), consequent) => consequent
 
-      case root @ EqCmp(left, right) if left == right => TrueLit()(root.pos, root.info)
+      case root @ EqCmp(left, right) if left == right && guaranteedToBeWellFormed(left) => TrueLit()(root.pos, root.info)
       case root @ EqCmp(BoolLit(left), BoolLit(right)) =>
         BoolLit(left == right)(root.pos, root.info)
       case root @ EqCmp(FalseLit(), right) => Not(right)(root.pos, root.info)
@@ -67,10 +76,8 @@ object Simplifier {
 
       case CondExp(TrueLit(), ifTrue, _) => ifTrue
       case CondExp(FalseLit(), _, ifFalse) => ifFalse
-      case root @ CondExp(_, FalseLit(), FalseLit()) =>
-        FalseLit()(root.pos, root.info)
-      case root @ CondExp(_, TrueLit(), TrueLit()) =>
-        TrueLit()(root.pos, root.info)
+      case CondExp(cond, ifTrue, ifFalse) if ifTrue == ifFalse && guaranteedToBeWellFormed(cond) =>
+        ifTrue
       case root @ CondExp(condition, FalseLit(), TrueLit()) =>
         Not(condition)(root.pos, root.info)
       case CondExp(condition, TrueLit(), FalseLit()) => condition

src/test/scala/SimplifierTests.scala

@@ -1,33 +1,42 @@
-// This Source Code Form is subject to the terms of the Mozilla Public
-// License, v. 2.0. If a copy of the MPL was not distributed with this
-// file, You can obtain one at http://mozilla.org/MPL/2.0/.
-//
-// Copyright (c) 2011-2019 ETH Zurich.
-
-import org.scalatest.funsuite.AnyFunSuite
-
-import scala.language.implicitConversions
-import org.scalatest.matchers.should.Matchers
-import viper.silver.ast._
-import viper.silver.ast.utility.Simplifier._
-
-class SimplifierTests extends AnyFunSuite with Matchers {
-  test("div") {
-    simplify(Div(0, 0)()) should be(Div(0, 0)())
-    simplify(Div(8, 2)()) should be(4: IntLit)
-  }
-
-  test("mod") {
-    simplify(Mod(0, 0)()) should be (Mod(0, 0)())
-    simplify(Mod(8, 3)()) should be (2: IntLit)
-    simplify(Mod(3, 8)()) should be (3: IntLit)
-    simplify(Mod(8, -3)()) should be (2: IntLit)
-    simplify(Mod(3, -8)()) should be (3: IntLit)
-    simplify(Mod(-8, 3)()) should be (1: IntLit)
-    simplify(Mod(-3, 8)()) should be (5: IntLit)
-    simplify(Mod(-8, -3)()) should be (1: IntLit)
-    simplify(Mod(-3, -8)()) should be (5: IntLit)
-  }
-
-  implicit def int2IntLit(i: Int): IntLit = IntLit(i)()
-}
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2019 ETH Zurich.
+
+import org.scalatest.funsuite.AnyFunSuite
+
+import scala.language.implicitConversions
+import org.scalatest.matchers.should.Matchers
+import viper.silver.ast._
+import viper.silver.ast.utility.Simplifier._
+
+class SimplifierTests extends AnyFunSuite with Matchers {
+  test("eq") {
+    val seq = LocalVar("someSeq", SeqType(Bool))()
+    val seqIndex = SeqIndex(
+      seq,
+      IntLit(1)()
+    )()
+    simplify(EqCmp(seqIndex, seqIndex)()) should be(EqCmp(seqIndex, seqIndex)())
+    simplify(EqCmp(seq, seq)()) should be(TrueLit()())
+  }
+  test("div") {
+    simplify(Div(0, 0)()) should be(Div(0, 0)())
+    simplify(Div(8, 2)()) should be(4: IntLit)
+  }
+
+  test("mod") {
+    simplify(Mod(0, 0)()) should be (Mod(0, 0)())
+    simplify(Mod(8, 3)()) should be (2: IntLit)
+    simplify(Mod(3, 8)()) should be (3: IntLit)
+    simplify(Mod(8, -3)()) should be (2: IntLit)
+    simplify(Mod(3, -8)()) should be (3: IntLit)
+    simplify(Mod(-8, 3)()) should be (1: IntLit)
+    simplify(Mod(-3, 8)()) should be (5: IntLit)
+    simplify(Mod(-8, -3)()) should be (1: IntLit)
+    simplify(Mod(-3, -8)()) should be (5: IntLit)
+  }
+
+  implicit def int2IntLit(i: Int): IntLit = IntLit(i)()
+}