Model Guided Code Repair

Model-Guided Code Repair

Overview

This skill enables automatic repair of code that violates temporal properties by analyzing model-checking counterexamples. It reasons about the root cause of violations at the model level, proposes minimal and semantically justified code modifications, and validates repairs through re-verification or test generation.

Repair Workflow

Follow this sequential process when repairing temporal property violations:

1. Analyze Input

Gather and understand three required inputs:

• Program source code: The code containing the violation
• Violated temporal property: The formal specification (LTL, CTL, or natural language description)
• Counterexample trace: The execution path demonstrating the violation

Read all inputs carefully. If the temporal property is in natural language, formalize it first.

2. Understand the Counterexample

Trace through the counterexample step-by-step:

• Identify the sequence of states and transitions
• Map counterexample states to program locations (line numbers, function calls)
• Identify variable values at each step
• Pinpoint the exact moment the property is violated

Output: A clear narrative of the execution path leading to the violation.

3. Identify Root Cause

Analyze why the violation occurs:

• Missing guards: Are conditions missing that should prevent certain transitions?
• Incorrect ordering: Are operations executed in the wrong sequence?
• Race conditions: Are there synchronization issues in concurrent code?
• Missing state updates: Are variables not being updated correctly?
• Incorrect logic: Are conditional expressions wrong?

Output: A precise diagnosis of the model-level cause.

4. Propose Repair Strategy

Design a minimal repair that:

• Directly addresses the root cause
• Preserves intended program behavior
• Minimizes code changes
• Maintains code readability

Common repair strategies:

• Add guards: Insert conditional checks to prevent invalid transitions
• Reorder operations: Adjust execution sequence to satisfy temporal ordering
• Add synchronization: Insert locks, semaphores, or barriers for concurrent code
• Update state management: Fix variable assignments or state transitions
• Strengthen preconditions: Add assertions or input validation

Output: A clear repair plan with justification.

5. Generate Repaired Code

Implement the repair:

• Make minimal, targeted changes to the source code
• Clearly mark what was changed (comments or annotations)
• Ensure the repair is syntactically correct
• Preserve existing code style and conventions

Output: Modified source code with changes clearly indicated.

6. Validate the Repair

Verify that the repair resolves the violation:

Option A: Re-run Model Checker

• Execute the model checker on the repaired code
• Verify the temporal property now holds
• Check that no new violations were introduced

Option B: Generate and Run Tests

• Create test cases based on the counterexample
• Generate additional tests for edge cases
• Execute tests and verify they pass
• Ensure existing tests still pass (regression testing)

Output: Validation results showing the property is satisfied.

7. Document the Repair

Provide a comprehensive explanation:

• Root cause: What caused the violation
• Repair strategy: Why this approach was chosen
• Minimality justification: Why this is the smallest necessary change
• Behavior preservation: How intended functionality is maintained
• Validation results: Evidence that the repair works

Output Format

Structure the final output as follows:

## Repaired Code

[Modified source code with changes clearly marked]

## Changes Made

- [Line X]: [Description of change]
- [Line Y]: [Description of change]

## Root Cause Analysis

[Explanation of what caused the violation]

## Repair Strategy

[Why this repair approach was chosen]
[Why it is minimal and semantically justified]

## Behavior Preservation

[How the repair maintains intended program behavior]

## Validation Results

[Model checking results OR test execution results]
[Confirmation that the property now holds]

Common Scenarios

Safety Property Violations

Example: "The system must never enter an error state"

• Look for missing error checks or exception handling
• Add guards to prevent invalid state transitions
• Validate with assertions or model checking

Liveness Property Violations

Example: "Every request must eventually be processed"

• Look for deadlocks, infinite loops, or missing progress conditions
• Add fairness constraints or progress guarantees
• Validate with liveness checking or timeout tests

Synchronization Issues

Example: "Shared resources must be accessed atomically"

• Look for race conditions or missing locks
• Add synchronization primitives (mutexes, semaphores)
• Validate with concurrency testing or model checking

State Machine Violations

Example: "State transitions must follow the specified protocol"

• Look for missing state checks or incorrect transition logic
• Add state validation or fix transition conditions
• Validate with state machine verification

Tips for Effective Repairs

• Start simple: Try the minimal fix first before complex refactoring
• Preserve structure: Maintain the original code architecture when possible
• Consider side effects: Ensure repairs don't break other properties
• Document assumptions: Note any assumptions made during repair
• Test thoroughly: Validate beyond just the violated property
• Iterate if needed: If the first repair doesn't work, analyze why and adjust

Integration with Model Checkers

This skill works with various model checking tools:

• SPIN: For Promela models and LTL properties
• NuSMV/nuXmv: For SMV models and CTL/LTL properties
• CBMC: For C programs with assertions
• Java PathFinder: For Java programs
• TLA+: For TLA+ specifications

When counterexamples are provided in tool-specific formats, translate them into a clear execution trace before analysis.