{aarch32-,}symbolic: Additional commentary

macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs

@@ -49,6 +49,9 @@ Helpful links:
 * <https://github.com/ARM-software/abi-aa/blob/a82eef0433556b30539c0d4463768d9feb8cfd0b/aapcs32/aapcs32.rst#621the-stack>
 * <https://learn.microsoft.com/en-us/cpp/build/overview-of-arm-abi-conventions?view=msvc-170>
 
+(The latter describes the Microsoft ARM ABI which is slightly different from the
+standard ARM ABI, but most of the content still applies.)
+
 This module is meant to be imported qualified.
 -}
 

symbolic/src/Data/Macaw/Symbolic/Stack.hs

@@ -110,8 +110,11 @@ createArrayStack bak mem slots sz = do
   (base, mem1) <- mallocStack bak mem sz
   mem2 <- CLM.doArrayStore bak mem1 base stackAlign arr sz
 
+  -- Put the stack pointer at the end of the stack allocation, i.e., an offset
+  -- that is one less than the allocation's size.
   off <- WI.bvSub sym sz =<< WI.bvOne sym ?ptrWidth
   end <- CLM.doPtrAddOffset bak mem2 base off
+
   let ptrBytes = WI.intValue ?ptrWidth `div` 8
   let slots' = fromIntegral (getExtraStackSlots slots)
   let slotsBytes = slots' * ptrBytes