shttpd/string/setops.c

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

#include <stddef.h>
#include <stdint.h>
#include <sHT/test.h>
#include <sHT/index.h>
#include <sHT/string/setops.h>

#include <string.h>

void
sHT_memcpy16_r2(uint16_t dest[], uint16_t from[], size_t e0, size_t b0, size_t b1)
{
	size_t e1 = b1 + (e0 - b0);
	size_t i0 = b0;
	size_t i1 = b1;
	if (sHT_ge(i0, e0))
		return;
	/*@ loop invariant i0NS: b0 <= i0 < e0;
	    loop invariant i1NS: i1 - i0 == b1 - b0;
	    loop invariant dest_sNS: \initialized(dest + (b0 .. i0 - 1));
	    loop invariant copyINS: memeq16{Here,Here}(dest + b0, from + b1, i0 - b0);
	    // loop assignsS dest[0 .. e0 - 1];
	    loop assigns i0, i1, dest[b0 .. e0 - 1];
	    loop variant e0 - i0; */
	do {	i0 = sHT_index_nospec(i0, e0);
		i1 = sHT_index_nospec(i1, e1);
		dest[i0] = from[i1];
		i0++, i1++;
	} while (sHT_lt(i0, e0));
}

void
sHT_bzero16_r1(uint16_t dest[], size_t e, size_t b)
{
	/* TODO: X86 has a CISC instruction to do approximately this */
	if (sHT_ge(b, e))
		return;
	size_t i = b;
	/*@ loop invariant iNS: b <= i < e;
	    loop invariant zeroINS: bzero16{Here}(dest + b, i - b);
	    // loop assigns dest[0 .. e - 1]
	    loop assigns i, dest[b .. e - 1];
	    loop variant e - i; */
	do {	dest[i = sHT_index_nospec(i, e)] = 0;
		i++;
	} while (sHT_lt(i, e));
}