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

Makefile

@@ -48,7 +48,7 @@ OBJS = ImpMain.o ImpParser.o ImpTypeChecker.o ImpFormula.o ImpAST.o \
 .y.hs:
 	happy -agci $<
 
-all: imp fixcalc
+all: imp fixcalc loopinv
 
 imp : $(OBJS) ImpParser.y ImpMain.hs
 	rm -f $@
@@ -58,6 +58,7 @@ imp : $(OBJS) ImpParser.y ImpMain.hs
 
 clean:
 	rm -f *.hi *.o *~ imp ImpParser.hs *.info a.omega a.all.c a.c a.out a.impi a.impt a.omega-err a.pre oc.out fixcalc FixCalcParser.hs log
+	rm -f loopinv-bin $(LOOPINV_DIR)/*.hi $(LOOPINV_DIR)/*.o
 
 install: fixcalc
 	scp fixcalc popeeaco@loris-7.ddns:/home/popeeaco/bin/.
@@ -77,6 +78,23 @@ fixcalc: $(FixCalcOBJS) FixCalcParser.y FixCalcMain.hs
 	ghc -o fixcalc $(HC_OPTS) -lstdc++ FixCalcMain.hs $(LIBS) $(OMEGA_LIBS)  $(RAZVAN_LIBS)
 #####
 
+##### LoopInv - Loop Invariant Generator
+LOOPINV_DIR = loopinv
+LOOPINV_SRCS = $(LOOPINV_DIR)/AST.hs $(LOOPINV_DIR)/Lexer.hs \
+               $(LOOPINV_DIR)/Parser.hs $(LOOPINV_DIR)/ImpEmit.hs \
+               $(LOOPINV_DIR)/Main.hs
+
+loopinv: $(LOOPINV_SRCS) imp
+	ghc -o loopinv-bin -i$(LOOPINV_DIR) -package process -package filepath \
+	    --make $(LOOPINV_DIR)/Main.hs
+
+loopinv-test: loopinv
+	cd $(LOOPINV_DIR)/examples && ../../loopinv-bin test1.c
+
+loopinv-clean:
+	rm -f loopinv-bin $(LOOPINV_DIR)/*.hi $(LOOPINV_DIR)/*.o
+#####
+
 static: $(FixCalcOBJS) FixCalcParser.y FixCalcMain.hs
 	rm -f fixcalc
 	ghc -o fixcalc $(HC_SOPTS) -lstdc++ FixCalcMain.hs $(LIBS) $(OMEGA_LIBS)  $(RAZVAN_LIBS)

loopinv/AST.hs

@@ -0,0 +1,52 @@
+-- | Simple AST for C subset (loops, assignments, basic expressions)
+module AST where
+
+-- | A program is a list of functions
+data Program = Program [Func]
+  deriving (Show, Eq)
+
+-- | Function definition
+data Func = Func {
+    funcRetType :: Type,
+    funcName    :: String,
+    funcParams  :: [(Type, String)],
+    funcBody    :: [Stmt]
+  }
+  deriving (Show, Eq)
+
+-- | Types we support
+data Type = TInt | TVoid
+  deriving (Show, Eq)
+
+-- | Statements
+data Stmt
+  = VarDecl Type String (Maybe Expr)    -- int x = 0;
+  | Assign String Expr                   -- x = expr;
+  | While Expr [Stmt]                    -- while (cond) { body }
+  | If Expr [Stmt] (Maybe [Stmt])        -- if (cond) { } else { }
+  | Return (Maybe Expr)                  -- return expr;
+  | ExprStmt Expr                        -- expr;
+  deriving (Show, Eq)
+
+-- | Expressions
+data Expr
+  = Var String                           -- variable
+  | Lit Int                              -- integer literal
+  | BinOp BinOp Expr Expr               -- e1 op e2
+  | UnaryOp UnaryOp Expr                -- op e
+  | Call String [Expr]                   -- func(args)
+  deriving (Show, Eq)
+
+-- | Binary operators
+data BinOp
+  = Add | Sub | Mul | Div | Mod         -- arithmetic
+  | Lt | Le | Gt | Ge | Eq | Ne         -- comparison
+  | And | Or                             -- logical
+  deriving (Show, Eq)
+
+-- | Unary operators
+data UnaryOp = Neg | Not
+  deriving (Show, Eq)
+
+
+

loopinv/ImpEmit.hs

@@ -0,0 +1,115 @@
+-- | Emit AST as Imp language syntax
+module ImpEmit (emitImp) where
+
+import AST
+import Data.List (intercalate)
+
+-- | Convert program to Imp source code
+emitImp :: Program -> String
+emitImp (Program funcs) = 
+    "#include \"Primitives.imp\"\n\n" ++
+    intercalate "\n\n" (map emitFunc funcs)
+
+-- | Emit a function
+emitFunc :: Func -> String
+emitFunc (Func retType name params body) =
+    emitType retType ++ " " ++ name ++ "(" ++ emitParams params ++ ") {\n" ++
+    emitStmts 1 body ++
+    "}"
+
+-- | Emit type
+emitType :: Type -> String
+emitType TInt = "int"
+emitType TVoid = "void"
+
+-- | Emit parameters
+emitParams :: [(Type, String)] -> String
+emitParams = intercalate ", " . map (\(t, n) -> emitType t ++ " " ++ n)
+
+-- | Emit statements with indentation
+emitStmts :: Int -> [Stmt] -> String
+emitStmts indent stmts = 
+    concatMap (emitStmt indent) (init' stmts) ++
+    emitStmtLast indent (last' stmts)
+  where
+    -- All statements except last get semicolon
+    init' [] = []
+    init' xs = init xs
+    -- Last statement has no trailing semicolon (Imp uses ; as separator)
+    last' [] = Nothing
+    last' xs = Just (last xs)
+
+-- | Emit a statement (not the last one - includes semicolon separator)
+emitStmt :: Int -> Stmt -> String
+emitStmt indent stmt = emitStmtCore indent stmt ++ ";\n"
+
+-- | Emit the last statement (no semicolon)
+emitStmtLast :: Int -> Maybe Stmt -> String
+emitStmtLast _ Nothing = ""
+emitStmtLast indent (Just stmt) = emitStmtCore indent stmt ++ "\n"
+
+-- | Emit statement core (without semicolon)
+emitStmtCore :: Int -> Stmt -> String
+emitStmtCore indent stmt = 
+    let ind = replicate (indent * 2) ' '
+    in case stmt of
+        VarDecl typ name Nothing ->
+            ind ++ emitType typ ++ " " ++ name ++ " := 0"  -- Imp needs initialization
+        VarDecl typ name (Just expr) ->
+            ind ++ emitType typ ++ " " ++ name ++ " := " ++ emitExpr expr
+        Assign name expr ->
+            ind ++ name ++ " := " ++ emitExpr expr
+        While cond body ->
+            ind ++ "while (" ++ emitExpr cond ++ ") do {\n" ++
+            emitStmts (indent + 1) body ++
+            ind ++ "}"
+        If cond thenBody Nothing ->
+            ind ++ "if " ++ emitExpr cond ++ " then {\n" ++
+            emitStmts (indent + 1) thenBody ++
+            ind ++ "} else { Void }"
+        If cond thenBody (Just elseBody) ->
+            ind ++ "if " ++ emitExpr cond ++ " then {\n" ++
+            emitStmts (indent + 1) thenBody ++
+            ind ++ "} else {\n" ++
+            emitStmts (indent + 1) elseBody ++
+            ind ++ "}"
+        Return Nothing ->
+            ind ++ "Void"
+        Return (Just expr) ->
+            ind ++ emitExpr expr
+        ExprStmt expr ->
+            ind ++ emitExpr expr
+
+-- | Emit expression
+emitExpr :: Expr -> String
+emitExpr (Var name) = name
+emitExpr (Lit n) = show n
+emitExpr (BinOp op e1 e2) = 
+    "(" ++ emitExpr e1 ++ " " ++ emitBinOp op ++ " " ++ emitExpr e2 ++ ")"
+emitExpr (UnaryOp op e) = emitUnaryOp op ++ emitExpr e
+emitExpr (Call name args) = 
+    name ++ "(" ++ intercalate ", " (map emitExpr args) ++ ")"
+
+-- | Emit binary operator
+emitBinOp :: BinOp -> String
+emitBinOp Add = "+"
+emitBinOp Sub = "-"
+emitBinOp Mul = "*"
+emitBinOp Div = "/"
+emitBinOp Mod = "%"
+emitBinOp Lt  = "<"
+emitBinOp Le  = "<="
+emitBinOp Gt  = ">"
+emitBinOp Ge  = ">="
+emitBinOp Eq  = "="      -- Imp uses = for equality in expressions
+emitBinOp Ne  = "<>"     -- Imp uses <> for not equal
+emitBinOp And = "&&"
+emitBinOp Or  = "||"
+
+-- | Emit unary operator
+emitUnaryOp :: UnaryOp -> String
+emitUnaryOp Neg = "-"
+emitUnaryOp Not = "!"
+
+
+

loopinv/Lexer.hs

@@ -0,0 +1,85 @@
+-- | Simple lexer for C subset
+module Lexer (Token(..), tokenize) where
+
+import Data.Char (isAlpha, isAlphaNum, isDigit, isSpace)
+
+-- | Tokens
+data Token
+  = TkInt | TkVoid                      -- types
+  | TkWhile | TkIf | TkElse | TkReturn  -- keywords
+  | TkIdent String                      -- identifier
+  | TkNum Int                           -- number
+  | TkPlus | TkMinus | TkStar | TkSlash | TkPercent  -- arithmetic
+  | TkLt | TkLe | TkGt | TkGe | TkEqEq | TkNe       -- comparison
+  | TkAnd | TkOr | TkNot                -- logical
+  | TkAssign                            -- =
+  | TkLParen | TkRParen                 -- ( )
+  | TkLBrace | TkRBrace                 -- { }
+  | TkSemi | TkComma                    -- ; ,
+  | TkEOF
+  deriving (Show, Eq)
+
+-- | Tokenize a string
+tokenize :: String -> [Token]
+tokenize [] = [TkEOF]
+tokenize s@(c:cs)
+  | isSpace c = tokenize cs
+  -- Skip single-line comments
+  | take 2 s == "//" = tokenize (dropWhile (/= '\n') s)
+  -- Skip multi-line comments
+  | take 2 s == "/*" = tokenize (skipBlockComment (drop 2 s))
+  -- Two-character operators
+  | take 2 s == "<=" = TkLe : tokenize (drop 2 s)
+  | take 2 s == ">=" = TkGe : tokenize (drop 2 s)
+  | take 2 s == "==" = TkEqEq : tokenize (drop 2 s)
+  | take 2 s == "!=" = TkNe : tokenize (drop 2 s)
+  | take 2 s == "&&" = TkAnd : tokenize (drop 2 s)
+  | take 2 s == "||" = TkOr : tokenize (drop 2 s)
+  -- Single-character operators
+  | c == '+' = TkPlus : tokenize cs
+  | c == '-' = TkMinus : tokenize cs
+  | c == '*' = TkStar : tokenize cs
+  | c == '/' = TkSlash : tokenize cs
+  | c == '%' = TkPercent : tokenize cs
+  | c == '<' = TkLt : tokenize cs
+  | c == '>' = TkGt : tokenize cs
+  | c == '=' = TkAssign : tokenize cs
+  | c == '!' = TkNot : tokenize cs
+  | c == '(' = TkLParen : tokenize cs
+  | c == ')' = TkRParen : tokenize cs
+  | c == '{' = TkLBrace : tokenize cs
+  | c == '}' = TkRBrace : tokenize cs
+  | c == ';' = TkSemi : tokenize cs
+  | c == ',' = TkComma : tokenize cs
+  -- Numbers
+  | isDigit c = let (num, rest) = span isDigit s
+                in TkNum (read num) : tokenize rest
+  -- Identifiers and keywords
+  | isAlpha c || c == '_' = 
+      let (ident, rest) = span isIdentChar s
+      in keywordOrIdent ident : tokenize rest
+  | otherwise = error $ "Unexpected character: " ++ [c]
+
+-- | Check if character can be part of identifier
+isIdentChar :: Char -> Bool
+isIdentChar c = isAlphaNum c || c == '_'
+
+-- | Convert identifier to keyword or keep as identifier
+keywordOrIdent :: String -> Token
+keywordOrIdent "int"    = TkInt
+keywordOrIdent "void"   = TkVoid
+keywordOrIdent "while"  = TkWhile
+keywordOrIdent "if"     = TkIf
+keywordOrIdent "else"   = TkElse
+keywordOrIdent "return" = TkReturn
+keywordOrIdent s        = TkIdent s
+
+-- | Skip block comment (find closing */)
+skipBlockComment :: String -> String
+skipBlockComment [] = []
+skipBlockComment s
+  | take 2 s == "*/" = drop 2 s
+  | otherwise = skipBlockComment (tail s)
+
+
+

