AutoFix: Automated Fixing of Programs

AutoFix targets automatic generation of fixes to faulty implementations. For information about automatic program repair by fixing contracts, please visit the homepage of the SpeciFix tool.

Overview

In program debugging, finding a failure is only the first step; what about locating and correcting the fault? Can we automate the whole process? The AutoFix project targets the automatic generation and validation of fixes for software faults.

AutoFix is a joint project between the Chair of Software Engineering of ETH Zurich and the Software Engineering Chair of Saarland University.

This page describes two tools developed within the AutoFix project that work on Eiffel source code: AutoFix-E, based on behavioral models of a class, and AutoFix-E2, introducing evidence-based techniques. The key insight behind both tools is to rely on contracts present in the software to ensure that the proposed fixes are semantically sound.

Model-based fixing in AutoFix-E: example and description

Let's consider a real fault found in routine duplicate from class TWO_WAY_SORTED_SET, and see how AutoFix can propose corrections for this fault. The duplicate routine takes a nonnegative argument n and returns a new set containing at most n elements starting from the current position of  the associated internal iterator, called cursor. After saving the current position of cursor as pos and initializing an empty set as Result, duplicate enters a loop that navigates the set data structure and iteratively adds the current item to Result, calls forth to move to the next element in the set, and updates the counter.

Figure 1.a shows the original faulty implication of duplicate, and Figure 1.b shows the fixed version suggested by AutoFix:

duplicate (n: INTEGER): TWO_WAY_SORTED_SET   
        -- Copy of sub-set beginning at cursor position,
        -- containing at most n element.

    do
        pos  := cursor
       
Result := new_chain
       
Result.forth

        from until  (counter  = n) or after loop



           
Result.put_left  (item)
            forth
            counter  := counter + 1

        end
        go_to (pos)
   
end


duplicate (n: INTEGER): TWO_WAY_SORTED_SET   
        -- Copy of sub-set beginning at cursor position,
        -- containing at most n element.

    do
        pos  := cursor
        Result := new_chain
        Result.forth

       
from until  (counter  = n) or after loop
           
if before then
                forth
           
else
               
Result.put_left (item)
                forth
                counter  := counter + 1
           
end
       
end
        go_to (pos)
   
end

(a) Faulty routine
(b) Fixed routine
Figure 1. A real fault from TWO_WAY_SORTED_SET.duplicate

The problem in the faulty version lies in the first line of the loop body, in the call to the query item, which returns the element under current cursor position. item only makes sense when the cursor is in side the list, so it has the following precondition:

item: ANY
        
-- Element under cursor
    
require (not before)  and  (not after)

The original crash of the program is indeed a precondition violation of the query item. In the context of duplicate, the second half of the precondition not after is guaranteed by the loop exit condition, so the reason of the failure must be that the cursor is in the before position. The failing situation is demonstrated in Figure 2.

Failing situations of item.
Figure 2. Failing situations of item.

Now let's have a look at the automatically fixed version on the right of the first graph. Autofix proposed this version after a few minutes of analysis. The fix is only inside of the loop body: an if-statement wraps around the original loop body. In the then-branch, forth is called to move cursor one position ahead, guarded by the condition before, otherwise, the original loop body is called in the else-branch.

How can AutoFix come up with this fix? There are two key steps:
  1. Find out the necessary failing condition by analyzing state invariant at each program location, especially the location right before the failue.
  2. Try to invoke some method to break the necessary failing condition before the failing location.
Figure 3 shows the architecture of the fixing process of AutoFix-E. AutoTest is first used to test the class, which generates both failing tests revealing faults, and passing tests revealing normal behavior of the tested routines. By analyzing the executions of the generated tests, we can find out that the expression before is always True only in failing tests, but False in all passing tests. This information is called fault profile. It shows strong hint of why a failure came to be. By analyzing only the passing tests, we can find out how different routines affect different queries. For example, by calling forth, we can change the query before from True to False. This information is called finite-state abstraction, or object behavior model.

Fixing process of AutoFix-E
Figure 3. Fixing process of AutoFix-E

In short, the fault profile tells us why there is a failure, that is the necessary failing condition, and the finite-state model tells us how to change the system state to avoid the necessary failing condition. AutoFix uses these two pieces of information to synthesize candidate fixes, and rerun the tests to validate those candidates. A candidate is reported as fix suggestions if and only if is passing all tests. For more details, you can check out the following slides, or the paper entitled Automated Fixing of Programs with Contracts listed below.

