stable-MIR

mtg with niko 2022-04-13

• would like to work out the customer goals before we spend too much time on architectural diagrams
• Niko's high-level vision
  • Rustc itself should be able to emit SMIR, in a versioned manner
  • A separate tool-lib will provide utilities to process the versions of SMIR
    • what are the initial deliverables for the tool-libs
    • eventually, conversion between distinct major versions
    • miri has logic to get all things in your dependency graph
    • traverse the call graph, data usage, emission (??)
    • better integration with cargo
    • first goal: reducing the amount of update you have to do to your code every time you update the compier
    • do not want to commit to version-conversion utilities for initial deliverables
  • The question of where borrowck should live is somewhat debatable:
    • either we have SMIR carry the results of borrowck data
    • and/or the tool-lib provides its own borrowck implementation that can generate that same data
    • and/or we ensure Rustc is also able to input SMIR (i.e. convert SMIR to its local MIR) and then apply the borrowck to that
  • there are other reasons to have Rustc support the ability to input SMIR.
  • The SMIR should at least support being polymorphic.
• another question: What is the way that these pieces communicate?
  • i.e. is the tool-lib something that is linked into the running rustc, or is it something that receives a serialized.
  • niko imagines customers wanting to answer questions like "what is the layout of this type" or "solve for this trait", which could be provided via a compiler query.
• (an alternative approach, which avoids as much dependency on Rustc developers:)
  • have tool-lib itself produce one tool that does directly link to rustc itself, and is in charge of the MIR to SMIR conversion.
  • this seems like a good way to handle initial development of the MIR to SMIR conversion, at the very least
• what is first deliverable?
  • ideally something that can actually integrate with an existing tool, e.g. Miri or Kani
  • Kani's needs: essentially a codegen backend. Needs SMIR, Layout. Ability to resolve trait methods to their specific concrete methods from the impl.
    • this indeed seems to require a resident process to be efficient (i.e offer the compiler as a service)
    • that, or you make these trait method resolutions part of the act of generating SMIR (i.e. the resolutions are embedded in the SMIR)?
      • but this increases the scope of the conversion code owned by Rustc itself.
• SMIR
  • IFDROP etc – niko logs this for later

Tool-lib Phases

• phases
  • phase 1 (nightly):
    • tools lib creates an unstable package that links against rustc
    • shared crate that supports SMIR
    • tool authors link against some version of tools lib, which implies they have to run against the version of rustc it was designed for
  • phase 2 (stable):
    • shared crate that supports SMIR
    • rustc supports some way to run a server and export SMIR and other data structures
      • maintained by rust compiler team at this juncture
    • tools libs communicates with any version of rustc via serialization
    • tool authors link against some version of tools lib
• sanity checks
  • Can const-eval run on SMIR?
    • today, const-eval runs post drop-elaboration.
• initial deliverable, II
  • should we consider Miri as the initial target tool to use SMIR, rather than Kani
    • some of what Niko envisages for tool-lib already is present in Miri
  • Check with Vytautas if they want to integrate with Prusti
• action item:
  • make a one-pager that summarizes the above
  • spell out the components that we expect will need their own stable definition. (Currently: MIR itself, types, layout, …)

local kickoff 2022-04-04

• form actual wg-stable-mir/initiative/project
  • all of below are either due by or need due-date detemrined by 2022-04-05
  • (pnkfelix) figure out whether it's (wg/initiative/project): lets go with project
  • (pnkfelix) add zulip stream
  • (pnkfelix) add ping team on github (probably PR on teams repo): https://github.com/rust-lang/team/blob/master/teams/project-stable-mir.toml
  • (pnkfelix) create a repo in the rust-lang organization filed as https://github.com/rust-lang/infra-team/issues/57 now created https://github.com/rust-lang/project-stable-mir, but it needs a README :)
• reach out to people who are interested
  • stakeholders ("why wasn't I consulted")
  • tool developers
    • kani
      • would like borrowck info
    • mirai
    • miri
      • needs type info
    • clippy-mir
      • needs type info
  • volunteers privmsg'ing
    • Vikram Pal (pnkfelix)
    • Oguz (oli)
• establish plan with milestones
  • what are we even doing? (celina)
    • define the initial customer and their needs
    • specifically: focus on how dataflow analyses that feed into the borrow-checker end up part of their needs, and thus end up part of requirements for (some customers of) stable-MIR
    • the distinct pre- and post-borrowck phases might want their own hooks
    • oli and celina agree that initial MVP probably doesn't need the borrowck metadata
  • third party crate with definition for MIR
    • development strategy (oli): 1:1 correspondance at outset, with trivial translation routine
    • then overtime, allows independent evolution
  • how to interface with rustc (TBD)
    • queries vs some form of serialization
    • alternate driver with extra backend (?)
      • alt driver may not be necessary; see cg_cranelift
      • but for ease of initial implementation, alt driver may be easiest path, especially for newcomer volunteers
  • how to represent in git (oli)
    • document at least some of the options and why this one was chosen (oli)