2
0
Fork 0

nova-image: remove Arch union type

This commit is contained in:
Ehmry - 2020-01-27 01:54:43 +01:00
parent 66db226f44
commit 0afe6af54d
5 changed files with 159 additions and 163 deletions

View File

@ -31,7 +31,7 @@ rec {
program = "${drv}/bin/nova-image"; program = "${drv}/bin/nova-image";
function = attrs: bootDesc: function = attrs: bootDesc:
nixpkgs.runCommand "nova-iso" (attrs // { inherit bootDesc; }) nixpkgs.runCommand "nova-iso" (attrs // { inherit bootDesc; })
"${drv}/bin/nova-image $bootDesc > $out"; "XDG_CACHE_HOME=$TMPDIR ${drv}/bin/nova-image $bootDesc > $out";
}; };
nova-iso = let nova-iso = let
@ -44,7 +44,7 @@ rec {
program = "${drv}/bin/nova-iso"; program = "${drv}/bin/nova-iso";
function = attrs: bootDesc: function = attrs: bootDesc:
nixpkgs.runCommand "nova.iso" attrs nixpkgs.runCommand "nova.iso" attrs
''${drv}/bin/nova-iso "${bootDesc}" > $out''; ''XDG_CACHE_HOME=$TMPDIR ${drv}/bin/nova-iso "${bootDesc}" > $out'';
}; };
render-init = render-init =

View File

