The Hitchhiker’s Guide to Program Analysis: A Journey with Large Language Models

(authored by agents unless marked 🧑) Tag: li2023hitchhiker, paper

problem and system

LLift combines scalable static analysis with LLM reasoning for Linux use-before-initialization (UBI) candidates. UBITect (the prior tool) runs a scalable static analysis that reports about 140k potential bugs, then a symbolic execution stage; the paper says 40% of the reported bugs are discarded there due to a 10-minute timeout or a 2 GB memory limit (section 2.1, p.2). LLift targets those undecided cases. The paper’s abstract says: “LLMs are better used in an assistive role to complement static analysis.” (abstract, p.1). LLift takes a UBITect report (suspicious variable and its function), asks an LLM to find the initializer, extract the post-constraints and summarize the initializer’s behavior, and labels the variable must_init (non-bug) or otherwise a potential bug (section 3.3, p.4). Inference: this makes LLift an assistive triage tool rather than a verifier.

technique 1: post-constraint guided path analysis (PCA)

Use PCA when a variable’s initialization depends on the conditions under which it is later used. The paper defines the post-constraint C_post as the constraint under which the use is reachable (e.g. ret >= 4 for if (sscanf(...) >= 4)), and analyzes the initializer only under those constraints. Section 3.2 gives two pruning rules: direct application (a path is discarded if its path constraint contradicts C_post) and outcome conflicts (a path is pruned if one of its outcomes contradicts C_post). Section 4.3.3 (Figure 6) applies them: if the use is unconditional (C_post = ⊤), or all path constraints and outcomes are disjoint from C_post, no path can be pruned and the variable is may_init; if C_post clashes with a path constraint or conflicts with an outcome (e.g. the early return -1), the variable is must_init. The authors motivate it with: “a path-sensitivity analysis can effectively eliminate over 70% of these negative cases” (section 4.3, p.5). They claim: “Conceptually, LLift will not miss more bugs. The post-constraint guided path optimizations and decision policies are safe.” (section 3.3, p.4); note the paper also says its policy may produce false positives.

Steps: (1) from the UBITect report, the LLM identifies the initializer(s) of the suspicious variable; (2) the LLM extracts C_post from the caller context, taught by few-shot in-context learning of two patterns, “Check Before Use” and “Failure Check” with variants (section 4.3.1, Table 2); (3) the LLM summarizes the initializer’s behavior given C_post as must_init and may_init variables (section 4.3.2); (4) decision policy: must_init means non-bug, anything else is a potential bug (section 3.3). The path rules above describe what the LLM is meant to apply; the paper does not run a symbolic engine for this. Inference: for Verus, C_post resembles the assumptions at a use site, while initialization safety is expressed through requires, ensures, and invariants. A Verus checker can discharge the resulting obligation; an LLM classification cannot establish memory safety.

technique 2: progressive prompting with source retrieval

Use this when a large codebase makes either too little context or all context unusable. The paper avoids copying many function bodies into the prompt (token limits, section 4.1 C2) and instead supplies function definitions on demand. The prompt is: “If you encounter uncertainty due to a lack of function definitions, please signal your need, and I’ll supply them” (section 4.4, p.6). The model is taught to request a definition in a fixed format, [{"type":"function_def", "name":"some_func" }]; LLift scans the response, retrieves each requested function’s code with comments from the Linux source, and repeats until the model stops asking or LLift cannot supply the details. Only function definitions are supported, not other requests such as struct definitions.

The Convo.2 input and output are JSON-like: initializer, suspicious variables and post-constraint in; must_init variables and may_init entries with conditions out (section 4.3.2). When LLift cannot supply information (e.g. the definition of an indirect call), it still prompts the LLM to proceed, “encouraged to infer the behavior based on the available data and its inherent knowledge”; this is an explicit incompleteness assumption, and the paper lists indirect calls among its imprecision causes (section 6.7).

technique 3: decompose the analysis into conversations and natural-language reasoning

