From f0a5a6f8e48fb5b10ceacb5d7b16cf8f2eaf939d Mon Sep 17 00:00:00 2001
From: koen <koenwermer@gmail.com>
Date: Tue, 6 Dec 2016 20:18:36 +0100
Subject: [PATCH] started with method calls. Method calls on objects are still
very buggy
---
HelperFunctions.hs | 62 +++++++++++++++++++++++++++++++++++++++-
Main.hs | 23 ++-------------
Settings.hs | 2 +-
Tests/methods.java | 30 ++++++++++++++++++++
WLP.hs | 71 +++++++++++++++++++++++++++++++++++++---------
5 files changed, 153 insertions(+), 35 deletions(-)
create mode 100644 Tests/methods.java
diff --git a/HelperFunctions.hs b/HelperFunctions.hs
index 1db0c74..6512372 100644
--- a/HelperFunctions.hs
+++ b/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
diff --git a/Main.hs b/Main.hs
index 970cd4a..2fe1ca8 100644
--- a/Main.hs
+++ b/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
diff --git a/Settings.hs b/Settings.hs
index c8ba2e8..689be15 100644
--- a/Settings.hs
+++ b/Settings.hs
@@ -1,7 +1,7 @@
module Settings where
testFile, postCond :: String
-testFile = "loops"
+testFile = "methods"
postCond = "x == 5"
nrOfUnroll :: Int
diff --git a/Tests/methods.java b/Tests/methods.java
new file mode 100644
index 0000000..1fd298d
--- /dev/null
+++ b/Tests/methods.java
@@ -0,0 +1,30 @@
+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
diff --git a/WLP.hs b/WLP.hs
index ab0cc72..675a171 100644
--- a/WLP.hs
+++ b/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
--
GitLab