Fixes to get macaw-symbolic building again.

macaw-symbolic/src/Data/Macaw/Symbolic/App.hs

@@ -248,15 +248,16 @@ valueToCrucible v = do
     M.BoolValue b -> do
       crucibleValue (C.BoolLit b)
     M.RelocatableValue w addr -> do
-      let seg = M.addrSegment addr
-      case M.segmentBase seg of
-        Just base -> do
-          crucibleValue (C.BVLit w (toInteger base + toInteger (addr^.M.addrOffset)))
-        Nothing -> do
+      case M.viewAddr addr of
+        Left base -> do
+          crucibleValue (C.BVLit w (toInteger base))
+        Right (seg,off) -> do
           let idx = M.segmentIndex seg
           segMap <- gets memSegmentMap
           case Map.lookup idx segMap of
-            Just a -> pure a
+            Just a -> do
+              offset <- crucibleValue (C.BVLit w (toInteger off))
+              crucibleValue (C.BVAdd w a offset)
             Nothing -> fail $ "internal: No Crucible address associated with segment."
     M.Initial r -> do
       regmap <- gets regValueMap
@@ -377,6 +378,8 @@ addMacawStmt stmt = do
     M.PlaceHolderStmt _vals msg -> do
       cmsg <- crucibleValue (C.TextLit (Text.pack msg))
       addTermStmt (C.ErrorStmt cmsg)
+    M.InstructionStart _ _ ->
+      pure ()
     M.Comment _txt -> do
       pure ()
     M.ExecArchStmt astmt -> do

src/Data/Macaw/Memory.hs

@@ -66,6 +66,7 @@ module Data.Macaw.Memory
   , absoluteAddr
   , relativeAddr
   , relativeSegmentAddr
+  , viewAddr
   , asAbsoluteAddr
   , asSegmentOff
   , diffAddr
@@ -658,11 +659,17 @@ asAbsoluteAddr RelativeAddr{} = Nothing
 
 -- | Return the resolved segment offset reference from an address.
 asSegmentOff :: Memory w -> MemAddr w -> Maybe (MemSegmentOff w)
-asSegmentOff mem (AbsoluteAddr addr) = resolveAbsoluteAddr mem addr
+asSegmentOff mem (AbsoluteAddr addr) =
+  resolveAbsoluteAddr mem addr
 asSegmentOff mem (RelativeAddr seg off) =
   addrWidthClass (memAddrWidth mem) $
     resolveSegmentOff seg off
 
+-- | This projects an addr into either an absolute address or a segment plus offset.
+viewAddr :: MemAddr w -> Either (MemWord w) (MemSegment w, MemWord w)
+viewAddr (AbsoluteAddr addr) = Left addr
+viewAddr (RelativeAddr seg off) = Right (seg,off)
+
 -- | Clear the least significant bit of an address.
 clearAddrLeastBit :: MemWidth w => MemAddr w -> MemAddr w
 clearAddrLeastBit sa =