Check that commands, events, parameters, and telemetry fit in framework buffers

compiler/lib/src/main/scala/analysis/CheckSemantics/CheckComponentDefs.scala

@@ -18,6 +18,7 @@ object CheckComponentDefs
     for {
       a <- super.defComponentAnnotatedNode(a1, aNode)
       c <- a.component.get.complete
+      _ <- CheckFrameworkBufferSizes.component(a, c)
     }
     yield {
       val symbol = Symbol.Component(aNode)

compiler/lib/src/main/scala/analysis/CheckSemantics/CheckFrameworkBufferSizes.scala

@@ -0,0 +1,148 @@
+package fpp.compiler.analysis
+
+import fpp.compiler.ast._
+import fpp.compiler.util._
+
+/** Check that the commands, events, telemetry channels, and parameters
+ *  of a component fit in the F Prime framework buffers that carry them */
+object CheckFrameworkBufferSizes {
+
+  /** A framework buffer, given by the framework constant that specifies
+   *  its size */
+  case class Buffer(sizeName: String)
+
+  /** The buffer that carries the arguments of a command */
+  val cmdArgBuffer = Buffer("FW_CMD_ARG_BUFFER_MAX_SIZE")
+
+  /** The buffer that carries the arguments of an event */
+  val logBuffer = Buffer("FW_LOG_BUFFER_MAX_SIZE")
+
+  /** The buffer that carries the value of a parameter */
+  val paramBuffer = Buffer("FW_PARAM_BUFFER_MAX_SIZE")
+
+  /** The buffer that carries the value of a telemetry channel */
+  val tlmBuffer = Buffer("FW_TLM_BUFFER_MAX_SIZE")
+
+  /** Check a component */
+  def component(a: Analysis, c: Component): Result.Result[Unit] =
+    for {
+      _ <- Result.foldLeft (sortById(c.commandMap)) (()) ((_, command) =>
+        command match {
+          case command: Command.NonParam =>
+            val data = command.aNode._2.data
+            checkSize(
+              a,
+              command.getLoc,
+              s"arguments of command ${command.getName}",
+              data.params.map(aNode => a.typeMap(aNode._2.data.typeName.id)),
+              cmdArgBuffer
+            )
+          case _: Command.Param => Right(())
+        }
+      )
+      _ <- Result.foldLeft (sortById(c.eventMap)) (()) ((_, event) =>
+        checkSize(
+          a,
+          event.getLoc,
+          s"arguments of event ${event.getName}",
+          event.aNode._2.data.params.map(
+            aNode => a.typeMap(aNode._2.data.typeName.id)
+          ),
+          logBuffer
+        )
+      )
+      _ <- Result.foldLeft (sortById(c.tlmChannelMap)) (()) ((_, channel) =>
+        checkSize(
+          a,
+          channel.getLoc,
+          s"value of telemetry channel ${channel.getName}",
+          List(channel.channelType),
+          tlmBuffer
+        )
+      )
+      _ <- Result.foldLeft (sortById(c.paramMap)) (()) ((_, param) =>
+        checkSize(
+          a,
+          param.getLoc,
+          s"value of parameter ${param.getName}",
+          List(param.paramType),
+          paramBuffer
+        )
+      )
+    } yield ()
+
+  /** Check that values of the types ts, serialized in sequence,
+   *  can fit in a framework buffer. If the buffer size constant is not
+   *  defined, there is nothing to check. The check uses the minimum
+   *  serialized size, in which every string is empty: it reports an
+   *  error only when no value of the types can fit in the buffer. */
+  private def checkSize(
+    a: Analysis,
+    loc: Location,
+    msg: String,
+    ts: List[Type],
+    buffer: Buffer
+  ): Result.Result[Unit] =
+    getFrameworkConstant(a, buffer.sizeName) match {
+      case None => Right(())
+      case Some((bufferSymbol, bufferSize)) =>
+        val sizeOpt = ts.foldLeft (Some(BigInt(0)): Option[BigInt]) ((sizeOpt, t) =>
+          for {
+            s1 <- sizeOpt
+            s2 <- getMinSerializedSize(a, t)
+          } yield s1 + s2
+        )
+        sizeOpt match {
+          case Some(size) if size > bufferSize =>
+            Left(
+              SemanticError.SerializedSizeTooLarge(
+                loc,
+                msg,
+                size,
+                buffer.sizeName,
+                bufferSize,
+                Locations.get(bufferSymbol.getNodeId)
+              )
+            )
+          case _ => Right(())
+        }
+    }
+
+  /** Get the minimum serialized size of a value of type t.
+   *  A string value is serialized as its length followed by its
+   *  characters, so its minimum size is the size of its length. */
+  private def getMinSerializedSize(a: Analysis, t: Type): Option[BigInt] =
+    t.getUnderlyingType match {
+      case _: Type.String => Some(getStringLengthSize(a))
+      case t: Type.Array =>
+        val n = BigInt(t.getArraySize.get)
+        getMinSerializedSize(a, t.anonArray.eltType).map(n * _)
+      case t: Type.Struct =>
+        t.anonStruct.members.foldLeft (Some(BigInt(0)): Option[BigInt]) {
+          case (sizeOpt, (m, t1)) =>
+            for {
+              s1 <- sizeOpt
+              s2 <- getMinSerializedSize(a, t1)
+            } yield s1 + s2 * t.sizes.getOrElse(m, 1)
+        }
+      case t => Type.SerializedSize.ty(a, t)
+    }
+
+  /** Get the serialized size of the length of a string */
+  private def getStringLengthSize(a: Analysis): BigInt = {
+    val symbol = a.frameworkDefinitions.typeMap("FwSizeStoreType")
+    Type.SerializedSize.ty(a, a.typeMap(symbol.getNodeId)).get
+  }
+
+  /** Get a framework constant and its value, if it is defined */
+  private def getFrameworkConstant(a: Analysis, name: String):
+    Option[(Symbol.Constant, BigInt)] =
+    a.frameworkDefinitions.constantMap.get(name).map(
+      symbol => (symbol, a.getBigIntValue(symbol.getNodeId))
+    )
+
+  /** Get the values of a map in order of their identifiers */
+  private def sortById[T](map: Map[BigInt, T]): List[T] =
+    map.toList.sortBy(_._1).map(_._2)
+
+}

compiler/lib/src/main/scala/analysis/ComputeDependencies/AddDependencies.scala

@@ -52,6 +52,42 @@ object AddDependencies
     } yield a
   }
 