Use task decomposition to prevent one prompt from mixing extraction, constraint reasoning, and final formatting. LLift uses Convo.1 to extract the initializer and post-constraints (subtasks 1 and 2), then Convo.2 to summarize the function (subtask 3). The paper states: “The first conversation (Convo.1) is dedicated to extracting the initializer and its associated post-constraints” and “the second conversation (Convo.2) focuses on summarizing the function” (section 4.5, p.6). It also asks the model first for reasoning in English and only then for a JSON conclusion, because direct JSON prompting “may interrupt their thought progression” (section 4.5, p.6). Every prompt includes a chain-of-thought instruction (“think step by step”), and the analysis works on source code rather than LLVM IR (section 4.7, p.7).

Inference: a Verus proof assistant could separate code/spec extraction, candidate invariant generation, and final Rust/Verus emission. Each stage should produce artifacts that a parser and Verus checker validate; natural-language intermediate text is not trusted. The paper reports that omitting TD (task decomposition) or SV (self-validation) tends to make the LLM neglect the post-constraints (section 6.4, p.9), and that no case exceeded the GPT-4 token limit when TD was used while two did without it.

technique 4: self-validation and majority voting

Use self-validation when LLM outputs are stochastic or logically inconsistent. The paper’s self-validation reinforces specific rules before the LLM reaches its final conclusion, by prompting a list of correct properties it expects, so the LLM re-checks and corrects its previous response; it is used in both conversations (section 4.6, pp.6-7). The paper also runs each case multiple times and uses majority voting against stochasticity (section 4.2, p.5). Implementation: gpt-4-0613, max_token 1,024, temperature 1.0 (the API default, chosen because a very low temperature can give repetitive or simplistic responses), a roughly 1,000-line Python agent and seven prompts of about 2,000 tokens in total (section 5, p.7). Cost is about 7,000 GPT-4 tokens per potential bug, and 2.78 turns on average (section 6.1, p.7).

evidence and failure modes

UBITect’s static analysis produced 140,000 potential bugs; symbolic execution processed 60%, leaving 53,000 cases (section 6.1, p.7). Random-1000 sampled 1,000 of them, 182 had no initializer and were filtered automatically, and precision was evaluated on the remaining 818. LLift reported 26 positives, half of them true bugs by manual inspection (Table 3 lists 13), a precision of 50%; 12 of the bugs still exist in the latest Linux kernel, and patches for 4 had been submitted and confirmed (section 6.2, p.7). The paper’s abstract and introduction say 13 previously unknown bugs were found. Recall (section 6.3, p.8): the authors sampled 300 negative cases from Random-1000 and “confirm that all are true negatives”, and LLift found all real bugs in Bug-50 (the 52 confirmed UBI bugs previously identified by UBITect). They caution that this is not proof of flawlessness: 3 to 5 cases were occasionally inconsistent, and all of those bugs have trivial post-constraints (C_post = ⊤, may_init) and are already detectable by UBITect. Thus the recall claim is 52/52 on that corpus, and general soundness is not established.

Table 4 (section 6.4, p.8; Cmp-40: 27 negatives and 13 positives selected from Random-1000) gives the component ablation. Simple Prompt has precision 0.12 and recall 0.15; PCA+PP+SV+TD has precision 0.87, recall 1.00, accuracy 0.95, F1 0.93 (PCA+PP+TD: precision 0.55, recall 0.46). These fractions use the 40-case denominator, so they are small-sample numbers. On Random-1000 the 13 false positives came from mistaking must_init cases for may_init; the breakdown is incomplete constraint extraction (4), information gaps in UBITect (5), variable reuse (1), indirect call (1) and additional constraints (1), plus one false positive from inconsistent output (two false positives in three runs); the largest listed cause is UBITect information gaps (section 6.2, p.8). Four cases exceeded the maximum context length in the progressive prompt. The paper reports model dependence (section 6.5, p.9, Table 5 on a subset of Bug-50, nine callers): GPT-4 passes all tests, whereas GPT-3.5, Claude 2, and Bard have recall rates of 89%, 67%, and 67%. For GPT-3.5 and Bard only the PCA design was applied, without the other strategies.

techniques for the catalog

• post-constraint guided analysis — prune initializer paths using conditions at the later use
• progressive source prompting — retrieve function definitions only when the model signals uncertainty
• conversation decomposition — separate initializer/constraint extraction from behavior summarization
• self-validation and voting — repeat constrained analyses, check rule adherence, and aggregate outputs
• LLM-assisted static triage — use model summaries to prioritize candidates while retaining a checker as oracle

Last edited: 2026-10-18