<commit_before>#lang scribble/base

@(require "cite.rkt"
          "bug-info.rkt"
          scribble/core
          scriblib/figure
          scriblib/footnote
          scribble/manual
          racket/format
          (only-in pict scale))

@title[#:tag "sec:benchmark"]{The Benchmark Models}

The programs in our benchmark come from two sources:
synthetic examples based on our experience with Redex over
the years and from models that we and others
have developed and bugs that were encountered during
the development process.

The benchmark has six different Redex models, each of which
provides a grammar of terms for the model and a soundness
property that is universally quantified over those terms.
Most of the models are of programming languages and most of
the soundness properties are type-soundness, but we also
include red-black trees with the property that insertion
preserves the red-black invariant, as well as one richer
property for one of the programming language models 
(discussed in @secref["sec:b:stlc-sub"]).

For each model, we have manually introduced bugs into a
number of copies of the model, such that each copy is
identical to the correct one, except for a single bug. The bugs
always manifest as a term that falsifies the soundness
property. 

The table in @figure-ref["fig:benchmark-overview"] gives an
overview of the benchmark suite, showing some numbers for
each model and bug. Each model has its name and the number
of lines of code for the bug-free model (the buggy versions
are always within a few lines of the originals). The line
number counts include the model and the specification of the
property.

Each bug has a number and, with the exception of the rvm
model, the numbers count from 1 up to the number of bugs.
The rvm model bugs are all from 
@citet[racket-virtual-machine]'s work and we follow their
numbering scheme (see @secref["sec:b:rvm"] for more
information about how we chose the bugs from that paper).

The @bold{S/M/D/U} column shows a classification of each bug as:
@itemlist[
  @item{@bold{S} (Shallow) Errors in the encoding of the system into Redex,
         due to typos or a misunderstanding of subtleties of Redex.}
  @item{@bold{M} (Medium) Errors in the algorithm behind the
         system, such as using too simple of a data-structure that doesn't
         allow some important distinction, or misunderstanding that some
         rule should have a side-condition that limits its applicability.}
  @item{@bold{D} (Deep) Errors in the developer's understanding of the system, 
         such as when a type system really isn't sound and the author
         doesn't realize it.}
  @item{@bold{U} (Unnatural) Errors that are unlikely to have come up in
         real Redex programs but are included for our own curiosity. There
         are only two bugs in this category.}]

The size column shows the size of the term representing the
smallest counterexample we know for each bug, where we
measure size as the number of pairs of parentheses and atoms
in the s-expression representation of the term.

Each subsection of this section introduces one of the
models in the benchmark, along with the errors we introduced
into each model. 

@figure*["fig:benchmark-overview" "Benchmark Overview"]{
 @centered{
  @tabular[#:sep 
           @hspace[1]
           #:column-properties '(left)
           #:row-properties '((baseline bottom-border) (baseline))
           (cons
            (list @bold{Model}
                  @bold{LoC}
                  @bold{Bug#}
                  @bold{S/M/D/U}
                  @bold{Size}
                  @bold{Description of Bug})
            (let ([last-type #f])
              (for/list ([t/n (in-list all-types/nums)])
                (define type (list-ref t/n 0))
                (define num (list-ref t/n 1))
                (begin0
                  (list (if (equal? last-type type)
                            ""
                            @seclink[(format "sec:b:~a" type)]{@(symbol->string type)})
                        (if (equal? last-type type)
                            ""
                            (format "~a" (get-line-count type)))
                        (number->string num)
                        (symbol->string (get-category type num))
                        (number->string (get-counterexample-size type num))
                        (element (style "ErrorDescriptionBox" '())
                                 (list (get-error type num))))
                  (set! last-type type)))))]
  }
}

@section[#:tag "sec:b:stlc"]{stlc} 
A simply-typed λ-calculus with base
types of numbers and lists of numbers, including the
constants @tt{+}, which operates on numbers, and
@tt{cons}, @tt{head}, @tt{tail}, and @tt{nil} (the empty
list), all of which operate only on lists of numbers. The
property checked is type soundness: the combination of
preservation (if a term has a type and takes a step, then
the resulting term has the same type) and progress (that
well-typed non-values always take a reduction step). 

We introduced nine different bugs into this system. The
first confuses the range and domain types of the function in
the application rule, and has the small counterexample: 
@racket[(hd 0)]. We consider this to be a shallow bug, since
it is essentially a typo and it is hard to imagine anyone
with any knowledge of type systems making this conceptual
mistake. Bug 2 neglects to specify that a fully applied 
@racket[cons] is a value, thus the list 
@racket[((cons 0) nil)] violates the progress property. We
consider this be be a medium bug, as it is not a typo, but
an oversight in the design of a system that is otherwise
correct in its approach.

We consider the next three bugs to be shallow. Bug 3
reverses the range and the domain of function types in the<commit_msg>unbreak redex pdf docs build<commit_after>#lang scribble/base

@(require "cite.rkt"
          "bug-info.rkt"
          scribble/core
          scriblib/figure
          scriblib/footnote
          scribble/manual
          racket/format
          (only-in pict scale))

@title[#:tag "sec:benchmark"]{The Benchmark Models}

The programs in our benchmark come from two sources:
synthetic examples based on our experience with Redex over
the years and from models that we and others
have developed and bugs that were encountered during
the development process.

The benchmark has six different Redex models, each of which
provides a grammar of terms for the model and a soundness
property that is universally quantified over those terms.
Most of the models are of programming languages and most of
the soundness properties are type-soundness, but we also
include red-black trees with the property that insertion
preserves the red-black invariant, as well as one richer
property for one of the programming language models 
(discussed in @secref["sec:b:stlc-sub"]).

For each model, we have manually introduced bugs into a
number of copies of the model, such that each copy is
identical to the correct one, except for a single bug. The bugs
always manifest as a term that falsifies the soundness
property. 

The table in @figure-ref["fig:benchmark-overview"] gives an
overview of the benchmark suite, showing some numbers for
each model and bug. Each model has its name and the number
of lines of code for the bug-free model (the buggy versions
are always within a few lines of the originals). The line
number counts include the model and the specification of the
property.

Each bug has a number and, with the exception of the rvm
model, the numbers count from 1 up to the number of bugs.
The rvm model bugs are all from 
@citet[racket-virtual-machine]'s work and we follow their
numbering scheme (see @secref["sec:b:rvm"] for more
information about how we chose the bugs from that paper).

The @bold{S/M/D/U} column shows a classification of each bug as:
@itemlist[
  @item{@bold{S} (Shallow) Errors in the encoding of the system into Redex,
         due to typos or a misunderstanding of subtleties of Redex.}
  @item{@bold{M} (Medium) Errors in the algorithm behind the
         system, such as using too simple of a data-structure that doesn't
         allow some important distinction, or misunderstanding that some
         rule should have a side-condition that limits its applicability.}
  @item{@bold{D} (Deep) Errors in the developer's understanding of the system, 
         such as when a type system really isn't sound and the author
         doesn't realize it.}
  @item{@bold{U} (Unnatural) Errors that are unlikely to have come up in
         real Redex programs but are included for our own curiosity. There
         are only two bugs in this category.}]

The size column shows the size of the term representing the
smallest counterexample we know for each bug, where we
measure size as the number of pairs of parentheses and atoms
in the s-expression representation of the term.

Each subsection of this section introduces one of the
models in the benchmark, along with the errors we introduced
into each model. 

@figure*["fig:benchmark-overview" "Benchmark Overview"]{
 @centered{
  @tabular[#:sep 
           @hspace[1]
           #:column-properties '(left)
           #:row-properties '((baseline bottom-border) (baseline))
           (cons
            (list @bold{Model}
                  @bold{LoC}
                  @bold{Bug#}
                  @bold{S/M/D/U}
                  @bold{Size}
                  @bold{Description of Bug})
            (let ([last-type #f])
              (for/list ([t/n (in-list all-types/nums)])
                (define type (list-ref t/n 0))
                (define num (list-ref t/n 1))
                (begin0
                  (list (if (equal? last-type type)
                            ""
                            @seclink[(format "sec:b:~a" type)]{@(symbol->string type)})
                        (if (equal? last-type type)
                            ""
                            (format "~a" (get-line-count type)))
                        (number->string num)
                        (symbol->string (get-category type num))
                        (number->string (get-counterexample-size type num))
                        (list (get-error type num)))
                  (set! last-type type)))))]
  }
}

@section[#:tag "sec:b:stlc"]{stlc} 
A simply-typed λ-calculus with base
types of numbers and lists of numbers, including the
constants @tt{+}, which operates on numbers, and
@tt{cons}, @tt{head}, @tt{tail}, and @tt{nil} (the empty
list), all of which operate only on lists of numbers. The
property checked is type soundness: the combination of
preservation (if a term has a type and takes a step, then
the resulting term has the same type) and progress (that
well-typed non-values always take a reduction step). 

We introduced nine different bugs into this system. The
first confuses the range and domain types of the function in
the application rule, and has the small counterexample: 
@racket[(hd 0)]. We consider this to be a shallow bug, since
it is essentially a typo and it is hard to imagine anyone
with any knowledge of type systems making this conceptual
mistake. Bug 2 neglects to specify that a fully applied 
@racket[cons] is a value, thus the list 
@racket[((cons 0) nil)] violates the progress property. We
consider this be be a medium bug, as it is not a typo, but
an oversight in the design of a system that is otherwise
correct in its approach.

We consider the next three bugs to be shallow. Bug 3
reverses the range and the domain of function types in the
{'fraction_non_alphanumeric': 0.07031655422937208, 'fraction_numerical': 0.0015568240788790867, 'mean_word_length': 2.7713633398564905, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 11, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 1, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3872489', 'n_tokens_mistral': 3130, 'n_tokens_neox': 2976, 'n_words': 1520}