qute - qute-symex.cabal

  1cabal-version:      3.4
  2name:               qute-symex
  3version:            0.1.0
  4synopsis:           A symbolic execution engine for the QBE intermediate language.
  5description:
  6  Based on the formal semantics of the [Qute](https://hackage.haskell.org/package/qute) package,
  7  this library provides a [symbolic execution](https://en.wikipedia.org/wiki/Symbolic_execution)
  8  engine for the QBE intermediate language. Thereby, it enables formal reasoning about a software
  9  under test using [SMT solvers](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories).
 10
 11  The underlying vision behind Qute's symbolic execution engine is further described in a
 12  [separate paper](https://www.ibr.cs.tu-bs.de/vss/Publications/2026/tempel_26_qute.pdf).
 13license:            GPL-3.0-only AND MIT
 14-- license-file:
 15author:             Sören Tempel
 16maintainer:         soeren+hackage@soeren-tempel.net
 17-- copyright:
 18category:           Language
 19build-type:         Simple
 20homepage:           https://git.8pit.net/qute
 21bug-reports:        https://github.com/nmeum/qute/issues
 22
 23source-repository head
 24    type: git
 25    location: https://git.8pit.net/qute.git
 26
 27common warnings
 28    -- -Wall-missed-specializations can be useful too
 29    ghc-options: -Wall
 30
 31common opts
 32    ghc-options: -fspecialise-aggressively
 33
 34library
 35    import:           warnings, opts
 36    -- other-modules:
 37    hs-source-dirs:   src
 38    default-language: GHC2021
 39
 40    build-depends:
 41      base,
 42      deepseq,
 43      mtl,
 44      directory,
 45      containers,
 46      exceptions,
 47      random,
 48      qute,
 49      qute-syntax,
 50      simple-smt
 51
 52    exposed-modules:
 53      SimpleBV,
 54      Language.QBE.Backend,
 55      Language.QBE.Backend.Model,
 56      Language.QBE.Backend.Store,
 57      Language.QBE.Backend.ExecTree,
 58      Language.QBE.Backend.DFS,
 59      Language.QBE.Backend.Tracer,
 60      Language.QBE.Simulator.Explorer,
 61      Language.QBE.Simulator.Symbolic.Expression,
 62      Language.QBE.Simulator.Concolic.State,
 63      Language.QBE.Simulator.Concolic.Expression
 64
 65benchmark qute-symex
 66    import:           warnings, opts
 67    default-language: GHC2021
 68    type:             exitcode-stdio-1.0
 69    hs-source-dirs:   bench
 70    main-is:          Main.hs
 71
 72    other-modules:
 73      SMTUnwind,
 74      SMT,
 75      Exec
 76
 77    build-depends:
 78      base,
 79      criterion ^>= 1.6.4.0,
 80      mtl,
 81      simple-smt,
 82      process,
 83      filepath,
 84      qute,
 85      qute-syntax,
 86      qute-symex
 87
 88test-suite qute-symex-test
 89    import:           warnings
 90    default-language: GHC2021
 91    type:             exitcode-stdio-1.0
 92    hs-source-dirs:   test
 93    main-is:          Main.hs
 94
 95    other-modules:
 96      Util,
 97      Golden,
 98      Backend,
 99      Explorer,
100      Symbolic,
101      Concolic,
102      BV
103
104    build-depends:
105        base,
106        filepath,
107        containers,
108        random,
109        qute,
110        qute-syntax,
111        qute-symex,
112        simple-smt,
113        tasty            >=1.4.3,
114        tasty-hunit      >=0.10,
115        tasty-golden     >=2.3.5,
116        tasty-quickcheck >=0.10.2