From c54ffb12b95887cb42750e9316b9814e40948b6b Mon Sep 17 00:00:00 2001
From: koen <koenwermer@gmail.com>
Date: Sat, 17 Dec 2016 18:29:58 +0100
Subject: [PATCH] binary operators being applied on expressions with
side-effects are now being handled correctly
---
Settings.hs | 4 ++--
Tests/side-effects.java | 8 ++++----
WLP.hs | 14 ++++++++------
3 files changed, 14 insertions(+), 12 deletions(-)
diff --git a/Settings.hs b/Settings.hs
index 4c43c93..2b7ac5a 100644
--- a/Settings.hs
+++ b/Settings.hs
@@ -2,7 +2,7 @@ module Settings where
testFile, postCond :: String
testFile = "side-effects"
-postCond = "(x == 6)"
+postCond = "(x == 2)"
nrOfUnroll :: Int
-nrOfUnroll = 4
\ No newline at end of file
+nrOfUnroll = 2
\ No newline at end of file
diff --git a/Tests/side-effects.java b/Tests/side-effects.java
index 683e22d..d26692b 100644
--- a/Tests/side-effects.java
+++ b/Tests/side-effects.java
@@ -6,12 +6,12 @@ public static class Main
x = 0;
y = 0;
int i = 0;
-
- while(i < f())
+ if((i++) + (i++) < 1)
{
- x += y;
- i++;
+ x++;
}
+ x++;
+ x++;
}
diff --git a/WLP.hs b/WLP.hs
index 433a759..f187e86 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -39,14 +39,16 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
fStmtBlock (Block bs) inh = fst $ foldr (\b ((r, env'), varNr') -> (wlpBlock (inh {acc = r, env = env', varNr = varNr'}) b, varNr' + 1)) ((acc inh, envBlock bs (env inh)), varNr 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' = getExp (foldExp wlpExpAlgebra e) inh
- in (getTrans (foldExp wlpExpAlgebra e) inh . (\q -> (e' &* fst (s1 inh) q) |* (neg e' &* fst (s2 inh) q)) . acc inh, env inh)
+ eTrans = getTrans (foldExp wlpExpAlgebra e) inh {acc = id} -- The guard might also have side effects
+ in ((\q -> (e' &* eTrans (fst (s1 inh {acc = id}) q)) |* (neg e' &* eTrans (fst (s2 inh {acc = id}) q))) . acc inh, env inh)
fWhile e s inh = let e' = getExp (foldExp wlpExpAlgebra e) inh
- in ((\q -> unrollLoop nrOfUnroll e' (getTrans (foldExp wlpExpAlgebra e) inh) (fst (s (inh {br = const q}))) q) . acc inh, env inh)
+ in ((\q -> unrollLoop nrOfUnroll e' (getTrans (foldExp wlpExpAlgebra e) inh {acc = id}) (fst (s (inh {acc = id, br = const q}))) q) . acc inh, env inh)
fBasicFor init me incr s inh = let loop = fst (fWhile (fromMaybeGuard me) (\inh' -> s (inh {acc = fst (wlp' inh' (incrToStmt incr))})) inh) in wlp' (inh {acc = loop}) (initToStmt init)
fEnhancedFor = error "EnhancedFor"
fEmpty inh = (acc inh, env inh) -- Empty does nothing, but still passes control to the next statement
fExpStmt e inh = snd $ foldExp wlpExpAlgebra e inh
- fAssert e _ inh = ((e &*) . getTrans (foldExp wlpExpAlgebra e) inh, env inh)
+ fAssert e _ inh = let e' = getExp (foldExp wlpExpAlgebra e) inh
+ in ((e' &*) . getTrans (foldExp wlpExpAlgebra e) inh, env inh)
fSwitch e bs inh = let (e', s1, s2) = desugarSwitch e bs in fIfThenElse e' (flip wlp' s1) (flip wlp' s2) (inh {acc = id, br = acc inh})
fDo s e inh = (fst (s (inh {acc = fst (fWhile e s inh)})), env inh) -- Do is just a while with the statement block executed one additional time. Break and continue still have to be handled in this additional execution.
fBreak _ inh = (br inh, env inh) -- wlp of the breakpoint. Control is passed to the statement after the loop
@@ -89,8 +91,8 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
-- Unrolls a while-loop a finite amount of times
unrollLoop :: Int -> Exp -> (Exp -> Exp) -> (Exp -> Exp) -> Exp -> Exp
- unrollLoop 0 g gTrans _ q = gTrans (neg g `imp` q)
- unrollLoop n g gTrans bodyTrans q = gTrans (neg g `imp` q) &* gTrans (g `imp` bodyTrans (unrollLoop (n - 1) g gTrans bodyTrans q))
+ 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)))
-- Converts initialization code of a for loop to a statement
@@ -184,7 +186,7 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
fPreBitCompl e inh = (PreBitCompl $ getExp e inh, (getTrans e inh, env inh))
fPreNot e inh = (PreNot $ getExp e inh, (getTrans e inh, env inh))
fCast t e inh = (getExp e inh, (getTrans e 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 (getTrans e1 (inh {acc = id}) (getExp e2 inh)), (getTrans e1 (inh {acc = getTrans e2 inh}), env inh)) -- Side effects of the first expression are applied before the second is evaluated, so we have to apply the transformer
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' = foldLhs inh lhs
--
GitLab