Skip to content

Commit d912494

Browse files
langston-barrettlangston-barrett
committed
syntax: Redex spec
Add a declarative specification for crucible-syntax grammar and typing.
1 parent 3bed3e3 commit d912494

File tree

16 files changed

+1809
-30
lines changed

16 files changed

+1809
-30
lines changed

‎.github/workflows/redex-check.yml‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
name: redex-check
2+
on:
3+
push:
4+
branches: [master, "release-**", "redex"]
5+
paths:
6+
- "crucible-syntax/redex/**"
7+
- "crucible-syntax/test-data/**"
8+
- ".github/workflows/redex-check.yml"
9+
pull_request:
10+
paths:
11+
- "crucible-syntax/redex/**"
12+
- "crucible-syntax/test-data/**"
13+
- ".github/workflows/redex-check.yml"
14+
workflow_dispatch:
15+
16+
jobs:
17+
redex-check:
18+
runs-on: ubuntu-24.04
19+
name: Redex type-checker
20+
steps:
21+
- uses: actions/checkout@v6
22+
23+
- name: Install Racket
24+
run: |
25+
sudo apt-get update
26+
sudo apt-get install -y racket
27+
28+
- name: Run test suite
29+
run: crucible-syntax/redex/test-suite.sh

‎.github/workflows/redex-fuzzer-nightly.yml‎

Lines changed: 91 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,91 @@
1+
name: redex-fuzzer
2+
3+
on:
4+
schedule:
5+
# Run nightly at 2:00 AM UTC
6+
- cron: '0 2 * * *'
7+
workflow_dispatch:
8+
inputs:
9+
count:
10+
description: 'Number of programs to generate'
11+
required: false
12+
default: '5000'
13+
size:
14+
description: 'Maximum program size'
15+
required: false
16+
default: '15'
17+
18+
jobs:
19+
fuzzer:
20+
runs-on: ubuntu-24.04
21+
name: Redex Parser Fuzzer
22+
timeout-minutes: 120
23+
steps:
24+
- uses: actions/checkout@v6
25+
26+
- name: Install Racket
27+
run: |
28+
sudo apt-get update
29+
sudo apt-get install -y racket
30+
31+
- name: Run fuzzer with type-checking
32+
id: fuzzer
33+
working-directory: crucible-syntax/redex
34+
run: |
35+
COUNT=${{ github.event.inputs.count || '5000' }}
36+
SIZE=${{ github.event.inputs.size || '15' }}
37+
38+
# Run the fuzzer and capture output
39+
./run-fuzzer.sh --count "$COUNT" --size "$SIZE" | tee fuzzer-output.txt
40+
41+
# Extract statistics
42+
WELL_TYPED=$(grep "Well-typed programs:" fuzzer-output.txt | grep -oP '\d+(?= \()' || echo "0")
43+
NON_WELL_TYPED=$(grep "Non-well-typed programs:" fuzzer-output.txt | grep -oP '\d+(?= \()' || echo "0")
44+
PARSE_OK=$(grep "Parse OK:" fuzzer-output.txt | grep -oP '\d+' || echo "0")
45+
PARSE_FAIL=$(grep "Parse FAIL:" fuzzer-output.txt | grep -oP '\d+' || echo "0")
46+
47+
echo "count=$COUNT" >> $GITHUB_OUTPUT
48+
echo "size=$SIZE" >> $GITHUB_OUTPUT
49+
echo "well_typed=$WELL_TYPED" >> $GITHUB_OUTPUT
50+
echo "non_well_typed=$NON_WELL_TYPED" >> $GITHUB_OUTPUT
51+
echo "parse_ok=$PARSE_OK" >> $GITHUB_OUTPUT
52+
echo "parse_fail=$PARSE_FAIL" >> $GITHUB_OUTPUT
53+
54+
# Fail if any parser failures
55+
if [ "$PARSE_FAIL" -gt 0 ]; then
56+
echo "ERROR: $PARSE_FAIL well-typed programs failed to parse!"
57+
exit 1
58+
fi
59+
60+
- name: Create summary
61+
if: always()
62+
run: |
63+
cat >> $GITHUB_STEP_SUMMARY << 'EOF'
64+
## Fuzzer Results
65+
66+
### Configuration
67+
- **Programs generated:** ${{ steps.fuzzer.outputs.count }}
68+
- **Maximum program size:** ${{ steps.fuzzer.outputs.size }}
69+
70+
### Type-checking Results
71+
| Category | Count | Percentage |
72+
|----------|-------|------------|
73+
| Well-typed programs | ${{ steps.fuzzer.outputs.well_typed }} | ${{ steps.fuzzer.outputs.well_typed }}/${{ steps.fuzzer.outputs.count }} |
74+
| Non-well-typed programs | ${{ steps.fuzzer.outputs.non_well_typed }} | ${{ steps.fuzzer.outputs.non_well_typed }}/${{ steps.fuzzer.outputs.count }} |
75+
76+
### Parser Test Results (Well-typed Programs Only)
77+
| Result | Count |
78+
|--------|-------|
79+
| ✅ Parse OK | ${{ steps.fuzzer.outputs.parse_ok }} |
80+
| ❌ Parse FAIL | ${{ steps.fuzzer.outputs.parse_fail }} |
81+
82+
${{ steps.fuzzer.outputs.parse_fail > 0 && '⚠️ **Warning:** Some well-typed programs failed to parse!' || '✅ **Success:** All well-typed programs parsed correctly!' }}
83+
EOF
84+
85+
- name: Upload fuzzer output
86+
if: always()
87+
uses: actions/upload-artifact@v4
88+
with:
89+
name: fuzzer-output
90+
path: crucible-syntax/redex/fuzzer-output.txt
91+
retention-days: 30

