Merge branch 'main' into sam/updateInox

core/src/main/scala/stainless/MainHelpers.scala

@@ -75,6 +75,7 @@ trait MainHelpers extends inox.MainHelpers { self =>
     frontend.optExtraDeps -> Description(General, "Fetch the specified extra source dependencies and add their source files to the session"),
     frontend.optExtraResolvers -> Description(General, "Extra resolvers to use to fetch extra source dependencies"),
     utils.Caches.optCacheDir -> Description(General, "Specify the directory in which cache files should be stored"),
+    utils.Caches.optBinaryCache -> Description(General, "Set Binary mode for the cache instead of Hash mode, i.e., the cache will contain the entire VC and program in serialized format. This is less space efficient."),
     testgen.optOutputFile -> Description(TestsGeneration, "Specify the output file"),
     testgen.optGenCIncludes -> Description(TestsGeneration, "(GenC variant only) Specify header includes"),
     equivchk.optCompareFuns -> Description(EquivChk, "Only consider functions f1,f2,... for equivalence checking"),

core/src/main/scala/stainless/utils/Caches.scala

@@ -30,6 +30,14 @@ object Caches {
     override val usageRhs = "DIR"
   }
 
+  object optBinaryCache extends inox.FlagOptionDef("binary-cache", false)
+
+  /**
+    * Return the filename for the cache file, depending on the type of cache (Hash or Binary).
+    */
+  def getCacheFilename(ctx: inox.Context): String = 
+    if (ctx.options.findOptionOrDefault(optBinaryCache)) "vccachebin.bin" else "vccachehash.bin" 
+
   /**
    * Get the cache file after creating the cache directory.
    *

core/src/main/scala/stainless/verification/VerificationCache.scala

@@ -15,6 +15,10 @@ import scala.util.{ Success, Failure }
 
 import inox.solvers.SolverFactory
 
+// For Hashing
+import java.security.MessageDigest
+import java.util.HexFormat
+
 object DebugSectionCacheHit extends inox.DebugSection("cachehit")
 object DebugSectionCacheMiss extends inox.DebugSection("cachemiss")
 
@@ -37,6 +41,8 @@ trait VerificationCache extends VerificationChecker { self =>
 
   private lazy val vccache = CacheLoader.get(context)
 
+  private val binaryCacheFlag = context.options.findOptionOrDefault(utils.Caches.optBinaryCache)
+
   override def checkVC(vc: VC, origVC: VC, sf: SolverFactory { val program: self.program.type }) = {
     reporter.debug(s" - Checking cache: '${vc.kind}' VC for ${vc.fid} @${vc.getPos}...")(using DebugSectionVerification)
 
@@ -51,9 +57,12 @@ trait VerificationCache extends VerificationChecker { self =>
       val (canonicalSymbols, canonicalExpr): (Symbols, Expr) =
         utils.Canonization(program)(program.symbols, vc.condition)
 
-      val key = serializer.serialize((vc.satisfiability, canonicalSymbols, canonicalExpr))
 
-      if (vccache `contains` key) {
+      val serialized = serializer.serialize((vc.satisfiability, canonicalSymbols, canonicalExpr))
+
+      val key: CacheKey = vccache.computeKey(serialized.bytes)
+      reporter.debug(s"Cache key size: ${key.content.size} bytes")(using DebugSectionVerification)
+      if (vccache.contains(key)) {
         reporter.debug(s"Cache hit: '${vc.kind}' VC for ${vc.fid.asString} @${vc.getPos}...")(using DebugSectionVerification)
         given DebugSectionCacheHit.type = DebugSectionCacheHit
         reporter.synchronized {
@@ -68,9 +77,8 @@ trait VerificationCache extends VerificationChecker { self =>
           reporter.ifDebug { debug =>
             given DebugSectionCacheMiss.type = DebugSectionCacheMiss
             given PrinterOptions = new PrinterOptions(printUniqueIds = true, printTypes = true, symbols = Some(canonicalSymbols))
-
+            
             debugVC(vc, origVC)
-
             debug("Canonical symbols:")
             debug(" ## SORTS ##")
             debug(canonicalSymbols.sorts.values.map(_.asString).toList.sorted.mkString("\n\n"))
@@ -103,18 +111,64 @@ object VerificationCache {
   private val serializer = utils.Serializer(stainless.trees)
   import serializer.{given, _}
 
+  object CacheKey{
+    def apply(content: Seq[Byte]): CacheKey = CacheKey(content.toArray)
+  }
+  case class CacheKey(content: Array[Byte]){
+    override def equals(that: Any): Boolean = that match {
+      case c: CacheKey => java.util.Arrays.equals(content, c.content)
+      case _ => false
+    }
+    override val hashCode: Int = java.util.Arrays.hashCode(content)
+
+    def toSeq: Seq[Byte] = content.toSeq
+  }
+
   /** Cache with the ability to save itself to disk. */
-  private class Cache(cacheFile: File) {
+  private class Cache(ctx: inox.Context, cacheFile: File) {
+    val hashingFunctionName = "SHA-256"
+    val hashSize = MessageDigest.getInstance(hashingFunctionName).getDigestLength()
+    val hashCache = !ctx.options.findOptionOrDefault(utils.Caches.optBinaryCache)
+
     // API
-    def contains(key: SerializationResult): Boolean = underlying contains key
-    def +=(key: SerializationResult) = underlying += key -> unusedCacheValue
-    def addPersistently(key: SerializationResult): Unit = {
+    def computeKey(content: Array[Byte]): CacheKey = 
+      if(hashCache) {
+        val bytes = MessageDigest.getInstance(hashingFunctionName).digest(content)
+        CacheKey(bytes)
+      } else {
+        CacheKey(content)
+      }
+    def contains(key: CacheKey): Boolean = underlying.contains(key)
+    def +=(key: CacheKey) = underlying += key -> unusedCacheValue
+    def addPersistently(key: CacheKey): Unit = {
       this += key
-      this.synchronized { serializer.serialize(key, out) }
+      this.synchronized { CacheKeySerializer.serialize(key, out) }
+    }
+
+    object CacheKeySerializer {
+      def serialize(key: CacheKey, out: OutputStream): Unit = {
+        if(hashCache){
+          assert(key.content.size == hashSize)
+          out.write(key.content)
+        } else {
+          serializer.serialize(key.toSeq, out)
+        }
+      }
+
+      def deserialize(in: InputStream): CacheKey = {
+        if(hashCache){
+          val bytes = new Array[Byte](hashSize)
+          if (in.available() < hashSize) throw new java.io.EOFException()
+          in.read(bytes)
+          CacheKey(bytes)
+        } else {
+          CacheKey(serializer.deserialize[Seq[Byte]](in))
+        }
+      }
     }
 
     // Implementation details
-    private val underlying = TrieMap[SerializationResult, Unit]() // Thread safe
+    private val underlying = TrieMap[CacheKey, Unit]() // Thread safe
     private val unusedCacheValue = ()
 
     // output stream used to save verified VCs
@@ -164,18 +218,18 @@ object VerificationCache {
      *      while being loaded!
      */
     def get(ctx: inox.Context): Cache = this.synchronized {
-      val cacheFile: File = utils.Caches.getCacheFile(ctx, "vccache.bin")
+      val cacheFile: File = utils.Caches.getCacheFile(ctx, utils.Caches.getCacheFilename(ctx))
 
       db.getOrElse(cacheFile, {
-        val cache = new Cache(cacheFile)
+        val cache = new Cache(ctx, cacheFile)
 
         if (cacheFile.exists) {
           val in = openStream(ctx, cacheFile)
 
           try {
             while (true) {
-              val s = serializer.deserialize[SerializationResult](in)
-              cache += s
+              val ck = cache.CacheKeySerializer.deserialize(in)
+              cache += ck
             }
           } catch {
             case e: java.io.EOFException => // Silently consume expected exception.

core/src/main/scala/stainless/verification/VerificationChecker.scala

@@ -379,8 +379,13 @@ trait VerificationChecker { self =>
               reporter.warning(vc.getPos, " => INVALID")
               reason match {
                 case VCStatus.CounterExample(cex) =>
-                  reporter.warning("Found counter-example:")
-                  reporter.warning("  " + cex.asString.replaceAll("\n", "\n  "))
+                  vc.kind match {
+                    case VCKind.MeasureMissing =>
+                      reporter.warning("Measure is missing, cannot check termination")
+                    case _ =>
+                      reporter.warning("Found counter-example:")
+                      reporter.warning("  " + cex.asString.replaceAll("\n", "\n  "))
+                  }
 
                 case VCStatus.Unsatisfiable =>
                   reporter.warning("Property wasn't satisfiable")

docs/RELEASE_NOTES.md

@@ -1,13 +1,15 @@
 # Release Notes
 
-## Version 0.9.8.8.7 (2024-09-15)
+## Version 0.9.8.9 (2024-10-19)
 
+- Default cache now only stores SHA-256 hash of formulas ( -binary-cache=true for old version)
 - Scala version is now 3.5.0
 - Inox now has a solver for ground assertions based on internal evaluator (Inox #218), called `eval`
 - Opaque Forall and ensures: help higher order contracts (#1567)
 - Option `--compact` also reduces progress messages (#1573)
 - Changed CI to use GitHub actions
 - Documented a limited use of `throw`
+- CI scripts as part of move to GitHub actions
 
 ## Version 0.9.8.8 (2024-08-22)
 

frontends/benchmarks/extraction/valid/Typedefs3.scala

@@ -0,0 +1,18 @@
+import stainless.lang.Set
+import stainless.lang.Bag
+import stainless.collection.List
+import stainless.lang.Map
+import stainless.lang.MutableMap
+
+object Typedefs3 {
+  type TypeSet[A] = Set[List[A]]
+  type TypeBag[A] = Bag[List[A]]
+  type TypeMap[A] = Map[Int, List[A]]
+  type TypeMutableMap[A] = MutableMap[Int, List[A]]
+
+  val t: TypeSet[Int] = Set(List(1, 2, 3), List(4, 5, 6))
+  val b: TypeBag[Int] = Bag((List(1, 2, 3), BigInt(3)), (List(4, 5, 6), BigInt(2)))
+  val m: TypeMap[Int] = Map(1 -> List(1, 2, 3), 2 -> List(4, 5, 6))
+  val mm: TypeMutableMap[Int] = MutableMap.withDefaultValue[Int, List[Int]](() => List(1, 2, 3))
+
+}

frontends/common/src/it/scala/stainless/verification/SatPrecondVerificationSuite.scala

@@ -19,7 +19,7 @@ class SatPrecondVerificationSuite extends VerificationComponentTestSuite {
     Set()
 
   private val ignorePrincess: Set[String] = ignoreCommon ++
-    Set()
+    Set("sat-precondition/valid/SATPrecond4")
 
   private val ignoreCodegen: Set[String] = Set()
 
@@ -46,7 +46,9 @@ class SatPrecondVerificationSuite extends VerificationComponentTestSuite {
             inox.optSelectedSolvers(Set(solver)),
             inox.solvers.optCheckModels(true),
             evaluators.optCodeGen(codeGen),
+            inox.optTimeout(3.seconds),
             inox.solvers.unrolling.optFeelingLucky(codeGen)) ++ seq
+
       }
     } yield conf
   }

frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala

@@ -2362,19 +2362,31 @@ class CodeExtraction(inoxCtx: inox.Context,
       case tpe if isStringSym(tpe.typeSymbol) => xt.StringType()
 
       case AppliedType(tr: TypeRef, Seq(tp)) if isSetSym(tr.symbol) =>
+        // We know the underlying is a set, but it may be hidden under an alias
+        // just as for Tuple below
+        val AppliedType(_, Seq(tp)) = tpt.dealias: @unchecked
         xt.SetType(extractType(tp))
 
       case AppliedType(tr: TypeRef, Seq(tp)) if isBagSym(tr.symbol) =>
+        // We know the underlying is a bag, but it may be hidden under an alias
+        // just as for Tuple below
+        val AppliedType(_, Seq(tp)) = tpt.dealias: @unchecked
         xt.BagType(extractType(tp))
 
       case FrontendBVType(signed, size) =>
         xt.AnnotatedType(xt.BVType(signed, size), Seq(xt.StrictBV))
 
       case AppliedType(tr: TypeRef, tps) if isMapSym(tr.symbol) =>
+        // We know the underlying is a map, but it may be hidden under an alias
+        // just as for Tuple below
+        val AppliedType(_, tps) = tpt.dealias: @unchecked
         val Seq(from, to) = tps map extractType
         xt.MapType(from, xt.ClassType(getIdentifier(optionSymbol), Seq(to)).setPos(pos))
 
       case AppliedType(tr: TypeRef, tps) if isMutableMapSym(tr.symbol) =>
+        // We know the underlying is a map, but it may be hidden under an alias
+        // just as for Tuple below
+        val AppliedType(_, tps) = tpt.dealias: @unchecked
         val Seq(from, to) = tps map extractType
         xt.MutableMapType(from, to)
 

frontends/library/stainless/lang/Set.scala

@@ -23,68 +23,89 @@ object Set {
     new Set(set)
   }
 
-  @extern @pure @library
-  def mkString[A](set: Set[A], infix: String)(format: A => String): String = {
-    set.theSet.map(format).toList.sorted.mkString(infix)
-  }
+  // @extern @pure @library
+  // def mkString[A](set: Set[A], infix: String)(format: A => String): String = {
+  //   set.theSet.map(format).toList.sorted.mkString(infix)
+  // }
+
+  extension[A](set: Set[A]) {
 
-  @library
-  implicit class SetOps[A](val set: Set[A]) extends AnyVal {
+    @library @extern @pure
+    def exists(p: A => Boolean): Boolean = {
+      set.theSet.exists(p)
+    }.ensuring(res => res == set.toList.exists(p))
 
-    @extern @pure
+    @library @extern @pure
+    def forall(p: A => Boolean): Boolean = {
+      set.theSet.forall(p)
+    }.ensuring(res => res == set.toList.forall(p))
+
+    @library @extern @pure
     def map[B](f: A => B): Set[B] = {
       new Set(set.theSet.map(f))
     }
 
-    @extern @pure
+    @library @extern @pure
     def mapPost1[B](f: A => B)(a: A): Unit = {
       ()
-   }.ensuring { _ =>
+    }.ensuring { _ =>
       !set.contains(a) || map[B](f).contains(f(a))
     }
 
-    @extern @pure
+    @library @extern @pure
     def mapPost2[B](f: A => B)(b: B): A = {
       require(map[B](f).contains(b))
       (??? : A)
-   }.ensuring { (a:A) =>
+    }.ensuring { (a:A) =>
       b == f(a) && set.contains(a)
     }
 
-    @extern @pure
+    @library @extern @pure
+    def flatMap[B](f: A => Set[B]): Set[B] = {
+      new Set(set.theSet.flatMap(f(_).theSet))
+    }
+
+    @library @extern @pure
+    def flatMapPost[B](f: A => Set[B])(b: B) = {
+      (??? : A)
+    }.ensuring { _ =>
+      set.flatMap(f).contains(b) == set.exists(a => f(a).contains(b))
+    }
+
+    @library @extern @pure
     def filter(p: A => Boolean): Set[A] = {
       new Set(set.theSet.filter(p))
     }
 
-    @extern @pure
+    @library @extern @pure
     def filterPost(p: A => Boolean)(a: A): Unit = {
       ()
    }.ensuring (_ => filter(p).contains(a) == (p(a) && set.contains(a)))
 
-    @extern @pure
+    @library @extern @pure
     def withFilter(p: A => Boolean): Set[A] = {
       new Set(set.theSet.filter(p))
     }
 
-    @extern @pure
+    @library @extern @pure
     def withFilterPost(p: A => Boolean)(a: A): Unit = {
       ()
    }.ensuring(_ => withFilter(p).contains(a) == (p(a) && set.contains(a)))
 
-    @extern @pure
+    @library @extern @pure
     def toList: List[A] = {
       List.fromScala(set.theSet.toList)
    }.ensuring(res => ListOps.noDuplicate(res) && res.content == set)
 
-    @extern @pure
+    @library @extern @pure
     def toListPost(a:A): Unit = {
       ()
    }.ensuring(_ => toList.contains(a) == set.contains(a))
 
-    @extern @pure
+    @library @extern @pure
     def toScala: ScalaSet[A] = set.theSet
 
-    @extern @pure
+    @library @extern @pure
     def mkString(infix: String)(format: A => String): String = {
       set.theSet.map(format).toList.sorted.mkString(infix)
     }