2
0
Fork 0

Refactor tests to use nested Init/Child type

This commit is contained in:
Ehmry - 2020-02-21 22:55:50 +01:00
parent bfebc6dcef
commit 94868758e5
28 changed files with 541 additions and 510 deletions

View File

@ -4,13 +4,9 @@ let Genode = env:DHALL_GENODE
let Prelude = Genode.Prelude let Prelude = Genode.Prelude
let Args = let Args = { config : Genode.Init.Type, rom : Genode.BootModules.Type } : Type
{ config : Genode.Init.Type
, rom : Genode.Prelude.Map.Type Text Genode.Boot.Rom
}
: Type
let RomEntry = Prelude.Map.Entry Text Genode.Boot.Rom let RomEntry = Prelude.Map.Entry Text Genode.BootModules.ROM.Type
let addLine = let addLine =
λ(e : RomEntry) λ(e : RomEntry)

View File

@ -4,19 +4,21 @@ let Genode = env:DHALL_GENODE
let Prelude = Genode.Prelude let Prelude = Genode.Prelude
let RomEntry = Prelude.Map.Entry Text Genode.Boot.Rom let BootModules = Genode.BootModules
let RomEntry = Prelude.Map.Entry Text BootModules.ROM.Type
let compile = let compile =
λ ( addressType λ ( addressType
: Text : Text
) )
→ λ(rom : Prelude.Map.Type Text Genode.Boot.Rom) → λ(rom : Prelude.Map.Type Text BootModules.ROM.Type)
→ let NaturalIndex = → let NaturalIndex =
{ index : Natural, value : Text } { index : Natural, value : Text }
let TextIndex = { index : Text, value : Text } let TextIndex = { index : Text, value : Text }
let moduleKeys = Prelude.Map.keys Text Genode.Boot.Rom rom let moduleKeys = Prelude.Map.keys Text BootModules.ROM.Type rom
let moduleValues = let moduleValues =
let f = let f =

View File

@ -5,11 +5,8 @@ let Genode = env:DHALL_GENODE
let render = let render =
λ(boot : Genode.Boot.Type) λ(boot : Genode.Boot.Type)
→ let rom = → let rom =
[ { mapKey = "config" Genode.BootModules.toRomTexts
, mapValue = (toMap { config = Genode.Init.render boot.config })
Genode.Boot.Rom.RomText (Genode.Init.render boot.config)
}
]
# boot.rom # boot.rom
in rom in rom

View File

@ -5,6 +5,9 @@ let Genode = env:DHALL_GENODE
let toRom = let toRom =
λ(mapKey : Text) λ(mapKey : Text)
→ λ(path : Text) → λ(path : Text)
→ [ { mapKey = mapKey, mapValue = Genode.Boot.Rom.RomPath path } ] → [ { mapKey = mapKey
, mapValue = Genode.BootModules.ROM.Type.RomPath path
}
]
in toRom in toRom

View File

@ -41,11 +41,17 @@
shellHook = '' shellHook = ''
export DHALL_PRELUDE="${packages.dhallPrelude}/package.dhall" export DHALL_PRELUDE="${packages.dhallPrelude}/package.dhall"
export DHALL_GENODE="${packages.dhallGenode}/package.dhall" export DHALL_GENODE="${packages.dhallGenode}/package.dhall"
export BASE_MANIFEST="${packages.genode.base.manifest}" export MANIFEST="${
export BASE_LINUX_MANIFEST="${packages.genode.base-linux.manifest}" with packages;
export BASE_HW_MANIFEST="${packages.base-hw-pc.manifest}" lib.mergeManifests [
export BASE_NOVA_MANIFEST="${packages.base-nova.manifest}" base-hw-pc
export OS_MANIFEST="${packages.genode.os.manifest}" base-nova
genode.base
genode.base-linux
genode.os
sotest-producer
]
}"
''; '';
}; };

View File

@ -6,8 +6,8 @@ stdenv.mkDerivation {
name = "dhall-genode"; name = "dhall-genode";
src = fetchgit { src = fetchgit {
url = "https://git.sr.ht/~ehmry/dhall-genode"; url = "https://git.sr.ht/~ehmry/dhall-genode";
rev = "472a300141766e58a68b605568eb881e0a944eca"; rev = "8d489b24fad71df04e0facae561bac17a25cb2a5";
sha256 = "03lxxrzyfkgf9c31ds93ndr1bl3a4rlynj377n9rhniz9xzl11y3"; sha256 = "0ngp1ipypf72z7nxsx1xxc051yx3gw7556nfgwsplpxa2y9msp0q";
}; };
DHALL_PRELUDE = prelude + "/package.dhall"; DHALL_PRELUDE = prelude + "/package.dhall";
buildCommand = '' buildCommand = ''

View File

@ -4,6 +4,6 @@ let Genode = env:DHALL_GENODE
let sumRam = let sumRam =
λ(boot : Genode.Boot.Type) λ(boot : Genode.Boot.Type)
→ let sum = Genode.Init.sumResources boot.config in sum.ram → let sum = Genode.Init.resources boot.config in sum.ram
in sumRam in sumRam

View File

@ -21,7 +21,7 @@ let
nova = (call: nova = (call:
((tests call) // { ((tests call) // {
noux = call ./noux.nix { }; # noux = call ./noux.nix { };
pci = call ./pci.nix { }; pci = call ./pci.nix { };
rtc = call ./rtc.nix { }; rtc = call ./rtc.nix { };
})) (import ./driver-nova.nix { })) (import ./driver-nova.nix {
@ -30,6 +30,7 @@ let
hw = (call: hw = (call:
((tests call) // { ((tests call) // {
# noux = call ./noux.nix { };
pci = call ./pci.nix { }; pci = call ./pci.nix { };
rtc = call ./rtc.nix { }; rtc = call ./rtc.nix { };
})) (import ./driver-hw.nix { })) (import ./driver-hw.nix {

View File

@ -2,28 +2,27 @@
let Genode = env:DHALL_GENODE let Genode = env:DHALL_GENODE
let Init = Genode.Init
let Child = Init.Child
let wrapHarness
: Init.Type → Child.Type
= env:DHALL_WRAP_HARNESS ? ./sotest-wrapper.dhall
in λ(boot : Genode.Boot.Type) in λ(boot : Genode.Boot.Type)
→ { config = → { config =
Genode.Init::{ 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 = , children =
[ { mapKey = "timer" [ { mapKey = "timer"
, mapValue = , mapValue =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = "hw_timer_drv" , binary = "hw_timer_drv"
, resources = { caps = 96, ram = Genode.units.MiB 1 }
, provides = [ "Timer" ] , provides = [ "Timer" ]
} }
} }
, { mapKey = "harness" , { mapKey = "harness", mapValue = wrapHarness boot.config }
, mapValue = Genode.Init.toStart boot.config
}
] ]
} }
, rom = , rom =
@ -33,6 +32,7 @@ in λ(boot : Genode.Boot.Type)
[ manifest.base-hw-pc.lib.ld [ manifest.base-hw-pc.lib.ld
, manifest.base-hw-pc.bin.hw_timer_drv , manifest.base-hw-pc.bin.hw_timer_drv
, manifest.os.bin.init , manifest.os.bin.init
, manifest.sotest-producer.bin.sotest-harness
] ]
# boot.rom # boot.rom
} }

