I think I found a bug in Idris 2's "refc" backend on 32-bit platforms. It is late, so tomorrow I will investigate. It's not a subtle bug, so I'm still unsure if I've got the right idea or if I'm just exhausted.
I tripped over this bug, if I understand correctly what's going on, immediately after getting "Hello World" in Idris atop the seL4 kernel. I'd never worked with seL4 or Idris 2 before. Learning curve was steeeeep.
Yeah, it's a bug. Swapping a couple things around fixed it. Need to come up with a cleaner fix, since it changes other behavior which I presume is NOT broken.
Should probably test to confirm.
Not gonna get the time to open an issue and describe the problem properly until this evening, most likely.
Briefly:
show "some string"
results in the first character of the string being mistaken for a pointer to an integer and dereferenced on arm32 platforms (the zynq7000 platform seL4 supports for "simulation," specifically).
If y'all can get a clean fix figured out ahead of me, more power to you. Otherwise I'll be returning to this problem and posting a clearer explanation of this bug this evening, once I'm back at a terminal.
Trying to trigger this bug in a more pared-back context and having trouble now. Bah. My understanding is still insufficient.
One weird thing I'm doing which could in theory cause problems: cross-compiling the Idris runtime and support libraries but generating the C code with a host-native compiler. Maybe this is the issue?
Gonna see what happens if I try triggering the bug on my OpenBSD i386 laptop. I've been developing on my aarch64 router up to this point.
If I can reproduce this bug in a non-seL4 context and get it written up, or else determine that it's actually my weird build setup that's the issue, I'm gonna play out the evening by v-tubing while I reinstall Windows 98 on my beige box.
Been meaning to do that shit forever. Sitting on a lot of old CDs for that purpose.
I'm not even into v-tubing generally, I just think it's the one way to stream without becoming recognizable.
Yeah, not happening. I can crash it in my weird little 32 bit qemu scenario, but my actual 32 bit box can't compile Chez and I keep getting an error when I try to actually get all of Idris converted to C code via the refc backend in an attempt to work around this.
That last part is concerning. I need to be able to bootstrap Idris from C. If I can't do that, I've gotta start looking for another language.
Ah, figured it out. Another late night, but maybe tomorrow I will have a clean write-up, maybe even a fix.
Bug report submitted, along with a shell script for reproducing it.
Took up my window of free time, but I should get another later today for hammering out and possibly even submitting a fix.
Ah. I forgot I'd downloaded the latest stable. The bug... may be fixed... in the development branch. 😖
Yes. Yes, it is.
I really spend a lot of time on this.
At least I learned a bit about how seL4 and Idris' refc backend work. 🫥