syntax: Redex spec

.github/workflows/redex-check.yml

@@ -0,0 +1,32 @@
+name: redex-check
+on:
+  push:
+    branches: [master, "release-**"]
+    paths:
+      - "crucible-syntax/redex/**"
+      - "crucible-syntax/test-data/**"
+      - ".github/workflows/redex-check.yml"
+  pull_request:
+    paths:
+      - "crucible-syntax/redex/**"
+      - "crucible-syntax/test-data/**"
+      - ".github/workflows/redex-check.yml"
+  workflow_dispatch:
+
+jobs:
+  redex-check:
+    runs-on: ubuntu-24.04
+    name: Redex type-checker
+    defaults:
+      run:
+        shell: bash
+    steps:
+      - uses: actions/checkout@v6
+
+      - name: Install Racket
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y racket
+
+      - name: Run test suite
+        run: crucible-syntax/redex/test-suite.sh

.github/workflows/redex-fuzzer.yml

@@ -0,0 +1,115 @@
+name: redex-fuzzer
+
+on:
+  pull_request:
+    paths:
+      - "crucible-syntax/redex/**"
+      - ".github/workflows/redex-fuzzer.yml"
+  schedule:
+    # Run nightly at 2:00 AM UTC
+    - cron: '0 2 * * *'
+  workflow_dispatch:
+    inputs:
+      count:
+        description: 'Number of programs to generate'
+        required: false
+        default: '200'
+      size:
+        description: 'Maximum program size'
+        required: false
+        default: '15'
+
+jobs:
+  fuzzer:
+    runs-on: ubuntu-24.04
+    name: Redex Parser Fuzzer
+    timeout-minutes: 120
+    defaults:
+      run:
+        shell: bash
+    steps:
+      - uses: actions/checkout@v6
+        with:
+          submodules: true
+
+      - name: Install Racket
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y racket
+
+      - name: Setup Haskell
+        uses: haskell-actions/setup@v2
+        with:
+          ghc-version: '9.10.2'
+          cabal-version: '3.10'
+
+      - name: Build crucible-syntax executable
+        working-directory: crucible-syntax
+        run: |
+          cabal update
+          cabal build exe:crucible-syntax
+          CRUCIBLE_BIN=$(cabal list-bin exe:crucible-syntax)
+          echo "CRUCIBLE_BIN=$CRUCIBLE_BIN" >> $GITHUB_ENV
+
+      - name: Run fuzzer with type-checking
+        id: fuzzer
+        working-directory: crucible-syntax/redex
+        run: |
+          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
+
+      - name: Create summary
+        if: always()
+        run: |
+          cat >> $GITHUB_STEP_SUMMARY << 'EOF'
+          ## Fuzzer Results
+
+          ### Configuration
+          - **Programs generated:** ${{ steps.fuzzer.outputs.count }}
+          - **Maximum program size:** ${{ steps.fuzzer.outputs.size }}
+
+          ### Type-checking Results
+          | Category | Count | Percentage |
+          |----------|-------|------------|
+          | Well-typed programs | ${{ steps.fuzzer.outputs.well_typed }} | ${{ steps.fuzzer.outputs.well_typed }}/${{ steps.fuzzer.outputs.count }} |
+          | Non-well-typed programs | ${{ steps.fuzzer.outputs.non_well_typed }} | ${{ steps.fuzzer.outputs.non_well_typed }}/${{ steps.fuzzer.outputs.count }} |
+
+          ### Parser Test Results (Well-typed Programs Only)
+          | Result | Count |
+          |--------|-------|
+          | ✅ Parse OK | ${{ steps.fuzzer.outputs.parse_ok }} |
+          | ❌ Parse FAIL | ${{ steps.fuzzer.outputs.parse_fail }} |
+
+          ${{ steps.fuzzer.outputs.parse_fail > 0 && '⚠️ **Warning:** Some well-typed programs failed to parse!' || '✅ **Success:** All well-typed programs parsed correctly!' }}
+          EOF
+
+      - name: Upload fuzzer output
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: fuzzer-output
+          path: crucible-syntax/redex/fuzzer-output.txt
+          retention-days: 30

crucible-syntax/README.txt

@@ -103,33 +103,14 @@ already have been set by the time that the .cbl file which declares the extern
 uses it. It is the responsibility of the client to ensure that externs are
 inserted into the Crucible symbolic global state before being accessed.
 
-Types
-
-si ::= 'Unicode' | 'Char16' | 'Char8'
-
-fi ::= 'Half' | 'Float' | 'Double' | 'Quad'
-     | 'X86_80' | 'DoubleDouble'
-
-t ::= 'Any' | 'Unit' | 'Bool' | 'Nat' | 'Integer' | 'Real'
-    | 'ComplexReal' | 'Char' | '(' 'String' si ')'
-    | '(' 'FP' fi ')' | '(' 'BitVector' n ')'
-    | '(' '->' t ... t ')' | '(' 'Maybe' t ')'
-    | '(' 'Sequence' t ')' | '(' 'Vector' t ')' | '(' 'Ref' t ')'
-    | '(' 'Struct' t ... t ')' | '(' 'Variant' t ... t ')'
-
-
-Expressions
-
-
-
-Registers
-
-
-Blocks
-
-
-Statements
+Formal grammar and typing rules
 
+The full grammar (types, expressions, statements, terminators, blocks,
+and top-level forms) is defined as a PLT Redex language in
+redex/grammar.rkt. Typing rules are defined as Redex judgment forms in
+redex/typing.rkt.
 
