shttpd/sHT/logic/failbit.h

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

#ifndef _sHT_FAILBIT_H
#define _sHT_FAILBIT_H

#include <stddef.h>
#include <sHT/test.h>

/* See doc/failbit.rst */

/* TODO: on-demand: only size_t is supported
   TODO: _Generic instead of type arguments  */

/* TODO: Sparse */
#define sHT_with_failbit

#define sHT_failbit_limit (((size_t) -1) ^ ((size_t) -1) >> 1)
#ifndef __FRAMAC__
_Static_assert(sHT_failbit_limit != 0, "above macro incorrect");
_Static_assert((sHT_failbit_limit & (sHT_failbit_limit - 1)) == 0, "above macro incorrect");
_Static_assert(sHT_failbit_limit << 1 == 0u, "above macro incorrect");
#else
#  include <stdint.h>
#endif

/* SMT provers seem to handle arithmetic better than bitwise
   operations. */
/*@ axiomatic Failbit {
      predicate good(ℤ v) = 0 <= v < sHT_failbit_limit;
      predicate bad(ℤ v) = sHT_failbit_limit <= v <= SIZE_MAX;

      lemma msb_bad: \forall ℤ v; bad(v) ==> v & sHT_failbit_limit;
      lemma nomsb_good: \forall ℤ v; good(v) ==> !(v & sHT_failbit_limit);

      lemma notgood_bad: \forall ℤ v; 0 <= v <= SIZE_MAX ==> (!good(v) ==> bad(v));
      lemma notbad_good: \forall ℤ v; 0 <= v <= SIZE_MAX ==> (!bad(v) ==> good(v));

      lemma failbit_range: \forall ℤ v; good(v) || bad(v) <==> 0 <= v <= SIZE_MAX;

      // ACSL doesn't seem to allow for subtypes
      logic ℤ fail_value(ℤ v);
      axiom good_value: \forall ℤ v; good(v) ==> fail_value(v) == v;
      axiom bad_value:
        \forall ℤ v; bad(v) ==> fail_value(v) == v - sHT_failbit_limit;

      lemma good_value0: \forall ℤ v; good(v) || bad(v)
          ==> fail_value(v) == (v & ~sHT_failbit_limit);
    } */

/* no-failure? */
/*@ terminates \true;
    assigns \result \from x;
    ensures resultNS: \result <==> good(x); */
__attribute__((const))
__attribute__((always_inline))
static inline _Bool
sHT_good(size_t x)
{
	return sHT_msb_unset_size_t(x);
}

/* failure? */
/*@ terminates \true;
    assigns \result \from x;
    ensures resultNS: \result <==> bad(x); */
__attribute__((const))
__attribute__((always_inline))
static inline _Bool
sHT_bad(size_t x)
{
	return sHT_msb_set_size_t(x);
}

/** Start the failbit machine in the success state */
/*@ requires r: x < sHT_failbit_limit;
    terminates \true;
    assigns \result \from x;
    ensures good: good(\result);
    ensures val: fail_value(\result) == x; */
static inline size_t
sHT_success(size_t x)
{
#	define sHT_success_const(x) ((x) + 0)
	return x;
}

/** Start the failbit machine in the error state */
/*@ requires r: x < sHT_failbit_limit;
    terminates \true;
    assigns \result \from x;
    ensures bad: !good(\result);
    ensures val: fail_value(\result) == x; */
static inline size_t
sHT_fail(size_t x)
{
#	define sHT_fail_const(x) ((x) + sHT_failbit_limit)
	return x + sHT_failbit_limit;
}

/*@ terminates \true;
    assigns \result \from x;
    ensures \result == fail_value(x); */
static inline size_t
sHT_fail_value(size_t x)
{
	return x & ~sHT_failbit_limit;
}

/* Transfer the failbit of `f` to `n`, with some restrictions. */
/*@ requires zero: fail_value(from) == 0;
    requires clean: to < sHT_failbit_limit;
    terminates \true;
    assigns \result \from from, to;
    ensures good: good(\result) <==> good(from);
    ensures val: fail_value(\result) == fail_value(to); */
static inline size_t
sHT_transfer_failbit_novalue(size_t from, size_t to)
{
	return from + to;
}

/** Fail machine `m` if `c` */
/*@ requires m_rw: \valid(m);
    requires m_s: \initialized(m);
    terminates \true;
    assigns *m \from \old(*m), r;
    ensures good: good(*m) <==> good(\old(*m)) && !r;
    ensures val: fail_value(*m) == fail_value(\old(*m)); */
__attribute__((always_inline))
static inline void
sHT_fail_if(size_t *m, _Bool r)
{
	/* TODO: this requires checking the machine code
	   for branches! */
	*m |= r ? sHT_failbit_limit : 0;
}

#endif