[PATCH] Add BINSEC.

Done

Details

2 participants

Julien Lepiller
soeren

Owner: unassigned

Submitted by: soeren

Severity: normal

soeren wrote on 3 Feb 16:03 +0100

Recipients:(address . guix-patches@gnu.org)

Message-ID:cover.1706972151.git.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

soeren wrote on 3 Feb 16:11 +0100

[PATCH] gnu: Add ocaml-iso8601

Recipients:(address . 68908@debbugs.gnu.org)

Message-ID:78a03f74beedf71f343dcd73baf4a31a4100ab14.1706972151.git.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")

soeren wrote on 3 Feb 16:11 +0100

[PATCH] gnu: Add ocaml-pp.

Recipients:(address . 68908@debbugs.gnu.org)

Message-ID:34e73be66b832c186ff8a3cc0be546950da67da8.1706972151.git.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")

soeren wrote on 3 Feb 16:11 +0100

[PATCH] gnu: Add ocaml-toml.

Recipients:(address . 68908@debbugs.gnu.org)

Message-ID:2d9d01dbdc500dbe07618c172645e99e3d2a62fa.1706972151.git.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")

soeren wrote on 3 Feb 16:12 +0100

[PATCH] gnu: Add ocaml-grain-dypgen.

Recipients:(address . 68908@debbugs.gnu.org)

Message-ID:88e924b717a307c24434e610f1b1c538fb8f9879.1706972151.git.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")

soeren wrote on 3 Feb 16:12 +0100

[PATCH] gnu: Add ocaml-ordering.

Recipients:(address . 68908@debbugs.gnu.org)

Message-ID:cda0b535ae0e7e85c16d93c5bfba66193987106f.1706972151.git.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)

soeren wrote on 3 Feb 16:12 +0100

[PATCH] gnu: Add ocaml-dyn.

Recipients:(address . 68908@debbugs.gnu.org)

Message-ID:bc496d140b7080708a474d0db9d120eb6bac4b0c.1706972151.git.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)

soeren wrote on 3 Feb 16:12 +0100

[PATCH] gnu: Add ocaml-stdune.

Recipients:(address . 68908@debbugs.gnu.org)

Message-ID:ade1d9a963c3f0d89136c6639cc48fc774d0e0ed.1706972151.git.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)

soeren wrote on 3 Feb 16:12 +0100

[PATCH] gnu: Add ocaml-dune-private-libs.

Recipients:(address . 68908@debbugs.gnu.org)

Message-ID:22782da727d7d93f129d6247ab19e5bd84b2976c.1706972151.git.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)

soeren wrote on 3 Feb 16:12 +0100

[PATCH] gnu: Add ocaml-dune-site.

Recipients:(address . 68908@debbugs.gnu.org)

Message-ID:19603445c6e4d01e6622116d9c9330bbda5d3e7b.1706972151.git.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)

soeren wrote on 3 Feb 16:12 +0100

[PATCH] gnu: Add binsec.

Recipients:(address . 68908@debbugs.gnu.org)

Message-ID:d9700078afdf2237d3a5070ab6223dc8e8d9329d.1706972151.git.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")

Julien Lepiller wrote on 3 Feb 22:52 +0100

Re: [bug#68908] [PATCH] Add BINSEC.

Recipients:(address . soeren@soeren-tempel.net)

Message-ID: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
> 
>

Julien Lepiller wrote on 11 Feb 17:32 +0100

Recipients:(address . soeren@soeren-tempel.net)

Message-ID: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ören Tempel wrote on 12 Feb 09:41 +0100

Recipients:(name . Julien Lepiller)(address . julien@lepiller.eu)

Message-ID: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

is:open	open issues
is:done	closed issues
submitter:<who>	search issue submitter
author:<who>	search by message author
date:yesterday..now	search by issue date
mdate:3m..2d	search by message date