System Design

The chis­eled statue pre­sented in research was, just a few months prior, a heap­ing mess of gran­ite. The process and chal­lenges in a project are often the most inter­est­ing tech­ni­cal aspects, this sec­tion high­lights spe­cific design deci­sions and rough edges of the Argus inter­nals. We fin­ish with a dis­cus­sion on known short­com­ings and future plans.

Shown in is the gen­eral sys­tem archi­tec­ture of Argus. There is a main com­po­nent, argus::analysis, that type-checks a Rust mod­ule and records all oblig­a­tions solved for by the trait solver. These oblig­a­tions are avail­able via the inspect_typeckhttps://doc.rust-lang.org/sta­ble/nightly-rustc/rustc_hir_typeck/fn.inspect_typeck.html func­tion that exposes oblig­a­tions via a call­back. This fea­ture was made avail­able by PR 119613 to expose oblig­a­tions such that third party tools can extract gen­er­ated proof trees. After type-check­ing, Argus ana­lyzes and fil­ters the recorded oblig­a­tions in the argus::analysis mod­ule. Analy­sis results are passed back to the Rust com­piler to extract nec­es­sary proof trees via the the proof tree vis­i­tor API. All data is then seri­al­ized into a cus­tom JSON for­mat and passed to the Argus web view. Argus has lit­tle depen­dence on VSCode. There is even an Argus MdBook util­ity. Here we detail the fil­ter and analy­sis steps of the argus::analysis mod­ule.

You Want What Again?

The first step in the Argus pipeline is to type-check the work­space mod­ules and record oblig­a­tions solved for dur­ing trait res­o­lu­tion. Post ini­tial type-check­ing, Argus now has a large set of oblig­a­tions and needs to deter­mine which the devel­oper would find use­ful. This set is com­prised of all queries made by the trait solver, deter­min­ing which are use­ful to debug an error is dif­fi­cult for three rea­sons. First, we don’t want to expose overly com­plex com­piler inter­nals. The trait sys­tem has sev­eral vari­ants of oblig­a­tion, many of which, don’t have a source code rep­re­sen­ta­tion. Sec­ond, after a failed oblig­a­tion the trait solver may learn new infor­ma­tion and then retry the query. There is no direct mech­a­nism to dis­tin­guish a failed oblig­a­tion from a failed oblig­a­tion that suc­ceeds on a sub­se­quent solve attempt. Third, the trait solver can solve oblig­a­tions that are not hard require­ments, but rather, the answer informs type infer­ence. I will refer to these as soft­line oblig­a­tions, their fail­ure does not always imply a type-check error.

Com­plex Oblig­a­tions Until now, dis­cus­sions of oblig­a­tions cen­tered around the form U: T, read as: “does type U imple­ment trait T?” As of April 2024, Rust has eight kinds of pred­i­cates the trait solver can ask, and an addi­tional seven “clause kinds” (a kind of pred­i­cate). Only three in total have an anal­o­gous source-code rep­re­sen­ta­tion. By default Argus only shows these three clause kinds to users:

• trait pred­i­cates: U: T
• region out­lives pred­i­cates: ‘a: ‘b
• type out­lives pred­i­cates: U: ‘a

Other pred­i­cates are hid­den by default and shown only if they are the direct cause of a type-check error. This includes queries such as “Is type U well-formed?” and “Can trait T be used as a trait object?” The goal is to avoid over­whelm­ing devel­op­ers with infor­ma­tion they may not need. (Or may not have known existed!)

Sub­se­quent Oblig­a­tions The trait solver not only returns a yes/no/maybe answer for each oblig­a­tion, but also a set of infer­ence vari­able con­straints. Added infer­ence con­straints may cause a pre­vi­ously ambigu­ous oblig­a­tion to suc­ceed. Con­sider again the sim­ple ToString trait exam­ple. The type sig­na­ture of the print_ln func­tion is fn print_ln<T>(v: T) where T: ToString, this means that the caller needs to pro­vide a type T that sat­is­fies the bound ToString. In the call­ing con­text the first oblig­a­tion given to the trait solver is 0?: ToString, where 0? is an infer­ence vari­able. This oblig­a­tion will result in an ambigu­ous response. How­ever, the solver will add the infer­ence con­straint 0? = Vec<f32>. The sub­se­quent iter­a­tion of this goal, Vec<f32>: ToString, is not ambigu­ous and fails. We do not want to show devel­op­ers the first ambigu­ous oblig­a­tion, only the sec­ond fail­ure. Argus cur­rently pig­gy­backs on Rust com­piler infra­struc­ture to test whether a failed oblig­a­tion \(O_F\) implies an ambigu­ous oblig­a­tion \(O_A\). It should be noted that this strat­egy is unsafe due to infer­ence vari­ables poten­tially leak­ing out of con­text.

Soft­line Oblig­a­tions Oblig­a­tions received from the com­piler come marked with a “cause code.” This encodes data about the ori­gin of the oblig­a­tion. For exam­ple, types returned from func­tions need to be sized. Con­sider the func­tion fn to_string(&self) -> String from the ToString trait. The oblig­a­tion String: Sized is solved for with a cause code SizedReturnType.https://doc.rust-lang.org/sta­ble/nightly-rustc/rustc_infer/traits/enum.Oblig­a­tion­CauseC­ode.html#vari­ant.Sized­Return­Type Unfor­tu­nately, to the authors cha­grin, there exists a dummy cause code, MiscObligationhttps://doc.rust-lang.org/sta­ble/nightly-rustc/rustc_infer/traits/enum.Oblig­a­tion­CauseC­ode.html#vari­ant.Mis­cOblig­a­tion that can be used when the oblig­a­tion is ill-clas­si­fied. This cause code is also used for soft­line oblig­a­tions. The issue is that Argus can­not ignore these oblig­a­tions as they can demon­strate impor­tant fail­ures.

Con­sider again the ToString trait, we will mod­ify the exam­ple main func­tion from to that shown in .

struct A;

fn main() {
  let v = vec![A];
  format!("{}", v.to_string());
}

The default behav­ior for Argus is to ignore mis­cel­la­neous oblig­a­tions, unless their span can be tracked to a method call. For method calls, Argus will remove mis­cel­la­neous oblig­a­tions and re-per­form method selec­tion, reg­is­ter­ing each oblig­a­tion as required.

Moving Forward

In future releases of Argus we hope to improve the col­lect and fil­ter steps in argus::analysis. In cer­tain cir­cum­stances Argus fil­ters too aggres­sively and impor­tant oblig­a­tions are fil­tered from the default view. This can be improved by track­ing the cause code within the Rust com­piler more pre­cisely, or a smarter analy­sis to dis­tin­guish truly mis­cel­la­neous oblig­a­tions from impor­tant ones. Mem­ory con­sump­tion dur­ing oblig­a­tion col­lec­tion can spike in even medium-sized code­bases. Argus needs to main­tain infor­ma­tion about each oblig­a­tion that it wishes to ana­lyze fur­ther, espe­cially ones for which a proof tree is gen­er­ated. The cur­rent Argus release does lit­tle to throw away data it will not use and these extra oblig­a­tions take up space. To throw away unnec­es­sary oblig­a­tions again requires the knowl­edge that an oblig­a­tion will not be shown to the user, our hope is that the prob­lems dur­ing col­lect and fil­ter can both be mit­i­gated by the extra prove­nance infor­ma­tion com­ing from the com­piler.