diff --git a/res/universal/res/simplify/simplify.pvl b/res/universal/res/simplify/simplify.pvl index dd4a486272..401fa1f4dd 100644 --- a/res/universal/res/simplify/simplify.pvl +++ b/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 } diff --git a/src/col/vct/col/ast/util/ExpressionEqualityCheck.scala b/src/col/vct/col/ast/util/ExpressionEqualityCheck.scala index f1e7ce1385..5b94a219c9 100644 --- a/src/col/vct/col/ast/util/ExpressionEqualityCheck.scala +++ b/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,6 +515,7 @@ class AnnotationVariableInfoGetter[G]() { lessThanEqVars.clear() upperBound.clear() lowerBound.clear() + usefullConditions.clear() for(clause <- annotations){ extractEqualities(clause) @@ -494,18 +523,21 @@ class AnnotationVariableInfoGetter[G]() { 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 = { diff --git a/src/col/vct/col/origin/Origin.scala b/src/col/vct/col/origin/Origin.scala index c67d35f2ba..53d40657b8 100644 --- a/src/col/vct/col/origin/Origin.scala +++ b/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,7 +96,7 @@ 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]] = { @@ -104,9 +104,9 @@ trait Context extends OriginContent { 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,26 +121,26 @@ 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}" @@ -148,7 +148,7 @@ case class ReadableOrigin(readable: Readable) extends Source { 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" @@ -156,7 +156,7 @@ case class OriginFilename(filename: String) extends Source { 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] { diff --git a/src/col/vct/col/resolve/lang/Java.scala b/src/col/vct/col/resolve/lang/Java.scala index bf46b73e1c..0aad2dc2a1 100644 --- a/src/col/vct/col/resolve/lang/Java.scala +++ b/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" diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala index c95973ca3a..4f3c8036b5 100644 --- a/src/main/vct/main/stages/Transformation.scala +++ b/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, diff --git a/src/rewrite/vct/rewrite/SimplifyNestedQuantifiers.scala b/src/rewrite/vct/rewrite/SimplifyNestedQuantifiers.scala index 01d3f79e35..67738b357a 100644 --- a/src/rewrite/vct/rewrite/SimplifyNestedQuantifiers.scala +++ b/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