content: {-|
  
  Module that automatically runs a user's static checker.
  
  staticCheckFunctionAsyn sets up the static checker's internal state given the user's
  configuration object. Then, it calls checkPaths to check every path in the given
  file.
  
  checkPaths automatically applies the user's static checker to each path in the file.
  
  -}
  module Static.Check (staticCheckFunctionAsync) where
  
  import           Control.Concurrent.STM.TQueue
  import           Control.Concurrent.Thread.Group
  import           Control.Monad.State.Strict      (forM_, unless, void)
  import           Control.Monad.State.Strict      (get, liftIO)
  import           Data.Maybe
  import           InternalIR.ModuleInfo
  import           LLVM.AST
  import           LLVMAST.Interface
  import           Prelude                         hiding (mod)
  import           Static.CheckerConfigDef
  import           Static.CheckerState
  
  -- | Setup an internal checker state and automatically run the user's static checker
  staticCheckFunctionAsync :: (Show a, Show b, Ord b)
                           => TQueue b
                           -> ThreadGroup
                           -> FilePath
                           -> ModuleInfo
                           -> Definition
                           -> CheckerConfig a b
                           -> IO ()
  staticCheckFunctionAsync tQueue tg filepath mod def config
    | isJust mBasicBlocks && not (null basicBlocks) = do
        let cfg0s = stateFromConfig filepath mod def config
            cfg1s = map (\cfg -> cfg { curBugs = tQueue, curTGroup = tg }) cfg0s
            act = do cfgInitialAction config
                     checkPaths config
                     cfgFinalAction config
        forM_ cfg1s $ \cfg1 -> evalChecker act cfg1
    | otherwise = return ()
    where
      mBasicBlocks = getFunctionBBs def
      basicBlocks = fromJust mBasicBlocks
  
  -- | Statically check all paths up to a bound specified by config.
  -- checkPaths applies the user's static checking function, also found in config,
  -- to each line of LLVM IR on each path. To do so, checkPaths creates an LLVM IR
  -- control flow graph on the fly (getNextBlocks).
  checkPaths :: (Show a, Show b)
             => CheckerConfig a b
             -> Checker a b ()
  checkPaths config = do
    -- Perform the check on each instruction in the block
    block <- getCurBlock
    path <- getPath
    forM_ (zip [0..] $ getBlockContents block) $ \(num, ninstr) -> cfgCheck config num ninstr
    -- Figure out if we should keep exploring this path
    nextBlocks <- getNextBlocks
    bound <- getBlockBound
    maxLoops <- getLoopBound
    -- Don't continue if the path is too long
    unless (length path >= bound) $ do
      forM_ nextBlocks $ \nextBlock -> fork $ do
        -- Don't continue if we've been through this loop too many times
        unless (occurs nextBlock path >= maxLoops) $ do
          -- Go to the next block and check it
          advanceTo nextBlock
          checkPaths config
  
  -- | Fork a thread in checker monad.
  fork :: Checker a b () -> Checker a b ()
  fork act = do
    s0 <- get
    void $ liftIO $ forkIO (curTGroup s0) $ evalChecker act s0
  
  occurs :: Eq a => a -> [a] -> Int
  occurs x = length . filter (x==)
  