fregel-1.2.0: compiler/Main.hs
{-# 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
-}