Skip to content

Commit

Permalink
add initial microkit vm support
Browse files Browse the repository at this point in the history
  • Loading branch information
@jasonbelt
jasonbelt committed Dec 10, 2024
1 parent 550bc8e commit 899f874
Show file tree
Hide file tree
Showing 14 changed files with 1,282 additions and 289 deletions.
17 changes: 17 additions & 0 deletions shared/src/main/scala/org/sireum/hamr/codegen/common/symbols/Symbols.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -181,6 +181,23 @@ import org.sireum.message.Position
return processors.elements
}

def getActualBoundProcessors(): ISZ[Processor] = {
var processors: Set[Processor] = Set.empty

for (process <- getProcesses()) {
getBoundProcessor(process) match {
case Some(aadlProcessor: AadlProcessor) => processors = processors + aadlProcessor
case Some(avp: AadlVirtualProcessor) =>
getActualBoundProcess(avp) match {
case Some(ap) => processors = processors + ap
case _ =>
}
case _ =>
}
}
return processors.elements
}

def hasVM(): B = {
return ops.ISZOps(getProcesses()).exists(p => p.toVirtualMachine(this))
}
Expand Down
469 changes: 259 additions & 210 deletions shared/src/main/scala/org/sireum/hamr/codegen/microkit/MicrokitCodegen.scala
View file

Large diffs are not rendered by default.

38 changes: 28 additions & 10 deletions shared/src/main/scala/org/sireum/hamr/codegen/microkit/connections/ConnectionStore.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,8 @@ package org.sireum.hamr.codegen.microkit.connections

import org.sireum._
import org.sireum.hamr.codegen.common.types.AadlType
import org.sireum.hamr.codegen.microkit.util.SharedMemoryRegion
import org.sireum.hamr.codegen.microkit.types.TypeUtil
import org.sireum.hamr.codegen.microkit.util.MemoryRegion
import org.sireum.hamr.codegen.microkit.util.Util.TAB

@sig trait ConnectionStore {
Expand All @@ -29,12 +30,12 @@ import org.sireum.hamr.codegen.microkit.util.Util.TAB
val receiverContributions: Map[ISZ[String], ConnectionContributions]) extends ConnectionStore

@sig trait SystemContributions {
def sharedMemoryRegionContributions: ISZ[SharedMemoryRegion]
def sharedMemoryRegionContributions: ISZ[MemoryRegion]

def channelContributions: ISZ[ST]
}

