From 1d5f100f382c41b528a6847c5d190d712e430d96 Mon Sep 17 00:00:00 2001 From: Jason Belt Date: Tue, 7 Jan 2025 17:26:09 -0600 Subject: [PATCH] microkit: handle unconnected ports --- .../hamr/codegen/arsit/nix/NixGen.scala | 6 +- .../common/resolvers/GclResolver.scala | 2 +- .../hamr/codegen/common/types/AadlType.scala | 12 +- .../codegen/microkit/MicrokitCodegen.scala | 257 +++++------------- .../connections/ConnectionStore.scala | 17 +- .../microkit/connections/ConnectionUtil.scala | 228 ++++++++++++++++ 6 files changed, 323 insertions(+), 199 deletions(-) create mode 100644 shared/src/main/scala/org/sireum/hamr/codegen/microkit/connections/ConnectionUtil.scala diff --git a/jvm/src/main/scala/org/sireum/hamr/codegen/arsit/nix/NixGen.scala b/jvm/src/main/scala/org/sireum/hamr/codegen/arsit/nix/NixGen.scala index 359d014..a64f42e 100644 --- a/jvm/src/main/scala/org/sireum/hamr/codegen/arsit/nix/NixGen.scala +++ b/jvm/src/main/scala/org/sireum/hamr/codegen/arsit/nix/NixGen.scala @@ -100,7 +100,7 @@ object NixGen { for (p <- ports.filter(p => CommonUtil.isDataPort(p.feature))) { val originatingType: AadlType = p._portType match { - case BitType(_, _, _, _, Some(o)) => o + case BitType(_, _, _, Some(o)) => o case _ => halt(s"Unexpected: Could not find originating type for ${p._portType} used by ${p.parentName}.${p.path}") } if (!seenTypes.contains(originatingType)) { @@ -203,7 +203,7 @@ object NixGen { val entry: ST = { if (types.rawConnections) { val originatingTypeNames: TypeNameProvider = p._portType match { - case BitType(_, _, _, _, Some(o)) => o.nameProvider + case BitType(_, _, _, Some(o)) => o.nameProvider case _ => halt(s"Unexpected: Could not find originating type for ${p._portType}") } @@ -662,7 +662,7 @@ object NixGen { val decl: ST = if (types.rawConnections) { val originatingTypeNames: TypeNameProvider = p._portType match { - case BitType(_, _, _, _, Some(o)) => o.nameProvider + case BitType(_, _, _, Some(o)) => o.nameProvider case _ => halt(s"Unexpected: Could not find originating type for ${p._portType}") } diff --git a/shared/src/main/scala/org/sireum/hamr/codegen/common/resolvers/GclResolver.scala b/shared/src/main/scala/org/sireum/hamr/codegen/common/resolvers/GclResolver.scala index d98d051..4698b8e 100644 --- a/shared/src/main/scala/org/sireum/hamr/codegen/common/resolvers/GclResolver.scala +++ b/shared/src/main/scala/org/sireum/hamr/codegen/common/resolvers/GclResolver.scala @@ -1470,7 +1470,7 @@ import org.sireum.hamr.codegen.common.resolvers.GclResolver._ return ta - case TODOType(ISZ("art", "Empty"), _, _, _) => + case TODOType(ISZ("art", "Empty"), _, _) => val adtAst: AST.Stmt.Adt = AST.Stmt.Adt( isRoot = F, diff --git a/shared/src/main/scala/org/sireum/hamr/codegen/common/types/AadlType.scala b/shared/src/main/scala/org/sireum/hamr/codegen/common/types/AadlType.scala index 1e4b61c..416a855 100644 --- a/shared/src/main/scala/org/sireum/hamr/codegen/common/types/AadlType.scala +++ b/shared/src/main/scala/org/sireum/hamr/codegen/common/types/AadlType.scala @@ -30,7 +30,7 @@ import org.sireum.hamr.ir @datatype class EnumType(val classifier: ISZ[String], val nameProvider: TypeNameProvider, - val container: Option[ir.Component], + @hidden val container: Option[ir.Component], val bitSize: Option[Z], val values: ISZ[String]) extends AadlType @@ -38,7 +38,7 @@ import org.sireum.hamr.ir @datatype class ArrayType(val classifier: ISZ[String], val nameProvider: TypeNameProvider, - val container: Option[ir.Component], + @hidden val container: Option[ir.Component], val bitSize: Option[Z], val dimensions: ISZ[Z], @@ -47,7 +47,7 @@ import org.sireum.hamr.ir @datatype class RecordType(val classifier: ISZ[String], val nameProvider: TypeNameProvider, - val container: Option[ir.Component], + @hidden val container: Option[ir.Component], val bitSize: Option[Z], val fields: Map[String, AadlType] @@ -56,7 +56,7 @@ import org.sireum.hamr.ir @datatype class BaseType(val classifier: ISZ[String], val nameProvider: TypeNameProvider, - val container: Option[ir.Component], + @hidden val container: Option[ir.Component], val bitSize: Option[Z], val slangType: SlangType.Type @@ -65,7 +65,7 @@ import org.sireum.hamr.ir @datatype class TODOType(val classifier: ISZ[String], val nameProvider: TypeNameProvider, - val container: Option[ir.Component], + @hidden val container: Option[ir.Component], val bitSize: Option[Z] ) extends AadlType @@ -73,7 +73,7 @@ import org.sireum.hamr.ir @datatype class BitType(val classifier: ISZ[String], val nameProvider: TypeNameProvider, - val container: Option[ir.Component], + @hidden val container: Option[ir.Component], val bitSize: Option[Z], val originatingType: Option[AadlType]) extends AadlType 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 36c76e1..64c6c7b 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 @@ -4,21 +4,18 @@ package org.sireum.hamr.codegen.microkit import org.sireum._ import org.sireum.hamr.codegen.common.containers.FileResource import org.sireum.hamr.codegen.common.plugin.Plugin -import org.sireum.hamr.codegen.common.symbols.{AadlDataPort, AadlEventDataPort, AadlEventPort, AadlFeatureEvent, AadlThread, SymbolTable} +import org.sireum.hamr.codegen.common.symbols.{AadlPort, AadlThread, SymbolTable} import org.sireum.hamr.codegen.common.types.{AadlType, AadlTypes, TypeUtil => CommonTypeUtil} -import org.sireum.hamr.codegen.common.util.{CodeGenResults, ResourceUtil} import org.sireum.hamr.codegen.common.util.HamrCli.CodegenOption +import org.sireum.hamr.codegen.common.util.{CodeGenResults, ResourceUtil} import org.sireum.hamr.codegen.microkit.MicrokitCodegen.{pacerSchedulingDomain, toolName} -import org.sireum.hamr.codegen.microkit.connections.{ConnectionContributions, ConnectionStore, TypeApiContributions} +import org.sireum.hamr.codegen.microkit.connections._ import org.sireum.hamr.codegen.microkit.lint.Linter -import org.sireum.hamr.codegen.microkit.types.{QueueTemplate, TypeStore, TypeUtil} +import org.sireum.hamr.codegen.microkit.types.{DefaultTypeStore, TypeStore, TypeUtil} import org.sireum.hamr.codegen.microkit.util._ +import org.sireum.hamr.codegen.microkit.vm.{VmMakefileTemplate, VmUser, VmUtil} 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" @@ -161,193 +158,85 @@ object MicrokitCodegen { for (srcPort <- srcThread.getPorts() if srcPort.direction == Direction.Out && symbolTable.outConnections.contains(srcPort.path)) { - var srcPutContributions: ISZ[ST] = ISZ() - - var outgoingPortType: Option[AadlType] = None() - - var typeApiContributions: ISZ[TypeApiContributions] = ISZ() var receiverContributions: Map[ISZ[String], ConnectionContributions] = Map.empty - var handledQueues: Set[Z] = Set.empty - for (outConnection <- symbolTable.getOutConnections(srcPort.path)) { symbolTable.componentMap.get(outConnection.dst.component.name).get match { case dstThread: AadlThread => + val dstPort = symbolTable.featureMap.get(outConnection.dst.feature.get.name).get - val dstContributions: DefaultConnectionContributions = { - assert( - (srcPort.isInstanceOf[AadlDataPort] && dstPort.isInstanceOf[AadlDataPort]) || - (srcPort.isInstanceOf[AadlEventPort] && dstPort.isInstanceOf[AadlEventPort]) || - (srcPort.isInstanceOf[AadlEventDataPort] && dstPort.isInstanceOf[AadlEventDataPort]), - s"Connected ports must be of the same type: ${srcPort.path} -> ${dstPort.path}") - - val isDataPort = srcPort.isInstanceOf[AadlDataPort] - val isEventPort = srcPort.isInstanceOf[AadlEventPort] - val isEventDataPort = srcPort.isInstanceOf[AadlEventDataPort] - - val dstQueueSize: Z = if (isDataPort) 1 - else dstPort.asInstanceOf[AadlFeatureEvent].queueSize - - val aadlType: AadlType = (srcPort, dstPort) match { - case (_: AadlEventPort, _: AadlEventPort) => - TypeUtil.eventPortType - case (srcPort: AadlEventDataPort, dstPort: AadlEventDataPort) => - assert(srcPort.aadlType == dstPort.aadlType, s"Currently expecting connected ports to have the same type ${outConnection.name}") - srcPort.aadlType - case (srcPort: AadlDataPort, dstPort: AadlDataPort) => - assert(srcPort.aadlType == dstPort.aadlType, s"Currently expecting connected ports to have the same type ${outConnection.name}") - srcPort.aadlType - case _ => - halt("Infeasible") - } - - val typeName = typeStore.get(aadlType).get - - if (outgoingPortType.isEmpty) { - outgoingPortType = Some(aadlType) - } else { - assert (outgoingPortType.get == aadlType) - } - - if (!handledQueues.contains(dstQueueSize)) { - typeApiContributions = typeApiContributions :+ TypeUtil.getTypeApiContributions(aadlType, typeName, dstQueueSize) - - val sharedMemVarName = QueueTemplate.getClientEnqueueSharedVarName(srcPort.identifier, dstQueueSize) - srcPutContributions = srcPutContributions :+ QueueTemplate.getClientPutEntry( - sharedMemoryVarName = sharedMemVarName, - queueElementTypeName = typeName.typeName, - queueSize = dstQueueSize, - isEventPort = isEventPort) - - handledQueues = handledQueues + dstQueueSize - } - - val sharedMemTypeName = QueueTemplate.getTypeQueueTypeName(typeName.typeName, dstQueueSize) - - val sharedVarName = QueueTemplate.getClientDequeueSharedVarName(dstPort.identifier, dstQueueSize) - val recvQueueTypeName = QueueTemplate.getClientRecvQueueTypeName(typeName.typeName, dstQueueSize) - val recvQueueVarName = QueueTemplate.getClientRecvQueueName(dstPort.identifier) - - var methodApiSigs: ISZ[ST] = ISZ() - var methodApis: ISZ[ST] = ISZ() - if (isEventPort || isEventDataPort) { - methodApiSigs = methodApiSigs :+ - QueueTemplate.getClientIsEmptyMethodSig(dstPort.identifier) :+ - QueueTemplate.getClientGetterMethodPollSig(dstPort.identifier, typeName.typeName, isEventPort) :+ - QueueTemplate.getClientGetterMethodSig(dstPort.identifier, typeName.typeName, isEventPort) - methodApis = methodApis :+ - QueueTemplate.getClientIsEmptyMethod(dstPort.identifier, typeName.typeName, dstQueueSize) :+ - QueueTemplate.getClientGetterMethodPoll(dstPort.identifier, typeName.typeName, dstQueueSize, isEventPort) :+ - QueueTemplate.getClientGetterMethod(dstPort.identifier, typeName.typeName, isEventPort) - } else { - methodApiSigs = methodApiSigs :+ - QueueTemplate.getClientGetterMethodSig(dstPort.identifier, typeName.typeName, F) - methodApis = methodApis :+ - QueueTemplate.getClientDataGetterMethod(dstPort.identifier, typeName.typeName, dstQueueSize, aadlType) - } - - var userMethodSignatures: ISZ[ST] = ISZ() - var userMethodDefaultImpls: ISZ[ST] = ISZ() - var computeContributions: ISZ[ST] = ISZ() - if (!dstThread.toVirtualMachine(symbolTable)) { - if (dstThread.isSporadic()) { - userMethodSignatures = userMethodSignatures :+ QueueTemplate.getClientEventHandlerMethodSig(dstPort.identifier) - - if (isEventPort || isEventDataPort) { - computeContributions = computeContributions :+ QueueTemplate.getClientSporadicComputeContributions(dstPort.identifier) - } - - userMethodDefaultImpls = userMethodDefaultImpls :+ QueueTemplate.getClientSporadicDefaultImplContributions(dstPort.identifier) - } - } - - DefaultConnectionContributions( - portName = dstPort.path, - portPriority = None(), - headerImportContributions = ISZ(), - implementationImportContributions = ISZ(), - userMethodSignatures = userMethodSignatures, - userMethodDefaultImpls = userMethodDefaultImpls, - defineContributions = ISZ(), - globalVarContributions = ISZ( - PortVaddr(s"volatile $sharedMemTypeName", s"*$sharedVarName"), - QueueVaddr(recvQueueTypeName, recvQueueVarName) - ), - apiMethodSigs = methodApiSigs, - apiMethods = methodApis, - initContributions = ISZ(QueueTemplate.getClientRecvInitMethodCall(dstPort.identifier, typeName.typeName, dstQueueSize)), - computeContributions = computeContributions, - sharedMemoryMapping = ISZ( - PortSharedMemoryRegion( - outgoingPortPath = srcPort.path, - queueSize = dstQueueSize, - varAddr = sharedVarName, - perms = ISZ(Perm.READ), - sizeInKiBytes = Util.defaultPageSizeInKiBytes, - physicalAddressInKiBytes = None()) - ) - ) - } - receiverContributions = receiverContributions + dstThread.path ~> dstContributions + + receiverContributions = receiverContributions + dstThread.path ~> + ConnectionUtil.processInPort(dstThread, dstPort.asInstanceOf[AadlPort], + Some(srcPort), Some(outConnection), typeStore, symbolTable) + case x => halt(s"Only handling thread to thread connections currently: $x") } - } + } // end processing out connections for the source port - val sPortType: String = typeStore.get(outgoingPortType.get).get.typeName - val isEventPort = outgoingPortType.get == TypeUtil.eventPortType - - val apiMethodSig = QueueTemplate.getClientPutMethodSig(srcPort.identifier, sPortType, isEventPort) - val apiMethod = QueueTemplate.getClientPutMethod(srcPort.identifier, sPortType, srcPutContributions, isEventPort) - - 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 :+ QueueVaddr(s"volatile $queueType", s"*$varName") - - initContributions = initContributions :+ QueueTemplate.getQueueInitMethod(varName, sPortType, queueSize) - - sharedMemoryMappings = sharedMemoryMappings :+ - PortSharedMemoryRegion( - outgoingPortPath = srcPort.path, - queueSize = queueSize, - varAddr = varName, - perms = ISZ(Perm.READ, Perm.WRITE), - sizeInKiBytes = Util.defaultPageSizeInKiBytes, - physicalAddressInKiBytes = None() - ) - } + val senderContributions = ConnectionUtil.processOutPort(srcPort, receiverContributions, typeStore) + + val typeApiContributions:ISZ[TypeApiContributions] = + (Set.empty ++ (for(rc <- receiverContributions.values) yield + TypeUtil.getTypeApiContributions(rc.aadlType, typeStore.get(rc.aadlType).get, rc.queueSize))).elements ret = ret :+ DefaultConnectionStore( systemContributions = DefaultSystemContributions( - sharedMemoryRegionContributions = sharedMemoryMappings, + sharedMemoryRegionContributions = senderContributions.sharedMemoryMapping, channelContributions = ISZ()), typeApiContributions = typeApiContributions, senderName = srcThread.path, - senderContributions = - DefaultConnectionContributions( - portName = srcPort.path, - portPriority = None(), - headerImportContributions = ISZ(), - implementationImportContributions = ISZ(), - userMethodSignatures = ISZ(), - userMethodDefaultImpls = ISZ(), - defineContributions = ISZ(), - globalVarContributions = sharedMemoryVars, - apiMethodSigs = ISZ(apiMethodSig), - apiMethods = ISZ(apiMethod), - initContributions = initContributions, - computeContributions = ISZ(), - sharedMemoryMapping = sharedMemoryMappings), + senderContributions = Some(senderContributions), receiverContributions = receiverContributions) + } // end processing connections for source port + + // now handle unconnected ports + + for (unconnectedOutPort <- srcThread.getPorts().filter(p => p.direction == Direction.Out).filter(p => !symbolTable.outConnections.contains(p.path))) { + val senderContributions = ConnectionUtil.processOutPort(unconnectedOutPort, Map.empty, typeStore) + val typeApiContributions = + TypeUtil.getTypeApiContributions(senderContributions.aadlType, typeStore.get(senderContributions.aadlType).get, senderContributions.queueSize) + + ret = ret :+ + DefaultConnectionStore( + systemContributions = + DefaultSystemContributions( + sharedMemoryRegionContributions = senderContributions.sharedMemoryMapping, + channelContributions = ISZ()), + typeApiContributions = ISZ(typeApiContributions), + senderName = srcThread.path, + senderContributions = Some(senderContributions), + receiverContributions = Map.empty + ) } - } + + for (unconnectedInPort <- srcThread.getPorts().filter(p => p.direction == Direction.In).filter(p => !symbolTable.inConnections.contains(p.path))) { + val receiverContributions = ConnectionUtil.processInPort( + dstThread = srcThread, dstPort = unconnectedInPort, + srcPort = None(), outConnection = None(), + typeStore = typeStore, symbolTable = symbolTable) + + val typeApiContributions = + TypeUtil.getTypeApiContributions(receiverContributions.aadlType, typeStore.get(receiverContributions.aadlType).get, receiverContributions.queueSize) + + ret = ret :+ + DefaultConnectionStore( + systemContributions = + DefaultSystemContributions( + sharedMemoryRegionContributions = receiverContributions.sharedMemoryMapping, + channelContributions = ISZ()), + typeApiContributions = ISZ(typeApiContributions), + senderName = srcThread.path, + senderContributions = None(), + receiverContributions = Map.empty + srcThread.path ~> receiverContributions) + + } + + } // end processing connections for threads return ret } @@ -377,16 +266,16 @@ object MicrokitCodegen { for (entry <- connectionStore) { - if (entry.senderName == t.path) { - headerImports = headerImports ++ entry.senderContributions.headerImportContributions - userMethodSignatures = userMethodSignatures ++ entry.senderContributions.userMethodSignatures - userMethodDefaultImpls = userMethodDefaultImpls ++ entry.senderContributions.userMethodDefaultImpls - codeApiMethodSigs = codeApiMethodSigs ++ entry.senderContributions.apiMethodSigs - codeApiMethods = codeApiMethods ++ entry.senderContributions.apiMethods - vaddrs = vaddrs ++ entry.senderContributions.globalVarContributions - initContributions = initContributions ++ entry.senderContributions.initContributions - computeContributions = computeContributions ++ entry.senderContributions.computeContributions - sharedMemoryRegions = sharedMemoryRegions ++ entry.senderContributions.sharedMemoryMapping + if (entry.senderName == t.path && entry.senderContributions.nonEmpty) { + headerImports = headerImports ++ entry.senderContributions.get.headerImportContributions + userMethodSignatures = userMethodSignatures ++ entry.senderContributions.get.userMethodSignatures + userMethodDefaultImpls = userMethodDefaultImpls ++ entry.senderContributions.get.userMethodDefaultImpls + codeApiMethodSigs = codeApiMethodSigs ++ entry.senderContributions.get.apiMethodSigs + codeApiMethods = codeApiMethods ++ entry.senderContributions.get.apiMethods + vaddrs = vaddrs ++ entry.senderContributions.get.globalVarContributions + initContributions = initContributions ++ entry.senderContributions.get.initContributions + computeContributions = computeContributions ++ entry.senderContributions.get.computeContributions + sharedMemoryRegions = sharedMemoryRegions ++ entry.senderContributions.get.sharedMemoryMapping } if (entry.receiverContributions.contains(t.path)) { val c = entry.receiverContributions.get(t.path).get 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 a11160b..1fb9466 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 @@ -16,7 +16,7 @@ import org.sireum.hamr.codegen.microkit.util.Util.TAB def senderName: ISZ[String] - def senderContributions: ConnectionContributions + def senderContributions: Option[ConnectionContributions] // component path -> contributions def receiverContributions: Map[ISZ[String], ConnectionContributions] @@ -26,7 +26,7 @@ import org.sireum.hamr.codegen.microkit.util.Util.TAB val systemContributions: SystemContributions, val typeApiContributions: ISZ[TypeApiContributions], val senderName: ISZ[String], - val senderContributions: ConnectionContributions, + val senderContributions: Option[ConnectionContributions], val receiverContributions: Map[ISZ[String], ConnectionContributions]) extends ConnectionStore @sig trait SystemContributions { @@ -69,8 +69,8 @@ import org.sireum.hamr.codegen.microkit.util.Util.TAB @datatype class DefaultTypeApiContributions(val aadlType: AadlType, val simpleFilename: String, - val header: ST, - val implementation: ST) extends TypeApiContributions + @hidden val header: ST, + @hidden val implementation: ST) extends TypeApiContributions @sig trait GlobalVarContribution { def typ: String @@ -116,6 +116,10 @@ import org.sireum.hamr.codegen.microkit.util.Util.TAB def computeContributions: ISZ[ST] def sharedMemoryMapping: ISZ[MemoryRegion] + + def aadlType: AadlType + + def queueSize: Z } @datatype class DefaultConnectionContributions(val portName: ISZ[String], @@ -130,4 +134,7 @@ import org.sireum.hamr.codegen.microkit.util.Util.TAB val apiMethods: ISZ[ST], val initContributions: ISZ[ST], val computeContributions: ISZ[ST], - val sharedMemoryMapping: ISZ[MemoryRegion]) extends ConnectionContributions \ No newline at end of file + val sharedMemoryMapping: ISZ[MemoryRegion], + + val aadlType: AadlType, + val queueSize: Z) extends ConnectionContributions \ No newline at end of file diff --git a/shared/src/main/scala/org/sireum/hamr/codegen/microkit/connections/ConnectionUtil.scala b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/connections/ConnectionUtil.scala new file mode 100644 index 0000000..0b5c896 --- /dev/null +++ b/shared/src/main/scala/org/sireum/hamr/codegen/microkit/connections/ConnectionUtil.scala @@ -0,0 +1,228 @@ +// #Sireum +package org.sireum.hamr.codegen.microkit.connections + +import org.sireum._ +import org.sireum.hamr.codegen.common.symbols.{AadlDataPort, AadlEventDataPort, AadlEventPort, AadlFeatureEvent, AadlPort, AadlThread, SymbolTable} +import org.sireum.hamr.codegen.common.types.AadlType +import org.sireum.hamr.codegen.microkit.types.{QueueTemplate, TypeStore, TypeUtil} +import org.sireum.hamr.codegen.microkit.util._ +import org.sireum.hamr.ir.{ConnectionInstance, Name} + +object ConnectionUtil { + + def getPortType(p: AadlPort): AadlType = { + p match { + case _: AadlEventPort => TypeUtil.eventPortType + case p: AadlEventDataPort => p.aadlType + case p: AadlDataPort => p.aadlType + case _ => halt("Infeasible") + } + } + + def processInPort(dstThread: AadlThread, + dstPort: AadlPort, + srcPort: Option[AadlPort], + outConnection: Option[ConnectionInstance], + typeStore: Map[AadlType, TypeStore], + symbolTable: SymbolTable, + ): DefaultConnectionContributions = { + + val aadlType: AadlType = (dstPort, srcPort) match { + case (p, None()) => getPortType(p) + case (srcPort, Some(dstPort)) => + assert( + (srcPort.isInstanceOf[AadlDataPort] && dstPort.isInstanceOf[AadlDataPort]) || + (srcPort.isInstanceOf[AadlEventPort] && dstPort.isInstanceOf[AadlEventPort]) || + (srcPort.isInstanceOf[AadlEventDataPort] && dstPort.isInstanceOf[AadlEventDataPort]), + s"Connected ports must be of the same type: ${srcPort.path} -> ${dstPort.path}") + + assert(getPortType(srcPort) == getPortType(dstPort), + s"Currently expecting connected ports to have the same type ${outConnection.get.name}") + + getPortType(srcPort) + } + + val isDataPort = dstPort.isInstanceOf[AadlDataPort] + val isEventPort = dstPort.isInstanceOf[AadlEventPort] + val isEventDataPort = dstPort.isInstanceOf[AadlEventDataPort] + + val dstQueueSize: Z = if (isDataPort) 1 + else dstPort.asInstanceOf[AadlFeatureEvent].queueSize + + val typeName = typeStore.get(aadlType).get + + val sharedMemTypeName = QueueTemplate.getTypeQueueTypeName(typeName.typeName, dstQueueSize) + + val sharedVarName = QueueTemplate.getClientDequeueSharedVarName(dstPort.identifier, dstQueueSize) + val recvQueueTypeName = QueueTemplate.getClientRecvQueueTypeName(typeName.typeName, dstQueueSize) + val recvQueueVarName = QueueTemplate.getClientRecvQueueName(dstPort.identifier) + + var methodApiSigs: ISZ[ST] = ISZ() + var methodApis: ISZ[ST] = ISZ() + if (isEventPort || isEventDataPort) { + methodApiSigs = methodApiSigs :+ + QueueTemplate.getClientIsEmptyMethodSig(dstPort.identifier) :+ + QueueTemplate.getClientGetterMethodPollSig(dstPort.identifier, typeName.typeName, isEventPort) :+ + QueueTemplate.getClientGetterMethodSig(dstPort.identifier, typeName.typeName, isEventPort) + methodApis = methodApis :+ + QueueTemplate.getClientIsEmptyMethod(dstPort.identifier, typeName.typeName, dstQueueSize) :+ + QueueTemplate.getClientGetterMethodPoll(dstPort.identifier, typeName.typeName, dstQueueSize, isEventPort) :+ + QueueTemplate.getClientGetterMethod(dstPort.identifier, typeName.typeName, isEventPort) + } else { + methodApiSigs = methodApiSigs :+ + QueueTemplate.getClientGetterMethodSig(dstPort.identifier, typeName.typeName, F) + methodApis = methodApis :+ + QueueTemplate.getClientDataGetterMethod(dstPort.identifier, typeName.typeName, dstQueueSize, aadlType) + } + + var userMethodSignatures: ISZ[ST] = ISZ() + var userMethodDefaultImpls: ISZ[ST] = ISZ() + var computeContributions: ISZ[ST] = ISZ() + if (!dstThread.toVirtualMachine(symbolTable)) { + if (dstThread.isSporadic()) { + userMethodSignatures = userMethodSignatures :+ QueueTemplate.getClientEventHandlerMethodSig(dstPort.identifier) + + if (isEventPort || isEventDataPort) { + computeContributions = computeContributions :+ QueueTemplate.getClientSporadicComputeContributions(dstPort.identifier) + } + + userMethodDefaultImpls = userMethodDefaultImpls :+ QueueTemplate.getClientSporadicDefaultImplContributions(dstPort.identifier) + } + } + + val memoryRegionName: ISZ[String] = if(srcPort.nonEmpty) srcPort.get.path else dstPort.path + + return DefaultConnectionContributions( + portName = dstPort.path, + portPriority = None(), + headerImportContributions = ISZ(), + implementationImportContributions = ISZ(), + userMethodSignatures = userMethodSignatures, + userMethodDefaultImpls = userMethodDefaultImpls, + defineContributions = ISZ(), + globalVarContributions = ISZ( + PortVaddr(s"volatile $sharedMemTypeName", s"*$sharedVarName"), + QueueVaddr(recvQueueTypeName, recvQueueVarName) + ), + apiMethodSigs = methodApiSigs, + apiMethods = methodApis, + initContributions = ISZ(QueueTemplate.getClientRecvInitMethodCall(dstPort.identifier, typeName.typeName, dstQueueSize)), + computeContributions = computeContributions, + sharedMemoryMapping = ISZ( + PortSharedMemoryRegion( + outgoingPortPath = memoryRegionName, + queueSize = dstQueueSize, + varAddr = sharedVarName, + perms = ISZ(Perm.READ), + sizeInKiBytes = Util.defaultPageSizeInKiBytes, + physicalAddressInKiBytes = None()) + ), + aadlType = aadlType, + queueSize = dstQueueSize + ) + } + + def processOutPort(srcPort: AadlPort, + receiverContributions: Map[ISZ[String], ConnectionContributions], + typeStore: Map[AadlType, TypeStore]): DefaultConnectionContributions = { + val isEventPort = srcPort.isInstanceOf[AadlEventPort] + + var sharedMemoryMappings: ISZ[MemoryRegion] = ISZ() + var sharedMemoryVars: ISZ[GlobalVarContribution] = ISZ() + var initContributions: ISZ[ST] = ISZ() + var srcPutContributions: ISZ[ST] = ISZ() + + var uniqueQueueSizes: Set[Z] = Set.empty + + val senderPortType: AadlType = getPortType(srcPort) + + for (receiverContribution <- receiverContributions.values if !uniqueQueueSizes.contains(receiverContribution.queueSize)) { + uniqueQueueSizes = uniqueQueueSizes + receiverContribution.queueSize + + if (receiverContribution.aadlType != senderPortType) { + // TODO change to reporter or ensure linter prevents thsi + halt("Connected ports must have the same type") + } + + val typeName = typeStore.get(receiverContribution.aadlType).get + + val sharedMemVarName = QueueTemplate.getClientEnqueueSharedVarName(srcPort.identifier, receiverContribution.queueSize) + srcPutContributions = srcPutContributions :+ QueueTemplate.getClientPutEntry( + sharedMemoryVarName = sharedMemVarName, + queueElementTypeName = typeName.typeName, + queueSize = receiverContribution.queueSize, + isEventPort = isEventPort) + + val sPortType: String = typeStore.get(receiverContribution.aadlType).get.typeName + val queueType = QueueTemplate.getTypeQueueTypeName(sPortType, receiverContribution.queueSize) + val varName = QueueTemplate.getClientEnqueueSharedVarName(srcPort.identifier, receiverContribution.queueSize) + sharedMemoryVars = sharedMemoryVars :+ QueueVaddr(s"volatile $queueType", s"*$varName") + + initContributions = initContributions :+ QueueTemplate.getQueueInitMethod(varName, sPortType, receiverContribution.queueSize) + + sharedMemoryMappings = sharedMemoryMappings :+ + PortSharedMemoryRegion( + outgoingPortPath = srcPort.path, + queueSize = receiverContribution.queueSize, + varAddr = varName, + perms = ISZ(Perm.READ, Perm.WRITE), + sizeInKiBytes = Util.defaultPageSizeInKiBytes, + physicalAddressInKiBytes = None() + ) + } + + if (receiverContributions.isEmpty) { + val typeName = typeStore.get(senderPortType).get + + val queueSize = 1 + + val sharedMemVarName = QueueTemplate.getClientEnqueueSharedVarName(srcPort.identifier, queueSize) + srcPutContributions = srcPutContributions :+ QueueTemplate.getClientPutEntry( + sharedMemoryVarName = sharedMemVarName, + queueElementTypeName = typeName.typeName, + queueSize = queueSize, + isEventPort = isEventPort) + + val sPortType: String = typeStore.get(senderPortType).get.typeName + val queueType = QueueTemplate.getTypeQueueTypeName(sPortType, queueSize) + val varName = QueueTemplate.getClientEnqueueSharedVarName(srcPort.identifier, queueSize) + sharedMemoryVars = sharedMemoryVars :+ QueueVaddr(s"volatile $queueType", s"*$varName") + + initContributions = initContributions :+ QueueTemplate.getQueueInitMethod(varName, sPortType, queueSize) + + sharedMemoryMappings = sharedMemoryMappings :+ + PortSharedMemoryRegion( + outgoingPortPath = srcPort.path, + queueSize = queueSize, + varAddr = varName, + perms = ISZ(Perm.READ, Perm.WRITE), + sizeInKiBytes = Util.defaultPageSizeInKiBytes, + physicalAddressInKiBytes = None() + ) + } + + val sPortType: String = typeStore.get(senderPortType).get.typeName + val apiMethodSig = QueueTemplate.getClientPutMethodSig(srcPort.identifier, sPortType, isEventPort) + val apiMethod = QueueTemplate.getClientPutMethod(srcPort.identifier, sPortType, srcPutContributions, isEventPort) + + return DefaultConnectionContributions( + portName = srcPort.path, + portPriority = None(), + headerImportContributions = ISZ(), + implementationImportContributions = ISZ(), + userMethodSignatures = ISZ(), + userMethodDefaultImpls = ISZ(), + defineContributions = ISZ(), + globalVarContributions = sharedMemoryVars, + apiMethodSigs = ISZ(apiMethodSig), + apiMethods = ISZ(apiMethod), + initContributions = initContributions, + computeContributions = ISZ(), + sharedMemoryMapping = sharedMemoryMappings, + + aadlType = senderPortType, + queueSize = 1 // outgoing port so queue size not relevant + ) + } + +}