View File

@ -34,20 +34,22 @@ let
''; '';
}; };
defaultScript = ''run_genode_until {child "init" exited with exit value 0} 60''; defaultScript = ''run_genode_until {[init] child "harness" exited with exit value 0} 60'';
mkTest = { name ? "unamed", testScript ? defaultScript, testConfig, testInputs ? [ ] mkTest = { name ? "unamed", testScript ? defaultScript, testConfig, testInputs ? [ ]
, env ? { }, ... # TODO: remove ... , env ? { }, ... # TODO: remove ...
}@t: }@t:
let let
testConfig' = "${./driver-hw-config.dhall} (${./sotest-wrapper.dhall} ${testConfig})"; testConfig' = "${./driver-hw-config.dhall} ${testConfig}";
manifest = lib.mergeManifests (with testPkgs; manifest = lib.mergeManifests (with testPkgs;
[ base-hw-pc genode.os sotest-producer ] [ base-hw-pc genode.os sotest-producer ]
++ testInputs); ++ testInputs);
env' = { env' = {
DHALL_PRELUDE = "${testPkgs.dhallPrelude}/package.dhall"; DHALL_PRELUDE = "${testPkgs.dhallPrelude}/package.dhall";
DHALL_GENODE = "${testPkgs.dhallGenode}/package.dhall"; DHALL_GENODE = "${testPkgs.dhallGenode}/package.dhall";
DHALL_WRAP_HARNESS = ./sotest-wrapper.dhall;
MANIFEST = manifest; MANIFEST = manifest;
XDG_CACHE_HOME = "/tmp";
} // env; } // env;
image = apps.hw-image.function env' testConfig'; image = apps.hw-image.function env' testConfig';
@ -91,7 +93,7 @@ let
global env global env
global spawn_id global spawn_id
set TEST_MIB [expr ($env(TEST_RAM) / 1048576) + 12] set TEST_MIB [expr ($env(TEST_RAM) / 1048576) + 16]
spawn ${hostPkgs.qemu_test}/bin/qemu-system-x86_64 \ spawn ${hostPkgs.qemu_test}/bin/qemu-system-x86_64 \
-machine q35 -serial mon:stdio -nographic \ -machine q35 -serial mon:stdio -nographic \
-m size=$TEST_MIB \ -m size=$TEST_MIB \
@ -112,6 +114,7 @@ let
preferLocalBuild = true; preferLocalBuild = true;
testName = name; testName = name;
DHALL_GENODE = "${testPkgs.dhallGenode}/package.dhall"; DHALL_GENODE = "${testPkgs.dhallGenode}/package.dhall";
DHALL_WRAP_HARNESS = ./sotest-wrapper.dhall;
MANIFEST = manifest; MANIFEST = manifest;
} '' } ''
mkdir -p $out/bin mkdir -p $out/bin
@ -135,14 +138,12 @@ let
inherit driver image test manifest; inherit driver image test manifest;
config = hostPkgs.runCommand (name + ".dhall") env' '' config = hostPkgs.runCommand (name + ".dhall") env' ''
export XDG_CACHE_HOME=''${TMPDIR:-/tmp}
${apps.dhall.program} <<< "${testConfig'}" > $out ${apps.dhall.program} <<< "${testConfig'}" > $out
''; '';
iso = apps.hw-iso.function env' testConfig'; iso = apps.hw-iso.function env' testConfig';
xml = hostPkgs.runCommand (name + ".config") env' '' xml = hostPkgs.runCommand (name + ".config") env' ''
export XDG_CACHE_HOME=''${TMPDIR:-/tmp}
${apps.render-init.program} "(${testConfig'}).config" > $out''; ${apps.render-init.program} "(${testConfig'}).config" > $out'';
sotest = hostPkgs.runCommand "hw-${name}-sotest" env' '' sotest = hostPkgs.runCommand "hw-${name}-sotest" env' ''

View File

