syscall_stub_gen_rs.py looks broken, is this used anywhere at all?

[axel-h]

I wonder if libsel4/tools/syscall_stub_gen_rs.py from PR #733 is broken since PR #789 changed the conditionals from XML attributes to tag. The change was applied for the C-header generator, but not for the Rust generator.
@nspin: is this tool used anywhere in your rust support? In case the script is broken, should we delete this of fix it?

See

• Add support for generating syscall_stubs for different languages #733
• Fix Issue774 #789

[nspin]

This script is not used in https://github.com/seL4/rust-sel4

[axel-h]

So, if there is no maintainer for this to fix it, deleting might be the best option?

[kent-mcleod]

It uses syscall_stub_gen.parse_xml_file from syscall_stub_gen.py to parse the xml files and the change you link doesn't break it.

[ratmice]

Yeah, from what I recall Kent is correct, at the time those changes were made I had tested it.
It was suprising to me that it didn't require any changes, exactly because it imports and uses the syscall_stub_gen as a python import.

However that stub_gen_rs was not changed to make any use of the conditions and before that it was only able to generate for a single kernel configuration. But I didn't want to change the output from underneath anyone, and being unsure how it was used, I just left it alone.

[kent-mcleod]

(@ratmice thanks for checking that it was still working at the time!)

As far as I can tell, it does make use of the conditions, eg for seL4_TCB_Configure below:

#[cfg(not(feature = "CONFIG_KERNEL_MCS"))]
/**
 * @xmlonly <manual name="Configure" label="tcb_configure"/> @endxmlonly
 * @brief @xmlonly Set the parameters of a TCB @endxmlonly
 * 
 * @xmlonly
 * <docref>See <autoref label="sec:threads"/></docref>
 * @endxmlonly
 * 
 * @param[in] _service Capability to the TCB which is being operated on.
 * @param[in] fault_ep CPtr to the endpoint which receives IPCs when this thread faults. Thi
s capability is in the CSpace of the thread being configured. 
 * @param[in] cspace_root The new CSpace root. 
 * @param[in] cspace_root_data Optionally set the guard and guard size of the new root CNode
. If set to zero, this parameter has no effect. 
 * @param[in] vspace_root The new VSpace root. 
 * @param[in] vspace_root_data Has no effect on x86 or ARM processors. 
 * @param[in] buffer Location of the thread's IPC buffer. Must be 512-byte aligned. The IPC 
buffer may not cross a page boundary. 
 * @param[in] bufferFrame Capability to a page containing the thread's IPC buffer. 
 * @return @xmlonly <errorenumdesc/> @endxmlonly
 * @retval seL4_IllegalOperation The  @xmlonly <texttt text="_service"/> @endxmlonly ,  @xml
only <texttt text="bufferFrame"/> @endxmlonly ,  @xmlonly <texttt text="cspace_root"/> @endx
mlonly , or  @xmlonly <texttt text="vspace_root"/> @endxmlonly  is a CPtr to a capability of
 the wrong type.
 * Or,  @xmlonly <texttt text="vspace_root"/> @endxmlonly  is not assigned to an ASID pool.
 * Or,  @xmlonly <texttt text="cspace_root_data"/> @endxmlonly  is invalid.
 * Or,  @xmlonly <texttt text="buffer"/> @endxmlonly  is not aligned.
 * Or,  @xmlonly <texttt text="bufferFrame"/> @endxmlonly  is retyped from a device untyped 
 @xmlonly <docref>(see <autoref label="sec:kernmemalloc"/>)</docref> @endxmlonly . 
 * @retval seL4_InvalidCapability The  @xmlonly <texttt text="_service"/> @endxmlonly  is a 
CPtr to a capability of the wrong type. 
 * @retval seL4_RevokeFirst The  @xmlonly <texttt text="bufferFrame"/> @endxmlonly ,  @xmlon
ly <texttt text="cspace_root"/> @endxmlonly , or  @xmlonly <texttt text="vspace_root"/> @end
xmlonly  is a CPtr to a capability of the wrong type. 
 */
#[inline(always)]
pub unsafe fn seL4_TCB_Configure(_service: seL4_TCB, fault_ep: seL4_Word, cspace_root: seL4_CNode, cspace_root_data: seL4_Word, vspace_root: seL4_CPtr, vspace_root_data: seL4_Word, buffer: seL4_Word, bufferFrame: seL4_CPtr) -> seL4_Result
{
        let tag = seL4_MessageInfo::new(InvocationLabel::TCBConfigure as seL4_Word, 0, 3, 4);
        let mut mr0: seL4_Word = 0;
        let mut mr1: seL4_Word = 0;
        let mut mr2: seL4_Word = 0;
        let mut mr3: seL4_Word = 0;

        /* Setup input capabilities. */
        seL4_SetCap(0, cspace_root);
        seL4_SetCap(1, vspace_root);
        seL4_SetCap(2, bufferFrame);

        /* Marshal and initialize parameters. */
        mr0 = (fault_ep as seL4_Word) as seL4_Word;
        mr1 = (cspace_root_data as seL4_Word) as seL4_Word;
        mr2 = (vspace_root_data as seL4_Word) as seL4_Word;
        mr3 = (buffer as seL4_Word) as seL4_Word;

        /* Perform the call, passing in-register arguments directly. */
        let output_tag = seL4_CallWithMRs(_service, tag,
                &mut mr0, &mut mr1, &mut mr2, &mut mr3);
        let error: seL4_Error = output_tag.get_label().into();

        /* Unmarshal registers into IPC buffer on error. */
        if error != seL4_Error::seL4_NoError {
                seL4_SetMR(0, mr0);
                seL4_SetMR(1, mr1);
                seL4_SetMR(2, mr2);
                seL4_SetMR(3, mr3);
        }

        error.into()
}