@ -26,9 +26,9 @@ in nixpkgs.writeScriptBin "nova-image" (with nixpkgs.buildPackages;
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
${dhallApps.dhall.program} text <<< "${ ${dhallApps.dhall.program} text <<< \
./nova-modules.as.dhall "(${./nova-modules.as.dhall}).to32bitImage ($@)" \
} ($@)" > "$TMPDIR/modules.as" > "$TMPDIR/modules.as"
# compile the boot modules into one object file # compile the boot modules into one object file
$CC -c -x assembler -o "$TMPDIR/boot_modules.o" "$TMPDIR/modules.as" $CC -c -x assembler -o "$TMPDIR/boot_modules.o" "$TMPDIR/modules.as"

View File

@ -4,123 +4,119 @@ let Genode = env:DHALL_GENODE
let Prelude = Genode.Prelude let Prelude = Genode.Prelude
let RomMap = Prelude.Map.Type Text Genode.Boot.Rom
let RomEntry = Prelude.Map.Entry Text Genode.Boot.Rom let RomEntry = Prelude.Map.Entry Text Genode.Boot.Rom
let Configuration = let compile =
{ arch : < x86_32 | x86_64 >, config : Genode.Init.Type, rom : RomMap } λ ( addressType
: Type : Text
)
→ λ(boot : Genode.Boot.Type)
→ let NaturalIndex =
{ index : Natural, value : Text }
let TextIndex = { index : Text, value : Text }
let rom =
[ { mapKey = "config"
, mapValue =
Genode.Boot.Rom.RomText (Genode.Init.render boot.config)
}
]
# boot.rom
let moduleKeys = Prelude.Map.keys Text Genode.Boot.Rom rom
let moduleValues =
let f =
λ(e : RomEntry)
→ merge
{ RomText = λ(text : Text) → ".ascii ${Text/show text}"
, RomPath = λ(path : Text) → ".incbin ${Text/show path}"
}
e.mapValue
in Prelude.List.map RomEntry Text f rom
let map =
λ(list : List Text)
→ λ(f : TextIndex → Text)
→ let indexedNatural = Prelude.List.indexed Text list
let indexed =
Prelude.List.map
NaturalIndex
TextIndex
( λ(x : NaturalIndex)
→ { index = Prelude.Natural.show x.index
, value = x.value
}
)
indexedNatural
let texts = Prelude.List.map TextIndex Text f indexed
in Prelude.Text.concatSep "\n" texts
let mapNames = map moduleKeys
let mapValues = map moduleValues
in ''
.set MIN_PAGE_SIZE_LOG2, 12
.set DATA_ACCESS_ALIGNM_LOG2, 3
.section .data
.p2align DATA_ACCESS_ALIGNM_LOG2
.global _boot_modules_headers_begin
_boot_modules_headers_begin:
''
++ mapNames
( λ ( m
: TextIndex
)
→ ''
${addressType} _boot_module_${m.index}_name
${addressType} _boot_module_${m.index}_begin
${addressType} _boot_module_${m.index}_end - _boot_module_${m.index}_begin
''
)
++ ''
.global _boot_modules_headers_end
_boot_modules_headers_end:
''
++ mapNames
( λ(m : TextIndex)
→ ''
.p2align DATA_ACCESS_ALIGNM_LOG2
_boot_module_${m.index}_name:
.string "${m.value}"
.byte 0
''
)
++ ''
.section .data.boot_modules_binaries
.global _boot_modules_binaries_begin
_boot_modules_binaries_begin:
''
++ mapValues
( λ(m : TextIndex)
→ ''
.p2align MIN_PAGE_SIZE_LOG2
_boot_module_${m.index}_begin:
${m.value}
_boot_module_${m.index}_end:
''
)
++ ''
.p2align MIN_PAGE_SIZE_LOG2
.global _boot_modules_binaries_end
_boot_modules_binaries_end:
''
in λ ( boot in { to32bitImage = compile ".long", to64bitImage = compile ".quad" }
: Configuration
)
→ let NaturalIndex =
{ index : Natural, value : Text }
let TextIndex = { index : Text, value : Text }
let rom =
[ { mapKey = "config"
, mapValue =
Genode.Boot.Rom.RomText (Genode.Init.render boot.config)
}
]
# boot.rom
let moduleKeys = Prelude.Map.keys Text Genode.Boot.Rom rom
let moduleValues =
let f =
λ(e : RomEntry)
→ merge
{ RomText = λ(text : Text) → ".ascii ${Text/show text}"
, RomPath = λ(path : Text) → ".incbin ${Text/show path}"
}
e.mapValue
in Prelude.List.map RomEntry Text f rom
let map =
λ(list : List Text)
→ λ(f : TextIndex → Text)
→ let indexedNatural = Prelude.List.indexed Text list
let indexed =
Prelude.List.map
NaturalIndex
TextIndex
( λ(x : NaturalIndex)
→ { index = Prelude.Natural.show x.index
, value = x.value
}
)
indexedNatural
let texts = Prelude.List.map TextIndex Text f indexed
in Prelude.Text.concatSep "\n" texts
let mapNames = map moduleKeys
let mapValues = map moduleValues
let addressType = merge { x86_32 = ".long", x86_64 = ".quad" } boot.arch
in ''
.set MIN_PAGE_SIZE_LOG2, 12
.set DATA_ACCESS_ALIGNM_LOG2, 3
.section .data
.p2align DATA_ACCESS_ALIGNM_LOG2
.global _boot_modules_headers_begin
_boot_modules_headers_begin:
''
++ mapNames
( λ ( m
: TextIndex
)
→ ''
${addressType} _boot_module_${m.index}_name
${addressType} _boot_module_${m.index}_begin
${addressType} _boot_module_${m.index}_end - _boot_module_${m.index}_begin
''
)
++ ''
.global _boot_modules_headers_end
_boot_modules_headers_end:
''
++ mapNames
( λ(m : TextIndex)
→ ''
.p2align DATA_ACCESS_ALIGNM_LOG2
_boot_module_${m.index}_name:
.string "${m.value}"
.byte 0
''
)
++ ''
.section .data.boot_modules_binaries
.global _boot_modules_binaries_begin
_boot_modules_binaries_begin:
''
++ mapValues
( λ(m : TextIndex)
→ ''
.p2align MIN_PAGE_SIZE_LOG2
_boot_module_${m.index}_begin:
${m.value}
_boot_module_${m.index}_end:
''
)
++ ''
.p2align MIN_PAGE_SIZE_LOG2
.global _boot_modules_binaries_end
_boot_modules_binaries_end:
''

View File

@ -2,15 +2,8 @@
let Genode = env:DHALL_GENODE let Genode = env:DHALL_GENODE
let Prelude = Genode.Prelude in λ(args : Genode.Boot.Type)
→ { config =
let RomMap = Prelude.Map.Type Text Genode.Boot.Rom
let Args = { config : Genode.Init.Type, rom : RomMap } : Type
in λ(args : Args)
→ { arch = let Arch = < x86_32 | x86_64 > in Arch.x86_64
, config =
Genode.Init::{ Genode.Init::{
, verbose = True , verbose = True
, defaultRoutes = , defaultRoutes =

View File

@ -2,35 +2,42 @@
let Genode = env:DHALL_GENODE let Genode = env:DHALL_GENODE
in λ ( _ in { config =
: {} Genode.Init::{
) , verbose = True
→ Genode.Init::{ , children =
, verbose = True toMap
, children = { test-libc =
toMap Genode.Init.Start::{
{ test-libc = , binary = "test-libc"
Genode.Init.Start::{ , exitPropagate = True
, binary = "test-libc" , resources = { caps = 200, ram = Genode.units.MiB 400 }
, exitPropagate = True , routes = [ Genode.ServiceRoute.parent "Timer" ]
, resources = { caps = 200, ram = Genode.units.MiB 400 } , config =
, routes = [ Genode.ServiceRoute.parent "Timer" ] Some
, config = ( Genode.Prelude.XML.text
Some ''
( Genode.Prelude.XML.text <config>
'' <vfs>
<config> <dir name="dev">
<vfs> <log/>
<dir name="dev"> <inline name="rtc">2019-08-20 15:01</inline>
<log/> </dir>
<inline name="rtc">2019-08-20 15:01</inline> </vfs>
</dir> <libc stdout="/dev/log" stderr="/dev/log" rtc="/dev/rtc"/>
</vfs> </config>
<libc stdout="/dev/log" stderr="/dev/log" rtc="/dev/rtc"/> ''
</config> )
'' }
) : Genode.Init.Start.Type
} }
: 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
]
}