Source-linked AI summary
Automated Fixing of Programs with Contracts
Yu Pei, Carlo A. Furia, Martin Nordio, Yi Wei, Bertrand Meyer, Andreas Zeller
TL;DR
Automated fix synthesis remains difficult, especially for general-purpose software, motivating AutoFix’s contract-guided debugging approach. AutoFix combines dynamic and static analyses with tests to generate and rank validated fixes for contract-annotated programs. Across 204 faults, it produced valid fixes for 42%, with 59% of those fixes judged proper and modest running times, while its applicability is constrained by the need for contracts and automatically testable faults.
Problem
Automating the synthesis of suitable fixes for faults in general-purpose software remains challenging despite advances in automated error detection.
Method
AutoFix uses contracts, dynamic and static analyses, fault localization, and passing and failing tests to generate, rank, and validate candidate fixes automatically.
Results
42% of 204 faults received valid fixes, and 59% of those fixes were proper, with median running time of 3 minutes across experiments.
Takeaways & Limitations
The results support AutoFix as a promising technique for automatically correcting many real-program faults with modest computational resources.
Takeaways & Limitations
AutoFix requires source-code contracts, which are used by only a small minority of software projects, and its experiments relied on automatically generated tests that restrict evaluated projects and faults.
Abstract
from arXiv · showhide
This paper describes AutoFix, an automatic debugging technique that can fix faults in general-purpose software. To provide high-quality fix suggestions and to enable automation of the whole debugging process, AutoFix relies on the presence of simple specification elements in the form of contracts (such as pre- and postconditions). Using contracts enhances the precision of dynamic analysis techniques for fault detection and localization, and for validating fixes. The only required user input to the AutoFix supporting tool is then a faulty program annotated with contracts; the tool produces a collection of validated fixes for the fault ranked according to an estimate of their suitability. In an extensive experimental evaluation, we applied AutoFix to over 200 faults in four code bases of different maturity and quality (of implementation and of contracts). AutoFix successfully fixed 42% of the faults, producing, in the majority of cases, corrections of quality comparable to those competent programmers would write; the used computational resources were modest, with an average time per fix below 20 minutes on commodity hardware. These figures compare favorably to the state of the art in automated program fixing, and demonstrate that the AutoFix approach is successfully applicable to reduce the debugging burden in real-world scenarios.
1 Introduction
AutoFix addresses the difficult problem of automating fault correction by using contracts to guide analysis and validate fixes. Evaluated on over 200 faults, it generated many validated and often high-quality fixes with modest computational resources.
- Automating suitable fix synthesis remains challenging despite increasing availability of automated error-detection techniques.
- AutoFix automatically generates ranked corrections for general-purpose software annotated with preconditions, postconditions, and class invariants.Its current implementation targets Eiffel, while the concepts apply to languages with comparable annotation mechanisms.
- Contracts support fault detection, correction suggestion, and validation, while dynamic invariant inference, static analysis, and fault localization guide ranked fix generation.The process uses test cases and contracts as oracles, requiring only an annotated program as user input.
- 86 of 204 faults, or 42%, received valid fixes, including 51 fixes judged genuine corrections comparable in quality to those competent programmers would write.The remaining valid fixes were useful patches that passed available regression tests but could alter intended behavior.
- AutoFix required modest resources, with average time per fix below 20 minutes on commodity hardware.About half the time was used to generate tests exposing the fault.
2 AutoFix in action
AutoFix detects and repairs a subtle cursor-management fault in a doubly-linked sorted set. Automatically generated tests expose the failure, and the tool produces validated suggestions including a proper correction.
- Moving items in sorted sets: move item removes an element, restores the saved cursor position, and reinserts the element immediately to the cursor’s left.Its implementation searches for the element, removes it, restores index, and calls put left.
- Moving items in sorted sets: The TWO WAY SORTED SET stores elements in a doubly-linked list, with index identifying the cursor position and boundary positions before and after the elements.The example contains four elements at positions 1 through 4, with the cursor at position 2.
- An error in move item: A few minutes of AutoTest expose an error when move item runs with index equal to count + 1, because removal decreases count and invalidates the cursor position.The invalid position causes move item to violate go i th’s precondition.
- An error in move item: The fault generalizes to cases where the moved element lies left of the initial cursor, causing put left to reinsert it incorrectly after removal shifts later elements.An incomplete postcondition fails to characterize this broader faulty behavior.
- An error in move item: AutoFix generates up to 10 valid fix suggestions without user input, including a proper fix that completely corrects the demonstrated error.The suggestions pass all available tests targeting move item.
3 Preliminaries: contracts, tests, and predicates
AutoFix represents contract-driven executions and program states with tests, expressions, Boolean predicates, and implications. These abstractions support fault identification, state comparison, and subsequent repair actions.
- Contracts and tests: Contracts specify correct routine behavior through preconditions, postconditions, intermediate assertions, and class invariants.Violating an assertion or a callee precondition identifies a fault at a routine location and contract clause.
- Contracts and tests: A test case is passing when it terminates without violating a contract and failing otherwise; each fixing session partitions tests into passing and failing sets for one targeted fault.The targeted fault is identified by its routine, failure location, and violated contract clause.
- Contracts and tests: AutoFix’s algorithm is independent of test-case origin, although the experiments use AutoTest random testing to make fault detection and fixing fully automatic.Short AutoTest sessions can produce suitable test cases for generating fixes.
- Predicates and state abstraction: AutoFix abstracts runtime object states using argumentless Boolean queries, expressions from program text or contracts, and Boolean combinations of these predicates.Boolean queries characterize absolute object properties and are always defined when they have no preconditions.
- Predicates and state abstraction: For a failing routine and contract clause, AutoFix extracts expressions, unfolds applicable queries, and combines them into Boolean predicates and their complements.The example includes routine and contract expressions such as Result, index, and comparisons involving constants.
- AutoFix pipeline: The overall pipeline generates passing and failing tests, identifies suspicious snapshots by comparing executions, synthesizes fix actions, and validates candidates against regression tests.Candidates that pass the regression suite are output to the user.
- Predicates and state abstraction: AutoFix also uses contract implications and mutated forms to capture object-state correlations, pruning redundant implications with Z3.Considering all possible implications would produce too many irrelevant predicates.
4 How AutoFix works
AutoFix processes failing and passing tests through behavioral abstraction, fault localization, fix synthesis, candidate validation, and ranking. It uses contracts and combined dynamic, static, and behavioral analyses to generate fixes, distinguishing merely valid fixes from proper fixes when specifications support that judgment.
- Program-state abstraction: AutoFix starts from passing and failing tests exposing a contract violation, then represents executions with snapshots linking a program location, predicate, and Boolean value.Snapshots are constructed through invariant analysis and enumeration.
- Fix synthesis: AutoFix synthesizes fix actions from snapshots, heuristics, behavioral abstractions, and specialized techniques for integer expressions, then instantiates predefined conditional fix schemas.The schemas inject candidate actions at selected program locations.
- Validation and ranking: Candidate fixes are retained when they pass all available tests, ranked by heuristic quality measures, and often include several valid alternatives for the same fault.Dynamic analysis is the principal source of evidence in the overall score.
- Fault localization: Dynamic analysis ranks snapshots rather than only locations, while control and expression dependence prioritize proximity to the failure and similarity to the violated contract.This adapts fault-localization principles to the state information needed for repair.
- Validation and ranking: A proper fix satisfies a routine’s complete behavioral specification, whereas an improper fix is valid but fails that specification; practical contracts can nevertheless often support confident proper-fix classification.The distinction separates fixes that merely evade available contract violations from fixes that remove faults without introducing other faulty or unexpected behavior.
- Validation and ranking: High-quality proper fixes often rank among the top 10 valid fixes, reducing the inspection burden for users selecting a deployable correction.Users can inspect the highest-ranked suggestions rather than the entire collection.
5 Experimental evaluation
AutoFix produced valid fixes for 42% of 204 faults, and 59% of those fixes were proper. Its results were generally repeatable and computationally modest, but success depended on reproducible failures and correct, sufficiently complete contracts.
- 86 (42%) of 204 randomly detected faults received valid fixes from AutoFix.
- 51 (59%) of the 86 valid fixes were proper, with quality comparable to fixes produced by professional programmers.Proper fixes represented 25% of all unique faults considered.
- AutoFix ran no more than 15 minutes per fault in 93.1% of experiments, with a median running time of 3 minutes.The reported standard deviation was 6.3 minutes.
- 48 (56%) of the faults fixed at least once were fixed in over 95% of sessions, showing substantial robustness to test-case variation.Across non-empty sessions, AutoFix produced a valid fix in 41% of sessions.
- Failure commonly arose when faults could not be reproduced or when contracts were incorrect or incomplete.Without failing test cases, AutoFix cannot be expected to work; incorrect or incomplete contracts can prevent the implementation from satisfying the specification.
- Proper fixes required more time on average than valid fixes, with a substantial fraction taking up to about 70 minutes.Most valid fixes were produced in 35 minutes or less, whereas proper fixes had a less strongly skewed time distribution.
6 Related work on automated fixing
Automated fixing research spans source-code repair, specialized domains, runtime techniques, and search-based approaches. AutoFix combines contracts with analysis and synthesis strategies, while its evaluation is comparable mainly to GenProg and Par and remains limited in scalability evidence.
- Automated fixing research covers source-code techniques, specialized domains, and runtime approaches.
- GenProg uses genetic programming to mutate programs until they pass regression tests, whereas Par combines genetic programming with predefined human-derived fix patterns.
- GenProg and Par are the only related source-code approaches evaluated comparably with AutoFix; other methods used seeded faults, few benchmarks, or lacked complete automation.
- AutoFix fixed 42% of 204 faults, while GenProg fixed 52% of 105 and Par fixed 23% of 119, but the figures are not directly comparable.
- AutoFix showed robustness to automatically generated tests, but more experiments are needed to evaluate scalability on much larger programs.
- AutoFix combines fault localization, fix actions and schemas, contracts, and automatic test-case generation for source-code repair.
7 Conclusions
Automated debugging has progressed from locating failures to generating workable fixes. AutoFix generated fixes for 42% of over 200 faults, often with programmer-comparable quality and under 20 minutes per fix, while retaining human assessment of generated code.
- Automated debugging evolved from failure isolation and localization toward completely automatic generation of workable fixes.
- AutoFix generated fixes for 42% of faults in experiments covering over 200 faults across software of various quality.
- 59% of AutoFix’s generated fixes were judged real corrections comparable in quality to those programmers familiar with the faulty programs could write.
- AutoFix required under 20 minutes per fix on standard hardware, including failed attempts and automatic test-case generation.
- Contracts are a key ingredient because they support and automate the debugging steps while requiring effort comparable to everyday programming activities.
- Human assessment remains assumed before generated fixes are retained, despite the possibility of fully automatic application.
Appendices
The appendix contains additional material omitted from the main text, organized under corresponding main-text section titles.
- The appendix provides additional material omitted from the main text and uses corresponding section titles for organization.
A.1 Another error in move item (Section 2.2)
The appendix illustrates two contract violations in move item: an invalid insertion position when index is 0 and an invalid boundary position after removal without updating index.
- When index is 0, go ith permits the position, but put left violates its precondition because no position exists to the left.
- At the boundary position count + 1, remove can delete an element without updating the cursor index.
- The second fault becomes invalid after removing an element inside the list, leaving the cursor position inconsistent with the list.
A.2 Automatic corrections of the errors in move item (Section 2.3)
AutoFix generates up to 10 valid fix suggestions for each of two errors in move item, including proper fixes that completely correct the errors. Other suggestions may pass available tests yet fail to capture the routine’s intended semantics.
- Generated corrections: Up to 10 valid fixes are generated for each of the two move item errors.The fixes pass all available tests targeting move item.
- Error-specific corrections: For the error occurring when v starts left of index, the fix decrements idx when idx > index after remove decreases count.The correction inserts lines 44–46 before the call to go ith.
- Proper versus improper fixes: Some alternative fixes pass all available tests but avoid failure without fully capturing move item’s intended implicit semantics.One improper fix discards v when before is false instead of preserving the programmer’s likely intent.
B.1 Experimental subjects (Section 5.2.1)
The experimental-subject metrics are presented in Table 27, which reports average code-base size and other measures after averaging over classes.
- Experimental subjects: Table 27 presents the same information as Table 7.
- Experimental subjects: The values in Table 27 are averaged over the number of classes.
- Experimental subjects: Table 27 reports the average size and other metrics of the code bases.
B.2 Experimental results (Section 5.3)
The experimental-results discussion includes a preliminary analysis of whether AutoTest produced tests of sufficient quality for fixing.
- Experimental results: Section B.2.1 preliminarily discusses how often AutoTest provided tests of good quality suitable for fixing.
- Experimental results: The test-quality discussion concerns AutoTest sessions used in the experimental evaluation.
- Experimental results: The discussion focuses on the suitability of generated tests for fixing.
B.2.1 Testability of the experimental subjects
The four code bases differ in testability: Base is generally easy to test, Cards and ELearn are harder, and TxtLib is mixed. Statistical tests confirm significant differences between the grouped subjects and in failing-test frequency.
- Testability measures: AutoTest’s testability distributions are summarized with histograms of tests generated across repeated sessions for each routine.Figure 28 covers four individual code bases and an overall distribution.
- Testability measures: Base is normally easily testable, Cards and ELearn are hard to test on average, and TxtLib is mixed.The text associates Base’s testability with its carefully designed interface and contracts.
- Statistical comparisons: Inter-group testability differences are significant, while intra-group differences are not significant for the specified partitions.The reported ranges are 692 ≤ U ≤ 1272 with p > 0.06 within groups, versus 264 ≤ U ≤ 1754 with p < 0.03 between groups.
- Failing-test frequency: The failing-to-passing test ratio is evaluated from repeated AutoTest sessions using a logarithmic horizontal scale.Figure 29 depicts the distribution of the mean ratio for each routine.
- Failing-test frequency: Base produces failing tests less frequently than the other code bases.The difference is significant for Base versus the other three code bases, with 105 ≤ U ≤ 445 and p < 10^-7.
C.1 Fault detection: automatic testing
AutoFix’s evaluation uses automatic testing approaches, including random and search-based techniques, with Figure 29 reporting failing-to-passing test ratios on logarithmic scales.
- Random testing is a simple automatic-testing approach applied successfully to diverse programs and libraries.
- Search-based test generation refines random testing to improve performance and accuracy, often using genetic algorithms.
- The evaluation also considers white-box testing techniques and approaches that use formal specifications.
C.2 Fault localization
AutoFix combines fault-localization techniques with contracts and dynamic analysis to narrow the code locations considered for automatic repair. The broader literature includes coverage-, state-, test-similarity-, and predictor-based approaches, while automated fixing extends localization toward synthesizing corrections.
- Fault localization identifies statements likely needing change to correct a fault, commonly using code coverage or program states.
- Coverage-based methods rank instructions by failure-related execution patterns, while state-based methods identify suspicious program states.
- Nearest-neighbor localization compares failing and passing tests to isolate candidate instructions, whereas Angelina reports runtime expressions whose changes may make failures pass.
- Automated localization can struggle with interacting faults, motivating techniques that separate effects and identify predictors for individual faults.
- Automated fixing addresses the broader debugging burden by adding correction synthesis beyond localization.
- AutoFix uses contracts to restrict localization to routine boundaries for contract-violation faults, then combines dynamic analysis techniques.