@ -1,36 +1,41 @@
-- SPDX-License-Identifier: CC0-1.0 -- SPDX-License-Identifier: CC0-1.0
let Genode = env:DHALL_GENODE let Genode = env:DHALL_GENODE
let Init = Genode.Init
let Child = Init.Child
let wrapHarness
: Init.Type → Child.Type
= env:DHALL_WRAP_HARNESS ? ./sotest-wrapper.dhall
let Child = Genode.Init.Child
in λ(boot : Genode.Boot.Type) in λ(boot : Genode.Boot.Type)
→ { config = → { config =
Genode.Init::{ Genode.Init::{
, verbose = True
, defaultRoutes =
Genode.Init.default.defaultRoutes
# [ Genode.ServiceRoute.child "Timer" "timer" ]
, children = , children =
[ { mapKey = "timer" [ { mapKey = "timer"
, mapValue = , mapValue =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = "linux_timer_drv" , binary = "linux_timer_drv"
, resources = { caps = 96, ram = Genode.units.MiB 1 }
, provides = [ "Timer" ] , provides = [ "Timer" ]
} }
} }
, { mapKey = "harness" , { mapKey = "harness", mapValue = wrapHarness boot.config }
, mapValue = Genode.Init.toStart boot.config
}
] ]
} }
, rom = , rom =
let manifest = env:MANIFEST let manifest = env:MANIFEST
in Genode.Boot.toRomPaths in Genode.BootModules.toRomPaths
[ manifest.base-linux.bin.core-linux [ manifest.base-linux.bin.core-linux
, manifest.base-linux.bin.ld , manifest.base-linux.bin.ld
, manifest.base-linux.bin.linux_timer_drv , manifest.base-linux.bin.linux_timer_drv
, manifest.os.bin.init , manifest.os.bin.init
, manifest.sotest-producer.bin.sotest-harness
] ]
# boot.rom # boot.rom
: Genode.Prelude.Map.Type Text Genode.Boot.Rom : Genode.BootModules.Type
} }

View File

@ -38,11 +38,14 @@ let
, env ? { }, ... }: , env ? { }, ... }:
with testPkgs; with testPkgs;
let let
testConfig' = "${./driver-linux-config.dhall} ${testConfig}";
env' = { env' = {
DHALL_PRELUDE = "${testPkgs.dhallPrelude}/package.dhall"; DHALL_PRELUDE = "${testPkgs.dhallPrelude}/package.dhall";
DHALL_GENODE = "${testPkgs.dhallGenode}/package.dhall"; DHALL_GENODE = "${testPkgs.dhallGenode}/package.dhall";
DHALL_WRAP_HARNESS = ./sotest-wrapper.dhall;
MANIFEST = lib.mergeManifests (with testPkgs; MANIFEST = lib.mergeManifests (with testPkgs;
[ genode.base-linux genode.os sotest-producer ] ++ testInputs); [ genode.base-linux genode.os sotest-producer ] ++ testInputs);
XDG_CACHE_HOME = "/tmp";
} // env; } // env;
toExports = env: toExports = env:
@ -70,8 +73,7 @@ let
global env global env
set env(XDG_CACHE_HOME) /tmp set env(XDG_CACHE_HOME) /tmp
exec ${apps.linux-image.program} \ exec ${apps.linux-image.program} ${testConfig'}
${./driver-linux-config.dhall} (${./sotest-wrapper.dhall} ${testConfig})
spawn ./core-linux spawn ./core-linux
wait_for_output $wait_for_re $timeout_value $spawn_id wait_for_output $wait_for_re $timeout_value $spawn_id
@ -81,7 +83,7 @@ let
driver = with hostPkgs; driver = with hostPkgs;
runCommand "genode-test-driver-${name}" { runCommand "genode-test-driver-${name}" {
buildInputs = [ makeWrapper expect ]; buildInputs = [ makeWrapper expect ];
inherit baseSetup testConfig testScript; inherit baseSetup testScript;
preferLocalBuild = true; preferLocalBuild = true;
testName = name; testName = name;
} '' } ''
@ -99,18 +101,15 @@ let
in test // { in test // {
inherit driver test; inherit driver test;
config = hostPkgs.runCommand (name + ".dhall") env' '' config = hostPkgs.runCommand (name + ".dhall") env' ''
${apps.dhall.program} <<< \ ${apps.dhall.program} <<< "(${testConfig'}).config" > $out
"(${./driver-linux-config.dhall} ${testConfig})" > $out
''; '';
xml = hostPkgs.runCommand (name + ".config") env' '' xml = hostPkgs.runCommand (name + ".config") env' ''
${apps.render-init.program} \ ${apps.render-init.program} "(${testConfig'}).config" > $out
"(${./driver-linux-config.dhall} ${testConfig}).config" > $out
''; '';
image = hostPkgs.runCommand (name + ".config") env' '' image = hostPkgs.runCommand (name + ".image.elf") env' ''
mkdir -p $out mkdir -p $out
pushd $out pushd $out
${apps.linux-image.program} \ ${apps.linux-image.program} "${testConfig'}"
"${./driver-linux-config.dhall} ${testConfig}"
''; '';
}; };

View File

@ -2,28 +2,27 @@
let Genode = env:DHALL_GENODE let Genode = env:DHALL_GENODE
let Init = Genode.Init
let Child = Init.Child
let wrapHarness
: Init.Type → Child.Type
= env:DHALL_WRAP_HARNESS ? ./sotest-wrapper.dhall
in λ(boot : Genode.Boot.Type) in λ(boot : Genode.Boot.Type)
→ { config = → { config =
Genode.Init::{ 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 = , children =
[ { mapKey = "timer" [ { mapKey = "timer"
, mapValue = , mapValue =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = "nova_timer_drv" , binary = "nova_timer_drv"
, resources = { caps = 96, ram = Genode.units.MiB 1 }
, provides = [ "Timer" ] , provides = [ "Timer" ]
} }
} }
, { mapKey = "harness" , { mapKey = "harness", mapValue = wrapHarness boot.config }
, mapValue = Genode.Init.toStart boot.config
}
] ]
} }
, rom = , rom =
@ -33,6 +32,7 @@ in λ(boot : Genode.Boot.Type)
[ manifest.base-nova.lib.ld [ manifest.base-nova.lib.ld
, manifest.base-nova.bin.nova_timer_drv , manifest.base-nova.bin.nova_timer_drv
, manifest.os.bin.init , manifest.os.bin.init
, manifest.sotest-producer.bin.sotest-harness
] ]
# boot.rom # boot.rom
} }

