Skip to content
Snippets Groups Projects
Commit 8fcbd2aa authored by koen's avatar koen
Browse files

Method calls implemented. Constructor methods and method arguments not yet implemented.

parent f0a5a6f8
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
HelperFunctions.hs
+ 9
− 0
View file @ 8fcbd2aa
......@@ -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)]
......
Substitute.hs
+ 9
− 9
View file @ 8fcbd2aa
......@@ -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)
......
Tests/methods.java
+ 11
− 4
View file @ 8fcbd2aa
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
WLP.hs
+ 30
− 23
View file @ 8fcbd2aa
......@@ -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
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment