Conversation
langston-barrett
added
the
pkg:crucible-syntax
langston-barrett
force-pushed
the
redex
branch
3 times, most recently
from
6fde6f9 to
d912494
Compare
langston-barrett
force-pushed
the
redex
branch
2 times, most recently
from
b65b091 to
248f526
Compare
|
Adding myself as a reviewer as a reminder to look at this later. |
Add a declarative specification for crucible-syntax grammar and typing.
|
I think this is fine as-is, but I might also attempt to make the Redex type-checker bidirectional. That would match the implementation more closely and allow it to handle some currently-disabled tests. |
langston-barrett
force-pushed
the
redex
branch
4 times, most recently
from
20e0ef4 to
aff6063
Compare
|
Fuzzing in CI is timing out, will try with a lower number of tests. Not sure why it doesn't yield any output, though. |
It wasn't comparing against the Haskell implementation.
RyanGlScott
left a comment
RyanGlScott
left a comment
There was a problem hiding this comment.
My Racket skills are rusty enough that I don't feel qualified to review this code in appreciable depth, but I do appreciate having a declarative specification for this language. The downside, of course, is that we now have an additional body of code that we need to keep updated any time we add a new language construct to crucible-syntax. I think we should add some developer documentation that describes what parts of the redex spec would need to be updated as part of this process.
| parseFile :: (IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) => FilePath -> IO () | ||
| parseFile path = do | ||
| contents <- T.readFile path | ||
| doParseCheck path contents False stderr |
There was a problem hiding this comment.
I'm not sure I understand why this crucible-syntax executable needs to exist. What does this do that crucible-cli's check subcommand can't do?
| set -o pipefail | ||
| COUNT=${{ github.event.inputs.count || '5000' }} | ||
| SIZE=${{ github.event.inputs.size || '15' }} | ||
|
|
||
| # Run the fuzzer and capture output (stdbuf ensures incremental output) | ||
| stdbuf -oL racket fuzz.rkt -n 1000 -s "$SIZE" --count "$COUNT" --type-stats --crucible "$CRUCIBLE_BIN" | tee fuzzer-output.txt | ||
|
|
||
| # Extract statistics | ||
| WELL_TYPED=$(grep "Well-typed programs:" fuzzer-output.txt | grep -oP '\d+(?= \()' || echo "0") | ||
| NON_WELL_TYPED=$(grep "Non-well-typed programs:" fuzzer-output.txt | grep -oP '\d+(?= \()' || echo "0") | ||
| PARSE_OK=$(grep "Parse OK:" fuzzer-output.txt | grep -oP '\d+' || echo "0") | ||
| PARSE_FAIL=$(grep "Parse FAIL:" fuzzer-output.txt | grep -oP '\d+' || echo "0") | ||
|
|
||
| echo "count=$COUNT" >> $GITHUB_OUTPUT | ||
| echo "size=$SIZE" >> $GITHUB_OUTPUT | ||
| echo "well_typed=$WELL_TYPED" >> $GITHUB_OUTPUT | ||
| echo "non_well_typed=$NON_WELL_TYPED" >> $GITHUB_OUTPUT | ||
| echo "parse_ok=$PARSE_OK" >> $GITHUB_OUTPUT | ||
| echo "parse_fail=$PARSE_FAIL" >> $GITHUB_OUTPUT | ||
|
|
||
| # Fail if any parser failures | ||
| if [ "$PARSE_FAIL" -gt 0 ]; then | ||
| echo "ERROR: $PARSE_FAIL well-typed programs failed to parse!" | ||
| exit 1 | ||
| fi |
There was a problem hiding this comment.
I am leery about checking in long series of shell commands like this into CI YAML files. I would prefer that these be factored out into scripts that the CI then invokes. Aside from making the YAML files more readable, this would also make it easier to reproduce the results of what CI is doing locally.
| ;; F — function signature environment | ||
| ;; ((fname (ty_arg ...) ty_ret) ...) | ||
| ;; Maps each function name to its argument types and return type. | ||
| ;; | ||
| ;; L — block label environment | ||
| ;; ((label) ... (label ty) ...) | ||
| ;; Maps each block label to nothing (plain jump target) or a | ||
| ;; single parameter type (output/maybe-branch/case target). | ||
| ;; | ||
| ;; G — global variable environment | ||
| ;; ((gname ty) ...) | ||
| ;; Maps each global name to its type. | ||
| ;; | ||
| ;; R — register environment | ||
| ;; ((reg ty) ...) | ||
| ;; Maps each mutable register name (prefixed with $) to its type. | ||
| ;; | ||
| ;; V — local variable environment | ||
| ;; ((x ty) ...) | ||
| ;; Maps each let-bound or argument name to its type. | ||
| ;; Extended by (let x e) statements; otherwise threaded unchanged. | ||
| ;; | ||
| ;; ty — a type (see grammar.rkt for the full ty non-terminal) | ||
| ;; ty_ret — return type of the enclosing function |
There was a problem hiding this comment.
It would help to add some comments to make it more visually obvious which are the inputs and outputs to the typing relation. I think that ty and ty_ret are the outputs, but better to make this a bit more explicit.
2 participants
Add a declarative specification for crucible-syntax grammar and typing. This spec is self-documenting and serves as a reference for the complete grammar and typing rules. It can even generate pretty diagrams!
The spec is tested against the existing crucible-syntax test-suite to ensure that it accepts and rejects the same things as the implementation.
I used a coding agent extensively to build the spec.