Embedded interfaces (#492)

* stuff * test case works, everything else not * temp * refactoring * bugfix * added the unit tests * bug fix * bug-fix * added Felix's test case * implemented my own feedback * removed commeted out code * more cleanup * fixed bug * added test * cycle detected * added a comment * cgedges * Generate correct implementation proof between interface types * Fix problems with termination edges transform * updated todo * Revert changes that are not supposed to be in this PR * Revert some changes from a previous commit * Add extra type-checks for better error messages * fix line of error * Update src/main/scala/viper/gobra/ast/internal/transform/CGEdgesTerminationTransform.scala Co-authored-by: Felix Wolf <[email protected]> * Incorporate Felix's feedback Co-authored-by: Felix A. Wolf <[email protected]> Co-authored-by: João Pereira <[email protected]> Co-authored-by: Felix Wolf <[email protected]>
viperproject · Jul 25, 2022 · 939805b · 939805b
1 parent 93346d6
commit 939805b
Show file tree

Hide file tree

Showing 31 changed files with 732 additions and 116 deletions.
diff --git a/src/main/scala/viper/gobra/ast/frontend/Ast.scala b/src/main/scala/viper/gobra/ast/frontend/Ast.scala
@@ -690,7 +690,7 @@ case class PPredType(args: Vector[PType]) extends PTypeLit
 case class PInterfaceType(
                            embedded: Vector[PInterfaceName],
                            methSpecs: Vector[PMethodSig],
-                           predSpec: Vector[PMPredicateSig]
+                           predSpecs: Vector[PMPredicateSig]
                          ) extends PTypeLit with PUnorderedScope
 
 sealed trait PInterfaceClause extends PNode

diff --git a/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala b/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala
@@ -591,7 +591,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     case TupleT(ts, _) => parens(showTypeList(ts))
     case PredT(args, _) => "pred" <> parens(showTypeList(args))
     case struct: StructT => emptyDoc <> block(hcat(struct.fields map showField))
-    case _: InterfaceT => "interface" <> parens("...")
+    case i: InterfaceT => "interface" <> parens("name is " <> i.name)
     case _: DomainT => "domain" <> parens("...")
     case ChannelT(elem, _) => "chan" <+> showType(elem)
     case SortT => "sort"

diff --git a/src/main/scala/viper/gobra/ast/internal/Program.scala b/src/main/scala/viper/gobra/ast/internal/Program.scala
@@ -33,22 +33,22 @@ case class Program(
 }
 
 class LookupTable(
-                 definedTypes: Map[(String, Addressability), Type],
-                 definedMethods: Map[MethodProxy, MethodLikeMember],
-                 definedFunctions: Map[FunctionProxy, FunctionLikeMember],
-                 definedMPredicates: Map[MPredicateProxy, MPredicateLikeMember],
-                 definedFPredicates: Map[FPredicateProxy, FPredicateLikeMember],
+                 private val definedTypes: Map[(String, Addressability), Type] = Map.empty,
+                 private val definedMethods: Map[MethodProxy, MethodLikeMember] = Map.empty,
+                 private val definedFunctions: Map[FunctionProxy, FunctionLikeMember] = Map.empty,
+                 private val definedMPredicates: Map[MPredicateProxy, MPredicateLikeMember] = Map.empty,
+                 private val definedFPredicates: Map[FPredicateProxy, FPredicateLikeMember] = Map.empty,
                  /**
                    * only has to be defined on types that implement an interface // might change depending on how embedding support changes
                    * SortedSet is used to achieve a consistent ordering of members across runs of Gobra
                    */
-                 val memberProxies: Map[Type, SortedSet[MemberProxy]],
+                 private val directMemberProxies: Map[Type, SortedSet[MemberProxy]] = Map.empty,
                  /**
                    * empty interface does not have to be included
                    * SortedSet is used to achieve a consistent ordering of members across runs of Gobra
                    */
-                 val interfaceImplementations: Map[InterfaceT, SortedSet[Type]],
-                 implementationProofPredicateAliases: Map[(Type, InterfaceT, String), FPredicateProxy]
+                 private val directInterfaceImplementations: Map[InterfaceT, SortedSet[Type]] = Map.empty,
+                 private val implementationProofPredicateAliases: Map[(Type, InterfaceT, String), FPredicateProxy] = Map.empty,
                  ) {
   def lookup(t: DefinedT): Type = definedTypes(t.name, t.addressability)
   def lookup(m: MethodProxy): MethodLikeMember = definedMethods(m)
@@ -61,22 +61,69 @@ class LookupTable(
   def getMPredicates: Iterable[MPredicateLikeMember] = definedMPredicates.values
   def getFPredicates: Iterable[FPredicateLikeMember] = definedFPredicates.values
 
-  def getDefinedTypes: Map[(String, Addressability), Type] = definedTypes
-  def getDefinedMethods: Map[MethodProxy, MethodLikeMember] = definedMethods
-  def getDefinedFunctions: Map[FunctionProxy, FunctionLikeMember] = definedFunctions
-  def getDefinedMPredicates: Map[MPredicateProxy, MPredicateLikeMember] = definedMPredicates
-  def getDefinedFPredicates: Map[FPredicateProxy, FPredicateLikeMember] = definedFPredicates
-  def getImplementationProofPredicateAliases: Map[(Type, InterfaceT, String), FPredicateProxy] = implementationProofPredicateAliases
-
-  def implementations(t: InterfaceT): SortedSet[Type] = interfaceImplementations.getOrElse(t.withAddressability(Addressability.Exclusive), SortedSet.empty)
-  def members(t: Type): SortedSet[MemberProxy] = memberProxies.getOrElse(t.withAddressability(Addressability.Exclusive), SortedSet.empty)
-  def lookup(t: Type, name: String): Option[MemberProxy] = members(t).find(_.name == name)
-
+  def lookupImplementations(t: InterfaceT): SortedSet[Type] = getImplementations.getOrElse(t.withAddressability(Addressability.Exclusive), SortedSet.empty)
+  def lookupNonInterfaceImplementations(t: InterfaceT): SortedSet[Type] = lookupImplementations(t).filterNot(_.isInstanceOf[InterfaceT])
+  def lookupMembers(t: Type): SortedSet[MemberProxy] = getMembers.getOrElse(t.withAddressability(Addressability.Exclusive), SortedSet.empty)
+  def lookup(t: Type, name: String): Option[MemberProxy] = lookupMembers(t).find(_.name == name)
   def lookupImplementationPredicate(impl: Type, itf: InterfaceT, name: String): Option[PredicateProxy] = {
     lookup(impl, name).collect{ case m: MPredicateProxy => m }.orElse{
       implementationProofPredicateAliases.get(impl, itf, name)
     }
   }
+
+  def getImplementations: Map[InterfaceT, SortedSet[Type]] = transitiveInterfaceImplementations
+  def getMembers: Map[Type, SortedSet[MemberProxy]] = transitiveMemberProxies
+
+  def merge(other: LookupTable): LookupTable = new LookupTable(
+    definedTypes ++ other.definedTypes,
+    definedMethods ++ other.definedMethods,
+    definedFunctions ++ other.definedFunctions,
+    definedMPredicates ++ other.definedMPredicates,
+    definedFPredicates ++ other.definedFPredicates,
+    directMemberProxies ++ other.directMemberProxies,
+    directInterfaceImplementations ++ other.directInterfaceImplementations,
+    implementationProofPredicateAliases ++ other.implementationProofPredicateAliases,
+  )
+
+  private lazy val (transitiveInterfaceImplementations, transitiveMemberProxies) = {
+    var res = directInterfaceImplementations
+    var resMemberProxies = directMemberProxies
+
+    for ((_, values) <- res; t <- values) t match {
+      case t: InterfaceT if !res.contains(t) => res += (t -> SortedSet.empty)
+      case _ =>
+    }
+
+    var change = false
+    var temp = res
+
+    def mergeProxies(l: Option[SortedSet[MemberProxy]], r: Option[SortedSet[MemberProxy]]): SortedSet[MemberProxy] = {
+      (l.getOrElse(SortedSet.empty[MemberProxy]) ++ r.getOrElse(SortedSet.empty[MemberProxy])).foldLeft((SortedSet.empty[MemberProxy], SortedSet.empty[String])){
+        case ((res, set), x) if set.contains(x.name) =>
+          // method redeclarations are currently rejected
+          Violation.violation(x.isInstanceOf[PredicateProxy], s"Found re-declaration or override of $x, which is currently not supported")
+          (res, set) // always take first in sorted set
+        case ((res, set), x) => (res ++ SortedSet(x), set ++ SortedSet(x.name))
+      }._1
+    }
+    val mapsTo = temp.compose[Type]{ case t: InterfaceT => t }
+    def trans(key: InterfaceT, t: Type): SortedSet[Type] = t match {
+      case mapsTo(set) =>
+        change = true
+        res += (key -> (res(key) ++ set))
+        resMemberProxies += (t -> mergeProxies(resMemberProxies.get(t), resMemberProxies.get(key)))
+        set
+
+      case _ => SortedSet.empty
+    }
+
+    do {
+      change = false
+      temp = temp.map{ case (key, values) => (key, values.flatMap(trans(key, _))) }
+    } while (change)
+
+    (res, resMemberProxies)
+  }
 }
 
 sealed trait Member extends Node

diff --git a/src/main/scala/viper/gobra/ast/internal/transform/CGEdgesTerminationTransform.scala b/src/main/scala/viper/gobra/ast/internal/transform/CGEdgesTerminationTransform.scala
@@ -25,9 +25,15 @@ object CGEdgesTerminationTransform extends InternalTransform {
       var methodsToAdd: Set[in.Member] = Set.empty
       var definedMethodsDelta: Map[in.MethodProxy, in.MethodLikeMember] = Map.empty
 
-      table.memberProxies.foreach {
+      def isEmbeddedMethod(subTProxy: in.MethodProxy, superTProxy: in.MethodProxy): Boolean = {
+        // The proxies for embedded methods defined in interface type superT are the same
+        // as the method proxies for the corresponding method in an embedding interface type subT
+        subTProxy == superTProxy
+      }
+
+      table.getMembers.foreach {
         case (t: in.InterfaceT, proxies) =>
-          val implementations = table.interfaceImplementations(t)
+          val implementations = table.lookupImplementations(t)
           proxies.foreach {
             case proxy: in.MethodProxy =>
               table.lookup(proxy) match {
@@ -48,38 +54,65 @@ object CGEdgesTerminationTransform extends InternalTransform {
                   *     }
                   *   }
                   */
-                case m: in.Method if m.terminationMeasures.nonEmpty =>
+                case m: in.Method if m.terminationMeasures.nonEmpty && m.receiver.typ == t =>
+                  // The restriction `m.receiver.typ` ensures that the member with the addtional call-graph edges
+                  // is only generated once, when looking at the original definition of the method (and not, for
+                  // example, when looking at an embedding of the method).
+
                   // only performs transformation if method has termination measures
                   val src = m.getMeta
                   val assumeFalse = in.Assume(in.ExprAssertion(in.BoolLit(b = false)(src))(src))(src)
+                  val optCallsToImpls = implementations.toVector.flatMap { subT: in.Type =>
+                    table.lookup(subT, proxy.name).toVector.map {
+
+                      case implProxy: in.MethodProxy if !subT.isInstanceOf[in.InterfaceT] =>
+                        // looking at a concrete implementation of the method
+                        in.If(
+                          in.EqCmp(in.TypeOf(m.receiver)(src), typeAsExpr(subT)(src))(src),
+                          in.Seqn(Vector(
+                            in.MethodCall(
+                              m.results map parameterAsLocalValVar,
+                              in.TypeAssertion(m.receiver, subT)(src),
+                              implProxy, m.args
+                            )(src),
+                            in.Return()(src)
+                          ))(src),
+                          in.Seqn(Vector())(src)
+                        )(src)
+
+                      case implProxy: in.MethodProxy if subT.isInstanceOf[in.InterfaceT]
+                        && isEmbeddedMethod(implProxy, proxy) =>
+                        // If the subtype (subT) is an interface type and the method is defined in subT
+                        // via an interface embedding, then the contract of the method is the same and
+                        // there is no need to generate extra proof obligations.
+                        // The soundness of this argument critically relies on the fact that if a type T implements
+                        // an interface B and B has interface A embedded, then T must implement A too.
+                        in.Seqn(Vector())(src)
+
+                      case _: in.MethodProxy if subT.isInstanceOf[in.InterfaceT] =>
+                        Violation.violation(s"Type $subT contains a re-definition of method ${proxy.name}. This is still not supported.")
+
+                      case v => Violation.violation(s"Expected a MethodProxy but got $v instead.")
+
+                    }
+                  }
                   val newBody = {
                     in.Block(
                       decls = Vector.empty,
-                      stmts = assumeFalse +: implementations.toVector.flatMap { t: in.Type =>
-                        table.lookup(t, proxy.name).map {
-                          case implProxy: in.MethodProxy =>
-                            in.If(
-                              in.EqCmp(in.TypeOf(m.receiver)(src), typeAsExpr(t)(src))(src),
-                              in.Seqn(Vector(
-                                in.MethodCall(
-                                  m.results map parameterAsLocalValVar,
-                                  in.TypeAssertion(m.receiver, t)(src),
-                                  implProxy, m.args
-                                )(src),
-                                in.Return()(src)
-                              ))(src),
-                              in.Seqn(Vector())(src)
-                            )(src)
-                          case v => Violation.violation(s"Expected a MethodProxy but got $v instead.")
-                        }
-                      }
+                      stmts = assumeFalse +: optCallsToImpls
                     )(src)
                   }
                   val newMember = in.Method(m.receiver, m.name, m.args, m.results, m.pres, m.posts, m.terminationMeasures, Some(newBody.toMethodBody))(src)
                   methodsToRemove += m
                   methodsToAdd += newMember
                   definedMethodsDelta += proxy -> newMember
 
+                case m: in.Method if m.terminationMeasures.nonEmpty && m.receiver.typ != t =>
+                  val recvT = m.receiver.typ.asInstanceOf[in.InterfaceT]
+                  // Sanity check: no method is ignored by this case analysis
+                  Violation.violation(table.lookupImplementations(recvT).contains(t),
+                    s"Method ${m.name} found for type $t even though its receiver is not $t or one of its supertypes.")
+
                 /**
                   * Transforms the abstract pure methods from interface declarations into non-abstract pure methods containing calls
                   * to all implementations' corresponding methods. The new body has the form
@@ -109,7 +142,7 @@ object CGEdgesTerminationTransform extends InternalTransform {
                   *   that are not easily reproducible via a transformation at the level of the internal code.
                   *
                   */
-                case m: in.PureMethod if m.terminationMeasures.nonEmpty =>
+                case m: in.PureMethod if m.terminationMeasures.nonEmpty && m.receiver.typ == t =>
                   Violation.violation(m.results.length == 1, "Expected one and only one out-parameter.")
                   Violation.violation(m.posts.isEmpty, s"Expected no postcondition, but got ${m.posts}.")
                   // only performs transformation if method has termination measures
@@ -124,17 +157,32 @@ object CGEdgesTerminationTransform extends InternalTransform {
                   val terminationCheckBody = {
                     val returnType = m.results.head.typ
                     val fallbackProxyCall = in.PureMethodCall(m.receiver, fallbackProxy, m.args, returnType)(src)
-                    val bodyFalseBranch = implementations.toVector.foldLeft[in.Expr](fallbackProxyCall) {
-                      case (accum: in.Expr, impl: in.Type) =>
-                        table.lookup(impl, proxy.name) match {
-                          case Some(implProxy: in.MethodProxy) =>
+                    val implProxies: Vector[(in.Type, in.MemberProxy)] = implementations.toVector.flatMap{ impl =>
+                      table.lookup(impl, proxy.name).map(implProxy => (impl, implProxy))
+                    }
+                    val bodyFalseBranch = implProxies.foldLeft[in.Expr](fallbackProxyCall) {
+                      case (accum: in.Expr, (subT: in.Type, implMemberProxy: in.MemberProxy)) =>
+                        implMemberProxy match {
+                          case implProxy: in.MethodProxy if !subT.isInstanceOf[in.InterfaceT] =>
                             in.Conditional(
-                              in.EqCmp(in.TypeOf(m.receiver)(src), typeAsExpr(impl)(src))(src),
-                              in.PureMethodCall(in.TypeAssertion(m.receiver, impl)(src), implProxy, m.args, returnType)(src),
+                              in.EqCmp(in.TypeOf(m.receiver)(src), typeAsExpr(subT)(src))(src),
+                              in.PureMethodCall(in.TypeAssertion(m.receiver, subT)(src), implProxy, m.args, returnType)(src),
                               accum,
                               returnType
                             )(src)
-                          case None => accum
+
+                          case implProxy: in.MethodProxy if subT.isInstanceOf[in.InterfaceT]
+                            && isEmbeddedMethod(implProxy, proxy) =>
+                            // If the subtype (subT) is an interface type and the method is defined in subT
+                            // via an interface embedding, then the contract of the method is the same and
+                            // there is no need to generate extra proof obligations.
+                            // The soundness of this argument critically relies on the fact that if a type T implements
+                            // and interface B and B has interface A embedded, then T must implement A too.
+                            accum
+
+                          case _: in.MethodProxy if subT.isInstanceOf[in.InterfaceT] =>
+                            Violation.violation(s"Type $subT contains a re-definition of method ${proxy.name}. This is still not supported.")
+
                           case v => Violation.violation(s"Expected a MethodProxy but got $v instead.")
                         }
                     }
@@ -148,6 +196,13 @@ object CGEdgesTerminationTransform extends InternalTransform {
                   definedMethodsDelta += fallbackProxy -> fallbackFunction
                   definedMethodsDelta += proxy -> transformedM
 
+
+                case m: in.PureMethod if m.terminationMeasures.nonEmpty && m.receiver.typ != t =>
+                 val recvT = m.receiver.typ.asInstanceOf[in.InterfaceT]
+                  // Sanity check: no method is ignored by this case analysis
+                  Violation.violation(table.lookupImplementations(recvT).contains(t),
+                    s"Pure method ${m.name} found for type $t even though its receiver is not $t or one of its supertypes.")
+
                 case _ =>
               }
             case _ =>
@@ -160,16 +215,7 @@ object CGEdgesTerminationTransform extends InternalTransform {
       in.Program(
         types = p.types,
         members = p.members.diff(methodsToRemove.toSeq).appendedAll(methodsToAdd),
-        table = new in.LookupTable(
-          definedTypes = table.getDefinedTypes,
-          definedMethods = table.getDefinedMethods ++ definedMethodsDelta,
-          definedFunctions = table.getDefinedFunctions,
-          definedMPredicates = table.getDefinedMPredicates,
-          definedFPredicates = table.getDefinedFPredicates,
-          memberProxies = table.memberProxies,
-          interfaceImplementations = table.interfaceImplementations,
-          implementationProofPredicateAliases = table.getImplementationProofPredicateAliases
-        )
+        table = p.table.merge(new in.LookupTable(definedMethods = definedMethodsDelta)),
       )(p.info)
   }