[bug#38635] [WIP PATCH] Add why3 and frama-c

[Julien Lepiller <julien@lepiller.eu>]

[-- Attachment #1: Type: text/plain, Size: 1648 bytes --]

Hi Guix!

Since there was some interest very recently, I took another look at my
incomplete why3 and frama-c packages. I updated them and polished them
a little. I encourage formal-method guixers to test these patches,
especially if you are a user of why3 or frama-c, because I'm not sure
how these tools are supposed to be working.

Note that I didn't include ide support in why3 because this adds ~1GiB
to the closure of the program. A good thing could be to separate the
why3 library (not required when using why3) from the main package, in a
separate output.

For some reason, frama-c doesn't work directly, it needs to be in an
environment where its dependencies are present, hence the propagation.
However, it's failing at runtime:

$ guix environment --ad-hoc frama-c ocaml ocaml-findlib
[env]$ frama-c --help

[kernel] User Error: cannot load plug-in 'zip': cannot load
module Details: error loading shared library:
/gnu/store/hsjnvq5li28ak2wjnwlmqsfbg246skcg-profile/lib/ocaml/site-lib/zip/zip.cmxa:
invalid ELF header [kernel] User Error: cannot load plug-in 'why3':
cannot load module Details: error loading shared library:
/gnu/store/hsjnvq5li28ak2wjnwlmqsfbg246skcg-profile/lib/ocaml/site-lib/why3/why3.cmxs:
undefined symbol: camlGzip [kernel] User Error: cannot load plug-in
'frama-c-wp': cannot load module Details: error loading shared library:
/gnu/store/daqn9vsc15j3slbalw2fag6amndv8x98-frama-c-20.0/lib/frama-c/plugins/top/Wp.cmxs:
undefined symbol: camlWhy3__Theory [kernel] User Error: Deferred error
message was emitted during execution. See above messages for more
information. [kernel] Frama-C aborted: invalid user input.

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #2: 0001-gnu-Add-why3.patch --]
[-- Type: text/x-patch, Size: 4884 bytes --]

From 9fc13943b29196763524ddbc247218398d889459 Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
Date: Mon, 16 Dec 2019 12:09:16 +0100
Subject: [PATCH 1/2] gnu: Add why3.

* gnu/packages/maths.scm (why3): New variable.
---
 gnu/packages/maths.scm | 67 +++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 66 insertions(+), 1 deletion(-)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 0ed61ad4a1..991f164737 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -28,7 +28,7 @@
 ;;; Copyright © 2018 Adam Massmann <massmannak@gmail.com>
 ;;; Copyright © 2018 Marius Bakke <mbakke@fastmail.com>
 ;;; Copyright © 2018 Eric Brown <brown@fastmail.com>
-;;; Copyright © 2018 Julien Lepiller <julien@lepiller.eu>
+;;; Copyright © 2018, 2019 Julien Lepiller <julien@lepiller.eu>
 ;;; Copyright © 2018 Amin Bandali <bandali@gnu.org>
 ;;; Copyright © 2019 Nicolas Goaziou <mail@nicolasgoaziou.fr>
 ;;; Copyright © 2019 Steve Sprang <scs@stevesprang.com>
@@ -61,6 +61,7 @@
   #:use-module ((guix build utils) #:select (alist-replace))
   #:use-module (guix build-system cmake)
   #:use-module (guix build-system gnu)
+  #:use-module (guix build-system ocaml)
   #:use-module (guix build-system python)
   #:use-module (guix build-system ruby)
   #:use-module (gnu packages algebra)
@@ -72,10 +73,12 @@
   #:use-module (gnu packages check)
   #:use-module (gnu packages cmake)
   #:use-module (gnu packages compression)
+  #:use-module (gnu packages coq)
   #:use-module (gnu packages curl)
   #:use-module (gnu packages cyrus-sasl)
   #:use-module (gnu packages documentation)
   #:use-module (gnu packages elf)
+  #:use-module (gnu packages emacs)
   #:use-module (gnu packages flex)
   #:use-module (gnu packages fltk)
   #:use-module (gnu packages fontutils)
@@ -101,6 +104,7 @@
   #:use-module (gnu packages mpi)
   #:use-module (gnu packages multiprecision)
   #:use-module (gnu packages netpbm)
+  #:use-module (gnu packages ocaml)
   #:use-module (gnu packages onc-rpc)
   #:use-module (gnu packages pcre)
   #:use-module (gnu packages popt)
@@ -4182,6 +4186,67 @@ as equations, scalars, vectors, and matrices.")
 theories} (SMT) solver.  It provides a C/C++ API, as well as Python bindings.")
     (license license:expat)))
 
