From e9f939a24528360db6ef4761964e1735aefa84e3 Mon Sep 17 00:00:00 2001
From: Your Name <you@example.com>
Date: Mon, 23 Sep 2024 16:30:55 -0400
Subject: [PATCH] {aarch32-,}symbolic: Additional commentary

---
 macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs | 3 +++
 symbolic/src/Data/Macaw/Symbolic/Stack.hs                     | 3 +++
 2 files changed, 6 insertions(+)

diff --git a/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs b/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs
index 74827d20..fbbe0d72 100644
--- a/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs
+++ b/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.
 -}
 
diff --git a/symbolic/src/Data/Macaw/Symbolic/Stack.hs b/symbolic/src/Data/Macaw/Symbolic/Stack.hs
index db48d8e6..8708be30 100644
--- a/symbolic/src/Data/Macaw/Symbolic/Stack.hs
+++ b/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