View File

@ -34,20 +34,22 @@ let
''; '';
}; };
defaultScript = ''run_genode_until {child "init" exited with exit value 0} 60''; defaultScript = ''run_genode_until {[init] child "harness" exited with exit value 0} 60'';
mkTest = { name ? "unamed", testScript ? defaultScript, testConfig, testInputs ? [ ] mkTest = { name ? "unamed", testScript ? defaultScript, testConfig, testInputs ? [ ]
, env ? { }, ... # TODO: remove ... , env ? { }, ... # TODO: remove ...
}@t: }@t:
let let
testConfig' = "${./driver-nova-config.dhall} (${./sotest-wrapper.dhall} ${testConfig})"; testConfig' = "${./driver-nova-config.dhall} ${testConfig}";
manifest = lib.mergeManifests (with testPkgs; manifest = lib.mergeManifests (with testPkgs;
[ base-nova genode.os sotest-producer ] [ base-nova genode.os sotest-producer ]
++ testInputs); ++ testInputs);
env' = { env' = {
DHALL_PRELUDE = "${testPkgs.dhallPrelude}/package.dhall"; DHALL_PRELUDE = "${testPkgs.dhallPrelude}/package.dhall";
DHALL_GENODE = "${testPkgs.dhallGenode}/package.dhall"; DHALL_GENODE = "${testPkgs.dhallGenode}/package.dhall";
DHALL_WRAP_HARNESS = ./sotest-wrapper.dhall;
MANIFEST = manifest; MANIFEST = manifest;
XDG_CACHE_HOME = "/tmp";
} // env; } // env;
image = apps.nova-image.function env' testConfig'; image = apps.nova-image.function env' testConfig';
@ -112,6 +114,7 @@ let
preferLocalBuild = true; preferLocalBuild = true;
testName = name; testName = name;
DHALL_GENODE = "${testPkgs.dhallGenode}/package.dhall"; DHALL_GENODE = "${testPkgs.dhallGenode}/package.dhall";
DHALL_WRAP_HARNESS = ./sotest-wrapper.dhall;
MANIFEST = manifest; MANIFEST = manifest;
} '' } ''
mkdir -p $out/bin mkdir -p $out/bin
@ -142,7 +145,6 @@ let
iso = apps.nova-iso.function env' "${testConfig'}"; iso = apps.nova-iso.function env' "${testConfig'}";
xml = hostPkgs.runCommand (name + ".config") env' '' xml = hostPkgs.runCommand (name + ".config") env' ''
export XDG_CACHE_HOME=''${TMPDIR:-/tmp}
${apps.render-init.program} "(${testConfig'}).config" > $out''; ${apps.render-init.program} "(${testConfig'}).config" > $out'';
sotest = hostPkgs.runCommand "nova-${name}-sotest" env' '' sotest = hostPkgs.runCommand "nova-${name}-sotest" env' ''

View File

@ -1,43 +0,0 @@
-- SPDX-License-Identifier: CC0-1.0
let Genode = env:DHALL_GENODE
in { config =
Genode.Init::{
, verbose = True
, children =
toMap
{ test-libc =
Genode.Init.Start::{
, binary = "test-libc"
, exitPropagate = True
, resources = { caps = 200, ram = Genode.units.MiB 400 }
, routes = [ Genode.ServiceRoute.parent "Timer" ]
, config =
Some
( Genode.Prelude.XML.text
''
<config>
<vfs>
<dir name="dev">
<log/>
<inline name="rtc">2019-08-20 15:01</inline>
</dir>
</vfs>
<libc stdout="/dev/log" stderr="/dev/log" rtc="/dev/rtc"/>
</config>
''
)
}
: Genode.Init.Start.Type
}
}
, rom =
let manifest = env:MANIFEST
in Genode.Boot.toRomPaths
[ manifest.libc.lib.libc
manifest.libc.lib.libm
manifest.test-libc.bin.test-libc
]
}

View File

@ -2,17 +2,23 @@
let Genode = env:DHALL_GENODE let Genode = env:DHALL_GENODE
let Child = Genode.Init.Child
in { config = in { config =
Genode.Init::{ Genode.Init::{
, verbose = True
, children = , children =
toMap toMap
{ test-log = { test-log =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = "test-log" , binary = "test-log"
, exitPropagate = True , exitPropagate = True
, resources = { caps = 500, ram = Genode.units.MiB 10 } , resources =
, routes = [ Genode.ServiceRoute.parent "Timer" ] Genode.Init.Resources::{
, caps = 500
, ram = Genode.units.MiB 10
}
, routes = [ Genode.Init.ServiceRoute.parent "Timer" ]
} }
} }
} }

View File

@ -2,22 +2,34 @@
let Genode = env:DHALL_GENODE let Genode = env:DHALL_GENODE
let Child = Genode.Init.Child
in { config = in { config =
Genode.Init::{ Genode.Init::{
, verbose = True
, children = , children =
toMap toMap
{ noux = { noux =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = "noux" , binary = "noux"
, exitPropagate = True , exitPropagate = True
, resources = { caps = 500, ram = Genode.units.MiB 10 } , resources =
, routes = [ Genode.ServiceRoute.parent "Timer" ] Genode.Init.Resources::{
, caps = 500
, ram = Genode.units.MiB 10
}
, routes = [ Genode.Init.ServiceRoute.parent "Timer" ]
, config = , config =
Some Genode.Init.Config::{
( Genode.Prelude.XML.text , attributes =
toMap
{ stdin = "/script"
, stdout = "/dev/log"
, stderr = "/dev/log"
}
, content =
[ Genode.Prelude.XML.text
'' ''
<config stdin="/script" stdout="/dev/log" stderr="/dev/log">
<fstab> <fstab>
<tar name="bash-minimal.tar" /> <tar name="bash-minimal.tar" />
<dir name="dev"> <log/> <null/> <zero/> </dir> <dir name="dev"> <log/> <null/> <zero/> </dir>
@ -29,9 +41,9 @@ in { config =
<start name="/bin/bash"> <start name="/bin/bash">
<env name="TERM" value="screen" /> <env name="TERM" value="screen" />
</start> </start>
</config>
'' ''
) ]
}
} }
} }
} }

View File

@ -2,74 +2,94 @@
let Genode = env:DHALL_GENODE let Genode = env:DHALL_GENODE
let XML = Genode.Prelude.XML
let Init = Genode.Init
let Child = Init.Child
let Resources = Init.Resources
let ServiceRoute = Init.ServiceRoute
in { config = in { config =
Genode.Init::{ Init::{
, verbose = True , verbose = True
, children = , children =
toMap toMap
{ test-pci = { test-pci =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = "test-pci" , binary = "test-pci"
, exitPropagate = True , exitPropagate = True
, resources = { caps = 96, ram = Genode.units.MiB 3 } , resources = Resources::{ ram = Genode.units.MiB 3 }
, routes = , routes = [ ServiceRoute.child "Platform" "platform_drv" ]
[ Genode.ServiceRoute.child "Platform" "platform_drv" ]
} }
, acpi_report_rom = , acpi_report_rom =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = "report_rom" , binary = "report_rom"
, resources = { caps = 96, ram = Genode.units.MiB 2 }
, provides = [ "ROM", "Report" ] , provides = [ "ROM", "Report" ]
, config = , config =
Some Init.Config::{
( Genode.Prelude.XML.text , content =
[ XML.text
'' ''
<config system="yes">
<policy label="smbios_decoder -> smbios_table" report="acpi_drv -> smbios_table"/> <policy label="smbios_decoder -> smbios_table" report="acpi_drv -> smbios_table"/>
<policy label="platform_drv -> acpi" report="acpi_drv -> acpi"/> <policy label="platform_drv -> acpi" report="acpi_drv -> acpi"/>
</config>
'' ''
) ]
}
} }
, acpi_drv = , acpi_drv =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = "acpi_drv" , binary = "acpi_drv"
, resources = { caps = 400, ram = Genode.units.MiB 4 } , resources =
Resources::{
, caps = 400
, ram = Genode.units.MiB 4
, constrainPhys = True , constrainPhys = True
}
, provides = [ "Platform", "Acpi" ] , provides = [ "Platform", "Acpi" ]
, routes = , routes =
[ Genode.ServiceRoute.child "Report" "acpi_report_rom" [ ServiceRoute.child "Report" "acpi_report_rom"
, Genode.ServiceRoute.parent "IRQ" , ServiceRoute.parent "IRQ"
, Genode.ServiceRoute.parent "IO_MEM" , ServiceRoute.parent "IO_MEM"
, Genode.ServiceRoute.parent "IO_PORT" , ServiceRoute.parent "IO_PORT"
] ]
} }
, platform_drv = , platform_drv =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = "platform_drv" , binary = "platform_drv"
, resources = { caps = 800, ram = Genode.units.MiB 4 } , resources =
Resources::{
, caps = 800
, ram = Genode.units.MiB 4
, constrainPhys = True , constrainPhys = True
}
, provides = [ "Platform", "Acpi" ] , provides = [ "Platform", "Acpi" ]
, routes = , routes =
[ Genode.ServiceRoute.parent "Timer" [ ServiceRoute.parent "Timer"
, Genode.ServiceRoute.parent "IRQ" , ServiceRoute.parent "IRQ"
, Genode.ServiceRoute.parent "IO_MEM" , ServiceRoute.parent "IO_MEM"
, Genode.ServiceRoute.parent "IO_PORT" , ServiceRoute.parent "IO_PORT"
, Genode.ServiceRoute.childLabel , ServiceRoute.childLabel
"ROM" "ROM"
"acpi_report_rom" "acpi_report_rom"
(Some "acpi") (Some "acpi")
(None Text) (None Text)
] ]
, config = , config =
Some Init.Config::{
( Genode.Prelude.XML.text , content =
[ XML.text
'' ''
<config>
<policy label_prefix="test-pci"> <pci class="ALL"/> </policy> <policy label_prefix="test-pci"> <pci class="ALL"/> </policy>
</config>
'' ''
) ]
}
} }
} }
} }

