| /* | |
| * simple_driver.c — Ring-buffer character device | |
| * | |
| * Call hierarchy (this is what makes GRACE interesting): | |
| * | |
| * dev_open → rb_init | |
| * dev_write → rb_is_full, rb_write | |
| * dev_read → rb_is_empty, rb_read | |
| * dev_close → (none) | |
| * | |
| * So GRACE must generate specs top-down: | |
| * Layer 1: dev_open, dev_write, dev_read, dev_close (entry points) | |
| * Layer 2: rb_init, rb_is_full, rb_write, rb_is_empty, rb_read (internals) | |
| * | |
| * Intentional bug: | |
| * rb_write() computes free space as (capacity - count + 1) instead of | |
| * (capacity - count), an off-by-one that allows writing one extra byte | |
| * when the buffer is exactly full, corrupting rb->count > rb->capacity. | |
| * | |
| * Spurious counterexample opportunity: | |
| * rb_is_full() has postcondition "returns 1 iff rb->count == rb->capacity". | |
| * With a weak precondition (count unconstrained), CBMC can find inputs | |
| * where count > capacity — but dev_write() always calls rb_init() first | |
| * via dev_open(), so count > capacity is unreachable from any real caller. | |
| * GRACE should detect this as spurious and refine the precondition. | |
| */ | |
| /* ------------------------------------------------------------------ */ | |
| /* Data structures */ | |
| /* ------------------------------------------------------------------ */ | |
| typedef struct { | |
| uint8_t *buf; /* backing storage */ | |
| size_t capacity; /* total capacity in bytes */ | |
| size_t head; /* write index */ | |
| size_t tail; /* read index */ | |
| size_t count; /* bytes currently stored */ | |
| } ring_buffer_t; | |
| typedef struct { | |
| ring_buffer_t rb; /* embedded ring buffer */ | |
| uint8_t backing[64]; /* fixed backing store */ | |
| int is_open; | |
| } char_dev_t; | |
| /* ------------------------------------------------------------------ */ | |
| /* Internal ring-buffer helpers (Layer 2 — called by dev_* functions) */ | |
| /* ------------------------------------------------------------------ */ | |
| /* | |
| * rb_init — initialise ring buffer with given capacity. | |
| * Called by: dev_open | |
| */ | |
| static void rb_init(ring_buffer_t *rb, uint8_t *buf, size_t capacity) | |
| { | |
| rb->buf = buf; | |
| rb->capacity = capacity; | |
| rb->head = 0; | |
| rb->tail = 0; | |
| rb->count = 0; | |
| } | |
| /* | |
| * rb_is_full — return 1 if no space remains. | |
| * Called by: dev_write | |
| */ | |
| static int rb_is_full(const ring_buffer_t *rb) | |
| { | |
| return rb->count == rb->capacity; | |
| } | |
| /* | |
| * rb_is_empty — return 1 if no data available. | |
| * Called by: dev_read | |
| */ | |
| static int rb_is_empty(const ring_buffer_t *rb) | |
| { | |
| return rb->count == 0; | |
| } | |
| /* | |
| * rb_write — append up to `len` bytes; return bytes written. | |
| * Called by: dev_write | |
| * | |
| * BUG: free = (capacity - count) + 1 should be (capacity - count). | |
| * This lets one extra byte be written when the buffer is full. | |
| */ | |
| static size_t rb_write(ring_buffer_t *rb, const uint8_t *data, size_t len) | |
| { | |
| size_t free = (rb->capacity - rb->count) + 1; /* <-- off-by-one bug */ | |
| size_t to_write = (len > free) ? free : len; | |
| for (size_t i = 0; i < to_write; i++) { | |
| rb->buf[rb->head] = data[i]; | |
| rb->head = (rb->head + 1) % rb->capacity; | |
| rb->count++; | |
| } | |
| return to_write; | |
| } | |
| /* | |
| * rb_read — consume up to `len` bytes into `buf`; return bytes read. | |
| * Called by: dev_read | |
| */ | |
| static size_t rb_read(ring_buffer_t *rb, uint8_t *buf, size_t len) | |
| { | |
| size_t avail = rb->count; | |
| size_t to_read = (len > avail) ? avail : len; | |
| for (size_t i = 0; i < to_read; i++) { | |
| buf[i] = rb->buf[rb->tail]; | |
| rb->tail = (rb->tail + 1) % rb->capacity; | |
| rb->count--; | |
| } | |
| return to_read; | |
| } | |
| /* ------------------------------------------------------------------ */ | |
| /* Public device API (Layer 1 — entry points, no callers in this file) */ | |
| /* ------------------------------------------------------------------ */ | |
| /* | |
| * dev_open — initialise device and open it. | |
| * Precondition: dev != NULL | |
| * Postcondition: dev->is_open == 1, ring buffer initialised and empty | |
| */ | |
| int dev_open(char_dev_t *dev) | |
| { | |
| if (dev->is_open) | |
| return -1; /* already open */ | |
| rb_init(&dev->rb, dev->backing, sizeof(dev->backing)); | |
| dev->is_open = 1; | |
| return 0; | |
| } | |
| /* | |
| * dev_write — write data into the device buffer. | |
| * Precondition: dev != NULL, dev->is_open == 1, data != NULL, len > 0 | |
| * Postcondition: returns bytes written (<= len); 0 if full | |
| */ | |
| int dev_write(char_dev_t *dev, const uint8_t *data, size_t len) | |
| { | |
| if (!dev->is_open) | |
| return -1; | |
| if (rb_is_full(&dev->rb)) | |
| return 0; | |
| return (int)rb_write(&dev->rb, data, len); | |
| } | |
| /* | |
| * dev_read — read data from the device buffer. | |
| * Precondition: dev != NULL, dev->is_open == 1, buf != NULL, len > 0 | |
| * Postcondition: returns bytes read (<= len); 0 if empty | |
| */ | |
| int dev_read(char_dev_t *dev, uint8_t *buf, size_t len) | |
| { | |
| if (!dev->is_open) | |
| return -1; | |
| if (rb_is_empty(&dev->rb)) | |
| return 0; | |
| return (int)rb_read(&dev->rb, buf, len); | |
| } | |
| /* | |
| * dev_close — close the device. | |
| * Precondition: dev != NULL, dev->is_open == 1 | |
| * Postcondition: dev->is_open == 0 | |
| */ | |
| int dev_close(char_dev_t *dev) | |
| { | |
| if (!dev->is_open) | |
| return -1; | |
| dev->is_open = 0; | |
| return 0; | |
| } | |