Skip to content

Commit

Permalink
Merge branch 'master' into clint
Browse files Browse the repository at this point in the history
  • Loading branch information
@ClintMcKenzieJr
ClintMcKenzieJr committed Jan 6, 2025
2 parents 61db9cc + 2398299 commit 3810272
Show file tree
Hide file tree
Showing 10 changed files with 155 additions and 108 deletions.
34 changes: 28 additions & 6 deletions bin/build.cmd
View file
Original file line number Diff line number Diff line change
Expand Up @@ -161,10 +161,31 @@ def regenTransformers(): Unit = {
"-m", "immutable,mutable") ++ asts).at(symbolPackagePath).console.runCheck()
}

def symLinkSireumJar(): Unit = {
val sireumjar = home.up.up / "bin" / "sireum.jar"
val bootstrapSireumjar = homeBin / "sireum.jar"
if (sireumjar.exists) {
if (!bootstrapSireumjar.isSymLink) {
bootstrapSireumjar.remove()
bootstrapSireumjar.mklink(sireumjar)
println(
st"""Replaced bootstrapping sireum.jar with $sireumjar.
|Please rerun the last task.""".render)
}
} else {
println(
st"""This task requires build.cmd be run using $sireumjar
|rather than the bootstrapping version. Please clone the kekinian repo and try again.""".render)
Os.exit(1)
}
}

