{-# LANGUAGE TupleSections, PatternGuards #-} 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.Monad.Uniq 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 as Map --import Data.IORef import Data.List (union, intersperse, partition) --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 :: [(Ident (), 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 :: Ident () -> 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 ++ " :: " ++ show sty tm <- getTypeMap case lookupTypeOfStateT sty tm of Right newSig -> 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 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, 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 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 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 i varMap of -- Is a variable Just (VSig ty p param _ _) -> do sty <- getStateType (Just nam) Nothing ty return (sty, p, param) -- Not a variable, must be a field Nothing -> do tm <- getTypeMap case Map.lookup i $ fields tm of Just (VSig ty p param _ _) -> do sty <- getStateType (Just nam) Nothing ty 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 i $ fields preTm of Just (VSig ty p _ _ _) -> do sty <- getStateType (Just (Name () EName (Just pre) i)) mPreTy ty debugPrint $ "lookupVar: " ++ prettyPrint pre ++ "." ++ prettyPrint i ++ " :: " ++ show sty 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) findBestMethod :: [TypeArgument ()] -> [TcType] -> [Sig] -- Works for both methods and constrs -> TcCodeM [Sig] findBestMethod tArgs argTys candidates = findBestFit =<< filterM isApplicable candidates where isApplicable :: Sig -> TcCodeM Bool isApplicable (tps, pTys, isVA) = (&&) <$> checkArgs tps tArgs <*> checkTys isVA pTys argTys 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 _ _ = return True -- TODO: Type arguments not yet handled correctly checkTys _ [] [] = return True checkTys b ps as | not b && length ps /= length as = return False | b && length ps > length as + 1 = return False checkTys True [p] [a] = (a `isAssignableTo` p) `orM` (a `isAssignableTo` arrayType p bottom) checkTys True [p] as = and <$> mapM (`isAssignableTo` p) as checkTys b (p:ps) (a:as) = (&&) <$> (a `isAssignableTo` p) <*> checkTys b ps as checkTys _ _ _ = return False findBestFit :: [Sig] -> TcCodeM [Sig] findBestFit [] = return [] findBestFit (x:xs) = go [x] xs go :: [Sig] -> [Sig] -> TcCodeM [Sig] go xs [] = return xs go xs (y:ys) = do bs0 <- mapM (\x -> y `moreSpecificThan` x) xs if and bs0 then go [y] ys else do bs1 <- mapM (\x -> x `moreSpecificThan` y) xs if and bs1 then go xs ys else go (y:xs) ys moreSpecificThan :: Sig -> Sig -> TcCodeM Bool moreSpecificThan (_,ps1,False) (_,ps2,False) = and <$> zipWithM (isAssignableTo) ps1 ps2 moreSpecificThan (_,ps1,True ) (_,ps2,True ) = do let n = length ps1 k = length ps2 undefined n k moreSpecificThan _ _ = undefined -- | 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 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 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, _, _)] -> case Map.lookup sig methodMap of Nothing -> panic (monadModule ++ ".lookupMethod") $ "Sig must be one of the keys of methodMap: " ++ show sig Just msig -> 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 i $ locks preTm of Just lsig -> return lsig Nothing -> fail $ "Lock " ++ prettyPrint (Name () LName mPre i) ++ " not in scope" {- getPolicy :: Name () -> TcCodeM (PrgPolicy TcActor) getPolicy n = do tm <- getTypeMap case lookupNamed policies n tm of Nothing -> fail $ "getPolicy: No such policy: " ++ prettyPrint n Just p -> return p -} lookupFieldT :: TcStateType -> Ident () -> TcCodeM VarFieldSig lookupFieldT typ i = do check (isRefType typ) $ "Not a reference type: " ++ prettyPrint typ aSig <- lookupTypeOfStateType typ case Map.lookup 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 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, _, _)] -> case Map.lookup sig mMap of Nothing -> panic (monadModule ++ ".lookupMethodT") $ "Sig must be one of the keys of methodMap: " ++ show sig Just msig -> return (tps, msig) lookupConstr :: TcClassType -> [TypeArgument ()] -> [TcType] -> TcCodeM ([TypeParam ()], [Ident ()], ConstrSig) lookupConstr ctyp tArgs argTys = do -- debugPrint $ "\n\n######## Looking up constructor! ######## \n" let typ = clsTypeToType ctyp -- debugPrint $ "typ: " ++ show typ (iaps, aSig) <- lookupTypeOfType typ -- debugPrint $ "aSig: " ++ show aSig let cMap = constrs $ tMembers aSig -- debugPrint $ "cMap: " ++ show 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,_,_)] -> case Map.lookup sig cMap of Nothing -> panic (monadModule ++ ".lookupConstr") $ "Sig must be one of the keys of constrMap: " ++ show sig Just csig -> return (tps, iaps, csig) --lookupLock :: Name () -> TcCodeM LockSig --lookupLock n = do -- tm <- getTypeMap -- -- debugTcCodeM $ show tm -- case lookupNamed locks n tm of -- Nothing -> fail $ "Unknown lock: " ++ prettyPrint n -- Just lsig -> return lsig 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) {-- Tying the knot for member policies setFieldPol :: Ident -> TcPolicy -> TcCodeM () setFieldPol i pF = do fMap <- (fields . typemap) <$> getEnv case Map.lookup (Name [i]) fMap of Nothing -> fail "panic: lookup of field failed when tying the knot" Just (VSig ty tempP stc fin) -> do case tempP of TcPolicyVar (TcMetaVar i ref) -> do mpol <- lift $ readIORef ref case mpol of Nothing -> do lift $ writeIORef ref (Just pF) Just _ -> fail "panic: field policy already written when tying the knot" _ -> fail "panic: field policy already set when tying the knot" setMethodPols :: Ident -> TcPolicy -> TcPolicy -> TcCodeM () setMethodPols i retM -} -------------------------------------------- -- 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 = instanceT ct <$> getInstanceActors mn ct | otherwise = return $ stateType ty registerStateType :: Ident () -> TcType -> Maybe (TcStateType) -> TcCodeM TcStateType 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 ()) -- field/var name (if decidable) -> Maybe (TcType) -- Containing object type -> TcType -- field/var/cell type -> Maybe TcStateType -- rhs state type (Nothing if no init) -> TcCodeM TcStateType updateStateType mN mTyO tyV mSty | tyV == actorT = do case mSty of Just sty | Just aid <- mActorId sty -> do maybeM mTyO $ \tyO -> scrambleActors (Just tyO) maybeM mN $ \n -> setActorId n aid return sty | otherwise -> panic (monadModule ++ ".updateStateType") $ "Actor state but non-actor target type: " ++ show (tyV, sty) Nothing -> panic (monadModule ++ ".updateStateType") $ "No state for actor assignment: " ++ show mN -- TODO {- updateStateType mN mTyO tyV mSty | tyV == policyT = do case mSty of Just sty | Just pbs <- mPolicyPol sty -> do -} updateStateType _mN _mTyO ty _mSty | isPrimType (stateType ty) = return $ stateType ty updateStateType _mN _mTyO _ty (Just sty) = return sty -- BOGUS!!! updateStateType _mN _mTyO ty Nothing = return $ stateType ty -- 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 uref <- getUniqRef state <- getState let oldXmap = exnS state newXmap = Map.fromList [(et, ExnPoint state pX)] mergedXmap <- liftIO $ mergeExns uref 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 uref <- getUniqRef state <- getState let (ts, sigs) = unzip exns xPoints <- mapM (\(wX, modsX) -> do s <- liftIO $ scramble uref FullV $ -- FullV should be Nothing - TODO state { lockMods = lockMods state ||>> modsX } return (s, wX)) sigs let oldXmap = exnS state newXmap = Map.fromList $ zip ts (map (uncurry ExnPoint) xPoints) mergedXmap <- liftIO $ mergeExns uref oldXmap 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 <- liftIO . getUniq =<< getUniqRef return $ VarPolicy (TcMetaVar uniq 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 -- debugTc $ "constraint: p1: " ++ show p1 -- debugTc $ "constraint: p2: " ++ show p2 -- st <- getState check b (str {-++ "\n\nState: " ++ show st -}) Right c -> addConstraint c str getParamPolicyBounds :: TcCodeM [(Ident (), 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 :: MonadTcDeclM m => TcType -> TcType -> m Bool isAssignableTo t1 t2 = liftTcDeclM $ if t1 == t2 -- identity conversion then return True else t1 `widensTo` t2 -- widening conversion (=<:) :: MonadTcDeclM m => TcType -> TcStateType -> m Bool lhs =<: rhs = isAssignableTo (unStateType rhs) lhs isCastableTo :: MonadTcDeclM m => TcType -> TcType -> m (Bool, Bool) -- (Can be cast, needs reference narrowing) isCastableTo t1 t2 = liftTcDeclM $ 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. b <- isAssignableTo t1 t2 if b then return (True, False) else 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 $ (pt2 `elem` narrowConvert pt1 ++ widenNarrowConvert pt1, 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 (True, False) else return (True, True) (TcRefT _rt1, TcRefT _rt2) -> do -- reference narrowing, no unboxing -- TODO: There are restrictions here, but not relevant at this point return (True, True) _ -> return (False, False) (<<:) :: MonadTcDeclM m => TcType -> TcStateType -> m (Bool, 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 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 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 -}