/usr/share/doc/racket/redex/benchmark.html

<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"/><title>5&nbsp;Automated Testing Benchmark</title><link rel="stylesheet" type="text/css" href="../scribble.css" title="default"/><link rel="stylesheet" type="text/css" href="../racket.css" title="default"/><link rel="stylesheet" type="text/css" href="figure.css" title="default"/><link rel="stylesheet" type="text/css" href="../manual-style.css" title="default"/><link rel="stylesheet" type="text/css" href="../manual-racket.css" title="default"/><link rel="stylesheet" type="text/css" href="../doc-site.css" title="default"/><script type="text/javascript" src="../scribble-common.js"></script><script type="text/javascript" src="figure.js"></script><script type="text/javascript" src="../manual-racket.js"></script><script type="text/javascript" src="../doc-site.js"></script><script type="text/javascript" src="../local-redirect/local-redirect.js"></script><script type="text/javascript" src="../local-redirect/local-user-redirect.js"></script><!--[if IE 6]><style type="text/css">.SIEHidden { overflow: hidden; }</style><![endif]--></head><body id="doc-racket-lang-org"><div class="tocset"><div class="tocview"><div class="tocviewlist tocviewlisttopspace"><div class="tocviewtitle"><table cellspacing="0" cellpadding="0"><tr><td style="width: 1em;"><a href="javascript:void(0);" title="Expand/Collapse" class="tocviewtoggle" onclick="TocviewToggle(this,&quot;tocview_0&quot;);">&#9660;</a></td><td></td><td><a href="index.html" class="tocviewlink" data-pltdoc="x">Redex:<span class="mywbr"> &nbsp;</span> Practical Semantics Engineering</a></td></tr></table></div><div class="tocviewsublisttop" style="display: block;" id="tocview_0"><table cellspacing="0" cellpadding="0"><tr><td align="right">1&nbsp;</td><td><a href="tutorial.html" class="tocviewlink" data-pltdoc="x">Amb:<span class="mywbr"> &nbsp;</span> A Redex Tutorial</a></td></tr><tr><td align="right">2&nbsp;</td><td><a href="redex2015.html" class="tocviewlink" data-pltdoc="x">Long Tutorial</a></td></tr><tr><td align="right">3&nbsp;</td><td><a href="fri-mor.html" class="tocviewlink" data-pltdoc="x">Extended Exercises</a></td></tr><tr><td align="right">4&nbsp;</td><td><a href="The_Redex_Reference.html" class="tocviewlink" data-pltdoc="x">The Redex Reference</a></td></tr><tr><td align="right">5&nbsp;</td><td><a href="" class="tocviewselflink" data-pltdoc="x">Automated Testing Benchmark</a></td></tr><tr><td align="right"></td><td><a href="doc-bibliography.html" class="tocviewlink" data-pltdoc="x">Bibliography</a></td></tr><tr><td align="right"></td><td><a href="doc-index.html" class="tocviewlink" data-pltdoc="x">Index</a></td></tr></table></div></div><div class="tocviewlist"><table cellspacing="0" cellpadding="0"><tr><td style="width: 1em;"><a href="javascript:void(0);" title="Expand/Collapse" class="tocviewtoggle" onclick="TocviewToggle(this,&quot;tocview_1&quot;);">&#9658;</a></td><td>5&nbsp;</td><td><a href="" class="tocviewselflink" data-pltdoc="x">Automated Testing Benchmark</a></td></tr></table><div class="tocviewsublistbottom" style="display: none;" id="tocview_1"><table cellspacing="0" cellpadding="0"><tr><td align="right">5.1&nbsp;</td><td><a href="#%28part._sec~3abenchmark%29" class="tocviewlink" data-pltdoc="x">The Benchmark Models</a></td></tr><tr><td align="right">5.2&nbsp;</td><td><a href="#%28part._manage%29" class="tocviewlink" data-pltdoc="x">Managing Benchmark Modules</a></td></tr><tr><td align="right">5.3&nbsp;</td><td><a href="#%28part._run%29" class="tocviewlink" data-pltdoc="x">Running Benchmark Models</a></td></tr><tr><td align="right">5.4&nbsp;</td><td><a href="#%28part._log%29" class="tocviewlink" data-pltdoc="x">Logging</a></td></tr><tr><td align="right">5.5&nbsp;</td><td><a href="#%28part._.Plotting%29" class="tocviewlink" data-pltdoc="x">Plotting</a></td></tr><tr><td align="right">5.6&nbsp;</td><td><a href="#%28part._sec~3afinding%29" class="tocviewlink" data-pltdoc="x">Finding the Benchmark Models</a></td></tr></table></div></div></div><div class="tocsub"><div class="tocsubtitle">On this page:</div><table class="tocsublist" cellspacing="0"><tr><td><span class="tocsublinknumber">5.1<tt>&nbsp;</tt></span><a href="#%28part._sec~3abenchmark%29" class="tocsubseclink" data-pltdoc="x">The Benchmark Models</a></td></tr><tr><td><span class="tocsublinknumber">5.1.1<tt>&nbsp;</tt></span><a href="#%28part._sec~3ab~3astlc%29" class="tocsubseclink" data-pltdoc="x">stlc</a></td></tr><tr><td><span class="tocsublinknumber">5.1.2<tt>&nbsp;</tt></span><a href="#%28part._sec~3ab~3apoly-stlc%29" class="tocsubseclink" data-pltdoc="x">poly-<wbr></wbr>stlc</a></td></tr><tr><td><span class="tocsublinknumber">5.1.3<tt>&nbsp;</tt></span><a href="#%28part._sec~3ab~3astlc-sub%29" class="tocsubseclink" data-pltdoc="x">stlc-<wbr></wbr>sub</a></td></tr><tr><td><span class="tocsublinknumber">5.1.4<tt>&nbsp;</tt></span><a href="#%28part._sec~3ab~3alet-poly%29" class="tocsubseclink" data-pltdoc="x">let-<wbr></wbr>poly</a></td></tr><tr><td><span class="tocsublinknumber">5.1.5<tt>&nbsp;</tt></span><a href="#%28part._sec~3ab~3alist-machine%29" class="tocsubseclink" data-pltdoc="x">list-<wbr></wbr>machine</a></td></tr><tr><td><span class="tocsublinknumber">5.1.6<tt>&nbsp;</tt></span><a href="#%28part._sec~3ab~3arbtrees%29" class="tocsubseclink" data-pltdoc="x">rbtrees</a></td></tr><tr><td><span class="tocsublinknumber">5.1.7<tt>&nbsp;</tt></span><a href="#%28part._sec~3ab~3adelim-cont%29" class="tocsubseclink" data-pltdoc="x">delim-<wbr></wbr>cont</a></td></tr><tr><td><span class="tocsublinknumber">5.1.8<tt>&nbsp;</tt></span><a href="#%28part._sec~3ab~3arvm%29" class="tocsubseclink" data-pltdoc="x">rvm</a></td></tr><tr><td><span class="tocsublinknumber">5.2<tt>&nbsp;</tt></span><a href="#%28part._manage%29" class="tocsubseclink" data-pltdoc="x">Managing Benchmark Modules</a></td></tr><tr><td><a href="#%28form._%28%28lib._redex%2Fbenchmark..rkt%29._define-rewrite%29%29" class="tocsubnonseclink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">define-<wbr></wbr>rewrite</span></span></a></td></tr><tr><td><a href="#%28form._%28%28lib._redex%2Fbenchmark..rkt%29._define-rewrite%2Fcompose%29%29" class="tocsubnonseclink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">define-<wbr></wbr>rewrite/<span class="mywbr"> &nbsp;</span>compose</span></span></a></td></tr><tr><td><a href="#%28form._%28%28lib._redex%2Fbenchmark..rkt%29._include%2Frewrite%29%29" class="tocsubnonseclink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">include/<span class="mywbr"> &nbsp;</span>rewrite</span></span></a></td></tr><tr><td><span class="tocsublinknumber">5.3<tt>&nbsp;</tt></span><a href="#%28part._run%29" class="tocsubseclink" data-pltdoc="x">Running Benchmark Models</a></td></tr><tr><td><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-gen-and-check%29%29" class="tocsubnonseclink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">run-<wbr></wbr>gen-<wbr></wbr>and-<wbr></wbr>check</span></span></a></td></tr><tr><td><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-results%29%29" class="tocsubnonseclink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">run-<wbr></wbr>results</span></span></a></td></tr><tr><td><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-gen-and-check%2Fmods%29%29" class="tocsubnonseclink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">run-<wbr></wbr>gen-<wbr></wbr>and-<wbr></wbr>check/<span class="mywbr"> &nbsp;</span>mods</span></span></a></td></tr><tr><td><span class="tocsublinknumber">5.4<tt>&nbsp;</tt></span><a href="#%28part._log%29" class="tocsubseclink" data-pltdoc="x">Logging</a></td></tr><tr><td><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._bmark-log-data%29%29" class="tocsubnonseclink" data-pltdoc="x"><span class="RktSym">bmark-<wbr></wbr>log-<wbr></wbr>data</span></a></td></tr><tr><td><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._benchmark-logging-to%29%29" class="tocsubnonseclink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">benchmark-<wbr></wbr>logging-<wbr></wbr>to</span></span></a></td></tr><tr><td><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._bmark-log-directory%29%29" class="tocsubnonseclink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">bmark-<wbr></wbr>log-<wbr></wbr>directory</span></span></a></td></tr><tr><td><span class="tocsublinknumber">5.5<tt>&nbsp;</tt></span><a href="#%28part._.Plotting%29" class="tocsubseclink" data-pltdoc="x">Plotting</a></td></tr><tr><td><span class="tocsublinknumber">5.6<tt>&nbsp;</tt></span><a href="#%28part._sec~3afinding%29" class="tocsubseclink" data-pltdoc="x">Finding the Benchmark Models</a></td></tr><tr><td><a href="#%28def._%28%28lib._redex%2Fbenchmark%2Fmodels%2Fall-info..rkt%29._all-mods%29%29" class="tocsubnonseclink" data-pltdoc="x"><span class="RktSym">all-<wbr></wbr>mods</span></a></td></tr></table></div></div><div class="maincolumn"><div class="main"><div class="navsettop"><span class="navleft"><form class="searchform"><input class="searchbox" style="color: #888;" type="text" value="...search manuals..." title="Enter a search string to search the manuals" onkeypress="return DoSearchKey(event, this, &quot;6.3&quot;, &quot;../&quot;);" onfocus="this.style.color=&quot;black&quot;; this.style.textAlign=&quot;left&quot;; if (this.value == &quot;...search manuals...&quot;) this.value=&quot;&quot;;" onblur="if (this.value.match(/^ *$/)) { this.style.color=&quot;#888&quot;; this.style.textAlign=&quot;center&quot;; this.value=&quot;...search manuals...&quot;; }"/></form>&nbsp;&nbsp;<a href="../index.html" title="up to the documentation top" data-pltdoc="x" onclick="return GotoPLTRoot(&quot;6.3&quot;);">top</a></span><span class="navright">&nbsp;&nbsp;<a href="The_Redex_Reference.html" title="backward to &quot;4 The Redex Reference&quot;" data-pltdoc="x">&larr; prev</a>&nbsp;&nbsp;<a href="index.html" title="up to &quot;Redex: Practical Semantics Engineering&quot;" data-pltdoc="x">up</a>&nbsp;&nbsp;<a href="doc-bibliography.html" title="forward to &quot;Bibliography&quot;" data-pltdoc="x">next &rarr;</a></span>&nbsp;</div><h3 x-source-module="(lib &quot;redex/redex.scrbl&quot;)" x-source-pkg="redex-doc" x-part-tag="&quot;benchmark&quot;">5<tt>&nbsp;</tt><a name="(part._benchmark)"></a><a name="(mod-path._redex/benchmark)"></a>Automated Testing Benchmark</h3><p><table cellspacing="0" cellpadding="0" class="defmodule"><tr><td align="left"><span class="hspace">&nbsp;</span><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=require.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fbase..rkt%2529._require%2529%2529&amp;version=6.3" class="RktStxLink Sq" data-pltdoc="x">require</a></span><span class="stt"> </span><a href="" class="RktModLink" data-pltdoc="x"><span class="RktSym">redex/benchmark</span></a><span class="RktPn">)</span></td><td align="right"><span class="RpackageSpec"><span class="Smaller">&nbsp;package:</span> <span class="stt">redex-benchmark</span></span></td></tr></table></p><p>Redex&rsquo;s automated testing benchmark provides a collection
of buggy models and falsifiable properties to test how
efficiently methods of automatic test case generation are
able to find counterexamples for the bugs.</p><p>Each entry in the benchmark contains a <a name="(tech._check)"></a><span style="font-style: italic">check</span> function
and multiple <a name="(tech._generate)"></a><span style="font-style: italic">generate</span> functions. The <a href="#%28tech._check%29" class="techoutside" data-pltdoc="x"><span class="techinside">check</span></a> function
determines if a given example is a counterexample (i.e. if
it uncovers the buggy behavior) and each of the <a href="#%28tech._generate%29" class="techoutside" data-pltdoc="x"><span class="techinside">generate</span></a>
functions generates candidate examples to be tried. There are multiple
ways to generate terms for each model. They typically correspond to different
uses of <span class="RktSym">generate-term</span>, but could be any way to generate examples.
See <span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-gen-and-check%29%29" class="RktValLink" data-pltdoc="x">run-gen-and-check</a></span> for the precise contracts for <a href="#%28tech._generate%29" class="techoutside" data-pltdoc="x"><span class="techinside">generate</span></a>
and <a href="#%28tech._check%29" class="techoutside" data-pltdoc="x"><span class="techinside">check</span></a> functions.</p><p>Most of the entries in the benchmark are small differences to existing,
bug-free models, where some small change to the model introduces the
bug. These changes are described using <span class="RktSym"><a href="#%28form._%28%28lib._redex%2Fbenchmark..rkt%29._define-rewrite%29%29" class="RktStxLink" data-pltdoc="x">define-rewrite</a></span>.</p><p>To run a benchmark entry with a particular generator, see <span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-gen-and-check%2Fmods%29%29" class="RktValLink" data-pltdoc="x">run-gen-and-check/mods</a></span>.</p><h4 x-source-module="(lib &quot;redex/redex.scrbl&quot;)" x-source-pkg="redex-doc" x-part-tag="&quot;sec:benchmark&quot;">5.1<tt>&nbsp;</tt><a name="(part._sec~3abenchmark)"></a>The Benchmark Models</h4><p>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.</p><p>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 <a href="#%28part._sec~3ab~3astlc-sub%29" data-pltdoc="x">stlc-sub</a>).</p><p>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.</p><p>The table in <a href="#%28counter._%28figure._fig~3abenchmark-overview%29%29" data-pltdoc="x">figure&nbsp;<span class="FigureRef">1</span></a> 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.</p><p>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
<a href="doc-bibliography.html#%28autobib._.Casey._.Klein%2C._.Robert._.Bruce._.Findler%2C._and._.Matthew._.Flatt.The._.Racket._virtual._machine._and._randomized._testing.Higher-.Order._and._.Symbolic._.Computation2013http~3a%2F%2Fplt..eecs..northwestern..edu%2Fracket-machine%2F%29" data-pltdoc="x">Klein et al.</a>&nbsp;(<a href="doc-bibliography.html#%28autobib._.Casey._.Klein%2C._.Robert._.Bruce._.Findler%2C._and._.Matthew._.Flatt.The._.Racket._virtual._machine._and._randomized._testing.Higher-.Order._and._.Symbolic._.Computation2013http~3a%2F%2Fplt..eecs..northwestern..edu%2Fracket-machine%2F%29" data-pltdoc="x">2013</a>)&rsquo;s work and we follow their
numbering scheme (see <a href="#%28part._sec~3ab~3arvm%29" data-pltdoc="x">rvm</a> for more
information about how we chose the bugs from that paper).</p><p><div class="SIntrapara">The <span style="font-weight: bold">S/M/D/U</span> column shows a classification of each bug as:
</div><div class="SIntrapara"><ul><li><p><span style="font-weight: bold">S</span> (Shallow) Errors in the encoding of the system into Redex,
 due to typos or a misunderstanding of subtleties of Redex.</p></li><li><p><span style="font-weight: bold">M</span> (Medium) Errors in the algorithm behind the
 system, such as using too simple of a data-structure that doesn&rsquo;t
 allow some important distinction, or misunderstanding that some
 rule should have a side-condition that limits its applicability.</p></li><li><p><span style="font-weight: bold">D</span> (Deep) Errors in the developer&rsquo;s understanding of the system,
 such as when a type system really isn&rsquo;t sound and the author
 doesn&rsquo;t realize it.</p></li><li><p><span style="font-weight: bold">U</span> (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.</p></li></ul></div></p><p>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.</p><p>Each subsection of this section introduces one of the
models in the benchmark, along with the errors we introduced
into each model.</p><blockquote class="FigureMulti"><blockquote class="Centerfigure"><blockquote class="FigureInside"><blockquote class="SCentered"><table cellspacing="0" cellpadding="0" style="border-collapse: collapse;"><tr><td align="left" valign="baseline" style="border-bottom: 1px solid black;"><p><span style="font-weight: bold">Model</span></p></td><td align="left" valign="baseline" style="border-bottom: 1px solid black;"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline" style="border-bottom: 1px solid black;"><p><span style="font-weight: bold">LoC</span></p></td><td align="left" valign="baseline" style="border-bottom: 1px solid black;"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline" style="border-bottom: 1px solid black;"><p><span style="font-weight: bold">Bug#</span></p></td><td align="left" valign="baseline" style="border-bottom: 1px solid black;"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline" style="border-bottom: 1px solid black;"><p><span style="font-weight: bold">S/M/D/U</span></p></td><td align="left" valign="baseline" style="border-bottom: 1px solid black;"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline" style="border-bottom: 1px solid black;"><p><span style="font-weight: bold">Size</span></p></td><td align="left" valign="baseline" style="border-bottom: 1px solid black;"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline" style="border-bottom: 1px solid black;"><p><span style="font-weight: bold">Description of Bug</span></p></td></tr><tr><td align="left" valign="baseline"><p><a href="#%28part._sec~3ab~3astlc%29" data-pltdoc="x">stlc</a></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>211</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>1</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>S</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>3</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>app rule the range of the function is matched to the argument</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>2</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>M</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>5</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>the ((cons v) v) value has been omitted</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>3</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>S</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>8</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>the order of the types in the function position of application has been swapped</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>4</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>S</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>9</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>the type of cons is incorrect</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>5</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>S</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>7</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>the tail reduction returns the wrong value</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>6</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>M</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>7</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>hd reduction acts on partially applied cons</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>7</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>M</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>9</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>evaluation isn't allowed on the rhs of applications</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>8</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>U</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>12</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>lookup always returns int</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>9</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>S</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>15</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>variables aren't required to match in lookup</p></td></tr><tr><td align="left" valign="baseline"><p><a href="#%28part._sec~3ab~3apoly-stlc%29" data-pltdoc="x">poly-stlc</a></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>277</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>1</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>S</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>6</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>app rule the range of the function is matched to the argument</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>2</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>M</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>11</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>the (([cons @ &#964;] v) v) value has been omitted</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>3</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>S</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>14</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>the order of the types in the function position of application has been swapped</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>4</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>S</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>15</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>the type of cons is incorrect</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>5</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>S</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>16</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>the tail reduction returns the wrong value</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>6</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>M</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>16</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>hd reduction acts on partially applied cons</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>7</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>M</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>9</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>evaluation isn't allowed on the rhs of applications</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>8</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>U</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>15</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>lookup always returns int</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>9</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>S</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>18</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>variables aren't required to match in lookup</p></td></tr><tr><td align="left" valign="baseline"><p><a href="#%28part._sec~3ab~3astlc-sub%29" data-pltdoc="x">stlc-sub</a></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>241</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>1</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>S</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>8</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>forgot the variable case</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>2</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>S</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>13</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>wrong order of arguments to replace call</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>3</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>S</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>10</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>swaps function and argument position in application</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>4</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>D</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>22</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>variable not fresh enough</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>5</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>SM</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>17</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>replace all variables</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>6</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>S</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>8</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>forgot the variable case</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>7</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>S</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>13</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>wrong order of arguments to replace call</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>8</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>S</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>10</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>swaps function and argument position in application</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>9</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>SM</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>17</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>replace all variables</p></td></tr><tr><td align="left" valign="baseline"><p><a href="#%28part._sec~3ab~3alet-poly%29" data-pltdoc="x">let-poly</a></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>640</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>1</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>S</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>8</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>use a lambda-bound variable where a type variable should have been</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>2</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>D</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>28</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>the classic polymorphic let + references bug</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>3</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>M</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>3</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>mix up types in the function case</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>4</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>S</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>8</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>misspelled the name of a metafunction in a side-condition, causing the occurs check to not happen</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>5</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>M</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>3</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>eliminate-G was written as if it always gets a Gx as input</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>6</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>M</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>6</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>&#8744; has an incorrect duplicated variable, leading to an uncovered case</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>7</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>D</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>12</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>used let --&gt; left-left-&#955; rewrite rule for let, but the right-hand side is less polymorphic</p></td></tr><tr><td align="left" valign="baseline"><p><a href="#%28part._sec~3ab~3alist-machine%29" data-pltdoc="x">list-machine</a></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>256</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>1</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>S</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>22</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>confuses the lhs value for the rhs value in cons type rule</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>2</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>M</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>22</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>var-set may skip a var with matching id (in reduction)</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>3</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>S</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>29</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>cons doesn't actually update the store</p></td></tr><tr><td align="left" valign="baseline"><p><a href="#%28part._sec~3ab~3arbtrees%29" data-pltdoc="x">rbtrees</a></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>187</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>1</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>M</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>13</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>ins does no rebalancing</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>2</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>M</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>15</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>the first case is removed from balance</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>3</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>S</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>51</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>doesn't increment black depth in non-empty case</p></td></tr><tr><td align="left" valign="baseline"><p><a href="#%28part._sec~3ab~3adelim-cont%29" data-pltdoc="x">delim-cont</a></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>287</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>1</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>M</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>46</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>guarded mark reduction doesn't wrap results with a list/c</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>2</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>M</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>25</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>list/c contracts aren't applied properly in the cons case</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>3</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>S</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>52</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>the function argument to call/comp has the wrong type</p></td></tr><tr><td align="left" valign="baseline"><p><a href="#%28part._sec~3ab~3arvm%29" data-pltdoc="x">rvm</a></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>712</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>2</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>M</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>24</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>stack offset / pointer confusion</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>3</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>D</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>33</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>application slots not initialized properly</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>4</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>M</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>17</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>mishandling branches when then branch needs more stack than else branch; bug in the boxenv case not checking a stack bound</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>5</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>M</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>23</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>mishandling branches when then branch needs more stack than else branch; bug in the let-rec case not checking a stack bound</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>6</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>M</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>15</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>forgot to implement the case-lam branch in verifier</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>14</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>M</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>27</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>certain updates to initialized slots could break optimizer assumptions</p></td></tr><tr><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p></p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>15</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>S</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>21</p></td><td align="left" valign="baseline"><p><span class="hspace">&nbsp;</span></p></td><td align="left" valign="baseline"><p>neglected to restrict case-lam to accept only 'val' arguments</p></td></tr></table></blockquote></blockquote></blockquote><p class="Centertext"><span class="Legend"><span class="FigureTarget"><a name="(counter._(figure._fig~3abenchmark-overview))" x-target-lift="Figure"></a>Figure&nbsp;1: </span>Benchmark Overview</span></p></blockquote><h5 x-source-module="(lib &quot;redex/redex.scrbl&quot;)" x-source-pkg="redex-doc" x-part-tag="&quot;sec:b:stlc&quot;">5.1.1<tt>&nbsp;</tt><a name="(part._sec~3ab~3astlc)"></a>stlc</h5><p>A simply-typed &#955;-calculus with base
types of numbers and lists of numbers, including the
constants <span class="stt">+</span>, which operates on numbers, and
<span class="stt">cons</span>, <span class="stt">head</span>, <span class="stt">tail</span>, and <span class="stt">nil</span> (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).</p><p>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:
<span class="RktPn">(</span><span class="RktSym">hd</span><span class="stt"> </span><span class="RktVal">0</span><span class="RktPn">)</span>. 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
<span class="RktSym">cons</span> is a value, thus the list
<span class="RktPn">(</span><span class="RktPn">(</span><span class="RktSym">cons</span><span class="stt"> </span><span class="RktVal">0</span><span class="RktPn">)</span><span class="stt"> </span><span class="RktSym">nil</span><span class="RktPn">)</span> 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.</p><p>We consider the next three bugs to be shallow. Bug 3
reverses the range and the domain of function types in the
type judgment for applications. This was one of the easiest
bug for all of our approaches to find. Bug 4 assigns
<span class="RktSym">cons</span> a result type of <span class="RktSym">int</span>. The fifth bug
returns the head of a list when <span class="RktSym">tl</span> is applied. Bug
6 only applies the <span class="RktSym">hd</span> constant to a partially
constructed list (i.e., the term <span class="RktPn">(</span><span class="RktSym">cons</span><span class="stt"> </span><span class="RktVal">0</span><span class="RktPn">)</span> instead
of <span class="RktPn">(</span><span class="RktPn">(</span><span class="RktSym">cons</span><span class="stt"> </span><span class="RktVal">0</span><span class="RktPn">)</span><span class="stt"> </span><span class="RktSym">nil</span><span class="RktPn">)</span>). Only the grammar based random
generation exposed bugs 5 and 6 and none of our approaches
exposed bug 4.</p><p>The seventh bug, also classified as medium, omits a production
from the definition of evaluation contexts and thus doesn&rsquo;t reduce
the right-hand-side of function applications.</p><p>Bug 8 always returns the type <span class="RktSym">int</span> when looking up
a variable&rsquo;s type in the context. This bug (and the identical one
in the next system) are the only bugs we classify as unnatural. We
included it because it requires a program to have a variable with
a type that is more complex that just <span class="RktSym">int</span> and to actually
use that variable somehow.</p><p>Bug 9 is simple; the variable lookup function has an error where it
doesn&rsquo;t actually compare its input to variable in the environment,
so it effectively means that each variable has the type of the nearest
enclosing lambda expression.</p><h5 x-source-module="(lib &quot;redex/redex.scrbl&quot;)" x-source-pkg="redex-doc" x-part-tag="&quot;sec:b:poly-stlc&quot;">5.1.2<tt>&nbsp;</tt><a name="(part._sec~3ab~3apoly-stlc)"></a>poly-stlc</h5><p>This is a polymorphic version of <a href="#%28part._sec~3ab~3astlc%29" data-pltdoc="x">stlc</a>, with
a single numeric base type, polymorphic lists, and polymorphic
versions of the list constants.
No changes were made to the model except those necessary to
make the list operations polymorphic.
There is no type inference in the model, so all polymorphic
terms are required to be instantiated with the correct
types in order for the function to type check.
Of course, this makes it much more difficult to automatically
generate well-typed terms, and thus counterexamples.
As with <span style="font-weight: bold">stlc</span>, the property checked is
type soundness.</p><p>All of the bugs in this system are identical to those in
<span style="font-weight: bold">stlc</span>, aside from any changes that had to be made
to translate them to this model.</p><p>This model is also a subset of the language specified in
<a href="doc-bibliography.html#%28autobib._.Micha~c5~82._.H..._.Pa~c5~82ka%2C._.Koen._.Claessen%2C._.Alejandro._.Russo%2C._and._.John._.Hughes.Testing._an._.Optimising._.Compiler._by._.Generating._.Random._.Lambda._.Terms.In._.Proc..._.International._.Workshop._on._.Automation._of._.Software._.Test2011http~3a%2F%2Fdl..acm..org%2Fcitation..cfm~3fid~3d1982615%29" data-pltdoc="x">Pa&#322;ka et al.</a>&nbsp;(<a href="doc-bibliography.html#%28autobib._.Micha~c5~82._.H..._.Pa~c5~82ka%2C._.Koen._.Claessen%2C._.Alejandro._.Russo%2C._and._.John._.Hughes.Testing._an._.Optimising._.Compiler._by._.Generating._.Random._.Lambda._.Terms.In._.Proc..._.International._.Workshop._on._.Automation._of._.Software._.Test2011http~3a%2F%2Fdl..acm..org%2Fcitation..cfm~3fid~3d1982615%29" data-pltdoc="x">2011</a>), who used a specialized and optimized
QuickCheck generator for a similar type system to find bugs
in GHC. We adapted this system (and its restriction in
<span style="font-weight: bold">stlc</span>) because it has already been used successfully
with random testing, which makes it a reasonable target for
an automated testing benchmark.</p><h5 x-source-module="(lib &quot;redex/redex.scrbl&quot;)" x-source-pkg="redex-doc" x-part-tag="&quot;sec:b:stlc-sub&quot;">5.1.3<tt>&nbsp;</tt><a name="(part._sec~3ab~3astlc-sub)"></a>stlc-sub</h5><p>The same language and type system as <a href="#%28part._sec~3ab~3astlc%29" data-pltdoc="x">stlc</a>,
except that in this case all of the errors are in the substitution
function.</p><p>Our own experience has been that it is easy to make subtle
errors when writing substitution functions, so we added this
set of tests specifically to target them with the benchmark.
There are two soundness checks for this system. Bugs 1-5 are
checked in the following way: given a candidate
counterexample, if it type checks, then all &#946;v-redexes in
the term are reduced (but not any new ones that might
appear) using the buggy substitution function to get a second
term. Then, these two terms are checked to see if they both
still type check and have the same type and that the result
of passing both to the evaluator is the same.</p><p>Bugs 4-9 are checked using type soundness for this system as
specified in the discussion of the <a href="#%28part._sec~3ab~3astlc%29" data-pltdoc="x">stlc</a> model. We
included two predicates for this system because we believe
the first to be a good test for a substitution function but
not something that a typical Redex user would write, while
the second is something one would see in most Redex models
but is less effective at catching bugs in the substitution
function.</p><p>The first substitution bug we introduced simply omits the
case that replaces the correct variable with the
term to be substituted. We considered this to be a shallow
error, and indeed all approaches were able to uncover it,
although the time it took to do so varied.</p><p>Bug 2 permutes the order of arguments when making a
recursive call. This is also categorized as a shallow bug,
although it is a common one, at least  based on our
experience writing substitutions in Redex.</p><p>Bug 3 swaps the function and argument positions of
an application while recurring, again essentially a typo and
a shallow error, although one of the more difficult to
find in this model.</p><p>The fourth substitution bug neglects to make the renamed
bound variable fresh enough when recurring past a
lambda. Specifically, it ensures that the new variable is
not one that appears in the body of the function, but it
fails to make sure that the variable is different from the
bound variable or the substituted variable. We categorized
this error as deep because it corresponds to a
misunderstanding of how to generate fresh variables, a
central concern of the substitution function.</p><p>Bug 5 carries out the substitution for all variables in the
term, not just the given variable. We categorized it as SM,
since it is essentially a missing side condition, although a
fairly egregious one.</p><p>Bugs 6-9 are duplicates of bugs 1-3 and bug 5, except that
they are tested with type soundness instead. (It is
impossible to detect bug 4 with this property.)</p><h5 x-source-module="(lib &quot;redex/redex.scrbl&quot;)" x-source-pkg="redex-doc" x-part-tag="&quot;sec:b:let-poly&quot;">5.1.4<tt>&nbsp;</tt><a name="(part._sec~3ab~3alet-poly)"></a>let-poly</h5><p>A language with ML-style <span class="stt">let</span> polymorphism, included in
the benchmark to explore the difficulty of finding the
classic let+references unsoundness. With the exception of
the classic bug, all of the bugs were errors made during
the development of this model (and that were caught during
development).</p><p>The first bug is simple; it corresponds to a typo, swapping
an <span class="stt">x</span> for a <span class="stt">y</span> in a rule such that a type variable
is used as a program variable.</p><p>Bug number 2 is the classic let+references bug. It changes the rule
for <span class="stt">let</span>-bound variables in such a way that generalization
is allowed even when the initial value expression is not a value.</p><p>Bug number 3 is an error in the function application case where the
wrong types are used for the function position (swapping two types
in the rule).</p><p>Bugs 4, 5, and 6 were errors in the definition of the unification
function that led to various bad behaviors.</p><p>Finally, bug 7 is a bug that was introduced early on, but was only
caught late in the development process of the model. It used a
rewriting rule for <span class="stt">let</span> expressions that simply reduced them
to the corresponding <span class="stt">((&#955;</span> expressions. This has the correct
semantics for evaluation, but the statement of type-soundness does not
work with this rewriting rule because the let expression has more
polymorphism that the corresponding application expression.</p><h5 x-source-module="(lib &quot;redex/redex.scrbl&quot;)" x-source-pkg="redex-doc" x-part-tag="&quot;sec:b:list-machine&quot;">5.1.5<tt>&nbsp;</tt><a name="(part._sec~3ab~3alist-machine)"></a>list-machine</h5><p> An implementation of
<a href="doc-bibliography.html#%28autobib._.Andrew._.W..._.Appel%2C._.Robert._.Dockins%2C._and._.Xavier._.Leroy.A._list-machine._benchmark._for._mechanized._metatheory.Journal._of._.Automated._.Reasoning._49%283%29%2C._pp..._453--4912012http~3a%2F%2Fwww..cs..princeton..edu%2F~7eappel%2Flistmachine%2F%29" data-pltdoc="x">Appel et al.</a>&nbsp;(<a href="doc-bibliography.html#%28autobib._.Andrew._.W..._.Appel%2C._.Robert._.Dockins%2C._and._.Xavier._.Leroy.A._list-machine._benchmark._for._mechanized._metatheory.Journal._of._.Automated._.Reasoning._49%283%29%2C._pp..._453--4912012http~3a%2F%2Fwww..cs..princeton..edu%2F~7eappel%2Flistmachine%2F%29" data-pltdoc="x">2012</a>)&rsquo;s list-machine benchmark. This is a
reduction semantics (as a pointer machine operating over an
instruction pointer and a store) and a type system for a
seven-instruction first-order assembly language that
manipulates <span class="stt">cons</span> and <span class="stt">nil</span> values. The property
checked is type soundness as specified in
<a href="doc-bibliography.html#%28autobib._.Andrew._.W..._.Appel%2C._.Robert._.Dockins%2C._and._.Xavier._.Leroy.A._list-machine._benchmark._for._mechanized._metatheory.Journal._of._.Automated._.Reasoning._49%283%29%2C._pp..._453--4912012http~3a%2F%2Fwww..cs..princeton..edu%2F~7eappel%2Flistmachine%2F%29" data-pltdoc="x">Appel et al.</a>&nbsp;(<a href="doc-bibliography.html#%28autobib._.Andrew._.W..._.Appel%2C._.Robert._.Dockins%2C._and._.Xavier._.Leroy.A._list-machine._benchmark._for._mechanized._metatheory.Journal._of._.Automated._.Reasoning._49%283%29%2C._pp..._453--4912012http~3a%2F%2Fwww..cs..princeton..edu%2F~7eappel%2Flistmachine%2F%29" data-pltdoc="x">2012</a>), namely that well-typed programs always
step or halt. Three mutations are included.</p><p>The first list-machine bug incorrectly uses the head position
of a cons pair where it should use the tail position in the
cons typing rule. This bug amounts to a typo and is classified
as simple.</p><p>The second bug is a missing side-condition in the rule that updates
the store that has the effect of updating the first position in
the store instead of the proper position in the store for
all of the store update operations. We classify this as a medium bug.</p><p>The final list-machine bug is a missing subscript in one rule
that has the effect that the list cons operator does not store
its result. We classify this as a simple bug.</p><h5 x-source-module="(lib &quot;redex/redex.scrbl&quot;)" x-source-pkg="redex-doc" x-part-tag="&quot;sec:b:rbtrees&quot;">5.1.6<tt>&nbsp;</tt><a name="(part._sec~3ab~3arbtrees)"></a>rbtrees</h5><p> A model that implements the red-black
tree insertion function and checks that insertion preserves
the red-black tree invariant (and that the red-black tree is
a binary search tree).</p><p>The first bug simply removes the re-balancing operation from
insert. We classified this bug as medium since it seems like
the kind of mistake that a developer might make in staging
the implementation. That is, the re-balancing operation is separate
and so might be put off initially, but then forgotten.</p><p>The second bug misses one situation in the re-balancing
operation, namely when a black node has two red nodes under
it, with the second red node to the right of the first. This
is a medium bug.</p><p>The third bug is in the function that counts the black depth in
the red-black tree predicate. It forgets to increment the count
in one situation. This is a simple bug.</p><h5 x-source-module="(lib &quot;redex/redex.scrbl&quot;)" x-source-pkg="redex-doc" x-part-tag="&quot;sec:b:delim-cont&quot;">5.1.7<tt>&nbsp;</tt><a name="(part._sec~3ab~3adelim-cont)"></a>delim-cont</h5><p><a href="doc-bibliography.html#%28autobib._.Asumu._.Takikawa%2C._.T..._.Stephen._.Strickland%2C._and._.Sam._.Tobin-.Hochstadt.Constraining._.Delimited._.Control._with._.Contracts.In._.Proc..._.European._.Symposium._on._.Programming%2C._pp..._229--2482013http~3a%2F%2Fdl..acm..org%2Fcitation..cfm~3fid~3d2450287%29" data-pltdoc="x">Takikawa et al.</a>&nbsp;(<a href="doc-bibliography.html#%28autobib._.Asumu._.Takikawa%2C._.T..._.Stephen._.Strickland%2C._and._.Sam._.Tobin-.Hochstadt.Constraining._.Delimited._.Control._with._.Contracts.In._.Proc..._.European._.Symposium._on._.Programming%2C._pp..._229--2482013http~3a%2F%2Fdl..acm..org%2Fcitation..cfm~3fid~3d2450287%29" data-pltdoc="x">2013</a>)&rsquo;s model of a contract and type system for
delimited control. The language
is Plotkin&rsquo;s PCF extended with operators for delimited continuations,
continuation marks, and contracts for those operations.
The property checked is type soundness. We added three bugs
to this model.</p><p>The first was a bug we found by mining the model&rsquo;s
git repository&rsquo;s history. This bug fails to put a list
contract around the result of extracting the marks from a
continuation, which has the effect of checking the contract
that is supposed to be on the elements of a list against the
list itself instead. We classify this as a medium bug.</p><p>The second bug was in the rule for handling list contracts. When checking
a contract against a cons pair, the rule didn&rsquo;t specify that it should
apply only when the contract is actually a list contract, meaning
that the cons rule would be used even on non-list contacts, leading
to strange contract checking. We consider this a medium bug because
the bug manifests itself as a missing <span class="RktSym">list/c</span> in the rule.</p><p>The last bug in this model makes a mistake in the typing
rule for the continuation operator. The mistake is to leave
off one-level of arrows, something that is easy to do with
so many nested arrow types, as continuations tend to have.
We classify this as a simple error.</p><h5 x-source-module="(lib &quot;redex/redex.scrbl&quot;)" x-source-pkg="redex-doc" x-part-tag="&quot;sec:b:rvm&quot;">5.1.8<tt>&nbsp;</tt><a name="(part._sec~3ab~3arvm)"></a>rvm</h5><p> A existing model and test
framework for the Racket virtual machine and bytecode
verifier&nbsp;(<a href="doc-bibliography.html#%28autobib._.Casey._.Klein%2C._.Robert._.Bruce._.Findler%2C._and._.Matthew._.Flatt.The._.Racket._virtual._machine._and._randomized._testing.Higher-.Order._and._.Symbolic._.Computation2013http~3a%2F%2Fplt..eecs..northwestern..edu%2Fracket-machine%2F%29" data-pltdoc="x">Klein et al.</a> <a href="doc-bibliography.html#%28autobib._.Casey._.Klein%2C._.Robert._.Bruce._.Findler%2C._and._.Matthew._.Flatt.The._.Racket._virtual._machine._and._randomized._testing.Higher-.Order._and._.Symbolic._.Computation2013http~3a%2F%2Fplt..eecs..northwestern..edu%2Fracket-machine%2F%29" data-pltdoc="x">2013</a>). The bugs were
discovered during the development of the model and reported
in section 7 of that paper. Unlike the rest of the models,
we do not number the bugs for this model sequentially but instead
use the numbers from <a href="doc-bibliography.html#%28autobib._.Casey._.Klein%2C._.Robert._.Bruce._.Findler%2C._and._.Matthew._.Flatt.The._.Racket._virtual._machine._and._randomized._testing.Higher-.Order._and._.Symbolic._.Computation2013http~3a%2F%2Fplt..eecs..northwestern..edu%2Fracket-machine%2F%29" data-pltdoc="x">Klein et al.</a>&nbsp;(<a href="doc-bibliography.html#%28autobib._.Casey._.Klein%2C._.Robert._.Bruce._.Findler%2C._and._.Matthew._.Flatt.The._.Racket._virtual._machine._and._randomized._testing.Higher-.Order._and._.Symbolic._.Computation2013http~3a%2F%2Fplt..eecs..northwestern..edu%2Fracket-machine%2F%29" data-pltdoc="x">2013</a>)&rsquo;s work.</p><p><div class="SIntrapara">We included only some of the bugs, excluding bugs for two
reasons:
</div><div class="SIntrapara"><ul><li><p>The paper tests two properties: an internal
soundness property that relates the verifier to the
virtual machine model, and an external property that
relates the verifier model to the verifier implementation.
We did not include any that require the latter properties because it
requires building a complete, buggy version of the Racket
runtime system to include in the benchmark.</p></li><li><p>We included all of the internal properties
except those numbered 1 and 7 for practical reasons. The
first is the only bug in the machine model, as opposed to
just the verifier, which would have required us to
include the entire VM model in the benchmark. The second
would have required modifying the abstract representation
of the stack in the verifier model in contorted way to
mimic a more C-like implementation of a global, imperative
stack. This bug was originally in the C implementation of
the verifier (not the Redex model) and to replicate it in
the Redex-based verifier model would require us to program
in a low-level imperative way in the Redex model,
something not easily done.</p></li></ul></div></p><p>These bugs are described in detail in <a href="doc-bibliography.html#%28autobib._.Casey._.Klein%2C._.Robert._.Bruce._.Findler%2C._and._.Matthew._.Flatt.The._.Racket._virtual._machine._and._randomized._testing.Higher-.Order._and._.Symbolic._.Computation2013http~3a%2F%2Fplt..eecs..northwestern..edu%2Fracket-machine%2F%29" data-pltdoc="x">Klein et al.</a>&nbsp;(<a href="doc-bibliography.html#%28autobib._.Casey._.Klein%2C._.Robert._.Bruce._.Findler%2C._and._.Matthew._.Flatt.The._.Racket._virtual._machine._and._randomized._testing.Higher-.Order._and._.Symbolic._.Computation2013http~3a%2F%2Fplt..eecs..northwestern..edu%2Fracket-machine%2F%29" data-pltdoc="x">2013</a>)&rsquo;s paper.</p><p>This model is unique in our benchmark suite because it
includes a function that makes terms more likely to be
useful test cases. In more detail, the machine model does
not have variables, but instead is stack-based; bytecode
expressions also contain internal pointers that must be
valid. Generating a random (or in-order) term is relatively
unlikely to produce one that satisfies these constraints.
For example, of the first 10,000 terms produced by
the in-order enumeration only 1625 satisfy the constraints.
The ad hoc random generator generators produces about 900
good terms in 10,000 attempts and the uniform random
generator produces about 600 in 10,000 attempts.</p><p>To make terms more likely to be good test cases, this
model includes a function that looks for out-of-bounds
stack offsets and bogus internal pointers and replaces
them with random good values. This function is applied
to each of the generated terms before using them to test
the model.</p><h4 x-source-module="(lib &quot;redex/redex.scrbl&quot;)" x-source-pkg="redex-doc" x-part-tag="&quot;manage&quot;">5.2<tt>&nbsp;</tt><a name="(part._manage)"></a>Managing Benchmark Modules</h4><p>This section describes utilities for making changes to existing modules to
create new ones, intended to assist in adding bugs to models and keeping
buggy models in sync with changes to the original model.</p><blockquote class="SVInsetFlow"><table cellspacing="0" cellpadding="0" class="boxed RBoxed"><tr><td><blockquote class="SubFlow"><div class="RBackgroundLabel SIEHidden"><div class="RBackgroundLabelInner"><p>syntax</p></div></div><table cellspacing="0" cellpadding="0" class="RktBlk RForeground"><tr><td><span class="RktPn">(</span><a name="(form._((lib._redex/benchmark..rkt)._define-rewrite))"></a><span title="Provided from: redex/benchmark | Package: redex-benchmark"><span class="RktSym"><a href="#%28form._%28%28lib._redex%2Fbenchmark..rkt%29._define-rewrite%29%29" class="RktStxDef RktStxLink" data-pltdoc="x">define-rewrite</a></span></span><span class="hspace">&nbsp;</span><span class="RktVar">id</span><span class="hspace">&nbsp;</span><span class="RktVar">from</span><span class="hspace">&nbsp;</span><span class="RktSym">==&gt;</span><span class="hspace">&nbsp;</span><span class="RktVar">to</span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;</span><span class="RktPn">[</span><span class="RktPn">#:context</span><span class="hspace">&nbsp;</span><span class="RktPn">(</span><span class="RktVar">context-id</span><span class="hspace">&nbsp;</span><span class="RktMeta">...</span><span class="RktPn">)</span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;&nbsp;</span><span class="RktPn">#:variables</span><span class="hspace">&nbsp;</span><span class="RktPn">(</span><span class="RktVar">variable-id</span><span class="hspace">&nbsp;</span><span class="RktMeta">...</span><span class="RktPn">)</span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;&nbsp;</span><span class="RktPn">#:once-only</span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;&nbsp;</span><span class="RktPn">#:exactly-once</span><span class="RktPn">]</span><span class="RktPn">)</span></td></tr></table></blockquote></td></tr></table></blockquote><p>Defines a syntax transformer bound to <span class="RktSym">id</span>, the effect of which is
to rewrite syntax matching the pattern <span class="RktSym">from</span> to the result
expression <span class="RktSym">to</span>. The <span class="RktSym">from</span> argument should follow the
grammar of a <span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=stx-patterns.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fstxcase-scheme..rkt%2529._syntax-case%2529%2529&amp;version=6.3" class="RktStxLink Sq" data-pltdoc="x">syntax-case</a></span> pattern, and <span class="RktSym">to</span> acts
as the corresponding result expression. The behavior of the match is the
same as <span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=stx-patterns.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fstxcase-scheme..rkt%2529._syntax-case%2529%2529&amp;version=6.3" class="RktStxLink Sq" data-pltdoc="x">syntax-case</a></span>, except that all identifiers in
<span class="RktSym">from</span> are treated as literals with the exception of an identifier
that has the same binding as a <span class="RktSym">variable-id</span> appearing in the
<span class="RktPn">#:variables</span> keyword argument, which is treated
as a pattern variable. (The reverse of the situation for
<span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=stx-patterns.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fstxcase-scheme..rkt%2529._syntax-case%2529%2529&amp;version=6.3" class="RktStxLink Sq" data-pltdoc="x">syntax-case</a></span>, where literals must be specified instead.)
The rewrite will only be applied in the context of a <span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=module.html%23%2528form._%2528%2528quote._%7E23%7E25kernel%2529._module%2529%2529&amp;version=6.3" class="RktStxLink Sq" data-pltdoc="x">module</a></span> form,
but it will be applied wherever possible within the module body,
subject to a few constraints.</p><p>The rest of the keyword arguments control where and how often the
rewrite may be applied. The <span class="RktPn">#:once-only</span> option specifies that the
rewrite can be applied no more than once, and the <span class="RktPn">#:exactly-once</span>
option asserts that the rewrite must be applied once (and no more). In both
cases a syntax error is raised if the condition is not met. The
<span class="RktPn">#:context</span> option searches for syntax of the form
<span class="RktPn">(</span><span class="RktSym">some-id</span><span class="stt"> </span><span class="RktPn">. </span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=pairs.html%23%2528def._%2528%2528lib._racket%252Flist..rkt%2529._rest%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">rest</a></span><span class="RktPn">)</span>, where the binding of <span class="RktSym">some-id</span>
matches that of the first <span class="RktSym">context-id</span> in the <span class="RktPn">#:context</span> list,
at which point it recurs on <span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=pairs.html%23%2528def._%2528%2528lib._racket%252Flist..rkt%2529._rest%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">rest</a></span> but drops the first id from the
list. Once every <span class="RktSym">context-id</span> has been matched, the
rewrite can be applied.</p><p><div class="SIntrapara"><blockquote class="SVInsetFlow"><table cellspacing="0" cellpadding="0" class="boxed RBoxed"><tr><td><blockquote class="SubFlow"><div class="RBackgroundLabel SIEHidden"><div class="RBackgroundLabelInner"><p>syntax</p></div></div><p class="RForeground"><span class="RktPn">(</span><a name="(form._((lib._redex/benchmark..rkt)._define-rewrite/compose))"></a><span title="Provided from: redex/benchmark | Package: redex-benchmark"><span class="RktSym"><a href="#%28form._%28%28lib._redex%2Fbenchmark..rkt%29._define-rewrite%2Fcompose%29%29" class="RktStxDef RktStxLink" data-pltdoc="x">define-rewrite/compose</a></span></span><span class="hspace">&nbsp;</span><span class="RktVar">id</span><span class="hspace">&nbsp;</span><span class="RktVar">rw-id</span><span class="hspace">&nbsp;</span><span class="RktMeta">...</span><span class="RktPn">)</span></p></blockquote></td></tr></table></blockquote></div><div class="SIntrapara">Defines a syntax transformer bound to <span class="RktSym">id</span>, assuming that
every <span class="RktSym">rw-id</span> also binds a syntax transformer, such that <span class="RktSym">id</span>
has the effect of applying all of the <span class="RktSym">rw-id</span>s.</div></p><p><div class="SIntrapara"><blockquote class="SVInsetFlow"><table cellspacing="0" cellpadding="0" class="boxed RBoxed"><tr><td><blockquote class="SubFlow"><div class="RBackgroundLabel SIEHidden"><div class="RBackgroundLabelInner"><p>syntax</p></div></div><p class="RForeground"><span class="RktPn">(</span><a name="(form._((lib._redex/benchmark..rkt)._include/rewrite))"></a><span title="Provided from: redex/benchmark | Package: redex-benchmark"><span class="RktSym"><a href="#%28form._%28%28lib._redex%2Fbenchmark..rkt%29._include%2Frewrite%29%29" class="RktStxDef RktStxLink" data-pltdoc="x">include/rewrite</a></span></span><span class="hspace">&nbsp;</span><span class="RktVar">path-spec</span><span class="hspace">&nbsp;</span><span class="RktVar">mod-id</span><span class="hspace">&nbsp;</span><span class="RktVar">rw-id</span><span class="hspace">&nbsp;</span><span class="RktMeta">...</span><span class="RktPn">)</span></p></blockquote></td></tr></table></blockquote></div><div class="SIntrapara">If the syntax designated by <span class="RktSym">path-spec</span> is a module, the module syntax
is inlined as a submodule with the identifier <span class="RktSym">mod-id</span>. Assumes each
<span class="RktSym">rw-id</span> binds a syntax transformer, and applies them to the resulting
module syntax. The syntax of <span class="RktSym">path-spec</span> must be same as for
<span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=include.html%23%2528form._%2528%2528lib._racket%252Finclude..rkt%2529._include%2529%2529&amp;version=6.3" class="RktStxLink Sq" data-pltdoc="x">include</a></span>.</div></p><p><div class="SIntrapara">For example, if the contents of the file mod-fx.rkt are:
</div><div class="SIntrapara"><blockquote class="SCodeFlow"><blockquote class="Rfilebox"><p class="Rfiletitle"><span class="Rfilename"><span class="stt">"mod-fx.rkt"</span></span></p><blockquote class="Rfilecontent"><table cellspacing="0" cellpadding="0" class="RktBlk"><tr><td><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=guide&amp;rel=Module_Syntax.html%23%2528part._hash-lang%2529&amp;version=6.3" class="RktModLink Sq" data-pltdoc="x"><span class="RktMod">#lang</span></a><span class="hspace">&nbsp;</span><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=index.html&amp;version=6.3" class="RktModLink Sq" data-pltdoc="x"><span class="RktSym">racket/base</span></a></td></tr><tr><td><span class="hspace">&nbsp;</span></td></tr><tr><td><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=require.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fbase..rkt%2529._provide%2529%2529&amp;version=6.3" class="RktStxLink Sq" data-pltdoc="x">provide</a></span><span class="hspace">&nbsp;</span><span class="RktSym">f</span><span class="RktPn">)</span></td></tr><tr><td><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=define.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fbase..rkt%2529._define%2529%2529&amp;version=6.3" class="RktStxLink Sq" data-pltdoc="x">define</a></span><span class="hspace">&nbsp;</span><span class="RktSym">x</span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">X!</span><span class="RktPn">)</span></td></tr><tr><td><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=define.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fbase..rkt%2529._define%2529%2529&amp;version=6.3" class="RktStxLink Sq" data-pltdoc="x">define</a></span><span class="hspace">&nbsp;</span><span class="RktPn">(</span><span class="RktSym">f</span><span class="hspace">&nbsp;</span><span class="RktSym">x</span><span class="RktPn">)</span><span class="hspace">&nbsp;</span><span class="RktSym">x</span><span class="RktPn">)</span></td></tr></table></blockquote></blockquote></blockquote></div><div class="SIntrapara">Then:
</div><div class="SIntrapara"><blockquote class="SCodeFlow"><table cellspacing="0" cellpadding="0" class="RktBlk"><tr><td><table cellspacing="0" cellpadding="0" class="RktBlk"><tr><td><span class="stt">&gt; </span><span class="RktPn">(</span><span class="RktSym"><a href="#%28form._%28%28lib._redex%2Fbenchmark..rkt%29._define-rewrite%29%29" class="RktStxLink" data-pltdoc="x">define-rewrite</a></span><span class="hspace">&nbsp;</span><span class="RktSym">xy-rw</span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;</span><span class="hspace">&nbsp;&nbsp;</span><span class="RktSym">x</span><span class="hspace">&nbsp;</span><span class="RktSym">==&gt;</span><span class="hspace">&nbsp;</span><span class="RktSym">y</span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;</span><span class="hspace">&nbsp;&nbsp;</span><span class="RktPn">#:context</span><span class="hspace">&nbsp;</span><span class="RktPn">(</span><span class="RktSym">f</span><span class="RktPn">)</span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;</span><span class="hspace">&nbsp;&nbsp;</span><span class="RktPn">#:once-only</span><span class="RktPn">)</span></td></tr></table></td></tr><tr><td><table cellspacing="0" cellpadding="0"><tr><td></td></tr></table></td></tr><tr><td><span class="stt">&gt; </span><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=require.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fbase..rkt%2529._require%2529%2529&amp;version=6.3" class="RktStxLink Sq" data-pltdoc="x">require</a></span><span class="hspace">&nbsp;</span><span class="RktVal">"mod-fx.rkt"</span><span class="RktPn">)</span></td></tr><tr><td><table cellspacing="0" cellpadding="0"><tr><td></td></tr></table></td></tr><tr><td><span class="stt">&gt; </span><span class="RktPn">(</span><span class="RktSym">f</span><span class="hspace">&nbsp;</span><span class="RktVal">3</span><span class="RktPn">)</span></td></tr><tr><td><p><span class="RktRes">3</span></p></td></tr><tr><td><span class="stt">&gt; </span><span class="RktPn">(</span><span class="RktSym"><a href="#%28form._%28%28lib._redex%2Fbenchmark..rkt%29._include%2Frewrite%29%29" class="RktStxLink" data-pltdoc="x">include/rewrite</a></span><span class="hspace">&nbsp;</span><span class="RktVal">"mod-fx.rkt"</span><span class="hspace">&nbsp;</span><span class="RktSym">submod-fx</span><span class="hspace">&nbsp;</span><span class="RktSym">xy-rw</span><span class="RktPn">)</span></td></tr><tr><td><table cellspacing="0" cellpadding="0"><tr><td></td></tr></table></td></tr><tr><td><span class="stt">&gt; </span><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=require.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fbase..rkt%2529._require%2529%2529&amp;version=6.3" class="RktStxLink Sq" data-pltdoc="x">require</a></span><span class="hspace">&nbsp;</span><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=require.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fbase..rkt%2529._prefix-in%2529%2529&amp;version=6.3" class="RktStxLink Sq" data-pltdoc="x">prefix-in</a></span><span class="hspace">&nbsp;</span><span class="RktSym">s:</span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">submod-fx</span><span class="RktPn">)</span><span class="RktPn">)</span></td></tr><tr><td><table cellspacing="0" cellpadding="0"><tr><td></td></tr></table></td></tr><tr><td><span class="stt">&gt; </span><span class="RktPn">(</span><span class="RktSym">s:f</span><span class="hspace">&nbsp;</span><span class="RktVal">3</span><span class="RktPn">)</span></td></tr><tr><td><p><span class="RktRes">'X!</span></p></td></tr></table></blockquote></div></p><h4 x-source-module="(lib &quot;redex/redex.scrbl&quot;)" x-source-pkg="redex-doc" x-part-tag="&quot;run&quot;">5.3<tt>&nbsp;</tt><a name="(part._run)"></a>Running Benchmark Models</h4><p><div class="SIntrapara"><blockquote class="SVInsetFlow"><table cellspacing="0" cellpadding="0" class="boxed RBoxed"><tr><td><blockquote class="SubFlow"><div class="RBackgroundLabel SIEHidden"><div class="RBackgroundLabelInner"><p>procedure</p></div></div><table cellspacing="0" cellpadding="0" class="prototype RForeground"><tr><td valign="top"><span class="RktPn">(</span><a name="(def._((lib._redex/benchmark..rkt)._run-gen-and-check))"></a><span title="Provided from: redex/benchmark | Package: redex-benchmark"><span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-gen-and-check%29%29" class="RktValDef RktValLink" data-pltdoc="x">run-gen-and-check</a></span></span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="RktVar">get-gen</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td></tr><tr><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="RktVar">check</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td></tr><tr><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="RktVar">seconds</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td></tr><tr><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span>[</td><td valign="top"><span class="RktPn">#:name</span><span class="hspace">&nbsp;</span><span class="RktVar">name</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td></tr><tr><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="RktPn">#:type</span><span class="hspace">&nbsp;</span><span class="RktVar">type</span>]<span class="RktPn">)</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top">&rarr;</td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-results~3f%29%29" class="RktValLink" data-pltdoc="x">run-results?</a></span></td></tr></table></blockquote></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;</span><span class="RktVar">get-gen</span><span class="hspace">&nbsp;</span>:<span class="hspace">&nbsp;</span><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=function-contracts.html%23%2528form._%2528%2528lib._racket%252Fcontract%252Fbase..rkt%2529._-%7E3e%2529%2529&amp;version=6.3" class="RktStxLink Sq" data-pltdoc="x"><span class="nobreak">-&gt;</span></a></span><span class="hspace">&nbsp;</span><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=function-contracts.html%23%2528form._%2528%2528lib._racket%252Fcontract%252Fbase..rkt%2529._-%7E3e%2529%2529&amp;version=6.3" class="RktStxLink Sq" data-pltdoc="x"><span class="nobreak">-&gt;</span></a></span><span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=data-structure-contracts.html%23%2528def._%2528%2528lib._racket%252Fcontract%252Fprivate%252Fmisc..rkt%2529._any%252Fc%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">any/c</a></span><span class="RktPn">)</span><span class="RktPn">)</span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;</span><span class="RktVar">check</span><span class="hspace">&nbsp;</span>:<span class="hspace">&nbsp;</span><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=function-contracts.html%23%2528form._%2528%2528lib._racket%252Fcontract%252Fbase..rkt%2529._-%7E3e%2529%2529&amp;version=6.3" class="RktStxLink Sq" data-pltdoc="x"><span class="nobreak">-&gt;</span></a></span><span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=data-structure-contracts.html%23%2528def._%2528%2528lib._racket%252Fcontract%252Fprivate%252Fmisc..rkt%2529._any%252Fc%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">any/c</a></span><span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=booleans.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._boolean%7E3f%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">boolean?</a></span><span class="RktPn">)</span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;</span><span class="RktVar">seconds</span><span class="hspace">&nbsp;</span>:<span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=data-structure-contracts.html%23%2528def._%2528%2528lib._racket%252Fcontract%252Fprivate%252Fmisc..rkt%2529._natural-number%252Fc%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">natural-number/c</a></span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;</span><span class="RktVar">name</span><span class="hspace">&nbsp;</span>:<span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=strings.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._string%7E3f%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">string?</a></span><span class="hspace">&nbsp;</span>=<span class="hspace">&nbsp;</span><span class="RktVal">"unknown"</span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;</span><span class="RktVar">type</span><span class="hspace">&nbsp;</span>:<span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=symbols.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._symbol%7E3f%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">symbol?</a></span><span class="hspace">&nbsp;</span>=<span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">unknown</span></td></tr></table></blockquote></div><div class="SIntrapara">Repeatedly <a href="#%28tech._generate%29" class="techoutside" data-pltdoc="x"><span class="techinside">generate</span></a>s random terms and <a href="#%28tech._check%29" class="techoutside" data-pltdoc="x"><span class="techinside">check</span></a>s if they are counterexamples
to some property defined by <span class="RktVar">check</span>, where a term is considered a counterexample
if <span class="RktVar">check</span> returns <span class="RktVal">#f</span> for that term.</div></p><p>The <span class="RktVar">get-gen</span> thunk is called to build a generator of random terms
(which may close over some state). A new generator is created each time the property
is found to be false.</p><p>Each <a href="#%28tech._generate%29" class="techoutside" data-pltdoc="x"><span class="techinside">generate</span></a>d term is passed to <span class="RktVar">check</span> to see if it is a counterexample.
The interval in milliseconds between counterexamples is
tracked, and the process is repeated either until the time specified by
<span class="RktVar">seconds</span> has elapsed or the standard error in the average interval
between counterexamples is less than 10% of the average.</p><p>The result is an instance of <span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-results%29%29" class="RktValLink" data-pltdoc="x">run-results</a></span> containing the total number of
terms <a href="#%28tech._generate%29" class="techoutside" data-pltdoc="x"><span class="techinside">generate</span></a>d, the total elapsed time, and the number of counterexamples found.
More detailed information can be obtained using the benchmark logging facilities,
for which <span class="RktVar">name</span> is refers to the name of the model, and <span class="RktVar">type</span>
is a symbol indicating the generation type used.</p><p><div class="SIntrapara"><blockquote class="SVInsetFlow"><table cellspacing="0" cellpadding="0" class="boxed RBoxed"><tr><td><blockquote class="SubFlow"><div class="RBackgroundLabel SIEHidden"><div class="RBackgroundLabelInner"><p>struct</p></div></div><p class="RForeground"><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=define-struct.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fbase..rkt%2529._struct%2529%2529&amp;version=6.3" class="RktStxLink Sq" data-pltdoc="x">struct</a></span><span class="stt"> </span><a name="(def._((lib._redex/benchmark..rkt)._run-results-cexps))"></a><a name="(def._((lib._redex/benchmark..rkt)._run-results-time))"></a><a name="(def._((lib._redex/benchmark..rkt)._run-results-tries))"></a><a name="(def._((lib._redex/benchmark..rkt)._run-results~3f))"></a><a name="(def._((lib._redex/benchmark..rkt)._struct~3arun-results))"></a><a name="(def._((lib._redex/benchmark..rkt)._run-results))"></a><span title="Provided from: redex/benchmark | Package: redex-benchmark"><span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-results%29%29" class="RktValDef RktValLink" data-pltdoc="x">run-results</a></span></span><span class="stt"> </span><span class="RktPn">(</span><span class="RktSym">tries</span><span class="stt"> </span><span class="RktSym">time</span><span class="stt"> </span><span class="RktSym">cexps</span><span class="RktPn">)</span><span class="RktPn">)</span></p></blockquote></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;</span><span class="RktSym">tries</span><span class="hspace">&nbsp;</span>:<span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=data-structure-contracts.html%23%2528def._%2528%2528lib._racket%252Fcontract%252Fprivate%252Fmisc..rkt%2529._natural-number%252Fc%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">natural-number/c</a></span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;</span><span class="RktSym">time</span><span class="hspace">&nbsp;</span>:<span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=data-structure-contracts.html%23%2528def._%2528%2528lib._racket%252Fcontract%252Fprivate%252Fmisc..rkt%2529._natural-number%252Fc%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">natural-number/c</a></span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;</span><span class="RktSym">cexps</span><span class="hspace">&nbsp;</span>:<span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=data-structure-contracts.html%23%2528def._%2528%2528lib._racket%252Fcontract%252Fprivate%252Fmisc..rkt%2529._natural-number%252Fc%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">natural-number/c</a></span></td></tr></table></blockquote></div><div class="SIntrapara">Minimal results for one run of a <a href="#%28tech._generate%29" class="techoutside" data-pltdoc="x"><span class="techinside">generate</span></a> and <a href="#%28tech._check%29" class="techoutside" data-pltdoc="x"><span class="techinside">check</span></a> pair.</div></p><p><div class="SIntrapara"><blockquote class="SVInsetFlow"><table cellspacing="0" cellpadding="0" class="boxed RBoxed"><tr><td><blockquote class="SubFlow"><div class="RBackgroundLabel SIEHidden"><div class="RBackgroundLabelInner"><p>procedure</p></div></div><table cellspacing="0" cellpadding="0" class="prototype RForeground"><tr><td valign="top"><span class="RktPn">(</span><a name="(def._((lib._redex/benchmark..rkt)._run-gen-and-check/mods))"></a><span title="Provided from: redex/benchmark | Package: redex-benchmark"><span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-gen-and-check%2Fmods%29%29" class="RktValDef RktValLink" data-pltdoc="x">run-gen-and-check/mods</a></span></span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="RktVar">gen-mod-path</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td></tr><tr><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="RktVar">check-mod-path</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td></tr><tr><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="RktVar">seconds</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span></td></tr><tr><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="hspace">&nbsp;</span>[</td><td valign="top"><span class="RktPn">#:name</span><span class="hspace">&nbsp;</span><span class="RktVar">name</span>]<span class="RktPn">)</span></td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top">&rarr;</td><td valign="top"><span class="hspace">&nbsp;</span></td><td valign="top"><span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-results~3f%29%29" class="RktValLink" data-pltdoc="x">run-results?</a></span></td></tr></table></blockquote></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;</span><span class="RktVar">gen-mod-path</span><span class="hspace">&nbsp;</span>:<span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=Module_Names_and_Loading.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._module-path%7E3f%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">module-path?</a></span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;</span><span class="RktVar">check-mod-path</span><span class="hspace">&nbsp;</span>:<span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=Module_Names_and_Loading.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._module-path%7E3f%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">module-path?</a></span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;</span><span class="RktVar">seconds</span><span class="hspace">&nbsp;</span>:<span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=data-structure-contracts.html%23%2528def._%2528%2528lib._racket%252Fcontract%252Fprivate%252Fmisc..rkt%2529._natural-number%252Fc%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">natural-number/c</a></span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;</span><span class="RktVar">name</span><span class="hspace">&nbsp;</span>:<span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=strings.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._string%7E3f%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">string?</a></span><span class="hspace">&nbsp;</span>=<span class="hspace">&nbsp;</span><span class="RktVal">"unknown"</span></td></tr></table></blockquote></div><div class="SIntrapara">Just like <span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-gen-and-check%29%29" class="RktValLink" data-pltdoc="x">run-gen-and-check</a></span>, except that <span class="RktVar">gen-mod-path</span> and
<span class="RktVar">check-mod-path</span> are module paths to a <span style="font-style: italic">generator module</span> and a
<span style="font-style: italic">check module</span>, which are assumed to have the following characteristics:
</div><div class="SIntrapara"><ul><li><p>A <span style="font-style: italic">generator module</span> provides the function <span class="RktSym">get-generator</span>,
  which meets the specification for the <span class="RktSym">get-gen</span> argument to
  <span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-gen-and-check%29%29" class="RktValLink" data-pltdoc="x">run-gen-and-check</a></span>, and <span class="RktSym">type</span>, which is a symbol
  designating the type of the generator.</p></li><li><p>A <span style="font-style: italic">check module</span> provides the function <span class="RktSym">check</span>, which meets
  the specification for the <span class="RktSym">check</span> argument to
  <span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-gen-and-check%29%29" class="RktValLink" data-pltdoc="x">run-gen-and-check</a></span>.</p></li></ul></div></p><h4 x-source-module="(lib &quot;redex/redex.scrbl&quot;)" x-source-pkg="redex-doc" x-part-tag="&quot;log&quot;">5.4<tt>&nbsp;</tt><a name="(part._log)"></a>Logging</h4><p><div class="SIntrapara"><blockquote class="SVInsetFlow"><table cellspacing="0" cellpadding="0" class="boxed RBoxed"><tr><td><blockquote class="SubFlow"><div class="RBackgroundLabel SIEHidden"><div class="RBackgroundLabelInner"><p>struct</p></div></div><p class="RForeground"><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=define-struct.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fbase..rkt%2529._struct%2529%2529&amp;version=6.3" class="RktStxLink Sq" data-pltdoc="x">struct</a></span><span class="stt"> </span><a name="(def._((lib._redex/benchmark..rkt)._bmark-log-data-data))"></a><a name="(def._((lib._redex/benchmark..rkt)._bmark-log-data~3f))"></a><a name="(def._((lib._redex/benchmark..rkt)._struct~3abmark-log-data))"></a><a name="(def._((lib._redex/benchmark..rkt)._bmark-log-data))"></a><span title="Provided from: redex/benchmark | Package: redex-benchmark"><span class="RktSym"><span class="RktSymDef RktSym">bmark-log-data</span></span></span><span class="stt"> </span><span class="RktPn">(</span><span class="RktSym">data</span><span class="RktPn">)</span><span class="RktPn">)</span></p></blockquote></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;</span><span class="RktSym">data</span><span class="hspace">&nbsp;</span>:<span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=data-structure-contracts.html%23%2528def._%2528%2528lib._racket%252Fcontract%252Fprivate%252Fmisc..rkt%2529._any%252Fc%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">any/c</a></span></td></tr></table></blockquote></div><div class="SIntrapara">Contains data logged by the benchmark, as described below.</div></p><p>Detailed information gathered during a benchmark run is logged to the <span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=logging.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._current-logger%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">current-logger</a></span>,
at the <span class="RktVal">'</span><span class="RktVal">info</span> level, with the message <span class="RktVal">"BENCHMARK-LOGGING"</span>. The
<span class="RktSym">data</span> field of the log message contains a <span class="RktSym">bmark-log-data</span> struct, which
wraps data of the form:</p><p><table cellspacing="0" cellpadding="0"><tr><td align="right" valign="baseline"><span class="hspace">&nbsp;&nbsp;</span><span class="RktVar">log-data</span></td><td align="left" valign="baseline"><span class="stt">&nbsp;</span></td><td align="center" valign="baseline">=</td><td align="left" valign="baseline"><span class="stt">&nbsp;</span></td><td align="left" valign="baseline"><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=pairs.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._list%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">list</a></span><span class="hspace">&nbsp;</span><span class="RktVar">event</span><span class="hspace">&nbsp;</span><span class="RktVar">timestamp</span><span class="hspace">&nbsp;</span><span class="RktVar">data-list</span><span class="RktPn">)</span></td></tr></table></p><p>Where <span class="RktSym">event</span> is a symbol that designates the type of event, and
<span class="RktSym">timestamp</span> is symbol that contains the <span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=time.html%23%2528def._%2528%2528lib._racket%252Fdate..rkt%2529._current-date%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">current-date</a></span> of the event in
ISO-8601 format.
The information in <span class="RktSym">data-list</span> depends on the event, but must be in the form
of a list alternating between a keyword and a datum, where the keyword is a short description
of the datum.</p><p><div class="SIntrapara">The following events are logged (the symbol designating the event is in parentheses, and
the form of the data logged for each event is shown):
</div><div class="SIntrapara"><ul><li><p><div class="SIntrapara">Run starts (<span class="RktVal">'</span><span class="RktVal">start</span>), logged when beginning a run with a new
            <a href="#%28tech._generate%29" class="techoutside" data-pltdoc="x"><span class="techinside">generate</span></a>/<a href="#%28tech._check%29" class="techoutside" data-pltdoc="x"><span class="techinside">check</span></a> pair.
</div><div class="SIntrapara"><table cellspacing="0" cellpadding="0"><tr><td align="right" valign="baseline"><span class="hspace">&nbsp;&nbsp;</span><span class="RktVar">data-list</span></td><td align="left" valign="baseline"><span class="stt">&nbsp;</span></td><td align="center" valign="baseline">=</td><td align="left" valign="baseline"><span class="stt">&nbsp;</span></td><td align="left" valign="baseline"><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=pairs.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._list%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">list</a></span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:model</span><span class="hspace">&nbsp;</span><span class="RktVar">model</span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:type</span><span class="hspace">&nbsp;</span><span class="RktVar">gen</span><span class="RktPn">)</span></td></tr></table></div></p></li><li><p><div class="SIntrapara">Run completions (<span class="RktVal">'</span><span class="RktVal">finished</span>), logged at the end of a run.
</div><div class="SIntrapara"><table cellspacing="0" cellpadding="0"><tr><td align="right" valign="baseline"><span class="hspace">&nbsp;&nbsp;</span><span class="RktVar">data-list</span></td><td align="left" valign="baseline"><span class="stt">&nbsp;</span></td><td align="center" valign="baseline">=</td><td align="left" valign="baseline"><span class="stt">&nbsp;</span></td><td align="left" valign="baseline"><table cellspacing="0" cellpadding="0" class="RktBlk"><tr><td><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=pairs.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._list%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">list</a></span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:model</span><span class="hspace">&nbsp;</span><span class="RktVar">model</span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:type</span><span class="hspace">&nbsp;</span><span class="RktVar">gen</span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:time-ms</span><span class="hspace">&nbsp;</span><span class="RktVar">time</span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:attempts</span><span class="hspace">&nbsp;</span><span class="RktVar">tries</span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:num-counterexamples</span><span class="hspace">&nbsp;</span><span class="RktVar">countxmps</span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:rate-terms/s</span><span class="hspace">&nbsp;</span><span class="RktVar">rate</span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:attempts/cexp</span><span class="hspace">&nbsp;</span><span class="RktVar">atts</span><span class="RktPn">)</span></td></tr></table></td></tr></table></div></p></li><li><p><div class="SIntrapara">Every counterexample found (<span class="RktVal">'</span><span class="RktVal">counterexample</span>).
</div><div class="SIntrapara"><table cellspacing="0" cellpadding="0"><tr><td align="right" valign="baseline"><span class="hspace">&nbsp;&nbsp;</span><span class="RktVar">data-list</span></td><td align="left" valign="baseline"><span class="stt">&nbsp;</span></td><td align="center" valign="baseline">=</td><td align="left" valign="baseline"><span class="stt">&nbsp;</span></td><td align="left" valign="baseline"><table cellspacing="0" cellpadding="0" class="RktBlk"><tr><td><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=pairs.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._list%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">list</a></span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:model</span><span class="hspace">&nbsp;</span><span class="RktVar">model</span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:type</span><span class="hspace">&nbsp;</span><span class="RktVar">gen</span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:counterexample</span><span class="hspace">&nbsp;</span><span class="RktVar">term</span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:iterations</span><span class="hspace">&nbsp;</span><span class="RktVar">tries</span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:time</span><span class="hspace">&nbsp;</span><span class="RktVar">time</span><span class="RktPn">)</span></td></tr></table></td></tr></table></div></p></li><li><p><div class="SIntrapara">New average intervals between counterexamples (<span class="RktVal">'</span><span class="RktVal">new-average</span>), which
    are recalculated whenever a counterexample is found.
</div><div class="SIntrapara"><table cellspacing="0" cellpadding="0"><tr><td align="right" valign="baseline"><span class="hspace">&nbsp;&nbsp;</span><span class="RktVar">data-list</span></td><td align="left" valign="baseline"><span class="stt">&nbsp;</span></td><td align="center" valign="baseline">=</td><td align="left" valign="baseline"><span class="stt">&nbsp;</span></td><td align="left" valign="baseline"><table cellspacing="0" cellpadding="0" class="RktBlk"><tr><td><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=pairs.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._list%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">list</a></span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:model</span><span class="hspace">&nbsp;</span><span class="RktVar">model</span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:type</span><span class="hspace">&nbsp;</span><span class="RktVar">gen</span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:average</span><span class="hspace">&nbsp;</span><span class="RktVar">avg</span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:stderr</span><span class="hspace">&nbsp;</span><span class="RktVar">err</span><span class="RktPn">)</span></td></tr></table></td></tr></table></div></p></li><li><p><div class="SIntrapara">Major garbage collections (<span class="RktVal">'</span><span class="RktVal">gc-major</span>).
</div><div class="SIntrapara"><table cellspacing="0" cellpadding="0"><tr><td align="right" valign="baseline"><span class="hspace">&nbsp;&nbsp;</span><span class="RktVar">data-list</span></td><td align="left" valign="baseline"><span class="stt">&nbsp;</span></td><td align="center" valign="baseline">=</td><td align="left" valign="baseline"><span class="stt">&nbsp;</span></td><td align="left" valign="baseline"><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=pairs.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._list%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">list</a></span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:amount</span><span class="hspace">&nbsp;</span><span class="RktVar">amount</span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:time</span><span class="hspace">&nbsp;</span><span class="RktVar">time</span><span class="RktPn">)</span></td></tr></table></div></p></li><li><p><div class="SIntrapara">Heartbeats (<span class="RktVal">'</span><span class="RktVal">hearbeat</span>) are logged every 10 seconds by the benchmark
            as a way to be sure that the benchmark has not crashed.
</div><div class="SIntrapara"><table cellspacing="0" cellpadding="0"><tr><td align="right" valign="baseline"><span class="hspace">&nbsp;&nbsp;</span><span class="RktVar">data-list</span></td><td align="left" valign="baseline"><span class="stt">&nbsp;</span></td><td align="center" valign="baseline">=</td><td align="left" valign="baseline"><span class="stt">&nbsp;</span></td><td align="left" valign="baseline"><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=pairs.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._list%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">list</a></span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:model</span><span class="hspace">&nbsp;</span><span class="RktVar">model</span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:type</span><span class="hspace">&nbsp;</span><span class="RktVar">gen</span><span class="RktPn">)</span></td></tr></table></div></p></li><li><p><div class="SIntrapara">Timeouts (<span class="RktVal">'</span><span class="RktVal">timeout</span>), which occur when generating or <a href="#%28tech._check%29" class="techoutside" data-pltdoc="x"><span class="techinside">check</span></a>ing a single
         takes term longer than 5 minutes.
</div><div class="SIntrapara"><table cellspacing="0" cellpadding="0"><tr><td align="right" valign="baseline"><span class="hspace">&nbsp;&nbsp;</span><span class="RktVar">data-list</span></td><td align="left" valign="baseline"><span class="stt">&nbsp;</span></td><td align="center" valign="baseline">=</td><td align="left" valign="baseline"><span class="stt">&nbsp;</span></td><td align="left" valign="baseline"><table cellspacing="0" cellpadding="0" class="RktBlk"><tr><td><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=pairs.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._list%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">list</a></span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:during</span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">check</span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:term</span><span class="hspace">&nbsp;</span><span class="RktVar">term</span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:model</span><span class="hspace">&nbsp;</span><span class="RktVar">model</span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:type</span><span class="hspace">&nbsp;</span><span class="RktVar">gen</span><span class="RktPn">)</span></td></tr></table></td></tr><tr><td align="right" valign="baseline"><span class="stt">&nbsp;</span></td><td align="left" valign="baseline"><span class="stt">&nbsp;</span></td><td align="center" valign="baseline">|</td><td align="left" valign="baseline"><span class="stt">&nbsp;</span></td><td align="left" valign="baseline"><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=pairs.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._list%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">list</a></span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:during</span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">generation</span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:model</span><span class="hspace">&nbsp;</span><span class="RktVar">model</span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">#:type</span><span class="hspace">&nbsp;</span><span class="RktVar">gen</span><span class="RktPn">)</span></td></tr></table></div></p></li></ul></div></p><p><div class="SIntrapara"><blockquote class="SVInsetFlow"><table cellspacing="0" cellpadding="0" class="boxed RBoxed"><tr><td><blockquote class="SubFlow"><div class="RBackgroundLabel SIEHidden"><div class="RBackgroundLabelInner"><p>procedure</p></div></div><p class="RForeground"><span class="RktPn">(</span><a name="(def._((lib._redex/benchmark..rkt)._benchmark-logging-to))"></a><span title="Provided from: redex/benchmark | Package: redex-benchmark"><span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._benchmark-logging-to%29%29" class="RktValDef RktValLink" data-pltdoc="x">benchmark-logging-to</a></span></span><span class="hspace">&nbsp;</span><span class="RktVar">filename</span><span class="hspace">&nbsp;</span><span class="RktVar">thunk</span><span class="RktPn">)</span><span class="hspace">&nbsp;</span>&rarr;<span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=data-structure-contracts.html%23%2528def._%2528%2528lib._racket%252Fcontract%252Fprivate%252Fmisc..rkt%2529._any%252Fc%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">any/c</a></span></p></blockquote></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;</span><span class="RktVar">filename</span><span class="hspace">&nbsp;</span>:<span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=strings.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._string%7E3f%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">string?</a></span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;</span><span class="RktVar">thunk</span><span class="hspace">&nbsp;</span>:<span class="hspace">&nbsp;</span><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=function-contracts.html%23%2528form._%2528%2528lib._racket%252Fcontract%252Fbase..rkt%2529._-%7E3e%2529%2529&amp;version=6.3" class="RktStxLink Sq" data-pltdoc="x"><span class="nobreak">-&gt;</span></a></span><span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=data-structure-contracts.html%23%2528def._%2528%2528lib._racket%252Fcontract%252Fprivate%252Fmisc..rkt%2529._any%252Fc%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">any/c</a></span><span class="RktPn">)</span></td></tr></table></blockquote></div><div class="SIntrapara">Intercepts events logged by the benchmark and writes the data specified by
the <span class="RktSym">log-data</span> production above to <span class="RktVar">filename</span>.</div></p><p><div class="SIntrapara"><blockquote class="SVInsetFlow"><table cellspacing="0" cellpadding="0" class="boxed RBoxed"><tr><td><blockquote class="SubFlow"><div class="RBackgroundLabel SIEHidden"><div class="RBackgroundLabelInner"><p>parameter</p></div></div><p class="RForeground"><span class="RktPn">(</span><a name="(def._((lib._redex/benchmark..rkt)._bmark-log-directory))"></a><span title="Provided from: redex/benchmark | Package: redex-benchmark"><span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._bmark-log-directory%29%29" class="RktValDef RktValLink" data-pltdoc="x">bmark-log-directory</a></span></span><span class="RktPn"></span><span class="RktPn">)</span></p></blockquote></td></tr><tr><td><span class="hspace">&nbsp;</span>&rarr;<span class="hspace">&nbsp;</span><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=data-structure-contracts.html%23%2528def._%2528%2528lib._racket%252Fcontract%252Fbase..rkt%2529._or%252Fc%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">or/c</a></span><span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=Manipulating_Paths.html%23%2528def._%2528%2528lib._racket%252Fprivate%252Fmisc..rkt%2529._path-string%7E3f%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">path-string?</a></span><span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=Manipulating_Paths.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._path-for-some-system%7E3f%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">path-for-some-system?</a></span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">up</span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">same</span><span class="RktPn">)</span></td></tr><tr><td><span class="RktPn">(</span><span title="Provided from: redex/benchmark | Package: redex-benchmark"><span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._bmark-log-directory%29%29" class="RktValDef RktValLink" data-pltdoc="x">bmark-log-directory</a></span></span><span class="hspace">&nbsp;</span><span class="RktVar">directory</span><span class="RktPn">)</span><span class="hspace">&nbsp;</span>&rarr;<span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=void.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._void%7E3f%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">void?</a></span></td></tr><tr><td><span class="hspace">&nbsp;&nbsp;</span><span class="RktVar">directory</span><span class="hspace">&nbsp;</span>:<span class="hspace">&nbsp;</span><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=data-structure-contracts.html%23%2528def._%2528%2528lib._racket%252Fcontract%252Fbase..rkt%2529._or%252Fc%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">or/c</a></span><span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=Manipulating_Paths.html%23%2528def._%2528%2528lib._racket%252Fprivate%252Fmisc..rkt%2529._path-string%7E3f%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">path-string?</a></span><span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=Manipulating_Paths.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._path-for-some-system%7E3f%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">path-for-some-system?</a></span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">up</span><span class="hspace">&nbsp;</span><span class="RktVal">'</span><span class="RktVal">same</span><span class="RktPn">)</span></td></tr><tr><td><table cellspacing="0" cellpadding="0" class="argcontract"><tr><td valign="top"><span class="hspace">&nbsp;</span>=<span class="hspace">&nbsp;</span></td><td valign="top"><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=Filesystem.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._current-directory%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">current-directory</a></span><span class="RktPn">)</span></td></tr></table></td></tr></table></blockquote></div><div class="SIntrapara">Controls the directory where <span class="RktSym">filename</span> in <span class="RktSym"><a href="#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._benchmark-logging-to%29%29" class="RktValLink" data-pltdoc="x">benchmark-logging-to</a></span> is located.</div></p><h4 x-source-module="(lib &quot;redex/redex.scrbl&quot;)" x-source-pkg="redex-doc" x-part-tag="&quot;Plotting&quot;">5.5<tt>&nbsp;</tt><a name="(part._.Plotting)"></a>Plotting</h4><p>Plotting and analysis tools consume data of the form produced by the benchmark
logging facilities (see <a href="#%28part._log%29" data-pltdoc="x">Logging</a>).</p><p><span style="font-style: italic">TODO!</span></p><h4 x-source-module="(lib &quot;redex/redex.scrbl&quot;)" x-source-pkg="redex-doc" x-part-tag="&quot;sec:finding&quot;">5.6<tt>&nbsp;</tt><a name="(part._sec~3afinding)"></a><a name="(mod-path._redex/benchmark/models/all-info)"></a>Finding the Benchmark Models</h4><p><table cellspacing="0" cellpadding="0" class="defmodule"><tr><td align="left" colspan="2"><span class="hspace">&nbsp;</span><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=require.html%23%2528form._%2528%2528lib._racket%252Fprivate%252Fbase..rkt%2529._require%2529%2529&amp;version=6.3" class="RktStxLink Sq" data-pltdoc="x">require</a></span><span class="stt"> </span><a href="#%28mod-path._redex%2Fbenchmark%2Fmodels%2Fall-info%29" class="RktModLink" data-pltdoc="x"><span class="RktSym">redex/benchmark/models/all-info</span></a><span class="RktPn">)</span></td></tr><tr><td align="left">&nbsp;</td><td align="right"><span class="RpackageSpec"><span class="Smaller">&nbsp;package:</span> <span class="stt">redex-benchmark</span></span></td></tr></table></p><p><div class="SIntrapara"><blockquote class="SVInsetFlow"><table cellspacing="0" cellpadding="0" class="boxed RBoxed"><tr><td><blockquote class="SubFlow"><div class="RBackgroundLabel SIEHidden"><div class="RBackgroundLabelInner"><p>procedure</p></div></div><p class="RForeground"><span class="RktPn">(</span><a name="(def._((lib._redex/benchmark/models/all-info..rkt)._all-mods))"></a><span title="Provided from: redex/benchmark/models/all-info | Package: redex-benchmark"><span class="RktSym"><span class="RktSymDef RktSym">all-mods</span></span></span><span class="RktPn"></span><span class="RktPn">)</span></p></blockquote></td></tr><tr><td><span class="hspace">&nbsp;</span>&rarr;<span class="hspace">&nbsp;</span><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=data-structure-contracts.html%23%2528def._%2528%2528lib._racket%252Fcontract%252Fprivate%252Fmisc..rkt%2529._listof%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">listof</a></span><span class="hspace">&nbsp;</span><span class="RktPn">(</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=data-structure-contracts.html%23%2528def._%2528%2528lib._racket%252Fcontract%252Fprivate%252Fmisc..rkt%2529._list%252Fc%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">list/c</a></span><span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=strings.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._string%7E3f%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">string?</a></span><span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=Module_Names_and_Loading.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._module-path%7E3f%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">module-path?</a></span><span class="hspace">&nbsp;</span><span class="RktSym"><a href="http://download.racket-lang.org/docs/6.3/html/local-redirect/index.html?doc=reference&amp;rel=Module_Names_and_Loading.html%23%2528def._%2528%2528quote._%7E23%7E25kernel%2529._module-path%7E3f%2529%2529&amp;version=6.3" class="RktValLink Sq" data-pltdoc="x">module-path?</a></span><span class="RktPn">)</span><span class="RktPn">)</span></td></tr></table></blockquote></div><div class="SIntrapara">Returns a list of
<a href="#%28tech._generate%29" class="techoutside" data-pltdoc="x"><span class="techinside">generate</span></a> and <a href="#%28tech._check%29" class="techoutside" data-pltdoc="x"><span class="techinside">check</span></a> pairs for a given model or set of models, such that for each
pair the first element is the name of the model, the second is a module defining a
generator, and the third is a module defining a <a href="#%28tech._check%29" class="techoutside" data-pltdoc="x"><span class="techinside">check</span></a> function.</div></p><p>The models included in the distribution of the benchmark are in the
<span class="stt">"redex/benchmark/models"</span> subdirectory of the <span class="RktSym">redex-benchmark</span>
package. In addition to the <a href="#%28mod-path._redex%2Fbenchmark%2Fmodels%2Fall-info%29" class="RktModLink" data-pltdoc="x"><span class="RktSym">redex/benchmark/models/all-info</span></a> library
documented here, each such subdirectory contains an info file named according to the
pattern <span class="stt">"&lt;name&gt;-info.rkt"</span>, defining a module that provides a model-specific
<span class="RktSym">all-mods</span> function.</p><p>A command line interface is provided by the file
<span class="stt">"redex/benchmark/run-benchmark.rkt"</span>,
which takes an &ldquo;info&rdquo; file as described above as its primary argument and provides
options for running the listed tests. It automatically writes results from each run to
a separate log file, all of which are located in a temporary directory.
(The directory path is printed to standard out at the beginning of the run).</p><div class="navsetbottom"><span class="navleft"><form class="searchform"><input class="searchbox" style="color: #888;" type="text" value="...search manuals..." title="Enter a search string to search the manuals" onkeypress="return DoSearchKey(event, this, &quot;6.3&quot;, &quot;../&quot;);" onfocus="this.style.color=&quot;black&quot;; this.style.textAlign=&quot;left&quot;; if (this.value == &quot;...search manuals...&quot;) this.value=&quot;&quot;;" onblur="if (this.value.match(/^ *$/)) { this.style.color=&quot;#888&quot;; this.style.textAlign=&quot;center&quot;; this.value=&quot;...search manuals...&quot;; }"/></form>&nbsp;&nbsp;<a href="../index.html" title="up to the documentation top" data-pltdoc="x" onclick="return GotoPLTRoot(&quot;6.3&quot;);">top</a></span><span class="navright">&nbsp;&nbsp;<a href="The_Redex_Reference.html" title="backward to &quot;4 The Redex Reference&quot;" data-pltdoc="x">&larr; prev</a>&nbsp;&nbsp;<a href="index.html" title="up to &quot;Redex: Practical Semantics Engineering&quot;" data-pltdoc="x">up</a>&nbsp;&nbsp;<a href="doc-bibliography.html" title="forward to &quot;Bibliography&quot;" data-pltdoc="x">next &rarr;</a></span>&nbsp;</div></div></div><div id="contextindicator">&nbsp;</div></body></html>
racket-doc 6.3-1 / usr / share / doc / racket / redex / benchmark.html
