add hamr ci

.github/workflows/ci-hamr.yml

@@ -0,0 +1,93 @@
+name: HAMR-codegen
+
+on: 
+  push:
+    paths:
+      - 'micro-examples/microkit/**'
+  schedule:
+    - cron: "0 2 * * 6" # every sunday at 2am      
+jobs:
+  container:
+    runs-on: ubuntu-latest
+    container:
+      image: jasonbelt/microkit_domain_scheduling
+    name: HAMR-codegen
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+        with:
+          path: inspecta
+          submodules: recursive
+      - name: Checkout
+        uses: actions/checkout@v4
+        with:
+          path: kekinian
+          repository: sireum/kekinian
+          submodules: recursive
+      - name: Cache Java
+        id: cache-java
+        uses: actions/cache@v4
+        with:
+          path: kekinian/bin/linux/java
+          key: ${{ runner.os }}-${{ hashFiles('kekinian/versions.properties') }}-java
+      - name: Cache Scala
+        id: cache-scala
+        uses: actions/cache@v4
+        with:
+          path: kekinian/bin/scala
+          key: ${{ runner.os }}-${{ hashFiles('kekinian/versions.properties') }}-scala
+      - name: Cache Coursier
+        id: cache-coursier
+        uses: actions/cache@v4
+        with:
+          path: kekinian/cache/coursier
+          key: ${{ runner.os }}-${{ hashFiles('kekinian/versions.properties') }}-coursier
+      - name: Cache OSATE
+        id: cache-osate
+        uses: actions/cache@v4
+        with:
+          path: kekinian/hamr/codegen/bin/linux/osate
+          key: ${{ runner.os }}-${{ hashFiles('kekinian/hamr/codegen/jvm/src/main/resources/phantom_versions.properties') }}-osate
+      - name: Build
+        run: |
+
+          export aptInstall="apt-get install -f -y --no-install-recommends"
+          export DEBIAN_FRONTEND=noninteractive
+          apt-get update
+          ${aptInstall} p7zip-full
+          
+          # Installing emacs installs some package(s) that resolve an issue where
+          # the OSATE gumbo parser fails to initialize when used in the docker container.
+          #${aptInstall} emacs
+
+          # github sets HOME to /github/home but some tools (Sireum's Os.home, Haskell) use
+          # the containers /root instead leading to inconsistent installs. Setting HOME
+          # to be root resolves the issue
+          # https://github.com/actions/runner/issues/1474#issuecomment-965805123
+          export HOME=/root
+
+          export GITHUB_DIR=$(pwd)
+
+          mv ./inspecta $HOME/
+          mv ./kekinian $HOME/
+
+          cd $HOME/
+
+          export SIREUM_HOME=$HOME/kekinian
+          export PATH=$SIREUM_HOME/bin:$PATH
+
+          $SIREUM_HOME/bin/build.cmd
+          rm -rf $SIREUM_HOME/out
+          
+          sireum
+
+          $SIREUM_HOME/hamr/codegen/bin/build.cmd install-osate-gumbo
+          export OSATE_HOME=$SIREUM_HOME/hamr/codegen/bin/linux/osate
+
+          export MICROKIT_BOARD=qemu_virt_aarch64
+          export MICROKIT_SDK=$HOME/microkit/release/microkit-sdk-1.4.1-dev.14+cf88629
+
+          $HOME/inspecta/micro-examples/microkit/.ci/test.cmd
+
+          # move kekinian back in order for caching to work
+          mv $HOME/kekinian $GITHUB_DIR/

micro-examples/microkit/.ci/test.cmd

@@ -0,0 +1,37 @@
+::/*#! 2> /dev/null                                 #
+@ 2>/dev/null # 2>nul & echo off & goto BOF         #
+if [ -z ${SIREUM_HOME} ]; then                      #
+  echo "Please set SIREUM_HOME env var"             #
+  exit -1                                           #
+fi                                                  #
+exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@"  #
+:BOF
+setlocal
+if not defined SIREUM_HOME (
+  echo Please set SIREUM_HOME env var
+  exit /B -1
+)
+%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %*
+exit /B %errorlevel%
+::!#*/
+// #Sireum
+
+import org.sireum._
+
+val rootDir = Os.slashDir.up
+
+val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin"
+val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum")
+
+var result: Z = 0
+def findCIs(p: Os.Path): Unit = {
+  if(p.isFile && p.name == "ci.cmd") {
+    val r = proc"$sireum slang run $p".console.echo.run()
+    result = result + r.exitCode
+  } else if(p.isDir) {
+    p.list.foreach((m: Os.Path) => findCIs(m))
+  }
+}
+findCIs(rootDir)
+
+Os.exit(result)

micro-examples/microkit/aadl_port_types/data/.ci/ci.cmd

@@ -0,0 +1,56 @@
+::/*#! 2> /dev/null                                 #
+@ 2>/dev/null # 2>nul & echo off & goto BOF         #
+if [ -z ${SIREUM_HOME} ]; then                      #
+  echo "Please set SIREUM_HOME env var"             #
+  exit -1                                           #
+fi                                                  #
+exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@"  #
+:BOF
+setlocal
+if not defined SIREUM_HOME (
+  echo Please set SIREUM_HOME env var
+  exit /B -1
+)
+%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %*
+exit /B %errorlevel%
+::!#*/
+// #Sireum
+
+import org.sireum._
+
+val homeDir = Os.slashDir.up
+
+val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin"
+val sireum = sireumBin / (if (Os.isWin) "sireum.bat" else "sireum")
+var result: Z = 0
+
+def run(title: String, verbose: B, proc: OsProto.Proc): Z = {
+  println(s"$title ...")
+  val r = (if (verbose) proc.console.echo else proc).run()
+  if (!r.ok) {
+    println(s"$title failed!")
+    cprintln(F, r.out)
+    cprintln(T, r.err)
+  }
+  return r.exitCode
+}
+
+println(
+  st"""**************************************************************************
+      |*                            DATA PORTS                                  *
+      |**************************************************************************""".render
+)
+
+if (result == 0) {
+  //result = run("Cleaning", F, proc"$sireum slang run ${homeDir / "bin" / "clean.cmd"}")
+}
+
+if (result == 0) {
+  result = run("Running codegen targeting Microkit", F, proc"$sireum slang run ${homeDir / "aadl" / "bin" / "run-hamr.cmd"} Microkit")
+}
+
+if (result == 0 && Os.env("MICROKIT_SDK").nonEmpty) {
+  result = run("Building the image", F, proc"make".at(homeDir / "hamr" / "microkit"))
+}
+
+Os.exit(result)

micro-examples/microkit/aadl_port_types/event/.ci/ci.cmd

@@ -0,0 +1,56 @@
+::/*#! 2> /dev/null                                 #
+@ 2>/dev/null # 2>nul & echo off & goto BOF         #
+if [ -z ${SIREUM_HOME} ]; then                      #
+  echo "Please set SIREUM_HOME env var"             #
+  exit -1                                           #
+fi                                                  #
+exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@"  #
+:BOF
+setlocal
+if not defined SIREUM_HOME (
+  echo Please set SIREUM_HOME env var
+  exit /B -1
+)
+%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %*
+exit /B %errorlevel%
+::!#*/
+// #Sireum
+
+import org.sireum._
+
+val homeDir = Os.slashDir.up
+
+val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin"
+val sireum = sireumBin / (if (Os.isWin) "sireum.bat" else "sireum")
+var result: Z = 0
+
+def run(title: String, verbose: B, proc: OsProto.Proc): Z = {
+  println(s"$title ...")
+  val r = (if (verbose) proc.console.echo else proc).run()
+  if (!r.ok) {
+    println(s"$title failed!")
+    cprintln(F, r.out)
+    cprintln(T, r.err)
+  }
+  return r.exitCode
+}
+
+println(
+  st"""**************************************************************************
+      |*                            EVENT PORTS                                 *
+      |**************************************************************************""".render
+)
+
+if (result == 0) {
+  //result = run("Cleaning", F, proc"$sireum slang run ${homeDir / "bin" / "clean.cmd"}")
+}
+
+if (result == 0) {
+  result = run("Running codegen targeting Microkit", F, proc"$sireum slang run ${homeDir / "aadl" / "bin" / "run-hamr.cmd"} Microkit")
+}
+
+if (result == 0 && Os.env("MICROKIT_SDK").nonEmpty) {
+  result = run("Building the image", F, proc"make".at(homeDir / "hamr" / "microkit"))
+}
+
+Os.exit(result)

