PaperlayerView exact revision on arXiv

Source-linked AI summary

Automatic Repair of Buggy If Conditions and Missing Preconditions with SMT

Favio Demarco, Jifeng Xuan, Daniel Le Berre, Martin Monperrus

arXiv:1404.3186v1cs.SE

TL;DR

Nopol addresses automatic repair of buggy if conditions and missing preconditions using test-suite executions, angelic fix localization, and SMT-based synthesis. It produces source patches when the encoded constraints are satisfiable, with preliminary cases including a real Apache Commons Math bug and artificial examples.

  • Problem

    Nopol targets common condition-related bugs: buggy if conditions and missing preconditions in object-oriented Java code.

  • Method

    Nopol instruments test-suite executions, uses angelic fix localization to select candidate locations, encodes execution data as SMT constraints, and translates solutions into patches.

  • Results

    Nopol finds a patch matching the developers’ patch for a Commons Math bug after analyzing 11 candidate if conditions using 352 test cases with one failing test.

  • Takeaways & Limitations

    Nopol demonstrates repair of its targeted fault model on a real-world Apache Commons Math bug and two artificial examples.

  • Takeaways & Limitations

    Nopol handles only programs with a single fault and does not stack patches.

Abstract

from arXiv · show

We present Nopol, an approach for automatically repairing buggy if conditions and missing preconditions. As input, it takes a program and a test suite which contains passing test cases modeling the expected behavior of the program and at least one failing test case embodying the bug to be repaired. It consists of collecting data from multiple instrumented test suite executions, transforming this data into a Satisfiability Modulo Theory (SMT) problem, and translating the SMT result -- if there exists one -- into a source code patch. Nopol repairs object oriented code and allows the patches to contain nullness checks as well as specific method calls.

1. INTRODUCTION

Nopol targets buggy if conditions and missing preconditions in Java using test-suite evidence, angelic fix localization, instrumentation, and SMT-based patch synthesis.

  • Nopol repairs buggy if conditions and missing preconditions in object-oriented Java programs.
  • The approach uses a program, passing tests that model expected behavior, and at least one failing test embodying the bug.
  • Nopol instruments executions, collects primitive and object-oriented state, encodes traces as an SMT problem, and translates solutions into source patches.
  • The approach extends repair to missing preconditions, nullness, and selected method calls while combining prior repair and SMT ideas with new techniques.
  • Angelic fix localization identifies potential repair locations and repair oracles by analyzing statements executed by the failing test.
  • A case study targets the Apache Commons Math library with 5000 lines of executable code and 352 JUnit test methods.

2. BACKGROUND

The background defines test-suite and oracle-based repair, motivates repair localization, and introduces buggy conditions and missing preconditions as target fault classes.

  • 2.1 Test Suite based Program Repair: Test-suite repair searches for patches that make failing tests pass while keeping other tests green.
  • 2.2 Oracle-based Program Repair: Oracle-based repair first identifies a location-value pair that would fix the bug, then synthesizes code producing that value across executions.
  • 2.2 Oracle-based Program Repair: Repair localization prioritizes places where a fix can be written rather than attempting to identify the root cause.
  • 2.3 Buggy if condition bugs: Buggy if conditions are condition-related faults, and one reported Java-project study found up to 18.6% of fixes changed an if condition.
  • 2.3 Buggy if condition bugs: Nopol can synthesize a safer gcd condition that compares each parameter with zero instead of multiplying them, avoiding arithmetic overflow.
  • 2.4 Missing precondition bugs: Missing preconditions omit checks needed to distinguish values such as null references or invalid array indexes, potentially allowing null-pointer exceptions.

3. OUR APPROACH

Nopol combines SMT-based program-synthesis encoding with angelic fix localization to repair buggy if conditions and missing preconditions in Java.

  • Nopol automatically repairs buggy if conditions and missing preconditions in Java source code.
  • The approach blends existing SMT-based synthesis ideas with the new technique of angelic fix localization.

3.1 Overview

Nopol localizes candidate repairs through test execution, encodes the observed conditional behavior in SMT, and converts satisfiable solutions into source patches.

  • Nopol uses angelic localization to identify repair locations, then collects each conditional expression’s context and expected value across the whole test suite.
  • The generated SMT formula preserves passing-test behavior while modifying behavior for failing tests; a satisfiable formula yields a source-code patch.
  • Nopol supports a subset of object-oriented primitives, including nullness and certain method calls.
  • The localization algorithm tests whether forcing executed if conditions to true or false makes the failing test pass, recording successful location-value pairs.

3.2 Angelic fix localization

