From af9fa2cea86348ab1b184a6c5e47e8e953df2d11 Mon Sep 17 00:00:00 2001 From: Tony Garnock-Jones Date: Wed, 13 Mar 2013 17:30:57 -0400 Subject: [PATCH] Typed implementation WIP --- api-untyped.rkt | 40 ++++++++ api.rkt | 150 +++++++++++++++++++--------- codec.rkt | 254 ++++++++++++++++++++++++++++-------------------- mapping.rkt | 14 +-- tk-dns.rkt | 87 +++++++++-------- 5 files changed, 346 insertions(+), 199 deletions(-) create mode 100644 api-untyped.rkt diff --git a/api-untyped.rkt b/api-untyped.rkt new file mode 100644 index 0000000..f9c926c --- /dev/null +++ b/api-untyped.rkt @@ -0,0 +1,40 @@ +#lang racket/base +;; Untyped struct definitions required to interoperate with typed-matrix's struct-map +;; See also Racket PR 13593. + +(require racket-typed-matrix/struct-map) + +(provide (struct-out domain)) + +;; (These utilities need to be defined ahead of the domain struct +;; definition.) +(define (domain=? a b recursive-equal?) + (recursive-equal? (domain-downcased-labels a) + (domain-downcased-labels b))) + +(define (domain-hash-1/2 d recursive-hash) + (recursive-hash (domain-downcased-labels d))) + +(struct domain (labels downcased-labels) + #:transparent + #:property prop:equal+hash (list domain=? domain-hash-1/2 domain-hash-1/2) + #:property prop:struct-map (lambda (f seed x) + (let-values (((labels seed) (f (domain-labels x) seed))) + (values (make-domain labels) seed)))) + +;; ListOf -> ListOf +;; Converts the 7-bit ASCII bytes in the argument to lower-case +;; equivalents. Used to normalize case for domain-name comparisons. +(define (downcase-labels labels) + (for/list ([label labels]) + (define b (make-bytes (bytes-length label))) + (for ([i (bytes-length label)]) + (define v (bytes-ref label i)) + (bytes-set! b i (if (<= 65 v 90) (+ 32 v) v))) + b)) + +;; ListOf -> DomainName +;; Replacement constructor for domain structs. Automatically downcases +;; labels appropriately. +(define (make-domain labels) + (domain labels (downcase-labels labels))) diff --git a/api.rkt b/api.rkt index 616a29f..1d6c76d 100644 --- a/api.rkt +++ b/api.rkt @@ -1,11 +1,16 @@ -#lang racket/base +#lang typed/racket/base ;; Definitions for use in the API to the functionality of the library. -(provide (except-out (struct-out domain) domain) +(provide DomainName + (except-out (struct-out domain) domain) (rename-out [make-domain domain]) domain-root? domain-parent + IPv4 + IPv6 + + Question (struct-out question) question-cyclic? question-too-glueless? @@ -14,21 +19,30 @@ cname-question ns-question + AnsweredQuestion + RR (struct-out answered-question) (struct-out rr) + CompleteAnswer (struct-out complete-answer) empty-complete-answer merge-answers extract-addresses + RData (struct-out hinfo) (struct-out minfo) (struct-out mx) (struct-out soa) (struct-out wks) (struct-out srv) + rr-rdata/cast + RRType + QueryType + RRClass + QueryClass type->value value->type qtype->value value->qtype class->value value->class @@ -39,42 +53,39 @@ (require racket/match) (require racket-typed-matrix/struct-map) -;; (These utilities need to be defined ahead of the domain struct -;; definition.) -(define (domain=? a b recursive-equal?) - (recursive-equal? (domain-downcased-labels a) - (domain-downcased-labels b))) - -(define (domain-hash-1/2 d recursive-hash) - (recursive-hash (domain-downcased-labels d))) - ;; A DomainName is a (domain ListOf), representing a domain ;; name. The head of the list is the leftmost label; for example, ;; www.google.com is represented as '(#"www" #"google" #"com"). -(struct domain (labels downcased-labels) - #:transparent - #:property prop:equal+hash (list domain=? domain-hash-1/2 domain-hash-1/2) - #:property prop:struct-map (lambda (f seed x) - (let-values (((labels seed) (f (domain-labels x) seed))) - (values (make-domain labels) seed)))) +(require/typed "api-untyped.rkt" + [#:struct domain ([labels : (Listof Bytes)] + [downcased-labels : (Listof Bytes)])]) +(define-type DomainName domain) ;; A ShortString is a String with length 255 or shorter. ;; An IPv4 is a (vector Byte Byte Byte Byte), representing an IPv4 ;; address. For example, 127.0.0.1 is represented as (vector 127 0 0 ;; 1). +(define-type IPv4 (Vector Byte Byte Byte Byte)) ;; An IPv6 is a Vector of length 16 containing Bytes, representing an ;; IPv6 address. For example, 2001:0db8:85a3:0000:0000:8a2e:0370:7334 ;; is represented as (vector #x20 #x01 #x0d #xb8 #x85 #xa3 #x00 #x00 ;; #x00 #x00 #x8a #x2e #x03 #x70 #x73 #x34). +(define-type IPv6 (Vector Byte Byte Byte Byte + Byte Byte Byte Byte + Byte Byte Byte Byte + Byte Byte Byte Byte)) ;; A Question is a (question DomainName QueryType QueryClass ;; QuestionContext), representing a DNS question: "What are the RRs ;; for the given name, type and class?" as well as a possible parent ;; question that the answer to this question is to contribute to the ;; answer to. -(struct question (name type class context) #:prefab) +(struct: question + ([name : DomainName] [type : QueryType] [class : QueryClass] [context : QuestionContext]) + #:prefab) +(define-type Question question) ;; A QuestionContext is one of ;; -- (cname-subq Question), resulting from the expansion of a CNAME @@ -87,32 +98,44 @@ ;; excessively-glueless subquestion not represented here, and should ;; *not* in turn be considered for gluelessness-restarting: this is ;; needed to avoid a different kind of infinite loop. -(struct subquestion (parent) #:prefab) -(struct cname-subq subquestion () #:prefab) -(struct ns-subq subquestion () #:prefab) +(struct: subquestion ([parent : Question]) #:prefab) +(struct: cname-subq subquestion () #:prefab) +(struct: ns-subq subquestion () #:prefab) +(define-type QuestionContext (U subquestion cname-subq ns-subq False 'restart)) ;; An AnsweredQuestion is an (answered-question Question ;; Maybe). -(struct answered-question (q a) #:prefab) +(struct: answered-question ([q : Question] [a : (Option CompleteAnswer)]) #:prefab) +(define-type AnsweredQuestion answered-question) ;; A CompleteAnswer is a (complete-answer Set Set Set) -(struct complete-answer (rrs authorities additional) #:prefab) +(struct: complete-answer + ([rrs : (Setof RR)] [authorities : (Setof RR)] [additional : (Setof RR)]) + #:prefab) +(define-type CompleteAnswer complete-answer) ;; An RR is a (rr DomainName RRType RRClass Uint32 RData), ;; representing a resource record. -(struct rr (name type class ttl rdata) #:prefab) +(struct: rr ([name : DomainName] + [type : RRType] + [class : RRClass] + [ttl : Nonnegative-Integer] + [rdata : RData]) + #:prefab) +(define-type RR rr) ;; An RData is one of ;; - a DomainName, for CNAME, MB, MD, MF, MG, MR, NS and PTR records ;; - an IPv4, an "A" record ;; - an IPv6, an "AAAA" record -;; - (hinfo ShortString ShortString), a host information record [O] +;; - (hinfo Bytes Bytes), a host information record [O] ;; - (minfo DomainName DomainName), a mailbox information record [O] ;; - (mx Uint16 DomainName), a mail exchanger record ;; - (soa DomainName DomainName Uint32 Uint32 Uint32 Uint32 Uint32), a ;; start-of-authority record ;; - (wks IPv4 Byte Bytes), a Well-Known Service [O] ;; - (srv Uint16 Uint16 Uint16 DomainName), an "SRV" record +;; - a ListOf, a txt record ;; - a Bytes, either a 'null type RR or any unrecognised RR type. ;; ;; In each case, the RData's variant MUST line up correctly with the @@ -120,17 +143,36 @@ ;; ;; Many of these variants are obsolete in today's DNS database (marked ;; [O] above). -(struct hinfo (cpu os) #:prefab) -(struct minfo (rmailbx emailbx) #:prefab) -(struct mx (preference exchange) #:prefab) -(struct soa (mname rname serial refresh retry expire minimum) #:prefab) -(struct wks (address protocol bitmap) #:prefab) -(struct srv (priority weight port target) #:prefab) +(struct: hinfo ([cpu : Bytes] [os : Bytes]) #:prefab) +(struct: minfo ([rmailbx : DomainName] [emailbx : DomainName]) #:prefab) +(struct: mx ([preference : Nonnegative-Integer] [exchange : DomainName]) #:prefab) +(struct: soa ([mname : DomainName] + [rname : DomainName] + [serial : Nonnegative-Integer] + [refresh : Nonnegative-Integer] + [retry : Nonnegative-Integer] + [expire : Nonnegative-Integer] + [minimum : Nonnegative-Integer]) #:prefab) +(struct: wks ([address : IPv4] [protocol : Byte] [bitmap : Bytes]) #:prefab) +(struct: srv ([priority : Nonnegative-Integer] + [weight : Nonnegative-Integer] + [port : Nonnegative-Integer] + [target : DomainName]) #:prefab) +(define-type RData (U DomainName IPv4 IPv6 hinfo minfo mx soa wks srv (Listof Bytes) Bytes)) + +(define-syntax-rule (rr-rdata/cast Type) + (lambda: ([rr : RR]) (cast (rr-rdata rr) Type))) ;; An RRType is a Symbol or a Number, one of the possibilities given ;; in the following define-mapping. It represents the type of an ;; RR. When used in an RR with an RData, the RRType and the RData ;; variant must correspond. +(define-type RRType (U 'a 'ns 'md 'mf 'cname 'soa 'mb 'mg + 'mr 'null 'wks 'ptr 'hinfo 'minfo 'mx 'txt + 'aaaa 'srv + Nonnegative-Integer)) +(: type->value : RRType -> Nonnegative-Integer) +(: value->type : Nonnegative-Integer -> RRType) (define-mapping type->value value->type #:forward-default values #:backward-default values @@ -156,6 +198,9 @@ ;; A QueryType is a Symbol or Number (as given in the following ;; define-mapping) or an RRType. It specifies the kinds of records ;; being sought after in a DNS query. +(define-type QueryType (U RRType 'axfr 'mailb 'maila '*)) +(: qtype->value : QueryType -> Nonnegative-Integer) +(: value->qtype : Nonnegative-Integer -> QueryType) (define-mapping qtype->value value->qtype #:forward-default type->value #:backward-default value->type @@ -168,6 +213,9 @@ ;; in the following define-mapping. It represents the "class" of DNS ;; records being discussed. All classes except 'in are obsolete in ;; today's DNS databases. +(define-type RRClass (U 'in 'cs 'ch 'hs Nonnegative-Integer)) +(: class->value : RRClass -> Nonnegative-Integer) +(: value->class : Nonnegative-Integer -> RRClass) (define-mapping class->value value->class #:forward-default values #:backward-default values @@ -179,6 +227,9 @@ ;; A QueryClass is a Symbol or Number (as given in the following ;; define-mapping) or an RRClass. It specifies the "class" of records ;; being sought after in a DNS query. +(define-type QueryClass (U RRClass '*)) +(: qclass->value : QueryClass -> Nonnegative-Integer) +(: value->qclass : Nonnegative-Integer -> QueryClass) (define-mapping qclass->value value->qclass #:forward-default class->value #:backward-default value->class @@ -187,6 +238,7 @@ ;; ListOf -> ListOf ;; Converts the 7-bit ASCII bytes in the argument to lower-case ;; equivalents. Used to normalize case for domain-name comparisons. +(: downcase-labels : (Listof Bytes) -> (Listof Bytes)) (define (downcase-labels labels) (for/list ([label labels]) (define b (make-bytes (bytes-length label))) @@ -198,24 +250,25 @@ ;; ListOf -> DomainName ;; Replacement constructor for domain structs. Automatically downcases ;; labels appropriately. +(: make-domain : (Listof Bytes) -> DomainName) (define (make-domain labels) (domain labels (downcase-labels labels))) -;; DomainName -> Boolean +(: domain-root? : DomainName -> Boolean) (define (domain-root? d) (null? (domain-labels d))) -;; DomainName -> Maybe +(: domain-parent : DomainName -> (Option DomainName)) (define (domain-parent d) (and (pair? (domain-labels d)) (domain (cdr (domain-labels d)) (cdr (domain-downcased-labels d))))) -;; -> CompleteAnswer +(: empty-complete-answer : -> CompleteAnswer) (define (empty-complete-answer) (complete-answer (set) (set) (set))) -;; CompleteAnswer CompleteAnswer -> CompleteAnswer +(: merge-answers : CompleteAnswer CompleteAnswer -> CompleteAnswer) (define (merge-answers a1 a2) (match-define (complete-answer n1 u1 d1) a1) (match-define (complete-answer n2 u2 d2) a2) @@ -223,7 +276,7 @@ (set-union u1 u2) (set-union d1 d2))) -;; DomainName Maybe -> SetOf +(: extract-addresses : DomainName (Option CompleteAnswer) -> (Setof IPv4)) (define (extract-addresses name ans) (match ans [#f ;; name-error/NXDOMAIN, so definitely no addresses. @@ -231,27 +284,29 @@ [(complete-answer ns us ds) (define rrs (set->list (set-union ns us ds))) (let loop ((names (list name)) - (ips (set)) - (seen (set))) + (ips ((inst set IPv4))) + (seen ((inst set DomainName)))) (if (null? names) ips (let* ((name (car names)) - (records (filter (lambda (rr) (equal? name (rr-name rr))) rrs))) + (records (filter (lambda: ([rr : RR]) (equal? name (rr-name rr))) rrs))) (if (set-member? seen name) (loop (cdr names) ips seen) - (let ((a-records (filter (lambda (rr) (equal? 'a (rr-type rr))) records)) - (cname-records (filter (lambda (rr) (equal? 'cname (rr-type rr))) records))) - (loop (append (map rr-rdata cname-records) (cdr names)) - (set-union ips (list->set (map rr-rdata a-records))) + (let ((a-records (filter (lambda: ([rr : RR]) (equal? 'a (rr-type rr))) records)) + (cname-records + (filter (lambda: ([rr : RR]) (equal? 'cname (rr-type rr))) records))) + (loop (append (map (rr-rdata/cast DomainName) cname-records) (cdr names)) + (set-union ips (list->set (map (rr-rdata/cast IPv4) a-records))) (set-add seen name)))))))])) ;; Question -> Boolean ;; #t iff this question is being asked in order to supply answers ;; contributing to a parent context that's trying to answer exactly ;; this question. +(: question-cyclic? : Question -> Boolean) (define (question-cyclic? q) (match-define (question name type class parent) q) - (let search ((ancestor parent)) + (let: search : Boolean ((ancestor : QuestionContext parent)) (match ancestor [(subquestion (question (== name) (== type) (== class) _)) #t] ;; uh-oh! A cycle! [(subquestion (question _ _ _ ancestor-parent)) (search ancestor-parent)] ;; recursive case @@ -263,9 +318,10 @@ ;; from the outside world, then that's too glueless. See ;; http://cr.yp.to/djbdns/notes.html in the sections "Gluelessness" ;; and "Expiring glue". +(: question-too-glueless? : Question -> Boolean) (define (question-too-glueless? q) (define count - (let search ((q q) (acc 0)) + (let: search : Integer ((q : Question q) (acc : Integer 0)) (match-define (question _ _ _ parent) q) (cond [(ns-subq? parent) (search (subquestion-parent parent) (+ acc 1))] @@ -281,6 +337,7 @@ ;; Question -> Boolean ;; #t iff this question is being asked in the context of some ;; excessively glueless subquestion. +(: question-restarted? : Question -> Boolean) (define (question-restarted? q) (match-define (question name type class parent) q) (let search ((ancestor parent)) @@ -292,16 +349,19 @@ ;; Question -> Question ;; Returns a question equivalent to q, but in a 'restart context, for ;; retracing from the roots in cases of excessive gluelessness. +(: restart-question : Question -> Question) (define (restart-question q) (struct-copy question q [context 'restart])) ;; DomainName Question -> Question ;; Produces a new question with CNAME context. +(: cname-question : DomainName Question -> Question) (define (cname-question name q) (match-define (question _ type class _) q) (question name type class (cname-subq q))) ;; DomainName Question -> Question ;; Produces a new question with NS context. +(: ns-question : DomainName Question -> Question) (define (ns-question name q) (question name 'a 'in (ns-subq q))) ;; TODO: 'aaaa ? diff --git a/codec.rkt b/codec.rkt index 7edbd6a..c22ef51 100644 --- a/codec.rkt +++ b/codec.rkt @@ -1,9 +1,17 @@ -#lang racket/base +#lang typed/racket/base ;; DNS wire-protocol codec. -(provide value->query-opcode query-opcode->value +(provide Opcode + ResponseCode + value->query-opcode query-opcode->value value->query-response-code query-response-code->value + DNSMessage + Direction + Authoritativeness + Truncatedness + RecursionDesired + RecursionAvailable (struct-out dns-message) packet->dns-message @@ -17,12 +25,18 @@ (require "api.rkt") (require "mapping.rkt") +(domain (list #"hello")) + (require racket/match) + (require racket-bitsyntax) ;; An Opcode is a Symbol or a Number, one of the possibilities given ;; in the following define-mapping. It represents a DNS message ;; operation; see the RFC for details. +(define-type Opcode (U 'query 'iquery 'status Nonnegative-Integer)) +(: value->query-opcode : Nonnegative-Integer -> Opcode) +(: query-opcode->value : Opcode -> Nonnegative-Integer) (define-mapping value->query-opcode query-opcode->value #:forward-default values #:backward-default values @@ -33,6 +47,11 @@ ;; A ResponseCode is a Symbol or a Number, one of the possibilities ;; given in the following define-mapping. It represents the outcome of ;; a DNS query. +(define-type ResponseCode (U 'no-error 'format-error 'server-failure + 'name-error 'not-implemented 'refused + Nonnegative-Integer)) +(: value->query-response-code : Nonnegative-Integer -> ResponseCode) +(: query-response-code->value : ResponseCode -> Nonnegative-Integer) (define-mapping value->query-response-code query-response-code->value (0 no-error) (1 format-error) @@ -48,57 +67,82 @@ ;; ;; Interpreted as either a DNS request or reply, depending on the ;; Direction. -(struct dns-message (id - direction - opcode - authoritative - truncated - recursion-desired - recursion-available - response-code - questions - answers - authorities - additional) - #:prefab) +(struct: dns-message ([id : Nonnegative-Integer] + [direction : Direction] + [opcode : Opcode] + [authoritative : Authoritativeness] + [truncated : Truncatedness] + [recursion-desired : RecursionDesired] + [recursion-available : RecursionAvailable] + [response-code : ResponseCode] + [questions : (Listof Question)] + [answers : (Listof RR)] + [authorities : (Listof RR)] + [additional : (Listof RR)]) + #:prefab) +(define-type DNSMessage dns-message) +(define-type Direction (U 'request 'response)) +(define-type Authoritativeness (U 'non-authoritative 'authoritative)) +(define-type Truncatedness (U 'not-truncated 'truncated)) +(define-type RecursionDesired (U 'no-recursion-desired 'recursion-desired)) +(define-type RecursionAvailable (U 'no-recursion-available 'recursion-available)) ;; Bit-syntax type for counted repeats of a value. ;; Example: Length-prefixed list of 32-bit unsigned words: -;; (bit-string-case input ([ len (vals :: (t:ntimes len bits 32)) ] vals)) -;; (bit-string (vals :: (t:ntimes bits 32))) +;; (bit-string-case input ([ len (vals :: (t:ntimes Integer len bits 32)) ] vals)) +;; (bit-string (vals :: (t:ntimes Integer bits 32))) (define-syntax t:ntimes (syntax-rules () - ((_ #t input ks kf times-to-repeat option ...) - (let loop ((count times-to-repeat) - (acc '()) - (input input)) - (cond - ((positive? count) (bit-string-case input - ([ (v :: option ...) (rest :: binary) ] - (loop (- count 1) (cons v acc) rest)) - (else (kf)))) - (else (ks (reverse acc) input))))) - ((_ #f vs option ...) - (t:listof #f vs option ...)))) + ((_ #t input0 ks kf Type times-to-repeat option ...) + (let () + ;; A simple loop without multiple-values or #f is much cleaner + ;; here, but I can't find a way of expressing the types + ;; required while making that work. This way, we avoid needing + ;; to mention the type of the result of calls to ks. + (: loop : Integer (Listof Type) BitString -> (Values (Option (Listof Type)) BitString)) + (define (loop count acc input) + (cond + ((positive? count) (bit-string-case input + ([ (v :: option ...) (rest :: binary) ] + (loop (- count 1) (cons v acc) rest)) + (else + (values #f input)))) + (else (values (reverse acc) input)))) + (let-values (((vs rest) (loop times-to-repeat '() input0))) + (if vs + (ks vs rest) + (kf))))) + ((_ #f val Type option ...) + (t:listof #f val Type option ...)))) ;; Bit-syntax type for repeats of a value until no more input available. ;; Example: List of 32-bit unsigned words: -;; (bit-string-case input ([ (vals :: (t:listof bits 32)) ] vals)) -;; (bit-string (vals :: (t:listof bits 32))) +;; (bit-string-case input ([ (vals :: (t:listof Integer bits 32)) ] vals)) +;; (bit-string (vals :: (t:listof Integer bits 32))) (define-syntax t:listof (syntax-rules () - ((_ #t input ks kf option ...) - (let loop ((acc '()) - (input input)) - (bit-string-case input - ([ (v :: option ...) (rest :: binary) ] - (loop (cons v acc) rest)) - ([] - (ks (reverse acc) #"")) - (else - (kf))))) - ((_ #f vs option ...) - (let loop ((vs vs)) + ((_ #t input0 ks kf Type option ...) + ;; The loop is unrolled once here to let Typed Racket propagate + ;; the type of v0 into the type of acc in the loop. When not + ;; unrolled, it gives acc type (Listof Any). + ;; TODO: come up with some other way of doing this that avoids the duplication. + (bit-string-case input0 + ([ (v0 :: option ...) (input1 :: binary) ] + (let loop ((acc (list v0)) + (input input1)) + (bit-string-case input + ([ (v :: option ...) (rest :: binary) ] + (loop (cons v acc) rest)) + ([] + (ks (reverse acc) #"")) + (else + (kf))))) + ([] + (ks '() #"")) + (else + (kf)))) + ((_ #f vs Type option ...) + (let: loop : BitString ((vs : (Listof Type) vs)) (cond ((pair? vs) (bit-string ((car vs) :: option ...) ((loop (cdr vs)) :: binary))) @@ -142,7 +186,7 @@ ;; +--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+ ;; -;; Bytes -> DNSMessage +(: packet->dns-message : BitString -> DNSMessage) ;; Parse an encoded DNS message packet into the corresponding Racket ;; structure. Raises an exception on failure. (define (packet->dns-message packet) @@ -163,16 +207,16 @@ (ancount :: bits 16) (nscount :: bits 16) (arcount :: bits 16) - (q-section :: (t:ntimes qdcount (t:question packet))) - (a-section :: (t:ntimes ancount (t:rr packet))) - (auth-section :: (t:ntimes nscount (t:rr packet))) - (additional-section :: (t:ntimes arcount (t:rr packet))) ] + (q-section :: (t:ntimes Question qdcount (t:question packet))) + (a-section :: (t:ntimes RR ancount (t:rr packet))) + (auth-section :: (t:ntimes RR nscount (t:rr packet))) + (additional-section :: (t:ntimes RR arcount (t:rr packet))) ] (dns-message id qr (value->query-opcode opcode) aa tc rd ra (value->query-response-code rcode) q-section a-section auth-section additional-section)))) -;; DNSMessage -> Bytes +(: dns-message->packet : DNSMessage -> Bytes) ;; Render a Racket structured DNS message using the DNS binary encoding. (define (dns-message->packet m) (bit-string->bytes @@ -191,10 +235,10 @@ ((length (dns-message-answers m)) :: bits 16) ((length (dns-message-authorities m)) :: bits 16) ((length (dns-message-additional m)) :: bits 16) - ((dns-message-questions m) :: (t:ntimes (t:question))) - ((dns-message-answers m) :: (t:ntimes (t:rr))) - ((dns-message-authorities m) :: (t:ntimes (t:rr))) - ((dns-message-additional m) :: (t:ntimes (t:rr)))))) + ((dns-message-questions m) :: (t:ntimes Question (t:question))) + ((dns-message-answers m) :: (t:ntimes RR (t:rr))) + ((dns-message-authorities m) :: (t:ntimes RR (t:rr))) + ((dns-message-additional m) :: (t:ntimes RR (t:rr)))))) ;; Bit-syntax type for a single bit, represented in Racket as one of ;; two possible symbolic values. @@ -228,13 +272,14 @@ ((_ #f val) (encode-domain-name val)))) -;; DomainName -> Bitstring +(: encode-domain-name : DomainName -> BitString) (define (encode-domain-name name) (define labels (domain-labels name)) - (bit-string (labels :: (t:listof (t:pascal-string "Label" 64))) + (bit-string (labels :: (t:listof Bytes (t:pascal-string "Label" 64))) (0 :: integer bytes 1))) ;; end of list of labels! -;; Bytes Bytes ListOf -> ListOf +(: parse-domain-name : + BitString BitString (Listof Natural) -> (Values (Listof Bytes) BitString)) ;; PRECONDITION: input never empty ;; INVARIANT: pointers-followed contains every "jump target" we have ;; jumped to so far during decoding of this domain-name, in order to @@ -273,13 +318,14 @@ ([ len (body :: binary bytes len) (rest :: binary) ] (ks (bit-string->bytes body) rest)) (else (kf)))) - ((_ #f s) - (t:pascal-string #f s "Character-string" 256)) - ((_ #f s string-kind length-limit) - (let ((len (bytes-length s))) - (when (>= len length-limit) - (error 't:pascal-string "~s too long: ~v" string-kind s)) - (bit-string len (s :: binary)))))) + ((_ #f val) + (t:pascal-string #f val "Character-string" 256)) + ((_ #f val string-kind length-limit) + (let: ([s : Bytes val]) + (let ((len (bytes-length s))) + (when (>= len length-limit) + (error 't:pascal-string "~s too long: ~v" string-kind s)) + (bit-string len (s :: binary))))))) ;; ;; The question section is used to carry the "question" in most queries, @@ -314,10 +360,11 @@ (value->qclass qclass) #f) tail)))) - ((_ #f q) - (bit-string ((question-name q) :: (t:domain-name)) - ((qtype->value (question-type q)) :: bits 16) - ((qclass->value (question-class q)) :: bits 16))))) + ((_ #f val) + (let: ([q : Question val]) + (bit-string ((question-name q) :: (t:domain-name)) + ((qtype->value (question-type q)) :: bits 16) + ((qclass->value (question-class q)) :: bits 16)))))) ;; ;; All RRs have the same top level format shown below: @@ -348,43 +395,35 @@ ;; packet because the RR may contain nested domain-names. (define-syntax t:rr (syntax-rules () - ((_ #t input ks kf whole-packet) - (decode-rr whole-packet input ks kf)) - ((_ #f rr) - (encode-rr rr)))) + ((_ #t input ks kf whole-packet0) + (let ((whole-packet whole-packet0)) + (bit-string-case input + ([ (name :: (t:domain-name whole-packet)) + (type-number :: bits 16) + (class :: bits 16) + (ttl :: bits 32) + (rdlength :: bits 16) + (rdata :: binary bytes rdlength) + (tail :: binary) ] + (let ((type (value->type type-number))) + (ks (rr name + type + (value->class class) + ttl + (decode-rdata whole-packet type rdata)) + tail))) + (else (kf))))) + ((_ #f val) + (let: ([rr : RR val]) + (let ((encoded-rdata (encode-rdata (rr-type rr) (rr-rdata rr)))) + (bit-string ((rr-name rr) :: (t:domain-name)) + ((type->value (rr-type rr)) :: bits 16) + ((class->value (rr-class rr)) :: bits 16) + ((rr-ttl rr) :: bits 32) + ((quotient (bit-string-length encoded-rdata) 8) :: bits 16) + (encoded-rdata :: binary))))))) -;; Bytes Bytes (RR Bytes -> A) ( -> A) -> A -;; Helper for t:rr. -(define (decode-rr whole-packet input ks kf) - (bit-string-case input - ([ (name :: (t:domain-name whole-packet)) - (type-number :: bits 16) - (class :: bits 16) - (ttl :: bits 32) - (rdlength :: bits 16) - (rdata :: binary bytes rdlength) - (tail :: binary) ] - (let ((type (value->type type-number))) - (ks (rr name - type - (value->class class) - ttl - (decode-rdata whole-packet type rdata)) - tail))) - (else (kf)))) - -;; RR -> Bitstring -;; Helper for t:rr. -(define (encode-rr rr) - (let ((encoded-rdata (encode-rdata (rr-type rr) (rr-rdata rr)))) - (bit-string ((rr-name rr) :: (t:domain-name)) - ((type->value (rr-type rr)) :: bits 16) - ((class->value (rr-class rr)) :: bits 16) - ((rr-ttl rr) :: bits 32) - ((/ (bit-string-length encoded-rdata) 8) :: bits 16) - (encoded-rdata :: binary)))) - -;; Bytes RRType Bytes -> RData +(: decode-rdata : BitString RRType BitString -> RData) ;; Decode RData according to the RRType. Takes the whole packet for ;; the same reason as t:rr does. (define (decode-rdata whole-packet type rdata) @@ -413,7 +452,7 @@ (minimum :: bits 32) ] (soa mname rname serial refresh retry expire minimum)))) ((txt) (bit-string-case rdata - ([ (strs :: (t:listof (t:pascal-string))) ] + ([ (strs :: (t:listof Bytes (t:pascal-string))) ] strs))) ((a) (bit-string-case rdata ([ a b c d ] @@ -423,7 +462,7 @@ (list->vector (bytes->list (bit-string->bytes ipv6-addr)))))) ((wks) (bit-string-case rdata ([ a b c d protocol (bitmap :: binary) ] - (wks (vector a b c d) protocol bitmap)))) + (wks (vector a b c d) protocol (bit-string->bytes bitmap))))) ((srv) (bit-string-case rdata ([ (priority :: bits 16) (weight :: bits 16) @@ -432,7 +471,7 @@ (srv priority weight port target)))) (else (bit-string->bytes rdata)))) -;; RRType RData -> Bitstring +(: encode-rdata : RRType RData -> BitString) ;; Encode RData according to the RRType. (define (encode-rdata type rdata) (case type @@ -451,7 +490,7 @@ ((soa-retry rdata) :: bits 32) ((soa-expire rdata) :: bits 32) ((soa-minimum rdata) :: bits 32))) - ((txt) (bit-string (rdata :: (t:listof (t:pascal-string))))) + ((txt) (bit-string (rdata :: (t:listof Bytes (t:pascal-string))))) ((a) (match rdata ((vector a b c d) (bit-string a b c d)))) ((aaaa) (bit-string ((list->bytes (vector->list rdata)) :: binary bits 128))) ((wks) (match (wks-address rdata) @@ -464,4 +503,5 @@ (else rdata))) ;; UInt32 +(: max-ttl : Nonnegative-Integer) (define max-ttl #xffffffff) diff --git a/mapping.rkt b/mapping.rkt index 5802654..9301a6b 100644 --- a/mapping.rkt +++ b/mapping.rkt @@ -1,4 +1,4 @@ -#lang racket/base +#lang typed/racket/base ;; Macros for defining weak and extensible mappings between sets of values (provide define-mapping) @@ -13,13 +13,13 @@ ((_ fn bn fd bd (lhs rhs) ...) (begin (define (fn l) - (case l - ((lhs) 'rhs) ... - (else (fd l)))) + (cond + ((eqv? l 'lhs) 'rhs) ... + (else (fd l)))) (define (bn r) - (case r - ((rhs) 'lhs) ... - (else (bd r)))))))) + (cond + ((eqv? r 'rhs) 'lhs) ... + (else (bd r)))))))) ;; Symbol -> raised exn:fail:contract ;; Used by default to complain when no specific mapping is found. diff --git a/tk-dns.rkt b/tk-dns.rkt index 885b941..aa99c8e 100644 --- a/tk-dns.rkt +++ b/tk-dns.rkt @@ -1,11 +1,11 @@ -#lang racket/base +#lang typed/racket/base ;; DNS drivers using racket-typed-matrix. (require racket/set) (require racket/match) (require "codec.rkt") -(require racket-typed-matrix/sugar-untyped) -(require racket-typed-matrix/drivers/udp-untyped) +(require racket-typed-matrix/sugar-typed) +(require racket-typed-matrix/drivers/udp) (provide (struct-out bad-dns-packet) (struct-out dns-request) @@ -14,25 +14,27 @@ dns-write-driver dns-spy) -(struct bad-dns-packet (detail source sink reason) #:prefab) -(struct dns-request (message source sink) #:prefab) -(struct dns-reply (message source sink) #:prefab) +(struct: bad-dns-packet + ([detail : Any] [source : UdpAddress] [sink : UdpAddress] [reason : Symbol]) #:prefab) +(struct: dns-request ([message : DNSMessage] [source : UdpAddress] [sink : UdpAddress]) #:prefab) +(struct: dns-reply ([message : DNSMessage] [source : UdpAddress] [sink : UdpAddress]) #:prefab) (define (dns-read-driver s) - (transition 'no-state + (transition: (void) : Void (at-meta-level - (endpoint #:subscriber (udp-packet-pattern (wild) s (wild)) - [(udp-packet source (== s) #"") - (begin (log-info "Debug dump packet received") - (send-message `(debug-dump)))] - [(udp-packet source (== s) body) - (send-message - (with-handlers ((exn:fail? (lambda (e) - (bad-dns-packet body source s 'unparseable)))) - (define message (packet->dns-message body)) - (case (dns-message-direction message) - ((request) (dns-request message source s)) - ((response) (dns-reply message source s)))))])))) + (endpoint: : Void + #:subscriber (udp-packet-pattern (wild) s (wild)) + [(udp-packet source (== s) #"") + (begin (log-info "Debug dump packet received") + (send-message `(debug-dump)))] + [(udp-packet source (== s) body) + (send-message + (with-handlers ((exn:fail? (lambda (e) + (bad-dns-packet body source s 'unparseable)))) + (define message (packet->dns-message body)) + (case (dns-message-direction message) + ((request) (dns-request message source s)) + ((response) (dns-reply message source s)))))])))) (define (dns-write-driver s) (define (translate message sink) @@ -40,26 +42,31 @@ (send-message (bad-dns-packet message s sink 'unencodable))))) (at-meta-level (send-message (udp-packet s sink (dns-message->packet message)))))) - (transition 'no-state - (endpoint #:subscriber (dns-request (wild) s (wild)) - [(dns-request message (== s) sink) (translate message sink)]) - (endpoint #:subscriber (dns-reply (wild) s (wild)) - [(dns-reply message (== s) sink) (translate message sink)]))) + (transition: (void) : Void + (endpoint: : Void + #:subscriber (dns-request (wild) s (wild)) + [(dns-request message (== s) sink) (translate message sink)]) + (endpoint: : Void + #:subscriber (dns-reply (wild) s (wild)) + [(dns-reply message (== s) sink) (translate message sink)]))) +(: dns-spy : (All (ParentState) -> (Action ParentState))) (define (dns-spy) - (spawn #:child - (transition 'none - (endpoint #:subscriber (wild) #:observer - [(dns-request message source sink) - (begin (log-info (format "DNS: ~v asks ~v ~v~n : ~v" - source sink (dns-message-id message) - (dns-message-questions message))) - (void))] - [(dns-reply message source sink) - (begin (log-info (format "DNS: ~v answers ~v~n : ~v" - source sink - message)) - (void))] - [x - (begin (log-info (format "DNS: ~v" x)) - (void))])))) + (spawn: #:parent : ParentState + #:child : Void + (transition: (void) : Void + (endpoint: : Void + #:subscriber (wild) #:observer + [(dns-request message source sink) + (begin (log-info (format "DNS: ~v asks ~v ~v~n : ~v" + source sink (dns-message-id message) + (dns-message-questions message))) + (void))] + [(dns-reply message source sink) + (begin (log-info (format "DNS: ~v answers ~v~n : ~v" + source sink + message)) + (void))] + [x + (begin (log-info (format "DNS: ~v" x)) + (void))]))))