Skip to content

Commit

Permalink
add hamr gen code
Browse files Browse the repository at this point in the history
  • Loading branch information
jasonbelt committed Aug 26, 2024
1 parent 48560dc commit 82daa6c
Show file tree
Hide file tree
Showing 41 changed files with 2,336 additions and 9 deletions.
3 changes: 3 additions & 0 deletions basic/test_data_port_periodic_three_domains_CASE/aadl/.system
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
system_impl=top.impl
system_impl_file=test_data_port_periodic_three_domains.aadl
projects=.
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
#include <camkes.h>
#include <stdio.h>
#include <sb_types.h>
#include <sb_producer_thread_i.h>
#include <sb_T1_i.h>

static int8_t _value;

Expand Down
Original file line number Diff line number Diff line change
@@ -1,20 +1,20 @@
#include <camkes.h>
#include <stdio.h>
#include <sb_types.h>
#include <sb_consumer_thread_i.h>
#include <sb_T2_i.h>

void init(const int64_t *in_arg) {
printf("[%s] init called\n", get_instance_name());
}

void compute(const int64_t * in_arg) {
int8_t _value;
int8_t value;

if (sb_read_port_read(&value)) {
printf("[%s] value {%d}\n", get_instance_name(), value);

if (sb_write_port_write( &_value )) {
printf("[%s] Sent %d\n", get_instance_name(), _value);
if (sb_write_port_write( &value )) {
printf("[%s] Sent %d\n", get_instance_name(), value);
} else {
printf("[%s] Unable to send\n", get_instance_name());
}
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,52 @@
::#! 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 hamrDir: Os.Path = Os.slashDir.up.up / "hamr"
val slangDir = hamrDir / "slang"
val cDir = hamrDir / "c"

val toKeep = ops.ISZOps(ISZ(
(slangDir / ".idea"),

(slangDir / "src" / "main" / "component"),
(slangDir / "src" / "test" / "bridge"),

(cDir / "ext-c/consumer_thread_i_consumer_consumer"),
(cDir / "ext-c/producer_thread_i_producer_producer"),
))


def rec(p: Os.Path, onlyDelAutoGen: B): Unit = {
if(p.isFile) {
if ((!toKeep.contains(p) && !onlyDelAutoGen) || ops.StringOps(p.read).contains("Do not edit")) {
p.remove()
println(s"Removed file: $p")
}
} else {
for (pp <- p.list) {
rec(pp, toKeep.contains(p) || onlyDelAutoGen)
}
if (p.list.isEmpty) {
p.removeAll()
println(s"Removed empty directory: $p")
}
}
}
rec(hamrDir, F)
Original file line number Diff line number Diff line change
@@ -0,0 +1,91 @@
::/*#! 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 aadlDir = Os.slashDir.up

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

val osate: Os.Path = Os.env("OSATE_HOME") match {
case Some(s) => Os.path(s) / (
if (Os.isWin) "osate.exe"
else if (Os.isLinux || Os.kind == Os.Kind.LinuxArm) "osate"
else "Contents/MacOS/osate")
case _ if (Os.isWin) => sireumBin / "win" / "fmide" / "fmide.exe"
case _ if (Os.isMac) => sireumBin / "mac" / "fmide.app" / "Contents" / "MacOS" / "osate"
case _ if (Os.isLinux) => sireumBin / "linux" / "fmide" / "fmide"
case _ =>
println("Unsupported operating system")
Os.exit(1)
halt("")
}

if (!osate.exists) {
eprintln("Please install FMIDE (e.g. '$SIREUM_HOME/bin/install/fmide.cmd') or OSATE (e.g. 'sireum hamr phantom -u')")
Os.exit(1)
halt("")
}

val osireum = ISZ(osate.string, "-nosplash", "--launcher.suppressErrors", "-data", "@user.home/.sireum", "-application", "org.sireum.aadl.osate.cli")

if(Os.cliArgs.size > 1) {
eprintln("Only expecting a single argument")
Os.exit(1)
}

val slangOutputDir = aadlDir.up / "hamr" / "slang"

val packageName = "base"

assert (!slangOutputDir.exists || (slangOutputDir / "src" / "main" / "component" / packageName).exists, s"Slang output dir exists but the package name is not $packageName")

val platform: String =
if(Os.cliArgs.nonEmpty) Os.cliArgs(0)
else "JVM"

val codegenArgs = ISZ[String]("hamr", "codegen",
"--platform", platform,
"--package-name", packageName,
"--output-dir", (aadlDir.up / "hamr" / "slang").string,
"--output-c-dir", (aadlDir.up / "hamr" / "c").string,
"--run-transpiler",
"--bit-width", "32",
"--max-string-size", "256",
"--max-array-size", "1",
"--exclude-component-impl",
"--verbose",
//"--no-proyek-ive",
"--camkes-output-dir", (aadlDir.up / "hamr" / s"camkes-${platform.string}").string,
"--experimental-options", "GENERATE_DOT_GRAPHS",
"--aadl-root-dir", aadlDir.string,
(aadlDir / ".system").string)

val results = Os.proc(osireum ++ codegenArgs).console.run()

// Running under windows results in 23 which is an indication
// a platform restart was requested. Codegen completes
// successfully and the cli app returns 0 so
// not sure why this is being issued.
if(results.exitCode == 0 || results.exitCode == 23) {
Os.exit(0)
} else {
println(results.err)
Os.exit(results.exitCode)
}
Original file line number Diff line number Diff line change
Expand Up @@ -27,12 +27,12 @@
//
const dschedule_t ksDomSchedule[] = { // (1 tick == 2ms)
{ .domain = 0, .length = 100 }, // all other seL4 threads, init, 200ms
{ .domain = 1, .length = 5 }, // T1 10ms
{ .domain = 2, .length = 5 }, // T1 10ms
{ .domain = 0, .length = 95 }, // domain0 190ms
{ .domain = 2, .length = 5 }, // T2 10ms
{ .domain = 3, .length = 5 }, // T2 10ms
{ .domain = 0, .length = 95 }, // domain0 190ms
{ .domain = 4, .length = 105 }, // T3 210ms
{ .domain = 0, .length = 95 }, // domain0 190ms
{ .domain = 3, .length = 5 }, // T3 10ms
{ .domain = 0, .length = 195 }, // domain0 390ms
// +
// -----------------------------------
// 1000ms
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
# Do not edit this file as it will be overwritten if HAMR codegen is rerun

cmake_minimum_required(VERSION 3.8.2)

project (top_impl_Instance C)

add_definitions(-DCAMKES)

include(${CMAKE_CURRENT_LIST_DIR}/CMake_CAmkES_VM_Options.cmake)

if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "(C|c?)lang")
add_compile_options("$<$<CONFIG:Release>:-Oz>")
elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU")
add_compile_options(-fstack-usage)
add_compile_options("$<$<CONFIG:Release>:-Os>")
endif()

add_subdirectory(${CMAKE_CURRENT_LIST_DIR}/types)

add_subdirectory(${CMAKE_CURRENT_LIST_DIR}/components/VM)

DeclareCAmkESComponent(T1_i_p1_t1
SOURCES components/T1_i_p1_t1//src/T1.c components/T1_i_p1_t1/src/sb_T1_i.c types/src/sp_int8_t.c
INCLUDES components/T1_i_p1_t1/includes/ types/includes types/includes
)

DeclareCAmkESComponent(T2_i_p2_t2
SOURCES components/T2_i_p2_t2//src/T2.c components/T2_i_p2_t2/src/sb_T2_i.c types/src/sp_int8_t.c types/src/sp_int8_t.c
INCLUDES components/T2_i_p2_t2/includes/ types/includes types/includes types/includes
)

DeclareCAmkESComponent(Pacer
SOURCES components/Pacer/src/Pacer.c
LIBS SB_Type_Library
)

DeclareCAmkESRootserver(top_impl_Instance.camkes)
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
option(BUILD_CROSSVM
"Checkout and configure linux to build crossvm module instead of using pre-configured rootfs"
OFF)

if("$ENV{BUILD_CROSSVM}" STREQUAL "ON")
set(BUILD_CROSSVM ON)
endif()
Loading

0 comments on commit 82daa6c

Please sign in to comment.