diff --git a/HelperFunctions.hs b/HelperFunctions.hs
index 4fa299fe65b55a46db5b17180b972d2cc58eff22..23c33a1ba49cf17d0b148a998f4b6f0321d66384 100644
--- a/HelperFunctions.hs
+++ b/HelperFunctions.hs
@@ -41,7 +41,9 @@ 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)))
+getReturnVarType decls s = case getMethodType decls (Ident (takeWhile (/= '$') (tail s))) of
+ Nothing -> PrimType undefined -- Kind of a hack. In case of library functions, it doesn't matter what type we return.
+ Just t -> t
-- Increments the call count for a given method
incrCallCount :: CallCount -> Ident -> CallCount
@@ -93,7 +95,7 @@ getMethod' classTypeDecls methodId = case (concatMap searchClass classTypeDecls)
-- Gets the statement(-block) defining the main method
getMainMethod :: [TypeDecl] -> Stmt
-getMainMethod classTypeDecls = fromJust $ getMethod classTypeDecls (Ident "main")
+getMainMethod classTypeDecls = fromJust' "getMainMethod" $ getMethod classTypeDecls (Ident "main")
-- Gets the class declarations
getDecls :: CompilationUnit -> [TypeDecl]
@@ -106,6 +108,12 @@ getStaticVars compUnit = concatMap fromTypeDecls (getDecls compUnit) where
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)
+
+-- Used for debugging
+fromJust' :: String -> Maybe a -> a
+fromJust' s ma = case ma of
+ Nothing -> error s
+ Just x -> x
true :: Exp
true = Lit (Boolean True)
diff --git a/Settings.hs b/Settings.hs
index 2b7ac5ac77dc2e8d31afc3091fbb34294839046a..80effa43a609c5b59e2f115248edf4226f3f7887 100644
--- a/Settings.hs
+++ b/Settings.hs
@@ -1,8 +1,8 @@
module Settings where
testFile, postCond :: String
-testFile = "side-effects"
-postCond = "(x == 2)"
+testFile = "2d-arrays1"
+postCond = "(true)"
nrOfUnroll :: Int
-nrOfUnroll = 2
\ No newline at end of file
+nrOfUnroll = 1
\ No newline at end of file
diff --git a/Tests/loops.java b/Tests/loops.java
index 4072c3e2d7a63bf758a5b889f38f2fa791a0cc02..913430806f86e6cb5796523f477d7399c7a1c829 100644
--- a/Tests/loops.java
+++ b/Tests/loops.java
@@ -4,15 +4,14 @@ public class C1
{
public static void main(String[] args)
{
- int i = 0;
-
- while(i < 6)
+ for(int i = 0; i < 6; i++)
{
- i++;
-
- if ( i == 5)
- break;
+ for(int j = 0; j < 6; j++)
+ {
+ if(true)
+ assert j == 1;
+ }
}
diff --git a/Tests/side-effects.java b/Tests/side-effects.java
index a70dcafdfa3b57be6404a594643ea9a01fdeefad..b6f078aad4c7911f7882192d9a812b011b54f17e 100644
--- a/Tests/side-effects.java
+++ b/Tests/side-effects.java
@@ -8,11 +8,10 @@ public static class Main
x = 0;
y = 0;
int i = 0;
- if((i++) + (i++) < 1)
+ if(h() < 1)
{
- x++;
+ x = f();
}
- x = blabla.g();
x++;
x++;
diff --git a/Verifier.hs b/Verifier.hs
index b63646334c74f81f779f01f1760e2967020009f2..cbe4ac8ef955cf9145b7be4334986f331f0669cd 100644
--- a/Verifier.hs
+++ b/Verifier.hs
@@ -6,6 +6,7 @@ import Z3.Monad
import System.IO.Unsafe
import Folds
+import HelperFunctions
-- | Checks wether the negation is unsatisfiable
@@ -61,7 +62,7 @@ expAssertAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQual
fThisClass = undefined
fInstanceCreation = undefined
fQualInstanceCreation = undefined
- fArrayCreate = undefined
+ fArrayCreate _ _ _ = mkTrue
fArrayCreateInit = undefined
fFieldAccess fieldAccess = case fieldAccess of
PrimaryFieldAccess e id -> case e of
@@ -75,7 +76,10 @@ expAssertAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQual
ArrayCreateInit t dim arrayInit -> mkInteger 0
_ -> error "length of non-array"
_ -> error (prettyPrint invocation)
- fArrayAccess _ = undefined
+ fArrayAccess arrayIndex = case arrayIndex of
+ ArrayIndex (ArrayCreate t _ _) _ -> foldExp expAssertAlgebra (getInitValue t)
+ ArrayIndex (ArrayCreateInit t _ _) _ -> foldExp expAssertAlgebra (getInitValue t)
+ ArrayIndex e _ -> foldExp expAssertAlgebra e
fExpName name = do
symbol <- mkStringSymbol (prettyPrint name)
mkIntVar symbol
@@ -95,51 +99,63 @@ expAssertAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQual
Mult -> do
ast1 <- e1
ast2 <- e2
- mkMul [ast1, ast2]
+ t <- mkTrue
+ if ast1 == t then mkTrue else mkMul [ast1, ast2]
Div -> do
ast1 <- e1
ast2 <- e2
- mkDiv ast1 ast2
+ t <- mkTrue
+ if ast1 == t then mkTrue else mkDiv ast1 ast2
Rem -> do
ast1 <- e1
ast2 <- e2
- mkRem ast1 ast2
+ t <- mkTrue
+ if ast1 == t then mkTrue else mkRem ast1 ast2
Add -> do
ast1 <- e1
ast2 <- e2
- mkAdd [ast1, ast2]
+ t <- mkTrue
+ if ast1 == t then mkTrue else mkAdd [ast1, ast2]
Sub -> do
ast1 <- e1
ast2 <- e2
- mkSub [ast1, ast2]
+ t <- mkTrue
+ if ast1 == t then mkTrue else mkSub [ast1, ast2]
LShift -> do
ast1 <- e1
ast2 <- e2
- mkBvshl ast1 ast2
+ t <- mkTrue
+ if ast1 == t then mkTrue else mkBvshl ast1 ast2
RShift -> do
ast1 <- e1
ast2 <- e2
- mkBvashr ast1 ast2
+ t <- mkTrue
+ if ast1 == t then mkTrue else mkBvashr ast1 ast2
RRShift -> do
ast1 <- e1
ast2 <- e2
- mkBvlshr ast1 ast2
+ t <- mkTrue
+ if ast1 == t then mkTrue else mkBvlshr ast1 ast2
LThan -> do
ast1 <- e1
ast2 <- e2
- mkLt ast1 ast2
+ t <- mkTrue
+ if ast1 == t then mkTrue else mkLt ast1 ast2
GThan -> do
ast1 <- e1
ast2 <- e2
- mkGt ast1 ast2
+ t <- mkTrue
+ if ast1 == t then mkTrue else mkGt ast1 ast2
LThanE -> do
ast1 <- e1
ast2 <- e2
- mkLe ast1 ast2
+ t <- mkTrue
+ if ast1 == t then mkTrue else mkLe ast1 ast2
GThanE -> do
ast1 <- e1
ast2 <- e2
- mkGe ast1 ast2
+ t <- mkTrue
+ if ast1 == t then mkTrue else mkGe ast1 ast2
Equal -> do
ast1 <- e1
ast2 <- e2
diff --git a/WLP.hs b/WLP.hs
index 65724a1d7ce1a57a45832089e063b87fc8c55a5c..283a8f7a15ff0c5f96d250701fd59fac40577018 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -43,7 +43,7 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
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 {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)
+ fBasicFor init me incr s inh = let loop = fst (fWhile (fromMaybeGuard me) (\inh' -> s (inh {acc = fst (wlp' inh {acc = id} (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
@@ -55,7 +55,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 [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
+ Just e -> fExpStmt (Assign (NameLhs (Name [fromJust' "fReturn" (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
@@ -77,7 +77,7 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
envBlock :: [BlockStmt] -> TypeEnv -> TypeEnv
envBlock bs env = foldl f env bs
where f env (LocalVars mods t vars) = foldr (\v env' -> (varName v, t):env') env vars
- f env (BlockStmt (BasicFor (Just (ForLocalVars mods t vars)) _ _ _)) = foldr (\v env' -> (varName v, t):env') env vars
+ f env (BlockStmt (BasicFor (Just (ForLocalVars mods t vars)) _ _ s)) = foldr (\v env' -> (varName v, t):env') env vars
f env _ = env
varName (VarDecl (VarId id) _) = Name [id]
@@ -147,7 +147,7 @@ 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 = (fromJust (object inh), (acc inh, env inh))
+ fThis inh = (fromJust' "fThis" (object inh), (acc inh, env inh))
fThisClass name inh = (ThisClass name, (acc inh, env inh))
fInstanceCreation typeArgs t args mBody inh = case args of
[ExpName (Name [Ident "#"])] -> (InstanceCreation typeArgs t args mBody, (acc inh, env inh)) -- '#' indicates we already called the constructor method using the correct arguments
@@ -159,11 +159,11 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
fArrayCreateInit t dim init inh = (ArrayCreateInit t dim init, (acc inh, env inh))
fFieldAccess fieldAccess inh = (ExpName (foldFieldAccess inh fieldAccess), (acc inh, env inh))
fMethodInv invocation inh = case invocation of
- MethodCall (Name [Ident "*assume"]) [e] -> (Lit Null, (if e == false then const true else imp e, env inh))
- _ -> (ExpName (Name [getReturnVar inh invocation]),
- (if getCallCount (calls inh) (invocationToId invocation) >= nrOfUnroll
- then const true
- else fst (wlp' (inh {acc = id, calls = incrCallCount (calls inh) (invocationToId invocation), ret = Just (getReturnVar inh invocation), object = getObject inh invocation}) (inlineMethod inh invocation)) . acc inh, env inh))
+ MethodCall (Name [Ident "*assume"]) [e] -> (false, (if e == false then const true else imp e, env inh))
+ _ -> if getCallCount (calls inh) (invocationToId invocation) >= nrOfUnroll
+ then (false, (const true, env inh))
+ else let callWlp = fst (wlp' (inh {acc = id, calls = incrCallCount (calls inh) (invocationToId invocation), ret = Just (getReturnVar inh invocation), object = getObject inh invocation}) (inlineMethod inh invocation))
+ in (callWlp (ExpName (Name [getReturnVar inh invocation])), (callWlp . acc inh, env inh))
fArrayAccess (ArrayIndex a i) inh = case catch inh of
Nothing -> (arrayAccess a i, (getTrans (foldExp wlpExpAlgebra a) inh, env inh))
Just (cs, f) -> (arrayAccess a i, (getTrans (foldExp wlpExpAlgebra a) inh {acc = id} . arrayAccessWlp a i inh, env inh))
@@ -275,7 +275,7 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
PrimaryFieldAccess e id -> case getExp (foldExp wlpExpAlgebra e) inh of
ExpName name -> Name (fromName name ++ [id])
x -> error ("foldFieldAccess: " ++ show x ++ show id)
- SuperFieldAccess id -> foldFieldAccess inh (PrimaryFieldAccess (fromJust (object inh)) id)
+ SuperFieldAccess id -> foldFieldAccess inh (PrimaryFieldAccess (fromJust' "foldFieldAccess" (object inh)) id)
ClassFieldAccess name id -> Name (fromName name ++ [id])
-- | Gets the expression attribute
@@ -292,7 +292,7 @@ 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 [] Nothing Nothing 0))
+wlp decls = wlpWithEnv decls []
-- | wlp with a given type environment
wlpWithEnv :: [TypeDecl] -> TypeEnv -> Stmt -> Exp -> Exp