diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/cobs.c | 115 | ||||
| -rw-r--r-- | src/noise.c | 2 | ||||
| -rw-r--r-- | src/packet_interface.c | 20 |
3 files changed, 112 insertions, 25 deletions
@@ -213,20 +213,66 @@ void cobs_decode_incremental_initialize(struct cobs_decode_state *state) { state->c = 0; } -int cobs_decode_incremental(struct cobs_decode_state *state, char *dst, size_t dstlen, char src) { +/*@ requires \separated(state, dst + (0..dstlen-1)); + requires \valid(state); + requires \valid(dst + (0..dstlen-1)); + requires 0 < dstlen <= 65535; + requires 0 <= state->p <= dstlen+1; + requires state->p != 0 ==> 1 <= state->c <= 255; + + ensures state->p != 0 ==> 1 <= state->c <= 255; + ensures 0 <= state->p <= dstlen+1; + ensures 0 <= \result <= dstlen || \result \in {-1, -2, -3, -4}; + ensures \result < -1 ==> state->p == 0 && state->c == 0; + assigns *state, dst[0..dstlen-1]; + + behavior eof_bad_empty_frame: + assumes state->p == 0 && src == 0; + ensures \result == -3; + assigns *state; + + behavior eof_good_frame: + assumes state->p != 0 && src == 0; + ensures \result >= 0 || \result == -2; + assigns *state; + + behavior decoding_no_overflow: + assumes src != 0 && state->p <= dstlen; + ensures \result == -1; + assigns *state, dst[0..dstlen-1]; + + behavior decoding_overflow: + assumes src != 0 && state->p > dstlen; + ensures \result == -4; + assigns *state; + + complete behaviors; + disjoint behaviors; + @*/ +int cobs_decode_incremental(struct cobs_decode_state *state, unsigned char *dst, size_t dstlen, unsigned char src) { if (state->p == 0) { - if (src == 0) - goto empty_errout; /* invalid framing. An empty frame would be [...] 00 01 00, not [...] 00 00 */ - state->c = (unsigned char)src; + if (src == 0) { + /* invalid framing. An empty frame would be [...] 00 01 00, not [...] 00 00 */ + cobs_decode_incremental_initialize(state); + //@ assert 0 <= state->p <= dstlen; + return -3; + } + state->c = src; state->p++; - return 0; + //@ assert 0 <= state->p <= dstlen; + return -1; } if (!src) { - if (state->c != 1) - goto errout; /* Invalid framing. The skip counter does not hit the end of the frame. */ - int rv = state->p-1; + if (state->c != 1) { + /* Invalid framing. The skip counter does not hit the end of the frame. */ + cobs_decode_incremental_initialize(state); + //@ assert 0 <= state->p <= dstlen; + return -2; + } + size_t rv = state->p-1; cobs_decode_incremental_initialize(state); + //@ assert 0 <= state->p <= dstlen; return rv; } @@ -234,26 +280,59 @@ int cobs_decode_incremental(struct cobs_decode_state *state, char *dst, size_t d state->c--; if (state->c == 0) { - state->c = (unsigned char)src; + state->c = src; val = 0; } else { val = src; } size_t pos = state->p-1; - if (pos >= dstlen) - return -2; /* output buffer too small */ + if (pos >= dstlen) { + cobs_decode_incremental_initialize(state); + //@ assert 0 <= state->p <= dstlen+1; + return -4; /* output buffer too small */ + } dst[pos] = val; + //@ assert 0 <= state->p <= dstlen; state->p++; - return 0; - -errout: - cobs_decode_incremental_initialize(state); + //@ assert 0 <= state->p <= dstlen+1; return -1; +} + +/*@ requires \valid_read(buf + (0..len-1)); + assigns \nothing; + @*/ +void handle_packet(unsigned char *buf, size_t len); -empty_errout: - cobs_decode_incremental_initialize(state); - return -3; +/*@ requires \valid(dst + (0..dstlen-1)); + requires \valid_read(src + (0..srclen-1)); + requires 0 < dstlen <= 65535; + assigns dst[0..dstlen-1]; + @*/ +void cobs_decode_test(unsigned char *src, size_t srclen, unsigned char *dst, size_t dstlen) { + struct cobs_decode_state state; + cobs_decode_incremental_initialize(&state); + //@ assert state.p == 0; + //@ assert state.c == 0; + //@ assert state.p != 0 ==> 1 <= state.c <= 255; + /*@ loop invariant \separated(&state, dst + (0..dstlen-1), &i); + loop invariant \valid(&state); + loop invariant \valid(dst + (0..dstlen-1)); + loop invariant 0 < dstlen <= 65535; + loop invariant 0 <= state.p <= dstlen+1; + loop invariant state.p != 0 ==> 1 <= state.c <= 255; + loop assigns dst[0..dstlen-1], state, i; + loop variant srclen-i; + @*/ + for (size_t i=0; i<srclen; i++) { + int rv = cobs_decode_incremental(&state, dst, dstlen, src[i]); + if (rv >= 0) + handle_packet(dst, rv); + if (rv == -1) + continue; + if (rv < -1) + continue; + } } #ifdef VALIDATION diff --git a/src/noise.c b/src/noise.c index 890b5b5..949a68d 100644 --- a/src/noise.c +++ b/src/noise.c @@ -199,8 +199,6 @@ void uninit_handshake(struct NoiseState *st, enum handshake_state new_state) { requires \separated(&usart2_out, st, buf, st->handshake, &st->handshake_hash); - assigns key_checked_trace; - ensures (st->handshake_state == HANDSHAKE_DONE_KNOWN_HOST) ==> key_checked_trace == 1; ensures (st->handshake_state != HANDSHAKE_IN_PROGRESS) ==> key_match_trace == 1 || (st->failed_handshakes > \old(st->failed_handshakes)); diff --git a/src/packet_interface.c b/src/packet_interface.c index 441fff9..98a1ef2 100644 --- a/src/packet_interface.c +++ b/src/packet_interface.c @@ -66,17 +66,27 @@ void usart2_isr(void) { } ssize_t rv = cobs_decode_incremental(&host_cobs_state, (char *)host_packet_buf, sizeof(host_packet_buf), data); - if (rv == -2) { - LOG_PRINTF("Host interface COBS packet too large\n"); + if (rv == 0) { + /* good, empty frame */ + LOG_PRINTF("Got empty frame from host\n"); + host_packet_length = -1; + } else if (rv == -1) { + /* Decoding frame, wait for next byte */ + } else if (rv == -2) { + LOG_PRINTF("Host interface COBS framing error\n"); host_packet_length = -1; } else if (rv == -3) { + /* invalid empty frame */ LOG_PRINTF("Got double null byte from host\n"); - } else if (rv < 0) { - LOG_PRINTF("Host interface COBS framing error\n"); + host_packet_length = -1; + } else if (rv == -4) { + /* frame too large */ + LOG_PRINTF("Got too large frame from host\n"); host_packet_length = -1; } else if (rv > 0) { + /* Good, non-empty frame */ host_packet_length = rv; - } /* else just return and wait for next byte */ + } TRACING_CLEAR(TR_HOST_IF_USART_IRQ); } |