Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix: Validate Circular Buffer Capacity #91

Merged
merged 8 commits into from
Nov 26, 2023
Merged

fix: Validate Circular Buffer Capacity #91

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
b42dac9
fix: Validate Circular Buffer Capacity
bushidocodes Nov 23, 2023
46ceb46
fix: cap memory in proof
bushidocodes Nov 23, 2023
d11433b
refactor: Remove suspicious power of 2 number
bushidocodes Nov 23, 2023
6bd4db7
Update exercises/practice/circular-buffer/.meta/proof.ci.wat
bushidocodes Nov 24, 2023
fc719e2
feat: Circular Buffer can grow up to four pages
bushidocodes Nov 25, 2023
60e16a2
Update exercises/practice/circular-buffer/circular-buffer.wat
bushidocodes Nov 25, 2023
e425c53
docs: Enhance hints for Circular Buffer
bushidocodes Nov 25, 2023
79b8f7d
docs: Update linear memory comment in proof.ci.wat for circular buffer
bushidocodes Nov 25, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions exercises/practice/circular-buffer/.docs/hints.md
View file
Open in desktop
bushidocodes marked this conversation as resolved.
Show resolved Hide resolved
Original file line number Diff line number Diff line change
@@ -1,3 +1,11 @@
# Hints

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

"The `memory.grow` instruction is used to grow a linear memory. The 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."

From https://webassembly.github.io/spec/core/syntax/instructions.html#syntax-instr-memory

"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"

From https://webassembly.github.io/spec/core/exec/runtime.html#page-size
65 changes: 53 additions & 12 deletions exercises/practice/circular-buffer/.meta/proof.ci.wat
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,31 +1,59 @@
(module
(memory 1)
;; a WebAssembly page is 64KiB, so each page holds up to 16384 i32s
;; Our linear memory is one page by default, but it is permitted to grow
;; up to four pages via use of the memory.grow instruction, which can hold
;; up to 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)))
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do you want (newCap - 1) / 16384 or (newCap / 16384) - 1 here? I think the latter.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The latter actually ends up allocating too few pages I believe due to integer division acting like a floor:

x idiv y ~= floor(x/y)

i.e. when we want to allocate a circular buffer that holds one more than we can fit in 1 page.

(newCap - 1) / 16384
((16385 - 1) idiv 16384) => (16384 idiv 16384) => 1

(newCap / 16384) - 1
((16385 idiv 16384) - 1) => (1 - 1) => 0

I checked this by modifying the solution to (memory.grow (i32.sub (i32.div_s (local.get $newCapacity) (i32.const 16384)) (i32.const 1))) and got the following:

    ✓ initializing negative capacity should error (2 ms)
    ✓ initializing capacity of 0 i32s should result in a linear memory with 1 page (1 ms)
    ✓ initializing capacity of 16384 i32s should result in a linear memory with 1 page
    ✕ initializing capacity of 16385 i32s should result in a linear memory with 2 pages (1 ms)
    ✓ initializing capacity of 32768 i32s should result in a linear memory with 2 pages (1 ms)
    ✕ initializing capacity of 32769 i32s should result in a linear memory with 3 pages
    ✓ initializing capacity of 49152 i32s should result in a linear memory with 3 pages
    ✕ initializing capacity of 49153 i32s should result in a linear memory with 4 pages
    ✓ initializing capacity of 65536 i32s should result in a linear memory with 4 pages
    
      ● CircularBuffer › initializing capacity of 16385 i32s should result in a linear memory with 2 pages

    expect(received).toEqual(expected) // deep equality

    Expected: 2
    Received: 1

      47 |   test("initializing capacity of 16385 i32s should result in a linear memory with 2 pages", () => {
      48 |     expect(currentInstance.exports.init(16385)).toEqual(0);
    > 49 |     expect(currentInstance.exports.mem.buffer.byteLength / 65536).toEqual(2);
         |                                                                   ^
      50 |   });
      51 |
      52 |   test("initializing capacity of 32768 i32s should result in a linear memory with 2 pages", () => {

      at Object.toEqual (circular-buffer.spec.js:49:67)

  ● CircularBuffer › initializing capacity of 32769 i32s should result in a linear memory with 3 pages

    expect(received).toEqual(expected) // deep equality

    Expected: 3
    Received: 2

      57 |   test("initializing capacity of 32769 i32s should result in a linear memory with 3 pages", () => {
      58 |     expect(currentInstance.exports.init(32769)).toEqual(0);
    > 59 |     expect(currentInstance.exports.mem.buffer.byteLength / 65536).toEqual(3);
         |                                                                   ^
      60 |   });
      61 |
      62 |   test("initializing capacity of 49152 i32s should result in a linear memory with 3 pages", () => {

      at Object.toEqual (circular-buffer.spec.js:59:67)

  ● CircularBuffer › initializing capacity of 49153 i32s should result in a linear memory with 4 pages

    expect(received).toEqual(expected) // deep equality

    Expected: 4
    Received: 3

      67 |   test("initializing capacity of 49153 i32s should result in a linear memory with 4 pages", () => {
      68 |     expect(currentInstance.exports.init(49153)).toEqual(0);
    > 69 |     expect(currentInstance.exports.mem.buffer.byteLength / 65536).toEqual(4);
         |                                                                   ^
      70 |   });
      71 |
      72 |   test("initializing capacity of 65536 i32s should result in a linear memory with 4 pages", () => {

      at Object.toEqual (circular-buffer.spec.js:69:67)

(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
View file
Open in desktop
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
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,16 @@
(module
(memory 1)
;; a WebAssembly page is 64KiB, so each page holds up to 16384 i32s
;; Our linear memory is one page by default, but it is permitted to grow
;; up to four pages via use of the memory.grow instruction, which can hold
;; up to 65536 i32s.
bushidocodes marked this conversation as resolved.
Show resolved Hide resolved
(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
Loading