From fcb0a48401a46bdb314a44239c93b39d11a6f6a4 Mon Sep 17 00:00:00 2001 From: Emery Hemingway Date: Tue, 28 Jan 2020 13:45:54 +0100 Subject: [PATCH] Lower single child tests for NOVA test wrapper If an single-child init is added to a list of children then it must be safe to lower the child and add it to the list directly. --- tests/driver-nova-config.dhall | 117 ++++++++++++++++++++------------- 1 file changed, 73 insertions(+), 44 deletions(-) diff --git a/tests/driver-nova-config.dhall b/tests/driver-nova-config.dhall index 6692d99..06dcfda 100644 --- a/tests/driver-nova-config.dhall +++ b/tests/driver-nova-config.dhall @@ -2,45 +2,74 @@ let Genode = env:DHALL_GENODE -in λ(args : Genode.Boot.Type) - → { config = - Genode.Init::{ - , verbose = True - , defaultRoutes = - Genode.Init.default.defaultRoutes - # [ Genode.ServiceRoute.parent "IO_MEM" - , Genode.ServiceRoute.parent "IO_PORT" - , Genode.ServiceRoute.parent "IRQ" - , Genode.ServiceRoute.child "Timer" "timer" - ] - , children = - [ { mapKey = "timer" - , mapValue = - Genode.Init.Start::{ - , binary = "nova_timer_drv" - , resources = { caps = 96, ram = Genode.units.MiB 1 } - , provides = [ "Timer" ] +let Prelude = Genode.Prelude + +let ChildEntry = Prelude.Map.Entry Text Genode.Init.Start.Type + +let toChildEntry = + λ(init : Genode.Init.Type) + → let childCount = Prelude.List.length ChildEntry init.children + + let onlyChild = Prelude.Natural.lessThan childCount 2 + + let child = + if onlyChild + + then Prelude.Optional.fold + ChildEntry + (Prelude.List.head ChildEntry init.children) + ChildEntry + (λ(child : ChildEntry) → child) + { mapKey = "" + , mapValue = Genode.Init.Start::{ binary = "" } + } + + else { mapKey = "init", mapValue = Genode.Init.toStart init } + + in child + +in λ(boot : Genode.Boot.Type) + → let child = toChildEntry boot.config + + in { config = + Genode.Init::{ + , defaultRoutes = + Genode.Init.default.defaultRoutes + # [ Genode.ServiceRoute.parent "IO_MEM" + , Genode.ServiceRoute.parent "IO_PORT" + , Genode.ServiceRoute.parent "IRQ" + , Genode.ServiceRoute.child "Timer" "timer" + ] + , children = + [ { mapKey = "timer" + , mapValue = + Genode.Init.Start::{ + , binary = "nova_timer_drv" + , resources = { caps = 96, ram = Genode.units.MiB 1 } + , provides = [ "Timer" ] + } } - } - , { mapKey = "harness" - , mapValue = - let child = Genode.Init.toStart args.config - - in Genode.Init.Start::{ + , { mapKey = "harness" + , mapValue = + Genode.Init.Start::{ , binary = "sotest-harness" , exitPropagate = True , resources = - { caps = child.resources.caps + 128 - , ram = child.resources.ram + Genode.units.MiB 1 + { caps = child.mapValue.resources.caps + 128 + , ram = + child.mapValue.resources.ram + + Genode.units.MiB 1 } , config = Some - ( Genode.Prelude.XML.element + ( Prelude.XML.element { name = "config" - , attributes = - Genode.Prelude.XML.emptyAttributes + , attributes = Prelude.XML.emptyAttributes , content = - [ Genode.Init.Start.toXML "init" child ] + [ Genode.Init.Start.toXML + child.mapKey + child.mapValue + ] } ) , routes = @@ -50,19 +79,19 @@ in λ(args : Genode.Boot.Type) (Some "platform") ] } - } - ] - } - , rom = - let manifest = env:MANIFEST - - in Genode.Boot.toRomPaths - [ { mapKey = "ld.lib.so" - , mapValue = manifest.base-nova.lib.ld-nova.mapValue } - , manifest.base-nova.bin.nova_timer_drv - , manifest.os.bin.init - , manifest.sotest-producer.bin.sotest-harness ] - # args.rom - } + } + , rom = + let manifest = env:MANIFEST + + in Genode.Boot.toRomPaths + [ Prelude.Map.keyText + "ld.lib.so" + manifest.base-nova.lib.ld-nova.mapValue + , manifest.base-nova.bin.nova_timer_drv + , manifest.os.bin.init + , manifest.sotest-producer.bin.sotest-harness + ] + # boot.rom + }