The S-expression language
This page describes how GREASE uses the the Crucible S-expression language. There are two ways that GREASE interacts with this language:
- Users can provide overrides written in it.
- Developers can write test-cases in it, see S-expression programs.
Each language supported by GREASE extends the base S-expression language with additional types and operations, see:
- macaw-symbolic-syntax for binaries
- macaw-aarch32-syntax for AArch32
- macaw-ppc-syntax for PowerPC
- macaw-x86-syntax for x86_64
- crucible-llvm-syntax for LLVM
S-expression-specific overrides
There are a few overrides that are only available in S-expression files (programs or overrides).
(declare @fresh-bytes ((name (String Unicode)) (num (Bitvector w))) (Vector (Bitvector 8)))
The bytes created using fresh-bytes
will be concretized and printed to the
terminal if GREASE finds a possible bug.
fresh-bytes
can be used to create overrides for functions that do I/O, such
as the following basic override for recv
, shown for x86_64 and LLVM:
; Basic x86_64 override for `recv`.
;
; Ignores `socket` and `flags`, always reads exactly `length` bytes.
(declare @fresh-bytes ((name (String Unicode)) (num (Bitvector 64))) (Vector (Bitvector 8)))
; `man 2 recv`: ssize_t recv(int socket, void *buffer, size_t length, int flags)
(defun @recv ((socket (Ptr 64)) (buffer (Ptr 64)) (length (Ptr 64)) (flags (Ptr 64))) (Ptr 64)
(registers
($ctr (Bitvector 64)) ; loop counter (going down)
($idx Nat) ; index into vector of bytes
($ptr (Ptr 64))) ; pointer to write the next byte into
(start start:
(let length-bv (pointer-to-bits length))
(let bytes (funcall @fresh-bytes "recv" length-bv))
(set-register! $ctr length-bv)
(set-register! $idx 0)
(set-register! $ptr buffer)
(jump loop:))
(defblock loop:
(let byte (vector-get bytes $idx))
(pointer-write (Bitvector 8) le $ptr byte)
(set-register! $ctr (- $ctr (bv 64 1)))
(set-register! $idx (+ $idx 1))
(let ptr (pointer-add $ptr (bv 64 1)))
(set-register! $ptr ptr)
(branch (equal? $ctr (bv 64 0)) end: loop:))
(defblock end:
(return length)))
; Basic LLVM override for `recv`.
;
; Ignores `socket` and `flags`. Always reads exactly `length` bytes.
(declare @fresh-bytes ((name (String Unicode)) (num (Bitvector 64))) (Vector (Bitvector 8)))
; `man 2 recv`: ssize_t recv(int socket, void *buffer, size_t length, int flags)
(defun @recv ((socket (Ptr 32)) (buffer (Ptr 64)) (length (Ptr 64)) (flags (Ptr 32))) (Ptr 64)
(registers
($ctr (Bitvector 64)) ; loop counter (going down)
($idx Nat) ; index into vector of bytes
($ptr (Ptr 64))) ; pointer to write the next byte into
(start start:
(let length-bv (ptr-offset 64 length))
(let bytes (funcall @fresh-bytes "recv" length-bv))
(set-register! $ctr length-bv)
(set-register! $idx 0)
(set-register! $ptr buffer)
(jump loop:))
(defblock loop:
(let byte (vector-get bytes $idx))
(let byte-ptr (ptr 8 0 byte))
(store none i8 $ptr byte-ptr)
(set-register! $ctr (- $ctr (bv 64 1)))
(set-register! $idx (+ $idx 1))
(let ptr (ptr-add-offset $ptr (bv 64 1)))
(set-register! $ptr ptr)
(branch (equal? $ctr (bv 64 0)) end: loop:))
(defblock end:
(return length)))
LLVM-specific overrides
For LLVM S-expression files (programs or overrides), the following overrides are also available:
(declare @read-bytes ((x (Ptr 64))) (Vector (Bitvector 8)))
(declare @read-c-string ((x (Ptr 64))) (String Unicode))
(declare @write-bytes ((dest (Ptr 64)) (src (Vector (Bitvector 8)))) Unit)
(declare @write-c-string ((dst (Ptr 64)) (src (String Unicode))) Unit)