shttpd/sHT/lex/findchar.h

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

#ifndef _sHT_LEX_FINDCHAR
#define _sHT_LEX_FINDCHAR

#include <sHT/bitvec.h>
#include <sHT/compiler.h>

#include <stddef.h>
#include <stdint.h>

/* TODO: is uint16_t, uint32_t, uint64_t more interesting?
   (e.g., more noise for attackers) */
typedef uint8_t sHT_charclass_limb;

#define sHT_charclass_n (256u)
#define sHT_charclass_limbs (sHT_charclass_n / 8)

/* Instances are generated by <tools/gen-character-bitvec.py>
   (currently in 'webdav' branch). */
typedef const sHT_charclass_limb sHT_charclass[sHT_charclass_limbs];

/* TODO: and \initialized */
/*@ predicate valid_charclass(sHT_charclass_limb *v)
      = \valid_read(&v[0 .. sHT_charclass_limbs - 1]); */

/*@ axiomatic Charclass {
      predicate in_charclass{L1}(sHT_charclass_limb *v, ℤ i)
        reads v[0 .. sHT_charclass_limbs - 1];
    } */

/** Test a byte is in a set */
/*@ requires valid: valid_charclass(s);
    terminates \true;
    assigns \result \from s[0 .. sHT_charclass_limbs - 1], c;
    ensures rNS: \result <==> in_charclass{Pre}(s, c); */
__attribute__((always_inline))
__attribute__((pure))
static inline _Bool
sHT_charclass_test(sHT_charclass s, uint8_t c)
{
	/* (* precondition satisfied by typing of c
	      (max(c) = 256 = 32 * 8) combined with (a) *) */
	return sHT_bit_test(s, c);
}

/** Find the first byte in a string belonging to a set

    (Starting at `b`, returning `e` on EOF). */
/*@ requires from_r: \valid_read(&from[b .. e - 1]);
    requires from_s: \initialized(&from[b .. e - 1]);
    requires s_valid: valid_charclass(s);
    requires ra: b <= e;
    requires rb: 0 < e;
    assigns \result;
    ensures before_NS: \forall ℤ j; b <= j < \result ==> !in_charclass(s, from[j]);
    ensures after_NS: \result != e ==> in_charclass(s, from[\result]);
    ensures result_rangeNS: b <= \result <= e;
    ensures result_rangeS: \result <= e; */
__attribute__((pure))
size_t
sHT_findchar(size_t e, const uint8_t from[e], size_t b, sHT_charclass s);

#endif