Loop Pre/Post Condition Generation with Exactness Verification

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)

a.c

@@ -0,0 +1,20 @@
+#include "Primitives.h"
+
+void simple(int n) {
+ int x = 0;
+ return whilef_0(x,n);
+ }
+
+void whilef_0(int x,int n) {
+ bool v_14 = lt(x,n);
+ if (v_14) {
+    {
+   int v_12 = 1;
+   x=plus(x,v_12);
+   };
+   return whilef_0(x,n);
+   } else {
+   return ;
+   };
+ }
+

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,168 @@
+-- | 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 (with variable hoisting for imp tool compatibility)
+emitFunc :: Func -> String
+emitFunc (Func retType name params body) =
+    let (hoisted, transformedBody) = hoistVarDecls body
+    in emitType retType ++ " " ++ name ++ "(" ++ emitParams params ++ ") {\n" ++
+       -- Emit hoisted declarations first (without initial value)
+       concatMap (emitHoistedDecl 1) hoisted ++
+       emitStmts 1 transformedBody ++
+       "}"
+
+-- | Emit a hoisted declaration (with default initialization - Imp requires it)
+emitHoistedDecl :: Int -> (Type, String) -> String
+emitHoistedDecl indent (typ, name) =
+    replicate (indent * 2) ' ' ++ emitType typ ++ " " ++ name ++ " := 0;\n"
+
+-- | Hoist variable declarations from inside loops to function level
+-- Returns (hoisted declarations, transformed statements)
+hoistVarDecls :: [Stmt] -> ([(Type, String)], [Stmt])
+hoistVarDecls stmts = 
+    let (hoisted, transformed) = unzip $ map hoistFromStmt stmts
+    in (concat hoisted, transformed)
+
+-- | Hoist from a single statement
+hoistFromStmt :: Stmt -> ([(Type, String)], Stmt)
+hoistFromStmt (While cond body) =
+    let (hoisted, transformedBody) = hoistFromBody body
+    in (hoisted, While cond transformedBody)
+hoistFromStmt (If cond thenBody elseBody) =
+    let (hoistedThen, transformedThen) = hoistFromBody thenBody
+        (hoistedElse, transformedElse) = case elseBody of
+            Just eb -> let (h, t) = hoistFromBody eb in (h, Just t)
+            Nothing -> ([], Nothing)
+    in (hoistedThen ++ hoistedElse, If cond transformedThen transformedElse)
+hoistFromStmt stmt = ([], stmt)
+
+-- | Hoist from body (inside a loop or if)
+-- This is where we actually hoist - VarDecls become assignments
+hoistFromBody :: [Stmt] -> ([(Type, String)], [Stmt])
+hoistFromBody stmts = 
+    let (hoisted, transformed) = unzip $ map hoistAndTransform stmts
+    in (concat hoisted, concat transformed)
+
+-- | Hoist a statement and transform VarDecl to Assign
+hoistAndTransform :: Stmt -> ([(Type, String)], [Stmt])
+hoistAndTransform (VarDecl typ name maybeExpr) =
+    -- Hoist the declaration, keep assignment in place
+    case maybeExpr of
+        Just expr -> ([(typ, name)], [Assign name expr])
+        Nothing -> ([(typ, name)], [Assign name (Lit 0)])
+hoistAndTransform (While cond body) =
+    let (hoisted, transformedBody) = hoistFromBody body
+    in (hoisted, [While cond transformedBody])
+hoistAndTransform (If cond thenBody elseBody) =
+    let (hoistedThen, transformedThen) = hoistFromBody thenBody
+        (hoistedElse, transformedElse) = case elseBody of
+            Just eb -> let (h, t) = hoistFromBody eb in (h, Just t)
+            Nothing -> ([], Nothing)
+    in (hoistedThen ++ hoistedElse, [If cond transformedThen transformedElse])
+hoistAndTransform stmt = ([], [stmt])
+
+-- | 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)
+
+
+