micro-examples/microkit/aadl_port_types/event_data/.ci/ci.cmd

@@ -0,0 +1,56 @@
+::/*#! 2> /dev/null                                 #
+@ 2>/dev/null # 2>nul & echo off & goto BOF         #
+if [ -z ${SIREUM_HOME} ]; then                      #
+  echo "Please set SIREUM_HOME env var"             #
+  exit -1                                           #
+fi                                                  #
+exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@"  #
+:BOF
+setlocal
+if not defined SIREUM_HOME (
+  echo Please set SIREUM_HOME env var
+  exit /B -1
+)
+%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %*
+exit /B %errorlevel%
+::!#*/
+// #Sireum
+
+import org.sireum._
+
+val homeDir = Os.slashDir.up
+
+val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin"
+val sireum = sireumBin / (if (Os.isWin) "sireum.bat" else "sireum")
+var result: Z = 0
+
+def run(title: String, verbose: B, proc: OsProto.Proc): Z = {
+  println(s"$title ...")
+  val r = (if (verbose) proc.console.echo else proc).run()
+  if (!r.ok) {
+    println(s"$title failed!")
+    cprintln(F, r.out)
+    cprintln(T, r.err)
+  }
+  return r.exitCode
+}
+
+println(
+  st"""**************************************************************************
+      |*                           EVENT DATA PORTS                             *
+      |**************************************************************************""".render
+)
+
+if (result == 0) {
+  //result = run("Cleaning", F, proc"$sireum slang run ${homeDir / "bin" / "clean.cmd"}")
+}
+
+if (result == 0) {
+  result = run("Running codegen targeting Microkit", F, proc"$sireum slang run ${homeDir / "aadl" / "bin" / "run-hamr.cmd"} Microkit")
+}
+
+if (result == 0 && Os.env("MICROKIT_SDK").nonEmpty) {
+  result = run("Building the image", F, proc"make".at(homeDir / "hamr" / "microkit"))
+}
+
+Os.exit(result)

micro-examples/microkit/port_queues/event_data/.ci/ci.cmd

@@ -0,0 +1,56 @@
+::/*#! 2> /dev/null                                 #
+@ 2>/dev/null # 2>nul & echo off & goto BOF         #
+if [ -z ${SIREUM_HOME} ]; then                      #
+  echo "Please set SIREUM_HOME env var"             #
+  exit -1                                           #
+fi                                                  #
+exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@"  #
+:BOF
+setlocal
+if not defined SIREUM_HOME (
+  echo Please set SIREUM_HOME env var
+  exit /B -1
+)
+%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %*
+exit /B %errorlevel%
+::!#*/
+// #Sireum
+
+import org.sireum._
+
+val homeDir = Os.slashDir.up
+
+val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin"
+val sireum = sireumBin / (if (Os.isWin) "sireum.bat" else "sireum")
+var result: Z = 0
+
+def run(title: String, verbose: B, proc: OsProto.Proc): Z = {
+  println(s"$title ...")
+  val r = (if (verbose) proc.console.echo else proc).run()
+  if (!r.ok) {
+    println(s"$title failed!")
+    cprintln(F, r.out)
+    cprintln(T, r.err)
+  }
+  return r.exitCode
+}
+
+println(
+  st"""**************************************************************************
+      |*                            PORT QUEUES                                 *
+      |**************************************************************************""".render
+)
+
+if (result == 0) {
+  //result = run("Cleaning", F, proc"$sireum slang run ${homeDir / "bin" / "clean.cmd"}")
+}
+
+if (result == 0) {
+  result = run("Running codegen targeting Microkit", F, proc"$sireum slang run ${homeDir / "aadl" / "bin" / "run-hamr.cmd"} Microkit")
+}
+
+if (result == 0 && Os.env("MICROKIT_SDK").nonEmpty) {
+  result = run("Building the image", F, proc"make".at(homeDir / "hamr" / "microkit"))
+}
+
+Os.exit(result)