Merge pull request #1127 from utwente-fmt/quick-fixes

Quick fixes

res/universal/res/simplify/simplify.pvl

@@ -44,6 +44,11 @@ axiom zero_mod { (∀int i; 0 % i == (0 then 1 % i;)) }
 
 axiom mod_def { (∀int num, int denom; (num/denom)*denom + (num%denom) == (num then 1/denom;)) }
 
+axiom mod_factor { (∀int num, int denom, int factor; (num+factor*denom) % denom == num%denom) }
+axiom mod_factor { (∀int num, int denom, int factor; (num+denom*factor) % denom == num%denom) }
+axiom mod_factor { (∀int num, int denom, int factor; (num-factor*denom) % denom == num%denom) }
+axiom mod_factor { (∀int num, int denom, int factor; (num-denom*factor) % denom == num%denom) }
+
 axiom not_true { !true == false }
 axiom not_false { !false == true }
 

src/col/vct/col/ast/util/ExpressionEqualityCheck.scala

@@ -2,6 +2,8 @@ package vct.col.ast.util
 
 import vct.col.ast.util.ExpressionEqualityCheck.isConstantInt
 import vct.col.ast._
+import vct.col.typerules.CoercionUtils
+import vct.col.util.AstBuildHelpers._
 import vct.result.VerificationError.UserError
 
 import scala.collection.mutable
