Merge pull request #810 from viperproject/keuscha/silicon-debugger

Silicon Debugging

src/main/scala/viper/silver/ast/Ast.scala

@@ -12,6 +12,7 @@ import pretty.FastPrettyPrinter
 import utility._
 import viper.silver.ast.utility.rewriter.Traverse.Traverse
 import viper.silver.ast.utility.rewriter.{Rewritable, StrategyBuilder, Traverse}
+import viper.silver.parser.PNode
 import viper.silver.verifier.errors.ErrorNode
 import viper.silver.verifier.{AbstractVerificationError, ConsistencyError, ErrorReason}
 
@@ -371,6 +372,11 @@ case object NoInfo extends Info {
   override val isCached = false
 }
 
+case class SourcePNodeInfo(sourcePNode: PNode) extends Info {
+  override val comment = Nil
+  override val isCached = false
+}
+
 case class AnnotationInfo(values: Map[String, Seq[String]]) extends Info {
   override val isCached = false
   override val comment = Nil

src/main/scala/viper/silver/ast/Expression.scala

@@ -15,6 +15,7 @@ import viper.silver.verifier.{ConsistencyError, VerificationResult}
 
 /** Expressions. */
 sealed trait Exp extends Hashable with Typed with Positioned with Infoed with TransformableErrors with PrettyExpression {
+  var simplified: Option[Exp] = None
   lazy val isPure = Expressions.isPure(this)
   def isHeapDependent(p: Program) = Expressions.isHeapDependent(this, p)
   def isTopLevelHeapDependent(p: Program) = Expressions.isTopLevelHeapDependent(this, p)
@@ -47,7 +48,7 @@ sealed trait Exp extends Hashable with Typed with Positioned with Infoed with Tr
    */
  // lazy val proofObligations = Expressions.proofObligations(this)
 
-  override def toString() = {
+  override lazy val toString = {
    // Carbon relies on expression pretty-printing resulting in a string without line breaks,
    // so for the special case of directly converting an expression to a string, we remove all line breaks
    // the pretty printer might have inserted.
@@ -360,6 +361,9 @@ case class PermSub(left: Exp, right: Exp)(val pos: Position = NoPosition, val in
 case class PermMul(left: Exp, right: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends DomainBinExp(PermMulOp) with PermExp with ForbiddenInTrigger
 case class IntPermMul(left: Exp, right: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends DomainBinExp(IntPermMulOp) with PermExp with ForbiddenInTrigger
 
+/** min expression used in the Silicon debugger */
+case class DebugPermMin(left: Exp, right: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends DomainBinExp(DebugPermMinOp) with PermExp with ForbiddenInTrigger
+
 // Comparison expressions
 case class PermLtCmp(left: Exp, right: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends DomainBinExp(PermLtOp) with ForbiddenInTrigger
 case class PermLeCmp(left: Exp, right: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends DomainBinExp(PermLeOp) with ForbiddenInTrigger
@@ -512,6 +516,12 @@ case class LabelledOld(exp: Exp, oldLabel: String)(val pos: Position = NoPositio
       Consistency.checkPure(exp)
 }
 
+/** Old expression that are used in the Silicon debugger. */
+case class DebugLabelledOld(exp: Exp, oldLabel: String)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends OldExp {
+  override lazy val check : Seq[ConsistencyError] =
+    Consistency.checkPure(exp)
+}
+
 case object LabelledOld {
   val LhsOldLabel = "lhs"
 }
@@ -713,6 +723,13 @@ case class Result(typ: Type)(val pos: Position = NoPosition, val info: Info = No
   lazy val name = "result"
 }
 
+/** A special local variable with a version for Silicon debugging */
+case class LocalVarWithVersion(name: String, typ: Type)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends AbstractLocalVar with Lhs {
+  def nameWithoutVersion = name.substring(0, name.lastIndexOf("@"))
+  override lazy val check: Seq[ConsistencyError] =
+    if (!Consistency.validUserDefinedIdentifier(name)) Seq(ConsistencyError("Local var name must be valid identifier.", pos)) else Seq()
+}
+
 // --- Mathematical sequences
 
 /**

src/main/scala/viper/silver/ast/Program.scala

@@ -729,6 +729,7 @@ case object ModOp extends ProdOp("%") with IntBinOp with IntDomainFunc
 case object PermAddOp extends SumOp("+") with PermBinOp with PermDomainFunc
 case object PermSubOp extends SumOp("-") with PermBinOp with PermDomainFunc
 case object PermMulOp extends ProdOp("*") with PermBinOp with PermDomainFunc
+case object DebugPermMinOp extends SumOp("min") with PermBinOp with PermDomainFunc
 case object IntPermMulOp extends ProdOp("*") with BinOp with PermDomainFunc {
   lazy val leftTyp = Int
   lazy val rightTyp = Perm

src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala

@@ -775,6 +775,8 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
         text("old") <> parens(show(exp))
       case LabelledOld(exp,label) =>
         text("old") <> brackets(label) <> parens(show(exp))
+      case DebugLabelledOld(exp, label) =>
+        text("old") <> brackets(label) <> parens(show(exp))
       case Let(v, exp, body) =>
         parens(text("let") <+> text(v.name) <+> "==" <> nest(defaultIndent, line <> parens(show(exp))) <+>
           "in" <> nest(defaultIndent, line <> show(body)))
@@ -891,6 +893,7 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter
 
       case null => uninitialized
       case u: PrettyUnaryExpression => showPrettyUnaryExp(u)
+      case DebugPermMin(e0, e1) => text("min") <> parens(show(e0) <> "," <+> show(e1))
       case b: PrettyBinaryExpression => showPrettyBinaryExp(b)
       case e: ExtensionExp => e.prettyPrint
       case _ => sys.error(s"unknown expression: ${e.getClass}")

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

@@ -127,7 +127,7 @@ object ImpureAssumeRewriter {
     val conds: Seq[Exp] =
       contextWithoutRcv
         .map(c => c._1._1.replace((c._1._2 zip rcv).toMap[Exp, Exp]))
-        .map(viper.silver.ast.utility.Simplifier.simplify)
+        .map(e => viper.silver.ast.utility.Simplifier.simplify(e))
 
     if (context.isEmpty) {
       assert(conds.isEmpty)

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

@@ -28,8 +28,8 @@ object Permissions {
 
   def multiplyExpByPerm(e: Exp, permFactor: Exp) : Exp = {
     assert(permFactor.typ == Perm,
-           "Internal error: attempted to permission-scale expression " + e.toString() +
-               " by non-permission-typed expression " + permFactor.toString())
+           "Internal error: attempted to permission-scale expression " + e.toString +
+               " by non-permission-typed expression " + permFactor.toString)
 
     if(permFactor.isInstanceOf[FullPerm])
       e

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

@@ -9,6 +9,7 @@ package viper.silver.ast.utility
 import viper.silver.ast.utility.Statements.EmptyStmt
 import viper.silver.ast._
 import viper.silver.ast.utility.rewriter._
+import viper.silver.utility.Common.Rational
 
 /**
  * An implementation for simplifications on the Viper AST.
@@ -21,109 +22,164 @@ object Simplifier {
    * 0 are not treated. Note that an expression with non-terminating evaluation due to endless recursion
    * might be transformed to terminating expression.
    */
-  def simplify[N <: Node](n: N): N = {
-    /* Always simplify children first, then treat parent. */
-    StrategyBuilder.Slim[Node]({
+  def simplify[N <: Node](n: N, assumeWelldefinedness: Boolean = false): N = {
+
+    val simplifySingle: PartialFunction[Node, Node] = {
       // expression simplifications
-      case root @ Not(BoolLit(literal)) =>
+      case root: Exp if root.simplified.isDefined =>
+        root.simplified.get
+      case root@Not(BoolLit(literal)) =>
         BoolLit(!literal)(root.pos, root.info)
       case Not(Not(single)) => single
+      case root@Not(EqCmp(a, b)) => NeCmp(a, b)(root.pos, root.info)
+      case root@Not(NeCmp(a, b)) => EqCmp(a, b)(root.pos, root.info)
+      case root@Not(GtCmp(a, b)) => LeCmp(a, b)(root.pos, root.info)
+      case root@Not(GeCmp(a, b)) => LtCmp(a, b)(root.pos, root.info)
+      case root@Not(LtCmp(a, b)) => GeCmp(a, b)(root.pos, root.info)
+      case root@Not(LeCmp(a, b)) => GtCmp(a, b)(root.pos, root.info)
 
       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(), _) => FalseLit()(root.pos, root.info)
+      case root@And(_, FalseLit()) => 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(), _) => TrueLit()(root.pos, root.info)
+      case root@Or(_, TrueLit()) => 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(TrueLit(), FalseLit()) =>
-        FalseLit()(root.pos, root.info)
+      case root@Implies(FalseLit(), _) => TrueLit()(root.pos, root.info)
+      case Implies(_, tl@TrueLit()) if assumeWelldefinedness => tl
       case Implies(TrueLit(), consequent) => consequent
+      case root@Implies(FalseLit(), _) => TrueLit()(root.pos, root.info)
+      case root@Implies(l1, Implies(l2, r)) => Implies(And(l1, l2)(), r)(root.pos, root.info)
 
-      // ME: Disabled since it is not equivalent in case the expression is not well-defined.
       // TODO: Consider checking if Expressions.proofObligations(left) is empty (requires adding the program as parameter).
-      // case root @ EqCmp(left, right) if left == right => TrueLit()(root.pos, root.info)
-      case root @ EqCmp(BoolLit(left), BoolLit(right)) =>
+      case root@EqCmp(left, right) if assumeWelldefinedness && left == right => 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)
-      case root @ EqCmp(left, FalseLit()) => Not(left)(root.pos, root.info)
+      case root@EqCmp(FalseLit(), right) => Not(right)(root.pos, root.info)
+      case root@EqCmp(left, FalseLit()) => Not(left)(root.pos, root.info)
       case EqCmp(TrueLit(), right) => right
       case EqCmp(left, TrueLit()) => left
-      case root @ EqCmp(IntLit(left), IntLit(right)) =>
+      case root@EqCmp(IntLit(left), IntLit(right)) =>
         BoolLit(left == right)(root.pos, root.info)
-      case root @ EqCmp(NullLit(), NullLit()) => TrueLit()(root.pos, root.info)
+      case root@EqCmp(NullLit(), NullLit()) => TrueLit()(root.pos, root.info)
 
-      case root @ NeCmp(BoolLit(left), BoolLit(right)) =>
+      case root@NeCmp(BoolLit(left), BoolLit(right)) =>
         BoolLit(left != right)(root.pos, root.info)
       case NeCmp(FalseLit(), right) => right
       case NeCmp(left, FalseLit()) => left
-      case root @ NeCmp(TrueLit(), right) => Not(right)(root.pos, root.info)
-      case root @ NeCmp(left, TrueLit()) => Not(left)(root.pos, root.info)
-      case root @ NeCmp(IntLit(left), IntLit(right)) =>
+      case root@NeCmp(TrueLit(), right) => Not(right)(root.pos, root.info)
+      case root@NeCmp(left, TrueLit()) => Not(left)(root.pos, root.info)
+      case root@NeCmp(IntLit(left), IntLit(right)) =>
         BoolLit(left != right)(root.pos, root.info)
-      case root @ NeCmp(NullLit(), NullLit()) =>
+      case root@NeCmp(NullLit(), NullLit()) =>
         FalseLit()(root.pos, root.info)
+      case root@NeCmp(left, right) if assumeWelldefinedness && left == right => FalseLit()(root.pos, root.info)
 
       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 root @ CondExp(condition, FalseLit(), TrueLit()) =>
+      case CondExp(_, ifTrue, ifFalse) if assumeWelldefinedness && ifTrue == ifFalse =>
+        ifTrue
+      case root@CondExp(condition, FalseLit(), TrueLit()) =>
         Not(condition)(root.pos, root.info)
       case CondExp(condition, TrueLit(), FalseLit()) => condition
-      case root @ CondExp(condition, FalseLit(), ifFalse) =>
+      case root@CondExp(condition, FalseLit(), ifFalse) =>
         And(Not(condition)(), ifFalse)(root.pos, root.info)
-      case root @ CondExp(condition, TrueLit(), ifFalse) =>
-        if(ifFalse.isPure) {
+      case root@CondExp(condition, TrueLit(), ifFalse) =>
+        if (ifFalse.isPure) {
           Or(condition, ifFalse)(root.pos, root.info)
         } else {
           Implies(Not(condition)(), ifFalse)(root.pos, root.info)
         }
-      case root @ CondExp(condition, ifTrue, FalseLit()) =>
+      case root@CondExp(condition, ifTrue, FalseLit()) =>
         And(condition, ifTrue)(root.pos, root.info)
-      case root @ CondExp(condition, ifTrue, TrueLit()) =>
+      case root@CondExp(condition, ifTrue, TrueLit()) =>
         Implies(condition, ifTrue)(root.pos, root.info)
 
-      case root @ Forall(_, _, BoolLit(literal)) =>
+      case root@Forall(_, _, BoolLit(literal)) =>
         BoolLit(literal)(root.pos, root.info)
-      case root @ Exists(_, _, BoolLit(literal)) =>
+      case root@Exists(_, _, BoolLit(literal)) =>
         BoolLit(literal)(root.pos, root.info)
 
-      case root @ Minus(IntLit(literal)) => IntLit(-literal)(root.pos, root.info)
+      case root@Minus(IntLit(literal)) => IntLit(-literal)(root.pos, root.info)
       case Minus(Minus(single)) => single
 
       case PermMinus(PermMinus(single)) => single
+      case PermMul(fst, FullPerm()) => fst
+      case PermMul(FullPerm(), snd) => snd
+      case root@PermMul(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        val product = Rational(a, b) * Rational(c, d)
+        FractionalPerm(IntLit(product.numerator)(root.pos, root.info), IntLit(product.denominator)(root.pos, root.info))(root.pos, root.info)
+      case PermMul(_, np@NoPerm()) if assumeWelldefinedness => np
+      case PermMul(np@NoPerm(), _) if assumeWelldefinedness => np
+
+      case PermMul(wc@WildcardPerm(), _) if assumeWelldefinedness => wc
+      case PermMul(_, wc@WildcardPerm()) if assumeWelldefinedness => wc
+
+      case root@PermGeCmp(a, b) if assumeWelldefinedness && a == b => TrueLit()(root.pos, root.info)
+      case root@PermLeCmp(a, b) if assumeWelldefinedness && a == b => TrueLit()(root.pos, root.info)
+      case root@PermGtCmp(a, b) if assumeWelldefinedness && a == b => FalseLit()(root.pos, root.info)
+      case root@PermLtCmp(a, b) if assumeWelldefinedness && a == b => FalseLit()(root.pos, root.info)
+
+      case root@PermGtCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) > Rational(c, d))(root.pos, root.info)
+      case root@PermGeCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) >= Rational(c, d))(root.pos, root.info)
+      case root@PermLtCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) < Rational(c, d))(root.pos, root.info)
+      case root@PermLeCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) <= Rational(c, d))(root.pos, root.info)
+      case root@EqCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) == Rational(c, d))(root.pos, root.info)
+      case root@NeCmp(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        BoolLit(Rational(a, b) != Rational(c, d))(root.pos, root.info)
+
+      case root@PermLeCmp(NoPerm(), WildcardPerm()) =>
+        TrueLit()(root.pos, root.info)
+      case root@NeCmp(WildcardPerm(), NoPerm()) =>
+        TrueLit()(root.pos, root.info)
 
-      case root @ GeCmp(IntLit(left), IntLit(right)) =>
+      case DebugPermMin(e0@AnyPermLiteral(a, b), e1@AnyPermLiteral(c, d)) =>
+        if (Rational(a, b) < Rational(c, d)) {
+          e0
+        } else {
+          e1
+        }
+      case root@PermSub(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        val diff = Rational(a, b) - Rational(c, d)
+        FractionalPerm(IntLit(diff.numerator)(root.pos, root.info), IntLit(diff.denominator)(root.pos, root.info))(root.pos, root.info)
+      case root@PermAdd(AnyPermLiteral(a, b), AnyPermLiteral(c, d)) =>
+        val sum = Rational(a, b) + Rational(c, d)
+        FractionalPerm(IntLit(sum.numerator)(root.pos, root.info), IntLit(sum.denominator)(root.pos, root.info))(root.pos, root.info)
+      case PermAdd(NoPerm(), rhs) => rhs
+      case PermAdd(lhs, NoPerm()) => lhs
+      case PermSub(lhs, NoPerm()) => lhs
+
+      case root@GeCmp(IntLit(left), IntLit(right)) =>
         BoolLit(left >= right)(root.pos, root.info)
-      case root @ GtCmp(IntLit(left), IntLit(right)) =>
+      case root@GtCmp(IntLit(left), IntLit(right)) =>
         BoolLit(left > right)(root.pos, root.info)
-      case root @ LeCmp(IntLit(left), IntLit(right)) =>
+      case root@LeCmp(IntLit(left), IntLit(right)) =>
         BoolLit(left <= right)(root.pos, root.info)
-      case root @ LtCmp(IntLit(left), IntLit(right)) =>
+      case root@LtCmp(IntLit(left), IntLit(right)) =>
         BoolLit(left < right)(root.pos, root.info)
 
-      case root @ Add(IntLit(left), IntLit(right)) =>
+      case root@Add(IntLit(left), IntLit(right)) =>
         IntLit(left + right)(root.pos, root.info)
-      case root @ Sub(IntLit(left), IntLit(right)) =>
+      case root@Sub(IntLit(left), IntLit(right)) =>
         IntLit(left - right)(root.pos, root.info)
-      case root @ Mul(IntLit(left), IntLit(right)) =>
+      case root@Mul(IntLit(left), IntLit(right)) =>
         IntLit(left * right)(root.pos, root.info)
       /* In the general case, Viper uses the SMT division and modulo. Scala's division is not in-sync with SMT division.
          For nonnegative dividends and divisors, all used division and modulo definitions coincide. So, in order to not
          not make any assumptions on the SMT division, division and modulo are simplified only if the dividend and divisor
          are nonnegative. Also see Carbon PR #448.
        */
-      case root @ Div(IntLit(left), IntLit(right)) if left >= bigIntZero && right > bigIntZero =>
+      case root@Div(IntLit(left), IntLit(right)) if left >= bigIntZero && right > bigIntZero =>
         IntLit(left / right)(root.pos, root.info)
-      case root @ Mod(IntLit(left), IntLit(right)) if left >= bigIntZero && right > bigIntZero =>
+      case root@Mod(IntLit(left), IntLit(right)) if left >= bigIntZero && right > bigIntZero =>
         IntLit(left % right)(root.pos, root.info)
 
       // statement simplifications
@@ -134,8 +190,38 @@ object Simplifier {
       case If(_, EmptyStmt, EmptyStmt) => EmptyStmt // remove empty If clause
       case If(TrueLit(), thn, _) => thn // remove trivial If conditions
       case If(FalseLit(), _, els) => els // remove trivial If conditions
-    }, Traverse.BottomUp) execute n
+    }
+
+    val simplifyAndCache = new PartialFunction[Node, Node] {
+      def apply(n: Node): Node = {
+        val simplified = simplifySingle.applyOrElse(n, (nn: Node) => nn)
+        n match {
+          case e: Exp =>
+            e.simplified = Some(simplified.asInstanceOf[Exp])
+            simplified.asInstanceOf[Exp].simplified = Some(simplified.asInstanceOf[Exp])
+          case _ =>
+        }
+        simplified
+      }
+
+      def isDefinedAt(n: Node): Boolean = n.isInstanceOf[Exp] || simplifySingle.isDefinedAt(n)
+    }
+
+    /* Always simplify children first, then treat parent. */
+    StrategyBuilder.Slim[Node](simplifyAndCache, Traverse.BottomUp).recurseFunc({
+      case e: Exp if e.simplified.isDefined => Nil
+    }) execute n
   }
 
   private val bigIntZero = BigInt(0)
+  private val bigIntOne = BigInt(1)
+
+  object AnyPermLiteral {
+    def unapply(p: Exp): Option[(BigInt, BigInt)] = p match {
+      case FullPerm() => Some((bigIntOne, bigIntOne))
+      case NoPerm() => Some((bigIntZero, bigIntOne))
+      case FractionalPerm(IntLit(n), IntLit(d)) => Some((n, d))
+      case _ => None
+    }
+  }
 }