qute

A software analysis framework built around the QBE intermediate language

git clone https://git.8pit.net/qute.git

  1cabal-version:      3.4
  2name:               qute
  3version:            0.1.0
  4synopsis:           A software analysis framework built around the QBE intermediate language.
  5description:
  6  This library provides formal semantics for the [QBE intermediate language](https://c9x.me/compile/)
  7  by providing [modular monadic semantics](https://doi.org/10.1007/3-540-61055-3_39) implemented using
  8  an [abstract monad](https://doi.org/10.1145/3607833). The package refers to this abstract monad as
  9  the 'Language.QBE.Simulator.State.Simulator' monad. It provides several primitives that are used by
 10  the "Language.QBE.Simulator" to /abstractly/ describe the semantics of QBE instructions. The
 11  'Language.QBE.Simulator.State.Simulator' can then be instantiated with /concrete/ semantics. For
 12  example, the "Language.QBE.Simulator.Default.State" module provides an instantiation using a
 13  'Control.Monad.State' monad. This instantiation, and the 'Language.QBE.Simulator.State.Simulator'
 14  itself, are parameterized over the representation of QBE instruction operand values.
 15
 16  To abstractly describe operations on values passed to QBE instructions, this library additionally
 17  provides an expression language abstraction in the "Language.QBE.Simulator.Expression" module.
 18  Further, an implementation of this expression language based on fixed-width integer values is
 19  available in the "Language.QBE.Simulator.Default.Expression" module.
 20
 21  A separate [qute-symex](https://hackage.haskell.org/package/qute-symex) package provides an
 22  implementation of the expression abstraction and the 'Language.QBE.Simulator.State.Simulator'
 23  monad for formal reasoning about a software under test using
 24  [symbolic execution](https://en.wikipedia.org/wiki/Symbolic_execution).
 25  Similar dynamic software testing techniques can be implemented using this library. Additionally,
 26  there is some preliminary support for static analysis as well through the
 27  "Language.QBE.Analysis.CFG" module.
 28
 29  More information on the underlying idea and vision behind Qute is available in a
 30  [separate paper](https://www.ibr.cs.tu-bs.de/vss/Publications/2026/tempel_26_qute.pdf).
 31license:            GPL-3.0-only AND MIT AND BSD-3-Clause
 32-- license-file:
 33author:             Sören Tempel
 34maintainer:         soeren+hackage@soeren-tempel.net
 35-- copyright:
 36category:           Language
 37build-type:         Simple
 38homepage:           https://git.8pit.net/qute
 39bug-reports:        https://github.com/nmeum/qute/issues
 40extra-source-files: test/testdata/*.qbe
 41
 42source-repository head
 43    type: git
 44    location: https://git.8pit.net/qute.git
 45
 46common warnings
 47    -- -Wall-missed-specializations can be useful too
 48    ghc-options: -Wall
 49
 50common opts
 51    ghc-options: -fspecialise-aggressively
 52
 53library
 54    import:           warnings, opts
 55    -- other-modules:
 56    hs-source-dirs:   src
 57    default-language: GHC2021
 58
 59    build-depends:
 60      base,
 61      array,
 62      bytestring,
 63      deepseq,
 64      template-haskell,
 65      qute-syntax,
 66      containers,
 67      exceptions,
 68      parsec,
 69      mtl
 70
 71    other-modules:
 72      Language.QBE.Simulator.Default.Generator
 73
 74    exposed-modules:
 75      Data.Archive,
 76      Language.QBE.Analysis.CFG,
 77      Language.QBE.Analysis.CDG,
 78      Language.QBE.Analysis.Graph,
 79      Language.QBE.Linker,
 80      Language.QBE.Simulator,
 81      Language.QBE.Simulator.ABI.C,
 82      Language.QBE.Simulator.ABI.Errno,
 83      Language.QBE.Simulator.ABI.POSIX,
 84      Language.QBE.Simulator.State,
 85      Language.QBE.Simulator.Error,
 86      Language.QBE.Simulator.Memory,
 87      Language.QBE.Simulator.Expression,
 88      Language.QBE.Simulator.Default.State,
 89      Language.QBE.Simulator.Default.Funcs,
 90      Language.QBE.Simulator.Default.Expression
 91
 92benchmark qute
 93    import:           warnings, opts
 94    default-language: GHC2021
 95    type:             exitcode-stdio-1.0
 96    hs-source-dirs:   bench
 97    main-is:          Main.hs
 98
 99    build-depends:
100      base,
101      criterion ^>= 1.6.4.0,
102      qute,
103      qute-syntax
104
105test-suite qute-test
106    import:           warnings
107    default-language: GHC2021
108    type:             exitcode-stdio-1.0
109    hs-source-dirs:   test
110    main-is:          Main.hs
111    -- Prevent GHGC from optimizing float2Double calls.
112    ghc-options:      -O0
113
114    other-modules:
115      Archive,
116      Linker,
117      Analysis,
118      Simulator,
119      Expression,
120      Memory,
121      State,
122      Util
123
124    build-depends:
125        base,
126        array,
127        parsec,
128        filepath,
129        qute,
130        qute-syntax,
131        containers,
132        exceptions,
133        mtl,
134        tasty        >=1.4.3,
135        tasty-hunit  >=0.10