GaloisInc / crucible

Crucible is a library for symbolic simulation of imperative programs

673 stars 44 forks source link

crucible-llvm-syntax: Concrete syntax for remaining LLVM syntax formers #1118

Open langston-barrett opened 1 year ago

langston-barrett commented 1 year ago

1113 introduced support for parsing syntax that corresponds to some of the constructors of `LLVMExtensionExpr` and `LLVMStmt`. We should extend this parser with syntax for all of these constructors:

LLVMExtensionExpr

[ ] X86Expr
[ ] LLVM_SideConditions
[x] LLVM_PointerExpr (#1113)
[x] LLVM_PointerBlock (#1113)
[x] LLVM_PointerOffset (#1113)
[x] LLVM_PointerIte (#1113)

[ ] LLVM_PushFrame
[ ] LLVM_PopFrame
[x] LLVM_Alloca (#1113)
[x] LLVM_Load (#1113)
[x] LLVM_Store (#1113)
[ ] LLVM_MemClear
[x] LLVM_LoadHandle (#1125)
[x] LLVM_ResolveGlobal (#1125)
[ ] LLVM_PtrEq
[ ] LLVM_PtrLe
[x] LLVM_PtrAddOffset (#1146)
[x] LLVM_PtrSubtract (#1146)
[ ] LLVM_Debug