#[cfg(feature = "CONFIG_KERNEL_MCS")]
/**
 * @xmlonly <manual name="Configure (MCS)" label="tcb_configure_mcs"/> @endxmlonly
 * @brief @xmlonly Set the parameters of a TCB @endxmlonly
 * 
 * @xmlonly
 * <docref>See <autoref label="sec:threads"/></docref>
 * @endxmlonly
 * 
 * @param[in] _service Capability to the TCB which is being operated on.
 * @param[in] cspace_root The new CSpace root. 
 * @param[in] cspace_root_data Optionally set the guard and guard size of the new root CNode. If set to zero, this parameter has no effect. 
 * @param[in] vspace_root The new VSpace root. 
 * @param[in] vspace_root_data Has no effect on x86 or ARM processors. 
 * @param[in] buffer Location of the thread's IPC buffer. Must be 512-byte aligned. The IPC buffer may not cross a page boundary. 
 * @param[in] bufferFrame Capability to a page containing the thread's IPC buffer. 
 * @return @xmlonly <errorenumdesc/> @endxmlonly
 * @retval seL4_AlignmentError The  @xmlonly <texttt text="buffer"/> @endxmlonly  is not aligned. 
 * @retval seL4_IllegalOperation The  @xmlonly <texttt text="_service"/> @endxmlonly ,  @xmlonly <texttt text="bufferFrame"/> @endxmlonly ,  @xmlonly <texttt text="cspace_root"/> @endxmlonly , or  @xmlonly <texttt text="vspace_root"/> @endxmlonly  is a CPtr to a capability of the wrong type.
 * Or,  @xmlonly <texttt text="vspace_root"/> @endxmlonly  is not assigned to an ASID pool.
 * Or,  @xmlonly <texttt text="cspace_root_data"/> @endxmlonly  is invalid.
 * Or,  @xmlonly <texttt text="bufferFrame"/> @endxmlonly  is retyped from a device untyped  @xmlonly <docref>(see <autoref label="sec:kernmemalloc"/>)</docref> @endxmlonly . 
 * @retval seL4_InvalidCapability The  @xmlonly <texttt text="_service"/> @endxmlonly  is a CPtr to a capability of the wrong type. 
 * @retval seL4_RevokeFirst The  @xmlonly <texttt text="bufferFrame"/> @endxmlonly ,  @xmlonly <texttt text="cspace_root"/> @endxmlonly , or  @xmlonly <texttt text="vspace_root"/> @endxmlonly  is a CPtr to a capability of the wrong type. 
 */
#[inline(always)]
pub unsafe fn seL4_TCB_Configure(_service: seL4_TCB, cspace_root: seL4_CNode, cspace_root_data: seL4_Word, vspace_root: seL4_CPtr, vspace_root_data: seL4_Word, buffer: seL4_Word, bufferFrame: seL4_CPtr) -> seL4_Result
{
        let tag = seL4_MessageInfo::new(InvocationLabel::TCBConfigure as seL4_Word, 0, 3, 3);
        let mut mr0: seL4_Word = 0;
        let mut mr1: seL4_Word = 0;
        let mut mr2: seL4_Word = 0;
        let mut mr3: seL4_Word = 0;

        /* Setup input capabilities. */
        seL4_SetCap(0, cspace_root);
        seL4_SetCap(1, vspace_root);
        seL4_SetCap(2, bufferFrame);

        /* Marshal and initialize parameters. */
        mr0 = (cspace_root_data as seL4_Word) as seL4_Word;
        mr1 = (vspace_root_data as seL4_Word) as seL4_Word;
        mr2 = (buffer as seL4_Word) as seL4_Word;
        mr3 = 0 as seL4_Word;

        /* Perform the call, passing in-register arguments directly. */
        let output_tag = seL4_CallWithMRs(_service, tag,
                &mut mr0, &mut mr1, &mut mr2, &mut mr3);
        let error: seL4_Error = output_tag.get_label().into();

        /* Unmarshal registers into IPC buffer on error. */
        if error != seL4_Error::seL4_NoError {
                seL4_SetMR(0, mr0);
                seL4_SetMR(1, mr1);
                seL4_SetMR(2, mr2);
                seL4_SetMR(3, mr3);
        }

        error.into()
}

[axel-h]

Thanks for checking. So given Nick's project is not using this script, does it have any test coverage anywhere? Does Nick's project produce something similar that might be the preferred artifact to use? Or should it use this, so we can ensure what this script produces can be used?

