vm tweak

sireum · Dec 16, 2024 · e2c01bf · e2c01bf
1 parent 868e405
commit e2c01bf
Show file tree

Hide file tree

Showing 7 changed files with 21 additions and 17 deletions.
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
@@ -136,6 +136,7 @@ object MicrokitCodegen {
       val content =
         st"""#pragma once
             |
+            |#include <stdbool.h>
             |#include <stdint.h>
             |
             |${Util.doNotEdit}
@@ -618,7 +619,7 @@ object MicrokitCodegen {
 
         userMethodDefaultImpls =
           st"""void $initializeMethodName(void) {
-              |  // implement me
+              |  printf("%s: $initializeMethodName invoked\n", microkit_name);
               |}""" +: userMethodDefaultImpls
 
         if (t.isPeriodic()) {
@@ -627,7 +628,7 @@ object MicrokitCodegen {
           computeContributions = computeContributions :+ st"${timeTriggeredMethodName}();"
           userMethodDefaultImpls = userMethodDefaultImpls :+
             st"""void $timeTriggeredMethodName(void) {
-                |  // implement me
+                |  printf("%s: $timeTriggeredMethodName invoked\n", microkit_name);
                 |}"""
         }
 

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
@@ -273,7 +273,7 @@ object QueueTemplate {
   def getClientSporadicDefaultImplContributions(portName: String): ST = {
     return (
       st"""void handle_$portName(void) {
-          |  // implement me
+          |  printf("%s: handel_$portName invoked\n", microkit_name);
           |}""")
   }
 
@@ -318,7 +318,16 @@ object QueueTemplate {
           |
           |#include <${TypeUtil.eventCounterFilename}>
           |#include <${TypeUtil.aadlTypesFilename}>
+          |
           |#include <stdbool.h>
+          |#include <stddef.h>
+          |#include <stdint.h>
+          |
+          |#if __has_include("util.h")
+          |#include <util.h>
+          |#elif __has_include("libvmm/util.util.h")
+          |#include <libvmm/util/util.h>
+          |#endif
           |
           |// 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
@@ -480,14 +489,6 @@ object QueueTemplate {
           | */
           |
           |#include <${queueHeaderFilename}>
-          |#include <stdint.h>
-          |#include <stddef.h>
-          |
-          |#if __has_include("util.h")
-          |#include <util.h>
-          |#elif __has_include("libvmm/util.util.h")
-          |#include <libvmm/util/util.h>
-          |#endif
           |
           |//------------------------------------------------------------------------------
           |// Sender API

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
@@ -62,6 +62,9 @@ object MakefileTemplate {
                            typeObjectNames: ISZ[String],
                            buildEntries: ISZ[ST],
                            elfEntries: ISZ[ST]): ST = {
+
+    val uniqueBuildEntries: ISZ[String] = (Set.empty[String] ++ (for(be <- buildEntries) yield be.render)).elements
+
     val content =
       st"""${Util.doNotEditMakefile}
           |
@@ -118,7 +121,7 @@ object MakefileTemplate {
           |%.o: $${TOP_DIR}/util/src/%.c Makefile
           |${TAB}$$(CC) -c $$(CFLAGS) $$< -o $$@ -I$$(TOP_DIR)/util/include
           |
-          |${(buildEntries, "\n\n")}
+          |${(uniqueBuildEntries, "\n\n")}
           |
           |${(elfEntries, "\n\n")}
           |

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
@@ -115,7 +115,7 @@ import org.sireum.hamr.codegen.microkit.util.Util.{KiBytesToHex}
                                   val children: ISZ[MicrokitDomain]) extends MicrokitDomain {
   @pure def prettyST: ST = {
     val domain: Option[ST] =
-      if (schedulingDomain.nonEmpty) Some(st""" domain="${schedulingDomain.get}"""")
+      if (schedulingDomain.nonEmpty) Some(st""" domain="domain_${schedulingDomain.get}"""")
       else None()
     val stId: Option[ST] =
       if (id.nonEmpty) Some(st""" id="${id.get}"""")

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
@@ -32,8 +32,8 @@ object VmMakefileTemplate {
           |
           |LIB_VMM_DIR ?= $$(VMM_DIR)
           |ifeq ("$$(wildcard $$(LIB_VMM_DIR)/tools)","")
-          |LIB_VMM_DIR := $${$threadId}/libvmm
-          |ifeq ("$$(wildcard $$(${threadId}_DIR))","")
+          |LIB_VMM_DIR := $$(${threadId}_DIR)/libvmm
+          |ifeq ("$$(wildcard $$(LIB_VMM_DIR)/tools)","")
           |$$(error Set VMM_DIR to point to a copy of https://github.com/au-ts/libvmm")
           |endif
           |endif

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
@@ -90,7 +90,6 @@ object VmUser {
           |}
           |
           |void ${componentPath}_timeTriggered(void) {
-          |  // implement me
           |  printf("%s: ${componentPath}_timeTriggered invoked\n", microkit_name);
           |}
           |

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
@@ -114,7 +114,7 @@ object VmUtil {
                       |}
                       |
                       |void $computeMethodName(void) {
-                      |  // implement me
+                      |  printf("%s: $computeMethodName invoked\n", microkit_name);
                       |}
                       |
                       |/*
-Original file line number
+Diff line change
@@ Expand Up / @@ -90,7 +90,6 @@ object VmUser { @@
               |}
               |
               |void ${componentPath}_timeTriggered(void) {
-              |  // implement me
               |  printf("%s: ${componentPath}_timeTriggered invoked\n", microkit_name);
               |}
               |
@@ Expand Down @@