Skip to content

Commit

Permalink
Merge pull request #1693 from GaloisInc/T1662
Browse files Browse the repository at this point in the history
Update submodule versions and fix #1662
  • Loading branch information
mergify[bot] authored Jun 28, 2022
2 parents 4666760 + 43af17f commit 8edd9cf
Show file tree
Hide file tree
Showing 11 changed files with 23 additions and 75 deletions.
2 changes: 1 addition & 1 deletion cabal.project
Original file line number Diff line number Diff line change
Expand Up @@ -42,4 +42,4 @@ packages:
source-repository-package
type: git
location: https://github.com/eddywestbrook/hobbits.git
tag: e2df7a85ea8dfebce2be8065afdca96cbaef12ae
tag: e49911ce987c4e0fea8c63608d16638b243b051f
2 changes: 1 addition & 1 deletion deps/crucible
2 changes: 1 addition & 1 deletion deps/cryptol
Submodule cryptol updated 59 files
+7 −3 .github/ci.sh
+3 −3 .github/wix.ps1
+36 −19 .github/workflows/ci.yml
+7 −0 .gitignore
+2 −2 .gitpod.Dockerfile
+30 −3 CHANGES.md
+1 −1 Dockerfile
+4 −3 README.md
+40 −40 cabal.GHC-8.10.7.config
+40 −40 cabal.GHC-8.8.4.config
+40 −40 cabal.GHC-9.0.2.config
+310 −0 cabal.GHC-9.2.2.config
+4 −2 cryptol-remote-api/CHANGELOG.md
+3 −3 cryptol-remote-api/Dockerfile
+4 −4 cryptol-remote-api/cryptol-remote-api.cabal
+8 −8 cryptol-remote-api/ghc-portability.patch
+4 −2 cryptol-remote-api/python/CHANGELOG.md
+2 −2 cryptol-remote-api/python/pyproject.toml
+6 −6 cryptol.cabal
+1 −1 deps/argo
+4 −2 src/Cryptol/AES.hs
+2 −2 src/Cryptol/Backend/Monad.hs
+3 −3 src/Cryptol/Eval.hs
+1 −1 src/Cryptol/Eval/Env.hs
+5 −1 src/Cryptol/Eval/Generic.hs
+5 −5 src/Cryptol/Eval/Reference.lhs
+7 −10 src/Cryptol/Eval/What4.hs
+1 −1 src/Cryptol/IR/FreeVars.hs
+3 −3 src/Cryptol/ModuleSystem/Env.hs
+1 −1 src/Cryptol/ModuleSystem/Interface.hs
+1 −1 src/Cryptol/ModuleSystem/Monad.hs
+1 −0 src/Cryptol/ModuleSystem/Name.hs
+2 −0 src/Cryptol/ModuleSystem/NamingEnv.hs
+1 −1 src/Cryptol/ModuleSystem/Renamer/Monad.hs
+3 −3 src/Cryptol/Parser.y
+4 −2 src/Cryptol/Parser/Layout.hs
+2 −2 src/Cryptol/Parser/NoInclude.hs
+4 −2 src/Cryptol/Parser/NoPat.hs
+6 −4 src/Cryptol/Parser/ParserUtils.hs
+36 −25 src/Cryptol/REPL/Command.hs
+6 −3 src/Cryptol/REPL/Monad.hs
+4 −1 src/Cryptol/Symbolic/SBV.hs
+5 −4 src/Cryptol/Transform/MonoValues.hs
+3 −0 src/Cryptol/Transform/Specialize.hs
+2 −0 src/Cryptol/TypeCheck/CheckModuleInstance.hs
+6 −2 src/Cryptol/TypeCheck/Error.hs
+2 −0 src/Cryptol/TypeCheck/Infer.hs
+2 −0 src/Cryptol/TypeCheck/Kind.hs
+4 −4 src/Cryptol/TypeCheck/Monad.hs
+2 −2 src/Cryptol/TypeCheck/Sanity.hs
+2 −0 src/Cryptol/TypeCheck/SimpType.hs
+25 −1 src/Cryptol/TypeCheck/TypePat.hs
+1 −0 tests/issues/issue1344.icry
+4 −0 tests/issues/issue1344.icry.stdout
+5 −0 tests/issues/issue1344/A.cry
+5 −0 tests/issues/issue1344/issue1344.cry
+7 −0 tests/issues/issue1359.icry
+5 −0 tests/issues/issue1359.icry.stdout
+2 −2 win32/cryptol.wxs
2 changes: 1 addition & 1 deletion deps/jvm-parser
2 changes: 1 addition & 1 deletion deps/macaw
Submodule macaw updated 127 files
78 changes: 13 additions & 65 deletions src/SAWScript/Crucible/LLVM/Skeleton.hs
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ import Control.Arrow
import Control.Monad
import Control.Lens

