Add loopinv tool that supports C to imp conversion for LFP-based loop invariant computation

[flyingapricot]

This MR introduces the first half of the loopinv tool, which is to build constraint abstractions of loops in C, and then use it to compute loop invariants via LFP.

Description

The tool currently converts C source code into Imp syntax, which serves as the constraint abstraction representation.

The existing imp tool then processes this Imp code and invokes fixCalc to compute the Least Fixed Point (LFP), which represents the loop invariant relation.

This PR focuses solely on the C-to-Imp conversion and integration with the existing imp tool, it does not yet generate ACSL annotations for Frama-C.

High-Level Approach

C source code is first tokenized by the lexer (Lexer.hs), which breaks the input into meaningful tokens such as keywords, identifiers, operators, and literals.

These tokens are then processed by a recursive descent parser (Parser.hs), which builds an Abstract Syntax Tree (AST) representing the program structure. The AST types are defined in AST.hs and support a subset of C including function definitions, variable declarations, while loops, assignments, and arithmetic/logical expressions.

Once the AST is constructed, the Imp emitter (ImpEmit.hs) traverses the tree and generates equivalent Imp code. The key syntactic differences handled during this translation include converting = to := for assignments, adding do after while conditions, and using ; as a statement separator rather than terminator. The main driver (Main.hs) orchestrates this pipeline: it reads the C file, runs the conversion, writes the generated Imp file, and then invokes the existing imp tool with the +infer flag to compute the LFP via fixCalc.

The output displayed is the raw result from the imp tool, which includes the computed LFP relation. This relation captures all possible input-output behaviors of the loop. For example, showing that a loop variable increases by a certain amount each iteration and what condition holds upon termination.

Usage

cd fixcalc_src
make loopinv
./loopinv-bin loopinv/examples/test1.c

# Result
================================================================
  LoopInv - Constraint Abstraction & LFP Computation
================================================================

Input: loopinv/examples/test1.c

=== Original C Code ===
// Simple counting loop
// Expected: loop invariant 0 <= x <= n

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




=== Converting to Imp (Constraint Abstraction) ===
Generated: loopinv/examples/test1.imp

#include "Primitives.imp"

void simple(int n) {
  int x := 0;
  while ((x < n)) do {
    x := (x + 1)
  }
}
=== Running imp tool (LFP computation via fixCalc) ===

Parsing...done!
Simple type-checking...done!
Inferring whilef_0...
Inferring whilef_0...done in 0.022991166 seconds
Inferring simple...
Inferring simple...done in 0.000637457 seconds
Inference...done in 0.023710586 seconds
============
SAFETY: All checks in the program were proven!
Total CPU time: 0.027611071 seconds

=== LFP Result (a.impt) ===

#include "Primitives.imp"

{-
OK:={[f_3]:(f_3 >= 1 || 0 >= f_3)};
ERRs:={ERR:(1 = 0)}
NEVER_BUG:={[f_3]:(f_3 >= 1 || 0 >= f_3)};
MUST_BUGs:={MUST_BUG:(1 = 0)}
MAY_BUG:=MAY_BUG:(1 = 0)
-}
Void simple(Int<f_3f> n)
  where
  ((f_3f >= 1 || 0 >= f_3f)),
  {NEVER_BUG:((f_3f >= 1 || 0 >= f_3f))}
{{
 Int<f_4f> x := 0;
 l_5:whilef_0(x,n)
 }}

{-
OK:={[PRMf_6,f_6,PRMf_7,f_7]:((PRMf_6 >= 1 + f_6 && PRMf_6 = PRMf_7 && PRMf_6 = f_7) || (PRMf_6 >= f_7 && f_7 = PRMf_7 && PRMf_6 = f_6))};
ERRs:={ERR:((1 = 0 || 1 = 0))}
NEVER_BUG:={[f_7,f_6]:(f_7 >= 1 + f_6 || f_6 >= f_7)};
MUST_BUGs:={MUST_BUG:(1 = 0)}
MAY_BUG:=MAY_BUG:(1 = 0)
-}
ref Void whilef_0(ref Int<f_6f> x,ref Int<f_7f> n)
  where
  (((PRMf_6f >= 1 + f_6f && PRMf_6f = PRMf_7f && PRMf_6f = f_7f) || (PRMf_6f >= f_7f && f_7f = PRMf_7f && PRMf_6f = f_6f))),
  {NEVER_BUG:((f_7f >= 1 + f_6f || f_6f >= f_7f))}
{{
 Bool<f_13f> v_14 := l_8:lt(x,n);
 if v_14
  then { {
   Int<f_11f> v_12 := 1;
   x:=l_9:plus(x,v_12)
   };
   l_10:whilef_0(x,n)
  } else { Void }
 }}