From 17258096d7fc916e101d19aa2393754d5bea8d44 Mon Sep 17 00:00:00 2001
From: ISWB Prasetya <iswbprasetya@iswbs-mbp.cs.uu.nl>
Date: Thu, 31 Aug 2017 15:45:29 +0200
Subject: [PATCH] working on fix on method calls
---
experiments/wermer2/WlpExperiment.hs | 22 +-
src/Javawlp/API.hs | 12 +-
src/Javawlp/Engine/HelperFunctions copy.hs | 311 +++++++++++++++
src/Javawlp/Engine/HelperFunctions.hs | 173 +++++---
src/Javawlp/Engine/WLP copy.hs | 444 +++++++++++++++++++++
src/Javawlp/Engine/WLP.hs | 56 ++-
6 files changed, 928 insertions(+), 90 deletions(-)
create mode 100644 src/Javawlp/Engine/HelperFunctions copy.hs
create mode 100644 src/Javawlp/Engine/WLP copy.hs
diff --git a/experiments/wermer2/WlpExperiment.hs b/experiments/wermer2/WlpExperiment.hs
index 8ba9599..8cfee05 100644
--- a/experiments/wermer2/WlpExperiment.hs
+++ b/experiments/wermer2/WlpExperiment.hs
@@ -7,6 +7,7 @@ import Javawlp.API
import Javawlp.Engine.HelperFunctions
import Javawlp.Engine.Verifier
import Javawlp.Engine.WLP
+import Language.Java.Pretty
import Language.Java.Syntax
import Z3.Monad
@@ -16,6 +17,9 @@ import System.IO.Unsafe
import System.FilePath
import System.Directory
import System.CPUTime
+import Data.IORef
+import Control.DeepSeq
+import Debug.Trace
-- ======================================================================
@@ -42,7 +46,7 @@ main1 subject = do
if classname `elem` has_equivmutants
then do
- check conf1 (classname ++ "_equiv_trivpost") mutantDir2 ["true"]
+ -- check conf1 (classname ++ "_equiv_trivpost") mutantDir2 ["true"]
check conf1 (classname ++ "_equiv_simplepost") mutantDir2 postconditions
-- check conf2 (classname ++ "_equiv_simplepost2") mutantDir2 postconditions
else return ()
@@ -59,11 +63,12 @@ clean = do
-- Each is specified as a tuple: (target-class, method-name, [post-cond1, post-cond2, ... ])
--
subjects = [ ("Triangle", "tritype1", ["returnValue == -1", "returnValue == 0", "returnValue == 1", "returnValue == 2"]) ,
- ("MinsMaxs", "getMinsMaxs", ["(mins[0]==0)" , "(maxs[0]==1)" , "(mins[1]==1)"])
+ ("MinsMaxs", "getMinsMaxs", ["(mins[0]==0)" , "(maxs[0]==1)" , "(mins[1]==1)"]),
+ ("Fibonacci", "fibonacciInteractive", ["f3==0"]) -- f3==0 is actually not a possibele output; but this will kill all major mutants; f3==2 on the otherhand, does not kill any mutant!
]
-- specify which subjects has equivalent mutants to compare against
-has_equivmutants = ["MinsMaxs"]
+has_equivmutants = ["MinsMaxs","Fibonacci"]
-- subjects which are to be included for false-positive-checking experiment
subjectsFor_FP_experiment = [ ]
@@ -83,7 +88,7 @@ tmpDir = "." </> "tmp"
-- standard wlp-configuration
stdWlpConfiguration = WLPConf {
nrOfUnroll=1,
- ignoreLibMethods=False,
+ ignoreLibMethods=True,
ignoreMainMethod =False
}
@@ -125,13 +130,14 @@ rawCheckMutant wlpConfiguration original mutantDir methodName postconds = do
-- this function will be used to compare the resulting wlps
let comparePreC p1 p2 = let
f = PreNot (p1 ==* p2)
- (result,_) = unsafeIsSatisfiable (extendEnv typeEnv1 decls1 mname) decls1 f
+ (result,_) = unsafeIsSatisfiable (extendEnv typeEnv1 decls1 mname) decls1 $ trace ("### " ++ prettyPrint f) f
complexity = exprComplexity f
in
(result,complexity)
- ps1 <- sequence [ wlpMethod wlpConfiguration typeEnv1 decls1 mname q | q <- qs ]
- ps2 <- sequence [ wlpMethod wlpConfiguration typeEnv2 decls2 mname q | q <- qs ]
+ ps1 <- sequence [ wlpMethod wlpConfiguration typeEnv1 decls1 mname q | q <- qs ]
+ ps2 <- sequence [ wlpMethod wlpConfiguration typeEnv2 decls2 mname q | q <- qs ]
+
logWriteLn ("## Checking mutant " ++ mutantPath)
let z_ = zipWith comparePreC ps1 ps2
let z = map fst z_
@@ -141,6 +147,8 @@ rawCheckMutant wlpConfiguration original mutantDir methodName postconds = do
else if all (== Unsat) z then return (Just True,complexity) -- the mutant definitely survives
else return (Nothing,complexity) -- some of the wlps are undecidable
+
+
-- check all mutants of a single subject
rawCheckAllMutants wlpConfiguration original mutantsRootDir methodName postconds = do
mdirs <- getMutantsSubdirs mutantsRootDir
diff --git a/src/Javawlp/API.hs b/src/Javawlp/API.hs
index ccc16b9..314d9ea 100644
--- a/src/Javawlp/API.hs
+++ b/src/Javawlp/API.hs
@@ -13,6 +13,8 @@ import Javawlp.Engine.Types
import Javawlp.Engine.HelperFunctions
import Javawlp.Engine.Verifier
+import Control.DeepSeq
+
-- | Parses a Java source file, and extracts the necessary information from the compilation unit
parseJava :: FilePath -> IO (TypeEnv, [TypeDecl], [Ident])
parseJava s = do
@@ -55,9 +57,12 @@ wlpMethod conf env decls methodName postCondition = do
let methodBody = case getMethod decls methodName of
Just stmt -> stmt
_ -> error "wlpMethod: cannot get the method body."
-
+
+ -- reset the counters for assigning fresh names
+ dummy1 <- resetVarPointer
+ dummy2 <- resetVarMethodInvokesCount
-- Calculate the wlp:
- return $ wlpWithEnv conf decls env' methodBody postCondition
+ dummy1 `deepseq` (length dummy2) `deepseq` return $ wlpWithEnv conf decls env' methodBody postCondition
-- | A variant of wlpMethod where we can specify a list of post-conditions.
-- It returns a list of pairs (p,q) where q is a post-condition and p is the
@@ -94,7 +99,8 @@ wlpMethods_ conf env decls methods_and_postconds
defaultConf :: WLPConf
defaultConf = WLPConf {
nrOfUnroll=1,
- ignoreLibMethods=False,
+ -- ignoreLibMethods=False,
+ ignoreLibMethods=True,
ignoreMainMethod =False
}
diff --git a/src/Javawlp/Engine/HelperFunctions copy.hs b/src/Javawlp/Engine/HelperFunctions copy.hs
new file mode 100644
index 0000000..9f29e24
--- /dev/null
+++ b/src/Javawlp/Engine/HelperFunctions copy.hs
@@ -0,0 +1,311 @@
+-- Copyright (c) 2017 Utrecht University
+-- Author: Koen Wermer
+
+-- Helper functions for the Java data structure
+module Javawlp.Engine.HelperFunctions where
+
+import Javawlp.Engine.Folds
+
+import Language.Java.Syntax
+import Language.Java.Pretty
+import Data.Maybe
+import System.IO.Unsafe
+import Data.IORef
+import Debug.Trace
+
+
+type TypeEnv = [(Name, Type)]
+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 -> PrimType IntT -- For now we assume library variables to be ints error ("can't find type of " ++ prettyPrint (Name idents) ++ "\r\n TypeEnv: " ++ show env)
+
+-- | Gets the type of a field of an object of given type
+getFieldType :: [TypeDecl] -> Type -> Name -> Type
+getFieldType _ t (Name []) = t
+getFieldType _ _ (Name [Ident "length"]) = PrimType IntT
+getFieldType decls (RefType (ClassRefType t)) (Name (f:fs)) = getFieldType decls (getFieldTypeFromClassDecl (getDecl t decls) f) (Name fs)
+ where
+ getFieldTypeFromClassDecl :: ClassDecl -> Ident -> Type
+ getFieldTypeFromClassDecl (ClassDecl _ _ _ _ _ (ClassBody decls)) id = getFieldTypeFromMemberDecls decls id
+
+ getFieldTypeFromMemberDecls :: [Decl] -> Ident -> Type
+ getFieldTypeFromMemberDecls [] _ = error "getFieldTypeFromMemberDecls"
+ getFieldTypeFromMemberDecls (MemberDecl (FieldDecl mods t (VarDecl varId _ : vars)) : decls) id = if getId varId == id then t else getFieldTypeFromMemberDecls (MemberDecl (FieldDecl mods t vars) : decls) id
+ getFieldTypeFromMemberDecls (_ : decls) id = getFieldTypeFromMemberDecls decls id
+
+ -- Gets the class declaration that matches a given type
+ getDecl :: ClassType -> [TypeDecl] -> ClassDecl
+ getDecl t@(ClassType [(ident, typeArgs)]) (x:xs) = case x of
+ ClassTypeDecl decl@(ClassDecl _ ident' _ _ _ _) -> if ident == ident' then decl else getDecl t xs
+ _ -> getDecl t xs
+ getDecl t _ = error ("fieldType: " ++ show t)
+
+-- | Gets the type of the class in which the method is defined
+getMethodClassType :: [TypeDecl] -> Ident -> Type
+getMethodClassType decls id = head $ concatMap (flip getMethodTypeFromClassDecl id) decls
+ where
+ getMethodTypeFromClassDecl :: TypeDecl -> Ident -> [Type]
+ getMethodTypeFromClassDecl (ClassTypeDecl (ClassDecl _ className _ _ _ (ClassBody decls))) id = getMethodTypeFromMemberDecls (RefType (ClassRefType (ClassType [(className , [])]))) decls id
+ getMethodTypeFromClassDecl _ _ = []
+
+ getMethodTypeFromMemberDecls :: Type -> [Decl] -> Ident -> [Type]
+ getMethodTypeFromMemberDecls t [] _ = []
+ getMethodTypeFromMemberDecls t (MemberDecl (MethodDecl _ _ _ id' _ _ _) : decls) id = if id' == id then [t] else getMethodTypeFromMemberDecls t decls id
+ getMethodTypeFromMemberDecls t (_ : decls) id = getMethodTypeFromMemberDecls t decls id
+
+-- | Adds the special variables *obj, returnValue and returnValueVar to a type environment, given the id of the method we're looking at
+extendEnv :: TypeEnv -> [TypeDecl] -> Ident -> TypeEnv
+extendEnv env decls methodId = case getMethodType decls methodId of
+ Nothing -> (Name [Ident "*obj"], getMethodClassType decls methodId) : env
+ Just (RefType _) -> (Name [Ident "returnValue"], returnValueType) : (Name [Ident "returnValueVar"], returnValueType) : (Name [Ident "*obj"], getMethodClassType decls methodId) : env
+ Just t -> (Name [Ident "returnValue"], t) : (Name [Ident "returnValueVar"], t) : (Name [Ident "*obj"], getMethodClassType decls methodId) : env
+
+-- | We introduce a special type for the return value,
+returnValueType :: Type
+returnValueType = RefType (ClassRefType (ClassType [(Ident "ReturnValueType", [])]))
+
+-- | Get's the type of a generated variable
+getReturnVarType :: [TypeDecl] -> String -> Type
+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
+incrCallCount [] id = [(id, 1)]
+incrCallCount ((id', c):xs) id = if id == id' then (id', c + 1) : xs else (id', c) : incrCallCount xs id
+
+
+-- Looks up the call count for a given method
+getCallCount :: CallCount -> Ident -> Int
+getCallCount [] id = 0
+getCallCount ((id', c):xs) id = if id == id' then c else getCallCount xs id
+
+getId :: VarDeclId -> Ident
+getId (VarId id) = id
+getId (VarDeclArray id) = getId id
+
+fromName :: Name -> [Ident]
+fromName (Name name) = name
+
+-- Gets the ident of the method from a name
+getMethodId :: Name -> Ident
+getMethodId = last . fromName
+
+-- Gets the statement(-block) defining a method
+getMethod :: [TypeDecl] -> Ident -> Maybe Stmt
+getMethod classTypeDecls methodId = fmap (\(b, _, _) -> b) (getMethod' classTypeDecls methodId)
+
+-- Gets the return type of a method
+getMethodType :: [TypeDecl] -> Ident -> Maybe Type
+getMethodType classTypeDecls methodId = getMethod' classTypeDecls methodId >>= (\(_, t, _) -> t)
+
+-- Gets the parameter declarations of a method
+getMethodParams :: [TypeDecl] -> Ident -> Maybe [FormalParam]
+getMethodParams classTypeDecls methodId = fmap (\(_, _, params) -> params) (getMethod' classTypeDecls methodId)
+
+-- Finds a method definition. This function assumes all methods are named differently
+getMethod' :: [TypeDecl] -> Ident -> Maybe (Stmt, Maybe Type, [FormalParam])
+getMethod' classTypeDecls methodId = case (concatMap searchClass classTypeDecls) of
+ r:_ -> Just r
+ [] -> Nothing -- Library function call
+ where
+ searchClass (ClassTypeDecl (ClassDecl _ _ _ _ _ (ClassBody decls))) = searchDecls decls
+ searchClass _ = []
+ searchDecls (MemberDecl (MethodDecl _ _ t id params _ (MethodBody (Just b))):_) | methodId == id = [(StmtBlock b, t, params)]
+ searchDecls (MemberDecl (ConstructorDecl _ _ id params _ (ConstructorBody _ b)):_) | methodId == toConstrId id = [(StmtBlock (Block b), Just (RefType (ClassRefType (ClassType [(id, [])]))), params)]
+ searchDecls (_:decls) = searchDecls decls
+ searchDecls [] = []
+ -- Adds a '#' to indicate the id refers to a constructor method
+ toConstrId (Ident s) = Ident ('#' : s)
+
+-- Gets the statement(-block) defining the main method
+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
+ searchClass _ = []
+ searchDecls (MemberDecl (MethodDecl _ _ _ id _ _ _):decls) = id : searchDecls decls
+ searchDecls (_:decls) = searchDecls decls
+ searchDecls [] = []
+
+-- Gets the class declarations
+getDecls :: CompilationUnit -> [TypeDecl]
+getDecls (CompilationUnit _ _ classTypeDecls) = classTypeDecls
+
+-- Checks if the var is introduced. Introduced variable names start with '$' voor return variables of methods and '#' for other variables
+isIntroducedVar :: Name -> Bool
+isIntroducedVar (Name (Ident ('#':_): _)) = True
+isIntroducedVar (Name (Ident ('$':_): _)) = True
+isIntroducedVar _ = False
+
+-- Gets the variable that represents the return value of an invocation of a method;
+-- the variable name is appended with a unique count to distinguish one invocation from another
+getReturnVar :: MethodInvocation -> Ident
+getReturnVar invocation = Ident (mname ++ "___retval" ++ show (getIncrLibMethodCallsCount methodid))
+ where
+ methodid@(Ident mname) = invocationToId invocation
+
+
+-- Gets the method Id from an invocation
+invocationToId :: MethodInvocation -> Ident
+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 getIncrVarPointer)
+
+-- Gets multiple new unique variables
+getVars :: Int -> [Ident]
+getVars 0 = []
+getVars n = Ident ('#' : show getIncrVarPointer) : getVars (n-1)
+
+-- The number of new variables introduced ; also used to assign new variable names
+varPointer :: IORef Int
+varPointer = unsafePerformIO $ newIORef 0
+
+resetVarPointer = do { writeIORef varPointer 0 ; readIORef varPointer }
+
+--- | Gets the current var-pointer and increases the pointer by 1
+getIncrVarPointer :: Int
+getIncrVarPointer = unsafePerformIO $ do
+ p <- readIORef varPointer
+ writeIORef varPointer (p + 1)
+ return p
+
+
+-- to count the number of calls to each library method
+varLibMethodCallsCount :: IORef CallCount
+varLibMethodCallsCount = unsafePerformIO $ newIORef []
+
+resetVarLibMethodCallsCount = do { writeIORef varLibMethodCallsCount [] ; readIORef varLibMethodCallsCount }
+
+getIncrLibMethodCallsCount :: Ident -> Int
+getIncrLibMethodCallsCount methodId = unsafePerformIO $ do
+ callcounts <- readIORef varLibMethodCallsCount
+ let callcounts' = incrCallCount callcounts methodId
+ let k = getCallCount callcounts' methodId
+ writeIORef varLibMethodCallsCount callcounts'
+ return k
+
+
+-- 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)
+
+false :: Exp
+false = Lit (Boolean False)
+
+
+-- Logical operators for expressions:
+(&*) :: Exp -> Exp -> Exp
+e1 &* e2 = BinOp e1 CAnd e2
+
+(|*) :: Exp -> Exp -> Exp
+e1 |* e2 = BinOp e1 COr e2
+
+neg :: Exp -> Exp
+neg = PreNot
+
+imp :: Exp -> Exp -> Exp
+e1 `imp` e2 = neg e1 |* e2
+
+(==*) :: Exp -> Exp -> Exp
+e1 ==* e2 = BinOp e1 Equal e2
+
+(/=*) :: Exp -> Exp -> Exp
+e1 /=* e2 = neg (e1 ==* e2)
+
+-- Gets the value from an array
+arrayAccess :: Exp -> [Exp] -> Exp
+arrayAccess a i = case a of
+ ArrayCreate t exps dim -> getInitValue t
+ ArrayCreateInit t dim arrayInit -> getInitValue t
+ _ -> ArrayAccess (ArrayIndex a i)
+
+-- Accesses fields of fields
+fieldAccess :: Exp -> Name -> FieldAccess
+fieldAccess e (Name [id]) = PrimaryFieldAccess e id
+fieldAccess e (Name (id:ids)) = fieldAccess (FieldAccess (PrimaryFieldAccess e id)) (Name ids)
+fieldAccess _ _ = error "FieldAccess without field name"
+
+-- | Gets the initial value for a given type
+getInitValue :: Type -> Exp
+getInitValue (PrimType t) = case t of
+ BooleanT -> Lit (Boolean False)
+ ByteT -> Lit (Word 0)
+ ShortT -> Lit (Int 0)
+ IntT -> Lit (Int 0)
+ LongT -> Lit (Int 0)
+ CharT -> Lit (Char '\NUL')
+ FloatT -> Lit (Float 0)
+ DoubleT -> Lit (Double 0)
+getInitValue (RefType t) = Lit Null
+
+
+-- counting expressing complexity
+exprComplexity :: Exp -> Int
+exprComplexity e = foldExp expComplexityCountAlgebra e
+
+-- | 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
+expComplexityCountAlgebra :: ExpAlgebra Int
+expComplexityCountAlgebra = (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 _ = 0
+ fClassLit = undefined
+ fThis = undefined
+ fThisClass = undefined
+ fInstanceCreation = undefined
+ fQualInstanceCreation = undefined
+ fArrayCreate = error "ArrayCreate"
+ fArrayCreateInit = undefined
+ fFieldAccess _ = 0
+ fMethodInv _ = 0
+ fArrayAccess _ = 0
+ fExpName _ = 0
+ fPostIncrement = undefined
+ fPostDecrement = undefined
+ fPreIncrement = undefined
+ fPreDecrement = undefined
+ fPrePlus _ = 0
+ fPreMinus _ = 0
+ fPreBitCompl = undefined
+ fPreNot e = e + 1
+ fCast = undefined
+ fBinOp e1 op e2 = case op of
+ And -> e1 + e2 + 1
+ Or -> e1 + e2 + 1
+ Xor -> e1 + e2 + 1
+ CAnd -> e1 + e2 + 1
+ COr -> e1 + e2 + 1
+ _ -> e1 + e2
+
+ fInstanceOf = undefined
+ fCond g e1 e2 = e1 + e2 + g + 1
+ fAssign = undefined
+ fLambda = undefined
+ fMethodRef = undefined
+
+
+
diff --git a/src/Javawlp/Engine/HelperFunctions.hs b/src/Javawlp/Engine/HelperFunctions.hs
index 9b324ff..d88b22b 100644
--- a/src/Javawlp/Engine/HelperFunctions.hs
+++ b/src/Javawlp/Engine/HelperFunctions.hs
@@ -11,7 +11,7 @@ import Language.Java.Pretty
import Data.Maybe
import System.IO.Unsafe
import Data.IORef
-
+import Debug.Trace
type TypeEnv = [(Name, Type)]
@@ -66,9 +66,6 @@ extendEnv env decls methodId = case getMethodType decls methodId of
Just (RefType _) -> (Name [Ident "returnValue"], returnValueType) : (Name [Ident "returnValueVar"], returnValueType) : (Name [Ident "*obj"], getMethodClassType decls methodId) : env
Just t -> (Name [Ident "returnValue"], t) : (Name [Ident "returnValueVar"], t) : (Name [Ident "*obj"], getMethodClassType decls methodId) : env
--- | Creates a string that that represents the return var name of a method call. This name is extended by a number to indicate the depth of the recursive calls
-makeReturnVarName :: Ident -> String
-makeReturnVarName (Ident s) = "$" ++ s ++ "$"
-- | We introduce a special type for the return value,
returnValueType :: Type
@@ -152,9 +149,11 @@ isIntroducedVar (Name (Ident ('#':_): _)) = True
isIntroducedVar (Name (Ident ('$':_): _)) = True
isIntroducedVar _ = False
--- Gets the variable that represents the return value of the method
+-- Gets the variable that represents the return value of an invocation of a method
getReturnVar :: MethodInvocation -> Ident
-getReturnVar invocation = Ident (makeReturnVarName (invocationToId invocation) ++ show (getIncrPointer varPointer))
+getReturnVar invocation = Ident (name ++ "___retval" ++ show (getIncrVarMethodInvokesCount methodid))
+ where
+ methodid@(Ident name) = invocationToId invocation
-- Gets the method Id from an invocation
invocationToId :: MethodInvocation -> Ident
@@ -169,24 +168,42 @@ arrayContentType t = t
-- Gets a new unique variable
getVar :: Ident
-getVar = Ident ('#' : show (getIncrPointer varPointer))
+getVar = Ident ('#' : show (getIncrVarPointer ()))
-- Gets multiple new unique variables
getVars :: Int -> [Ident]
getVars 0 = []
-getVars n = Ident ('#' : show (getIncrPointer varPointer)) : getVars (n-1)
+getVars n = Ident ('#' : show (getIncrVarPointer ())) : getVars (n-1)
--- The number of variables introduced
-varPointer :: IORef Integer
+-- The number of new variables introduced ; also used to assign new variable names
+varPointer :: IORef Int
varPointer = unsafePerformIO $ newIORef 0
---- | Gets the current var pointer and increases the pointer by 1
-getIncrPointer :: IORef Integer -> Integer
-getIncrPointer ref = unsafePerformIO $
- do
- p <- readIORef ref
- writeIORef ref (p + 1)
- return p
+resetVarPointer = do { writeIORef varPointer 0 ; readIORef varPointer }
+
+-- | Gets the current var-pointer and increases the pointer by 1.
+-- Don't drop the dummy () argument; this is to force a re-evaluation of the expression. Otherwise we will
+-- get the same integer every time.
+getIncrVarPointer :: () -> Int
+getIncrVarPointer () = unsafePerformIO $ do
+ p <- readIORef varPointer
+ writeIORef varPointer (p + 1)
+ return p
+
+-- | To keep track of the number of times each method is invoked; also used to assign unique return-value
+-- name to each method invocation.
+varMethodInvokesCount :: IORef CallCount
+varMethodInvokesCount = unsafePerformIO $ newIORef []
+
+resetVarMethodInvokesCount = do { writeIORef varMethodInvokesCount [] ; readIORef varMethodInvokesCount }
+
+getIncrVarMethodInvokesCount :: Ident -> Int
+getIncrVarMethodInvokesCount methodid = unsafePerformIO $ do
+ callcount <- readIORef varMethodInvokesCount
+ let callcount' = incrCallCount callcount methodid
+ let k = getCallCount callcount' methodid
+ writeIORef varMethodInvokesCount callcount'
+ return k
-- Used for debugging
fromJust' :: String -> Maybe a -> a
@@ -250,45 +267,83 @@ getInitValue (RefType t) = Lit Null
-- counting expressing complexity
exprComplexity :: Exp -> Int
exprComplexity e = foldExp expComplexityCountAlgebra e
-
--- | 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
-expComplexityCountAlgebra :: ExpAlgebra Int
-expComplexityCountAlgebra = (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 _ = 0
- fClassLit = undefined
- fThis = undefined
- fThisClass = undefined
- fInstanceCreation = undefined
- fQualInstanceCreation = undefined
- fArrayCreate = error "ArrayCreate"
- fArrayCreateInit = undefined
- fFieldAccess _ = 0
- fMethodInv _ = 0
- fArrayAccess _ = 0
- fExpName _ = 0
- fPostIncrement = undefined
- fPostDecrement = undefined
- fPreIncrement = undefined
- fPreDecrement = undefined
- fPrePlus _ = 0
- fPreMinus _ = 0
- fPreBitCompl = undefined
- fPreNot e = e + 1
- fCast = undefined
- fBinOp e1 op e2 = case op of
- And -> e1 + e2 + 1
- Or -> e1 + e2 + 1
- Xor -> e1 + e2 + 1
- CAnd -> e1 + e2 + 1
- COr -> e1 + e2 + 1
- _ -> e1 + e2
-
- fInstanceOf = undefined
- fCond g e1 e2 = e1 + e2 + g + 1
- fAssign = undefined
- fLambda = undefined
- fMethodRef = undefined
-
-
-
+ where
+ expComplexityCountAlgebra :: ExpAlgebra Int
+ expComplexityCountAlgebra = (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 _ = 0
+ fClassLit = undefined
+ fThis = undefined
+ fThisClass = undefined
+ fInstanceCreation = undefined
+ fQualInstanceCreation = undefined
+ fArrayCreate = error "ArrayCreate"
+ fArrayCreateInit = undefined
+ fFieldAccess _ = 0
+ fMethodInv _ = 0
+ fArrayAccess _ = 0
+ fExpName _ = 0
+ fPostIncrement = undefined
+ fPostDecrement = undefined
+ fPreIncrement = undefined
+ fPreDecrement = undefined
+ fPrePlus _ = 0
+ fPreMinus _ = 0
+ fPreBitCompl = undefined
+ fPreNot e = e + 1
+ fCast = undefined
+ fBinOp e1 op e2 = case op of
+ And -> e1 + e2 + 1
+ Or -> e1 + e2 + 1
+ Xor -> e1 + e2 + 1
+ CAnd -> e1 + e2 + 1
+ COr -> e1 + e2 + 1
+ _ -> e1 + e2
+
+ fInstanceOf = undefined
+ fCond g e1 e2 = e1 + e2 + g + 1
+ fAssign = undefined
+ fLambda = undefined
+ fMethodRef = undefined
+
+{-
+normalizeInvocationNumbers :: Exp -> Exp
+normalizeInvocationNumbers e = normalize e
+ where
+ isCall s =
+
+ normalize e = case e of
+ Lit lit -> fLit lit
+
+ PrePlus e -> fPrePlus (fold e)
+ PreMinus e -> fPreMinus (fold e)
+ PreBitCompl e -> fPreBitCompl (fold e)
+ PreNot e -> fPreNot (fold e)
+ Cast t e -> fCast t (fold e)
+ BinOp e1 op e2 -> fBinOp (fold e1) op (fold e2)
+ InstanceOf e refType -> fInstanceOf (fold e) refType
+ Cond g e1 e2 -> fCond (fold g) (fold e1) (fold e2)
+ Lambda lParams lExp -> fLambda lParams lExp
+
+
+ ClassLit mt -> fClassLit mt
+ This -> fThis
+ ThisClass name -> fThisClass name
+ InstanceCreation typeArgs classType args mBody -> fInstanceCreation typeArgs classType args mBody
+ QualInstanceCreation e typeArgs ident args mBody -> fQualInstanceCreation (fold e) typeArgs ident args mBody
+ ArrayCreate t exps dim -> fArrayCreate t (map fold exps) dim
+ ArrayCreateInit t dim arrayInit -> fArrayCreateInit t dim arrayInit
+ FieldAccess fieldAccess -> fFieldAccess fieldAccess
+ MethodInv invocation -> fMethodInv invocation
+ ArrayAccess i -> fArrayAccess i
+ ExpName name -> fExpName name
+ PostIncrement e -> fPostIncrement (fold e)
+ PostDecrement e -> fPostDecrement (fold e)
+ PreIncrement e -> fPreIncrement (fold e)
+ PreDecrement e -> fPreDecrement (fold e)
+
+
+
+ Assign lhs assOp e -> fAssign lhs assOp (fold e)
+
+ MethodRef className methodName -> fMethodRef className methodName
+ -}
diff --git a/src/Javawlp/Engine/WLP copy.hs b/src/Javawlp/Engine/WLP copy.hs
new file mode 100644
index 0000000..3f8d1b1
--- /dev/null
+++ b/src/Javawlp/Engine/WLP copy.hs
@@ -0,0 +1,444 @@
+-- Copyright (c) 2017 Utrecht University
+-- Author: Koen Wermer
+
+-- Implementing the wlp transformer.
+module Javawlp.Engine.WLP where
+
+import Language.Java.Syntax
+import Language.Java.Lexer
+import Language.Java.Parser
+import Data.Maybe
+import Data.List
+import Debug.Trace
+
+import Javawlp.Engine.Folds
+import Javawlp.Engine.Verifier
+import Javawlp.Engine.Substitute
+import Javawlp.Engine.HelperFunctions
+
+data WLPConf = WLPConf {
+ -- the max. number of times a loop/recursion is unrolled
+ nrOfUnroll :: Int,
+ -- When ignoreLibMethods is true, library calls will simply be ignored (treated as skip).
+ -- When false, we consider library methods but make no assumptions about them (so the WLP will be true)
+ ignoreLibMethods :: Bool,
+ ignoreMainMethod :: Bool
+ }
+
+-- | A type for the inherited attribute
+data Inh = Inh {wlpConfig :: WLPConf, -- Some configuration parameters for the wlp
+ acc :: Exp -> Exp, -- The accumulated transformer of the current block up until the current statement
+ br :: Exp -> Exp, -- The accumulated transformer up until the last loop (this is used when handling break statements etc.)
+ -- Wish: adding this attribute to handle "continue" commands:
+ cont :: Exp -> Exp, -- The accumulated transformer to handle the "continue" jump
+ catch :: [ExceptionTable], -- the hierarchy of catch-finalize blocks to jump, with the first one in the list being the immediate handlers to look up
+ env :: TypeEnv, -- The type environment for typing expressions
+ decls :: [TypeDecl], -- Class declarations
+ reccalls :: CallCount, -- The number of recursive calls per method
+ ret :: Maybe Ident, -- The name of the return variable when handling a method call
+ object :: Maybe Exp -- The object the method is called from when handling a method call
+ }
+
+-- | Representing the handler + finalize sections of a try-catch-block.
+data ExceptionTable = ExceptionTable
+ [Catch] -- the handlers
+ (Maybe Block) -- the finalize code, if any
+ (Exp -> Exp) -- the continuation post-wlp, which is to composed after the whole try-catch block
+
+
+
+
+
+-- | A type synonym for the synthesized attributea
+type Syn = Exp -> Exp -- The wlp transformer
+
+-- | The algebra that defines the wlp transformer for statements
+-- The synthesized attribute is the resulting 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
+
+ -- 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
+
+ fIfThen e s1 = fIfThenElse e s1 acc -- 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
+ in trans . substVar' inh var e' . (\q -> (ExpName (Name [var]) &* s1 inh q) |* (neg (ExpName (Name [var])) &* s2 inh q))
+
+ fWhile e s inh = let (e', trans) = foldExp wlpExpAlgebra e inh{acc = id}
+ var = getVar
+ numberOfUnrolling = nrOfUnroll $ wlpConfig $ inh
+ -- Wish: this seems to be wrong:
+ -- in (\q -> unrollLoopOpt inh{br = const q} numberOfUnrolling e' trans s q)
+ -- Fixing:
+ in (\q -> unrollLoopOpt inh{br = (\q'-> acc inh q)} numberOfUnrolling e' trans s q)
+
+ fBasicFor init me incr s inh = let
+ -- encode the for loop as a while-loop
+ -- loop below is the wlp-transformer over the loop without the initialization part:
+ loop = fWhile (fromMaybeGuard me) -- the guard
+ -- constructing s ; incr.
+ -- However, this looks to be wrong:
+ -- (\inh' -> s (inh'{acc = wlp' inh'{acc = id} (incrToStmt incr)}) )
+ -- Fixing to:
+ (\inh' -> s (inh'{acc = wlp' inh' (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
+ fExpStmt e inh = snd $ foldExp wlpExpAlgebra e inh
+ fAssert e _ inh = let (e', trans) = foldExp wlpExpAlgebra e inh {acc = id}
+ in (trans . (e' &*) . acc 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 = -- 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.
+ let
+ whileTransf = fWhile e s inh
+ in
+ s (inh {acc = whileTransf, br = acc inh, cont = whileTransf })
+
+ fBreak _ inh = br inh -- wlp of the breakpoint. Control is passed to the statement after the loop
+
+ -- Wish: his seems to be wrong
+ -- fContinue _ inh = id -- at a continue statement it's as if the body of the loop is fully executed
+ -- Fixing to:
+ fContinue _ inh = cont inh
+
+ fReturn me inh = case me of
+ Nothing -> id -- Return ignores acc, as it terminates the method
+ 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
+
+ [] -> {- we have no more handlers, so the exception escape -} (\q -> q &* throwException e)
+
+ (ExceptionTable cs f postTransf : therest) ->
+ case getCatch (decls inh) (env inh) e cs of
+ -- no matching handler is found in the immediate exception-table;
+ -- search higher up:
+ Nothing ->
+ let rethrowTransf = fThrow e inh{catch = therest}
+ in
+ -- we will first do the finally section, then rethrow the exception before passing
+ -- up to the higher level handlers
+ case f of
+ Nothing -> rethrowTransf
+ Just finalizer -> -- trace ("\n ## invoking finalizer on MISmatch " ++ show finalizer) $
+ fStmtBlock finalizer inh{acc=rethrowTransf,catch=therest}
+
+ -- a matching handler is found; handle it, compose with finalizer if there is one:
+ Just handler ->
+ let
+ finalizeTransf = case f of
+ Nothing -> postTransf
+ Just finalizer -> -- trace "\n ## invoking finalizer on match " $
+ fStmtBlock finalizer inh{acc=postTransf,catch=therest}
+ in
+ fStmtBlock handler inh{acc=finalizeTransf,catch=therest}
+
+ fTry (Block bs) cs f inh = let
+ excTable = ExceptionTable cs f (acc inh)
+ normalfinalyTranf = case f of
+ Nothing -> acc inh
+ Just b -> fStmtBlock b inh
+ in
+ fStmtBlock (Block bs) inh{acc=normalfinalyTranf, catch = excTable : catch inh}
+
+ fLabeled _ s = s
+
+ -- Helper functions
+
+ -- A block also keeps track of the types of declared variables
+ wlpBlock :: Inh -> BlockStmt -> Syn
+ wlpBlock inh b = case b of
+ BlockStmt s -> wlp' inh s
+ LocalClass _ -> (acc inh)
+ LocalVars mods t vars -> foldr (\v r -> (wlpDeclAssignment t (inh {acc = r}) v)) (acc inh) vars
+
+ -- wlp of a var declaration that also assigns a value. Declaring without assignment assigns the default value
+ wlpDeclAssignment :: Type -> Inh -> VarDecl -> Exp -> Exp
+ wlpDeclAssignment t inh (VarDecl (VarId ident) Nothing) = case t of
+ PrimType _ -> substVar (env inh) (decls inh) (NameLhs (Name [ident])) (getInitValue t) . acc inh
+ -- We don't initialize ref types to null, because we want to keep pointer information
+ RefType _ -> acc inh
+ wlpDeclAssignment t inh (VarDecl (VarId ident) (Just (InitExp e))) = snd (foldExp wlpExpAlgebra (Assign (NameLhs (Name [ident])) EqualA e) inh)
+ wlpDeclAssignment _ _ _ = error "ArrayCreateInit is not supported"
+
+ -- Unrolls a while-loop a finite amount of times
+ unrollLoop :: Inh -> Int -> Exp -> (Exp -> Exp) -> (Inh -> Exp -> Exp) -> Exp -> Exp
+ unrollLoop inh 0 g gTrans _ = let var = getVar
+ -- in gTrans . substVar' inh var g . (neg (ExpName (Name [var])) `imp`) . acc inh
+ in gTrans . substVar' inh var g . (neg (ExpName (Name [var])) &*) . acc inh
+ unrollLoop inh n g gTrans bodyTrans = let
+ var = getVar
+ nextUnrollingTrans = unrollLoop inh (n-1) g gTrans bodyTrans
+ in gTrans
+ . substVar' inh var g
+ . (\q -> (neg (ExpName (Name [var])) &* acc inh q)
+ |*
+ ((ExpName (Name [var])) &* bodyTrans inh{acc = nextUnrollingTrans, cont = nextUnrollingTrans} q))
+
+ -- An optimized version of unroll loop to reduce the size of the wlp
+ unrollLoopOpt :: Inh -> Int -> Exp -> (Exp -> Exp) -> (Inh -> Exp -> Exp) -> Exp -> Exp
+ unrollLoopOpt inh n g gTrans bodyTrans q
+ | gTrans (bodyTrans inh q) == acc inh q = acc inh q -- q is not affected by the loop
+ | otherwise = unrollLoop inh n g gTrans bodyTrans q -- default to the standard version of unroll loop
+
+ -- Converts initialization code of a for loop to a statement
+ initToStmt :: Maybe ForInit -> Stmt
+ initToStmt Nothing = Empty
+ initToStmt (Just (ForInitExps es)) = StmtBlock (Block (map (BlockStmt . ExpStmt) es))
+ initToStmt (Just (ForLocalVars mods t vars)) = StmtBlock (Block [LocalVars mods t vars])
+
+ -- Replaces an absent guard with "True"
+ fromMaybeGuard :: Maybe Exp -> Exp
+ fromMaybeGuard Nothing = true
+ fromMaybeGuard (Just e) = e
+
+ -- Converts increment code of a for loop to a statement
+ incrToStmt :: Maybe [Exp] -> Stmt
+ incrToStmt Nothing = Empty
+ incrToStmt (Just es) = StmtBlock (Block (map (BlockStmt . ExpStmt) es))
+
+ -- Converts a switch into nested if-then-else statements. The switch is assumed to be non-trivial.
+ desugarSwitch :: Exp -> [SwitchBlock] -> (Exp, Stmt, Stmt)
+ desugarSwitch e [SwitchBlock l bs] = case l of
+ SwitchCase e' -> (BinOp e Equal e', StmtBlock (Block (addBreak bs)), Break Nothing)
+ Default -> (true, StmtBlock (Block (addBreak bs)), Empty)
+ where addBreak bs = bs ++ [BlockStmt (Break Nothing)] -- Adds an explicit break statement add the end of a block (used for the final block)
+ desugarSwitch e sbs@(SwitchBlock l bs:sbs') = case l of
+ SwitchCase e' -> (BinOp e Equal e', StmtBlock (switchBlockToBlock sbs), otherCases)
+ Default -> (true, StmtBlock (switchBlockToBlock sbs), otherCases)
+ where otherCases = let (e', s1, s2) = desugarSwitch e sbs' in IfThenElse e' s1 s2
+
+ -- Gets the statements from a switch statement
+ switchBlockToBlock :: [SwitchBlock] -> Block
+ switchBlockToBlock [] = Block []
+ switchBlockToBlock (SwitchBlock l bs:sbs) = case switchBlockToBlock sbs of
+ Block b -> Block (bs ++ b)
+
+throwException :: Exp -> Exp
+throwException e = false
+
+getCatch :: [TypeDecl] -> TypeEnv -> Exp -> [Catch] -> Maybe Block
+getCatch decls env e [] = Nothing
+getCatch decls env e (Catch p b:cs) = if catches decls env p e then Just b else getCatch decls env e cs
+
+-- Checks whether a catch block catches a certain error
+catches :: [TypeDecl] -> TypeEnv -> FormalParam -> Exp -> Bool
+catches decls env (FormalParam _ t _ _) e = t == RefType (ClassRefType (ClassType [(Ident "Exception", [])])) ||
+ case e of
+ ExpName name -> lookupType decls env name == t
+ InstanceCreation _ t' _ _ -> t == RefType (ClassRefType t')
+
+
+-- | The algebra that defines the wlp transformer for expressions with side effects
+-- The first attribute is the expression itself (this is passed to handle substitutions in case of assignments)
+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)
+ 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
+ _ -> -- Create a var, assign a new instance to var, then call the constructor method on var
+ let varId = getReturnVar invocation
+ var = Name [varId]
+ invocation = MethodCall (Name [varId, Ident ("#" ++ getClassName t)]) args
+ in (ExpName var, (substVar (env inh) (decls inh) (NameLhs var) (InstanceCreation typeArgs t [ExpName (Name [Ident "#"])] mBody) . snd ((fMethodInv invocation) inh {acc = id}) . acc inh))
+ 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 = (foldFieldAccess inh fieldAccess, (acc inh))
+ fMethodInv invocation inh = let
+ varId = getReturnVar invocation
+ result_ = ExpName (Name [varId])
+ numberOfUnrolling = nrOfUnroll $ wlpConfig inh
+ in
+ case invocation of
+ -- *assume is a meta-function, handle this first:
+ MethodCall (Name [Ident "*assume"]) [e] -> (result_, (if e == false then const true else imp e))
+
+ _ -> if isLibraryMethod inh invocation
+ -- library method, so we can't unroll:
+ then if ignoreLibMethods $ wlpConfig $ inh
+ then (result_, acc inh) -- we are to ignore lib-functions, so it behaves as a skip
+ else (result_, const true) -- treat lib-function as a miracle
+ -- not a library method, unroll:
+ else if getCallCount (reccalls inh) (invocationToId invocation) >= numberOfUnrolling
+ then {- Recursion limit is reached! Force to avoid analyzing this execution path -} (result_ , const false)
+ else let
+ inh' = inh {acc = id,
+ reccalls = incrCallCount (reccalls inh) (invocationToId invocation),
+ ret = Just varId,
+ object = getObject inh invocation}
+ callWlp = wlp' inh' (inlineMethod inh invocation)
+ in (result_ , (callWlp . acc inh))
+
+ fArrayAccess (ArrayIndex a i) inh = let (a', atrans) = foldExp wlpExpAlgebra a inh {acc = id}
+ i' = map (flip (foldExp wlpExpAlgebra) inh {acc = id}) i
+ in (arrayAccess a' (map fst i'), foldl (.) atrans (map snd i') . arrayAccessWlp a' (map fst i') inh)
+
+ fExpName name inh = (editName inh name, acc inh)
+ -- x++ increments x but evaluates to the original value
+ fPostIncrement e inh = let (e', trans) = e inh in
+ case e' of
+ -- Wish: this is incorrect
+ -- var@(ExpName name) -> (var, substVar (env inh) (decls inh) (NameLhs name) (BinOp var Add (Lit (Int 1))) . trans)
+ -- fix:
+ var@(ExpName name) -> (BinOp var Sub (Lit (Int 1)), substVar (env inh) (decls inh) (NameLhs name) (BinOp var Add (Lit (Int 1))) . trans)
+ exp -> (exp, trans)
+ fPostDecrement e inh = let (e', trans) = e inh in
+ case e' of
+ -- incorrect
+ -- var@(ExpName name) -> (var, substVar (env inh) (decls inh) (NameLhs name) (BinOp var Sub (Lit (Int 1))) . trans)
+ var@(ExpName name) -> (BinOp var Add (Lit (Int 1)), substVar (env inh) (decls inh) (NameLhs name) (BinOp var Sub (Lit (Int 1))) . trans)
+ exp -> (exp, trans)
+ -- ++x increments x and evaluates to the new value of x
+ fPreIncrement e inh = let (e', trans) = e inh in
+ case e' of
+ -- Wish: this is incorrect
+ -- var@(ExpName name) -> (BinOp var Add (Lit (Int 1)), substVar (env inh) (decls inh) (NameLhs name) (BinOp var Add (Lit (Int 1))) . trans)
+ -- fix:
+ var@(ExpName name) -> (var, substVar (env inh) (decls inh) (NameLhs name) (BinOp var Add (Lit (Int 1))) . trans)
+ exp -> (BinOp exp Add (Lit (Int 1)), trans)
+ fPreDecrement e inh = let (e', trans) = e inh in
+ case e' of
+ -- incorrect
+ -- var@(ExpName name) -> (BinOp var Sub (Lit (Int 1)), substVar (env inh) (decls inh) (NameLhs name) (BinOp var Sub (Lit (Int 1))) . trans)
+ var@(ExpName name) -> (var, substVar (env inh) (decls inh) (NameLhs name) (BinOp var Sub (Lit (Int 1))) . trans)
+ exp -> (BinOp exp Sub (Lit (Int 1)), trans)
+ fPrePlus e inh = let (e', trans) = e inh in (e', trans)
+ fPreMinus e inh = let (e', trans) = e inh in (PreMinus e', trans)
+ fPreBitCompl e inh = let (e', trans) = e inh in (PreBitCompl e', trans)
+ fPreNot e inh = let (e', trans) = e inh in (PreNot e', trans)
+ 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}
+ [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}
+ (g', transg) = g inh {acc = id}
+ in (Cond g' e1' e2', (transg . (\q -> (g' &* trans1 q) |* (neg g' &* trans2 q)) . acc inh))
+ fAssign lhs op e inh = let (lhs', lhsTrans) = foldLhs inh {acc = id} lhs
+ rhs' = desugarAssign lhs' op e'
+ (e', trans) = e inh {acc = id}
+ in (rhs', lhsTrans . trans . substVar (env inh) (decls inh) lhs' rhs' . acc inh)
+ fLambda = error "lambda"
+ fMethodRef = error "method reference"
+
+ -- gets the transformer for array access (as array access may throw an error)
+ arrayAccessWlp :: Exp -> [Exp] -> Inh -> Exp -> Exp
+ arrayAccessWlp a i inh q =
+ let
+ accessConstraint = (foldr (\(i, l) e -> e &* (BinOp i LThan l) &* (BinOp i GThanE (Lit (Int 0)))) true (zip i (dimLengths a)))
+ arrayException = InstanceCreation [] (ClassType [(Ident "ArrayIndexOutOfBoundsException", [])]) [] Nothing
+ in
+ case catch inh of
+ [] -> {- no handler, then impose the constraint -} accessConstraint &* acc inh q
+ _ -> (accessConstraint &* acc inh q) |* wlp' inh (Throw arrayException) q
+
+ dimLengths a = case a of
+ ArrayCreate t exps dim -> exps
+ _ -> map (\n -> MethodInv (MethodCall (Name [Ident "*length"]) [a, (Lit (Int n))])) [0..]
+
+ -- Edits a name expression to handle build-in constructs
+ editName :: Inh -> Name -> Exp
+ editName inh (Name name) | last name == Ident "length" = case lookupType (decls inh) (env inh) (Name (take (length name - 1) name)) of -- For arrays we know that "length" refers to the length of the array
+ RefType (ArrayType _) -> MethodInv (MethodCall (Name [Ident "*length"]) [ExpName (Name (take (length name - 1) name)), (Lit (Int 0))])
+
+ _ -> ExpName (Name name)
+ | otherwise = ExpName (Name name)
+
+ isLibraryMethod :: Inh -> MethodInvocation -> Bool
+ isLibraryMethod inh (MethodCall name _) = getMethod (decls inh) (getMethodId name) == Nothing
+ isLibraryMethod inh (PrimaryMethodCall _ _ id _) = getMethod (decls inh) id == Nothing
+
+ -- Inlines a methodcall. Only non-library method should be inlined!
+ -- This creates a variable to store the return value in
+ inlineMethod :: Inh -> MethodInvocation -> Stmt
+ inlineMethod inh invocation = StmtBlock (Block (getParams inh invocation ++ [BlockStmt (getBody inh invocation)])) where
+ -- Gets the body of the method
+ getBody :: Inh -> MethodInvocation -> Stmt
+ getBody inh invocation = fromJust $ getMethod (decls inh) (invocationToId invocation)
+
+ -- Assigns the supplied parameter values to the parameter variables
+ getParams :: Inh -> MethodInvocation -> [BlockStmt]
+ getParams inh (MethodCall name args) = case getMethodParams (decls inh) (getMethodId name) of
+ Nothing -> []
+ Just params -> zipWith assignParam params args
+ getParams inh (PrimaryMethodCall _ _ id args) = case getMethodParams (decls inh) id of
+ Nothing -> []
+ Just params -> zipWith assignParam params args
+ getParams inh _ = undefined
+ -- Creates an assignment statement to a parameter variable
+ assignParam :: FormalParam -> Exp -> BlockStmt
+ assignParam (FormalParam mods t _ varId) e = LocalVars mods t [VarDecl varId (Just (InitExp e))]
+
+ -- 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))))
+ | otherwise = Nothing
+ getObject inh (PrimaryMethodCall e _ _ _) = case e of
+ This -> object inh
+ _ -> Just e
+ getObject inh _ = undefined
+
+ -- Gets the name of the class as a string from the type
+ getClassName :: ClassType -> String
+ getClassName (ClassType xs) = let Ident s = fst (last xs) in s
+
+ -- Gets the return type of a method
+ getType :: Inh -> MethodInvocation -> Maybe Type
+ getType inh invocation = getMethodType (decls inh) (invocationToId invocation)
+
+ -- Folds the expression part of an lhs
+ foldLhs :: Inh -> Lhs -> (Lhs, Syn)
+ 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 "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
+ foldFieldAccess :: Inh -> FieldAccess -> Exp
+ foldFieldAccess inh fieldAccess = case fieldAccess of
+ PrimaryFieldAccess e id -> case fst (foldExp wlpExpAlgebra e inh) of
+ 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 -> ExpName (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 :: WLPConf -> [TypeDecl] -> Stmt -> Exp -> Exp
+wlp config decls = wlpWithEnv config decls []
+
+-- | wlp with a given type environment
+wlpWithEnv :: WLPConf -> [TypeDecl] -> TypeEnv -> Stmt -> Exp -> Exp
+wlpWithEnv config decls env = wlp' (Inh config id id id [] env decls [] (Just (Ident "returnValue")) (Just (ExpName (Name [Ident "targetObj_"]))))
+
+-- wlp' lets you specify the inherited attributes
+wlp' :: Inh -> Stmt -> Syn
+wlp' inh s = foldStmt wlpStmtAlgebra s inh
+
diff --git a/src/Javawlp/Engine/WLP.hs b/src/Javawlp/Engine/WLP.hs
index eb70594..d2c7912 100644
--- a/src/Javawlp/Engine/WLP.hs
+++ b/src/Javawlp/Engine/WLP.hs
@@ -7,6 +7,7 @@ module Javawlp.Engine.WLP where
import Language.Java.Syntax
import Language.Java.Lexer
import Language.Java.Parser
+import Language.Java.Pretty
import Data.Maybe
import Data.List
import Debug.Trace
@@ -34,7 +35,7 @@ data Inh = Inh {wlpConfig :: WLPConf, -- Some configuration parame
catch :: [ExceptionTable], -- the hierarchy of catch-finalize blocks to jump, with the first one in the list being the immediate handlers to look up
env :: TypeEnv, -- The type environment for typing expressions
decls :: [TypeDecl], -- Class declarations
- calls :: CallCount, -- The number of recursive calls per method
+ reccalls :: CallCount, -- The number of recursive calls per method
ret :: Maybe Ident, -- The name of the return variable when handling a method call
object :: Maybe Exp -- The object the method is called from when handling a method call
}
@@ -45,7 +46,9 @@ data ExceptionTable = ExceptionTable
(Maybe Block) -- the finalize code, if any
(Exp -> Exp) -- the continuation post-wlp, which is to composed after the whole try-catch block
-
+
+
+
-- | A type synonym for the synthesized attributea
type Syn = Exp -> Exp -- The wlp transformer
@@ -257,15 +260,30 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
fArrayCreateInit t dim init inh = error "ArrayCreateInit" -- (ArrayCreateInit t dim init, acc inh)
fFieldAccess fieldAccess inh = (foldFieldAccess inh fieldAccess, (acc inh))
fMethodInv invocation inh = let
- numberOfUnrolling = nrOfUnroll $ wlpConfig $ inh
+ varId = getReturnVar invocation
+ result_ = ExpName (Name [varId])
+ numberOfUnrolling = nrOfUnroll $ wlpConfig inh
in
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) >= numberOfUnrolling -- Check the recursion depth
- then (undefined, const true) -- Recursion limit reached: we just assume the post codition will hold
- else let varId = getReturnVar invocation
- callWlp = wlp' (inh {acc = id, calls = incrCallCount (calls inh) (invocationToId invocation), ret = Just varId, object = getObject inh invocation}) (inlineMethod inh invocation)
- in (ExpName (Name [varId]), (callWlp . acc inh))
+ -- *assume is a meta-function, handle this first:
+ MethodCall (Name [Ident "*assume"]) [e] -> (result_, (if e == false then const true else imp e))
+
+ _ -> if isLibraryMethod inh invocation
+ -- library method, so we can't unroll:
+ then if ignoreLibMethods $ wlpConfig $ inh
+ then (result_, acc inh) -- we are to ignore lib-functions, so it behaves as a skip
+ else (result_, const true) -- treat lib-function as a miracle
+ -- not a library method, unroll:
+ else if getCallCount (reccalls inh) (invocationToId invocation) >= numberOfUnrolling
+ then {- Recursion limit is reached! Force to avoid analyzing this execution path -} (result_ , const false)
+ else let
+ inh' = inh {acc = id,
+ reccalls = incrCallCount (reccalls inh) (invocationToId invocation),
+ ret = Just varId,
+ object = getObject inh invocation}
+ callWlp = wlp' inh' (inlineMethod inh invocation)
+ in (result_ , (callWlp . acc inh))
+
fArrayAccess (ArrayIndex a i) inh = let (a', atrans) = foldExp wlpExpAlgebra a inh {acc = id}
i' = map (flip (foldExp wlpExpAlgebra) inh {acc = id}) i
in (arrayAccess a' (map fst i'), foldl (.) atrans (map snd i') . arrayAccessWlp a' (map fst i') inh)
@@ -343,22 +361,18 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
_ -> ExpName (Name name)
| otherwise = ExpName (Name name)
- -- Inlines a methodcall. This creates a variable to store the return value in
+ isLibraryMethod :: Inh -> MethodInvocation -> Bool
+ isLibraryMethod inh (MethodCall name _) = getMethod (decls inh) (getMethodId name) == Nothing
+ isLibraryMethod inh (PrimaryMethodCall _ _ id _) = getMethod (decls inh) id == Nothing
+
+ -- Inlines a methodcall. Only non-library method should be inlined!
+ -- This creates a variable to store the return value in
inlineMethod :: Inh -> MethodInvocation -> Stmt
inlineMethod inh invocation = StmtBlock (Block (getParams inh invocation ++ [BlockStmt (getBody inh invocation)])) where
-- Gets the body of the method
getBody :: Inh -> MethodInvocation -> Stmt
- getBody inh (MethodCall name _) = case getMethod (decls inh) (getMethodId name) of
- Nothing -> if (ignoreLibMethods $ wlpConfig $ inh)
- then Empty
- else ExpStmt $ MethodInv (MethodCall (Name [Ident "*assume"]) [false])
- Just s -> s
- getBody inh (PrimaryMethodCall _ _ id _) = case getMethod (decls inh) id of
- Nothing -> if (ignoreLibMethods $ wlpConfig $ inh)
- then Empty
- else ExpStmt $ MethodInv (MethodCall (Name [Ident "*assume"]) [false])
- Just s -> s
- getBody inh _ = undefined
+ getBody inh invocation = fromJust $ getMethod (decls inh) (invocationToId invocation)
+
-- Assigns the supplied parameter values to the parameter variables
getParams :: Inh -> MethodInvocation -> [BlockStmt]
getParams inh (MethodCall name args) = case getMethodParams (decls inh) (getMethodId name) of
--
GitLab