[PATCH] Add BINSEC.

  • Done
  • quality assurance status badge
Details
2 participants
  • Julien Lepiller
  • soeren
Owner
unassigned
Submitted by
soeren
Severity
normal
S
S
soeren wrote on 3 Feb 16:03 +0100
(address . guix-patches@gnu.org)
cover.1706972151.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

This patchset adds a package for BINSEC https://binsec.github.io/.
BINSEC is a popular tool for binary program analysis using symbolic
execution. Symbolic execution is a technique for automated software
testing and an active area of computer science research. This package
for BINSEC is part of and ongoing effort to package symbolic execution
tools in Guix, thereby easing the creation of computational environments
for reproducible research in the symbolic execution domain.

BINSEC requires 9 new OCaml packages, most of them originate in Dune.

Sören Tempel (10):
gnu: Add ocaml-iso8601
gnu: Add ocaml-toml.
gnu: Add ocaml-pp.
gnu: Add ocaml-grain-dypgen.
gnu: Add ocaml-ordering.
gnu: Add ocaml-dyn.
gnu: Add ocaml-stdune.
gnu: Add ocaml-dune-private-libs.
gnu: Add ocaml-dune-site.
gnu: Add binsec.

gnu/packages/ocaml.scm | 213 +++++++++++++++++++++++++++++++++++++++++
1 file changed, 213 insertions(+)


base-commit: 179bb57d2532ee6b81791e078b0f782cbf88cb84
S
S
soeren wrote on 3 Feb 16:11 +0100
[PATCH] gnu: Add ocaml-iso8601
(address . 68908@debbugs.gnu.org)
78a03f74beedf71f343dcd73baf4a31a4100ab14.1706972151.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

* gnu/packages/ocaml.scm (ocaml-iso8601): New variable.

Signed-off-by: Sören Tempel <soeren@soeren-tempel.net>
---
gnu/packages/ocaml.scm | 20 ++++++++++++++++++++
1 file changed, 20 insertions(+)

