module Language.Haskell.Liquid.GhcInterface (
getGhcInfo
) where
import IdInfo
import InstEnv
import Bag (bagToList)
import ErrUtils
import GHC hiding (Target, desugarModule)
import DriverPhases (Phase(..))
import DriverPipeline (compileFile)
import Text.PrettyPrint.HughesPJ
import HscTypes hiding (Target)
import CoreSyn
import Class
import Var
import CoreMonad (liftIO)
import DataCon
import qualified Control.Exception as Ex
import GHC.Paths (libdir)
import System.FilePath ( replaceExtension, normalise)
import DynFlags
import Control.Monad (filterM, foldM, when, forM, forM_, liftM)
import Control.Applicative hiding (empty)
import Data.Monoid hiding ((<>))
import Data.List (find, nub)
import Data.Maybe (catMaybes, maybeToList)
import qualified Data.HashSet as S
import System.Console.CmdArgs.Verbosity (whenLoud)
import System.Directory (removeFile, createDirectoryIfMissing, doesFileExist)
import Language.Fixpoint.Types hiding (Result, Expr)
import Language.Fixpoint.Misc
import Language.Haskell.Liquid.Types
import Language.Haskell.Liquid.Errors
import Language.Haskell.Liquid.ANFTransform
import Language.Haskell.Liquid.Bare
import Language.Haskell.Liquid.GhcMisc
import Language.Haskell.Liquid.Misc
import Language.Haskell.Liquid.PrettyPrint
import Language.Haskell.Liquid.Visitors
import Language.Haskell.Liquid.CmdLine (withCabal, withPragmas)
import Language.Haskell.Liquid.Parse
import qualified Language.Haskell.Liquid.Measure as Ms
import Language.Fixpoint.Names
import Language.Fixpoint.Files
getGhcInfo :: Config -> FilePath -> IO (Either ErrorResult GhcInfo)
getGhcInfo cfg target = (Right <$> getGhcInfo' cfg target)
`Ex.catch` (\(e :: SourceError) -> handle e)
`Ex.catch` (\(e :: Error) -> handle e)
`Ex.catch` (\(e :: [Error]) -> handle e)
where
handle = return . Left . result
getGhcInfo' cfg0 target
= runGhc (Just libdir) $ do
liftIO $ cleanFiles target
addTarget =<< guessTarget target Nothing
(name,tgtSpec) <- liftIO $ parseSpec target
cfg <- liftIO $ withPragmas cfg0 target $ Ms.pragmas tgtSpec
cfg <- liftIO $ withCabal cfg
let paths = idirs cfg
updateDynFlags cfg
liftIO $ whenLoud $ putStrLn ("paths = " ++ show paths)
let name' = ModName Target (getModName name)
impNames <- allDepNames <$> depanal [] False
impSpecs <- getSpecs (real cfg) (totality cfg) target paths impNames [Spec, Hs, LHs]
compileCFiles =<< liftIO (foldM (\c (f,_,s) -> withPragmas c f (Ms.pragmas s)) cfg impSpecs)
impSpecs' <- forM impSpecs $ \(f,n,s) -> do
when (not $ isSpecImport n) $
addTarget =<< guessTarget f Nothing
return (n,s)
load LoadAllTargets
modguts <- getGhcModGuts1 target
hscEnv <- getSession
coreBinds <- liftIO $ anormalize (not $ nocaseexpand cfg) hscEnv modguts
let datacons = [ dataConWorkId dc
| tc <- mgi_tcs modguts
, dc <- tyConDataCons tc
]
let impVs = importVars coreBinds ++ classCons (mgi_cls_inst modguts)
let defVs = definedVars coreBinds
let useVs = readVars coreBinds
let letVs = letVars coreBinds
let derVs = derivedVars coreBinds $ fmap (fmap is_dfun) $ mgi_cls_inst modguts
logicmap <- liftIO makeLogicMap
(spec, imps, incs) <- moduleSpec cfg coreBinds (impVs ++ defVs) letVs name' modguts tgtSpec logicmap impSpecs'
liftIO $ whenLoud $ putStrLn $ "Module Imports: " ++ show imps
hqualFiles <- moduleHquals modguts paths target imps incs
return $ GI hscEnv coreBinds derVs impVs (letVs ++ datacons) useVs hqualFiles imps incs spec
makeLogicMap
= do lg <- getCoreToLogicPath
lspec <- readFile lg
return $ parseSymbolToLogic lg lspec
classCons :: Maybe [ClsInst] -> [Id]
classCons Nothing = []
classCons (Just cs) = concatMap (dataConImplicitIds . head . tyConDataCons . classTyCon . is_cls) cs
derivedVars :: CoreProgram -> Maybe [DFunId] -> [Id]
derivedVars cbs (Just fds) = concatMap (derivedVs cbs) fds
derivedVars _ Nothing = []
derivedVs :: CoreProgram -> DFunId -> [Id]
derivedVs cbs fd = concatMap bindersOf cbf ++ deps
where cbf = filter f cbs
f (NonRec x _) = eqFd x
f (Rec xes ) = any eqFd (fst <$> xes)
eqFd x = varName x == varName fd
deps :: [Id]
deps = concatMap dep $ (unfoldingInfo . idInfo <$> concatMap bindersOf cbf)
dep (DFunUnfolding _ _ e) = concatMap grapDep e
dep (CoreUnfolding {uf_tmpl = e}) = grapDep e
dep _ = []
grapDep :: CoreExpr -> [Id]
grapDep e = freeVars S.empty e
updateDynFlags cfg
= do df <- getSessionDynFlags
let df' = df { importPaths = idirs cfg ++ importPaths df
, libraryPaths = idirs cfg ++ libraryPaths df
, includePaths = idirs cfg ++ includePaths df
, profAuto = ProfAutoCalls
, ghcLink = LinkInMemory
, hscTarget = HscInterpreted
, ghcMode = CompManager
, log_action = \_ _ _ _ _ -> return ()
} `xopt_set` Opt_MagicHash
`gopt_set` Opt_ImplicitImportQualified
`gopt_set` Opt_PIC
#if __GLASGOW_HASKELL__ >= 710
`gopt_set` Opt_Debug
#endif
(df'',_,_) <- parseDynamicFlags df' (map noLoc $ ghcOptions cfg)
setSessionDynFlags $ df''
compileCFiles cfg
= do df <- getSessionDynFlags
setSessionDynFlags $ df { includePaths = nub $ idirs cfg ++ includePaths df
, importPaths = nub $ idirs cfg ++ importPaths df
, libraryPaths = nub $ idirs cfg ++ libraryPaths df }
hsc <- getSession
os <- mapM (\x -> liftIO $ compileFile hsc StopLn (x,Nothing)) (nub $ cFiles cfg)
df <- getSessionDynFlags
setSessionDynFlags $ df { ldInputs = map (FileOption "") os ++ ldInputs df }
mgi_namestring = moduleNameString . moduleName . mgi_module
importVars = freeVars S.empty
definedVars = concatMap defs
where
defs (NonRec x _) = [x]
defs (Rec xes) = map fst xes
getGhcModGuts1 :: FilePath -> Ghc MGIModGuts
getGhcModGuts1 fn = do
modGraph <- getModuleGraph
case find ((== fn) . msHsFilePath) modGraph of
Just modSummary -> do
mod_p <- parseModule modSummary
mod_guts <- coreModule <$> (desugarModule =<< typecheckModule (ignoreInline mod_p))
let deriv = getDerivedDictionaries mod_guts
return $! (miModGuts (Just deriv) mod_guts)
Nothing -> exitWithPanic "Ghc Interface: Unable to get GhcModGuts"
getDerivedDictionaries cm = instEnvElts $ mg_inst_env cm
cleanFiles :: FilePath -> IO ()
cleanFiles fn
= do forM_ bins (tryIgnore "delete binaries" . removeFileIfExists)
tryIgnore "create temp directory" $ createDirectoryIfMissing False dir
where
bins = replaceExtension fn <$> ["hi", "o"]
dir = tempDirectory fn
removeFileIfExists f = doesFileExist f >>= (`when` removeFile f)
moduleHquals mg paths target imps incs
= do hqs <- specIncludes Hquals paths incs
hqs' <- moduleImports [Hquals] paths (mgi_namestring mg : imps)
hqs'' <- liftIO $ filterM doesFileExist [extFileName Hquals target]
let rv = sortNub $ hqs'' ++ hqs ++ (snd <$> hqs')
liftIO $ whenLoud $ putStrLn $ "Reading Qualifiers From: " ++ show rv
return rv
moduleSpec cfg cbs vars defVars target mg tgtSpec logicmap impSpecs
= do addImports impSpecs
addContext $ IIModule $ moduleName $ mgi_module mg
env <- getSession
let specs = (target,tgtSpec):impSpecs
let imps = sortNub $ impNames ++ [ symbolString x
| (_,spec) <- specs
, x <- Ms.imports spec
]
ghcSpec <- liftIO $ makeGhcSpec cfg target cbs vars defVars exports env logicmap specs
return (ghcSpec, imps, Ms.includes tgtSpec)
where
exports = mgi_exports mg
impNames = map (getModString.fst) impSpecs
addImports = mapM (addContext . IIDecl . qualImportDecl . getModName . fst)
allDepNames = concatMap (map declNameString . ms_textual_imps)
declNameString = moduleNameString . unLoc . ideclName . unLoc
patErrorName = "PatErr"
realSpecName = "Real"
notRealSpecName = "NotReal"
getSpecs rflag tflag target paths names exts
= do fs' <- sortNub <$> moduleImports exts paths names
patSpec <- getPatSpec paths tflag
rlSpec <- getRealSpec paths rflag
let fs = patSpec ++ rlSpec ++ fs'
liftIO $ whenLoud $ putStrLn ("getSpecs: " ++ show fs)
transParseSpecs exts paths (S.singleton target) mempty (map snd fs)
getPatSpec paths totalitycheck
| totalitycheck
= (map (patErrorName, )) . maybeToList <$> moduleFile paths patErrorName Spec
| otherwise
= return []
getRealSpec paths freal
| freal
= (map (realSpecName, )) . maybeToList <$> moduleFile paths realSpecName Spec
| otherwise
= (map (notRealSpecName, )) . maybeToList <$> moduleFile paths notRealSpecName Spec
transParseSpecs _ _ _ specs []
= return specs
transParseSpecs exts paths seenFiles specs newFiles
= do newSpecs <- liftIO $ mapM (\f -> addFst3 f <$> parseSpec f) newFiles
impFiles <- moduleImports exts paths $ specsImports newSpecs
let seenFiles' = seenFiles `S.union` (S.fromList newFiles)
let specs' = specs ++ map (third noTerm) newSpecs
let newFiles' = [f | (_,f) <- impFiles, not (f `S.member` seenFiles')]
transParseSpecs exts paths seenFiles' specs' newFiles'
where
specsImports ss = nub $ concatMap (map symbolString . Ms.imports . thd3) ss
noTerm spec = spec { Ms.decr=mempty, Ms.lazy=mempty, Ms.termexprs=mempty }
third f (a,b,c) = (a,b,f c)
parseSpec :: FilePath -> IO (ModName, Ms.BareSpec)
parseSpec file
= do whenLoud $ putStrLn $ "parseSpec: " ++ file
either Ex.throw return . specParser file =<< readFile file
specParser file str
| isExtFile Spec file = specSpecificationP file str
| isExtFile Hs file = hsSpecificationP file str
| isExtFile LHs file = lhsSpecificationP file str
| otherwise = exitWithPanic $ "SpecParser: Cannot Parse File " ++ file
moduleImports :: GhcMonad m => [Ext] -> [FilePath] -> [String] -> m [(String, FilePath)]
moduleImports exts paths names
= liftM concat $ forM names $ \name -> do
map (name,) . catMaybes <$> mapM (moduleFile paths name) exts
moduleFile :: GhcMonad m => [FilePath] -> String -> Ext -> m (Maybe FilePath)
moduleFile paths name ext
| ext `elem` [Hs, LHs]
= do mg <- getModuleGraph
case find ((==name) . moduleNameString . ms_mod_name) mg of
Nothing -> liftIO $ getFileInDirs (extModuleName name ext) paths
Just ms -> return $ normalise <$> ml_hs_file (ms_location ms)
| otherwise
= liftIO $ getFileInDirs (extModuleName name ext) paths
specIncludes :: GhcMonad m => Ext -> [FilePath] -> [FilePath] -> m [FilePath]
specIncludes ext paths reqs
= do let libFile = extFileNameR ext $ symbolString preludeName
let incFiles = catMaybes $ reqFile ext <$> reqs
liftIO $ forM (libFile : incFiles) $ \f -> do
mfile <- getFileInDirs f paths
case mfile of
Just file -> return file
Nothing -> errorstar $ "cannot find " ++ f ++ " in " ++ show paths
reqFile ext s
| isExtFile ext s
= Just s
| otherwise
= Nothing
instance PPrint GhcSpec where
pprint spec = (text "******* Target Variables ********************")
$$ (pprint $ tgtVars spec)
$$ (text "******* Type Signatures *********************")
$$ (pprintLongList $ tySigs spec)
$$ (text "******* Assumed Type Signatures *************")
$$ (pprintLongList $ asmSigs spec)
$$ (text "******* DataCon Specifications (Measure) ****")
$$ (pprintLongList $ ctors spec)
$$ (text "******* Measure Specifications **************")
$$ (pprintLongList $ meas spec)
instance PPrint GhcInfo where
pprint info = (text "*************** Imports *********************")
$+$ (intersperse comma $ text <$> imports info)
$+$ (text "*************** Includes ********************")
$+$ (intersperse comma $ text <$> includes info)
$+$ (text "*************** Imported Variables **********")
$+$ (pprDoc $ impVars info)
$+$ (text "*************** Defined Variables ***********")
$+$ (pprDoc $ defVars info)
$+$ (text "*************** Specification ***************")
$+$ (pprint $ spec info)
$+$ (text "*************** Core Bindings ***************")
$+$ (pprint $ cbs info)
instance Show GhcInfo where
show = showpp
instance PPrint [CoreBind] where
pprint = pprDoc . tidyCBs
instance PPrint TargetVars where
pprint AllVars = text "All Variables"
pprint (Only vs) = text "Only Variables: " <+> pprint vs
instance Result SourceError where
result = (`Crash` "Invalid Source")
. concatMap errMsgErrors
. bagToList
. srcErrorMessages
errMsgErrors e = [ ErrGhc (errMsgSpan e) (pprint e)]