started with method calls. Method calls on objects are still very buggy

HelperFunctions.hs

@@ -5,7 +5,8 @@ import Language.Java.Syntax
 import Language.Java.Pretty
 import Data.Maybe
 
-type TypeEnv = [(Name, Type)]
+type TypeEnv    = [(Name, Type)]
+type CallCount  = [(Ident, Int)]
 
 -- | Retrieves the type from the environment
 lookupType :: [TypeDecl] -> TypeEnv -> Name -> Type
@@ -33,9 +34,62 @@ getFieldType decls (RefType (ClassRefType t)) (Name (f:fs)) = getFieldType decls
                                                                 _ -> getDecl t xs
         getDecl _ _ = error "nested class"
         
+-- Increments the call count for a given method
+incrCallCount :: CallCount -> Ident -> CallCount
+incrCallCount [] id             = [(id, 1)]
+incrCallCount ((id', c):xs) id  = if id == id' then (id', c + 1) : xs else (id', c) : incrCallCount xs id
+
+
+-- Looks up the call count for a given method
+getCallCount :: CallCount -> Ident -> Int
+getCallCount [] id             = 0
+getCallCount ((id', c):xs) id  = if id == id' then c else getCallCount xs id
+        
 getId :: VarDeclId -> Ident
 getId (VarId id) = id
 getId (VarDeclArray id) = getId id
+
+fromName :: Name -> [Ident]
+fromName (Name name) = name
+
+-- Gets the ident of the method from a name
+getMethodId :: Name -> Ident
+getMethodId = last . fromName
+
+-- Gets the statement(-block) defining a method
+getMethod :: [TypeDecl] -> Ident -> Stmt
+getMethod classTypeDecls methodId = fst (getMethod' classTypeDecls methodId)
+
+-- Gets the return type of a method
+getMethodType :: [TypeDecl] -> Ident -> Maybe Type
+getMethodType classTypeDecls methodId = snd (getMethod' classTypeDecls methodId)
+
+-- Finds a method definition. This function assumes all methods are named differently
+getMethod' :: [TypeDecl] -> Ident -> (Stmt, Maybe Type)
+getMethod' classTypeDecls methodId = case (concatMap searchClass classTypeDecls) of
+                                        r:_     -> r
+                                        []      -> error ("non-existing method: " ++ show methodId)
+  where
+    searchClass (ClassTypeDecl (ClassDecl _ _ _ _ _ (ClassBody decls))) = searchDecls decls
+    searchDecls (MemberDecl (MethodDecl _ _ t id _ _ (MethodBody (Just b))):_) | methodId == id = [(StmtBlock b, t)]
+    searchDecls (_:decls) = searchDecls decls
+    searchDecls [] = []
+
+-- Gets the statement(-block) defining the main method and initializes the heap
+getMainMethod :: [TypeDecl] -> Stmt
+getMainMethod classTypeDecls = getMethod classTypeDecls (Ident "main")
+
+-- Gets the class declarations
+getDecls :: CompilationUnit -> [TypeDecl]
+getDecls (CompilationUnit _ _ classTypeDecls) = classTypeDecls
+
+-- Gets the static member declarations and puts them in the type environment
+getStaticVars :: CompilationUnit -> TypeEnv
+getStaticVars compUnit = concatMap fromTypeDecls (getDecls compUnit) where
+    fromTypeDecls (ClassTypeDecl (ClassDecl _ _ _ _ _ (ClassBody decls))) = concatMap fromMemberDecl decls
+    fromMemberDecl (MemberDecl (FieldDecl mods t varDecls)) = if Static `elem` mods then map (fromVarDecl t) varDecls else []
+    fromMemberDecl _                                        = []
+    fromVarDecl t (VarDecl varId _) = (Name [getId varId], t)
         
 true :: Exp
 true = Lit (Boolean True)
@@ -70,6 +124,12 @@ arrayAccess a i = case a of
                     ArrayCreateInit t dim arrayInit -> getInitValue t
                     _                               -> ArrayAccess (ArrayIndex a i)
 
+-- Accesses fields of fields
+fieldAccess :: Exp -> Name -> FieldAccess
+fieldAccess e (Name [id])       = PrimaryFieldAccess e id
+fieldAccess e (Name (id:ids))   = fieldAccess (FieldAccess (PrimaryFieldAccess e id)) (Name ids)
+fieldAccess _ _ = error "FieldAccess without field name"
+                    
 -- | Gets the initial value for a given type
 getInitValue :: Type -> Exp
 getInitValue (PrimType t) = case t of

Main.hs

@@ -22,33 +22,16 @@ main = do
     case result of
         Left error -> print error
         Right compUnit -> do
+                            putStrLn "\r\n-----Code-----"
+                            print compUnit
                             putStrLn "\r\n-----WLP-----"
-                            let pred = wlpWithEnv (getDecls compUnit) (getStaticVars compUnit) (getStmt compUnit) postCond'
+                            let pred = wlpWithEnv (getDecls compUnit) (getStaticVars compUnit) (getMainMethod (getDecls compUnit)) postCond'
                             putStrLn . prettyPrint $ pred
                             putStrLn "\r\n-----Correctness-----"
                             if unsafeIsTrue pred then putStrLn "WLP evaluates to true" else (if unsafeIsFalse pred then putStrLn "WLP evaluates to false" else putStrLn "undecidable")
                             
                             
 
--- Gets the statement(-block) defining the main method and initializes the heap
-getStmt :: CompilationUnit -> Stmt
-getStmt (CompilationUnit _ _ classTypeDecls) =  (head (concatMap getInit classTypeDecls)) where
-    getInit (ClassTypeDecl (ClassDecl _ _ _ _ _ (ClassBody decls))) = getInit' decls
-    getInit' [] = []
-    getInit' (MemberDecl (MethodDecl _ _ _ (Ident "main") _ _ (MethodBody (Just b))):_) = [StmtBlock b]
-    getInit' (_:decls) = getInit' decls
-
--- Gets the class declarations
-getDecls :: CompilationUnit -> [TypeDecl]
-getDecls (CompilationUnit _ _ classTypeDecls) = classTypeDecls
-
--- Gets the static member declarations and puts them in the type environment
-getStaticVars :: CompilationUnit -> TypeEnv
-getStaticVars compUnit = concatMap fromTypeDecls (getDecls compUnit) where
-    fromTypeDecls (ClassTypeDecl (ClassDecl _ _ _ _ _ (ClassBody decls))) = concatMap fromMemberDecl decls
-    fromMemberDecl (MemberDecl (FieldDecl mods t varDecls)) = if Static `elem` mods then map (fromVarDecl t) varDecls else []
-    fromMemberDecl _                                        = []
-    fromVarDecl t (VarDecl varId _) = (Name [getId varId], t)
 
 -- The post-condition (for testing)
 postCond' :: Exp

Settings.hs

 module Settings where
 
 testFile, postCond :: String
-testFile = "loops"
+testFile = "methods"
 postCond = "x == 5"
 
 nrOfUnroll :: Int

Tests/methods.java

+public static class Main
+{
+    static int x;
+    public static void main(String[] args) 
+    {
+        C1 c1 = new C1();
+        c1.c += 2; //c1.method1();
+        x = c1.c;
+    }
+    
+    
+    
+    public static void method() 
+    {
+    }
+}
+
+public class C1
+{
+    int c;
+    
+    public C1()
+    {
+    }
+    
+    public void method1()
+    {
+     //  c++;
+    }
+}
\ No newline at end of file

WLP.hs

@@ -15,11 +15,14 @@ import Settings
     
 
 -- | A type for the inherited attribute
-data Inh = Inh {acc     :: Exp -> Exp,  -- The accumulated transformer of the current block up until the current statement
-                br      :: Exp -> Exp,  -- The accumulated transformer up until the last loop (this is used when handling break statements etc.)
-                catch   :: Maybe ([Catch], Bool), -- The catches when executing a block in a try statement, and a Bool indicating wether there is a finally-block
-                env     :: TypeEnv,     -- The type environment for typing expressions
-                decls   :: [TypeDecl] -- Class declarations
+data Inh = Inh {acc     :: Exp -> Exp,              -- The accumulated transformer of the current block up until the current statement
+                br      :: Exp -> Exp,              -- The accumulated transformer up until the last loop (this is used when handling break statements etc.)
+                catch   :: Maybe ([Catch], Bool),   -- The catches when executing a block in a try statement, and a Bool indicating wether there is a finally-block
+                env     :: TypeEnv,                 -- The type environment for typing expressions
+                decls   :: [TypeDecl],              -- Class declarations
+                calls   :: CallCount,               -- The number of recursive calls per method
+                ret     :: Maybe Ident,             -- The name of the return variable when handling a method call
+                object  :: Maybe Exp                -- The object the method is called from when handling a method call
                 }
             
            
@@ -49,7 +52,7 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
     fContinue _ inh                 = (id, env inh)     -- at a continue statement it's as if the body of the loop is fully executed
     fReturn me inh                  = case me of
                                         Nothing -> (id, env inh) -- Return ignores acc, as it terminates the method
-                                        Just e  -> fExpStmt (Assign (NameLhs (Name [Ident "return"])) EqualA e) inh -- We treat "return e" as an assignment to the variable return
+                                        Just e  -> fExpStmt (Assign (NameLhs (Name [fromJust (ret inh)])) EqualA e) (inh {acc = id}) -- We treat "return e" as an assignment to a variable specifically created to store the return value in
                                                             
     fSynchronized _                 = fStmtBlock
     fThrow e inh                    = case catch inh of
@@ -81,7 +84,7 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
                                                                 PrimType _ -> substVar (env inh) (decls inh) (NameLhs (Name [ident])) (getInitValue t) . acc inh
                                                                 -- We don't initialize ref types to null, because we want to keep pointer information
                                                                 RefType _ -> acc inh 
-    wlpDeclAssignment t inh (VarDecl (VarId ident) (Just (InitExp e)))  = substVar (env inh) (decls inh) (NameLhs (Name [ident])) e . acc inh
+    wlpDeclAssignment t inh (VarDecl (VarId ident) (Just (InitExp e)))  = getTrans (foldExp wlpExpAlgebra (Assign (NameLhs (Name [ident])) EqualA e)) inh 
               
     -- Unrolls a while-loop a finite amount of times
     unrollLoop :: Int -> Exp -> (Exp -> Exp) -> Exp -> Exp
@@ -148,12 +151,15 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
     fArrayCreate t dimLengths dim inh                   = (ArrayCreate t (map (flip getExp inh) dimLengths) dim, (acc inh, env inh))
     fArrayCreateInit t dim init inh                     = (ArrayCreateInit t dim init, (acc inh, env inh))
     fFieldAccess fieldAccess inh                        = (FieldAccess fieldAccess, (acc inh, env inh))
-    fMethodInv invocation inh                           = (Lit Null, (acc inh, env inh))
+    fMethodInv invocation inh                           = (ExpName (Name [getReturnVar inh invocation]), 
+                                                          (if getCallCount (calls inh) (invocationToId invocation) >= nrOfUnroll
+                                                          then const true
+                                                          else fst (wlp' (inh {env = maybe (env inh) (\t -> (Name [getReturnVar inh invocation], t) : env inh) (getType inh invocation), calls = incrCallCount (calls inh) (invocationToId invocation), ret = Just (getReturnVar inh invocation), object = Just (getObject invocation)}) (inlineMethod inh invocation)) . acc inh, env inh))
     fArrayAccess (ArrayIndex a i) inh                   = case catch inh of
                                                             Nothing      -> (arrayAccess a i, (acc inh, env inh))
                                                             Just (cs, f) -> (arrayAccess a i, (arrayAccessWlp a i inh, env inh))
     
-    fExpName name inh                                   = (ExpName name, (acc inh, env inh))
+    fExpName name inh                                   = (varInObject (object inh) name, (acc inh, env inh))
     -- x++ increments x but evaluates to the original value
     fPostIncrement e inh                                = case getExp e inh of
                                                             var@(ExpName name) -> (var, (substVar (env inh) (decls inh) (NameLhs name) (BinOp var Add (Lit (Int 1))) . acc inh, env inh))
@@ -176,8 +182,9 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
     fBinOp e1 op e2 inh                                 = (BinOp (getExp e1 inh) op (getExp e2 inh), (getTrans e1 (inh {acc = getTrans e2 inh}), env inh)) 
     fInstanceOf                                         = error "instanceOf"
     fCond g e1 e2 inh                                   = (Cond (getExp g inh) (getExp e1 inh) (getExp e2 inh), (getTrans g (inh {acc = id}) . (\q -> (getExp g inh &* getTrans e1 (inh {acc = id}) q) |* (neg (getExp g inh) &* getTrans e2 (inh {acc = id}) q)) . acc inh, env inh))
-    fAssign lhs op e inh                                = let rhs = desugarAssign lhs op (getExp e inh) 
-                                                          in  (rhs, (substVar (env inh) (decls inh) lhs rhs . getTrans e inh, env inh))
+    fAssign lhs op e inh                                = let lhs' = lhsInObject (object inh) lhs
+                                                              rhs' = desugarAssign lhs' op (getExp e inh) 
+                                                          in  (rhs', (substVar (env inh) (decls inh) lhs' rhs' . getTrans e inh, env inh))
     fLambda                                             = error "lambda"
     fMethodRef                                          = error "method reference"
                             
@@ -191,6 +198,44 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
     dimLengths a = case a of
                     ArrayCreate t exps dim          -> exps
                     _                               -> map (\n -> MethodInv (MethodCall (Name [Ident "*length"]) [a, (Lit (Int n))])) [0..]
+                    
+    -- Inlines a methodcall. This creates a variable to store the return value in
+    inlineMethod :: Inh -> MethodInvocation -> Stmt
+    inlineMethod inh (MethodCall name args) = getMethod (decls inh) (getMethodId name)
+    inlineMethod inh (PrimaryMethodCall _ _ id args) = getMethod (decls inh) id
+    inlineMethod inh _ = undefined
+    
+    -- Gets the variable that represents the return value of the method
+    getReturnVar :: Inh -> MethodInvocation -> Ident
+    getReturnVar inh invocation = Ident (show (invocationToId invocation) ++ show (getCallCount (calls inh) (invocationToId invocation)))
+    
+    -- Gets the object a method is called from
+    getObject :: MethodInvocation -> Exp
+    getObject (MethodCall name _) = ExpName (Name (take (length (fromName name) - 1) (fromName name)))
+    getObject (PrimaryMethodCall e _ _ _) = e
+    getObject _ = undefined
+    
+    -- Gets the return type of a method
+    getType :: Inh -> MethodInvocation -> Maybe Type
+    getType inh invocation = getMethodType (decls inh) (invocationToId invocation)
+    
+    -- Gets the method Id from an invocation
+    invocationToId :: MethodInvocation -> Ident
+    invocationToId (MethodCall name _) = getMethodId name
+    invocationToId (PrimaryMethodCall _ _ id _) = id
+    invocationToId _ = undefined
+    
+    -- Changes the lhs to refer to a field of a given object
+    lhsInObject :: Maybe Exp -> Lhs -> Lhs
+    lhsInObject Nothing lhs     = lhs
+    lhsInObject (Just obj) lhs  = case lhs of
+                                    NameLhs name -> FieldLhs (fieldAccess obj name)
+                                    _ -> error "TODO: lhsInObject"
+                                    
+    -- Changes the var to refer to a field of a given object
+    varInObject :: Maybe Exp -> Name -> Exp
+    varInObject Nothing name    = ExpName name
+    varInObject (Just obj) name = FieldAccess (fieldAccess obj name)
 
 -- | Gets the expression attribute
 getExp :: (Inh -> (Exp, Syn)) -> Inh -> Exp
@@ -206,11 +251,11 @@ getEnv f inh = let (_, (_, env)) = f inh in env
     
 -- | Calculates the weakest liberal pre-condition of a statement and a given post-condition
 wlp :: [TypeDecl] -> Stmt -> Exp -> Exp
-wlp decls = fst . (wlp' (Inh id id Nothing [] decls))
+wlp decls = fst . (wlp' (Inh id id Nothing [] decls [] Nothing Nothing))
 
 -- | wlp with a given type environment
 wlpWithEnv :: [TypeDecl] -> TypeEnv -> Stmt -> Exp -> Exp
-wlpWithEnv decls env = fst . (wlp' (Inh id id Nothing env decls))
+wlpWithEnv decls env = fst . (wlp' (Inh id id Nothing env decls [] Nothing Nothing))
 
 -- wlp' lets you specify the inherited attributes
 wlp' :: Inh -> Stmt -> Syn