Toggle diff (31 lines)
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index e166cdec2f..e9ada32bde 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -2058,6 +2058,26 @@ (define-public ocaml5.0-result
#:ocaml ,ocaml-5.0
#:findlib ,ocaml5.0-findlib))))
+(define-public ocaml-iso8601
+ (package
+ (name "ocaml-iso8601")
+ (version "0.2.6")
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/ocaml-community/ISO8601.ml")
+ (commit version)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "0nzadswspizi7s6sf67icn2xgc3w150x8vdg5nk1mjrm2s98n6d3"))))
+ (build-system dune-build-system)
+ (propagated-inputs (list ocaml-stdlib-shims ocaml-core-unix ocaml-ounit))
+ (synopsis "Parser and printer for date-times in ISO8601")
+ (description "ISO 8601 and RFC 3339 date parsing for OCaml.")
+ (home-page "https://github.com/ocaml-community/ISO8601.ml")
+ (license license:expat)))
+
(define-public ocaml-topkg
(package
(name "ocaml-topkg")
S
S
soeren wrote on 3 Feb 16:11 +0100
[PATCH] gnu: Add ocaml-pp.
(address . 68908@debbugs.gnu.org)
34e73be66b832c186ff8a3cc0be546950da67da8.1706972151.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

* gnu/packages/ocaml.scm (ocaml-pp): New variable.

Signed-off-by: Sören Tempel <soeren@soeren-tempel.net>
---
gnu/packages/ocaml.scm | 23 +++++++++++++++++++++++
1 file changed, 23 insertions(+)

Toggle diff (34 lines)
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index fcb45793aa..ac44b084d5 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -2101,6 +2101,29 @@ (define-public ocaml-toml
(home-page "https://github.com/ocaml-toml/To.ml")
(license license:expat)))
+(define-public ocaml-pp
+ (package
+ (name "ocaml-pp")
+ (version "1.2.0")
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/ocaml-dune/pp")
+ (commit version)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "0ylwb8lbjzj1prnal3c5p404dvh7bv4s19cvgrplnd7s46lvnj50"))))
+ (build-system dune-build-system)
+ (native-inputs (list ocaml-ppx-expect))
+ (home-page "https://github.com/ocaml-dune/pp")
+ (synopsis "Pretty-printing library")
+ (description
+ "Pretty-printing library allowing custom formatting of defined
+types and values. The API is intended as an alternative to the
+@code{Format} module of the OCaml standard library.")
+ (license license:expat)))
+
(define-public ocaml-topkg
(package
(name "ocaml-topkg")
S
S
soeren wrote on 3 Feb 16:11 +0100
[PATCH] gnu: Add ocaml-toml.
(address . 68908@debbugs.gnu.org)
2d9d01dbdc500dbe07618c172645e99e3d2a62fa.1706972151.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

* gnu/packages/ocaml.scm (ocaml-toml): New variable.

Signed-off-by: Sören Tempel <soeren@soeren-tempel.net>
---
gnu/packages/ocaml.scm | 23 +++++++++++++++++++++++
1 file changed, 23 insertions(+)

Toggle diff (34 lines)
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index e9ada32bde..fcb45793aa 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -2078,6 +2078,29 @@ (define-public ocaml-iso8601
(home-page "https://github.com/ocaml-community/ISO8601.ml")
(license license:expat)))
+(define-public ocaml-toml
+ (package
+ (name "ocaml-toml")
+ (version "7.1.0")
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/ocaml-toml/To.ml")
+ (commit version)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "0z2873mj3i6h9cg8zlkipcjab8jympa4c4avhk4l04755qzphkds"))))
+ (build-system dune-build-system)
+ (propagated-inputs (list ocaml-base ocaml-mdx ocaml-menhir ocaml-iso8601))
+ (synopsis "TOML library for OCaml")
+ (description
+ "This package provides an OCaml library for interacting with files
+in the @acronym{TOML, Tom's Obvious Minimal Language} format. Specifically,
+it provides parser, a serializer, and a pretty printer.")
+ (home-page "https://github.com/ocaml-toml/To.ml")
+ (license license:expat)))
+
(define-public ocaml-topkg
(package
(name "ocaml-topkg")
S
S
soeren wrote on 3 Feb 16:12 +0100
[PATCH] gnu: Add ocaml-grain-dypgen.
(address . 68908@debbugs.gnu.org)
88e924b717a307c24434e610f1b1c538fb8f9879.1706972151.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

* gnu/packages/ocaml.scm (ocaml-grain-dypgen): New variable.

Signed-off-by: Sören Tempel <soeren@soeren-tempel.net>
---
gnu/packages/ocaml.scm | 35 +++++++++++++++++++++++++++++++++++
1 file changed, 35 insertions(+)

Toggle diff (46 lines)
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index ac44b084d5..b77acdf0d4 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -2124,6 +2124,41 @@ (define-public ocaml-pp
@code{Format} module of the OCaml standard library.")
(license license:expat)))
+(define-public ocaml-grain-dypgen
+ (package
+ (name "ocaml-grain-dypgen")
+ (version "0.2")
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/grain-lang/dypgen")
+ (commit version)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "1jyxkvi75nchk5kmhqixmjy70z55gmlqa83pxn0hsv2qxvyqxavw"))))
+ (build-system ocaml-build-system)
+ (arguments
+ (list
+ ;; Upstream does not have a test suite.
+ #:tests? #f
+ #:make-flags #~(let ((out #$output))
+ (list (string-append "OCAMLLIBDIR=" out
+ "/lib/ocaml/site-lib")
+ (string-append "BINDIR=" out "/bin")
+ (string-append "MANDIR=" out "/share/man")))
+ #:phases #~(modify-phases %standard-phases
+ (delete 'configure))))
+ (native-inputs (list ocaml-findlib))
+ (properties `((upstream-name . "grain_dypgen")))
+ (home-page "https://github.com/grain-lang/dypgen")
+ (synopsis "Self-extensible parsers and lexers for OCaml")
+ (description
+ "@acronym{GLR, generalized LR} parser generator for OCaml, it is
+able to generate self-extensible parsers (also called adaptive parsers)
+as well as extensible lexers for the parsers it produces.")
+ (license license:cecill-b)))
+
(define-public ocaml-topkg
(package
(name "ocaml-topkg")
S
S
soeren wrote on 3 Feb 16:12 +0100
[PATCH] gnu: Add ocaml-ordering.
(address . 68908@debbugs.gnu.org)
cda0b535ae0e7e85c16d93c5bfba66193987106f.1706972151.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

* gnu/packages/ocaml.scm (ocaml-ordering): New variable.

Signed-off-by: Sören Tempel <soeren@soeren-tempel.net>
---
gnu/packages/ocaml.scm | 14 ++++++++++++++
1 file changed, 14 insertions(+)

Toggle diff (25 lines)
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index b77acdf0d4..1d9fd31d49 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -8305,6 +8305,20 @@ (define-public ocaml-fix
that involve memoization and recursion.")
(license license:lgpl2.0)))
+(define-public ocaml-ordering
+ (package
+ (inherit dune)
+ (name "ocaml-ordering")
+ (build-system dune-build-system)
+ (arguments
+ '(#:package "ordering"
+ ;; No separate test suite from dune.
+ #:tests? #f))
+ (propagated-inputs (list ocaml-odoc))
+ (synopsis "Element ordering library provided by Dune")
+ (description "Element ordering library provided by Dune.")
+ (license license:expat)))
+
(define-public ocaml-dune-build-info
(package
(inherit dune)
S
S
soeren wrote on 3 Feb 16:12 +0100
[PATCH] gnu: Add ocaml-dyn.
(address . 68908@debbugs.gnu.org)
bc496d140b7080708a474d0db9d120eb6bac4b0c.1706972151.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

* gnu/packages/ocaml.scm (ocaml-dyn): New variable.

Signed-off-by: Sören Tempel <soeren@soeren-tempel.net>
---
gnu/packages/ocaml.scm | 14 ++++++++++++++
1 file changed, 14 insertions(+)

Toggle diff (25 lines)
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 1d9fd31d49..93b38b1442 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -8319,6 +8319,20 @@ (define-public ocaml-ordering
(description "Element ordering library provided by Dune.")
(license license:expat)))
+(define-public ocaml-dyn
+ (package
+ (inherit dune)
+ (name "ocaml-dyn")
+ (build-system dune-build-system)
+ (arguments
+ '(#:package "dyn"
+ ;; No separate test suite from dune.
+ #:tests? #f))
+ (propagated-inputs (list ocaml-ordering ocaml-pp ocaml-odoc))
+ (synopsis "Dynamic type")
+ (description "Dynamic type")
+ (license license:expat)))
+
(define-public ocaml-dune-build-info
(package
(inherit dune)
S
S
soeren wrote on 3 Feb 16:12 +0100
[PATCH] gnu: Add ocaml-stdune.
(address . 68908@debbugs.gnu.org)
ade1d9a963c3f0d89136c6639cc48fc774d0e0ed.1706972151.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

* gnu/packages/ocaml.scm (ocaml-stdune): New variable.

Signed-off-by: Sören Tempel <soeren@soeren-tempel.net>
---
gnu/packages/ocaml.scm | 17 +++++++++++++++++
1 file changed, 17 insertions(+)

Toggle diff (28 lines)
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 93b38b1442..4d61610335 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -8333,6 +8333,23 @@ (define-public ocaml-dyn
(description "Dynamic type")
(license license:expat)))
+(define-public ocaml-stdune
+ (package
+ (inherit dune)
+ (name "ocaml-stdune")
+ (build-system dune-build-system)
+ (arguments
+ '(#:package "stdune"
+ ;; No separate test suite from dune.
+ #:tests? #f))
+ (propagated-inputs (list ocaml-dyn ocaml-ordering ocaml-pp ocaml-csexp
+ ocaml-odoc))
+ (synopsis "Dune's unstable standard library")
+ (description
+ "This library ships the Dune standard library, the library does not
+provide any backwards compatibility or stability guarantees.")
+ (license license:expat)))
+
(define-public ocaml-dune-build-info
(package
(inherit dune)
S
S
soeren wrote on 3 Feb 16:12 +0100
[PATCH] gnu: Add ocaml-dune-private-libs.
(address . 68908@debbugs.gnu.org)
22782da727d7d93f129d6247ab19e5bd84b2976c.1706972151.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

* gnu/packages/ocaml.scm (ocaml-dune-private-libs): New variable.

Signed-off-by: Sören Tempel <soeren@soeren-tempel.net>
---
gnu/packages/ocaml.scm | 19 +++++++++++++++++++
1 file changed, 19 insertions(+)

Toggle diff (30 lines)
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 4d61610335..f2d18d0205 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -8350,6 +8350,25 @@ (define-public ocaml-stdune
provide any backwards compatibility or stability guarantees.")
(license license:expat)))
+(define-public ocaml-dune-private-libs
+ (package
+ (inherit dune)
+ (name "ocaml-dune-private-libs")
+ (build-system dune-build-system)
+ (arguments
+ '(#:package "dune-private-libs"
+ ;; No separate test suite from dune.
+ #:tests? #f))
+ (propagated-inputs (list ocaml-csexp ocaml-pp ocaml-dyn ocaml-stdune
+ ocaml-odoc))
+ (synopsis "Private libraries of Dune")
+ (description
+ "This OCaml library provides several private APIs shared between
+various Dune-internal packages. It is not intended for public use by
+the authors and does therefore not provide any stability guarantees.
+Nonetheless, many OCaml packages depend on this library.")
+ (license license:expat)))
+
(define-public ocaml-dune-build-info
(package
(inherit dune)
S
S
soeren wrote on 3 Feb 16:12 +0100
[PATCH] gnu: Add ocaml-dune-site.
(address . 68908@debbugs.gnu.org)
19603445c6e4d01e6622116d9c9330bbda5d3e7b.1706972151.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

* gnu/packages/ocaml.scm (ocaml-dune-site): New variable.

Signed-off-by: Sören Tempel <soeren@soeren-tempel.net>
---
gnu/packages/ocaml.scm | 15 +++++++++++++++
1 file changed, 15 insertions(+)

Toggle diff (26 lines)
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index f2d18d0205..8701b4cb23 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -8369,6 +8369,21 @@ (define-public ocaml-dune-private-libs
Nonetheless, many OCaml packages depend on this library.")
(license license:expat)))
+(define-public ocaml-dune-site
+ (package
+ (inherit dune)
+ (name "ocaml-dune-site")
+ (build-system dune-build-system)
+ (arguments
+ '(#:package "dune-site"
+ ;; No separate test suite from dune.
+ #:tests? #f))
+ (propagated-inputs (list ocaml-dune-private-libs ocaml-odoc))
+ (synopsis "Embed locations information inside executable and libraries")
+ (description "This OCaml library allows embedding information inside
+executable binaries and libraries, it is provided by Dune.")
+ (license license:expat)))
+
(define-public ocaml-dune-build-info
(package
(inherit dune)
S
S
soeren wrote on 3 Feb 16:12 +0100
[PATCH] gnu: Add binsec.
(address . 68908@debbugs.gnu.org)
d9700078afdf2237d3a5070ab6223dc8e8d9329d.1706972151.git.soeren@soeren-tempel.net
From: Sören Tempel <soeren@soeren-tempel.net>

* gnu/packages/ocaml.scm (binsec): New variable.

Signed-off-by: Sören Tempel <soeren@soeren-tempel.net>
---
gnu/packages/ocaml.scm | 33 +++++++++++++++++++++++++++++++++
1 file changed, 33 insertions(+)

Toggle diff (44 lines)
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 8701b4cb23..f76d9e089d 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -1345,6 +1345,39 @@ (define-public lablgtk
libpanel, librsvg and quartz.")
(license license:lgpl2.1)))
+(define-public binsec
+ (package
+ (name "binsec")
+ (version "0.8.1")
+ (source
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/binsec/binsec")
+ (commit version)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "0j6lwj20jaq0702v2fqvsrax1400zqbvz5q2cmjqhvrjzcfcl0kr"))))
+ (build-system dune-build-system)
+ (native-inputs (list gmp ocaml-qcheck ocaml-ounit2))
+ (propagated-inputs (list ocaml-base
+ ocaml-dune-site
+ ocaml-menhir
+ ocaml-graph
+ ocaml-zarith
+ ocaml-grain-dypgen
+ ocaml-toml))
+ (synopsis "Binary-level analysis platform")
+ (description
+ "BINSEC is a binary analysis platform which implements analysis
+techniques such as symbolic execution. The goal of BINSEC is to improve
+software security at the binary level through binary analysis. BINSEC
+is a research tool which relies on prior work in binary code analysis
+at the intersection of formal methods, program analysis security and
+software engineering.")
+ (home-page "https://binsec.github.io/")
+ (license license:lgpl2.1)))
+
(define-public unison
(package
(name "unison")
J
J
Julien Lepiller wrote on 3 Feb 22:52 +0100
Re: [bug#68908] [PATCH] Add BINSEC.
(address . soeren@soeren-tempel.net)
20240203225208.72a14eae@tachikoma.lepiller.eu
Le Sat, 3 Feb 2024 16:03:19 +0100,
soeren@soeren-tempel.net a écrit :

Toggle quote (13 lines)
> From: Sören Tempel <soeren@soeren-tempel.net>
>
> This patchset adds a package for BINSEC <https://binsec.github.io/>.
> BINSEC is a popular tool for binary program analysis using symbolic
> execution. Symbolic execution is a technique for automated software
> testing and an active area of computer science research. This package
> for BINSEC is part of and ongoing effort to package symbolic execution
> tools in Guix, thereby easing the creation of computational
> environments for reproducible research in the symbolic execution
> domain.
>
> BINSEC requires 9 new OCaml packages, most of them originate in Dune.

Thanks for the patch series! I have another series I need to push first
(which I should be able to do after FOSDEM):
https://issues.guix.gnu.org/64249.I recognise the dune packages from
this other patch series here. We'll drop them, sorry you had to do this
work for nothing.

I can't take a look right now, but I'm super excited to get binsec in
Guix!

Toggle quote (20 lines)
> Sören Tempel (10):
> gnu: Add ocaml-iso8601
> gnu: Add ocaml-toml.
> gnu: Add ocaml-pp.
> gnu: Add ocaml-grain-dypgen.
> gnu: Add ocaml-ordering.
> gnu: Add ocaml-dyn.
> gnu: Add ocaml-stdune.
> gnu: Add ocaml-dune-private-libs.
> gnu: Add ocaml-dune-site.
> gnu: Add binsec.
>
> gnu/packages/ocaml.scm | 213
> +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 213
> insertions(+)
>
>
> base-commit: 179bb57d2532ee6b81791e078b0f782cbf88cb84
>
>
J
J
Julien Lepiller wrote on 11 Feb 17:32 +0100
(address . soeren@soeren-tempel.net)
20240211173211.25210c9a@lepiller.eu
Applied to master as 8b679328512fbf5ca4c50c446884fc6069fdb589 to
16d2be641424815a1779119bb64bc6ba1be1161b, with minor tweaks to the
description of a few packages, removed ocaml-findlib from inputs, since
it's already implicit, and added a copyright line for you. Thanks!
Closed
S
S
Sören Tempel wrote on 12 Feb 09:41 +0100
(name . Julien Lepiller)(address . julien@lepiller.eu)
3LMU4EMXHNHRG.3EN4FKJ5JG3JK@8pit.net
Julien Lepiller <julien@lepiller.eu> wrote:
Toggle quote (5 lines)
> Applied to master as 8b679328512fbf5ca4c50c446884fc6069fdb589 to
> 16d2be641424815a1779119bb64bc6ba1be1161b, with minor tweaks to the
> description of a few packages, removed ocaml-findlib from inputs, since
> it's already implicit, and added a copyright line for you. Thanks!

Thank you for merging this! Is there any chance you could also take a look at
my KLEE patch https://issues.guix.gnu.org/68296? Similar to BinSec, KLEE is
a very popular symbolic execution tool. Unfortunately, I couldn't find a
suitable team for this patch and hence it has been stale for a while.

Greetings
Sören
Closed
?
Your comment

This issue is archived.

To comment on this conversation send an email to 68908@debbugs.gnu.org

To respond to this issue using the mumi CLI, first switch to it
mumi current 68908
Then, you may apply the latest patchset in this issue (with sign off)
mumi am -- -s
Or, compose a reply to this issue
mumi compose
Or, send patches to this issue
mumi send-email *.patch