initial implementation of javaExpToLExprAlgebra

src/LogicIR/Backend/Z3.hs

@@ -5,26 +5,20 @@ import Z3.Monad
 import LogicIR.Expr
 import LogicIR.Fold
 
-nExprToZ3Ast :: NExpr -> Z3 AST
-nExprToZ3Ast = foldNExpr nExprToZ3AstAlgebra
-
-nExprToZ3AstAlgebra :: NExprAlgebra (Z3 AST)
-nExprToZ3AstAlgebra = (fConst, fVar, fUnop, fBinop, fArray) where
-    fConst = undefined
-    fVar = undefined
-    fUnop = undefined
-    fBinop = undefined
-    fArray = undefined
-
 lExprToZ3Ast :: LExpr -> Z3 AST
 lExprToZ3Ast = foldLExpr lExprToZ3AstAlgebra
 
 lExprToZ3AstAlgebra :: LExprAlgebra (Z3 AST)
-lExprToZ3AstAlgebra = (fConst, fVar, fNot, fBinop, fComp, fQuant, fArray) where
-    fConst = undefined
-    fVar = undefined
-    fNot = undefined
-    fBinop = undefined
-    fComp = undefined
-    fQuant = undefined
-    fArray = undefined
\ No newline at end of file
+lExprToZ3AstAlgebra = (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, fnConst, fnVar, fnUnop, fnBinop, fnArray) where
+    flConst = undefined
+    flVar = undefined
+    flNot = undefined
+    flBinop = undefined
+    flComp = undefined
+    flQuant = undefined
+    flArray = undefined
+    fnConst = undefined
+    fnVar = undefined
+    fnUnop = undefined
+    fnBinop = undefined
+    fnArray = undefined
\ No newline at end of file

src/LogicIR/Expr.hs

 module LogicIR.Expr where
 
