blob: dd84df2a59512987fe1de4c696196079e0856a85 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
|
;;; Packages for theorem provers
;;;
;;; SPDX-FileCopyrightText: 2025 Nguyễn Gia Phong
;;; SPDX-License-Identifier: GPL-3.0-or-later
(define-module (loftix deduction)
#:use-module (gnu packages)
#:use-module (gnu packages check)
#:use-module (gnu packages digest)
#:use-module (gnu packages maths)
#:use-module (gnu packages pkg-config)
#:use-module (guix build-system cmake)
#:use-module (guix build-system pyproject)
#:use-module (guix download)
#:use-module (guix gexp)
#:use-module (guix git-download)
#:use-module ((guix licenses) #:prefix license:)
#:use-module (guix packages))
(define-public z3-for-fuzzolic
(let* ((base z3)
(base-version "4.14.1")
(base-tag (string-append "z3-" base-version))
(revision "fuzzolic")
(commit "268d10d0d99083a18cde2d615e0f9de82d7b201d")
(upstream "https://github.com/Z3Prover/z3"))
(hidden-package
(package
(inherit base)
(name "z3-for-fuzzolic")
(version (git-version base-version revision commit))
(source
(origin
(inherit (package-source base))
(uri (git-reference (url upstream)
(commit base-tag)))
(file-name (git-file-name name version))
(sha256
(base32 "1gdknrqnnigfh1h833ks3vbrp4j74mfg6188c0k4xbl5zv6h6fx5"))
(patches
(list
(origin
(method url-fetch)
(uri (string-append upstream "/compare/" base-tag
".." commit ".diff"))
(sha256
(base32 "07fga2jn5830fz9snwbzz2mpm2qqfjchsb969rqs7pf5py0h93fp"))
(file-name (string-append name ".patch")))))))
(home-page "https://github.com/season-lab/z3")
(synopsis "Z3 for FUZZOLIC")))))
(define-public fuzzy-sat
(let ((commit "99094f664abcc7cb8ff7d04eb894616b89a15efc"))
(package
(name "fuzzy-sat")
(version (git-version "0.1" "master" commit))
(home-page "https://github.com/season-lab/fuzzy-sat")
(source
(origin
(method git-fetch)
(uri (git-reference (url home-page)
(commit commit)))
(file-name (git-file-name name version))
(sha256
(base32 "1wq2a5j73aigw64bhf4s2qgkda114vfpmwiy353m0f54f5fg6sh3"))
(patches (search-patches "patches/fuzzy-sat-unbundle.patch"
"patches/fuzzy-sat-install.patch"))))
(build-system cmake-build-system)
(arguments
'(#:phases (modify-phases %standard-phases
(replace 'check
(lambda* (#:key source tests? #:allow-other-keys)
(when tests?
(setenv "FUZZY_BIN" "tools/fuzzy-solver")
(invoke "pytest" "-p" "no:cacheprovider" "-v"
(string-append source "/tests/run.py"))))))))
(native-inputs (list pkg-config python-pytest))
(inputs (list xxhash z3-for-fuzzolic))
(synopsis "Approximate solver for concolic execution")
(description "Fuzzy SAT is an approximate solver that borrows ideas
from the fuzzing domain. It is tailored to the symbolic expressions
generated by concolic engines and can replace classic SMT solvers
in this context. By analyzing the expressions contained in symbolic queries,
Fuzzy SAT performs informed mutations to possibly generate
new valuable inputs.")
(license license:gpl2+))))
|