Crux.SVCOMP

This module provides various helper functionality for participating in the SV-COMP comptetion, including parsing comptetion set files, configuration data, reporting results, etc.

Documentation

data SVCOMPOptions (f :: Type -> Type)

Constructors

SVCOMPOptions

Fields

• svcompBlacklist :: [FilePath]

  Benchmarks to skip when evaluating in SV-COMP mode

• svcompArch :: f Arch

  The architecture assumed for the verification task

• svcompSpec :: f FilePath

  The file containing the specification text used to verify the program. Likely a .prp file.

• svcompWitnessOutput :: FilePath

  Write the witness automaton to this filename

data Arch

Constructors

Arch32

Arch64

Instances

Show Arch

Defined in Crux.SVCOMP

Methods

showsPrec :: Int -> Arch -> ShowS

show :: Arch -> String

showList :: [Arch] -> ShowS

Eq Arch

Defined in Crux.SVCOMP

Methods

(==) :: Arch -> Arch -> Bool

(/=) :: Arch -> Arch -> Bool

Ord Arch

Defined in Crux.SVCOMP

Methods

compare :: Arch -> Arch -> Ordering

(<) :: Arch -> Arch -> Bool

(<=) :: Arch -> Arch -> Bool

(>) :: Arch -> Arch -> Bool

(>=) :: Arch -> Arch -> Bool

max :: Arch -> Arch -> Arch

min :: Arch -> Arch -> Arch

archSpec :: ValueSpec Arch

parseArch :: (Arch -> opts -> opts) -> String -> OptSetter opts

processSVCOMPOptions :: SVCOMPOptions Maybe -> IO (SVCOMPOptions Identity)

We cannot verify an SV-COMP program without knowing the architecture and the specification. Unfortunately, Crux's command-line argument parser makes it somewhat awkward to require certain arguments (without defaults). As a hacky workaround, we parse the command-line arguments for the architecture/specification as if they were optional and later check here to see if they were actually provided, throwing an error if they were not provided.

svcompOptions :: Config (SVCOMPOptions Maybe)

propertyVerdict :: VerificationTask -> Maybe Bool

data ComputedVerdict

Constructors

Verified

Falsified

Unknown

Instances

ToJSON ComputedVerdict

Defined in Crux.SVCOMP

Methods

toJSON :: ComputedVerdict -> Value

toEncoding :: ComputedVerdict -> Encoding

toJSONList :: [ComputedVerdict] -> Value

toEncodingList :: [ComputedVerdict] -> Encoding

omitField :: ComputedVerdict -> Bool

Generic ComputedVerdict

Defined in Crux.SVCOMP

Associated Types

type Rep ComputedVerdict :: Type -> Type

Methods

from :: ComputedVerdict -> Rep ComputedVerdict x

to :: Rep ComputedVerdict x -> ComputedVerdict

Show ComputedVerdict

Defined in Crux.SVCOMP

Methods

showsPrec :: Int -> ComputedVerdict -> ShowS

show :: ComputedVerdict -> String

showList :: [ComputedVerdict] -> ShowS

Eq ComputedVerdict

Defined in Crux.SVCOMP

Methods

(==) :: ComputedVerdict -> ComputedVerdict -> Bool

(/=) :: ComputedVerdict -> ComputedVerdict -> Bool

Ord ComputedVerdict

Defined in Crux.SVCOMP

Methods

compare :: ComputedVerdict -> ComputedVerdict -> Ordering

(<) :: ComputedVerdict -> ComputedVerdict -> Bool

(<=) :: ComputedVerdict -> ComputedVerdict -> Bool

(>) :: ComputedVerdict -> ComputedVerdict -> Bool

(>=) :: ComputedVerdict -> ComputedVerdict -> Bool

max :: ComputedVerdict -> ComputedVerdict -> ComputedVerdict

min :: ComputedVerdict -> ComputedVerdict -> ComputedVerdict

type Rep ComputedVerdict

Defined in Crux.SVCOMP

