crucible-llvm-syntax: Syntax for LLVM alloca statement

crucible-llvm-syntax/crucible-llvm-syntax.cabal

@@ -96,6 +96,7 @@ library
     crucible-syntax,
     mtl,
     parameterized-utils >= 0.1.7,
+    prettyprinter,
     text,
     what4,
 

crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs

@@ -16,6 +16,8 @@ import Control.Monad.State.Strict (MonadState(..))
 import Control.Monad.Writer.Strict (MonadWriter(..))
 import Data.Functor ((<&>))
 
+import Prettyprinter (pretty)
+
 import Data.Parameterized.Context qualified as Ctx
 import Data.Parameterized.Some (Some(..))
 
@@ -27,6 +29,8 @@ import Lang.Crucible.CFG.Reg qualified as Reg
 import Lang.Crucible.CFG.Extension (IsSyntaxExtension)
 import Lang.Crucible.Types (TypeRepr(..))
 
+import Lang.Crucible.LLVM.DataLayout (Alignment)
+import Lang.Crucible.LLVM.DataLayout qualified as DataLayout
 import Lang.Crucible.LLVM.Extension (LLVM)
 import Lang.Crucible.LLVM.Extension qualified as Ext
 import Lang.Crucible.LLVM.MemModel (Mem, pattern LLVMPointerRepr)
@@ -76,7 +80,7 @@ llvmAtomParser ::
   ) =>
   GlobalVar Mem -> 
   m (Some (Atom s))
-llvmAtomParser _mvar =
+llvmAtomParser mvar =
   Parse.depCons Parse.atomName $
     \case
       Atom.AtomName "ptr" -> do
@@ -115,4 +119,20 @@ llvmAtomParser _mvar =
           let expr = Ext.LLVM_PointerIte w b p1 p2
           Some <$> Parse.freshAtom loc (Reg.EvalApp (Expr.ExtensionApp expr))
 
+      Atom.AtomName "alloca" -> do
+        loc <- Parse.position
+        (align, assign) <- 
+          Parse.cons
+            parseAlign
+            (Parse.operands (Ctx.Empty Ctx.:> BVRepr ?ptrWidth))
+        let (Ctx.Empty, sz) = Ctx.decompose assign
+        let stmt = Ext.LLVM_Alloca ?ptrWidth mvar sz align (show (pretty loc))
+        Some <$> Parse.freshAtom loc (Reg.EvalExt stmt)
+
       _ -> empty
+  where
+    parseAlign :: MonadSyntax Atomic m => m Alignment
+    parseAlign = do
+      s <- Parse.atomName
+      unless (s == Atom.AtomName "none") Parse.cut
+      pure DataLayout.noAlignment

crucible-llvm-syntax/test-data/ptr.cbl

@@ -8,4 +8,8 @@
     (let off (ptr-offset 64 p))
     (assert! (equal? blk0 blk) "block numbers equal")
     (assert! (equal? off0 off) "offsets equal")
+
+    (let sz (bv 64 1))
+    (let a (alloca none sz))
+
     (return p)))

crucible-llvm-syntax/test-data/ptr.out.good

@@ -8,6 +8,8 @@
       (let off (ptr-offset 64 p))
       (assert! (equal? blk0 blk) "block numbers equal")
       (assert! (equal? off0 off) "offsets equal")
+      (let sz (bv 64 1))
+      (let a (alloca none sz))
       (return p)))
 
 test-ptr
@@ -38,6 +40,10 @@ test-ptr
   $10 = stringLit("offsets equal")
   % 10:5
   assert($9, $10)
-  % 11:5
+  % 12:13
+  $11 = bVLit(64, BV 1)
+  % 13:12
+  $12 = alloca crucible-llvm-syntax-test-memory $11 Alignment 0 test-data/ptr.cbl:13:12
+  % 15:5
   return $4
   % no postdom