shttpd/sHT/lex/nat.h

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

#ifndef _sHT_LEX_NAT_H
#define _sHT_LEX_NAT_H

#include <limits.h>
#include <stdint.h>

#include <sHT/logic/failbit.h>
#include <sHT/logic/arithmetic.h>

struct sHT_decimal_u32
{
	sHT_with_failbit
	size_t end;
	/* On AMD64 SystemV, the third argument and second return
	  value are mapped to the same register -- no register
	  shuffling is necessary.

	  TODO: ARM, etc. */
	sHT_overflowing
	uint_least32_t val;
};

/** Parse a natural, decimal number

  The first character is skipped,
  the first digit is taken to be `val`.
  On overflow, `sHT_bad(ret.end)`.

  Requires:
  (a): SliceCap(read ^ set, length, from)
  (b): 0 < length < failbit_limit(size_t)
  (c): nonspec: 0 ≤ first < 10

  Definitions:
  - end := maximalise k : { k | 1 ≤ k ≤ length },
      match decimal* from 1 k
  - d (k : nat, 0 ≤ k < end) :=
    match k
    | 0 ⇒ first
    | S _ ⇒ decimal->nat (from [k])
    (* Capability:
      k < end, end < length
      ⇒ (1) k < length

      Satisfied by (a), 0 ≤ k, (1) *)
    end
  - nonspec: value := string->nat end d

  Ensures:
  (w): 0 ≤ fail_value(size_t, ret.end) ≤ length
  (x): nonspec: fail_value(size_t, ret.end) = end
  (y): nonspec: value ∈ \bounds(ret.value) ↔ good(size_t, ret.end)
  (z): value = ret.val */
__attribute__((pure))
struct sHT_decimal_u32
sHT_decimal_u32_c1(size_t length, const unsigned char from[length], uint_least32_t first);

#endif