crucible-llvm-syntax: Concrete syntax for loading function handles

GaloisInc · Nov 9, 2023 · 9adc57d · 9adc57d
1 parent ef469cc
commit 9adc57d
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 1 deletion.
diff --git a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
@@ -169,6 +169,18 @@ llvmAtomParser mvar =
  let stmt = Ext.LLVM_Load mvar ptr tyRep storTy align
  Some <$> Parse.freshAtom loc (Reg.EvalExt stmt)
 
+ Atom.AtomName "load-handle" -> Parse.describe "LLVM load-handle arguments" $ do
+ loc <- Parse.position
+ (Some ret, (Some args, assign)) <-
+ Parse.cons
+ Parse.isType
+ (Parse.cons
+ (Parse.someAssign "list of argument types" Parse.isType)
+ (Parse.operands (Ctx.Empty Ctx.:> LLVMPointerRepr ?ptrWidth)))
+ let (Ctx.Empty, ptr) = Ctx.decompose assign
+ let stmt = Ext.LLVM_LoadHandle mvar ptr args ret
+ Some <$> Parse.freshAtom loc (Reg.EvalExt stmt)
+
  Atom.AtomName "store" -> Parse.describe "LLVM store arguments" $ do
  loc <- Parse.position
  Parse.depCons parseAlign $ \align ->

diff --git a/crucible-llvm-syntax/test-data/ptr.cbl b/crucible-llvm-syntax/test-data/ptr.cbl
@@ -20,5 +20,6 @@
  (let voff (ptr-offset 8 v))
  (assert! (equal? vblk0 vblk) "stored block numbers equal")
  (assert! (equal? voff0 voff) "stored offsets equal")
+ (let h (load-handle (Ptr 64) ((Ptr 64)) a))
 
  (return p)))
diff --git a/crucible-llvm-syntax/test-data/ptr.out.good b/crucible-llvm-syntax/test-data/ptr.out.good
@@ -19,6 +19,7 @@
  (let voff (ptr-offset 8 v))
  (assert! (equal? vblk0 vblk) "stored block numbers equal")
  (assert! (equal? voff0 voff) "stored offsets equal")
+ (let h (load-handle (Ptr 64) ((Ptr 64)) a))
  (return p)))
 
 test-ptr
@@ -77,6 +78,8 @@ test-ptr
  $22 = stringLit("stored offsets equal")
  % 22:5
  assert($21, $22)
- % 24:5
+ % 23:12
+ $23 = loadFunctionHandle crucible-llvm-syntax-test-memory $12
+ % 25:5
  return $4
  % no postdom