y# This is a combination of 2 commits.

Improve equivalence checking: function call matching, norm, mkTest
epfl-lara · Sep 26, 2022 · 9a945fa · 9a945fa
1 parent 33158cb
commit 9a945fa
Show file tree

Hide file tree

Showing 9 changed files with 599 additions and 160 deletions.
diff --git a/core/src/main/scala/stainless/Component.scala b/core/src/main/scala/stainless/Component.scala
@@ -44,6 +44,13 @@ object optModels extends inox.OptionDef[Seq[String]] {
   val usageRhs = "f1,f2,..."
 }
 
+object optNorm extends inox.OptionDef[String] {
+  val name = "norm"
+  val default = ""
+  val parser = inox.OptionParsers.stringParser
+  val usageRhs = "f"
+}
+
 trait ComponentRun { self =>
   val component: Component
   val trees: ast.Trees

diff --git a/core/src/main/scala/stainless/MainHelpers.scala b/core/src/main/scala/stainless/MainHelpers.scala
@@ -30,6 +30,7 @@ trait MainHelpers extends inox.MainHelpers { self =>
     optFunctions -> Description(General, "Only consider functions f1,f2,..."),
     optCompareFuns -> Description(General, "Only consider functions f1,f2,... for equivalence checking"),
     optModels -> Description(General, "Consider functions f1, f2, ... as model functions for equivalence checking"),
+    optNorm -> Description(General, "Use function f as normalization function for equivalence checking"),
     extraction.utils.optDebugObjects -> Description(General, "Only print debug output for functions/adts named o1,o2,..."),
     extraction.utils.optDebugPhases -> Description(General, {
       // f interpolator does not process escape sequence, we workaround that with the following trick.

diff --git a/core/src/main/scala/stainless/Report.scala b/core/src/main/scala/stainless/Report.scala
@@ -96,15 +96,19 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType =>
     case Level.Error   => Console.RED
   }
 
-  def hasError(identifier: Identifier)(using inox.Context): Boolean = {
-    annotatedRows.exists(elem => elem match {
-      case RecordRow(id, pos, level, extra, time) => level == Level.Error && id == identifier
+  def hasError(identifier: Option[Identifier])(using inox.Context): Boolean = identifier match {
+    case None => false
+    case Some(i) => annotatedRows.exists(elem => elem match {
+      case RecordRow(id, pos, level, extra, time) => {
+        (level == Level.Error && id == i)
+      }
     })
   }
 
-  def hasUnknown(identifier: Identifier)(using inox.Context): Boolean = {
-    annotatedRows.exists(elem => elem match {
-      case RecordRow(id, pos, level, extra, time) => level == Level.Warning && id == identifier
+  def hasUnknown(identifier: Option[Identifier])(using inox.Context): Boolean = identifier match {
+    case None => false
+    case Some(i) => annotatedRows.exists(elem => elem match {
+      case RecordRow(id, pos, level, extra, time) => level == Level.Warning && id == i
     })
   }
 

diff --git a/core/src/main/scala/stainless/extraction/package.scala b/core/src/main/scala/stainless/extraction/package.scala
@@ -24,7 +24,7 @@ package stainless
 package object extraction {
 
   val phases: Seq[(String, String)] = Seq(
-    "UserFiltering"             -> "Removes all the library functions not used by the user",
+    "UserFiltering"             -> "Remove all the library functions not used by the user",
     "Preprocessing"             -> "A preprocessing phase before the pipeline",
     "PartialFunctions"          -> "Lift partial function preconditions",
     "XlangLowering"             -> "Lowering phase at the end of xlang phases",
@@ -54,8 +54,8 @@ package object extraction {
     "ChooseEncoder"             -> "Encodes chooses as functions",
     "FunctionInlining"          -> "Transitively inline marked functions",
     "LeonInlining"              -> "Transitively inline marked functions (closer to what Leon did)",
-    "Trace"                     -> "Apply the traceInduct tactic during verification of the annotated function.",
-    "SizedADTExtraction"        -> "Transforms calls to 'indexedAt' to the 'SizedADT' tree",
+    "Trace"                     -> "Compare --compareFuns functions for equivalence. Expand @traceInduct",
+    "SizedADTExtraction"        -> "Transform calls to 'indexedAt' to the 'SizedADT' tree",
     "InductElimination"         -> "Replace @induct annotation by explicit recursion",
     "MeasureInference"          -> "Infer and inject measures in recursive functions",
     "PartialEvaluation"         -> "Partially evaluate marked function calls",