;;   This file is part of scheme-GNUnet, a partial Scheme port of GNUnet.
;;   Copyright (C) 2021 GNUnet e.V.
;;
;;   GNUnet is free software: you can redistribute it and/or modify it
;;   under the terms of the GNU Affero General Public License as published
;;   by the Free Software Foundation, either version 3 of the License,
;;   or (at your option) any later version.
;;
;;   GNUnet 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
;;   Affero General Public License for more details.
;;
;;   You should have received a copy of the GNU Affero General Public License
;;   along with this program.  If not, see <http://www.gnu.org/licenses/>.
;;
;;   SPDX-License-Identifier: AGPL-3.0-or-later

(import (quickcheck)
	(quickcheck property)
	(quickcheck arbitrary)
	(quickcheck generator)
	(bytestructures guile)
	(srfi srfi-1)
	(srfi srfi-26)
	(ice-9 binary-ports)
	(ice-9 control)
	(ice-9 receive)
	(rnrs bytevectors)
	(rnrs conditions)
	(gnu gnunet util cmsg)
	(gnu gnunet utils bv-slice))

(define lcov? #f)

(define (slice->bv x)
  (let ((new (make-bytevector (slice-length x))))
    (slice-copy! x (bv-slice/read-write new))
    new))

(define (slice-contents-equal? x y)
  (bytevector=? (slice->bv x)
		(slice->bv y)))

(define (a-equal? a b)
  (let-syntax ((tx (syntax-rules ()
		     ((_ (eq proj) ...)
		      (and (eq (proj a) (proj b))
			   ...)))))
    (tx (= ancillary:protocol)
	(= ancillary:type)
	(slice-contents-equal? ancillary:data))))

(define (al-equal? a b)
  (every a-equal? a b))

(define (av-equal? a b)
  (al-equal? (vector->list a) (vector->list b)))

(if lcov?
    ;; Less tests, so the tests don't take too long to finish.
    (configure-quickcheck
     (stop? (lambda (success-count _)
	      (>= success-count 10)))
     (size (lambda (test-number)
	     (if (zero? test-number) 0
		 (+ 3 (quotient test-number 1))))))
    ;; Likewise
    (configure-quickcheck
     (stop? (lambda (success-count _)
	      (>= success-count 100)))
     (size (lambda (test-number)
	     (if (zero? test-number) 0 ; <-- I don't know what I'm doing
		 (1+ (quotient test-number 6)))))))


;; Generate control data.

(define choose-ancillary-slice-or-bogus
  (generator-let*
   ((len (choose-one/weighted
	  ;; overly small
	  `((1 . ,(choose-integer 0 (@@ (gnu gnunet util cmsg)
					cmsghdr:size)))
	    ;; perfectly aligned
	    (1 . ,(generator-lift
		   (cute * (@@ (gnu gnunet util cmsg) cmsghdr:size) <>)
		   (choose-integer 0 5)))
	    ;; other
	    (1 . ,(choose-integer (@@ (gnu gnunet util cmsg)
				      cmsghdr:size)
				  90)))))
    ;; not very interesting
    (level choose-byte)
    (type choose-byte)
    ;; Apparently len can be shorter
    ;; than the control message and even shorter than the message header,
    ;; see comment in glibc.  (Please do not spread this practice.)
    (padding (choose-one/weighted
	      `((3 . ,(generator-return 0))
		(1 . ,(choose-integer (- len) 17)))))
    ;; ! there is no guarantee padding bytes will be zero.
    (padding-bytes (choose-bytevector (max padding 0))))
   (let* ((bv (make-bytevector (+ len (max padding 0))))
	  (header (make-bytevector (@@ (gnu gnunet util cmsg)
				       cmsghdr:size))))
     ;; ^ on some architectures, this may already contain some padding
     ;; zero bytes at the end due to alignment.  These will be overwritten later.
     (let-syntax ((set (syntax-rules ()
			 ((_ field val)
			  (bytestructure-set!* header 0
					       (@@ (gnu gnunet util cmsg)
						   cmsghdr)
					       'field val)))))
       (set len len)
       (set level level)
       (set type type))
     (bytevector-copy! header 0
		       bv 0
		       (min (bytevector-length header)
			    (bytevector-length bv)))
     (if (<= 0 padding)
	 (bytevector-copy! padding-bytes 0
			   bv len
			   (bytevector-length padding-bytes)))
     (generator-return (bv-slice/read-write bv 0 (+ len padding))))))

;; Append multiple ancillary message slices into a single
;; control data

(define choose-control-data-bv
  (sized-generator
   (lambda (n-parts)
     (generator-lift (lambda (parts)
		       (receive (port get-bv)
			   (open-bytevector-output-port)
			 (for-each (lambda (part)
				     (put-bytevector port
						     (slice-bv part)
						     (slice-offset part)
						     (slice-length part)))
			   parts)
			 (get-bv)))
		     (choose-list choose-ancillary-slice-or-bogus n-parts)))))

(define choose-control-data
  (generator-lift (compose slice/read-only bv-slice/read-write)
		  choose-control-data-bv))

(define $control-data
  (arbitrary
   (gen choose-control-data)
   (xform (lambda _ (throw 'oops)))))

(define choose-slice/read-only
  (generator-lift (compose slice/read-only bv-slice/read-write)
		  (sized-generator choose-bytevector)))

(define $ancillary
  (arbitrary
   (gen (generator-lift make-ancillary
			(choose-integer 0 65535)
			(choose-integer 0 65535)
			choose-slice/read-only))
   (xform #f)))


;; Tests
;; Overview:
;;  * count-ancillaries is a morphism
;;  * control->ancillary-list & control->ancillary-vector
;;    only differ in typing
;;  * FAILS
;;    control->ancillary-vector after ancillary-vector->bytevector
;;    is identity (up to freshness, aside from bv -> slice mapping)
;; * split-ancillary works as expected on a single, whole ancillary
;; * align-len (private) satisties many nice properties
;;   (idempotence, some kind of morphism, monotonity,
;;   an alternative definition ...)

(define (call-with-maximum proc)
  (let ((n -1))
    (proc (lambda (x)
	    (set! n (max x n))))
    n))

(define-syntax-rule (with-maximum increment body body* ...)
  (call-with-maximum
   (lambda (increment) body body* ...)))

(define-syntax-rule (false-if-assertion exp exp* ...)
  (with-exception-handler
      (lambda (e) #f)
    (lambda () exp exp* ...)
    #:unwind? #t
    #:unwind-for-type &assertion))

(define (t)

  ;; Make sure we generate a few ancillary messages
  ;; and not just some random bytevectors.
  ;; (disabled as it is nondeterministic).

  #;
  (test-assert "test case generator is not horribly broken"
  (> (with-maximum consider
  (quickcheck
  (property ((cd $control-data))
  (consider (count-ancillaries cd))
  #t)))
  2))

  
  ;; Verify count-ancillaries is a morphism,
  ;; and control->ancillary-list & control->ancillary-vector and
  ;; are more or less the same.
  (test-assert "[prop] count-ancillaries & control->ancillary-list"
    (quickcheck
     (property ((cd $control-data))
       (false-if-assertion
	(= (count-ancillaries cd)
	   (length (control->ancillary-list cd)))))))

  (test-assert "[prop] count-ancillaries & control->ancillary-vector"
    (quickcheck
     (property ((cd $control-data))
       (false-if-assertion
	(= (count-ancillaries cd)
	   (vector-length (control->ancillary-vector cd)))))))

  (test-assert "[prop] control->ancillary-list & vector->list"
    (quickcheck
     (property ((cd $control-data))
       (false-if-assertion
	(al-equal? (control->ancillary-list cd)
		   (vector->list (control->ancillary-vector cd)))))))

  ;; ancillaries->bytevector & control->ancillary-list
  (test-assert "[prop] control->ancillary-vector after ancillary-vector->bytevector"
    (quickcheck
     (property ((acv ($vector $ancillary)))
       (false-if-assertion
	(av-equal? acv
		   (control->ancillary-vector
		    (slice/read-only
		     (bv-slice/read-write
		      (ancillary-vector->bytevector acv)))))))))

  (test-assert "[prop] split-ancillary on whole ancillary"
    (quickcheck
     (property ((ac $ancillary))
       (false-if-assertion
	(receive (protocol type slice rest)
            (split-ancillary (bv-slice/read-write
			      (ancillary-vector->bytevector (vector ac))))
          (and (= (slice-length rest) 0)
               (slice-readable? rest)
               (a-equal? (make-ancillary protocol type slice) ac)))))))

  (define-syntax-rule (case-values exp case ...)
    (call-with-values (lambda () exp)
      (case-lambda case ...)))


  
  ;; Verify the alignment function works as expected.
  (define align-len (@@ (gnu gnunet util cmsg) align-len))
  (define (aligned? n)
    (= (align-len n) n))

  (test-assert "0 is aligned" (aligned? 0))
  (test-assert "size_t is aligned"
    (aligned? (bytestructure-descriptor-size size_t)))
  (test-assert "[prop] multiples of aligned data are aligned"
    (quickcheck
     (property ((n $natural)
		(m $natural))
       (aligned? (* n (align-len m))))))
  (test-assert "[prop] aligned -> positive"
    (quickcheck
     (property ((n $natural))
       (<= 0 (align-len n)))))
  (test-assert "[prop] aligning is monotonuous"
    (quickcheck
     (property ((n $natural)
		(delta $natural))
       (<= (align-len n)
	   (align-len (+ n delta))))))
  (test-assert "[prop] aligned > unaligned"
    (quickcheck
     (property ((n $natural))
       (<= n (align-len n)))))
  (test-assert "[prop] align-len is idempotent"
    (quickcheck
     (property ((n $natural))
       (= (align-len (align-len n)) (align-len n)))))
  (test-assert "[prop] align-len & addition (one part aligned)"
    (quickcheck
     (property ((n $natural)
		(m $natural))
       (let ((n (align-len n)))
	 (= (align-len (+ n m))
	    (+ n (align-len m)))))))
  (test-assert "[prop] align-len in terms of modulo, + and min"
    (let ((s (bytestructure-descriptor-size size_t)))
      (quickcheck
       (property ((n $natural))
	 (= (align-len n)
	    (let ((m (modulo n s)))
	      (if (= m 0)
		  n ; <-- already aligned
		  (+ s (- n m)))))))))

  
  ;; control-size is well-behaving
  (test-assert "[prop] control-size length is aligned"
    (quickcheck
     (property ((s ($list $natural)))
       (aligned? (apply control-size s)))))

  (test-equal "control-size of empty list"
    0
    (control-size))

  (test-assert "[prop] control-size is a morphism (append & +)"
    (quickcheck
     (property ((n ($list ($list $natural))))
       (= (apply control-size (apply append n))
	  (apply + (map (lambda (l) (apply control-size l)) n))))))

  ;; control-size is sufficient
  (test-assert "[prop] length of ancillary->bytevector is control-size"
    (quickcheck
     (property ((ac $ancillary))
       (let* ((bv (ancillary-vector->bytevector (vector ac)))
	      (bv-len (bytevector-length bv)))
	 (= bv-len (control-size (slice-length (ancillary:data ac))))))))

  (test-assert "[prop] data written by write-ancillary->control! is control-size"
    (quickcheck
     (property ((ac $ancillary))
       (let ((dest (make-slice/read-write
		    (control-size (slice-length (ancillary:data ac))))))
	 (case-values
	  (write-ancillary->control! dest ac)
	  (() #f) ; <-- there should be plenty of space
	  ((n) (= n (slice-length dest))))))))

  (test-assert "[prop] ... even if more bytes are writable"
    (quickcheck
     (property ((ac $ancillary)
		(extra $byte))
       (let ((dest (make-slice/read-write
		    (control-size (slice-length (ancillary:data ac))
				  (floor/ extra 4)))))
	 (case-values
	  (write-ancillary->control! dest ac)
	  (() #f) ; <-- there should be plenty of space (too much, actually)
	  ((n) (= n (control-size (slice-length (ancillary:data ac))))))))))

  
  ;; control-size is required
  (test-assert "[prop] write-ancillary->control! fails when too little space (incl. unaligned)"
    (quickcheck
     (property ((ac $ancillary)
		(less $byte))
       (let* ((bv (ancillary-vector->bytevector (vector ac)))
	      (plenty-of-space (bytevector-length bv))
	      (less (floor/ less 16)) ; Otherwise we see ‘Gave up! Passed only 1 est’.
	      (too-small (slice/write-only
			  (make-slice/read-write
			   (max 0 (min (- plenty-of-space 1) less))))))
	 (test-when (< less plenty-of-space)
		    (case-values
		     (write-ancillary->control! too-small ac)
		     (() #t)
		     ((n) #f)))))))

  (test-assert "[prop] write-ancillary-vector->control! fails when too little space is passed"
    (quickcheck
     (property ((ac ($vector $ancillary))
		(less $byte))
       (let* ((bv (ancillary-vector->bytevector ac))
	      (plenty-of-space (bytevector-length bv))
	      (less (floor/ less 16)) ; Otherwise we see ‘Gave up! Passed only 1 est’.
	      (too-small (slice/write-only
			  (make-slice/read-write
			   (max 0 (min (- plenty-of-space 1) less))))))
	 (test-when (< less plenty-of-space)
		    (with-exception-handler
			(lambda (e) #t)
		      (lambda ()
			(write-ancillary-vector->control! too-small ac)
			#f)
		      #:unwind? #t
		      #:unwind-for-type &control-data-too-small)))))))

(use-modules (system vm coverage))

(if lcov?
    (call-with-values (lambda () (with-code-coverage t))
      (lambda (data)
	(let ((port (open-output-file "lcov.info")))
	  (coverage-data->lcov data port)
	  (close port))))
    (t))