{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

module Lang.Crucible.Syntax.Prog
  ( assertNoExterns
  , assertNoForwardDecs
  , doParseCheck
  ) where

import Control.Monad

import qualified Data.Map as Map
import Data.Map (Map)
import Data.Text (Text)
import qualified Data.Text.IO as T
import qualified Prettyprinter as PP
import System.IO
import System.Exit
import Text.Megaparsec as MP

import Data.Parameterized.Nonce
import Data.Parameterized.Some (Some(Some))

import qualified Lang.Crucible.CFG.Core as C
import Lang.Crucible.CFG.Extension (IsSyntaxExtension)
import Lang.Crucible.CFG.Reg
import Lang.Crucible.CFG.SSAConversion

import Lang.Crucible.Syntax.Concrete
import Lang.Crucible.Syntax.SExpr
import Lang.Crucible.Syntax.Atoms

import Lang.Crucible.Analysis.Postdom
import Lang.Crucible.FunctionHandle

import What4.FunctionName

assertNoExterns :: Map GlobalName (Some GlobalVar) -> IO ()
assertNoExterns :: Map GlobalName (Some GlobalVar) -> IO ()
assertNoExterns Map GlobalName (Some GlobalVar)
externs =
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Map GlobalName (Some GlobalVar) -> Bool
forall k a. Map k a -> Bool
Map.null Map GlobalName (Some GlobalVar)
externs) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
  do String -> IO ()
putStrLn String
"Externs not currently supported"
     IO ()
forall a. IO a
exitFailure

assertNoForwardDecs :: Map FunctionName SomeHandle -> IO ()
assertNoForwardDecs :: Map FunctionName SomeHandle -> IO ()
assertNoForwardDecs Map FunctionName SomeHandle
fds =
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Map FunctionName SomeHandle -> Bool
forall k a. Map k a -> Bool
Map.null Map FunctionName SomeHandle
fds) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
  do String -> IO ()
putStrLn String
"Forward declarations not currently supported"
     IO ()
forall a. IO a
exitFailure

-- | The main loop body, useful for both the program and for testing.
doParseCheck
   :: (IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext)
   => FilePath -- ^ The name of the input (appears in source locations)
   -> Text     -- ^ The contents of the input
   -> Bool     -- ^ Whether to pretty-print the input data as well
   -> Handle   -- ^ A handle that will receive the output
   -> IO ()
doParseCheck :: forall ext.
(IsSyntaxExtension ext, ?parserHooks::ParserHooks ext) =>
String -> Text -> Bool -> Handle -> IO ()
doParseCheck String
fn Text
theInput Bool
pprint Handle
outh =
  do Some NonceGenerator IO x
ng <- IO (Some (NonceGenerator IO))
newIONonceGenerator
     HandleAllocator
ha <- IO HandleAllocator
newHandleAllocator
     case Parsec Void Text [Syntax Atomic]
-> String
-> Text
-> Either (ParseErrorBundle Text Void) [Syntax Atomic]
forall e s a.
Parsec e s a -> String -> s -> Either (ParseErrorBundle s e) a
MP.parse (Parser ()
skipWhitespace Parser ()
-> Parsec Void Text [Syntax Atomic]
-> Parsec Void Text [Syntax Atomic]
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Void Text Identity (Syntax Atomic)
-> Parsec Void Text [Syntax Atomic]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many (Parser Atomic -> ParsecT Void Text Identity (Syntax Atomic)
forall a. Parser a -> Parser (Syntax a)
sexp Parser Atomic
atom) Parsec Void Text [Syntax Atomic]
-> Parser () -> Parsec Void Text [Syntax Atomic]
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
eof) String
fn Text
theInput of
       Left ParseErrorBundle Text Void
err ->
         do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ ParseErrorBundle Text Void -> String
