Skip to content

[DRAFT] Update linker to enable cross-language C/Rust linking #7537

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 6 commits into
base: develop
Choose a base branch
from

Conversation

danielsn
Copy link
Contributor

Currently, the CBMC linker takes a fairly strict interpreation of compabibility between compilation units. Rust has a more relaxed view when doing FFI linking: two types are identical if they have the same bitpattern, even if they appear different at the surface level.

For example, the Rust linker would consider the following types equivalent:

// empty struct
struct Unit {};

//These are both considered equivilent to uint32_t*
struct OptionRef { uint32_t* p;};
struct OptionRefWithEmptyFields { struct Unit u; uint32_t* p;};

Update the linker to make this work

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@danielsn danielsn changed the title Update linker to enable cross-language C/Rust linking [DRAFT] Update linker to enable cross-language C/Rust linking Feb 14, 2023
Signed-off-by: Felipe R. Monteiro <[email protected]>
@kroening
Copy link
Member

Linking may have very language-specific aspects. It's not obvious that we want to have one linker that can link just about any language. In particular, a particular idiom may be well permitted in one language, and a bug in another.

@martin-cs
Copy link
Collaborator

@danielsn I am cautiously optimistic about this. It would be really cool if we could do this but I am a bit worried whether we can capture the necessary details involved in FFI and cross-language linking.

Paging @tautschnig who has spent way more time thinking about linking than me.

@tautschnig tautschnig self-assigned this Mar 8, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants