Skip to content

Commit

Permalink
Merge branch 'main' of github.com:loonwerks/INSPECTA-models
Browse files Browse the repository at this point in the history
  • Loading branch information
John-Hatcliff committed Jan 22, 2025
2 parents 9780fcc + 6ba8320 commit c267eff
Show file tree
Hide file tree
Showing 559 changed files with 61,455 additions and 1,174 deletions.
15 changes: 8 additions & 7 deletions .github/workflows/ci-hamr.yml
Original file line number Diff line number Diff line change
Expand Up @@ -12,12 +12,12 @@ on:
- 'micro-examples/microkit/**'
- 'isolette/**'
schedule:
- cron: "0 2 * * 6" # every sunday at 2am
- cron: "0 2 * * 6" # every sunday at 2am

jobs:
container:
ci:
runs-on: ubuntu-latest
container:
image: jasonbelt/microkit_domain_scheduling:latest
container: jasonbelt/microkit_domain_scheduling:latest
name: HAMR-codegen
steps:
- name: Checkout
Expand Down Expand Up @@ -66,10 +66,11 @@ jobs:
export MICROKIT_SDK=$(find /home/microkit/microkit/release/ -type d -name microkit-sdk*)
export MICROKIT_BOARD=qemu_virt_aarch64
export DEMO_ROOT=$HOME/ku
export DEMO_ROOT=$HOME/provers
mv $(pwd)/INSPECTA-models $DEMO_ROOT/
rm -rf ${DEMO_ROOT}/Sireum # remove bootstrap version
export SIREUM_HOME=$(pwd)/Sireum
export PATH=$SIREUM_HOME/bin:$PATH
Expand All @@ -88,7 +89,7 @@ jobs:
sireum slang run $SIREUM_HOME/hamr/codegen/bin/build.cmd install-osate-gumbo
export OSATE_HOME=$SIREUM_HOME/bin/linux/osate
export ASP_BIN=/home/microkit/ku/asp-libs/bin
export ASP_BIN=/home/microkit/provers/asp-libs/bin
#env
$DEMO_ROOT/INSPECTA-models/.github/workflows/hamr-ci.cmd
$DEMO_ROOT/INSPECTA-models/.github/workflows/hamr/hamr-ci.cmd
98 changes: 0 additions & 98 deletions .github/workflows/hamr-ci.cmd

This file was deleted.

53 changes: 53 additions & 0 deletions .github/workflows/hamr/attestation-utils.cmd
Original file line number Diff line number Diff line change
@@ -0,0 +1,53 @@
::/*#! 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.up.up

val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin"
val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum")

val attestations = Os.Path.walk(rootDir, T, T, p => p.name == "attestation" && p.isDir && (p / "run-attestation.cmd").exists)

val canonical = rootDir / "isolette" / "attestation" / "run-attestation.cmd"

if (ops.ISZOps(Os.cliArgs).contains("update")) {
for (a <- attestations if (a != canonical.up)) {
a.removeAll()
a.mkdir()
canonical.copyOverTo(a / "run-attestation.cmd")
println(s"Wrote: ${a / "run-attestation.cmd"}")
}
} else if (ops.ISZOps(Os.cliArgs).contains("provision")) {
for (a <- attestations if (a != canonical.up)) {
proc"$sireum slang run ${a / "run-attestation.cmd"} provision".console.run()
}
} else if (ops.ISZOps(Os.cliArgs).contains("appraise")) {
for (a <- attestations) {
if ( (a.up / "aadl").exists) {
proc"$sireum slang run ${a / "run-attestation.cmd"} aadl".console.run()
}
if ( (a.up / "sysml").exists) {
proc"$sireum slang run ${a / "run-attestation.cmd"} sysml".console.run()
}
}
} else {
println("Usage: update | provision | appraise")
}

43 changes: 43 additions & 0 deletions .github/workflows/hamr/hamr-ci.cmd
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
::/*#! 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.up.up

val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin"
val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum")

val excludes: ops.ISZOps[Os.Path] = ops.ISZOps(ISZ(
rootDir / "micro-examples" / "case-transition-models"
))

var result: Z = 0
def findCIs(p: Os.Path): Unit = {
if (!excludes.contains(p)) {
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)
5 changes: 5 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -1,3 +1,8 @@
**/.metals/
**/.vscode/
**/.cache/
**/.idea/
**/.bloop/
**/out/
compile_commands.json
sysml-aadl-libraries
22 changes: 18 additions & 4 deletions isolette/.ci/ci.cmd
Original file line number Diff line number Diff line change
Expand Up @@ -45,16 +45,16 @@ if (result == 0) {
result = run("Cleaning", F, proc"$sireum slang run ${homeDir / "aadl" / "bin" / "clean.cmd"}")
}

if (result == 0) {
result = run("Running codegen from AADL model targeting JVM", F, proc"$sireum slang run ${homeDir / "aadl" / "bin" / "run-hamr.cmd"} JVM")
if (result == 0 && !(homeDir / "sysml" / "sysml-aadl-libraries").exists) {
result = run("Cloning https://github.com/santoslab/sysml-aadl-libraries.git", F, proc"git clone https://github.com/santoslab/sysml-aadl-libraries.git sysml-aadl-libraries".at(homeDir / "sysml"))
}

if (result == 0) {
result = run("Verifying via Logika", T, proc"$sireum slang run ${homeDir / "hamr" / "slang" / "bin" / "run-logika.cmd"}")
result = run("Running codegen from AADL model targeting JVM", F, proc"$sireum slang run ${homeDir / "aadl" / "bin" / "run-hamr.cmd"} JVM")
}

if (result == 0) {
result = run("Cloning https://github.com/santoslab/sysml-aadl-libraries.git", F, proc"git clone https://github.com/santoslab/sysml-aadl-libraries.git sysml/sysml-aadl-libraries".at(homeDir / "sysml"))
result = run("Verifying via Logika", T, proc"$sireum slang run ${homeDir / "hamr" / "slang" / "bin" / "run-logika.cmd"}")
}

if (result == 0) {
Expand All @@ -73,16 +73,30 @@ if (result == 0) {
result = run("Running codegen from AADL model targeting Microkit", F, proc"$sireum slang run ${homeDir / "aadl" / "bin" / "run-hamr.cmd"} Microkit")
}

if (result == 0) {
result = run("Running AADL attestation", F, proc"$sireum slang run ${homeDir / "attestation" / "run-attestation.cmd"} aadl")
}

if (result == 0 && Os.env("MICROKIT_SDK").nonEmpty) {
result = run("Building the image", F, proc"make".at(homeDir / "hamr" / "microkit"))
if ((homeDir / "hamr" / "microkit" / "build").exists) {
(homeDir / "hamr" / "microkit" / "build").removeAll()
}
}

if (result == 0) {
result = run("Running codegen from SysMLv2 model targeting Microkit", F, proc"$sireum slang run ${homeDir / "sysml" / "bin" / "run-hamr.cmd"} Microkit")
}

if (result == 0) {
result = run("Running SysMLv2 attestation", F, proc"$sireum slang run ${homeDir / "attestation" / "run-attestation.cmd"} sysml")
}

if (result == 0 && Os.env("MICROKIT_SDK").nonEmpty) {
result = run("Building the image", F, proc"make".at(homeDir / "hamr" / "microkit"))
if ((homeDir / "hamr" / "microkit" / "build").exists) {
(homeDir / "hamr" / "microkit" / "build").removeAll()
}
}

Os.exit(result)
Loading

0 comments on commit c267eff

Please sign in to comment.