qute

A software analysis framework built around the QBE intermediate language

git clone https://git.8pit.net/qute.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 (qute-packages)
  6  #:use-module ((ice-9 popen) #:select (open-pipe*))
  7  #:use-module ((ice-9 rdelim) #:select (read-string))
  8  #:use-module (guix transformations) ; XXX: needed for 'simple-cc'
  9  #:use-module ((guix licenses) #:prefix license:)
 10  #:use-module ((gnu packages c) #:prefix c:)
 11  #:use-module (gnu packages check)
 12  #:use-module (gnu packages haskell)
 13  #:use-module (gnu packages haskell-apps)
 14  #:use-module (gnu packages haskell-check)
 15  #:use-module (gnu packages haskell-xyz)
 16  #:use-module (gnu packages maths)
 17  #:use-module (gnu packages python)
 18  #:use-module (guix build-system copy)
 19  #:use-module (guix build-system haskell)
 20  #:use-module (guix download)
 21  #:use-module (guix gexp)
 22  #:use-module (guix git-download)
 23  #:use-module (guix packages))
 24
 25(define (pipe-command command)
 26  (let* ((port (apply open-pipe* OPEN_READ command))
 27         (output (string-trim-right (read-string port))))
 28    (close-port port)
 29    output))
 30
 31(define %srcdir
 32  (pipe-command '("git" "rev-parse" "--show-toplevel")))
 33
 34;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 35
 36;; TODO: This can be removed once scc-0.2 has been released.
 37;; See <https://git.simple-cc.org/scc/commit/575a2d87cac49174b7f53aa6ac5f9186c2165697.html>.
 38(define-public simple-cc
 39  (let* ((revision "1")
 40         (patch (string-append %srcdir "/.guix/patches/simple-cc-void-return.patch"))
 41         (scc-pkg (package-with-extra-patches
 42                   c:simple-cc
 43                   (list patch))))
 44    (package/inherit scc-pkg
 45      (version (string-append (package-version scc-pkg) "-" revision)))))
 46
 47;; ktest-tool python script from KLEE for inspecting .ktest file
 48;; generated by qute-symex(1) from the qute-cli package.
 49(define-public ktest-tool
 50  (package/inherit klee
 51    (name "ktest-tool")
 52    (build-system copy-build-system)
 53    (inputs (list python-minimal))
 54    (native-inputs '())
 55    (arguments
 56      (list
 57        #:phases
 58        #~(modify-phases %standard-phases
 59            (add-after 'unpack 'fix-shebang
 60              (lambda* (#:key inputs #:allow-other-keys)
 61                (substitute* "tools/ktest-tool/ktest-tool"
 62                  (("#!/usr/bin/env python3")
 63                   (string-append
 64                     "#!"
 65                     (search-input-file inputs "/bin/python3")))))))
 66        #:install-plan
 67        #~'(("tools/ktest-tool/ktest-tool" "bin/ktest-tool"))))
 68    (home-page "https://klee-se.org")
 69    (synopsis "Tool for KLEE's ktest test input format")))
 70
 71(define-public ghc-simple-smt
 72  (package
 73    (name "ghc-simple-smt")
 74    (version "1.0.1")
 75    (source
 76     (origin
 77       (method url-fetch)
 78       (uri (hackage-uri "simple-smt" version))
 79       (sha256
 80        (base32 "0iw0kg4ga5g393x4j9xqgrlr6mzwm5xdjg9mjp7jc2q7igrfcx5z"))))
 81    (build-system haskell-build-system)
 82    (arguments
 83     `(#:tests? #f
 84       #:configure-flags '("lib:simple-smt")))
 85    (properties '((upstream-name . "simple-smt")))
 86    (home-page "https://github.com/yav/simple-smt")
 87    (synopsis "Simple library to interact with SMT solvers via SMT-LIB")
 88    (description
 89     "This package provides a simple library to interact with an external
 90@acronym{SMT, satisfiability modulo theories} solver (such as @code{z3})
 91via the standardized @url{https://smt-lib.org, SMT-LIB} format.")
 92    (license license:bsd-3)))
 93
 94;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 95
 96(define-public qute-syntax
 97  (package
 98    (name "qute-syntax")
 99    (version "0.1.0.0")
100    (source (local-file (string-append %srcdir "/qute-syntax")
101                        "git-checkout"
102                        #:recursive? #t))
103    (build-system haskell-build-system)
104    (inputs (list ghc-9.2))
105    (native-inputs
106      (list
107        c:qbe
108        ghc-tasty
109        ghc-tasty-hunit
110        ghc-tasty-golden))
111    (synopsis "Parser library for the QBE intermediate language")
112    (description "")
113    (home-page "https://git.8pit.net/qute")
114    (license (list license:expat license:bsd-2 license:gpl3))))
115
116(define-public qute
117  (package
118    (name "qute")
119    (version "0.1.0.0")
120    (source (local-file (string-append %srcdir "/qute")
121                        "git-checkout"
122                        #:recursive? #t))
123    (build-system haskell-build-system)
124    (inputs (list ghc-9.2))
125    (native-inputs
126      (list
127        qute-syntax
128        ghc-tasty
129        ghc-tasty-hunit))
130    (synopsis "Analysis library for the QBE intermediate language")
131    (description "")
132    (home-page "https://git.8pit.net/qute")
133    (license (list license:expat license:gpl3))))
134
135(define-public qute-symex
136  (package
137    (name "qute-symex")
138    (version "0.1.0.0")
139    (source (local-file (string-append %srcdir "/qute-symex")
140                        "git-checkout"
141                        #:recursive? #t))
142    (build-system haskell-build-system)
143    (inputs (list ghc-9.2
144                  bitwuzla)) ;needed for 'check.
145    (native-inputs
146      (list
147        qute
148        qute-syntax
149        ghc-tasty
150        ghc-tasty-hunit
151        ghc-tasty-golden
152        ghc-tasty-quickcheck
153        ghc-simple-smt))
154    (synopsis "Symbolic executor for the QBE intermediate language")
155    (description "")
156    (home-page "https://git.8pit.net/qute")
157    (license (list license:expat license:gpl3))))
158
159(define-public qute-cli
160  (package
161    (name "qute-cli")
162    (version "0.1.0.0")
163    (source (local-file (string-append %srcdir "/qute-cli")
164                        "git-checkout"
165                        #:recursive? #t))
166    (build-system haskell-build-system)
167    (inputs (list ghc-9.2))
168    (native-inputs
169      (list
170        qute
171        qute-syntax
172        qute-symex
173        ghc-optparse-applicative
174        ghc-tasty-hunit))
175    (synopsis "Command line utilities for qute")
176    (description "")
177    (home-page "https://git.8pit.net/qute")
178    (license (list license:gpl3))))