shttpd/sHT/logic/failbit.h

// SPDX-License-Identifier: GPL-3.0-or-later
// Copyright © 2019 Ariadne Devos

#ifndef _sHT_FAILBIT_H
#define _sHT_FAILBIT_H

#include <sHT/test.h>

/* See doc/failbit.rst */

/* TODO: Sparse */
#define sHT_with_failbit

#define _sHT_failbit(T) (((T) -1) ^ ((T) -1) >> 1)
_Static_assert(_sHT_failbit(unsigned) != 0, "above macro incorrect");
_Static_assert((_sHT_failbit(unsigned) & (_sHT_failbit(unsigned) - 1u)) == 0, "above macro incorrect");
_Static_assert(_sHT_failbit(unsigned) << 1 == 0u, "above macro incorrect");

/** no-failure-p?

  Ensures:
  (z): nonspec: ret ↔ good(T, x) */
#define sHT_good(T, x) (sHT_and_none((x), _sHT_failbit(T)))

/** failure-p?

  Ensures:
  (z): nonspec: ret ↔ ¬good(T, x) */
#define sHT_bad(T, x) sHT_lt0(x)

/** Start the failbit machine in the success state

  Requires:
  (a): failbit_clean(T, x)

  Ensures:
  (y): good(T, ret)
  (z): fail_value(T, ret) = x */
#define sHT_success(T, x) (x)

/** Start the failbit machine in the error state
  Requires:
  (a): failbit_clean(T, x)

  Ensures:
  (y): ¬good(T, ret)
  (z): fail_value(T, ret) = x */
#define sHT_fail(T, x) ((x) | _sHT_failbit(T))

/** Fail machine `f` if `c`

  Requires:
  (a): (read ∧ write ∧ set) (*f)

  Invariant:
  (p): fail_value(T, *f)

  Ensures:
  (z): good(T, new *f) ↔ good(T, old *f) ∧ ¬c */
#define sHT_fail_if(T, f, c) \
	do { \
		*(f) |= (c) ? _sHT_failbit(T) : 0; \
	} while (0)

/** Ensures: (z): ret = fail_value(T, f) */
#define sHT_fail_value(T, f) ((f) & ~_sHT_failbit(T))

/** type T, 2 ** (log2(\max(T)) - 1) (see sHT_failbit_clean) */
#define sHT_failbit_limit(T) (_sHT_failbit(T))

/* (not supposed to be used by code, yet) */
/** ∀i : ℕ, 0 ≤ i < failbit_limit(T) ↔ failbit_clean(T, i) */
#define sHT_failbit_clean(T, x) /* !((x) & _sHT_failbit(T)) */

/* Transfer the failbit of `f` to `n`, with some restrictions.

  Requires:
  (a): fail_value(T, f) = 0
  (b): failbit_clean(T, n)
    (required, as `n`'s msb may not leak into good(T, ret))

  Ensures:
  (y): good(T, ret) ↔ good(T, f)
  (z): fail_value(T, ret) = n */
#define sHT_transfer_failure_novalue(T, f, n) ((f) | (n))

#endif