Evidence-based fixing in AutoFix-E2: example and description

Figure 4.a shows another faulty routine in class TWO_WAY_SORTED_SET. The routine move_item takes an argument v, which must be a non-Void element stored in the set, and moves it to the position to the left of the internal cursor (attribute index). To this end, the routine saves the cursor position into a local variable idx, moves index to where v occurs in the set, removes this occurrence of v, restores index to its initial position, and inserts v to the left of the cursor. The implementation shown fails with a violation of go_i_th(idx)'s precondition whenever the internal cursor initially points to the last valid cursor position count + 1 (see Figure 5). In fact, the removal of one element in the set invalidates the position stored in idx, expressible as count + 2 with respect to the value of count after removal. A closer look reveals that the routine is incorrect even in cases when this precondition violation does not occur: if v appears to the left of the internal cursor initially, the sequence of operations moves v to an incorrect "off-by-one" position. Figure 4.b shows a fix suggested by AutoFix-E2; the fix corrects the routine even for the cases when it does not trigger a precondition violation invoking go_i_th(idx).

    move_item (v: G)
            -- Move `v' to the left of cursor.
        require
            v /= Void
            has (v)
        local
            idx: INTEGER
            found: BOOLEAN
        do
            idx := index
            from start until found or after loop
                found := (v = item)
                if not found then forth end
            end
            check found and not after end
            remove

            go_i_th (idx)
            put_left (v)

        end

  go_i_th (i: INTEGER) require 0 <= i <= count + 1
  put_left (v: G) require not before
  before: BOOLEAN do Result := (index = 0) end

ove_item (v: G)
            -- Move `v' to the left of cursor.
        require
            v /= Void
            has (v)
        local
            idx: INTEGER
            found: BOOLEAN
        do
            idx := index
            from start until found or after loop
                found := (v = item)
                if not found then forth end
            end
            check found and not after end
            remove
           
if index < idx then idx := idx - 1 end
            go_i_th (idx)
            put_left (v)

        end

  go_i_th (i: INTEGER) require 0 <= i <= count + 1
  put_left (v: G) require not before
  before: BOOLEAN do Result := (index = 0) end
(a) Faulty routine
(b) Fixed routine
Figure 4. A real fault from TWO_WAY_SORTED_SET.move_item

The effect of calling remove in move_item when index  = count + 1 and after hold initially
Figure 5. The effect of calling remove in move_item when index  = count + 1 and after hold initially: the following invocation of go_i_th(idx) triggers a precondition violation.


Fixing process of AutoFix-E2
Figure 6: How evidence-based fixing works. Run AutoTest to automatically generate passing and failing test cases for the input Eiffel classes. Extract a set of expressions from the text of the classes' routines. Compute the expression dependence score edep between expressions—measuring their syntactic similarity—and the control dependence score cdep between program locations—measuring  how close they are on the control-flow graph. Compute the dynamic score dyn between expressions, measuring how more often an expression is mentioned in failing rather than passing test cases. Combine the three scores (edep, cdep, dyn) into the score fixme, which determines a global ranking of expressions. Enumerate possible fixing actions for the expressions with highest fixme score. Generate candidate fixes by injecting the fix actions into the faulty routine. The candidate fixes that pass all the regression test suite are considered valid.

Experiments with AutoFix-E and AutoFix-E2

In an experiment conducted in Febrary 2010, we applied AutoFix-E to 42 faults found in production Eiffel software, and it was able to fix 16 (38%) of them. We selected a few faults and sent them to profressional Eiffel programmers, and most of the time, they reported exactly the same fixes. (Faults, results, and a short user manual)

The experiments with AutoFix-E2 include two data sets. In the first one, AutoFix-E2 was applied to 15 faults from EiffelBase (in large part, a subset of the faults used to evaluate AutoFix-E mentioned above); AutoFix-E2 produced correct fixes for 12 of these faults, some of which are beyond the capabilities of AutoFix-E. The second data set includes 5 faults from a library manipulating text documents developed as student project; AutoFix-E2 fixed 3 of these faults. (This package includes the complete data sets.)

The papers mentioned in the publications section of this page detail the experiments with AutoFix-E and AutoFix-E2.

Downloads

AutoFix-E and AutoFix-E2 are part of the Eve integrated verification environment, the research branch of EiffelStudio

Funding

The following subjects have contributed to funding the AutoTest project:

Publications

Contacts



Dynamic contract inference system