Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Add main to functions array #42

Open
jberthold opened this issue Feb 4, 2025 · 1 comment
Open

Add main to functions array #42

jberthold opened this issue Feb 4, 2025 · 1 comment

Comments

@jberthold
Copy link
Member

The functions array lists all functions that are being called (i.e., occur within a TerminatorKind::Call in a block anywhere within one of the items). Typically main is not one of these functions. However, we need main to be available so we can restore its blocks when returning from a call - and we should anyway strive to have complete data in the functions array, i.e., all items we have should also occur there.

  • modify the functions data collection to include the main function
@jberthold jberthold mentioned this issue Feb 4, 2025
Merged
jberthold added a commit to runtimeverification/mir-semantics that referenced this issue Feb 4, 2025
@jberthold @gtrepta
Basic support for control flow (calls and returns without data) (#445)
b5adfdc 
* Various adaptations to `kmir.md` so that we can look up functions by
their type `Ty`
  - `functions` table is now keyed on `Ty` instead of `DefId`
  - `caller` and `currentFunc` fields likewise contain a `Ty`
- the `main` function is added to the functions table with `ty(-1)` key
to work around a shortfall of stable-mir-json:
runtimeverification/stable-mir-json#42
- various other adaptations and stub code to write function call
arguments to resp. local values
* A basic program where `main()` calls `a()`, which calls `b()`, which
calls `c()` is added as a first integration test
* The `#init` function is adapted to support executing functions other
than `main` (not tested yet)

---------

Co-authored-by: Guy Repta <[email protected]>
@jberthold
Copy link
Member Author

After an initial inspection of how we collect the functions in the functions array, this turns out to be more complicated than expected:

  • The Ty ID in the functions mapping is assigned by stable_mir when the function item is converted.
  • The tables where this mapping is stored cannot be accessed directly.
  • Therefore, we could construct the main item but we cannot find its Ty ID - it would require a reverse lookup in the table to go from the symbol name to the Ty ID.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@jberthold