quebex

A software analysis framework built around the QBE intermediate language

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

  1;; SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>
  2;;
  3;; SPDX-License-Identifier: GPL-3.0-only
  4
  5(define-module (quebex-packages)
  6  #:use-module (guix) ; XXX: this helps 'current-source-directory'
  7  #:use-module ((guix licenses) #:prefix license:)
  8  #:use-module (gnu packages c)
  9  #:use-module (gnu packages check)
 10  #:use-module (gnu packages haskell)
 11  #:use-module (gnu packages haskell-apps)
 12  #:use-module (gnu packages haskell-check)
 13  #:use-module (gnu packages haskell-xyz)
 14  #:use-module (gnu packages maths)
 15  #:use-module (gnu packages python)
 16  #:use-module (guix build-system copy)
 17  #:use-module (guix build-system haskell)
 18  #:use-module (guix download)
 19  #:use-module (guix gexp)
 20  #:use-module (guix git-download)
 21  #:use-module (guix packages))
 22
 23;; ktest-tool python script from KLEE for inspecting .ktest file
 24;; generated by quebex-symex(1) from the quebex-cli package.
 25(define-public ktest-tool
 26  (package/inherit klee
 27    (name "ktest-tool")
 28    (build-system copy-build-system)
 29    (inputs (list python-minimal))
 30    (native-inputs '())
 31    (arguments
 32      (list
 33        #:phases
 34        #~(modify-phases %standard-phases
 35            (add-after 'unpack 'fix-shebang
 36              (lambda* (#:key inputs #:allow-other-keys)
 37                (substitute* "tools/ktest-tool/ktest-tool"
 38                  (("#!/usr/bin/env python3")
 39                   (string-append
 40                     "#!"
 41                     (search-input-file inputs "/bin/python3")))))))
 42        #:install-plan
 43        #~'(("tools/ktest-tool/ktest-tool" "bin/ktest-tool"))))
 44    (home-page "https://klee-se.org")
 45    (synopsis "Tool for KLEE's ktest test input format")))
 46
 47(define-public ghc-simple-smt
 48  (package
 49    (name "ghc-simple-smt")
 50    (version "0.9.8")
 51    (source
 52     (origin
 53       (method url-fetch)
 54       (uri (hackage-uri "simple-smt" version))
 55       (sha256
 56        (base32 "0imimkpzbd013gadkg7sc05jr70lffaij4ijzk368iw8xgvgxyf9"))))
 57    (build-system haskell-build-system)
 58    (properties '((upstream-name . "simple-smt")))
 59    (home-page "https://github.com/yav/simple-smt")
 60    (synopsis "Simple way to interact with an SMT solver process.")
 61    (description
 62     "This package provides a simple way to interact with an SMT solver process.")
 63    (license license:bsd-3)))
 64
 65;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 66
 67(define %srcdir
 68  (string-append (current-source-directory) "/../.."))
 69
 70(define-public quebex-syntax
 71  (package
 72    (name "quebex-syntax")
 73    (version "0.1.0.0")
 74    (source (local-file (string-append %srcdir "/quebex-syntax")
 75                        "git-checkout"
 76                        #:recursive? #t))
 77    (build-system haskell-build-system)
 78    (inputs (list ghc-9.2))
 79    (native-inputs
 80      (list
 81        qbe
 82        ghc-tasty
 83        ghc-tasty-hunit
 84        ghc-tasty-golden))
 85    (synopsis "Parser library for the QBE intermediate language")
 86    (description "")
 87    (home-page "https://git.8pit.net/quebex")
 88    (license (list license:expat license:bsd-2 license:gpl3))))
 89
 90(define-public quebex
 91  (package
 92    (name "quebex")
 93    (version "0.1.0.0")
 94    (source (local-file (string-append %srcdir "/quebex")
 95                        "git-checkout"
 96                        #:recursive? #t))
 97    (build-system haskell-build-system)
 98    (inputs (list ghc-9.2))
 99    (native-inputs
100      (list
101        quebex-syntax
102        ghc-tasty
103        ghc-tasty-hunit))
104    (synopsis "Analysis library for the QBE intermediate language")
105    (description "")
106    (home-page "https://git.8pit.net/quebex")
107    (license (list license:expat license:gpl3))))
108
109(define-public quebex-symex
110  (package
111    (name "quebex-symex")
112    (version "0.1.0.0")
113    (source (local-file (string-append %srcdir "/quebex-symex")
114                        "git-checkout"
115                        #:recursive? #t))
116    (build-system haskell-build-system)
117    (inputs (list ghc-9.2))
118    (propagated-inputs (list bitwuzla)) ;; TODO: Wrapper on quebex-cli?
119    (native-inputs
120      (list
121        quebex
122        quebex-syntax
123        ghc-tasty
124        ghc-tasty-hunit
125        ghc-tasty-golden
126        ghc-tasty-quickcheck
127        ghc-simple-smt))
128    (synopsis "Symbolic executor for the QBE intermediate language")
129    (description "")
130    (home-page "https://git.8pit.net/quebex")
131    (license (list license:expat license:gpl3))))
132
133(define-public quebex-cli
134  (package
135    (name "quebex-cli")
136    (version "0.1.0.0")
137    (source (local-file (string-append %srcdir "/quebex-cli")
138                        "git-checkout"
139                        #:recursive? #t))
140    (build-system haskell-build-system)
141    (inputs (list ghc-9.2))
142    (native-inputs
143      (list
144        quebex
145        quebex-syntax
146        quebex-symex
147        ghc-optparse-applicative
148        ghc-tasty-hunit))
149    (synopsis "Command line utilities for Quebex")
150    (description "")
151    (home-page "https://git.8pit.net/quebex")
152    (license (list license:gpl3))))