View File

@ -2,26 +2,28 @@
let Genode = env:DHALL_GENODE let Genode = env:DHALL_GENODE
let Child = Genode.Init.Child
in { config = in { config =
Genode.Init::{ Genode.Init::{
, verbose = True
, children = , children =
toMap toMap
{ test-rtc = { test-rtc =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = "test-rtc" , binary = "test-rtc"
, resources = { caps = 128, ram = Genode.units.MiB 2 }
, exitPropagate = True , exitPropagate = True
, routes = , routes =
[ Genode.ServiceRoute.parent "Timer" [ Genode.Init.ServiceRoute.parent "Timer"
, Genode.ServiceRoute.child "Rtc" "rtc_drv" , Genode.Init.ServiceRoute.child "Rtc" "rtc_drv"
] ]
} }
, rtc_drv = , rtc_drv =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = "rtc_drv" , binary = "rtc_drv"
, provides = [ "Rtc" ] , provides = [ "Rtc" ]
, routes = [ Genode.ServiceRoute.parent "IO_PORT" ] , routes = [ Genode.Init.ServiceRoute.parent "IO_PORT" ]
} }
} }
} }

View File

@ -2,16 +2,26 @@
let Genode = env:DHALL_GENODE let Genode = env:DHALL_GENODE
let Init = Genode.Init
let Child = Init.Child
in { config = in { config =
Genode.Init::{ Init::{
, verbose = True
, children = , children =
toMap toMap
{ test-signal = { test-signal =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = "test-signal" , binary = "test-signal"
, exitPropagate = True , exitPropagate = True
, resources = { caps = 500, ram = Genode.units.MiB 10 } , priority = 5
, resources =
Init.Resources::{
, caps = 500
, ram = Genode.units.MiB 10
}
, routes = [ Init.ServiceRoute.parent "Timer" ]
} }
} }
} }

