{-# LANGUAGE TupleSections #-} module Language.Java.Paragon.TypeCheck.TcStmt where import Language.Java.Paragon.Syntax import Language.Java.Paragon.Pretty import Language.Java.Paragon.Interaction 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.TypeMap import Language.Java.Paragon.TypeCheck.TcExp import Language.Java.Paragon.TypeCheck.Evaluate import Control.Monad (unless) import Control.Applicative ( (<$>) ) --import Data.Maybe (fromJust) import Prelude hiding (catch) tcStmtModule :: String tcStmtModule = typeCheckerBase ++ ".TcStmt" ----------------------------------- -- Typechecking Statements -- ----------------------------------- tcStmt :: TypeCheck (TcCodeM r) Stmt -- Rule EMPTY tcStmt (Empty _) = return $ Empty Nothing -- Rule EXPSTMT tcStmt (ExpStmt _ e) = do (_,_,e') <- tcExp e return $ ExpStmt Nothing e' -- Rule BLOCK tcStmt (StmtBlock _ b) = StmtBlock Nothing <$> tcBlock b -- Rule IF tcStmt (IfThenElse _ c s1 s2) = do (tyC, pC, c') <- tcExp c --check (tyC `elem` [booleanT, clsTypeToType . fromJust . box $ BooleanT ()]) check (isBoolConvertible tyC) $ "if-statement requires a condition of type compatible with boolean\n" ++ "Found type: " ++ prettyPrint tyC extendBranchPC pC ("branch dependent on condition " ++ prettyPrint c) $ do (s1', s2') <- (maybeM (mLocks tyC) (\ls -> applyLockMods ([],ls)) >> tcStmt s1) ||| tcStmt s2 return $ IfThenElse Nothing c' s1' s2' -- Rule IFTHEN tcStmt (IfThen _ c s) = do IfThenElse no c' s' _ <- tcStmt (IfThenElse () c s (Empty ())) return (IfThen no c' s') -- Rule WHILE tcStmt (While _ c sBody) = do s <- getState -- Starting state S (tyC, pC, c') <- 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 sBody' <- 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] return $ While Nothing c' sBody' -- Rule BASICFOR tcStmt (BasicFor _ mForInit mTest mUp body) = do (mForInit', forf) <- withInits mForInit $ do s <- getState (tyC, pC, mTest') <- case mTest of Nothing -> return (booleanT, bottom, Nothing) Just test -> do (ty, p, test') <- tcExp test return (ty, p, Just test') 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 body' <- tcStmt body mUp' <- case mUp of Nothing -> return Nothing Just up -> do (_,_,up') <- unzip3 <$> mapM tcExp up return $ Just up' -- 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] return $ \mForInit' -> BasicFor Nothing mForInit' mTest' mUp' body' return $ forf mForInit' -- Rule BREAK tcStmt (Break _ Nothing) = do pc <- getCurrentPC breakE throwExn ExnBreak pc return $ Break Nothing Nothing -- Rule CONTINUE tcStmt (Continue _ Nothing) = do pc <- getCurrentPC continueE throwExn ExnContinue pc return $ Continue Nothing Nothing -- 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 return $ Return Nothing Nothing -- Rule RETURN tcStmt (Return _ (Just e)) = do (tyR, pR) <- getReturn (tyE, pE, e') <- tcExp e checkM (tyR =<: tyE) $ "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 return $ Return Nothing (Just e') -- Rule THROW tcStmt (Throw _ eX) = do (tyX, pX, eX') <- 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 return $ Throw Nothing eX' -- Rule TRYCATCH tcStmt (Try _ block [catch] Nothing) = do let Catch _ (FormalParam _ ms t False (VarId _ i)) cBlock = catch tyP <- liftTcDeclM $ evalSrcType t -- TODO check tyP <: "Throwable" pR <- liftTcDeclM $ 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)}] block' <- tcBlock block extendVarEnv i (VSig tyP pR True False (isFinal ms)) $ do -- E* = E[vars{x +-> (tyP, pR)}] msX <- getExnState (ExnType tyP) maybeM msX $ mergeWithState -- S* = St <> St[exns](X)[state] cBlock' <- tcBlock cBlock deactivateExn (ExnType tyP) let catch' = Catch Nothing (FormalParam Nothing (map notAppl ms) (notAppl t) False (VarId Nothing (notAppl i))) cBlock' return $ Try Nothing block' [catch'] Nothing -- Rule TRYFINALLY tcStmt (Try _ block [] (Just finBlock)) = do sS <- getState -- Must store starting state for later block' <- 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]] finBlock' <- tcBlock finBlock sF <- getState useExnState sStar -- S' = Sf[exns = S*[exns]] mergeWithState sF -- <> Sf return $ Try Nothing block' [] (Just finBlock') -- Pre-process TRYCATCH/TRYFINALLY tcStmt (Try _ blk catches mFinally) = do let catchChain = linearise catches mFinally blk 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 os@(Open _ (Lock _ n@(Name _ nt mPre i) as)) = do unless (nt == LName) $ panic (tcStmtModule ++ ".tcStmt:Open") $ "Unexpected name: " ++ show n LSig pL arL _ <- lookupLock mPre i -- (_,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) return $ notAppl os -- Rule CLOSE tcStmt cs@(Close _ (Lock _ n@(Name _ nt mPre i) as)) = do unless (nt == LName) $ panic (tcStmtModule ++ ".tcStmt:Close") $ "Unexpected name: " ++ show n LSig pL arL _ <- lookupLock mPre i -- (_,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 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) return $ notAppl cs -- Rule OPENIN tcStmt (OpenBlock _ l@(Lock _ n@(Name _ nt mPre i) as) block) = do unless (nt == LName) $ panic (tcStmtModule ++ ".tcStmt:OpenBlock") $ "Unexpected name: " ++ show n LSig pL arL _ <- lookupLock mPre i -- (_,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 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] $ OpenBlock Nothing (notAppl l) <$> tcBlock block tcStmt s = fail $ "Unsupported statement: " ++ prettyPrint s withInits :: Maybe (ForInit ()) -> TcCodeM r a -> TcCodeM r (Maybe (ForInit T), a) withInits Nothing tca = (Nothing,) <$> tca withInits (Just (ForInitExps _ es)) tca = do (_,_,es') <- unzip3 <$> mapM tcExp es (Just $ ForInitExps Nothing es',) <$> tca withInits (Just (ForLocalVars _ ms t vds)) tca = do pV <- localVarPol ms tyV <- liftTcDeclM $ evalSrcType t (vds', a) <- tcLocalVars pV tyV (isFinal ms) vds [] $ tca return $ (Just $ ForLocalVars Nothing (map notAppl ms) (notAppl t) vds', a) ---------------------------------------- -- Typechecking Blocks and BlockStmts -- ---------------------------------------- tcBlock :: TypeCheck (TcCodeM r) Block tcBlock (Block _ bss) = Block Nothing <$> tcBlockStmts bss tcBlockStmts :: [BlockStmt ()] -> TcCodeM r [BlockStmt T] -- Rule EMPTYBLOCK tcBlockStmts [] = return [] -- Rule BLOCKSTMT tcBlockStmts (BlockStmt _ stmt : bss) = do stmt' <- tcStmt stmt bss' <- tcBlockStmts bss return (BlockStmt Nothing stmt':bss') -- Rule LOCALVARINIT/LOCALVARDECL tcBlockStmts (LocalVars _ ms t vds : bss) = do pV <- localVarPol ms tyV <- liftTcDeclM $ evalSrcType t -- debugTc $ "Array type pre: " ++ prettyPrint t (vds', bss') <- tcLocalVars pV tyV (isFinal ms) vds [] $ tcBlockStmts bss return (LocalVars Nothing (map notAppl ms) (notAppl t) vds' : bss') tcBlockStmts (b:_bss) = fail $ "Unsupported block statement: " ++ prettyPrint b tcLocalVars :: ActorPolicy -> TcType -> Bool -> [VarDecl ()] -> [VarDecl T] -> TcCodeM r a -> TcCodeM r ([VarDecl T], a) tcLocalVars _ _ _ [] acc cont = cont >>= \a -> return (reverse acc, a) -- Rule LOCALVARDECL tcLocalVars pV tyV fin (vd@(VarDecl _ (VarId _ i) Nothing):vds) acc cont = do tyV' <- if tyV == actorT then actorIdT <$> newActorId i else return tyV extendVarEnv i (VSig tyV' pV False False fin) $ do addBranchPC (varE (mkSimpleName EName i)) $ do tcLocalVars pV tyV fin vds (notAppl vd : acc) cont -- Rule LOCALVARINIT (Exp) tcLocalVars pV tyV fin (VarDecl _ (VarId _ i) (Just (InitExp _ e)):vds) acc cont = do (tyE, pE, e') <- tcExp e checkM (tyV =<: tyE) $ "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 False fin) $ do addBranchPC (varE (mkSimpleName EName i)) $ do let vd = VarDecl Nothing (VarId Nothing $ notAppl i) (Just (InitExp Nothing e')) tcLocalVars pV tyV fin vds (vd:acc) cont -- Rule LOCALVARINIT (Array) tcLocalVars pV tyV fin (VarDecl _ (VarId _ i) (Just (InitArray _ arr)):vds) acc cont = do case mArrayType tyV of Just (tyA, pAs) -> do -- debugTc $ "Array type post: " ++ prettyPrint tyV arr' <- tcArrayInit tyA pAs arr extendVarEnv i (VSig tyV pV False False fin) $ do let vd = VarDecl Nothing (VarId Nothing $ notAppl i) (Just (InitArray Nothing arr')) tcLocalVars pV tyV fin vds (vd:acc) cont Nothing -> fail $ "Variable " ++ prettyPrint i ++ " of non-array type " ++ prettyPrint tyV ++ " given literal array initializer" tcLocalVars _ _ _ (vd:_) _ _ = fail $ "Deprecated array syntax not supported: " ++ prettyPrint vd localVarPol :: [Modifier ()] -> TcCodeM r ActorPolicy localVarPol ms = case [ p | Reads _ p <- ms ] of [] -> newMetaPolVar --return bottom [p] -> liftTcDeclM $ evalPolicy p _ -> fail $ "Only one read policy allowed on local variable" --------------------------------------------------- -- Typechecking Explicit Constructor Invocations -- --------------------------------------------------- tcEci :: TypeCheck (TcCodeM r) ExplConstrInv tcEci eci = do (tyT, nwtas, as, con) <- case eci of ThisInvoke _ nwtas as -> (,nwtas,as,ThisInvoke) <$> getThisType SuperInvoke _ nwtas as -> (,nwtas,as,SuperInvoke) <$> getSuperType _ -> fail $ "PrimarySuperInvoke not yet supported: " ++ prettyPrint eci (_,_,as') <- tcCreate tyT (map (ActualArg ()) nwtas) as return $ con Nothing (map notAppl nwtas) as'