@datatype class DefaultSystemContributions(val sharedMemoryRegionContributions: ISZ[SharedMemoryRegion],
@datatype class DefaultSystemContributions(val sharedMemoryRegionContributions: ISZ[MemoryRegion],
val channelContributions: ISZ[ST]) extends SystemContributions

@sig trait TypeApiContributions {
Expand All @@ -43,7 +44,7 @@ import org.sireum.hamr.codegen.microkit.util.Util.TAB
def simpleFilename: String

@pure def objectName: String = {
return s"$simpleFilename.o"
return s"$$(TOP_DIR)/build/$simpleFilename.o"
}

@pure def headerFilename: String = {
Expand All @@ -56,8 +57,8 @@ import org.sireum.hamr.codegen.microkit.util.Util.TAB

@pure def buildEntry: ST = {
return (
st"""$objectName: $${TOP}/src/$implementationFilename Makefile
|${TAB}$$(CC) -c $$(CFLAGS) $$< -o $$@ -I$${TOP}/include
st"""$objectName: $$(TOP_DIR)/${TypeUtil.typesDir}/src/$implementationFilename Makefile
|${TAB}$$(CC) -c $$(CFLAGS) $$< -o $$@ $$(TOP_INCLUDE)
""")
}

Expand All @@ -71,6 +72,23 @@ import org.sireum.hamr.codegen.microkit.util.Util.TAB
val header: ST,
val implementation: ST) extends TypeApiContributions

@sig trait GlobalVarContribution {
def typ: String
def varName: String

def pretty: ST = {
return st"$typ $varName;"
}
}
@datatype class PortVaddr(val typ: String,
val varName: String) extends GlobalVarContribution

@datatype class QueueVaddr(val typ: String,
val varName: String) extends GlobalVarContribution

@datatype class VMRamVaddr (val typ: String,
val varName:String) extends GlobalVarContribution

@sig trait ConnectionContributions {

def portName: ISZ[String]
Expand All @@ -87,7 +105,7 @@ import org.sireum.hamr.codegen.microkit.util.Util.TAB

def defineContributions: ISZ[ST]

def globalVarContributions: ISZ[(String, String)]
def globalVarContributions: ISZ[GlobalVarContribution]

def apiMethodSigs: ISZ[ST]

Expand All @@ -97,7 +115,7 @@ import org.sireum.hamr.codegen.microkit.util.Util.TAB

def computeContributions: ISZ[ST]

def sharedMemoryMapping: ISZ[SharedMemoryRegion]
def sharedMemoryMapping: ISZ[MemoryRegion]
}

@datatype class DefaultConnectionContributions(val portName: ISZ[String],
Expand All @@ -107,9 +125,9 @@ import org.sireum.hamr.codegen.microkit.util.Util.TAB
val userMethodSignatures: ISZ[ST],
val userMethodDefaultImpls: ISZ[ST],
val defineContributions: ISZ[ST],
val globalVarContributions: ISZ[(String, String)],
val globalVarContributions: ISZ[GlobalVarContribution],
val apiMethodSigs: ISZ[ST],
val apiMethods: ISZ[ST],
val initContributions: ISZ[ST],
val computeContributions: ISZ[ST],
val sharedMemoryMapping: ISZ[SharedMemoryRegion]) extends ConnectionContributions
val sharedMemoryMapping: ISZ[MemoryRegion]) extends ConnectionContributions
42 changes: 27 additions & 15 deletions shared/src/main/scala/org/sireum/hamr/codegen/microkit/lint/Linter.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
package org.sireum.hamr.codegen.microkit.lint

import org.sireum._
import org.sireum.hamr.codegen.common.symbols.{AadlProcess, Dispatch_Protocol, SymbolTable}
import org.sireum.hamr.codegen.common.symbols.{AadlProcess, AadlProcessor, AadlVirtualProcessor, Dispatch_Protocol, SymbolTable}
import org.sireum.hamr.codegen.common.types.AadlTypes
import org.sireum.hamr.codegen.common.util.HamrCli
import org.sireum.hamr.codegen.microkit.MicrokitCodegen
Expand All @@ -12,21 +12,35 @@ import org.sireum.message.Reporter
object Linter {

def lint(model: Aadl, options: HamrCli.CodegenOption, types: AadlTypes, symbolTable: SymbolTable, reporter: Reporter): B = {
val allProcesses = symbolTable.getProcesses()

for (p <- symbolTable.getAllBoundProcessors()) {
if (p.getClockPeriod().isEmpty) {
reporter.error(p.component.identifier.pos, MicrokitCodegen.toolName, "Bound processors must be assigned a clock period.")
}
if (p.getFramePeriod().isEmpty) {
reporter.error(p.component.identifier.pos, MicrokitCodegen.toolName, "Bound processors must be assigned a frame period.")
for (p <- allProcesses) {
p.getBoundProcessor(symbolTable) match {
case Some(x) =>
val actualProcessor: AadlProcessor =
x match {
case avp: AadlVirtualProcessor =>
symbolTable.getActualBoundProcess(avp) match {
case Some(ap) => ap
case _ =>
reporter.error(avp.component.identifier.pos, MicrokitCodegen.toolName, "Virtual processors must be bound to an actual processor")
return F
}
case ap: AadlProcessor => ap
}
if (actualProcessor.getClockPeriod().isEmpty) {
reporter.error(actualProcessor.component.identifier.pos, MicrokitCodegen.toolName, "Bound processors must be assigned a clock period.")
}
if (actualProcessor.getFramePeriod().isEmpty) {
reporter.error(actualProcessor.component.identifier.pos, MicrokitCodegen.toolName, "Bound processors must be assigned a frame period.")
}
case _ =>
reporter.error(p.component.identifier.pos, MicrokitCodegen.toolName, "Processes must be bound to an actual processor")
}
}

var assignedDomains: Map[Z, AadlProcess] = Map.empty
for (p <- symbolTable.getProcesses()){
if (p.getBoundProcessor(symbolTable).isEmpty) {
reporter.error(p.component.identifier.pos, MicrokitCodegen.toolName, "Processes must be bound to a processor.")
}
for (p <- allProcesses){
if (p.getThreads().size > 1) {
reporter.error(p.component.identifier.pos, MicrokitCodegen.toolName, "Processes can only contain a single thread.")
}
Expand All @@ -49,9 +63,9 @@ object Linter {
if (t.period.isEmpty) {
reporter.error(t.component.identifier.pos, MicrokitCodegen.toolName, s"Periodic threads must be assigned a period property.")
}
//case Dispatch_Protocol.Sporadic =>
case Dispatch_Protocol.Sporadic =>
case s =>
//reporter.error(t.component.identifier.pos, MicrokitCodegen.toolName, s"Dispatch protocol ${s.name} is not currently supported.")
reporter.error(t.component.identifier.pos, MicrokitCodegen.toolName, s"Dispatch protocol ${s.name} is not currently supported.")
}

t.period match {
Expand All @@ -62,6 +76,4 @@ object Linter {

return !reporter.hasError
}


}
7 changes: 6 additions & 1 deletion shared/src/main/scala/org/sireum/hamr/codegen/microkit/types/QueueTemplate.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -319,7 +319,6 @@ object QueueTemplate {
|#include <${TypeUtil.eventCounterFilename}>
|#include <${TypeUtil.aadlTypesFilename}>
|#include <stdbool.h>
|#include <util.h>
|
|// Queue size must be an integer factor of the size for ${TypeUtil.eventCounterTypename} (an unsigned
|// integer type). Since we are using standard C unsigned integers for the
Expand Down Expand Up @@ -484,6 +483,12 @@ object QueueTemplate {
|#include <stdint.h>
|#include <stddef.h>
|
|#if __has_include("util.h")
|#include <util.h>
|#elif __has_include("libvmm/util.util.h")
|#include <libvmm/util/util.h>
|#endif
|
|//------------------------------------------------------------------------------
|// Sender API
|//
Expand Down
2 changes: 2 additions & 0 deletions shared/src/main/scala/org/sireum/hamr/codegen/microkit/types/TypeUtil.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,8 @@ import org.sireum.message.Reporter

object TypeUtil {

val typesDir: String = "types"

val allTypesFilename: String = brand("types.h")

val aadlTypesFilename: String = brand("aadl_types.h")
Expand Down
20 changes: 0 additions & 20 deletions shared/src/main/scala/org/sireum/hamr/codegen/microkit/util/Containers.scala
View file

This file was deleted.

76 changes: 54 additions & 22 deletions shared/src/main/scala/org/sireum/hamr/codegen/microkit/util/MakefileContainer.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ import org.sireum.hamr.codegen.microkit.types.TypeUtil
@datatype class MakefileContainer(val resourceSuffix: String,
val relativePath: Option[String],
val hasHeader: B,
val isVM: B,
val hasUserContent: B) {

@strictpure def cHeaderFilename: String = s"$resourceSuffix.h"
Expand All @@ -27,11 +28,11 @@ import org.sireum.hamr.codegen.microkit.types.TypeUtil

@strictpure def monImplFilename: String = s"${resourceSuffix}_MON.c"


@strictpure def vmArchive: String = s"${resourceSuffix}.a"

@pure def getElfNames: ISZ[String] = {
var ret: ISZ[String] = ISZ(elfName)
if (hasUserContent) {
if (hasUserContent || isVM) {
ret = ret :+ monElfName
}
return ret
Expand All @@ -46,9 +47,13 @@ import org.sireum.hamr.codegen.microkit.types.TypeUtil
return ret
}

@strictpure def relativePathSrcDir: String = if (relativePath.nonEmpty) s"${relativePath.get}/src" else ""
@strictpure def relativePathDir: String = if (relativePath.nonEmpty) s"${relativePath.get}" else ""

@strictpure def relativePathSrcDir: String = if (relativePath.nonEmpty) s"${relativePathDir}/src" else ""

@strictpure def relativePathIncludeDir: String = if (relativePath.nonEmpty) s"${relativePathDir}/include" else ""

@strictpure def relativePathIncludeDir: String = if (relativePath.nonEmpty) s"${relativePath.get}/include" else ""
@strictpure def relativePathVmBoardDir: String = if (relativePath.nonEmpty) s"${relativePathDir}/board" else ""

@pure def OBJSEntry: ST = {
var ret = st"${ops.StringOps(resourceSuffix).toUpper}_OBJS := $$(${TypeUtil.make_TYPE_OBJS}) $objName"
Expand All @@ -62,39 +67,66 @@ import org.sireum.hamr.codegen.microkit.types.TypeUtil
@pure def buildEntry: ST = {
val TAB: String = "\t"
// FIXME spilt output into include and src directories
val header: Option[String] = if (hasHeader) Some(s" -I$${TOP}/$relativePathIncludeDir") else None()
val userContributions: Option[ST] =
if (hasUserContent)
Some(
val header: Option[String] = if (hasHeader) Some(s" -I$$(TOP_DIR)/$relativePathIncludeDir") else None()
if (hasUserContent) {
return(
st"""# monitor
|$monObjName: $${TOP}/$relativePathSrcDir/$monImplFilename Makefile
|${TAB}$$(CC) -c $$(CFLAGS) $$< -o $$@ -I$${TOP}/include$header
|$monObjName: $$(TOP_DIR)/$relativePathSrcDir/$monImplFilename Makefile
|${TAB}$$(CC) -c $$(CFLAGS) $$< -o $$@ $$(TOP_INCLUDE)$header
|
|# user code
|$userObjName: $${TOP}/$relativePathSrcDir/$cUserImplFilename Makefile
|${TAB}$$(CC) -c $$(CFLAGS) $$< -o $$@ -I$${TOP}/include$header
|$userObjName: $$(TOP_DIR)/$relativePathSrcDir/$cUserImplFilename Makefile
|${TAB}$$(CC) -c $$(CFLAGS) $$< -o $$@ $$(TOP_INCLUDE)/$header
|
|$objName: $$(TOP_DIR)/$relativePathSrcDir/$cImplFilename Makefile
|${TAB}$$(CC) -c $$(CFLAGS) $$< -o $$@ $$(TOP_INCLUDE)$header""")
} else if (isVM) {
return(
st"""# monitor
|$monObjName: $$(TOP_DIR)/$relativePathSrcDir/$monImplFilename Makefile
|${TAB}$$(CC) -c $$(CFLAGS) $$< -o $$@ $$(TOP_INCLUDE)$header
|
|# $vmArchive contains a VM
|.PHONY: $vmArchive
|$vmArchive:
|ifeq (, $$(wildcard $$(TOP_DIR)/${relativePathDir}/board/$$(MICROKIT_BOARD)/Makefile))
|${TAB}$$(error Didn't find: $$(TOP_DIR)/$relativePathDir/board/$$(MICROKIT_BOARD)/Makefile);
|endif
|${TAB}mkdir -p $$(TOP_DIR)/$relativePathDir/build
|${TAB}cp $$(TOP_DIR)/$relativePathDir/board/$${MICROKIT_BOARD}/Makefile $$(TOP_DIR)/$relativePathDir/build
|${TAB}make -C $$(TOP_DIR)/$relativePathDir/build
|""")
else None()
val ret =
st"""$userContributions
|$objName: $${TOP}/$relativePathSrcDir/$cImplFilename Makefile
|${TAB}$$(CC) -c $$(CFLAGS) $$< -o $$@ -I$${TOP}/include$header"""
return ret
}
else {
return (
st"""
|$objName: $$(TOP_DIR)/$relativePathSrcDir/$cImplFilename Makefile
|${TAB}$$(CC) -c $$(CFLAGS) $$< -o $$@ -I$$(TOP_INCLUDE)$header""")
}
}

@pure def elfEntry: ST = {
val TAB: String = "\t"
if (hasUserContent) {
val ret =
st"""$monElfName: $$(${TypeUtil.make_TYPE_OBJS}) $monObjName
st"""$monElfName: $monObjName
|${TAB}$$(LD) $$(LDFLAGS) $$^ $$(LIBS) -o $$@
|
|$elfName: $$(${TypeUtil.make_TYPE_OBJS}) $userObjName $objName
|$elfName: $$(${Util.make_UTIL_OBJS}) $$(${TypeUtil.make_TYPE_OBJS}) $userObjName $objName
|${TAB}$$(LD) $$(LDFLAGS) $$^ $$(LIBS) -o $$@"""
return ret
} else {
} else if (isVM) {
val ret =
st"""$monElfName: $monObjName
|${TAB}$$(LD) $$(LDFLAGS) $$^ $$(LIBS) -o $$@
|
|$elfName: $$(${TypeUtil.make_TYPE_OBJS}) $vmArchive
|${TAB}$$(LD) $$(LDFLAGS) --start-group -lmicrokit -Tmicrokit.ld $$(TYPE_OBJS) $vmArchive --end-group -o $$@"""
return ret
}
else {
val ret =
st"""$elfName: $$(${TypeUtil.make_TYPE_OBJS}) $objName
st"""$elfName: $$(${Util.make_UTIL_OBJS}) $$(${TypeUtil.make_TYPE_OBJS}) $objName
|${TAB}$$(LD) $$(LDFLAGS) $$^ $$(LIBS) -o $$@"""
return ret
}
Expand Down
Loading

0 comments on commit 899f874

Please sign in to comment.