From 8fcbd2aa73cb380349b88c73a58319fc50ced88a Mon Sep 17 00:00:00 2001
From: koen <koenwermer@gmail.com>
Date: Fri, 9 Dec 2016 23:39:40 +0100
Subject: [PATCH] Method calls implemented. Constructor methods and method
arguments not yet implemented.
---
HelperFunctions.hs | 9 ++++++++
Substitute.hs | 18 ++++++++--------
Tests/methods.java | 15 +++++++++----
WLP.hs | 53 ++++++++++++++++++++++++++--------------------
4 files changed, 59 insertions(+), 36 deletions(-)
diff --git a/HelperFunctions.hs b/HelperFunctions.hs
index 6512372..1b0c1c4 100644
--- a/HelperFunctions.hs
+++ b/HelperFunctions.hs
@@ -10,6 +10,7 @@ type CallCount = [(Ident, Int)]
-- | Retrieves the type from the environment
lookupType :: [TypeDecl] -> TypeEnv -> Name -> Type
+lookupType decls env (Name [(Ident s@('$':_))]) = getReturnVarType decls s -- Names starting with a '$' symbol are generated and represent the return variable of a function
lookupType decls env (Name idents) = case lookup (Name [head idents]) env of
Just t -> getFieldType decls t (Name (tail idents))
Nothing -> error ("can't find type of " ++ prettyPrint (Name idents) ++ "\r\n TypeEnv: " ++ show env)
@@ -34,6 +35,14 @@ getFieldType decls (RefType (ClassRefType t)) (Name (f:fs)) = getFieldType decls
_ -> getDecl t xs
getDecl _ _ = error "nested class"
+-- | Creates a string that that represents the return var name of a method call. This name is extended by a number to indicate the depth of the recursive calls
+makeReturnVarName :: Ident -> String
+makeReturnVarName (Ident s) = "$" ++ s ++ "$"
+
+-- | Get's the type of a generated variable
+getReturnVarType :: [TypeDecl] -> String -> Type
+getReturnVarType decls s = fromJust $ getMethodType decls (Ident (takeWhile (/= '$') (tail s)))
+
-- Increments the call count for a given method
incrCallCount :: CallCount -> Ident -> CallCount
incrCallCount [] id = [(id, 1)]
diff --git a/Substitute.hs b/Substitute.hs
index 41e5bdf..ed79237 100644
--- a/Substitute.hs
+++ b/Substitute.hs
@@ -47,8 +47,8 @@ substVarExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQu
_ -> ExpName (Name name)
-- done:
Just [] -> ExpName (Name name)
- -- check a combination and recurse:
- Just ((nameInit, lhsNameInit) : combs') -> flip (foldExp substVarExpAlgebra) (inh {combs = Just combs'}) $
+ -- check a combination and recurse when necessary:
+ Just ((nameInit, lhsNameInit) : combs') ->
case lhs inh of
NameLhs (Name lhsName) -> case lookupType (decls inh) (env inh) (Name lhsNameInit) of
PrimType _ | lhsName == name -> rhs inh
@@ -56,24 +56,24 @@ substVarExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQu
ExpName (Name rhsName) | take (length lhsName) name == lhsName -> ExpName (Name (rhsName ++ drop (length lhsName) name))
-- accessing o1.x might affect o2.x if o1 and o2 point to the same object:
| name == nameInit ++ drop (length lhsNameInit) lhsName && length name > length nameInit -> Cond (ExpName (Name nameInit) ==* ExpName (Name lhsNameInit)) (rhs inh) (ExpName (Name name))
- | otherwise -> ExpName (Name name)
+ | otherwise -> foldExp substVarExpAlgebra (ExpName (Name name)) (inh {combs = Just combs'})
-- we substitute instance creation only if we access a field, to not lose pointer information
-- example: {x = new obj} doesn't affect {x = y} but it does affect {x.a = y.a}
InstanceCreation _ _ _ _ | length lhsName < length name && take (length lhsName) name == lhsName -> getFields (decls inh) (rhs inh) (drop (length lhsName) name)
| length lhsName < length name && take (length lhsName) name == nameInit ++ drop (length nameInit) lhsName -> Cond (ExpName (Name nameInit) ==* ExpName (Name lhsNameInit)) (getFields (decls inh) (rhs inh) (drop (length lhsName) name)) (ExpName (Name name))
- | otherwise -> ExpName (Name name)
+ | otherwise -> foldExp substVarExpAlgebra (ExpName (Name name)) (inh {combs = Just combs'})
-- the same idea for arrays
- ArrayCreate _ _ _ | not $ arrayLookup inh -> ExpName (Name name)
- ArrayCreateInit _ _ _ | not $ arrayLookup inh -> ExpName (Name name)
+ ArrayCreate _ _ _ | not $ arrayLookup inh -> foldExp substVarExpAlgebra (ExpName (Name name)) (inh {combs = Just combs'})
+ ArrayCreateInit _ _ _ | not $ arrayLookup inh -> foldExp substVarExpAlgebra (ExpName (Name name)) (inh {combs = Just combs'})
_ | take (length lhsName) name == lhsName -> getFields (decls inh) (rhs inh) (drop (length lhsName) name)
| name == nameInit ++ drop (length lhsNameInit) lhsName -> Cond (ExpName (Name nameInit) ==* ExpName (Name lhsNameInit)) (rhs inh) (ExpName (Name name))
-- the assignment doesn't affect this expression:
- | otherwise -> ExpName (Name name)
- _ -> ExpName (Name name)
- _ -> ExpName (Name name)
+ | otherwise -> foldExp substVarExpAlgebra (ExpName (Name name)) (inh {combs = Just combs'})
+ _ -> foldExp substVarExpAlgebra (ExpName (Name name)) (inh {combs = Just combs'})
+ _ -> foldExp substVarExpAlgebra (ExpName (Name name)) (inh {combs = Just combs'})
fPostIncrement e inh = PostIncrement (e inh)
fPostDecrement e inh = PostDecrement (e inh)
fPreIncrement e inh = PreIncrement (e inh)
diff --git a/Tests/methods.java b/Tests/methods.java
index 1fd298d..0ded15c 100644
--- a/Tests/methods.java
+++ b/Tests/methods.java
@@ -1,17 +1,19 @@
public static class Main
{
- static int x;
+ static int x, y;
public static void main(String[] args)
{
C1 c1 = new C1();
- c1.c += 2; //c1.method1();
+ c1.method1();
+ c1.method1();
x = c1.c;
}
- public static void method()
+ public static int method()
{
+ return 1;
}
}
@@ -25,6 +27,11 @@ public class C1
public void method1()
{
- // c++;
+ this.c += 1;
+ }
+
+ public int method2()
+ {
+ return 1;
}
}
\ No newline at end of file
diff --git a/WLP.hs b/WLP.hs
index 675a171..eaaf3c1 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -144,22 +144,22 @@ wlpExpAlgebra :: ExpAlgebra (Inh -> (Exp, Syn))
wlpExpAlgebra = (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 lit inh = (Lit lit, (acc inh, env inh))
fClassLit mType inh = (ClassLit mType, (acc inh, env inh))
- fThis inh = (This, (acc inh, env inh))
+ fThis inh = (fromJust (object inh), (acc inh, env inh))
fThisClass name inh = (ThisClass name, (acc inh, env inh))
fInstanceCreation typeArgs t args mBody inh = (InstanceCreation typeArgs t args mBody, (acc inh, env inh))
fQualInstanceCreation e typeArgs t args mBody inh = (QualInstanceCreation (getExp e inh) typeArgs t args mBody, (getTrans e inh, env inh))
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))
+ fFieldAccess fieldAccess inh = (ExpName (foldFieldAccess inh fieldAccess), (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))
+ else fst (wlp' (inh {acc = id, calls = incrCallCount (calls inh) (invocationToId invocation), ret = Just (getReturnVar inh invocation), object = 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 = (varInObject (object inh) name, (acc inh, env inh))
+ fExpName name inh = (ExpName 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))
@@ -179,12 +179,12 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
fPreBitCompl e inh = (PreBitCompl $ getExp e inh, (acc inh, env inh))
fPreNot e inh = (PreNot $ getExp e inh, (acc inh, env inh))
fCast t e inh = (getExp e inh, (acc inh, env inh))
- fBinOp e1 op e2 inh = (BinOp (getExp e1 inh) op (getExp e2 inh), (getTrans e1 (inh {acc = getTrans e2 inh}), env inh))
+ fBinOp e1 op e2 inh = (BinOp (getExp e1 inh) op (getExp e2 inh), (getTrans e2 (inh {acc = getTrans e1 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 lhs' = lhsInObject (object inh) lhs
+ fAssign lhs op e inh = let lhs' = foldLhs inh lhs
rhs' = desugarAssign lhs' op (getExp e inh)
- in (rhs', (substVar (env inh) (decls inh) lhs' rhs' . getTrans e inh, env inh))
+ in (rhs', (getTrans e inh {acc = id} . substVar (env inh) (decls inh) lhs' rhs' . acc inh, env inh))
fLambda = error "lambda"
fMethodRef = error "method reference"
@@ -207,13 +207,14 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
-- 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)))
+ getReturnVar inh invocation = Ident (makeReturnVarName (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
+ getObject :: MethodInvocation -> Maybe Exp
+ getObject (MethodCall name _) | length (fromName name) > 1 = Just (ExpName (Name (take (length (fromName name) - 1) (fromName name))))
+ | otherwise = Nothing
+ getObject (PrimaryMethodCall e _ _ _) = Just e
+ getObject _ = undefined
-- Gets the return type of a method
getType :: Inh -> MethodInvocation -> Maybe Type
@@ -225,17 +226,23 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
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)
+ -- Folds the expression part of an lhs
+ foldLhs :: Inh -> Lhs -> Lhs
+ foldLhs inh lhs = case lhs of
+ FieldLhs (PrimaryFieldAccess e id) -> case getExp (foldExp wlpExpAlgebra e) inh of
+ ExpName name -> NameLhs (Name (fromName name ++ [id]))
+ _ -> error "foldFieldAccess"
+ ArrayLhs (ArrayIndex e i) -> ArrayLhs (ArrayIndex (getExp (foldExp wlpExpAlgebra e) inh) (map (\e -> getExp (foldExp wlpExpAlgebra e) inh) i))
+ lhs' -> lhs'
+
+ -- Folds the expression part of a fieldaccess and simplifies it to a name
+ foldFieldAccess :: Inh -> FieldAccess -> Name
+ foldFieldAccess inh fieldAccess = case fieldAccess of
+ PrimaryFieldAccess e id -> case getExp (foldExp wlpExpAlgebra e) inh of
+ ExpName name -> Name (fromName name ++ [id])
+ _ -> error "foldFieldAccess"
+ SuperFieldAccess id -> foldFieldAccess inh (PrimaryFieldAccess (fromJust (object inh)) id)
+ ClassFieldAccess name id -> Name (fromName name ++ [id])
-- | Gets the expression attribute
getExp :: (Inh -> (Exp, Syn)) -> Inh -> Exp
--
GitLab