content: {- | This is the SVCOMP utility for crux-llvm.  It is designed to run
     the inputs for the "Competition on Software Verification" (SV-COMP).
     Specifically, it takes as inputs:
  
     * A file containing a specification to check, and
  
     * An architecture (either @32bit@ or @64bit@) to assume, and
  
     * A input C file.
  
     It will then attempt to verify the file against that specification,
     eventually printing @VERIFIED@, @FALSIFIED@, or @UNKNOWN@ depending on the
     results. If the result is @VERIFIED@ or @FALSFIED@, it will also produce a
     witness automaton which represents a proof that the program does or does not
     meet the specification.
  -}
  
  {-# Language DeriveAnyClass #-}
  {-# Language DeriveGeneric #-}
  {-# Language ImplicitParams #-}
  {-# Language OverloadedStrings #-}
  {-# Language RankNTypes #-}
  
  module Main (main) where
  
  import Control.Applicative ( Alternative(..) )
  import Control.Exception ( SomeException, try )
  import Control.Monad.Extra ( whenJust )
  import qualified Crypto.Hash.SHA256 as SHA256 ( hash )
  import Data.Aeson ( ToJSON )
  import qualified Data.Attoparsec.Text as Atto
  import qualified Data.ByteString.Base16 as B16 ( encode )
  import qualified Data.ByteString.Char8 as B ( readFile, unpack )
  import Data.Foldable ( traverse_, toList )
  import Data.Function ( on )
  import Data.Functor.Identity ( Identity(..) )
  import Data.Functor.WithIndex ( FunctorWithIndex(..) )
  import qualified Data.List.Extra as L
  import Data.Maybe ( mapMaybe )
  import Data.Sequence ( Seq )
  import qualified Data.Text as T
  import qualified Data.Text.Encoding as T
  import Data.Time.LocalTime ( getZonedTime )
  import Data.Version ( showVersion )
  import GHC.Generics ( Generic )
  import System.Exit ( exitFailure, exitSuccess )
  import System.FilePath ( (</>) )
  
  -- crucible
  import Lang.Crucible.Backend ( CrucibleEvent(..) )
  
  -- crux
  import qualified Crux
  import Crux.Config.Common ( CruxOptions(..), outputOptions )
  import qualified Crux.Log as Log
  import Crux.Report
  import Crux.SVCOMP hiding (SVCompLanguage(..))
  import Crux.SVCOMP.Witness
  import Crux.Types as Crux
  
  -- what4
  import What4.Expr.GroundEval ( GroundValueWrapper )
  import What4.ProgramLoc ( Position(..), ProgramLoc, plFunction, plSourceLoc )
  
  -- local
  import Crux.LLVM.Compile
  import Crux.LLVM.Config
  import qualified Crux.LLVM.Log as Log
  import Crux.LLVM.Simulate
  import CruxLLVMMain ( processLLVMOptions )
  import Paths_crux_llvm (version)
  import qualified SVComp.Log as Log
  
  data SVCompLogging
    = LoggingCrux Log.CruxLogMessage
    | LoggingCruxLLVM Log.CruxLLVMLogMessage
    | LoggingSVComp Log.SVCompLogMessage
    deriving (Generic, ToJSON)
  
  svCompLoggingToSayWhat :: SVCompLogging -> SayWhat
  svCompLoggingToSayWhat (LoggingCrux msg) = Log.cruxLogMessageToSayWhat msg
  svCompLoggingToSayWhat (LoggingCruxLLVM msg) = Log.cruxLLVMLogMessageToSayWhat msg
  svCompLoggingToSayWhat (LoggingSVComp msg) = Log.svCompLogMessageToSayWhat msg
  
  withSVCompLogging ::
    ( ( Log.SupportsCruxLogMessage SVCompLogging
      , Log.SupportsCruxLLVMLogMessage SVCompLogging
      , Log.SupportsSVCompLogMessage SVCompLogging
      ) => computation ) ->
    computation
  withSVCompLogging computation = do
    let ?injectCruxLogMessage = LoggingCrux
        ?injectCruxLLVMLogMessage = LoggingCruxLLVM
        ?injectSVCompLogMessage = LoggingSVComp
      in computation
  
  main :: IO ()
  main = withSVCompLogging $ do
    cfg <- llvmCruxConfig
    let opts = Crux.cfgJoin cfg svcompOptions
    mkOutCfg <- Crux.defaultOutputConfig svCompLoggingToSayWhat
    Crux.loadOptions mkOutCfg "crux-llvm-svcomp" version opts
      $ \(co0,(lo0,svOpts)) ->
      do (cruxOpts, llvmOpts) <- processLLVMOptions (co0{ outDir = "results" </> "SVCOMP" },lo0)
         svOpts' <- processSVCOMPOptions svOpts
         let tgt = case runIdentity $ svcompArch svOpts' of
                     Arch32 -> "i386-unknown-linux-elf"
                     Arch64 -> "x86_64-unknown-linux-elf"
             llvmOpts' = llvmOpts { targetArch = Just tgt }
         processInputFiles cruxOpts llvmOpts' svOpts'
  
  processInputFiles :: Log.Logs msgs
                    => Log.SupportsCruxLLVMLogMessage msgs
                    => Log.SupportsSVCompLogMessage msgs
                    => CruxOptions -> LLVMOptions -> SVCOMPOptions Identity
                    -> IO ()
  processInputFiles cruxOpts llvmOpts svOpts =
    traverse_ process $ Crux.inputFiles cruxOpts
    where
      process :: FilePath -> IO ()
      process inputFile = do
        mbBcFile <- genBitCodeMaybe inputFile
        whenJust mbBcFile $ \bcFile ->
          evaluateBitCode inputFile bcFile
  
      genBitCodeMaybe :: FilePath -> IO (Maybe FilePath)
      genBitCodeMaybe inputFile
        | or [ L.isSuffixOf bl inputFile | bl <- svcompBlacklist svOpts ]
        = do Log.saySVComp (Log.Skipping Log.DueToBlacklist (T.pack inputFile))
             return Nothing
        | otherwise
        = Just <$> genBitCode cruxOpts llvmOpts
  
      evaluateBitCode :: FilePath -> FilePath -> IO ()
      evaluateBitCode inputFile bcFile = withSVCompLogging $ do
        mkOutCfg <- Crux.defaultOutputConfig svCompLoggingToSayWhat
        let ?outputConfig = mkOutCfg (Just (outputOptions cruxOpts))
        mres <- try $
                 do res <- Crux.runSimulator cruxOpts (simulateLLVMFile bcFile llvmOpts)
                    generateReport cruxOpts res
                    return res
  
        case mres of
          Left e ->
            do Log.saySVComp Log.SimulatorThrewException
               Log.logException (e :: SomeException)
               exitFailure
  
          Right res@(CruxSimulationResult cmpl gls) ->
            do let numTotalGoals = sum (Crux.totalProcessedGoals . fst <$> gls)
               let numDisprovedGoals = sum (Crux.disprovedGoals . fst <$> gls)
               let numProvedGoals = sum (Crux.provedGoals . fst <$> gls)
  
               let verdict
                     | numDisprovedGoals > 0 = Falsified
                     | ProgramComplete <- cmpl
                     , numProvedGoals == numTotalGoals = Verified
                     | otherwise = Unknown
  
               specFileContents <- B.readFile $ runIdentity $ svcompSpec svOpts
               let specFileText = T.decodeUtf8 specFileContents
               prop <- case Atto.parseOnly propParse specFileText of
                         Left msg ->
                           do Log.saySVComp $ Log.PropertyParseError specFileText (T.pack msg)
                              exitFailure
                         Right p -> return p
  
               witType <- case verdict of
                            Verified  -> do Crux.logSimResult True res
                                            Log.saySVComp $ Log.Verdict Verified prop
                                            pure CorrectnessWitness
                            Falsified -> do Crux.logSimResult True res
                                            Log.saySVComp $ Log.Verdict Falsified prop
                                            pure ViolationWitness
                            Unknown   -> do Log.saySVComp $ Log.Verdict Unknown prop
                                            exitSuccess
  
               inputFileContents <- B.readFile inputFile
               creationTime <- getZonedTime
               let mkWitness nodes edges = Witness
                     { witnessType           = witType
                     , witnessSourceCodeLang = C
                     , witnessProducer       = "crux-llvm-" ++ showVersion version
                     , witnessSpecification  = L.trim $ B.unpack specFileContents
                     , witnessProgramFile    = inputFile
                     , witnessProgramHash    = B16.encode $ SHA256.hash inputFileContents
                     , witnessArchitecture   = runIdentity $ svcompArch svOpts
                     , witnessCreationTime   = creationTime
                     , witnessNodes          = nodes
                     , witnessEdges          = edges
                     }
                   trivialCorrectnessWitness = mkWitness [(mkNode 0) { nodeEntry = Just True }] []
  
               writeFile (svcompWitnessOutput svOpts) $ ppWitness $ case witType of
                 CorrectnessWitness -> trivialCorrectnessWitness
                 ViolationWitness   -> let (nodes, edges) = mkViolationWitness $ fmap snd gls
                                       in mkWitness nodes edges
  
  mkViolationWitness :: Seq ProvedGoals -> ([WitnessNode], [WitnessEdge])
  mkViolationWitness gs =
    case L.firstJust findNotProvedGoal $ toList gs of
      Nothing -> error "Could not find event log for counterexample"
      Just (_mv, events) ->
        let locs  = -- It is possible for certain LLVM instructions which do not
                    -- directly map back to source locations to be given a line
                    -- number of 0. (See #862 for an example.) Line number 0
                    -- wreaks havoc on witness validators, so we filter out such
                    -- locations to avoid this.
                    filter ((/= Just 0) . programLocSourcePosLine) $
                    -- Witness validators aren't hugely fond of using the same
                    -- line number multiple times successively, so remove
                    -- consecutive duplicates.
                    removeRepeatsBy ((==) `on` programLocSourcePosLine) $
                    mapMaybe locationReachedEventLoc events
            edges = imap violationEdge locs
            nodes = violationNodes $ length edges
        in (nodes, edges)
    where
      findNotProvedGoal :: ProvedGoals -> Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
      findNotProvedGoal (Branch pg1 pg2)          = findNotProvedGoal pg1 <|> findNotProvedGoal pg2
      findNotProvedGoal (NotProvedGoal _ _ _ _ x _) = x
      findNotProvedGoal ProvedGoal{}              = Nothing
  
      violationNodes :: Int -> [WitnessNode]
      violationNodes numEdges =
        map (\idx -> (mkNode idx)
                       { nodeEntry     = if idx == 0        then Just True else Nothing
                       , nodeViolation = if idx == numEdges then Just True else Nothing
                       })
            [0..numEdges]
  
      locationReachedEventLoc :: CrucibleEvent GroundValueWrapper -> Maybe ProgramLoc
      locationReachedEventLoc (LocationReachedEvent loc) = Just loc
      locationReachedEventLoc CreateVariableEvent{}      = Nothing
  
      violationEdge :: Int -> ProgramLoc -> WitnessEdge
      violationEdge idx loc =
        let mbSourcePos = programLocSourcePos loc in
        (mkEdge idx (idx+1))
          { edgeStartLine       = fst <$> mbSourcePos
          , edgeAssumptionScope = Just $ show $ plFunction loc
            -- crux-llvm–specific extensions
          , edgeStartColumn     = snd <$> mbSourcePos
          }
  
      programLocSourcePos :: ProgramLoc -> Maybe (Int, Int)
      programLocSourcePos pl =
        case plSourceLoc pl of
          SourcePos _ l c -> Just (l, c)
          BinaryPos{}     -> Nothing
          OtherPos{}      -> Nothing
          InternalPos     -> Nothing
  
      programLocSourcePosLine :: ProgramLoc -> Maybe Int
      programLocSourcePosLine = fmap fst . programLocSourcePos
  