search

seL4 / seL4_libs

No-assurance libraries for rapid-prototyping of seL4 apps.
https://docs.sel4.systems
Other
52 stars 63 forks source link

rework kernel/generated/arch/object/structures_gen.h to allow including it #20

Open axel-h opened 4 years ago

axel-h commented 4 years ago

See my pull request https://github.com/seL4/seL4_libs/pull/19 why this would be a useful. Is there a ways that parts of it could be made available in the seL4 API headers?

kent-mcleod commented 4 years ago

Are you talking about just the enum cap_tag part? It's hard because user level isn't supposed to be able to query type information about a cap. Maybe we could look at how seL4_DebugCapIdentify is defined and change it to return the same information, but not directly tied to the internal seL4 enum values.

axel-h commented 4 years ago

Seems to me that is the usual trade off between debug features and release code. In Debug mode you want to be able to have some insights and thus need some headers or definitions that are not meant to be really public. Wouldn't it be possible that things like the enum cap_tag" are simply put into a separate header file that has no includes? Then this header file can be included in debug builds by libsel4debug and thus become available to others indirectly when they include libsel4debug? No other module would then have a direct dependency here, all such "debug hacks" are well constained in libsel4debug. After all, what is the real point on hiding some technical details that one desperately want for debugging and low level development purposes? If information is duplicated in hard coded magic numbers, I consider it even worse. That tends to end in a pitfall if something changes - because you never really notice this until things start behaving very strangely.