module Language.Java.Paragon.TypeCheck.TcExp 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.Actors import Language.Java.Paragon.TypeCheck.Locks import Language.Java.Paragon.TypeCheck.Monad.TcCodeM import Language.Java.Paragon.TypeCheck.Monad import Language.Java.Paragon.TypeCheck.Types import Language.Java.Paragon.TypeCheck.TypeMap import Data.List ( (\\) ) import Data.Maybe (fromJust) import qualified Data.Map as Map import Control.Applicative ( (<$>) ) import Control.Arrow ( first ) import Control.Monad ( when ) tcExpModule :: String tcExpModule = typeCheckerBase ++ ".TcExp" --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 _ _) = clsTypeToType stringT litType (Null _ ) = nullT --litType l = error $ "litType: " ++ show l ----------------------------------- -- Checking expressions -- ----------------------------------- --debugTc str = liftIO $ putStrLn $ "DEBUG: Tc: " ++ str --debugTc _ = return () tcExp :: Exp () -> TcCodeM r (TcType, ActorPolicy, Exp T) -- Rule PAREN tcExp (Paren _ e) = do (ty, p, e') <- tcExp e return (ty, p, Paren (Just ty) e') -- Rule LIT tcExp (Lit _ l) = let ty = litType l in return (ty, bottom, Lit (Just ty) (notAppl l)) -- Rule THIS tcExp (This _) = do ty <- getThisType --debugPrint $ "getThisType: " ++ show ty let tTy = clsTypeToType ty return (tTy, bottom, This $ Just tTy) -- Rule BINOP tcExp (BinOp _ e1 op e2) = do (ty1, p1, e1') <- tcExp e1 (ty2, p2, e2') <- tcExp e2 tyRes <- opType op ty1 ty2 return (tyRes, p1 `join` p2, BinOp (Just tyRes) e1' (notAppl op) e2') -- Rule VAR/FIELD tcExp (ExpName _ n) = case n of Name _ EName mPre i -> do (ty1, pol, _) <- lookupVar mPre i ty <- case ty1 of TcPrimT (PolicyT _) -> policyPolT <$> getPolicy n TcPrimT (ActorT _) -> actorIdT <$> getActorId n _ -> return ty1 return (ty, pol, ExpName (Just ty) (notAppl n)) Name _ LName mPre i -> do LSig pL arL _ <- lookupLock mPre i check (arL == 0) $ "Lock " ++ prettyPrint n ++ " expects " ++ show arL ++ " arguments but has been given none." let ty = lockT [TcLock n []] return $ (ty, pL, ExpName (Just ty) (notAppl n)) Name _ EOrLName mPre i -> do tryCatch (tcExp $ ExpName () $ Name () EName mPre i) (\_ -> tcExp $ ExpName () $ Name () LName mPre i) _ -> panic (tcExpModule ++ ".tcExp:ExpName") $ "Unexpected name: " ++ show n -- Rule VARASS/FIELDASS tcExp ex@(Assign _ lhs _op rhs) = do debugPrint $ prettyPrint ex (tyV, pV, mtyO, mEnt, mN, lhs') <- case lhs of NameLhs _ n@(Name _ EName mPre iF) -> do case mPre of Nothing -> do -- VARASS (tyV, pV, _) <- lookupVar Nothing iF return (tyV, pV, Nothing, Just (varE n), Just n, NameLhs (Just tyV) (notAppl n)) Just pre -> do -- FIELDASS (Just tyO, tmO, pO) <- lookupPrefixName pre case Map.lookup iF $ fields tmO of Just (VSig tyF pF _ _ _) -> do constraint [] pO pF $ "Cannot update field " ++ prettyPrint iF ++ " of object " ++ prettyPrint pre ++ ": policy of field must be no less restrictive than that of the " ++ "object when updating\n" ++ "Object policy: " ++ prettyPrint pO ++ "\n" ++ "Field policy: " ++ prettyPrint pF return (tyF, pF, Just tyO, Just (varE n), Just n, NameLhs (Just tyF) (notAppl n)) Nothing -> fail $ "Object " ++ prettyPrint pre ++ " of type " ++ prettyPrint tyO ++ " does not have a field named " ++ prettyPrint iF NameLhs _ n -> panic (tcExpModule ++ ".tcEcp:Assign") $ "NameLhs not an EName: " ++ show n FieldLhs _ (PrimaryFieldAccess _ e fi) -> do (tyE, pE, e') <- tcExp e (VSig tyF pF _ _ _) <- lookupFieldT tyE fi let eEnt = case e of This _ -> Just $ thisFE fi _ -> Nothing constraint [] pE pF $ "Cannot update field " ++ prettyPrint fi ++ " of object resulting from expression " ++ prettyPrint e ++ ": policy of field must be no less restrictive than that of the " ++ "object when updating\n" ++ "Object policy: " ++ prettyPrint pE ++ "\n" ++ "Field policy: " ++ prettyPrint pF return (tyF, pF, Just tyE, eEnt, Nothing, FieldLhs (Just tyF) (PrimaryFieldAccess (Just tyF) e' (notAppl fi))) ArrayLhs _ (ArrayIndex _ arrE iE) -> do (tyA, pA, arrE') <- tcExp arrE case tyA of TcRefT (TcArrayT tyElem pElem) -> do (tyI, pI, iE') <- tcExp iE check (isIntConvertible tyI) $ "Non-integral expression of type " ++ prettyPrint tyI ++ " used as array index expression" constraintLS pI pA $ "When assigning into an array, the policy on the index " ++ "expression may be no more restrictive than the policy of " ++ "the array itself\n" ++ "Array: " ++ prettyPrint arrE ++ "\n" ++ " has policy " ++ prettyPrint pA ++ "\n" ++ "Index: " ++ prettyPrint iE ++ "\n" ++ " has policy " ++ prettyPrint pI constraint [] pA pElem $ "Cannot update element in array resulting from expression " ++ prettyPrint arrE ++ ": policy of elements must be no less restrictive than that of the " ++ "array itself when updating\n" ++ "Array policy: " ++ prettyPrint pA ++ "\n" ++ "Element policy: " ++ prettyPrint pElem return (tyElem, pElem, Just tyA, Nothing, Nothing, ArrayLhs (Just tyElem) (ArrayIndex (Just tyElem) arrE' iE')) _ -> fail $ "Cannot index non-array expression " ++ prettyPrint arrE ++ " of type " ++ prettyPrint tyA _ -> fail $ "Lhs not supported: " ++ prettyPrint lhs (tyRhs, pRhs, rhs') <- tcExp rhs -- Check all the necessary constraints: -- TODO: Check that _op is allowed on tyV checkM (tyV =<: tyRhs) $ "Type mismatch: " ++ prettyPrint tyRhs ++ " <=> " ++ prettyPrint tyV -- Check: E[branchPC](n) <= pV bpcs <- maybe getBranchPC_ getBranchPC mEnt constraintPC bpcs pV $ \p src -> "Assignment to " ++ prettyPrint lhs ++ " with policy " ++ prettyPrint pV ++ " not allowed in " ++ src ++ " with write effect bound " ++ prettyPrint p -- Check: exnPC(S) <= pV epcs <- getExnPC constraintPC epcs pV $ \p src -> "Assignment to " ++ prettyPrint lhs ++ " with policy " ++ prettyPrint pV ++ " not allowed in " ++ src ++ " with write effect bound " ++ prettyPrint p -- Check: pRhs <= pV modulo L constraintLS pRhs pV $ "Cannot assign result of expression " ++ prettyPrint rhs ++ " with policy " ++ prettyPrint pRhs ++ " to location " ++ prettyPrint lhs ++ " with policy " ++ prettyPrint pV -- Check: pO <= pV, if pO exists -- maybeM mpO (\pO -> constraint [] pO pV $ -- "When changing the state of an object, the policy of the changed field may not " ++ -- "be less restrictive than the policy of the object\n" ++ -- " -- 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, Assign (Just tyV) lhs' (notAppl _op) rhs') -- Rule CALL tcExp (MethodInv _ mi) = do (ty, p, mi') <- tcMethodOrLockInv mi return (ty, p, MethodInv (Just ty) mi') -- Rule NEW tcExp (InstanceCreation _ tas ct args Nothing) = do -- debugPrint $ "tcExp: " ++ show e tyT <- liftTcDeclM $ evalSrcClsType ct (ty, p, args') <- tcCreate tyT tas args return (ty, p, InstanceCreation (Just ty) (map notAppl tas) (notAppl ct) args' Nothing) -- Rule COND tcExp (Cond _ c e1 e2) = do (tyC, pC, c') <- tcExp c --check (tyC `elem` [booleanT, clsTypeToType . fromJust . box $ BooleanT ()]) check (isBoolConvertible tyC) $ "Conditional expression requires a condition of type compatible with boolean\n" ++ "Found type: " ++ prettyPrint tyC extendBranchPC pC ("conditional expression dependent on expression " ++ prettyPrint c) $ do ((ty1, p1, e1'), (ty2, p2, e2')) <- (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, Cond (Just ty1) c' e1' e2') tcExp (PolicyExp _ pl) = do pRep <- tcPolicyExp pl let ty = policyPolT $ RealPolicy pRep return (ty, bottom, PolicyExp (Just ty) (notAppl pl)) tcExp (PostIncrement _ e) = do (tyE, pE, e') <- tcExp e check (isNumConvertible tyE) $ "Post-increment operator used at non-numeric type " ++ prettyPrint tyE return (tyE, pE, PostIncrement (Just tyE) e') tcExp (PostDecrement _ e) = do (tyE, pE, e') <- tcExp e check (isNumConvertible tyE) $ "Post-decrement operator used at non-numeric type " ++ prettyPrint tyE return (tyE, pE, PostDecrement (Just tyE) e') tcExp (PreIncrement _ e) = do (tyE, pE, e') <- tcExp e check (isNumConvertible tyE) $ "Pre-increment operator used at non-numeric type " ++ prettyPrint tyE return (tyE, pE, PreIncrement (Just tyE) e') tcExp (PreDecrement _ e) = do (tyE, pE, e') <- tcExp e check (isNumConvertible tyE) $ "Pre-decrement operator used at non-numeric type " ++ prettyPrint tyE return (tyE, pE, PreDecrement (Just tyE) e') -- Unary promotion prefix operator -- Rule PREP tcExp (PrePlus _ e) = do (tyE, pE, e') <- tcExp e check (isNumConvertible tyE) $ "Pre-plus operator used at non-numeric type " ++ prettyPrint tyE let ty = unaryNumPromote_ tyE return (ty, pE, PrePlus (Just ty) e') tcExp (PreMinus _ e) = do (tyE, pE, e') <- tcExp e check (isNumConvertible tyE) $ "Pre-minus operator used at non-numeric type " ++ prettyPrint tyE let ty = unaryNumPromote_ tyE return (ty, pE, PreMinus (Just ty) e') tcExp (PreBitCompl _ e) = do (tyE, pE, e') <- tcExp e check (isIntConvertible tyE) $ "Pre-complement bit operator used at non-integral type " ++ prettyPrint tyE let ty = unaryNumPromote_ tyE return (ty, pE, PreBitCompl (Just ty) e') tcExp (PreNot _ e) = do (tyE, pE, e') <- tcExp e check (isBoolConvertible tyE) $ "Pre-complement boolean operator used at non-boolean type " ++ prettyPrint tyE return (booleanT, pE, PreNot (Just booleanT) e') tcExp (Cast _ t e) = do (tyE, pE, e') <- tcExp e tyC <- liftTcDeclM $ evalSrcType t (canCast, canExn) <- tyC <<: tyE check canCast $ "Wrong type at cast" when (canExn) $ -- TODO: could throw ClassCastException return () return (tyC, pE, Cast (Just tyC) (notAppl t) e') tcExp (FieldAccess _ fa) = do (ty, p, fa') <- tcFieldAccess fa return (ty, p, FieldAccess (Just ty) fa') -- Arrays tcExp (ArrayCreate _ bt dimEsPs dimImplPs) = do baseTy <- liftTcDeclM $ 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, dimE1') <- 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, dimEsRest) <- 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 let ty = mkArrayType baseTy (polEDims ++ polIDims) dimPs' = map (fmap notAppl) $ snd $ unzip dimEsPs dimEsPs' = zip (dimE1':dimEsRest) dimPs' dimImplPs' = map (fmap notAppl) dimImplPs return (ty, pol1, ArrayCreate (Just ty) (notAppl bt) dimEsPs' dimImplPs') where checkDimExprs :: [ActorPolicy] -- Accumulated policies of earlier dimensions -> [Exp T] -- Accumulated annotated expressions -> [(Exp (), Maybe (Policy ()))] -- Remaining dimexprs/pols -> ActorPolicy -- Policy of previous dimension -> TcCodeM r ([ActorPolicy], [Exp T]) checkDimExprs accP accE [] pPrev = return $ (reverse (pPrev:accP), reverse accE) checkDimExprs accP accE ((e,mp):emps) pPrev = do (tyE,pE,e') <- tcExp e check (isIntConvertible tyE) $ nonIntErr tyE -- Each dimexpr must satisfy the policy of the outer dim constraintLS pE pPrev $ "Array dimension expression has too restrictive policy:\n" ++ "Expression: " ++ prettyPrint e ++ "\n" ++ " with policy: " ++ prettyPrint pE ++ "\n" ++ "Declared policy bound: " ++ prettyPrint pPrev pNext <- evalMaybePol mp checkDimExprs (pPrev:accP) (e':accE) 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 <- liftTcDeclM $ 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 arrInit' <- tcArrayInit baseTy dimPols arrInit -- Return the specified array type -- Literal array initializers have known length, -- so their apparent policy is bottom let ty = mkArrayType baseTy dimPols return (ty, bottom, ArrayCreateInit (Just ty) (notAppl bt) (map (fmap notAppl) dimImplPs) arrInit') tcExp (ArrayAccess _ (ArrayIndex _ arrE iE)) = do (tyA, pA, arrE') <- tcExp arrE case tyA of TcRefT (TcArrayT tyElem pElem) -> do (tyI, pI, iE') <- tcExp iE check (isIntConvertible tyI) $ "Non-integral expression of type " ++ prettyPrint tyI ++ " used as array index expression" -- constraintLS pI pA $ " " -- Not true: pI just adds to the outgoing level return (tyElem, pElem `join` pA `join` pI, ArrayAccess (Just tyElem) (ArrayIndex (Just tyElem) arrE' iE')) _ -> fail $ "Cannot index non-array expression " ++ prettyPrint arrE ++ " of type " ++ prettyPrint tyA tcExp e = fail $ "tcExp: Unsupported expression: " ++ prettyPrint e -------------------------- -- Array initializers tcArrayInit :: TcType -> [ActorPolicy] -> TypeCheck (TcCodeM r) ArrayInit tcArrayInit baseType (pol1:pols) (ArrayInit _ inits) = do (ps, inits') <- unzip <$> mapM (tcVarInit baseType pols) inits mapM_ (\(p,e) -> constraintLS p pol1 $ "Expression in array initializer has too restrictive policy:\n" ++ "Expression: " ++ prettyPrint e ++ " with policy: " ++ prettyPrint p ++ "Declared policy bound: " ++ prettyPrint pol1 ) (zip ps inits) return $ ArrayInit Nothing inits' tcArrayInit _ [] _ = fail $ "Array initializer has too many dimensions" tcVarInit :: TcType -> [ActorPolicy] -> VarInit () -> TcCodeM r (ActorPolicy, VarInit T) tcVarInit baseType pols (InitExp _ e) = do -- debugPrint $ "Pols: " ++ show pols -- debugPrint $ "Exp: " ++ show e (tyE,pE,e') <- 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, InitExp Nothing e') tcVarInit baseType pols (InitArray _ arr) = do arr' <- tcArrayInit baseType pols arr return (bottom, InitArray Nothing arr') evalMaybePol :: Maybe (Policy ()) -> TcCodeM r ActorPolicy evalMaybePol = maybe (return bottom) (liftTcDeclM . evalPolicy) -------------------------- -- Field Access tcFieldAccess :: FieldAccess () -> TcCodeM r (TcType, ActorPolicy, FieldAccess T) tcFieldAccess (PrimaryFieldAccess _ e fi) = do (tyE,pE,e') <- 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, PrimaryFieldAccess (Just tyF) e' (notAppl fi)) tcFieldAccess fa = error $ "Unsupported field access: " ++ prettyPrint fa -------------------------- -- Instance creation tcCreate :: TcClassType -> [TypeArgument ()] -> [Argument ()] -> TcCodeM r (TcType, ActorPolicy, [Argument T]) tcCreate ctyT tas args = do (tysArgs, psArgs, args') <- unzip3 <$> mapM tcExp args (tps,genCti) <- lookupConstr ctyT tas tysArgs -- TODO: Check that the arguments in tyT -- match those expected by the type -- TODO: Type argument inference check (length tps == length tas) $ "Wrong number of type arguments in instance creation expression.\n" ++ "Constructor expects " ++ show (length tps) ++ " arguments but has been given " ++ show (length tas) tArgs <- liftTcDeclM $ mapM (uncurry evalSrcTypeArg) (zip tps tas) -- tm <- 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 when calling constructor " ++ prettyPrint ctyT ++ ":\n" ++ "Required lock state: " ++ prettyPrint lExp ++ "\n" ++ "Current lock state: " ++ prettyPrint l -- Check argument constraints mapM_ (\(arg,argP,parP) -> constraintLS argP parP $ "Constructor applied to argument with too restrictive policy:\n" ++ "Constructor: " ++ prettyPrint ctyT ++ "\n" ++ "Argument: " ++ prettyPrint arg ++ " with policy: " ++ prettyPrint argP ++ "Declared policy bound: " ++ prettyPrint parP ) (zip3 args psArgs psPars) -- Check E[branchPC](*) <= pW bpcs <- getBranchPC_ constraintPC bpcs pW $ \p src -> "Constructor " ++ prettyPrint ctyT ++ " with declared write effect " ++ prettyPrint pW ++ " not allowed in " ++ src ++ " with write effect bound " ++ prettyPrint p -- Check exnPC(S) <= pW epc <- getExnPC constraintPC epc pW $ \p src -> "Constructor " ++ prettyPrint ctyT ++ " with declared write effect " ++ prettyPrint pW ++ " not allowed in " ++ src ++ " with write effect bound " ++ prettyPrint p -- Check Exns(X)[write] <= E[exns](X)[write] AND -- Check Exns(X)[read] >= E[exns](X)[read] mapM_ (uncurry $ exnConsistent (Right ctyT)) 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 ctyT, bottom, args') -------------------------- -- Method invocations -- | Check a method invocation, which could possibly represent -- a lock query expression. tcMethodOrLockInv :: MethodInvocation () -> TcCodeM r (TcType, ActorPolicy, MethodInvocation T) tcMethodOrLockInv (MethodCallOrLockQuery _ (Name _ MOrLName mPre i) args) = do -- We couldn't resolve without type information whether -- this truly is a method or a lock. baseTm <- getTypeMap preTm <- case mPre of Nothing -> return baseTm Just pre -> do (_, preTm, _) <- lookupPrefixName pre return preTm let nt = case Map.lookup i $ locks preTm of Just _ -> LName Nothing -> MName tcMethodOrLockInv (MethodCallOrLockQuery () (Name () nt mPre i) args) tcMethodOrLockInv (MethodCallOrLockQuery _ nam@(Name _ LName mPre i) args) = do -- This is a lock query LSig pL arL _ <- lookupLock mPre i check (arL == length args) $ "Lock " ++ prettyPrint nam ++ " expects " ++ show arL ++ " arguments but has been given " ++ show (length args) (tysArgs, psArgs, args') <- unzip3 <$> mapM tcExp args 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 nam $ map (fromJust . mActorId) tysArgs] return (tyR, foldl1 join (pL:psArgs), MethodCallOrLockQuery (Just tyR) (notAppl nam) args') tcMethodOrLockInv mi = tcMethodInv mi -- | Check a true method invocation tcMethodInv :: MethodInvocation () -> TcCodeM r (TcType, ActorPolicy, MethodInvocation T) tcMethodInv mi = do debugPrint $ "tcMethodInv: " ++ prettyPrint mi (n, msig, args, psArgs, pE, ef) <- case mi of MethodCallOrLockQuery _ n@(Name _ MName mPre i) args -> do -- This is a true method call (tysArgs, psArgs, args') <- unzip3 <$> mapM tcExp args (pPath, tps, msig) <- lookupMethod mPre i [] tysArgs check (null tps) $ "Method " ++ prettyPrint i ++ " expects " ++ show (length tps) ++ " type arguments but has been\ \ given 0" return $ (n, msig, args, psArgs, pPath, \ty -> MethodCallOrLockQuery (Just ty) (notAppl n) args') MethodCallOrLockQuery _ n _ -> panic (tcExpModule ++ ".tcMethodInv") $ "Unexpected name: " ++ show n PrimaryMethodCall _ e tas i args -> do (tyE, pE, e') <- tcExp e (tysArgs, psArgs, args') <- unzip3 <$> mapM tcExp args let tas' = map (ActualArg ()) tas (tps, genMSig) <- lookupMethodT tyE i tas' tysArgs tArgs <- liftTcDeclM $ mapM (uncurry evalSrcTypeArg) $ zip tps tas' let msig = instantiate (zip tps tArgs) genMSig return $ (mkSimpleName MName i, msig, args, psArgs, pE, \ty -> PrimaryMethodCall (Just ty) e' (map notAppl tas) (notAppl i) args') _ -> fail $ "tcMethodInv: Unsupported method call" let (MSig tyR pR psPars pW lExp lMods exns) = msig -- Check lockstates l <- getCurrentLockState check (null (lExp \\ l)) $ "Lockstate too weak when calling method " ++ prettyPrint n ++ ":\n" ++ "Required lock state: " ++ prettyPrint lExp ++ "\n" ++ "Current lock state: " ++ prettyPrint l -- Check argument constraints mapM_ (\(arg,argP,parP) -> constraintLS argP parP $ "Method applied to argument with too restrictive policy:\n" ++ "Method invocation: " ++ prettyPrint mi ++ "\n" ++ "Argument: " ++ prettyPrint arg ++ " with policy: " ++ prettyPrint argP ++ "Declared policy bound: " ++ prettyPrint parP ) (zip3 args psArgs psPars) -- Check E[branchPC](*) <= pW bpcs <- getBranchPC_ constraintPC bpcs pW $ \p src -> "Method " ++ prettyPrint n ++ " with declared write effect " ++ prettyPrint pW ++ " not allowed in " ++ src ++ " with write effect bound " ++ prettyPrint p -- Check exnPC(S) <= pW epc <- getExnPC constraintPC epc pW $ \p src -> "Method " ++ prettyPrint n ++ " with declared write effect " ++ prettyPrint pW ++ " not allowed in " ++ src ++ " with write effect bound " ++ prettyPrint p -- Check Exns(X)[write] <= E[exns](X)[write] AND -- Check Exns(X)[read] >= E[exns](X)[read] mapM_ (uncurry $ exnConsistent (Left n)) 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, ef tyR) ----------------------------------- -- Policy expressions -- Treat them as pure compile-time for now tcPolicyExp :: PolicyExp () -> TcCodeM r (PrgPolicy TcActor) tcPolicyExp (PolicyLit _ cs) = do tcCs <- mapM tcClause cs return (TcPolicy tcCs) tcPolicyExp pe@(PolicyOf _ i) = do (_, _, param) <- lookupVar Nothing i check param $ "policyof may only be used on parameters: " ++ prettyPrint pe return $ TcRigidVar i tcPolicyExp (PolicyTypeVar _ i) = do _ <- lookupVar Nothing i return $ TcRigidVar i tcPolicyExp (PolicyThis _) = return TcThis tcClause :: Clause () -> TcCodeM r (TcClause TcActor) tcClause (Clause _ h ats) = do tcH <- tcActor h tcAs <- mapM tcAtom ats return (TcClause tcH tcAs) tcAtom :: Atom () -> TcCodeM r TcAtom tcAtom (Atom _ n@(Name _ LName mPre i) as) = do LSig _ ar _ <- lookupLock mPre i check (length as == ar) $ "Arity mismatch in policy" tcAs <- mapM tcActor as return (TcAtom n tcAs) tcAtom (Atom _ n _) = panic (tcExpModule ++ ".tcAtom") $ "None-lock name: " ++ show n tcActor :: Actor () -> TcCodeM r TcActor tcActor (Var _ i) = return $ TcVar i tcActor (Actor _ n) = TcActor <$> tcActorName n tcActorName :: ActorName () -> TcCodeM r ActorId tcActorName (ActorName _ n) = getActorId n tcActorName (ActorTypeVar _ i) = return $ ActorTPVar i ----------------------------------- -- Types of operators -- ----------------------------------- opType :: Op () -> TcType -> TcType -> TcCodeM 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 == clsTypeToType stringT || t2 == clsTypeToType stringT = return $ clsTypeToType 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 opType op _ _ = panic (tcExpModule ++ ".opType") $ show op {- 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]) splitName _ = panic (tcExpModule ++ ".splitName") "AntiQName should not appear in AST being type-checked" -}