From e6d937655b652e9290e220583097ad3a6581280f Mon Sep 17 00:00:00 2001 From: Lars Date: Wed, 10 Jan 2024 14:34:38 +0100 Subject: [PATCH 1/6] Simplify rules for modulo --- res/universal/res/simplify/simplify.pvl | 5 +++++ 1 file changed, 5 insertions(+) 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 } From c985039efe49f25581c288cf925d382ba191c69b Mon Sep 17 00:00:00 2001 From: Lars Date: Wed, 10 Jan 2024 14:36:05 +0100 Subject: [PATCH 2/6] Nicer warning for no triggers --- src/col/vct/col/ast/node/NodeImpl.scala | 5 +++++ src/col/vct/col/print/Ctx.scala | 7 +++++-- src/rewrite/vct/rewrite/SimplifyNestedQuantifiers.scala | 4 ++-- 3 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/col/vct/col/ast/node/NodeImpl.scala b/src/col/vct/col/ast/node/NodeImpl.scala index 0f6f8f20a9..b110cca022 100644 --- a/src/col/vct/col/ast/node/NodeImpl.scala +++ b/src/col/vct/col/ast/node/NodeImpl.scala @@ -133,6 +133,11 @@ trait NodeImpl[G] extends Show { this: Node[G] => Group(show).toStringWithContext } + def toInlineStringWithoutHash: String = { + implicit val ctx = Ctx(withoutHash=true).namesIn(this).copy(width = Int.MaxValue) + Group(show).toStringWithContext + } + def highlight(node: Node[_]): HasContext = new HasContext { def contextText: String = { diff --git a/src/col/vct/col/print/Ctx.scala b/src/col/vct/col/print/Ctx.scala index f3012447da..1940f41b56 100644 --- a/src/col/vct/col/print/Ctx.scala +++ b/src/col/vct/col/print/Ctx.scala @@ -22,6 +22,7 @@ case class Ctx( tabWidth: Int = 4, names: Map[Declaration[_], String] = Map.empty, inSpec: Boolean = false, + withoutHash: Boolean = false, ) { def namesIn[G](node: Node[G]): Ctx = copy(names = { @@ -30,8 +31,10 @@ case class Ctx( namer.finish.asInstanceOf[Map[Declaration[_], String]] }) - def name(decl: Declaration[_]): String = - names.getOrElse(decl, s"${decl.o.getPreferredNameOrElse().ucamel}_${decl.hashCode()}") + def name(decl: Declaration[_]): String = { + val hash = if(withoutHash) "" else "_${decl.hashCode()}" + names.getOrElse(decl, s"${decl.o.getPreferredNameOrElse().ucamel}${hash}") + } def name(ref: Ref[_, _ <: Declaration[_]]): String = name(Try(ref.decl).getOrElse(return "?brokenref?")) diff --git a/src/rewrite/vct/rewrite/SimplifyNestedQuantifiers.scala b/src/rewrite/vct/rewrite/SimplifyNestedQuantifiers.scala index e18ac165a7..46d44549c3 100644 --- a/src/rewrite/vct/rewrite/SimplifyNestedQuantifiers.scala +++ b/src/rewrite/vct/rewrite/SimplifyNestedQuantifiers.scala @@ -63,9 +63,9 @@ case class SimplifyNestedQuantifiers[Pre <: Generation]() extends Rewriter[Pre] val res = rewriteDefault(e) res match { case Starall(_, Nil, body) if !body.exists { case InlinePattern(_, _, _) => true } => - logger.warn(f"The binder `${e.toInlineString}` contains no triggers") + logger.warn(f"The binder `${e.o.shortPositionText}`:`${e.toInlineStringWithoutHash}` contains no triggers") case Forall(_, Nil, body) if !body.exists { case InlinePattern(_, _, _) => true } => - logger.warn(f"The binder `${e.toInlineString}` contains no triggers") + logger.warn(f"The binder `${e.o.shortPositionText}`:`${e.toInlineStringWithoutHash}` contains no triggers") case _ => } res From 2e5172d1dd88fbb0cbba0d88857fb5a728104fb0 Mon Sep 17 00:00:00 2001 From: Lars Date: Wed, 10 Jan 2024 14:36:47 +0100 Subject: [PATCH 3/6] Resolve expressions earlier (solves rewrite issue) --- src/main/vct/main/stages/Transformation.scala | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) 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, From a5f27701b1ce73c56cc471203c773312b9229338 Mon Sep 17 00:00:00 2001 From: Lars Date: Wed, 10 Jan 2024 14:37:40 +0100 Subject: [PATCH 4/6] Better expression checker --- .../ast/util/ExpressionEqualityCheck.scala | 40 +++++++++++++++++-- 1 file changed, 36 insertions(+), 4 deletions(-) diff --git a/src/col/vct/col/ast/util/ExpressionEqualityCheck.scala b/src/col/vct/col/ast/util/ExpressionEqualityCheck.scala index f1e7ce1385..dbf06cb235 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 = { From 74a71ec3da22edf30462c26f810d9435844a1257 Mon Sep 17 00:00:00 2001 From: Lars Date: Mon, 26 Feb 2024 14:51:20 +0100 Subject: [PATCH 5/6] Have an inline origin that does not compress the line --- .../ast/util/ExpressionEqualityCheck.scala | 2 +- src/col/vct/col/origin/Origin.scala | 46 ++++++++++--------- src/col/vct/col/resolve/lang/Java.scala | 2 +- 3 files changed, 26 insertions(+), 24 deletions(-) diff --git a/src/col/vct/col/ast/util/ExpressionEqualityCheck.scala b/src/col/vct/col/ast/util/ExpressionEqualityCheck.scala index dbf06cb235..5b94a219c9 100644 --- a/src/col/vct/col/ast/util/ExpressionEqualityCheck.scala +++ b/src/col/vct/col/ast/util/ExpressionEqualityCheck.scala @@ -433,7 +433,7 @@ class AnnotationVariableInfoGetter[G]() { 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 _: Constant[G] => true case _ => false } } 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" From 29201bf5b3cae2363f6f23c1f2adf5192888ec27 Mon Sep 17 00:00:00 2001 From: Lars Date: Mon, 26 Feb 2024 14:56:23 +0100 Subject: [PATCH 6/6] Remove withoutHash stuff --- src/col/vct/col/ast/node/NodeImpl.scala | 5 ----- src/col/vct/col/print/Ctx.scala | 7 ++----- 2 files changed, 2 insertions(+), 10 deletions(-) diff --git a/src/col/vct/col/ast/node/NodeImpl.scala b/src/col/vct/col/ast/node/NodeImpl.scala index 5c530cd563..3953072d7d 100644 --- a/src/col/vct/col/ast/node/NodeImpl.scala +++ b/src/col/vct/col/ast/node/NodeImpl.scala @@ -157,11 +157,6 @@ trait NodeImpl[G] extends Show { this: Node[G] => Group(show).toStringWithContext } - def toInlineStringWithoutHash: String = { - implicit val ctx = Ctx(withoutHash=true).namesIn(this).copy(width = Int.MaxValue) - Group(show).toStringWithContext - } - def highlight(node: Node[_]): HasContext = new HasContext { def contextText: String = { diff --git a/src/col/vct/col/print/Ctx.scala b/src/col/vct/col/print/Ctx.scala index 1940f41b56..f3012447da 100644 --- a/src/col/vct/col/print/Ctx.scala +++ b/src/col/vct/col/print/Ctx.scala @@ -22,7 +22,6 @@ case class Ctx( tabWidth: Int = 4, names: Map[Declaration[_], String] = Map.empty, inSpec: Boolean = false, - withoutHash: Boolean = false, ) { def namesIn[G](node: Node[G]): Ctx = copy(names = { @@ -31,10 +30,8 @@ case class Ctx( namer.finish.asInstanceOf[Map[Declaration[_], String]] }) - def name(decl: Declaration[_]): String = { - val hash = if(withoutHash) "" else "_${decl.hashCode()}" - names.getOrElse(decl, s"${decl.o.getPreferredNameOrElse().ucamel}${hash}") - } + def name(decl: Declaration[_]): String = + names.getOrElse(decl, s"${decl.o.getPreferredNameOrElse().ucamel}_${decl.hashCode()}") def name(ref: Ref[_, _ <: Declaration[_]]): String = name(Try(ref.decl).getOrElse(return "?brokenref?"))