+To generate SVG diagrams of the grammar and typing rules, run:
 
+  racket redex/doc.rkt
 

crucible-syntax/app/Main.hs

@@ -0,0 +1,29 @@
+{-# LANGUAGE ImplicitParams #-}
+module Main (main) where
+
+import qualified Data.Text.IO as T
+import System.Environment (getArgs, getProgName)
+import System.Exit (exitFailure)
+import System.IO (stderr, hPutStrLn)
+
+import Lang.Crucible.CFG.Extension (IsSyntaxExtension)
+import Lang.Crucible.Syntax.Concrete (defaultParserHooks, ParserHooks)
+import Lang.Crucible.Syntax.Prog (doParseCheck)
+
+main :: IO ()
+main = do
+  args <- getArgs
+  case args of
+    [] -> do
+      prog <- getProgName
+      hPutStrLn stderr $ "Usage: " ++ prog ++ " FILE [FILE ...]"
+      hPutStrLn stderr "Parse crucible-syntax files and exit 0 on success or 1 on failure"
+      exitFailure
+    files -> do
+      let ?parserHooks = defaultParserHooks
+      mapM_ parseFile files
+
+parseFile :: (IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) => FilePath -> IO ()
+parseFile path = do
+  contents <- T.readFile path
+  doParseCheck path contents False stderr

crucible-syntax/cabal.project

@@ -0,0 +1,5 @@
+-- Include crucible-syntax and its direct dependencies from the workspace
+packages:
+  .
+  ../crucible/
+  ../dependencies/what4/what4/

crucible-syntax/crucible-syntax.cabal

@@ -161,3 +161,13 @@ test-suite crucible-syntax-tests
     text,
     what4
 
+executable crucible-syntax
+  import: shared
+  main-is: Main.hs
+  hs-source-dirs: app
+  build-depends:
+    base,
+    crucible,
+    crucible-syntax,
+    text
+

crucible-syntax/redex/.gitignore

@@ -0,0 +1 @@
+doc/

crucible-syntax/redex/README.md

@@ -0,0 +1,73 @@
+# Crucible-Syntax Redex specification
+
+A formal specification and reference implementation of the Crucible intermediate language syntax using PLT Redex.
+
+## Overview
+
+This directory contains:
+- **Grammar definition** (`grammar.rkt`) - Formal grammar for Crucible syntax
+- **Type system** (`typing.rkt`) - Type-checking rules and judgments
+- **Parser** (`parse.rkt`) - S-expression parser that transforms surface syntax to AST
+- **Type checker** (`check.rkt`) - Command-line tool for validating `.cbl` files
+- **Fuzzer** (`fuzz.rkt`) - Property-based testing via random program generation
+- **Documentation** (`doc.rkt`, `doc/`) - Auto-generated reference documentation
+
+## Usage
+
+### Requirements
+
+- [Racket](https://racket-lang.org/) 8.0+
+- Redex package (included with Racket distribution)
+
+### Type-check a program
+
+```bash
+racket check.rkt path/to/program.cbl
+```
+
+### Run the test suite
+
+```bash
+./test-suite.sh
+```
+
+### Run the fuzzer
+
+```bash
+# Quick test (100 attempts, size 3)
+racket fuzz.rkt -n 100 -s 3
+
+# Full fuzzer run with type-checking (1000 attempts, generate 5000 programs, size 15)
+racket fuzz.rkt -n 1000 -s 15 --count 5000 --type-stats
+
+# Save generated programs to directory
+racket fuzz.rkt -n 500 -s 10 --count 1000 --type-stats --write ./output-dir
+
+# With Haskell parser validation (if crucible-syntax binary is available)
+racket fuzz.rkt -n 500 -s 10 --count 1000 --type-stats --crucible path/to/crucible-syntax
+```
+
+Options:
+- `-n, --attempts N` - Number of round-trip tests (default: 1000)
+- `-s, --size N` - Maximum term size (default: 5)
+- `--count N` - Number of programs to generate (default: 100)
+- `--type-stats` - Generate and type-check programs
+- `--write DIR` - Save generated .cbl files to directory
+- `--crucible PATH` - Test Haskell parser on well-typed programs using crucible-syntax executable
+
+### Generate documentation
+
+```bash
+racket doc.rkt
+# Opens documentation in browser
+```
+
+## Testing
+
+The specification is tested via:
+
+1. **Unit tests** - Hand-written `.cbl` programs in `../test-data/`
+2. **Fuzzer** - Generates random programs and validates:
+   - Parser round-trip: `parse(unparse(ast)) = ast`
+   - Well-typed programs parse correctly
+   - Type-checker finds issues in ill-typed programs

crucible-syntax/redex/check.rkt

@@ -0,0 +1,25 @@
+#lang racket/base
+
+(require racket/cmdline
+         redex/reduction-semantics
+         "parse.rkt"
+         "typing.rkt")
+
+(define files
+  (command-line
+   #:program "check"
+   #:args files files))
+
+(define all-ok? #t)
+
+(for ([f (in-list files)])
+  (printf "~a ... " f)
+  (with-handlers ([exn:fail? (lambda (e)
+                    (printf "FAIL: ~a\n" (exn-message e))
+                    (set! all-ok? #f))])
+    (define forms (parse-file f))
+    (if (or (null? forms) (judgment-holds (prog-ok ,forms)))
+        (printf "OK\n")
+        (begin (printf "FAIL\n") (set! all-ok? #f)))))
+
+(exit (if all-ok? 0 1))