suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

change redex-check's default strategy to do both

Browse Source 
enumeration and random generation in a manner
supported by our study
This commit is contained in:
Robby Findler 2014-03-26 00:33:38 -05:00
parent 89ef6f831e
commit 494f32084a
3 changed files with 73 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl
View File

@ -2027,8 +2027,15 @@ using the @racket[match-bindings] produced by @racket[match]ing
@math{t} against @racket[pattern]. The form of @racket[template] controls
how @math{t} is generated:
@itemlist[@item{@racket[language @#,ttpattern]:
In this case, @racket[redex-check] randomly generates terms that match
@racket[_pattern].}
In this case, @racket[redex-check] uses an ad hoc strategy for
generating @racket[_pattern]. For the first 10 seconds, it uses
in-order enumeration to pick terms. After that, it
alternates back and forth between in-order enumeration
and the ad hoc random generator. After the 10 minute mark,
it switches over to using just the ad hoc random generator.}
@item{@racket[language @#,ttpattern #:ad-hoc]:
In this case, @racket[redex-check] uses an ad hoc random generator
to generate terms that match @racket[_pattern].}
@item{@racket[language @#,ttpattern #:in-order]:
In this case, @racket[redex-check] uses an enumeration
of @racket[_pattern], checking each @math{t} one at a time}

62
pkgs/redex-pkgs/redex-lib/redex/private/generate-term.rkt
View File

@ -93,6 +93,7 @@
(define-syntax (redex-check stx)
(define valid-kws
(list* '#:satisfying
'#:ad-hoc
'#:enum
'#:uniform-at-random
'#:in-order
@ -126,13 +127,15 @@
[(form lang #:satisfying . rest)
(raise-syntax-error 'redex-check "#:satisfying expected judgment form or metafunction syntax followed by a property" stx #'rest)]
[(form lang pat #:enum biggest-e property . kw-args)
(redex-check/pat stx #'form #'lang #'pat #'property #'biggest-e #f #f #'kw-args)]
(redex-check/pat stx #'form #'lang #'pat #'property #'biggest-e #f #f #f #'kw-args)]
[(form lang pat #:uniform-at-random p-value property . kw-args)
(redex-check/pat stx #'form #'lang #'pat #'property #f #'p-value #f #'kw-args)]
(redex-check/pat stx #'form #'lang #'pat #'property #f #'p-value #f #f #'kw-args)]
[(form lang pat #:in-order property . kw-args)
(redex-check/pat stx #'form #'lang #'pat #'property #f #f #t #'kw-args)]
(redex-check/pat stx #'form #'lang #'pat #'property #f #f #t #f #'kw-args)]
[(form lang pat #:ad-hoc property . kw-args)
(redex-check/pat stx #'form #'lang #'pat #'property #f #f #f #t #'kw-args)]
[(form lang pat property . kw-args)
(redex-check/pat stx #'form #'lang #'pat #'property #f #f #f #'kw-args)]))
(redex-check/pat stx #'form #'lang #'pat #'property #f #f #f #f #'kw-args)]))
(define-struct gen-fail ())
@ -217,7 +220,7 @@
#,keep-going-stx)))))))
(define-for-syntax (redex-check/pat orig-stx form lang pat property
enum-bound-e enum-p-value in-order?
enum-bound-e enum-p-value in-order? ad-hoc?
kw-args)
(with-syntax ([(syncheck-exp pattern (name ...) (name/ellipses ...))
(rewrite-side-conditions/check-errs
@ -290,12 +293,59 @@
(ith-generator #,lang `pattern #,enum-bound-e #,enum-p-value)
property att ret (and print? show) (or fix (λ (x) x)) term-match
keep-going?)]
[else
[ad-hoc?
#`(check-one
#,(term-generator lang #'pattern 'redex-check)
property att ret (and print? show) fix (and fix term-match)
keep-going?)]
[else
#`(check-one
(default-generator #,lang `pattern)
property att ret (and print? show) (or fix (λ (x) x)) term-match
keep-going?)])])))))))
(define (default-generator lang pat)
(define ad-hoc-generator ((compile lang 'redex-check) pat))
(define enum (with-handlers ([exn:fail? (λ (x) #f)])
;; would be better if the pat-enumerator were to
;; return something to indicate failure instead of
;; raising an exception so that bugs in there wouldn't
;; turn into #f here
(pat-enumerator (compiled-lang-enum-table lang) pat)))
(cond
[enum
(define in-bounds (if (= +inf.0 (enum-size enum))
(λ (x) x)
(λ (x) (modulo x (enum-size enum)))))
(define start-time (current-inexact-milliseconds))
(define interleave-start-attempt #f)
(define interleave-time (+ start-time (* 1000 10))) ;; 10 seconds later
(define pure-random-start-attempt #f)
(define pure-random-time (+ start-time (* 1000 60 10))) ;; 10 minutes later
(λ (_size _attempt _retries)
(define now (current-inexact-milliseconds))
(cond
[(<= now interleave-time)
(values (enum-ith enum (in-bounds (- _attempt 1))) 'ignored)]
[(<= now pure-random-time)
(unless interleave-start-attempt (set! interleave-start-attempt _attempt))
(define interleave-attempt (- _attempt interleave-start-attempt))
(cond
[(odd? interleave-attempt)
(ad-hoc-generator _size (/ (- interleave-attempt 1) 2) _retries)]
[else
(define enum-id (in-bounds (+ interleave-start-attempt (/ interleave-attempt 2) -1)))
(values (enum-ith enum enum-id) 'ignored)])]
[else
(unless pure-random-start-attempt (set! pure-random-start-attempt _attempt))
(ad-hoc-generator _size
(+ (- _attempt pure-random-start-attempt)
(quotient (- pure-random-start-attempt pure-random-start-attempt)
2))
_retries)]))]
[else
ad-hoc-generator]))
(define (ith-generator lang pat enum-bound enum-p-value)
(define enum-lang (compiled-lang-enum-table lang))
(define enum (pat-enumerator enum-lang pat))

9
pkgs/redex-pkgs/redex-test/redex/tests/rg-test.rkt
View File

@ -803,7 +803,7 @@
(test (let/ec k
(parameterize ([generation-decisions
(decisions #:nt (list (λ _ (k #t))))])
(redex-check lang d #t #:attempts 1 #:print? #f #:attempt-size add1)
(redex-check lang d #:ad-hoc #t #:attempts 1 #:print? #f #:attempt-size add1)
#f))
#t)
@ -893,6 +893,13 @@
#rx"^redex-check: unable to generate LHS of impossible in 42")))
(test (let ([checked 0])
(redex-check lang n #:ad-hoc (set! checked (add1 checked))
#:print? #f
#:attempts 10)
checked)
10)
(test (let ([checked 0])
(redex-check lang n #:enum 100 (set! checked (add1 checked))
#:print? #f