The paralegal-flow tool is responsible for extracting SPDGs from the program you want to analyze. The flow analyzer integrates with cargo and rustc and can be invoked on the command line simply by running cargo paralegal-flow. In addition to the command line version there is also a programmatic way to invoke it via the SPDGGenCommand type that is as part of the paralegal-policy framework.

This guide explains how the SDPG extraction works and how to configure the flow analyzer with command line flags. When using the programmatic interface you can use SPDGGen::get_command() to get access to the underling shell Command and pass additional arguments with Command::args().

The following overview table lists all command line options available, a short description and links to the section of the guide with more information. You can also always see the full list of options available when you run cargo paralegal-flow --help. The most common and useful options are highlighted in green.

Flag / Argument Purpose Further Reading
--external-annotations <FILE> Provide a file with additional markers for third party code. External Annotations
--no-cross-function-analysis Disable cross function analysis Cross-Function Analysis
-- <CARGO OPTIONS> Pass additional flags (like --features) to cargo. Must be the last passed option

Advanced Options for debugging and development. You will likely not not need these with the exception of --dump serialized-flow-graph.

Flag / Argument Purpose Further Reading
--verbose More output (up to log level “info”)
--debug Debugging output, intended for developers of paralegal-flow
--debug-target <CTRL> The name of a controller for which to enable debug output.
--dump <TYPE> Output analyzer intermediate representations
--abort-after-analysis Force rustc to abort compilation once the SPDG has been created. Caching
--target <NAME> Select the crate for which to run the analysis. You can also select this via cargo options passed after --.
--relaxed Turn errors for sanity checks into warnings.
--result-path <PATH> A file to write the Forge model to.

You may also pass any of these options as environment variables by upper-casing the name. Some of the environment variables use the PARALEGAL_ prefix to avoid confusion. Check cargo paralegal-flow --help for the environment variable names used.

Cross-Function Analysis

SPDGs span across call sites, which lets policies reason about relationships that span the whole program. Cross-Function Analysis is enabled by default but can be disabled by passing the --no-cross-function-analysis argument. It is generally not recommended because Rust code tends to be comprised of a lot of functions, severely limiting the scope of the analysis without cross-function analysis enabled.

The cross function SPDG is constructed by expanding functions at their call site by the SPDG for their body. Paralegal only expands functions in the currently compiling crate and expands recursive functions once.

Type Signature Abstraction

Paralegal’s SPDG generation supports only single-crate SPDGs. This means it can only generate SPDGs for the functions in one crate. The data flow passing through any function not from the local crate is abstracted using its type signature and the function is represented atomically as a node in the final SPDG. This means any inputs of the function become incoming edges and all mutable arguments and the return values become output edges. As an example consider the function modify_extract in the following example

// (extern)
fn modify_extract(
	read: &T, writen: &mut Q
) -> R;

fn main() {
	let src1 = make_t();
	let mut src2 = make_q();
	let result = modify_extract(
		&src1, &mut src2
	);
	read_result(result);
	read_src2(src_2);
	read_src1(src_1);
}

Which would be represented in the SPDG roughly as

graph TD
  make_t --src1--> modify_extract --result--> read_result
	make_q --src2--> modify_extract --src2--> read_src2
	make_t --src1--> read_src1

Type Signature Abstraction is not field sensitive, unlike cross-function PDG generation and inline elision.

Field Sensitivity

Paralegal tracks control and data flow independently for each field and variant. It also distinguishes between pointers and what they point to. It preserves the field sensitivity for all calls to crate-local function. For functions from external crates, Paralegal is currently unable to load the function bodies and therefore conservatively approximates data flows using the mutability annotations on the type signature, which introduces some spurious connections.

Programmatic Interface

For your convenience paralegal-policy provides a programmatic interface for invoking paralegal-flow. The aim is to ensure that the command is called with the right arguments to produce the SPDG output used by the graph query engine and to deal with filenames for you.

SPDGGenCommand is the entry point for invoking the SDPG extractor. The ::global() method uses cargo paralegal-flow for this purpose, e.g. a global installation of cargo-paralegal-flow that was performed with cargo install. ::custom() lets you instead pick a different binary to run, for instance from a local installation.