Skip to content

Commit

Permalink
fix: Validate Circular Buffer Capacity (#91)
Browse files Browse the repository at this point in the history
* fix: Validate Circular Buffer Capacity

* fix: cap memory in proof

* refactor: Remove suspicious power of 2 number

* Update exercises/practice/circular-buffer/.meta/proof.ci.wat

Co-authored-by: Glenn Jackman <glenn.jackman@gmail.com>

* feat: Circular Buffer can grow up to four pages

* Update exercises/practice/circular-buffer/circular-buffer.wat

Co-authored-by: Glenn Jackman <glenn.jackman@gmail.com>

* docs: Enhance hints for Circular Buffer

* docs: Update linear memory comment in proof.ci.wat for circular buffer

---------

Co-authored-by: Glenn Jackman <glenn.jackman@gmail.com>
  • Loading branch information
bushidocodes and glennj authored Nov 26, 2023
1 parent 9b783f0 commit 3a409e5
Show file tree
Hide file tree
Showing 4 changed files with 133 additions and 17 deletions.
15 changes: 14 additions & 1 deletion exercises/practice/circular-buffer/.docs/hints.md
Original file line number Diff line number Diff line change
@@ -1,3 +1,16 @@
# Hints

Linear memory is byte-addressable, but `i32` has a width of four bytes.
`i32` has a width of four bytes.

"A memory instance... holds a vector of bytes. The length of the vector always is a multiple of the WebAssembly page size, which is defined to be the constant 65536"

[WebAssembly Specification: Memory Instances](https://webassembly.github.io/spec/core/exec/runtime.html#page-size)

"The `memory.size` instruction returns the current size of a memory. The `memory.grow` instruction grows memory by a given delta and returns the previous size, or -1 if enough memory cannot be allocated. Both instructions operate in units of page size."

[WebAssembly Specification: Memory Instructions](https://webassembly.github.io/spec/core/syntax/instructions.html#syntax-instr-memory)

Further References:

- [memory.size at MDN](https://developer.mozilla.org/en-US/docs/WebAssembly/Reference/Memory/Size)
- [memory.grow at MDN](https://developer.mozilla.org/en-US/docs/WebAssembly/Reference/Memory/Grow)
65 changes: 53 additions & 12 deletions exercises/practice/circular-buffer/.meta/proof.ci.wat
Original file line number Diff line number Diff line change
@@ -1,31 +1,59 @@
(module
(memory 1)
;; Linear memory is allocated one page by default.
;; A page is 64KiB, and that can hold up to 16384 i32s.
;; We will permit memory to grow to a maximum of four pages.
;; The maximum capacity of our buffer is 65536 i32s.
(memory (export "mem") 1 4)
(global $head (mut i32) (i32.const -1))
(global $tail (mut i32) (i32.const -1))
(global $capacity (mut i32) (i32.const 0))
(global $i32Size i32 (i32.const 4))


;; capacity: the number of elements to store
;; elementSize: the size of the element to store in bytes
;; Does not support resizing circular buffer. Wipes all data
;;
;; Initialize a circular buffer of i32s with a given capacity
;;
;; @param {i32} newCapacity - capacity of the circular buffer between 0 and 65,536
;; in order to fit in four 64KiB WebAssembly pages.
;;
;; @returns {i32} 0 on success or -1 on error
;;
(func (export "init") (param $newCapacity i32) (result i32)
;; a WebAssembly page is 4096 bytes, so up to 1024 i32s
(if (i32.gt_s (local.get $newCapacity) (i32.const 1024)) (then
(return (i32.const -1))
))
;; a WebAssembly page is 64KiB, so each page holds up to 16384 i32s
;; Our linear memory can grow up to four pages, so we can hold up to 65536 i32s
(if (i32.or
(i32.lt_s (local.get $newCapacity) (i32.const 0))
(i32.gt_s (local.get $newCapacity) (i32.const 65536))) (then
(return (i32.const -1))))

(global.set $head (i32.const -1))
(global.set $tail (i32.const -1))
(global.set $capacity (local.get $newCapacity))
(i32.const 0)

;; We do not need to grow the memory if the new capacity is less than 16384
(if (result i32) (i32.le_s (local.get $newCapacity) (i32.const 16384)) (then
(i32.const 0)
) (else
;; memory.grow returns old size on success or -1 on failure
(memory.grow (i32.div_s (i32.sub (local.get $newCapacity) (i32.const 1)) (i32.const 16384)))
(if (result i32) (i32.ne (i32.const -1)) (i32.const 0) (i32.const -1))
))
)

;;
;; Clear the circular buffer
;;
(func (export "clear")
(global.set $head (i32.const -1))
(global.set $tail (i32.const -1))
)

;;
;; Add an element to the circular buffer
;;
;; @param {i32} elem - element to add to the circular buffer
;;
;; @returns {i32} 0 on success or -1 if full
;;
(func (export "write") (param $elem i32) (result i32)
(local $temp i32)
;; Table has capacity of zero
Expand All @@ -52,6 +80,14 @@
(i32.const 0)
)

;;
;; Add an element to the circular buffer, overwriting the oldest element
;; if the buffer is full
;;
;; @param {i32} elem - element to add to the circular buffer
;;
;; @returns {i32} 0 on success or -1 if full (capacity of zero)
;;
(func (export "forceWrite") (param $elem i32) (result i32)
(local $temp i32)
;; Table has capacity of zero
Expand All @@ -78,7 +114,12 @@
(i32.const 0)
)

;; Go-style error handling type (i32,i32)
;;
;; Read the oldest element from the circular buffer, if not empty
;;
;; @returns {i32} element on success or -1 if empty
;; @returns {i32} status code set to 0 on success or -1 if empty
;;
(func (export "read") (result i32 i32)
(local $result i32)

Expand All @@ -99,4 +140,4 @@
(global.set $head (i32.rem_u (i32.add (global.get $head) (i32.const 1)) (global.get $capacity)))
(return (local.get $result) (i32.const 0))
)
)
)
60 changes: 59 additions & 1 deletion exercises/practice/circular-buffer/circular-buffer.spec.js
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,55 @@ describe("CircularBuffer", () => {
}
});

test("reading empty buffer should fail", () => {
test("initializing negative capacity should error", () => {
expect(currentInstance.exports.init(-1)).toEqual(-1);
});

xtest("initializing capacity of 0 i32s should result in a linear memory with 1 page", () => {
expect(currentInstance.exports.init(0)).toEqual(0);
expect(currentInstance.exports.mem.buffer.byteLength / 65536).toEqual(1);
});

xtest("initializing capacity of 16384 i32s should result in a linear memory with 1 page", () => {
expect(currentInstance.exports.init(16384)).toEqual(0);
expect(currentInstance.exports.mem.buffer.byteLength / 65536).toEqual(1);
});

xtest("initializing capacity of 16385 i32s should result in a linear memory with 2 pages", () => {
expect(currentInstance.exports.init(16385)).toEqual(0);
expect(currentInstance.exports.mem.buffer.byteLength / 65536).toEqual(2);
});

xtest("initializing capacity of 32768 i32s should result in a linear memory with 2 pages", () => {
expect(currentInstance.exports.init(32768)).toEqual(0);
expect(currentInstance.exports.mem.buffer.byteLength / 65536).toEqual(2);
});

xtest("initializing capacity of 32769 i32s should result in a linear memory with 3 pages", () => {
expect(currentInstance.exports.init(32769)).toEqual(0);
expect(currentInstance.exports.mem.buffer.byteLength / 65536).toEqual(3);
});

xtest("initializing capacity of 49152 i32s should result in a linear memory with 3 pages", () => {
expect(currentInstance.exports.init(49152)).toEqual(0);
expect(currentInstance.exports.mem.buffer.byteLength / 65536).toEqual(3);
});

xtest("initializing capacity of 49153 i32s should result in a linear memory with 4 pages", () => {
expect(currentInstance.exports.init(49153)).toEqual(0);
expect(currentInstance.exports.mem.buffer.byteLength / 65536).toEqual(4);
});

xtest("initializing capacity of 65536 i32s should result in a linear memory with 4 pages", () => {
expect(currentInstance.exports.init(65536)).toEqual(0);
expect(currentInstance.exports.mem.buffer.byteLength / 65536).toEqual(4);
});

xtest("initializing capacity greater than 65536 should error", () => {
expect(currentInstance.exports.init(65537)).toEqual(-1);
});

xtest("reading empty buffer should fail", () => {
expect(currentInstance.exports.init(1)).toEqual(0);
expect(currentInstance.exports.read()).toEqual([-1, -1]);
});
Expand Down Expand Up @@ -143,4 +191,14 @@ describe("CircularBuffer", () => {
expect(currentInstance.exports.read()).toEqual([4, 0]);
expect(currentInstance.exports.read()).toEqual([-1, -1]);
});

xtest("Should be able to write and read up to the full capacity of four 64Kib pages", () => {
expect(currentInstance.exports.init(65536)).toEqual(0);
for (let i = 0; i < 65536; i++) {
expect(currentInstance.exports.write(i)).toEqual(0);
}
for (let i = 0; i < 65536; i++) {
expect(currentInstance.exports.read()).toEqual([i, 0]);
}
});
});
10 changes: 7 additions & 3 deletions exercises/practice/circular-buffer/circular-buffer.wat
Original file line number Diff line number Diff line change
@@ -1,12 +1,16 @@
(module
(memory 1)
;; Linear memory is allocated one page by default.
;; A page is 64KiB, and that can hold up to 16384 i32s.
;; We will permit memory to grow to a maximum of four pages.
;; The maximum capacity of our buffer is 65536 i32s.
(memory (export "mem") 1 4)
;; Add globals here!

;;
;; Initialize a circular buffer of i32s with a given capacity
;;
;; @param {i32} newCapacity - capacity of the circular buffer between 0 and 1024
;; in order to fit in a single WebAssembly page
;; @param {i32} newCapacity - capacity of the circular buffer between 0 and 65,536
;; in order to fit in four 64KiB WebAssembly pages.
;;
;; @returns {i32} 0 on success or -1 on error
;;
Expand Down

0 comments on commit 3a409e5

Please sign in to comment.