{-# Language TypeSynonymInstances,FlexibleInstances,MultiParamTypeClasses,FunctionalDependencies,RankNTypes,FlexibleContexts,KindSignatures,ScopedTypeVariables #-} module Main where import TypeChecker import Analysis import Parser hiding (processFile,main) import Normalization import ASTData import ASTTrans import GenSMT import Spec import NtoIR import IRtoPregel (genCode') import System.Environment import System.IO import System.Process import System.Timeout import System.IO.Unsafe getOpts :: [String] -> IO (Option, [String]) getOpts ags = run defaultOpt [] (if length ags == 0 then ["-h"] else ags) where run ops fs [] = return (ops, fs) run ops fs (xs:xss) = case xs of "-h" -> do printHelp() return (ops, []) "-oz" -> do run (ops { zipOpt = True }) fs xss "-omz" -> do run (ops { mzFusionOpt = True }) fs xss "-opc" -> do run (ops { pcFusionOpt = True }) fs xss -- Iwasaki: imported optimizer code of Morihata and Kato "-oec" -> do run (ops { elimCommOpt = True }) fs xss "-oei" -> do run (ops { elimIdOpt = True }) fs xss "-ovh" -> do run (ops { useV2HOpt = True }) fs xss "-omc" -> do run (ops { useMsgCombOpt = True }) fs xss "-smt" -> do run (ops { useSmt = True }) fs xss "-smtpath" -> do let (h:t) = xss run (ops { smtPath = h }) fs t "-smtoption" -> do let (h:t) = xss run (ops { smtOption = h }) fs t "-smttimeout" -> do let (h:t) = xss run (ops { smtTimeout = read h }) fs t "-printsmt" -> do run (ops { printSmt = True }) fs xss -- Iwasaki : enabled to output ast, nast, and ir "-i" -> do run (ops { genMode = IROnly }) fs xss "-a" -> do run (ops { genMode = ASTOnly }) fs xss "-na" -> do run (ops { genMode = NASTOnly }) fs xss "-g" -> do run (ops { genMode = Giraph }) fs xss "-p" -> do run (ops { genMode = PregelPlus }) fs xss "-o" -> do let (h:t) = xss run (ops { outputFile = Just h }) fs t "-n" -> do let (h:t) = xss run (ops { normLevel = read h }) fs t _ -> if head xs == '-' then do hPutStrLn stderr ("Unknown option " ++ xs ++ " specified, ignored.") run ops fs xss else do run ops (fs ++ [xs]) xss printHelp () = do mapM_ putStrLn ms where ms = [ "fregel [options] file ..." , "Options:" , " -h show help" , " -oz enable zip-elimination optimization (not completed yet)" -- gmap (gzip ... gzip) can be compiled at once into a single phase, -- avoiding redundant intermediate data structures (i.e., pairs) , " -omz enable map*zip* fusion" -- phases without communication will be executed (fused) in , " -opc enable prev-curr-fusion optimization " -- for gmap and gzip, only one of prev and curr is necessary. -- in this case, XXX_curr should be replaced with XXX_prev. , " -oei eliminate sending identity values, if possible" , " -oec eliminate communications of the same values, if possible" , " -ovh use voteToHalt, if possible" , " -omc use message combiner (Pregel+ only)" , " -smt use Z3 solover when -oec/-ovh are specified" , " -smtpath path specify the path of Z3 solver (default is /usr/local/bin/z3)" , " -smtoption opt specify options given to Z3 solver (default is \"-smt2 -in\")" , " -smttimeout t specify the timeout of Z3 smt solver (default is 5*10^6)" , " -printsmt print programs for Z3 smt solver" , " -n N set normalziation level to |N| (1--10), and" , " produce the normalized Fregel program (with types when N < 0)" , " -i generate IR" , " -a generate AST" , " -na generate Normalzed AST" , " -g generate Giraph code (default)" , " -p generate Pregel+ code" , " -o file output to a specified file" ] main :: IO () main = do ags <- getArgs (ops, files) <- getOpts ags mapM_ (processFile ops) files processFile ops file = do asts <- parseFile'' file let asts' = map topoSortOnly asts --you need to do topological sort!!!! let asts2' = if elimIdOpt ops then map transIdElim asts' else asts' -- mapM_ putStrLn $ ppProgramSpec (head asts2') -- put the type information into asts2' by using typing0. let asts2 = map (fst . typing0) asts2' let sfnss = map collectVCStepfns asts2 -- type of sfns is [[PregelStepfn]] -- ppp "sfnss = " `seq` ppp sfnss `seq` putStrLn "Hello\n" stepfns3 <- if elimCommOpt ops && useSmt ops then mapM (applySMTOpt "elimCommOpt" ops (const True) genCommElimSpec id) (zip sfnss asts2) else if useSmt ops then return $ mapM (map (\sfn -> (sfn, False))) sfnss else return (take (length asts2) (repeat [])) -- else return [] -- putStrLn ("stepfns3 = " ++ show stepfns3) let asts3 = asts2 -- mapM_ putStrLn $ ppProgramSpec (head asts3) stepfns4 <- if useV2HOpt ops && useSmt ops then mapM (applySMTOpt "voteToHaltOpt" ops isTermFix genInactivateSpec id) (zip sfnss asts3) else if useSmt ops then return $ map (map (\sfn -> (sfn, False))) sfnss else return (take (length asts3) (repeat [])) -- else return [] -- putStrLn ("stepfns4 = " ++ show stepfns4) let asts4 = asts3 let sfss = zipWith (zipWith mg) stepfns3 stepfns4 where mg ((name,_,_,_,_),ec) (_,vh) = (name, ec, if ec then vh else False) -- putStrLn ("sfss = " ++ show sfss) let pregelFiles = concat (zipWith run asts4 sfss) where run ast sfs = let nn = normLevel ops n = if nn < 0 then -nn else nn in if n < numNormStages - 1 then [(if nn < 0 then pptprintStr' else ppprintStr') n (fst (normalizationX (n+2) ast ops))] else if n == numNormStages - 1 then [printNStr' (normalizationAll' ast ops)] else genCode' ast (normalizationAll' ast ops) ops sfs mapM_ (uncurry writeFile) pregelFiles where isTermFix (_, _, _, DTermF _, _) = True isTermFix _ = False {- applySMTOpt s ops gen trans (sfns, pr) = let DProgramSpec _ (DProg _ gdefs _ _) _ = pr in do smts <- mapM (invokeSMT s ops gen gdefs) sfns let stepfns = zip sfns smts return stepfns -} -- only stepfns that satisfy `pred' are applied to SMT applySMTOpt s ops pred gen trans (sfns, pr) = do smts <- mapM f sfns let stepfns = zip sfns smts return stepfns where DProgramSpec _ (DProg _ gdefs _ _) _ = pr f sfn = if pred sfn then invokeSMT s ops gen gdefs sfn else return False invokeSMT :: String -> Option -> ([DGroundDef a] -> PregelStepfn a -> String) -> [DGroundDef a] -> PregelStepfn a -> IO Bool invokeSMT s ops gen gdefs psf@(name,_,_,_,_) = do let ga = gen gdefs psf if printSmt ops then putStrLn ga else return () putStr ("Checking " ++ s ++ " for " ++ name ++ " ... ") --putStrLn ("input to the solver: \n" ++ ga) r <- timeout to $ readProcess solver options ga -- putStrLn(show r) -- let r = Just "unsat\n" let res = case r of Just "unsat\n" -> True Just "sat\n" -> False Nothing -> False putStrLn ("done. result is " ++ (if res then "unsat" else "sat")) return res {- case r of Just "unsat\n" -> return True Nothing -> return False -} where to = smtTimeout ops -- (5 * 10^6) -- for Ubutnu, do "sudo apt-get install z3", and set the path: -- smtSolver = "/usr/bin/z3" solver = smtPath ops -- "c:/cygwin64/home/fooofo/z3/bin/z3.exe" options = words (smtOption ops) -- ["-smt2", "-in"] {- :l Main.hs ast <- parseFile' "ds_maptest.fgl" ppprint ast let nrm = normalizationAll ast --- crashes during the generation of "dsmapMain.java" let ast1 = fst (dependencyC 1 ast) ppprint ast1 let ast2 = typing ast1 ppprint ast2 let nrm = normalizationAll ast :l Main.hs ast <- parseFile' "ziptest.fgl" ppprint ast let nrm = normalizationAll ast -}