+-- TODO: pretty printer
 -- Based on my (Duncan's) previous work: https://github.com/mrexodia/wp/blob/master/Wp.hs
 
 data Primitive = PBool
@@ -32,14 +33,6 @@ data NBinop = NAdd
             | NXor
             deriving (Show, Eq, Read)
 
--- Numeral expressions
-data NExpr = NConst Int -- Integer constant
-           | NVar Var -- Variable
-           | NUnop NUnop NExpr -- Unary operator
-           | NBinop NExpr NBinop NExpr -- Binary operators
-           | NArray Var NExpr -- Integer array access
-           deriving (Show, Eq, Read)
-
 -- Reference: https://en.wikipedia.org/wiki/First-order_logic#Logical_symbols
 
 -- Logical operators
@@ -54,13 +47,16 @@ data QOp = QAll | QAny
          deriving (Show, Eq, Read)
 
 -- Comparison operators
-data COp = CEqual
-         | CLess
-         | CGreater
-         | CLeq
-         | CGeq
+data COp = CEqual -- a == b
+         | CNEqual -- a != b
+         | CLess -- a < b
+         | CGreater -- a > b
+         | CLeq -- a <= b
+         | CGeq -- a >= b
          deriving (Show, Eq, Read)
 
+type NExpr = LExpr
+
 -- Logical expressions
 data LExpr = LConst Bool -- True/False
            | LVar Var -- Variable
@@ -68,5 +64,11 @@ data LExpr = LConst Bool -- True/False
            | LBinop LExpr LBinop LExpr -- Logical operator
            | LComp NExpr COp NExpr -- Integer comparison
            | LQuant QOp [Var] LExpr -- Logical quantifier
-           | LArray Var NExpr -- Logical array access (TODO: remove?)
+           | LArray Var [NExpr] -- Logical array access (TODO: remove?)
+
+           | NConst Int -- Integer constant
+           | NVar Var -- Variable
+           | NUnop NUnop NExpr -- Unary operator
+           | NBinop NExpr NBinop NExpr -- Binary operators
+           | NArray Var [NExpr] -- Integer array access
            deriving (Show, Eq, Read)
\ No newline at end of file

src/LogicIR/Fold.hs

@@ -2,42 +2,34 @@ module LogicIR.Fold where
 
 import LogicIR.Expr
 
--- Fold algrbra for numeral expressions
-type NExprAlgebra r = (Int -> r, -- NConst
-                       Var -> r, -- NVar
-                       NUnop -> r -> r, -- NUnop
-                       r -> NBinop -> r -> r, -- NBinop
-                       Var -> r -> r -- NArray
-                      )
-
--- Fold for numeral expressions
-foldNExpr :: NExprAlgebra r -> NExpr -> r
-foldNExpr (fConst, fVar, fUnop, fBinop, fArray) = fold where
-    fold e = case e of
-                  NConst n -> fConst n
-                  NVar n -> fVar n
-                  NUnop o e -> fUnop o (fold e)
-                  NBinop a o b -> fBinop (fold a) o (fold b)
-                  NArray n e -> fArray n (fold e)
-
 -- Fold algebra for logical expressions
 type LExprAlgebra r = (Bool -> r, -- LConst
                        Var -> r, -- LVar
                        r -> r, -- LNot
                        r -> LBinop -> r -> r, -- LBinop
-                       NExpr -> COp -> NExpr -> r, -- LComp
+                       r -> COp -> r -> r, -- LComp
                        QOp -> [Var] -> r -> r, -- LQuant
-                       Var -> NExpr -> r -- LArray
+                       Var -> [NExpr] -> r, -- LArray
+                       Int -> r, -- NConst
+                       Var -> r, -- NVar
+                       NUnop -> r -> r, -- NUnop
+                       r -> NBinop -> r -> r, -- NBinop
+                       Var -> [NExpr] -> r -- NArray
                       )
 
 -- Fold for logical expressions
 foldLExpr :: LExprAlgebra r -> LExpr -> r
-foldLExpr (fConst, fVar, fNot, fBinop, fComp, fQuant, fArray) = fold where
+foldLExpr (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, fnConst, fnVar, fnUnop, fnBinop, fnArray) = fold where
     fold e = case e of
-                  LConst c -> fConst c
-                  LVar n -> fVar n
-                  LNot e -> fNot (fold e)
-                  LBinop a o b -> fBinop (fold a) o (fold b)
-                  LComp a o b -> fComp a o b
-                  LQuant o vs e -> fQuant o vs (fold e)
-                  LArray n e -> fArray n e
\ No newline at end of file
+                  LConst c -> flConst c
+                  LVar n -> flVar n
+                  LNot e -> flNot (fold e)
+                  LBinop a o b -> flBinop (fold a) o (fold b)
+                  LComp a o b -> flComp (fold a) o (fold b)
+                  LQuant o vs e -> flQuant o vs (fold e)
+                  LArray n e -> flArray n e
+                  NConst n -> fnConst n
+                  NVar n -> fnVar n
+                  NUnop o e -> fnUnop o (fold e)
+                  NBinop a o b -> fnBinop (fold a) o (fold b)
+                  NArray n e -> fnArray n e
\ No newline at end of file

src/LogicIR/Frontend/Java.hs

 module LogicIR.Frontend.Java (javaExpToLExpr) where
 
 import Javawlp.Engine.Folds
+import Javawlp.Engine.HelperFunctions
 
 import Language.Java.Syntax
+import Language.Java.Syntax.Types
 import Language.Java.Parser
 import Language.Java.Pretty
 
 import LogicIR.Expr
+import Data.Typeable
 
-javaExpToLExpr :: Exp -> LExpr
+javaExpToLExpr :: Exp -> TypeEnv -> [TypeDecl] -> LExpr
 javaExpToLExpr = foldExp javaExpToLExprAlgebra
 
-javaExpToLExprAlgebra :: ExpAlgebra LExpr
+javaExpToLExprAlgebra :: ExpAlgebra (TypeEnv -> [TypeDecl] -> LExpr)
 javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualInstanceCreation, fArrayCreate, fArrayCreateInit, fFieldAccess, fMethodInv, fArrayAccess, fExpName, fPostIncrement, fPostDecrement, fPreIncrement, fPreDecrement, fPrePlus, fPreMinus, fPreBitCompl, fPreNot, fCast, fBinOp, fInstanceOf, fCond, fAssign, fLambda, fMethodRef) where
-    fLit = undefined
+    fLit lit _ _ = case lit of
+                    Boolean b -> LConst b
+                    Int n -> NConst (fromIntegral n) -- TODO: use Integer in LExpr?
+                    _ -> error $ show $ lit
     fClassLit = undefined
     fThis = undefined
     fThisClass = undefined