View File

@ -2,38 +2,45 @@
let Genode = env:DHALL_GENODE let Genode = env:DHALL_GENODE
let manifest = env:MANIFEST let Init = Genode.Init
let Child = Init.Child
in { config = in { config =
Genode.Init::{ Init::{
, children = , children =
toMap toMap
{ solo5 = { solo5 =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = "solo5-test_blk" , binary = "solo5-test_blk"
, exitPropagate = True , exitPropagate = True
, resources = { caps = 256, ram = Genode.units.MiB 3 } , resources =
Init.Resources::{ caps = 256, ram = Genode.units.MiB 3 }
, routes = , routes =
[ Genode.ServiceRoute.parent "Timer" [ Init.ServiceRoute.parent "Timer"
, Genode.ServiceRoute.child "Block" "block" , Init.ServiceRoute.child "Block" "block"
] ]
} }
, block = , block =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = "ram_block" , binary = "ram_block"
, provides = [ "Block" ] , provides = [ "Block" ]
, resources = { caps = 96, ram = Genode.units.MiB 9 } , resources = Init.Resources::{ ram = Genode.units.MiB 9 }
, config = , config =
Some Init.Config::{
( Genode.Prelude.XML.text , attributes =
'' toMap { size = "8M", block_size = "4096" }
<config size="8M" block_size="4096"/> }
''
)
} }
} }
} }
, rom = , rom =
Genode.Boot.toRomPaths let manifest = env:MANIFEST
[ manifest.solo5-tests.bin.solo5-test_blk, manifest.os.bin.ram_block ]
in Genode.BootModules.toRomPaths
[ manifest.solo5-tests.bin.solo5-test_blk
, manifest.os.bin.ram_block
]
} }

View File

@ -2,12 +2,9 @@
let Genode = env:DHALL_GENODE let Genode = env:DHALL_GENODE
let RomMap = Genode.Prelude.Map.Type Text Genode.Boot.Rom in λ(boot : Genode.Boot.Type)
let Args = { config : Genode.Init.Type, rom : RomMap } : Type
in λ(boot : Args)
→ { config = boot.config → { config = boot.config
, rom = , rom =
Genode.Boot.toRomPaths [ (env:MANIFEST).solo5.lib.solo5 ] # boot.rom Genode.BootModules.toRomPaths [ (env:MANIFEST).solo5.lib.solo5 ]
# boot.rom
} }

View File