[ratmice]

I believe Nick may be using the following:
https://github.com/seL4/rust-sel4/blob/29fa149dcbe48f8089821cb78eed3681380e4038/crates/sel4/sys/build/xml/syscalls/mod.rs
But in general it seems unlikely to me that the stubs generated by this and those by Nick's project would be in any way interchangable.

I tried to do a little bit of spelunking, but didn't come up with much, iirc these were part of a project here,
https://github.com/AmbiML

all those repositories now redirect to google, but I couldn't find any evidence of the syscall_stub_gen_rs.py having
ever been used within their repository, they appear to still use a version of the script which pre-dates syscall_stub_gen_rs.py.

https://opensecura.googlesource.com/sw/cantrip/userland/+/refs/heads/master/apps/system/components/cantrip-os-common/src/sel4-sys/tools/syscall_stub_gen.py
Called from here:
https://opensecura.googlesource.com/sw/cantrip/userland/+/refs/heads/master/apps/system/components/cantrip-os-common/src/sel4-sys/build.rs

I wasn't able to check this repository out:

warning: remote HEAD refers to nonexistent ref, unable to checkout

But this repo on the same site pre-dates the inclusion of the _rs.py version, though their are repos on the github that contain it.
https://opensecura.googlesource.com/3p/sel4/sel4/+/refs/heads/master/libsel4/tools/

I should also mention that these all repos all appear to have recent activity on them, so it seems unlikely to me that this script is actually being used anywhere

[nspin]

I believe Nick may be using the following:
https://github.com/seL4/rust-sel4/blob/29fa149dcbe48f8089821cb78eed3681380e4038/crates/sel4/sys/build/xml/syscalls/mod.rs
But in general it seems unlikely to me that the stubs generated by this and those by Nick's project would be in any way interchangable.

Yes, the approach taken by https://github.com/seL4/rust-sel4 is quite different. The output of the code you linked is not meant to have meaning outside of the context of the cargo build invocation it belongs to.

[ratmice]

Overall I would in general be in favor of deprecating this in favor of Nick's code if it really isn't used anywhere.
If it is used recommending that people switch to Nick's library, assuming that is within reason.

1. I find the code generated to be very un-rust like and produces a ton of warnings.
   This is largely because it doesn't use the standard rust naming conventions, and rust compiler is opinionated on its style.
   These can't just fixed without also changing the code incompatibly.
2. It's much more natural to do as Nick does, and just run rust code/avoiding the need to invoke python within
   rust build scripts.

Notes about getting deprecation output visible:

I believe the intent of this script is to be executed from within build.rs.
That is what the external version of this script used within the code I linked previously in my last comment does.

*build.rs when run from cargo suppresses stderr and stdout, so it is likely that deprecation warnings
should emit a line beginning with cargo:warning= to stdout to ensure they are visible.

cargo:warning=This script has been deprecated in favor of https://github.com/seL4/rust-sel4/

emitting to stdout shouldn't be a problem since it appears to write code to a file rather than stdout.

[axel-h]

With the current script for seL4_TCB_SetAffinity the condition parameter can be

(!defined(CONFIG_KERNEL_MCS) && defined(CONFIG_ENABLE_SMP_SUPPORT))

and this generates

#[cfg(not(feature = "CONFIG_KERNEL_MCS && CONFIG_ENABLE_SMP_SUPPORT"))]

where this should be

#[cfg(all(not(feature = "CONFIG_KERNEL_MCS"), feature = "CONFIG_ENABLE_SMP_SUPPORT"))]

instead.

[axel-h]

Also, from CMake we get CONFIG_ENABLE_SMP_SUPPORT and in the C-Headers we add the helper ENABLE_SMP_SUPPORT. But the script translated CONFIG_MAX_NUM_NODES > 1 to feature = "CONFIG_SMP_SUPPORT", which makes we wonder if this shouldn't be feature = "CONFIG_ENABLE_SMP_SUPPORT" actually?

[kent-mcleod]

This file is still used by CantripOS by my understanding. As discussed in the original PR #733, we accepted pulling this module as a separate file that could directly depend on the original syscall_stub_gen.py and stay closer in sync with updates to the xml files while trying to avoid any ongoing maintenance burden.

It should largely be able to be ignored unless we decide to remove the original syscall_stub_gen.py script and fundamentally change the approach taken for describing the seL4 user ABI.

[ratmice]

@kent-mcleod As far as I can see though, they still use the their own script¹ called from here². I think it is what they originally submitted that became sycall_stub_gen_rs.py) hosted in their own repository.

(this is the TLDR of my comment here): #1223 (comment)

Footnotes

1. https://opensecura.googlesource.com/sw/cantrip/userland/+/refs/heads/master/apps/system/components/cantrip-os-common/src/sel4-sys/tools/syscall_stub_gen.py ↩

2. https://opensecura.googlesource.com/sw/cantrip/userland/+/refs/heads/master/apps/system/components/cantrip-os-common/src/sel4-sys/build.rs#95 ↩