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
 22extra-source-files:
 23  test/testdata/*.qbe,
 24  test/golden/*.qbe
 25
 26source-repository head
 27    type: git
 28    location: https://git.8pit.net/qute.git
 29
 30common warnings
 31    -- -Wall-missed-specializations can be useful too
 32    ghc-options: -Wall
 33
 34common opts
 35    -- -threaded required by simple-smt, see <https://github.com/yav/simple-smt/issues/28>.
 36    ghc-options: -fspecialise-aggressively -threaded
 37
 38library
 39    import:           warnings, opts
 40    -- other-modules:
 41    hs-source-dirs:   src
 42    default-language: GHC2021
 43
 44    build-depends:
 45      base,
 46      deepseq,
 47      mtl,
 48      directory,
 49      containers,
 50      exceptions,
 51      random,
 52      qute,
 53      qute-syntax,
 54      simple-smt
 55
 56    exposed-modules:
 57      SimpleBV,
 58      Language.QBE.Backend,
 59      Language.QBE.Backend.Model,
 60      Language.QBE.Backend.Store,
 61      Language.QBE.Backend.ExecTree,
 62      Language.QBE.Backend.DFS,
 63      Language.QBE.Backend.Tracer,
 64      Language.QBE.Simulator.Explorer,
 65      Language.QBE.Simulator.Symbolic.Expression,
 66      Language.QBE.Simulator.Concolic.State,
 67      Language.QBE.Simulator.Concolic.Expression
 68
 69benchmark qute-symex
 70    import:           warnings, opts
 71    default-language: GHC2021
 72    type:             exitcode-stdio-1.0
 73    hs-source-dirs:   bench
 74    main-is:          Main.hs
 75
 76    other-modules:
 77      SMTUnwind,
 78      SMT,
 79      Exec
 80
 81    build-depends:
 82      base,
 83      criterion ^>= 1.6.4.0,
 84      mtl,
 85      simple-smt >= 1.0.1,
 86      process,
 87      filepath,
 88      qute,
 89      qute-syntax,
 90      qute-symex
 91
 92test-suite qute-symex-test
 93    import:           warnings, opts
 94    default-language: GHC2021
 95    type:             exitcode-stdio-1.0
 96    hs-source-dirs:   test
 97    main-is:          Main.hs
 98
 99    other-modules:
100      Util,
101      Golden,
102      Backend,
103      Explorer,
104      Symbolic,
105      Concolic,
106      BV
107
108    build-depends:
109        base,
110        filepath,
111        containers,
112        random,
113        qute,
114        qute-syntax,
115        qute-symex,
116        simple-smt,
117        tasty            >=1.4.3,
118        tasty-hunit      >=0.10,
119        tasty-golden     >=2.3.5,
120        tasty-quickcheck >=0.10.2