Skip to content

Typed/untyped interop is unsound for structs, given a sufficiently powerful inspector #787

Open
@lexi-lambda

Description

@lexi-lambda

As reported by @LiberalArtist on the mailing list, a sufficiently powerful inspector can break type system invariants and create unsoundness due to insufficient protection of reflective operations on structs. Here’s a self-contained program that reproduces the issue and demonstrates the unsoundness:

#lang racket

(module s typed/racket
  (provide (struct-out must-be-integer)
           must-be-integer-add1)
  (struct must-be-integer ([v : Integer]))
  (define (must-be-integer-add1 [x : must-be-integer])
    (add1 (must-be-integer-v x))))

(require racket/runtime-path)

(define-runtime-module-path-index s-mpi '(submod "." s))

(define-values [must-be-integer must-be-integer-add1]
  (parameterize ([current-inspector (make-inspector)])
    (values (dynamic-require s-mpi 'must-be-integer)
            (dynamic-require s-mpi 'must-be-integer-add1))))

; Succeeds, but shouldn’t!
(define-values [struct:must-be-integer* skipped?] (struct-info (must-be-integer 1)))
((struct-type-make-constructor struct:must-be-integer*) "not an integer")

; Also succeeds, but shouldn’t!
(must-be-integer-add1 ((struct-type-make-constructor struct:must-be-integer*) "not an integer"))

This is possibly caused by racket/racket#2359.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions