shttpd/sHT/logic/arithmetic.h

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

#ifndef _sHT_LOGIC_ARITHMETIC
#define _sHT_LOGIC_ARITHMETIC

#include <sHT/logic/failbit.h>

/** The variable really is in ℕ (for proofs), but
  the range supported by the computer is limited.

  The actual value the code sees may wrap-around,
  so that must always be checked -- with the following
  functions. */
#define sHT_overflowing

/** Calculate a * b + c, tracking overflow

  (a, b, c : T, ret : T *, T ⊂ ℕ, M ∈ { uintN_t | N })

  Requires:
  - good(M, *m) <-> { a, b, c } ⊂ \bounds(T)
  - (read ^ write) (*ret)
  - (read ^ write ^ set) (*mask)

  Invariant:
  - failvalue(M, *m)

  Ensures:
  - good(M, *m) := good(M, old *m) ^ (a * b + c ∈ \bounds(T))
  - ret = a * b + c */
#define sHT_muladd_overflow(T, M, ret, a, b, c, m) \
	do { \
		/* Computation is correct, failure is always maintained,
		  a, b and c are non-negative so failure is set on overflow. */ \
		sHT_fail_if(M, (m), __builtin_mul_overflow((a), (b), (ret))); \
		sHT_fail_if(M, (m), __builtin_add_overflow(*(ret), (c), (ret))); \
	} while (0)

#endif