import qualified Data.IntMap.Strict as IntMap
import Data.Maybe
import Data.Text (Text)
import qualified Data.Text as Text
Expand All @@ -36,6 +37,7 @@ import Data.Set (Set)
import qualified Data.Set as Set

import qualified Text.LLVM as LLVM
import qualified Text.LLVM.DebugUtils as LLVM

--------------------------------------------------------------------------------
-- ** Skeletons
Expand Down Expand Up @@ -101,43 +103,27 @@ parseType (LLVM.Array i t) = pure $ TypeSkeleton t True
]
parseType t = pure $ TypeSkeleton t False []

debugInfoGlobalLines :: LLVM.Module -> Map Text Int
debugInfoGlobalLines = go . LLVM.modUnnamedMd
where
go :: [LLVM.UnnamedMd] -> Map Text Int
go (LLVM.UnnamedMd
{ LLVM.umValues = LLVM.ValMdDebugInfo
(LLVM.DebugInfoGlobalVariable LLVM.DIGlobalVariable
{ LLVM.digvName = Just n
, LLVM.digvLine = l
}
)
}:xs) = Map.insert (Text.pack n) (fromIntegral l) $ go xs
go (_:xs) = go xs
go [] = Map.empty

parseGlobal :: Map Text Int -> LLVM.Global -> IO GlobalSkeleton
parseGlobal :: Map String Int -> LLVM.Global -> IO GlobalSkeleton
parseGlobal ls LLVM.Global
{ LLVM.globalSym = LLVM.Symbol s
, LLVM.globalType = t
, LLVM.globalValue = v
, LLVM.globalAttrs = LLVM.GlobalAttrs { LLVM.gaConstant = c }
} = do
let nm = Text.pack s
ty <- parseType t
pure GlobalSkeleton
{ _globSkelName = Text.pack s
, _globSkelLoc = flip Location Nothing <$> Map.lookup nm ls
, _globSkelLoc = flip Location Nothing <$> Map.lookup s ls
, _globSkelType = ty
, _globSkelMutable = not c
, _globSkelInitialized = isJust v
}