‎crucible-syntax/README.txt‎

Lines changed: 7 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -103,33 +103,14 @@ already have been set by the time that the .cbl file which declares the extern
103103
uses it. It is the responsibility of the client to ensure that externs are
104104
inserted into the Crucible symbolic global state before being accessed.
105105

106-
Types
107-
108-
si ::= 'Unicode' | 'Char16' | 'Char8'
109-
110-
fi ::= 'Half' | 'Float' | 'Double' | 'Quad'
111-
| 'X86_80' | 'DoubleDouble'
112-
113-
t ::= 'Any' | 'Unit' | 'Bool' | 'Nat' | 'Integer' | 'Real'
114-
| 'ComplexReal' | 'Char' | '(' 'String' si ')'
115-
| '(' 'FP' fi ')' | '(' 'BitVector' n ')'
116-
| '(' '->' t ... t ')' | '(' 'Maybe' t ')'
117-
| '(' 'Sequence' t ')' | '(' 'Vector' t ')' | '(' 'Ref' t ')'
118-
| '(' 'Struct' t ... t ')' | '(' 'Variant' t ... t ')'
119-
120-
121-
Expressions
122-
123-
124-
125-
Registers
126-
127-
128-
Blocks
129-
130-
131-
Statements
106+
Formal grammar and typing rules
132107

108+
The full grammar (types, expressions, statements, terminators, blocks,
109+
and top-level forms) is defined as a PLT Redex language in
110+
redex/grammar.rkt. Typing rules are defined as Redex judgment forms in
111+
redex/typing.rkt.
133112

113+
To generate SVG diagrams of the grammar and typing rules, run:
134114

115+
racket redex/doc.rkt
135116

‎crucible-syntax/redex/.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
doc/

