{- CAO Compiler
Copyright (C) 2014 Cryptography and Information Security Group, HASLab - INESC TEC and Universidade do Minho
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see . -}
{-# LANGUAGE PatternGuards #-}
{-
Module : $Header$
Description : Compiler main module
Copyright : (C) 2014 Cryptography and Information Security Group, HASLab - INESC TEC and Universidade do Minho
License : GPL
Maintainer : Paulo Silva
Stability : experimental
Portability : non-portable
-}
module Main.Compiler ( caoComp ) where
import Control.Monad
import Control.Monad.State
import Data.Maybe (fromMaybe)
import System.Directory (doesFileExist, getPermissions, readable, findExecutable)
import System.FilePath(splitExtension, addExtension, takeFileName)
import System.IO
import Language.CAO.Analysis.CFG
import Language.CAO.Analysis.SSA
import Language.CAO.Common.Error
import Language.CAO.Common.Monad
import Language.CAO.Common.State
import Language.CAO.Common.Var
import Language.CAO.Parser.Config
import Language.CAO.Parser.Parser ( parseFile )
import Language.CAO.Platform.Specification
import Language.CAO.Syntax
import Language.CAO.Syntax.Tidy
import Language.CAO.Transformation.Expand
import Language.CAO.Transformation.Eval
import Language.CAO.Transformation.Indist
import Language.CAO.Transformation.Simplify
import Language.CAO.Transformation.Target
import qualified Language.CAO.Translation.C as NC
import Language.CAO.Translation.PreC
import Language.CAO.Typechecker ( tcCaoAST )
import Main.Flags
import Main.Dot
_WRONG_MODE :: a
_WRONG_MODE = error ": Panic! unexpected mode!"
caoComp :: Options -> IO ()
caoComp opts@(Comp {}) = do
-- Check config file
let cfg_file = config opts
exists_cfg <- doesFileExist cfg_file
when (not exists_cfg) $
error $ "Error: could not find config file: `" ++ cfg_file ++ "'."
cfg_permissions <- getPermissions cfg_file
when (not (readable cfg_permissions)) $
error $ "Error: config file `" ++ cfg_file ++ "' is not readable."
-- Check input file
let input_file = input opts
(file, extension) = splitExtension input_file
when (null input_file) $ error $ "Error: no input file."
exists_input <- doesFileExist input_file
when (not exists_input) $
error $ "Error: could not find input file: `" ++ input_file ++ "'."
when (extension /= ".cao") $
error $ "Error: input file format not recognized: `" ++ extension ++"'."
input_permissions <- getPermissions input_file
when (not (readable input_permissions)) $
error $ "Error: input file `" ++ input_file ++ "' is not readable."
-- Check Yices
yices <- checkYices
-- Output file
let output_file = fromMaybe (addExtension (takeFileName file) ".c") (output opts)
cfg <- loadConfig cfg_file
(c_prog, warn) <- runCaoResultWarn $ compile cfg opts yices
hPutStrLn stderr $ showCaoWarnings warn
writeFile output_file c_prog
caoComp _
= _WRONG_MODE
checkYices :: IO (Maybe FilePath)
checkYices = do
yices <- findExecutable "yices"
maybe (hPutStrLn stderr "Without Yices some conditions may not be verified correctly") (const (return ())) yices
return yices
--------------------------------------------------------------------------------
-- Main compilation function:
-- pipeline = parser -> typechecker -> seq expansion
-- -> eval -> simplify -> optimize -> C
compile :: TranslationSpec -> Options -> Maybe FilePath -> CaoResult String
compile cfg opts yices = do
let file_name = input opts
setFileName file_name
setYices yices
-- Parse
parsed_ast <- parseFile file_name
-- TypeCheck prog
let mode = runmode opts
(tc_ast,_) <- tcCaoAST mode parsed_ast
dump mode (verbose opts) (ddump_tc opts) (dcheck opts) tc_ast
-- Expand sequences
seq_exp_ast <- whenOpt (fexpand)
(\_ a -> expandSequences a) opts tc_ast
dump mode (verbose opts) (ddump_expand opts && fexpand opts) (dcheck opts) seq_exp_ast
-- Eval
let eval_ast = evalExpr seq_exp_ast
dump mode (verbose opts) (ddump_eval opts) (dcheck opts) eval_ast
-- Simplify
simpl_ast <- simplifyCaoAST (initProcName $ globalTransSpec cfg) eval_ast
dump mode (verbose opts) (ddump_simpl opts) (dcheck opts) simpl_ast
-- Optimize
opt_ast <- whenOpt optimize
optProg opts simpl_ast
dump mode (verbose opts) (ddump_opt opts) (dcheck opts) opt_ast
--- Platform dependent ---
-- Not valid CAO code anymore --
-- Target
target_ast <- targetCaoAST cfg opt_ast
dump mode (verbose opts) (ddump_target opts) (dcheck opts) target_ast
-- PreC
prec_ast <- cao2prec cfg target_ast
dump mode (verbose opts) (ddump_prec opts) (dcheck opts) prec_ast
-- Cao2C
NC.cao2c cfg prec_ast
--------------------------------------------------------------------------------
-- Optimization
whenOpt :: Monad m =>
(Options -> Bool) -> (Options -> a -> m a) -> Options -> a -> m a
whenOpt fm f o a
| fm o = f o a
| otherwise = return a
optProg :: Options -> Prog Var -> CaoResult (Prog Var)
optProg opts prog = do
-- ToCFG
let cfg = buildCFG prog
maybe (return ()) (generateCFG opts cfg) $ dgen_cfg opts
-- ToSSA
ssa_cfg <- mapM toSSA cfg
maybe (return ()) (generateCFG opts ssa_cfg) $ dgen_ssa opts
-- SSA back translation
let back_cfg' = map fromSSA ssa_cfg
-- >> Indistinguishable functions
back_cfg <- maybe (return back_cfg') (flip (uncurry mkIndistFun) back_cfg') $ findist_fun opts
-- From CFG
let opt_ast = toAST back_cfg
return opt_ast
--------------------------------------------------------------------------------
-- Dump mode
dump :: RunMode -> Bool -> Bool -> Bool -> Prog Var -> CaoResult ()
dump m _ True True = \ ast -> do
s <- get
put initialState
_ <- tcCaoAST m (fmap varName (tidyCaoAST ast))
put s
liftIO $ hPutStrLn stderr "Dumped code type checked with success"
dump _ v True False
= liftIO . hPutStrLn stderr . doDump
where
doDump | v = showCaoASTDebug
| otherwise = showCaoAST
dump _ _ False _
= const $ return ()