loopinv/Main.hs

@@ -0,0 +1,86 @@
+-- | LoopInv: Build constraint abstractions and compute loop invariants via LFP
+-- 
+-- This tool:
+-- 1. Converts C code to Imp syntax (constraint abstraction)
+-- 2. Runs the imp tool which uses fixCalc to compute LFP
+-- 3. Shows the result
+--
+module Main where
+
+import System.Environment (getArgs)
+import System.Process (readProcessWithExitCode)
+import System.Exit (ExitCode(..))
+import System.FilePath (takeBaseName, takeDirectory, (</>))
+
+import Lexer (tokenize)
+import Parser (parse)
+import ImpEmit (emitImp)
+
+main :: IO ()
+main = do
+    args <- getArgs
+    case args of
+        [inputFile] -> processFile inputFile
+        _ -> showHelp
+
+showHelp :: IO ()
+showHelp = do
+    putStrLn "LoopInv - Loop Invariant Generator using fixCalc"
+    putStrLn ""
+    putStrLn "Usage: loopinv <input.c>"
+    putStrLn ""
+    putStrLn "This tool:"
+    putStrLn "  1. Converts C code to Imp (constraint abstraction)"
+    putStrLn "  2. Runs imp tool to compute loop invariants via LFP (fixCalc)"
+    putStrLn "  3. Displays the computed result"
+
+processFile :: FilePath -> IO ()
+processFile inputFile = do
+    putStrLn "================================================================"
+    putStrLn "  LoopInv - Constraint Abstraction & LFP Computation"
+    putStrLn "================================================================"
+    putStrLn ""
+
+    -- Step 1: Read and parse C code
+    putStrLn $ "Input: " ++ inputFile
+    putStrLn ""
+    cCode <- readFile inputFile
+
+    putStrLn "=== Original C Code ==="
+    putStrLn cCode
+
+    -- Step 2: Convert to Imp (constraint abstraction)
+    putStrLn "=== Converting to Imp (Constraint Abstraction) ==="
+    let tokens = tokenize cCode
+    let ast = parse tokens
+    let impCode = emitImp ast
+
+    let impFile = takeDirectory inputFile </> takeBaseName inputFile ++ ".imp"
+    writeFile impFile impCode
+    putStrLn $ "Generated: " ++ impFile
+    putStrLn ""
+    putStrLn impCode
+
+    -- Step 3: Run imp tool (which calls fixCalc for LFP)
+    putStrLn "=== Running imp tool (LFP computation via fixCalc) ==="
+    putStrLn ""
+
+    let impBin = "./imp"
+    (exitCode, stdout, stderr) <- readProcessWithExitCode impBin [impFile, "+infer"] ""
+
+    case exitCode of
+        ExitSuccess -> do
+            putStrLn stdout
+
+            -- Show the LFP result
+            putStrLn "=== LFP Result (a.impt) ==="
+            putStrLn ""
+            imptContent <- readFile "a.impt"
+            putStrLn imptContent
+
+        ExitFailure code -> do
+            putStrLn $ "Error: imp tool failed with code " ++ show code
+            putStrLn "stderr:"
+            putStrLn stderr
+            putStrLn "stdout:"
+            putStrLn stdout