crux-llvm-0.8: svcomp/Main.hs
{- | 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