module Language.Java.Paragon.TypeCheck.TcStmt where import Language.Java.Paragon.Syntax import Language.Java.Paragon.Pretty import Language.Java.Paragon.TypeCheck.Policy import Language.Java.Paragon.TypeCheck.Monad import Language.Java.Paragon.TypeCheck.Locks import Language.Java.Paragon.TypeCheck.Types import Language.Java.Paragon.TypeCheck.TcEnv -- The relevant things should really import Language.Java.Paragon.TypeCheck.TcState -- be re-exported by .Monad import Language.Java.Paragon.TypeCheck.TcExp import Language.Java.Paragon.TypeCheck.Evaluate --import Control.Monad (liftM) import Control.Applicative ( (<$>) ) ----------------------------------- -- Typechecking Statements -- ----------------------------------- tcStmt :: Stmt () -> Tc r () -- Rule EMPTY tcStmt (Empty _) = return () -- Rule EXPSTMT tcStmt (ExpStmt _ e) = ignore $ tcExp e -- Rule BLOCK tcStmt (StmtBlock _ b) = tcBlock b -- Rule IF tcStmt (IfThenElse _ c s1 s2) = do (tyC, pC) <- tcExp c checkM (liftCont $ tyC <: booleanT) $ "Cannot convert type to boolean" extendBranchPC pC ("branch dependent on condition " ++ prettyPrint c) $ do ignore $ (maybeM (mLocks tyC) (\ls -> applyLockMods ([],ls)) >> tcStmt s1) ||| tcStmt s2 -- Rule IFTHEN tcStmt (IfThen _ c s) = tcStmt (IfThenElse () c s (Empty ())) -- Rule WHILE tcStmt (While _ c sBody) = do s <- getState -- Starting state S (tyC, pC) <- tcExp c check (isBoolConvertible tyC) $ "Cannot convert type to boolean" extendBranchPC pC ("loop over condition " ++ prettyPrint c) $ addBranchPC breakE $ addBranchPC continueE $ do maybeM (mLocks tyC) (\ls -> applyLockMods ([],ls)) -- First iteration of body tcStmt sBody -- Approximate state to the possible ones -- at the start of the loop sCont <- getExnState ExnContinue -- TODO smart constructor maybeM sCont $ mergeWithState mergeWithState s -- S* = S <> Ss <> Ss[exns](continue)[state] deactivateExn ExnContinue -- S** = S*[exns /= continue] -- Second iteration of condition _ <- tcExp c -- This is only to get the (potentially) more difficult constraints maybeM (mLocks tyC) (\ls -> applyLockMods ([],ls)) -- Second iteration of body tcStmt sBody -- Again for the sake of the constraints, and outgoing state -- Fix outgoing state sBreak <- getExnState ExnBreak -- Sb = Ss'[exns](break)[state] maybeM sBreak mergeWithState -- S' = Se' <> Sb deactivateExn ExnBreak -- S'' = S'[exns /= break] -- Rule BASICFOR tcStmt (BasicFor _ mForInit mTest mUp body) = do withInits mForInit $ do s <- getState (tyC, pC) <- maybe (return (booleanT, bottom)) tcExp mTest check (isBoolConvertible tyC) $ "Test in basic for loop must have a bool-convertible type. \n" ++ "Found type: " ++ prettyPrint tyC maybe id (\test -> extendBranchPC pC ("for loop dependent on condition " ++ prettyPrint test)) mTest $ addBranchPC breakE $ addBranchPC continueE $ do maybeM (mLocks tyC) (\ls -> applyLockMods ([],ls)) -- First iteration of body tcStmt body _ <- maybe (return undefined) (mapM tcExp) mUp -- Approximate state to the possible ones -- at the start of the loop sCont <- getExnState ExnContinue -- TODO smart constructor maybeM sCont $ mergeWithState mergeWithState s -- S* = S <> Ss <> Ss[exns](continue)[state] deactivateExn ExnContinue -- S** = S*[exns /= continue] -- Second iteration of condition _ <- maybe (return undefined) tcExp mTest -- This is only to get the (potentially) more difficult constraints maybeM (mLocks tyC) (\ls -> applyLockMods ([],ls)) -- Second iteration of body tcStmt body -- Again for the sake of the constraints, and outgoing state _ <- maybe (return undefined) (mapM tcExp) mUp -- Fix outgoing state sBreak <- getExnState ExnBreak -- Sb = Ss'[exns](break)[state] maybeM sBreak mergeWithState -- S' = Se' <> Sb deactivateExn ExnBreak -- S'' = S'[exns /= break] -- Rule BREAK tcStmt (Break _ Nothing) = do pc <- getCurrentPC breakE throwExn ExnBreak pc -- Rule CONTINUE tcStmt (Continue _ Nothing) = do pc <- getCurrentPC continueE throwExn ExnContinue pc -- Rule RETURNVOID tcStmt (Return _ Nothing) = do (tyR, pR) <- getReturn check (tyR == voidT) $ "Encountered unexpected empty return statement" check (pR == top) $ "Internal error: tcStmt: " ++ "void return with non-top return policy should never happen" pc <- getCurrentPC returnE throwExn ExnReturn pc -- Rule RETURN tcStmt (Return _ (Just e)) = do (tyR, pR) <- getReturn (tyE, pE) <- tcExp e checkM (liftCont $ tyE <: tyR) $ "Returned value has wrong type: " ++ prettyPrint tyE ++ "\n" ++ "Expecting type: " ++ prettyPrint tyR -- Check pE <=[L] pR constraintLS pE pR $ "Returned value has too restrictive policy:\n" ++ "Return expression: " ++ prettyPrint e ++ "\n" ++ " with policy: " ++ prettyPrint pE ++ "\n" ++ "Declared policy bound: " ++ prettyPrint pR -- Check E[branchPC](return) <= pR bpcs <- getBranchPC returnE constraintPC bpcs pR $ \p src -> "Returning from method, visible at policy " ++ prettyPrint pR ++ ", not allowed in " ++ src ++ " with write effect bound " ++ prettyPrint p -- Check exnPC(S) <= pR epc <- getExnPC constraintPC epc pR $ \p src -> "Returning from method, visible at policy " ++ prettyPrint pR ++ ", not allowed in " ++ src ++ " with write effect bound " ++ prettyPrint p throwExn ExnReturn pR -- Rule THROW tcStmt (Throw _ eX) = do (tyX, pX) <- tcExp eX -- TODO: check (tyX <: "Throwable") (rX, wX) <- lookupExn tyX -- Check E[branchPC](X) <= E[exns](X)[write] bpc <- getBranchPC (exnE tyX) constraintPC bpc wX $ \p src -> "Exception with write effect " ++ prettyPrint wX ++ " may not be thrown in " ++ src ++ " with write effect bound " ++ prettyPrint p -- Check exnPC(S) <= E[exns](X)[write] epc <- getExnPC constraintPC epc wX $ \p src -> "Exception with write effect " ++ prettyPrint wX ++ " may not be thrown in " ++ src ++ " with write effect bound " ++ prettyPrint p -- Check pX <=[L] E[exns](X)[read] constraintLS pX rX $ "Thrown value has too restrictive policy:\n" ++ "Expression thrown: " ++ prettyPrint eX ++ "\n" ++ " of type: " ++ prettyPrint tyX ++ "\n" ++ " with policy: " ++ prettyPrint pX ++ "\n" ++ "Declared exception policy: " ++ prettyPrint rX throwExn (ExnType tyX) wX -- Rule TRYCATCH tcStmt (Try _ block [catch] Nothing) = do let Catch _ (FormalParam _ ms t isVar (VarId _ i)) cBlock = catch tyP <- liftCont $ evalSrcType t -- TODO check tyP <: "Throwable" pR <- liftCont $ getReadPolicy ms -- getParamPolicy i ms pW <- newMetaPolVar -- \pi, where \pi is fresh addBranchPC (exnE tyP) $ -- E' = E[branchPC{tyP +-> bottom}, registerExn tyP pR pW $ do -- exns{tyP +-> (pR, \pi)}] tcBlock block extendVarEnv i (VSig tyP pR False (isFinal ms)) $ do -- E* = E[vars{x +-> (tyP, pR)}] msX <- getExnState (ExnType tyP) maybeM msX $ mergeWithState -- S* = St <> St[exns](X)[state] tcBlock cBlock deactivateExn (ExnType tyP) -- Rule TRYFINALLY tcStmt (Try _ block [] (Just finBlock)) = do sS <- getState -- Must store starting state for later tcBlock block -- TODO: we actually merge with "too many" states here -- unfortunate, but conservative mergeActiveExnStates -- S* = St <> <>{ Sx | X <- dom(St[exns]), St[exns](X)[state] = Sx } sStar <- getState useExnState sS -- S** = S*[exns = S[exns]] tcBlock finBlock sF <- getState useExnState sStar -- S' = Sf[exns = S*[exns]] mergeWithState sF -- <> Sf -- Pre-process TRYCATCH/TRYFINALLY tcStmt (Try _ block catches mFin) = do let catchChain = linearise catches mFin block tcStmt catchChain where linearise :: [Catch ()] -> Maybe (Block ()) -> Block () -> Stmt () linearise [] justFin block = Try () block [] justFin linearise [c] Nothing block = Try () block [c] Nothing linearise (c:cs) mFin block = linearise cs mFin $ bl (Try () block [c] Nothing) bl :: Stmt () -> Block () bl = Block () . return . BlockStmt () -- Rule OPEN -- TODO change the list of actor names to a list of expressions (parser, AST, here) tcStmt (Open _ (Lock _ n as)) = do (LSig pL arL) <- lookupLock n -- (_,pL) <- lookupVar n check (length as == arL) $ "Lock " ++ prettyPrint n ++ " expects " ++ show arL ++ " arguments but has been given " ++ show (length as) -- Check pI <=[L] pL psAs <- map snd <$> mapM lookupActorName as mapM_ (\(a,pA) -> constraintLS pA pL $ "Lock " ++ prettyPrint n ++ " with policy " ++ prettyPrint pL ++ " cannot be opened for actor " ++ prettyPrint a ++ " with policy " ++ prettyPrint pA ) (zip as psAs) -- Check E[branchPC](L) <= pL bpc <- getBranchPC (lockE n) constraintPC bpc pL $ \p src -> "Opening lock " ++ prettyPrint n ++ " with policy " ++ prettyPrint pL ++ " not allowed in " ++ src ++ " with write effect bound " ++ prettyPrint p -- Check exnPC(S) <= pL epc <- getExnPC constraintPC epc pL $ \p src -> "Opening lock " ++ prettyPrint n ++ " with policy " ++ prettyPrint pL ++ " not allowed in " ++ src ++ " with write effect bound " ++ prettyPrint p aids <- mapM tcActorName as openLock (TcLock n aids) -- Rule CLOSE tcStmt (Close _ (Lock _ n as)) = do (LSig pL arL) <- lookupLock n -- (_,pL) <- lookupVar n -- LTI arL pL <- lookupLock n check (length as == arL) $ "Lock " ++ prettyPrint n ++ " expects " ++ show arL ++ " arguments but has been given " ++ show (length as) -- Check pI <=[L] pL l <- getCurrentLockState psAs <- map snd <$> mapM lookupActorName as mapM_ (\(arg,argP) -> constraintLS argP pL $ "Lock " ++ prettyPrint n ++ " with policy " ++ prettyPrint pL ++ " cannot be closed for actor " ++ prettyPrint arg ++ " with policy " ++ prettyPrint argP ) (zip as psAs) -- Check E[branchPC](L) <= pL bpc <- getBranchPC (lockE n) constraintPC bpc pL $ \p src -> "Closing lock " ++ prettyPrint n ++ " with policy " ++ prettyPrint pL ++ " not allowed in " ++ src ++ " with write effect bound " ++ prettyPrint p -- Check exnPC(S) <= pL epc <- getExnPC constraintPC epc pL $ \p src -> "Closing lock " ++ prettyPrint n ++ " with policy " ++ prettyPrint pL ++ " not allowed in " ++ src ++ " with write effect bound " ++ prettyPrint p aids <- mapM tcActorName as closeLock (TcLock n aids) -- Rule OPENIN tcStmt (OpenBlock _ (Lock _ n as) block) = do LSig pL arL <- lookupLock n -- (_,pL) <- lookupVar n --debugTc $ "pL: " ++ prettyPrint n ++ ": " ++ show pL check (length as == arL) $ "Lock " ++ prettyPrint n ++ " expects " ++ show arL ++ " arguments but has been given " ++ show (length as) -- Check pI <=[L] pL l <- getCurrentLockState psAs <- map snd <$> mapM lookupActorName as --debugTc $ "psAs: " ++ show psAs mapM_ (\(arg,argP) -> constraintLS argP pL $ "Lock " ++ prettyPrint n ++ " with policy " ++ prettyPrint pL ++ " cannot be opened for actor " ++ prettyPrint arg ++ " with policy " ++ prettyPrint argP ) (zip as psAs) aids <- mapM tcActorName as extendLockEnv [TcLock n aids] $ tcBlock block tcStmt s = fail $ "Unsupported statement: " ++ prettyPrint s withInits :: Maybe (ForInit ()) -> Tc r () -> Tc r () withInits Nothing tca = tca withInits (Just (ForInitExps _ es)) tca = do _ <- mapM tcExp es tca withInits (Just (ForLocalVars _ ms t vds)) tca = do pV <- localVarPol ms tyV <- liftCont $ evalSrcType t tcLocalVars pV tyV (isFinal ms) vds $ tca ---------------------------------------- -- Typechecking Blocks and BlockStmts -- ---------------------------------------- tcBlock :: Block () -> Tc r () tcBlock (Block _ bss) = tcBlockStmts bss tcBlockStmts :: [BlockStmt ()] -> Tc r () -- Rule EMPTYBLOCK tcBlockStmts [] = return () -- Rule BLOCKSTMT tcBlockStmts (BlockStmt _ stmt : bss) = tcStmt stmt >> tcBlockStmts bss -- Rule LOCALVARINIT/LOCALVARDECL tcBlockStmts (LocalVars _ ms t vds : bss) = do pV <- localVarPol ms tyV <- liftCont $ evalSrcType t -- debugTc $ "Array type pre: " ++ prettyPrint t tcLocalVars pV tyV (isFinal ms) vds $ tcBlockStmts bss tcBlockStmts (b:bss) = fail $ "Unsupported block statement: " ++ prettyPrint b tcLocalVars :: TcPolicy -> TcType -> Bool -> [VarDecl ()] -> Tc r () -> Tc r () tcLocalVars _ _ _ [] cont = cont -- Rule LOCALVARDECL tcLocalVars pV tyV fin (VarDecl _ (VarId _ i) Nothing:vds) cont = do tyV' <- if tyV == actorT then actorIdT <$> newActorId i else return tyV extendVarEnv i (VSig tyV' pV False fin) $ do addBranchPC (varE (Name () [i])) $ do tcLocalVars pV tyV fin vds cont -- Rule LOCALVARINIT (Exp) tcLocalVars pV tyV fin (VarDecl _ (VarId _ i) (Just (InitExp _ e)):vds) cont = do (tyE, pE) <- tcExp e checkM (liftCont $ tyE <: tyV) $ "Type mismatch: " ++ prettyPrint tyE ++ " <=> " ++ prettyPrint tyV constraintLS pE pV $ "Cannot assign result of expression " ++ prettyPrint e ++ " with policy " ++ prettyPrint pE ++ " to variable " ++ prettyPrint i ++ " with policy " ++ prettyPrint pV tyV' <- case mActorId tyE of Nothing -> return tyV Just aid -> do newActorIdWith i aid return $ actorIdT aid extendVarEnv i (VSig tyV' pV False fin) $ do addBranchPC (varE (Name () [i])) $ do tcLocalVars pV tyV fin vds cont -- Rule LOCALVARINIT (Array) tcLocalVars pV tyV fin (VarDecl _ (VarId _ i) (Just (InitArray _ arr)):vds) cont = do case mArrayType tyV of Just (tyA, pAs) -> do -- debugTc $ "Array type post: " ++ prettyPrint tyV tcArrayInit tyA pAs arr extendVarEnv i (VSig tyV pV False fin) $ tcLocalVars pV tyV fin vds cont Nothing -> fail $ "Variable " ++ prettyPrint i ++ " of non-array type " ++ prettyPrint tyV ++ " given literal array initializer" localVarPol :: [Modifier ()] -> Tc r TcPolicy localVarPol ms = case [ p | Reads _ p <- ms ] of [] -> return bottom --newMetaPolVar [p] -> liftCont $ evalPolicy p