+  override def specCommandAnnotatedNode(
+    a: Analysis,
+    node: Ast.Annotated[AstNode[Ast.SpecCommand]]
+  ) =
+    for {
+      a <- super.specCommandAnnotatedNode(a, node)
+      a <- frameworkBufferUses(a, CheckFrameworkBufferSizes.cmdArgBuffer)
+    } yield a
+
+  override def specEventAnnotatedNode(
+    a: Analysis,
+    node: Ast.Annotated[AstNode[Ast.SpecEvent]]
+  ) =
+    for {
+      a <- super.specEventAnnotatedNode(a, node)
+      a <- frameworkBufferUses(a, CheckFrameworkBufferSizes.logBuffer)
+    } yield a
+
+  override def specParamAnnotatedNode(
+    a: Analysis,
+    node: Ast.Annotated[AstNode[Ast.SpecParam]]
+  ) =
+    for {
+      a <- super.specParamAnnotatedNode(a, node)
+      a <- frameworkBufferUses(a, CheckFrameworkBufferSizes.paramBuffer)
+    } yield a
+
+  override def specTlmChannelAnnotatedNode(
+    a: Analysis,
+    node: Ast.Annotated[AstNode[Ast.SpecTlmChannel]]
+  ) =
+    for {
+      a <- super.specTlmChannelAnnotatedNode(a, node)
+      a <- frameworkBufferUses(a, CheckFrameworkBufferSizes.tlmBuffer)
+    } yield a
+
   override def stateMachineUse(a: Analysis, node: AstNode[Ast.QualIdent], use: Name.Qualified) =
     analyzeUse(a, Ast.SpecLoc.StateMachine, use, node.data.isAbsolute)
 
@@ -142,6 +178,20 @@ object AddDependencies
       isAbsolute
     ).map(addDependencies (a)).getOrElse(Right(a))
 
