git.iko.soy/Idris-dev
on master help sign in
Add a basic reachability check.
5590ab8Matus Tejiscak
src/Idris/Erasure.hs+24−14
compare with master
unifiedsplit
@@ -58,23 +58,26 @@ performUsageAnalysis = do
58 [] -> return [] -- no main -> not compiling -> reachability irrelevant
58 [] -> return [] -- no main -> not compiling -> reachability irrelevant
59 _ -> do
59 _ -> do
60 ci <- idris_classes <$> getIState
60 ci <- idris_classes <$> getIState
61+ cg <- idris_callgraph <$> getIState
62+ opt <- idris_optimisation <$> getIState
61
63
62 -- Build the dependency graph.
64 -- Build the dependency graph.
63 let depMap = buildDepMap ci ctx mainName
65 let depMap = buildDepMap ci ctx mainName
64
66
65 -- Search for reachable nodes in the graph.
67 -- Search for reachable nodes in the graph.
66 let (residDeps, (reachableNames, minUse)) = minimalUsage depMap
68 let (residDeps, (reachableNames, minUse)) = minimalUsage depMap
69+ usage = M.toList minUse
67
70
68 -- Print some debug info.
71 -- Print some debug info.
69 logLvl 3 $ "Reachable names:\n" ++ unlines (map (indent . show) . S.toList $ reachableNames)
72 logLvl 3 $ "Reachable names:\n" ++ unlines (map (indent . show) . S.toList $ reachableNames)
70− logLvl 4 $ "Minimal usage:\n" ++ fmtUseMap minUse
73+ logLvl 4 $ "Minimal usage:\n" ++ fmtUseMap usage
71 logLvl 5 $ "Residual deps:\n" ++ unlines (map fmtItem . M.toList $ residDeps)
74 logLvl 5 $ "Residual deps:\n" ++ unlines (map fmtItem . M.toList $ residDeps)
72
75
73− -- Check that everything reachable is accessible
76+ -- Check that everything reachable is accessible.
74− checkAccessibility minUse
77+ mapM_ (checkAccessibility opt) usage
75
78
76 -- Store the usage info in the internal state.
79 -- Store the usage info in the internal state.
77− mapM_ storeUsage . M.toList $ minUse
80+ mapM_ (storeUsage cg) usage
78
81
79 return $ S.toList reachableNames
82 return $ S.toList reachableNames
80 where
83 where
@@ -84,18 +87,25 @@ performUsageAnalysis = do
84 fmtItem :: (Cond, Set Node) -> String
87 fmtItem :: (Cond, Set Node) -> String
85 fmtItem (cond, deps) = indent $ show (S.toList cond) ++ " -> " ++ show (S.toList deps)
88 fmtItem (cond, deps) = indent $ show (S.toList cond) ++ " -> " ++ show (S.toList deps)
86
89
87− fmtUseMap :: UseMap -> String
90+ fmtUseMap :: [(Name, IntSet)] -> String
88− fmtUseMap = unlines . map (\(n,is) -> indent $ show n ++ " -> " ++ show (IS.toList is)) . M.toList
91+ fmtUseMap = unlines . map (\(n,is) -> indent $ show n ++ " -> " ++ show (IS.toList is))
89
92
90− storeUsage :: (Name, IntSet) -> Idris ()
93+ storeUsage :: Ctxt CGInfo -> (Name, IntSet) -> Idris ()
91− storeUsage (n, args) = do
94+ storeUsage cg (n, args)
92− cg <- idris_callgraph <$> getIState
93− case lookupCtxt n cg of
95+ | [x] <- lookupCtxt n cg
94− [x] -> addToCG n x{ usedpos = IS.toList args } -- functions
96+ = addToCG n x{ usedpos = IS.toList args } -- functions
95− _ -> addToCG n (CGInfo [] [] [] [] (IS.toList args)) -- data ctors
96
97
98+ | otherwise
99+ = addToCG n (CGInfo [] [] [] [] (IS.toList args)) -- data ctors
100+
97−checkAccessibility :: UseMap -> Idris ()
101+ checkAccessibility :: Ctxt OptInfo -> (Name, IntSet) -> Idris ()
98−checkAccessibility umap = return ()
102+ checkAccessibility opt (n, reachable)
103+ | [Optimise col nt forc rec inaccessible] <- lookupCtxt n opt
104+ = let collision = IS.fromList inaccessible `IS.intersection` reachable
105+ in unless (IS.null collision)
106+ . fail $ "Erasure checker: inaccessible arguments reachable: " ++ show (IS.toList collision)
107+
108+ | otherwise = return ()
99
109
100-- Find the minimal consistent usage by forward chaining.
110-- Find the minimal consistent usage by forward chaining.
101minimalUsage :: Deps -> (Deps, (Set Name, UseMap))
111minimalUsage :: Deps -> (Deps, (Set Name, UseMap))