I’ve set up my environment both by adding all of the build dependencies and by setting up containers. Either way, I get the same error message. I’m running into:
jonathon@container:~/sel4test$ repo init -u https://github.com/seL4/seL4test-manifest.git
File "/home/jonathon/sel4test/.repo/repo/main.py", line 79
file=sys.stderr)
^
SyntaxError: invalid syntax
Any help is appreciated!
This appears to be an issue with the android repo tool (Referência do comando do Repo | Android Open Source Project) that we use. Does repo --version work? It seems like newer versions of the tool use python as the executable and expect python3. This may not be the case on your system or in the docker container. Our setup instructions normally expect that the repo commands are run outside of the container and so this issue may not have been noticed yet.
When I’m in the sel4Test directory, repo --version gives the same error. Outside that directory, it says that repo has not been installed and to run repo init.
I’m not running this in the container, I just wanted to be clear that I had taken both approaches and got the same results.
I’m also running on Ubuntu 18.04 LTS
What does python --version give you?
What version is your python binary? repository - neither python 3 nor python 2 works well on ubuntu 18.04 with repo? - Ask Ubuntu has an answer that claims retrying with the downloaded script might work. .repo/repo/repo init -u https://github.com/seL4/seL4test-manifest.git
In both environments python --version returns Python 2.7.17
using ./.repo/repo/repo init worked in the environment where I set up the build dependencies manually
I’m getting a new error now. init-build.sh runs fine, but when I run ninja, I get FAILED: kernel/CMakeFiles/kernel.elf.dir/kernel_all.c.obj
this is the verbose error
FAILED: kernel/CMakeFiles/kernel.elf.dir/kernel_all.c.obj
/usr/bin/ccache /usr/bin/gcc --sysroot=/home/jonathon/sel4/sel4Test/build-x86 -I/home/jonathon/sel4/sel4Test/kernel/include -I/home/jonathon/sel4/sel4Test/kernel/include/64 -I/home/jonathon/sel4/sel4Test/kernel/include/arch/x86 -I/home/jonathon/sel4/sel4Test/kernel/include/arch/x86/arch/64 -I/home/jonathon/sel4/sel4Test/kernel/include/plat/pc99 -I/home/jonathon/sel4/sel4Test/kernel/include/plat/pc99/plat/64 -I/home/jonathon/sel4/sel4Test/kernel/libsel4/include -I/home/jonathon/sel4/sel4Test/kernel/libsel4/arch_include/x86 -I/home/jonathon/sel4/sel4Test/kernel/libsel4/sel4_arch_include/x86_64 -I/home/jonathon/sel4/sel4Test/kernel/libsel4/sel4_plat_include/pc99 -I/home/jonathon/sel4/sel4Test/kernel/libsel4/mode_include/64 -Ikernel/gen_config -Ikernel/autoconf -Ikernel/gen_headers -Ikernel/generated -m64 -march=nehalem -D__KERNEL_64__ -O2 -g -DNDEBUG -nostdinc -nostdlib -O2 -DHAVE_AUTOCONF -DDEBUG -g -ggdb -mcmodel=kernel -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -std=c99 -Wall -Werror -Wstrict-prototypes -Wmissing-prototypes -Wnested-externs -Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull -ffreestanding -fno-common -mno-mmx -mno-sse -mno-sse2 -mno-3dnow -MD -MT kernel/CMakeFiles/kernel.elf.dir/kernel_all.c.obj -MF kernel/CMakeFiles/kernel.elf.dir/kernel_all.c.obj.d -o kernel/CMakeFiles/kernel.elf.dir/kernel_all.c.obj -c kernel/kernel_all.c
/home/jonathon/sel4/sel4Test/kernel/src/arch/x86/idle.c:17:1: error: ‘naked’ attribute directive ignored [-Werror=attributes]
{
^
/home/jonathon/sel4/sel4Test/kernel/src/arch/x86/idle.c: In function ‘idle_thread’:
/home/jonathon/sel4/sel4Test/kernel/src/arch/x86/idle.c:25:1: error: ‘noreturn’ function does return [-Werror]
}
^
cc1: all warnings being treated as errors
This is progress and points to a too-old gcc version. Unfortunately our installation instructions for Ubuntu 18 have gotten slightly out of date, the default gcc version there is too old (7 instead of 8), see also https://github.com/seL4/seL4/issues/574.
I don’t have a Ubuntu machine handy to test this, but I believe something like
sudo apt install gcc-8
sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-8 800 --slave /usr/bin/g++ g++ /usr/bin/g++-8
might work.
That worked, but needs to be
sudo apt install gcc-8 g++-8
I get most of the way through now, but the simulation isn’t running. I have three errors that I’m seeing.
When I run pip install sel4-deps I get
Complete output from command python setup.py egg_info:
Traceback (most recent call last):
File "<string>", line 1, in <module>
IOError: [Errno 2] No such file or directory: '/tmp/pip-build-nOl1tg/jsonschema/setup.py'
----------------------------------------
Command "python setup.py egg_info" failed with error code 1 in /tmp/pip-build-nOl1tg/jsonschema/
When I run ninja i get
[120/263] Building C object apps/sel4t...MakeFiles/sel4debug.dir/src/caps.c.obj
/home/jonathon/sel4/sel4test/projects/seL4_libs/libsel4debug/src/caps.c: In function ‘debug_cap_identify’:
/home/jonathon/sel4/sel4test/projects/seL4_libs/libsel4debug/src/caps.c:17:18: warning: format ‘%d’ expects argument of type ‘int’, but argument 2 has type ‘seL4_CPtr’ {aka ‘long unsigned int’} [-Wformat=]
printf("Cap %d has type %d\n", cap, type);
~^ ~~~
%ld
and when I run ./simulate I get an error and it freezes
vka_alloc_object_at_maybe_dev@object.h:58 failed to allocate object of size 2147483648, error1
vka_alloc_object_at_maybe_dev@object.h:58 failed to allocate object of size 1073741824, error1
vka_alloc_object_at_maybe_dev@object.h:58 failed to allocate object of size 536870912, error1
./simulate: QEMU Failed
I tried this on Ubuntu 20.04 and get the same results, with the same object sizes.
On 20.04, the pip install command worked, and I did not need the work around running repo as ./.repo/repo/repo. I did need to install repo and python-pip manually because they aren’t available in apt for 20.04.
Would you recommend another distro or did I miss something obvious?
The failed to allocate messages are not necessarily fatal, but it should not say QEMU failed. This should work on Ubuntu 20, but I currently don’t have one running to test on.
@kent-mcleod2 are you running Ubuntu?
@gerwin.klein this was my fault. I thought Hyper-V exposed virtualization extensions to the VM’s by default, but that turned out to not be the case. Once I enabled those, the tests ran fine.
By the way. I just read your paper on the proofing process of seL4. Nice work. The more I learn about verification, the more I wonder why it isn’t taught much earlier. Most of the articles I’m finding come from Princeton, Yale, etc or orgs like CSIRO, so it seems it hasn’t trickled into the main stream yet. I was surprised in your article that you were testing basic features of the process like division of labor. I assumed these were properties just by extension of being able to do so in programming, so I never even thought to test that.
Thanks, and I’m glad sel4test worked out after all.
Formal software verification is slowly making its way into the mainstream, but it is still not that common. Big companies like Amazon, Apple, etc do have formal verification teams, and there are plenty of small companies as well already. It’s still quite some way before we could call it anything like commonplace, but that’s the goal. It’s not suitable for everything, but it has plenty of room to grow.
We have some math routines (we think…?) that have been giving us trouble, so I pitched it at work as an option since it’s been persistent for a while and debugging doesn’t seem to have turned up anything. We’re a small company, and without internal knowledge we’re fighting the full learning curve. At this point, I think two semesters of DAFNY or Isabelle or Coq rather than two semesters of C++ would move a lot of people very far along on this path.
Thanks for your help! To a better future!