type Rep ComputedVerdict = D1 ('MetaData "ComputedVerdict" "Crux.SVCOMP" "crux-0.7-DD4jascIe8aJ5p2f7vnjLq" 'False) (C1 ('MetaCons "Verified" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Falsified" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Unknown" 'PrefixI 'False) (U1 :: Type -> Type)))

data BenchmarkSet

Constructors

BenchmarkSet

Fields

• benchmarkName :: Text
• benchmarkTasks :: [VerificationTask]

Instances

Show BenchmarkSet

Defined in Crux.SVCOMP

Methods

showsPrec :: Int -> BenchmarkSet -> ShowS

show :: BenchmarkSet -> String

showList :: [BenchmarkSet] -> ShowS

Eq BenchmarkSet

Defined in Crux.SVCOMP

Methods

(==) :: BenchmarkSet -> BenchmarkSet -> Bool

(/=) :: BenchmarkSet -> BenchmarkSet -> Bool

Ord BenchmarkSet

Defined in Crux.SVCOMP

Methods

compare :: BenchmarkSet -> BenchmarkSet -> Ordering

(<) :: BenchmarkSet -> BenchmarkSet -> Bool

(<=) :: BenchmarkSet -> BenchmarkSet -> Bool

(>) :: BenchmarkSet -> BenchmarkSet -> Bool

(>=) :: BenchmarkSet -> BenchmarkSet -> Bool

max :: BenchmarkSet -> BenchmarkSet -> BenchmarkSet

min :: BenchmarkSet -> BenchmarkSet -> BenchmarkSet

data SVCompProperty

Constructors

CheckNoError Text

CheckValidFree

CheckValidDeref

CheckValidMemtrack

CheckValidMemCleanup

CheckDefBehavior

CheckNoOverflow

CheckTerminates

CoverageFQL Text

Instances

ToJSON SVCompProperty

Defined in Crux.SVCOMP

Methods

toJSON :: SVCompProperty -> Value

toEncoding :: SVCompProperty -> Encoding

toJSONList :: [SVCompProperty] -> Value

toEncodingList :: [SVCompProperty] -> Encoding

omitField :: SVCompProperty -> Bool

Generic SVCompProperty

Defined in Crux.SVCOMP

Associated Types

type Rep SVCompProperty :: Type -> Type

Methods

from :: SVCompProperty -> Rep SVCompProperty x

to :: Rep SVCompProperty x -> SVCompProperty

Show SVCompProperty

Defined in Crux.SVCOMP

Methods

showsPrec :: Int -> SVCompProperty -> ShowS

show :: SVCompProperty -> String

showList :: [SVCompProperty] -> ShowS

Eq SVCompProperty

Defined in Crux.SVCOMP

Methods

(==) :: SVCompProperty -> SVCompProperty -> Bool

(/=) :: SVCompProperty -> SVCompProperty -> Bool

Ord SVCompProperty

Defined in Crux.SVCOMP

Methods

compare :: SVCompProperty -> SVCompProperty -> Ordering

(<) :: SVCompProperty -> SVCompProperty -> Bool

(<=) :: SVCompProperty -> SVCompProperty -> Bool

(>) :: SVCompProperty -> SVCompProperty -> Bool

(>=) :: SVCompProperty -> SVCompProperty -> Bool

max :: SVCompProperty -> SVCompProperty -> SVCompProperty

min :: SVCompProperty -> SVCompProperty -> SVCompProperty

type Rep SVCompProperty

Defined in Crux.SVCOMP

type Rep SVCompProperty = D1 ('MetaData "SVCompProperty" "Crux.SVCOMP" "crux-0.7-DD4jascIe8aJ5p2f7vnjLq" 'False) (((C1 ('MetaCons "CheckNoError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text)) :+: C1 ('MetaCons "CheckValidFree" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CheckValidDeref" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CheckValidMemtrack" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "CheckValidMemCleanup" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CheckDefBehavior" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CheckNoOverflow" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CheckTerminates" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CoverageFQL" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text))))))

data SVCompLanguage

Constructors

C CDataModel

Java

Instances

Show SVCompLanguage

Defined in Crux.SVCOMP

