paragon 0.1.13 → 0.1.15
raw patch · 17 files changed
+742/−298 lines, 17 files
Files
- paragon.cabal +1/−1
- src/Language/Java/Paragon.hs +6/−3
- src/Language/Java/Paragon/Parser.hs +78/−7
- src/Language/Java/Paragon/Pretty.hs +4/−3
- src/Language/Java/Paragon/Syntax.hs +3/−3
- src/Language/Java/Paragon/TypeCheck.hs +103/−39
- src/Language/Java/Paragon/TypeCheck/Actors.hs +4/−4
- src/Language/Java/Paragon/TypeCheck/Constraints.hs +3/−1
- src/Language/Java/Paragon/TypeCheck/Containment.hs +5/−5
- src/Language/Java/Paragon/TypeCheck/Monad.hs +181/−83
- src/Language/Java/Paragon/TypeCheck/Monad/TcMonad.hs +9/−4
- src/Language/Java/Paragon/TypeCheck/TcEnv.hs +59/−42
- src/Language/Java/Paragon/TypeCheck/TcExp.hs +133/−42
- src/Language/Java/Paragon/TypeCheck/TcState.hs +12/−2
- src/Language/Java/Paragon/TypeCheck/TcStmt.hs +89/−54
- src/Language/Java/Paragon/TypeCheck/Types.hs +49/−2
- src/Language/Java/Paragon/TypeCheck/Uniq.hs +3/−3
paragon.cabal view
@@ -1,5 +1,5 @@ Name: paragon-Version: 0.1.13+Version: 0.1.15 License: BSD3 License-File: LICENSE Author: Niklas Broberg
src/Language/Java/Paragon.hs view
@@ -33,7 +33,7 @@ deriving (Show, Eq) versionString, usageHeader :: String-versionString = "Paragon Compiler version: 0.1.13"+versionString = "Paragon Compiler version: 0.1.15" usageHeader = "Usage: parac [OPTION...] files..." options :: [OptDescr Flag]@@ -68,10 +68,13 @@ compile :: [Flag] -> String -> IO () compile flags filePath = do- let (directory,fileName) = splitFileName filePath --relative or absolute path?+ finePrint $ "Filepath: " ++ filePath+ let (directoryRaw,fileName) = splitFileName filePath --relative or absolute path?+ -- Workaround for old and buggy 'filepath' versions+ directory = if null directoryRaw then "./" else directoryRaw let pDir = case [ dir | PiPath dir <- flags ] of p:_ -> p- _ -> "."+ _ -> "./" fc <- readFile filePath ast <- liftE $ parser compilationUnit fc extraPrint "Parsing complete!"
src/Language/Java/Paragon/Parser.hs view
@@ -668,10 +668,10 @@ -- For loops forInit :: P (ForInit ()) -forInit = (do +forInit = (try $ do (m,t,vds) <- localVarDecl return $ ForLocalVars () m t vds) <|> - seplist1 stmtExp comma >>= return . ForInitExps () + ForInitExps () <$> seplist1 stmtExp comma forUp :: P [Exp ()] forUp = seplist1 stmtExp comma @@ -910,6 +910,9 @@ FieldAccess () fa -> return fa _ -> fail "" +fieldAccessExp :: P (Exp ()) +fieldAccessExp = FieldAccess () <$> fieldAccess + {- fieldAccess :: P FieldAccess fieldAccess = try fieldAccessNPS <|> do @@ -1115,7 +1118,12 @@ (tok Op_AAnd >> return (CAnd ())) <|> (tok Op_OOr >> return (COr ())) +typeArgInfixOp :: P (Op ()) +typeArgInfixOp = + (tok Op_Star >> return (Mult ())) <|> + (tok Op_Plus >> return (Add ())) + ---------------------------------------------------------------------------- -- Types @@ -1197,6 +1205,58 @@ bounds = tok KW_Extends >> seplist1 refType (tok Op_And) typeArgs :: P [TypeArgument ()] +typeArgs = tok Op_LThan {- < -} >> typeArgsSuffix + +typeArgsSuffix :: P [TypeArgument ()] +typeArgsSuffix = + (do tok Op_Query + wcArg <- Wildcard () <$> opt wildcardBound + rest <- typeArgsEnd + return $ wcArg:rest) <|> + (do lArg <- ActualArg () <$> parens (ActualLockState () <$> seplist1 lock comma) + rest <- typeArgsEnd + return $ lArg:rest) <|> + (try $ do rt <- refType + rest <- typeArgsEnd + let tArg = case nameOfRefType rt of + Just n -> ActualName () n + _ -> ActualType () rt + return $ (ActualArg () tArg):rest) <|> + (do eArg <- ActualArg () . ActualExp () <$> argExp + rest <- typeArgsEnd + return $ eArg:rest) + + where nameOfRefType :: RefType () -> Maybe (Name ()) + nameOfRefType (ClassRefType _ (ClassType _ ias)) = + let (is, as) = unzip ias + in if all null as then Just (Name () is) else Nothing + nameOfRefType _ = Nothing + +typeArgsEnd :: P [TypeArgument ()] +typeArgsEnd = + (tok Op_GThan {- > -} >> return []) <|> + (tok Comma >> typeArgsSuffix) + +argExp :: P (Exp ()) +argExp = do + e1 <- argExp1 + fe <- argExpSuffix + return $ fe e1 + +argExp1 :: P (Exp ()) +argExp1 = PolicyExp () <$> policyExp + <|> try methodInvocationExp + <|> try fieldAccessExp + <|> ExpName () <$> name + +argExpSuffix :: P (Exp () -> Exp ()) +argExpSuffix = + (do op <- typeArgInfixOp + e2 <- argExp + return $ \e1 -> BinOp () e1 op e2) <|> return id + +{- +typeArgs :: P [TypeArgument ()] typeArgs = angles $ seplist1 typeArg comma typeArg :: P (TypeArgument ()) @@ -1209,14 +1269,20 @@ ActualPolicy () . ExpName () <$> (tok KW_P_Policy >> name) <|> ActualActor () <$> (tok KW_P_Actor >> name) <|> ActualType () <$> refType - +-} wildcardBound :: P (WildcardBound ()) wildcardBound = tok KW_Extends >> ExtendsBound () <$> refType <|> tok KW_Super >> SuperBound () <$> refType nonWildTypeArgs :: P [NonWildTypeArgument ()] -nonWildTypeArgs = angles $ seplist nonWildTypeArg (tok Comma) +nonWildTypeArgs = typeArgs >>= mapM checkNonWild + where checkNonWild (ActualArg _ arg) = return arg + checkNonWild _ = fail "Use of wildcard in non-wild context" + +--nonWildTypeArgs :: P [NonWildTypeArgument ()] +--nonWildTypeArgs = angles $ seplist nonWildTypeArg (tok Comma) + ---------------------------------------------------------------------------- -- Names @@ -1426,7 +1492,7 @@ actIs = [ i | ActorParam _ i <- pars ] polIs = [ i | PolicyParam _ i <- pars ] --- Instantiation is needed for all four kinds. +{-- Instantiation is needed for all four kinds. instantiate :: Data a => [(TypeParam (), TypeArgument ())] -> a -> a instantiate pas = transformBi instT . transformBi instA @@ -1471,7 +1537,12 @@ typs = [ (i,rt) | (TypeParam _ i _, ActualArg _ (ActualType _ rt)) <- pas ] - as = [ (i,n) | (ActorParam _ i, ActualArg _ (ActualActor _ n )) <- pas ] - ps = [ (i,p) | (PolicyParam _ i, ActualArg _ (ActualPolicy _ p )) <- pas ] + as = [ (i,e) | (ActorParam _ i, ActualArg _ (ActualExp _ e )) <- pas ] + ++ [ (i, ExpName () $ Name () $ fst $ unzip iargs) + | (ActorParam _ i, ActualArg _ (ActualType _ (ClassRefType _ (ClassType _ iargs))) <- pas ] + ps = [ (i,e) | (PolicyParam _ i, ActualArg _ (ActualExp _ e )) <- pas ] + ++ [ (i, ExpName () $ Name () $ fst $ unzip iargs) + | (PolicyParam _ i, ActualArg _ (ActualType _ (ClassRefType _ (ClassType _ iargs))) <- pas ] lps = [ (i,le) | (LockStateParam _ i, ActualArg _ (ActualLockState _ le)) <- pas ] +-}
src/Language/Java/Paragon/Pretty.hs view
@@ -350,6 +350,7 @@ pretty (ForLocalVars _ mods t vds) = hsep $ map pretty mods ++ pretty t: punctuate comma (map pretty vds) + pretty (ForInitExps _ es) = hsep $ punctuate comma $ map pretty es ----------------------------------------------------------------------- @@ -562,10 +563,10 @@ pretty (Wildcard _ mBound) = char '?' <+> maybePP mBound instance Pretty (NonWildTypeArgument a) where + pretty (ActualName _ n) = pretty n pretty (ActualType _ t) = pretty t - pretty (ActualPolicy _ p) = text "policy" <+> pretty p - pretty (ActualActor _ n) = text "actor" <+> pretty n - pretty (ActualLockState _ ls) = text "lock[]" <+> ppArgs ls -- HACK ALERT + pretty (ActualExp _ e) = pretty e + pretty (ActualLockState _ ls) = {- text "lock[]" <+> -} ppArgs ls -- HACK ALERT instance Pretty (WildcardBound a) where pretty (ExtendsBound _ rt) = text "extends" <+> pretty rt
src/Language/Java/Paragon/Syntax.hs view
@@ -490,9 +490,9 @@ deriving (Eq,Ord,Show,Typeable,Data,Functor) data NonWildTypeArgument a - = ActualType a (RefType a) - | ActualPolicy a (Policy a) - | ActualActor a (Name a) + = ActualName a (Name a) -- Can mean a type or an exp + | ActualType a (RefType a) + | ActualExp a (Exp a) -- Constrained to argExp | ActualLockState a [Lock a] deriving (Eq,Ord,Show,Typeable,Data,Functor)
src/Language/Java/Paragon/TypeCheck.hs view
@@ -3,6 +3,7 @@ import Language.Java.Paragon.Syntax import Language.Java.Paragon.Parser import Language.Java.Paragon.Pretty+import Language.Java.Paragon.Verbosity import Language.Java.Paragon.TypeCheck.Actors import Language.Java.Paragon.TypeCheck.Constraints@@ -35,15 +36,16 @@ typeCheck :: DirectoryPath -> DirectoryPath -> CompilationUnit () -> IO (CompilationUnit ()) typeCheck currentDir piDir ast@(CompilationUnit _ pkg imps [td]) = do+ finePrint $ "Current dir: " ++ show currentDir let (skoTd, skoTy) = skolemTypeDecl td e <- runTcCont skoTy $ do withEnvFromImps piDir "" allImps $ do- --debug "Import env setup"+ debug "Import env setup" withEnvFromImp currentDir (tdIdentStr skoTd) thisPackage $ do- --debug "TypeMap completed"+ debug "Initial type map completed" tm <- getTypeMap- --debug $ "TypeMap: " ++ show tm- withExpandedNames skoTd $ \fullTd -> do+ debug $ "Initial type map: " ++ show tm+ withExpandedNames piDir allImps skoTd $ \fullTd -> do --debug $ "Full AST:\n" ++ prettyPrint fullTd typeCheckTd fullTd -- debug $ "Type checking completed!"@@ -55,12 +57,13 @@ where allImps = defaultImportDecls ++ imps -withExpandedNames :: TypeDecl () -> (TypeDecl () -> TcCont r a) -> TcCont r a-withExpandedNames td tcbaf = do+withExpandedNames :: DirectoryPath -> [ImportDecl ()] -> TypeDecl () -> (TypeDecl () -> TcCont r a) -> TcCont r a+withExpandedNames piDir imps td tcbaf = do+ mNames <- buildExpansionMap piDir imps tm <- getTypeMap --debug $ "TypeMap: " ++ show tm- let mNames = buildExpansionMap tm- fullTd = expandNames mNames td+ -- let mNames = buildExpansionMap tm+ let fullTd = expandNames mNames td --debug $ "ExpansionMap: " ++ show mNames tcbaf fullTd @@ -80,6 +83,41 @@ Nothing -> ct expandCT ct = ct +buildExpansionMap :: DirectoryPath -> [ImportDecl ()] -> TcCont r (Map (Ident ()) [Ident ()])+buildExpansionMap piDir imps = foldM (buildExpMapFromImp piDir) Map.empty imps++buildExpMapFromImp :: DirectoryPath + -> Map (Ident ()) [Ident ()] + -> ImportDecl () + -> TcCont r (Map (Ident ()) [Ident ()])+buildExpMapFromImp piDir em imp@(ImportDecl _ stat (Name _ is) onDemand) = + case (stat, onDemand) of+ (False, False) -> do -- Single-type: import pkg.path.TypeName;+ let relative = pathOf is+ absoluteFile = piDir ++ pSep:relative ++ ".pi"+ className = last is+ checkM (liftIO $ doesFileExist absoluteFile) $+ "Cannot find interface file for import " ++ prettyPrint imp+ return $ Map.insert className is em+ (False, True) -> do -- On-demand package: import pkg.path.*;+ let relative = pathOf is+ absoluteDir = piDir ++ pSep:relative ++ [pSep]+ checkM (liftIO $ doesDirectoryExist absoluteDir) $+ "Cannot find package for import " ++ prettyPrint imp+ names <- liftIO $ getDirectoryContents absoluteDir+ let classNames = + [ Ident () base+ | name <- names+ , let (base, extn) = (takeBaseName name, takeExtension name)+ , extn == ".pi"+ -- , base /= thisStr + ]+ newMap = Map.fromList (zip classNames (map ((is++) . return) classNames))+ return $ Map.union em newMap++ ++{- buildExpansionMap :: TypeMap -> Map (Ident ()) [Ident ()] buildExpansionMap tm = let fs = Map.keys (fields tm)@@ -90,7 +128,7 @@ ptms = map (second buildExpansionMap) pts mps = map (\(i,mp) -> Map.map (i:) mp) ptms in foldl Map.union m1 mps-+-} ------------------------------------------------------------------ -- Implicitly imported core packages -- TODO: Not yet used.@@ -121,6 +159,8 @@ withEnvFromImp :: DirectoryPath -> String -> (ImportDecl ()) -> TcCont r a -> TcCont r a -- import java.*; withEnvFromImp piDir thisStr imp@(ImportDecl _ False (Name _ pkgNames) True) tcba = do+ when (null pkgNames) $+ debug $ "Setting up import from current dir: " ++ show piDir --debug $ "Setting up import of: " ++ prettyPrint (Name pkgNames) let relative = pathOf pkgNames absoluteDir = piDir ++ pSep:relative ++ [pSep]@@ -130,6 +170,7 @@ , let (base, extn) = (takeBaseName name, takeExtension name) , extn == ".pi" , base /= thisStr ]+ debug $ "Found files: " ++ show classPathsAndNames withEnvFromPkg pkgNames classPathsAndNames $ tcba -- import java.TypeName;@@ -141,8 +182,21 @@ pkgNames = init clsPkgName withEnvFromSingleClass pkgNames absoluteFile className $ tcba +-- import static java.TypeName.Ident;+withEnvFromImp piDir _ imp@(ImportDecl _ True (Name _ pathToIdent) False) tcba = do+ error "Single static import not yet supported" +-- import static java.TypeName.*;+withEnvFromImp piDir _ imp@(ImportDecl _ True (Name _ clsPkgName) True) tcba = do+ let relative = pathOf clsPkgName+ absoluteFile = piDir ++ pSep:relative ++ ".pi"+ (Ident _ className) = last clsPkgName+ pkgNames = init clsPkgName+ withEnvFromSingleClass [] absoluteFile className $ tcba+ ++ withEnvFromPkg :: [Ident ()] -> [(FilePath, String)] -> TcCont r a -> TcCont r a withEnvFromPkg [] [] tcba = tcba -- Hack for the "this" package withEnvFromPkg pkgPath [] tcba = do@@ -205,7 +259,7 @@ where spawnActor, evalActor, aliasActor :: ([Modifier ()],VarDecl ()) -> TcCont r a -> TcCont r a spawnActor (ms, VarDecl _ (VarId _ i) _) tcba = do- a <- freshActorId+ a <- freshActorId (prettyPrint i) p <- getReadPolicy ms let vti = VSig actorT p (Static () `elem` ms) (Final () `elem` ms) withTypeMap (\tm -> tm { actors = Map.insert i a (actors tm),@@ -531,13 +585,14 @@ withFoldMap typeCheckLockDecl ls $ tcba typeCheckLockDecl :: MemberDecl () -> TcCont r a -> TcCont r a-typeCheckLockDecl (LockDecl _ ms i mps props) tcba = do-{-- lPol <- getLockPolicy ms- -- TODO: Store lock properties!- let arity = length mps- withTypeMap (\tm -> - tm { lockArities = Map.insert i arity (lockArities tm) }) $ -}- tcba+typeCheckLockDecl (LockDecl _ ms i mps mprops) tcba = do+ lsig <- withErrCtxt ("When checking signature of lock " ++ prettyPrint i ++ ":\n") $ do+ pol <- getLockPolicy ms+-- return $ VSig (lockT []) pol True True+ -- TODO: Check properties!+ return $ LSig pol (length mps)+ withTypeMap (\tm -> tm { locks = Map.insert i lsig (locks tm) }) $+ tcba -- end Locks ---------------------------------------------------------------@@ -670,6 +725,7 @@ ++ concat (intersperse ", " (map prettyPrint fis)) ++ ":\n") $ do -- 1. Check field type ty <- evalSrcType t+ debug $ "Type evaluated to: " ++ show ty -- _ <- lookupTypeOfT ty <$> getTypeMap -- TODO -- 2. Typecheck and evaluate field policy let rPolExps = [ e | Reads _ e <- ms ]@@ -694,6 +750,7 @@ addField vti (VarDecl _ (VarId _ i) _) = withTypeMap $ \tm -> tm { fields = Map.insert i vti (fields tm) }+ addField _ vd = \_ -> fail $ "Deprecated declaration: " ++ prettyPrint vd -- Methods typeCheckSignature st md@(MethodDecl _ ms tps retT i ps exns mb) tcba@@ -705,12 +762,13 @@ withFoldMap withTypeParam tps $ do -- 1. Check return type ty <- evalReturnType retT+ {- We've checked this in evalReturnType already when (isRefType ty) $ do mTm <- lookupTypeOfT ty <$> getTypeMap case mTm of Just _ -> return () Nothing -> fail $ "Unknown type: " ++ prettyPrint ty-+ -} -- 2. Typecheck and evaluate policy modifiers withFoldMap withParam ps $ checkPolicyMods st ms "typeCheckSignature: At most one return/write modifier allowed per method"@@ -768,16 +826,16 @@ withTypeMap (\tm -> tm { constrs = Map.insert pTs (tps,cti) (constrs tm) }) $ tcba --- Locks-typeCheckSignature st ld@(LockDecl _ ms i mps mprops) tcba = do+-- Locks -- already handled+-- typeCheckSignature st ld@(LockDecl _ ms i mps mprops) tcba = tcba --debug $ "typeCheckSignature: " ++ prettyPrint ld- lsig <- withErrCtxt ("When checking signature of lock " ++ prettyPrint i ++ ":\n") $ do- pol <- getLockPolicy ms+-- lsig <- withErrCtxt ("When checking signature of lock " ++ prettyPrint i ++ ":\n") $ do+-- pol <- getLockPolicy ms -- return $ VSig (lockT []) pol True True -- TODO: Check properties!- return $ LSig pol (length mps)- withTypeMap (\tm -> tm { locks = Map.insert i lsig (locks tm) }) $- tcba+-- return $ LSig pol (length mps)+-- withTypeMap (\tm -> tm { locks = Map.insert i lsig (locks tm) }) $+-- tcba typeCheckSignature _ _ tcba = tcba @@ -793,11 +851,11 @@ typeCheckExnSig st (ExceptionSpec _ ms xT) = do withErrCtxt ("When checking signature for declared exception " ++ prettyPrint xT ++ ":\n") $ do ty <- TP.TcRefT <$> evalSrcRefType xT- -- Check that type exists+ {-- Check that type exists - now done in evalSrcRefType mTm <- lookupTypeOfT ty <$> getTypeMap case mTm of Just _ -> return ()- Nothing -> fail $ "Unknown exception type: " ++ prettyPrint ty+ Nothing -> fail $ "Unknown exception type: " ++ prettyPrint ty -} checkPolicyMods st ms "typeCheckSignature: At most one read/write modifier allowed per exception" rPol <- getReadPolicy ms@@ -847,7 +905,7 @@ -- tm <- getTypeMap -- debug $ show tm -- debug $ "typeCheckPolicyMod " ++ show polExp- ((ty, _pol), cs) <- runTc (simpleEnv top) st + ((ty, _pol), cs) <- runTc (simpleEnv top $ "policy modifier " ++ prettyPrint polExp) st (--liftBase (debug "inside runTC") >> tcExp polExp) check (null cs) $ "Internal WTF: typeCheckPolicyMod: Constraints in policy exp?!?"@@ -870,7 +928,7 @@ typeCheckInitDecl :: TcPolicy -> TcState -> Block () -> TcCont r TcState typeCheckInitDecl lim st bl = do tm <- getTypeMap- (st,cs) <- runTc (simpleEnv lim) st $+ (st,cs) <- runTc (simpleEnv lim $ "initializer block") st $ addBranchPCList (Map.keys (fields tm)) $ do tcBlock bl getState@@ -908,10 +966,14 @@ case mInit of Nothing -> return () Just (InitExp _ e) -> do- (_,cs) <- runTc (simpleEnv lim) st $ do+ (_,cs) <- runTc (simpleEnv lim $ "field initializer " ++ prettyPrint e) st $ do (ty, pol) <- tcExp e checkM (liftCont $ ty <: matchTy) $ "typeCheckVarDecl: type mismatch"- constraint_ pol matchPol+ constraint [] pol matchPol $+ "Cannot assign result of expression " ++ prettyPrint e +++ " with policy " ++ prettyPrint pol +++ " to location " ++ prettyPrint i ++ + " with policy " ++ prettyPrint matchPol solve cs Just (InitArray _ arr) -> case mArrayType matchTy of@@ -919,7 +981,7 @@ ++ " of non-array type " ++ prettyPrint matchTy ++ " given literal array initializer" Just (baseTy, pols) -> do- (_,cs) <- runTc (simpleEnv lim) st $+ (_,cs) <- runTc (simpleEnv lim $ "array initializer " ++ prettyPrint arr) st $ tcArrayInit baseTy pols arr solve cs -- _ -> error $ "typeCheckVarDecl: Array syntax not yet supported"@@ -940,15 +1002,16 @@ pars = map fst parVtis exnPols = map (second $ \es -> (exnReads es, exnWrites es)) xSigs exnLMods = map (second exnMods) xSigs- parEnts = [ (VarEntity $ Name () [i], bottom) | i <- pars ]- exnEnts = [ (ExnEntity t, bottom) | t <- map fst xSigs ]- branchMap = Map.insert returnE bottom $ Map.fromList (parEnts ++ exnEnts)+ parEnts = [ (VarEntity $ Name () [i], []) | i <- pars ]+ exnEnts = [ (ExnEntity t, []) | t <- map fst xSigs ]+ branchMap = Map.insert returnE [] $ Map.fromList (parEnts ++ exnEnts)+ writeErr = "body of method " ++ prettyPrint i env = TcEnv { vars = Map.fromList parVtis, lockstate = expLs, returnI = Just (tyRet, pRet), exnsE = Map.fromList exnPols,- branchPCE = (branchMap, pWri)+ branchPCE = (branchMap, [(pWri, writeErr)]) } -- debug $ "Using env: " ++ show env@@ -988,13 +1051,14 @@ fieEnts = concat [ [ThisFieldEntity i,VarEntity (Name () [i])] | (i, VSig _ _ False _) <- Map.assocs (fields tm) ] --debug $ "fieEnts: " ++ show fieEnts- let branchMap = Map.fromList $ zip (parEnts ++ exnEnts ++ fieEnts) (repeat bottom)+ let branchMap = Map.fromList $ zip (parEnts ++ exnEnts ++ fieEnts) (repeat [])+ writeErr = "body of constructor " ++ prettyPrint ci env = TcEnv { vars = Map.fromList parVtis, lockstate = expLs, returnI = error "Cannot return from constructor", exnsE = Map.fromList exnPols,- branchPCE = (branchMap, pWri)+ branchPCE = (branchMap, [(pWri, writeErr)]) } --debug $ "Using branch map: " ++ show (branchPCE env)@@ -1088,4 +1152,4 @@ debug :: String -> TcCont r ()-debug str = liftIO $ putStrLn $ "DEBUG: " ++ str+debug str = liftIO $ finePrint $ "DEBUG: " ++ str
src/Language/Java/Paragon/TypeCheck/Actors.hs view
@@ -17,7 +17,7 @@ -- which actor(s) it can represent, we list that. -- Otherwise an empty list means it could be an alias -- of any other actor.-data ActorId = Fresh Int | Alias Int | ActorTPVar (Ident ())+data ActorId = Fresh Int String | Alias Int | ActorTPVar (Ident ()) deriving (Show, Eq, Ord, Data, Typeable) infix 5 `unifies`, `unify`@@ -25,7 +25,7 @@ -- Precondition: No ActorTPVars unifies :: ActorId -> ActorId -> Bool -- If we have the exact (fresh) ids, we can tell exactly-unifies (Fresh x) (Fresh y) = x == y+unifies (Fresh x _) (Fresh y _) = x == y unifies _ _ = True -- If either side is an alias, check if it could represent the fresh side. --unifies (Alias x xs) (Fresh y) = null xs || y `elem` xs@@ -47,8 +47,8 @@ reprs (Alias x xs) = x:xs -} getId :: ActorId -> Int-getId (Fresh x) = x-getId (Alias x) = x+getId (Fresh x _) = x+getId (Alias x ) = x {- reprName :: ActorId -> Name
src/Language/Java/Paragon/TypeCheck/Constraints.hs view
@@ -7,5 +7,7 @@ data Constraint = LRT TcPolicyRec TcPolicy TcPolicy deriving Show -solve :: [Constraint] -> TcCont r ()+type ConstraintWMsg = (Constraint, String)++solve :: [ConstraintWMsg] -> TcCont r () solve cs = liftIO $ mapM_ print cs -- DEBUG
src/Language/Java/Paragon/TypeCheck/Containment.hs view
@@ -44,7 +44,7 @@ SubstM tau maxID = groundSubst m d (TcClause ruleHead ruleBody) = d -- include facts to database that all concrete values are actors: - allAreActors = map (\x -> TcAtom (Name () [Ident () actorAtomString]) [TcActor (Fresh x)]) [0..maxID] + allAreActors = map (\x -> TcAtom (Name () [Ident () actorAtomString]) [TcActor (Fresh x $ "#"++show x)]) [0..maxID] -- For joins and meets, we want to try all the candidates. -- We have that @@ -176,7 +176,7 @@ where rh = aliasToFreshAtom ruleHead rb = map aliasToFreshAtom ruleBody aliasToFreshAtom (TcAtom name actors) = TcAtom name (map aliasToFreshActor actors) - aliasToFreshActor (TcActor (Alias i)) = TcActor (Fresh i) + aliasToFreshActor (TcActor (Alias i)) = TcActor (Fresh i $ "#"++show i) aliasToFreshActor x = x -- Returns the highest integer found as actorID @@ -185,8 +185,8 @@ where h = getHeighestActorId ruleHead b = foldl (\t atom -> max (getHeighestActorId atom) t) 0 ruleBody getHeighestActorId (TcAtom name actors) = foldl (\t actor -> max (acc actor) t ) 0 actors - acc (TcActor (Fresh i)) = i - acc _ = 0 + acc (TcActor (Fresh i _)) = i + acc _ = 0 -- Returns an extended substitution mapping all variables in TcAtom -- to fresh constants not occurring in the first two arguments @@ -198,7 +198,7 @@ freshSubstActor sub@(SubstM mapping maxId) (TcVar id) = case lookupSubst id mapping of Just _ -> sub -- already mapped to a constant - Nothing -> SubstM (add mapping id (TcActor (Fresh (maxId + 1)))) (maxId + 1) + Nothing -> SubstM (add mapping id (TcActor (Fresh (maxId + 1) $ "#"++show (maxId + 1)))) (maxId + 1) freshSubstActor sub _ = sub
src/Language/Java/Paragon/TypeCheck/Monad.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE TupleSections #-} module Language.Java.Paragon.TypeCheck.Monad ( check, checkM, ignore, orElse, maybeM,@@ -10,7 +11,7 @@ lookupFieldT, lookupMethod, lookupMethodT, lookupConstr, - lookupLockArity, + lookupLock, lookupExn, registerExn, registerExns, extendLockEnv,@@ -29,12 +30,14 @@ activateExns, deactivateExn, getExnState, mergeActiveExnStates, useExnState, + getCurrentPC,+ getCurrentLockState, applyLockMods, openLock, closeLock, newMetaPolVar, - constraint, constraint_, constraintLS,+ constraint, constraintPC, constraintLS, exnConsistent, extendTypeMapP, extendTypeMapT, lookupPkgTypeMap,@@ -47,7 +50,8 @@ getReadPolicy, getWritePolicy, getLockPolicy, getParamPolicy, getReturnPolicy, - fromSrcType, (<:),+ --fromSrcType, + (<:), evalPolicy, evalPolicyExp, evalLock, evalActor,@@ -63,6 +67,7 @@ import Language.Java.Paragon.Syntax import Language.Java.Paragon.Pretty+import Language.Java.Paragon.Verbosity --import Language.Java.Paragon.TypeCheck.Monad.TcBase import Language.Java.Paragon.TypeCheck.Monad.TcCont@@ -86,9 +91,11 @@ import Data.IORef import Data.List (union, intersperse) -debug str = liftIO $ putStrLn $ "DEBUG: " ++ str+debug str = liftIO $ finePrint $ "DEBUG: " ++ str+-- debug _ = return () debugTc = liftCont . debug + -------------------------------------------- -- -- -- Monad-independent helpers --@@ -188,13 +195,16 @@ _ -> do -- There's more, so the variable is -- being dereferenced- let mTyTm = lookupTypeOfT ty tm- case mTyTm of- Just tyTm -> return (Just tyTm, ty, p, is)- Nothing -> fail $ "Trying to dereference variable "- ++ prettyPrint i ++- " but its type " ++ prettyPrint ty ++- " is not a (known) object type"+ let eTyTm = lookupTypeOfT ty tm+ case eTyTm of+ Right tyTm -> return (Just tyTm, ty, p, is)+ Left Nothing -> + fail $ "Trying to dereference variable "+ ++ prettyPrint i +++ " but its type " ++ prettyPrint ty +++ " is not a (known) object type"+ Left (Just err) -> fail err+ case mNewTm of Nothing -> return (ty, pol) -- We're done Just newTm -> aux newTm ty pol rest -- Keep traversing the chain@@ -210,11 +220,12 @@ _ -> do -- There's more, so the field is being dereferenced baseTm <- liftCont getTypeMap case lookupTypeOfT typ baseTm of- Just tyTm -> return $ (Just tyTm, typ, p)- Nothing -> fail $ "Trying to dereference variable "- ++ prettyPrint i ++- " but its type " ++ prettyPrint typ ++- " is not a (known) object type"+ Right tyTm -> return $ (Just tyTm, typ, p)+ Left Nothing -> fail $ "Trying to dereference variable "+ ++ prettyPrint i +++ " but its type " ++ prettyPrint typ +++ " is not a (known) object type"+ Left (Just err) -> fail err Nothing -> case Map.lookup i (locks tm) of Just (LSig pol ar) -> do@@ -248,19 +259,21 @@ <- do varMap <- vars <$> getEnv case Map.lookup i varMap of Just (VSig ty p _ _) -> do- let mTyTm = lookupTypeOfT ty tm- case mTyTm of+ -- debugTc $ "Type found: " ++ prettyPrint ty+ let eTyTm = lookupTypeOfT ty tm+ case eTyTm of -- We found the variable, and it -- has an object type- Just tyTm -> return (Just ty, tyTm, p, is, False)+ Right tyTm -> return (Just ty, tyTm, p, is, False) -- We found the variable, but its -- type is not derefereceable, or -- we don't know about it at all- Nothing -> fail $ "Trying to dereference variable " - ++ prettyPrint nam ++- " but its type "- ++ prettyPrint ty ++- " is not a (known) object type"+ Left Nothing -> fail $ "Trying to dereference variable " + ++ prettyPrint (Name () (init n)) +++ " but its type "+ ++ prettyPrint ty +++ " is not a (known) object type"+ Left (Just err) -> fail err Nothing -> return (Nothing,tm,bottom,n,True) aux mTy newTm allowPkgT pol rest ts @@ -296,12 +309,12 @@ -- field exists, so find its related typemap baseTm <- liftCont getTypeMap case lookupTypeOfT typ baseTm of- Just newTm -> return $ (Just typ, newTm, pol, False)- Nothing -> fail $ "Trying to dereference field "- ++ prettyPrint i ++- maybe "" (\ty -> " of class " ++ prettyPrint ty) mTy- ++ " but its type " ++ prettyPrint typ ++- " is not a (known) object type"+ Right newTm -> return $ (Just typ, newTm, pol, False)+ Left Nothing -> fail $ "Trying to dereference field "+ ++ prettyPrint i +++ maybe "" (\ty -> " of class " ++ prettyPrint ty) mTy+ ++ " but its type " ++ prettyPrint typ +++ " is not a (known) object type" Nothing -> if allowPkgT then case Map.lookup i (pkgsAndTypes tm) of@@ -336,10 +349,11 @@ lookupFieldT :: TcType -> Ident () -> Tc r VarFieldSig lookupFieldT typ i = do check (isRefType typ) $ "Not a reference type: " ++ prettyPrint typ- mATm <- lookupTypeOfT typ <$> liftCont getTypeMap- case mATm of- Nothing -> fail $ "Unknown reference type: " ++ prettyPrint typ- Just aTm -> + eATm <- lookupTypeOfT typ <$> liftCont getTypeMap+ case eATm of+ Left (Just err) -> fail err + Left Nothing -> fail $ "Unknown reference type: " ++ prettyPrint typ+ Right aTm -> case Map.lookup i (fields aTm) of Just vti -> return vti Nothing -> fail $ "Class " ++ prettyPrint typ@@ -348,10 +362,11 @@ lookupMethodT :: TcType -> Ident () -> [TcType] -> Tc r ([TypeParam ()], MethodSig) lookupMethodT typ i pts = do check (isRefType typ) $ "Not a reference type: " ++ prettyPrint typ- mATm <- lookupTypeOfT typ <$> liftCont getTypeMap- case mATm of- Nothing -> fail $ "Unknown reference type: " ++ prettyPrint typ- Just aTm -> + eATm <- lookupTypeOfT typ <$> liftCont getTypeMap+ case eATm of+ Left (Just err) -> fail err + Left Nothing -> fail $ "Unknown reference type: " ++ prettyPrint typ+ Right aTm -> case Map.lookup (i,pts) (methods aTm) of Just pmti -> return pmti Nothing -> fail $ "Class " ++ prettyPrint typ@@ -359,22 +374,24 @@ lookupConstr :: TcClassType -> [TcType] -> Tc r ([TypeParam ()], ConstrSig) lookupConstr ctyp pts = do- mATm <- lookupTypeOfT (clsTypeToType ctyp) <$> liftCont getTypeMap- case mATm of- Nothing -> fail $ "Unknown class type: " ++ prettyPrint ctyp- Just aTm -> + eATm <- lookupTypeOfT (clsTypeToType ctyp) <$> liftCont getTypeMap+ case eATm of+ Left (Just err) -> fail err + Left Nothing -> fail $ "Unknown class type: " ++ prettyPrint ctyp+ Right aTm -> case Map.lookup pts (constrs aTm) of Just pcti -> return pcti Nothing -> fail $ "Class " ++ prettyPrint ctyp ++ " does not have a constructor matching argument types " ++ "(" ++ concat (intersperse ", " (map prettyPrint pts)) ++ ")" -lookupLockArity :: Name () -> Tc r Int-lookupLockArity n = do+lookupLock :: Name () -> Tc r LockSig+lookupLock n = do tm <- liftCont getTypeMap+ -- debugTc $ show tm case lookupNamed locks n tm of Nothing -> fail $ "Unknown lock: " ++ prettyPrint n- Just lsig -> return $ lArity lsig+ Just lsig -> return lsig lookupExn :: TcType -> Tc r (TcPolicy, TcPolicy) lookupExn tyX = do@@ -398,32 +415,38 @@ extendLockEnv locks = withEnv $ \env -> env { lockstate = lockstate env `union` locks } -getBranchPC :: Entity -> Tc r TcPolicy+getBranchPC :: Entity -> Tc r [(TcPolicy, String)] getBranchPC e = do env <- getEnv -- debugTc $ "Env: " ++ show env return $ branchPC (Just e) env -getBranchPC_ :: Tc r TcPolicy+getBranchPC_ :: Tc r [(TcPolicy, String)] getBranchPC_ = do env <- getEnv return $ branchPC Nothing env -extendBranchPC :: TcPolicy -> Tc r a -> Tc r a-extendBranchPC = withEnv . joinBranchPC+extendBranchPC :: TcPolicy -> String -> Tc r a -> Tc r a+extendBranchPC p str = withEnv $ joinBranchPC p str addBranchPCList :: [Ident ()] -> Tc r a -> Tc r a addBranchPCList is = withEnv $ \env -> let (bm, def) = branchPCE env- newBm = foldl (\m i -> Map.insert (VarEntity (Name () [i])) bottom m) bm is+ newBm = foldl (\m i -> Map.insert (VarEntity (Name () [i])) [] m) bm is in env { branchPCE = (newBm, def) } -addBranchPC :: Entity -> TcPolicy -> Tc r a -> Tc r a-addBranchPC ent pol = +addBranchPC :: Entity -> Tc r a -> Tc r a+addBranchPC ent = withEnv $ \env -> let (bm, def) = branchPCE env- newBm = Map.insert ent pol bm+ newBm = Map.insert ent [] bm in env { branchPCE = (newBm, def) } +getCurrentPC :: Entity -> Tc r TcPolicy+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 -> Tc r () setFieldPol i pF = do@@ -477,7 +500,7 @@ newActorId :: Ident () -> Tc r ActorId newActorId i = do - aid <- liftCont freshActorId+ aid <- liftCont $ freshActorId (prettyPrint i) newActorIdWith i aid return aid @@ -488,8 +511,10 @@ return aid -freshActorId, aliasActorId :: TcCont r ActorId-freshActorId = (liftIO . newFresh) =<< getUniqRef+freshActorId :: String -> TcCont r ActorId+freshActorId str = (liftIO . flip newFresh str) =<< getUniqRef++aliasActorId :: TcCont r ActorId aliasActorId = (liftIO . newAlias) =<< getUniqRef @@ -503,7 +528,7 @@ -- Exception tracking -getExnPC :: Tc r TcPolicy+getExnPC :: Tc r [(TcPolicy, String)] getExnPC = exnPC <$> getState throwExn :: ExnType -> TcPolicy -> Tc r ()@@ -583,19 +608,20 @@ -- Working with constraints -- -------------------------------------------- -constraint :: [TcLock] -> TcPolicy -> TcPolicy -> Tc r ()-constraint ls p1 p2 = do -- addConstraint $ LRT ls p1 p2+constraint :: [TcLock] -> TcPolicy -> TcPolicy -> String -> Tc r ()+constraint ls p1 p2 str = do -- addConstraint $ LRT ls p1 p2 g <- getGlobalLockProps case lrt (g `recmeet` rls) p1 p2 of Left b -> do- --debugTc $ "constraint: p1: " ++ show p1- --debugTc $ "constraint: p2: " ++ show p2- check b $ "Cannot solve constraint p <= q where" ++ --show (LRT (g `recmeet` rls) p1 p2)+-- debugTc $ "constraint: p1: " ++ show p1+-- debugTc $ "constraint: p2: " ++ show p2+ check b str {-+ $ "Cannot solve constraint p <= q where" ++ --show (LRT (g `recmeet` rls) p1 p2) "\n* p = " ++ prettyPrint p1 ++ "\n* q = " ++ prettyPrint p2 ++ "\nin the presence of lock state {" ++- concat (intersperse ", " (map prettyPrint ls)) ++ "}"- Right c -> addConstraint c+ concat (intersperse ", " (map prettyPrint ls)) ++ "}" -}+ Right c -> addConstraint c str where rls = locksToRec ls getGlobalLockProps :: Tc r TcPolicyRec@@ -604,24 +630,48 @@ locksToRec :: [TcLock] -> TcPolicyRec locksToRec ls = TcPolicyRec (map (\x -> TcClause x []) (map lockToAtom ls)) -constraint_, constraintLS :: TcPolicy -> TcPolicy -> Tc r ()-constraint_ = constraint []--constraintLS p1 p2 = do+constraintLS :: TcPolicy -> TcPolicy -> String -> Tc r ()+constraintLS p1 p2 str = do l <- getCurrentLockState- constraint l p1 p2+ withErrCtxtTc ("In the context of lock state: " ++ prettyPrint l ++ "\n") $+ constraint l p1 p2 str -exnConsistent :: TcType -> ExnSig -> Tc r ()-exnConsistent exnTy (ExnSig rX wX _) = do+constraintPC :: [(TcPolicy, String)] -> TcPolicy -> (TcPolicy -> String -> String) -> Tc r ()+constraintPC bpcs pW msgf = mapM_ (uncurry $ constraintPC_ pW msgf) bpcs+ where constraintPC_ :: TcPolicy -> (TcPolicy -> String -> String) + -> TcPolicy -> String -> Tc r ()+ -- Don't take lock state into account+ constraintPC_ pW msgf pPC src = constraint [] pPC pW (msgf pPC src)+ +++exnConsistent :: Either (Name ()) (ClassType ()) -> TcType -> ExnSig -> Tc r ()+exnConsistent caller exnTy (ExnSig 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_ wX wE- constraint_ rE rX+ constraint [] wX wE $+ "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 [] rE rX $ -- 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 less restrictive than " ++ + prettyPrint rE + -------------------------------------------- -- Working with typemaps -- --------------------------------------------@@ -653,9 +703,10 @@ lookupPkgTypeMap :: [Ident ()] -> TcCont r TypeMap lookupPkgTypeMap is = do- mTm <- lookupTypeOfN (Name () is) <$> getTypeMap- maybe (fail $ "Unknown package: " ++ prettyPrint (Name () is))- return mTm+ eTm <- lookupTypeOfN (Name () is) <$> getTypeMap+ case eTm of+ Right tm -> return tm+ Left _ -> fail $ "Unknown package: " ++ prettyPrint (Name () is) ------------------------------------------------------------------- -- Evaluating types@@ -677,18 +728,64 @@ evalSrcRefType (ClassRefType _ ct) = TcClsRefT <$> evalSrcClsType ct evalSrcClsType :: ClassType () -> TcCont r TcClassType-evalSrcClsType (ClassType _ iArgs) = - TcClassT <$> mapM (\(i,tas) -> (\ts -> (i, ts)) <$> mapM evalSrcTypeArg tas) iArgs+evalSrcClsType ct@(ClassType _ iArgs) = do+ debug $ "Evaluating class type: " ++ show ct+ baseTm <- getTypeMap+ debug $ "Current type map: " ++ show baseTm+ TcClassT <$> aux baseTm [] iArgs++ where aux :: TypeMap -- Typemap of outer type (or top-level)+ -> [(Ident (), [TcTypeArg])] -- Accumulated type (reversed)+ -> [(Ident (), [TypeArgument ()])] -- Type to traverse+ -> TcCont r [(Ident (), [TcTypeArg])] -- Result (re-reversed)+ aux _ accTy [] = return $ reverse accTy+ aux tm accTy ((i,tas):rest) = do+ debug $ "Looking up type: " ++ show i+ debug $ "Types field: " ++ show (types tm)+ (newTm, tArgs) <- + case Map.lookup i (types tm) of+ Just (pars, tsig) -> do+ debug $ "Type found"+ tArgs <- mapM (uncurry evalSrcTypeArg) (zip pars tas)+ debug "Type arguments evaluated"+ return (instantiate (zip pars tArgs) (tMembers tsig), tArgs)+ Nothing -> case Map.lookup i (packages tm) of+ Just tm -> do check (null tas) $ + "Packages cannot have type arguments"+ return (tm, [])+ Nothing -> fail $ "Unknown type: " ++ prettyPrint i+ debug $ "Rest of type to evaluate: " ++ show rest+ aux newTm ((i,tArgs):accTy) rest++-- TcClassT <$> mapM (\(i,tas) -> (\ts -> (i, ts)) <$> mapM evalSrcTypeArg tas) iArgs -evalSrcTypeArg :: TypeArgument () -> TcCont r TcTypeArg-evalSrcTypeArg (ActualArg _ a) = evalSrcNWTypeArg a-evalSrcTypeArg _ = fail "evalSrcTypeArg: Wildcards not yet supported"+evalSrcTypeArg :: TypeParam () -> TypeArgument () -> TcCont r TcTypeArg+evalSrcTypeArg tp (ActualArg _ a) = evalSrcNWTypeArg tp a+evalSrcTypeArg _ _ = fail "evalSrcTypeArg: Wildcards not yet supported" -evalSrcNWTypeArg :: NonWildTypeArgument () -> TcCont r TcTypeArg+evalSrcNWTypeArg :: TypeParam () -> NonWildTypeArgument () -> TcCont r TcTypeArg+-- Types may be names or types -- TODO: Check bounds+evalSrcNWTypeArg tp@(TypeParam {}) (ActualName _ (Name _ is)) = do+ TcActualType . TcClsRefT <$> evalSrcClsType (ClassType () $ map (,[]) is)+evalSrcNWTypeArg (TypeParam {}) (ActualType _ rt) = TcActualType <$> evalSrcRefType rt+-- Actors may only be names -- TODO: must be final+evalSrcNWTypeArg (ActorParam {}) (ActualName _ n) = TcActualActor <$> evalActorId n+-- Policies may be names, or special expressions -- TODO: names must be final+evalSrcNWTypeArg (PolicyParam {}) (ActualName _ n) = TcActualPolicy <$> evalPolicy (ExpName () n)+evalSrcNWTypeArg (PolicyParam {}) (ActualExp _ e) = TcActualPolicy <$> evalPolicy e+-- Lock states must be locks+evalSrcNWTypeArg (LockStateParam {}) (ActualLockState _ ls) = TcActualLockState <$> mapM evalLock ls++evalSrcNWTypeArg tp nwta = + fail $ "Trying to instantiate type parameter " ++ prettyPrint tp +++ " with incompatible type argument " ++ prettyPrint nwta++{- evalSrcNWTypeArg (ActualType _ rt) = TcActualType <$> evalSrcRefType rt evalSrcNWTypeArg (ActualPolicy _ p) = TcActualPolicy <$> evalPolicy p evalSrcNWTypeArg (ActualActor _ n) = TcActualActor <$> evalActorId n evalSrcNWTypeArg (ActualLockState _ ls) = TcActualLockState <$> mapM evalLock ls+-} evalPolicy :: Exp () -> TcCont r TcPolicy evalPolicy e = case e of@@ -762,7 +859,7 @@ Nothing -> fail $ "getActor: No such actor: " ++ prettyPrint n getActor (ActorTypeVar _ i) = return $ ActorTPVar i --- From source+{-- From source fromSrcType :: TypeMap -> Type () -> TcType fromSrcType tm (PrimType _ pt) = TcPrimT pt@@ -826,6 +923,7 @@ fromSrcAtom :: TypeMap -> Atom () -> TcAtom fromSrcAtom tm (Atom _ n as) = TcAtom n $ map (fromSrcActor tm) as +-} ------------------------------------------------------------------------------------- getReadPolicy, getWritePolicy, getLockPolicy :: [Modifier ()] -> TcCont r TcPolicy
src/Language/Java/Paragon/TypeCheck/Monad/TcMonad.hs view
@@ -27,9 +27,9 @@ -- and a writer for constraints newtype Tc r a =- Tc (TcEnv -> TcState -> TcCont r (a, TcState, [Constraint]))+ Tc (TcEnv -> TcState -> TcCont r (a, TcState, [ConstraintWMsg])) -runTc :: TcEnv -> TcState -> Tc r a -> TcCont r (a, [Constraint])+runTc :: TcEnv -> TcState -> Tc r a -> TcCont r (a, [ConstraintWMsg]) runTc env state (Tc f) = do (a,_,cs) <- f env state return (a, cs)@@ -93,6 +93,11 @@ a <- tcba return (a, s, []) +withErrCtxtTc :: String -> Tc r a -> Tc r a+withErrCtxtTc str (Tc f) = Tc $ \e s -> withErrCtxt str (f e s)+ ++ -- Running in parallel infix 1 ||| (|||) :: Tc r a -> Tc r b -> Tc r (a,b)@@ -135,6 +140,6 @@ -- Constraints -addConstraint :: Constraint -> Tc r ()-addConstraint c = Tc (\_ s -> return ((), s, [c]))+addConstraint :: Constraint -> String -> Tc r ()+addConstraint c str = Tc (\_ s -> return ((), s, [(c,str)]))
src/Language/Java/Paragon/TypeCheck/TcEnv.hs view
@@ -2,6 +2,7 @@ module Language.Java.Paragon.TypeCheck.TcEnv where import Language.Java.Paragon.Syntax+import Language.Java.Paragon.Pretty import Language.Java.Paragon.TypeCheck.Actors import Language.Java.Paragon.TypeCheck.Policy@@ -19,6 +20,8 @@ import Data.Generics (Data(..),Typeable(..)) #endif +import Debug.Trace+ type Map = Map.Map data TypeMap = TypeMap {@@ -70,20 +73,21 @@ lockstate :: [TcLock], returnI :: Maybe (TcType, TcPolicy), exnsE :: Map TcType (TcPolicy, TcPolicy),- branchPCE :: (Map Entity TcPolicy, TcPolicy)+ branchPCE :: (Map Entity [(TcPolicy, String)], [(TcPolicy, String)]) } deriving (Show, Data, Typeable) -- Env to use when typechecking expressions not inside method -- bodies, e.g. in field initializers and policy modifiers-simpleEnv :: TcPolicy -> TcEnv-simpleEnv brPol = TcEnv {- vars = Map.empty,- lockstate = [],- returnI = Nothing, -- error "No returns in simple env",- exnsE = Map.empty,- branchPCE = (Map.empty, brPol)- }+simpleEnv :: TcPolicy -> String -> TcEnv+simpleEnv brPol str = + TcEnv {+ vars = Map.empty,+ lockstate = [],+ returnI = Nothing, -- error "No returns in simple env",+ exnsE = Map.empty,+ branchPCE = (Map.empty, [(brPol,str)])+ } data Entity = VarEntity (Name ()) | ThisFieldEntity (Ident ())@@ -174,10 +178,10 @@ instT rt = rt instA :: ActorId -> ActorId-{- instA av@(ActorTPVar i) =+ instA av@(ActorTPVar i) = case lookup i as of Just a -> a- Nothing -> av -}+ Nothing -> av instA a = a instP :: TcPolicy -> TcPolicy@@ -208,66 +212,79 @@ -- Working with the branchPC -- -------------------------------------- -branchPC :: Maybe Entity -> TcEnv -> TcPolicy+branchPC :: Maybe Entity -> TcEnv -> [(TcPolicy, String)] branchPC men (TcEnv { branchPCE = (bm, def) }) = flip (maybe def) men $ \en -> maybe def id (Map.lookup en bm) -joinBranchPC :: TcPolicy -> TcEnv -> TcEnv-joinBranchPC p env = let (bm, def) = branchPCE env- in env { branchPCE = (Map.map (`join` p) bm, def `join` p) }+joinBranchPC :: TcPolicy -> String -> TcEnv -> TcEnv+joinBranchPC p str env = let (bm, def) = branchPCE env+ in env { branchPCE = (Map.map ((p, str):) bm, (p,str):def) } -------------------------------------- -- Working with the lookups -- -------------------------------------- lookupNamed :: (TypeMap -> Map (Ident ()) a) -> Name () -> TypeMap -> Maybe a-lookupNamed recf (Name _ is) tm =- let mActualTm = lookupTypeOfN (Name () $ init is) tm- in maybe Nothing (Map.lookup (last is) . recf) mActualTm+lookupNamed recf nam@(Name _ is) tm =+ case lookupTypeOfN (Name () $ init is) tm of+ Right actualTm -> Map.lookup (last is) (recf actualTm)+ Left err -> Nothing lookupNamedMethod :: Name () -> [TcType] -> TypeMap -> Maybe ([TypeParam ()],MethodSig) lookupNamedMethod (Name _ is) ts tm = - let mActualTm = lookupTypeOfN (Name () $ init is) tm- in maybe Nothing (Map.lookup (last is, ts) . methods) mActualTm+ case lookupTypeOfN (Name () $ init is) tm of+ Right actualTm -> Map.lookup (last is, ts) (methods actualTm)+ Left err -> Nothing pkgsAndTypes :: TypeMap -> Map (Ident ()) TypeMap pkgsAndTypes tm = Map.union (packages tm) -- disregard type parameters (Map.map (tMembers . snd) $ types tm) -lookupTypeOfN :: Name () -> TypeMap -> Maybe TypeMap-lookupTypeOfN (Name _ is) tm = aux is (Just tm) tm- where aux :: [Ident ()] -> Maybe TypeMap -> TypeMap -> Maybe TypeMap- aux _ Nothing _ = Nothing- aux [] mtm _ = mtm- aux (i:is) (Just tm) baseTm =+lookupTypeOfN :: Name () -> TypeMap -> Either (Maybe String) TypeMap+lookupTypeOfN nam@(Name _ is) tm = aux is (Right tm) tm+ where aux :: [Ident ()] + -> Either (Maybe String) TypeMap + -> TypeMap + -> Either (Maybe String) TypeMap+ aux _ err@(Left _) _ = err+ aux [] etm _ = etm+ aux (i:is) (Right tm) baseTm = let mNewTm = case Map.lookup i (fields tm) of Just (VSig typ _ _ _) -> lookupTypeOfT typ baseTm Nothing -> case Map.lookup i (pkgsAndTypes tm) of- Just aTm -> Just aTm- Nothing -> Nothing -- error "lookupTypeOfN: No such name"+ Just aTm -> Right aTm+ Nothing -> Left Nothing -- $ "Unknown name: " ++ prettyPrint nam in aux is mNewTm baseTm -lookupTypeOfT :: TcType -> TypeMap -> Maybe TypeMap+lookupTypeOfT :: TcType -> TypeMap -> Either (Maybe String) TypeMap lookupTypeOfT (TcRefT refT) = lookupTypeOfT' refT-lookupTypeOfT t = const Nothing -- error $ "lookupTypeOfT: Unexpected type: " ++ show t+lookupTypeOfT t = const $ Left Nothing -lookupTypeOfT' :: TcRefType -> TypeMap -> Maybe TypeMap-lookupTypeOfT' (TcClsRefT (TcClassT iargs)) tm = aux iargs (Just tm)- where aux :: [(Ident (), [TcTypeArg])] -> Maybe TypeMap -> Maybe TypeMap- aux _ Nothing = Nothing- aux [] mtm = mtm- aux ((i, args):iargs) (Just tm) =- let mNewTm =+lookupTypeOfT' :: TcRefType -> TypeMap -> Either (Maybe String) TypeMap+lookupTypeOfT' (TcClsRefT (TcClassT iargs)) tm = aux iargs (Right tm)+ where aux :: [(Ident (), [TcTypeArg])] + -> Either (Maybe String) TypeMap + -> Either (Maybe String) TypeMap+ aux _ err@(Left _) = err+ aux [] etm = etm+ aux ((i, args):iargs) (Right tm) = -- traceShow args $+ let eNewTm = case Map.lookup i (types tm) of- Just (pars, tsig) -> Just $ instantiate (zip pars args) (tMembers tsig)+ Just (pars, tsig) -> + if length pars == length args+ then Right $ instantiate (zip pars args) (tMembers tsig)+ else Left $ Just $ + "Wrong number of type arguments in class type.\n" +++ "Type " ++ prettyPrint i ++ " expects " ++ show (length pars) +++ " arguments but has been given " ++ show (length args) Nothing -> case Map.lookup i (packages tm) of- Just tm -> Just tm- Nothing -> Nothing -- error $ "lookupTypeOfT: No such type: " ++ show i- in aux iargs mNewTm+ Just tm -> Right tm+ Nothing -> Left Nothing -- $ "Unknown type : " ++ prettyPrint i+ in aux iargs eNewTm -lookupTypeOfT' (TcArrayT ty pol) _ = Just $ hardCodedArrayTM ty pol+lookupTypeOfT' (TcArrayT ty pol) _ = Right $ hardCodedArrayTM ty pol -- TODO: Insert array support
src/Language/Java/Paragon/TypeCheck/TcExp.hs view
@@ -38,7 +38,8 @@ -- Checking expressions -- ----------------------------------- -debugTc str = liftCont $ liftIO $ putStrLn $ "DEBUG: Tc: " ++ str+--debugTc str = liftCont $ liftIO $ putStrLn $ "DEBUG: Tc: " ++ str+debugTc _ = return () tcExp :: Exp () -> Tc r (TcType, TcPolicy) @@ -76,28 +77,42 @@ return (ty, pol) -- Rule VARASS/FIELDASS-tcExp (Assign _ lhs op rhs) = do-- (tyV, pV, mtyO, mpO, mEnt, mN) <- +tcExp ex@(Assign _ lhs op rhs) = do+ debugTc $ prettyPrint ex+ (tyV, pV, mtyO, mEnt, mN) <- case lhs of NameLhs _ n -> do let (mo,f) = splitName n -- TODO: This is bogus case mo of Nothing -> do -- VARASS (tyV, pV) <- lookupVar f- return (tyV, pV, Nothing, Nothing, Just (varE n), Just n)+ return (tyV, pV, Nothing, Just (varE n), Just n) Just o -> do -- FIELDASS (tyO,pO) <- lookupVar o let (Name _ [i]) = f (VSig tyF pF _ _) <- lookupFieldT tyO i- return (tyF, pF, Just tyO, Just pO, Just (varE n), Just n)+ constraint [] pO pF $ + "Cannot update field " ++ prettyPrint i ++ " of object " +++ prettyPrint o ++ + ": 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) FieldLhs _ (PrimaryFieldAccess _ e fi) -> do (tyE, pE) <- tcExp e (VSig tyF pF _ _) <- lookupFieldT tyE fi let eEnt = case e of This _ -> Just $ thisFE fi _ -> Nothing- return (tyF, pF, Just tyE, Just pE, eEnt, Nothing)+ 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) ArrayLhs _ (ArrayIndex _ arrE iE) -> do (tyA, pA) <- tcExp arrE case tyA of@@ -106,8 +121,22 @@ check (isIntConvertible tyI) $ "Non-integral expression of type " ++ prettyPrint tyI ++ " used as array index expression"- constraintLS pI pA- return (tyElem, pElem, Just tyA, Just pA, Nothing, Nothing)+ 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) _ -> fail $ "Cannot index non-array expression " ++ prettyPrint arrE ++ " of type " ++ prettyPrint tyA@@ -122,17 +151,27 @@ checkM (liftCont $ tyRhs <: tyV) $ "Type mismatch: " ++ prettyPrint tyRhs ++ " <=> " ++ prettyPrint tyV -- Check: E[branchPC](n) <= pV- bpc <- maybe getBranchPC_ getBranchPC mEnt-- -- debugTc $ "BPC: " ++ prettyPrint bpc- constraint_ bpc pV+ 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- epc <- getExnPC- constraint_ epc 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+ 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)+-- 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@@ -156,25 +195,48 @@ -- END DEBUG (tysArgs, psArgs) <- unzip <$> mapM tcExp args (tps,genCti) <- lookupConstr tyT tysArgs- tArgs <- liftCont $ mapM evalSrcTypeArg tas+ -- 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 <- liftCont $ mapM (uncurry evalSrcTypeArg) (zip tps tas) -- tm <- liftCont getTypeMap let cti = instantiate (zip tps tArgs) genCti let (CSig psPars pW lExp lMods exns) = cti -- Check lockstates l <- getCurrentLockState- check (null (lExp \\ l)) $ "Lockstate too weak"+ check (null (lExp \\ l)) $ + "Lockstate too weak when calling constructor " ++ prettyPrint ct ++ ":\n" ++ + "Required lock state: " ++ prettyPrint lExp ++ "\n" +++ "Current lock state: " ++ prettyPrint l -- Check argument constraints- mapM_ (uncurry (constraint l)) (zip psArgs psPars)+ mapM_ (\(arg,argP,parP) -> + constraintLS argP parP $+ "Constructor applied to argument with too restrictive policy:\n" ++ + "Constructor expression: " ++ prettyPrint e ++ "\n" +++ "Argument: " ++ prettyPrint arg +++ " with policy: " ++ prettyPrint argP +++ "Declared policy bound: " ++ prettyPrint parP+ ) (zip3 args psArgs psPars) -- Check E[branchPC](*) <= pW- bpc <- getBranchPC_- constraint_ bpc pW+ bpcs <- getBranchPC_+ constraintPC bpcs pW $ \p src ->+ "Constructor " ++ prettyPrint ct ++ " with declared write effect " ++ prettyPrint pW +++ " not allowed in " ++ src +++ " with write effect bound " ++ prettyPrint p -- Check exnPC(S) <= pW epc <- getExnPC- constraint_ epc pW+ constraintPC epc pW $ \p src ->+ "Constructor " ++ prettyPrint ct ++ " 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) exns+ mapM (uncurry $ exnConsistent (Right ct)) exns -- Fix outgoing state let exns' = map (first ExnType) exns@@ -188,7 +250,7 @@ tcExp (Cond _ c e1 e2) = do (tyC, pC) <- tcExp c checkM (liftCont $ tyC <: booleanT) $ "Cannot convert type to boolean"- extendBranchPC pC $ do+ extendBranchPC pC ("conditional expression dependent on expression " ++ prettyPrint c) $ do ((ty1, p1), (ty2, p2)) <- (maybeM (mLocks tyC) (\ls -> applyLockMods ([], ls)) >> tcExp e1) ||| tcExp e2 check (ty1 == ty2) $ "Types of branches don't match"@@ -292,7 +354,11 @@ (tyE,pE) <- tcExp e check (isIntConvertible tyE) $ nonIntErr tyE -- Each dimexpr must satisfy the policy of the outer dim- constraintLS pE pPrev+ 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:acc) emps pNext @@ -322,8 +388,8 @@ check (isIntConvertible tyI) $ "Non-integral expression of type " ++ prettyPrint tyI ++ " used as array index expression"- constraintLS pI pA- return (tyElem, pElem `join` pA)+-- constraintLS pI pA $ " " -- Not true: pI just adds to the outgoing level+ return (tyElem, pElem `join` pA `join` pI) _ -> fail $ "Cannot index non-array expression " ++ prettyPrint arrE ++ " of type " ++ prettyPrint tyA@@ -337,7 +403,12 @@ tcArrayInit :: TcType -> [TcPolicy] -> ArrayInit () -> Tc r () tcArrayInit baseType (pol1:pols) (ArrayInit _ inits) = do ps <- mapM (tcVarInit baseType pols) inits- mapM_ (\p -> constraintLS p pol1) ps+ 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) tcArrayInit _ [] _ = fail $ "Array initializer has too many dimensions" tcVarInit :: TcType -> [TcPolicy] -> VarInit () -> Tc r TcPolicy@@ -382,43 +453,63 @@ tcMethodInv :: MethodInvocation () -> Tc r (TcType, TcPolicy) tcMethodInv mi = do- --debugTc $ "tcMethodInv: " ++ show mi+ debugTc $ "tcMethodInv: " ++ prettyPrint mi mSigORlSig <- case mi of MethodCall _ n args -> do (tysArgs, psArgs) <- unzip <$> mapM tcExp args eML <- lookupMethod n tysArgs+ debugTc $ show eML case eML of- Left (pPath,_tps,mti) -> return $ Left (mti, psArgs, pPath)+ Left (pPath,_tps,mti) -> return $ Left (n,mti,args, psArgs, pPath) Right (pPath,lsig) -> return $ Right (n,lsig, pPath, tysArgs, psArgs) PrimaryMethodCall _ e tas i args -> do (tyE, pE) <- tcExp e (tysArgs, psArgs) <- unzip <$> mapM tcExp args (tps,genMti) <- lookupMethodT tyE i tysArgs- tArgs <- liftCont $ mapM (evalSrcTypeArg . ActualArg ()) tas+ tArgs <- liftCont $ mapM (uncurry evalSrcTypeArg) $ + zip tps (map (ActualArg ()) tas) let mti = instantiate (zip tps tArgs) genMti- return $ Left (mti, psArgs, pE)+ return $ Left (Name () [i], mti, args, psArgs, pE) _ -> fail $ "tcMethodInv: Unsupported method call" case mSigORlSig of -- This is a method call- Left (mti, psArgs, pE) -> do+ Left (n, mti, args, psArgs, pE) -> do let (MSig tyR pR psPars pW lExp lMods exns) = mti-+-- debugTc $ "Method call" -- Check lockstates l <- getCurrentLockState- check (null (lExp \\ l)) $ "Lockstate too weak: " ++ "(" ++ show lExp ++ ", " ++ show l ++ ")"+ 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_ (uncurry (constraint l)) (zip psArgs psPars)+ 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)+-- mapM_ (uncurry (constraint l)) (zip psArgs psPars)+-- debugTc $ "Arguments checked" -- Check E[branchPC](*) <= pW- bpc <- getBranchPC_- constraint_ bpc 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- constraint_ epc pW+ 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) exns+ mapM (uncurry $ exnConsistent (Left n)) exns -- Fix outgoing state let exns' = map (first ExnType) exns@@ -466,7 +557,7 @@ tcAtom :: Atom () -> Tc r TcAtom tcAtom (Atom _ n as) = do- ar <- lookupLockArity n+ (LSig _ ar) <- lookupLock n check (length as == ar) $ "Arity mismatch in policy" tcAs <- mapM tcActor as return (TcAtom n tcAs)
src/Language/Java/Paragon/TypeCheck/TcState.hs view
@@ -1,6 +1,8 @@ module Language.Java.Paragon.TypeCheck.TcState where import Language.Java.Paragon.Syntax+import Language.Java.Paragon.Pretty+import Text.PrettyPrint (text) import Language.Java.Paragon.TypeCheck.Policy import Language.Java.Paragon.TypeCheck.Actors@@ -105,5 +107,13 @@ return (ExnPoint st w) -- This should probably be pre-computed each time the map is updated instead-exnPC :: TcState -> TcPolicy-exnPC s = foldl join bottom $ map epWrite $ Map.elems $ exnS s+exnPC :: TcState -> [(TcPolicy, String)]+exnPC s = map (\(tyX,ptX) -> (epWrite ptX, errorSrc tyX)) $ Map.assocs $ exnS s++errorSrc :: ExnType -> String+errorSrc et = "area of influence of " +++ case et of+ ExnBreak -> "a break statement"+ ExnContinue -> "a continue statement"+ ExnReturn -> "a return statement"+ ExnType tX -> "exception " ++ prettyPrint tX
src/Language/Java/Paragon/TypeCheck/TcStmt.hs view
@@ -36,7 +36,7 @@ tcStmt (IfThenElse _ c s1 s2) = do (tyC, pC) <- tcExp c checkM (liftCont $ tyC <: booleanT) $ "Cannot convert type to boolean"- extendBranchPC pC $ do+ extendBranchPC pC ("branch dependent on condition " ++ prettyPrint c) $ do ignore $ (maybeM (mLocks tyC) (\ls -> applyLockMods ([],ls)) >> tcStmt s1) ||| tcStmt s2 -- Rule IFTHEN@@ -47,9 +47,9 @@ s <- getState -- Starting state S (tyC, pC) <- tcExp c check (isBoolConvertible tyC) $ "Cannot convert type to boolean"- extendBranchPC pC $- addBranchPC breakE bottom $- addBranchPC continueE bottom $ + extendBranchPC pC ("loop over condition " ++ prettyPrint c) $+ addBranchPC breakE $+ addBranchPC continueE $ do maybeM (mLocks tyC) (\ls -> applyLockMods ([],ls)) -- First iteration of body tcStmt sBody@@ -81,10 +81,11 @@ check (isBoolConvertible tyC) $ "Test in basic for loop must have a bool-convertible type. \n" ++ "Found type: " ++ prettyPrint tyC- extendBranchPC pC $- addBranchPC breakE bottom $- addBranchPC continueE bottom $ do- do maybeM (mLocks tyC) (\ls -> applyLockMods ([],ls))+ maybe id (\test -> extendBranchPC pC + ("for loop dependent on condition " ++ prettyPrint test)) mTest $+ addBranchPC breakE $+ addBranchPC continueE $ do+ maybeM (mLocks tyC) (\ls -> applyLockMods ([],ls)) -- First iteration of body tcStmt body _ <- maybe (return undefined) (mapM tcExp) mUp@@ -112,17 +113,13 @@ -- Rule BREAK tcStmt (Break _ Nothing) = do- bpc <- getBranchPC breakE- epc <- getExnPC- s <- getState- throwExn ExnBreak (bpc `join` epc)+ pc <- getCurrentPC breakE+ throwExn ExnBreak pc -- Rule CONTINUE tcStmt (Continue _ Nothing) = do- bpc <- getBranchPC continueE- epc <- getExnPC- s <- getState- throwExn ExnContinue (bpc `join` epc)+ pc <- getCurrentPC continueE+ throwExn ExnContinue pc -- Rule RETURNVOID tcStmt (Return _ Nothing) = do@@ -131,10 +128,8 @@ check (pR == top) $ "Internal error: tcStmt: " ++ "void return with non-top return policy should never happen" - bpc <- getBranchPC returnE- epc <- getExnPC- s <- getState- throwExn ExnReturn (bpc `join` epc)+ pc <- getCurrentPC returnE+ throwExn ExnReturn pc -- Rule RETURN tcStmt (Return _ (Just e)) = do@@ -145,15 +140,23 @@ "Expecting type: " ++ prettyPrint tyR -- Check pE <=[L] pR- l <- getCurrentLockState- constraint l pE pR+ constraintLS pE pR $+ "Returned value has too restrictive policy:\n" +++ "Return expression: " ++ prettyPrint e ++ "\n" +++ " with policy: " ++ prettyPrint pE ++ "\n" +++ "Declared policy bound: " ++ prettyPrint pR -- Check E[branchPC](return) <= pR- bpc <- getBranchPC returnE- constraint_ bpc pR+ bpcs <- getBranchPC returnE+ constraintPC bpcs pR $ \p src ->+ "Returning from method, visible at policy " ++ prettyPrint pR +++ ", not allowed in " ++ src +++ " with write effect bound " ++ prettyPrint p -- Check exnPC(S) <= pR epc <- getExnPC- constraint_ epc pR-+ constraintPC epc pR $ \p src ->+ "Returning from method, visible at policy " ++ prettyPrint pR +++ ", not allowed in " ++ src +++ " with write effect bound " ++ prettyPrint p throwExn ExnReturn pR -- Rule THROW@@ -163,14 +166,23 @@ (rX, wX) <- lookupExn tyX -- Check E[branchPC](X) <= E[exns](X)[write] bpc <- getBranchPC (exnE tyX)- constraint_ bpc wX+ constraintPC bpc wX $ \p src ->+ "Exception with write effect " ++ prettyPrint wX ++ + " may not be thrown in " ++ src +++ " with write effect bound " ++ prettyPrint p -- Check exnPC(S) <= E[exns](X)[write] epc <- getExnPC- constraint_ epc wX+ constraintPC epc wX $ \p src ->+ "Exception with write effect " ++ prettyPrint wX ++ + " may not be thrown in " ++ src +++ " with write effect bound " ++ prettyPrint p -- Check pX <=[L] E[exns](X)[read]- l <- getCurrentLockState- constraint l pX rX-+ constraintLS pX rX $+ "Thrown value has too restrictive policy:\n" +++ "Expression thrown: " ++ prettyPrint eX ++ "\n" +++ " of type: " ++ prettyPrint tyX ++ "\n" +++ " with policy: " ++ prettyPrint pX ++ "\n" +++ "Declared exception policy: " ++ prettyPrint rX throwExn (ExnType tyX) wX -- Rule TRYCATCH@@ -179,9 +191,9 @@ tyP <- liftCont $ evalSrcType t -- TODO check tyP <: "Throwable" pR <- liftCont $ getReadPolicy ms -- getParamPolicy i ms- pW <- newMetaPolVar -- \pi, where \pi is fresh- addBranchPC (exnE tyP) bottom $ -- E' = E[branchPC{tyP +-> bottom},- registerExn tyP pR pW $ do -- exns{tyP +-> (pR, \pi)}]+ pW <- newMetaPolVar -- \pi, where \pi is fresh+ addBranchPC (exnE tyP) $ -- E' = E[branchPC{tyP +-> bottom},+ registerExn tyP pR pW $ do -- exns{tyP +-> (pR, \pi)}] tcBlock block extendVarEnv i (VSig tyP pR False (isFinal ms)) $ do -- E* = E[vars{x +-> (tyP, pR)}] msX <- getExnState (ExnType tyP)@@ -216,29 +228,37 @@ -- Rule OPEN -- TODO change the list of actor names to a list of expressions (parser, AST, here) tcStmt (Open _ (Lock _ n as)) = do- arL <- lookupLockArity n- (_,pL) <- lookupVar n+ (LSig pL arL) <- lookupLock n+ -- (_,pL) <- lookupVar n check (length as == arL) $ "Lock " ++ prettyPrint n ++ " expects " ++ show arL ++ " arguments but has been given " ++ show (length as) -- Check pI <=[L] pL- l <- getCurrentLockState psAs <- map snd <$> mapM lookupActorName as- mapM_ (flip (constraint l) pL) psAs+ mapM_ (\(a,pA) -> constraintLS pA pL $ + "Lock " ++ prettyPrint n ++ " with policy " ++ prettyPrint pL +++ " cannot be opened for actor " ++ prettyPrint a +++ " with policy " ++ prettyPrint pA+ ) (zip as psAs) -- Check E[branchPC](L) <= pL bpc <- getBranchPC (lockE n)- constraint_ bpc pL+ constraintPC bpc pL $ \p src ->+ "Opening lock " ++ prettyPrint n ++ " with policy " ++ prettyPrint pL +++ " not allowed in " ++ src +++ " with write effect bound " ++ prettyPrint p -- Check exnPC(S) <= pL epc <- getExnPC- constraint_ epc pL-+ constraintPC epc pL $ \p src ->+ "Opening lock " ++ prettyPrint n ++ " with policy " ++ prettyPrint pL +++ " not allowed in " ++ src +++ " with write effect bound " ++ prettyPrint p aids <- mapM tcActorName as openLock (TcLock n aids) -- Rule CLOSE tcStmt (Close _ (Lock _ n as)) = do- arL <- lookupLockArity n- (_,pL) <- lookupVar n+ (LSig pL arL) <- lookupLock n+-- (_,pL) <- lookupVar n -- LTI arL pL <- lookupLock n check (length as == arL) $ "Lock " ++ prettyPrint n ++ " expects " ++ show arL @@ -246,23 +266,31 @@ -- Check pI <=[L] pL l <- getCurrentLockState psAs <- map snd <$> mapM lookupActorName as- mapM_ (flip (constraint l) pL) psAs+ mapM_ (\(arg,argP) -> constraintLS argP pL $+ "Lock " ++ prettyPrint n ++ " with policy " ++ prettyPrint pL +++ " cannot be closed for actor " ++ prettyPrint arg +++ " with policy " ++ prettyPrint argP+ ) (zip as psAs) -- Check E[branchPC](L) <= pL bpc <- getBranchPC (lockE n)- constraint_ bpc pL+ constraintPC bpc pL $ \p src ->+ "Closing lock " ++ prettyPrint n ++ " with policy " ++ prettyPrint pL +++ " not allowed in " ++ src +++ " with write effect bound " ++ prettyPrint p -- Check exnPC(S) <= pL epc <- getExnPC- constraint_ epc pL-+ constraintPC epc pL $ \p src ->+ "Closing lock " ++ prettyPrint n ++ " with policy " ++ prettyPrint pL +++ " not allowed in " ++ src +++ " with write effect bound " ++ prettyPrint p aids <- mapM tcActorName as closeLock (TcLock n aids) -- Rule OPENIN tcStmt (OpenBlock _ (Lock _ n as) block) = do- arL <- lookupLockArity n- (_,pL) <- lookupVar n+ LSig pL arL <- lookupLock n+ -- (_,pL) <- lookupVar n --debugTc $ "pL: " ++ prettyPrint n ++ ": " ++ show pL--- LTI arL pL <- lookupLock n check (length as == arL) $ "Lock " ++ prettyPrint n ++ " expects " ++ show arL ++ " arguments but has been given " ++ show (length as)@@ -270,7 +298,11 @@ l <- getCurrentLockState psAs <- map snd <$> mapM lookupActorName as --debugTc $ "psAs: " ++ show psAs- mapM_ (flip (constraint l) pL) psAs+ mapM_ (\(arg,argP) -> constraintLS argP pL $+ "Lock " ++ prettyPrint n ++ " with policy " ++ prettyPrint pL +++ " cannot be opened for actor " ++ prettyPrint arg +++ " with policy " ++ prettyPrint argP+ ) (zip as psAs) aids <- mapM tcActorName as extendLockEnv [TcLock n aids] $@@ -325,7 +357,7 @@ then actorIdT <$> newActorId i else return tyV extendVarEnv i (VSig tyV' pV False fin) $ do- addBranchPC (varE (Name () [i])) bottom $ do+ addBranchPC (varE (Name () [i])) $ do tcLocalVars pV tyV fin vds cont -- Rule LOCALVARINIT (Exp)@@ -333,14 +365,17 @@ (tyE, pE) <- tcExp e checkM (liftCont $ tyE <: tyV) $ "Type mismatch: " ++ prettyPrint tyE ++ " <=> " ++ prettyPrint tyV- constraintLS pE pV+ constraintLS pE pV $+ "Cannot assign result of expression " ++ prettyPrint e +++ " with policy " ++ prettyPrint pE +++ " to variable " ++ prettyPrint i ++ " with policy " ++ prettyPrint pV tyV' <- case mActorId tyE of Nothing -> return tyV Just aid -> do newActorIdWith i aid return $ actorIdT aid extendVarEnv i (VSig tyV' pV False fin) $ do- addBranchPC (varE (Name () [i])) bottom $ do+ addBranchPC (varE (Name () [i])) $ do tcLocalVars pV tyV fin vds cont -- Rule LOCALVARINIT (Array)
src/Language/Java/Paragon/TypeCheck/Types.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE CPP, DeriveDataTypeable #-}+{-# LANGUAGE CPP, DeriveDataTypeable, TupleSections, FlexibleInstances #-} module Language.Java.Paragon.TypeCheck.Types where import Language.Java.Paragon.Syntax@@ -79,6 +79,9 @@ qualClsType :: [Ident ()] -> TcType qualClsType = clsTypeWArg . map (\i -> (i, [])) +nameToClsType :: Name () -> TcClassType+nameToClsType (Name _ is) = TcClassT $ map (\i -> (i,[])) is+ stringT :: TcType stringT = clsType (Ident () "String") @@ -120,6 +123,12 @@ isRefType (TcRefT _) = True isRefType _ = False +mNameRefType :: TcRefType -> Maybe (Name ())+mNameRefType (TcClsRefT (TcClassT iargs)) =+ let (is, as) = unzip iargs+ in if all null as then Just (Name () is) else Nothing+mNameRefType _ = Nothing+ isNullType (TcRefT (TcClsRefT TcNullT)) = True isNullType _ = False @@ -154,7 +163,39 @@ ------------------------------------------- -- Type operations +widenConvert :: PrimType () -> [PrimType ()]+widenConvert pt = case pt of+ FloatT _ -> map ($()) [DoubleT]+ LongT _ -> map ($()) [DoubleT, FloatT]+ IntT _ -> map ($()) [DoubleT, FloatT, LongT]+ ShortT _ -> map ($()) [DoubleT, FloatT, LongT, IntT]+ CharT _ -> map ($()) [DoubleT, FloatT, LongT, IntT]+ ByteT _ -> map ($()) [DoubleT, FloatT, LongT, IntT, ShortT]+ _ -> [] +narrowConvert :: PrimType () -> [PrimType ()]+narrowConvert pt = case pt of+ ShortT _ -> map ($()) [ByteT, CharT]+ CharT _ -> map ($()) [ByteT, ShortT]+ IntT _ -> map ($()) [ByteT, ShortT, CharT]+ LongT _ -> map ($()) [ByteT, ShortT, CharT, IntT]+ FloatT _ -> map ($()) [ByteT, ShortT, CharT, IntT, LongT]+ DoubleT _ -> map ($()) [ByteT, ShortT, CharT, IntT, LongT, FloatT]+ _ -> []++widenNarrowConvert :: PrimType () -> [PrimType ()]+widenNarrowConvert (ByteT _) = [CharT ()]+widenNarrowConvert _ = []+++boxConvert :: TcType -> Maybe (TcType)+boxConvert (TcPrimT pt) = case pt of+ BooleanT () -> Just $ TcRefT $ TcClsRefT $ TcClassT $ + map (\s -> (Ident () s,[])) ["java", "lang", "Boolean" ]+ _ -> Nothing+ ++ unboxConvert :: TcType -> Maybe (PrimType ()) unboxConvert (TcPrimT t) = Just t unboxConvert (TcRefT (TcClsRefT (TcClassT is))) =@@ -168,6 +209,7 @@ ["java", "lang", "Float" ] -> Just $ FloatT () ["java", "lang", "Double" ] -> Just $ DoubleT () _ -> Nothing+unboxConvert _ = Nothing isNumConvertible :: TcType -> Bool isNumConvertible t =@@ -184,6 +226,7 @@ isBoolConvertible :: TcType -> Bool isBoolConvertible t = unboxConvert t == Just (BooleanT ()) + unaryNumPromote :: TcType -> Maybe (PrimType ()) unaryNumPromote t = case unboxConvert t of@@ -208,6 +251,8 @@ binaryNumPromote_ :: TcType -> TcType -> TcType binaryNumPromote_ t1 t2 = TcPrimT . fromJust $ binaryNumPromote t1 t2 ++ --------------------------------------------- -- Pretty printing @@ -269,7 +314,7 @@ pretty (TcVar i) = char '\'' <> pretty i instance Pretty ActorId where- pretty (Fresh k) = text ('#':show k)+ pretty (Fresh k s) = text s <> text ('#':show k) pretty (Alias k) = text ('@':show k) pretty (ActorTPVar i) = pretty i @@ -278,6 +323,8 @@ opt (not $ null aids) (parens (hcat (punctuate (char ',') $ map pretty aids))) pretty (TcLockVar i) = pretty i +instance Pretty [TcLock] where+ pretty ls = brackets $ hcat (punctuate (char ',') $ map pretty ls) ppTypeParams :: Pretty a => [a] -> Doc
src/Language/Java/Paragon/TypeCheck/Uniq.hs view
@@ -20,7 +20,7 @@ newAlias u = do uniq <- getUniq u return $ Alias uniq -newFresh :: Uniq -> IO ActorId-newFresh u = do uniq <- getUniq u- return $ Fresh uniq+newFresh :: Uniq -> String -> IO ActorId+newFresh u str = do uniq <- getUniq u+ return $ Fresh uniq str