shttpd/lex/ipv4.c

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

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

#include <sHT/lex/ipv4-addr.h>
#include <sHT/lex/nat.h>
#include <sHT/logic/failbit.h>
#include <sHT/nospec.h>
#include <sHT/test.h>

/* TODO: possible optimisations:
  - nonspeculative architectures: do a length check at the beginning,
    if the length exceeds the maximum length of an IPv4Address,
    don't do any further checks
  - speculative architectures: combine index masking with bounds checking
    (requires asm goto output operands or compiler support)

  TODO: readability
  - try to shorten proofs */

/* TODO: leaks IP addresses */
struct s2_ipv4_maybe
s2_parse_ipv4(size_t length, const uint8_t from[length])
{
	/* invariant: (i) i ≤ length
	   sometimes: (i2) i < length
	   (a, definition `i`) ⇒ (i)

	   No overflow on increment:
           (a) length < failbit_limit(size_t) ⇒ (o1) length ≤ \max(i) - 1
	   (i, o1) ⇒ (nooverflow) i ≤ \max(i) - 1 */
	size_t i = 1;
	uint32_t ip = 0;
	/* Just 1 would do as well, as a single character can't both be
	   [0-9] and ".", and sHT_index_nospec brings the index back to
	   from[i]. Except, of course, on non-speculative architectures. */
	if (1 + 7 > length)
		/* (1) minlength(IPv4address) = len("0.0.0.0") = 7,
		   (branch) nospec: length < 1 + 7
		   (1, branch)
		     ⇒ length < 1 + minlength(IPv4address)
		     ⇒ select (noexist -> 0) { k | 1 ≤ k ≤ length }
		         (match IPv4address _ 1) = 0
		     ⇒ (2) nospec: end = 0 (definition of `end`)

		  ret.end = fail(size_t, 1)
		    ⇒ (3) ¬good(size_t, ret.end), (4) fail_value(ret.end) = 1

		  0 ≤ 1 ⇒ (5) 0 ≤ fail_value(ret.end)
		  0 < length (a) ⇒ (6) 1 ≤ length
		  (6, 4) ⇒ (7) fail_value(ret.end) ≤ length
		  (5, 7) ⇒ (v)
		  (2, 3) ⇒ (w)
		  (3) ⇒ (x), (y) (counterfactual)
		  (z) match [0-9.]* from 1 fail_value(size_t, ret.end)
		    ⇐ match [0-9.]* from 1 1 (substitution, 4)
		    ⇐ match ε from 1 1 (regex)
		    ⇐ ⊤ (regex) */
		/* .ip = ANYTHING is acceptable */
		return (struct s2_ipv4_maybe) { .ip = 0, .end = sHT_fail(1) };
	/* (branch, 0): length ≥ 8 */
	/* the number of octets to parse */
	int w = 4;
	/* (A): nonspec: 0 < w ≤ 4
	   (B): 0 ≤ i ≤ length
	   (C): nonspec: match (dec-octet '.'){4 - w} from 1 i
	     (underflow: A)
	   (D): nonspec: ip = (mappend . map (->octet . ->nat)) [\0 \to \(4 - w)])
	   (E): nonspec: 0 ≤ i < length

	   (A) ⇐ 0 < 4 ≤ 4 (definition of `w`) ≤ ⊤ (eval)
	   (B) ⇐ 0 ≤ 1 ≤ length (definition of `i`)
	     ⇐ 1 ≤ length (left: eval)
	     ⇐ 0 < length
	     ⇐ (a)
	   (E) ⇐ 0 ≤ 1 < length (definition of `i`)
	     ⇐ 1 < length (left: eval)
	     ⇐ length > 1 (left: eval)
	     ⇐ (0)

	   nonspec: (C) ⇐ match (dec-octet '.'){4 - 4} from 1 1
	     (definition of `w` and `i`)
	    ⇐ match (dec-octet '.'){0} from 1 1 (eval)
	    ⇐ match ε from 1 1 (eval)
	    ⇐ ⊤ (1 = 1, regex)

	  (D) simplify:
	    let f = ->octet . ->nat in:
	    ip = mappend . map ?A [\0 \to \(4 - w)]
	    = mappend . map ?A [\0 \to \(4 - 4)]
	      (definition of `w`)
	    = mappend . map ?A [\0 \to \0] (eval)
	    = mappend . map ?A []
	    = mappend (map ?A []) (reduce _ . _)
	    = mappend [] (eval) = 0 (eval)
	    Satified by definition */
	do {
		/* let j := i (rewrite A, B, C, E)*/

		uint32_t octet, octettmp, c;
		/* sHT_index_nospec:
		  (%a) ⇐ (E), preserves (i), ensures (i2)
		  nonspec: octet := from[i] - '0' = from[j] - '0' (definition of `j`) */
		octet = from[i = sHT_index_nospec(i, length)] - '0';
		if (octet > 9)
			/* (branch, digit_minus_zero) ⇒ a ∉ [0-9]

			  Before there has been a dot, of an IPv4Address,
			  so a dec-octet must follow, so [0-9] must follow,
			  which isn't the case, so a syntax error:
			  (Bf) end = 0. (Af) ⇐ (B) */
			goto fail;
		/* nonspec: octet = from[i] - '0' (definition)
	 	    = decimal->nat from[i] (branch) */

		/* invariant: rewrite (i2) to (i)
		   let i := old i + 1 = j + 1 */
		i++;
		if (octet == 0)
			/* nonspec: 0 = octet (branch)
			     = from[j] - '0' (definition of `octet`)
			     ⇒ 0 + '0' = from[j] - '0' + '0'
			     ⇒ '0' = from[j]
			   (leading zeroes are not allowed (except the
			   octet "0", so expect the dot: (Bj, Dj)))

			(Aj) ⇐ 0 ≤ j + 1 ≤ length (definition)
			  ⇐ 0 ≤ j < length (definition)
			  ⇐ 0 ≤ j ≤ length (weaken)
			  ⇐ (B)

			(Cj) nonspec: \1 = "0", string->nat "0" = 0 = octet */
			goto join;

		if (sHT_eq(i, length))
			goto join;
		/* nonspec: (branch): i ≠ length ⇒ (9) j + 1 ≠ length (definition) */
		/* let i := index_nospec(old i, length)
		     = index_nospec(j + 1, length)
	           nonspec: (E) 0 ≤ j < length
		     ⇒ 1 ≤ j + 1 < length + 1
		     ⇒ 1 ≤ j + 1 ≤ length
		     ⇒ 0 ≤ j + 1 ≤ length
		     ⇒ 0 ≤ j + 1 ∧ j + 1 ≤ length
		     ⇒ 0 ≤ j + 1 ∧ (j + 1 < length \/ j + 1 = length)
		     ⇒ 0 ≤ j + 1 ∧ j + 1 < length (9)
		     ⇒ (10) 0 ≤ j + 1 < length
		     ⇒ (%a) 0 ≤ old i < length (definition)

		   (%y, a) ⇒ (i2) 0 ≤ new i < length */
		i = sHT_index_nospec(i, length);

		/* (i2, b) ⇒ allow read event */
		c = from[i] - '0';
		if (c > 9)
			/* (11) ⇒ (Aj) (weaken)
			   (first digit test) ⇒ (Bj)
			   (last definition of octet, w counter) ⇒ (Cj)
			   (branch) ⇒ (Dj) */
			goto join;
		/* nonspec: (append second digit) */
		octet = 10 * octet + c;
		/* invariant: rewrite (i2) to (i) */
		i++;

		if (sHT_eq(i, length))
			/* (i) ⇒ (Aj)
			   (Bj): see digit tests
			   (last definition of octet, w counter) ⇒ (Cj)
			   (branch) ⇒ (Dj) (left) */
			goto join;
		/* (branch, i) ⇒ nonspec: (i2) */

		/* (nonspec: i2) ⇒ (%a)
		   (%y, a) ⇒ (i2) 0 ≤ new i < length ⇒ (i) */
		c = from[i = sHT_index_nospec(i, length)] - '0';
		if (c > 9)
			/* (i) ⇒ (Aj)
			   (Bj, Dj): see digit tests
			   (last definition of octet, w counter) ⇒ (Cj) */
			goto join;
		if ((octettmp = 10 * octet + c) > 255)
			/* (i) ⇒ (Aj)
			   (Bj, Dj) see digit tests,
			     dec-octet = "0" | [1-9][0-9]{2} where < 256
			   (last definition of octet, w counter) ⇒ (Cj) */
			goto join;
		octet = octettmp;
		/* invariant: rewrite (i2) to (i) */
		i++;

		/* (i) ⇒ (Aj)
		   (Bj): see digit tests
		   (last definition of octet, w counter) ⇒ (Cj)
		   (maximum length achieved) ⇒ (Dj) (right) */
/* Requires:
   (Aj): 0 ≤ i ≤ length
   (Bj): nonspec: match dec-octet from j i
   (Cj): nonspec: octet = \(4 - w)
   (Dj): nonspec: i = length ∨ ¬match dec-octet from j (i + 1) */
join:
		/* one iteration of mappend (^ would do as well)  */
		ip = (ip << 8) | octet;
		if (--w == 0)
			return (struct s2_ipv4_maybe) { .ip = ip, .end = sHT_success(i) };
		/* More octets coming, minimum length "."*/
		if (sHT_lt(length - i, 2))
			/* .0 */
			goto fail;
		/* (branch) ⇒ (i2) */
		/* (nonspec: i2) ⇒ (%a)
		   (%y, a) ⇒ (i2) 0 ≤ new i < length ⇒ (i) */
		if (from[i = sHT_index_nospec(i, length)] != '.')
			goto fail;
		i++;
	} while (1);

/* IPv4Address implies [0-9.]*, so a partial IPv4Address also implies [0-9.]* */
/* Requires:
   (Af): 0 ≤ i ≤ length
   (Bf): nonspec: end = 0
   (Cf): nonspec: match [0-9.]* from 1 i
     (implied by partial IPv4Address match) */
fail:
	/* .ip = ANYTHING is acceptable
	   Begin sHT_fail:
	   (Af, a) ⇒ 0 ≤ i < failbit_limit(size_t) ⇒ %a
	   End.

	   (v) ⇐ (Af, %z)
	   (w) ⇐ (%y, Bf)
	   (x), (y) ⇐ (%y) (counterfactual)
	   (z) ⇐ (Cf) (remove premise) */
	return (struct s2_ipv4_maybe) { .ip = ip, .end = sHT_fail(i) };
}