+  /** Add a dependency for the framework constant that specifies the size
+   *  of a framework buffer. The constant is optional: if it has no
+   *  location specifier, then there is no dependency. */
+  private def frameworkBufferUses(
+    a: Analysis,
+    buffer: CheckFrameworkBufferSizes.Buffer
+  ): Result =
+    analyzeUse(
+      a,
+      Ast.SpecLoc.Constant,
+      Name.Qualified.fromIdentList(List(buffer.sizeName)),
+      true
+    )
+
   private def addDependenciesForFile(a: Analysis, file: File): Result =
     val scopeNameList = a.scopeNameList
     val result = for {

compiler/lib/src/main/scala/util/Error.scala

@@ -339,6 +339,12 @@ sealed trait Error {
         Error.print (Some(loc)) (s"redefinition of symbol ${name}")
         System.err.println("previous definition is here:")
         System.err.println(prevLoc)
+      case SemanticError.SerializedSizeTooLarge(loc, msg, size, constName, constSize, constLoc) =>
+        Error.print (Some(loc)) (
+          s"$msg: at least $size bytes are required, but $constName is $constSize bytes"
+        )
+        System.err.println(s"$constName is defined here:")
+        System.err.println(constLoc)
       case SemanticError.StateMachine.CallSiteTypeMismatch(
         loc,
         teKind,
@@ -839,6 +845,15 @@ object SemanticError {
     loc: Location,
     prevLoc: Location
   ) extends Error
+  /** Serialized size too large for a framework buffer */
+  final case class SerializedSizeTooLarge(
+    loc: Location,
+    msg: String,
+    size: BigInt,
+    constName: String,
+    constSize: BigInt,
+    constLoc: Location
+  ) extends Error
   /** State machine semantic errors */
   object StateMachine {
     /** Call site type mismatch */

compiler/tools/fpp-check/test/command/buffer_size_ok.fpp

@@ -0,0 +1,22 @@
+type FwSizeStoreType = U16
+
+constant FW_CMD_ARG_BUFFER_MAX_SIZE = 6
+
+module Fw {
+
+  port Cmd
+  port CmdReg
+  port CmdResponse
+
+}
+
+passive component C {
+
+  command recv port cmdIn
+  command reg port cmdRegOut
+  command resp port cmdResponseOut
+
+  @ 4 bytes for x, plus at least 2 bytes for s
+  sync command C(x: U32, s: string size 100)
+
+}

compiler/tools/fpp-check/test/command/buffer_size_too_large.fpp

@@ -0,0 +1,21 @@
+constant FW_CMD_ARG_BUFFER_MAX_SIZE = 8
+
+module Fw {
+
+  port Cmd
+  port CmdReg
+  port CmdResponse
+
+}
+
+array A = [3] U32
+
+passive component C {
+
+  command recv port cmdIn
+  command reg port cmdRegOut
+  command resp port cmdResponseOut
+
+  sync command C(a: A)
+
+}

compiler/tools/fpp-check/test/command/buffer_size_too_large.ref.txt

@@ -0,0 +1,9 @@
+fpp-check
+[ local path prefix ]/compiler/tools/fpp-check/test/command/buffer_size_too_large.fpp:19.3
+  sync command C(a: A)
+  ^
+error: arguments of command C: at least 12 bytes are required, but FW_CMD_ARG_BUFFER_MAX_SIZE is 8 bytes
+FW_CMD_ARG_BUFFER_MAX_SIZE is defined here:
+[ local path prefix ]/compiler/tools/fpp-check/test/command/buffer_size_too_large.fpp:1.1
+constant FW_CMD_ARG_BUFFER_MAX_SIZE = 8
+^

compiler/tools/fpp-check/test/command/tests.sh

@@ -2,6 +2,8 @@ tests="
 async_passive
 bad_opcode
 bad_priority
+buffer_size_ok
+buffer_size_too_large
 duplicate_name
 duplicate_name_param_save
 duplicate_name_param_set

compiler/tools/fpp-check/test/event/buffer_size_ok.fpp

@@ -0,0 +1,24 @@
+type FwSizeStoreType = U16
+
+constant FW_LOG_BUFFER_MAX_SIZE = 6
+
+module Fw {
+
+  port Log
+  port LogText
+  port Time
+
+}
+
+passive component C {
+
+  event port eventOut
+  text event port textEventOut
+  time get port timeGetOut
+
+  @ 4 bytes for x, plus at least 2 bytes for s
+  event E(x: U32, s: string size 100) \
+    severity activity low \
+    format "{} {}"
+
+}

compiler/tools/fpp-check/test/event/buffer_size_string_in_struct.fpp

@@ -0,0 +1,26 @@
+type FwSizeStoreType = U16
+
+constant FW_LOG_BUFFER_MAX_SIZE = 9
+
+module Fw {
+
+  port Log
+  port LogText
+  port Time
+
+}
+
+@ At least 2 bytes for s, plus 8 bytes for x
+struct S { s: string size 100, x: U64 }
+
+passive component C {
+
+  event port eventOut
+  text event port textEventOut
+  time get port timeGetOut
+
+  event E(s: S) \
+    severity activity low \
+    format "{}"
+
+}

compiler/tools/fpp-check/test/event/buffer_size_string_in_struct.ref.txt

@@ -0,0 +1,9 @@
+fpp-check
+[ local path prefix ]/compiler/tools/fpp-check/test/event/buffer_size_string_in_struct.fpp:22.3
+  event E(s: S) \
+  ^
+error: arguments of event E: at least 10 bytes are required, but FW_LOG_BUFFER_MAX_SIZE is 9 bytes
+FW_LOG_BUFFER_MAX_SIZE is defined here:
+[ local path prefix ]/compiler/tools/fpp-check/test/event/buffer_size_string_in_struct.fpp:3.1
+constant FW_LOG_BUFFER_MAX_SIZE = 9
+^

compiler/tools/fpp-check/test/event/buffer_size_too_large.fpp

@@ -0,0 +1,21 @@
+constant FW_LOG_BUFFER_MAX_SIZE = 8
+
+module Fw {
+
+  port Log
+  port LogText
+  port Time
+
+}
+
+passive component C {
+
+  event port eventOut
+  text event port textEventOut
+  time get port timeGetOut
+
+  event E(x: U32, y: U64) \
+    severity activity low \
+    format "{} {}"
+
+}