Hello,

LANG=en_US.UTF-8 ./init --tut hello-camkes-0

or

LANGUAGE=en_US.UTF-8 ./init --tut hello-camkes-0

did not work.

Seems I was able to resolve this with the following commands:

update-locale LANG=en_US.UTF-8
dpkg-reconfigure locales
update-locale LANG=en_US.UTF-8
export LANG=en_US.UTF-8

After the project built successfully, I tired executing ./simulate and I got 
the following assertion:

Assertion failed: free_slot_end - free_slot_start >= 
CONFIG_CAPDL_LOADER_MAX_OBJECTS 
(../projects/camkes/capdl/capdl-loader-app/src/main.c: parse_bootinfo: 562)

I recieved the below output:

# ./simulate
qemu-system-x86_64  -cpu 
Nehalem,-vme,+pdpe1gb,-xsave,-xsaveopt,-xsavec,-fsgsbase,-invpcid,enforce 
-nographic -serial mon:stdio -m size=512M  -kernel images/kernel-x86_64-pc99 
-initrd images/capdl-loader-image-x86_64-pc99
Boot config: debug_port = 0x3f8
Boot config: disable_iommu = false
Detected 1 boot module(s):
  module #0: start=0xa17000 end=0xaef0e8 size=0xd80e8 
name='images/capdl-loader-image-x86_64-pc99'
Parsing GRUB physical memory map
Physical Memory Region from 0 size 9fc00 type 1
Physical Memory Region from 9fc00 size 400 type 2
Physical Memory Region from f0000 size 10000 type 2
Physical Memory Region from 100000 size 1fee0000 type 1
Adding physical memory region 0x100000-0x1ffe0000
Physical Memory Region from 1ffe0000 size 20000 type 2
Physical Memory Region from fffc0000 size 40000 type 2
Multiboot gave us no video information
ACPI: RSDP paddr=0xf68c0
ACPI: RSDP vaddr=0xf68c0
ACPI: RSDT paddr=0x1ffe15fc
ACPI: RSDT vaddr=0x1ffe15fc
Kernel loaded to: start=0x100000 end=0xa16000 size=0x916000 entry=0x10125e
ACPI: RSDT paddr=0x1ffe15fc
ACPI: RSDT vaddr=0x1ffe15fc
ACPI: FADT paddr=0x1ffe1458
ACPI: FADT vaddr=0x1ffe1458
ACPI: FADT flags=0x80a5
ACPI: MADT paddr=0x1ffe154c
ACPI: MADT vaddr=0x1ffe154c
ACPI: MADT apic_addr=0xfee00000
ACPI: MADT flags=0x1
ACPI: MADT_APIC apic_id=0x0
ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0
ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0
ACPI: MADT_ISO bus=0 source=5 gsi=5 flags=0xd
ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd
ACPI: MADT_ISO bus=0 source=10 gsi=10 flags=0xd
ACPI: MADT_ISO bus=0 source=11 gsi=11 flags=0xd
ACPI: 1 CPU(s) detected
ELF-loading userland images from boot modules:
size=0x210000 v_entry=0x407fef v_start=0x400000 v_end=0x610000 p_start=0xaf0000 
p_end=0xd00000
Moving loaded userland images to final location: from=0xaf0000 to=0xa16000 
size=0x210000
Starting node #0 with APIC ID 0
Mapping kernel window is done
Booting all finished, dropped to user space
Assertion failed: free_slot_end - free_slot_start >= 
CONFIG_CAPDL_LOADER_MAX_OBJECTS 
(../projects/camkes/capdl/capdl-loader-app/src/main.c: parse_bootinfo: 562)


After commenting out the assertion and rebuilding, things seemed to work 
properly. I see the comment above the assertion says:

    /* We need to be able to actual store caps to the maximum number of objects
     * we may be dealing with.
     * This check can still pass and initialisation fail as we need extra slots 
for duplicates
     * for CNodes and TCBs.
     */


