Merge branch 'master' into x86-return-trunc

GaloisInc · Oct 5, 2020 · 974e910 · 974e910
2 parents 082d3f2 + 6247f9a
commit 974e910
Show file tree

Hide file tree

Showing 8 changed files with 12 additions and 12 deletions.
diff --git a/deps/crucible b/deps/crucible
diff --git a/deps/cryptol b/deps/cryptol
diff --git a/deps/macaw b/deps/macaw
diff --git a/deps/saw-core b/deps/saw-core
diff --git a/deps/what4 b/deps/what4
diff --git a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs
@@ -103,7 +103,7 @@ typeOfSetupValue _cc env _nameEnv val =
     MS.SetupTerm tt ->
       case ttSchema tt of
         Cryptol.Forall [] [] ty ->
-          case toJVMType (Cryptol.evalValType Map.empty ty) of
+          case toJVMType (Cryptol.evalValType mempty ty) of
             Nothing -> fail "typeOfSetupValue: non-representable type"
             Just jty -> return jty
         s -> fail $ unlines [ "typeOfSetupValue: expected monomorphic term"
@@ -158,7 +158,7 @@ resolveTypedTerm ::
 resolveTypedTerm cc tm =
   case ttSchema tm of
     Cryptol.Forall [] [] ty ->
-      resolveSAWTerm cc (Cryptol.evalValType Map.empty ty) (ttTerm tm)
+      resolveSAWTerm cc (Cryptol.evalValType mempty ty) (ttTerm tm)
     _ -> fail "resolveSetupVal: expected monomorphic term"
 
 resolveSAWPred ::

diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs
@@ -152,7 +152,7 @@ ppLLVMVal ::
 ppLLVMVal cc val = do
   sym <- Ov.getSymInterface
   mem <- readGlobal (Crucible.llvmMemVar (ccLLVMContext cc))
-  liftIO $ Crucible.ppLLVMValWithGlobals sym (Crucible.memImplGlobalMap mem) val
+  pure $ Crucible.ppLLVMValWithGlobals sym (Crucible.memImplSymbolMap mem) val
 
 -- | Resolve a 'SetupValue' into a 'LLVMVal' and pretty-print it
 ppSetupValueAsLLVMVal ::
@@ -336,7 +336,7 @@ ppArgs sym cc cs (Crucible.RegMap args) = do
   case Crucible.lookupGlobal (Crucible.llvmMemVar (ccLLVMContext cc)) (cc^.ccLLVMGlobals) of
     Nothing -> fail "Internal error: Couldn't find LLVM memory variable"
     Just mem -> do
-      traverse (Crucible.ppLLVMValWithGlobals sym (Crucible.memImplGlobalMap mem) . fst) =<<
+      map (Crucible.ppLLVMValWithGlobals sym (Crucible.memImplSymbolMap mem) . fst) <$>
         liftIO (zipWithM aux expectedArgTypes (assignmentToList args))
 
 -- | This function is responsible for implementing the \"override\" behavior

diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
@@ -182,7 +182,7 @@ typeOfSetupValue' cc env nameEnv val =
     SetupTerm tt ->
       case ttSchema tt of
         Cryptol.Forall [] [] ty ->
-          case toLLVMType dl (Cryptol.evalValType Map.empty ty) of
+          case toLLVMType dl (Cryptol.evalValType mempty ty) of
             Left err -> fail (toLLVMTypeErrToString err)
             Right memTy -> return memTy
         s -> fail $ unlines [ "typeOfSetupValue: expected monomorphic term"
@@ -345,7 +345,7 @@ resolveTypedTerm ::
 resolveTypedTerm cc tm =
   case ttSchema tm of
     Cryptol.Forall [] [] ty ->
-      resolveSAWTerm cc (Cryptol.evalValType Map.empty ty) (ttTerm tm)
+      resolveSAWTerm cc (Cryptol.evalValType mempty ty) (ttTerm tm)
     _ -> fail "resolveSetupVal: expected monomorphic term"
 
 resolveSAWPred ::
@@ -650,7 +650,7 @@ memArrayToSawCoreTerm crucible_context endianess typed_term = do
 
   case ttSchema typed_term of
     Cryptol.Forall [] [] cryptol_type -> do
-      let evaluated_type = (Cryptol.evalValType Map.empty cryptol_type)
+      let evaluated_type = Cryptol.evalValType mempty cryptol_type
       fresh_array_const <- scFreshGlobal saw_context "arr"
         =<< scArrayType saw_context offset_type_term byte_type_term
       execStateT
+34 −22		crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
+19 −28		crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs
+9 −6		crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Value.hs
+50 −0		.github/workflows/ci.yaml
+5 −5		.gitignore
+0 −30		.travis.yml
+48 −57		cabal.project.dist.ghc-8.8.4.freeze
+8 −0		cabal.project.werror
+34 −13		cryptol-saw-core/saw/Cryptol.sawcore
+9 −3		cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
+4 −0		cryptol-saw-core/test/instance.cry
+1 −1		what4/src/What4/Interface.hs
+16 −0		what4/test/ExprBuilderSMTLib2.hs