module Language.Java.Paragon.TypeCheck.TcExp where import Language.Java.Paragon.Syntax import Language.Java.Paragon.Pretty import Language.Java.Paragon.TypeCheck.Policy import Language.Java.Paragon.TypeCheck.Actors import Language.Java.Paragon.TypeCheck.Locks import Language.Java.Paragon.TypeCheck.Monad 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 Data.List ( (\\) ) import Data.Maybe (fromJust) import Control.Applicative ( (<$>) ) import Control.Monad ( (=<<) ) import Control.Arrow ( first ) import qualified Data.Map as Map ----------------------------------- -- Types of literal values -- ----------------------------------- litType :: Literal () -> TcType litType (Int _ _) = intT litType (Word _ _) = longT litType (Float _ _) = floatT litType (Double _ _) = doubleT litType (Boolean _ _) = booleanT litType (Char _ _) = charT litType (String _ _) = stringT litType (Null _ ) = nullT --litType l = error $ "litType: " ++ show l ----------------------------------- -- Checking expressions -- ----------------------------------- debugTc str = liftCont $ liftIO $ putStrLn $ "DEBUG: Tc: " ++ str tcExp :: Exp () -> Tc r (TcType, TcPolicy) -- Rule PAREN tcExp (Paren _ e) = tcExp e -- Rule LIT tcExp (Lit _ l) = return (litType l, bottom) -- Rule THIS tcExp (This _) = do ty <- getThisType --debugTc $ "getThisType: " ++ show ty return (ty, bottom) -- Rule BINOP tcExp (BinOp _ e1 op e2) = do (ty1, p1) <- tcExp e1 (ty2, p2) <- tcExp e2 tyRes <- opType op ty1 ty2 return (tyRes, p1 `join` p2) -- Rule VAR/FIELD tcExp (ExpName _ n) = do --debugTc $ "tcExp ExpName: " ++ show n -- lookupVar handles all the complexity of -- finding the correct actor id, if applicable (ty1,pol) <- lookupVar n ty <- case ty1 of TcPrimT (PolicyT _) -> policyPolT <$> getPolicy n TcLockT [] -> return $ lockT [TcLock n []] TcPrimT (ActorT _) -> actorIdT <$> getActorId n _ -> return ty1 --debugTc $ show (ty,pol) return (ty, pol) -- Rule VARASS/FIELDASS tcExp (Assign _ lhs op rhs) = do (tyV, pV, mtyO, mpO, mEnt, mN) <- case lhs of NameLhs _ n -> do let (mo,f) = splitName n -- TODO: This is bogus case mo of Nothing -> do -- VARASS (tyV, pV) <- lookupVar f return (tyV, pV, Nothing, Nothing, Just (varE n), Just n) Just o -> do -- FIELDASS (tyO,pO) <- lookupVar o let (Name _ [i]) = f (VSig tyF pF _ _) <- lookupFieldT tyO i return (tyF, pF, Just tyO, Just pO, Just (varE n), Just n) FieldLhs _ (PrimaryFieldAccess _ e fi) -> do (tyE, pE) <- tcExp e (VSig tyF pF _ _) <- lookupFieldT tyE fi let eEnt = case e of This _ -> Just $ thisFE fi _ -> Nothing return (tyF, pF, Just tyE, Just pE, eEnt, Nothing) ArrayLhs _ (ArrayIndex _ arrE iE) -> do (tyA, pA) <- tcExp arrE case tyA of TcRefT (TcArrayT tyElem pElem) -> do (tyI, pI) <- tcExp iE check (isIntConvertible tyI) $ "Non-integral expression of type " ++ prettyPrint tyI ++ " used as array index expression" constraintLS pI pA return (tyElem, pElem, Just tyA, Just pA, Nothing, Nothing) _ -> fail $ "Cannot index non-array expression " ++ prettyPrint arrE ++ " of type " ++ prettyPrint tyA _ -> fail $ "Lhs not supported: " ++ prettyPrint lhs (tyRhs, pRhs) <- tcExp rhs -- Check all the necessary constraints: checkM (liftCont $ tyRhs <: tyV) $ "Type mismatch: " ++ prettyPrint tyRhs ++ " <=> " ++ prettyPrint tyV -- Check: E[branchPC](n) <= pV bpc <- maybe getBranchPC_ getBranchPC mEnt -- debugTc $ "BPC: " ++ prettyPrint bpc constraint_ bpc pV -- Check: exnPC(S) <= pV epc <- getExnPC constraint_ epc pV -- Check: pRhs <= pV modulo L constraintLS pRhs pV -- Check: pO <= pV, if pO exists maybeM mpO (\pO -> constraint_ pO pV) -- Update actor tracker if applicable maybeM (mActorId tyRhs) $ \aid -> do maybeM mtyO $ \tyO -> scrambleActors (Just tyO) maybeM mN $ \n -> setActorId n aid return (tyV, pV) -- Rule CALL tcExp (MethodInv _ mi) = tcMethodInv mi -- Rule NEW tcExp e@(InstanceCreation _ tas ct args mBody) = do -- debugTc $ "tcExp: " ++ show e tyT <- liftCont $ evalSrcClsType ct -- DEBUG --debugTc $ "Type: " ++ show tyT --tm <- liftCont getTypeMap --let tyTm = lookupTypeOfT (clsTypeToType tyT) tm --debugTc $ "TypeMap: " ++ show (Map.keys $ constrs tyTm) -- END DEBUG (tysArgs, psArgs) <- unzip <$> mapM tcExp args (tps,genCti) <- lookupConstr tyT tysArgs tArgs <- liftCont $ mapM evalSrcTypeArg tas -- tm <- liftCont getTypeMap let cti = instantiate (zip tps tArgs) genCti let (CSig psPars pW lExp lMods exns) = cti -- Check lockstates l <- getCurrentLockState check (null (lExp \\ l)) $ "Lockstate too weak" -- Check argument constraints mapM_ (uncurry (constraint l)) (zip psArgs psPars) -- Check E[branchPC](*) <= pW bpc <- getBranchPC_ constraint_ bpc pW -- Check exnPC(S) <= pW epc <- getExnPC constraint_ epc pW -- Check Exns(X)[write] <= E[exns](X)[write] AND -- Check Exns(X)[read] >= E[exns](X)[read] mapM (uncurry exnConsistent) exns -- Fix outgoing state let exns' = map (first ExnType) exns activateExns exns' -- ==> S' = Sn[exns{X +-> (Sx, exns(X)[write])}] applyLockMods lMods -- ==> S'' = S'[lockMods ||>>= lMods, scrambleActors Nothing -- ==> actors scrambled] return (clsTypeToType tyT, bottom) -- Rule COND tcExp (Cond _ c e1 e2) = do (tyC, pC) <- tcExp c checkM (liftCont $ tyC <: booleanT) $ "Cannot convert type to boolean" extendBranchPC pC $ do ((ty1, p1), (ty2, p2)) <- (maybeM (mLocks tyC) (\ls -> applyLockMods ([], ls)) >> tcExp e1) ||| tcExp e2 check (ty1 == ty2) $ "Types of branches don't match" return (ty1, pC `join` p1 `join` p2) tcExp (PolicyExp _ pl) = do pRep <- tcPolicyExp pl return (policyPolT pRep, bottom) tcExp (PostIncrement _ e) = do (tyE, pE) <- tcExp e check (isNumConvertible tyE) $ "Post-increment operator used at non-numeric type " ++ prettyPrint tyE return (tyE, pE) tcExp (PostDecrement _ e) = do (tyE, pE) <- tcExp e check (isNumConvertible tyE) $ "Post-decrement operator used at non-numeric type " ++ prettyPrint tyE return (tyE, pE) tcExp (PreIncrement _ e) = do (tyE, pE) <- tcExp e check (isNumConvertible tyE) $ "Pre-increment operator used at non-numeric type " ++ prettyPrint tyE return (tyE, pE) tcExp (PreDecrement _ e) = do (tyE, pE) <- tcExp e check (isNumConvertible tyE) $ "Pre-decrement operator used at non-numeric type " ++ prettyPrint tyE return (tyE, pE) -- Unary promotion prefix operator -- Rule PREP tcExp (PrePlus _ e) = do (tyE, pE) <- tcExp e check (isNumConvertible tyE) $ "Pre-plus operator used at non-numeric type " ++ prettyPrint tyE return (unaryNumPromote_ tyE, pE) tcExp (PreMinus _ e) = do (tyE, pE) <- tcExp e check (isNumConvertible tyE) $ "Pre-minus operator used at non-numeric type " ++ prettyPrint tyE return (unaryNumPromote_ tyE, pE) tcExp (PreBitCompl _ e) = do (tyE, pE) <- tcExp e check (isIntConvertible tyE) $ "Pre-complement bit operator used at non-integral type " ++ prettyPrint tyE return (unaryNumPromote_ tyE, pE) tcExp (PreNot _ e) = do (tyE, pE) <- tcExp e check (isBoolConvertible tyE) $ "Pre-complement boolean operator used at non-boolean type " ++ prettyPrint tyE return (booleanT, pE) tcExp (Cast _ t e) = do (tyE, pE) <- tcExp e tyC <- liftCont $ evalSrcType t checkM (liftCont $ tyE <: tyC) $ "Wrong type at cast" return (tyC, pE) tcExp (FieldAccess _ fa) = tcFieldAccess fa -- Arrays tcExp (ArrayCreate _ bt dimEsPs dimImplPs) = do baseTy <- liftCont $ evalSrcType bt -- Check the types and policies of all dimension expressions check (not $ null dimEsPs) $ "Array creation must have at least one dimension expression, or an explicit initializer" let ((dimE1,mDimP1):dimEsPsRest) = dimEsPs -- at least one exists, checked above -- The first dimexpr will determine the policy -- of the whole array creation expression (ty1, pol1) <- tcExp dimE1 -- Dimexprs must have integral-convertible types check (isIntConvertible ty1) $ nonIntErr ty1 -- Check that the remaining dimexprs each conform to -- the policy given at the level outside it polEDims <- checkDimExprs [] dimEsPsRest =<< evalMaybePol mDimP1 -- Evaluate given policies for implicit dimensions polIDims <- mapM evalMaybePol dimImplPs -- Return the array type, and the policy of the outermost dimexpr return (mkArrayType baseTy (polEDims ++ polIDims), pol1) where checkDimExprs :: [TcPolicy] -- Accumulated policies of earlier dimensions -> [(Exp (), Maybe (Policy ()))] -- Remaining dimexprs/pols -> TcPolicy -- Policy of previous dimension -> Tc r [TcPolicy] checkDimExprs acc [] pPrev = return $ reverse (pPrev:acc) checkDimExprs acc ((e,mp):emps) pPrev = do (tyE,pE) <- tcExp e check (isIntConvertible tyE) $ nonIntErr tyE -- Each dimexpr must satisfy the policy of the outer dim constraintLS pE pPrev pNext <- evalMaybePol mp checkDimExprs (pPrev:acc) emps pNext nonIntErr :: TcType -> String nonIntErr ty = "Non-integral expression of type " ++ prettyPrint ty ++ " used as dimension expression in array creation" tcExp (ArrayCreateInit _ bt dimImplPs arrInit) = do baseTy <- liftCont $ evalSrcType bt -- Evaluate given policies for implicit (all) dimensions dimPols <- mapM evalMaybePol dimImplPs -- Check that the initializer has the right type and policies -- of subexpressions tcArrayInit baseTy dimPols arrInit -- Return the specified array type -- Literal array initializers have known length, -- so their apparent policy is bottom return (mkArrayType baseTy dimPols, bottom) tcExp (ArrayAccess _ (ArrayIndex _ arrE iE)) = do (tyA, pA) <- tcExp arrE case tyA of TcRefT (TcArrayT tyElem pElem) -> do (tyI, pI) <- tcExp iE check (isIntConvertible tyI) $ "Non-integral expression of type " ++ prettyPrint tyI ++ " used as array index expression" constraintLS pI pA return (tyElem, pElem `join` pA) _ -> fail $ "Cannot index non-array expression " ++ prettyPrint arrE ++ " of type " ++ prettyPrint tyA tcExp e = fail $ "tcExp: Unsupported expression: " ++ prettyPrint e -------------------------- -- Array initializers tcArrayInit :: TcType -> [TcPolicy] -> ArrayInit () -> Tc r () tcArrayInit baseType (pol1:pols) (ArrayInit _ inits) = do ps <- mapM (tcVarInit baseType pols) inits mapM_ (\p -> constraintLS p pol1) ps tcArrayInit _ [] _ = fail $ "Array initializer has too many dimensions" tcVarInit :: TcType -> [TcPolicy] -> VarInit () -> Tc r TcPolicy tcVarInit baseType pols (InitExp _ e) = do -- debugTc $ "Pols: " ++ show pols -- debugTc $ "Exp: " ++ show e (tyE,pE) <- tcExp e let elemType = mkArrayType baseType pols check (tyE == elemType) $ "Expression " ++ prettyPrint e ++ " in array initializer has type " ++ prettyPrint tyE ++ " but array expects elements of type " ++ prettyPrint elemType return pE tcVarInit baseType pols (InitArray _ arr) = do tcArrayInit baseType pols arr return bottom evalMaybePol :: Maybe (Policy ()) -> Tc r TcPolicy evalMaybePol = maybe (return bottom) (liftCont . evalPolicy) -------------------------- -- Field Access tcFieldAccess :: FieldAccess () -> Tc r (TcType, TcPolicy) tcFieldAccess (PrimaryFieldAccess _ e fi) = do (tyE,pE) <- tcExp e case tyE of -- Ugly hack to get the oft-used "length" function working TcRefT (TcArrayT tyElem pElem) -> if fi == Ident () "length" then return (intT, pE) else fail $ "Unsupported array field: " ++ prettyPrint fi _ -> do VSig tyF pFi _ _ <- lookupFieldT tyE fi return (tyF, pE `join` pFi) tcFieldAccess fa = error $ "Unsupported field access: " ++ prettyPrint fa -------------------------- -- Method invocations tcMethodInv :: MethodInvocation () -> Tc r (TcType, TcPolicy) tcMethodInv mi = do --debugTc $ "tcMethodInv: " ++ show mi mSigORlSig <- case mi of MethodCall _ n args -> do (tysArgs, psArgs) <- unzip <$> mapM tcExp args eML <- lookupMethod n tysArgs case eML of Left (pPath,_tps,mti) -> return $ Left (mti, psArgs, pPath) Right (pPath,lsig) -> return $ Right (n,lsig, pPath, tysArgs, psArgs) PrimaryMethodCall _ e tas i args -> do (tyE, pE) <- tcExp e (tysArgs, psArgs) <- unzip <$> mapM tcExp args (tps,genMti) <- lookupMethodT tyE i tysArgs tArgs <- liftCont $ mapM (evalSrcTypeArg . ActualArg ()) tas let mti = instantiate (zip tps tArgs) genMti return $ Left (mti, psArgs, pE) _ -> fail $ "tcMethodInv: Unsupported method call" case mSigORlSig of -- This is a method call Left (mti, psArgs, pE) -> do let (MSig tyR pR psPars pW lExp lMods exns) = mti -- Check lockstates l <- getCurrentLockState check (null (lExp \\ l)) $ "Lockstate too weak: " ++ "(" ++ show lExp ++ ", " ++ show l ++ ")" -- Check argument constraints mapM_ (uncurry (constraint l)) (zip psArgs psPars) -- Check E[branchPC](*) <= pW bpc <- getBranchPC_ constraint_ bpc pW -- Check exnPC(S) <= pW epc <- getExnPC constraint_ epc pW -- Check Exns(X)[write] <= E[exns](X)[write] AND -- Check Exns(X)[read] >= E[exns](X)[read] mapM (uncurry exnConsistent) exns -- Fix outgoing state let exns' = map (first ExnType) exns activateExns exns' -- ==> S' = Sn[exns{X +-> (Sx, exns(X)[write])}] applyLockMods lMods -- ==> S'' = S'[lockMods ||>>= lMods, scrambleActors Nothing -- ==> actors scrambled] return (tyR, pE `join` pR) -- This is a lock query Right (n, lsig, pE, tysArgs, psArgs) -> do let (LSig pL pAr) = lsig check (pAr == length tysArgs) $ "Lock expects " ++ show pAr ++ " arguments but has been given " ++ show (length tysArgs) -- TODO: better error message, printing out WHICH lock mapM_ (\ty -> check (isActorType ty) $ "Trying to query lock with argument of type " ++ prettyPrint ty ++ "\n" ++ "All arguments to lock query must be of type actor") tysArgs let tyR = lockT [TcLock n $ map (fromJust . mActorId) tysArgs] return (tyR, foldl1 join (pL:psArgs)) ----------------------------------- -- Policy expressions -- Treat them as pure compile-time for now tcPolicyExp :: PolicyExp () -> Tc r TcPolicy tcPolicyExp (PolicyLit _ cs) = do tcCs <- mapM tcClause cs return $ TcPolicy tcCs tcPolicyExp (PolicyOf _ i) = do _ <- lookupVar (Name () [i]) return $ TcRigidVar i tcPolicyExp (PolicyTypeVar _ i) = do _ <- lookupVar (Name () [i]) return $ TcRigidVar i tcClause :: Clause () -> Tc r (TcClause TcActor) tcClause (Clause _ h ats) = do tcH <- tcActor h tcAs <- mapM tcAtom ats return (TcClause tcH tcAs) tcAtom :: Atom () -> Tc r TcAtom tcAtom (Atom _ n as) = do ar <- lookupLockArity n check (length as == ar) $ "Arity mismatch in policy" tcAs <- mapM tcActor as return (TcAtom n tcAs) tcActor :: Actor () -> Tc r TcActor tcActor (Var _ i) = return $ TcVar i tcActor (Actor _ n) = TcActor <$> tcActorName n tcActorName :: ActorName () -> Tc r ActorId tcActorName (ActorName _ n) = getActorId n tcActorName (ActorTypeVar _ i) = return $ ActorTPVar i ----------------------------------- -- Types of operators -- ----------------------------------- opType :: Op () -> TcType -> TcType -> Tc r TcType -- First the special cases: policy operators, and String conversion opType (Mult _) (TcPolicyPolT p1) (TcPolicyPolT p2) = return (TcPolicyPolT (p1 `join` p2)) opType (Add _) (TcPolicyPolT p1) (TcPolicyPolT p2) = return (TcPolicyPolT (p1 `meet` p2)) opType (Add _) t1 t2 | t1 == stringT || t2 == stringT = return stringT opType op t1 t2 -- Numeric operators | op `elem` (map ($()) [Mult, Div, Rem, Add, Sub]) = do check (isNumConvertible t1) $ "Numeric operator " ++ prettyPrint op ++ " used with non-numeric operand of type " ++ prettyPrint t1 check (isNumConvertible t2) $ "Numeric operator " ++ prettyPrint op ++ " used with non-numeric operand of type " ++ prettyPrint t2 return $ binaryNumPromote_ t1 t2 -- Shift operators | op `elem` (map ($()) [LShift, RShift, RRShift]) = do check (isIntConvertible t1) $ "Shift operator " ++ prettyPrint op ++ " used with non-integral operand of type " ++ prettyPrint t1 check (isIntConvertible t2) $ "Shift operator " ++ prettyPrint op ++ " used with non-integral operand of type " ++ prettyPrint t2 return $ unaryNumPromote_ t1 -- Relational operators | op `elem` (map ($()) [LThan, GThan, LThanE, GThanE]) = do check (isNumConvertible t1) $ "Numerical comparison operator " ++ prettyPrint op ++ " used with non-numeric operand of type " ++ prettyPrint t1 check (isNumConvertible t2) $ "Numerical comparison operator " ++ prettyPrint op ++ " used with non-numeric operand of type " ++ prettyPrint t2 return booleanT | op `elem` [Equal (), NotEq ()] = do case binaryNumPromote t1 t2 of Just _ -> return () _ | isBoolConvertible t1 && isBoolConvertible t2 -> return () | isRefType t1 && isRefType t2 -> return () _ -> fail $ "Equality operator " ++ prettyPrint op ++ " used with incomparable operands of types " ++ prettyPrint t1 ++ " and " ++ prettyPrint t2 return booleanT | op `elem` [And (), Or (), Xor ()] = if isBoolConvertible t1 then do check (isBoolConvertible t2) $ "Logical operator " ++ prettyPrint op ++ " used with non-boolean operand of type " ++ prettyPrint t2 return booleanT else if isIntConvertible t1 then do check (isIntConvertible t2) $ "Bitwise operator " ++ prettyPrint op ++ " used with non-integral operand of type " ++ prettyPrint t2 return $ binaryNumPromote_ t1 t2 else fail $ "Bitwise/logical operator " ++ prettyPrint op ++ " used with non-integral and non-boolean operand of type " ++ prettyPrint t1 | op `elem` [CAnd (), COr ()] = do check (isBoolConvertible t1) $ "Logical operator " ++ prettyPrint op ++ " used with non-boolean operand of type " ++ prettyPrint t1 check (isBoolConvertible t2) $ "Logical operator " ++ prettyPrint op ++ " used with non-boolean operand of type " ++ prettyPrint t2 return booleanT splitName :: Name () -> (Maybe (Name ()), Name ()) splitName (Name _ is) = let (o,f) = (init is, last is) mo = if null o then Nothing else Just (Name () o) in (mo, Name () [f])