From 306bc9ee452aab7cc6e6910e4a315286cd3b34c2 Mon Sep 17 00:00:00 2001
From: koen <koenwermer@gmail.com>
Date: Sun, 8 Jan 2017 00:31:47 +0100
Subject: [PATCH] WLP is now calculated for every method seperately, instead of
just for the main method. The code for filling the type environment is now
seperated from the rest of the program.
---
HelperFunctions.hs | 21 ++++--
Main.hs | 27 ++++---
Settings.hs | 2 +-
Tests/2d-arrays1.java | 14 ++--
Tests/arrays1.java | 16 ++--
Tests/methods.java | 10 +--
Types.hs | 79 ++++++++++++++++++++
Verifier.hs | 166 ++++++++++++++++++++++--------------------
WLP.hs | 33 ++++-----
9 files changed, 234 insertions(+), 134 deletions(-)
create mode 100644 Types.hs
diff --git a/HelperFunctions.hs b/HelperFunctions.hs
index fea1187..05c39c0 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 2fe1ca8..5f45bdd 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 0653c92..0e4b16f 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 9841c30..6d1d2ba 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 9f0ef34..fdffebf 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 47b8dfd..661059a 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 0000000..26d984d
--- /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 d86c402..c2406e9 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 8ebf692..c84dd05 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
--
GitLab