One example to understand SemFix: Program Repair via Semantic Analysis

One example to understand SemFix: Program Repair via Semantic Analysis

Basic Information

• Authors: Hoang Duong Thien Nguyen, Dawei Qi, Abhik Roychoudhury
• Pulication: ICSE'13
• Description: Semantic Program Repair

Example

Buggy code:

Test Suite:

Overview

Step 1: Fault Localization

Tarantula is applied to produce a suspiciousness ranklist of statements.

Step 2: Generate Repair Constraint via Symbolic Execution

Constraints: f(1, 11, 110) > 110∧f(1, 0, 100) ≤ 100∧f(1, −20, 60) > 60

Step 3: Generate a Repair

Employ program synthesis to solve the constraint for f in order to get a concrete function. Program synthesis requires basic components (e.g. constants, 「+」, 「−」) as ingredients to construct the function f.
In this technique, these components are incrementally provided to program synthesis.

In the first trial, only a constant is allowed. However, no constant function can satisfy the above constraint. We then allow function f to use one 「+」, i.e. f can take either the form of var1 + c or var1+var2, where var1 and var2 are in {inhibit, up_sep, down_sep} and c is an integer constant. The synthesis procedure can find a solution f(inhibit, up sep, down sep) = up sep + 100 which is a successful repair to the program in Fig. 1. Note that if 「−」 is used instead of 「+」, we will get f(inhibit, up sep, down sep) = up sep − (−100) as repair.