parseArg :: LLVM.Typed LLVM.Ident -> (Maybe Text, Maybe Location) -> IO ArgSkeleton
parseArg :: LLVM.Typed LLVM.Ident -> (Maybe String, Maybe Location) -> IO ArgSkeleton
parseArg LLVM.Typed { LLVM.typedType = t } (nm, loc) = do
ty <- parseType t
pure ArgSkeleton
{ _argSkelName = nm
{ _argSkelName = Text.pack <$> nm
, _argSkelLoc = loc
, _argSkelType = ty
}
Expand Down Expand Up @@ -167,7 +153,7 @@ stmtDebugDeclares
, Just (LLVM.ValMdLoc LLVM.DebugLoc { LLVM.dlLine = line, LLVM.dlCol = col }) <- lookup "dbg" md
= Map.insert (fromIntegral a) (Location (fromIntegral line) . Just $ fromIntegral col) $ stmtDebugDeclares stmts
stmtDebugDeclares
(LLVM.Effect
(LLVM.Effect
(LLVM.Call _ _
(LLVM.ValSymbol (LLVM.Symbol s))
[ _
Expand All @@ -185,45 +171,7 @@ stmtDebugDeclares (_:stmts) = stmtDebugDeclares stmts
defineName :: LLVM.Define -> Text
defineName LLVM.Define { LLVM.defName = LLVM.Symbol s } = Text.pack s

debugInfoArgNames :: LLVM.Module -> LLVM.Define -> Map Int Text
debugInfoArgNames m d =
case Map.lookup "dbg" $ LLVM.defMetadata d of
Just (LLVM.ValMdRef s) -> scopeArgs s
_ -> Map.empty
where
scopeArgs :: Int -> Map Int Text
scopeArgs s = go $ LLVM.modUnnamedMd m
where go :: [LLVM.UnnamedMd] -> Map Int Text
go [] = Map.empty
go (LLVM.UnnamedMd
{ LLVM.umValues =
LLVM.ValMdDebugInfo
(LLVM.DebugInfoLocalVariable
LLVM.DILocalVariable
{ LLVM.dilvScope = Just (LLVM.ValMdRef s')
, LLVM.dilvArg = a
, LLVM.dilvName = Just n
})}:xs) =
if s == s' then Map.insert (fromIntegral a) (Text.pack n) $ go xs else go xs
go (_:xs) = go xs

debugInfoDefineLines :: LLVM.Module -> Map Text Int
debugInfoDefineLines = go . LLVM.modUnnamedMd
where
go :: [LLVM.UnnamedMd] -> Map Text Int
go (LLVM.UnnamedMd
{ LLVM.umValues = LLVM.ValMdDebugInfo
(LLVM.DebugInfoSubprogram LLVM.DISubprogram
{ LLVM.dispName = Just n
, LLVM.dispIsDefinition = True
, LLVM.dispLine = l
}
)
}:xs) = Map.insert (Text.pack n) (fromIntegral l) $ go xs
go (_:xs) = go xs
go [] = Map.empty

parseDefine :: Map Text Int -> LLVM.Module -> LLVM.Define -> IO FunctionSkeleton
parseDefine :: Map String Int -> LLVM.Module -> LLVM.Define -> IO FunctionSkeleton
parseDefine _ _ LLVM.Define { LLVM.defVarArgs = True } =
fail "Skeleton generation does not support varargs"
parseDefine ls m d@LLVM.Define
Expand All @@ -233,13 +181,13 @@ parseDefine ls m [email protected]
, LLVM.defRetType = ret
} = do
let stmts = mconcat $ LLVM.bbStmts <$> body
let argNames = debugInfoArgNames m d
let argNames = LLVM.debugInfoArgNames m d
let debugDeclares = stmtDebugDeclares stmts
argSkels <- zipWithM parseArg args $ (flip Map.lookup argNames &&& flip Map.lookup debugDeclares) <$> [1, 2..]
argSkels <- zipWithM parseArg args $ (flip IntMap.lookup argNames &&& flip Map.lookup debugDeclares) <$> [1, 2..]
retTy <- parseType ret
pure FunctionSkeleton
{ _funSkelName = Text.pack s
, _funSkelLoc = flip Location Nothing <$> Map.lookup (Text.pack s) ls
, _funSkelLoc = flip Location Nothing <$> Map.lookup s ls
, _funSkelArgs = argSkels
, _funSkelRet = retTy
, _funSkelCalls = Set.intersection
Expand All @@ -249,8 +197,8 @@ parseDefine ls m [email protected]

moduleSkeleton :: LLVM.Module -> IO ModuleSkeleton
moduleSkeleton ast = do
globs <- mapM (parseGlobal $ debugInfoGlobalLines ast) $ LLVM.modGlobals ast
funs <- mapM (parseDefine (debugInfoDefineLines ast) ast) $ LLVM.modDefines ast
globs <- mapM (parseGlobal $ LLVM.debugInfoGlobalLines ast) $ LLVM.modGlobals ast
funs <- mapM (parseDefine (LLVM.debugInfoDefineLines ast) ast) $ LLVM.modDefines ast
pure $ ModuleSkeleton
{ _modSkelGlobals = Map.fromList $ (\g -> (g ^. globSkelName, g)) <$> globs
, _modSkelFunctions = Map.fromList $ (\f -> (f ^. funSkelName, f)) <$> funs
Expand Down

0 comments on commit 8edd9cf

Please sign in to comment.