Skip to content

Commit 5ea8d45

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

File tree

13 files changed

+1332
-26
lines changed

13 files changed

+1332
-26
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-**"]
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

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

‎crucible-syntax/redex/doc.rkt‎

Lines changed: 92 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,92 @@
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+
;; --------------------------------------------------------------
71+
;; Write output
72+
73+
(make-directory* output-dir)
74+
75+
(printf "Writing SVG files to ~a/\n" output-dir)
76+
(save-svg! grammar-pict "grammar.svg")
77+
(save-svg! lookup-pict "lookup.svg")
78+
(save-svg! expr-pict "expr-type.svg")
79+
(save-svg! stmt-pict "stmt-ok.svg")
80+
(save-svg! term-pict "term-ok.svg")
81+
82+
;; Also write a combined single-page version
83+
(define full-doc
84+
(vc-append 30
85+
grammar-pict
86+
lookup-pict
87+
expr-pict
88+
stmt-pict
89+
term-pict))
90+
(save-svg! full-doc "spec.svg")
91+
92+
(printf "Done.\n")

‎crucible-syntax/redex/grammar.rkt‎

Lines changed: 162 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,162 @@
1+
#lang racket/base
2+
3+
(require redex/reduction-semantics)
4+
5+
(provide crucible-syntax)
6+
7+
(define-language crucible-syntax
8+
;; Floating-point precisions
9+
(fp-prec Float Double Half Quad DoubleDouble X86-80)
10+
11+
;; Rounding modes
12+
(rm rne rna rtp rtn rtz)
13+
14+
;; String encodings
15+
(enc Unicode)
16+
17+
;; Types
18+
(ty Unit Bool Integer Nat Real Any
19+
(String enc)
20+
(Maybe ty)
21+
(Bitvector number)
22+
(FP fp-prec)
23+
(Ref ty)
24+
(Struct ty ...)
25+
(Variant ty ...)
26+
(Vector ty)
27+
(Sequence ty)
28+
(-> ty ... ty))
29+
30+
;; Names
31+
(x variable-not-otherwise-mentioned)
32+
(label variable-not-otherwise-mentioned)
33+
(fname variable-not-otherwise-mentioned)
34+
(reg variable-not-otherwise-mentioned)
35+
(gname variable-not-otherwise-mentioned)
36+
37+
;; Operator categories (for grouping typing rules)
38+
(numeric-varop + - *)
39+
(numeric-binop / mod)
40+
(numeric-cmpop < <=)
41+
(numeric-unop negate abs)
42+
(bool-varop and or xor)
43+
(bv-varop bv-xor bv-or)
44+
(bv-binop bv-and shl lshr ashr /$ smod)
45+
(bv-predop bv-carry bv-scarry bv-sborrow <$ <=$)
46+
(bv-extop zero-extend sign-extend)
47+
(fp-from-bvop ubv-to-fp sbv-to-fp)
48+
(fp-to-bvop fp-to-ubv fp-to-sbv)
49+
50+
;; Expressions
51+
(e unit-val
52+
#t #f
53+
number
54+
string
55+
x
56+
(the ty e)
57+
;; arithmetic (polymorphic: numeric + bitvector)
58+
(numeric-varop e e e ...)
59+
(numeric-binop e e)
60+
;; comparison
61+
(numeric-cmpop e e) (equal? e e)
62+
;; unary numeric
63+
(numeric-unop e)
64+
;; boolean
65+
(bool-varop e e e ...) (not e)
66+
(integer? e)
67+
;; conditional
68+
(if e e e)
69+
;; function call & reference
70+
(funcall fname e ...)
71+
(fun-ref fname)
72+
;; string
73+
(string-concat e e) (show e) (fresh ty)
74+
(string-empty enc) (string-length e)
75+
;; register & global
76+
(reg-ref reg) (global-ref gname)
77+
;; Any
78+
(to-any e) (from-any ty e)
79+
;; Maybe
80+
(nothing ty) (just e) (from-just e e)
81+
;; Bitvector
82+
(bv number number)
83+
(bv-varop e e e ...)
84+
(bv-binop e e) (bv-not e)
85+
(bool-to-bv number e)
86+
(bv-extop number e)
87+
(bv-concat e e) (bv-trunc number e)
88+
(bv-select number number e)
89+
(bv-nonzero e)
90+
(bv-predop e e)
91+
;; Floating point
92+
(binary-to-fp fp-prec e) (fp-to-binary e)
93+
(fp-from-bvop fp-prec rm e)
94+
(fp-to-bvop number rm e)
95+
(fp-to-real e) (real-to-fp fp-prec rm e)
96+
;; Reference
97+
(ref e) (deref e)
98+
;; Struct
99+
(struct e ...)
100+
(get-field number e) (set-field e number e)
101+
;; Variant
102+
(inj ty number e) (proj number e)
103+
;; Vector
104+
(vector e ...) (empty-vector ty)
105+
(vector-replicate e e)
106+
(vector-empty? e) (vector-size e)
107+
(vector-get e e) (vector-set e e e)
108+
(vector-cons e e)
109+
;; Sequence
110+
(seq-nil ty)
111+
(seq-cons e e) (seq-append e e)
112+
(seq-nil? e) (seq-length e)
113+
(seq-head e) (seq-tail e) (seq-uncons e))
114+
115+
;; Statements
116+
(s (let x e)
117+
(print e)
118+
(println e)
119+
(funcall fname e ...)
120+
(set-register! reg e)
121+
(set-global! gname e)
122+
(assert! e e)
123+
(assume! e e)
124+
(set-ref! e e)
125+
(drop-ref! e)
126+
(breakpoint string any))
127+
128+
;; Terminators
129+
(t (return e)
130+
(jump label)
131+
(branch e label label)
132+
(error e)
133+
(tail-call fname e ...)
134+
(output label e)
135+
(maybe-branch e label label)
136+
(case e label ...))
137+
138+
;; Blocks
139+
(block (start label s ... t)
140+
(defblock label s ... t)
141+
(defblock (label x ty) s ... t))
142+
143+
;; Functions
144+
(defun (defun fname ((x ty) ...) ty block block ...)
145+
(defun fname ((x ty) ...) ty
146+
(registers (reg ty) ...) block block ...))
147+
148+
;; Top-level forms
149+
(top-form defun
150+
(defglobal gname ty)
151+
(declare fname (ty ...) ty)
152+
(extern gname ty))
153+
154+
;; Programs
155+
(prog (top-form ...))
156+
157+
;; Environments (for typing)
158+
(V ((x ty) ...))
159+
(F ((fname (ty ...) ty) ...))
160+
(L any)
161+
(G ((gname ty) ...))
162+
(R ((reg ty) ...)))

0 commit comments

Comments
 (0)