diff --git a/HelperFunctions.hs b/HelperFunctions.hs
index f694921445a179825be07e026897f0eb3fbff479..dc3c81ee4ff0515d8ff9a3fe29ab44cc807d8dec 100644
--- a/HelperFunctions.hs
+++ b/HelperFunctions.hs
@@ -2,25 +2,41 @@
module HelperFunctions where
import Language.Java.Syntax
-import System.IO
-import System.IO.Unsafe
-import Data.IORef
+import Language.Java.Pretty
+import Data.Maybe
+type TypeEnv = [(Name, Type)]
-heap :: Exp
-heap = FieldAccess (ClassFieldAccess (Name []) (Ident "<heap>"))
-
-heapPointer :: IORef Integer
-heapPointer = unsafePerformIO $ newIORef 0
-
--- | Gets the current heap pointer and increases the pointer by 1
-getIncrPointer :: IORef Integer -> Integer
-getIncrPointer ref = unsafePerformIO $
- do
- p <- readIORef ref
- writeIORef ref (p + 1)
- return p
-
+-- | Retrieves the type from the environment
+lookupType :: [TypeDecl] -> TypeEnv -> Name -> Type
+lookupType decls env (Name idents) = case lookup (Name [head idents]) env of
+ Just t -> getFieldType decls t (Name (tail idents))
+ Nothing -> 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 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 _ _ = error "nested class"
+
+getId :: VarDeclId -> Ident
+getId (VarId id) = id
+getId (VarDeclArray id) = getId id
+
true :: Exp
true = Lit (Boolean True)
diff --git a/Main.hs b/Main.hs
index b46fdc76bfbee7495be4a6a4f8a6875055b4e6d2..0731c735b3dffea608140fcd9d078fce00730aed 100644
--- a/Main.hs
+++ b/Main.hs
@@ -3,13 +3,15 @@ module Main where
import Language.Java.Syntax
import Language.Java.Parser
import Language.Java.Pretty
+import Data.List
import WLP
import Verifier
+import HelperFunctions
-testFile = "try-catch-finally"
+testFile = "objects"
@@ -26,27 +28,38 @@ main = do
Left error -> print error
Right compUnit -> print compUnit --(getStmt compUnit)
- putStrLn "\r\n-----WLP-----"
- case result of
- Left error -> print error
- Right compUnit -> putStrLn . prettyPrint $ wlp (getStmt compUnit) postCond
-
-
- putStrLn "\r\n-----Correctness-----"
+
case result of
Left error -> print error
- Right compUnit -> if unsafeIsTrue (wlp (getStmt compUnit) postCond) then putStrLn "WLP evaluates to true" else (if unsafeIsFalse (wlp (getStmt compUnit) postCond) then putStrLn "WLP evaluates to false" else putStrLn "undecidable")
-
+ Right compUnit -> do
+ putStrLn "\r\n-----WLP-----"
+ let pred = wlpWithEnv (getDecls compUnit) (getStaticVars compUnit) (getStmt 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")
+
+
--- Gets the statement(-block) defining the main method for simple tests
+-- Gets the statement(-block) defining the main method and initializes the heap
getStmt :: CompilationUnit -> Stmt
-getStmt (CompilationUnit _ _ classTypeDecls) = head (concatMap getInit classTypeDecls) where
+getStmt (CompilationUnit _ _ classTypeDecls) = (head (concatMap getInit classTypeDecls)) where
getInit (ClassTypeDecl (ClassDecl _ _ _ _ _ (ClassBody decls))) = getInit' decls
getInit' [] = []
getInit' (MemberDecl (MethodDecl _ _ _ (Ident "main") _ _ (MethodBody (Just b))):_) = [StmtBlock b]
getInit' (_:decls) = getInit' decls
+-- 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)
-- The post-condition (for testing)
postCond :: Exp
-postCond = BinOp (ExpName (Name [Ident "x"])) Equal (Lit (Int 1))
\ No newline at end of file
+postCond = BinOp (ExpName (Name [Ident "x"])) Equal (Lit (Float 2))
\ No newline at end of file
diff --git a/Substitute.hs b/Substitute.hs
index eca9a441b738a69eee5f8a697ec7308cbfaeb696..473b078297f21f21ed8920e0ba9e57977e87a93b 100644
--- a/Substitute.hs
+++ b/Substitute.hs
@@ -7,7 +7,7 @@ import Folds
import HelperFunctions
-substVarExpAlgebra :: ExpAlgebra ((Lhs, Exp) -> Exp)
+substVarExpAlgebra :: ExpAlgebra ((Lhs, Exp, TypeEnv, [TypeDecl]) -> Exp)
substVarExpAlgebra = (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 _ = Lit lit
fClassLit mt _ = ClassLit mt
@@ -17,16 +17,33 @@ substVarExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQu
fQualInstanceCreation e typeArgs ident args mBody inh = QualInstanceCreation (e inh) typeArgs ident args mBody
fArrayCreate t exps dim inh = ArrayCreate t (map ($ inh) exps) dim
fArrayCreateInit t dim arrayInit _ = ArrayCreateInit t dim arrayInit
- fFieldAccess fieldAccess (lhs, rhs) = case lhs of
- FieldLhs fieldAccess' -> case fieldAccess of
- PrimaryFieldAccess e ident -> error "todo: fieldAccess substitution"
- SuperFieldAccess ident -> error "todo: fieldAccess substitution"
- ClassFieldAccess name ident -> error "todo: fieldAccess substitution"
+ fFieldAccess fieldAccess (lhs, rhs, env, decls) = case lhs of
+ FieldLhs fieldAccess' -> case fieldAccess of
+ PrimaryFieldAccess e ident -> error "todo: fieldAccess substitution"
+ SuperFieldAccess ident -> error "todo: fieldAccess substitution"
+ ClassFieldAccess name ident -> error "todo: fieldAccess substitution"
+ _ -> FieldAccess fieldAccess
fMethodInv invocation _ = MethodInv invocation
- fArrayAccess (ArrayIndex a i) (lhs, rhs) = case lhs of
- ArrayLhs (ArrayIndex a' i') -> Cond (foldr (\(i1, i2) e -> e &* (i1 ==* i2)) (a ==* a') (zip i i')) rhs (ArrayAccess (ArrayIndex a i))
- fExpName name (lhs, rhs) = case lhs of
- NameLhs name' -> if name == name' then rhs else ExpName name
+ fArrayAccess (ArrayIndex a i) (lhs, rhs, env, decls) = let a' = substVar env decls lhs rhs a
+ i' = map (substVar env decls lhs rhs) i in
+ case lhs of
+ ArrayLhs (ArrayIndex a'' i'') -> Cond (foldr (\(i1, i2) e -> e &* (i1 ==* i2)) (a' ==* a'') (zip i' i'')) rhs (ArrayAccess (ArrayIndex a' i'))
+ _ -> ArrayAccess (ArrayIndex a' i')
+ fExpName (Name name) (lhs, rhs, env, decls) = case lhs of
+ NameLhs (Name name') -> case lookupType decls env (Name name') of
+ PrimType _ | name' == name -> rhs
+ | otherwise -> ExpName (Name name)
+ RefType t -> let getFields e [] = e
+ getFields e (f : fs) = getFields (FieldAccess (PrimaryFieldAccess e f)) fs
+ in if [head name] == name' then getFields rhs (tail name) else Cond (ExpName (Name [head name]) ==* ExpName (Name name')) (getFields rhs (tail name)) (ExpName (Name name))
+
+
+
+ -- | name' == name -> rhs
+ -- | isPrefixOf name' name -> let getFields e [f] = FieldAccess (PrimaryFieldAccess e f)
+ -- getFields e (f : fs) = getFields (FieldAccess (PrimaryFieldAccess e f)) fs
+ -- in getFields rhs (drop (length name') name)
+ -- | otherwise -> Cond (ExpName (Name [head name]) ==* ExpName (Name [head name'])) rhs (ExpName (Name name))
fPostIncrement e inh = PostIncrement (e inh)
fPostDecrement e inh = PostDecrement (e inh)
fPreIncrement e inh = PreIncrement (e inh)
@@ -39,7 +56,7 @@ substVarExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQu
fBinOp e1 op e2 inh = BinOp (e1 inh) op (e2 inh)
fInstanceOf e refType inh = InstanceOf (e inh) refType
fCond g e1 e2 inh = Cond (g inh) (e1 inh) (e2 inh)
- fAssign lhs assOp e inh = Assign lhs assOp (e inh) -- TODO
+ fAssign lhs assOp e inh = Assign lhs assOp (e inh)
fLambda lParams lExp _ = Lambda lParams lExp
fMethodRef className methodName _ = MethodRef className methodName
@@ -64,5 +81,5 @@ desugarAssign lhs op e = case op of
lhsToExp (ArrayLhs arrayIndex) = undefined
-- | Substitutes all occurences of a specific free variable by an expression
-substVar :: Lhs -> Exp -> Exp -> Exp
-substVar lhs rhs e = foldExp substVarExpAlgebra e (lhs, rhs)
\ No newline at end of file
+substVar :: TypeEnv -> [TypeDecl] -> Lhs -> Exp -> Exp -> Exp
+substVar env decls lhs rhs e = foldExp substVarExpAlgebra e (lhs, rhs, env, decls)
\ No newline at end of file
diff --git a/Tests/Test2.java b/Tests/objects.java
similarity index 65%
rename from Tests/Test2.java
rename to Tests/objects.java
index 5df40d738170146a3ae35579f197386671743a17..ecd594b58d21f5a814934992851dcc586d431c72 100644
--- a/Tests/Test2.java
+++ b/Tests/objects.java
@@ -1,16 +1,16 @@
public class HelloWorld
{
static int c;
- static Circle circle;
+ static Circle circle1, circle2;
public static void main(String[] args)
{
- c = 0;
- int x = 1;
- bool b;
- if(b)
- x = 2;
- // circle = new Circle(1, 1);
+ float x = 1;
+ circle1 = new Circle(2, 2);
+ circle2 = new Circle(2, 2);
+ circle2 = circle1;
+ circle2.center = 3;
+ x = circle1.center;
}
private static void someOtherFunction()
@@ -30,4 +30,4 @@ public class Circle
this.center = center;
this.radius = radius;
}
-}
\ No newline at end of file
+}
diff --git a/Verifier.hs b/Verifier.hs
index 3c1e833d4c27031aab9bd9b8559e029ee7e89d50..ed5aa982a2d1d31f30561ea9582b350b72825e54 100644
--- a/Verifier.hs
+++ b/Verifier.hs
@@ -39,31 +39,39 @@ unsafeIsTrue = unsafePerformIO . evalZ3 . isTrue
unsafeIsFalse :: Exp -> Bool
unsafeIsFalse = unsafePerformIO . evalZ3 . isFalse
+stringToBv :: String -> Z3 AST
+stringToBv [] = mkIntNum 0 >>= mkInt2bv 8
+stringToBv (c:cs) = do
+ c' <- mkIntNum (fromEnum c) >>= mkInt2bv 8
+ cs' <- stringToBv cs
+ mkConcat c' cs'
+
+
-- | 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 = (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
Int n -> mkInteger n
- Word n -> error "word"
+ Word n -> mkInteger n
Float d -> mkRealNum d
Double d -> mkRealNum d
Boolean b -> mkBool b
Char c -> do sort <- mkIntSort
mkInt (fromEnum c) sort
- String s -> error "string"
+ String s -> stringToBv s
Null -> do sort <- mkIntSort
mkInt 0 sort
fClassLit = undefined
fThis = undefined
fThisClass = undefined
- fInstanceCreation = undefined
+ fInstanceCreation _ _ _ _ = mkInteger 2-- TODO
fQualInstanceCreation = undefined
fArrayCreate = undefined
fArrayCreateInit = undefined
- fFieldAccess = undefined
+ fFieldAccess fieldAccess = mkInteger 2-- TODO
fMethodInv = undefined
- fArrayAccess = undefined
+ fArrayAccess _ = mkInteger 2-- TODO
fExpName name = mkStringSymbol (prettyPrint name) >>= mkIntVar
fPostIncrement = undefined
fPostDecrement = undefined
@@ -156,7 +164,14 @@ expAssertAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQual
ast2 <- e2
mkOr [ast1, ast2]
fInstanceOf = undefined
- fCond = undefined
+ fCond g e1 e2 = do
+ astg <- g
+ assert astg
+ result <- check
+ case result of
+ Sat -> e1
+ Unsat -> e2
+ _ -> error "can't evaluate if-condition"
fAssign = undefined
fLambda = undefined
fMethodRef = undefined
\ No newline at end of file
diff --git a/WLP.hs b/WLP.hs
index c4b897108785c783f78cc8b935c0c75c4efc8df5..0344abf049e07ad5ac436617f904ec9365a23ec6 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -25,15 +25,14 @@ data Inh = Inh {acc :: Exp -> Exp, -- The accumulated transformer of the cu
loop :: Exp -> Exp, -- The wlp of the current loop statement not including initialization code. It refers to the loop starting from the loop continuation point.
catch :: Maybe ([Catch], Bool), -- The catches when executing a block in a try statement, and a Bool indicating wether there is a finally-block
env :: TypeEnv, -- The type environment for typing expressions
- decls :: [ClassDecl]} -- Class declarations
+ decls :: [TypeDecl] -- Class declarations
+ }
-- | A type synonym for the synthesized attributea
type Syn = (Exp -> Exp, -- The wlp transformer
TypeEnv) -- The type environment
-type TypeEnv = [(Name, Type)]
-
-- | 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.
@@ -59,7 +58,7 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
fSynchronized _ = fStmtBlock
fThrow e inh = case catch inh of
Nothing -> ((\q -> q &* throwException e), env inh) -- 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), env inh) (flip fStmtBlock (inh {acc = id, catch = Nothing})) (getCatch (env inh) e cs))
+ Just (cs, f) -> (maybe (if f then id else (\q -> q &* throwException e), env inh) (flip fStmtBlock (inh {acc = id, catch = Nothing})) (getCatch (decls inh) (env inh) e cs))
fTry b cs f inh = let (r, env') = (fStmtBlock b (inh {acc = id, catch = Just (cs, isJust f)})) in (r . maybe (acc inh) (fst . flip fStmtBlock (inh {env = env'})) f, env inh) -- The finally-block is always executed
fLabeled _ s = s
@@ -81,8 +80,8 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
-- 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) = substVar (NameLhs (Name [ident])) (getInitValue t) . acc inh
- wlpDeclAssignment t inh (VarDecl (VarId ident) (Just (InitExp e))) = substVar (NameLhs (Name [ident])) e . acc inh
+ wlpDeclAssignment t inh (VarDecl (VarId ident) Nothing) = substVar (env inh) (decls inh) (NameLhs (Name [ident])) (getInitValue t) . acc inh
+ wlpDeclAssignment t inh (VarDecl (VarId ident) (Just (InitExp e))) = substVar (env inh) (decls inh) (NameLhs (Name [ident])) e . acc inh
inv = true -- for simplicity, "True" is used as an invariant for now
@@ -115,16 +114,16 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
throwException :: Exp -> Exp
throwException e = if diffExc then MethodInv (MethodCall (Name [Ident "Exception"]) [e]) else false
- getCatch :: TypeEnv -> Exp -> [Catch] -> Maybe Block
- getCatch env e [] = Nothing
- getCatch env e (Catch p b:cs) = if catches env p e then Just b else getCatch env e cs
+ 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 :: TypeEnv -> FormalParam -> Exp -> Bool
- catches env (FormalParam _ t _ _) e = t == RefType (ClassRefType (ClassType [(Ident "Exception", [])])) ||
- case e of
- ExpName name -> lookupType env name == t
- InstanceCreation _ t' _ _ -> t == RefType (ClassRefType t')
+ 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)
@@ -134,29 +133,29 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
fClassLit = undefined
fThis = undefined
fThisClass = undefined
- fInstanceCreation typeArgs t args mBody inh = let p = getIncrPointer heapPointer in (ArrayAccess (ArrayIndex heap [Lit (Int p)]), (substVar (ArrayLhs (ArrayIndex heap [Lit (Int p)])) (makeObjectArray (decls inh) t args mBody) . acc inh, env inh)) -- TODO: assign default values to fields. basically the WLP of: heap[p] = new object[#fields]
+ fInstanceCreation typeArgs t args mBody inh = (InstanceCreation typeArgs t args mBody, (acc inh, env inh)) --let p = getIncrPointer heapPointer in (ExpName (Name [Ident (show p)]), (substVar (env inh) (decls inh) (ArrayLhs (ArrayIndex heap [Lit (Int p)])) (makeObjectArray (decls inh) t args mBody) . acc inh, env inh)) -- TODO: assign default values to fields. basically the WLP of: heap[p] = new object[#fields]
fQualInstanceCreation e typeArgs t args mBody inh = (QualInstanceCreation (getExp e inh) typeArgs t args mBody, (getTrans e inh, env inh))
fArrayCreate t dimLengths dim inh = (ArrayCreate t (map (flip getExp inh) dimLengths) dim, (acc inh, env inh))
fArrayCreateInit t dim init inh = (ArrayCreateInit t dim init, (acc inh, env inh))
fFieldAccess fieldAccess inh = case fieldAccess of
- PrimaryFieldAccess e (Ident field) -> (ArrayAccess (ArrayIndex e [Lit (String field)]), (acc inh, env inh)) -- Objects are modelled as arrays
- _ -> undefined
+ PrimaryFieldAccess e (Ident field) -> (ArrayAccess (ArrayIndex (getExp (foldExp wlpExpAlgebra e) inh) [Lit (String field)]), (acc inh, env inh)) -- Objects are modelled as arrays
+ _ -> error "fieldaccess"
fMethodInv = error "method call"
fArrayAccess arrayIndex inh = (ArrayAccess arrayIndex, (acc inh, env inh))
fExpName name inh = (ExpName name, (acc inh, env inh))
-- x++ increments x but evaluates to the original value
fPostIncrement e inh = case getExp e inh of
- var@(ExpName name) -> (var, (substVar (NameLhs name) (BinOp var Add (Lit (Int 1))) . acc inh, env inh))
+ var@(ExpName name) -> (var, (substVar (env inh) (decls inh) (NameLhs name) (BinOp var Add (Lit (Int 1))) . acc inh, env inh))
exp -> (exp, (acc inh, env inh))
fPostDecrement e inh = case getExp e inh of
- var@(ExpName name) -> (var, (substVar (NameLhs name) (BinOp var Rem (Lit (Int 1))) . acc inh, env inh))
+ var@(ExpName name) -> (var, (substVar (env inh) (decls inh) (NameLhs name) (BinOp var Rem (Lit (Int 1))) . acc inh, env inh))
exp -> (exp, (acc inh, env inh))
-- ++x increments x and evaluates to the new value of x
fPreIncrement e inh = case getExp e inh of
- var@(ExpName name) -> (BinOp var Add (Lit (Int 1)), (substVar (NameLhs name) (BinOp var Add (Lit (Int 1))) . acc inh, env inh))
+ var@(ExpName name) -> (BinOp var Add (Lit (Int 1)), (substVar (env inh) (decls inh) (NameLhs name) (BinOp var Add (Lit (Int 1))) . acc inh, env inh))
exp -> (BinOp exp Add (Lit (Int 1)), (acc inh, env inh))
fPreDecrement e inh = case getExp e inh of
- var@(ExpName name) -> (BinOp var Rem (Lit (Int 1)), (substVar (NameLhs name) (BinOp var Rem (Lit (Int 1))) . acc inh, env inh))
+ var@(ExpName name) -> (BinOp var Rem (Lit (Int 1)), (substVar (env inh) (decls inh) (NameLhs name) (BinOp var Rem (Lit (Int 1))) . acc inh, env inh))
exp -> (BinOp exp Rem (Lit (Int 1)), (acc inh, env inh))
fPrePlus e inh = (getExp e inh, (acc inh, env inh))
fPreMinus e inh = (PreMinus $ getExp e inh, (acc inh, env inh))
@@ -166,7 +165,8 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
fBinOp e1 op e2 inh = (BinOp (getExp e1 inh) op (getExp e2 inh), (getTrans e1 (inh {acc = getTrans e2 inh}), env inh))
fInstanceOf = error "TODO: instanceOf"
fCond g e1 e2 inh = (Cond (getExp g inh) (getExp e1 inh) (getExp e2 inh), (getTrans g (inh {acc = id}) . (\q -> (getExp g inh &* getTrans e1 (inh {acc = id}) q) |* (neg (getExp g inh) &* getTrans e2 (inh {acc = id}) q)) . acc inh, env inh))
- fAssign lhs op e inh = let rhs = desugarAssign lhs op (getExp e inh) in (rhs, (substVar lhs rhs . getTrans e inh, env inh))
+ fAssign lhs op e inh = let rhs = desugarAssign lhs op (getExp e inh)
+ in (rhs, (substVar (env inh) (decls inh) lhs rhs . getTrans e inh, env inh))
fLambda = error "lambda"
fMethodRef = error "method reference"
@@ -184,22 +184,54 @@ getTrans f inh = let (_, (trans, _)) = f inh in trans
getEnv :: (Inh -> (Exp, Syn)) -> Inh -> TypeEnv
getEnv f inh = let (_, (_, env)) = f inh in env
--- | Retrieves the type from the environment
-lookupType :: TypeEnv -> Name -> Type
-lookupType env name = fromJust (lookup name env)
-
-- | Creates an array that represents an object
-makeObjectArray :: [ClassDecl] -> ClassType -> [Argument] -> (Maybe ClassBody) -> Exp
-makeObjectArray decls t args mBody = undefined
-
+{- makeObjectArray :: [TypeDecl] -> ClassType -> [Argument] -> (Maybe ClassBody) -> Exp
+makeObjectArray decls t = makeObjectArray' (getDecl t decls)
+ where
+ makeObjectArray' :: ClassDecl -> [Argument] -> (Maybe ClassBody) -> Exp
+ makeObjectArray' (ClassDecl _ _ _ _ _ (ClassBody decls)) args mbody = initObj decls
+
+ -- 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 _ _ = error "nested class"
+
+ -- Initializes the member variables (without calling the constructor etc.)
+ initObj :: [Decl] -> Exp
+ initObj decls = foldr (\(ident, e) arr -> Assign (ArrayLhs (ArrayIndex arr [Lit (String ident)])) EqualA e) (ArrayCreate (RefType (ClassRefType (ClassType []))) [Lit (Int (toEnum (length decls)))] 0) (getFields decls)
+
+ getFields :: [Decl] -> [(String, Exp)]
+ getFields = foldr f []
+ where
+ f (MemberDecl (FieldDecl mods t (v : vars))) = f (MemberDecl (FieldDecl mods t vars)) . f' (MemberDecl (FieldDecl mods t [v]))
+ f _ = id
+ f' (MemberDecl (FieldDecl _ t [(VarDecl ident mInit)])) = case mInit of
+ Nothing -> ((getId ident, getInitValue t) :)
+ Just (InitExp e) -> ((getId ident, e) :)
+ Just (InitArray arrayInit) -> ((getId ident, ArrayCreateInit t (getDims ident) arrayInit) :)
+ getId (VarId (Ident id)) = id
+ getId (VarDeclArray id) = getId id
+ getDims (VarId id) = 0
+ getDims (VarDeclArray id) = getDims id + 1 -}
+
-- Initializes the heap
initHeap :: Exp
-initHeap = Assign (NameLhs (Name [Ident "<heap>"])) EqualA (ArrayCreate (RefType undefined) [Lit (Int 10000)] 0)
+initHeap = Assign (NameLhs (Name [Ident "<heap>"])) EqualA (Lit Null) --(ArrayCreate objectType [Lit (Int 10000)] 0)
+
+-- gets a value from the heap
+--getFromHeap :: Name -> Exp
+--getFromHeap (Name idents) = foldl (\e (Ident id) -> ArrayAccess (ArrayIndex e [Lit (String id)])) heap idents
-- | Calculates the weakest liberal pre-condition of a statement and a given post-condition
-wlp :: Stmt -> Exp -> Exp
-wlp = fst . (wlp' (Inh id id id Nothing [] undefined))
+wlp :: [TypeDecl] -> Stmt -> Exp -> Exp
+wlp decls = fst . (wlp' (Inh id id id Nothing [] decls))
+
+-- | wlp with a given type environment
+wlpWithEnv :: [TypeDecl] -> TypeEnv -> Stmt -> Exp -> Exp
+wlpWithEnv decls env = fst . (wlp' (Inh id id id Nothing env decls))
-- wlp' lets you specify the inherited attributes
wlp' :: Inh -> Stmt -> Syn