benchsupport: don't run timer tests if no ltimer

[midnightveil]

Some platforms don't have an ltimer (e.g. Cheshire). In these cases, ltimer_default_init won't compile.

Conditionally disable the IRQUSER and SMP benchmarks when there is no ltimer to use.

Resolving seL4/ci-actions#388 (comment)

[kent-mcleod]

This option won't be defined until the utils_libs cmake module is imported later in the project. So at this point it may be better to make it a platform based test?

[midnightveil]

This does seem to work though, I was testing it interactively inside sel4bench.

Though I was yes sort of confused how CMake dependency ordering works; everything is where it is because otherwise this wasn't defined before here.

[kent-mcleod]

CMake does process things procedurally but it has generator expressions that implement a generation phase processing that happens at the end of CMake processing.

But the config system that the build uses doesn't use generator expressions and so all of the config options are evaluated in the order they're get and set.

But then because the config options are also stored in the cache (because they can be set by a user on the command line or interactively), running CMake a second time can sometimes hide configuration logic bugs because it uses the cache values from the last run.

[kent-mcleod]

It's not very user friendly. I've wondered about dropping the caching from the options so that they're always evaluated fresh, but that then loses the ability to do the interactive config editing

[midnightveil]

Ah, yes, this is correct. However, even when it's from a cache rebuild, and it prints:

[0/1] Re-running CMake...
CMake Warning at settings.cmake:184 (message):
  Platform has no timer, disabling IRQUSER bench
Call Stack (most recent call first):
  CMakeLists.txt:9 (include)

It still seems to stay enabled in the cache... and the IRQ tests seems to run.

[midnightveil]

Would there be a good way to get this evaluated beforehand?

IDK, I don't really like the idea of hardcoding platforms in sel4bench when the ltimer code can export config that tells us whether it's supported. It seems really likely to go out of sync if someone adds support to the platsupport for a timer.