Merge branch 'main' into sam/hashmap_getkeys

.github/workflows/bolts-CI.yml

@@ -10,22 +10,30 @@ jobs:
     runs-on: [self-hosted, linux]
     env:
       # define Java options for both official sbt and sbt-extras
-      JAVA_OPTS: -Dsbt.io.implicit.relative.glob.conversion=allow -Xss512M -Xms1024M -Xmx12G -XX:MaxMetaspaceSize=2G -XX:+UseCodeCacheFlushing -XX:ReservedCodeCacheSize=768M
-      JVM_OPTS:  -Dsbt.io.implicit.relative.glob.conversion=allow -Xss512M -Xms1024M -Xmx12G -XX:MaxMetaspaceSize=2G -XX:+UseCodeCacheFlushing -XX:ReservedCodeCacheSize=768M
+      JAVA_OPTS: -Dsbt.io.implicit.relative.glob.conversion=allow -Xss512M -Xms1024M -Xmx12G -XX:MaxMetaspaceSize=2G -XX:+UseCodeCacheFlushing -XX:ReservedCodeCacheSize=768M 
+      JVM_OPTS:  -Dsbt.io.implicit.relative.glob.conversion=allow -Xss512M -Xms1024M -Xmx12G -XX:MaxMetaspaceSize=2G -XX:+UseCodeCacheFlushing -XX:ReservedCodeCacheSize=768M 
+      JAVA_OPTS_TMP_DIR: /tmp/tmp_${{ github.run_id }}_${{ github.run_attempt }}
     steps:
     - name: Checkout
       uses: actions/checkout@v4
       with:
         submodules: recursive
     - name: Setup JDK
-      uses: actions/setup-java@v3
+      uses: actions/setup-java@v4
       with:
         distribution: temurin
         java-version: 17
+    - name: Setup java options
+      run: |
+          echo "JAVA_OPTS=$JAVA_OPTS -Djava.io.tmpdir=$JAVA_OPTS_TMP_DIR" >> "$GITHUB_ENV" && \
+          echo "JVM_OPTS=$JVM_OPTS -Djava.io.tmpdir=$JAVA_OPTS_TMP_DIR" >> "$GITHUB_ENV" && \
+          echo "SBT_OPTS=-Djava.io.tmpdir=$JAVA_OPTS_TMP_DIR --sbt-dir $JAVA_OPTS_TMP_DIR" >> "$GITHUB_ENV"
+    - name: Creating temp folder
+      run: rm -rf $JAVA_OPTS_TMP_DIR && mkdir -p $JAVA_OPTS_TMP_DIR && chmod 777 $JAVA_OPTS_TMP_DIR
     - name: Install stainless and solvers
-      run: ./install_stainless_and_solvers.sh $GITHUB_WORKSPACE/.local/bin $GITHUB_WORKSPACE/.local
+      run: ./install_stainless_and_solvers.sh $GITHUB_WORKSPACE/.local/bin $GITHUB_WORKSPACE/.local && echo "PATH=$GITHUB_WORKSPACE/.local/bin:$PATH" >> "$GITHUB_ENV"
     - name: Add stainless to PATH
-      run: echo "$GITHUB_WORKSPACE/.local/stainless/frontends/dotty/target/universal/stage/bin" >> $GITHUB_PATH
+      run: echo "$GITHUB_WORKSPACE/.local/stainless/frontends/dotty/target/universal/stage/bin" >> $GITHUB_PATH && echo "PATH=$GITHUB_WORKSPACE/.local/stainless/frontends/dotty/target/universal/stage/bin:$PATH" >> "$GITHUB_ENV"
     - name: Test stainless availability
       run: stainless-dotty --version
     - name: Add solvers to PATH

data-structures/uarray/UArrayExample.scala

@@ -88,15 +88,19 @@ object UArrayExample:
   end UArray
 
   object UArray:
-    @extern
-    def ofSize[T: ClassTag](size: Int): UArray[T] = {
-      require(0 <= size)
+    @extern @ignore // used because `new Array[T]` leaks out of @extern due to some compiler magic
+    def _ofSize[T: ClassTag](size: Int): UArray[T] = {
       @ghost val definedNot = Array.fill(size)(false)
       given ct: realClassTag[T] = summon[ClassTag[T]].real
       val content = new Array[T](size)
       UArray[T](content, size, definedNot)
-    }.ensuring(res => res.size == size)
+    }
 
+    @extern
+    def ofSize[T: ClassTag](size: Int): UArray[T] = {
+      require(0 <= size)
+      _ofSize[T](size)
+    }.ensuring(res => res.size == size)
 
   end UArray
 

run-one-test.sh

