crucible-llvm-syntax: Add concrete syntax for resolving globals

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

@@ -97,6 +97,7 @@ library
     crucible >= 0.1,
     crucible-llvm,
     crucible-syntax,
+    llvm-pretty,
     mtl,
     parameterized-utils >= 0.1.7,
     prettyprinter,

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

@@ -19,9 +19,13 @@ import Control.Monad.IO.Class (MonadIO(..))
 import Control.Monad.State.Strict (MonadState(..))
 import Control.Monad.Writer.Strict (MonadWriter(..))
 import Data.Functor ((<&>))
+import qualified Data.Text as Text
 
 import Prettyprinter (pretty)
 
+-- Optimally, this library wouldn't depend on llvm-pretty...
+import Text.LLVM.AST as L (Symbol(Symbol))
+
 import Data.Parameterized.Context qualified as Ctx
 import Data.Parameterized.Some (Some(..))
 
@@ -181,6 +185,13 @@ llvmAtomParser mvar =
         let stmt = Ext.LLVM_LoadHandle mvar ptr args ret
         Some <$> Parse.freshAtom loc (Reg.EvalExt stmt)
 
+      Atom.AtomName "resolve-global" -> Parse.describe "LLVM resolve-global arguments" $ do
+        loc <- Parse.position
+        let parseSymb = Mem.GlobalSymbol . L.Symbol . Text.unpack <$> Parse.string
+        (symb, ()) <- Parse.cons parseSymb Parse.emptyList
+        let stmt = Ext.LLVM_ResolveGlobal ?ptrWidth mvar symb
+        Some <$> Parse.freshAtom loc (Reg.EvalExt stmt)
+
       Atom.AtomName "store" -> Parse.describe "LLVM store arguments" $ do
         loc <- Parse.position
         Parse.depCons parseAlign $ \align ->

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

@@ -20,6 +20,8 @@
     (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))
+
+    (let g (resolve-global "malloc"))
+    (let h (load-handle (Ptr 64) ((Ptr 64)) g))
 
     (return p)))

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

@@ -19,7 +19,8 @@
       (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))
+      (let g (resolve-global "malloc"))
+      (let h (load-handle (Ptr 64) ((Ptr 64)) g))
       (return p)))
 
 test-ptr
@@ -78,8 +79,10 @@ test-ptr
   $22 = stringLit("stored offsets equal")
   % 22:5
   assert($21, $22)
-  % 23:12
-  $23 = loadFunctionHandle crucible-llvm-syntax-test-memory $12
-  % 25:5
+  % 24:12
+  $23 = resolveGlobal crucible-llvm-syntax-test-memory "malloc"
+  % 25:12
+  $24 = loadFunctionHandle crucible-llvm-syntax-test-memory $23
+  % 27:5
   return $4
   % no postdom