Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Heapster: freshen LLVM global names #1531

Merged
merged 3 commits into from
Dec 3, 2021
Merged

Heapster: freshen LLVM global names #1531

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
0445c11
added scFreshenGlobalIdent to find a fresh Ident to use for a SAW cor…
Dec 2, 2021
f1d4d64
bug fix: LLVM globals are translated to fresh names, so that globals …
Dec 2, 2021
d69969c
Merge branch 'master' into heapster/freshen-llvm-globals
Dec 3, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
13 changes: 12 additions & 1 deletion saw-core/src/Verifier/SAW/SharedTerm.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,7 @@ module Verifier.SAW.SharedTerm
, scExtCns
, scGlobalDef
, scRegisterGlobal
, scFreshenGlobalIdent
-- ** Recursors and datatypes
, scRecursorElimTypes
, scRecursorRetTypeType
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down