def regenClis(): Unit = {
symLinkSireumJar()
val utilDir = home / "shared" / "src" / "main" / "scala" / "org" / "sireum" / "hamr" / "codegen" / "common" / "util"
// NOTE: cliJson.sc emits what's in $SIREUM_HOME/bin/sireum.jar's version of
// hamr's cli so regen that first, rebuild sireum.jar, then call this method

proc"${sireum} tools cligen -p org.sireum.hamr.codegen.common.util -n HamrCli -o ${utilDir.value} ${(utilDir / "cliJson.sc")}".console.runCheck()


Expand All @@ -179,8 +200,11 @@ def regenClis(): Unit = {
def addOptions(opts: ISZ[org.sireum.cli.CliOpt.Opt], optGroup: String): Unit = {
for (o <- opts) {
val longKey = s"--${o.longKey}"
longs = longs :+ st"""val $optGroup${o.name}: String = "$longKey""""
allLongs = allLongs :+ st"$optGroup${o.name}"
@strictpure def sanitize(s: String): ST =
st"${ops.StringOps(s).replaceAllLiterally("/", "_")}"
val id = sanitize(s"$optGroup${o.name}")
longs = longs :+ st"""val $id: String = "$longKey""""
allLongs = allLongs :+ id
o.tpe match {
case f: Type.Flag =>
toStrings = toStrings :+
Expand Down Expand Up @@ -227,8 +251,8 @@ def regenClis(): Unit = {
|}"""
}
if (o.shortKey.nonEmpty) {
shorts = shorts :+ st"""val $optGroup${o.name}: String = "-${o.shortKey.get}""""
allShorts = allShorts :+ st"$optGroup${o.name}"
shorts = shorts :+ st"""val $id: String = "-${o.shortKey.get}""""
allShorts = allShorts :+ id
}
}
}
Expand Down Expand Up @@ -325,8 +349,6 @@ def regenClis(): Unit = {
println(s"Modified: $hamrCli")
}



// Ignore the Tipe error "'hamr' is not a member of package 'org.sireum'"
process(
tool = org.sireum.hamr.codegen.HamrCodegenCli.codeGenTool,
Expand Down
16 changes: 16 additions & 0 deletions bin/formBuilder.cmd
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,22 @@ val sireum: Os.Path = homeBin / (if (Os.isWin) "sireum.bat" else "sireum")
val sireumJar: Os.Path = homeBin / "sireum.jar"
val appDir: Os.Path = homeBin / (if (Os.isMac) "mac" else if (Os.isWin) "win" else "linux")

if (!sireumJar.isSymLink) {
val sireumjar = home.up.up / "bin" / "sireum.jar"
if (sireumjar.exists) {
(homeBin / "sireum.jar").remove()
(homeBin / "sireum.jar").mklink(sireumjar)
println(
st"""Replaced bootstrapping sireum.jar with $sireumjar.
|Please rerun the last task.""".render)
} else {
println(
st"""This task requires $sireumjar
|rather than the bootstrapping version. Please clone the kekinian repo and try again.""".render)
Os.exit(1)
}
}

val ignoreKeys: Set[String] = Set(ISZ(
"devicesAsThreads", "line", "verbose", "parseableMessages", "genSbtMill", "noProyekIve", "noEmbedArt",
"runTranspiler", "system", "experimentalOptions", "sourcepath", "workspaceRootDir"))
Expand Down
116 changes: 63 additions & 53 deletions jvm/src/main/scala/org/sireum/hamr/codegen/CodeGen.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,9 @@ object CodeGen {
return CodeGenResults.empty
}

val systemRootDirectory: Os.Path = getSystemRoot(model, options.workspaceRootDir)
var modOptions = options

val systemRootDirectory: Os.Path = getSystemRoot(model, modOptions.workspaceRootDir)

def getPath(path: String): Os.Path = {
val p = Os.path(path)
Expand All @@ -47,26 +49,33 @@ object CodeGen {
else systemRootDirectory / path) // make the user's request relative to the system's root directory
}

val outputDir: Path = getPath(options.outputDir.getOrElse("hamr"))
val outputDir: Path = getPath(modOptions.outputDir.getOrElse("hamr"))

val slangOutputDir: Path = getPath(options.slangOutputDir.getOrElse((outputDir / "slang").value))
val slangOutputDir: Path = getPath(modOptions.slangOutputDir.getOrElse((outputDir / "slang").value))

val output_shared_C_Directory: Path = getPath(options.slangOutputCDir.getOrElse((outputDir / "c").value))
val output_shared_C_Directory: Path = getPath(modOptions.slangOutputCDir.getOrElse((outputDir / "c").value))

val camkesOutputDir: Path = getPath(options.camkesOutputDir.getOrElse((outputDir / "camkes").value))
val sel4Type: String = if (modOptions.platform == CodegenHamrPlatform.Microkit) "microkit" else "camkes"
val sel4OutputDir: Path = getPath(modOptions.sel4OutputDir.getOrElse((outputDir / sel4Type).value))

val output_platform_C_Directory: Path =
if (options.platform == CodegenHamrPlatform.SeL4) camkesOutputDir / DirectoryUtil.DIR_SLANG_LIBRARIES
if (modOptions.platform == CodegenHamrPlatform.SeL4) sel4OutputDir / DirectoryUtil.DIR_SLANG_LIBRARIES
else output_shared_C_Directory

val packageName: String = if (options.packageName.nonEmpty) {
cleanupPackageName(options.packageName.get)
val packageName: String = if (modOptions.packageName.nonEmpty) {
cleanupPackageName(modOptions.packageName.get)
} else {
cleanupPackageName("base" )
}

modOptions = modOptions(
packageName = Some(packageName),
outputDir = Some(outputDir.canon.value),
slangOutputDir = Some(slangOutputDir.canon.value),
sel4OutputDir = Some(sel4OutputDir.canon.value))

val (runArsit, runACT, runMicrokit, runRos2, isTranspilerProject, isSlangProject): (B, B, B, B, B, B) =
options.platform match {
modOptions.platform match {
case CodegenHamrPlatform.JVM => (T, F, F, F, F, T)

case CodegenHamrPlatform.Linux => (T, F, F, F, T, T)
Expand All @@ -85,9 +94,9 @@ object CodeGen {

var reporterIndex = z"0"

if (options.runtimeMonitoring && isTranspilerProject) {
if (modOptions.runtimeMonitoring && isTranspilerProject) {
reporter.error(None(), toolName, "Runtime monitoring support for transpiled projects has not been added yet. Disable runtime-monitoring before transpiling")
reporterIndex = printMessages(reporter.messages, options.verbose, reporterIndex, ISZ())
reporterIndex = printMessages(reporter.messages, modOptions.verbose, reporterIndex, ISZ())
return CodeGenResults.empty
}

Expand All @@ -96,37 +105,38 @@ object CodeGen {

var wroteOutArsitResources: B = F

val result: Option[ModelElements] = ModelUtil.resolve(model, model.components(0).identifier.pos, packageName, options, reporter)
reporterIndex = printMessages(reporter.messages, options.verbose, reporterIndex, ISZ())
val result: Option[ModelElements] = ModelUtil.resolve(model, model.components(0).identifier.pos, packageName, modOptions, reporter)
reporterIndex = printMessages(reporter.messages, modOptions.verbose, reporterIndex, ISZ())
if (result.isEmpty) {
return CodeGenResults.empty
}

val (rmodel, aadlTypes, symbolTable): (Aadl, AadlTypes, SymbolTable) = (result.get.model, result.get.types, result.get.symbolTable)

if (options.runtimeMonitoring && symbolTable.getThreads().isEmpty) {
if (modOptions.runtimeMonitoring && symbolTable.getThreads().isEmpty) {
reporter.error(None(), toolName, "Model must contain threads in order to enable runtime monitoring")
return CodeGenResults.empty
}

if (~reporter.hasError && runRos2) {
val results = Ros2Codegen().run(rmodel, options, aadlTypes, symbolTable, plugins, reporter)
val results = Ros2Codegen().run(rmodel, modOptions, aadlTypes, symbolTable, plugins, reporter)
if (!reporter.hasError) {
writeOutResources(results.fileResources, reporter)
}
if (!options.parseableMessages) {
reporterIndex = printMessages(reporter.messages, options.verbose, reporterIndex, ISZ())
if (!modOptions.parseableMessages) {
reporterIndex = printMessages(reporter.messages, modOptions.verbose, reporterIndex, ISZ())
}
return CodeGenResults(resources = results.fileResources, auxResources = ISZ())
}

if (!reporter.hasError && runMicrokit) {
val results = MicrokitCodegen().run(rmodel, options, aadlTypes, symbolTable, plugins, reporter)
reporter.info(None(), toolName, "Generating Microkit artifacts...")
val results = MicrokitCodegen().run(rmodel, modOptions, aadlTypes, symbolTable, plugins, reporter)
if (!reporter.hasError) {
writeOutResources(results.resources, reporter)
}
if (!options.parseableMessages) {
reporterIndex = printMessages(reporter.messages, options.verbose, reporterIndex, ISZ())
if (!modOptions.parseableMessages) {
reporterIndex = printMessages(reporter.messages, modOptions.verbose, reporterIndex, ISZ())
}
return results
}
Expand All @@ -135,49 +145,49 @@ object CodeGen {

val genBlessEntryPoints = false
val ipc = arsit.util.IpcMechanism.SharedMemory
val platform = arsit.util.ArsitPlatform.byName(options.platform.name).get
val platform = arsit.util.ArsitPlatform.byName(modOptions.platform.name).get
val fileSep = StringOps(org.sireum.Os.fileSep).first

val opt = arsit.util.ArsitOptions(
slangOutputDir = slangOutputDir,
packageName = packageName,
noEmbedArt = options.noEmbedArt,
noEmbedArt = modOptions.noEmbedArt,
bless = genBlessEntryPoints,
verbose = options.verbose,
runtimeMonitoring = options.runtimeMonitoring,
devicesAsThreads = options.devicesAsThreads,
genSbtMill = options.genSbtMill,
verbose = modOptions.verbose,
runtimeMonitoring = modOptions.runtimeMonitoring,
devicesAsThreads = modOptions.devicesAsThreads,
genSbtMill = modOptions.genSbtMill,
ipc = ipc,
auxCodeDirs = options.slangAuxCodeDirs,
auxCodeDirs = modOptions.slangAuxCodeDirs,
outputSharedCDir = output_shared_C_Directory,
outputPlatformCDir = output_platform_C_Directory,
excludeImpl = options.excludeComponentImpl,
excludeImpl = modOptions.excludeComponentImpl,
platform = platform,
bitWidth = options.bitWidth,
maxStringSize = options.maxStringSize,
maxArraySize = options.maxArraySize,
bitWidth = modOptions.bitWidth,
maxStringSize = modOptions.maxStringSize,
maxArraySize = modOptions.maxArraySize,
pathSeparator = fileSep,
experimentalOptions = options.experimentalOptions,
experimentalOptions = modOptions.experimentalOptions,

runSlangCheck = !ExperimentalOptions.disableSlangCheck(options.experimentalOptions)
runSlangCheck = !ExperimentalOptions.disableSlangCheck(modOptions.experimentalOptions)
)

reporter.info(None(), toolName, "Generating Slang artifacts...")
reporterIndex = printMessages(reporter.messages, options.verbose, reporterIndex, ISZ())
reporterIndex = printMessages(reporter.messages, modOptions.verbose, reporterIndex, ISZ())

val results = arsit.Arsit.run(rmodel, opt, aadlTypes, symbolTable, plugins, reporter)

arsitResources = arsitResources ++ results.resources
arsitAuxResources = arsitAuxResources ++ results.auxResources

reporterIndex = printMessages(reporter.messages, options.verbose, reporterIndex, ISZ(ARSIT_INSTRUCTIONS_MESSAGE_KIND))
reporterIndex = printMessages(reporter.messages, modOptions.verbose, reporterIndex, ISZ(ARSIT_INSTRUCTIONS_MESSAGE_KIND))

arsitResources = removeDuplicates(arsitResources, reporter)

val sergenConfigs = Resource.projectSergenConfigs(arsitAuxResources)
if (!reporter.hasError && isSlangProject && sergenConfigs.nonEmpty &&
!ExperimentalOptions.disableSergen(options.experimentalOptions) &&
!options.noEmbedArt // only run sergen and slangcheck when art is embedded
!ExperimentalOptions.disableSergen(modOptions.experimentalOptions) &&
!modOptions.noEmbedArt // only run sergen and slangcheck when art is embedded
) {
// doesn't matter what 'o.writeOutResources' is, sergen/slangcheck needs the
// resources to be written out
Expand All @@ -188,7 +198,7 @@ object CodeGen {

if (!reporter.hasError) {
reporter.info(None(), toolName, "Generating serializer/deserializers for data types via sergen ...")
reporterIndex = printMessages(reporter.messages, options.verbose, reporterIndex, ISZ())
reporterIndex = printMessages(reporter.messages, modOptions.verbose, reporterIndex, ISZ())

for (sc <- sergenConfigs if !reporter.hasError) {
sergenCallback(sc, reporter)
Expand All @@ -198,8 +208,8 @@ object CodeGen {

val slangCheckConfigs = Resource.projectSlangCheckConfigs(arsitAuxResources)
if (!reporter.hasError && isSlangProject && slangCheckConfigs.nonEmpty &&
!ExperimentalOptions.disableSlangCheck(options.experimentalOptions) &&
!options.noEmbedArt // only run sergen and slangcheck when art is embedded
!ExperimentalOptions.disableSlangCheck(modOptions.experimentalOptions) &&
!modOptions.noEmbedArt // only run sergen and slangcheck when art is embedded
) {
// doesn't matter what 'o.writeOutResources' is, sergen/slangcheck needs the
// resources to be written out
Expand All @@ -210,15 +220,15 @@ object CodeGen {

if (!reporter.hasError) {
reporter.info(None(), toolName, "Generating SlangCheck artifacts ...")
reporterIndex = printMessages(reporter.messages, options.verbose, reporterIndex, ISZ())
reporterIndex = printMessages(reporter.messages, modOptions.verbose, reporterIndex, ISZ())

for (sc <- slangCheckConfigs if !reporter.hasError) {
slangCheckCallback(sc, reporter)
}
}
}

if (!reporter.hasError && !options.noProyekIve && isSlangProject) {
if (!reporter.hasError && !modOptions.noProyekIve && isSlangProject) {
// doesn't matter what 'o.writeOutResources' is, proyek ive needs the
// resources to be written out
if (!wroteOutArsitResources) {
Expand Down Expand Up @@ -249,15 +259,15 @@ object CodeGen {
)

reporter.info(None(), toolName, "Generating IVE and Scala Metals project via Proyek ...")
reporterIndex = printMessages(reporter.messages, options.verbose, reporterIndex, ISZ())
reporterIndex = printMessages(reporter.messages, modOptions.verbose, reporterIndex, ISZ())

if (proyekIveCallback(proyekConfig) != 0) {
reporter.error(None(), toolName, "Proyek did not complete successfully")
}
}
}

if (!reporter.hasError && options.runTranspiler && isTranspilerProject) {
if (!reporter.hasError && modOptions.runTranspiler && isTranspilerProject) {

// doesn't matter what 'o.writeOutResources' is, transpiler needs the
// resources to be written out
Expand All @@ -268,7 +278,7 @@ object CodeGen {

if (!reporter.hasError) {
reporter.info(None(), toolName, "Transpiling project ...")
reporterIndex = printMessages(reporter.messages, options.verbose, reporterIndex, ISZ())
reporterIndex = printMessages(reporter.messages, modOptions.verbose, reporterIndex, ISZ())

for (transpilerConfig <- Resource.projectTranspilerConfigs(results.auxResources) if !reporter.hasError) {
// CTranspiler prints all the messages in the passed in reporter so
Expand All @@ -287,22 +297,22 @@ object CodeGen {

if (!reporter.hasError && runACT) {

val platform = org.sireum.hamr.codegen.act.util.ActPlatform.byName(options.platform.name).get
val platform = org.sireum.hamr.codegen.act.util.ActPlatform.byName(modOptions.platform.name).get
reporter.info(None(), toolName, "Generating CAmkES artifacts...")

val actOptions = org.sireum.hamr.codegen.act.util.ActOptions(
camkesOutputDir = camkesOutputDir.value,
auxFiles = getAuxFiles(options.camkesAuxCodeDirs, F, reporter),
workspaceRootDir = options.workspaceRootDir,
sel4OutputDir = sel4OutputDir.value,
auxFiles = getAuxFiles(modOptions.sel4AuxCodeDirs, F, reporter),
workspaceRootDir = modOptions.workspaceRootDir,
platform = platform,
hamrBasePackageName = Some(packageName),
experimentalOptions = options.experimentalOptions
experimentalOptions = modOptions.experimentalOptions
)

val results = org.sireum.hamr.codegen.act.Act.run(rmodel, actOptions, aadlTypes, symbolTable, reporter)
actResources = actResources ++ results.resources

reporterIndex = printMessages(reporter.messages, options.verbose, reporterIndex, ISZ(ACT_INSTRUCTIONS_MESSAGE_KIND))
reporterIndex = printMessages(reporter.messages, modOptions.verbose, reporterIndex, ISZ(ACT_INSTRUCTIONS_MESSAGE_KIND))
}

actResources = removeDuplicates(actResources, reporter)
Expand All @@ -315,7 +325,7 @@ object CodeGen {
writeOutResources(actResources, reporter)
}

reporterIndex = printMessages(reporter.messages, options.verbose, reporterIndex, ISZ())
reporterIndex = printMessages(reporter.messages, modOptions.verbose, reporterIndex, ISZ())

if (!reporter.hasError && shouldWriteOutResources) {
// always print out any instructional messages
Expand All @@ -327,7 +337,7 @@ object CodeGen {
}
}

if (reporter.hasError && !options.verbose) { // at least need to print out the error messages
if (reporter.hasError && !modOptions.verbose) { // at least need to print out the error messages
printMessages(reporter.errors, T, 0, ISZ())
}

Expand Down
Loading

0 comments on commit 3810272

Please sign in to comment.