From 2cbf9687126e5cac74040dfaee81189fbdc52ae2 Mon Sep 17 00:00:00 2001 From: "Felix A. Wolf" Date: Fri, 15 Mar 2024 00:43:38 +0100 Subject: [PATCH 1/7] added distinction of opaque functions --- .../silver/ast/utility/chopper/Chopper.scala | 83 ++++++++++++------- 1 file changed, 54 insertions(+), 29 deletions(-) diff --git a/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala b/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala index c4b3b7222..eb7e0970c 100644 --- a/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala +++ b/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala @@ -7,7 +7,7 @@ package viper.silver.ast.utility.chopper import viper.silver.ast -import viper.silver.ast.QuantifiedExp +import viper.silver.ast.{AnnotationInfo, QuantifiedExp} import viper.silver.ast.utility.{Nodes, Visitor} import scala.annotation.tailrec @@ -517,6 +517,7 @@ object Penalty { method: Int, methodSpec: Int, function: Int, + functionSig: Int, predicate: Int, predicateSig: Int, field: Int, @@ -534,7 +535,7 @@ object Penalty { * Followed by predicates with a body and domain axioms. */ val defaultPenaltyConfig: PenaltyConfig = PenaltyConfig( - method = 0, methodSpec = 0, function = 20, predicate = 10, predicateSig = 2, field = 1, + method = 0, methodSpec = 0, function = 20, functionSig = 5, predicate = 10, predicateSig = 2, field = 1, domainType = 1, domainFunction = 1, domainAxiom = 5, sharedThreshold = 50 ) @@ -544,7 +545,8 @@ object Penalty { override def penalty(xs: Vertices.Vertex): Int = xs match { case _: Vertices.Method => conf.method case _: Vertices.MethodSpec => conf.methodSpec - case _: Vertices.Function => conf.function + case _: Vertices.FunctionBody => conf.function + case _: Vertices.FunctionSig => conf.functionSig case _: Vertices.PredicateBody => conf.predicate case _: Vertices.PredicateSig => conf.predicateSig case _: Vertices.Field => conf.field @@ -670,19 +672,22 @@ object Vertices { * */ sealed trait Vertex + /** Represents a Viper method member without the body. */ + case class MethodSpec(methodName: String) extends Vertex + /** Represents a Viper method member. */ case class Method private[Vertices](methodName: String) extends Vertex - /** Represents a Viper method member without the body. */ - case class MethodSpec(methodName: String) extends Vertex + /** Represents an opaque Viper function member without the body. */ + case class FunctionSig(functionName: String) extends Vertex - /** Represents a Viper function member. */ - case class Function(functionName: String) extends Vertex + /** Represents an opaque Viper function member. */ + case class FunctionBody private[Vertices](functionName: String) extends Vertex - /** Represents a Viper predicate member. */ + /** Represents a Viper predicate member without the body. */ case class PredicateSig(predicateName: String) extends Vertex - /** Represents a Viper predicate member without the body. */ + /** Represents a Viper predicate member. */ case class PredicateBody private[Vertices](predicateName: String) extends Vertex /** Represents a Viper field member. */ @@ -712,11 +717,21 @@ object Vertices { private[Vertices] def apply(predicateName: String): PredicateBody = new PredicateBody(predicateName) } + object FunctionBody { + private[Vertices] def apply(functionName: String): FunctionBody = new FunctionBody(functionName) + } + /** This function is only allowed to be called in the following cases: * 1) applying [[Vertices.toDefVertex]] to the predicate referenced by `predicateName` returns a [[Vertices.PredicateBody]] instance. * 2) The result is used as the target of a dependency. * */ - def unsageGetPredicateBody(predicateName: String): PredicateBody = Vertices.PredicateBody(predicateName) + def unsafeGetPredicateBody(predicateName: String): PredicateBody = Vertices.PredicateBody(predicateName) + + /** This function is only allowed to be called in the following cases: + * 1) applying [[Vertices.toDefVertex]] to the predicate referenced by `predicateName` returns a [[Vertices.PredicateBody]] instance. + * 2) The result is used as the target of a dependency. + * */ + def unsafeGetFunctionBody(functionName: String): FunctionBody = Vertices.FunctionBody(functionName) } trait Vertices { @@ -725,15 +740,9 @@ trait Vertices { def toDefVertex(m: ast.Member): Vertex = { m match { - case m: ast.Method => m.body match { - case Some(_) => Vertices.Method(m.name) - case None => Vertices.MethodSpec(m.name) - } - case m: ast.Predicate => m.body match { - case Some(_) => Vertices.PredicateBody(m.name) - case None => Vertices.PredicateSig(m.name) - } - case m: ast.Function => Vertices.Function(m.name) + case m: ast.Method => Vertices.Method(m.name) + case m: ast.Predicate => Vertices.PredicateBody(m.name) + case m: ast.Function => Vertices.FunctionBody(m.name) case m: ast.Field => Vertices.Field(m.name) case m: ast.Domain => Vertices.DomainType(ast.DomainType(domain = m, (m.typVars zip m.typVars).toMap)) case _: ast.ExtensionMember => @@ -747,7 +756,7 @@ trait Vertices { def toUseVertex(m: ast.Member): Vertex = { m match { case m: ast.Method => Vertices.MethodSpec(m.name) - case m: ast.Function => Vertices.Function(m.name) + case m: ast.Function => Vertices.FunctionSig(m.name) case m: ast.Predicate => Vertices.PredicateSig(m.name) case m: ast.Field => Vertices.Field(m.name) case m: ast.Domain => Vertices.DomainType(ast.DomainType(domain = m, (m.typVars zip m.typVars).toMap)) @@ -776,7 +785,12 @@ trait Vertices { val filteredStubs = stubs.filterNot(stub => ms.exists(_.name == stub.name)) (ms ++ filteredStubs).toSeq } - val funcs = vertices.collect { case v: Function => functionTable(v.functionName) }.toSeq + val funcs = { + val fsigs = vertices.collect { case v: FunctionSig => val f = functionTable(v.functionName); f.copy(body = None)(f.pos, f.info, f.errT) }.toSeq + val fbodies = vertices.collect { case v: FunctionBody => functionTable(v.functionName) }.toSeq + val filteredSigs = fsigs.filterNot(sig => fbodies.exists(_.name == sig.name)) + fbodies ++ filteredSigs + } val preds = { val psigs = vertices.collect { case v: PredicateSig => val p = predicateTable(v.predicateName); p.copy(body = None)(p.pos, p.info, p.errT) }.toSeq val pbodies = vertices.collect { case v: PredicateBody => predicateTable(v.predicateName) }.toSeq @@ -836,10 +850,17 @@ trait Edges { this: Vertices => case p: ast.Predicate => dependenciesToChildren(member, defVertex) ++ - p.formalArgs.flatMap(dependenciesToChildren(_, useVertex)) ++ - Seq(defVertex -> useVertex) + p.formalArgs.flatMap(dependenciesToChildren(_, useVertex)) + + case f: ast.Function => + dependenciesToChildren(member, defVertex) ++ + (f.pres ++ f.posts ++ f.formalArgs ++ f.result).flatMap(dependenciesToChildren(_, useVertex)) ++ + (f.info.getUniqueInfo[AnnotationInfo] match { + case Some(ai) if ai.values.contains("opaque") => Seq() + case _ => Seq(useVertex -> defVertex) // for non opaque functions a use dependency is a def dependency + }) - case _: ast.Function | _: ast.Field => dependenciesToChildren(member, defVertex) + case _: ast.Field => dependenciesToChildren(member, defVertex) case d: ast.Domain => d.axioms.flatMap { ax => @@ -860,7 +881,7 @@ trait Edges { this: Vertices => * depend on the axiom. */ val outsideQuantifiers = Visitor.deepCollect[ast.Node, Seq[Vertices.Vertex]](Seq(ax.exp), { - case x: ast.QuantifiedExp => Seq.empty + case _: ast.QuantifiedExp => Seq.empty case x => Nodes.subnodes(x) })(directUsages).flatten @@ -929,13 +950,17 @@ trait Edges { this: Vertices => { case n: ast.MethodCall => Seq(Vertices.MethodSpec(n.methodName)) - case n: ast.FuncApp => Seq(Vertices.Function(n.funcname)) + // The call is fine because the result is used as the target of a dependency. + case n: ast.FuncApp => n.info.getUniqueInfo[AnnotationInfo] match { + case Some(ai) if ai.values.contains("reveal") => Seq(Vertices.unsafeGetFunctionBody(n.funcname)) + case _ => Seq(Vertices.FunctionSig(n.funcname)) + } case n: ast.DomainFuncApp => Seq(Vertices.DomainFunction(n.funcname)) case n: ast.PredicateAccess => Seq(Vertices.PredicateSig(n.predicateName)) // The call is fine because the result is used as the target of a dependency. - case n: ast.Unfold => Seq(Vertices.unsageGetPredicateBody(n.acc.loc.predicateName)) - case n: ast.Fold => Seq(Vertices.unsageGetPredicateBody(n.acc.loc.predicateName)) - case n: ast.Unfolding => Seq(Vertices.unsageGetPredicateBody(n.acc.loc.predicateName)) + case n: ast.Unfold => Seq(Vertices.unsafeGetPredicateBody(n.acc.loc.predicateName)) + case n: ast.Fold => Seq(Vertices.unsafeGetPredicateBody(n.acc.loc.predicateName)) + case n: ast.Unfolding => Seq(Vertices.unsafeGetPredicateBody(n.acc.loc.predicateName)) case n: ast.FieldAccess => Seq(Vertices.Field(n.field.name)) case n: ast.Type => usagesInType(n).collect { case t: ast.DomainType => Vertices.DomainType(t) } } From c9c9100a9835ee1987fc67aafcd40a9b1db4d2b9 Mon Sep 17 00:00:00 2001 From: "Felix A. Wolf" Date: Fri, 15 Mar 2024 00:52:22 +0100 Subject: [PATCH 2/7] fixed some names --- .../silver/ast/utility/chopper/Chopper.scala | 32 +++++++++---------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala b/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala index eb7e0970c..91b9e845c 100644 --- a/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala +++ b/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala @@ -545,8 +545,8 @@ object Penalty { override def penalty(xs: Vertices.Vertex): Int = xs match { case _: Vertices.Method => conf.method case _: Vertices.MethodSpec => conf.methodSpec - case _: Vertices.FunctionBody => conf.function - case _: Vertices.FunctionSig => conf.functionSig + case _: Vertices.Function => conf.function + case _: Vertices.FunctionSpec => conf.functionSig case _: Vertices.PredicateBody => conf.predicate case _: Vertices.PredicateSig => conf.predicateSig case _: Vertices.Field => conf.field @@ -679,10 +679,10 @@ object Vertices { case class Method private[Vertices](methodName: String) extends Vertex /** Represents an opaque Viper function member without the body. */ - case class FunctionSig(functionName: String) extends Vertex + case class FunctionSpec(functionName: String) extends Vertex /** Represents an opaque Viper function member. */ - case class FunctionBody private[Vertices](functionName: String) extends Vertex + case class Function private[Vertices](functionName: String) extends Vertex /** Represents a Viper predicate member without the body. */ case class PredicateSig(predicateName: String) extends Vertex @@ -717,8 +717,8 @@ object Vertices { private[Vertices] def apply(predicateName: String): PredicateBody = new PredicateBody(predicateName) } - object FunctionBody { - private[Vertices] def apply(functionName: String): FunctionBody = new FunctionBody(functionName) + object Function { + private[Vertices] def apply(functionName: String): Function = new Function(functionName) } /** This function is only allowed to be called in the following cases: @@ -728,10 +728,10 @@ object Vertices { def unsafeGetPredicateBody(predicateName: String): PredicateBody = Vertices.PredicateBody(predicateName) /** This function is only allowed to be called in the following cases: - * 1) applying [[Vertices.toDefVertex]] to the predicate referenced by `predicateName` returns a [[Vertices.PredicateBody]] instance. + * 1) applying [[Vertices.toDefVertex]] to the function referenced by `functionName` returns a [[Vertices.Function]] instance. * 2) The result is used as the target of a dependency. * */ - def unsafeGetFunctionBody(functionName: String): FunctionBody = Vertices.FunctionBody(functionName) + def unsafeGetFunction(functionName: String): Function = Vertices.Function(functionName) } trait Vertices { @@ -742,7 +742,7 @@ trait Vertices { m match { case m: ast.Method => Vertices.Method(m.name) case m: ast.Predicate => Vertices.PredicateBody(m.name) - case m: ast.Function => Vertices.FunctionBody(m.name) + case m: ast.Function => Vertices.Function(m.name) case m: ast.Field => Vertices.Field(m.name) case m: ast.Domain => Vertices.DomainType(ast.DomainType(domain = m, (m.typVars zip m.typVars).toMap)) case _: ast.ExtensionMember => @@ -756,7 +756,7 @@ trait Vertices { def toUseVertex(m: ast.Member): Vertex = { m match { case m: ast.Method => Vertices.MethodSpec(m.name) - case m: ast.Function => Vertices.FunctionSig(m.name) + case m: ast.Function => Vertices.FunctionSpec(m.name) case m: ast.Predicate => Vertices.PredicateSig(m.name) case m: ast.Field => Vertices.Field(m.name) case m: ast.Domain => Vertices.DomainType(ast.DomainType(domain = m, (m.typVars zip m.typVars).toMap)) @@ -786,10 +786,10 @@ trait Vertices { (ms ++ filteredStubs).toSeq } val funcs = { - val fsigs = vertices.collect { case v: FunctionSig => val f = functionTable(v.functionName); f.copy(body = None)(f.pos, f.info, f.errT) }.toSeq - val fbodies = vertices.collect { case v: FunctionBody => functionTable(v.functionName) }.toSeq - val filteredSigs = fsigs.filterNot(sig => fbodies.exists(_.name == sig.name)) - fbodies ++ filteredSigs + val fs = vertices.collect { case v: FunctionSpec => val f = functionTable(v.functionName); f.copy(body = None)(f.pos, f.info, f.errT) }.toSeq + val stubs = vertices.collect { case v: Function => functionTable(v.functionName) }.toSeq + val filteredStubs = fs.filterNot(stub => stubs.exists(_.name == stub.name)) + fs ++ filteredStubs } val preds = { val psigs = vertices.collect { case v: PredicateSig => val p = predicateTable(v.predicateName); p.copy(body = None)(p.pos, p.info, p.errT) }.toSeq @@ -952,8 +952,8 @@ trait Edges { this: Vertices => case n: ast.MethodCall => Seq(Vertices.MethodSpec(n.methodName)) // The call is fine because the result is used as the target of a dependency. case n: ast.FuncApp => n.info.getUniqueInfo[AnnotationInfo] match { - case Some(ai) if ai.values.contains("reveal") => Seq(Vertices.unsafeGetFunctionBody(n.funcname)) - case _ => Seq(Vertices.FunctionSig(n.funcname)) + case Some(ai) if ai.values.contains("reveal") => Seq(Vertices.unsafeGetFunction(n.funcname)) + case _ => Seq(Vertices.FunctionSpec(n.funcname)) } case n: ast.DomainFuncApp => Seq(Vertices.DomainFunction(n.funcname)) case n: ast.PredicateAccess => Seq(Vertices.PredicateSig(n.predicateName)) From 2cbbbd23387be7d0ca8ad211df0b30650fad3c83 Mon Sep 17 00:00:00 2001 From: "Felix A. Wolf" Date: Fri, 15 Mar 2024 00:58:26 +0100 Subject: [PATCH 3/7] fixed two comments --- src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala b/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala index 91b9e845c..3e6ad175c 100644 --- a/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala +++ b/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala @@ -678,10 +678,10 @@ object Vertices { /** Represents a Viper method member. */ case class Method private[Vertices](methodName: String) extends Vertex - /** Represents an opaque Viper function member without the body. */ + /** Represents a Viper function member without the body. */ case class FunctionSpec(functionName: String) extends Vertex - /** Represents an opaque Viper function member. */ + /** Represents a Viper function member. */ case class Function private[Vertices](functionName: String) extends Vertex /** Represents a Viper predicate member without the body. */ From 8d230cedfacb29016da8d3eb0a5dcb40088f6fc9 Mon Sep 17 00:00:00 2001 From: "Felix A. Wolf" Date: Fri, 15 Mar 2024 13:50:52 +0100 Subject: [PATCH 4/7] fixed that stubs do not overwrite bodies for functions --- src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala b/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala index 3e6ad175c..31025e612 100644 --- a/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala +++ b/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala @@ -786,8 +786,8 @@ trait Vertices { (ms ++ filteredStubs).toSeq } val funcs = { - val fs = vertices.collect { case v: FunctionSpec => val f = functionTable(v.functionName); f.copy(body = None)(f.pos, f.info, f.errT) }.toSeq - val stubs = vertices.collect { case v: Function => functionTable(v.functionName) }.toSeq + val fs = vertices.collect { case v: Function => functionTable(v.functionName) }.toSeq + val stubs = vertices.collect { case v: FunctionSpec => val f = functionTable(v.functionName); f.copy(body = None)(f.pos, f.info, f.errT) }.toSeq val filteredStubs = fs.filterNot(stub => stubs.exists(_.name == stub.name)) fs ++ filteredStubs } From 7f00d01aca0195ff5809f9a8ed1f262f3242ffed Mon Sep 17 00:00:00 2001 From: "Felix A. Wolf" Date: Fri, 15 Mar 2024 13:54:31 +0100 Subject: [PATCH 5/7] fixed filtering of function stubs --- src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala b/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala index 31025e612..104002de2 100644 --- a/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala +++ b/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala @@ -788,7 +788,7 @@ trait Vertices { val funcs = { val fs = vertices.collect { case v: Function => functionTable(v.functionName) }.toSeq val stubs = vertices.collect { case v: FunctionSpec => val f = functionTable(v.functionName); f.copy(body = None)(f.pos, f.info, f.errT) }.toSeq - val filteredStubs = fs.filterNot(stub => stubs.exists(_.name == stub.name)) + val filteredStubs = stubs.filterNot(stub => fs.exists(_.name == stub.name)) fs ++ filteredStubs } val preds = { From ec375f9b191daf8f2bf02937ff9660c0c90b7e04 Mon Sep 17 00:00:00 2001 From: "Felix A. Wolf" Date: Fri, 15 Mar 2024 14:26:30 +0100 Subject: [PATCH 6/7] fixed test --- .../viper/silver/ast/utility/chopper/Chopper.scala | 11 +++++++---- src/test/scala/ChopperTests.scala | 2 +- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala b/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala index 104002de2..932b9fcc2 100644 --- a/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala +++ b/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala @@ -7,7 +7,7 @@ package viper.silver.ast.utility.chopper import viper.silver.ast -import viper.silver.ast.{AnnotationInfo, QuantifiedExp} +import viper.silver.ast.AnnotationInfo import viper.silver.ast.utility.{Nodes, Visitor} import scala.annotation.tailrec @@ -805,7 +805,10 @@ trait Vertices { val totalDs = (ds ++ fs.keys ++ as.keys).distinct totalDs.map { d => - d.copy(functions = fs.getOrElse(d, Seq.empty), axioms = as.getOrElse(d, Seq.empty))(d.pos, d.info, d.errT) + d.copy( + functions = fs.getOrElse(d, Seq.empty), + axioms = as.getOrElse(d, Seq.empty), + )(d.pos, d.info, d.errT) } } @@ -814,7 +817,7 @@ trait Vertices { functions = funcs, predicates = preds, fields = fields, - domains = domains + domains = domains, )(program.pos, program.info, program.errT) } } @@ -885,7 +888,7 @@ trait Edges { this: Vertices => case x => Nodes.subnodes(x) })(directUsages).flatten - def fromQuantifier(triggers: Seq[ast.Trigger], qexp: QuantifiedExp): Seq[Vertices.Vertex] = { + def fromQuantifier(triggers: Seq[ast.Trigger], qexp: ast.QuantifiedExp): Seq[Vertices.Vertex] = { val triggerUsages = triggers.map(usages) if (triggerUsages.exists(_.isEmpty)) { // if there is a trigger w/o usages, we are conservative and diff --git a/src/test/scala/ChopperTests.scala b/src/test/scala/ChopperTests.scala index 0b480d554..f954432c6 100644 --- a/src/test/scala/ChopperTests.scala +++ b/src/test/scala/ChopperTests.scala @@ -231,7 +231,7 @@ class ChopperTests extends AnyFunSuite with Matchers with Inside { result.length shouldBe 2 result shouldEqual Vector( ast.Program(Seq.empty, Seq.empty, Seq.empty, Seq(caller1, calleeStub), Seq.empty, Seq.empty)(), - ast.Program(Seq.empty, Seq.empty, Seq.empty, Seq(caller2, callee), Seq.empty, Seq.empty)(), + ast.Program(Seq.empty, Seq.empty, Seq.empty, Seq(callee, caller2), Seq.empty, Seq.empty)(), ) } From 1f8d9367465a1ad5ae961c7f968fccf0692028e2 Mon Sep 17 00:00:00 2001 From: Felix Wolf <60103963+Felalolf@users.noreply.github.com> Date: Thu, 21 Mar 2024 10:00:51 +0100 Subject: [PATCH 7/7] Update src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala added comma to comment --- src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala b/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala index 932b9fcc2..e0647ef2d 100644 --- a/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala +++ b/src/main/scala/viper/silver/ast/utility/chopper/Chopper.scala @@ -860,7 +860,7 @@ trait Edges { this: Vertices => (f.pres ++ f.posts ++ f.formalArgs ++ f.result).flatMap(dependenciesToChildren(_, useVertex)) ++ (f.info.getUniqueInfo[AnnotationInfo] match { case Some(ai) if ai.values.contains("opaque") => Seq() - case _ => Seq(useVertex -> defVertex) // for non opaque functions a use dependency is a def dependency + case _ => Seq(useVertex -> defVertex) // for non opaque functions, a use dependency is a def dependency }) case _: ast.Field => dependenciesToChildren(member, defVertex)