@ -50,17 +50,11 @@ let
{ {
name = "net"; name = "net";
testConfig = ./net.dhall; testConfig = ./net.dhall;
testScript = ''
run_genode_until {child "init" exited with exit value 0} 30
'';
} }
{ {
name = "net_2if"; name = "net_2if";
testConfig = ./net_2if.dhall; testConfig = ./net_2if.dhall;
testScript = ''
run_genode_until {child "init" exited with exit value 0} 30
'';
} }
{ {

View File

@ -2,61 +2,71 @@
let Genode = env:DHALL_GENODE let Genode = env:DHALL_GENODE
let manifest = env:MANIFEST let Init = Genode.Init
let Child = Init.Child
let Res = Init.Resources
let ServiceRoute = Init.ServiceRoute
in { config = in { config =
Genode.Init::{ Init::{
, children = , children =
toMap toMap
{ nic = { nic =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = "nic_loopback" , binary = "nic_loopback"
, provides = [ "Nic" ] , provides = [ "Nic" ]
} }
, bridge = , bridge =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = "nic_bridge" , binary = "nic_bridge"
, resources = { caps = 200, ram = Genode.units.MiB 6 } , resources = Res::{ caps = 200, ram = Genode.units.MiB 6 }
, provides = [ "Nic" ] , provides = [ "Nic" ]
, routes = [ Genode.ServiceRoute.child "Nic" "nic" ] , routes = [ ServiceRoute.child "Nic" "nic" ]
, config = , config =
Some Init.Config::{
( Genode.Prelude.XML.text , attributes = toMap { mac = "02:02:02:02:03:00" }
, content =
[ Genode.Prelude.XML.text
'' ''
<config mac="02:02:02:02:03:00" verbose="no">
<policy label_prefix="solo5" ip_addr="10.0.0.2"/> <policy label_prefix="solo5" ip_addr="10.0.0.2"/>
<default-policy/> <default-policy/>
</config>
'' ''
) ]
}
} }
, solo5 = , solo5 =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = "solo5-test_net" , binary = "solo5-test_net"
, resources = { caps = 256, ram = Genode.units.MiB 3 } , resources = Res::{ caps = 256, ram = Genode.units.MiB 3 }
, routes = , routes =
[ Genode.ServiceRoute.parent "Timer" [ ServiceRoute.parent "Timer"
, Genode.ServiceRoute.child "Nic" "bridge" , ServiceRoute.child "Nic" "bridge"
] ]
, config = , config =
Some Init.Config::{
( Genode.Prelude.XML.text , content =
"<config><cmdline>limit</cmdline></config>" [ Genode.Prelude.XML.text "<cmdline>limit</cmdline>"
) ]
}
} }
, ping = , ping =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = "ping" , binary = "ping"
, exitPropagate = True , exitPropagate = True
, resources = { caps = 128, ram = Genode.units.MiB 6 } , resources = Res::{ caps = 128, ram = Genode.units.MiB 6 }
, routes = , routes =
[ Genode.ServiceRoute.parent "Timer" [ ServiceRoute.parent "Timer"
, Genode.ServiceRoute.child "Nic" "bridge" , ServiceRoute.child "Nic" "bridge"
] ]
, config = , config =
Some Init.Config::{
( Genode.Prelude.XML.leaf
{ name = "config"
, attributes = , attributes =
toMap toMap
{ interface = "10.0.0.72/24" { interface = "10.0.0.72/24"
@ -65,12 +75,13 @@ in { config =
, verbose = "no" , verbose = "no"
} }
} }
)
} }
} }
} }
, rom = , rom =
Genode.Boot.toRomPaths let manifest = env:MANIFEST
in Genode.BootModules.toRomPaths
[ manifest.os.bin.nic_loopback [ manifest.os.bin.nic_loopback
, manifest.os.bin.nic_bridge , manifest.os.bin.nic_bridge
, manifest.os.bin.ping , manifest.os.bin.ping

View File

@ -2,65 +2,75 @@
let Genode = env:DHALL_GENODE let Genode = env:DHALL_GENODE
let manifest = env:MANIFEST let Init = Genode.Init
let Child = Init.Child
let Res = Init.Resources
in { config = in { config =
Genode.Init::{ Init::{
, children = , children =
toMap toMap
{ nic = { nic =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = "nic_loopback" , binary = "nic_loopback"
, provides = [ "Nic" ] , provides = [ "Nic" ]
} }
, bridge = , bridge =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = "nic_bridge" , binary = "nic_bridge"
, resources = { caps = 200, ram = Genode.units.MiB 8 } , resources = Res::{ caps = 200, ram = Genode.units.MiB 8 }
, provides = [ "Nic" ] , provides = [ "Nic" ]
, routes = [ Genode.ServiceRoute.child "Nic" "nic" ] , routes = [ Genode.Init.ServiceRoute.child "Nic" "nic" ]
, config = , config =
Some Init.Config::{
( Genode.Prelude.XML.text , content =
[ Genode.Prelude.XML.text
'' ''
<config mac="02:02:02:02:03:00" verbose="no">
<policy label="solo5 -> service0" ip_addr="10.0.0.2"/> <policy label="solo5 -> service0" ip_addr="10.0.0.2"/>
<policy label="solo5 -> service1" ip_addr="10.1.0.2"/> <policy label="solo5 -> service1" ip_addr="10.1.0.2"/>
<default-policy/> <default-policy/>
</config>
'' ''
) ]
}
} }
, solo5 = , solo5 =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = "solo5-test_net_2if" , binary = "solo5-test_net_2if"
, resources = { caps = 256, ram = Genode.units.MiB 5 } , resources = Res::{ caps = 256, ram = Genode.units.MiB 5 }
, routes = , routes =
[ Genode.ServiceRoute.parent "Timer" [ Genode.Init.ServiceRoute.parent "Timer"
, Genode.ServiceRoute.child "Nic" "bridge" , Genode.Init.ServiceRoute.child "Nic" "bridge"
] ]
, config = , config =
Some Init.Config::{
( Genode.Prelude.XML.text , content =
[ Genode.Prelude.XML.text
'' ''
<config><cmdline>limit</cmdline></config> "<cmdline>limit</cmdline>"
'' ''
) ]
}
} }
, clients = , clients =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = "sequence" , binary = "sequence"
, exitPropagate = True , exitPropagate = True
, resources = { caps = 256, ram = Genode.units.MiB 8 } , resources = Res::{ caps = 256, ram = Genode.units.MiB 8 }
, routes = , routes =
[ Genode.ServiceRoute.parent "Timer" [ Genode.Init.ServiceRoute.parent "Timer"
, Genode.ServiceRoute.child "Nic" "bridge" , Genode.Init.ServiceRoute.child "Nic" "bridge"
] ]
, config = , config =
Some Init.Config::{
( Genode.Prelude.XML.text , content =
[ Genode.Prelude.XML.text
'' ''
<config>
<start name="ping0"> <start name="ping0">
<binary name="ping"/> <binary name="ping"/>
<config interface="10.0.0.72/24" dst_ip="10.0.0.2" period_sec="1" count="4"/> <config interface="10.0.0.72/24" dst_ip="10.0.0.2" period_sec="1" count="4"/>
@ -69,14 +79,16 @@ in { config =
<binary name="ping"/> <binary name="ping"/>
<config interface="10.1.0.72/24" dst_ip="10.1.0.2" period_sec="1" count="4"/> <config interface="10.1.0.72/24" dst_ip="10.1.0.2" period_sec="1" count="4"/>
</start> </start>
</config>
'' ''
) ]
}
} }
} }
} }
, rom = , rom =
Genode.Boot.toRomPaths let manifest = env:MANIFEST
in Genode.BootModules.toRomPaths
[ manifest.solo5-tests.bin.solo5-test_net_2if [ manifest.solo5-tests.bin.solo5-test_net_2if
, manifest.os.bin.sequence , manifest.os.bin.sequence
, manifest.os.bin.nic_bridge , manifest.os.bin.nic_bridge

View File

@ -2,37 +2,42 @@
let Genode = env:DHALL_GENODE let Genode = env:DHALL_GENODE
in λ(testBinary : Genode.Prelude.Map.Entry Text Text) let Prelude = Genode.Prelude
let Init = Genode.Init
let Child = Init.Child
let Config = Init.Config
in λ(testBinary : Prelude.Map.Entry Text Text)
→ { config = → { config =
Genode.Init::{ Init::{
, children = , children =
toMap toMap
{ solo5 = { solo5 =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = testBinary.mapKey , binary = testBinary.mapKey
, exitPropagate = True , exitPropagate = True
, resources = { caps = 256, ram = Genode.units.MiB 3 } , resources =
Init.Resources::{
, caps = 256
, ram = Genode.units.MiB 3
}
, config = , config =
Some Config::{
( Genode.Prelude.XML.element
{ name = "config"
, attributes =
[] : Genode.Prelude.Map.Type Text Text
, content = , content =
[ Genode.Prelude.XML.element [ Prelude.XML.element
{ name = "cmdline" { name = "cmdline"
, attributes = , attributes = Prelude.XML.emptyAttributes
[] : Genode.Prelude.Map.Type Text Text , content = [ Prelude.XML.text "Hello_Solo5" ]
, content =
[ Genode.Prelude.XML.text
"Hello_Solo5"
]
} }
] ]
} }
) , routes = [ Init.ServiceRoute.parent "Timer" ]
} }
} }
} }
, rom = Genode.Boot.toRomPaths [ testBinary ] , rom = Genode.BootModules.toRomPaths [ testBinary ]
} }

