make router_options.c compile

_CoqProject

@@ -55,3 +55,4 @@
 -Q _build/default/linux/casestudies/proofs/page_alloc_find_buddy refinedc.linux.casestudies.page_alloc_find_buddy
 -Q _build/default/examples/proofs/pointers refinedc.examples.pointers
 -Q _build/default/linux/casestudies/proofs/pgtable refinedc.linux.casestudies.pgtable
+-Q _build/default/linux/casestudies/proofs/router_options refinedc.linux.casestudies.router_options

linux/casestudies/proofs/router_options/router_options_lemmas.v

+From refinedc.typing Require Import typing.
+
+(* struct, const *)
+
+Record ipv4_header := {
+  version_ihl : Z;
+}.

linux/casestudies/router_options.c

+//@rc::import router_options_lemmas from refinedc.linux.casestudies.router_options
+
+#include <stdint.h>
+#include <stdbool.h>
+#include <refinedc.h>
+
+struct [[rc::refined_by("header : ipv4_header")]] ipv4_hdr {
+    [[rc::field("{version_ihl header} @ int<u8>")]]
+    uint8_t version_ihl; // [7..4] version    [3..0] header length (in int32)
+    // uint8_t type_of_service;
+    // uint16_t total_length;
+    // uint16_t packet_id;
+    // uint16_t fragment_offset;
+    // uint8_t time_to_live;
+    // uint8_t next_proto_id;
+    // uint16_t hdr_checksum;
+    // uint32_t src_addr;
+    // uint32_t dst_addr;
+};
+
+// [[rc::parameters("header : ipv4_header", "ip : Z", "timestamp : Z", "p : loc")]]
+// [[rc::args("p @ &own<header @ ipv4_hdr>", "ip @ int<u32>", "timestamp @ int<u32>")]]
+[[rc::trust_me]]
+bool handle_packet_timestamp(struct ipv4_hdr* header, uint32_t router_ip, uint32_t current_milliseconds_utc)
+{
+    // header length >= 5 * int32
+    uint8_t options_length = (header->version_ihl & 0xF) - 5;
+    // options begin where ipv4_hdr ends
+    uint8_t* options_bytes = (uint8_t*) ((uint32_t*) header + 5);
+    uint8_t options_bytes_count = options_length * 4;
+    // each option consists of its type, length (in bytes) and value (if any)
+    while (options_bytes_count > 0) {
+        // Option type
+        uint8_t opt_type = *options_bytes;
+        options_bytes++;
+
+        if (opt_type == 0) {
+            // End of options
+            break;
+        }
+
+        if (opt_type == 1) {
+            // No-op
+            continue;
+        }
+
+        // Option length (in bytes)
+        uint8_t opt_length = *options_bytes;
+        options_bytes++;
+
+        // We're only interested in the timestamp
+        if (opt_type != 68) {
+            // -2 since we skipped type and length already
+            options_bytes += opt_length - 2;
+            continue;
+        }
+
+        // the current option is timestamp
+        uint8_t timestamp_flag; // to avoid name conflicts among local variables in different scopes
+
+        // OK, we have a timestamp option; now, let's look at the pointer to see if we can do something
+        // Remember pointer pointer (ha...) for later
+        uint8_t* timestamp_pointer_ptr = options_bytes;
+        uint8_t timestamp_pointer = *options_bytes;
+        options_bytes++;
+        if (timestamp_pointer > opt_length) {
+            // Timestamp full!
+            // Let's increment the overflow instead
+            uint8_t timestamp_overflow = (*options_bytes & 0xF0) >> 4;
+            if (timestamp_overflow == 0xF) {
+                // Overflow overflow... discard packet, as per RFC 791
+                return false;
+            }
+
+            // Increment overflow, continue
+            timestamp_flag = *options_bytes & 0xF;
+            *options_bytes = ((timestamp_overflow + 1) << 4) + timestamp_flag;
+            // *options_bytes++ : should be parsed as *(options_bytes++), which is just options_bytes++
+            options_bytes++;
+
+            // Skip remaining bytes; -2 because we counted type and length, -2 because we counter pointer and overflow/flag
+            *options_bytes += (opt_length - 2 - 2);
+            continue;
+        }
+
+        // We have a timestamp option, and it's not full!
+        // ...or is it? Still need to check whether we have space to write stuff
+
+        // First get the flag, to know whether timestamps are prefixed with addresses
+        timestamp_flag = *options_bytes & 0xF;
+        // *options_bytes++ : same as above
+        options_bytes++;
+
+        // timestamp pointer -1 cause it has a +1 according to the spec
+        uint8_t remaining_length = opt_length - (timestamp_pointer - 1);
+        uint8_t required_length = timestamp_flag == 0 ? 4 : 8;
+        if (remaining_length < required_length) {
+            // Not enough space, drop packet as per RFC 791
+            return false;
+        }
+
+        // OK, so we have enough space; let's go write!
+        // Remove 5 from the pointer since we have already skipped over type, length, pointer, overflow/flag, and pointer has a +1
+        options_bytes += (timestamp_pointer - 5);
+
+        // May be unaligned. Have fun dealing with _that_, contract writer! :D
+        uint32_t* timestamp_bytes = (uint32_t*) options_bytes;
+
+        // ... but first, if the tag is 3, addresses are pre-determined, so let's check whether we are supposed to write
+        if (timestamp_flag == 3) {
+            if (*timestamp_bytes != router_ip) {
+                // Not for us
+                continue;
+            }
+
+            timestamp_bytes++;
+        }
+
+        // If flag is 1, write our IP
+        if (timestamp_flag == 1) {
+            *timestamp_bytes = router_ip;
+            timestamp_bytes++;
+        }
+
+        // Write the timestamp
+        *timestamp_bytes = current_milliseconds_utc;
+
+        // Increment the pointer
+        *timestamp_pointer_ptr = *timestamp_pointer_ptr + required_length;
+
+        // Then, skip over the remaining bytes (-2 because the timestamp pointer is the 3rd byte)
+        options_bytes = timestamp_pointer_ptr + opt_length - 2;
+    } // end of loop
+
+    // If we reached this, we're good!
+    return true;
+}