Merge pull request #1531 from GaloisInc/heapster/freshen-llvm-globals

Heapster: freshen LLVM global names

heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs

@@ -231,7 +231,9 @@ permEnvAddGlobalConst sc mod_name dlevel endianness w env global =
   case translateLLVMValueTop dlevel endianness w env global of
     Nothing -> return env
     Just (sh, t) ->
-      do let ident = mkSafeIdent mod_name $ show $ L.globalSym global
+      do ident <-
+           scFreshenGlobalIdent sc $
+           mkSafeIdent mod_name $ show $ L.globalSym global
          complete_t <- completeOpenTerm sc t
          tp <- completeOpenTermType sc t
          scInsertDef sc mod_name ident tp complete_t

saw-core/src/Verifier/SAW/SharedTerm.hs

@@ -70,6 +70,7 @@ module Verifier.SAW.SharedTerm
   , scExtCns
   , scGlobalDef
   , scRegisterGlobal
+  , scFreshenGlobalIdent
     -- ** Recursors and datatypes
   , scRecursorElimTypes
   , scRecursorRetTypeType
@@ -269,7 +270,7 @@ import Control.Lens
 import Control.Monad.State.Strict as State
 import Control.Monad.Reader
 import Data.Bits
-import Data.List (inits)
+import Data.List (inits, find)
 import Data.Maybe
 import qualified Data.Foldable as Fold
 import Data.Foldable (foldl', foldlM, foldrM, maximum)
@@ -441,6 +442,16 @@ scRegisterGlobal sc ident t =
         Just _ -> (m, True)
         Nothing -> (HMap.insert ident t m, False)
 
+-- | Find a variant of an identifier that is not already being used as a global,
+-- by possibly adding a numeric suffix
+scFreshenGlobalIdent :: SharedContext -> Ident -> IO Ident
+scFreshenGlobalIdent sc ident =
+  readIORef (scGlobalEnv sc) >>= \gmap ->
+  return $ fromJust $ find (\i -> not $ HMap.member i gmap) $
+  ident : map (mkIdent (identModule ident) .
+               Text.append (identBaseName ident) .
+               Text.pack . show) [(0::Integer) ..]
+
 -- | Create a function application term.
 scApply :: SharedContext
         -> Term -- ^ The function to apply