+(define-public why3
+  (package
+    (name "why3")
+    (version "1.2.1")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "https://gforge.inria.fr/frs/download.php/file"
+                                  "/38185/why3-" version ".tar.gz"))
+              (sha256
+               (base32
+                "014gkwisjp05x3342zxkryb729p02ngx1hcjjsrplpa53jzgz647"))))
+    (build-system ocaml-build-system)
+    (native-inputs
+     `(("coq" ,coq)
+       ("ocaml" ,ocaml)
+       ("which" ,which)))
+    (propagated-inputs
+     `(("camlzip" ,camlzip)
+       ("ocaml-graph" ,ocaml-graph)
+       ("ocaml-menhir" ,ocaml-menhir)
+       ("ocaml-num" ,ocaml-num)
+       ("ocaml-zarith" ,ocaml-zarith)))
+    (inputs
+     `(("coq-flocq" ,coq-flocq)
+       ("emacs-minimal" ,emacs-minimal)
+       ("zlib" ,zlib)))
+    (arguments
+     `(#:phases
+       (modify-phases %standard-phases
+         (add-before 'configure 'fix-configure
+           (lambda _
+             (setenv "CONFIG_SHELL" (which "sh"))
+             (substitute* "configure"
+               ;; find ocaml-num in the correct directory
+               (("\\$DIR/nums.cma") "$DIR/../nums.cma")
+               (("\\$DIR/num.cmi") "$DIR/../num.cmi"))
+             #t))
+         (add-after 'configure 'fix-makefile
+           (lambda _
+             (substitute* "Makefile"
+               ;; find ocaml-num in the correct directory
+               (("site-lib/num") "site-lib"))
+             #t))
+	 (add-after 'install 'install-lib
+	   (lambda _
+	     (invoke "make" "byte")
+	     (invoke "make" "install-lib")
+	     #t)))))
+    (home-page "http://why3.lri.fr")
+    (synopsis "Deductive program verification")
+    (description "Why3 provides a language for specification and programming,
+called WhyML, and relies on external theorem provers, both automated and
+interactive, to discharge verification conditions.  Why3 comes with a standard
+library of logical theories (integer and real arithmetic, Boolean operations,
+sets and maps, etc.) and basic programming data structures (arrays, queues,
+hash tables, etc.).  A user can write WhyML programs directly and get
+correct-by-construction OCaml programs through an automated extraction
+mechanism.  WhyML is also used as an intermediate language for the verification
+of C, Java, or Ada programs.")
+    (license license:lgpl2.1)))
+
 (define-public elpa
   (package
     (name "elpa")
-- 
2.24.0


[-- Attachment #3: 0002-gnu-Add-frama-c.patch --]
[-- Type: text/x-patch, Size: 2267 bytes --]

From f9501f1cc5725d49c69c948f6f7cc70c13f1dbdc Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
Date: Mon, 16 Dec 2019 12:40:18 +0100
Subject: [PATCH 2/2] gnu: Add frama-c.

* gnu/packages/maths.scm (frama-c): New variable.
---
 gnu/packages/maths.scm | 38 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 38 insertions(+)

diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 991f164737..d4e3e74c98 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -4247,6 +4247,44 @@ mechanism.  WhyML is also used as an intermediate language for the verification
 of C, Java, or Ada programs.")
     (license license:lgpl2.1)))
 
+(define-public frama-c
+  (package
+    (name "frama-c")
+    (version "20.0")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "http://frama-c.com/download/frama-c-"
+                                  version "-Calcium.tar.gz"))
+              (sha256
+               (base32
+                "03dvn162djylj2skmk6vv75gh87mm4s5cspkzcrlm5x0rlla2yqn"))))
+    (build-system ocaml-build-system)
+    (arguments
+     `(#:tests? #f; no test target in Makefile
+       #:phases
+       (modify-phases %standard-phases
+         (add-before 'configure 'export-shell
+           (lambda* (#:key inputs #:allow-other-keys)
+             (setenv "CONFIG_SHELL" (string-append (assoc-ref inputs "bash")
+                                                   "/bin/sh"))
+             #t)))))
+    (inputs
+     `(("gmp" ,gmp)))
+    (propagated-inputs
+     `(("ocaml-biniou" ,ocaml-biniou)
+       ("ocaml-easy-format" ,ocaml-easy-format)
+       ("ocaml-graph" ,ocaml-graph)
+       ("ocaml-yojson" ,ocaml-yojson)
+       ("ocaml-zarith" ,ocaml-zarith)
+       ("why3" ,why3)))
+    (home-page "http://frama-c.com")
+    (synopsis "C source code analysis platform")
+    (description "Frama-C is an extensible and collaborative platform dedicated
+to source-code analysis of C software.  The Frama-C analyzers assist you in
+various source-code-related activities, from the navigation through unfamiliar
+projects up to the certification of critical software.")
+    (license license:lgpl2.1+)))
+
 (define-public elpa
   (package
     (name "elpa")
-- 
2.24.0