@@ -23,26 +23,28 @@ function run_tests {
   # Check if there is a verify.sh file in the project folder
   # If yes, then echo a message saying we run it and its content, then run it, other run the command X
   status=-1
+  # find .
+  # find /tmp/
   if [ -f "$project/verify.sh" ]; then
     echo "Running verify.sh script in bolts project: $project..."
     cd "$project"
     echo "$ cat ./verify.sh"
     cat "./verify.sh"
     echo ""
     if [ "$ADMIT_VCS" = true ]; then
-      bash "./verify.sh" "--compact" "--admit-vcs=true"
+      bash "./verify.sh" "--compact" "--admit-vcs=true" "--debug=stack"
     else
-      bash "./verify.sh" "--compact"
+      bash "./verify.sh" "--compact" "--debug=stack"
     fi
     status=$?
     cd -
   else
     echo "Running '$STAINLESS --config-file=$conf $@' on bolts project: $project..."
     echo "$ find $project -name '*.scala' -exec $STAINLESS --config-file=$conf $@ {} +"
     if [ "$ADMIT_VCS" = true ]; then
-      find "$project" -name '*.scala' -exec $STAINLESS "--config-file=$conf" "--compact" "--admit-vcs=true" "$@" {} +
+      find "$project" -name '*.scala' -exec $STAINLESS "--config-file=$conf" "--compact" "--admit-vcs=true" "--debug=stack" "$@" {} +
     else
-      find "$project" -name '*.scala' -exec $STAINLESS "--config-file=$conf" "$@" {} +
+      find "$project" -name '*.scala' -exec $STAINLESS "--config-file=$conf" "--debug=stack" "$@" {} +
     fi
     status=$?
   fi

tctests.txt

@@ -32,3 +32,4 @@ tutorials/simple-transform
 tutorials/fmcad2021/alt-diffs
 tutorials/fmcad2021/binary-search
 tutorials/fmcad2021/find-index
+tutorials/explicit-memory

tutorials/explicit-memory/ExplicitMemory.scala

@@ -0,0 +1,105 @@
+import stainless.annotation.*
+import stainless.lang.*
+import scala.annotation.*
+object ExplicitMemory:
+
+  opaque type Ref[A] = Int
+  case class Mem(a: Array[Int], var free: Int):
+    require(0 <= free && free <= a.size)
+
+  @extern
+  def initMem(size: Int): Mem = {
+    Mem(Array.tabulate(size)(i => 0), 0)
+  }.ensuring(res => res.free == 0 && res.a.size == size)
+
+
+  inline def valid(addr: Int, k: Int)(using m: Mem): Boolean =
+    0 < k && 0 <= addr && addr <= m.free && k <= m.free - k
+
+  inline def valid(addr: Int)(using m: Mem): Boolean =
+    0 <= addr && addr < m.free // valid(addr, 1)
+
+  def available(k: Int)(using m: Mem): Boolean =
+    0 < k && m.free <= m.a.size && k <= m.a.size - m.free
+
+  def allocate(k: Int)(using m: Mem): Int =
+    require(available(k))
+    val res = m.free
+    m.free = m.free + k
+    res
+
+  def newInt(initVal: Int)(using m: Mem): Ref[Int] =
+    require(available(1))
+    val addr = allocate(1)
+    addr.fill(initVal)
+    addr
+
+  def newLong(initVal: Long)(using m: Mem): Ref[Long] =
+    require(available(2))
+    val addr = allocate(2)
+    addr.fill(initVal)
+    addr
+
+
+  extension (addr: Ref[Int])(using m: Mem)
+    def fill(v: Int): Unit =
+      require(valid(addr))
+      m.a(addr) = v
+
+    def :=(addrV: Ref[Int]): Unit =
+      require(valid(addr) && valid(addrV))
+      m.a(addr) = m.a(addrV)
+
+    def apply(): Int =
+      require(valid(addr))
+      m.a(addr)
+
+  extension (addr: Ref[Long])(using m: Mem)
+    def fill(v: Long): Unit = {
+      require(valid(addr) && valid(addr + 1))
+      m.a(addr) = (v >> 32).toInt
+      m.a(addr + 1) = (v & 0xFFFFFFFF).toInt    
+    }
+
+    def ::=(addrV: Ref[Long]): Unit =
+      require(valid(addr) && valid(addr + 1) && 
+              valid(addrV) && valid(addrV + 1))
+      m.a(addr) = m.a(addrV)
+      m.a(addr + 1) = m.a(addrV + 1)
+
+    @pure
+    def longValue: Long =
+      require(valid(addr) && valid(addr + 1))
+      val hi = m.a(addr).toLong << 32
+      val lo = m.a(addr + 1).toLong
+      hi + lo
+
+  def test2 =
+    given m: Mem = initMem(100)
+    val x = newInt(42)
+    val y = newInt(8)
+    {
+      val y = x
+      y := newInt(13)
+    }
+    var i = 0
+    (while i < 20 do
+      decreases(20 - i)
+      val t = newLong(0L)
+      i += 1).invariant(0 <= i && i <= 50 && available(50 - 2*i))
+
+  @main @extern
+  def test =
+    given m: Mem = initMem(100)
+    val x = newInt(42)
+    val y = newInt(8)
+    println(f"x == ${x()}, y == ${y()}")
+    {
+      val y = x
+      y := newInt(13)
+      println(f"x == ${x()}, y == ${y()}")
+    }
+    println(f"x == ${x()}, y == ${y()}")
+    var z = newLong(0L)
+    z = x
+    println(f"z == ${z.longValue}")

tutorials/futures/PossibleFutures.scala

@@ -3,51 +3,122 @@ import stainless.lang.*
 import stainless.lang.StaticChecks.*
 
 object PossibleFutures:
+  @extern
+  def sleep(t: Int): Unit =
+    Thread.sleep(scala.util.Random.nextInt(t))
+
+  def slow(x: Int): Int =
+    sleep(100)
+    x
+
+  @extern
+  def say(s: String): Unit =
+    println(s)
+
+  @extern
+  def myGet[A](opt: Option[A], s: String): A =
+    opt match
+      case Some(v) => 
+        say(s + " get succeeded ")
+        v
+      case None() =>
+        say(s + " get failed")
+        throw Exception("myGet failed")
 
   // constructure is private: enforce using Future.apply and hence asynchrony
-  class Future[A](private val todo : () => A):
+  class Future[R](private val todo : () => R):
     @ghost 
-    def expected: A = todo() // predicted value. Public, but spec only
+    def expected: R = todo() // predicted value. Public, but spec only
 
-    def await: A = {
+    def await: R = {
       todo()
     }.ensuring(_ == expected)
 
   object Future:
+    @ignore    
+    class FunctionThread[A,B](var input: Option[A] = None[A](),
+                              var output: Option[B] = None[B](),
+                              f: A => B) extends Thread:
+      def setInput(a: A): Unit = synchronized:
+        input match
+          case None() => 
+            input = Some(a)
+            this.notifyAll()
+          case _ => 
+            say("input double set!")
+
+      override def run: Unit = synchronized:
+        while input.isEmpty do
+          FunctionThread.this.wait()
+        if output.isEmpty then
+          output = Some(f(input.get))
+          FunctionThread.this.notifyAll()
+        else
+          say("output double set!")
+
+      def getOutput: B = synchronized:
+        while output.isEmpty do
+          FunctionThread.this.wait()
+        output.get
+    end FunctionThread
+
     @extern
     def apply[A](todo: () => A): Future[A] = {      
-      var result: Option[A] = None[A]()
-      val t = new Thread:        
-        override def run: Unit =
-          result = Some(todo())
-          println(f"Computed $result")
-
-      t.start               
-      def expandedTodo: A =
-        t.join
-        result.get
-
-      new Future[A](() => expandedTodo)
+      val t = FunctionThread(None[Unit](), None[A](), (_:Unit) => todo())
+      t.setInput(())
+      t.start            
+      new Future[A](() => t.getOutput)
     }.ensuring(_.expected == todo())
 
+    // Instead of general promises, we ask for body to depend on a future
+    @extern
+    def runBody[A,B](body: Future[A] => Future[B]): A => B =
+      val ta = FunctionThread[A,A](None[A](), None[A](), (x:A) => x)
+      ta.start
+
+      val fa = new Future[A](() => ta.getOutput)
+      val fb = body(fa)
+
+      def result(a:A): B =
+        ta.setInput(a)
+        fb.await
+
+      result
+    end runBody
+
+  // ------------------ Example -----------------
+
   def small(x:Int): Boolean = 
     -128 <= x && x < 127
 
-  @extern
-  def sleep(t: Int): Unit =
-    Thread.sleep(scala.util.Random.nextInt(t))
-
-  def slow(x: Int): Int =
-    sleep(100)
-    x
+  def addOne(x: Future[Int]): Int =
+    require(small(x.expected))    
+    x.await + 1
 
-  def addThree(x: Future[Int]) =  
-    require(small(x.expected))
+  def addThree(x: Future[Int]): Int =  
+    require(small(x.expected))    
     val two = Future(() => slow(1))
-    val one = Future(() => slow(2))
+    val one = Future(() => slow(2))    
     one.await + two.await + x.await
+
+  def addFour(x: Future[Int]) =  
+    require(small(x.expected))    
+    val two = Future(() => slow(1))
+    val one = Future(() => slow(2))    
+    val body: Future[Int] => Future[Int] =
+      (y: Future[Int]) =>
+        Future: () =>
+          val t: Int = one.await + two.await + x.await
+          say("Already did some useful work!")
+          val yres = y.await
+          if small(yres) then t + y.await
+          else 0
+    val f = Future.runBody(body)
+    val yv: Int = slow(slow(50))
+    say("Only now we provide the argument")
+    f(yv) 
 
   // run to observe that values are computed asynchronously 
   @main @extern
   def test =
-    println(f"The result is: ${addThree(Future(() => slow(100)))}")
+    println(f"The result is: ${addFour(Future(() => slow(100)))}")