Skip to content
Snippets Groups Projects
Main.hs 7.84 KiB
Newer Older
  • Learn to ignore specific revisions
  • chrg's avatar
    chrg committed
    {-# LANGUAGE ApplicativeDo #-}
    
    chrg's avatar
    chrg committed
    {-# LANGUAGE BlockArguments #-}
    {-# LANGUAGE DerivingVia #-}
    
    chrg's avatar
    chrg committed
    {-# LANGUAGE FlexibleContexts #-}
    
    chrg's avatar
    chrg committed
    {-# LANGUAGE ImportQualifiedPost #-}
    
    chrg's avatar
    chrg committed
    {-# LANGUAGE OverloadedStrings #-}
    
    chrg's avatar
    chrg committed
    
    
    chrg's avatar
    chrg committed
    import Control.Monad.IRTree qualified as IRTree
    
    chrg's avatar
    chrg committed
    import ReduceC qualified
    
    chrg's avatar
    chrg committed
    
    
    chrg's avatar
    chrg committed
    import Colog
    import Control.Applicative
    import Control.Monad
    
    import Control.Monad.State
    
    chrg's avatar
    chrg committed
    import Data.Foldable
    
    chrg's avatar
    chrg committed
    import Data.Function
    
    chrg's avatar
    chrg committed
    import Data.Functor
    
    chrg's avatar
    chrg committed
    import Data.IORef (atomicModifyIORef', atomicWriteIORef, newIORef)
    
    chrg's avatar
    chrg committed
    import Data.List.NonEmpty qualified as NE
    
    chrg's avatar
    chrg committed
    import Data.RPath qualified as RPath
    
    chrg's avatar
    chrg committed
    import Data.Text qualified as Text
    
    import Data.Time (getCurrentTime)
    import Data.Time qualified as Time
    
    chrg's avatar
    chrg committed
    import Data.Time.Format.ISO8601 (iso8601Show)
    
    chrg's avatar
    chrg committed
    import GHC.Stack
    
    chrg's avatar
    chrg committed
    import Language.C qualified as C
    
    chrg's avatar
    chrg committed
    import Options.Applicative
    import System.Directory
    import System.Exit
    import System.FilePath
    import System.IO
    
    chrg's avatar
    chrg committed
    import System.IO.Error (tryIOError)
    
    chrg's avatar
    chrg committed
    import System.IO.Temp
    
    chrg's avatar
    chrg committed
    import System.Process.Typed
    import Text.Pretty.Simple
    import Text.PrettyPrint qualified as P
    import Prelude hiding (log)
    
    chrg's avatar
    chrg committed
    
    main :: IO ()
    
    chrg's avatar
    chrg committed
    main =
      join
        . execParser
    
    chrg's avatar
    chrg committed
        $ info (run <**> helper)
    
    chrg's avatar
    chrg committed
          . fold
    
    chrg's avatar
    chrg committed
        $ []
    
    process :: (WithLog env (Msg sev) m, MonadIO m) => sev -> Text.Text -> m a -> m a
    process sev p ma = do
      msg "Started "
      a <- ma
      msg "Done "
      pure a
    
    chrg's avatar
    chrg committed
     where
    
    chrg's avatar
    chrg committed
      s = withFrozenCallStack callStack
      msg t = Colog.logMsg (Msg sev s (t <> p))
    
    
    chrg's avatar
    chrg committed
    data Mode
      = Lin
      | Exp
      deriving (Show, Read, Eq, Ord, Enum)
    
    
    chrg's avatar
    chrg committed
    run :: (HasCallStack) => Parser (IO ())
    run = do
    
    chrg's avatar
    chrg committed
      mode <-
        option auto $
    
    chrg's avatar
    chrg committed
          fold
    
    chrg's avatar
    chrg committed
            [ long "mode"
    
    chrg's avatar
    chrg committed
            , help "search mode (Lin, Exp)"
            , value Exp
    
    chrg's avatar
    chrg committed
            ]
    
    chrg's avatar
    chrg committed
    
    
    chrg's avatar
    chrg committed
      verbose <-
        flag False True $
          fold
            [ long "verbose"
            , short 'v'
            , help "log more"
            ]
    
    
      checkmode <-
    
    chrg's avatar
    chrg committed
        flag False True $
          fold
    
            [ long "dry-run"
            , short 'n'
            , help "don't do any reduction"
            ]
    
    
    chrg's avatar
    chrg committed
      keywords <-
        many . option auto $
          fold
            [ long "keyword"
            , short 'k'
    
    chrg's avatar
    chrg committed
            , help "special versions of the code"
    
    chrg's avatar
    chrg committed
            ]
    
    
    chrg's avatar
    chrg committed
      validity <-
    
    chrg's avatar
    chrg committed
        optional $
    
    chrg's avatar
    chrg committed
          option auto $
    
    chrg's avatar
    chrg committed
            fold
              [ long "validity"
    
    chrg's avatar
    chrg committed
              , short 'V'
              , help "check the output for the validity code and output debug information"
    
    chrg's avatar
    chrg committed
              ]
    
    chrg's avatar
    chrg committed
    
    
    chrg's avatar
    chrg committed
      debug <-
        flag False True $
          fold
            [ long "debug"
            , short 'D'
            , help "keep debug versions of all copies"
            ]
    
    
    chrg's avatar
    chrg committed
      fixpoint <-
        flag False True $
          fold
            [ long "fixpoint"
            , short 'F'
            , help "run the computation to a fixpoint"
            ]
    
    
    chrg's avatar
    chrg committed
      pedandic <-
    
    chrg's avatar
    chrg committed
        flag False True $
          fold
    
    chrg's avatar
    chrg committed
            [ long "pedandic"
            , short 'P'
            , help "when checking for validity, throw error if command fails"
    
    chrg's avatar
    chrg committed
            ]
    
    chrg's avatar
    chrg committed
    
      cmd <- strArgument $ fold [metavar "COMMAND"]
    
      file <- strArgument $ fold [metavar "FILE"]
    
    chrg's avatar
    chrg committed
    
    
    chrg's avatar
    chrg committed
        time <- getCurrentTime
    
        let
          fmt m = do
            t' <- getCurrentTime
            pure
              ( Text.pack
                  ( Time.formatTime
                      Time.defaultTimeLocale
                      "%_3m:%04ES "
    
    chrg's avatar
    chrg committed
                      (t' `Time.diffUTCTime` time)
    
    chrg's avatar
    chrg committed
        let logger =
              filterBySeverity (if verbose then Debug else Info) msgSeverity $
                cmapM fmt logTextStderr
    
        usingLoggerT logger do
    
    chrg's avatar
    chrg committed
          counter <- liftIO (newIORef (0 :: Int))
    
    
    chrg's avatar
    chrg committed
          let
            test f = process D ("test " <> Text.pack f) do
    
    chrg's avatar
    chrg committed
              err <- liftIO $ runProcess (proc cmd [])
    
    chrg's avatar
    chrg committed
              log D (Text.pack $ show err)
    
    chrg's avatar
    chrg committed
              pure err
    
    chrg's avatar
    chrg committed
    
    
    chrg's avatar
    chrg committed
            output f c = process D ("writing " <> Text.pack f) do
              let x = P.render (C.pretty (c $> C.undefNode))
              liftIO $ writeFile f x
    
    
            cleanup f = do
              logError "Cleaning up"
              liftIO do
                copyFile (f <.> "bak") f
                removeFile (f <.> "bak")
              liftIO exitFailure
    
    
    chrg's avatar
    chrg committed
            check ::
              FilePath ->
              [RPath.AnnotatedChoice (String, C.Position)] ->
              C.CTranslationUnit C.NodeInfo ->
              LoggerT (Msg Severity) IO Bool
    
    chrg's avatar
    chrg committed
            check f l c = process D "Checking predictate" do
    
    chrg's avatar
    chrg committed
              let xs = NE.nonEmpty (filter ((RPath.Yes ==) . RPath.choice) l)
    
    chrg's avatar
    chrg committed
              let decided = length l - RPath.numberOfUndecided l
    
    chrg's avatar
    chrg committed
    
              count <- liftIO (atomicModifyIORef' counter (\a -> (a + 1, a)))
    
    chrg's avatar
    chrg committed
              logInfo
    
    chrg's avatar
    chrg committed
                ( "Checking (num: "
                    <> Text.pack (show count)
                    <> ") D="
    
    chrg's avatar
    chrg committed
                    <> Text.pack (show decided <> "/" <> show (length l))
    
    chrg's avatar
    chrg committed
                    <> ": "
    
    chrg's avatar
    chrg committed
                    <> Text.pack (maybe "-" ((\(r, p) -> r <> " at " <> show p) . RPath.label . NE.last) xs)
    
    chrg's avatar
    chrg committed
                )
    
    chrg's avatar
    chrg committed
              output f c
    
    chrg's avatar
    chrg committed
              res <- test f
    
    chrg's avatar
    chrg committed
              when debug $ liftIO do
                copyFile f ("case-" <> show count <.> "c")
    
    
    chrg's avatar
    chrg committed
              ret <- case res of
                ExitSuccess -> do
                  liftIO $ copyFile f (f <.> "last")
                  pure True
                ExitFailure x
                  | Just x == validity -> do
                      folder <- liftIO do
    
    chrg's avatar
    chrg committed
                        temp <- getCanonicalTemporaryDirectory
    
    chrg's avatar
    chrg committed
                        createTempDirectory temp "rtree-c"
                      logWarning $ "Produced invalid code, see " <> Text.pack folder <> " for details"
                      liftIO do
    
    chrg's avatar
    chrg committed
                        withFile (folder </> "reduction.path") WriteMode \h -> do
                          forM (takeWhile ((/= RPath.Undecided) . RPath.choice) l) \(RPath.AnnotatedChoice c' (msg, pos)) -> do
                            hPutStr h [RPath.debugShowChoice c']
                            hPutStr h " "
                            hPutStr h msg
                            hPutStr h " at "
                            hPrint h pos
    
    chrg's avatar
    chrg committed
                        copyFile cmd (folder </> takeFileName cmd)
    
    chrg's avatar
    chrg committed
                        copyFile f (folder </> takeFileName f)
    
    chrg's avatar
    chrg committed
                        tryIOError do
                          copyFile (f <.> "last") (folder </> takeFileName (f <.> "last"))
    
    chrg's avatar
    chrg committed
                        pure folder
                      when pedandic do
                        logError "Pedandic, stoping now."
                        liftIO exitFailure
                      pure False
                  | otherwise -> pure False
              logInfo ("Predicate was " <> Text.pack (show ret))
              pure ret
    
    chrg's avatar
    chrg committed
    
    
    chrg's avatar
    chrg committed
          let bak = file <.> "bak"
    
          process D "backing up file" do
            liftIO $ copyFile file bak
    
          process I "check predicate" do
            t <- test file
    
    chrg's avatar
    chrg committed
            unless (t == ExitSuccess) do
    
    chrg's avatar
    chrg committed
              logError "did not satisify predicate"
    
    chrg's avatar
    chrg committed
              liftIO exitFailure
    
          c <- process D "parsing file" do
            parseCFile file
    
          output file c
    
          process I "sanity checks" do
            c' <- parseCFile file
            unless (void c' == void c) do
              liftIO do
                withFile "error.1.hs" WriteMode (`pHPrint` void c)
                withFile "error.2.hs" WriteMode (`pHPrint` void c')
    
              logError "Outputted a different file than I read... Please report original file and error.{1,2}.hs"
    
    chrg's avatar
    chrg committed
              liftIO exitFailure
    
    
    chrg's avatar
    chrg committed
            let rtree = ReduceC.defaultReduceCWithKeywords keywords c
            t <- check file [] (IRTree.extract rtree)
    
    
    chrg's avatar
    chrg committed
            unless t do
    
              logError "file did not satisfy predicate"
    
    chrg's avatar
    chrg committed
              liftIO exitFailure
    
    
          when checkmode do
    
    chrg's avatar
    chrg committed
            logInfo "In checking mode, stopping now"
    
            liftIO exitSuccess
    
    chrg's avatar
    chrg committed
    
    
    chrg's avatar
    chrg committed
          l <-
    
    chrg's avatar
    chrg committed
            c & fix \rec prevc -> do
    
    chrg's avatar
    chrg committed
              let rtree = ReduceC.defaultReduceCWithKeywords keywords prevc
              c' <- case mode of
                Lin -> IRTree.reduce (check file) rtree
                Exp -> IRTree.reduceAdaptive (check file) rtree
    
    
    chrg's avatar
    chrg committed
              if fixpoint && (c' $> ()) /= (prevc $> ())
                then do
                  logInfo "Running again until fixpoint"
                  rec c'
                else pure c'
    
    chrg's avatar
    chrg committed
    
    
    chrg's avatar
    chrg committed
          output file l
    
    chrg's avatar
    chrg committed
          logInfo "Everything went well"
    
    chrg's avatar
    chrg committed
     where
      parseCFile file = do
        res <- liftIO $ C.parseCFilePre file
        case res of
          Right c -> pure c
          Left err -> do
            logError (Text.pack (show err))
            liftIO exitFailure