[bug#68908] [PATCH] Add BINSEC.

[bug#68908] [PATCH] Add BINSEC.

[soeren]

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

[bug#68908] [PATCH] gnu: Add ocaml-iso8601

[soeren]

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(+)

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")

[bug#68908] [PATCH] gnu: Add ocaml-toml.

[soeren]

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(+)

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")

[bug#68908] [PATCH] gnu: Add ocaml-pp.

[soeren]

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(+)

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")

[bug#68908] [PATCH] gnu: Add ocaml-grain-dypgen.

[soeren]

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(+)

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")

[bug#68908] [PATCH] gnu: Add ocaml-ordering.

[soeren]

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(+)

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)

[bug#68908] [PATCH] gnu: Add ocaml-dyn.

[soeren]

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(+)

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)

[bug#68908] [PATCH] gnu: Add ocaml-stdune.

[soeren]

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(+)

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)

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

[soeren]

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(+)

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)

[bug#68908] [PATCH] gnu: Add ocaml-dune-site.

[soeren]

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(+)

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)

[bug#68908] [PATCH] gnu: Add binsec.

[soeren]

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(+)

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")

[bug#68908] [PATCH] Add BINSEC.

[Julien Lepiller]

Le Sat,  3 Feb 2024 16:03:19 +0100,
soeren@soeren-tempel.net a écrit :

> 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!

> 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
> 
> 

bug#68908: [PATCH] Add BINSEC.

[Julien Lepiller]

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!

[bug#68908] [PATCH] Add BINSEC.

[Sören Tempel]

Julien Lepiller <julien@lepiller.eu> wrote:
> 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