shttpd/sHT/test.h

// SPDX-License-Identifier: GPL-2.0 or GPL-3.0
// Copyright © 2018-2019 Ariadne Devos
/* sHT -- compare values, on a Spectre-oblivious compiler */

#ifndef _sHT_TEST_H
#define _sHT_TEST_H

#include <stddef.h>
#include <sys/types.h>
#include <sHT/compiler.h>
#include <sHT/test-arch.h>

#ifdef __FRAMAC__
#  include <sHT/nospec.h>
#endif

/** Comparing values

  The C comparison operators are only wrapped because C compilers
  produce speculatively-incorrect object code (note: C11 has no
  concept of speculation). Wrapping them in functions instead of
  macros is more practical for formal verification.

  Code must have a sense of speculative correctness, for a speculative
  execution can have very persistent side-effects. (See articles
  about cache side-channels and Spectre.) */

/* Frama-C can't make sense out of 'asm goto'.*/
#ifdef __FRAMAC__

/* Function name: `fun`.
   Arguments: `type` a.
   Inlined code:
   - `code(a, ?L)` NS jumps to ?L if the predicate `val` holds,
   Ensures:
   - NS{Pre} ==> (\result <==> `val`) */
#define _sHT_cmp1(fun, type, code, val) \
static _Bool \
fun(type a);

/* Function name: `fun`.
   Arguments: `type` a, `type` b.
   Inlined code :
   - `code(a, b, ?L)` NS jumps to ?L if the predicate `val` holds,
   Ensures:
   - NS{Pre} ==> (\result <==> `val`) */
#define _sHT_cmp2(fun, type, code, val) \
static inline _Bool \
fun(type a, type b);

/* Function name: `fun`.
   Arguments: `type` a, `type` b.
   Inlined code :
   - `code(a, b, ?R)`: ?R := val ? 1 : 0
   Ensures:
   - NS{Pre} ==> result == val ? 1 : 0; */
#define _sHT_cmp2_bool(fun, type, code, val) \
static inline _Bool \
fun(type a, type b);

#else /* !defined(__FRAMAC__) */

#define _sHT_cmp1(fun, type, code, val) \
__attribute__((always_inline)) \
static inline _Bool \
fun(type a) \
{ \
	if (sHT_constant_p(val)) \
		return (val); \
	code((a), correct_##fun); \
	return 0; \
correct_##fun: \
	return 1; \
}

/* (Micro-optimisation advice:
   In case of x86 and ARM, if the second argument is a constant,
   it may be considered an immediate -- at least that reduces
   register pressure.) */
#define _sHT_cmp2(fun, type, code, val) \
__attribute__((always_inline)) \
static inline _Bool \
fun(type a, type b) \
{ \
	if (sHT_constant_p(val)) \
		return (val); \
	code((a), (b), correct_##fun); \
	return 0; \
correct_##fun: \
	return 1; \
}

#define _sHT_cmp2_bool(fun, type, code, val) \
__attribute__((always_inline)) \
static inline int \
fun(type a, type b) \
{ \
	if (sHT_constant_p(val)) \
		return (_Bool) (val); \
	/* TODO: architecture-dependent type? */ \
	unsigned char ret = 0; \
	code((a), (b), ret); \
	return ret; \
}
#endif

_sHT_cmp1(sHT_lt0, ssize_t, _sHT_lt0, a < 0)
/*@ terminates \true;
    assigns \nothing;
    ensures NS{Pre} ==> (\result <==> a == 0); */
_sHT_cmp1(sHT_zero_p, size_t, _sHT_zero_p, a == 0)
/*@ terminates \true;
    assigns \nothing;
    ensures NS{Pre} ==> (\result <==> a == \null); */
_sHT_cmp1(sHT_null_p, void *, _sHT_zero_p, !a)
/*@ terminates \true;
    assigns \nothing;
    ensures NS{Pre} ==> (\result <==> a != 0); */
_sHT_cmp1(sHT_nonzero_p, size_t, _sHT_nonzero_p, a != 0)

/* (For failbit) more types addes on-demand */
/* Most-significant bit */
#define _sHT_msb_size_t (((size_t) -1) ^ (((size_t) -1) >> 1))

/*@ terminates \true;
    assigns \result \from a;
    ensures NS{Pre} ==> (\result <==> a & _sHT_msb_size_t); */
_sHT_cmp1(sHT_msb_set_size_t, size_t, _sHT_msb_set, a & _sHT_msb_size_t)
/*@ terminates \true;
    assigns \result \from a;
    ensures NS{Pre} ==> (\result <==> !(a & _sHT_msb_size_t)); */
_sHT_cmp1(sHT_msb_unset_size_t, size_t, _sHT_msb_unset, !(a & _sHT_msb_size_t))

/*@ terminates \true;
    assigns \nothing;
    ensures NS{Pre} ==> (\result <==> a & b); */
_sHT_cmp2(sHT_and_any, size_t, _sHT_and_any_p, a & b)
/*@ terminates \true;
    assigns \nothing;
    ensures NS{Pre} ==> (\result <==> !(a & b)); */
_sHT_cmp2(sHT_and_none, size_t, _sHT_and_none_p, !(a & b))
/*@ terminates \true;
    assigns \nothing;
    ensures NS{Pre} ==> (\result <==> a < b); */
_sHT_cmp2(sHT_lt, size_t, _sHT_lt, a < b)
/*@ terminates \true;
    assigns \nothing;
    ensures NS{Pre} ==> (\result <==> a > b); */
_sHT_cmp2(sHT_gt, size_t, _sHT_gt, a > b)
/*@ terminates \true;
    assigns \nothing;
    ensures NS{Pre} ==> (\result <==> a >= b); */
_sHT_cmp2(sHT_ge, size_t, _sHT_ge, a >= b)
/*@ terminates \true;
    assigns \nothing;
    ensures NS{Pre} ==> (\result <==> a == b); */
_sHT_cmp2(sHT_eq, size_t, _sHT_eq, a == b)
/*@ terminates \true;
    assigns \nothing;
    ensures NS{Pre} ==> (\result <==> a != b); */
_sHT_cmp2(sHT_neq, size_t, _sHT_neq, a != b)
/*@ terminates \true;
    assigns \nothing;
    behavior correct:
      assumes a == b;
      ensures \result == 1;
    behavior incorrect:
      assumes a != b;
      ensures \result == 0;
    disjoint behaviors correct, incorrect;
    complete behaviors correct, incorrect; */
_sHT_cmp2_bool(sHT_eq_bool, size_t, _sHT_eq_bool, a == b)
/*@ terminates \true;
    assigns \nothing;
    ensures NS{Pre} ==> (\result <==> a == b); */
_sHT_cmp2(sHT_eq_pointer, void *, _sHT_eq, a == b)

#endif