add manual unit tests

open-platform-models/isolate-ethernet-simple/hamr/slang/src/main/component/base/SW/ArduPilot_Impl_seL4_ArduPilot_ArduPilot.scala

@@ -4,10 +4,15 @@ package base.SW
 
 import org.sireum._
 import base._
+import org.sireum.Random.Impl.Xoshiro256
 
 // This file will not be overwritten so is safe to edit
 object ArduPilot_Impl_seL4_ArduPilot_ArduPilot {
 
+  def freshRandomLib: RandomLib = {
+    RandomLib(Random.Gen64Impl(Xoshiro256.create))
+  }
+
   def initialise(api: ArduPilot_Impl_Initialization_Api): Unit = {
     // event data ports so nothing to initialize
   }
@@ -17,6 +22,13 @@ object ArduPilot_Impl_seL4_ArduPilot_ArduPilot {
 
     val apiUsage_EthernetFramesRx: Option[SW.StructuredEthernetMessage_i] = api.get_EthernetFramesRx()
     api.logInfo(s"Received on event data port EthernetFramesRx: ${apiUsage_EthernetFramesRx}")
+
+    val txOut = freshRandomLib.nextSWStructuredEthernetMessage_i()(
+      internetProtocol = InternetProtocol.IPV6,
+      frameProtocol = FrameProtocol.ARP,
+      arpType = ARP_Type.REQUEST)
+
+    api.put_EthernetFramesTx(txOut)
   }
 
   def finalise(api: ArduPilot_Impl_Operational_Api): Unit = { }

open-platform-models/isolate-ethernet-simple/hamr/slang/src/test/bridge/base/SW/Firewall_Impl_seL4_Firewall_Firewall_GumboX_Manual.scala

@@ -0,0 +1,58 @@
+package base.SW
+
+import base.GumboXUtil.GumboXResult
+import base.SW.Firewall_Impl_seL4_Firewall_Firewall_UnitTestConfiguration_Util._
+import base.util.{Container, UnitTestConfigurationBatch}
+import org.sireum.Random.Impl.Xoshiro256
+import org.sireum._
+import base.RandomLib
+
+// This file will not be overwritten so is safe to edit
+
+class Firewall_Impl_seL4_Firewall_Firewall_GumboX_Manual extends Firewall_Impl_seL4_Firewall_Firewall_GumboX_TestHarness_ScalaTest {
+  def freshRandomLib: RandomLib = {
+    RandomLib(Random.Gen64Impl(Xoshiro256.create))
+  }
+
+  override def verbose: B = F
+
+  test("Violate assumption 'onlyOneInEvent'") {
+
+    val rxIn = freshRandomLib.nextSWStructuredEthernetMessage_i()
+    val txIn = freshRandomLib.nextSWStructuredEthernetMessage_i()
+
+    testComputeCB(api_EthernetFramesRxIn = Some(rxIn), api_EthernetFramesTxIn = Some(txIn)) match {
+      case GumboXResult.Pre_Condition_Unsat =>
+        println("Precondition violated")
+      case x => assert (F, s"Wasn't expecting: $x")
+    }
+  }
+
+  test ("Violate datatype invariant 'relateFrameProtocolToArpType'") {
+    val rxIn = freshRandomLib.nextSWStructuredEthernetMessage_i()(
+      frameProtocol = FrameProtocol.TCP, arpType = ARP_Type.REPLY)
+
+    testComputeCB(api_EthernetFramesRxIn = Some(rxIn), api_EthernetFramesTxIn = None()) match {
+      case GumboXResult.Pre_Condition_Unsat =>
+        println("Precondition violated")
+      case x => assert (F, s"Wasn't expecting: $x")
+    }
+  }
+
+  test(" RC_INSPECTA_00-HLR-6: Allow RxIn + IPV4 + TCP + port whitelisted") {
+    val msg = StructuredEthernetMessage_i(
+      internetProtocol = InternetProtocol.IPV4,
+      frameProtocol = FrameProtocol.TCP,
+      portIsWhitelisted = T,
+      arpType = ARP_Type.NA,
+
+      malformedFrame = freshRandomLib.nextB(),
+      rawMessage = freshRandomLib.nextSWRawEthernetMessage())
+
+    testComputeCB(api_EthernetFramesRxIn = Some(msg), api_EthernetFramesTxIn = None()) match {
+      case GumboXResult.Post_Condition_Pass =>
+        println("Post-condition held")
+      case x => assert (F, s"Wasn't expecting $x")
+    }
+  }
+}

open-platform-models/isolate-ethernet-simple/hamr/slang/src/test/bridge/base/SW/Firewall_Impl_seL4_Firewall_Firewall_Test.scala

@@ -1,11 +1,17 @@
 package base.SW
 
+import base.RandomLib
 import org.sireum._
 import base.SW._
+import org.sireum.Random.Impl.Xoshiro256
 
 // This file will not be overwritten so is safe to edit
 class Firewall_Impl_seL4_Firewall_Firewall_Test extends Firewall_Impl_seL4_Firewall_Firewall_ScalaTest {
 
+  def freshRandomLib: RandomLib = {
+    RandomLib(Random.Gen64Impl(Xoshiro256.create))
+  }
+/*
   test("Example Unit Test for Initialise Entry Point"){
     // Initialise Entry Point doesn't read input port values, so just proceed with
     // launching the entry point code
@@ -20,4 +26,170 @@ class Firewall_Impl_seL4_Firewall_Firewall_Test extends Firewall_Impl_seL4_Firew
     // use get_XXX methods and check_concrete_output() from test/util/../YYY_TestApi
     // retrieve values from output ports and check against expected results
   }
+*/
+  test("RC_INSPECTA_00-HLR-6: Allow RxIn + IPV4 + TCP + port whitelisted") {
+    val msg = StructuredEthernetMessage_i(
+      internetProtocol = InternetProtocol.IPV4,
+      frameProtocol = FrameProtocol.TCP,
+      portIsWhitelisted = T,
+      arpType = ARP_Type.NA,
+
+      malformedFrame = freshRandomLib.nextB(),
+      rawMessage = freshRandomLib.nextSWRawEthernetMessage())
+
+    put_EthernetFramesRxIn(msg)
+
+    testCompute()
+
+    get_EthernetFramesRxOut() match {
+      case Some(payload) => assert (payload == msg)
+      case _ => assert (F)
+    }
+
+    assert (get_EthernetFramesTxOut().isEmpty)
+  }
+
+  test("RC_INSPECTA_00-HLR-4: Drop RxIn + IPV4 + TCP + port not whitelisted") {
+    val msg = StructuredEthernetMessage_i(
+      internetProtocol = InternetProtocol.IPV4,
+      frameProtocol = FrameProtocol.TCP,
+      portIsWhitelisted = F,
+      arpType = ARP_Type.NA,
+
+      malformedFrame = freshRandomLib.nextB(),
+      rawMessage = freshRandomLib.nextSWRawEthernetMessage())
+
+    put_EthernetFramesRxIn(msg)
+
+    testCompute()
+
+    assert (get_EthernetFramesRxOut().isEmpty)
+
+    assert (get_EthernetFramesTxOut().isEmpty)
+  }
+
+  test("RC_INSPECTA_00-HLR-5: RxIn + IPV4 + ARP Request ~> ARP Reply") {
+    val msg = StructuredEthernetMessage_i(
+      internetProtocol = InternetProtocol.IPV4,
+      frameProtocol = FrameProtocol.ARP,
+      arpType = ARP_Type.REQUEST,
+
+      portIsWhitelisted = freshRandomLib.nextB(),
+      malformedFrame = freshRandomLib.nextB(),
+      rawMessage = freshRandomLib.nextSWRawEthernetMessage())
+
+    put_EthernetFramesRxIn(msg)
+
+    testCompute()
+
+    get_EthernetFramesTxOut() match {
+      case Some(payload) => assert (payload.arpType == ARP_Type.REPLY, "Expected arp reply on TxOut")
+      case _ => assert(F)
+    }
+
+    assert (get_EthernetFramesRxOut().isEmpty)
+  }
+
+  test("RC_INSPECTA_00-HLR-5: Drop RxIn + IPV4 + ARP Reply") {
+    val msg = StructuredEthernetMessage_i(
+      internetProtocol = InternetProtocol.IPV4,
+      frameProtocol = FrameProtocol.ARP,
+      arpType = ARP_Type.REPLY,
+
+      portIsWhitelisted = freshRandomLib.nextB(),
+      malformedFrame = freshRandomLib.nextB(),
+      rawMessage = freshRandomLib.nextSWRawEthernetMessage())
+
+    put_EthernetFramesRxIn(msg)
+
+    testCompute()
+
+    assert (get_EthernetFramesTxOut().isEmpty)
+
+    assert (get_EthernetFramesRxOut().isEmpty)
+  }
+
+  test("RC_INSPECTA_00-HLR-2: Drop RxIn + IPV6") {
+    val arpType = freshRandomLib.nextSWARP_TypeType()
+    val msg = StructuredEthernetMessage_i(
+      internetProtocol = InternetProtocol.IPV6,
+
+      frameProtocol = if (arpType == ARP_Type.NA) FrameProtocol.TCP else FrameProtocol.ARP,
+      arpType = arpType,
+      portIsWhitelisted = freshRandomLib.nextB(),
+      malformedFrame = freshRandomLib.nextB(),
+      rawMessage = freshRandomLib.nextSWRawEthernetMessage())
+
+    put_EthernetFramesRxIn(msg)
+
+    testCompute()
+
+    assert (get_EthernetFramesTxOut().isEmpty)
+
+    assert (get_EthernetFramesRxOut().isEmpty)
+  }
+
+  test("RC_INSPECTA_00-HLR-7: Allow TxIn + IPV4") {
+    val arpType = freshRandomLib.nextSWARP_TypeType()
+    val msg = StructuredEthernetMessage_i(
+      internetProtocol = InternetProtocol.IPV4,
+
+      frameProtocol = if (arpType == ARP_Type.NA) FrameProtocol.TCP else FrameProtocol.ARP,
+      arpType = arpType,
+      portIsWhitelisted = freshRandomLib.nextB(),
+      malformedFrame = freshRandomLib.nextB(),
+      rawMessage = freshRandomLib.nextSWRawEthernetMessage())
+
+    put_EthernetFramesTxIn(msg)
+
+    testCompute()
+
+    get_EthernetFramesTxOut() match {
+      case Some(payload) => assert(payload == msg)
+      case _ => assert (F)
+    }
+
+    assert (get_EthernetFramesRxOut().isEmpty)
+  }
+
+  test("RC_INSPECTA_00-HLR-7: Allow TxIn + IPV6 + ARP") {
+    val msg = StructuredEthernetMessage_i(
+      internetProtocol = InternetProtocol.IPV6,
+      frameProtocol = FrameProtocol.ARP,
+      arpType = ARP_Type.REPLY,
+
+      portIsWhitelisted = freshRandomLib.nextB(),
+      malformedFrame = freshRandomLib.nextB(),
+      rawMessage = freshRandomLib.nextSWRawEthernetMessage())
+
+    put_EthernetFramesTxIn(msg)
+
+    testCompute()
+
+    get_EthernetFramesTxOut() match {
+      case Some(payload) => assert(payload == msg)
+      case _ => assert (F)
+    }
+
+    assert (get_EthernetFramesRxOut().isEmpty)
+  }
+
+  test("RC_INSPECTA_00-HLR-7: Drop TxIn + IPV6 + TCP") {
+    val msg = StructuredEthernetMessage_i(
+      internetProtocol = InternetProtocol.IPV6,
+      frameProtocol = FrameProtocol.TCP,
+      arpType = ARP_Type.NA,
+
+      portIsWhitelisted = freshRandomLib.nextB(),
+      malformedFrame = freshRandomLib.nextB(),
+      rawMessage = freshRandomLib.nextSWRawEthernetMessage())
+
+    put_EthernetFramesTxIn(msg)
+
+    testCompute()
+
+    assert (get_EthernetFramesTxOut().isEmpty)
+
+    assert (get_EthernetFramesRxOut().isEmpty)
+  }
 }