From 806da098552f05bd4c3af82ba54bdae8c1ad54f1 Mon Sep 17 00:00:00 2001 From: Francesc Rocher Date: Thu, 21 Mar 2024 08:46:33 +0100 Subject: [PATCH] Initial support for Ada/SPARK --- lisp/ob-ada-spark.el | 496 +++++++++++++++++++++++++ testing/examples/ob-ada-spark-test.org | 300 +++++++++++++++ testing/lisp/test-ob-ada-spark.el | 240 ++++++++++++ 3 files changed, 1036 insertions(+) create mode 100644 lisp/ob-ada-spark.el create mode 100644 testing/examples/ob-ada-spark-test.org create mode 100644 testing/lisp/test-ob-ada-spark.el diff --git a/lisp/ob-ada-spark.el b/lisp/ob-ada-spark.el new file mode 100644 index 000000000..79f40df69 --- /dev/null +++ b/lisp/ob-ada-spark.el @@ -0,0 +1,496 @@ +;;; ob-ada-spark.el --- org-babel functions for Ada & SPARK -*- lexical-binding: t; -*- + +;; Copyright (C) 2021-2024 Free Software Foundation, Inc. + +;; Author: Francesc Rocher +;; Maintainer: Francesc Rocher +;; Keywords: literate programming, reproducible research, Ada/SPARK +;; URL: https://orgmode.org + +;; This file is part of GNU Emacs. + +;; GNU Emacs is free software: you can redistribute it and/or modify +;; it under the terms of the GNU General Public License as published by +;; the Free Software Foundation, either version 3 of the License, or +;; (at your option) any later version. + +;; GNU Emacs is distributed in the hope that it will be useful, +;; but WITHOUT ANY WARRANTY; without even the implied warranty of +;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +;; GNU General Public License for more details. + +;; You should have received a copy of the GNU General Public License +;; along with ob-ada-spark. If not, see . + +;;; Commentary: + +;; Org-Babel support for evaluating Ada & SPARK code and proving SPARK code. + +;;; Requirements: + +;; * An Ada compiler (gnatmake) +;; * A SPARK formal verification tool (gnatprove) +;; * Emacs ada-mode, optional but strongly recommended, see +;; + +;;; Code: + +(require 'ob) +(require 'time-stamp) + +(org-assert-version) + +(defvar org-babel-tangle-lang-exts) +(add-to-list 'org-babel-tangle-lang-exts '("ada" . "adb")) + +(defvar org-babel-temporary-directory) + +(defvar org-babel-default-header-args:ada '((:args . nil) + (:cflags . nil) + (:pflags . nil) + (:prove . nil) + (:template . nil) + (:unit . nil) + (:with . nil)) + "Ada/SPARK default header arguments.") + +(defconst org-babel-header-args:ada '((args . any) + (cflags . any) + (pflags . any) + (prove . ((nil t))) + (template . :any) + (unit . :any) + (with . nil)) + "Ada/SPARK specific header arguments.") + +(defconst ob-ada-spark-template-var-name-format "ob-ada-spark-template:%s" + "Format of the name of the template variables. +All templates must be defined in a variable with a name +compatible with this format. The template name is only the '%s' +part. From the source block, templates can be used in the +':template' header with the template name. + +For example, the template defined in the variable +`ob-ada-spark-template:ada-main' is used in the header of the +source block with ':template ada-main'.") + +(defcustom org-babel-ada-spark-compile-command "gnatmake" + "Command used to compile Ada/SPARK code into an executable. +May be either a command in the path, like gnatmake, or an +absolute path name. + +If using Alire 2.x, install the default native toolchain, with +`alr install gnat_native', and write here the path to gnatmake or +append $HOME/.alire/bin to PATH." + :group 'org-babel + :type 'string + :package-version '(Org . "9.7") + :safe #'stringp) + +(defcustom org-babel-ada-spark-prove-command "gnatprove" + "Command used to prove SPARK code. +May be either a command in the path, like gnatprove, or an +absolute path name, like /opt/ada/bin/gnatprove. + +If using Alire 2.x, install gnatprove, `alr install gnatprove', +and write here the path to gnatprove or append $HOME/.alire/bin +to PATH." + :group 'org-babel + :type 'string + :package-version '(Org . "9.7") + :safe #'stringp) + +(defcustom org-babel-ada-spark-default-compile-flags + "-f -we -gnata -gnateF -gnateV -gnatf -gnatVa -gnatwa -gnatX -gnat2022 -gnatW8" + "Default compiler flags for Ada and SPARK. +These flags are used to compile Ada and SPARK code. Any +additional flags specified in the ':clfags' header is passed +after the default ones. + +Default flags for gnatmake are: + + -f Force recompilations of non predefined units + -we Treat all warnings as errors + -gnata Assertions enabled. Pragma Assert/Debug to be activated + -gnateF Check overflow on predefined Float types + -gnateV Validity checks on subprogram parameters + -gnatf Full errors. Verbose details, all undefined references + -gnatwa Enable selected warning modes (turn on all info/warnings) + -gnatX Language extensions permitted + -gnat2022 Ada 2022 mode + -gnatW8 Wide character encoding method (?=h/u/s/e/8/b) +" + :group 'org-babel + :type 'string + :package-version '(Org . "9.7") + :safe #'stringp) + +(defcustom org-babel-ada-spark-default-prove-flags + "-f --assumptions --level=4 --report=all --verbose" + "Default flags for gnatprove. +These flags are used to prove SPARK code. Any additional flag +specified in the ':pflags' header is passed after the default +ones. + +The compiler flags are also passed to gnatprove using the +'-cargs' flag, both the the default flags in +`org-babel-ada-spark-default-compile-flags' and the flags +specified in the ':cflags' header, in that order. + +Default flags for gnatprove are: + + -f Force recompilation/analysis of all units + --assumptions Output assumptions information + --level=4 Set the level of proof (0 = faster to 4 = more powerful) + --report=all Set the report mode of GNATprove (r=fail*, all, + provers, statistics) + --verbose Output extra verbose information +" + :group 'org-babel + :type 'string + :package-version '(Org . "9.7") + :safe #'stringp) + +(defcustom org-babel-ada-spark-default-file-header + (lambda () + (format + "----------------------------------------------------------------------------- +-- +-- Source code generated automatically by 'org-babel-tangle' from +-- file %s +-- %s +-- +-- DO NOT EDIT!! +-- +----------------------------------------------------------------------------- + +" + (buffer-file-name (current-buffer)) + (time-stamp-string "%Y-%02m-%02d %02H:%02M:%02S"))) + "Header written in files generated with `org-babel-tangle'." + :group 'org-babel + :type 'function + :package-version '(Org . "9.7")) + +(defvar ob-ada-spark-template:ada-main + '((:params . ((:unit . "main") (:cflags . "-gnatW8"))) + (:body . "with Ada.Text_IO; use Ada.Text_IO; +%s +procedure Main is +%s +end Main; +")) + "Template for a basic Main procedure written in Ada 2022. +Makes use of the Ada.Text_IO (with and use clauses). Admits +additional with'ed packages and a procedure body. + +Use this template as a starting point for new Ada templates. All +templates must include two placeholders, for the with section and +for the body. + +Example of use: + +#+begin_src ada :template ada-main :with System.OS_Lib + Time : constant String := Current_Time_String; +begin + Put_Line (Time); +#+end_src + +The resulting body is: + +with Ada.Text_IO; use Ada.Text_IO; +with System.OS_Lib; use System.OS_Lib; + +procedure Main is + Time : constant String := Current_Time_String; +begin + Put_Line (Time); +end Main; +") + +(defvar ob-ada-spark-template:spark-main + '((:params . ((:cflags . "-gnatW8") (:prove . t) (:unit . "main"))) + (:body . "with Ada.Text_IO; use Ada.Text_IO; +%s +procedure Main with Spark_Mode => On is +%s +end Main; +")) + "Template for a basic Main procedure written in SPARK. +Makes use of the Ada.Text_IO (with and use clauses). Admits +additional with'ed packages and a procedure body. + +Use this template as a starting point for new SPARK templates. All +templates must include two placeholders, for the with section and +for the body. + +Example of use: + +#+begin_src ada :template ada-main :with System.OS_Lib + Put_Line (Current_Time_String); +#+end_src + +The resulting body is: + +with Ada.Text_IO; use Ada.Text_IO; +with System.OS_Lib; use System.OS_Lib; + +procedure Main is +begin + Put_Line (Current_Time_String); +end Main; +") + +(defun ob-ada-spark-replace-params-from-template (params) + "Replace headers in PARAMS with headers defined in the template. +If a template defines a set of params, replace the values in +PARAMS with the values defined in the template, overwriting +parameters already defined in the source code block. +Return the new list of PARAMS, or the original list if the +template does not define any header or no template is used." + (let* ((template-name (cdr (assq :template params))) + (template (eval + (intern-soft + (format ob-ada-spark-template-var-name-format + template-name))))) + (if template + (progn + (message "-- replacing params from template %s" template-name) + (mapc (lambda (p) + (assq-delete-all (car p) params)) + (cdr (assq :params template))) + (append params (cdr (assq :params template)))) + params))) + +(defun org-babel-expand-body:ada (body params) + "Expand BODY according to PARAMS and return the expanded body. +Body expansion comprises replacement of template and literal +variables. +First, template is filled with the value of ':with' and ':body' +headers in PARAMS. Second, all literal variables are replaced by +the values found in the ':var' header of PARAMS." + (let* ((template-name (cdr (assq :template params))) + (template (eval + (intern-soft + (format ob-ada-spark-template-var-name-format + template-name)))) + (vars (org-babel--get-vars params)) + (with (cdr (assq :with params)))) + + (if (and template-name (null template)) + (error + "Invalid template name '%s', variable ob-ada-spark-template:%s undefined" + template-name template-name)) + + ;; Use the body defined in the template, if any. It needs two + ;; parameters: the 'with' section (defined in params) and the + ;; 'body' section (the contents of source code block) + (setq body + (if template + (progn + (message "-- expanding body from template %s" template-name) + (format + ;; body's template as format control string + (cdr (assq :body template)) + (if (null with) "" + ;; replace :with parameter + (mapconcat + (lambda (w) (format "with %s; use %s;\n" w w)) + (split-string with " " t) + "")) + ;; use body in the source code block + body)) + body)) + + ;; expand literal variables in the body, if any + (when vars + (mapc + (lambda (var) + (let ((key (car var)) + (val (cdr var))) + (setq body (string-replace (format "%s" key) (format "%s" val) body)))) + vars)) + body)) + +(defun org-babel-execute:ada (body params) + "Execute or prove a block of Ada/SPARK code with org-babel. +BODY contains the Ada/SPARK source code to evaluate. PARAMS is +the list of source code block parameters. + +This function is called by `org-babel-execute-src-block'" + (let* ((processed-params (org-babel-process-params params)) + (all-params + (ob-ada-spark-replace-params-from-template processed-params)) + (full-body (org-babel-expand-body:ada body all-params)) + (prove (cdr (assq :prove all-params)))) + (if prove + (ob-ada-spark-prove full-body all-params) + (ob-ada-spark-execute full-body all-params)))) + +(defun ob-ada-spark-execute (body params) + "Execute or prove a block of Ada/SPARK code with org-babel. +BODY contains the Ada/SPARK source code to evaluate, already +expanded when using templates. PARAMS is the list of source code +block parameters, also expanded with the template parameters. + +This function is called by `org-babel-execute:ada'" + (let* ((args (cdr (assq :args params))) + (cflags (cdr (assq :cflags params))) + (unit (cdr (assq :unit params))) + (default-directory (org-babel-temp-directory)) + (tmp-src-file (if unit + (file-name-concat (org-babel-temp-directory) + (concat unit ".adb")) + (org-babel-temp-file "ada-src-" ".adb"))) + (tmp-bin-file (if unit + (file-name-concat (org-babel-temp-directory) unit) + (org-babel-temp-file "ada-bin-" org-babel-exeext)))) + + ;; write compilation unit + (with-temp-file tmp-src-file (insert body)) + + ;; clean previous evaluation of the same unit + (if (stringp unit) + (cl-mapcar + (lambda (ext) + (let ((file (file-name-concat default-directory + (concat unit ext)))) + (if (file-exists-p file) (delete-file file)))) + '("" ".ali" ".o"))) + + ;; compile + (setq compile-command + (format "%s %s -o %s %s %s" + org-babel-ada-spark-compile-command + (or org-babel-ada-spark-default-compile-flags "") + tmp-bin-file + (or cflags "") + tmp-src-file)) + (message "-- Ada compile-command: %s" compile-command) + (org-babel-eval compile-command "") + + ;; execute + (let* ((exec-command (concat tmp-bin-file (if args (concat " " args) ""))) + (results + (org-trim + (org-remove-indentation + (org-babel-eval exec-command ""))))) + (org-babel-reassemble-table + (org-babel-result-cond (cdr (assq :result-params params)) + (org-babel-read results) + (let ((tmp-file (org-babel-temp-file "ada-"))) + (with-temp-file tmp-file (insert results)) + (org-babel-import-elisp-from-file tmp-file))) + (org-babel-pick-name + (cdr (assq :colname-names params)) (cdr (assq :colnames params))) + (org-babel-pick-name + (cdr (assq :rowname-names params)) (cdr (assq :rownames params))))))) + +(defun ob-ada-spark-prove (body params) + "Prove a block of SPARK code with org-babel. +BODY contains the SPARK source code to prove, already expanded +when using templates. PARAMS is the list of source code block +parameters, also expanded with the template parameters. + +This function is called by `org-babel-execute:ada'" + (let* ((cflags (cdr (assq :cflags params))) + (pflags (cdr (assq :pflags params))) + (unit (cdr (assq :unit params))) + (default-directory (org-babel-temp-directory)) + (tmp-src-file (if unit (concat unit ".adb") "spark_src.adb")) + (tmp-gpr-file (if unit (concat unit ".gpr") "spark_prj.gpr")) + (tmp-project (file-name-sans-extension tmp-gpr-file)) + (prove-command-args + (format "-P %s %s %s -u %s -cargs %s %s" + tmp-gpr-file + (or org-babel-ada-spark-default-prove-flags "") + (or pflags "") + tmp-src-file + (or org-babel-ada-spark-default-compile-flags "") + (or cflags "")))) + + ;; write compilation unit + (with-temp-file tmp-src-file (insert body)) + + ;; create temporary project + (with-temp-file tmp-gpr-file + (insert (format "project %s is + for Source_Dirs use (\"%s\"); + for Source_Files use (\"%s\"); + for Main use (\"%s\"); +end %s; +" + tmp-project + default-directory + tmp-src-file + tmp-src-file + tmp-project))) + + ;; remove gnatprove directory and clean previous evaluation of the + ;; same unit + (delete-directory + (file-name-concat org-babel-temporary-directory "gnatprove") t) + (org-babel-eval + (format "%s --clean %s" + org-babel-ada-spark-prove-command prove-command-args) + "") + + ;; invoke gnatprove + (let* ((prove-command + (format "%s %s" + org-babel-ada-spark-prove-command prove-command-args)) + (results + (org-trim + (org-remove-indentation + (org-babel-eval prove-command ""))))) + (message "-- SPARK prove-command: %s" prove-command) + (org-babel-reassemble-table + (org-babel-result-cond (cdr (assq :result-params params)) + (org-babel-read results) + (let ((tmp-file (org-babel-temp-file "ada-"))) + (with-temp-file tmp-file (insert results)) + (org-babel-import-elisp-from-file tmp-file))) + (org-babel-pick-name + (cdr (assq :colname-names params)) (cdr (assq :colnames params))) + (org-babel-pick-name + (cdr (assq :rowname-names params)) (cdr (assq :rownames params))))))) + +(defun org-babel-prep-session:ada-spark () + "This function does nothing. +Ada and SPARK are compiled languages with no support for +sessions." + (error "Ada & SPARK are compiled languages -- no support for sessions")) + +(defvar ada-skel-initial-string--backup "") + +(defun ob-ada-spark-pre-tangle-hook () + "This function is called just before `org-babel-tangle'. +When using tangle to export Ada/SPARK code to a file, this +function is used to set the header of the file according to the +value of the variable `org-babel-ada-spark-default-file-header'." + ;; ada-skel-initial-string is defined in ada-mode and is inserted + ;; automatically when Emacs sets ada-mode in an empty buffer; switching + ;; temporarily its value so the org-babel-ada-spark-default-file-header is + ;; inserted + (if (boundp 'ada-skel-initial-string) + (progn (setq ada-skel-initial-string--backup ada-skel-initial-string) + (setq ada-skel-initial-string (funcall org-babel-ada-spark-default-file-header))))) + +(defun ob-ada-spark-post-tangle-hook () + "This function is called just after `org-babel-tangle'. +Once the file has been generated, this function restores the +value of the header inserted into Ada/SPARK files." + ;; if ada-skel-initial-string has not been inserted by ada-mode, then + ;; insert the default header + (if (boundp 'ada-skel-initial-string) + (setq ada-skel-initial-string ada-skel-initial-string--backup) + (save-excursion + (goto-char (point-min)) + (insert (funcall org-babel-ada-spark-default-file-header))))) + +(add-hook 'org-babel-pre-tangle-hook #'ob-ada-spark-pre-tangle-hook) +(add-hook 'org-babel-post-tangle-hook #'ob-ada-spark-post-tangle-hook) + +(provide 'ob-ada-spark) + +;;; ob-ada-spark.el ends here diff --git a/testing/examples/ob-ada-spark-test.org b/testing/examples/ob-ada-spark-test.org new file mode 100644 index 000000000..dec1e371c --- /dev/null +++ b/testing/examples/ob-ada-spark-test.org @@ -0,0 +1,300 @@ +#+PROPERTY: results silent scalar +#+title:A collection of examples for ob-ada-spark tests + +* Simple programs + +** Hello world +:PROPERTIES: +:ID: 778e63c2-2644-4a6f-8e7d-f956fa3d9241 +:END: + +#+name: Hello world +#+begin_src ada :results silent + with Ada.Text_IO; + procedure Hello_World is + begin + Ada.Text_IO.Put_Line ("Hello world"); + end Hello_World; +#+end_src + +** Recursive Fibonacci +:PROPERTIES: +:ID: 6281cb40-26cc-423e-88c8-e8f26901ee4a +:END: + +#+name: Recursive Fibonacci +#+begin_src ada :unit fibonacci :results silent + with Ada.Text_IO; + procedure Fibonacci is + function fib (n : Natural) return Natural is + (if n <= 2 then 1 else fib (n-1) + fib (n-2)); + Fib_15 : Natural; + begin + Fib_15 := fib (15); + Ada.Text_IO.Put_Line (Fib_15'Image); + end Fibonacci; +#+end_src + +** Sequential Fibonacci +:PROPERTIES: +:ID: 41b4514b-0d46-4011-b5fa-7997aecf75a9 +:END: + +#+name Sequential Fibonacci +#+begin_src ada :unit fibonacci :results silent + with Ada.Text_IO; use Ada.Text_IO; + procedure Fibonacci is + function fib (n : Natural) return Natural is + fn1, fn2 : Natural := 1; + begin + return result : Natural := 1 do + for i in reverse 3 .. n loop + result := fn1 + fn2; + fn2 := fn1; + fn1 := result; + end loop; + end return; + end fib; + Fib_15 : constant Natural := fib (15); + begin + Ada.Text_IO.Put_Line (Fib_15'Image); + end Fibonacci; +#+end_src + +** UTF8 identifiers +:PROPERTIES: +:ID: 06e4dc5b-5566-486b-81af-cb7c547d46f1 +:END: + +#+name: UTF8 indetifiers +#+begin_src ada :unit average :results silent + with Ada.Text_IO; use Ada.Text_IO; + procedure Average is + Σ_numbers : Natural := 0; + α, β, Δ_x : Natural := 1; + Average : Float; + begin + loop + Σ_numbers := @ + α; + exit when α > 100; + α := @ + Δ_x; + β := @ + 1; + Δ_X := @ * 2; + end loop; + Average := Float (Σ_numbers) / Float (β); + Put_Line ("Average:" & Natural (Average)'Image); + end Average; +#+end_src + +* Using templates + +** Main template +:PROPERTIES: +:ID: a2a64153-a7b6-4c32-84c5-a589f0caac93 +:END: + +#+name: Main template +#+begin_src ada :template ada-main :results silent +begin + Put_Line ("Hello world"); +#+end_src + +** Fibonacci +:PROPERTIES: +:ID: cbef4ee3-63e3-4295-8b26-e2470e30b1ff +:END: + +#+name: Fibonacci +#+begin_src ada :template ada-main :results silent + -- declaratiions + function fib (n : Natural) return Natural is + (if n <= 2 then 1 else fib (n-1) + fib (n-2)); + Fib_15 : Natural; + +begin + Fib_15 := fib (15); + Put_Line (Fib_15'Image); +#+end_src + +** Invalid template name +:PROPERTIES: +:ID: 3fb0ac1c-dfed-4d2f-9803-d1dea18eec45 +:END: + +#+name: Invalid template +#+begin_src ada :template foo-bar :results silent +begin + Put_Line ("Hello world"); +#+end_src + +* Literate programming + +** Hello noweb +:PROPERTIES: +:ID: 5386221e-da6f-411f-8dd5-3045e14b2e15 +:END: + +#+name: __Say_Hello_Noweb__ +#+begin_src ada + Put_Line ("Hello noweb"); +#+end_src + +#+header: :noweb yes +#+name: Hello noweb +#+begin_src ada :unit hello_world :results silent scalar + with Ada.Text_IO; use Ada.Text_IO; + procedure Hello_World is + begin + <<__Say_Hello_Noweb__>> + end Hello_World; +#+end_src + +** Constant literals +:PROPERTIES: +:ID: 1bc1f537-e31f-4b8e-adb3-bdd474673e17 +:END: + +#+name: __Say_Hello__ +#+begin_src ada + Put ("Hello"); +#+end_src + +#+header: :noweb yes +#+header: :var __TIMES__=3 +#+name: Constant literals +#+begin_src ada :template ada-main :results silent scalar +begin + for I in 1 .. __TIMES__ loop + Put (I'Image & " "); + <<__Say_Hello__>> + end loop; +#+end_src + +#+header: :var __MESSAGE__="Hellow world" +#+name: Constant literals - invalid literal name +#+begin_src ada :template ada-main :results silent scalar + Put_Line ("Message: " & __MSG__); +#+end_src + +** Evaluated literals +:PROPERTIES: +:ID: 7cc220c1-a917-4af4-a497-7e247f1c15ae +:END: + +#+header: :var __SUM__=(+ 1 1 3 5 8 13 34 55 89 144) +#+name: Variable evaluation +#+begin_src ada :template ada-main :results silent scalar +begin + Put_Line ("SUM is __SUM__"); +#+end_src + +* User-Defined templates + +For the test, the template =ob-ada-spark-template:test= is defined in +the file =test-ob-ada-spark.el=. + +** Test +:PROPERTIES: +:ID: 70feb9e8-19f1-402b-b1d0-4c8ccdf2cfe4 +:END: + +#+name: Test +#+begin_src ada :template test + Write_Answer (42); +#+end_src + +** Using and evaluated literals +:PROPERTIES: +:ID: 2a05b182-07bf-4ba5-9cca-128919cb837e +:END: + +#+header: :var __Answer__=(* 21 2) +#+name: Using evaluated literals +#+begin_src ada :template test + Write_Answer (__Answer__); +#+end_src + +** Using noweb and evaluated literals +:PROPERTIES: +:ID: 69e852b1-a278-4051-8719-917cfb59c582 +:END: + +#+name: __Write_Answer__ +#+begin_src ada :template test + Write_Answer (__Answer__); +#+end_src + +#+header: :noweb yes +#+header: :var __Answer__=(* 21 2) +#+name: Using noweb and evaluated literals +#+begin_src ada :template test + <<__Write_Answer__>> +#+end_src + +* Proving SPARK code + +** Increment + +#+name: __Increment__ +#+begin_src ada + subtype Nat16 is Natural range 0 .. 2**16; + Number : Nat16 := Nat16'Last - 1; + + procedure Increment (X : in out Nat16) with + Global => null, + Depends => (X => X), + Pre => (X < Nat16'Last), + Post => (X = X'Old + 1) + is + begin + X := X + 1; + end Increment; + +begin + Increment (Number); + Put_Line ("Last Nat16 is" & Number'Image); +#+end_src + +** Stone +:PROPERTIES: +:ID: fd628dbb-aacc-4931-aab5-5816f7c85b46 +:END: + +#+name: Stone +#+header: :noweb yes +#+begin_src ada :template spark-main :pflags --mode=stone :results scalar + <<__Increment__>> +#+end_src + +** Bronze +:PROPERTIES: +:ID: 79b4ca15-8127-467d-b239-dd190cb45f2d +:END: + +#+name: Bronze +#+header: :noweb yes +#+begin_src ada :template spark-main :pflags --mode=bronze :results scalar + <<__Increment__>> +#+end_src + +** Silver +:PROPERTIES: +:ID: 4529e47f-835a-4410-883a-b3fab0026553 +:END: + +#+name: Silver +#+header: :noweb yes +#+begin_src ada :template spark-main :pflags --mode=silver :results scalar + <<__Increment__>> +#+end_src + +** Gold +:PROPERTIES: +:ID: 371d0f89-4281-48b4-a70b-d0b51d515423 +:END: + +#+name: Gold +#+header: :noweb yes +#+begin_src ada :template spark-main :pflags --mode=gold :results scalar + <<__Increment__>> +#+end_src diff --git a/testing/lisp/test-ob-ada-spark.el b/testing/lisp/test-ob-ada-spark.el new file mode 100644 index 000000000..21ab66026 --- /dev/null +++ b/testing/lisp/test-ob-ada-spark.el @@ -0,0 +1,240 @@ +;;; test-ob-ada-spark.el --- tests for ob-ada-spark.el -*- lexical-binding: t; -*- + +;; Copyright (c) 2024 Free Software Foundation, Inc. +;; Authors: Francesc Rocher +;; Maintainer: Francesc Rocher + +;; This file is part of GNU Emacs. + +;; This program is free software; you can redistribute it and/or modify +;; it under the terms of the GNU General Public License as published by +;; the Free Software Foundation, either version 3 of the License, or +;; (at your option) any later version. + +;; This program is distributed in the hope that it will be useful, +;; but WITHOUT ANY WARRANTY; without even the implied warranty of +;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +;; GNU General Public License for more details. + +;; You should have received a copy of the GNU General Public License +;; along with this program. If not, see . + +;;; Code: +(require 'ob-core) +(require 'ob-ada-spark) + +(org-test-for-executable "gnatmake") +(org-test-for-executable "gnatprove") + +(unless (featurep 'ob-ada-spark) + (signal 'missing-test-dependency "Support for Ada and SPARK code blocks")) + +;; Simple programs + +(ert-deftest ob-ada-spark/simple/hello-world () + "Simple program: Hello world" + (org-test-at-id + "778e63c2-2644-4a6f-8e7d-f956fa3d9241" + (org-babel-next-src-block) + (should (equal "Hello world" (org-babel-execute-src-block))))) + +(ert-deftest ob-ada-spark/simple/recursive-fibonacci () + "Simple program: Recursive Fibonacci" + (org-test-at-id + "6281cb40-26cc-423e-88c8-e8f26901ee4a" + (org-babel-next-src-block) + (should (= 610 (org-babel-execute-src-block))))) + +(ert-deftest ob-ada-spark/simple/sequential-fibonacci () + "Simple program: Sequential Fibonacci" + (org-test-at-id + "41b4514b-0d46-4011-b5fa-7997aecf75a9" + (org-babel-next-src-block) + (should (= 610 (org-babel-execute-src-block))))) + +(ert-deftest ob-ada-spark/simple/utf8-identifiers () + "Simple program: UTF-8 indentifiers" + (org-test-at-id + "06e4dc5b-5566-486b-81af-cb7c547d46f1" + (org-babel-next-src-block) + (should (equal "Average: 32" (org-babel-execute-src-block))))) + +(ert-deftest ob-ada-spark/simple/utf8-identifiers-error () + "Simple program: UTF-8 indentifiers" + (org-test-at-id + "06e4dc5b-5566-486b-81af-cb7c547d46f1" + (org-babel-next-src-block 2) + (when (should (buffer-live-p (get-buffer org-babel-error-buffer-name))) + (kill-buffer org-babel-error-buffer-name)) + :type 'error)) + +;; Using templates + +(ert-deftest ob-ada-spark/using-templates/main-template () + "Using templates: Main template" + (org-test-at-id + "a2a64153-a7b6-4c32-84c5-a589f0caac93" + (org-babel-next-src-block) + (should (equal "Hello world" (org-babel-execute-src-block))))) + +(ert-deftest ob-ada-spark/using-templates/fibonacci () + "Using templates: Fibonacci" + (org-test-at-id + "cbef4ee3-63e3-4295-8b26-e2470e30b1ff" + (org-babel-next-src-block) + (should (= 610 (org-babel-execute-src-block))))) + +(ert-deftest ob-ada-spark/using-templates/invlaid-template-name () + "Using templates: Invalid template name" + (org-test-at-id + "3fb0ac1c-dfed-4d2f-9803-d1dea18eec45" + (org-babel-next-src-block) + (when (should (buffer-live-p (get-buffer org-babel-error-buffer-name))) + (kill-buffer org-babel-error-buffer-name)) + :type 'error)) + +;; Literate programming + +(ert-deftest ob-ada-spark/literate-programming/hello-noweb () + "Literate programming: Hello noweb" + (org-test-at-id + "5386221e-da6f-411f-8dd5-3045e14b2e15" + (org-babel-next-src-block 2) + (should (equal "Hello noweb" (org-babel-execute-src-block))))) + +(ert-deftest ob-ada-spark/literate-programming/constant-literals () + "Literate programming: Constant literals" + (org-test-at-id + "1bc1f537-e31f-4b8e-adb3-bdd474673e17" + (org-babel-next-src-block 2) + (should (equal "1 Hello 2 Hello 3 Hello" + (org-babel-execute-src-block))))) + +(ert-deftest ob-ada-spark/literate-programming/constant-literals-invalid-literal-name () + "Literate programming: Constant literals - Invalid literal name" + (org-test-at-id + "1bc1f537-e31f-4b8e-adb3-bdd474673e17" + (org-babel-next-src-block 3) + (when (should (buffer-live-p (get-buffer org-babel-error-buffer-name))) + (kill-buffer org-babel-error-buffer-name)) + :type 'error)) + +(ert-deftest ob-ada-spark/using-templates/evaluated-literals () + "Using templates: Evaluated literals" + (org-test-at-id + "7cc220c1-a917-4af4-a497-7e247f1c15ae" + (org-babel-next-src-block) + (should (equal "SUM is 353" (org-babel-execute-src-block))))) + +;; User-defined templates + +(setq ob-ada-spark-template:test + '((:params . ((:unit . "main") (:results silent))) + (:body . " +with Ada.Text_IO; use Ada.Text_IO; +%s +procedure Main is + procedure Write_Answer (N : Natural) is + begin + Put_Line (\"Answer:\" & N'Image); + end Write_Answer; +begin + %s +end Main; +"))) + +(ert-deftest ob-ada-spark/user-defined-template/test () + "Users-defined templates: Test" + (org-test-at-id + "70feb9e8-19f1-402b-b1d0-4c8ccdf2cfe4" + (org-babel-next-src-block) + (should (equal "Answer: 42" (org-babel-execute-src-block))))) + +(ert-deftest ob-ada-spark/user-defined-template/using-evaluated-literals () + "Users-defined templates: Using evaluated literals" + (org-test-at-id + "2a05b182-07bf-4ba5-9cca-128919cb837e" + (org-babel-next-src-block) + (should (equal "Answer: 42" (org-babel-execute-src-block))))) + +(ert-deftest ob-ada-spark/user-defined-template/using-noweb-and-evaluated-literals () + "Users-defined templates: Using noweb and evaluated literals" + (org-test-at-id + "69e852b1-a278-4051-8719-917cfb59c582" + (org-babel-next-src-block 2) + (should (equal "Answer: 42" (org-babel-execute-src-block))))) + +;; Proving SPARK Code + +(ert-deftest ob-ada-spark/proving-spark-code/stone () + "Proving SPARK code: Stone" + (org-test-at-id + "fd628dbb-aacc-4931-aab5-5816f7c85b46" + (org-babel-next-src-block) + (org-babel-execute-src-block) + (should (search-forward "#+begin_example" nil t)) + (forward-line 1) + (let ((report-begin (point-at-bol)) + (report-end 0)) + (should (search-forward "#+end_example" nil t)) + (forward-line -1) + (setq report-end (point-at-eol)) + (should + (string-match + "Phase 1 of 2: generation of Global contracts ... +\\(.\\|\n\\)+ +Phase 2 of 2: full checking of SPARK legality rules ..." + (buffer-substring-no-properties report-begin report-end)))))) + +(ert-deftest ob-ada-spark/proving-spark-code/bronze () + "Proving SPARK code: Bronze" + (org-test-at-id + "79b4ca15-8127-467d-b239-dd190cb45f2d" + (org-babel-next-src-block) + (org-babel-execute-src-block) + (should (search-forward "#+begin_example" nil t)) + (forward-line 1) + (let ((report-begin (point-at-bol)) + (report-end 0)) + (should (search-forward "#+end_example" nil t)) + (forward-line -1) + (setq report-end (point-at-eol)) + (should + (string-match + "Phase 1 of 2: generation of Global contracts ... +\\(.\\|\n\\)+ +Phase 2 of 2: analysis of data and information flow ... +\\(.\\|\n\\)+ +main.adb:8:07: info: data dependencies proved +main.adb:9:07: info: flow dependencies proved" + (buffer-substring-no-properties report-begin report-end)))))) + +(ert-deftest ob-ada-spark/proving-spark-code/silver () + "Proving SPARK code: Silver" + (org-test-at-id + "4529e47f-835a-4410-883a-b3fab0026553" + (org-babel-next-src-block) + (org-babel-execute-src-block) + (should (search-forward "#+begin_example" nil t)) + (forward-line 1) + (let ((report-begin (point-at-bol)) + (report-end 0)) + (should (search-forward "#+end_example" nil t)) + (forward-line -1) + (setq report-end (point-at-eol)) + (should + (string-match + "Phase 1 of 2: generation of Global contracts ... +\\(.\\|\n\\)+ +Phase 2 of 2: flow analysis and proof ... +\\(.\\|\n\\)+ +main.adb:8:07: info: data dependencies proved +main.adb:9:07: info: flow dependencies proved +main.adb:11:18: info: postcondition proved +main.adb:14:14: info: range check proved +main.adb:18:04: info: precondition proved +main.adb:19:30: info: range check proved" + (buffer-substring-no-properties report-begin report-end)))))) + +(provide 'test-ob-ada-spark) +;;; test-ob-ada-spark.el ends here -- 2.43.0