Source-linked AI summary
Cause Clue Clauses: Error Localization using Maximum Satisfiability
Manu Jose, Rupak Majumdar
TL;DR
Debugging long failing traces requires locating the few statements responsible for a violated specification. The paper reduces this task to symbolic execution plus partial MAX-SAT, and reports precise localization and repair suggestions for benchmark faults, while noting scalability limits for complex programs and large traces.
Problem
Debugging requires reducing long failing executions to a few source lines that explain the specification violation.
Method
BugAssist encodes a failing trace as a Boolean formula, fixes the failing input and desired post-condition as hard constraints, and uses MAX-SAT complements to identify candidate statements.
Results
The experiments and conclusions report that BugAssist can precisely localize errors and identify potential fixes, often isolating exact statements or lines.
Takeaways & Limitations
The MAX-SAT formulation supports both error localization and automated suggestions for repairs such as off-by-one and operator changes.
Takeaways & Limitations
Without trace reduction, the method may blow up the state space and may be unsuitable for programs with complex calls or enormous code.
Abstract
from arXiv · showhide
Much effort is spent everyday by programmers in trying to reduce long, failing execution traces to the cause of the error. We present a new algorithm for error cause localization based on a reduction to the maximal satisfiability problem (MAX-SAT), which asks what is the maximum number of clauses of a Boolean formula that can be simultaneously satisfied by an assignment. At an intuitive level, our algorithm takes as input a program and a failing test, and comprises the following three steps. First, using symbolic execution, we encode a trace of a program as a Boolean trace formula which is satisfiable iff the trace is feasible. Second, for a failing program execution (e.g., one that violates an assertion or a post-condition), we construct an unsatisfiable formula by taking the trace formula and additionally asserting that the input is the failing test and that the assertion condition does hold at the end. Third, using MAX-SAT, we find a maximal set of clauses in this formula that can be satisfied together, and output the complement set as a potential cause of the error. We have implemented our algorithm in a tool called bug-assist for C programs. We demonstrate the surprising effectiveness of the tool on a set of benchmark examples with injected faults, and show that in most cases, bug-assist can quickly and precisely isolate the exact few lines of code whose change eliminates the error. We also demonstrate how our algorithm can be modified to automatically suggest fixes for common classes of errors such as off-by-one.
1. Introduction
BugAssist localizes faults by encoding a failing execution as an unsatisfiable Boolean formula and using MAX-SAT to identify program statements whose alteration could eliminate the failure.
- The algorithm takes a program, correctness specification, and failing execution, then outputs a minimal set of statements whose replacement could make that execution infeasible.
- It constructs a Boolean trace formula whose satisfiability corresponds to feasibility of the executed program path.
- For a failing execution, it conjoins the trace formula with failing-input and post-condition constraints, producing an unsatisfiable extended formula.
- MAX-SAT maximizes satisfiable clauses, and the complement identifies candidate clauses mapped back to source statements; hard constraints preserve the failing input and required post-condition.
- BugAssist implements the method for C programs using CBMC and an off-the-shelf MAXSAT solver, with experiments on five Siemens benchmark programs containing injected faults.
- Unlike approaches relying on successful runs or trace comparisons, the approach does not require a successful benchmark execution and reports locations where the bug could be corrected.
2. Motivating Example
The motivating example shows how BugAssist reduces an out-of-bounds array failure to specific statements and can test nearby edits as repair suggestions.
- With input index = 1, the example’s else-branch sets index to 3, causing an out-of-bounds array dereference.
- BugAssist begins from the failing test and constructs a symbolic trace formula encoding the executed path.
- The combined formula asserts the failing input and the desired assertion, so it is unsatisfiable for the error-inducing execution.
- Partial MAX-SAT marks test-input and assertion constraints hard, while grouped statement clauses are soft and map solver results back to source lines.
- MAX-SAT identifies line 4 as a potential error location, and changing its constant to an integer less than 2 and greater than -2 can satisfy the formula.
- The method reports lines 1 and 4 separately, whereas the backward slice contains lines 1, 4, and 5.
- For off-by-one repairs, BugAssist tests nearby constant changes; replacing 2 with 1 makes the error path infeasible, and similar checks address operator mistakes.
3. Preliminaries
The preliminaries define program traces and their Boolean encodings, then explain how selector variables and partial MAX-SAT expose minimal clause sets as candidate bug locations.
- A program is modeled as a control-flow graph whose transitions impose constraints relating current and next-state variables.
- A trace is feasible when some computation follows its transitions while satisfying every transition constraint.
- The trace formula conjoins transition constraints over successive variable copies and is satisfiable exactly when the trace is feasible.
- MAX-SAT maximizes satisfied clauses, while partial MAX-SAT maximizes soft clauses subject to satisfying every hard clause.
- The complement of a maximum satisfiable subset is minimal and consists of clauses whose removal makes the instance satisfiable, serving as an oracle for potential bug locations.
- Selector variables enable or disable all clauses associated with a transition, allowing statements to be grouped and mapped at line or module granularity.
4. Algorithm
The localization algorithm generates a failing execution, separates hard input and assertion constraints from soft trace constraints, and iteratively enumerates minimal transition sets associated with the failure.
- BugAssist has two phases: generate a failing execution and find a minimal set of transitions that renders that execution infeasible.
- Failing executions may come from failed tests or bounded model checking when no tests are available.
- The algorithm obtains a concrete test and trace, then constructs formulas containing the test, assertion, and first trace-formula component as hard constraints.
- The second trace-formula component is soft, so partial MAX-SAT explores subsets of transitions whose alteration could make the failing transition infeasible.
- Each CoMSS returned by the solver is output as a potential bug location, and blocking clauses prevent previously reported sets from being rediscovered.
- Repeated runs with different failing traces can rank locations by their frequency of appearance, while multiple selector variables indicate fixes requiring multiple locations.
5. Extensions
The extensions use BugAssist’s localized fault sites to suggest repairs and use weighted clause grouping to identify the earliest loop iteration associated with a failure.
- 5.1 Extension 1: Automated Repair: BugAssist narrows automated repair to potential bug locations before searching for replacements.The general replacement space is large, so the extension targets common programmer errors pragmatically.
- 5.1 Extension 1: Automated Repair: The extension demonstrates automated repair for off-by-one errors, including boundary mistakes caused by using < instead of ≤ or vice versa.These errors can also arise when programmers treat sequence indices as starting at one rather than zero.
- 5.1 Extension 1: Automated Repair: For candidate lines containing constants, the repair procedure tests changing each constant by +1 or −1 and checks whether the resulting program satisfies the properties.It constructs two modified programs and accepts a repair when one has no error trace.
- 5.2 Extension 2: Debugging Loops: The loop-debugging extension assigns selector variables to successive unwindings and weights their soft clauses so earlier iterations receive greater weight.Each loop-body duplication through the unwinding limit η receives a selector variable, and its clauses enter the partial MAX-SAT instance as weighted soft clauses.
- 5.2 Extension 2: Debugging Loops: Weighted MAX-SAT then selects lower-iteration clauses first, helping pinpoint the initial loop iteration that can reproduce the failure.The weights act as penalties for falsifying soft clauses, causing least-iteration clauses to be preferred.
6. Experimental Results
BugAssist was evaluated on Siemens benchmark programs using CBMC-generated traces, golden outputs, and injected faults. It precisely localized most TCAS faults, while trace reduction enabled larger experiments but some cases remained computationally expensive or approximate.
- Experimental Setup: BugAssist used CBMC for failing traces, MSUnCORE for weighted partial MAX-SAT, and MiniSAT2 to synthesize the off-by-one fix.Experiments ran on a 3.16 GHz Intel Core 2 Duo CPU with 7.6 GB RAM.
- TCAS Experiments: The TCAS evaluation used 41 faulty versions of a 173-line aircraft collision-avoidance program and 1600 valid test cases.Golden outputs from the original program served as specifications for faulty versions.
- TCAS Experiments: 95% of 1440 BugAssist runs pinpointed the exact TCAS bug location.The evaluation used each failing testcase with its golden output as the assertion to satisfy.
- TCAS Experiments: For TCAS version v2, BugAssist reduced inspection to 8 potential locations, or 4.6% of the program, and found the exact fault in all 69 failing-test runs.Reported runtimes were negligible.
- TCAS Experiments: Across most TCAS versions, BugAssist found the correct location; on average, candidate inspection fell to 8% of the total code.For exceptions such as v12, v28, and v35, frequency ranking still gave exact locations more than half of the runs and other locations provided clues.
- Larger Examples: Trace reduction substantially decreased MAX-SAT instance sizes in larger Siemens programs, and BugAssist found exact locations in all but print token.Reduction used slicing, concolic execution, or delta debugging before analysis.
- Larger Examples: For totinfo, program slicing reduced the trace to 21 assignments with runtime below one second.The slice removed assignments irrelevant to the checked assertion.
- Larger Examples: Concrete execution reduced print token’s trace from 65K assignments to 239, but required assuming concretized functions and loops were bug-free.The tool localized the error to an assignment rather than the exact comparison because constant propagation abstracted the variable.
7. Scalability and Limitations
The method’s scalability is constrained by its dependence on the Boolean encoding and unreduced execution traces, especially for large or complex programs. Trace reduction and incremental solving are identified as ways to mitigate these costs.
- Encoding constraints: Fault localization depends on translating program code into Boolean clauses, so code-omission faults cannot be detected directly.The method instead attempts to modify expressions present in the current program to satisfy the asserted property.
- Potential improvements: Incremental SAT across MAX-SAT iterations could considerably reduce running time, while unsatisfiable-core extraction may further aid localization.These are proposed improvements to the current solving and localization process.
- Scalability limits: Without trace reduction, the method may blow up the state space and become unsuitable for programs with complex calls or enormous codebases.The entire Boolean representation of the program is used, increasing the error-trace formula as program size and complexity grow.
8. Conclusions
The paper applies Boolean MAX-SAT techniques to localize program errors and identify potential fixes, leveraging modern solver advances. It reports precise and scalable localization, supports IDE-assisted debugging, and outlines future work on automated repair guidance.
- Conclusions: Boolean MAX-SAT techniques can localize program errors and identify potential fixes, extending the success of Boolean satisfiability for error detection.The conclusion presents MAX-SAT as similarly effective for localization and potential repair identification.
- Conclusions: Modern SAT and MAX-SAT solver advances support precise and scalable error localization at different granularities, including statements and modules.Clauses from the same module can be grouped to localize bugs at module level.
- Conclusions: An Eclipse plugin marks potential bugs and repair capabilities during development and supports automated repairs such as off-by-one fixes.The plugin is intended to help programmers find bug locations and analyze suitable fixes.
- Conclusions: Future work includes predicting expression-specific error types from software-repository bug patterns to guide automated repair strategies.The paper also proposes constructive suggestions, such as bounds for constants that satisfy the required properties.