But I still don't quite understand what this assertion is trying to check and 
why it doesn't really seem needed since commenting it out made things work 
properly (stdout showed "Hello CAmkES World"). If I were to guess, I'd assume 
that the check is performed to just make sure there is a decent amount of space 
to store capabilities in userspace? While I was messing around in the main.c of 
capdl-loader-app, I wanted to put print statments to see the values of 
free_slot_end and free_slot_start to get an idea of what these values were, but 
I didn't see a way to display them to stdout (printf didn't work and I don't 
know where ZF_LOGD is logging info to).

Regards,

Austin




________________________________
From: Austin Owens
Sent: Saturday, July 20, 2019 5:27 PM
To: devel@sel4.systems <devel@sel4.systems>
Subject: CAmkES Tutorial Generation Issues

Hello,

I am able to generate, build, and execute the majority of tutorials using init, 
ninja, qemu, etc. within sel4-tutorials-manifest. However, I am having issues 
generating the tutorials specifically for the CamkES tutorials.

I have installed all of the system requirements and I am running on Ubuntu 18. 
The output I get is the following:

# ./init --tut hello-camkes-0
loading initial cache file ../settings.cmake
-- The C compiler identification is GNU 7.4.0
-- Check for working C compiler: /usr/bin/gcc
-- Check for working C compiler: /usr/bin/gcc -- works
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Detecting C compile features
-- Detecting C compile features - done
-- The CXX compiler identification is GNU 7.4.0
-- Check for working CXX compiler: /usr/bin/g++
-- Check for working CXX compiler: /usr/bin/g++ -- works
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- The ASM compiler identification is GNU
-- Found assembler: /usr/bin/gcc
-- CPIO test cpio_reproducible_flag FAILED
-- Performing Test compiler_arch_test
-- Performing Test compiler_arch_test - Success
-- /root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/ast.pickle 
is out of date. Regenerating...
-- 
/root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/camkes-gen.cmake
 is out of date. Regenerating...
CAmkES uses UTF-8 encoding, but your locale's preferred encoding is 
ansi_x3.4-1968. You can override your locale with the LANG environment variable.
CMake Error at tools/seL4/cmake-tool/helpers/make.cmake:19 (file):
  file failed to open for reading (No such file or directory):

    
/root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/camkes_gen/deps_1
Call Stack (most recent call first):
  tools/seL4/cmake-tool/helpers/make.cmake:77 (MakefileDepsToList)
  tools/camkes/camkes.cmake:460 (execute_process_with_stale_check)
  hello-camkes-0/CMakeLists.txt:13 (GenerateCAmkESRootserver)


CMake Error at tools/camkes/camkes.cmake:480 (message):
  Failed to generate
  
/root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/camkes-gen.cmake
Call Stack (most recent call first):
  hello-camkes-0/CMakeLists.txt:13 (GenerateCAmkESRootserver)


-- Configuring incomplete, errors occurred!
See also 
"/root/sel4-tutorials-manifest/hello-camkes-0_build/CMakeFiles/CMakeOutput.log".
Traceback (most recent call last):
  File "./init", line 96, in <module>
  File "./init", line 85, in main
  File "/root/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 
107, in init_directories
    return _init_build_directory(config, initialised, build_directory, 
tute_directory, output, config_dict=config_dict)
  File "/root/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 
75, in _init_build_directory
    return sh.cmake(args + ['..'], _cwd=directory, _out=output, _err=output)
  File "/usr/local/lib/python3.6/dist-packages/sh.py", line 1427, in __call__
    return RunningCommand(cmd, call_args, stdin, stdout, stderr)
  File "/usr/local/lib/python3.6/dist-packages/sh.py", line 774, in __init__
    self.wait()
  File "/usr/local/lib/python3.6/dist-packages/sh.py", line 792, in wait
    self.handle_command_exit_code(exit_code)
  File "/usr/local/lib/python3.6/dist-packages/sh.py", line 815, in 
handle_command_exit_code
    raise exc
sh.ErrorReturnCode_1:

  RAN: /usr/local/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja 
-DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-0 -C 
../settings.cmake ..

  STDOUT:


  STDERR:



I am not sure if ast.pickle and camkes-gen.cmake being out of date has anything 
to do with deps_1 file not being present. It's not possible to copy the deps_0 
file to deps_1 since calling the './init --tut hello-camkes-0' command again 
creates a new project directory. Is there something obvious that I am missing?

Thanks,

Austin

_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Reply via email to