From 5f6f718040a0e10280af568a18b4e4f0f3db2464 Mon Sep 17 00:00:00 2001
From: Eddy Westbrook <westbrook@galois.com>
Date: Mon, 2 May 2022 12:58:44 -0700
Subject: [PATCH] fixed translateLLVMValue on string values, which was somehow
 giving an incorrect translation; also fixed up the comments on
 translateLLVMValue to help clarify what it is supposed to return

---
 heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs
index 8b63988c41..7a37b3d2b5 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs
@@ -83,7 +83,8 @@ ppLLVMConstExpr :: L.ConstExpr -> String
 ppLLVMConstExpr ce =
   L.withConfig (L.Config True True True) (show $ PPHPJ.nest 2 $ L.ppConstExpr ce)
 
--- | Translate a typed LLVM 'L.Value' to a Heapster permission + translation
+-- | Translate a typed LLVM 'L.Value' to a Heapster shape + an element of the
+-- translation of that shape to a SAW core type
 translateLLVMValue :: (1 <= w, KnownNat w) => NatRepr w -> L.Type -> L.Value ->
                       LLVMTransM (PermExpr (LLVMShapeType w), OpenTerm)
 translateLLVMValue w tp@(L.PrimType (L.Integer n)) (L.ValInteger i) =
@@ -124,7 +125,8 @@ translateLLVMValue _ _ (L.ValString bytes) =
         foldr1 PExpr_SeqShape $
         map (PExpr_FieldShape . LLVMFieldShape . ValPerm_Eq .
              PExpr_LLVMWord . bvBV . BV.word8) bytes in
-  return (sh, unitOpenTerm)
+  let tm = foldr1 pairOpenTerm $ map (const unitOpenTerm) bytes in
+  return (sh, tm)
 -- NOTE: we don't translate strings to one big bitvector value because that
 -- seems to mess up the endianness
 {-