Support 'require' and 'ensuring' message overloads

epfl-lara · Mar 1, 2023 · 4422f93 · 4422f93
1 parent 87b66ff
commit 4422f93
Show file tree

Hide file tree

Showing 7 changed files with 60 additions and 12 deletions.
diff --git a/frontends/benchmarks/verification/valid/RequireEnsuringMessages.scala b/frontends/benchmarks/verification/valid/RequireEnsuringMessages.scala
@@ -0,0 +1,15 @@
+object RequireEnsuringMessages {
+  case class MyClass(a: Int) {
+    require(a > 0, "a must be strictly positive")
+  }
+
+  def useMyClass(mc: MyClass): Int = {
+    assert(mc.a > 0, "a is surely strictly positive")
+    mc.a
+  }.ensuring(_ > -42, "trivially trivial")
+
+  def createMyClass(a: Int): MyClass = {
+    require(a > 0, "To create MyClass, a must be strictly positive")
+    MyClass(a)
+  }
+}
diff --git a/frontends/benchmarks/verification/valid/RequireEnsuringMessagesStaticChecks.scala b/frontends/benchmarks/verification/valid/RequireEnsuringMessagesStaticChecks.scala
@@ -0,0 +1,17 @@
+import stainless.lang.StaticChecks._
+
+object RequireEnsuringMessages {
+  case class MyClass(a: Int) {
+    require(a > 0, "a must be strictly positive")
+  }
+
+  def useMyClass(mc: MyClass): Int = {
+    assert(mc.a > 0, "a is surely strictly positive")
+    mc.a
+  }.ensuring(_ > -42, "trivially trivial")
+
+  def createMyClass(a: Int): MyClass = {
+    require(a > 0, "To create MyClass, a must be strictly positive")
+    MyClass(a)
+  }
+}
diff --git a/frontends/dotty/src/main/scala/stainless/frontends/dotc/ASTExtractors.scala b/frontends/dotty/src/main/scala/stainless/frontends/dotc/ASTExtractors.scala
@@ -1026,10 +1026,12 @@ trait ASTExtractors {
       * first call in the block). */
     object ExRequiredExpression {
       def unapply(tree: tpd.Apply): Option[(tpd.Tree, Boolean)] = tree match {
-        case Apply(ExSymbol("scala", "Predef$", "require"), Seq(body)) =>
+        // An optional message may comes after `body`, but we do not make use of it.
+        case Apply(ExSymbol("scala", "Predef$", "require"), body +: _) =>
           Some((body, false))
 
-        case Apply(ExSymbol("stainless", "lang", "StaticChecks$", "require"), Seq(body)) =>
+        // Ditto
+        case Apply(ExSymbol("stainless", "lang", "StaticChecks$", "require"), body +: _) =>
           Some((body, true))
 
         case _ => None
@@ -1106,14 +1108,16 @@ trait ASTExtractors {
 
     object ExEnsuredExpression {
       def unapply(tree: tpd.Tree): Option[(tpd.Tree, tpd.Tree, Boolean)] = tree match {
+        // An optional message may comes after `contract`, but we do not make use of it.
         case ExCall(Some(rec),
           ExSymbol("scala", "Predef$", "Ensuring", "ensuring"),
-          _, Seq(contract)
+          _, contract +: _
         ) => Some((rec, contract, false))
 
+        // Ditto
         case ExCall(Some(rec),
           ExSymbol("stainless", "lang", "StaticChecks$", "Ensuring", "ensuring"),
-          _, Seq(contract)
+          _, contract +: _
         ) => Some((rec, contract, true))
 
         case _ => None

diff --git a/frontends/dotty/src/main/scala/stainless/frontends/dotc/FragmentChecker.scala b/frontends/dotty/src/main/scala/stainless/frontends/dotc/FragmentChecker.scala
@@ -247,7 +247,7 @@ class FragmentChecker(inoxCtx: inox.Context)(using override val dottyCtx: DottyC
 
     val RequireMethods =
       defn.ScalaPredefModule.info.decl(Names.termName("require")).alternatives.toSet
-        + Symbols.requiredModule("stainless.lang.StaticChecks").info.decl(Names.termName("require"))
+        ++ Symbols.requiredModule("stainless.lang.StaticChecks").info.decl(Names.termName("require")).alternatives.toSet
 
     private val stainlessReplacement = mutable.Map(
       defn.ListClass -> "stainless.collection.List",

diff --git a/frontends/library/stainless/lang/StaticChecks.scala b/frontends/library/stainless/lang/StaticChecks.scala
@@ -6,7 +6,9 @@ object StaticChecks {
 
   @library
   implicit class Ensuring[A](val x: A) extends AnyVal {
-    def ensuring(@ghost cond: (A) => Boolean): A = x
+    def ensuring(@ghost cond: A => Boolean): A = x
+
+    def ensuring(@ghost cond: A => Boolean, msg: => String): A = x
   }
 
   @library @ignore
@@ -28,8 +30,14 @@ object StaticChecks {
   @library
   def require(@ghost pred: => Boolean): Unit = ()
 
+  @library
+  def require(@ghost pred: => Boolean, msg: => String): Unit = ()
+
   @library
   def assert(@ghost pred: => Boolean): Unit = ()
 
+  @library
+  def assert(@ghost pred: => Boolean, msg: => String): Unit = ()
+
 }
 
diff --git a/frontends/scalac/src/main/scala/stainless/frontends/scalac/ASTExtractors.scala b/frontends/scalac/src/main/scala/stainless/frontends/scalac/ASTExtractors.scala
@@ -236,14 +236,16 @@ trait ASTExtractors(val global: Global) {
     /** Extracts the 'ensuring' contract from an expression. */
     object ExEnsuredExpression {
       def unapply(tree: Apply): Option[(Tree,Tree,Boolean)] = tree match {
+        // An optional message may comes after `contract`, but we do not make use of it.
         case Apply(Select(Apply(TypeApply(
               ExSelected("scala", "Predef", "Ensuring"),
-              _ :: Nil), body :: Nil), ExNamed("ensuring")), contract :: Nil)
+              _ :: Nil), body :: Nil), ExNamed("ensuring")), contract :: _)
           => Some((body, contract, false))
 
+        // Ditto
         case Apply(Select(Apply(TypeApply(
               ExSelected("stainless", "lang", "StaticChecks", "Ensuring"),
-              _ :: Nil), body :: Nil), ExNamed("ensuring")), contract :: Nil)
+              _ :: Nil), body :: Nil), ExNamed("ensuring")), contract :: _)
           => Some((body, contract, true))
 
         case _ => None
@@ -381,10 +383,12 @@ trait ASTExtractors(val global: Global) {
      * first call in the block). */
     object ExRequiredExpression {
       def unapply(tree: Apply): Option[(Tree, Boolean)] = tree match {
-        case Apply(ExSelected("scala", "Predef", "require"), contractBody :: Nil) =>
+        // An optional message may comes after `contractBody`, but we do not make use of it.
+        case Apply(ExSelected("scala", "Predef", "require"), contractBody :: _) =>
           Some((contractBody, false))
 
-        case Apply(ExSelected("stainless", "lang", "StaticChecks", "require"), contractBody :: Nil) =>
+        // Ditto
+        case Apply(ExSelected("stainless", "lang", "StaticChecks", "require"), contractBody :: _) =>
           Some((contractBody, true))
 
         case _ => None

diff --git a/frontends/scalac/src/main/scala/stainless/frontends/scalac/FragmentChecker.scala b/frontends/scalac/src/main/scala/stainless/frontends/scalac/FragmentChecker.scala
@@ -209,8 +209,8 @@ trait FragmentChecker extends SubComponent { self: StainlessExtraction =>
       ++ rootMirror.getRequiredModule("scala.math.BigInt").info.decl(nme.apply).alternatives).toSet
 
     val RequireMethods =
-      (definitions.PredefModule.info.decl(newTermName("require")).alternatives.toSet
-        + rootMirror.getRequiredModule("stainless.lang.StaticChecks").info.decl(newTermName("require")))
+      definitions.PredefModule.info.decl(newTermName("require")).alternatives.toSet
+        ++ rootMirror.getRequiredModule("stainless.lang.StaticChecks").info.decl(newTermName("require")).alternatives.toSet
 
 
     private val stainlessReplacement = mutable.Map(