diff --git a/.github/workflows/bolts-CI.yml b/.github/workflows/bolts-CI.yml index faa2e7ed..e3ba58b4 100644 --- a/.github/workflows/bolts-CI.yml +++ b/.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 diff --git a/data-structures/uarray/UArrayExample.scala b/data-structures/uarray/UArrayExample.scala index 27ea4322..82709a41 100644 --- a/data-structures/uarray/UArrayExample.scala +++ b/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 diff --git a/run-one-test.sh b/run-one-test.sh index 7445fa7d..12001f6a 100755 --- a/run-one-test.sh +++ b/run-one-test.sh @@ -23,6 +23,8 @@ 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" @@ -30,9 +32,9 @@ function run_tests { 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 - @@ -40,9 +42,9 @@ function run_tests { 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 diff --git a/tctests.txt b/tctests.txt index 0ecd4205..62668e31 100644 --- a/tctests.txt +++ b/tctests.txt @@ -32,3 +32,4 @@ tutorials/simple-transform tutorials/fmcad2021/alt-diffs tutorials/fmcad2021/binary-search tutorials/fmcad2021/find-index +tutorials/explicit-memory diff --git a/tutorials/explicit-memory/ExplicitMemory.scala b/tutorials/explicit-memory/ExplicitMemory.scala new file mode 100644 index 00000000..f50ea235 --- /dev/null +++ b/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}") diff --git a/tutorials/futures/PossibleFutures.scala b/tutorials/futures/PossibleFutures.scala index ca40bb18..1b60748d 100644 --- a/tutorials/futures/PossibleFutures.scala +++ b/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)))}") \ No newline at end of file + println(f"The result is: ${addFour(Future(() => slow(100)))}")