Methods

showsPrec :: Int -> SVCompLanguage -> ShowS

show :: SVCompLanguage -> String

showList :: [SVCompLanguage] -> ShowS

Eq SVCompLanguage

Defined in Crux.SVCOMP

Methods

(==) :: SVCompLanguage -> SVCompLanguage -> Bool

(/=) :: SVCompLanguage -> SVCompLanguage -> Bool

Ord SVCompLanguage

Defined in Crux.SVCOMP

Methods

compare :: SVCompLanguage -> SVCompLanguage -> Ordering

(<) :: SVCompLanguage -> SVCompLanguage -> Bool

(<=) :: SVCompLanguage -> SVCompLanguage -> Bool

(>) :: SVCompLanguage -> SVCompLanguage -> Bool

(>=) :: SVCompLanguage -> SVCompLanguage -> Bool

max :: SVCompLanguage -> SVCompLanguage -> SVCompLanguage

min :: SVCompLanguage -> SVCompLanguage -> SVCompLanguage

data CDataModel

Constructors

ILP32

LP64

Instances

Show CDataModel

Defined in Crux.SVCOMP

Methods

showsPrec :: Int -> CDataModel -> ShowS

show :: CDataModel -> String

showList :: [CDataModel] -> ShowS

Eq CDataModel

Defined in Crux.SVCOMP

Methods

(==) :: CDataModel -> CDataModel -> Bool

(/=) :: CDataModel -> CDataModel -> Bool

Ord CDataModel

Defined in Crux.SVCOMP

Methods

compare :: CDataModel -> CDataModel -> Ordering

(<) :: CDataModel -> CDataModel -> Bool

(<=) :: CDataModel -> CDataModel -> Bool

(>) :: CDataModel -> CDataModel -> Bool

(>=) :: CDataModel -> CDataModel -> Bool

max :: CDataModel -> CDataModel -> CDataModel

min :: CDataModel -> CDataModel -> CDataModel

data VerificationTask

Constructors

VerificationTask

Fields

• verificationSourceFile :: FilePath
• verificationInputFiles :: [FilePath]
• verificationProperties :: [(SVCompProperty, Maybe Bool)]
• verificationLanguage :: SVCompLanguage

Instances

Show VerificationTask

Defined in Crux.SVCOMP

Methods

showsPrec :: Int -> VerificationTask -> ShowS

show :: VerificationTask -> String

showList :: [VerificationTask] -> ShowS

Eq VerificationTask

Defined in Crux.SVCOMP

Methods

(==) :: VerificationTask -> VerificationTask -> Bool

(/=) :: VerificationTask -> VerificationTask -> Bool

Ord VerificationTask

Defined in Crux.SVCOMP

Methods

compare :: VerificationTask -> VerificationTask -> Ordering

(<) :: VerificationTask -> VerificationTask -> Bool

(<=) :: VerificationTask -> VerificationTask -> Bool

(>) :: VerificationTask -> VerificationTask -> Bool

(>=) :: VerificationTask -> VerificationTask -> Bool

max :: VerificationTask -> VerificationTask -> VerificationTask

min :: VerificationTask -> VerificationTask -> VerificationTask

checkParse :: Parser SVCompProperty

coverParse :: Parser SVCompProperty

bracketedText :: Parser Text

propParse :: Parser SVCompProperty

loadVerificationTask :: FilePath -> IO VerificationTask

compilePats :: [Text] -> [Pattern]

loadSVCOMPBenchmarks :: CruxOptions -> IO [BenchmarkSet]

loadBenchmarkSet :: FilePath -> IO BenchmarkSet

type TaskMap = Map VerificationTask [BenchmarkSet]

deduplicateTasks :: [BenchmarkSet] -> TaskMap

There is significant overlap between the various verification tasks found in different benchmark sets in the SV-COMP repository. This operation collects together all the potentially duplicated tasks found in a collection of benchmark sets and places them in a map, ensuring there is at most one reference to each one. The tasks are the keys of the map; the benchmark set(s) that referenced a given task are stored in the elements the map.