Loop Pre/Post Condition Generation with Exactness Verification

[flyingapricot]

This PR aims to the loopinv tool to generate pre- and post-conditions for C loops using Least Fixed Point (LFP) computation, with an exactness verification to classify results as EXACT (EX) or OVER-APPROXIMATE (OX).

---

Feature 1: Loop Pre/Post Conditions in Case Format with Prime Notation

Approach

1. Parse C code and convert to imp tool's intermediate representation
2. Run the imp tool to compute the relational LFP (least fixed point) that captures the input-output relationship of each loop
3. Extract the LFP formula from a.impt output file
4. Convert to prime notation where:
   • x = pre-state value (value before loop)
   • x' = post-state value (value after loop)
5. Split LFP into disjuncts - each disjunct represents a different execution case
6. Format as case clauses in the form:

   case { precondition ens postcondition }
   

Output Format

=== Loop Pre/Post Conditions ===
Raw LFP: (PRMf_xf=f_nf & f_xf>=f_nf) | (PRMf_xf=f_nf & 1+f_xf<=f_nf)
Prime Notation: (x'=n & x>=n) | (x'=n & 1+x<=n)

Disjunct 1: x'=n & x>=n
Disjunct 2: x'=n & 1+x<=n

case { x>=n ens x'=n }
case { 1+x<=n ens x'=n }

Results

Test Case	Description	Cases Generated
test1.c (simple loop)	while(x<n) x++	case { x>=n ens x'=n }, case { 1+x<=n ens x'=n }
test3.c (countdown)	while(x>0) x--	case { x<=0 ens x'=0 }, case { x>=1 ens x'=0 }
test2.c (nested)	nested loops	Multiple cases for inner/outer loops
test_tricky.c	while(x<n) x+=2	case { true ens x'>=n }

---

Feature 2: EX/OX Exactness Verification

Motivation

LFP computation may use widening to ensure termination, which can result in over-approximations. We need a way to determine if the computed LFP is:

• EXACT (EX): Precisely captures the loop's behavior
• OVER-APPROXIMATE (OX): Sound but may include spurious behaviors

Approach - Semantic Fixed-Point Verification

We verify exactness by checking if F satisfies the fixed-point equation:

F = base ∪ (F ∘ step)

Where:

• F = the computed LFP (relational summary)
• base = loop exit condition (when loop doesn't execute)
• step = single iteration effect
• ∘ = relational composition

Verification Logic:

1. Generate a fixcalc query that defines:

   • F(x, n, x', n') - the computed LFP
   • base(x, n, x', n') - base case: x >= n && x' = x && n' = n
   • step(x, n, x', n') - step relation: x < n && x' = x + 1 && n' = n
   • Fcomp(x, n, x', n') - composition: ∃x_t, n_t: F(x, n, x_t, n_t) && step(x_t, n_t, x', n')
   • combined - base || Fcomp

2. Check bidirectional subset relations:

   F ⊆ combined  (soundness)
   combined ⊆ F  (completeness)
   

3. If both hold, result is EXACT (EX); otherwise OVER-APPROXIMATE (OX)

Results

Test Case	Result	Reason
test1.c (simple loop)	EX	Linear arithmetic, exact computation
test3.c (countdown)	EX	Linear arithmetic, exact computation
test2.c (nested)	OX	Complex control flow requires widening
test_tricky.c	OX	Non-linear increment (x+=2) - Presburger arithmetic cannot express parity constraints

Sample Output

=== Exactness Verification ===
Generating exactness check query...
Running fixcalc verification...
Result: EXACT (EX)
The computed LFP precisely captures the loop's input-output relation.

---

Testing

Test 1: Simple Loop (test1.c) - EX

void simple(int n) {
    int x = 0;
    while (x < n) { x = x + 1; }
}

Output:

Prime notation: (((x' >= 1 + x && x' = n' && x' = n) || (x' >= n && n = n' && x' = x)))

case {
  n >= 1 + x ens x' = n && n' = n
  x >= n ens n' = n && x' = x
}

=== Result: EX ===
The LFP is EXACT - it precisely captures the loop's input-output relation.

Test 2: Countdown Loop (test3.c) - EX

void countdown(int n) {
    int x = n;
    while (x > 0) { x = x - 1; }
}

Output:

Prime notation: (((x >= 1 && 0 = x') || (0 >= x' && x' = x)))

case {
  x >= 1 ens x' = 0
  0 >= x ens x' = x
}

=== Result: EX ===
The LFP is EXACT - it precisely captures the loop's input-output relation.

Test 3: Tricky Loop (test_tricky.c) - OX

void tricky(int n) {
    int x = 0;
    while (x < n) { x = x + 2; }
}

Output:

Prime notation: ((((n' >= 1 + x && x' >= 2 + x) && n' = n) || ((x' >= n' && x' >= x) && n' = n)))

case {
  n >= 1 + x ens n' = n && x' >= 2 + x
  true ens n' = n && x' >= n && x' >= x
}

=== Result: OX ===
The LFP is OVER-APPROXIMATE - it may include behaviors that cannot happen.

This loop is OX because Presburger arithmetic cannot express parity constraints (the exact result would be x' = n or x' = n + 1 depending on parity).

---

Limitations

1. Presburger Arithmetic: fixcalc only supports linear integer arithmetic. Non-linear operations (multiplication, modulo) lead to over-approximations.
2. Nested Loops: Complex nesting patterns may trigger widening, resulting in OX results even when a more precise analysis might exist.