microkit: handle unconnected ports

sireum · Jan 7, 2025 · 1d5f100 · 1d5f100
1 parent dd4efd0
commit 1d5f100
Show file tree

Hide file tree

Showing 6 changed files with 323 additions and 199 deletions.
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
@@ -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
@@ -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
@@ -30,15 +30,15 @@ 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
 
 @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,15 +65,15 @@ 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
 
 @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