{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeSynonymInstances #-} {-# OPTIONS_GHC -fno-cse #-} {-@ LIQUID "--diff" @-} -- | This module contains all the code needed to output the result which -- is either: `SAFE` or `WARNING` with some reasonable error message when -- something goes wrong. All forms of errors/exceptions should go through -- here. The idea should be to report the error, the source position that -- causes it, generate a suitable .json file and then exit. module Language.Haskell.Liquid.UX.CmdLine ( -- * Get Command Line Configuration getOpts, mkOpts, defConfig -- * Update Configuration With Pragma , withPragmas -- * Canonicalize Paths in Config , canonicalizePaths -- * Exit Function , exitWithResult , addErrors -- * Diff check mode , diffcheck ) where import Prelude hiding (error) import Control.Monad import Data.Maybe import Data.Aeson (encode) import qualified Data.ByteString.Lazy.Char8 as B import System.Directory import System.Exit import System.Environment import System.Console.CmdArgs.Explicit import System.Console.CmdArgs.Implicit hiding (Loud) import System.Console.CmdArgs.Text import Data.List (nub) import System.FilePath (dropFileName, isAbsolute, takeDirectory, ()) import qualified Language.Fixpoint.Types.Config as FC -- a hiding (Config, linear, elimBound, elimStats, -- nonLinCuts, getOpts, cores, minPartSize, -- maxPartSize, eliminate, defConfig, -- stringTheory, -- withPragmas, -- extensionality, -- alphaEquivalence, betaEquivalence, normalForm) -- import Language.Fixpoint.Utils.Files import Language.Fixpoint.Misc import Language.Fixpoint.Types.Names import Language.Fixpoint.Types hiding (Error, Result, saveQuery) import qualified Language.Fixpoint.Types as F import Language.Haskell.Liquid.UX.Annotate import Language.Haskell.Liquid.UX.Config import Language.Haskell.Liquid.GHC.Misc import Language.Haskell.Liquid.Misc import Language.Haskell.Liquid.Types.PrettyPrint import Language.Haskell.Liquid.Types hiding (name, typ) import qualified Language.Haskell.Liquid.UX.ACSS as ACSS import Text.Parsec.Pos (newPos) import Text.PrettyPrint.HughesPJ hiding (Mode) --------------------------------------------------------------------------------- -- Config Magic Numbers---------------------------------------------------------- --------------------------------------------------------------------------------- defaultMaxParams :: Int defaultMaxParams = 2 --------------------------------------------------------------------------------- -- Parsing Command Line---------------------------------------------------------- --------------------------------------------------------------------------------- config :: Mode (CmdArgs Config) config = cmdArgsMode $ Config { files = def &= typ "TARGET" &= args &= typFile , idirs = def &= typDir &= help "Paths to Spec Include Directory " , fullcheck = def &= help "Full Checking: check all binders (DEFAULT)" , diffcheck = def &= help "Incremental Checking: only check changed binders" , higherorder = def &= help "Allow higher order binders into the logic" , extensionality = def &= help "Allow function extentionality axioms" , alphaEquivalence = def &= help "Allow lambda alpha-equivalence axioms" , betaEquivalence = def &= help "Allow lambda beta-equivalence axioms" , normalForm = def &= help "Allow lambda normalization-equivalence axioms" , higherorderqs = def &= help "Allow higher order qualifiers to get automatically instantiated" , linear = def &= help "Use uninterpreted integer multiplication and division" , stringTheory = def &= help "Interpretation of Strings by z3" , saveQuery = def &= help "Save fixpoint query to file (slow)" , checks = def &= help "Check a specific (top-level) binder" &= name "check-var" , pruneUnsorted = def &= help "Disable prunning unsorted Predicates" &= name "prune-unsorted" , notermination = def &= help "Disable Termination Check" &= name "no-termination-check" , gradual = def &= help "Enable gradual refinementtype checking" &= name "gradual" , totalHaskell = def &= help "Check for termination and totality, Overrides no-termination flags" &= name "total-Haskell" , autoproofs = def &= help "Automatically construct proofs from axioms" &= name "auto-proofs" , nowarnings = def &= help "Don't display warnings, only show errors" &= name "no-warnings" , noannotations = def &= help "Don't create intermediate annotation files" &= name "no-annotations" , trustInternals = False &= help "Trust GHC generated code" &= name "trust-internals" , nocaseexpand = def &= help "Don't expand the default case in a case-expression" &= name "no-case-expand" , strata = def &= help "Enable Strata Analysis" , notruetypes = def &= help "Disable Trueing Top Level Types" &= name "no-true-types" , totality = def &= help "Check totality" , cores = def &= help "Use m cores to solve logical constraints" , minPartSize = FC.defaultMinPartSize &= help "If solving on multiple cores, ensure that partitions are of at least m size" , maxPartSize = FC.defaultMaxPartSize &= help ("If solving on multiple cores, once there are as many partitions " ++ "as there are cores, don't merge partitions if they will exceed this " ++ "size. Overrides the minpartsize option.") , smtsolver = def &= help "Name of SMT-Solver" , noCheckUnknown = def &= explicit &= name "no-check-unknown" &= help "Don't complain about specifications for unexported and unused values " , maxParams = defaultMaxParams &= help "Restrict qualifier mining to those taking at most `m' parameters (2 by default)" , shortNames = def &= name "short-names" &= help "Print shortened names, i.e. drop all module qualifiers." , shortErrors = def &= name "short-errors" &= help "Don't show long error messages, just line numbers." , cabalDir = def &= name "cabal-dir" &= help "Find and use .cabal to add paths to sources for imported files" , ghcOptions = def &= name "ghc-option" &= typ "OPTION" &= help "Pass this option to GHC" , cFiles = def &= name "c-files" &= typ "OPTION" &= help "Tell GHC to compile and link against these files" , port = defaultPort &= name "port" &= help "Port at which lhi should listen" , exactDC = def &= help "Exact Type for Data Constructors" &= name "exact-data-cons" , noMeasureFields = def &= help "Do not automatically lift data constructor fields into measures" &= name "no-measure-fields" , scrapeImports = False &= help "Scrape qualifiers from imported specifications" &= name "scrape-imports" &= explicit , scrapeInternals = False &= help "Scrape qualifiers from auto generated specifications" &= name "scrape-internals" &= explicit , scrapeUsedImports = False &= help "Scrape qualifiers from used, imported specifications" &= name "scrape-used-imports" &= explicit , elimStats = False &= name "elimStats" &= help "Print eliminate stats" , elimBound = Nothing &= name "elimBound" &= help "Maximum chain length for eliminating KVars" , noslice = False &= name "noSlice" &= help "Disable non-concrete KVar slicing" , json = False &= name "json" &= help "Print results in JSON (for editor integration)" , counterExamples = False &= name "counter-examples" &= help "Attempt to generate counter-examples to type errors (experimental!)" , timeBinds = False &= name "time-binds" &= help "Solve each (top-level) asserted type signature separately & time solving." , untidyCore = False &= name "untidy-core" &= help "Print fully qualified identifier names in verbose mode" , eliminate = FC.Some &= name "eliminate" &= help "Use elimination for 'all' (use TRUE for cut-kvars), 'some' (use quals for cut-kvars) or 'none' (use quals for all kvars)." -- , noEliminate -- = False &= name "no-eliminate" -- &= help "Don't use KVar elimination during solving" --, oldEliminate -- = False &= name "old-eliminate" -- &= help "Use old eliminate algorithm (temp. for benchmarking)" , noPatternInline = False &= name "no-pattern-inline" &= help "Don't inline special patterns (e.g. `>>=` and `return`) during constraint generation." , noSimplifyCore = False &= name "no-simplify-core" &= help "Don't simplify GHC core before constraint generation" , nonLinCuts = True &= name "non-linear-cuts" &= help "(TRUE) Treat non-linear kvars as cuts" , autoInstantiate = def &= help "How to instantiate axiomatized functions `smtinstances` for SMT instantiation, `liquidinstances` for terminating instantiation" &= name "automatic-instances" , proofMethod = def &= help "Specify what method to use to create instances. Options `arithmetic`, `rewrite`, `allmathods`. Default is `rewrite`" &= name "proof-method" , fuel = defFuel &= help "Fuel parameter for liquid instances (default is 2)" &= name "fuel" , debugInstantionation = False &= help "Debug Progress in liquid instantiation" &= name "debug-instantiation" } &= verbosity &= program "liquid" &= help "Refinement Types for Haskell" &= summary copyright &= details [ "LiquidHaskell is a Refinement Type based verifier for Haskell" , "" , "To check a Haskell file foo.hs, type:" , " liquid foo.hs " ] defaultPort :: Int defaultPort = 3000 getOpts :: [String] -> IO Config getOpts as = do cfg0 <- envCfg cfg1 <- mkOpts =<< cmdArgsRun' config { modeValue = (modeValue config) { cmdArgsValue = cfg0 } } as cfg <- fixConfig cfg1 when (json cfg) $ setVerbosity Quiet whenNormal $ putStrLn copyright withSmtSolver cfg cmdArgsRun' :: Mode (CmdArgs a) -> [String] -> IO a cmdArgsRun' md as = case parseResult of Left e -> putStrLn (helpMsg e) >> exitFailure Right a -> cmdArgsApply a where helpMsg e = showText defaultWrap $ helpText [e] HelpFormatDefault md parseResult = process md as -- <$> getArgs -------------------------------------------------------------------------------- withSmtSolver :: Config -> IO Config -------------------------------------------------------------------------------- withSmtSolver cfg = case smtsolver cfg of Just _ -> return cfg Nothing -> do smts <- mapM findSmtSolver [FC.Z3, FC.Cvc4, FC.Mathsat] case catMaybes smts of (s:_) -> return (cfg {smtsolver = Just s}) _ -> panic Nothing noSmtError where noSmtError = "LiquidHaskell requires an SMT Solver, i.e. z3, cvc4, or mathsat to be installed." findSmtSolver :: FC.SMTSolver -> IO (Maybe FC.SMTSolver) findSmtSolver smt = maybe Nothing (const $ Just smt) <$> findExecutable (show smt) fixConfig :: Config -> IO Config fixConfig cfg = do pwd <- getCurrentDirectory cfg <- canonicalizePaths pwd cfg return $ canonConfig cfg -- | Attempt to canonicalize all `FilePath's in the `Config' so we don't have -- to worry about relative paths. canonicalizePaths :: FilePath -> Config -> IO Config canonicalizePaths pwd cfg = do tgt <- canonicalizePath pwd isdir <- doesDirectoryExist tgt is <- mapM (canonicalize tgt isdir) $ idirs cfg cs <- mapM (canonicalize tgt isdir) $ cFiles cfg return $ cfg { idirs = is, cFiles = cs } canonicalize :: FilePath -> Bool -> FilePath -> IO FilePath canonicalize tgt isdir f | isAbsolute f = return f | isdir = canonicalizePath (tgt f) | otherwise = canonicalizePath (takeDirectory tgt f) envCfg :: IO Config envCfg = do so <- lookupEnv "LIQUIDHASKELL_OPTS" case so of Nothing -> return defConfig Just s -> parsePragma $ envLoc s where envLoc = Loc l l l = newPos "ENVIRONMENT" 0 0 copyright :: String copyright = "LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.\n" -- [NOTE:searchpath] -- 1. not convinced we should add the file's directory to the search path -- 2. tests fail if you flip order of idirs' mkOpts :: Config -> IO Config mkOpts cfg = do let files' = sortNub $ files cfg id0 <- getIncludeDir return $ cfg { files = files' , idirs = (dropFileName <$> files') -- [NOTE:searchpath] ++ [id0 gHC_VERSION, id0] ++ idirs cfg } -------------------------------------------------------------------------------- -- | Updating options -------------------------------------------------------------------------------- canonConfig :: Config -> Config canonConfig cfg = cfg { diffcheck = diffcheck cfg && not (fullcheck cfg) -- , eliminate = if higherOrderFlag cfg then FC.All else eliminate cfg } -------------------------------------------------------------------------------- withPragmas :: Config -> FilePath -> [Located String] -> IO Config -------------------------------------------------------------------------------- withPragmas cfg fp ps = foldM withPragma cfg ps >>= canonicalizePaths fp >>= (return . canonConfig) withPragma :: Config -> Located String -> IO Config withPragma c s = withArgs [val s] $ cmdArgsRun config { modeValue = (modeValue config) { cmdArgsValue = c } } parsePragma :: Located String -> IO Config parsePragma = withPragma defConfig defConfig :: Config defConfig = Config { files = def , idirs = def , fullcheck = def , linear = def , stringTheory = def , higherorder = def , extensionality = def , alphaEquivalence = def , betaEquivalence = def , normalForm = def , higherorderqs = def , diffcheck = def , saveQuery = def , checks = def , noCheckUnknown = def , notermination = def , gradual = False , totalHaskell = def , autoproofs = def , nowarnings = def , noannotations = def , trustInternals = False , nocaseexpand = def , strata = def , notruetypes = def , totality = def , pruneUnsorted = def , exactDC = def , noMeasureFields = def , cores = def , minPartSize = FC.defaultMinPartSize , maxPartSize = FC.defaultMaxPartSize , maxParams = defaultMaxParams , smtsolver = def , shortNames = def , shortErrors = def , cabalDir = def , ghcOptions = def , cFiles = def , port = defaultPort , scrapeInternals = False , scrapeImports = False , scrapeUsedImports = False , elimStats = False , elimBound = Nothing , json = False , counterExamples = False , timeBinds = False , untidyCore = False -- , noEliminate = False , eliminate = FC.Some , noPatternInline = False , noSimplifyCore = False , nonLinCuts = True , autoInstantiate = def , proofMethod = def , fuel = defFuel , debugInstantionation = False , noslice = False } defFuel :: Int defFuel = 2 ------------------------------------------------------------------------ -- | Exit Function ----------------------------------------------------- ------------------------------------------------------------------------ ------------------------------------------------------------------------ exitWithResult :: Config -> [FilePath] -> Output Doc -> IO (Output Doc) ------------------------------------------------------------------------ exitWithResult cfg targets out = do annm <- {-# SCC "annotate" #-} annotate cfg targets out whenNormal $ donePhase Loud "annotate" -- let r = o_result out -- `addErrors` o_errors out consoleResult cfg out annm return out -- { o_result = r } consoleResult :: Config -> Output a -> ACSS.AnnMap -> IO () consoleResult cfg | json cfg = consoleResultJson cfg | otherwise = consoleResultFull cfg consoleResultFull :: Config -> Output a -> t -> IO () consoleResultFull cfg out _ = do let r = o_result out writeCheckVars $ o_vars out cr <- resultWithContext r writeResult cfg (colorResult r) cr consoleResultJson :: t -> t1 -> ACSS.AnnMap -> IO () consoleResultJson _ _ annm = do putStrLn "RESULT" B.putStrLn . encode . ACSS.errors $ annm resultWithContext :: FixResult UserError -> IO (FixResult CError) resultWithContext = mapM errorWithContext instance Show (CtxError Doc) where show = showpp writeCheckVars :: Symbolic a => Maybe [a] -> IO () writeCheckVars Nothing = return () writeCheckVars (Just []) = colorPhaseLn Loud "Checked Binders: None" "" writeCheckVars (Just ns) = colorPhaseLn Loud "Checked Binders:" "" >> forM_ ns (putStrLn . symbolString . dropModuleNames . symbol) type CError = CtxError Doc writeResult :: Config -> Moods -> F.FixResult CError -> IO () writeResult cfg c = mapM_ (writeDoc c) . zip [0..] . resDocs tidy where tidy = if shortErrors cfg then F.Lossy else F.Full writeDoc c (i, d) = writeBlock c i $ lines $ render d writeBlock _ _ [] = return () writeBlock c 0 ss = forM_ ss (colorPhaseLn c "") writeBlock _ _ ss = forM_ ("\n" : ss) putStrLn resDocs :: F.Tidy -> F.FixResult CError -> [Doc] resDocs _ F.Safe = [text "RESULT: SAFE"] resDocs k (F.Crash xs s) = text "RESULT: ERROR" : text s : pprManyOrdered k "" (errToFCrash <$> xs) resDocs k (F.Unsafe xs) = text "RESULT: UNSAFE" : pprManyOrdered k "" (nub xs) errToFCrash :: CtxError a -> CtxError a errToFCrash ce = ce { ctErr = tx $ ctErr ce} where tx (ErrSubType l m g t t') = ErrFCrash l m g t t' tx e = e {- TODO: Never used, do I need to exist? reportUrl = text "Please submit a bug report at: https://github.com/ucsd-progsys/liquidhaskell" -} addErrors :: FixResult a -> [a] -> FixResult a addErrors r [] = r addErrors Safe errs = Unsafe errs addErrors (Unsafe xs) errs = Unsafe (xs ++ errs) addErrors r _ = r instance Fixpoint (F.FixResult CError) where toFix = vcat . resDocs F.Full