Merge pull request #601 from viperproject/meilers_predicate_consisten…

…cy_check Consistency check for predicate access arguments
viperproject · Aug 24, 2022 · f261bcc · f261bcc
2 parents fc8fef2 + 6761f8c
commit f261bcc
Show file tree

Hide file tree

Showing 2 changed files with 46 additions and 2 deletions.
diff --git a/src/main/scala/viper/silver/ast/Program.scala b/src/main/scala/viper/silver/ast/Program.scala
@@ -36,6 +36,7 @@ case class Program(domains: Seq[Domain], fields: Seq[Field], functions: Seq[Func
     checkMethodCallsAreValid ++
     checkFunctionApplicationsAreValid ++
     checkDomainFunctionApplicationsAreValid ++
+    checkPredicateAccessesAreValid ++
     checkAbstractPredicatesUsage ++
     checkIdentifiers
 
@@ -114,6 +115,28 @@ case class Program(domains: Seq[Domain], fields: Seq[Field], functions: Seq[Func
     s
   }
 
+  /** Checks that the predicate access arguments are assignable to formalArgs.
+    **/
+  lazy val checkPredicateAccessesAreValid: Seq[ConsistencyError] = {
+    var s = Seq.empty[ConsistencyError]
+
+    for (predAcc@PredicateAccess(args, name) <- this) {
+      this.findPredicateOptionally(name) match {
+        case None => // Consistency error already reported by checkIdentifiers
+        case Some(predDef) => {
+          if (!Consistency.areAssignable(args, predDef.formalArgs)) {
+            s :+= ConsistencyError(
+              s"Predicate $name with formal arguments ${predDef.formalArgs} cannot be used with provided arguments $args.",
+              predAcc.pos
+            )
+          }
+        }
+      }
+    }
+
+    s
+  }
+
   /** Checks that the applied domain functions exists, that the arguments of function applications are assignable to
     * formalArgs, that the type of function applications matches with the type of the function definition and that also
     * the name of the domain matches.
@@ -264,6 +287,8 @@ case class Program(domains: Seq[Domain], fields: Seq[Field], functions: Seq[Func
     }
   }
 
+  def findPredicateOptionally(name: String): Option[Predicate] = this.predicates.find(_.name == name)
+
   def findPredicate(name: String): Predicate = {
     this.predicates.find(_.name == name) match {
       case Some(p) => p

diff --git a/src/test/scala/ConsistencyTests.scala b/src/test/scala/ConsistencyTests.scala
@@ -127,6 +127,13 @@ class ConsistencyTests extends AnyFunSuite with Matchers {
         body          = None
       )()
 
+    val pred =
+      Predicate(
+        name          = "P",
+        formalArgs    = Seq(LocalVarDecl("x", Int)()),
+        body          = None
+      )()
+
     val callerIntVarDecl = LocalVarDecl("intRes", Int)()
     val callerIntVar = LocalVar("intRes", Int)()
     val callerBoolVarDecl = LocalVarDecl("boolRes", Bool)()
@@ -147,23 +154,35 @@ class ConsistencyTests extends AnyFunSuite with Matchers {
         Seq()
       )()
 
+    val callerPosts =
+      Seq(
+        // Wrong: zero arguments
+        PredicateAccessPredicate(PredicateAccess(Seq(), "P")(), FullPerm()())(),
+        // Wrong: wrong argument type
+        PredicateAccessPredicate(PredicateAccess(Seq(callerBoolVar), "P")(), FullPerm()())(),
+        // Correct
+        PredicateAccessPredicate(PredicateAccess(Seq(callerIntVar), "P")(), FullPerm()())()
+      )
+
     val caller =
       Method(
         name          = "caller",
         formalArgs    = Seq(),
         formalReturns = Seq(callerIntVarDecl, callerBoolVarDecl),
         pres          = Seq(),
-        posts         = Seq(),
+        posts         = callerPosts,
         body          = Some(callerBody)
       )()
 
     val program =
-      Program(domains    = Seq(), fields     = Seq(), functions  = Seq(func), predicates = Seq(), methods    = Seq(caller), extensions = Seq())()
+      Program(domains    = Seq(), fields     = Seq(), functions  = Seq(func), predicates = Seq(pred), methods    = Seq(caller), extensions = Seq())()
 
     program.checkTransitively shouldBe Seq(
       ConsistencyError("Function f with formal arguments List(x: Int) cannot be applied to provided arguments List().", NoPosition),
       ConsistencyError("No matching function f found of return type Bool, instead found with return type Int.", NoPosition),
       ConsistencyError("Function f with formal arguments List(x: Int) cannot be applied to provided arguments List(boolRes).", NoPosition),
+      ConsistencyError("Predicate P with formal arguments List(x: Int) cannot be used with provided arguments List().", NoPosition),
+      ConsistencyError("Predicate P with formal arguments List(x: Int) cannot be used with provided arguments List(boolRes).", NoPosition),
       ConsistencyError("No matching identifier g found of type Function.", NoPosition)
     )
   }