@@ -23,18 +29,54 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation,
     fArrayCreateInit = undefined
     fFieldAccess = undefined
     fMethodInv = undefined
-    fArrayAccess = undefined
-    fExpName = undefined
+    fArrayAccess arrayIndex env decls = case arrayIndex of -- TODO: better type checking + multiple dimension arrays
+                                             ArrayIndex (ExpName name) [ExpName index] ->
+                                                let (arrayType, indexType) = (lookupType decls env name, lookupType decls env index) in
+                                                    case arrayType of
+                                                         (RefType (ArrayType (PrimType IntT))) ->
+                                                            case indexType of
+                                                                 PrimType IntT -> NArray (Var (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)
     fPostIncrement = undefined
     fPostDecrement = undefined
     fPreIncrement = undefined
     fPreDecrement = undefined
-    fPrePlus = undefined
-    fPreMinus = undefined
+    fPrePlus e env decls = e env decls
+    fPreMinus e env decls = NUnop NNeg (e env decls)
     fPreBitCompl = undefined
     fPreNot = undefined
     fCast = undefined
-    fBinOp = undefined
+    fBinOp e1 op e2 env decls = let (a, b) = (e1 env decls, e2 env decls) in -- TODO: type checking
+                                case op of
+                                     -- Integer
+                                     Mult -> NBinop a NMul b
+                                     Div -> NBinop a NDiv b
+                                     Rem -> NBinop a NRem b
+                                     Add -> NBinop a NAdd b
+                                     Sub  -> NBinop a NSub b
+                                     LShift -> NBinop a NShl b
+                                     RShift -> NBinop a NShr b
+                                     RRShift -> undefined
+                                     And -> NBinop a NAnd b
+                                     Or -> NBinop a NOr b
+                                     Xor -> NBinop a NXor b
+                                     -- Logical
+                                     CAnd -> LBinop a LAnd b
+                                     COr -> LBinop a LOr b
+                                     -- Comparisons
+                                     LThan -> LComp a CLess b
+                                     GThan -> LComp a CGreater b
+                                     LThanE -> LComp a CLeq b
+                                     GThanE -> LComp a CGeq b
+                                     Equal -> LComp a CEqual b
+                                     NotEq -> LComp a CNEqual b
     fInstanceOf = undefined
     fCond = undefined
     fAssign = undefined

src/SimpleFormulaChecker.hs

@@ -111,6 +111,7 @@ determineFormulaEq m1@(decls1, mbody1, env1) m2@(decls2, mbody2, env2) name = do
     -- get preconditions
     let (e1, e2) = (extractCond m1 name, extractCond m2 name)
     putStrLn $ "e1:\n" ++ prettyPrint e1 ++ "\n\ne2:\n" ++ prettyPrint e2 ++ "\n"
+    putStrLn $ show $ javaExpToLExpr e1 env1 decls1
     {--- get postconditions
     let (post1, post2) = (extractCond m1 "post", extractCond m2 "post")
     putStrLn $ "post1:\n" ++ prettyPrint post1 ++ "\npost2:\n" ++ prettyPrint post2 ++ "\n"-}
@@ -144,4 +145,6 @@ compareSpec method1 method2 = do
 
 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")
\ No newline at end of file
+testNeq = compareSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec2")
+
+blub = compareSpec (edslSrc, "simple1") (edslSrc, "simple1")
\ No newline at end of file

src/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java

@@ -79,6 +79,22 @@ public class Main {
         a[j] = temp;
     }
 
+    public static void simple1(int[] a, int i, int j) {
+        pre(i >= 0 && j >= 0);
+        // introducing vars to remember old values
+        int oldai = a[i], oldaj = a[j];
+        swap(a, i, j);
+        post(a[j] == oldai && a[i] == oldaj);
+    }
+
+    public static void simple2(int[] a, int i, int j) {
+        pre(a.length > 0 && i >= 0 && j >= 0);
+        // introducing vars to remember old values
+        int oldai = a[i], oldaj = a[j];
+        swap(a, i, j);
+        post(a[j] == oldai && a[i] == oldaj);
+    }
+
     public static void swap_spec1(int[] a, int i, int j) {
         pre(a != null);
         pre(a.length > 0);