Check Typed Jerboa owned moves
ober
c15496fb9de9cc8524a88d4c0018f1e1ae0b8a7d
--- a/docs/jerboa-to-rust.md +++ b/docs/jerboa-to-rust.md @@ -317,8 +317,10 @@ Mappings: Current landing: the typed front end recognizes resource declarations and the `(Owned T)` / `(Borrow T)` / `(MutBorrow T)` type constructors. The checker -validates those type references but does not yet enforce linear movement, -borrowing, or Drop lowering. +validates those type references and catches first-order straight-line Owned +movement errors: use after move and duplicate moves in one call. It does not +yet enforce path-sensitive movement, borrow lifetimes, borrowed-from-owned +coercions, or Drop lowering. At the C ABI boundary, references cannot cross directly. Use opaque handles. --- a/docs/typed-jerboa.md +++ b/docs/typed-jerboa.md @@ -506,8 +506,11 @@ The compiler should reject: Current landing: the front end recognizes `(resource Name)` and `(resource Name #:close close-fn)` declarations. Resource names participate in the type namespace, and `(Owned T)` / `(Borrow T)` / `(MutBorrow T)` are checked -compound type constructors. Linear move/borrow flow checks are still future -work. +compound type constructors. The checker now enforces a first straight-line +linear rule: passing an Owned variable to a consuming call moves it, later uses +of that variable in the same straight-line body are rejected, and moving the +same variable twice in one call is rejected. Path-sensitive branch joins, +borrow lifetimes, and borrowed-from-owned coercions are still future work. ## FFI Types @@ -897,8 +900,9 @@ Minimum excluded features: caller's effect list to cover the callee's effects; pure callers reject effectful callees. - Add linear resource types. Resource declarations and Owned/Borrow/MutBorrow - type constructors are parsed and type-checked; movement and borrowing rules - are not enforced yet. + type constructors are parsed and type-checked. The checker now catches + straight-line use-after-move and duplicate moves for Owned variables; richer + movement and borrowing rules are not enforced yet. - 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 --- a/lib/jerboa/typed/checker.ss +++ b/lib/jerboa/typed/checker.ss @@ -80,6 +80,10 @@ "Use pure by itself, or omit it and list the concrete effects."] [(effect-mismatch) "Add the callee effects to the caller's #:effects list, or call the effectful function from an effectful boundary."] + [(use-after-move) + "Do not use an Owned value after passing it to a consuming call."] + [(duplicate-move) + "Move an Owned value at most once in a single call."] [(bad-call-arity) "Pass exactly the number of arguments required by the typed function, constructor, accessor, or predicate."] [(argument-type-mismatch) @@ -263,6 +267,10 @@ (eq? expected any-value-type) (and (eq? actual 'Nat) (eq? expected 'Int)))) + (def (owned-type? type) + (and (pair? type) + (eq? (car type) 'Owned))) + (def (param-env params) (map (lambda (param) (cons (typed-param-name param) @@ -875,6 +883,135 @@ (normalize-effects caller-effects)))) '())) + (def (moved-name-errors expr moved) + (if (and (symbol? expr) (memq expr moved)) + (list (make-check-error 'use-after-move + "owned value used after move" + expr)) + '())) + + (def (call-owned-argument-names name args) + (let ([sig (lookup-name name (*call-env*))]) + (if (not sig) + '() + (let loop ([expected (typed-call-sig-param-types sig)] + [actual args] + [out '()]) + (cond + [(or (null? expected) (null? actual)) + (reverse out)] + [(and (owned-type? (car expected)) + (symbol? (car actual))) + (loop (cdr expected) + (cdr actual) + (cons (car actual) out))] + [else + (loop (cdr expected) (cdr actual) out)]))))) + + (def (duplicate-move-errors names expr) + (map (lambda (name) + (make-check-error 'duplicate-move + "owned value moved more than once in one call" + (list name expr))) + (duplicates names))) + + (def (check-ownership-body exprs env moved) + (let loop ([rest exprs] [current-moved moved] [errors '()]) + (if (null? rest) + (values current-moved (reverse errors)) + (let-values ([(next-moved expr-errors) + (check-ownership-expression + (car rest) + env + current-moved)]) + (loop (cdr rest) + next-moved + (append (reverse expr-errors) errors)))))) + + (def (check-ownership-sequence exprs env moved) + (check-ownership-body exprs env moved)) + + (def (check-ownership-call name args env moved expr) + (let-values ([(after-args arg-errors) + (check-ownership-body args env moved)]) + (let* ([owned-args (call-owned-argument-names name args)] + [duplicate-errors (duplicate-move-errors owned-args expr)] + [next-moved + (let loop ([rest owned-args] [out after-args]) + (if (null? rest) + out + (loop (cdr rest) (add-unique (car rest) out))))]) + (values next-moved + (append arg-errors duplicate-errors))))) + + (def (check-let-ownership bindings body env moved expr) + (if (not (list? bindings)) + (values moved '()) + (let-values ([(after-bindings binding-errors) + (check-ownership-body + (map cadr + (let loop ([rest bindings] [out '()]) + (cond + [(null? rest) (reverse out)] + [(and (pair? (car rest)) + (pair? (cdr (car rest)))) + (loop (cdr rest) (cons (car rest) out))] + [else (loop (cdr rest) out)]))) + env + moved)]) + (let-values ([(after-body body-errors) + (check-ownership-body body env after-bindings)]) + (values after-body + (append binding-errors body-errors)))))) + + (def (check-ownership-expression expr env moved) + (cond + [(symbol? expr) + (values moved (moved-name-errors expr moved))] + [(not (pair? expr)) + (values moved '())] + [else + (case (car expr) + [(begin) + (check-ownership-sequence (cdr expr) env moved)] + [(let) + (if (< (length expr) 3) + (values moved '()) + (check-let-ownership (cadr expr) (cddr expr) env moved expr))] + [(if) + (if (= (length expr) 4) + (let-values ([(after-cond cond-errors) + (check-ownership-expression (cadr expr) env moved)] + [(_then then-errors) + (check-ownership-expression (caddr expr) env moved)] + [(_else else-errors) + (check-ownership-expression (cadddr expr) env moved)]) + (values after-cond + (append cond-errors then-errors else-errors))) + (values moved '()))] + [(match) + (if (< (length expr) 2) + (values moved '()) + (let-values ([(after-target target-errors) + (check-ownership-expression (cadr expr) env moved)]) + (let loop ([rest (cddr expr)] [errors target-errors]) + (if (null? rest) + (values after-target errors) + (let ([clause (car rest)]) + (if (and (pair? clause) (pair? (cdr clause))) + (let-values ([(_branch branch-errors) + (check-ownership-body + (cdr clause) + env + moved)]) + (loop (cdr rest) + (append errors branch-errors))) + (loop (cdr rest) errors)))))))] + [else + (if (symbol? (car expr)) + (check-ownership-call (car expr) (cdr expr) env moved expr) + (values moved '()))])])) + (def (infer-function-call name args env type-names expr) (let ([sig (lookup-name name (*call-env*))]) (if (not sig) @@ -956,26 +1093,33 @@ expr)))])) (def (check-def-body def type-names) - (let-values ([(actual-type body-errors) + (let ([env (param-env (typed-def-params def))]) + (let-values ([(actual-type body-errors) (parameterize ([*current-effects* (normalize-effects (typed-def-effects def))]) (infer-body (typed-def-body def) - (param-env (typed-def-params def)) - type-names))]) - (append - body-errors - (if (and actual-type - (valid-type? (typed-def-return-type def) type-names) - (not (type-assignable? actual-type - (typed-def-return-type def)))) - (list (make-check-error 'return-type-mismatch - "function body type does not match declared return type" - (list (typed-def-name def) - (typed-def-return-type def) - actual-type))) - '())))) + env + type-names))] + [(_moved ownership-errors) + (check-ownership-body + (typed-def-body def) + env + '())]) + (append + body-errors + ownership-errors + (if (and actual-type + (valid-type? (typed-def-return-type def) type-names) + (not (type-assignable? actual-type + (typed-def-return-type def)))) + (list (make-check-error 'return-type-mismatch + "function body type does not match declared return type" + (list (typed-def-name def) + (typed-def-return-type def) + actual-type))) + '()))))) (def (check-declaration decl type-names) (cond --- a/tests/test-typed-checker.ss +++ b/tests/test-typed-checker.ss @@ -189,6 +189,59 @@ 0))) '(bad-type-arity)) +(test "owned resource can move once" + (error-kinds + '(typed-library (resource move-once) + (export ok) + (resource FileHandle) + (record Sink ((mut closed? : Bool))) + (def (consume (fh : (Owned FileHandle)) (sink : Sink)) : Unit + (Sink-closed?-set! sink #t)) + (def (ok (fh : (Owned FileHandle)) (sink : Sink)) : Unit + (consume fh sink)))) + '()) + +(test "borrowed resource can be reused" + (error-kinds + '(typed-library (resource borrow-reuse) + (export ok) + (resource FileHandle) + (def (size (fh : (Borrow FileHandle))) : Nat + 0) + (def (ok (fh : (Borrow FileHandle))) : Nat + (size fh) + (size fh)))) + '()) + +(test "owned resource use after move rejected" + (error-kinds + '(typed-library (resource use-after-move) + (export bad) + (resource FileHandle) + (record Sink ((mut closed? : Bool))) + (def (consume (fh : (Owned FileHandle)) (sink : Sink)) : Unit + (Sink-closed?-set! sink #t)) + (def (owned-size (fh : (Owned FileHandle))) : Nat + 0) + (def (bad (fh : (Owned FileHandle)) (sink : Sink)) : Nat + (consume fh sink) + (owned-size fh)))) + '(use-after-move)) + +(test "owned resource duplicate move rejected" + (error-kinds + '(typed-library (resource duplicate-move) + (export bad) + (resource FileHandle) + (record Sink ((mut closed? : Bool))) + (def (take-two (a : (Owned FileHandle)) + (b : (Owned FileHandle)) + (sink : Sink)) : Unit + (Sink-closed?-set! sink #t)) + (def (bad (fh : (Owned FileHandle)) (sink : Sink)) : Unit + (take-two fh fh sink)))) + '(duplicate-move)) + (test "body can return parameter" (error-kinds '(typed-library (body param)