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.

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

Update submodule versions and fix #1662 #1693

Merged
merged 2 commits into from
Jun 28, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
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