Skip to content

Conversation

@midnightveil
Copy link
Contributor

@midnightveil midnightveil commented May 29, 2025

Depends on #197 to be merged first.


When a platform does not have CONFIG_LIB_PLAT_SUPPORT_HAVE_TIMER set,
we were removing the declaration of ltimer_default_init since #193.
This was because there was also no definition and so caused a linker
error anyway, so I thought it wouldn't matter if it was defined or not.

This was fine for sel4bench uses, as we used #ifdef to remove the
callers of ltimer_default_init when there was no timer. However,
this broke sel4test: seL4/ci-actions#411 for
Cheshire, as whilst sel4test had its CONFIG_HAVE_TIMER disabled, the
compiler still saw a call to ltimer_default_init:

/sel4test/apps/sel4test-driver/src/main.c: In function ‘init_timer’:
/sel4test/apps/sel4test-driver/src/main.c:180:17:
    error: implicit declaration of function ‘ltimer_default_init’

180 | error = ltimer_default_init(&env.ltimer, env.ops, NULL, NULL);
    |         ^~~~~~~~~~~~~~~~~~~

The implementation of sel4test has:

if (config_set(CONFIG_HAVE_TIMER)) {
    int error;

    error = ltimer_default_init(&env.ltimer, env.ops, NULL, NULL);
    ZF_LOGF_IF(error, "Failed to setup the timers");

    /* ... */
}

When ltimer_default_init was still declared, the compiler would elide
the link to the ltimer_default_init symbol and so it would compile
fine, as `CONFIG_HAVE_TIMER`` is a compile-time constant.

This commit undoes this change, and leaves ltimer_default_init always
declare, unbreaking the sel4test builds when there is no timer.

In addition, we add __attribute__((error(msg))) to the declaration of
ltimer_default_init conditionally. This is documented by both GCC 1
and by Clang 2 to only fire if it can't be elided with compile-time
optimisations. This is then fine for sel4bench (function call #ifdef
out entirely) and sel4test (CONFIG_HAVE_TIMER is compile-time known).

We were implicitly relying on the compiler to elide the link against
ltimer_default_init based on the compile-time constant anyway; so this
doesn't make the builds any more reliant on compiler optimisations.

As a demonstration of the diagnostic emitted if sel4test doesn't disable
the timer tests when the platform has no timer, the following error is
emitted during builds:

/sel4test/apps/sel4test-driver/src/main.c:180:17:
  error: call to ‘ltimer_default_init’ declared with attribute
    error: no ltimer support for this platform

  180 |  error = ltimer_default_init(&env.ltimer, env.ops, NULL, NULL);
      |          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

This should hopefully be much clearer than a link-time failure.

@Indanz
Copy link
Contributor

Indanz commented May 29, 2025

__attribute__(error) can't fix anything, it only turns link time errors into compile time errors, so it can't solve anything on its own, just make it easier to fix breakage. So the real change is removing the #ifndef CONFIG_LIB_PLAT_SUPPORT_NO_PLATFORM_LTIMER block. However, although that fixes the undeclared function issue, but not the underlaying problem.

So to me it seems the real fix for sel4test Cheshire builds is to unset Sel4testHaveTimer. If we do that, none of this nor the recently introduced CONFIG_LIB_PLAT_SUPPORT_NO_PLATFORM_LTIMER config option are needed and can be removed again.

@midnightveil
Copy link
Contributor Author

midnightveil commented May 29, 2025

__attribute__(error) can't fix anything, it only turns link time errors into compile time errors, so it can't solve anything on its own, just make it easier to fix breakage. So the real change is removing the #ifndef CONFIG_LIB_PLAT_SUPPORT_NO_PLATFORM_LTIMER block. However, although that fixes the undeclared function issue, but not the underlaying problem.

Yes; it turns link time errors into compile time errors. But in this case I'm turning a compile time error (because of an implicit function declaration) into no compile time error (because the if (config_set(HAVE_TIMER)) branch is compile-time known to be false).

I could remove the #ifndef entirely, yes, that's true. But then we're still relying on the compiler to elide the call to ltimer_default_init() because of the compile-time known constant, and just not emit in the binary. If it doesn't do that then we get an (obsure and confusing) link time error.

Why I did it this way is that I am essentially removing the #ifndef on the function declaration; but I'm leaving in the obvious compile time error with __attribute((error)).

So to me it seems the real fix for sel4test Cheshire builds is to unset Sel4testHaveTimer.

No, it already does. This underlying issue is this issue.
(Also, did I not already explain this in the PR message? Was something unclear?)

@Indanz
Copy link
Contributor

Indanz commented May 29, 2025

Yes; it turns link time errors into compile time errors. But in this case I'm turning a compile time error (because of an implicit function declaration) into no compile time error (because the if (config_set(HAVE_TIMER)) branch is compile-time known to be false).

Okay.

I could remove the #ifndef entirely, yes, that's true. But then we're still relying on the compiler to elide the call to ltimer_default_init() because of the compile-time known constant, and just not emit in the binary. If it doesn't do that then we get an (obsure and confusing) link time error.

That seems better to me than having those ugly attributes everywhere. If you get link errors for ltimer functions it is clear that the platform doesn't support them, saying the same at compile time doesn't help in figuring out why not. But that's my opinion, no strong feelings about this.

Why I did it this way is that I am essentially removing the #ifndef on the function declaration; but I'm leaving in the obvious compile time error with __attribute((error)).

So to me it seems the real fix for sel4test Cheshire builds is to unset Sel4testHaveTimer.

No, it already does. This underlying issue is this issue. (Also, did I not already explain this in the PR message? Was something unclear?)

Well, you said "Instead, use __attribute__(error). [...] This unbreaks the sel4test code", that confused me, as it seemed you were relying on some subtle compiler specific behaviour of add those. And in that confusion I forgot why removing the ifndef fixes things.

The problem for me was the emphasis on __attribute((error)), both in commit title and description. So you started fine with describing what the problem is, but then instead of saying what the fix is directly (removing the #ifndef), you went on about the unrelated, but nice to have error attribute, which was just confusing and not strictly speaking relevant to the actual fix, which was basically reverting commit 7f80c3c (which would be good to mention too, as it's relevant).

I'd have done your initial problem description + say what the fix is, but then explain why instead of reverting, you add the error attribute.

@midnightveil midnightveil marked this pull request as draft May 30, 2025 02:03
@midnightveil midnightveil force-pushed the sel4test-ltimer-fix branch from 108ccd7 to afcc52f Compare May 30, 2025 04:15
@midnightveil midnightveil marked this pull request as ready for review May 30, 2025 04:19
@midnightveil
Copy link
Contributor Author

I've rewritten the commit message now, hopefully it should be a bit clearer.

@midnightveil midnightveil changed the title use __attribute__(error) for unsupported ltimer fn fix error implicit declaration of ltimer functions May 30, 2025
Copy link
Contributor

@Indanz Indanz left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks.

This also contains #197, but that will hopefully be sorted if #197 gets merged first and this one is brought up-to-date (if nothing gets rebased...).

@Indanz Indanz force-pushed the sel4test-ltimer-fix branch 3 times, most recently from 0cd54a6 to cddcbec Compare May 30, 2025 21:31
Signed-off-by: julia <git.ts@trainwit.ch>
When a platform does not have `CONFIG_LIB_PLAT_SUPPORT_HAVE_TIMER` set,
we _were_ removing the declaration of `ltimer_default_init` since seL4#193.
This was because there was also no definition and so caused a linker
error anyway, so I thought it wouldn't matter if it was defined or not.

This was fine for sel4bench uses, as we used `#ifdef` to remove the
callers of `ltimer_default_init` when there was no timer. However,
this broke sel4test: seL4/ci-actions#411 for
Cheshire, as whilst sel4test had its CONFIG_HAVE_TIMER disabled, the
compiler still saw a call to `ltimer_default_init`:

    /sel4test/apps/sel4test-driver/src/main.c: In function ‘init_timer’:
    /sel4test/apps/sel4test-driver/src/main.c:180:17:
        error: implicit declaration of function ‘ltimer_default_init’

    180 | error = ltimer_default_init(&env.ltimer, env.ops, NULL, NULL);
        |         ^~~~~~~~~~~~~~~~~~~

