diff --git a/lib/linux-script.dhall b/lib/linux-script.dhall
index 7ed5c1d..9f6f418 100644
--- a/lib/linux-script.dhall
+++ b/lib/linux-script.dhall
@@ -27,16 +27,17 @@ let addLine =
}
e.mapValue
-in λ(args : Args) -> \(out : Text)
- →
- { config = Genode.Init.render args.config
- , script = Prelude.List.fold
- RomEntry
- args.rom
- Text
- addLine
- ''
- #!/bin/sh
- ln -s ${out}/config config
- ''
- }
+in λ(args : Args)
+ → λ(out : Text)
+ → { config = Genode.Init.render args.config
+ , script =
+ Prelude.List.fold
+ RomEntry
+ args.rom
+ Text
+ addLine
+ ''
+ #!/bin/sh
+ ln -s ${out}/config config
+ ''
+ }
diff --git a/tests/block_router.dhall b/tests/block_router.dhall
index 4d67e9a..9b2e4db 100644
--- a/tests/block_router.dhall
+++ b/tests/block_router.dhall
@@ -1,6 +1,8 @@
-- SPDX-License-Identifier: CC0-1.0
-let Genode = env:DHALL_GENODE
+let Test = ./test.dhall ? env:DHALL_GENODE_TEST
+
+let Genode = Test.Genode
let Prelude = Genode.Prelude
@@ -14,8 +16,8 @@ let Resources = Init.Resources
let ServiceRoute = Init.ServiceRoute
-in Genode.Boot::{
- , config = Init::{
+let init =
+ Init::{
, verbose = True
, children =
let blockTest =
@@ -112,7 +114,9 @@ in Genode.Boot::{
[ XML.leaf
{ name = "partition"
, attributes = toMap
- { type = "24B69406-18A1-428D-908E-D21A1437122C" }
+ { type =
+ "24B69406-18A1-428D-908E-D21A1437122C"
+ }
}
]
}
@@ -129,6 +133,9 @@ in Genode.Boot::{
, test-part2 = blockTest
}
}
+
+in Test::{
+ , children = Test.initToChildren init
, rom =
Genode.BootModules.toRomPaths
[ { mapKey = "gpt.rom", mapValue = "./gpt.raw" } ]
diff --git a/tests/driver-hw.nix b/tests/driver-hw.nix
index ac6ad85..c7a88ca 100644
--- a/tests/driver-hw.nix
+++ b/tests/driver-hw.nix
@@ -45,7 +45,7 @@ let
testConfig' = "${./test-wrapper.dhall} ${testConfig} (toMap ${manifest})";
testEnv' = {
DHALL_GENODE = "${testPkgs.dhallGenode}/source.dhall";
- XDG_CACHE_HOME = "/tmp";
+ DHALL_GENODE_TEST = "${./test.dhall}";
} // testEnv;
image = lib.hwImage name testEnv' testConfig';
diff --git a/tests/driver-linux.nix b/tests/driver-linux.nix
index a1c43cd..03fc48c 100644
--- a/tests/driver-linux.nix
+++ b/tests/driver-linux.nix
@@ -43,7 +43,7 @@ let
testConfig' = "${./test-wrapper.dhall} ${testConfig} (toMap ${manifest})";
env' = {
DHALL_GENODE = "${testPkgs.dhallGenode}/source.dhall";
- XDG_CACHE_HOME = "/tmp";
+ DHALL_GENODE_TEST = "${./test.dhall}";
} // env;
build = lib.linuxScript name env' testConfig';
@@ -70,9 +70,6 @@ let
global image_dir spawn_id
- global env
- set env(XDG_CACHE_HOME) /tmp
-
exec sh ${build}/script
spawn ./core-linux
@@ -100,13 +97,13 @@ let
in test // {
inherit build driver test;
- config = buildPackages.runCommand (name + ".dhall") env' ''
+ config = lib.runDhallCommand (name + ".dhall") env' ''
${apps.dhall.program} <<< "(${testConfig'}).config" > $out
'';
- xml = buildPackages.runCommand (name + ".config") env' ''
+ xml = lib.runDhallCommand (name + ".config") env' ''
${apps.render-init.program} <<< "(${testConfig'}).config" > $out
'';
- image = buildPackages.runCommand (name + ".image.elf") env' ''
+ image = lib.runDhallCommand (name + ".image.elf") env' ''
mkdir -p $out
pushd $out
. ${build}/script
diff --git a/tests/driver-nova.nix b/tests/driver-nova.nix
index 2af38ca..1206993 100644
--- a/tests/driver-nova.nix
+++ b/tests/driver-nova.nix
@@ -46,7 +46,7 @@ let
testConfig' = "${./test-wrapper.dhall} ${testConfig} (toMap ${manifest})";
testEnv' = {
DHALL_GENODE = "${testPkgs.dhallGenode}/source.dhall";
- XDG_CACHE_HOME = "/tmp";
+ DHALL_GENODE_TEST = "${./test.dhall}";
} // testEnv;
image = lib.novaImage name testEnv' testConfig';
diff --git a/tests/driver_manager.dhall b/tests/driver_manager.dhall
index 172104b..1381b7a 100644
--- a/tests/driver_manager.dhall
+++ b/tests/driver_manager.dhall
@@ -1,8 +1,10 @@
-- SPDX-License-Identifier: CC0-1.0
+let Test = ./test.dhall ? env:DHALL_GENODE_TEST
+
let drivers = env:drivers ? ../compositions/pc-drivers.dhall
-let Genode = env:DHALL_GENODE
+let Genode = Test.Genode
let Init = Genode.Init
@@ -24,8 +26,8 @@ let childRomRoute =
let label = λ(_ : Text) → { local = _, route = _ }
-in Genode.Boot::{
- , config = Init::{
+let init =
+ Init::{
, verbose = True
, children = toMap
{ drivers =
@@ -91,59 +93,61 @@ in Genode.Boot::{
}
}
}
- , rom =
- Genode.Boot.toRomTexts
- ( toMap
- { capslock = ""
- , numlock = ""
- , usb_policy = ""
- }
- # [ { mapKey = "fb_drv.config"
- , mapValue =
- ''
-
-
-
- ''
- }
- , { mapKey = "input_filter.config"
- , mapValue =
- ''
-
-
-
-
-
- ''
- }
- ]
- )
- }
+
+let rom =
+ Genode.Boot.toRomTexts
+ ( toMap
+ { capslock = ""
+ , numlock = ""
+ , usb_policy = ""
+ }
+ # [ { mapKey = "fb_drv.config"
+ , mapValue =
+ ''
+
+
+
+ ''
+ }
+ , { mapKey = "input_filter.config"
+ , mapValue =
+ ''
+
+
+
+
+
+ ''
+ }
+ ]
+ )
+
+in Test::{ children = Test.initToChildren init, rom = rom }
diff --git a/tests/log.dhall b/tests/log.dhall
index d54d882..22d437c 100644
--- a/tests/log.dhall
+++ b/tests/log.dhall
@@ -1,23 +1,23 @@
-- SPDX-License-Identifier: CC0-1.0
-let Genode = env:DHALL_GENODE
+let Test = ./test.dhall ? env:DHALL_GENODE_TEST
+
+let Genode = Test.Genode
let Child = Genode.Init.Child
-in Genode.Boot::{
- , config = Genode.Init::{
- , children = toMap
- { test-log =
- Child.flat
- Child.Attributes::{
- , binary = "test-log"
- , exitPropagate = True
- , resources = Genode.Init.Resources::{
- , caps = 500
- , ram = Genode.units.MiB 10
- }
- , routes = [ Genode.Init.ServiceRoute.parent "Timer" ]
+in Test::{
+ , children = toMap
+ { test-log =
+ Child.flat
+ Child.Attributes::{
+ , binary = "test-log"
+ , exitPropagate = True
+ , resources = Genode.Init.Resources::{
+ , caps = 500
+ , ram = Genode.units.MiB 10
}
- }
- }
+ , routes = [ Genode.Init.ServiceRoute.parent "Timer" ]
+ }
+ }
}
diff --git a/tests/noux.dhall b/tests/noux.dhall
index d9e3e7e..669c835 100644
--- a/tests/noux.dhall
+++ b/tests/noux.dhall
@@ -1,46 +1,46 @@
-- SPDX-License-Identifier: CC0-1.0
-let Genode = env:DHALL_GENODE
+let Test = ./test.dhall ? env:DHALL_GENODE_TEST
+
+let Genode = Test.Genode
let Child = Genode.Init.Child
-in Genode.Boot::{
- , config = Genode.Init::{
- , children = toMap
- { noux =
- Child.flat
- Child.Attributes::{
- , binary = "noux"
- , exitPropagate = True
- , resources = Genode.Init.Resources::{
- , caps = 500
- , ram = Genode.units.MiB 10
- }
- , routes = [ Genode.Init.ServiceRoute.parent "Timer" ]
- , config = Genode.Init.Config::{
- , attributes = toMap
- { stdin = "/script"
- , stdout = "/dev/log"
- , stderr = "/dev/log"
- }
- , content =
- [ Genode.Prelude.XML.text
- ''
-
-
-
-
-
- echo "hello world"
-
-
-
-
-
- ''
- ]
- }
+in Test::{
+ , children = toMap
+ { noux =
+ Child.flat
+ Child.Attributes::{
+ , binary = "noux"
+ , exitPropagate = True
+ , resources = Genode.Init.Resources::{
+ , caps = 500
+ , ram = Genode.units.MiB 10
}
- }
- }
+ , routes = [ Genode.Init.ServiceRoute.parent "Timer" ]
+ , config = Genode.Init.Config::{
+ , attributes = toMap
+ { stdin = "/script"
+ , stdout = "/dev/log"
+ , stderr = "/dev/log"
+ }
+ , content =
+ [ Genode.Prelude.XML.text
+ ''
+
+
+
+
+
+ echo "hello world"
+
+
+
+
+
+ ''
+ ]
+ }
+ }
+ }
}
diff --git a/tests/pci.dhall b/tests/pci.dhall
index fa458e9..88f0b22 100644
--- a/tests/pci.dhall
+++ b/tests/pci.dhall
@@ -1,6 +1,8 @@
-- SPDX-License-Identifier: CC0-1.0
-let Genode = env:DHALL_GENODE
+let Test = ./test.dhall ? env:DHALL_GENODE_TEST
+
+let Genode = Test.Genode
let XML = Genode.Prelude.XML
@@ -14,8 +16,8 @@ let ServiceRoute = Init.ServiceRoute
let label = λ(_ : Text) → { local = _, route = _ } : Child.Attributes.Label
-in Genode.Boot::{
- , config = Init::{
+let init =
+ Init::{
, verbose = True
, children = toMap
{ test-pci =
@@ -71,4 +73,5 @@ in Genode.Boot::{
}
}
}
- }
+
+in Test::{ children = Test.initToChildren init }
diff --git a/tests/rtc.dhall b/tests/rtc.dhall
index 83c33e4..b7eb8d9 100644
--- a/tests/rtc.dhall
+++ b/tests/rtc.dhall
@@ -1,11 +1,13 @@
-- SPDX-License-Identifier: CC0-1.0
-let Genode = env:DHALL_GENODE
+let Test = ./test.dhall ? env:DHALL_GENODE_TEST
+
+let Genode = Test.Genode
let Child = Genode.Init.Child
-in Genode.Boot::{
- , config = Genode.Init::{
+let init =
+ Genode.Init::{
, children = toMap
{ test-rtc =
Child.flat
@@ -26,4 +28,5 @@ in Genode.Boot::{
}
}
}
- }
+
+in Test::{ children = Test.initToChildren init }
diff --git a/tests/signal.dhall b/tests/signal.dhall
index d634a12..a5a4d4f 100644
--- a/tests/signal.dhall
+++ b/tests/signal.dhall
@@ -1,26 +1,26 @@
-- SPDX-License-Identifier: CC0-1.0
-let Genode = env:DHALL_GENODE
+let Test = ./test.dhall ? env:DHALL_GENODE_TEST
+
+let Genode = Test.Genode
let Init = Genode.Init
let Child = Init.Child
-in Genode.Boot::{
- , config = Init::{
- , children = toMap
- { test-signal =
- Child.flat
- Child.Attributes::{
- , binary = "test-signal"
- , exitPropagate = True
- , priority = 5
- , resources = Init.Resources::{
- , caps = 500
- , ram = Genode.units.MiB 10
- }
- , routes = [ Init.ServiceRoute.parent "Timer" ]
+in Test::{
+ , children = toMap
+ { test-signal =
+ Child.flat
+ Child.Attributes::{
+ , binary = "test-signal"
+ , exitPropagate = True
+ , priority = 5
+ , resources = Init.Resources::{
+ , caps = 500
+ , ram = Genode.units.MiB 10
}
- }
- }
+ , routes = [ Init.ServiceRoute.parent "Timer" ]
+ }
+ }
}
diff --git a/tests/solo5/blk.dhall b/tests/solo5/blk.dhall
index e50e7fa..e9057fc 100644
--- a/tests/solo5/blk.dhall
+++ b/tests/solo5/blk.dhall
@@ -6,8 +6,8 @@ let Init = Genode.Init
let Child = Init.Child
-in Genode.Boot::{
- , config = Init::{
+let init =
+ Init::{
, children = toMap
{ solo5 =
Child.flat
@@ -35,4 +35,5 @@ in Genode.Boot::{
}
}
}
- }
+
+in Init.toChild init Init.Attributes.default
diff --git a/tests/solo5/default.nix b/tests/solo5/default.nix
index c1bb6be..d17ffd7 100644
--- a/tests/solo5/default.nix
+++ b/tests/solo5/default.nix
@@ -5,7 +5,7 @@ with pkgs;
let
defaultScript = ''
- run_genode_until {SUCCESS} 30
+ run_genode_until {SOTEST END} 30
'';
mkTest' = { name, testConfig, testScript ? defaultScript, testInputs ? [ ]
@@ -23,66 +23,30 @@ let
mkTests = testList: builtins.listToAttrs (map applyMkTest testList);
- toSimple = name: ''(${./simple.dhall} \"solo5-test_${name}\")'';
-
genodeDepot = pkgs.genodeSources.depot;
genodeMake = pkgs.genodeSources.make;
tests = [
{
- name = "blk";
- testConfig = ./blk.dhall;
- testInputs = [ (genodeDepot "ram_block") ];
- }
-
- {
- name = "fpu";
- testConfig = toSimple "fpu";
- }
-
- {
- name = "globals";
- testConfig = toSimple "globals";
- }
-
- {
- name = "hello";
- testConfig = toSimple "hello";
- }
-
- {
- name = "net";
- testConfig = ./net.dhall;
- testInputs = (map genodeDepot [ "nic_bridge" "nic_loopback" ])
- ++ (map genodeMake [ "app/ping" ]);
- }
-
- {
- name = "net_2if";
- testConfig = ./net_2if.dhall;
- testInputs = (map genodeDepot [ "sequence" "nic_bridge" "nic_loopback" ])
- ++ (map genodeMake [ "app/ping" ]);
- }
-
- {
- name = "quiet";
- testConfig = toSimple "quiet";
+ name = "multi";
+ testConfig = "${./.}/solo5.dhall";
+ testInputs = map genodeMake [ "app/ping" ] ++ (map genodeDepot [
+ "ram_block"
+ "nic_bridge"
+ "nic_loopback"
+ "sequence"
+ "rtc_drv"
+ ]);
}
{
name = "ssp";
- testConfig = toSimple "ssp";
+ testConfig = ./ssp.dhall;
testScript = ''
run_genode_until {Error: stack protector check failed} 30
'';
}
- ] ++ (testEnv.lib.optional (!testEnv.isLinux) {
- name = "time";
- testConfig = ./time.dhall;
- testInputs = [ (genodeDepot "rtc_drv") ];
- }
-
- );
+ ];
in mkTests tests
diff --git a/tests/solo5/net.dhall b/tests/solo5/net.dhall
index b5a4f9b..be89290 100644
--- a/tests/solo5/net.dhall
+++ b/tests/solo5/net.dhall
@@ -10,8 +10,8 @@ let Res = Init.Resources
let ServiceRoute = Init.ServiceRoute
-in Genode.Boot::{
- , config = Init::{
+let init =
+ Init::{
, children = toMap
{ nic =
Child.flat
@@ -72,4 +72,5 @@ in Genode.Boot::{
}
}
}
- }
+
+in Init.toChild init Init.Attributes.default
diff --git a/tests/solo5/net_2if.dhall b/tests/solo5/net_2if.dhall
index 8a9a337..eea827b 100644
--- a/tests/solo5/net_2if.dhall
+++ b/tests/solo5/net_2if.dhall
@@ -8,8 +8,8 @@ let Child = Init.Child
let Res = Init.Resources
-in Genode.Boot::{
- , config = Init::{
+let init =
+ Init::{
, children = toMap
{ nic =
Child.flat
@@ -81,4 +81,5 @@ in Genode.Boot::{
}
}
}
- }
+
+in Init.toChild init Init.Attributes.default
diff --git a/tests/solo5/simple.dhall b/tests/solo5/simple.dhall
deleted file mode 100644
index fb3ba5b..0000000
--- a/tests/solo5/simple.dhall
+++ /dev/null
@@ -1,39 +0,0 @@
--- SPDX-License-Identifier: CC0-1.0
-
-let Genode = env:DHALL_GENODE
-
-let Prelude = Genode.Prelude
-
-let Init = Genode.Init
-
-let Child = Init.Child
-
-let Config = Init.Config
-
-in λ(testBinary : Text)
- → Genode.Boot::{
- , config = Init::{
- , children = toMap
- { solo5 =
- Child.flat
- Child.Attributes::{
- , binary = testBinary
- , exitPropagate = True
- , resources = Init.Resources::{
- , caps = 256
- , ram = Genode.units.MiB 3
- }
- , config = Config::{
- , content =
- [ Prelude.XML.element
- { name = "cmdline"
- , attributes = Prelude.XML.emptyAttributes
- , content = [ Prelude.XML.text "Hello_Solo5" ]
- }
- ]
- }
- , routes = [ Init.ServiceRoute.parent "Timer" ]
- }
- }
- }
- }
diff --git a/tests/solo5/solo5.dhall b/tests/solo5/solo5.dhall
new file mode 100644
index 0000000..9ee1adf
--- /dev/null
+++ b/tests/solo5/solo5.dhall
@@ -0,0 +1,45 @@
+-- SPDX-License-Identifier: CC0-1.0
+
+let Test = ../test.dhall ? env:DHALL_GENODE_TEST
+
+let Genode = Test.Genode
+
+let Prelude = Genode.Prelude
+
+let Init = Genode.Init
+
+let Child = Init.Child
+
+let Config = Init.Config
+
+let toSimple =
+ λ(testName : Text)
+ → Child.flat
+ Child.Attributes::{
+ , binary = "solo5-test_${testName}"
+ , resources = Init.Resources::{ caps = 256, ram = Genode.units.MiB 3 }
+ , config = Config::{
+ , content =
+ [ Prelude.XML.element
+ { name = "cmdline"
+ , attributes = Prelude.XML.emptyAttributes
+ , content = [ Prelude.XML.text "Hello_Solo5" ]
+ }
+ ]
+ }
+ , routes = [ Init.ServiceRoute.parent "Timer" ]
+ }
+
+let tests
+ : Prelude.Map.Type Text Child.Type
+ = [ { mapKey = "quiet", mapValue = toSimple "quiet" }
+ , { mapKey = "hello", mapValue = toSimple "hello" }
+ , { mapKey = "globals", mapValue = toSimple "globals" }
+ , { mapKey = "fpu", mapValue = toSimple "fpu" }
+ , { mapKey = "time", mapValue = ./time.dhall }
+ , { mapKey = "blk", mapValue = ./blk.dhall }
+ , { mapKey = "net", mapValue = ./net.dhall }
+ , { mapKey = "net_2if", mapValue = ./net_2if.dhall }
+ ]
+
+in Test::{ children = tests }
diff --git a/tests/solo5/ssp.dhall b/tests/solo5/ssp.dhall
new file mode 100644
index 0000000..00fa501
--- /dev/null
+++ b/tests/solo5/ssp.dhall
@@ -0,0 +1,9 @@
+-- SPDX-License-Identifier: CC0-1.0
+
+let Test = ../test.dhall ? env:DHALL_GENODE_TEST
+
+let Child = Test.Genode.Init.Child
+
+let test = Child.flat Child.Attributes::{ binary = "solo5-test_ssp" }
+
+in Test::{ children = toMap { ssp = test } }
diff --git a/tests/solo5/time.dhall b/tests/solo5/time.dhall
index 87a62a8..4ca43f3 100644
--- a/tests/solo5/time.dhall
+++ b/tests/solo5/time.dhall
@@ -2,32 +2,38 @@
let Genode = env:DHALL_GENODE
-let Child = Genode.Init.Child
+let Init = Genode.Init
-in Genode.Boot::{
- , config = Genode.Init::{
+let Child = Init.Child
+
+let init =
+ Init::{
, children = toMap
{ solo5 =
Child.flat
Child.Attributes::{
, binary = "solo5-test_time"
, exitPropagate = True
- , resources = Genode.Init.Resources::{
+ , resources = Init.Resources::{
, caps = 256
, ram = Genode.units.MiB 3
}
, routes =
- [ Genode.Init.ServiceRoute.parent "Timer"
- , Genode.Init.ServiceRoute.child "Rtc" "clock"
+ [ Init.ServiceRoute.parent "Timer"
+ , Init.ServiceRoute.child "Rtc" "rtc_drv"
]
}
- , clock =
+ , rtc_drv =
Child.flat
Child.Attributes::{
, binary = "rtc_drv"
+ , exitPropagate = True
, provides = [ "Rtc" ]
- , routes = [ Genode.Init.ServiceRoute.parent "IO_PORT" ]
+ , routes = [ Init.ServiceRoute.parent "IO_PORT" ]
}
}
}
- }
+
+in Init.toChild
+ init
+ Init.Attributes::{ routes = [ Init.ServiceRoute.parent "IO_PORT" ] }
diff --git a/tests/test-wrapper.dhall b/tests/test-wrapper.dhall
index b303c5e..91eb074 100644
--- a/tests/test-wrapper.dhall
+++ b/tests/test-wrapper.dhall
@@ -1,6 +1,7 @@
-- SPDX-License-Identifier: CC0-1.0
+let Test = ./test.dhall ? env:DHALL_GENODE_TEST
-let Genode = env:DHALL_GENODE
+let Genode = Test.Genode
let Prelude = Genode.Prelude
@@ -8,13 +9,18 @@ let Init = Genode.Init
let Child = Init.Child
+let TextMapType = Prelude.Map.Type Text
+
+let Children = TextMapType Child.Type
+
let wrapHarness
- : Init.Type → Child.Type
- = λ(init : Init.Type)
+ : Children → Child.Type
+ = λ(children : Children)
→ Child.nested
- (toMap { init = Genode.Init.toChild init Init.Attributes.default })
+ children
Child.Attributes::{
, binary = "sotest-harness"
+ , exitPropagate = True
, resources = Init.Resources::{ ram = Genode.units.MiB 4 }
, routes =
[ Init.ServiceRoute.parentLabel
@@ -28,35 +34,31 @@ let wrapHarness
]
}
-let TextMapType = Prelude.Map.Type Text
-
-in λ(boot : Genode.Boot.Type)
+in λ(test : Test.Type)
→ λ(inputsManifest : TextMapType (TextMapType Text))
- → boot
- ⫽ { config = Init::{
- , children =
- [ { mapKey = "timer"
- , mapValue =
- Child.flat
- Child.Attributes::{
- , binary = "timer_drv"
- , provides = [ "Timer" ]
- }
- }
- , { mapKey = "harness", mapValue = wrapHarness boot.config }
- ]
- }
- , rom =
- let inputRoms =
- Genode.BootModules.toRomPaths
- ( Prelude.List.concat
- (Prelude.Map.Entry Text Text)
- ( Prelude.Map.values
- Text
- (Prelude.Map.Type Text Text)
- inputsManifest
- )
- )
-
- in boot.rom # inputRoms
+ → Genode.Boot::{
+ , config = Init::{
+ , children =
+ [ { mapKey = "timer"
+ , mapValue =
+ Child.flat
+ Child.Attributes::{
+ , binary = "timer_drv"
+ , provides = [ "Timer" ]
+ }
+ }
+ , { mapKey = "harness", mapValue = wrapHarness test.children }
+ ]
}
+ , rom =
+ test.rom
+ # Genode.BootModules.toRomPaths
+ ( Prelude.List.concat
+ (Prelude.Map.Entry Text Text)
+ ( Prelude.Map.values
+ Text
+ (Prelude.Map.Type Text Text)
+ inputsManifest
+ )
+ )
+ }
diff --git a/tests/test.dhall b/tests/test.dhall
new file mode 100644
index 0000000..9ee791e
--- /dev/null
+++ b/tests/test.dhall
@@ -0,0 +1,32 @@
+let Genode = env:DHALL_GENODE
+
+let Prelude = Genode.Prelude
+
+let Init = Genode.Init
+
+in { Genode = Genode
+ , Type =
+ { children : Prelude.Map.Type Text Init.Child.Type
+ , rom : Genode.BootModules.Type
+ }
+ , default.rom = [] : Genode.BootModules.Type
+ , initToChildren =
+ λ(init : Init.Type)
+ → toMap
+ { init =
+ Init.toChild
+ init
+ Init.Attributes::{
+ , routes =
+ [ Init.ServiceRoute.parentLabel
+ "LOG"
+ (Some "SOTEST")
+ (Some "unlabeled")
+ , Init.ServiceRoute.parent "IO_MEM"
+ , Init.ServiceRoute.parent "IO_PORT"
+ , Init.ServiceRoute.parent "IRQ"
+ , Init.ServiceRoute.child "Timer" "timer"
+ ]
+ }
+ }
+ }