implement array length operator

src/LogicIR/Backend/Pretty.hs

@@ -44,10 +44,10 @@ prettyNUnop NNeg = "-"
 prettyNUnop NNot = "~"
 
 prettyVar :: Var -> String
-prettyVar (Var t n) = '(' : prettyType t ++ ")" ++ n
+prettyVar (Var t n) = prettyType t ++ ":" ++ n
 
 prettyLExprAlgebra :: LExprAlgebra String
-prettyLExprAlgebra = (flConst, prettyVar, flNot, flBinop, flComp, flQuant, flArray, fnConst, prettyVar, fnUnop, fnBinop, fnArray, fnIf) where
+prettyLExprAlgebra = (flConst, prettyVar, flNot, flBinop, flComp, flQuant, flArray, fnConst, prettyVar, fnUnop, fnBinop, fnArray, fnIf, fnLen) where
     flConst b = if b then "true" else "false"
     flNot a = '!' : a
     flBinop a o b = a ++ " " ++ prettyLBinop o ++ " " ++ b
@@ -58,4 +58,5 @@ prettyLExprAlgebra = (flConst, prettyVar, flNot, flBinop, flComp, flQuant, flArr
     fnUnop o a = prettyNUnop o ++ a
     fnBinop a o b = a ++ " " ++ prettyNBinop o ++ " " ++ b
     fnArray = flArray
-    fnIf c a b = "(" ++ c ++ ") ? (" ++ a ++ ") : (" ++ b ++ ")"
\ No newline at end of file
+    fnIf c a b = "(" ++ c ++ ") ? (" ++ a ++ ") : (" ++ b ++ ")"
+    fnLen v = "len(" ++ prettyVar v ++ ")"
\ No newline at end of file

src/LogicIR/Backend/Z3.hs

@@ -9,7 +9,7 @@ lExprToZ3Ast :: LExpr -> Z3 AST
 lExprToZ3Ast = foldLExpr lExprToZ3AstAlgebra
 
 lExprToZ3AstAlgebra :: LExprAlgebra (Z3 AST)
-lExprToZ3AstAlgebra = (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, fnConst, fnVar, fnUnop, fnBinop, fnArray, fnIf) where
+lExprToZ3AstAlgebra = (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, fnConst, fnVar, fnUnop, fnBinop, fnArray, fnIf, fnLen) where
     flConst = undefined
     flVar = undefined
     flNot = undefined
@@ -22,4 +22,5 @@ lExprToZ3AstAlgebra = (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray,
     fnUnop = undefined
     fnBinop = undefined
     fnArray = undefined
-    fnIf = undefined
\ No newline at end of file
+    fnIf = undefined
+    fnLen = undefined
\ No newline at end of file

src/LogicIR/Expr.hs

@@ -57,7 +57,7 @@ data COp = CEqual -- a == b
 
 type NExpr = LExpr
 
--- Logical expressions
+-- Logical expressions (TODO: clean up duplicates)
 data LExpr = LConst Bool -- True/False
            | LVar Var -- Variable
            | LNot LExpr -- Logical negation/not
@@ -72,4 +72,5 @@ data LExpr = LConst Bool -- True/False
            | NBinop NExpr NBinop NExpr -- Binary operators
            | NArray Var [NExpr] -- Integer array access
            | NIf LExpr NExpr NExpr -- if c then a else b
+           | NLen Var -- len(array)
            deriving (Show, Eq, Read)
\ No newline at end of file

src/LogicIR/Fold.hs

@@ -15,12 +15,13 @@ type LExprAlgebra r = (Bool -> r, -- LConst
                        NUnop -> r -> r, -- NUnop
                        r -> NBinop -> r -> r, -- NBinop
                        Var -> [NExpr] -> r, -- NArray
-                       r -> r -> r -> r -- NIf
+                       r -> r -> r -> r, -- NIf
+                       Var -> r -- NLen
                       )
 
 -- Fold for logical expressions
 foldLExpr :: LExprAlgebra r -> LExpr -> r
-foldLExpr (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, fnConst, fnVar, fnUnop, fnBinop, fnArray, fnIf) = fold where
+foldLExpr (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, fnConst, fnVar, fnUnop, fnBinop, fnArray, fnIf, fnLen) = fold where
     fold e = case e of
                   LConst c -> flConst c
                   LVar n -> flVar n
@@ -34,4 +35,5 @@ foldLExpr (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, fnConst, fn
                   NUnop o e -> fnUnop o (fold e)
                   NBinop a o b -> fnBinop (fold a) o (fold b)
                   NArray n e -> fnArray n e
-                  NIf c a b -> fnIf (fold c) (fold a) (fold b)
\ No newline at end of file
+                  NIf c a b -> fnIf (fold c) (fold a) (fold b)
+                  NLen v -> fnLen v
\ No newline at end of file

src/LogicIR/Frontend/Java.hs

@@ -39,12 +39,17 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation,
                                                                  PrimType IntT -> NArray (Var (TArray (TPrim PInt)) (prettyPrint name)) [NVar (Var (TPrim PInt) (prettyPrint index))]
                                                                  _ -> error $ show (arrayIndex, indexType)
                                                          _ -> error $ show (arrayIndex, arrayType)
-    fExpName name env decls = let symbol = prettyPrint name in let t = lookupType decls env name in
-                                    -- If we're not dealing with library methods, we should be able to get the type from the type environment
-                                    case t of
-                                        PrimType BooleanT    -> LVar (Var (TPrim PBool) symbol)
-                                        PrimType IntT        -> NVar (Var (TPrim PInt) symbol)
-                                        t                    -> error ("Verifier: Type of " ++ prettyPrint name ++ " unknown or not implemented: " ++ show t)
+    fExpName name env decls = case name of -- TODO: better type checking + multiple dimension arrays + better abstractions
+                                   Name [Ident a, Ident "length"] -> let arrayType = lookupType decls env (Name [Ident a]) in
+                                                                     case arrayType of
+                                                                          (RefType (ArrayType (PrimType IntT))) -> NLen (Var (TArray (TPrim PInt)) a)
+                                                                          _ -> error $ show (name, arrayType)
+                                   _ -> let symbol = prettyPrint name in let t = lookupType decls env name in
+                                        -- If we're not dealing with library methods, we should be able to get the type from the type environment
+                                        case t of
+                                             PrimType BooleanT    -> LVar (Var (TPrim PBool) symbol)
+                                             PrimType IntT        -> NVar (Var (TPrim PInt) symbol)
+                                             t                    -> error ("Verifier: Type of " ++ prettyPrint name ++ " unknown or not implemented: " ++ show t)
     fPostIncrement = error "fPostIncrement has side effects..."
     fPostDecrement = error "fPostDecrement has side effects..."
     fPreIncrement = error "fPreIncrement has side effects..."

src/SimpleFormulaChecker.hs

@@ -149,4 +149,4 @@ edslSrc = "javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
 testEq = compareSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec1")
 testNeq = compareSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec2")
 
-blub = compareSpec (edslSrc, "simple1") (edslSrc, "simple1")
\ No newline at end of file
+blub = compareSpec (edslSrc, "simple2") (edslSrc, "simple2")
\ No newline at end of file