We now fixed this in the mainline repositories. Thanks for sharing.
________________________________
From: Devel <[email protected]> on behalf of Nogin, Aleksey
<[email protected]>
Sent: Thursday, 21 November 2019 7:52 PM
To: [email protected] <[email protected]>
Subject: [seL4] Nasty bug in
global-components/templates/rpc-signalling.template.c
After spending a few hours debugging time server not working for me, I realized
that global-components/templates/rpc-signalling.template.c that was added
earlier this year contains the following
/*- set badge = str(configuration[c.instance.name].get("%s_attributes" %
c.interface.name)).strip('"') -*/
[…]
/*- do badges.sort() -*/
[…]
int /*? me.interface.name ?*/_largest_badge(void) {
return /*? badges[len(badges) - 1] ?*/;
}
Unfortunately for me, my Trusted Build generated camkes had the attributes
numbered 1,2,3,10,11,12,13 and therefore the above core was claiming that the
time_server_largest_badge is 3 :(. Obviously, the issue is the combination of
the str and sort, resulting in the last badge being the one largest
lexicographically, not numerically :(. Replacing the str with int (and
correspondingly removing the strip) solved the problem for me.
P.S. Well, solved that particular problem for me, not the problem of time
server not working – looks like now I will have to debug
FAULT HANDLER: data fault from time_server.time_server_0_control (ID 0x2) on
address 0x84b8ba, pc = 0x42439d, fsr = 0x4
FAULT HANDLER: Register dump:
FAULT HANDLER: rip :0x42439d
FAULT HANDLER: rsp :0x454cf0
FAULT HANDLER: rflags :0x10202
FAULT HANDLER: rax :0x413a33
FAULT HANDLER: rbx :0x437e88
FAULT HANDLER: rcx :0x0
FAULT HANDLER: rdx :0x437e98
FAULT HANDLER: rsi :0x28
FAULT HANDLER: rdi :0x437e98
FAULT HANDLER: rbp :0x454d70
FAULT HANDLER: r8 :0xffffffff
FAULT HANDLER: r9 :0x0
FAULT HANDLER: r10 :0xe8
FAULT HANDLER: r11 :0x293
FAULT HANDLER: r12 :0x413a32
FAULT HANDLER: r13 :0x84b8ba
FAULT HANDLER: r14 :0x0
FAULT HANDLER: r15 :0x0
FAULT HANDLER: fs_base :0x44a460
FAULT HANDLER: gs_base :0x0
FAULT HANDLER: memory map:
FAULT HANDLER: +-- 0x0000000000458fff --
FAULT HANDLER: | guard page
FAULT HANDLER: +-- 0x0000000000458000 --
FAULT HANDLER: | IPC buffer
FAULT HANDLER: +-- 0x0000000000457000 --
FAULT HANDLER: | guard page
FAULT HANDLER: +-- 0x0000000000456000 --
FAULT HANDLER: | guard page
FAULT HANDLER: +-- 0x0000000000455000 --
FAULT HANDLER: | stack
FAULT HANDLER: +-- 0x0000000000451000 --
FAULT HANDLER: | guard page
FAULT HANDLER: +-- 0x0000000000450000 --
FAULT HANDLER: | code and data
FAULT HANDLER: +-- 0x0000000000400000 –
:(
Aleksey
CONFIDENTIALITY NOTICE: The information transmitted in this email, including
attachments, is intended only for the person(s) or entity to which it is
addressed and may contain confidential, proprietary and/or privileged material
exempt from disclosure under applicable law. Any review, retransmission,
dissemination or other use of, or taking of any action in reliance upon this
information by persons or entities other than the intended recipient is
prohibited. If you received this message in error, please contact the sender
immediately and destroy any copies of this information in their entirety.
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
