diff --git a/HelperFunctions.hs b/HelperFunctions.hs
index fea11878aff214779080ab361ebd90389329ab99..05c39c01421cdc499f291cfdeaaf9f3376380a95 100644
--- a/HelperFunctions.hs
+++ b/HelperFunctions.hs
@@ -102,17 +102,17 @@ getMethod' classTypeDecls methodId = case (concatMap searchClass classTypeDecls)
getMainMethod :: [TypeDecl] -> Stmt
getMainMethod classTypeDecls = fromJust' "getMainMethod" $ getMethod classTypeDecls (Ident "main")
+-- Gets a list of all method Idents (except constructor methods)
+getMethodIds :: [TypeDecl] -> [Ident]
+getMethodIds classTypeDecls = concatMap searchClass classTypeDecls where
+ searchClass (ClassTypeDecl (ClassDecl _ _ _ _ _ (ClassBody decls))) = searchDecls decls
+ searchDecls (MemberDecl (MethodDecl _ _ _ id _ _ _):decls) = id : searchDecls decls
+ searchDecls (_:decls) = searchDecls decls
+ searchDecls [] = []
+
-- Gets the class declarations
getDecls :: CompilationUnit -> [TypeDecl]
getDecls (CompilationUnit _ _ classTypeDecls) = classTypeDecls
-
--- Gets the static member declarations and puts them in the type environment
-getStaticVars :: CompilationUnit -> TypeEnv
-getStaticVars compUnit = concatMap fromTypeDecls (getDecls compUnit) where
- fromTypeDecls (ClassTypeDecl (ClassDecl _ _ _ _ _ (ClassBody decls))) = concatMap fromMemberDecl decls
- 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)
-- Checks if the var is introduced. Introduced variable names start with '$' voor return variables of methods and '#' for other variables
isIntroducedVar :: Name -> Bool
@@ -130,6 +130,11 @@ invocationToId (MethodCall name _) = getMethodId name
invocationToId (PrimaryMethodCall _ _ id _) = id
invocationToId _ = undefined
+-- Gets the type of the elements of an array. Recursion is needed in the case of multiple dimensional arrays
+arrayContentType :: Type -> Type
+arrayContentType (RefType (ArrayType t)) = arrayContentType t
+arrayContentType t = t
+
-- Gets a new unique variable
getVar :: Ident
getVar = Ident ('#' : show (getIncrPointer varPointer))
diff --git a/Main.hs b/Main.hs
index 2fe1ca8026b904983167af0e463accc91a1679fd..5f45bdd5689bf60381b01451b1a436882f98df20 100644
--- a/Main.hs
+++ b/Main.hs
@@ -4,10 +4,12 @@ import Language.Java.Syntax
import Language.Java.Parser
import Language.Java.Pretty
import Data.List
+import Control.Monad
import System.FilePath(joinPath)
import WLP
+import Types
import Verifier
import HelperFunctions
import Settings
@@ -22,16 +24,23 @@ main = do
case result of
Left error -> print error
Right compUnit -> do
- putStrLn "\r\n-----Code-----"
- print compUnit
- putStrLn "\r\n-----WLP-----"
- let pred = wlpWithEnv (getDecls compUnit) (getStaticVars compUnit) (getMainMethod (getDecls compUnit)) postCond'
- putStrLn . prettyPrint $ pred
- putStrLn "\r\n-----Correctness-----"
- if unsafeIsTrue pred then putStrLn "WLP evaluates to true" else (if unsafeIsFalse pred then putStrLn "WLP evaluates to false" else putStrLn "undecidable")
+ let decls = getDecls compUnit
+ let methods = getMethodIds decls
+ let env = getTypeEnv compUnit decls methods
+ -- putStrLn "\r\n-----Code-----"
+ -- print compUnit
+ mapM_ (testMethod compUnit env decls) methods
-
-
+-- | Calculates and prints the wlp for a given method
+testMethod :: CompilationUnit -> TypeEnv -> [TypeDecl] -> Ident -> IO ()
+testMethod compUnit env decls id = do
+ putStrLn "--------------"
+ putStrLn (prettyPrint id ++ "\r\n")
+ let pred = wlpWithEnv decls env (fromJust' "testMethod" $ getMethod decls id) postCond'
+ putStrLn . prettyPrint $ pred
+ putStrLn ""
+ if unsafeIsTrue env pred then putStrLn "WLP evaluates to true" else (if unsafeIsFalse env pred then putStrLn "WLP evaluates to false" else putStrLn "undecidable")
+ putStrLn "--------------"
-- The post-condition (for testing)
postCond' :: Exp
diff --git a/Settings.hs b/Settings.hs
index 0653c923a48040ec5b61689e81b9e9650329ca79..0e4b16f0750287d364f51c0c7c582b23ce59ed6b 100644
--- a/Settings.hs
+++ b/Settings.hs
@@ -1,7 +1,7 @@
module Settings where
testFile, postCond :: String
-testFile = "arrays3"
+testFile = "arrays1"
postCond = "(true)"
nrOfUnroll :: Int
diff --git a/Tests/2d-arrays1.java b/Tests/2d-arrays1.java
index 9841c300e3ada474acea61334094e94ebbec4a42..6d1d2baeb4ccf5ab2d387edfe5b9b1d252159b33 100644
--- a/Tests/2d-arrays1.java
+++ b/Tests/2d-arrays1.java
@@ -59,9 +59,9 @@ public class Life {
}
public static boolean occupiedNext(int numNeighbors, boolean occupied){
- if( occupied && (numNeighbors == 2 || numNeighbors == 3))
+ if(occupied && ((numNeighbors == 2) || (numNeighbors == 3)))
return true;
- else if (!occupied && numNeighbors == 3)
+ else if ((!occupied) && (numNeighbors == 3))
return true;
else
return false;
@@ -69,17 +69,17 @@ public class Life {
private static int numNeighbors(boolean[][] world, int row, int col) {
int num2 = world[row][col] ? -1 : 0;
- for(int r1 = row - 1; r1 <= row + 1; r1++)
- for(int c1 = col - 1; c1 <= col + 1; c1++)
- if( inbounds(world, r1, c1) && world[r1][c1] )
+ for(int r1 = (row - 1); r1 <= (row + 1); r1++)
+ for(int c1 = (col - 1); c1 <= (col + 1); c1++)
+ if((inbounds(world, r1, c1)) && (world[r1][c1]) )
num2++;
return num2;
}
private static boolean inbounds(boolean[][] world, int i, int c2) {
- return i >= 0 && i < world.length && c2 >= 0 &&
- c2 < world[0].length;
+ return (i >= 0) && (i < world.length) && (c2 >= 0) &&
+ (c2 < world[0].length);
}
diff --git a/Tests/arrays1.java b/Tests/arrays1.java
index 9f0ef348a3a52d3df25870c0ca2e0953c1625d66..fdffebf49a2f2358e0e190d823968da3781f67a6 100644
--- a/Tests/arrays1.java
+++ b/Tests/arrays1.java
@@ -9,7 +9,7 @@ public class ArrayExamples
findAndPrintPairs(list, 5);
bubblesort(list);
- /*
+
showList(list);
list = new int[11];
@@ -23,14 +23,14 @@ public class ArrayExamples
list = new int[1];
bubblesort(list);
showList(list);
- */
+
}
// pre: list != null, list.length > 0
// post: return index of minimum element of array
public static int findMin(int[] list2)
- { assert list2 != null && list2.length > 0 : "failed precondition";
+ { assert (list2 != null) && (list2.length > 0) : "failed precondition";
int indexOfMin = 0;
for(int k = 1; k < list2.length; k++)
@@ -49,7 +49,7 @@ public class ArrayExamples
* argument
*/
public static void badResize(int[] list3, int newSize)
- { assert list3 != null && newSize >= 0 : "failed precondition";
+ { assert (list3 != null) && (newSize >= 0) : "failed precondition";
int[] temp = new int[newSize];
int limit = Math.min(list3.length, newSize);
@@ -70,7 +70,7 @@ public class ArrayExamples
* will be copied into the new array
*/
public static int[] goodResize(int[] list4, int newSize)
- { assert list4 != null && newSize >= 0 : "failed precondition";
+ { assert (list4 != null) && (newSize >= 0) : "failed precondition";
int[] result = new int[newSize];
int limit = Math.min(list4.length, newSize);
@@ -110,7 +110,7 @@ public class ArrayExamples
{
assert list6 != null : "failed precondition";
- int temp;
+ int temp2;
boolean changed = true;
for(int n = 0; (n < list6.length) && changed; n++)
{ changed = false;
@@ -119,9 +119,9 @@ public class ArrayExamples
"is out of bounds.";
if(list6[o] > list6[o+1])
{ changed = true;
- temp = list6[o + 1];
+ temp2 = list6[o + 1];
list6[o + 1] = list6[o];
- list6[o] = temp;
+ list6[o] = temp2;
}
}
}
diff --git a/Tests/methods.java b/Tests/methods.java
index 47b8dfdcea5a197a035670288a461f4810d1e6b1..661059a1105f84f837a7ebd7148640f67d67d064 100644
--- a/Tests/methods.java
+++ b/Tests/methods.java
@@ -6,8 +6,8 @@ public static class Main
C c1, c2;
c1 = new C(1);
c2 = new C(0);
- c1.method1(1);
- c2.method1(1);
+ c1.method1(1, true);
+ c2.method1(1, true);
x = c1.c + c2.c;
// C.staticMethod();
}
@@ -34,12 +34,12 @@ public class C
x = 4;
}
- public void method1(int n)
+ public void method1(int n, boolean b)
{
-
+ assert b;
this.c += n;
if(this.c < 2)
- this.method1();
+ this.method1();
}
public int method2()
diff --git a/Types.hs b/Types.hs
new file mode 100644
index 0000000000000000000000000000000000000000..26d984dd9f39a226072d356c8bcd927f6aeaaf0e
--- /dev/null
+++ b/Types.hs
@@ -0,0 +1,79 @@
+module Types where
+
+import Language.Java.Syntax
+import Data.Maybe
+import Data.List
+
+import Folds
+import HelperFunctions
+import Settings
+
+
+typesStmtAlgebra :: StmtAlgebra TypeEnv
+typesStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhancedFor, fEmpty, fExpStmt, fAssert, fSwitch, fDo, fBreak, fContinue, fReturn, fSynchronized, fThrow, fTry, fLabeled) where
+ fStmtBlock b = envBlock b
+ fIfThen e s1 = s1
+ fIfThenElse e s1 s2 = s1 ++ s2
+ fWhile e s = s
+ fBasicFor init me incr s = case init of
+ Just (ForLocalVars mods t vars) -> foldr (\v env' -> (varName v, t):env') s vars
+ _ -> s
+ fEnhancedFor = error "EnhancedFor"
+ fEmpty = []
+ fExpStmt e = []
+ fAssert e _ = []
+ fSwitch e bs = concatMap envSwitch bs
+ fDo s e = s
+ fBreak _ = []
+ fContinue _ = []
+ fReturn me = []
+ fSynchronized _ _ = []
+ fThrow e = []
+ fTry b cs f = envBlock b ++ concatMap envCatch cs ++
+ (case f of
+ Just b -> envBlock b
+ _ -> [])
+ fLabeled _ s = s
+
+
+ -- Adds declarations within a block to a type environment
+ envBlock :: Block -> TypeEnv
+ envBlock (Block bs) = foldl f [] bs
+ where f env (LocalVars mods t vars) = foldr (\v env' -> (varName v, t):env') env vars
+ f env (BlockStmt s) = foldStmt typesStmtAlgebra s ++ env
+ f env _ = env
+
+ varName (VarDecl (VarId id) _) = Name [id]
+
+ -- Adds declarations within a switchblock block to a type environment
+ envSwitch :: SwitchBlock -> TypeEnv
+ envSwitch (SwitchBlock _ bs) = envBlock (Block bs)
+
+ -- Adds declarations within a catchblock block to a type environment
+ envCatch :: Catch -> TypeEnv
+ envCatch (Catch (FormalParam _ t _ varId) b) = (Name [getId varId], t) : envBlock b
+
+
+-- Gets the types of all variables that are declared in a statement
+getStmtTypeEnv :: Stmt -> TypeEnv
+getStmtTypeEnv = foldStmt typesStmtAlgebra
+
+-- Gets the parameters of a function and puts them in the type environment
+getMethodTypeEnv :: [TypeDecl] -> Ident -> TypeEnv
+getMethodTypeEnv decls id = case getMethodParams decls id of
+ Nothing -> []
+ Just params -> map fromParam params
+ where
+ fromParam (FormalParam _ t _ paramId) = (Name [getId paramId], t)
+
+-- Gets the static member declarations and puts them in the type environment
+getStaticVarsTypeEnv :: CompilationUnit -> TypeEnv
+getStaticVarsTypeEnv compUnit = concatMap fromTypeDecls (getDecls compUnit) where
+ fromTypeDecls (ClassTypeDecl (ClassDecl _ _ _ _ _ (ClassBody decls))) = concatMap fromMemberDecl decls
+ 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)
+
+-- Gets the type env for a compilation unit
+getTypeEnv :: CompilationUnit -> [TypeDecl] -> [Ident] -> TypeEnv
+getTypeEnv compUnit decls methods = getStaticVarsTypeEnv compUnit ++ concatMap (getMethodTypeEnv decls) methods ++ concatMap (getStmtTypeEnv . fromJust . getMethod decls) methods
\ No newline at end of file
diff --git a/Verifier.hs b/Verifier.hs
index d86c402736874307f12a349bd831eb60733f7dc3..c2406e9720b9305ff1586422653d60e217f54cd0 100644
--- a/Verifier.hs
+++ b/Verifier.hs
@@ -10,15 +10,15 @@ import HelperFunctions
-- | Checks wether the negation is unsatisfiable
-isTrue :: Exp -> Z3 Bool
-isTrue e = isFalse (PreNot e)
+isTrue :: TypeEnv -> Exp -> Z3 Bool
+isTrue env e = isFalse env (PreNot e)
-- | Checks wether the expression is unsatisfiable
-isFalse :: Exp -> Z3 Bool
-isFalse e =
+isFalse :: TypeEnv -> Exp -> Z3 Bool
+isFalse env e =
do
- ast <- foldExp expAssertAlgebra e
+ ast <- foldExp expAssertAlgebra e env
assert ast
result <- check
solverReset
@@ -27,12 +27,12 @@ isFalse e =
_ -> return False
-- | Unsafe version of isTrue
-unsafeIsTrue :: Exp -> Bool
-unsafeIsTrue = unsafePerformIO . evalZ3 . isTrue
+unsafeIsTrue :: TypeEnv -> Exp -> Bool
+unsafeIsTrue env = unsafePerformIO . evalZ3 . isTrue env
-- | Unsafe version of isFalse
-unsafeIsFalse :: Exp -> Bool
-unsafeIsFalse = unsafePerformIO . evalZ3 . isFalse
+unsafeIsFalse :: TypeEnv -> Exp -> Bool
+unsafeIsFalse env = unsafePerformIO . evalZ3 . isFalse env
stringToBv :: String -> Z3 AST
stringToBv [] = mkIntNum 0 >>= mkInt2bv 8
@@ -44,9 +44,9 @@ stringToBv (c:cs) = do
-- | Defines the convertion from an expression to AST so that Z3 can assert satisfiability
-- This is used to fold expressions generated by the WLP transformer, so not all valid Java expressions need to be handled
-expAssertAlgebra :: ExpAlgebra (Z3 AST)
+expAssertAlgebra :: ExpAlgebra (TypeEnv -> Z3 AST)
expAssertAlgebra = (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 = case lit of
+ fLit lit _ = case lit of
Int n -> mkInteger n
Word n -> mkInteger n
Float d -> mkRealNum d
@@ -62,127 +62,139 @@ expAssertAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQual
fThisClass = undefined
fInstanceCreation = undefined
fQualInstanceCreation = undefined
- fArrayCreate = undefined
+ fArrayCreate = error "ArrayCreate"
fArrayCreateInit = undefined
- fFieldAccess fieldAccess = case fieldAccess of
+ fFieldAccess fieldAccess _ = case fieldAccess of
PrimaryFieldAccess e id -> case e of
InstanceCreation _ t args _ -> undefined
_ -> undefined
SuperFieldAccess id -> mkStringSymbol (prettyPrint (Name [id])) >>= mkIntVar
ClassFieldAccess (Name name) id -> mkStringSymbol (prettyPrint (Name (name ++ [id]))) >>= mkIntVar
- fMethodInv invocation = case invocation of
+ fMethodInv invocation env = case invocation of
MethodCall (Name [Ident "*length"]) [a, (Lit (Int n))] -> case a of
- ArrayCreate t exps dim -> foldExp expAssertAlgebra (if fromEnum n < length exps then (exps !! fromEnum n) else Lit (Int 0))
+ ArrayCreate t exps dim -> foldExp expAssertAlgebra (if fromEnum n < length exps then (exps !! fromEnum n) else Lit (Int 0)) env
ArrayCreateInit t dim arrayInit -> mkInteger 0
- _ -> error "length of non-array"
+ ExpName name -> do
+ symbol <- mkStringSymbol ("*length(" ++ prettyPrint name ++ ", " ++ show n ++ ")")
+ mkIntVar symbol
+ Cond g a1 a2 -> foldExp expAssertAlgebra (Cond g (MethodInv (MethodCall (Name [Ident "*length"]) [a1, (Lit (Int n))])) (MethodInv (MethodCall (Name [Ident "*length"]) [a2, (Lit (Int n))]))) env
+ _ -> error ("length of non-array: " ++ prettyPrint a)
_ -> error (prettyPrint invocation)
- 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
+ fArrayAccess arrayIndex env = case arrayIndex of
+ ArrayIndex (ArrayCreate t _ _) _ -> foldExp expAssertAlgebra (getInitValue t) env
+ ArrayIndex (ArrayCreateInit t _ _) _ -> foldExp expAssertAlgebra (getInitValue t) env
+ ArrayIndex (ExpName name) i -> do
+ symbol <- mkStringSymbol (prettyPrint name ++ "[" ++ show i ++ "]")
+ case fmap arrayContentType (lookup name env) of
+ Just (PrimType BooleanT) -> mkBoolVar symbol
+ Just (PrimType FloatT) -> mkRealVar symbol
+ Just (PrimType DoubleT) -> mkRealVar symbol
+ _ -> mkIntVar symbol
+ ArrayIndex (Cond g a1 a2) i -> foldExp expAssertAlgebra (Cond g (ArrayAccess (ArrayIndex a1 i)) (ArrayAccess (ArrayIndex a2 i))) env
+ ArrayIndex e _ -> foldExp expAssertAlgebra e env
+ fExpName name env = do
+ symbol <- mkStringSymbol (prettyPrint name)
+ case lookup name env of
+ Just (PrimType BooleanT) -> mkBoolVar symbol
+ Just (PrimType FloatT) -> mkRealVar symbol
+ Just (PrimType DoubleT) -> mkRealVar symbol
+ _ -> mkIntVar symbol
fPostIncrement = undefined
fPostDecrement = undefined
fPreIncrement = undefined
fPreDecrement = undefined
- fPrePlus e = e
- fPreMinus e = do
- ast <- e
- zero <- mkInteger 0
- mkSub [zero, ast]
+ fPrePlus e env = e env
+ fPreMinus e env = do
+ ast <- e env
+ zero <- mkInteger 0
+ mkSub [zero, ast]
fPreBitCompl = undefined
- fPreNot e = e >>= mkNot
+ fPreNot e env = e env >>= mkNot
fCast = undefined
- fBinOp e1 op e2 = case op of
+ fBinOp e1 op e2 env = case op of
Mult -> do
- ast1 <- e1
- ast2 <- e2
+ ast1 <- e1 env
+ ast2 <- e2 env
mkMul [ast1, ast2]
Div -> do
- ast1 <- e1
- ast2 <- e2
+ ast1 <- e1 env
+ ast2 <- e2 env
mkDiv ast1 ast2
Rem -> do
- ast1 <- e1
- ast2 <- e2
+ ast1 <- e1 env
+ ast2 <- e2 env
mkRem ast1 ast2
Add -> do
- ast1 <- e1
- ast2 <- e2
+ ast1 <- e1 env
+ ast2 <- e2 env
mkAdd [ast1, ast2]
Sub -> do
- ast1 <- e1
- ast2 <- e2
+ ast1 <- e1 env
+ ast2 <- e2 env
mkSub [ast1, ast2]
LShift -> do
- ast1 <- e1
- ast2 <- e2
+ ast1 <- e1 env
+ ast2 <- e2 env
mkBvshl ast1 ast2
RShift -> do
- ast1 <- e1
- ast2 <- e2
+ ast1 <- e1 env
+ ast2 <- e2 env
mkBvashr ast1 ast2
RRShift -> do
- ast1 <- e1
- ast2 <- e2
+ ast1 <- e1 env
+ ast2 <- e2 env
mkBvlshr ast1 ast2
LThan -> do
- ast1 <- e1
- ast2 <- e2
+ ast1 <- e1 env
+ ast2 <- e2 env
mkLt ast1 ast2
GThan -> do
- ast1 <- e1
- ast2 <- e2
+ ast1 <- e1 env
+ ast2 <- e2 env
mkGt ast1 ast2
LThanE -> do
- ast1 <- e1
- ast2 <- e2
+ ast1 <- e1 env
+ ast2 <- e2 env
mkLe ast1 ast2
GThanE -> do
- ast1 <- e1
- ast2 <- e2
+ ast1 <- e1 env
+ ast2 <- e2 env
mkGe ast1 ast2
Equal -> do
- ast1 <- e1
- ast2 <- e2
+ ast1 <- e1 env
+ ast2 <- e2 env
mkEq ast1 ast2
NotEq -> do
- ast1 <- e1
- ast2 <- e2
+ ast1 <- e1 env
+ ast2 <- e2 env
eq <- mkEq ast1 ast2
mkNot eq
And-> do
- ast1 <- e1
- ast2 <- e2
+ ast1 <- e1 env
+ ast2 <- e2 env
mkAnd [ast1, ast2]
Or -> do
- ast1 <- e1
- ast2 <- e2
+ ast1 <- e1 env
+ ast2 <- e2 env
mkOr [ast1, ast2]
Xor -> do
- ast1 <- e1
- ast2 <- e2
+ ast1 <- e1 env
+ ast2 <- e2 env
mkXor ast1 ast2
CAnd -> do
- ast1 <- e1
- ast2 <- e2
+ ast1 <- e1 env
+ ast2 <- e2 env
mkAnd [ast1, ast2]
COr -> do
- ast1 <- e1
- ast2 <- e2
+ ast1 <- e1 env
+ ast2 <- e2 env
mkOr [ast1, ast2]
fInstanceOf = undefined
- fCond g e1 e2 = do
- astg <- (g >>= mkNot)
- assert astg
- result <- check
- solverReset
- case result of
- Sat -> e2
- Unsat -> e1
- _ -> error "can't evaluate if-condition"
+ fCond g e1 e2 env = do
+ astg <- g env
+ ast1 <- e1 env
+ ast2 <- e2 env
+ mkIte astg ast1 ast2
fAssign = undefined
fLambda = undefined
fMethodRef = undefined
\ No newline at end of file
diff --git a/WLP.hs b/WLP.hs
index 8ebf692f8dd3900aa3fdbce762c78a0e7dd10add..c84dd05fdc5d4d526b372b263c92ef64e07cc942 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -34,7 +34,7 @@ type Syn = Exp -> Exp -- The wlp transformer
-- Statements that pass control to the next statement have to explicitly combine their wlp function with the accumulated function, as some statements (e.g. break) ignore the accumulated function.
wlpStmtAlgebra :: StmtAlgebra (Inh -> Syn)
wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhancedFor, fEmpty, fExpStmt, fAssert, fSwitch, fDo, fBreak, fContinue, fReturn, fSynchronized, fThrow, fTry, fLabeled) where
- 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.
+ fStmtBlock (Block bs) inh = foldr (\b r -> wlpBlock inh {acc = r} 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}
var = getVar
@@ -60,7 +60,7 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
fThrow e inh = case catch inh of
Nothing -> ((\q -> q &* throwException e)) -- acc is ignored, as the rest of the block is not executed
Just (cs, f) -> (maybe (if f then id else (\q -> q &* throwException e)) (flip fStmtBlock (inh {acc = id, catch = Nothing})) (getCatch (decls inh) (env inh) e cs))
- fTry (Block bs) cs f inh = let r = (fStmtBlock (Block bs) (inh {acc = id, catch = Just (cs, isJust f)})) in (r . maybe (acc inh) (flip fStmtBlock (inh {env = envBlock bs (env inh)})) f) -- The finally-block is always executed
+ fTry (Block bs) cs f inh = let r = (fStmtBlock (Block bs) (inh {acc = id, catch = Just (cs, isJust f)})) in (r . maybe (acc inh) (flip fStmtBlock inh) f) -- The finally-block is always executed
fLabeled _ s = s
-- Helper functions
@@ -71,14 +71,6 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
BlockStmt s -> wlp' inh s
LocalClass _ -> (acc inh)
LocalVars mods t vars -> foldr (\v r -> (wlpDeclAssignment t (inh {acc = r}) v)) (acc inh) vars
-
- -- Adds declarations within a block to a type environment
- 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)) _ _ s)) = foldr (\v env' -> (varName v, t):env') env vars
- f env _ = env
- varName (VarDecl (VarId id) _) = Name [id]
-- wlp of a var declaration that also assigns a value. Declaring without assignment assigns the default value
wlpDeclAssignment :: Type -> Inh -> VarDecl -> Exp -> Exp
@@ -149,7 +141,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))
fClassLit mType inh = (ClassLit mType, (acc inh))
- fThis inh = (fromJust' "fThis" (object inh), (acc inh))
+ fThis inh = (fromJust' "fThis" (object inh), acc inh)
fThisClass name inh = (ThisClass name, (acc inh))
fInstanceCreation typeArgs t args mBody inh = case args of
[ExpName (Name [Ident "#"])] -> (InstanceCreation typeArgs t args mBody, acc inh) -- '#' indicates we already called the constructor method using the correct arguments
@@ -161,7 +153,7 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
fQualInstanceCreation e typeArgs t args mBody inh = error "fQualInstanceCreation"
fArrayCreate t dimLengths dim inh = (ArrayCreate t (map (\e -> fst (e inh)) dimLengths) dim, acc inh)
fArrayCreateInit t dim init inh = error "ArrayCreateInit" -- (ArrayCreateInit t dim init, acc inh)
- fFieldAccess fieldAccess inh = (ExpName (foldFieldAccess inh fieldAccess), (acc inh))
+ fFieldAccess fieldAccess inh = (foldFieldAccess inh fieldAccess, (acc inh))
fMethodInv invocation inh = case invocation of
MethodCall (Name [Ident "*assume"]) [e] -> (false, (if e == false then const true else imp e)) -- *assume is the regular assume function
_ -> if getCallCount (calls inh) (invocationToId invocation) >= nrOfUnroll -- Check the recursion depth
@@ -276,20 +268,23 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
foldLhs inh lhs = case lhs of
FieldLhs (PrimaryFieldAccess e id) -> case foldExp wlpExpAlgebra e inh of
(ExpName name, trans) -> (NameLhs (Name (fromName name ++ [id])), trans)
- _ -> error "foldFieldAccess"
+ _ -> error "foldLhs"
ArrayLhs (ArrayIndex a i) -> let (a', aTrans) = foldExp wlpExpAlgebra a inh
i' = map (\x -> foldExp wlpExpAlgebra x inh) i
in (ArrayLhs (ArrayIndex a' (map fst i')), foldl (\trans (_, iTrans) -> trans . iTrans) aTrans i' . arrayAccessWlp a' (map fst i') inh)
lhs' -> (lhs', id)
- -- Folds the expression part of a fieldaccess and simplifies it to a name
- foldFieldAccess :: Inh -> FieldAccess -> Name
+ -- Folds the expression part of a fieldaccess and simplifies it
+ foldFieldAccess :: Inh -> FieldAccess -> Exp
foldFieldAccess inh fieldAccess = case fieldAccess of
PrimaryFieldAccess e id -> case fst (foldExp wlpExpAlgebra e inh) of
- ExpName name -> Name (fromName name ++ [id])
- x -> error ("foldFieldAccess: " ++ show x ++ show id)
+ ExpName name -> ExpName (Name (fromName name ++ [id]))
+ ArrayAccess (ArrayIndex a i) -> let (a', aTrans) = foldExp wlpExpAlgebra a inh
+ i' = map (\x -> foldExp wlpExpAlgebra x inh) i
+ in MethodInv (MethodCall (Name [Ident "*length"]) [a, (Lit (Int (toEnum (length i'))))])
+ x -> error ("foldFieldAccess: " ++ show x ++ " . " ++ show id)
SuperFieldAccess id -> foldFieldAccess inh (PrimaryFieldAccess (fromJust' "foldFieldAccess" (object inh)) id)
- ClassFieldAccess name id -> Name (fromName name ++ [id])
+ ClassFieldAccess name id -> ExpName (Name (fromName name ++ [id]))
-- Simplified version of substVar, handy to use with introduced variables
@@ -302,7 +297,7 @@ wlp decls = wlpWithEnv decls []
-- | wlp with a given type environment
wlpWithEnv :: [TypeDecl] -> TypeEnv -> Stmt -> Exp -> Exp
-wlpWithEnv decls env = wlp' (Inh id id Nothing env decls [] Nothing Nothing)
+wlpWithEnv decls env = wlp' (Inh id id Nothing env decls [] Nothing (Just (ExpName (Name [Ident "#obj"]))))
-- wlp' lets you specify the inherited attributes
wlp' :: Inh -> Stmt -> Syn