-
Notifications
You must be signed in to change notification settings - Fork 37
Description
Context: We had a near-miss in #850 where SLOTHY introduced the use of callee-saved registers, but they were not saved/restored. Luckily, the CI caught this, but only in a few tests compared to the overall number of jobs we are running. Even though the HOL-Light proofs would ultimately have caught this, we need to do better at catching this early.
Task: Write an ABI checker for assembly files. The checker should take an assembly file as input and confirm empirically whether the file adheres to the target architecture's calling convention. The assembly file can be assumed to contain exactly one function symbol. On a high level, the checker is expected to run or emulate the function under test with random inputs and check whether the output adheres to the calling convention. Care has to be taken regarding pointer arguments: Those cannot be randomly chosen, or otherwise the function under test will likely segfault. Here, the checker either needs a way to find out (potentially empirically) which arguments need to be pointers; or, it needs this information explicitly -- this is TBD.
To get going, the initial target architecture should be AArch64.
SLOTHY does something similar for its selftest: It uses unicorn
to emulate the input and output assembly on randomly chosen inputs. One could consider extending this functionality to an ABI checker hosted in the SLOTHY repository, and then just reuse that via nix
.