GaloisInc / crucible

Crucible is a library for symbolic simulation of imperative programs
617 stars 42 forks source link

syntax: Accept more characters in function names #1200

Open langston-barrett opened 3 months ago

langston-barrett commented 3 months ago

I recently encountered a situation in which I wanted to scan a Crucible-LLVM-syntax file for declares to decide which LLVM overrides to register. However, I realized that the S-expression syntax makes it impossible to declare functions with names matching various LLVM intrinsics, e.g. llvm.memset.p0i8.i64, because they contain ., which is lexically invalid as part of function names. This is odd, because internally, Crucible represents function names as plain Text, meaning there is no necessary reason to forbid additional characters. We should probably allow more characters in the syntax so that it can express more valid Crucible CFGs.