The implementation of sel4test has:

    if (config_set(CONFIG_HAVE_TIMER)) {
        int error;

        error = ltimer_default_init(&env.ltimer, env.ops, NULL, NULL);
        ZF_LOGF_IF(error, "Failed to setup the timers");

        /* ... */
    }

When `ltimer_default_init` was still declared, the compiler would elide
the link to the `ltimer_default_init` symbol and so it would compile
fine, as `CONFIG_HAVE_TIMER`` is a compile-time constant.

This commit undoes this change, and leaves `ltimer_default_init` always
declare, unbreaking the sel4test builds when there is no timer.

In addition, we add `__attribute__((error(msg)))` to the declaration of
`ltimer_default_init` conditionally. This is documented by both GCC [1]
and by Clang [2] to only fire if it can't be elided with compile-time
optimisations. This is then fine for sel4bench (function call `#ifdef`
out entirely) and sel4test (`CONFIG_HAVE_TIMER` is compile-time known).

We were implicitly relying on the compiler to elide the link against
`ltimer_default_init` based on the compile-time constant anyway; so this
doesn't make the builds any more reliant on compiler optimisations.

As a demonstration of the diagnostic emitted if sel4test doesn't disable
the timer tests when the platform has no timer, the following error is
emitted during builds:

/sel4test/apps/sel4test-driver/src/main.c:180:17:
  error: call to ‘ltimer_default_init’ declared with attribute
    error: no ltimer support for this platform

  180 |  error = ltimer_default_init(&env.ltimer, env.ops, NULL, NULL);
      |          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

This should hopefully be much clearer than a link-time failure.

[1]: https://gcc.gnu.org/onlinedocs/gcc/Common-Function-Attributes.html
[2]: https://clang.llvm.org/docs/AttributeReference.html#error-warning

Signed-off-by: julia <git.ts@trainwit.ch>
@Indanz Indanz force-pushed the sel4test-ltimer-fix branch from cddcbec to c49ddd7 Compare May 30, 2025 21:34
@Indanz Indanz merged commit d4062e7 into seL4:master May 30, 2025
24 checks passed
@midnightveil midnightveil deleted the sel4test-ltimer-fix branch January 5, 2026 13:10
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants