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 utils)
 23  #:use-module (guix git-download)
 24  #:use-module (guix packages))
 25
 26(define (pipe-command command)
 27  (let* ((port (apply open-pipe* OPEN_READ command))
 28         (output (string-trim-right (read-string port))))
 29    (close-port port)
 30    output))
 31
 32(define %srcdir
 33  (pipe-command '("git" "rev-parse" "--show-toplevel")))
 34
 35;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 36
 37(define-public simple-cc
 38  (let ((commit "dc2467847308d6c9e1e19d139938ff5c4aba1343")
 39        (revision "3"))
 40    (package/inherit c:simple-cc
 41      (name "simple-cc")
 42      (version (git-version (package-version c:simple-cc) revision commit))
 43      (source
 44        (origin
 45          (method git-fetch)
 46          (uri (git-reference
 47                 (url "https://git.8pit.net/scc.git")
 48                 (commit commit)))
 49          (file-name (git-file-name name version))
 50          (sha256
 51            (base32 "1ls3csagx321fxbqiay9ygbjrras3bq5f7cfdw6h64x14s4npfmq"))))
 52      (arguments
 53        (substitute-keyword-arguments (package-arguments c:simple-cc)
 54          ((#:tests? _ #f) #f) ;; TODO: Figure out why tests fail on Git HEAD.
 55          ((#:phases phases #~%standard-phases)
 56           #~(modify-phases #$phases
 57               ;; gcc-scc.sh has been removed in Git HEAD, create an empty file to
 58               ;; allow using the existing 'fix-paths phase without it erroring.
 59               (add-before 'fix-paths 'touch-dummy
 60                 (lambda _
 61                   (call-with-output-file "src/libc/gcc-scc.sh" (const #t)))))))))))
 62
 63;; ktest-tool python script from KLEE for inspecting .ktest file
 64;; generated by qute-symex(1) from the qute-cli package.
 65(define-public ktest-tool
 66  (package/inherit klee
 67    (name "ktest-tool")
 68    (build-system copy-build-system)
 69    (inputs (list python-minimal))
 70    (native-inputs '())
 71    (arguments
 72      (list
 73        #:phases
 74        #~(modify-phases %standard-phases
 75            (add-after 'unpack 'fix-shebang
 76              (lambda* (#:key inputs #:allow-other-keys)
 77                (substitute* "tools/ktest-tool/ktest-tool"
 78                  (("#!/usr/bin/env python3")
 79                   (string-append
 80                     "#!"
 81                     (search-input-file inputs "/bin/python3")))))))
 82        #:install-plan
 83        #~'(("tools/ktest-tool/ktest-tool" "bin/ktest-tool"))))
 84    (home-page "https://klee-se.org")
 85    (synopsis "Tool for KLEE's ktest test input format")))
 86
 87;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 88
 89(define-public qute-syntax
 90  (package
 91    (name "qute-syntax")
 92    (version "0.1.0.0")
 93    (source (local-file (string-append %srcdir "/qute-syntax")
 94                        "git-checkout"
 95                        #:recursive? #t))
 96    (build-system haskell-build-system)
 97    (native-inputs
 98      (list
 99        c:qbe
100        ghc-tasty
101        ghc-tasty-hunit
102        ghc-tasty-golden))
103    (synopsis "Parser library for the QBE intermediate language")
104    (description "")
105    (home-page "https://git.8pit.net/qute")
106    (license (list license:expat license:bsd-2 license:gpl3))))
107
108(define-public qute
109  (package
110    (name "qute")
111    (version "0.1.0.0")
112    (source (local-file (string-append %srcdir "/qute")
113                        "git-checkout"
114                        #:recursive? #t))
115    (build-system haskell-build-system)
116    (native-inputs
117      (list
118        qute-syntax
119        ghc-tasty
120        ghc-tasty-hunit))
121    (synopsis "Analysis library for the QBE intermediate language")
122    (description "")
123    (home-page "https://git.8pit.net/qute")
124    (license (list license:expat license:gpl3))))
125
126(define-public qute-symex
127  (package
128    (name "qute-symex")
129    (version "0.1.0.0")
130    (source (local-file (string-append %srcdir "/qute-symex")
131                        "git-checkout"
132                        #:recursive? #t))
133    (build-system haskell-build-system)
134    (inputs (list bitwuzla)) ;needed for 'check.
135    (native-inputs
136      (list
137        qute
138        qute-syntax
139        ghc-tasty
140        ghc-tasty-hunit
141        ghc-tasty-golden
142        ghc-tasty-quickcheck
143        ghc-simple-smt))
144    (synopsis "Symbolic executor for the QBE intermediate language")
145    (description "")
146    (home-page "https://git.8pit.net/qute")
147    (license (list license:expat license:gpl3))))
148
149(define-public qute-cli
150  (package
151    (name "qute-cli")
152    (version "0.1.0.0")
153    (source (local-file (string-append %srcdir "/qute-cli")
154                        "git-checkout"
155                        #:recursive? #t))
156    (build-system haskell-build-system)
157    (native-inputs
158      (list
159        qute
160        qute-syntax
161        qute-symex
162        ghc-optparse-applicative
163        ghc-tasty-hunit))
164    (synopsis "Command line utilities for qute")
165    (description "")
166    (home-page "https://git.8pit.net/qute")
167    (license (list license:gpl3))))