@@ -79,6 +81,7 @@ class ExpressionEqualityCheck[G](info: Option[AnnotationVariableInfo[G]]) {
     case Mod(e1, e2) => for {i1 <- isConstantIntRecurse(e1); i2 <- isConstantIntRecurse(e2)} yield eucl_mod(i1, i2)
     case TruncDiv(e1, e2) => for {i1 <- isConstantIntRecurse(e1); i2 <- isConstantIntRecurse(e2)} yield i1 / i2
     case TruncMod(e1, e2) => for {i1 <- isConstantIntRecurse(e1); i2 <- isConstantIntRecurse(e2)} yield i1 % i2
+    case UMinus(e1) => for {i1 <- isConstantIntRecurse(e1)} yield -i1
 
     case BitAnd(e1, e2) => for {i1 <- isConstantIntRecurse(e1); i2 <- isConstantIntRecurse(e2)} yield i1 & i2
     case ComputationalAnd(e1, e2) => for {i1 <- isConstantIntRecurse(e1); i2 <- isConstantIntRecurse(e2)} yield i1 & i2
@@ -172,6 +175,7 @@ class ExpressionEqualityCheck[G](info: Option[AnnotationVariableInfo[G]]) {
   def isNonZero(e: Expr[G]):Boolean = e match {
     case v: Local[G] => info.exists(_.variableNotZero.contains(v))
     case _ => isConstantInt(e).getOrElse(0) != 0
+    case _ => lessThenEq(const(1)(e.o), e).getOrElse(false)
   }
 
   def unfoldComm[B <: BinExpr[G]](e: Expr[G])(implicit tag: ClassTag[B]): Seq[Expr[G]] = {
@@ -282,6 +286,9 @@ class ExpressionEqualityCheck[G](info: Option[AnnotationVariableInfo[G]]) {
       case (e1, name2: Local[G]) =>
         replaceVariable(name2, e1)
 
+      case (inv: MethodInvocation[G], _) if !inv.ref.decl.pure => false
+      case (_, inv: MethodInvocation[G]) if !inv.ref.decl.pure => false
+
       // In the general case, we are just interested in syntactic equality
       case (e1, e2) => e1 == e2
     }
@@ -311,7 +318,8 @@ case class AnnotationVariableInfo[G](variableEqualities: Map[Local[G], List[Expr
                                      variableSynonyms: Map[Local[G], Int], variableNotZero: Set[Local[G]],
                                      lessThanEqVars: Map[Local[G], Set[Local[G]]],
                                      upperBound: Map[Local[G], BigInt],
-                                     lowerBound: Map[Local[G], BigInt])
+                                     lowerBound: Map[Local[G], BigInt],
+                                     usefullConditions: mutable.ArrayBuffer[Expr[G]])
 
 /** This class gathers information about variables, such as:
   * `requires x == 0` and stores that x is equal to the value 0.
@@ -336,6 +344,8 @@ class AnnotationVariableInfoGetter[G]() {
   // lowerBound(v) = 5 Captures that variable v is greater than or equal to 5
   val lowerBound: mutable.Map[Local[G], BigInt] = mutable.Map()
 
+  val usefullConditions: mutable.ArrayBuffer[Expr[G]] = mutable.ArrayBuffer()
+
   def extractEqualities(e: Expr[G]): Unit = {
     e match{
       case Eq(e1, e2) =>
@@ -410,6 +420,24 @@ class AnnotationVariableInfoGetter[G]() {
     if(upperBound.contains(m) && upperBound(m) <= 0) lessThanEqVars.getOrElseUpdate(n, mutable.Set()).addOne(k)
   }
 
+  def isBool[G](e: Expr[G]) = {
+    CoercionUtils.getCoercion(e.t, TBool[G]()).isDefined
+  }
+
+  def isInt[G](e: Expr[G]) = {
+    CoercionUtils.getCoercion(e.t, TInt[G]()).isDefined
+  }
+  def isSimpleExpr(e: Expr[G]): Boolean = {
+    e match {
+      case e if(!isInt(e) && !isBool(e)) => false
+      case SeqMember(e1, Range(from, to)) => isSimpleExpr(e1) && isSimpleExpr(from) && isSimpleExpr(to)
+      case e: BinExpr[G] => isSimpleExpr(e.left) && isSimpleExpr(e.right)
+      case _: Local[G] => true
+      case _: Constant[G] => true
+      case _ => false
+    }
+  }
+
   def extractComparisons(e: Expr[G]): Unit = {
     e match{
       case Neq(e1, e2) =>
@@ -487,25 +515,29 @@ class AnnotationVariableInfoGetter[G]() {
     lessThanEqVars.clear()
     upperBound.clear()
     lowerBound.clear()
+    usefullConditions.clear()
 
     for(clause <- annotations){
       extractEqualities(clause)
     }
 
     val res = AnnotationVariableInfo[G](variableEqualities.view.mapValues(_.toList).toMap, variableValues.toMap,
       variableSynonyms.toMap, Set[Local[G]](), Map[Local[G], Set[Local[G]]](), Map[Local[G],BigInt](),
-      Map[Local[G],BigInt]())
+      Map[Local[G],BigInt](), usefullConditions)
     equalCheck = ExpressionEqualityCheck(Some(res))
 
     for(clause <- annotations){
-      extractComparisons(clause)
+      if(isSimpleExpr(clause)) {
+        extractComparisons(clause)
+        usefullConditions.addOne(clause)
+      }
     }
 
     distributeInfo()
 
     AnnotationVariableInfo(variableEqualities.view.mapValues(_.toList).toMap, variableValues.toMap,
       variableSynonyms.toMap, variableNotZero.toSet, lessThanEqVars.view.mapValues(_.toSet).toMap,
-      upperBound.toMap, lowerBound.toMap)
+      upperBound.toMap, lowerBound.toMap, usefullConditions)
   }
 
   def distributeInfo(): Unit = {

src/col/vct/col/origin/Origin.scala

@@ -40,7 +40,7 @@ trait OriginContent {
    * The part must not contain newlines. Consumers of the inline context should make sure to shorten breadcrumbs and
    * add an ellipsis where approriate, whereas the definition should not try to shorten the breadcrumb (within reason).
    */
-  def inlineContext(tail: Origin): Option[Seq[String]] = None
+  def inlineContext(tail: Origin, compress: Boolean = true): Option[Seq[String]] = None
 
   /**
    * Short description of the source position indicated by this origin. This should refer to the oldest cq original
@@ -96,17 +96,17 @@ case class SourceName(name: String) extends NameStrategy {
  */
 trait Context extends OriginContent {
   protected def contextHere(tail: Origin): (String, Origin)
-  protected def inlineContextHere(tail: Origin): (String, Origin)
+  protected def inlineContextHere(tail: Origin, compress: Boolean): (String, Origin)
   protected def shortPositionHere(tail: Origin): (String, Origin)
 
   override def context(tail: Origin): Option[Seq[String]] = {
     val (head, tailAfterContext) = contextHere(tail)
     Some(head +: tailAfterContext.context.getOrElse(Nil))
   }
 
-  override def inlineContext(tail: Origin): Option[Seq[String]] = {
-    val (head, tailAfterContext) = inlineContextHere(tail)
-    Some(head +: tailAfterContext.inlineContext.getOrElse(Nil))
+  override def inlineContext(tail: Origin, compress: Boolean = true): Option[Seq[String]] = {
+    val (head, tailAfterContext) = inlineContextHere(tail, compress)
+    Some(head +: tailAfterContext.inlineContext(compress).getOrElse(Nil))
   }
 
   override def shortPosition(tail: Origin): Option[String] = {
@@ -121,42 +121,42 @@ trait Context extends OriginContent {
  */
 case class LabelContext(label: String) extends Context {
   override protected def contextHere(tail: Origin): (String, Origin) = (s"At $label:", tail)
-  override protected def inlineContextHere(tail: Origin): (String, Origin) = (label, tail)
+  override protected def inlineContextHere(tail: Origin, compress: Boolean): (String, Origin) = (label, tail)
   override protected def shortPositionHere(tail: Origin): (String, Origin) = (label, tail)
 }
 
 trait Source extends Context {
   def positionContext(position: PositionRange): String
-  def inlinePositionContext(position: PositionRange): String
+  def inlinePositionContext(position: PositionRange, compress: Boolean = true): String
   protected def genericContext: String
   protected def genericInlineContext: String
   def genericShortPosition: String
 
   override protected def contextHere(tail: Origin): (String, Origin) = (genericContext, tail)
-  override protected def inlineContextHere(tail: Origin): (String, Origin) = (genericInlineContext, tail)
+  override protected def inlineContextHere(tail: Origin, compress: Boolean): (String, Origin) = (genericInlineContext, tail)
   override protected def shortPositionHere(tail: Origin): (String, Origin) = (genericShortPosition, tail)
 }
 
 case class ReadableOrigin(readable: Readable) extends Source {
   def positionContext(position: PositionRange): String =
     genericContext + "\n" + HR + InputOrigin.contextLines(readable, position)
-  def inlinePositionContext(position: PositionRange): String = InputOrigin.inlineContext(readable, position)
+  def inlinePositionContext(position: PositionRange, compress: Boolean): String = InputOrigin.inlineContext(readable, position, compress)
   override def genericContext: String = s"At ${readable.fileName}"
   override def genericInlineContext: String = s"${readable.fileName}"
   override def genericShortPosition: String = s"${readable.fileName}"
 }
 
 case class OriginFilename(filename: String) extends Source {
   def positionContext(position: PositionRange): String = genericContext
-  def inlinePositionContext(position: PositionRange): String = genericInlineContext
+  def inlinePositionContext(position: PositionRange, compress: Boolean): String = genericInlineContext
   override def genericContext: String = s"At $filename"
   override def genericInlineContext: String = s"$filename"
   override def genericShortPosition: String = s"$filename"
 }
 
 case class InlineBipContext(bipContext: String) extends Source {
   def positionContext(position: PositionRange): String = InputOrigin.contextLines(LiteralReadable("literal", bipContext), position)
-  def inlinePositionContext(position: PositionRange): String = InputOrigin.inlineContext(LiteralReadable("literal", bipContext), position)
+  def inlinePositionContext(position: PositionRange, compress: Boolean): String = InputOrigin.inlineContext(LiteralReadable("literal", bipContext), position)
   override def genericContext: String = s"From literal"
   override def genericInlineContext: String = "literal"
   override def genericShortPosition: String = "literal"
@@ -177,9 +177,9 @@ case class PositionRange(startLineIdx: Int, endLineIdx: Int, startEndColIdx: Opt
       case (_, None) => ("At broken position", tail)
     }
 
-  override protected def inlineContextHere(tail: Origin): (String, Origin) =
+  override protected def inlineContextHere(tail: Origin, compress: Boolean): (String, Origin) =
     tail.spanFind[Source] match {
-      case (_, Some((source, tail))) => (source.inlinePositionContext(this), tail)
+      case (_, Some((source, tail))) => (source.inlinePositionContext(this, compress), tail)
       case (_, None) => ("broken position", tail)
     }
 
@@ -271,11 +271,11 @@ final case class Origin(originContents: Seq[OriginContent]) extends Blame[Verifi
   def contextText: String =
     context.map(_.mkString("\n" + HR)).getOrElse("[unknown context]")
 
-  def inlineContext: Option[Seq[String]] =
-    originContents.headOption.flatMap(_.inlineContext(tail).orElse(tail.inlineContext))
+  def inlineContext(compress: Boolean = true): Option[Seq[String]] =
+    originContents.headOption.flatMap(_.inlineContext(tail, compress).orElse(tail.inlineContext(compress)))
 
   def inlineContextText: String =
-    inlineContext.map(_.mkString(" > ")).getOrElse("[unknown context]")
+    inlineContext(true).map(_.mkString(" > ")).getOrElse("[unknown context]")
 
   def shortPosition: Option[String] =
     originContents.headOption.flatMap(_.shortPosition(tail).orElse(tail.shortPosition))
@@ -435,20 +435,22 @@ object InputOrigin {
     }
   }
 
-  def inlineContext(readable: Readable, position: PositionRange): String =
-    readable.readLines().slice(position.startLineIdx, position.endLineIdx+1) match {
+  def inlineContext(readable: Readable, position: PositionRange, compress: Boolean = true): String = {
+    def compressF: String => String = if(compress) compressInlineText else identity[String]
+    readable.readLines().slice(position.startLineIdx, position.endLineIdx + 1) match {
       case Nil => "(empty source region)"
       case line +: Nil => position.startEndColIdx match {
-        case None => compressInlineText(line)
-        case Some((start, end)) => compressInlineText(line.slice(start, end))
+        case None => compressF(line)
+        case Some((start, end)) => compressF(line.slice(start, end))
       }
       case first +: moreLines =>
         val (context, last) = (moreLines.init, moreLines.last)
         position.startEndColIdx match {
-          case None => compressInlineText((first +: context :+ last).mkString("\n"))
-          case Some((start, end)) => compressInlineText((first.drop(start) +: context :+ last.take(end)).mkString("\n"))
+          case None => compressF((first +: context :+ last).mkString("\n"))
+          case Some((start, end)) => compressF((first.drop(start) +: context :+ last.take(end)).mkString("\n"))
         }
     }
+  }
 }
 
 case class BlameCollector() extends Blame[VerificationFailure] {

src/col/vct/col/resolve/lang/Java.scala

@@ -33,7 +33,7 @@ case object Java extends LazyLogging {
 
   object JRESource extends Source {
     override def positionContext(position: PositionRange): String = genericContext
-    override def inlinePositionContext(position: PositionRange): String = genericInlineContext
+    override def inlinePositionContext(position: PositionRange, compress: Boolean): String = genericInlineContext
     override protected def genericContext: String = "At node loaded reflectively from the JRE"
     override protected def genericInlineContext: String = "JRE"
     override def genericShortPosition: String = "JRE"

src/main/vct/main/stages/Transformation.scala

@@ -258,6 +258,7 @@ case class SilverTransformation
     ConstantifyFinalFields,
 
     // Resolve side effects including method invocations, for encodetrythrowsignals.
+    ResolveExpressionSideChecks,
     ResolveExpressionSideEffects,
     EncodeTryThrowSignals,
 
@@ -268,8 +269,6 @@ case class SilverTransformation
 
     CheckContractSatisfiability.withArg(checkSat),
 
-    ResolveExpressionSideChecks,
-
     DesugarCollectionOperators,
     EncodeNdIndex,
 

src/rewrite/vct/rewrite/SimplifyNestedQuantifiers.scala

@@ -63,9 +63,11 @@ case class SimplifyNestedQuantifiers[Pre <: Generation]() extends Rewriter[Pre]
             val res = rewriteDefault(e)
             res match {
               case Starall(_, Nil, body) if !body.exists { case InlinePattern(_, _, _) | InLinePatternLocation(_, _) => true} =>
-                logger.warn(f"The binder `${e.toInlineString}` contains no triggers")
+                val trigger = e.o.inlineContext(false).map(_.head).getOrElse("unknown context")
+                logger.warn(f"The binder `${e.o.shortPositionText}`:`${trigger} contains no triggers`")
               case Forall(_, Nil, body) if !body.exists { case InlinePattern(_, _, _) | InLinePatternLocation(_, _) => true } =>
-                logger.warn(f"The binder `${e.toInlineString}` contains no triggers")
+                val trigger = e.o.inlineContext(false).map(_.head).getOrElse("unknown context")
+                logger.warn(f"The binder `${e.o.shortPositionText}`:`${trigger} contains no triggers`")
               case _ =>
             }
             res