{-# LANGUAGE TupleSections, PatternGuards, BangPatterns #-} module Language.Java.Paragon.TypeCheck.Monad ( {- check, checkM, ignore, orElse, maybeM, withFold, withFoldMap, getReturn, extendVarEnvList, extendVarEnv, lookupPrefixName, lookupVar, lookupActorName, --lookupField, lookupFieldT, lookupMethod, lookupMethodT, lookupConstr, lookupLock, lookupExn, registerExn, registerExns, extendLockEnv, getBranchPC, getBranchPC_, extendBranchPC, addBranchPC, addBranchPCList, getActorId, setActorId, newActorId, newActorIdWith, newUnknownId, freshActorId, unknownActorId, scrambleActors, getPolicy, getExnPC, throwExn, activateExns, deactivateExn, getExnState, mergeActiveExnStates, useExnState, getCurrentPC, getCurrentLockState, applyLockMods, openLock, closeLock, newMetaPolVar, constraint, constraintPC, constraintLS, exnConsistent, extendTypeMapP, extendTypeMapT, -- lookupPkgTypeMap, -- getTypeMap, withTypeMap, evalSrcType, evalSrcRefType, evalSrcClsType, evalSrcTypeArg, evalSrcNWTypeArg, evalReturnType, getReadPolicy, getWritePolicy, getLockPolicy, getParamPolicy, getReturnPolicy, --fromSrcType, (<:), evalPolicy, evalPolicyExp, evalLock, evalActor, -} module Language.Java.Paragon.TypeCheck.Monad.TcCodeM, module Language.Java.Paragon.TypeCheck.Monad, {- debug, debugTc, solve -} ) where import Language.Java.Paragon.Syntax import Language.Java.Paragon.Pretty import Language.Java.Paragon.Interaction --import Language.Java.Paragon.TypeCheck.Monad.TcBase --import Language.Java.Paragon.TypeCheck.Monad.TcCont --import Language.Java.Paragon.TypeCheck.Monad.TcMonad import Language.Java.Paragon.TypeCheck.Monad.TcDeclM import Language.Java.Paragon.TypeCheck.Monad.TcCodeM import Language.Java.Paragon.TypeCheck.Monad.CodeEnv import Language.Java.Paragon.TypeCheck.Monad.CodeState import Language.Java.Paragon.TypeCheck.Types import Language.Java.Paragon.TypeCheck.TypeMap import Language.Java.Paragon.TypeCheck.Actors import Language.Java.Paragon.TypeCheck.Policy import Language.Java.Paragon.TypeCheck.Locks import Language.Java.Paragon.TypeCheck.Containment import Language.Java.Paragon.TypeCheck.Constraints import Control.Monad hiding (join) -- (filterM, zipWithM, when) --import qualified Control.Monad (join) as Monad import Control.Applicative ( (<$>), (<*>) ) --import Control.Arrow ( first, second ) import qualified Data.Map.Strict as Map --import Data.IORef import Data.List (union, intersperse, partition) import Data.Maybe (isJust) import Data.Generics.Uniplate.Data import qualified Data.ByteString.Char8 as B --debug :: String -> TcDeclM () --debug str = liftIO $ finePrint $ "DEBUG: " ++ str --debugTc :: String -> TcCodeM () --debugTc = liftTcDeclM . debug monadModule :: String monadModule = typeCheckerBase ++ ".Monad" -------------------------------------------- -- Working with the env -- -------------------------------------------- -- this --getThisType :: TcCodeM TcType --getThisType = liftCont getThisT -- returns getReturn :: TcCodeM (TcType, ActorPolicy) getReturn = do mRet <- returnI <$> getEnv case mRet of Nothing -> fail "Attempting to use 'return' in a simple expression context" Just ret -> return ret {- registerReturn :: TcType -> TcPolicy -> TcCodeM r a -> TcCodeM r a registerReturn ty p = withEnv $ \env -> env { returnI = (ty,p) } -} -- lookup entities --fieldEnvToVars :: TcCodeM r a -> TcCodeM r a --fieldEnvToVars = withEnv $ \env -> env { vars = fields (typemap env) } extendVarEnvList :: [(B.ByteString, VarFieldSig)] -> TcCodeM a -> TcCodeM a extendVarEnvList vs = withEnv $ \env -> let oldVmap = vars env newVmap = foldl (\m (i,vti) -> Map.insert i vti m) oldVmap vs in env { vars = newVmap } extendVarEnv :: B.ByteString -> VarFieldSig -> TcCodeM a -> TcCodeM a --extendVarEnv i = extendVarEnvN i --extendVarEnvN :: Ident -> VarFieldSig -> TcCodeM a -> TcCodeM a extendVarEnv i vti = withEnv $ \env -> let oldVmap = vars env newVmap = Map.insert i vti oldVmap in env { vars = newVmap } lookupActorName :: ActorName () -> TcCodeM (TcStateType, ActorPolicy) lookupActorName (ActorName _ nam@(Name _ nt mPre i)) | nt == EName = do (ty, pol, _) <- lookupVar mPre i return (ty, pol) | otherwise = panic (monadModule ++ ".lookupActorName") $ "Not an EName: " ++ show nam lookupActorName (ActorTypeVar _ i) = do (ty, pol, _) <- lookupVar Nothing i return (ty, pol) lookupActorName n = panic (monadModule ++ ".lookupActorName") $ "Unexpected AntiQName: " ++ show n -- | Lookup the prefix part of a name, which has to be dereferenceable. -- Returns the relevant type (Nothing if package), its typemap -- and the accumulated policy of the name access path. lookupPrefixName :: Name () -> TcCodeM (Maybe TcStateType, TypeMap, ActorPolicy) lookupPrefixName n@(Name _ EName Nothing i) = do -- Special case: This *could* be a var, since those can only -- appear first in the name, i.e. prefix == Nothing -- We can piggyback on lookupVar since its preconditions are met (sty, p, _) <- lookupVar Nothing i -- debugPrint $ "lookupPrefixName: " ++ prettyPrint i ++ " :: " ++ prettyPrint sty tm <- getTypeMap case lookupTypeOfStateT sty tm of Right newSig -> do -- debugPrint $ prettyPrint newSig -- debugPrint $ "\nSig before instantiation: " -- ++ prettyPrint (tMembers newSig) -- debugPrint $ "\nSig after instantiation: " -- ++ prettyPrint (instThis p (tMembers newSig)) ++ "\n" return (Just sty, instThis p $ tMembers newSig, p) Left (Just err) -> fail err _ -> panic (monadModule ++ ".lookupPrefixName") $ "Unknown variable or field: " ++ show n lookupPrefixName n@(Name _ nt mPre i) = do baseTm <- getTypeMap (mPreSty, preTm, prePol) <- case mPre of Nothing -> do return (Nothing, baseTm, bottom) Just pre -> lookupPrefixName pre baseTm2 <- getTypeMap case nt of EName -> case Map.lookup (unIdent i) $ fields preTm of Just (VSig ty p _ _ _) -> do -- debugPrint $ "lookupPrefixName: EName: " ++ prettyPrint n ++ -- " :: " ++ prettyPrint ty -- debugPrint $ show (packages baseTm2) ++ "\n" sty <- getStateType (Just n) mPreSty ty case lookupTypeOfStateT sty baseTm2 of Right tsig -> return (Just sty, instThis p $ tMembers tsig, prePol `joinWThis` p) Left (Just err) -> fail err _ -> panic (monadModule ++ ".lookupPrefixName") $ "Unknown type: " ++ show ty Nothing -> panic (monadModule ++ ".lookupPrefixName") $ "Not a field: " ++ show n TName -> do (_tps, _iaps, tsig) <- case Map.lookup (unIdent i) $ types preTm of Nothing -> liftTcDeclM $ fetchType n -- panic (monadModule ++ ".lookupPrefixName") -- $ "Not a type: " ++ show n Just tinfo -> return tinfo -- This lookup arises from refering to static fields, and then type arguments aren't given. -- TODO: Check that field *is* static. -- check (null tps) $ -- "Type " ++ prettyPrint n ++ " expects " ++ -- show (length tps) ++ " but has been given none." return (Just . stateType . TcRefT $ tType tsig, tMembers tsig, prePol) PName -> case Map.lookup (unIdent i) $ packages preTm of Nothing -> do liftTcDeclM $ fetchPkg n return (Nothing, emptyTM, prePol) -- panic (monadModule ++ ".lookupPrefixName") -- $ "Not a package: " ++ show n Just tm -> return (Nothing, tm, prePol) _ -> panic (monadModule ++ ".lookupPrefixName") $ "Malformed prefix name: " ++ show n lookupPrefixName n = panic (monadModule ++ ".lookupPrefixName") $ "Malformed prefix name: " ++ show n -- | Lookup the type and policy of a field or variable access path. -- Precondition: Name is the decomposition of an EName lookupVar :: Maybe (Name ()) -> Ident () -> TcCodeM (TcStateType, ActorPolicy, Bool) lookupVar Nothing i = do -- Could be a single variable let nam = Name () EName Nothing i -- Reconstructing for lookups varMap <- vars <$> getEnv case Map.lookup (unIdent i) varMap of -- Is a variable Just (VSig ty p param _ _) -> do sty <- getStateType (Just nam) Nothing ty --debugPrint $ "%%% " ++ prettyPrint i ++ " is a variable!" --debugPrint $ prettyPrint ty return (sty, p, param) -- Not a variable, must be a field Nothing -> do tm <- getTypeMap case Map.lookup (unIdent i) $ fields tm of Just (VSig ty p param _ _) -> do sty <- getStateType (Just nam) Nothing ty --debugPrint $ "Var: " ++ prettyPrint i ++ " " ++ show (sty, p) return (sty, p, param) Nothing -> panic (monadModule ++ ".lookupVar") $ "Not a var or field: " ++ show i lookupVar (Just pre) i = do (mPreTy, preTm, prePol) <- lookupPrefixName pre case Map.lookup (unIdent i) $ fields preTm of Just (VSig ty p _ _ _) -> do let nam = Name () EName (Just pre) i --debugPrint $ "lookupVar: " ++ prettyPrint nam ++ " :: " ++ prettyPrint ty --debugPrint $ " mPreTy: " ++ show mPreTy sty <- getStateType (Just nam) mPreTy ty return (sty, prePol `joinWThis` p, False) Nothing -> case mPreTy of Just preTy -> fail $ "Type " ++ prettyPrint preTy ++ " does not have a field named " ++ prettyPrint i Nothing -> panic (monadModule ++ ".lookupVar") $ "EName as direct child of PName: " ++ show (Name () EName (Just pre) i) type Sig = ([TypeParam ()], [TcType], Bool) type APPairs = [(ActorPolicy, ActorPolicy)] findBestMethod :: [TypeArgument ()] -> [TcType] -> [Sig] -- Works for both methods and constrs -> TcCodeM [(Sig, APPairs)] findBestMethod tArgs argTys candidates = do --debugPrint $ "findBestMethod: " --debugPrint $ " Candidates: " --mapM_ (debugPrint . (" " ++) . prettyPrint) candidates --debugPrint $ " Argument types: " --debugPrint $ " " ++ prettyPrint argTys mps <- mapM isApplicable candidates res <- findBestFit [ (c, ps) | (c, Just ps) <- zip candidates mps ] --debugPrint $ "Best method done" return res -- findBestFit =<< filterM isApplicable candidates where isApplicable :: Sig -> TcCodeM (Maybe APPairs) isApplicable (tps, pTys, isVA) = do b1 <- checkArgs tps tArgs if b1 then do tyArgs <- liftTcDeclM $ mapM (uncurry evalSrcTypeArg) $ zip tps tArgs let pTys' = instantiate (zip tps tyArgs) pTys --debugPrint $ "isApplicable: " -- ++ show (isVA, map prettyPrint pTys', map prettyPrint argTys) ps <- checkTys isVA pTys' argTys --debugPrint $ " .... " -- ++ maybe "Nope" (prettyPrint . (map (\(a,b) -> [a,b]))) ps return ps else return Nothing checkArgs :: [TypeParam ()] -> [TypeArgument ()] -> TcCodeM Bool checkArgs [] [] = return True checkArgs (tp:tps) (ta:tas) = (&&) <$> checkArg tp ta <*> checkArgs tps tas checkArgs _ _ = return False checkArg :: TypeParam () -> TypeArgument () -> TcCodeM Bool checkArg tp ta = liftTcDeclM $ isRight <$> tryM (evalSrcTypeArg tp ta) checkTys :: Bool -> [TcType] -> [TcType] -> TcCodeM (Maybe APPairs) checkTys _ [] [] = return $ Just [] checkTys b ps as | not b && length ps /= length as = return Nothing | b && length ps > length as + 1 = return Nothing checkTys True [p] [a] = do mps <- a `isAssignableTo` p case mps of Just _ -> return $ mps Nothing -> a `isAssignableTo` arrayType p bottom checkTys True [p] as = do mpps <- zipWithM isAssignableTo as (repeat p) -- [M [(P,P)]] return $ concat <$> sequence mpps checkTys b (p:ps) (a:as) = do mps <- a `isAssignableTo` p case mps of Just aps -> do mAps' <- checkTys b ps as return $ fmap (aps++) mAps' Nothing -> return Nothing checkTys _ _ _ = return Nothing findBestFit :: [(Sig, APPairs)] -> TcCodeM [(Sig, APPairs)] findBestFit [] = return [] findBestFit (x:xs) = go [x] xs go :: [(Sig, APPairs)] -> [(Sig, APPairs)] -> TcCodeM [(Sig, APPairs)] go xs [] = return xs go xs (y:ys) = do bs0 <- mapM (\x -> fst y `moreSpecificThan` fst x) xs if and bs0 then go [y] ys else do bs1 <- mapM (\x -> fst x `moreSpecificThan` fst y) xs if and bs1 then go xs ys else go (y:xs) ys moreSpecificThan :: Sig -> Sig -> TcCodeM Bool moreSpecificThan (_,ps1,False) (_,ps2,False) = do mpss <- zipWithM isAssignableTo ps1 ps2 -- [M [(P,P)]] return $ isJust $ sequence mpss moreSpecificThan _ _ = fail $ "Varargs not yet supported" {- moreSpecificThan (_,ps1,True ) (_,ps2,True ) = do let n = length ps1 k = length ps2 undefined n k moreSpecificThan _ _ = undefined -} isRight :: Either a b -> Bool isRight (Right _) = True isRight _ = False -- | Lookup the signature of a method, and the policy of its access path. lookupMethod :: Maybe (Name ()) -- Access path -> Ident () -- Method name -> [TypeArgument ()] -- Type arguments -> [TcType] -- Argument types -> TcCodeM (ActorPolicy, [TypeParam ()], MethodSig) lookupMethod mPre i tArgs argTys = do --debugPrint $ "lookupMethod: " ++ show (mPre, i, argTys) baseTm <- getTypeMap (mPreTy, preTm, prePol) <- case mPre of Nothing -> return (Nothing, baseTm, bottom) Just pre -> lookupPrefixName pre case Map.lookup (unIdent i) $ methods preTm of Nothing -> fail $ case mPreTy of Just preTy -> "Type " ++ prettyPrint preTy ++ " does not have a method named " ++ prettyPrint i Nothing -> "No method named " ++ prettyPrint i ++ " is in scope" Just methodMap -> do --debugPrint $ prettyPrint methodMap bests <- findBestMethod tArgs argTys (Map.keys methodMap) case bests of [] -> fail $ case mPreTy of Just preTy -> "Type " ++ prettyPrint preTy ++ " does not have a method named " ++ prettyPrint i ++ " matching argument types (" ++ (unwords $ intersperse ", " $ map prettyPrint argTys) ++ ")" Nothing -> "No method named " ++ prettyPrint i ++ " matching argument types (" ++ (unwords $ intersperse ", " $ map prettyPrint argTys) ++ ") is in scope" (_:_:_) -> fail $ case mPreTy of Just preTy -> "Type " ++ prettyPrint preTy ++ " has more than one most specific method " ++ prettyPrint i ++ " matching argument types (" ++ (unwords $ intersperse ", " $ map prettyPrint argTys) ++ ")" Nothing -> "More than one most specific method named " ++ prettyPrint i ++ " matching argument types (" ++ (unwords $ intersperse ", " $ map prettyPrint argTys) ++ ") is in scope" [(sig@(tps, _, _), aps)] -> case Map.lookup sig methodMap of Nothing -> panic (monadModule ++ ".lookupMethod") $ "Sig must be one of the keys of methodMap: " ++ show sig Just msig -> do mapM_ (\(p,q) -> do constraint [] p q $ "Cannot unify policy type parameters at call to method " ++ prettyPrint i ++ ":\n" ++ " p: " ++ prettyPrint p ++ "\n" ++ " q: " ++ prettyPrint q constraint [] q p $ "Cannot unify policy type parameters at call to method " ++ prettyPrint i ++ ":\n" ++ " p: " ++ prettyPrint q ++ "\n" ++ " q: " ++ prettyPrint p) aps return (prePol, tps, msig) -- | Lookup the signature of a lock -- note that all locks are static, -- so the policy of the access path is irrelevant. lookupLock :: Maybe (Name ()) -- Access path -> Ident () -- Name of lock -> TcCodeM LockSig lookupLock mPre i = do baseTm <- getTypeMap preTm <- case mPre of Nothing -> return baseTm Just pre -> do (_, preTm, _) <- lookupPrefixName pre return preTm case Map.lookup (unIdent i) $ locks preTm of Just lsig -> return lsig Nothing -> fail $ "Lock " ++ prettyPrint (Name () LName mPre i) ++ " not in scope" lookupFieldT :: TcStateType -> Ident () -> TcCodeM VarFieldSig lookupFieldT typ i = do check (isRefType typ) $ "Not a reference type: " ++ prettyPrint typ aSig <- lookupTypeOfStateType typ case Map.lookup (unIdent i) (fields $ tMembers aSig) of Just vti -> return vti Nothing -> fail $ "Class " ++ prettyPrint typ ++ " does not have a field named " ++ prettyPrint i lookupMethodT :: TcStateType -> Ident () -> [TypeArgument ()] -> [TcType] -> TcCodeM ([TypeParam ()], MethodSig) lookupMethodT typ i tArgs argTys = do check (isRefType typ) $ "Not a reference type: " ++ prettyPrint typ aSig <- lookupTypeOfStateType typ case Map.lookup (unIdent i) (methods $ tMembers aSig) of Nothing -> fail $ "Class " ++ prettyPrint typ ++ " does not have a method named " ++ prettyPrint i Just mMap -> do bests <- findBestMethod tArgs argTys (Map.keys mMap) case bests of [] -> fail $ "Type " ++ prettyPrint typ ++ " does not have a method named " ++ prettyPrint i ++ " matching argument types (" ++ (unwords $ intersperse ", " $ map prettyPrint argTys) ++ ")" (_:_:_) -> fail $ "Type " ++ prettyPrint typ ++ " has more than one most specific method " ++ prettyPrint i ++ " matching argument types (" ++ (unwords $ intersperse ", " $ map prettyPrint argTys) ++ ")" [(sig@(tps, _, _), aps)] -> case Map.lookup sig mMap of Nothing -> panic (monadModule ++ ".lookupMethodT") $ "Sig must be one of the keys of methodMap: " ++ show sig Just msig -> do mapM_ (\(p,q) -> do constraint [] p q $ "Cannot unify policy type parameters at method call:\n" ++ " p: " ++ prettyPrint p ++ "\n" ++ " q: " ++ prettyPrint q constraint [] q p $ "Cannot unify policy type parameters at method call:\n" ++ " p: " ++ prettyPrint q ++ "\n" ++ " q: " ++ prettyPrint p) aps return (tps, msig) lookupConstr :: TcClassType -> [TypeArgument ()] -> ActorPolicy -- policyof(this), i.e. the result -> [TcType] -> TcCodeM ([TypeParam ()], [B.ByteString], ConstrSig) lookupConstr ctyp tArgs pThis argTys = do --debugPrint $ "\n\n######## Looking up constructor! ######## \n" let typ = clsTypeToType ctyp --debugPrint $ "typ: " ++ prettyPrint typ -- tm <- getTypeMap -- debugPrint $ prettyPrint tm (iaps, aSig) <- lookupTypeOfType typ -- debugPrint $ "aSig: " ++ show aSig let cMap = constrs $ tMembers aSig --debugPrint $ "cMap: " --debugPrint $ prettyPrint cMap let cMap' = instThis pThis cMap bests <- findBestMethod tArgs argTys (Map.keys cMap') case bests of [] -> fail $ "Type " ++ prettyPrint ctyp ++ " does not have a constructor \ \matching argument types (" ++ (unwords $ intersperse ", " $ map prettyPrint argTys) ++ ")" (_:_:_) -> fail $ "Type " ++ prettyPrint ctyp ++ " has more than one most specific \ \constructor matching argument types (" ++ (unwords $ intersperse ", " $ map prettyPrint argTys) ++ ")" [(sig@(tps,_,_), aps)] -> case Map.lookup sig cMap' of Nothing -> panic (monadModule ++ ".lookupConstr") $ "Sig must be one of the keys of constrMap: " ++ show sig Just csig -> do mapM_ (\(p,q) -> do constraint [] p q $ "Cannot unify policy type parameters at constructor call:\n" ++ " p: " ++ prettyPrint p ++ "\n" ++ " q: " ++ prettyPrint q constraint [] q p $ "Cannot unify policy type parameters at constructor call:\n" ++ " p: " ++ prettyPrint q ++ "\n" ++ " q: " ++ prettyPrint p) aps return (tps, iaps, csig) lookupExn :: TcType -> TcCodeM (ActorPolicy, ActorPolicy) lookupExn tyX = do exnMap <- exnsE <$> getEnv case Map.lookup tyX exnMap of Just ps -> return ps Nothing -> fail $ "lookupExn: Unregistered exception type: " ++ prettyPrint tyX registerExn_ :: TcType -> PrgPolicy TcActor -> PrgPolicy TcActor -> TcCodeM a -> TcCodeM a registerExn_ tyX rX wX = registerExn tyX (RealPolicy rX) (RealPolicy wX) registerExn :: TcType -> ActorPolicy -> ActorPolicy -> TcCodeM a -> TcCodeM a registerExn tyX rX wX = registerExns [(tyX, (rX,wX))] registerExns :: [(TcType, (ActorPolicy, ActorPolicy))] -> TcCodeM a -> TcCodeM a registerExns tysPols = withEnv $ \env -> let oldMap = exnsE env newMap = foldl (\m (t,ps) -> Map.insert t ps m) oldMap tysPols in env { exnsE = newMap } extendLockEnv :: [TcLock] -> TcCodeM a -> TcCodeM a extendLockEnv locs = withEnv $ \env -> env { lockstate = lockstate env `union` locs } getBranchPC :: Entity -> TcCodeM [(ActorPolicy, String)] getBranchPC e = do env <- getEnv -- debugTcCodeM $ "Env: " ++ show env return $ branchPC (Just e) env getBranchPC_ :: TcCodeM [(ActorPolicy, String)] getBranchPC_ = do env <- getEnv return $ branchPC Nothing env extendBranchPC :: ActorPolicy -> String -> TcCodeM a -> TcCodeM a extendBranchPC p str = withEnv $ joinBranchPC p str addBranchPCList :: [Ident ()] -> TcCodeM a -> TcCodeM a addBranchPCList is = withEnv $ \env -> let (bm, def) = branchPCE env newBm = foldl (\m i -> Map.insert (VarEntity (mkSimpleName EName i)) [] m) bm is in env { branchPCE = (newBm, def) } addBranchPC :: Entity -> TcCodeM a -> TcCodeM a addBranchPC ent = withEnv $ \env -> let (bm, def) = branchPCE env newBm = Map.insert ent [] bm in env { branchPCE = (newBm, def) } getCurrentPC :: Entity -> TcCodeM ActorPolicy getCurrentPC ent = do bpcs <- fst . unzip <$> getBranchPC ent epcs <- fst . unzip <$> getExnPC return $ foldl join bottom (bpcs ++ epcs) -------------------------------------------- -- Working with states -- -------------------------------------------- {- -- Leave actor mappings from fields startState :: TcCodeM () startState = updateState $ \s -> s { lockMods = noMods, exnS = Map.empty } -} -- Instance analysis getStateType :: Maybe (Name ()) -- field/var name (if decidable) -> Maybe TcStateType -- containing object state type -> TcType -- field/var/cell type -> TcCodeM TcStateType getStateType mn mtyO ty | ty == actorT = do actorIdT <$> getActorId mn mtyO | ty == policyT = do policyPolT <$> getPolicyBounds mn mtyO | Just ct <- mClassType ty = do debugPrint $ "getStateType: " ++ show (fmap prettyPrint mn, fmap prettyPrint mtyO, prettyPrint ct) instanceT ct <$> getInstanceActors ct mn mtyO | otherwise = return $ stateType ty getActorId :: Maybe (Name ()) -> Maybe TcStateType -> TcCodeM ActorId getActorId Nothing Nothing = liftTcDeclM unknownActorId getActorId (Just (Name _ EName mPre i)) mstyO = do -- Check if already exists: (vm, upd) <- touchPrefix mPre -- Prefix guaranteed to exist let ast = actorSt vm case Map.lookup (unIdent i) ast of Just ai -> return $ aID ai Nothing -> do tm <- case mstyO of Just styO -> do tsig <- lookupTypeOfStateType styO return $ tMembers tsig Nothing -> getTypeMap (stab, aid) <- case Map.lookup (unIdent i) $ actors tm of Just aid -> return (True, aid) Nothing -> do newAid <- liftTcDeclM unknownActorId return (False, newAid) let ai = AI stab aid setState $ upd $ vm { actorSt = Map.insert (unIdent i) ai ast } return aid getActorId mn ms = panic (monadModule ++ ".getActorId") $ show (mn, ms) getPolicyBounds :: Maybe (Name ()) -> Maybe TcStateType -> TcCodeM ActorPolicyBounds getPolicyBounds Nothing Nothing = return $ PolicyBounds bottom top getPolicyBounds (Just (Name _ EName mPre i)) mstyO = do (vm, upd) <- touchPrefix mPre -- Prefix guaranteed to exist let pst = policySt vm case Map.lookup (unIdent i) pst of -- Check if already exists: Just pif -> return $ pBounds pif Nothing -> do tm <- case mstyO of Just styO -> do tsig <- lookupTypeOfStateType styO return $ tMembers tsig Nothing -> getTypeMap (stab, pbs) <- case Map.lookup (unIdent i) $ policies tm of Just pol -> return (True, KnownPolicy $ RealPolicy pol) Nothing -> return (False, PolicyBounds bottom top) let pif = PI stab pbs setState $ upd $ vm { policySt = Map.insert (unIdent i) pif pst } return pbs getPolicyBounds mn ms = panic (monadModule ++ ".getPolicyBounds") $ show (mn, ms) getInstanceActors :: TcClassType -> Maybe (Name ()) -> Maybe TcStateType -> TcCodeM [ActorId] getInstanceActors ct@(TcClassT tyN _) Nothing Nothing = do (iaps, _) <- lookupTypeOfType (clsTypeToType ct) mapM (instanceActorId . Name () EName (Just tyN) . Ident ()) iaps getInstanceActors ct@(TcClassT tyN _) (Just (Name _ EName mPre i)) mstyO = do vm <- getPrefix mPre -- Prefix guaranteed to exist let ist = instanceSt vm -- debugPrint $ show ist -- Check if already exists: case Map.lookup (unIdent i) ist of Just ii -> return $ iImplActorArgs ii Nothing -> do tm <- case mstyO of Just styO -> do debugPrint $ "styO: " ++ show styO tsig <- lookupTypeOfStateType styO return $ tMembers tsig Nothing -> debugPrint ("No mstyO!") >> getTypeMap (stab, aids) <- case Map.lookup (unIdent i) $ fields tm of Just (VSig ty _ _ _ fin) -> do (iaps, _) <- lookupTypeOfType ty aids <- mapM (instanceActorId . Name () EName (Just tyN) . Ident ()) iaps return (fin, aids) Nothing -> do --debugPrint $ prettyPrint tm panic (monadModule ++ ".getInstanceActors") $ "No such field: " ++ prettyPrint ct ++ "." ++ prettyPrint i let ii = II (TcClsRefT ct) stab False -- TODO: Freshness aids emptyVM debugPrint $ "Forced to touch" (_, upd) <- touchPrefix mPre setState $ upd $ vm { instanceSt = Map.insert (unIdent i) ii ist } return aids getInstanceActors ct mn ms = panic (monadModule ++ ".getPolicyBounds") $ show (ct, mn, ms) registerParamType :: Ident () -> TcType -> TcCodeM () registerParamType i ty = registerStateType i ty True Nothing registerStateType :: Ident () -- Entity to register -> TcType -- Its type -> Bool -- Its stability -> Maybe TcStateType -- rhs state type (Nothing if no initialiser) -> TcCodeM () registerStateType i tyV stab mRhsSty = ignore $ updateStateType (Just (Name () EName Nothing i, stab)) tyV mRhsSty {- registerStateType i tyV mSty | tyV == actorT = do case mSty of Nothing -> actorIdT <$> newActorId i -- fresh generation Just sty -> case mActorId sty of Nothing -> panic (monadModule ++ ".registerStateType") $ "Actor state but non-actor target type: " ++ show (tyV, sty) Just aid -> do newActorIdWith i aid return $ actorIdT aid registerStateType i tyV mSty | tyV == policyT = do let pbs = case mSty of Nothing -> PolicyBounds bottom top Just sty -> case mPolicyPol sty of Nothing -> panic (monadModule ++ ".registerStateType") $ "Policy state but non-policy target type: " ++ show (tyV, sty) Just bs -> bs updateState $ \s -> s { policySt = Map.insert (mkSimpleName EName i) pbs $ policySt s } return $ policyPolT pbs registerStateType i tyV mSty | Just ct <- mClassType tyV = do debugPrint $ "registerStateType: " ++ show (i, tyV, mSty) case mSty of -- no initialiser Nothing -> return $ instanceT ct [] -- ?? Just sty -> case mInstanceType sty of Just (_, aids) -> do updateState $ \s -> s { instanceSt = Map.insert (mkSimpleName EName i) aids $ instanceSt s } return $ instanceT ct aids Nothing | isNullType sty -> return $ instanceT ct [] | otherwise -> panic (monadModule ++ ".registerStateType") $ "Instance state but non-instance target type: " ++ show (tyV, sty) registerStateType _i tyV _mSty = return $ stateType tyV -} updateStateType :: Maybe (Name (), Bool) -- field/var name and stability (if decidable) -> TcType -- field/var/cell type -> Maybe TcStateType -- rhs state type (Nothing if no initialiser) -> TcCodeM TcStateType updateStateType mN tyV mRhsSty | tyV == actorT = actorIdT <$> updateActorId mN mRhsSty updateStateType mN tyV mRhsSty | tyV == policyT = policyPolT <$> updatePolicyBounds mN mRhsSty updateStateType mN tyV mRhsSty | Just ct <- mClassType tyV = instanceT ct <$> updateInstanceActors ct mN mRhsSty updateStateType _ tyV _ = return $ stateType tyV updateActorId :: Maybe (Name (), Bool) -- field/var name and stability (if decidable) -> Maybe TcStateType -- rhs state type (Nothing if no initialiser) -> TcCodeM ActorId updateActorId Nothing (Just rhsSty) = case mActorId rhsSty of Just aid -> return aid Nothing -> panic (monadModule ++ ".updateActorId") $ "Non-actor rhs for actor field: " ++ show rhsSty updateActorId (Just (Name _ EName mPre i, stab)) mRhsSty = do (vm, upd) <- touchPrefix mPre aid <- case mRhsSty of Nothing -> liftTcDeclM $ freshActorId (prettyPrint i) Just sty | Just aid <- mActorId sty -> return aid Just _ -> panic (monadModule ++ ".updateActorId") $ "Non-actor rhs for actor field: " ++ show mRhsSty setState $ upd $ vm { actorSt = Map.insert (unIdent i) (AI stab aid) $ actorSt vm } return aid updateActorId mn _ = panic (monadModule ++ ".updateActorId") $ show mn updatePolicyBounds :: Maybe (Name (), Bool) -- field/var name and stability (if decidable) -> Maybe TcStateType -- rhs state type (Nothing if no initialiser) -> TcCodeM ActorPolicyBounds updatePolicyBounds Nothing (Just rhsSty) = case mPolicyPol rhsSty of Just pbs -> return pbs Nothing -> panic (monadModule ++ ".updatePolicyBounds") $ "Non-policy rhs for policy field: " ++ show rhsSty updatePolicyBounds (Just (Name _ EName mPre i, stab)) mRhsSty = do (vm, upd) <- touchPrefix mPre pbs <- case mRhsSty of Nothing -> return $ KnownPolicy top -- default for "primitive" policy types Just sty | Just pbs <- mPolicyPol sty -> return pbs Just _ -> panic (monadModule ++ ".updatePolicyBounds") $ "Non-policy rhs for policy field: " ++ show mRhsSty setState $ upd $ vm { policySt = Map.insert (unIdent i) (PI stab pbs) $ policySt vm } return pbs updatePolicyBounds mn _ = panic (monadModule ++ ".updatePolicyBounds") $ show mn updateInstanceActors :: TcClassType -> Maybe (Name (), Bool) -- field/var name and stability (if decidable) -- -> Maybe TcStateType -- containing type -> Maybe TcStateType -- rhs state type (Nothing if no initialiser) -> TcCodeM [ActorId] updateInstanceActors ct Nothing (Just rhsSty) = do -- debugPrint $ "updateInstanceActors Nothing: " ++ show (ct, rhsSty) case mInstanceType rhsSty of Just (_, aids) -> return aids Nothing | isNullType rhsSty -> getInstanceActors ct Nothing Nothing Nothing -> panic (monadModule ++ ".updateInstanceActors") $ "Non-instance rhs for class type field: " ++ show rhsSty updateInstanceActors ct@(TcClassT tyN _) (Just (_n@(Name _ EName mPre i), stab)) mRhsSty = do debugPrint $ "updateInstanceActors Just: " ++ show (prettyPrint _n, stab, prettyPrint ct, fmap prettyPrint mRhsSty) (vm, upd) <- touchPrefix mPre iaas <- case mRhsSty of Nothing -> do (iaps, _) <- lookupTypeOfType (clsTypeToType ct) mapM (instanceActorId . Name () EName (Just tyN) . Ident ()) iaps Just sty | Just (_, aids) <- mInstanceType sty -> return aids | isNullType sty -> getInstanceActors ct Nothing Nothing Just _ -> panic (monadModule ++ ".updateInstanceActors") $ "Non-instance rhs for class type field: " ++ show mRhsSty let ist = instanceSt vm ii <- case Map.lookup (unIdent i) ist of Just ii -> return ii Nothing -> return $ II (TcClsRefT ct) stab False -- TODO: Freshness iaas emptyVM setState $ upd $ vm { instanceSt = Map.insert (unIdent i) ii ist } return iaas updateInstanceActors _ mn _ = panic (monadModule ++ ".updateInstanceActors") $ show mn {- updateStateType mN _mTyO tyV sty | tyV == actorT = do case mActorId sty of Just aid -> do -- maybeM mTyO $ \tyO -> scrambleActors (Just tyO) maybeM mN $ \n -> setActorId n aid return sty _ -> panic (monadModule ++ ".updateStateType") $ "Actor state but non-actor target type: " ++ show (tyV, sty) -- TODO {- updateStateType mN mTyO tyV mSty | tyV == policyT = do case mSty of Just sty | Just pbs <- mPolicyPol sty -> do -} updateStateType _mN _mTyO ty _sty | isPrimType (stateType ty) = return $ stateType ty updateStateType mN _mTyO ty sty | Just ct <- mClassType ty = case sty of TcInstance _ aids -> return $ TcInstance ct aids _ | isNullType sty -> TcInstance ct <$> getInstanceActors mN ct _ | isArrayType sty -> return $ TcInstance ct [] _ -> panic (monadModule ++ ".updateStateType") $ "Class type target but no instance type" ++ show (ty, sty) updateStateType _mN _mTyO _ty sty = return sty -- BOGUS!!! -- Instance Analysis getInstanceActors :: Maybe (Name ()) -> TcClassType -> TcCodeM [ActorId] getInstanceActors mn ct@(TcClassT tyN _) = do instanceMap <- instanceSt <$> getState case maybe Nothing (\n -> Map.lookup n instanceMap) mn of Nothing -> do (iaps, _) <- lookupTypeOfType (clsTypeToType ct) mapM (instanceActorId . Name () EName (Just tyN)) iaps Just aids -> return aids -- Policy Analysis getPolicyBounds :: Maybe (Name ()) -> Maybe TcStateType -> TcCodeM ActorPolicyBounds getPolicyBounds mn mtyO = do policyMap <- policySt <$> getState case maybe Nothing (\n -> Map.lookup n policyMap) mn of Nothing -> case (mtyO, mn) of (Just styO, Just (Name _ _ _ i)) -> do tsig <- lookupTypeOfStateType styO case Map.lookup i $ policies $ tMembers tsig of Just pol -> return $ KnownPolicy $ RealPolicy pol Nothing -> return $ PolicyBounds bottom top _ -> return $ PolicyBounds bottom top Just pif -> return pif -- Actor Analysis getActorId :: Maybe (Name ()) -> Maybe TcStateType -> TcCodeM ActorId getActorId mn mtyO = do actorMap <- actorSt <$> getState case maybe Nothing (\n -> Map.lookup n actorMap) mn of Nothing -> case (mtyO, mn) of (Just styO, Just (Name _ _ _ i)) -> do tsig <- lookupTypeOfStateType styO case Map.lookup i $ actors $ tMembers tsig of Just aid -> return aid Nothing -> liftTcDeclM $ unknownActorId _ -> liftTcDeclM $ unknownActorId Just ai -> return $ aID ai setActorId :: Name () -> ActorId -> TcCodeM () setActorId n aid = updateState setAct where setAct :: CodeState -> CodeState setAct s@(CodeState { actorSt = actMap }) = s { actorSt = Map.adjust replId n actMap } replId (AI _ st) = AI aid st newActorIdWith :: Ident () -> ActorId -> TcCodeM () newActorIdWith i aid = do updateState insertAct where insertAct :: CodeState -> CodeState insertAct s@(CodeState { actorSt = actMap }) = s { actorSt = Map.insert (mkSimpleName EName i) (AI aid Stable) actMap } newActorId :: Ident () -> TcCodeM ActorId newActorId i = do aid <- liftTcDeclM $ freshActorId (prettyPrint i) newActorIdWith i aid return aid newUnknownId :: Ident () -> TcCodeM ActorId newUnknownId i = do aid <- liftTcDeclM unknownActorId newActorIdWith i aid return aid -} {- scrambleActors :: Maybe TcType -> TcCodeM () scrambleActors mtc = do let stb = maybe FullV (FieldV . Just . typeName_) mtc state <- getState u <- getUniqRef newState <- liftIO $ scramble u stb state setState newState -} -- Exception tracking getExnPC :: TcCodeM [(TcPolicy TcActor, String)] getExnPC = exnPC <$> getState throwExn :: ExnType -> TcPolicy TcActor -> TcCodeM () throwExn et pX = do debugPrint $ "throwExn: " ++ show et state <- getState let !oldXmap = exnS state newXmap = Map.fromList [(et, ExnPoint state pX)] mergedXmap <- liftBase $ mergeExns oldXmap newXmap setState $ state { exnS = mergedXmap } deactivateExn :: ExnType -> TcCodeM () deactivateExn et = updateState $ \s -> let oldEmap = exnS s newEmap = Map.delete et oldEmap in s { exnS = newEmap } activateExns :: [(ExnType, (ActorPolicy, LockMods))] -> TcCodeM () activateExns exns = do state <- getState let (ts, sigs) = unzip exns xPoints = map (\(wX, modsX) -> let !s = -- scramble $ -- FullV should be Nothing - TODO state { lockMods = lockMods state ||>> modsX } in (s, wX)) sigs let -- oldXmap = exnS state newXmap = Map.fromList $ zip ts (map (uncurry ExnPoint) xPoints) !mergedXmap <- liftBase $ mergeExns (exnS state) newXmap setState $ state { exnS = mergedXmap } getExnState :: ExnType -> TcCodeM (Maybe CodeState) getExnState et = do eMap <- exnS <$> getState return $ epState <$> Map.lookup et eMap mergeActiveExnStates :: TcCodeM () mergeActiveExnStates = do exnMap <- exnS <$> getState mapM_ (mergeWithState . epState) $ Map.elems exnMap useExnState :: CodeState -> TcCodeM () useExnState es = updateState (\s -> s { exnS = exnS es }) -- Lockstate tracking getCurrentLockState :: TcCodeM [TcLock] getCurrentLockState = do base <- lockstate <$> getEnv mods <- lockMods <$> getState return $ snd $ ([], base) ||>> mods applyLockMods :: LockMods -> TcCodeM () applyLockMods lms = do updateState $ \s -> s { lockMods = lockMods s ||>> lms } openLock, closeLock :: TcLock -> TcCodeM () openLock l = applyLockMods ([],[l]) closeLock l = applyLockMods ([l],[]) -- Policy inference newMetaPolVar :: Ident () -> TcCodeM ActorPolicy newMetaPolVar i = do uniq <- getFreshInt return $ VarPolicy (TcMetaVar uniq $ unIdent i) --newRigidPolVar :: TcCodeM TcPolicy --newRigidPolVar = do -- uniq <- lift . getUniq =<< getUniqRef -- return $ TcRigidVar uniq -------------------------------------------- -- Working with constraints -- -------------------------------------------- constraint :: [TcLock] -> ActorPolicy -> ActorPolicy -> String -> TcCodeM () constraint ls p q str = do -- addConstraint $ LRT ls p1 p2 g <- getGlobalLockProps bs <- getParamPolicyBounds case lrt bs g ls p q of Left b -> do -- st <- getState check b (str {-++ "\n\nState: " ++ show st -}) Right c -> addConstraint c str getParamPolicyBounds :: TcCodeM [(B.ByteString, ActorPolicy)] getParamPolicyBounds = parBounds <$> getEnv getGlobalLockProps :: TcCodeM [TcClause TcAtom] getGlobalLockProps = do cs <- go <$> getTypeMap return cs where go :: TypeMap -> [TcClause TcAtom] go tm = let lps = map lProps $ Map.elems $ locks tm tlps = map (go . tMembers . (\(_,_,x) -> x)) $ Map.elems $ types tm plps = map go $ Map.elems $ packages tm in concat $ lps ++ tlps ++ plps locksToRec :: [TcLock] -> (PrgPolicy TcAtom) locksToRec ls = TcPolicy (map (\x -> TcClause x []) (map lockToAtom ls)) constraintLS :: ActorPolicy -> ActorPolicy -> String -> TcCodeM () constraintLS p1 p2 str = do l <- getCurrentLockState withErrCtxt ("In the context of lock state: " ++ prettyPrint l ++ "\n") $ constraint l p1 p2 str constraintPC :: [(ActorPolicy, String)] -> ActorPolicy -> (ActorPolicy -> String -> String) -> TcCodeM () constraintPC bpcs pW msgf = mapM_ (uncurry constraintPC_) bpcs where constraintPC_ :: ActorPolicy -> String -> TcCodeM () -- Don't take lock state into account constraintPC_ pPC src = constraint [] pPC pW (msgf pPC src) exnConsistent :: Either (Name ()) TcClassType -> TcType -> (ActorPolicy, ActorPolicy) -> TcCodeM () exnConsistent caller exnTy (rX,wX) = do exnMap <- exnsE <$> getEnv --debugTc $ "Using exnMap: " ++ show exnMap let (callerName, callerSort) = case caller of Left n -> (prettyPrint n , "method" ) Right ct -> (prettyPrint ct, "constructor") case Map.lookup exnTy exnMap of Nothing -> fail $ "Unchecked exception: " ++ prettyPrint (typeName_ exnTy) Just (rE, wE) -> do constraint [] wE wX $ "Exception " ++ prettyPrint exnTy ++ ", thrown by invocation of " ++ callerSort ++ " " ++ callerName ++ ", has write effect " ++ prettyPrint wX ++ " but the context in which the " ++ callerSort ++ " is invoked expects its write effect to be no less restrictive than " ++ prettyPrint wE constraint [] rX rE $ -- constraintLS? "Exception " ++ prettyPrint exnTy ++ ", thrown by invocation of " ++ callerSort ++ " " ++ callerName ++ ", has policy " ++ prettyPrint rX ++ " but the context in which the " ++ callerSort ++ " is invoked expects its policy to be no more restrictive than " ++ prettyPrint rE ------------------------------------------------------------ -- Subtyping/conversion/promotion -- Note that we do NOT allow unchecked conversion or capture conversion. -- We don't give crap about backwards compatibility here, and even if we -- did, we would have to rule it out because it would be unsound. isAssignableTo :: TcType -> TcType -> TcCodeM (Maybe [(ActorPolicy, ActorPolicy)]) isAssignableTo t1 t2 = do case t1 `equivTo` t2 of -- identity conversion Just ps -> return $ Just ps Nothing -> do b <- liftTcDeclM $ t1 `widensTo` t2 -- widening conversion return $ if b then Just [] else Nothing (=<:) :: TcType -> TcStateType -> TcCodeM (Maybe [(ActorPolicy, ActorPolicy)]) lhs =<: rhs = isAssignableTo (unStateType rhs) lhs equivTo :: TcType -> TcType -> Maybe [(ActorPolicy, ActorPolicy)] equivTo (TcRefT rt1) (TcRefT rt2) = equivRefT rt1 rt2 where equivRefT :: TcRefType -> TcRefType -> Maybe [(ActorPolicy, ActorPolicy)] equivRefT (TcArrayT t1 p1) (TcArrayT t2 p2) = do ps <- t1 `equivTo` t2 return $ (p1,p2):ps equivRefT (TcClsRefT ct1) (TcClsRefT ct2) = equivClsT ct1 ct2 equivRefT _ _ = if rt1 == rt2 then return [] else Nothing equivClsT :: TcClassType -> TcClassType -> Maybe [(ActorPolicy, ActorPolicy)] equivClsT (TcClassT n1 tas1) (TcClassT n2 tas2) = if n1 /= n2 then Nothing else equivTypeArgs tas1 tas2 equivTypeArgs :: [TcTypeArg] -> [TcTypeArg] -> Maybe [(ActorPolicy, ActorPolicy)] equivTypeArgs tas1 tas2 = concat <$> sequence (map (uncurry equivTypeArg) (zip tas1 tas2)) equivTypeArg :: TcTypeArg -> TcTypeArg -> Maybe [(ActorPolicy, ActorPolicy)] equivTypeArg (TcActualPolicy p1) (TcActualPolicy p2) = Just [(p1, p2)] equivTypeArg (TcActualType r1) (TcActualType r2) = equivRefT r1 r2 equivTypeArg a1 a2 = if a1 == a2 then return [] else Nothing equivTo t1 t2 = if t1 == t2 then return [] else Nothing isCastableTo :: TcType -> TcType -> TcCodeM (Maybe [(ActorPolicy, ActorPolicy)], Bool) -- (Can be cast, needs reference narrowing) isCastableTo t1 t2 = do -- 'isAssignableTo' handles the cases of identity, primitive widening, -- boxing + reference widening and unboxing + primitive widening. -- It also handles reference widening, but not with subsequent unboxing. mps <- isAssignableTo t1 t2 case mps of Just ps -> return (Just ps, False) Nothing -> liftTcDeclM $ do -- What we have left is primitive narrowing, primitive widening+narrowing, -- reference widening + unboxing, and reference narrowing + optional unboxing. -- Only the last one, that includes reference narrowing, can throw a ClassCastException. case (t1, t2) of (TcPrimT pt1, TcPrimT pt2) -> -- primitive (widening +) narrowing return $ (if pt2 `elem` narrowConvert pt1 ++ widenNarrowConvert pt1 then Just [] else Nothing, False) (TcRefT rt1, TcPrimT pt2) | Just ct2 <- box pt2 -> do -- reference widening + unboxing AND -- reference narrowing + unboxing -- We cheat and compare to the boxing of the target instead -- since box/unbox are inverses. let rt2 = TcClsRefT ct2 bWide <- rt1 `subTypeOf` rt2 if bWide then return (Just [], False) else return (Just [], True) (TcRefT _rt1, TcRefT _rt2) -> do -- reference narrowing, no unboxing -- TODO: There are restrictions here, but not relevant at this point return (Just [], True) _ -> return (Nothing, False) (<<:) :: TcType -> TcStateType -> TcCodeM (Maybe [(ActorPolicy, ActorPolicy)], Bool) lhs <<: rhs = isCastableTo (unStateType rhs) lhs -- widening conversion can come in four basic shapes: -- 1) pt/pt -> widening primitive conversion -- 2) rt/rt -> widening reference conversion -- 3) pt/rt -> boxing conversion + widening reference conversion -- 4) rt/pt -> unboxing conversion + widening primitive conversion widensTo :: TcType -> TcType -> TcDeclM Bool widensTo (TcPrimT pt1) (TcPrimT pt2) = return $ pt2 `elem` widenConvert pt1 widensTo (TcRefT rt1) (TcRefT rt2) = rt1 `subTypeOf` rt2 widensTo (TcPrimT pt1) t2@(TcRefT _) = maybe (return False) (\ct -> clsTypeToType ct `widensTo` t2) (box pt1) widensTo (TcRefT rt1) t2@(TcPrimT _) = case rt1 of TcClsRefT ct -> maybe (return False) (\pt -> TcPrimT pt `widensTo` t2) (unbox ct) _ -> return False {-- 5) Paragon-specific types widensTo t1 t2 | isPolicyType t1 && t2 == policyT = return True | isLockType t1 && t2 == booleanT = return True | isActorType t1 && t2 == actorT = return True -} widensTo _ _ = return False subTypeOf :: TcRefType -> TcRefType -> TcDeclM Bool subTypeOf TcNullT _ = return True subTypeOf rt1 rt2 = (rt2 `elem`) <$> ([TcClsRefT objectT] ++) <$> superTypes rt1 where superTypes :: TcRefType -> TcDeclM [TcRefType] superTypes rt = do tm <- getTypeMap tsig <- case lookupTypeOfRefT rt tm of Left Nothing -> do case rt of TcClsRefT (TcClassT n tas) -> do (tps, _iaps, tsig) <- fetchType n return $ instantiate (zip tps tas) tsig _ -> panic (monadModule ++ ".subTypeOf") $ show rt Left err -> panic (monadModule ++ ".subTypeOf") $ "Looking up type:" ++ show rt ++ "\nError: " ++ show err Right (_,tsig) -> return tsig let sups = tSupers tsig impls = tImpls tsig allS = map TcClsRefT $ sups ++ impls supsups <- mapM superTypes allS return $ concat $ allS:supsups ------------------------------------------ -- Constraints resolution -- ------------------------------------------ -- Resolution thanks to the transitive closure. solve :: [ConstraintWMsg] -> TcDeclM () solve cs = do finePrint $ "Solving constraints..." debugPrint $ show (length cs) let wcs = [c | (c, _) <- cs] --Extract constraints wcs' = concat $ map splitCstrs wcs --Split them : (Join p q <= r)<=>((p<=r)/\(q<=r)) --print "wcs" --mapM_ print wcs --print "wcs'" --mapM_ print wcs' cvars = filter isCstrVar wcs' --Get the "p<=X" constraints, X MetaVar --print "cvars" --mapM_ print cvars cvarsm = foldl linker Map.empty cvars --Map to X the list of p s.t. p<=X csubsts = Map.foldrWithKey --Realize the substitutions (\x pxs cs' -> foldr (\px cs'' -> substitution x px cs'') cs' pxs) wcs' cvarsm (_toInfer, ccstright) = partition isCstrVar csubsts toBeChecked = filter noVarLeft ccstright mapM_ (checkCstr ("The system failed to infer the set of unspecified policies ")) toBeChecked finePrint $ "Constraints successfully solved!" checkCstr :: String -> Constraint -> TcDeclM () checkCstr str (LRT bs g ls p q) = do case lrt bs g ls p q of Left b -> do check b str Right _ -> panic (monadModule ++ ".checkCstr") $ "This set of constraint should be solved !" {- solve :: [ConstraintWMsg] -> TcDeclM () solve cs = liftIO $ do wcs <- return [(p, q) | (LRT _ p q, _) <- cs] cvars <- filterM isCstrVar wcs cvarsm <- return (foldl linker Map.empty cvars) csubsts <- return (Map.foldlWithKey (\cs' x pxs -> foldl (\cs'' px-> (substitution x px cs'')) cs' pxs) wcs cvarsm) tobechecked <- filterM (\c -> do b <- (isCstrVar c); return $ not b) csubsts mapM_ print tobechecked mapM_ (checkCstr "The unspecified variable's policies inference leads, without taking into account the global policy, to an unsolvable system. Please explicite them.") tobechecked -} -------------------------------------------------- -- State scrambling -- 'scramble' should be called at method calls, -- and will remove everything that is not known -- not to be affected by that call. scrambleState :: TcCodeM () scrambleState = do -- s1 <- getState -- debugPrint $ "\nScrambling: " ++ show s1 updateState scramble -- s2 <- getState -- debugPrint $ "Scrambling done: " ++ show s2 ++ "\n" scramble :: CodeState -> CodeState scramble = transformBi scr where scr :: VarMap -> VarMap scr (VarMap aMap pMap iMap tMap) = VarMap (deleteIf (const $ not . aStable) aMap) (deleteIf (const $ not . pStable) pMap) (deleteIf (const $ not . iStable) iMap) tMap -- fixed recursively by transformBi -- 'scrambleT' should be called when a field is -- updated, and will remove everything that could -- be an update-through-alias of that field. scrambleT :: TcRefType -> Ident () -> Bool -> TcCodeM () scrambleT rtyO iF fresh = setState =<< transformBiM scr =<< getState -- "updateStateM" where scr :: InstanceInfo -> TcCodeM InstanceInfo scr isig = do appl <- liftTcDeclM $ (iType isig) `subTypeOf` rtyO return $ if appl && not (fresh && iFresh isig) then isig { iMembers = scrVM $ iMembers isig } else isig scrVM :: VarMap -> VarMap scrVM (VarMap aMap pMap iMap tMap) = let matches k _v = k == unIdent iF in VarMap (deleteIf matches aMap) (deleteIf matches pMap) (deleteIf matches iMap) tMap -- will be empty deleteIf :: Ord k => (k -> v -> Bool) -> Map k v -> Map k v deleteIf test = snd . Map.partitionWithKey test