Skip to content
Snippets Groups Projects
Commit 4f03bd7e authored by koen's avatar koen
Browse files

objects

parent 6bcd1e68
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
HelperFunctions.hs
+ 33
− 17
View file @ 4f03bd7e
......@@ -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)
......
Main.hs
+ 26
− 13
View file @ 4f03bd7e
......@@ -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
Substitute.hs
+ 30
− 13
View file @ 4f03bd7e
......@@ -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
Tests/Test2.java → Tests/objects.java
+ 8
− 8
View file @ 4f03bd7e
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
}
Verifier.hs
+ 21
− 6
View file @ 4f03bd7e
......@@ -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
WLP.hs
+ 64
− 32
View file @ 4f03bd7e
......@@ -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
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment