Test typed handle stale drops
ober
dcc881e1040609d0cf7f8774d0f8fab0f758cb7d
--- a/docs/jerboa-to-rust.md +++ b/docs/jerboa-to-rust.md @@ -615,7 +615,8 @@ Second module: typed `rope`. wrapper boundary as opaque handles. `String` and `Bytes` returns now cross through generated byte buffer ownership helpers. Generated wrappers can explicitly drop typed handles. Option, result, automatic handle finalization, - and richer handle conversions remain future work. + and richer handle conversions remain future work. Boundary tests now cover + stale handle use after drop and double-drop rejection. ### Milestone 3: Records and Variants @@ -642,7 +643,9 @@ Second module: typed `rope`. - Add owned resource handle registry. - Add linear resource checking. - Add Rust `Drop` integration. -- Add boundary tests for stale and double-close handles. +- Add boundary tests for stale and double-close handles. Initial generated + wrapper smoke tests now reject using dropped handles and reject dropping the + same handle twice. ### Milestone 6: Static Integration --- a/docs/typed-jerboa.md +++ b/docs/typed-jerboa.md @@ -187,7 +187,8 @@ Current landing: handles, and explicit handle drops. The same target now also runs a small Jerboa caller through `support/typed-run.ss`, so the caller can use public wrapper functions from ordinary `(jerboa prelude)` code without an explicit - wrapper `load`. + wrapper `load`. Wrapper smoke tests cover stale handle use after drop and + double-drop rejection. - `support/typed-rust.ss`, `make typed-rust`, and `make typed-build` generate a disposable Cargo crate under `build/typed/rust`; `typed-build` also writes wrappers under `build/typed/jerboa` and runs `cargo build` against the @@ -878,7 +879,10 @@ Minimum excluded features: - Add effect annotations. - Check pure/effectful call relationships. - Add linear resource types. -- Model FFI handles. +- Model FFI handles. The current generated wrapper layer models same-module + record and variant handles as tagged opaque values, exposes explicit handle + drops, clears dropped handle ids, and has boundary tests for stale use and + double-close rejection. ### Milestone 6: LLVM Prototype --- a/tests/test-typed-split-tree-caller.ss +++ b/tests/test-typed-split-tree-caller.ss @@ -13,6 +13,13 @@ (set! fail (+ fail 1)) (displayln "FAIL " name)))) +(def (raises? thunk) + (try + (begin + (thunk) + #f) + (catch (e) #t))) + (def (split-tree-summary tree) (alist (size (split-tree-size tree)) @@ -56,7 +63,9 @@ (and (%typed-rust-handle-drop! inner) (and (%typed-rust-handle-drop! left) (and (%typed-rust-handle-drop! middle) - (%typed-rust-handle-drop! right)))))))) + (%typed-rust-handle-drop! right))))))) + (check "caller double drop rejected" + (raises? (lambda () (%typed-rust-handle-drop! root))))) (displayln "") (displayln "Typed split-tree Jerboa caller smoke: " pass " passed, " fail " failed") --- a/tests/test-typed-split-tree-e2e.ss +++ b/tests/test-typed-split-tree-e2e.ss @@ -135,6 +135,8 @@ (check "drop split handle" (%typed-rust-handle-drop! root)) +(check "double drop split handle rejected" + (raises? (lambda () (%typed-rust-handle-drop! root)))) (check "dropped split handle rejected" (raises? (lambda () (split-tree-size root)))) --- a/tests/test-typed-wrapper-e2e.ss +++ b/tests/test-typed-wrapper-e2e.ss @@ -64,6 +64,8 @@ (define dropped-box (make-box 31)) (check "handle drop" (%typed-rust-handle-drop! dropped-box)) +(check "double handle drop rejected" + (raises? (lambda () (%typed-rust-handle-drop! dropped-box)))) (check "dropped handle rejected" (raises? (lambda () (box-value dropped-box)))) (check "add-one rejects non-Nat"