forall s e.
(VisualStream s, TraversableStream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> String
errorBundlePretty ParseErrorBundle Text Void
err
            IO ()
forall a. IO a
exitFailure
       Right [Syntax Atomic]
v ->
         do Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
pprint (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
              [Syntax Atomic] -> (Syntax Atomic -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Syntax Atomic]
v ((Syntax Atomic -> IO ()) -> IO ())
-> (Syntax Atomic -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$
                \Syntax Atomic
e -> Handle -> Text -> IO ()
T.hPutStrLn Handle
outh (Syntax Atomic -> Text
forall {k} (s :: k). Syntax Atomic -> Text
printExpr Syntax Atomic
e) IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Handle -> String -> IO ()
hPutStrLn Handle
outh String
""
            Either (ExprErr x) (ParsedProgram ext)
cs <- NonceGenerator IO x
-> HandleAllocator
-> [(SomeHandle, Position)]
-> TopParser x (ParsedProgram ext)
-> IO (Either (ExprErr x) (ParsedProgram ext))
forall s a.
NonceGenerator IO s
-> HandleAllocator
-> [(SomeHandle, Position)]
-> TopParser s a
-> IO (Either (ExprErr s) a)
top NonceGenerator IO x
ng HandleAllocator
ha [] (TopParser x (ParsedProgram ext)
 -> IO (Either (ExprErr x) (ParsedProgram ext)))
-> TopParser x (ParsedProgram ext)
-> IO (Either (ExprErr x) (ParsedProgram ext))
forall a b. (a -> b) -> a -> b
$ [Syntax Atomic] -> TopParser x (ParsedProgram ext)
forall ext s.
(TraverseExt ext, IsSyntaxExtension ext,
 ?parserHooks::ParserHooks ext) =>
[Syntax Atomic] -> TopParser s (ParsedProgram ext)
prog [Syntax Atomic]
v
            case Either (ExprErr x) (ParsedProgram ext)
cs of
              Left ExprErr x
err -> Handle -> String -> IO ()
hPutStrLn Handle
outh (Doc Any -> String
forall a. Show a => a -> String
show (ExprErr x -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. ExprErr x -> Doc ann
PP.pretty ExprErr x
err))
              Right (ParsedProgram{ parsedProgCFGs :: forall ext. ParsedProgram ext -> [AnyCFG ext]
parsedProgCFGs = [AnyCFG ext]
ok
                                  , parsedProgExterns :: forall ext. ParsedProgram ext -> Map GlobalName (Some GlobalVar)
parsedProgExterns = Map GlobalName (Some GlobalVar)
externs
                                  , parsedProgForwardDecs :: forall ext. ParsedProgram ext -> Map FunctionName SomeHandle
parsedProgForwardDecs = Map FunctionName SomeHandle
fds
                                  }) -> do
                Map GlobalName (Some GlobalVar) -> IO ()
assertNoExterns Map GlobalName (Some GlobalVar)
externs
                Map FunctionName SomeHandle -> IO ()
assertNoForwardDecs Map FunctionName SomeHandle
fds
                [AnyCFG ext] -> (AnyCFG ext -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [AnyCFG ext]
ok ((AnyCFG ext -> IO ()) -> IO ()) -> (AnyCFG ext -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$
                 \(AnyCFG CFG ext blocks init ret
theCfg) ->
                   do C.SomeCFG CFG ext blocks init ret
ssa <- SomeCFG ext init ret -> IO (SomeCFG ext init ret)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SomeCFG ext init ret -> IO (SomeCFG ext init ret))
-> SomeCFG ext init ret -> IO (SomeCFG ext init ret)
forall a b. (a -> b) -> a -> b
$ CFG ext blocks init ret -> SomeCFG ext init ret
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
IsSyntaxExtension ext =>
CFG ext s init ret -> SomeCFG ext init ret
toSSA CFG ext blocks init ret
theCfg
                      Handle -> String -> IO ()
hPutStrLn Handle
outh (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ FnHandle init ret -> String
forall a. Show a => a -> String
show (FnHandle init ret -> String) -> FnHandle init ret -> String
forall a b. (a -> b) -> a -> b
$ CFG ext blocks init ret -> FnHandle init ret
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> FnHandle init ret
cfgHandle CFG ext blocks init ret
theCfg
                      Handle -> String -> IO ()
hPutStrLn Handle
outh (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Bool -> CFGPostdom blocks -> CFG ext blocks init ret -> Doc Any
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType) ann.
PrettyExt ext =>
Bool -> CFGPostdom blocks -> CFG ext blocks init ret -> Doc ann
C.ppCFG' Bool
True (CFG ext blocks init ret -> CFGPostdom blocks
forall ext (b :: Ctx (Ctx CrucibleType)) (i :: Ctx CrucibleType)
       (r :: CrucibleType).
CFG ext b i r -> CFGPostdom b
postdomInfo CFG ext blocks init ret
ssa) CFG ext blocks init ret
ssa