Skip to content

Instantly share code, notes, and snippets.

@atondwal
Last active August 29, 2015 14:19
Show Gist options
  • Save atondwal/67c6c55b970cd097eca2 to your computer and use it in GitHub Desktop.
Save atondwal/67c6c55b970cd097eca2 to your computer and use it in GitHub Desktop.
{-# LANGUAGE TupleSections #-}
import Data.Maybe
import Data.Monoid (mconcat, mempty)
import System.Exit
import Control.Applicative ((<$>))
import Control.Monad
import Control.DeepSeq
import Text.PrettyPrint.HughesPJ
import CoreSyn
import Var
import System.Console.CmdArgs.Verbosity (whenLoud)
import System.Console.CmdArgs.Default
import qualified Language.Fixpoint.Config as FC
import qualified Language.Haskell.Liquid.DiffCheck as DC
import Language.Fixpoint.Misc
import Language.Fixpoint.Interface
import Language.Fixpoint.Types (sinfo)
import Language.Haskell.Liquid.Types
import Language.Haskell.Liquid.Errors
import Language.Haskell.Liquid.CmdLine
import Language.Haskell.Liquid.GhcInterface
import Language.Haskell.Liquid.Constraint.Generate
import Language.Haskell.Liquid.Constraint.ToFixpoint
import Language.Haskell.Liquid.Constraint.Types
import Language.Haskell.Liquid.TransformRec
import Language.Haskell.Liquid.Annotate (mkOutput)
-- import Language.Haskell.Liquid.FaultLocal
main :: IO b
main = do cfg0 <- getOpts
res <- mconcat <$> mapM (checkOne cfg0) (files cfg0)
let ecode = resultExit $ {- traceShow "RESULT" $ -} o_result res
-- putStrLn $ "ExitCode: " ++ show ecode
-- exitWith ecode
case ecode of
ExitSuccess -> exitWith ecode
ExitFailure _ -> do
putStrLn "Do you want to perform fault localization (yes/no)?"
ans <- getLine
if ans == "yes"
then do
consFL <- checkOneFL cfg0 $ head $ files cfg0
putStrLn ("# of constraints implicated: " ++ (show $ length consFL))
forM_ consFL (\cons -> do
print $ ci_loc $ sinfo cons)
exitWith ecode
else exitWith ecode
checkOneFL cfg0 t = do
val <- getGhcInfo cfg0 t
case val of
Left _ -> return []
Right info -> liquidOneFL t info
liquidOneFL target info = do
let cfg = config $ spec info
let cbs' = transformScope (cbs info)
dc <- prune cfg cbs' target info
let cgi = {-# SCC "generateConstraints" #-} generateConstraints $! info {cbs = cbs'}
-- cgi `deepseq` 0
let cons = fixCs cgi
consFL <- deltaDebug cfg target cgi info dc cons []
return consFL
-- test() for delta debugging algorithm
-- intuitively, check if set of constraints cons induces
-- failure of the refinement
testDelta cfg target cgi info dc cons = do
putStrLn $ "testing delta: " ++ (show $ length cons)
let cgi' = cgi { fixCs = cons }
out <- solveCs cfg target cgi' info dc
let ecode = resultExit $ o_result out
case ecode of
ExitSuccess -> return False
ExitFailure _ -> return True
deltaDebug _ _ _ _ _ [c] _ = return [c]
deltaDebug cfg target cgi info dc cons r = do
let (c1, c2) = splitAt ((length cons) `div` 2) cons
test1 <- testDelta cfg target cgi info dc (c1 ++ r)
test2 <- testDelta cfg target cgi info dc (c2 ++ r)
if test1
then if test2
then do
d1 <- deltaDebug cfg target cgi info dc c1 r
d2 <-deltaDebug cfg target cgi info dc c2 r
return (d1 ++ d2)
else deltaDebug cfg target cgi info dc c1 r
else if test2
then deltaDebug cfg target cgi info dc c2 r
else do
d1 <- deltaDebug cfg target cgi info dc c1 (c2 ++ r)
d2 <- deltaDebug cfg target cgi info dc c2 (c1 ++ r)
return (d1 ++ d2)
checkOne :: Config -> FilePath -> IO (Output Doc)
checkOne cfg0 t = getGhcInfo cfg0 t >>= either errOut (liquidOne t)
where
errOut r = exitWithResult cfg0 t $ mempty { o_result = r}
liquidOne :: FilePath -> GhcInfo -> IO (Output Doc)
liquidOne target info =
do donePhase Loud "Extracted Core using GHC"
let cfg = config $ spec info
whenLoud $ do putStrLn "**** Config **************************************************"
print cfg
whenLoud $ do putStrLn $ showpp info
putStrLn "*************** Original CoreBinds ***************************"
putStrLn $ showpp (cbs info)
let cbs' = transformScope (cbs info)
whenLoud $ do donePhase Loud "transformRecExpr"
putStrLn "*************** Transform Rec Expr CoreBinds *****************"
putStrLn $ showpp cbs'
putStrLn "*************** Slicing Out Unchanged CoreBinds *****************"
dc <- prune cfg cbs' target info
let cbs'' = maybe cbs' DC.newBinds dc
let cgi = {-# SCC "generateConstraints" #-} generateConstraints $! info {cbs = cbs''}
cgi `deepseq` donePhase Loud "generateConstraints"
out <- solveCs cfg target cgi info dc
donePhase Loud "solve"
let out' = mconcat [maybe mempty DC.oldOutput dc, out]
DC.saveResult target out'
exitWithResult cfg target out'
-- checkedNames :: Maybe DC.DiffCheck -> Maybe [Name.Name]
checkedNames dc = concatMap names . DC.newBinds <$> dc
where
names (NonRec v _ ) = [showpp $ shvar v]
names (Rec xs) = map (shvar . fst) xs
shvar = showpp . varName
-- prune :: Config -> [CoreBind] -> FilePath -> GhcInfo -> IO (Maybe Diff)
prune cfg cbs target info
| not (null vs) = return . Just $ DC.DC (DC.thin cbs vs) mempty
| diffcheck cfg = DC.slice target cbs
| otherwise = return Nothing
where
vs = tgtVars $ spec info
-- printConstraints :: [SubC] -> IO ()
-- printConstraints cons = forM_ cons (print . consWeight)
solveCs cfg target cgi info dc
= do
let finfo = cgInfoFInfo info cgi
(r, sol) <- solve fx target (hqFiles info) finfo
let names = checkedNames dc
let warns = logErrors cgi
let annm = annotMap cgi
let res = ferr sol r
let out0 = mkOutput cfg res sol annm
return $ out0 { o_vars = names } { o_errors = warns} { o_result = res }
where
fx = def { FC.solver = fromJust (smtsolver cfg), FC.real = real cfg }
ferr s r = fmap (tidyError s) $ result $ sinfo <$> r
-- filterConstraints filt finfo =
-- finfo { cm = M.fromList $ filt $ M.toList $ cm finfo }
-- writeCGI tgt cgi = {-# SCC "ConsWrite" #-} writeFile (extFileName Cgi tgt) str
-- where
-- str = {-# SCC "PPcgi" #-} showpp cgi
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment