arm: improve error for unsupported IssueSGISignal

Fail early with IllegalOperation if IssueSGISignal is not supported at
all for the platform.

This also helps with verification, because the later range check gets
simplified away automatically, leading to divergent code paths.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein
2025-08-19 10:50:25 +01:00
parent 9d17561157
commit 5e08006c48

View File

@@ -95,6 +95,14 @@ exception_t Arch_decodeIRQControlInvocation(word_t invLabel, word_t length,
current_syscall_error.type = seL4_TruncatedMessage;
return EXCEPTION_SYSCALL_ERROR;
}
// wrap_config_set to prevent verification automation from simplifying it away
if (wrap_config_set(NUM_SGIS) == 0) {
current_syscall_error.type = seL4_IllegalOperation;
userError("IRQControl: IssueSGISignal not available on this platform.");
return EXCEPTION_SYSCALL_ERROR;
}
word_t irq = getSyscallArg(0, buffer);
word_t target = getSyscallArg(1, buffer);
word_t index = getSyscallArg(2, buffer);