shttpd/sHT/logic/arithmetic.h

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

#ifndef _sHT_LOGIC_ARITHMETIC
#define _sHT_LOGIC_ARITHMETIC

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

/** Non-overflowing integer multiply-add */
/*@ requires NS ==> a * b + c <= UINT32_MAX;
    terminates \true;
    assigns \result \from a, b, c;
    ensures NS ==> \result == a * b + c; */
static inline uint32_t
sHT_muladd_nooverflowNS_u32(uint32_t a, uint32_t b, uint32_t c)
{
	return a * b + c;
}

/** 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 ⊂ ℕ)

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

  Invariant:
  - failvalue(*m)

  Ensures:
  - good(*m) := good(old *m) ^ (a * b + c ∈ \bounds(T))
  - ret = a * b + c */
#define sHT_muladd_overflow(T, 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), __builtin_mul_overflow((a), (b), (ret))); \
		sHT_fail_if((m), __builtin_add_overflow(*(ret), (c), (ret))); \
	} while (0)

#endif