symbolic-syntax: Syntactic sugar

[langston-barrett]

macaw-symbolic encodes functions as Crucible CFGs that take and return a struct of all the register values. This struct has a lot of fields. Here's a very simple no-op Macaw x86_64 CFG written in the symbolic-syntax:

(defun @test ((regs (Struct
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      (Ptr 3)  
                      (Ptr 2)  
                      (Ptr 2)  
                      (Ptr 2)  
                      (Ptr 2)  
                      (Ptr 2)  
                      (Ptr 2)  
                      (Ptr 2)  
                      (Ptr 2)  
                      (Ptr 80) 
                      (Ptr 80) 
                      (Ptr 80) 
                      (Ptr 80) 
                      (Ptr 80) 
                      (Ptr 80) 
                      (Ptr 80) 
                      (Ptr 80) 
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512))))
                    (Struct
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      (Ptr 64) 
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      Bool           
                      (Ptr 3)  
                      (Ptr 2)  
                      (Ptr 2)  
                      (Ptr 2)  
                      (Ptr 2)  
                      (Ptr 2)  
                      (Ptr 2)  
                      (Ptr 2)  
                      (Ptr 2)  
                      (Ptr 80) 
                      (Ptr 80) 
                      (Ptr 80) 
                      (Ptr 80) 
                      (Ptr 80) 
                      (Ptr 80) 
                      (Ptr 80) 
                      (Ptr 80) 
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512)
                      (Ptr 512))
  (start start:
    (return regs)))

This is way too long to write in a bunch of test cases. Additionally, accessing individual registers involves loading fields from this struct at certain indices, but such statements don't really incidate which registers are being accessed.

We should introduce some syntactic sugar to make it easier to write macaw-symbolic CFGs. In particular, we should add:

• A type for the register struct for each architecture, e.g., X86_64Regs which would be a synonym for the above
• get-reg and set-reg statements that take a human-readable register name like rsi and map it to an appropriate get/set field operation on the register struct

This could be accomplished using the ParserHooks argument to machineCodeParserHooks.

[RyanGlScott]

An alternative approach (which was adopted by the ambient-verifier tool's override syntax) is to allow giving S-expression functions ordinary type signatures like this:

(defun @test ((x Int)) Int
  (start start:
    (return x)))

And then mapping the argument and result values to the corresponding registers. Most of the time, this is far more convenient, and it makes the overrides more portable across architectures. It does have the downside of not giving the user fine-grained control over the register state, however. As a concrete example of where this would be important, ARM's __aeabi_uidivmod function returns two values in registers instead of just one, which would not be straightforward to model with the typical one-return-value convention that most crucible-syntax functions use. Perhaps we could devise a way for users to choose which syntax they prefer.