View File

@ -2,31 +2,41 @@
let Genode = env:DHALL_GENODE let Genode = env:DHALL_GENODE
let manifest = env:MANIFEST let Child = Genode.Init.Child
let test = manifest.solo5-tests.bin.solo5-test_time
in { config = in { config =
Genode.Init::{ Genode.Init::{
, children = , children =
toMap toMap
{ solo5 = { solo5 =
Genode.Init.Start::{ Child.flat
, binary = test.mapKey Child.Attributes::{
, binary = "solo5-test_time"
, exitPropagate = True , exitPropagate = True
, resources = { caps = 256, ram = Genode.units.MiB 3 } , resources =
Genode.Init.Resources::{
, caps = 256
, ram = Genode.units.MiB 3
}
, routes = , routes =
[ Genode.ServiceRoute.parent "Timer" [ Genode.Init.ServiceRoute.parent "Timer"
, Genode.ServiceRoute.child "Rtc" "clock" , Genode.Init.ServiceRoute.child "Rtc" "clock"
] ]
} }
, clock = , clock =
Genode.Init.Start::{ Child.flat
Child.Attributes::{
, binary = "rtc_drv" , binary = "rtc_drv"
, provides = [ "Rtc" ] , provides = [ "Rtc" ]
, routes = [ Genode.ServiceRoute.parent "IO_PORT" ] , routes = [ Genode.Init.ServiceRoute.parent "IO_PORT" ]
} }
} }
} }
, rom = Genode.Boot.toRomPaths [ test, manifest.os.bin.rtc_drv ] , rom =
let manifest = env:MANIFEST
in Genode.BootModules.toRomPaths
[ manifest.solo5-tests.bin.solo5-test_time
, manifest.os.bin.rtc_drv
]
} }

View File

@ -1,53 +1,29 @@
-- SPDX-License-Identifier: CC0-1.0 -- SPDX-License-Identifier: CC0-1.0
let Genode = env:DHALL_GENODE let Genode = env:DHALL_GENODE
let Prelude = Genode.Prelude let Init = Genode.Init
in λ(boot : Genode.Boot.Type) let Child = Init.Child
→ let child =
{ mapKey = "test", mapValue = Genode.Init.toStart boot.config }
in { config = let wrapSotest
Genode.Init::{ : Init.Type → Child.Type
, verbose = True = λ(init : Init.Type)
, children = → Child.nested
toMap (toMap { init = Genode.Init.toChild init Init.Attributes.default })
{ harness = Child.Attributes::{
Genode.Init.Start::{
, binary = "sotest-harness" , binary = "sotest-harness"
, exitPropagate = True , resources = Init.Resources::{ ram = Genode.units.MiB 4 }
, resources =
{ caps = child.mapValue.resources.caps + 128
, ram =
child.mapValue.resources.ram
+ Genode.units.MiB 1
}
, config =
Some
( Prelude.XML.element
{ name = "config"
, attributes = Prelude.XML.emptyAttributes
, content =
[ Genode.Init.Start.toXML
child.mapKey
child.mapValue
]
}
)
, routes = , routes =
[ Genode.ServiceRoute.parentLabel [ Init.ServiceRoute.parentLabel
"LOG" "LOG"
(Some "SOTEST") (Some "SOTEST")
(Some "unlabeled") (Some "unlabeled")
, Init.ServiceRoute.parent "IO_MEM"
, Init.ServiceRoute.parent "IO_PORT"
, Init.ServiceRoute.parent "IRQ"
, Init.ServiceRoute.child "Timer" "timer"
] ]
} }
}
}
, rom =
let manifest = env:MANIFEST
in Genode.Boot.toRomPaths in wrapSotest
[ manifest.sotest-producer.bin.sotest-harness ]
# boot.rom
: Genode.Prelude.Map.Type Text Genode.Boot.Rom
}