diff --git a/HelperFunctions.hs b/HelperFunctions.hs
index 4809a1fc9b3ecd8f89f7379038d6d3b6c115a011..32205bc9b80ae6283f6789cb806d8b2e40f66b5b 100644
--- a/HelperFunctions.hs
+++ b/HelperFunctions.hs
@@ -15,6 +15,7 @@ type CallCount = [(Ident, Int)]
-- | Retrieves the type from the environment
lookupType :: [TypeDecl] -> TypeEnv -> Name -> Type
lookupType decls env (Name ((Ident s@('$':_)) : idents)) = getFieldType decls (getReturnVarType decls s) (Name idents) -- Names starting with a '$' symbol are generated and represent the return variable of a function
+lookupType decls env (Name ((Ident s@('#':_)) : idents)) = PrimType undefined -- Names starting with a '#' symbol are generated and represent a variable introduced by handling operators
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)
@@ -118,7 +119,26 @@ isIntroducedVar :: Name -> Bool
isIntroducedVar (Name (Ident ('#':_): _)) = True
isIntroducedVar (Name (Ident ('$':_): _)) = True
isIntroducedVar _ = False
+
+-- Gets the variable that represents the return value of the method
+getReturnVar :: MethodInvocation -> Ident
+getReturnVar invocation = Ident (makeReturnVarName (invocationToId invocation) ++ show (getIncrPointer varPointer))
+
+-- Gets the method Id from an invocation
+invocationToId :: MethodInvocation -> Ident
+invocationToId (MethodCall name _) = getMethodId name
+invocationToId (PrimaryMethodCall _ _ id _) = id
+invocationToId _ = undefined
+
+-- Gets a new unique variable
+getVar :: Ident
+getVar = Ident ('#' : show (getIncrPointer varPointer))
+-- Gets multiple new unique variables
+getVars :: Int -> [Ident]
+getVars 0 = []
+getVars n = Ident ('#' : show (getIncrPointer varPointer)) : getVars (n-1)
+
-- The number of variables introduced
varPointer :: IORef Integer
varPointer = unsafePerformIO $ newIORef 0
diff --git a/Settings.hs b/Settings.hs
index bcb07f1e986b4b2754c4326e9f296f48414589dd..e7dc8c03afdbc043b6225c5aec8f8e26329b1558 100644
--- a/Settings.hs
+++ b/Settings.hs
@@ -1,8 +1,8 @@
module Settings where
testFile, postCond :: String
-testFile = "methods"
-postCond = "(x == 4)"
+testFile = "side-effects"
+postCond = "(x == 2)"
nrOfUnroll :: Int
-nrOfUnroll = 2
\ No newline at end of file
+nrOfUnroll = 1
\ No newline at end of file
diff --git a/Tests/side-effects.java b/Tests/side-effects.java
index b6f078aad4c7911f7882192d9a812b011b54f17e..5626bc62cd91f805b40f5dd31b0eaa5a158726a6 100644
--- a/Tests/side-effects.java
+++ b/Tests/side-effects.java
@@ -6,9 +6,9 @@ public static class Main
public static void main(String[] args)
{
x = 0;
- y = 0;
+ y = 3;
int i = 0;
- if(h() < 1)
+ while(f() < y)
{
x = f();
}
diff --git a/WLP.hs b/WLP.hs
index b602748131d4d175a31cdb2d58295355ee384fe2..295691abc967f668004d4257b0a04d8173788fb1 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -37,9 +37,11 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
fStmtBlock (Block bs) inh = foldr (\b r -> wlpBlock (inh {acc = r, env = envBlock bs (env inh)}) b) (acc inh) bs -- The result of the last block-statement will be the accumulated transformer for the second-last etc. The type environment is build from the left, so it has to be done seperately.
fIfThen e s1 = fIfThenElse e s1 (const id) -- if-then is just an if-then-else with an empty else-block
fIfThenElse e s1 s2 inh = let (e', trans) = foldExp wlpExpAlgebra e inh {acc = id}
- in ((\q -> (e' &* trans ((s1 inh {acc = id}) q)) |* (neg e' &* trans ((s2 inh {acc = id}) q))) . acc inh)
+ var = getVar
+ in trans . substVar' inh var e' . (\q -> (ExpName (Name [var]) &* s1 inh {acc = id} q) |* (neg (ExpName (Name [var])) &* s2 inh {acc = id} q)) . acc inh
fWhile e s inh = let (e', trans) = foldExp wlpExpAlgebra e inh {acc = id}
- in ((\q -> unrollLoop nrOfUnroll e' trans ((s (inh {acc = id, br = const q}))) q) . acc inh)
+ var = getVar
+ in (\q -> unrollLoop inh nrOfUnroll e' trans (s (inh {acc = id, br = const q})) q) . acc inh
fBasicFor init me incr s inh = let loop = (fWhile (fromMaybeGuard me) (\inh' -> s (inh {acc = (wlp' inh {acc = id} (incrToStmt incr))})) inh) in wlp' (inh {acc = loop}) (initToStmt init)
fEnhancedFor = error "EnhancedFor"
fEmpty inh = (acc inh) -- Empty does nothing, but still passes control to the next statement
@@ -87,9 +89,11 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
wlpDeclAssignment t inh (VarDecl (VarId ident) (Just (InitExp e))) = snd (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) -> Exp -> Exp
- unrollLoop 0 g gTrans _ q = (neg g `imp` gTrans q)
- unrollLoop n g gTrans bodyTrans q = (neg g `imp` gTrans q) &* (g `imp` gTrans (bodyTrans (unrollLoop (n - 1) g gTrans bodyTrans q)))
+ unrollLoop :: Inh -> Int -> Exp -> (Exp -> Exp) -> (Exp -> Exp) -> Exp -> Exp
+ unrollLoop inh 0 g gTrans _ = let var = getVar
+ in gTrans . substVar' inh var g . (neg (ExpName (Name [var])) `imp`)
+ unrollLoop inh n g gTrans bodyTrans = let var = getVar
+ in gTrans . substVar' inh var g . (\q -> (ExpName (Name [var]) &* bodyTrans q) |* (neg (ExpName (Name [var])) &* unrollLoop inh (n-1) g gTrans bodyTrans q))
-- Converts initialization code of a for loop to a statement
@@ -194,7 +198,8 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
fCast t e inh = let (e', trans) = e inh in (e', trans)
fBinOp e1 op e2 inh = let (e1', trans1) = e1 inh {acc = id}
(e2', trans2) = e2 inh {acc = id}
- in (BinOp e1' op e2', trans1 . trans2 . acc inh) -- Side effects of the first expression are applied before the second is evaluated, so we have to apply the transformer
+ [var1, var2] = getVars 2
+ in (BinOp (ExpName (Name [var1])) op (ExpName (Name [var2])), trans1 . substVar' inh var1 e1' . trans2 . substVar' inh var2 e2' . acc inh) -- Side effects of the first expression are applied before the second is evaluated
fInstanceOf = error "instanceOf"
fCond g e1 e2 inh = let (e1', trans1) = e1 inh {acc = id}
(e2', trans2) = e2 inh {acc = id}
@@ -243,14 +248,6 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
assignParam :: FormalParam -> Exp -> BlockStmt
assignParam (FormalParam mods t _ varId) e = LocalVars mods t [VarDecl varId (Just (InitExp e))]
- -- Gets the variable that represents the return value of the method
- getReturnVar :: MethodInvocation -> Ident
- getReturnVar invocation = Ident (makeReturnVarName (invocationToId invocation) ++ show (getIncrPointer varPointer))
-
- -- Gets a new unique variable
- getVar :: Ident
- getVar = Ident ('#' : show (getIncrPointer varPointer))
-
-- Gets the object a method is called from
getObject :: Inh -> MethodInvocation -> Maybe Exp
getObject inh (MethodCall name _) | length (fromName name) > 1 = Just (ExpName (Name (take (length (fromName name) - 1) (fromName name))))
@@ -268,12 +265,6 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
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
-
-- Folds the expression part of an lhs
foldLhs :: Inh -> Lhs -> Lhs
foldLhs inh lhs = case lhs of
@@ -292,8 +283,12 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
x -> error ("foldFieldAccess: " ++ show x ++ show id)
SuperFieldAccess id -> foldFieldAccess inh (PrimaryFieldAccess (fromJust' "foldFieldAccess" (object inh)) id)
ClassFieldAccess name id -> Name (fromName name ++ [id])
-
+
+-- Simplified version of substVar, handy to use with introduced variables
+substVar' :: Inh -> Ident -> Exp -> Syn
+substVar' inh var e = substVar (env inh) (decls inh) (NameLhs (Name [var])) e
+
-- | Calculates the weakest liberal pre-condition of a statement and a given post-condition
wlp :: [TypeDecl] -> Stmt -> Exp -> Exp
wlp decls = wlpWithEnv decls []