Angelic fix localization modifies candidate conditions or statements during failing-test execution to identify repair locations and expected outputs for synthesis. Nopol keeps this search tractable by using binary values, suspiciousness ranking, and a fixed value across repeated executions, with reduced coverage for sequences of changing values.

  • 3.2 Angelic fix localization: Angelic fix localization identifies a potential repair location and the expected value needed to guide SMT synthesis.For buggy conditions, forcing true or false and observing a passing failing test yields a location–value pair; missing-precondition localization instead skips statements and records false.
  • 3.2.1 If Conditions: For buggy if conditions, the search space is 2 × n when n executed conditions each receive one fixed Boolean value.Repeated executions of the same condition are treated as having the same angelic value, and only the failing test case is needed for this localization.
  • 3.2.2 Missing Preconditions: For missing preconditions, Nopol tests each executed statement once with that statement skipped; a passing result yields the oracle false.The search space equals the number of executed statements, and repeated executions are completely skipped together.
  • 3.2.3 Discussion: Nopol ranks executed conditions and statements by Ochiai suspiciousness, manipulating the most suspicious candidates first.The ranking uses failing and passing coverage counts, although the supplied equation text is incomplete.
  • 3.2.3 Discussion: If no angelic pair is found, repeated executions could require a changing value sequence, but Nopol excludes such sequences to keep the search space small.The paper reports that most if conditions are evaluated only once per test case and identifies systematic study of this issue as future work.

3.3 Runtime Trace Collection for Repair

After localization, Nopol collects primitive, nullness, and side-effect-free object-state information at candidate locations, pairing each execution context with an expected outcome. These data support SMT synthesis for object-oriented conditions and preconditions.

  • 3.3 Runtime Trace Collection for Repair: Nopol collects primitive values, object nullness, and state-query results at each angelic location for synthesis.Collected data include local variables, parameters, fields, and side-effect-free methods such as size() and isEmpty() on in-scope objects.
  • 3.3 Runtime Trace Collection for Repair: For buggy conditions, expected outcomes are angelic values on failing tests and actual condition evaluations on passing tests.Nopol collects these outcomes for every execution of the location.
  • 3.3 Runtime Trace Collection for Repair: For missing preconditions, expected outcomes are true on passing tests and false on failing tests so the buggy statement is skipped.This outcome definition directly reflects the missing-precondition angelic localization oracle.
  • 3.3.3 Object-oriented Specific Data Collection: Nopol supports object-oriented repairs by incorporating nullness checks and manually supplied, side-effect-free state-query methods.The state-query method list is domain-specific and supplied to Nopol in advance.

3.4 Encoding Repair in SMT

Nopol encodes repair as a typed component-based synthesis problem in SMT, wiring building blocks to collected inputs so the resulting expression matches expected outcomes across executions. It incrementally expands the available building blocks to manage solver cost.

  • 3.4 Encoding Repair in SMT: Nopol’s SMT encoding searches for a typed expression whose output matches every collected input–outcome pair.The encoding supports Boolean, integer, and real values and translates a satisfying model into a source-level Boolean expression.
  • 3.4.1 Building Blocks: Building blocks include comparisons, arithmetic operators, and Boolean operators, and may appear multiple times in a synthesized expression.Each block has typed inputs, an output, and a formula encoding its semantics.
  • 3.4.2 SMT Encoding: Location variables encode the patch structure, while value variables encode execution-specific values and connect block inputs and outputs.Additional constraints enforce type compatibility, one-to-one wiring, and an acyclic ordering in which arguments are defined before use.
  • 3.4.2 SMT Encoding: The final patch constraint requires one shared wiring structure to satisfy all collected execution pairs and syntactic well-formedness constraints.The functional constraint instantiates collected inputs and expected outputs for each pair before combining them globally.
  • 3.4.5 Levels: Synthesis starts with one instance of inexpensive comparison blocks, then adds logic, arithmetic, and more instances in successive levels.The optimization of these predefined levels remains future work, and division requires care to avoid division by zero.

3.5 Deriving a Patch from an SMT model

When the SMT problem is satisfiable, Nopol receives assignments for location variables and reconstructs the source expression by traversing backward from the designated output. Unconnected building blocks are discarded from the resulting patch.

  • 3.5 Deriving a Patch from an SMT model: A satisfying SMT assignment is converted into source code by backward traversal from the output location.The model may assign locations to building blocks that are not connected to the final output.
  • 3.5 Deriving a Patch from an SMT model: The running example yields the Boolean patch f2(i0, i0), which repairs the buggy condition or missing precondition.The model binds the output to f2, supplies the same integer input twice, and leaves f1 unused.

4. EVALUATION

Nopol is evaluated on three conditional-repair case studies: Tcas, a real Apache Commons Math bug, and a missing-precondition example. Across these cases, it localizes candidate repair points, encodes runtime information as SMT, and produces patches that pass the available tests, including a developer-matching repair for Percentile.

  • 4. EVALUATION: Nopol combines angelic fix localization, whole-test-suite trace collection, SMT encoding, and source-patch generation in its repair workflow.Its prototype uses Spoon, GZoltar, jSMTLIB, and CVC4 for Java source manipulation, localization, SMT generation, and solving.
  • 4.1 Case Study: Tcas Example from SemFix: In Tcas, Nopol generates if (up_sep != 0), a test-suite-correct patch that differs from the SemFix repair because the tests cannot distinguish them.Both patches pass all test cases, while the supplied tests lack cases that separate the alternatives.
  • 4. EVALUATION: The evaluation covers Tcas, a 5,000-line Apache Commons Math library with 352 JUnit tests, and an artificial missing-precondition case.The Tcas example uses 135 lines of code and five test cases; the missing-precondition example uses two test cases.
  • 4.2 Case Study: Commons-Math Library: Nopol matches the developer patch for Apache Commons Math’s Percentile bug using a 352-test suite with one failing test.The synthesized condition is pos >= n, found after analyzing 11 candidate if conditions.
  • 4.3 Case Study: Missing Precondition Example: For the missing-precondition example, Nopol synthesizes if (result.length() < index) to prevent the failing execution from reaching the exception.The repair is equivalent to the original intended condition because result.length() is 0 in the relevant case.

5. LIMITATIONS

Nopol's effectiveness is constrained by its single-fault assumption, the expressiveness of its building blocks, test-suite coverage, supported method calls, and SMT-solver capabilities.

  • Single point of failure: Nopol handles only programs with a single fault because it does not stack patches.Stacking patches would make the search space exponentially larger.
  • Granularity of building blocks: Patch generation depends on building-block granularity: small sets limit repairs, while large sets can produce complex, non-minimal patches.The authors identify improving the selection of building blocks as future work.
  • Non-fixable bugs: Non-trivial repairs for buggy if conditions require both boolean outcomes to appear in at least one passing and one failing test case.Without suitable coverage, Nopol may be unable to synthesize a patch beyond replacing the condition with a Boolean constant.
  • Conditions including methods with parameters: Nopol currently supports conditional method calls without parameters but cannot synthesize conditions requiring methods with parameters.Collecting values for multiple parameters would introduce a combinatorial data-collection step.
  • Limitations of SMT solvers: CVC4 is sufficient for the evaluated constraints, but its lack of full non-linear arithmetic support may hinder conditions using multiplication or division.The evaluation is preliminary, and the authors consider using another solver such as Z3.

6. RELATED WORK

Related work spans test-suite-based repair, semantic constraint solving, fix-pattern mining, probabilistic repair guidance, program synthesis, and fault localization.

  • Test-suite based repair: GenProg generates candidate patches by applying genetic programming to weighted program statements represented in an abstract syntax tree.Its candidates are evaluated repeatedly against a given test suite.
  • Test-suite based repair: SemFix combines symbolic execution, constraint solving, and program synthesis, whereas Nopol additionally repairs missing preconditions.The passage identifies missing-precondition repair as the key difference from SemFix.
  • Test-suite based repair: Par uses predefined fix patterns to avoid nonsensical patches caused by random mutation operators and evaluates patches with human subjects.Its evaluation involved 253 participants, including students and developers.
  • Repair-action mining: Historical repair mining models repair actions probabilistically from more than 62,000 versioning transactions across 14 open-source Java repositories.The resulting distributions can guide future repair as prior knowledge.
  • Program synthesis: Program-synthesis research replaces manual or formal specifications with input-output oracles and uses SMT solvers to synthesize constraints.The cited work evaluates this strategy on 25 program-deobfuscation benchmarks.
  • Fault localization: Fault localization ranks suspicious statements using test spectra and metrics such as Tarantula and Ochiai, while repair localization targets places where patches can be written.The related work distinguishes locating root causes from locating potentially repairable statements.

7. CONCLUSION

Nopol combines angelic fix localization, execution-trace collection, and SMT encoding to repair buggy if conditions and missing preconditions. Preliminary examples include an Apache Common Maths bug and two artificial cases, while broader evaluation and loop-condition support remain future work.

  • Conclusion: Nopol's preliminary evaluation reports fixes for its target fault model on an Apache Common Maths bug and two artificial examples.The approach targets buggy if conditions and missing preconditions in test-suite-based repair.
  • Conclusion: Nopol converts execution traces at suspicious statements into SMT problems and translates solutions into patches.Angelic fix localization is used to identify the suspicious statements.
  • Conclusion: Future work will evaluate Nopol on more real-world bugs and extend it to conditionals in loop structures such as while and for loops.The current conclusion limits the reported evaluation and supported conditional contexts.
Loading 1404.3186v1…