‎crucible-syntax/redex/check.rkt‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
#lang racket/base
2+
3+
(require racket/cmdline
4+
redex/reduction-semantics
5+
"parse.rkt"
6+
"typing.rkt")
7+
8+
(define files
9+
(command-line
10+
#:program "check"
11+
#:args files files))
12+
13+
(define all-ok? #t)
14+
15+
(for ([f (in-list files)])
16+
(printf "~a ... " f)
17+
(with-handlers ([exn:fail? (lambda (e)
18+
(printf "FAIL: ~a\n" (exn-message e))
19+
(set! all-ok? #f))])
20+
(define forms (parse-file f))
21+
(if (or (null? forms) (judgment-holds (prog-ok ,forms)))
22+
(printf "OK\n")
23+
(begin (printf "FAIL\n") (set! all-ok? #f)))))
24+
25+
(exit (if all-ok? 0 1))

‎crucible-syntax/redex/doc.rkt‎

Lines changed: 114 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,114 @@
1+
#lang racket/base
2+
3+
(require racket/cmdline
4+
racket/format
5+
racket/file
6+
redex/pict
7+
pict
8+
file/convertible
9+
"grammar.rkt"
10+
"typing.rkt")
11+
12+
;; --------------------------------------------------------------
13+
;; Configuration
14+
15+
(define output-dir
16+
(command-line
17+
#:program "doc"
18+
#:args ([dir "doc"])
19+
dir))
20+
21+
;; --------------------------------------------------------------
22+
;; Helpers
23+
24+
(define (save-svg! p filename)
25+
(define path (build-path output-dir filename))
26+
(define svg-bytes (convert p 'svg-bytes))
27+
(unless svg-bytes
28+
(error 'save-svg! "conversion to SVG failed for ~a" filename))
29+
(call-with-output-file path
30+
(lambda (out) (write-bytes svg-bytes out))
31+
#:exists 'replace)
32+
(printf " ~a\n" path))
33+
34+
(define (heading txt)
35+
(text txt '(bold . modern) 14))
36+
37+
(define (section title . picts)
38+
(apply vc-append 10 (heading title) picts))
39+
40+
;; --------------------------------------------------------------
41+
;; Render pieces
42+
43+
(printf "Rendering grammar...\n")
44+
(define grammar-pict
45+
(section "Grammar" (render-language crucible-syntax)))
46+
47+
(printf "Rendering lookup judgments...\n")
48+
(define lookup-pict
49+
(section "Lookup"
50+
(render-judgment-form lookup)
51+
(render-judgment-form fun-lookup)
52+
(render-judgment-form reg-lookup)
53+
(render-judgment-form global-lookup)))
54+
55+
(printf "Rendering expression typing...\n")
56+
(define expr-pict
57+
(section "Expression Typing"
58+
(render-judgment-form expr-type)))
59+
60+
(printf "Rendering statement typing...\n")
61+
(define stmt-pict
62+
(section "Statement Typing"
63+
(render-judgment-form stmt-ok)))
64+
65+
(printf "Rendering terminator typing...\n")
66+
(define term-pict
67+
(section "Terminator Typing"
68+
(render-judgment-form term-ok)))
69+
70+
(printf "Rendering block & function typing...\n")
71+
(define block-pict
72+
(section "Block Typing"
73+
(render-judgment-form stmts-ok)
74+
(render-judgment-form block-ok)
75+
(render-judgment-form blocks-ok)))
76+
77+
(define defun-pict
78+
(section "Function Typing"
79+
(render-judgment-form defun-ok)))
80+
81+
(define prog-pict
82+
(section "Program Typing"
83+
(render-judgment-form funs-ok)
84+
(render-judgment-form prog-ok)))
85+
86+
;; --------------------------------------------------------------
87+
;; Write output
88+
89+
(make-directory* output-dir)
90+
91+
(printf "Writing SVG files to ~a/\n" output-dir)
92+
(save-svg! grammar-pict "grammar.svg")
93+
(save-svg! lookup-pict "lookup.svg")
94+
(save-svg! expr-pict "expr-type.svg")
95+
(save-svg! stmt-pict "stmt-ok.svg")
96+
(save-svg! term-pict "term-ok.svg")
97+
(save-svg! block-pict "block-ok.svg")
98+
(save-svg! defun-pict "defun-ok.svg")
99+
(save-svg! prog-pict "prog-ok.svg")
100+
101+
;; Also write a combined single-page version
102+
(define full-doc
103+
(vc-append 30
104+
grammar-pict
105+
lookup-pict
106+
expr-pict
107+
stmt-pict
108+
term-pict
109+
block-pict
110+
defun-pict
111+
prog-pict))
112+
(save-svg! full-doc "spec.svg")
113+
114+
(printf "Done.\n")

0 commit comments

Comments
 (0)