diff --git a/shared/src/main/scala/org/sireum/hamr/codegen/common/symbols/Symbols.scala b/shared/src/main/scala/org/sireum/hamr/codegen/common/symbols/Symbols.scala index d9418ae..5995223 100644 --- a/shared/src/main/scala/org/sireum/hamr/codegen/common/symbols/Symbols.scala +++ b/shared/src/main/scala/org/sireum/hamr/codegen/common/symbols/Symbols.scala @@ -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)) } diff --git a/shared/src/main/scala/org/sireum/hamr/codegen/microkit/MicrokitCodegen.scala b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/MicrokitCodegen.scala index 27631e7..ed42d4e 100644 --- a/shared/src/main/scala/org/sireum/hamr/codegen/microkit/MicrokitCodegen.scala +++ b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/MicrokitCodegen.scala @@ -12,12 +12,13 @@ import org.sireum.hamr.codegen.microkit.MicrokitCodegen.toolName import org.sireum.hamr.codegen.microkit.connections.{ConnectionContributions, ConnectionStore, TypeApiContributions} import org.sireum.hamr.codegen.microkit.lint.Linter import org.sireum.hamr.codegen.microkit.types.{QueueTemplate, TypeStore, TypeUtil} -import org.sireum.hamr.codegen.microkit.util.{Channel, MakefileContainer, MemoryMap, MemoryRegion, Perm, PortSharedMemoryRegion, ProtectionDomain, SchedulingDomain, SharedMemoryRegion, SystemDescription, Util} +import org.sireum.hamr.codegen.microkit.util._ import org.sireum.hamr.ir.{Aadl, Direction} import org.sireum.message.Reporter import org.sireum.hamr.codegen.microkit.connections._ import org.sireum.hamr.codegen.microkit.types._ import org.sireum.hamr.codegen.microkit.util.Util.TAB +import org.sireum.hamr.codegen.microkit.vm.{VmMakefileTemplate, VmUser, VmUtil} object MicrokitCodegen { val toolName: String = "Mircokit Codegen" @@ -70,13 +71,19 @@ object MicrokitCodegen { id = None(), stackSizeInKiBytes = None(), memMaps = ISZ(), + irqs = ISZ(), programImage = s"${MicrokitCodegen.pacerName}.elf", children = ISZ()) portPacerToEndOfFrame = getNextPacerChannelId portEndOfFrameToPacer = getNextPacerChannelId - val mk = MakefileContainer(resourceSuffix = MicrokitCodegen.pacerName, relativePath = Some(s"${MicrokitCodegen.dirComponents}/${ops.StringOps(MicrokitCodegen.pacerName).toLower}"), hasHeader = F, hasUserContent = F) + val mk = MakefileContainer( + resourceSuffix = MicrokitCodegen.pacerName, + relativePath = Some(s"${MicrokitCodegen.dirComponents}/${ops.StringOps(MicrokitCodegen.pacerName).toLower}"), + hasHeader = F, + isVM = F, + hasUserContent = F) makefileContainers = makefileContainers :+ mk val content = @@ -127,19 +134,18 @@ object MicrokitCodegen { } val content = - st"""#ifndef ${Util.toPreprocessorName(TypeUtil.aadlTypesFilename)} - |#define ${Util.toPreprocessorName(TypeUtil.aadlTypesFilename)} + st"""#pragma once | |#include | + |${Util.doNotEdit} + | |${(forwardDefs, "\n\n")} | |${(defs, "\n\n")} - | - |#endif |""" - val outputdir = s"${options.camkesOutputDir.get}/${MicrokitCodegen.dirInclude}" + val outputdir = s"${options.camkesOutputDir.get}/${TypeUtil.typesDir}/${MicrokitCodegen.dirInclude}" val path = s"$outputdir/${TypeUtil.aadlTypesFilename}" resources = resources :+ ResourceUtil.createResourceH(path, content, T, T) @@ -242,14 +248,16 @@ object MicrokitCodegen { var userMethodSignatures: ISZ[ST] = ISZ() var userMethodDefaultImpls: ISZ[ST] = ISZ() var computeContributions: ISZ[ST] = ISZ() - if (dstThread.isSporadic()) { - userMethodSignatures = userMethodSignatures :+ QueueTemplate.getClientEventHandlerMethodSig(dstPort.identifier) + if (!dstThread.toVirtualMachine(symbolTable)) { + if (dstThread.isSporadic()) { + userMethodSignatures = userMethodSignatures :+ QueueTemplate.getClientEventHandlerMethodSig(dstPort.identifier) - if (isEventPort || isEventDataPort) { - computeContributions = computeContributions :+ QueueTemplate.getClientSporadicComputeContributions(dstPort.identifier) - } + if (isEventPort || isEventDataPort) { + computeContributions = computeContributions :+ QueueTemplate.getClientSporadicComputeContributions(dstPort.identifier) + } - userMethodDefaultImpls = userMethodDefaultImpls :+ QueueTemplate.getClientSporadicDefaultImplContributions(dstPort.identifier) + userMethodDefaultImpls = userMethodDefaultImpls :+ QueueTemplate.getClientSporadicDefaultImplContributions(dstPort.identifier) + } } DefaultConnectionContributions( @@ -261,8 +269,8 @@ object MicrokitCodegen { userMethodDefaultImpls = userMethodDefaultImpls, defineContributions = ISZ(), globalVarContributions = ISZ( - (s"volatile $sharedMemTypeName", s"*$sharedVarName"), - (recvQueueTypeName, recvQueueVarName) + PortVaddr(s"volatile $sharedMemTypeName", s"*$sharedVarName"), + QueueVaddr(recvQueueTypeName, recvQueueVarName) ), apiMethodSigs = methodApiSigs, apiMethods = methodApis, @@ -274,7 +282,8 @@ object MicrokitCodegen { queueSize = dstQueueSize, varAddr = sharedVarName, perms = ISZ(Perm.READ), - dataSizeInKiBytes = Util.defaultPageSizeInKiBytes) + sizeInKiBytes = Util.defaultPageSizeInKiBytes, + physicalAddressInKiBytes = None()) ) ) } @@ -290,13 +299,13 @@ object MicrokitCodegen { val apiMethodSig = QueueTemplate.getClientPutMethodSig(srcPort.identifier, sPortType, isEventPort) val apiMethod = QueueTemplate.getClientPutMethod(srcPort.identifier, sPortType, srcPutContributions, isEventPort) - var sharedMemoryMappings: ISZ[SharedMemoryRegion] = ISZ() - var sharedMemoryVars: ISZ[(String, String)] = ISZ() + var sharedMemoryMappings: ISZ[MemoryRegion] = ISZ() + var sharedMemoryVars: ISZ[GlobalVarContribution] = ISZ() var initContributions: ISZ[ST] = ISZ() for (queueSize <- handledQueues.elements) { val queueType = QueueTemplate.getTypeQueueTypeName(sPortType, queueSize) val varName = QueueTemplate.getClientEnqueueSharedVarName(srcPort.identifier, queueSize) - sharedMemoryVars = sharedMemoryVars :+ (s"volatile $queueType", s"*$varName") + sharedMemoryVars = sharedMemoryVars :+ QueueVaddr(s"volatile $queueType", s"*$varName") initContributions = initContributions :+ QueueTemplate.getQueueInitMethod(varName, sPortType, queueSize) @@ -306,7 +315,8 @@ object MicrokitCodegen { queueSize = queueSize, varAddr = varName, perms = ISZ(Perm.READ, Perm.WRITE), - dataSizeInKiBytes = Util.defaultPageSizeInKiBytes + sizeInKiBytes = Util.defaultPageSizeInKiBytes, + physicalAddressInKiBytes = None() ) } @@ -339,20 +349,29 @@ object MicrokitCodegen { return ret } - def processThread(t: AadlThread, connectionStore: ISZ[ConnectionStore]): (ProtectionDomain, Z) = { + def processThread(t: AadlThread, + connectionStore: ISZ[ConnectionStore]): + (MicrokitDomain, ISZ[MemoryRegion], Z) = { + + var retMemoryRegions: ISZ[MemoryRegion] = ISZ() + + val isVM = t.toVirtualMachine(symbolTable) + val threadId = getName(t.path) val threadMonId = st"${getName(t.path)}_MON" var headerImports: ISZ[String] = ISZ() var userMethodSignatures: ISZ[ST] = ISZ() var userMethodDefaultImpls: ISZ[ST] = ISZ() - var vaddrs: ISZ[(String, String)] = ISZ() + var vaddrs: ISZ[GlobalVarContribution] = ISZ() var codeApiMethodSigs: ISZ[ST] = ISZ() var codeApiMethods: ISZ[ST] = ISZ() var initContributions: ISZ[ST] = ISZ() var computeContributions: ISZ[ST] = ISZ() var nextMemAddressInKiBytes = 262144 - var sharedMemoryRegions: ISZ[SharedMemoryRegion] = ISZ() + var sharedMemoryRegions: ISZ[MemoryRegion] = ISZ() + + val initializeMethodName = st"${threadId}_initialize" for (entry <- connectionStore) { @@ -393,7 +412,12 @@ object MicrokitCodegen { case _ => halt("Infeasible") } - val mk = MakefileContainer(resourceSuffix = threadId.render, relativePath = Some(s"${MicrokitCodegen.dirComponents}/${threadId.render}"), hasHeader = T, hasUserContent = T) + val mk = MakefileContainer( + resourceSuffix = threadId.render, + relativePath = Some(s"${MicrokitCodegen.dirComponents}/${threadId.render}"), + hasHeader = T, + isVM = isVM, + hasUserContent = !isVM) makefileContainers = makefileContainers :+ mk val computeExecutionTime: Z = t.getComputeExecutionTime() match { @@ -407,33 +431,125 @@ object MicrokitCodegen { SchedulingDomain(name = schedulingDomain, length = computeExecutionTime) var childMemMaps: ISZ[MemoryMap] = ISZ() + var childIrqs: ISZ[IRQ] = ISZ() + + var vms: ISZ[MicrokitDomain] = ISZ() + if (isVM) { + val vmName = s"${threadId.render}" + + val guestRam = VirtualMachineMemoryRegion( + typ = VirtualMemoryRegionType.RAM, + threadPath = t.path, + sizeInKiBytes = Util.defaultVmRamSizeInKiBytes, + physicalAddressInKiBytes = None() + ) + + val hostVaddr = VMRamVaddr("uintptr_t", guestRam.vmmVaddrName) + + vaddrs = vaddrs :+ hostVaddr + + childMemMaps = childMemMaps :+ MemoryMap( + memoryRegion = guestRam.name, + vaddrInKiBytes = 1048576, // 0x40_000_000 + perms = ISZ(Perm.READ, Perm.WRITE), + varAddr = Some(hostVaddr.varName), + cached = None()) + + retMemoryRegions = retMemoryRegions :+ guestRam + + nextMemAddressInKiBytes = nextMemAddressInKiBytes + guestRam.sizeInKiBytes + + val gicRegion = VirtualMachineMemoryRegion( + typ = VirtualMemoryRegionType.GIC, + threadPath = t.path, + sizeInKiBytes = 4, // 0x1000 + physicalAddressInKiBytes = Some(131328) // 0x8040000 + ) + retMemoryRegions = retMemoryRegions :+ gicRegion + + val serialRegion = VirtualMachineMemoryRegion( + typ = VirtualMemoryRegionType.SERIAL, + threadPath = t.path, + sizeInKiBytes = 4, // 0x1000 + physicalAddressInKiBytes = Some(147456) // 0x9_000_000 + ) + retMemoryRegions = retMemoryRegions :+ serialRegion + + childIrqs = childIrqs :+ IRQ(id = 1, irq = 33) + + vms = vms :+ VirtualMachine( + name = vmName, + vcpuId = "0", + schedulingDomain = Some(schedulingDomain), + memMaps = ISZ(MemoryMap( + memoryRegion = guestRam.name, + vaddrInKiBytes = 1048576, // 0x40_000_000 + perms = ISZ(Perm.READ, Perm.WRITE, Perm.EXECUTE), + varAddr = None(), + cached = None()), + + // Any access to the GIC from + // 0x8010000 - 0x8011000 will access the VCPU interface. All other + // accesses will result in virtual memory faults, routed to the VMM. + MemoryMap( + memoryRegion = gicRegion.name, + vaddrInKiBytes = 131136, // 0x8_010_000 + perms = ISZ(Perm.READ, Perm.WRITE), + varAddr = None(), + cached = Some(F) + ), + MemoryMap( + memoryRegion = serialRegion.name, + vaddrInKiBytes = 147456, // 0x9_000_000 + perms = ISZ(Perm.READ, Perm.WRITE), + varAddr = None(), + cached = Some(F) + )) + ) + + val boardPath = s"${options.camkesOutputDir.get}/${mk.relativePathVmBoardDir}/qemu_virt_aarch64" + + val vmmMake = VmMakefileTemplate.Makefile(threadId.render) + resources = resources :+ ResourceUtil.createResource(s"${boardPath}/Makefile", vmmMake, T) + + + val vmm_config = VmUtil.vmm_config( + guestDtbVaddrInHex = "0x4f000000", + guestInitRamDiskVaddrInHex = "0x4d700000", + maxIrqs = 1 + ) + resources = resources :+ ResourceUtil.createResource(s"${options.camkesOutputDir.get}/${mk.relativePathIncludeDir}/${threadId.render}_user.h", vmm_config, T) + } + + val childStackSizeInKiBytes: Option[Z] = t.stackSizeInBytes() match { + case Some(bytes) => Some(Util.bytesToKiBytes(bytes)) + case _ => None() + } + for (r <- sharedMemoryRegions) { r match { case p: PortSharedMemoryRegion => - childMemMaps = childMemMaps :+ MemoryMap( - memoryRegion = p.regionName, + memoryRegion = p.name, vaddrInKiBytes = nextMemAddressInKiBytes, perms = p.perms, - varAddr = p.varAddr) - nextMemAddressInKiBytes = nextMemAddressInKiBytes + p.dataSizeInKiBytes + varAddr = Some(p.varAddr), + cached = None()) + nextMemAddressInKiBytes = nextMemAddressInKiBytes + p.sizeInKiBytes case _ => halt("") } } - val stackSizeInKiBytes: Option[Z] = t.stackSizeInBytes() match { - case Some(bytes) => Some(Util.bytesToKiBytes(bytes)) - case _ => None() - } - - val child = ProtectionDomain( - name = threadId.render, - schedulingDomain = Some(schedulingDomain), - id = Some(s"1"), - stackSizeInKiBytes = stackSizeInKiBytes, - memMaps = childMemMaps, - programImage = mk.elfName, - children = ISZ()) + val child = + ProtectionDomain( + name = threadId.render, + schedulingDomain = Some(schedulingDomain), + id = Some(s"1"), + stackSizeInKiBytes = childStackSizeInKiBytes, + memMaps = childMemMaps, + irqs = childIrqs, + programImage = mk.elfName, + children = vms) xmlProtectionDomains = xmlProtectionDomains :+ ProtectionDomain( @@ -442,6 +558,7 @@ object MicrokitCodegen { id = None(), stackSizeInKiBytes = None(), memMaps = ISZ(), + irqs = ISZ(), programImage = mk.monElfName, children = ISZ(child)) @@ -467,7 +584,9 @@ object MicrokitCodegen { val headerFileName = s"${threadId.render}.h" val monImplSource = - st"""#include "$headerFileName" + st"""#include + | + |${Util.doNotEdit} | |#define PORT_PACER $pacerChannelId | @@ -492,28 +611,46 @@ object MicrokitCodegen { val monImplPath = s"${options.camkesOutputDir.get}/${mk.relativePathSrcDir}/${mk.monImplFilename}" resources = resources :+ ResourceUtil.createResource(monImplPath, monImplSource, T) - val initializeMethodName = st"${threadId}_initialize" - userMethodSignatures = st"void ${initializeMethodName}(void)" +: userMethodSignatures - - userMethodDefaultImpls = - st"""void $initializeMethodName(void) { - | // implement me - |}""" +: userMethodDefaultImpls - - if (t.isPeriodic()) { - val timeTriggeredMethodName = st"${threadId}_timeTriggered" - userMethodSignatures = userMethodSignatures :+ st"void ${timeTriggeredMethodName}(void)" - computeContributions = computeContributions :+ st"${timeTriggeredMethodName}();" - userMethodDefaultImpls = userMethodDefaultImpls :+ - st"""void $timeTriggeredMethodName(void) { + val userNotifyMethodName = st"${threadId}_notify" + initContributions = initContributions :+ st"$initializeMethodName();" + userMethodSignatures = st"void ${initializeMethodName}(void)" +: userMethodSignatures + userMethodSignatures = userMethodSignatures :+ st"void ${userNotifyMethodName}(microkit_channel channel)" + + userMethodDefaultImpls = + st"""void $initializeMethodName(void) { | // implement me - |}""" - } + |}""" +: userMethodDefaultImpls + + if (t.isPeriodic()) { + val timeTriggeredMethodName = st"${threadId}_timeTriggered" + userMethodSignatures = userMethodSignatures :+ st"void ${timeTriggeredMethodName}(void)" + computeContributions = computeContributions :+ st"${timeTriggeredMethodName}();" + userMethodDefaultImpls = userMethodDefaultImpls :+ + st"""void $timeTriggeredMethodName(void) { + | // implement me + |}""" + } + + userMethodDefaultImpls = userMethodDefaultImpls :+ + st"""void $userNotifyMethodName(microkit_channel channel) { + | // this method is called when the monitor does not handle the passed in channel + | switch (channel) { + | default: + | printf("%s: Unexpected channel %d\n", microkit_name, channel); + | } + |}""" - val vaddrEntries: ISZ[ST] = for (v <- vaddrs) yield st"${v._1} ${v._2};" + var vaddrEntries: ISZ[ST] = ISZ() + for (v <- vaddrs) { + if (!v.isInstanceOf[VMRamVaddr]) { + vaddrEntries = vaddrEntries :+ v.pretty + } + } val implSource = st"""#include "$headerFileName" + | + |${Util.doNotEdit} | |${(for (u <- userMethodSignatures) yield st"$u;", "\n")} | @@ -525,8 +662,6 @@ object MicrokitCodegen { | |void init(void) { | ${(initContributions, "\n\n")} - | - | $initializeMethodName(); |} | |void notified(microkit_channel channel) { @@ -534,6 +669,8 @@ object MicrokitCodegen { | case PORT_FROM_MON: | ${(computeContributions, "\n\n")} | break; + | default: + | ${userNotifyMethodName}(channel); | } |} |""" @@ -541,20 +678,41 @@ object MicrokitCodegen { val implPath = s"${options.camkesOutputDir.get}/${mk.relativePathSrcDir}/${mk.cImplFilename}" resources = resources :+ ResourceUtil.createResource(implPath, implSource, T) - val userImplSource = - st"""#include "$headerFileName" - | - |${(userMethodDefaultImpls, "\n\n")} - |""" val userImplPath = s"${options.camkesOutputDir.get}/${mk.relativePathSrcDir}/${mk.cUserImplFilename}" + val userImplSource: ST = + if (isVM) { + val cand = vaddrs.filter(f => f.isInstanceOf[VMRamVaddr]) + assert (cand.size == 1, s"didn't find a guest ram vaddr for ${t.identifier}: ${cand.size}") + VmUser.vmUserCode(threadId, cand(0).pretty) + } else { + st"""#include "$headerFileName" + | + |${Util.safeToEdit} + | + |${(userMethodDefaultImpls, "\n\n")} + |""" + } resources = resources :+ ResourceUtil.createResource(userImplPath, userImplSource, F) + val utilIncludes: ST = + if (isVM) + st"""#include + |#include """ + else + st"""#include + |#include """ + val himports: ISZ[ST] = for (h <- headerImports) yield st"#include <$h>" val headerSource = - st"""#include + st"""#pragma once + | + |$utilIncludes |#include |#include |#include <${TypeUtil.allTypesFilename}> + | + |${Util.doNotEdit} + | |${(himports, "\n")} | |${(codeApiMethodSigs, ";\n")}; @@ -562,7 +720,7 @@ object MicrokitCodegen { val headerPath = s"${options.camkesOutputDir.get}/${mk.relativePathIncludeDir}/${mk.cHeaderFilename}" resources = resources :+ ResourceUtil.createResource(headerPath, headerSource, T) - return (child, computeExecutionTime) + return (child, retMemoryRegions, computeExecutionTime) } // end processThread @@ -570,9 +728,9 @@ object MicrokitCodegen { return CodeGenResults(ISZ(), ISZ()) } - val boundProcessors = symbolTable.getAllBoundProcessors() + val boundProcessors = symbolTable.getActualBoundProcessors() if (boundProcessors.size != 1) { - reporter.error(None(), toolName, "Currently handling models with exactly one bound processor") + reporter.error(None(), toolName, "Currently only handling models with exactly one actual bound processor") return CodeGenResults(ISZ(), ISZ()) } var framePeriod: Z = 0 @@ -585,23 +743,23 @@ object MicrokitCodegen { val typeStore = processTypes() - var typeHeaderFilenemes: ISZ[String] = ISZ(TypeUtil.aadlTypesFilename) + var typeHeaderFilenames: ISZ[String] = ISZ(TypeUtil.aadlTypesFilename) var typeImplFilenames: ISZ[String] = ISZ() - var objectNames: ISZ[String] = ISZ() + var typeObjectNames: ISZ[String] = ISZ() - val baseIncludePath = s"${options.camkesOutputDir.get}/${MicrokitCodegen.dirInclude}" + val baseTypesIncludePath = s"${options.camkesOutputDir.get}/${TypeUtil.typesDir}/${MicrokitCodegen.dirInclude}" val connectionStore = processConnections(typeStore) for (entry <- connectionStore) { - val srcPath = s"${options.camkesOutputDir.get}/${MicrokitCodegen.dirSrc}" + val srcPath = s"${options.camkesOutputDir.get}/${TypeUtil.typesDir}/${MicrokitCodegen.dirSrc}" for (tc <- entry.typeApiContributions) { - typeHeaderFilenemes = typeHeaderFilenemes :+ tc.headerFilename + typeHeaderFilenames = typeHeaderFilenames :+ tc.headerFilename typeImplFilenames = typeImplFilenames :+ tc.implementationFilename - objectNames = objectNames :+ tc.objectName + typeObjectNames = typeObjectNames :+ tc.objectName buildEntries = buildEntries :+ tc.buildEntry - val headerPath = s"$baseIncludePath/${tc.headerFilename}" + val headerPath = s"$baseTypesIncludePath/${tc.headerFilename}" resources = resources :+ ResourceUtil.createResourceH( path = headerPath, content = tc.header, overwrite = T, isDatatype = T) @@ -611,25 +769,27 @@ object MicrokitCodegen { } } - val eventCounterPath = s"$baseIncludePath/${TypeUtil.eventCounterFilename}" + val eventCounterPath = s"$baseTypesIncludePath/${TypeUtil.eventCounterFilename}" resources = resources :+ ResourceUtil.createResourceH( path = eventCounterPath, content = TypeUtil.eventCounterContent, overwrite = T, isDatatype = T) val allTypesContent = - st"""#ifndef ${Util.toPreprocessorName(TypeUtil.allTypesFilename)} - |#define ${Util.toPreprocessorName(TypeUtil.allTypesFilename)} + st"""#pragma once | - |${(for (i <- typeHeaderFilenemes) yield st"#include <$i>", "\n")} + |${Util.doNotEdit} | - |#endif""" - val allTypesPath = s"$baseIncludePath/${TypeUtil.allTypesFilename}" + |${(for (i <- typeHeaderFilenames) yield st"#include <$i>", "\n")} + |""" + val allTypesPath = s"$baseTypesIncludePath/${TypeUtil.allTypesFilename}" resources = resources :+ ResourceUtil.createResourceH( path = allTypesPath, content = allTypesContent, overwrite = T, isDatatype = T) + var memoryRegions: ISZ[MemoryRegion] = ISZ() var usedBudget: Z = 0 for (t <- symbolTable.getThreads()) { val results = processThread(t, connectionStore) - usedBudget = usedBudget + results._2 + memoryRegions = memoryRegions ++ results._2 + usedBudget = usedBudget + results._3 } addPacerComponent() @@ -649,10 +809,10 @@ object MicrokitCodegen { } xmlScheds = xmlScheds :+ SchedulingDomain(name = "domain0", length = framePeriod - usedBudget) - var memoryRegions: ISZ[MemoryRegion] = ISZ() + for (e <- connectionStore; s <- e.systemContributions.sharedMemoryRegionContributions) { - memoryRegions = memoryRegions :+ MemoryRegion(name = s.regionName, sizeInKiBytes = s.dataSizeInKiBytes) + memoryRegions = memoryRegions :+ s } val sd = SystemDescription( @@ -668,39 +828,7 @@ object MicrokitCodegen { val dotPath = s"${options.camkesOutputDir.get}/microkit.dot" resources = resources :+ ResourceUtil.createResource(path = dotPath, content = sysDot, overwrite = T) - val makefileContents = - st"""ifeq ($$(strip $$(MICROKIT_SDK)),) - |$$(error MICROKIT_SDK must be specified) - |endif - |override MICROKIT_SDK := $$(abspath $${MICROKIT_SDK}) - | - |BUILD_DIR ?= build - |# By default we make a debug build so that the client debug prints can be seen. - |MICROKIT_CONFIG ?= debug - | - |export CPU := cortex-a53 - |QEMU := qemu-system-aarch64 - | - |CC := clang - |LD := ld.lld - |export MICROKIT_TOOL ?= $$(abspath $$(MICROKIT_SDK)/bin/microkit) - | - |export BOARD_DIR := $$(abspath $$(MICROKIT_SDK)/board/qemu_virt_aarch64/debug) - |export TOP:= $$(abspath $$(dir $${MAKEFILE_LIST})) - |IMAGE_FILE := $$(BUILD_DIR)/loader.img - |REPORT_FILE := $$(BUILD_DIR)/report.txt - | - |all: $${IMAGE_FILE} - | - |qemu $${IMAGE_FILE} $${REPORT_FILE} clean clobber: $$(IMAGE_FILE) $${BUILD_DIR}/Makefile FORCE - |${TAB}$${MAKE} -C $${BUILD_DIR} MICROKIT_SDK=$${MICROKIT_SDK} $$(notdir $$@) - | - |$${BUILD_DIR}/Makefile: ${MicrokitCodegen.systemMakeFilename} - |${TAB}mkdir -p $${BUILD_DIR} - |${TAB}cp ${MicrokitCodegen.systemMakeFilename} $${BUILD_DIR}/Makefile - | - |FORCE: - |""" + val makefileContents = MakefileTemplate.mainMakefile val makefilePath = s"${options.camkesOutputDir.get}/Makefile" resources = resources :+ ResourceUtil.createResource(makefilePath, makefileContents, T) @@ -715,101 +843,22 @@ object MicrokitCodegen { val elfEntries: ISZ[ST] = for (mk <- makefileContainers) yield mk.elfEntry - val systemmkContents = - st"""ifeq ($$(strip $$(MICROKIT_SDK)),) - |$$(error MICROKIT_SDK must be specified) - |endif - | - |MICROKIT_TOOL ?= $$(MICROKIT_SDK)/bin/microkit - | - |ifeq ("$$(wildcard $$(MICROKIT_TOOL))","") - |$$(error Microkit tool not found at $${MICROKIT_TOOL}) - |endif - | - |ifeq ($$(strip $$(MICROKIT_BOARD)),) - |$$(error MICROKIT_BOARD must be specified) - |endif - | - |BUILD_DIR ?= build - |# By default we make a debug build so that the client debug prints can be seen. - |MICROKIT_CONFIG ?= debug - | - |QEMU := qemu-system-aarch64 - | - |CC := clang - |LD := ld.lld - |AR := llvm-ar - |RANLIB := llvm-ranlib - | - |CFLAGS := -mcpu=$$(CPU) \ - |${TAB}-mstrict-align \ - |${TAB}-nostdlib \ - |${TAB}-ffreestanding \ - |${TAB}-g3 \ - |${TAB}-O3 \ - |${TAB}-Wall -Wno-unused-function -Werror -Wno-unused-command-line-argument \ - |${TAB}-target aarch64-none-elf \ - |${TAB}-I$$(BOARD_DIR)/include - |LDFLAGS := -L$$(BOARD_DIR)/lib - |LIBS := --start-group -lmicrokit -Tmicrokit.ld --end-group - | - | - |${TypeUtil.make_TYPE_OBJS} := printf.o util.o ${(objectNames, " ")} - | - |SYSTEM_FILE := $${TOP}/${MicrokitCodegen.microkitSystemXmlFilename} - | - |IMAGES := ${(elfFiles, " ")} - |IMAGE_FILE = loader.img - |REPORT_FILE = report.txt - | - |all: $$(IMAGE_FILE) - |${TAB}CHECK_FLAGS_BOARD_MD5:=.board_cflags-$$(shell echo -- $${CFLAGS} $${BOARD} $${MICROKIT_CONFIG}| shasum | sed 's/ *-//') - | - |$${CHECK_FLAGS_BOARD_MD5}: - |${TAB}-rm -f .board_cflags-* - |${TAB}touch $$@ - | - |%.o: $${TOP}/%.c Makefile - |${TAB}$$(CC) -c $$(CFLAGS) $$< -o $$@ -I$${TOP}/include - | - |printf.o: $${TOP}/${MicrokitCodegen.dirSrc}/printf.c Makefile - |${TAB}$$(CC) -c $$(CFLAGS) $$< -o $$@ -I$${TOP}/include - | - |util.o: $${TOP}/${MicrokitCodegen.dirSrc}/util.c Makefile - |${TAB}$$(CC) -c $$(CFLAGS) $$< -o $$@ -I$${TOP}/include - | - |${(buildEntries, "\n\n")} - | - |${(elfEntries, "\n\n")} - | - |$$(IMAGE_FILE): $$(IMAGES) $$(SYSTEM_FILE) - |${TAB}$$(MICROKIT_TOOL) $$(SYSTEM_FILE) --search-path $$(BUILD_DIR) --board $$(MICROKIT_BOARD) --config $$(MICROKIT_CONFIG) -o $$(IMAGE_FILE) -r $$(REPORT_FILE) - | - | - |qemu: $$(IMAGE_FILE) - |${TAB}$$(QEMU) -machine virt,virtualization=on \ - |${TAB}${TAB}${TAB}-cpu cortex-a53 \ - |${TAB}${TAB}${TAB}-serial mon:stdio \ - |${TAB}${TAB}${TAB}-device loader,file=$$(IMAGE_FILE),addr=0x70000000,cpu-num=0 \ - |${TAB}${TAB}${TAB}-m size=2G \ - |${TAB}${TAB}${TAB}-nographic - | - |clean:: - |${TAB}rm -f ${(oFiles, " ")} - | - |clobber:: clean - |${TAB}rm -f ${(elfFiles, " ")} $${IMAGE_FILE} $${REPORT_FILE} - |""" + val systemmkContents = MakefileTemplate.systemMakefile( + elfFiles = elfFiles, + typeObjectNames = typeObjectNames, + buildEntries = buildEntries, + elfEntries = elfEntries) + val systemmkPath = s"${options.camkesOutputDir.get}/${MicrokitCodegen.systemMakeFilename}" resources = resources :+ ResourceUtil.createResource(systemmkPath, systemmkContents, T) - val includePath = s"${options.camkesOutputDir.get}/${MicrokitCodegen.dirInclude}" - val srcPath = s"${options.camkesOutputDir.get}/${MicrokitCodegen.dirSrc}" - resources = resources :+ ResourceUtil.createResource(s"${includePath}/printf.h", Util.printfh, T) - resources = resources :+ ResourceUtil.createResource(s"${srcPath}/printf.c", Util.printfc, T) - resources = resources :+ ResourceUtil.createResource(s"${includePath}/util.h", Util.utilh, T) - resources = resources :+ ResourceUtil.createResource(s"${srcPath}/util.c", Util.utilc, T) + val utilIncludePath = s"${options.camkesOutputDir.get}/${Util.utilDir}/${MicrokitCodegen.dirInclude}" + val utilSrcPath = s"${options.camkesOutputDir.get}/${Util.utilDir}/${MicrokitCodegen.dirSrc}" + resources = resources :+ ResourceUtil.createResource(s"${utilIncludePath}/printf.h", Util.printfh, T) + resources = resources :+ ResourceUtil.createResource(s"${utilSrcPath}/printf.c", Util.printfc, T) + resources = resources :+ ResourceUtil.createResource(s"${utilIncludePath}/util.h", Util.utilh, T) + resources = resources :+ ResourceUtil.createResource(s"${utilSrcPath}/util.c", Util.utilc, T) return CodeGenResults(resources = resources, auxResources = ISZ()) } diff --git a/shared/src/main/scala/org/sireum/hamr/codegen/microkit/connections/ConnectionStore.scala b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/connections/ConnectionStore.scala index 4cd3cf5..a11160b 100644 --- a/shared/src/main/scala/org/sireum/hamr/codegen/microkit/connections/ConnectionStore.scala +++ b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/connections/ConnectionStore.scala @@ -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 { @@ -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 { @@ -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 = { @@ -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) """) } @@ -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] @@ -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] @@ -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], @@ -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 \ No newline at end of file + val sharedMemoryMapping: ISZ[MemoryRegion]) extends ConnectionContributions \ No newline at end of file diff --git a/shared/src/main/scala/org/sireum/hamr/codegen/microkit/lint/Linter.scala b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/lint/Linter.scala index 8d87aa5..264978f 100644 --- a/shared/src/main/scala/org/sireum/hamr/codegen/microkit/lint/Linter.scala +++ b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/lint/Linter.scala @@ -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 @@ -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.") } @@ -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 { @@ -62,6 +76,4 @@ object Linter { return !reporter.hasError } - - } diff --git a/shared/src/main/scala/org/sireum/hamr/codegen/microkit/types/QueueTemplate.scala b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/types/QueueTemplate.scala index fe13ebb..742ab97 100644 --- a/shared/src/main/scala/org/sireum/hamr/codegen/microkit/types/QueueTemplate.scala +++ b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/types/QueueTemplate.scala @@ -319,7 +319,6 @@ object QueueTemplate { |#include <${TypeUtil.eventCounterFilename}> |#include <${TypeUtil.aadlTypesFilename}> |#include - |#include | |// 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 @@ -484,6 +483,12 @@ object QueueTemplate { |#include |#include | + |#if __has_include("util.h") + |#include + |#elif __has_include("libvmm/util.util.h") + |#include + |#endif + | |//------------------------------------------------------------------------------ |// Sender API |// diff --git a/shared/src/main/scala/org/sireum/hamr/codegen/microkit/types/TypeUtil.scala b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/types/TypeUtil.scala index 62b098f..cf0922f 100644 --- a/shared/src/main/scala/org/sireum/hamr/codegen/microkit/types/TypeUtil.scala +++ b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/types/TypeUtil.scala @@ -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") diff --git a/shared/src/main/scala/org/sireum/hamr/codegen/microkit/util/Containers.scala b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/util/Containers.scala deleted file mode 100644 index 474a8b7..0000000 --- a/shared/src/main/scala/org/sireum/hamr/codegen/microkit/util/Containers.scala +++ /dev/null @@ -1,20 +0,0 @@ -// #Sireum -package org.sireum.hamr.codegen.microkit.util - -import org.sireum._ - -@sig trait SharedMemoryRegion { - def regionName: String - def dataSizeInKiBytes: Z -} - -@datatype class PortSharedMemoryRegion(val outgoingPortPath: ISZ[String], - val queueSize: Z, - val varAddr: String, - val perms: ISZ[Perm.Type], - val dataSizeInKiBytes: Z) extends SharedMemoryRegion{ - - def regionName: String = { - return st"${(outgoingPortPath, "_")}_${queueSize}_Memory_Region".render - } -} diff --git a/shared/src/main/scala/org/sireum/hamr/codegen/microkit/util/MakefileContainer.scala b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/util/MakefileContainer.scala index 93e50ac..0b40af5 100644 --- a/shared/src/main/scala/org/sireum/hamr/codegen/microkit/util/MakefileContainer.scala +++ b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/util/MakefileContainer.scala @@ -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" @@ -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 @@ -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" @@ -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 } diff --git a/shared/src/main/scala/org/sireum/hamr/codegen/microkit/util/MakefileTemplate.scala b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/util/MakefileTemplate.scala new file mode 100644 index 0000000..3e20dda --- /dev/null +++ b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/util/MakefileTemplate.scala @@ -0,0 +1,145 @@ +// #Sireum +package org.sireum.hamr.codegen.microkit.util + +import org.sireum._ +import org.sireum.hamr.codegen.microkit.MicrokitCodegen +import org.sireum.hamr.codegen.microkit.types.TypeUtil +import org.sireum.hamr.codegen.microkit.util.Util.TAB + +object MakefileTemplate { + + def mainMakefile: ST = { + val content = + st"""${Util.doNotEditMakefile} + | + |ifeq ($$(strip $$(MICROKIT_SDK)),) + |$$(error MICROKIT_SDK must be specified) + |endif + |override MICROKIT_SDK := $$(abspath $${MICROKIT_SDK}) + | + |SYSTEM_MAKEFILE ?= system.mk + | + |export CPU = cortex-a53 + |export QEMU = qemu-system-aarch64 + | + |export AR := ar + |export CC := clang + |export DTC := dtc + |export LD := ld.lld + |export RANLIB := llvm-ranlib + | + |export TOP_DIR := $$(abspath $$(dir $${MAKEFILE_LIST})) + |export TOP_BUILD_DIR := $$(abspath build) + | + |export TARGET := aarch64-none-elf + | + |# By default we make a debug build so that the client debug prints can be seen. + |export MICROKIT_CONFIG ?= debug + | + |export MICROKIT_SDK := $$(abspath $$(MICROKIT_SDK)) + |export MICROKIT_TOOL := $$(abspath $$(MICROKIT_SDK)/bin/microkit) + |export MICROKIT_BOARD_DIR := $$(abspath $$(MICROKIT_SDK)/board/$$(MICROKIT_BOARD)/$$(MICROKIT_CONFIG)) + | + | + |IMAGE_FILE := $$(TOP_BUILD_DIR)/loader.img + |REPORT_FILE := $$(TOP_BUILD_DIR)/report.txt + | + |all: $${IMAGE_FILE} + | + |qemu $${IMAGE_FILE} $${REPORT_FILE} clean clobber: $$(IMAGE_FILE) $${TOP_BUILD_DIR}/Makefile FORCE + | $${MAKE} -C $${TOP_BUILD_DIR} $$(notdir $$@) + | + |$${TOP_BUILD_DIR}/Makefile: $$(SYSTEM_MAKEFILE) + | mkdir -p $${TOP_BUILD_DIR} + | cp $$(SYSTEM_MAKEFILE) $${TOP_BUILD_DIR}/Makefile + | + |FORCE: + |""" + return content + } + + @pure def systemMakefile(elfFiles: ISZ[String], + typeObjectNames: ISZ[String], + buildEntries: ISZ[ST], + elfEntries: ISZ[ST]): ST = { + val content = + st"""${Util.doNotEditMakefile} + | + |ifeq ($$(strip $$(MICROKIT_SDK)),) + |$$(error MICROKIT_SDK must be specified) + |endif + | + |MICROKIT_TOOL ?= $$(MICROKIT_SDK)/bin/microkit + | + |ifeq ("$$(wildcard $$(MICROKIT_TOOL))","") + |$$(error Microkit tool not found at $${MICROKIT_TOOL}) + |endif + | + |ifeq ($$(strip $$(MICROKIT_BOARD)),) + |$$(error MICROKIT_BOARD must be specified) + |endif + | + |CFLAGS := -mcpu=$$(CPU) \ + |${TAB}-mstrict-align \ + |${TAB}-ffreestanding \ + |${TAB}-nostdlib \ + |${TAB}-g3 \ + |${TAB}-O3 \ + |${TAB}-Wall -Wno-unused-function -Werror -Wno-unused-command-line-argument \ + |${TAB}-I$$(MICROKIT_BOARD_DIR)/include \ + |${TAB}-target $$(TARGET) + | + |LDFLAGS := -L$$(MICROKIT_BOARD_DIR)/lib + |LIBS := --start-group -lmicrokit -Tmicrokit.ld --end-group + | + |SYSTEM_FILE := $$(TOP_DIR)/${MicrokitCodegen.microkitSystemXmlFilename} + | + |IMAGES := ${(elfFiles, " ")} + |IMAGE_FILE = loader.img + |REPORT_FILE = report.txt + | + |UTIL_OBJS = printf.o util.o + | + |TYPES_DIR = $$(TOP_DIR)/types + |TYPE_OBJS := ${(typeObjectNames, " ")} + | + |# exporting TOP_TYPES_INCLUDE in case other makefiles need it + |export TOP_TYPES_INCLUDE = -I$$(TYPES_DIR)/include + | + |TOP_INCLUDE = $$(TOP_TYPES_INCLUDE) -I$$(TOP_DIR)/util/include + | + |all: $$(IMAGE_FILE) + |${TAB}CHECK_FLAGS_BOARD_MD5:=.board_cflags-$$(shell echo -- $${CFLAGS} $${MICROKIT_BOARD} $${MICROKIT_CONFIG}| shasum | sed 's/ *-//') + | + |$${CHECK_FLAGS_BOARD_MD5}: + |${TAB}-rm -f .board_cflags-* + |${TAB}touch $$@ + | + |%.o: $${TOP_DIR}/util/src/%.c Makefile + |${TAB}$$(CC) -c $$(CFLAGS) $$< -o $$@ -I$$(TOP_DIR)/util/include + | + |${(buildEntries, "\n\n")} + | + |${(elfEntries, "\n\n")} + | + |$$(IMAGE_FILE): $$(IMAGES) $$(SYSTEM_FILE) + |${TAB}$$(MICROKIT_TOOL) $$(SYSTEM_FILE) --search-path $$(TOP_BUILD_DIR) --board $$(MICROKIT_BOARD) --config $$(MICROKIT_CONFIG) -o $$(IMAGE_FILE) -r $$(REPORT_FILE) + | + | + |qemu: $$(IMAGE_FILE) + |${TAB}$$(QEMU) -machine virt,virtualization=on \ + |${TAB}${TAB}${TAB}-cpu cortex-a53 \ + |${TAB}${TAB}${TAB}-serial mon:stdio \ + |${TAB}${TAB}${TAB}-device loader,file=$$(IMAGE_FILE),addr=0x70000000,cpu-num=0 \ + |${TAB}${TAB}${TAB}-m size=2G \ + |${TAB}${TAB}${TAB}-nographic + | + |clean:: + |${TAB}rm -f $${(oFiles, " ")} + | + |clobber:: clean + |${TAB}rm -f ${(elfFiles, " ")} $${IMAGE_FILE} $${REPORT_FILE} + |""" + return content + } +} diff --git a/shared/src/main/scala/org/sireum/hamr/codegen/microkit/util/SystemDescription.scala b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/util/SystemDescription.scala index 023610a..da7c968 100644 --- a/shared/src/main/scala/org/sireum/hamr/codegen/microkit/util/SystemDescription.scala +++ b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/util/SystemDescription.scala @@ -66,15 +66,53 @@ import org.sireum.hamr.codegen.microkit.util.Util.{KiBytesToHex} @strictpure def prettyST: ST = st"""""" } +@sig trait MicrokitDomain { + def name: String + def schedulingDomain: Option[String] + + def memMaps: ISZ[MemoryMap] + + def prettyST: ST + + def toDot: ST + + def getDotMemConnections: ISZ[ST] +} + +@datatype class VirtualMachine(val name: String, + val vcpuId: String, + val schedulingDomain: Option[String], + val memMaps: ISZ[MemoryMap]) extends MicrokitDomain { + + override def prettyST: ST = { + val stMaps: Option[ST] = + if (memMaps.nonEmpty) Some(st"${(for (m <- memMaps) yield m.prettyST, "\n")}") + else None() + return (st""" + | + | $stMaps + |""") + } + + override def toDot: ST = { + return st"toDot: TODO" + } + + override def getDotMemConnections: ISZ[ST] = { + return ISZ(st"getDotMemConnections: TODO") + } +} + @datatype class ProtectionDomain (val name: String, val schedulingDomain: Option[String], val id: Option[String], val stackSizeInKiBytes: Option[Z], val memMaps: ISZ[MemoryMap], + val irqs: ISZ[IRQ], val programImage: String, - val children: ISZ[ProtectionDomain]) { + val children: ISZ[MicrokitDomain]) extends MicrokitDomain { @pure def prettyST: ST = { val domain: Option[ST] = if (schedulingDomain.nonEmpty) Some(st""" domain="${schedulingDomain.get}"""") @@ -89,6 +127,9 @@ import org.sireum.hamr.codegen.microkit.util.Util.{KiBytesToHex} val stMaps: Option[ST] = if (memMaps.nonEmpty) Some(st"${(for (m <- memMaps) yield m.prettyST, "\n")}") else None() + val irqsOpt: Option[ST] = + if (irqs.nonEmpty) Some(st"${(for (i <- irqs) yield i.prettyST, "\n")}") + else None() val stackSizeOpt: Option[ST] = stackSizeInKiBytes match { case Some(k) => Some(st""" stack_size="${KiBytesToHex(k)}"""") @@ -96,9 +137,10 @@ import org.sireum.hamr.codegen.microkit.util.Util.{KiBytesToHex} } val ret = st""" - | $stChildren - | $stMaps | + | $stMaps + | $irqsOpt + | $stChildren |""" return ret } @@ -131,11 +173,61 @@ import org.sireum.hamr.codegen.microkit.util.Util.{KiBytesToHex} } } -@datatype class MemoryRegion (name: String, - sizeInKiBytes: Z) { - @strictpure def prettyST: ST = st"""""" +@sig trait MemoryRegion { + def name: String + def sizeInKiBytes: Z + def physicalAddressInKiBytes: Option[Z] - @strictpure def toDot: ST = st"$name" + @pure def prettyST: ST = { + val physAddr: Option[ST] = + if (physicalAddressInKiBytes.nonEmpty) Some( + st""" + | phys_addr="${KiBytesToHex(physicalAddressInKiBytes.get)}"""") + else None() + return ( + st"""""") + } + + @pure def toDot: ST = { + return st"$name" + } +} + +@datatype class PortSharedMemoryRegion(val outgoingPortPath: ISZ[String], + val queueSize: Z, + val varAddr: String, + val perms: ISZ[Perm.Type], + val sizeInKiBytes: Z, + val physicalAddressInKiBytes: Option[Z]) extends MemoryRegion { + + def name: String = { + return st"${(outgoingPortPath, "_")}_${queueSize}_Memory_Region".render + } +} + +@enum object VirtualMemoryRegionType { + "GIC" + "RAM" + "SERIAL" +} + +@datatype class VirtualMachineMemoryRegion(val typ: VirtualMemoryRegionType.Type, + val threadPath: ISZ[String], + val sizeInKiBytes: Z, + val physicalAddressInKiBytes: Option[Z]) extends MemoryRegion { + def name: String = { + val suffix: String = typ match { + case VirtualMemoryRegionType.GIC => "GIC" + case VirtualMemoryRegionType.RAM => "Guest_RAM" + case VirtualMemoryRegionType.SERIAL => "Serial" + } + return st"${(threadPath, "_")}_VM_${suffix}".render + } + + def vmmVaddrName: String = { + return s"${name}_vaddr" + } } @datatype class Channel (val firstPD: String, @@ -153,21 +245,44 @@ import org.sireum.hamr.codegen.microkit.util.Util.{KiBytesToHex} } } +@datatype class IRQ(val id: Z, + val irq: Z) { + @pure def prettyST: ST = { + return st"""""" + } +} + @datatype class MemoryMap (val memoryRegion: String, val vaddrInKiBytes: Z, val perms: ISZ[Perm.Type], - val varAddr: String) { + val varAddr: Option[String], + val cached: Option[B]) { @pure def prettyST: ST = { - val stPerms = st"""${(for (p <- perms) yield (if (p == Perm.READ) "r" else "w"), "")}""" + val stPerms = st"""${(for (p <- perms) yield ( + if (p == Perm.READ) "r" + else if (p == Perm.WRITE) "w" + else "x"), "")}""" + val setVarAddr: Option[String] = + if (varAddr.nonEmpty) Some(s"setvar_vaddr=\"${varAddr.get}\"") + else None() + val cachedOpt: Option[ST] = + if (cached.nonEmpty) Some(st"""cached="${if(cached.get) "true" else "false"}"""") + else None() return ( st"""""") + | $setVarAddr + | $cachedOpt + |/>""") } @pure def toDotConnection: ST = { - val style: Option[ST] = + val style: Option[ST] = { + if (perms.size == 3){ + assert (ops.ISZOps(perms).contains(Perm.EXECUTE) && + ops.ISZOps(perms).contains(Perm.READ) && ops.ISZOps(perms).contains(Perm.WRITE)) + } if (perms.size == 2) { assert (ops.ISZOps(perms).contains(Perm.READ) && ops.ISZOps(perms).contains(Perm.WRITE)) Some(st"dir=both,") @@ -178,6 +293,7 @@ import org.sireum.hamr.codegen.microkit.util.Util.{KiBytesToHex} else { halt("Infeasible") } + } return st"$varAddr -> $memoryRegion [$style style=dashed]" } @@ -187,6 +303,7 @@ import org.sireum.hamr.codegen.microkit.util.Util.{KiBytesToHex} } @enum object Perm { + "EXECUTE" "READ" "WRITE" } \ No newline at end of file diff --git a/shared/src/main/scala/org/sireum/hamr/codegen/microkit/util/Util.scala b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/util/Util.scala index 4a5c5fd..d3f4cc3 100644 --- a/shared/src/main/scala/org/sireum/hamr/codegen/microkit/util/Util.scala +++ b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/util/Util.scala @@ -7,13 +7,25 @@ object Util { val TAB: String = "\t" + val utilDir: String = "util" + + val make_UTIL_OBJS: String = "UTIL_OBJS" + val defaultPageSizeInKiBytes: Z = 4 val MemAlignmentInKiBytes: Z = 4 + // 0x10_000_000 + val defaultVmRamSizeInKiBytes: Z = bytesToKiBytes(268435456) @strictpure def brand(s:String):String = s"sb_$s" + @strictpure def safeToEdit: ST = st"// This file will not be overwritten if codegen is rerun" + @strictpure def doNotEdit: ST = st"// Do not edit this file as it will be overwritten if codegen is rerun" + + @strictpure def safeToEditMakefile: ST = st"# This file will not be overwritten if codegen is rerun" + @strictpure def doNotEditMakefile: ST = st"# Do not edit this file as it will be overwritten if codegen is rerun" + @pure def toPreprocessorName(s: String): String = { return ops.StringOps(ops.StringOps(s).replaceAllLiterally(".", "_")).toUpper } diff --git a/shared/src/main/scala/org/sireum/hamr/codegen/microkit/vm/VmMakefileTemplate.scala b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/vm/VmMakefileTemplate.scala new file mode 100644 index 0000000..2edb739 --- /dev/null +++ b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/vm/VmMakefileTemplate.scala @@ -0,0 +1,256 @@ +// #Sireum + +package org.sireum.hamr.codegen.microkit.vm + +import org.sireum._ +import org.sireum.hamr.codegen.microkit.util.Util + +object VmMakefileTemplate { + + @pure def Makefile(threadId: String): ST = { + val ret = + st"""${Util.safeToEditMakefile} + | + |ifeq ($$(strip $$(MICROKIT_SDK)),) + |$$(error MICROKIT_SDK must be specified) + |endif + | + |ifeq ($$(strip $$(MICROKIT_BOARD)),) + |$$(error MICROKIT_BOARD must be specified) + |endif + | + |${threadId}_DIR := $$(shell dirname $$(shell pwd)) + | + |# @ivanv: need to have a step for putting in the initrd node into the DTB, + |# right now it is unfortunately hard-coded. + | + |# @ivanv: check that the path of SDK_PATH/MICROKIT_BOARD exists + |# @ivanv: Have a list of supported boards to check with, if it's not one of those + |# have a helpful message that lists all the support boards. + | + |# @ivanv: incremental builds don't work with LINUX_IMAGE_DIR changing + | + |LIB_VMM_DIR ?= $$(VMM_DIR) + |ifeq ("$$(wildcard $$(LIB_VMM_DIR)/tools)","") + |LIB_VMM_DIR := $${$threadId}/libvmm + |ifeq ("$$(wildcard $$(${threadId}_DIR))","") + |$$(error Set VMM_DIR to point to a copy of https://github.com/au-ts/libvmm") + |endif + |endif + | + |LIB_VMM_TOOLS_DIR := $$(LIB_VMM_DIR)/tools + |LIB_VMM_SRC_DIR := $$(LIB_VMM_DIR)/src + |export SDDF=$$(LIB_VMM_DIR)/dep/sddf + | + |LINUX_IMAGE_DIR := $$(${threadId}_DIR)/board/$$(MICROKIT_BOARD) + |LINUX := $$(LINUX_IMAGE_DIR)/linux + |DTS := $$(LINUX_IMAGE_DIR)/linux.dts + |DTB := $$(TOP_BUILD_DIR)/linux.dtb + |INITRD := $$(LINUX_IMAGE_DIR)/rootfs.cpio.gz + | + |# Toolchain flags + |# FIXME: For optimisation we should consider providing the flag -mcpu. + |# FIXME: We should also consider whether -mgeneral-regs-only should be + |# used to avoid the use of the FPU and therefore seL4 does not have to + |# context switch the FPU. + |# Note we only need -Wno-unused-command-line-argument because in Nix + |# passes an extra `--gcc-toolchain` flag which we do not need. + |CFLAGS := \ + | -mstrict-align \ + | -ffreestanding \ + | -g3 \ + | -O3 \ + | -Wno-unused-command-line-argument \ + | -Wall -Wno-unused-function -Werror \ + | -DMICROKIT_CONFIG_$$(MICROKIT_CONFIG) \ + | -DBOARD_$$(MICROKIT_BOARD) \ + | -I$$(LIB_VMM_DIR)/include \ + | -I$$(MICROKIT_BOARD_DIR)/include \ + | -I$$(SDDF)/include \ + | -MD \ + | -MP \ + | -target $$(TARGET) + | + |LDFLAGS := -L$$(MICROKIT_BOARD_DIR)/lib + |LIBS := --start-group -lmicrokit -Tmicrokit.ld libvmm.a --end-group + | + |CHECK_FLAGS_BOARD_MD5:=.board_cflags-$$(shell echo -- $$(CFLAGS) $$(MICROKIT_BOARD) $$(MICROKIT_CONFIG) | shasum | sed 's/ *-//') + | + |$$(CHECK_FLAGS_BOARD_MD5): + | -rm -f .board_cflags-* + | touch $$@ + | + |${threadId}_INCLUDE = -I$$(${threadId}_DIR)/include + | + |all: $$(TOP_BUILD_DIR)/${threadId}.a + | + |$$(DTB): + |ifeq ("", "$$(shell which $$(DTC))") + | $$(error "Could not find dependency: Device Tree Compiler (dtc)") + |endif + | $$(LIB_VMM_TOOLS_DIR)/dtscat $$(DTS) $$(LINUX_IMAGE_DIR)/overlay.dts > $$(TOP_BUILD_DIR)/linux.dts + | # @ivanv: Shouldn't supress warnings + | $$(DTC) -q -I dts -O dtb $$(TOP_BUILD_DIR)/linux.dts > $$@ + | + |#$$(TOP_BUILD_DIR)/package_guest_images.o: $$(LIB_VMM_TOOLS_DIR)/package_guest_images.S $$(LINUX_IMAGE_DIR) $$(LINUX) $$(INITRD) $$(DTB) + |$$(TOP_BUILD_DIR)/package_guest_images.o: $$(LIB_VMM_TOOLS_DIR)/package_guest_images.S $$(LINUX_IMAGE_DIR) $$(DTB) + | $$(CC) -c -g3 -x assembler-with-cpp \ + | -DGUEST_KERNEL_IMAGE_PATH=\"$$(LINUX)\" \ + | -DGUEST_DTB_IMAGE_PATH=\"$$(DTB)\" \ + | -DGUEST_INITRD_IMAGE_PATH=\"$$(INITRD)\" \ + | -target $$(TARGET) \ + | $$< \ + | -o $$@ + | + |# NOTE: the type libraries will be linked in via the top level makefile so here + |# we just need to include $$(TOP_TYPES_INCLUDE) + |$$(TOP_BUILD_DIR)/%.o: $$(${threadId}_DIR)/src/%.c $$(TOP_BUILD_DIR)/Makefile + | $$(CC) -c $$(CFLAGS) $$< -o $$@ $$(TOP_TYPES_INCLUDE) $$(${threadId}_INCLUDE) + | + |-include vmm.d + |include $$(LIB_VMM_DIR)/vmm.mk + |vpath %.c $$(LIB_VMM_DIR) + | + |$$(TOP_BUILD_DIR)/${threadId}.a: libvmm.a $$(TOP_BUILD_DIR)/${threadId}.o $$(TOP_BUILD_DIR)/${threadId}_user.o $$(TOP_BUILD_DIR)/package_guest_images.o Makefile + | $$(AR) r libvmm.a $$(TOP_BUILD_DIR)/${threadId}.o $$(TOP_BUILD_DIR)/${threadId}_user.o $$(TOP_BUILD_DIR)/package_guest_images.o + | cp libvmm.a $$@ + | + |clean:: + | rm -rf $$(TOP_BUILD_DIR) + |""" + return ret + } + + /* + @pure def oldMakefile(): ST = { + val ret = + st"""# Copyright 2021, Breakaway Consulting Pty. Ltd. + |# Copyright 2022, UNSW (ABN 57 195 873 179) + |# Copyright 2024, DornerWorks + |# + |# SPDX-License-Identifier: BSD-2-Clause + |# + | + |ifeq ($$(strip $$(MICROKIT_SDK)),) + |$$(error MICROKIT_SDK must be specified) + |endif + | + |ifeq ($$(strip $$(MICROKIT_BOARD)),) + |$$(error MICROKIT_BOARD must be specified) + |endif + | + |# All dependencies needed to compile the VMM + |DTC := dtc + |CC := clang + |LD := ld.lld + |AR := llvm-ar + |MICROKIT_TOOL ?= $$(MICROKIT_SDK)/bin/microkit + | + |BUILD_DIR := ../../../build + |CONFIG ?= debug + | + |# @ivanv: need to have a step for putting in the initrd node into the DTB, + |# right now it is unfortunately hard-coded. + | + |# @ivanv: check that the path of SDK_PATH/MICROKIT_BOARD exists + |# @ivanv: Have a list of supported boards to check with, if it's not one of those + |# have a helpful message that lists all the support boards. + | + |# @ivanv: incremental builds don't work with IMAGE_DIR changing + | + |MICROKIT_BOARD_DIR := $$(MICROKIT_SDK)/board/$$(MICROKIT_BOARD)/$$(CONFIG) + |VMM := deps/libvmm + |VMM_TOOLS := $$(VMM)/tools + |VMM_SRC_DIR := $$(VMM)/src + | + |IMAGE_DIR := board/$$(MICROKIT_BOARD) + |LINUX := $$(IMAGE_DIR)/linux + |DTS := $$(IMAGE_DIR)/linux.dts + |DTB := $$(BUILD_DIR)/linux.dtb + |INITRD := $$(IMAGE_DIR)/rootfs.cpio.gz + | + |IMAGE_URL := https://github.com/dornerworks/meta-inspecta-sut/releases/download + |IMAGE_VER := v0.1.0-baseline + | + |# @ivanv: should only compile printf.o in debug + |# VMM_OBJS := vmm.o printf.o virq.o linux.o guest.o psci.o smc.o fault.o util.o vgic.o vgic_v2.o package_guest_images.o tcb.o vcpu.o + |VMM_OBJS := vmm.o virq.o linux.o guest.o psci.o smc.o fault.o vmm_util.o vgic.o vgic_v2.o package_guest_images.o tcb.o vcpu.o mmio.o + | + |# Toolchain flags + |# FIXME: For optimisation we should consider providing the flag -mcpu. + |# FIXME: We should also consider whether -mgeneral-regs-only should be + |# used to avoid the use of the FPU and therefore seL4 does not have to + |# context switch the FPU. + |# Note we only need -Wno-unused-command-line-argument because in Nix + |# passes an extra `--gcc-toolchain` flag which we do not need. + |CFLAGS := -mstrict-align \ + | -g3 \ + | -O3 \ + | -ffreestanding \ + | -nostdlib \ + | -Wno-unused-command-line-argument \ + | -Wall -Wno-unused-function -Werror \ + | -I$$(VMM)/include \ + | -I$$(VMM_SRC_DIR) \ + | -I$$(MICROKIT_BOARD_DIR)/include \ + | -DMICROKIT_BOARD_$$(MICROKIT_BOARD) \ + | -DCONFIG_$$(CONFIG) \ + | -target aarch64-none-elf + | + |LDFLAGS := -L$$(MICROKIT_BOARD_DIR)/lib + |LIBS := -lmicrokit -Tmicrokit.ld + | + |# all: directories $$(BUILD_DIR)/vmm.elf + |all: directories $$(addprefix $$(BUILD_DIR)/, $$(VMM_OBJS)) + | + |directories: + | $$(shell mkdir -p $$(BUILD_DIR)) + | + |$$(DTB): $$(DTS) + |ifeq ("", "$$(shell which $$(DTC))") + | $$(error "Could not find dependency: Device Tree Compiler (dtc)") + |endif + | # @ivanv: Shouldn't supress warnings + | $$(DTC) -q -i $$(IMAGE_DIR) -I dts -O dtb $$< > $$@ + | + | + |#$$(BUILD_DIR)/package_guest_images.o: $$(VMM_TOOLS)/package_guest_images.S $$(IMAGE_DIR) $$(LINUX) $$(INITRD) $$(DTB) + |$$(BUILD_DIR)/package_guest_images.o: $$(VMM_TOOLS)/package_guest_images.S $$(IMAGE_DIR) $$(DTB) + | $$(CC) -c -g3 -x assembler-with-cpp \ + | -DGUEST_KERNEL_IMAGE_PATH=\"$$(LINUX)\" \ + | -DGUEST_DTB_IMAGE_PATH=\"$$(DTB)\" \ + | -DGUEST_INITRD_IMAGE_PATH=\"$$(INITRD)\" \ + | -target aarch64-none-elf \ + | $$< -o $$@ + | + |$$(BUILD_DIR)/%.o: %.c Makefile + | $$(CC) -c $$(CFLAGS) $$< -o $$@ + | + |$$(BUILD_DIR)/%.o: virtio/%.c Makefile + | $$(CC) -c $$(CFLAGS) $$< -o $$@ + | + |$$(BUILD_DIR)/%.o: $$(VMM_SRC_DIR)/%.c Makefile + | $$(CC) -c $$(CFLAGS) $$< -o $$@ + | + |$$(BUILD_DIR)/vmm_util.o: $$(VMM_SRC_DIR)/util/util.c Makefile + | $$(CC) -c $$(CFLAGS) $$< -o $$(BUILD_DIR)/vmm_util.o + | + |$$(BUILD_DIR)/mmio.o: $$(VMM_SRC_DIR)/virtio/mmio.c Makefile + | $$(CC) -c $$(CFLAGS) $$< -o $$@ + | + |$$(BUILD_DIR)/%.o: $$(VMM_SRC_DIR)/arch/aarch64/%.c Makefile + | $$(CC) -c $$(CFLAGS) $$< -o $$@ + | + |$$(BUILD_DIR)/%.o: $$(VMM_SRC_DIR)/arch/aarch64/vgic/%.c Makefile + | $$(CC) -c $$(CFLAGS) $$< -o $$@ + | + |# $$(BUILD_DIR)/vmm.elf: $$(addprefix $$(BUILD_DIR)/, $$(VMM_OBJS)) + |# $$(LD) $$(LDFLAGS) $$^ $$(LIBS) -o $$@ + | + |clean: + | rm -rf $$(BUILD_DIR) + |""" + + return ret + }*/ +} diff --git a/shared/src/main/scala/org/sireum/hamr/codegen/microkit/vm/VmUser.scala b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/vm/VmUser.scala new file mode 100644 index 0000000..3a632e2 --- /dev/null +++ b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/vm/VmUser.scala @@ -0,0 +1,163 @@ +// #Sireum + +package org.sireum.hamr.codegen.microkit.vm + +import org.sireum._ +import org.sireum.hamr.codegen.microkit.util.Util + +object VmUser { + def vmUserCode(componentPath: ST, + guestRamVaddr: ST + ): ST = { + val content: ST = + st""" + | + |#include <$componentPath.h> + |#include <${componentPath}_user.h> + |#include + |#include + |#include + |#include + | + |${Util.safeToEdit} + | + |// Data for the guest's kernel image. + |extern char _guest_kernel_image[]; + |extern char _guest_kernel_image_end[]; + | + |// Data for the device tree to be passed to the kernel. + |extern char _guest_dtb_image[]; + |extern char _guest_dtb_image_end[]; + | + |// Data for the initial RAM disk to be passed to the kernel. + |extern char _guest_initrd_image[]; + |extern char _guest_initrd_image_end[]; + | + |// Microkit will set this variable to the start of the guest RAM memory region. + |$guestRamVaddr; + | + |static int get_dev_irq_by_ch(microkit_channel ch); + |static int get_dev_ch_by_irq(int irq, microkit_channel *ch); + |static void pt_dev_ack(size_t vcpu_id, int irq, void *cookie); + | + |void ${componentPath}_initialize(void) { + | // Initialise the VMM, the VCPU(s), and start the guest + | LOG_VMM("starting \"%s\"\n", microkit_name); + | + | // Place all the binaries in the right locations before starting the guest + | + | size_t kernel_size = _guest_kernel_image_end - _guest_kernel_image; + | size_t dtb_size = _guest_dtb_image_end - _guest_dtb_image; + | size_t initrd_size = _guest_initrd_image_end - _guest_initrd_image; + | + | // https://github.com/au-ts/libvmm/blob/a996382581b9dbb7f067b25f312e87264c7b8ace/include/libvmm/arch/aarch64/linux.h#L37 + | // https://github.com/au-ts/libvmm/blob/a996382581b9dbb7f067b25f312e87264c7b8ace/src/arch/aarch64/linux.c#L11 + | uintptr_t kernel_pc = linux_setup_images(top_impl_Instance_consumer_p_p_consumer_VM_Guest_RAM_vaddr, + | (uintptr_t) _guest_kernel_image, + | kernel_size, + | (uintptr_t) _guest_dtb_image, + | GUEST_DTB_VADDR, + | dtb_size, + | (uintptr_t) _guest_initrd_image, + | GUEST_INIT_RAM_DISK_VADDR, + | initrd_size); + | + | if (!kernel_pc) { + | LOG_VMM_ERR("Failed to initialise guest images\n"); + | return; + | } + | + | // Initialise the virtual GIC driver + | bool success = virq_controller_init(GUEST_VCPU_ID); + | if (!success) { + | LOG_VMM_ERR("Failed to initialise emulated interrupt controller\n"); + | return; + | } + | + | // Register Pass-through device IRQs + | for(int i=0; i < MAX_IRQS; i++) { + | success = virq_register(GUEST_VCPU_ID, mk_irqs[i].irq, &pt_dev_ack, NULL); + | // Just in case there are already interrupts available to handle, we ack them here. + | microkit_irq_ack(mk_irqs[i].channel); + | } + | + | // Finally start the guest / + | // https://github.com/au-ts/libvmm/blob/a996382581b9dbb7f067b25f312e87264c7b8ace/include/libvmm/guest.h#L10 + | // https://github.com/au-ts/libvmm/blob/a996382581b9dbb7f067b25f312e87264c7b8ace/src/guest.c#L11 + | guest_start(GUEST_VCPU_ID, kernel_pc, GUEST_DTB_VADDR, GUEST_INIT_RAM_DISK_VADDR); + | + | LOG_VMM("Guest started, leaving ${componentPath}_initialize"); + |} + | + |void ${componentPath}_timeTriggered(void) { + | // implement me + | printf("%s: ${componentPath}_timeTriggered invoked\n", microkit_name); + |} + | + |void ${componentPath}_notify(microkit_channel ch) { + | switch (ch) { + | case SERIAL_IRQ_CH: { + | bool success = virq_inject(GUEST_VCPU_ID, SERIAL_IRQ); + | if (!success) { + | LOG_VMM_ERR("IRQ %d dropped on vCPU %d\n", SERIAL_IRQ, GUEST_VCPU_ID); + | } + | break; + | } + | default: + | printf("Unexpected channel, ch: 0x%lx\n", ch); + | } + |} + | + |/* + | * The primary purpose of the VMM after initialisation is to act as a fault-handler. + | * Whenever our guest causes an exception, it gets delivered to this entry point for + | * the VMM to handle. + | */ + |seL4_Bool fault(microkit_child child, microkit_msginfo msginfo, microkit_msginfo *reply_msginfo) { + | // https://github.com/au-ts/libvmm/blob/29aceb2acb7611cc5678d6fc235913684af7893e/src/arch/aarch64/fault.c#L436 + | bool success = fault_handle(child, msginfo); + | if (success) { + | // Now that we have handled the fault successfully, we reply to it so + | // that the guest can resume execution. + | *reply_msginfo = microkit_msginfo_new(0, 0); + | return seL4_True; + | } + | + | return seL4_False; + |} + | + |static int get_dev_irq_by_ch(microkit_channel ch) { + | for(int i=0; i < MAX_IRQS; i++) { + | if (mk_irqs[i].channel == ch) { + | return mk_irqs[i].irq; + | } + | } + | + | return -1; + |} + | + |static int get_dev_ch_by_irq(int irq, microkit_channel *ch) { + | for(int i=0; i < MAX_IRQS; i++) { + | if (mk_irqs[i].irq == irq) { + | *ch = mk_irqs[i].channel; + | return 0; + | } + | } + | + | return -1; + |} + | + |static void pt_dev_ack(size_t vcpu_id, int irq, void *cookie) { + | // For now we by default simply ack the IRQ, we have not + | // come across a case yet where more than this needs to be done. + | microkit_channel ch = 0; + | int status = get_dev_ch_by_irq(irq, &ch); + | if (!status) { + | microkit_irq_ack(ch); + | } + |} + |""" + return content + } + +} diff --git a/shared/src/main/scala/org/sireum/hamr/codegen/microkit/vm/VmUtil.scala b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/vm/VmUtil.scala new file mode 100644 index 0000000..fe1cd0d --- /dev/null +++ b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/vm/VmUtil.scala @@ -0,0 +1,185 @@ +// #Sireum +package org.sireum.hamr.codegen.microkit.vm + +import org.sireum._ +import org.sireum.hamr.codegen.microkit.util.Util + +object VmUtil { + + @pure def vmm_c(guestRamVaddr: String, + initMethodName: String, + computeMethodName: String): ST = { + + val content = st"""#include + |#include + |#include + |#include + |#include + |#include + |#include + |#include + |#include + |#include + |#include + |#include + |#include "vmm_config.h" + | + |/* Data for the guest's kernel image. */ + |extern char _guest_kernel_image[]; + |extern char _guest_kernel_image_end[]; + | + |/* Data for the device tree to be passed to the kernel. */ + |extern char _guest_dtb_image[]; + |extern char _guest_dtb_image_end[]; + | + |/* Data for the initial RAM disk to be passed to the kernel. */ + |extern char _guest_initrd_image[]; + |extern char _guest_initrd_image_end[]; + | + |/* Microkit will set this variable to the start of the guest RAM memory region. */ + |uintptr_t $guestRamVaddr; + | + |static int get_dev_irq_by_ch(microkit_channel ch) { + | for(int i=0; i + | + |${Util.safeToEdit} + | + |#if defined(BOARD_qemu_virt_aarch64) + |#define GUEST_DTB_VADDR $guestDtbVaddrInHex + |#define GUEST_INIT_RAM_DISK_VADDR $guestInitRamDiskVaddrInHex + |#else + |#error Need to define guest kernel image address and DTB address + |#endif + | + |#define MAX_IRQS $maxIrqs + | + |#if defined(BOARD_qemu_virt_aarch64) + |#define SERIAL_IRQ_CH 1 + |#define SERIAL_IRQ 33 + |#else + |#error Need to define IRQs + |#endif + | + |struct mk_irq { + | int irq; + | microkit_channel channel; + |}; + | + |struct mk_irq mk_irqs[MAX_IRQS] = { + | { // Serial + | .irq = SERIAL_IRQ, + | .channel = SERIAL_IRQ_CH + | } + |}; + |""" + return ret + } +}