GaloisInc · brianhuffman · Jan 7, 2021 · Jan 6, 2021 · Nov 18, 2020 · Jan 7, 2021
diff --git a/deps/argo b/deps/argo
diff --git a/deps/crucible b/deps/crucible
diff --git a/deps/cryptol b/deps/cryptol
diff --git a/deps/cryptol-specs b/deps/cryptol-specs
diff --git a/deps/elf-edit b/deps/elf-edit
diff --git a/deps/llvm-pretty b/deps/llvm-pretty
diff --git a/deps/llvm-pretty-bc-parser b/deps/llvm-pretty-bc-parser
diff --git a/deps/macaw b/deps/macaw
diff --git a/deps/saw-core b/deps/saw-core
diff --git a/deps/saw-core-coq b/deps/saw-core-coq
diff --git a/s2nTests/docker/awslc.dockerfile b/s2nTests/docker/awslc.dockerfile
@@ -8,7 +8,7 @@ WORKDIR /saw-script
 RUN mkdir -p /saw-script && \
     git clone https://github.com/GaloisInc/aws-lc-verification.git && \
     cd aws-lc-verification && \
-    git checkout fe647883ee5cc84309cc71d5e1e2cbce0b27be23 && \
+    git checkout 7f648fffe7a1f1097171279001ddab359a5749ab && \
     git config --file=.gitmodules submodule.src.url https://github.com/awslabs/aws-lc && \
     git submodule sync && \
     git submodule update --init

diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs
@@ -435,10 +435,7 @@ setupPrePointsTos mspec cc env pts mem0 = foldM doPointsTo mem0 pts
         JVMPointsToField _loc lhs fid rhs ->
           do lhs' <- resolveJVMRefVal lhs
              rhs' <- resolveSetupVal cc env tyenv nameEnv rhs
-             -- TODO: Change type of CJ.doFieldStore to take a FieldId instead of a String.
-             -- Then we won't have to match the definition of 'fieldIdText' here.
-             let key = J.unClassName (J.fieldIdClass fid) ++ "." ++ J.fieldIdName fid
-             CJ.doFieldStore sym mem lhs' key (injectJVMVal sym rhs')
+             CJ.doFieldStore sym mem lhs' fid (injectJVMVal sym rhs')
         JVMPointsToElem _loc lhs idx rhs ->
           do lhs' <- resolveJVMRefVal lhs
              rhs' <- resolveSetupVal cc env tyenv nameEnv rhs

diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs
@@ -663,10 +663,7 @@ learnPointsTo opts sc cc spec prepost pt = do
     JVMPointsToField loc ptr fid val ->
       do ty <- typeOfSetupValue cc tyenv nameEnv val
          rval <- resolveAllocIndexJVM ptr
-         -- TODO: Change type of CJ.doFieldStore to take a FieldId instead of a String.
-         -- Then we won't have to match the definition of 'fieldIdText' here.
-         let key = J.unClassName (J.fieldIdClass fid) ++ "." ++ J.fieldIdName fid
-         dyn <- liftIO $ CJ.doFieldLoad sym globals rval key
+         dyn <- liftIO $ CJ.doFieldLoad sym globals rval fid
          v <- liftIO $ projectJVMVal sym ty ("field load " ++ J.fieldIdName fid ++ ", " ++ show loc) dyn
          matchArg opts sc cc spec prepost v ty val
 
@@ -810,10 +807,7 @@ executePointsTo opts sc cc spec pt = do
       do (_, val') <- resolveSetupValueJVM opts cc sc spec val
          rval <- resolveAllocIndexJVM ptr
          let dyn = injectJVMVal sym val'
-         -- TODO: Change type of CJ.doFieldStore to take a FieldId instead of a String.
-         -- Then we won't have to match the definition of 'fieldIdText' here.
-         let key = J.unClassName (J.fieldIdClass fid) ++ "." ++ J.fieldIdName fid
-         globals' <- liftIO $ CJ.doFieldStore sym globals rval key dyn
+         globals' <- liftIO $ CJ.doFieldStore sym globals rval fid dyn
          OM (overrideGlobals .= globals')
 
     JVMPointsToElem _loc ptr idx val ->
+3 −1		NEWS.rst
+21 −29		argo/src/Argo.hs
+137 −39		argo/src/Argo/DefaultMain.hs
+1 −1		argo/src/Argo/Netstring.hs
+20 −20		argo/src/Argo/Socket.hs
+5 −0		file-echo-api/README.rst
+1 −0		file-echo-api/file-echo-api.cabal
+23 −6		file-echo-api/file-echo-api/Main.hs
+32 −9		file-echo-api/src/FileEchoServer.hs
+39 −0		file-echo-api/test-scripts/file-echo-tests.py
+2 −1		.gitignore
+2 −2		crucible-jvm/src/Lang/Crucible/JVM/Context.hs
+56 −14		crucible-jvm/src/Lang/Crucible/JVM/Simulate.hs
+7 −7		crucible-jvm/src/Lang/Crucible/JVM/Translation/Class.hs
+19 −14		crucible-jvm/src/Lang/Crucible/JVM/Translation/Monad.hs
+134 −10		crucible-llvm/test/Tests.hs
+10 −2		crux-llvm/README.md
+29 −11		crux-llvm/crux-llvm.cabal
+4 −0		crux-llvm/exe/Main.hs
+2 −2		crux-llvm/src/Crux/LLVM/Compile.hs
+6 −1		crux-llvm/svcomp/Main.hs
+2 −1		crux-mir/src/Mir/DefId.hs
+9 −4		crux-mir/src/Mir/Generator.hs
+1 −1		crux-mir/src/Mir/Language.hs
+6 −6		crux-mir/src/Mir/Trans.hs
+0 −1		crux/crux.cabal
+21 −17		crux/src/Crux/Config/Doc.hs
+11 −12		crux/src/Crux/Model.hs
+13 −17		crux/src/Crux/Types.hs
+191 −0		cryptol-remote-api/README.rst
+35 −5		cryptol-remote-api/src/CryptolServer/Data/Expression.hs
+89 −1		cryptol-remote-api/src/CryptolServer/Data/Type.hs
+31 −0		cryptol-remote-api/test-scripts/cryptol-tests.py
+6 −0		cryptol-remote-api/test-scripts/test-data/M.cry
+54 −0		.github/workflows/build.yml
+70 −0		.github/workflows/llvm-quick-fuzz.yml
+0 −135		.travis.yml
+48 −27		fuzzing/Main.hs
+4 −2		llvm-disasm/LLVMDis.hs
+40 −20		src/Data/LLVM/BitCode/IR/Metadata.hs
+13 −4		.github/workflows/ci.yaml
+2 −0		base/src/Data/Macaw/Dwarf.hs
+1 −3		cabal.project.werror
+3 −5		macaw-ppc/tests/PPC64InstructionCoverage.hs
+5 −6		macaw-ppc/tests/PPC64Tests.hs
+14 −10		macaw-ppc/tests/Shared.hs
+1 −1		refinement/macaw-refinement.cabal
+41 −10		x86/src/Data/Macaw/X86/Semantics.hs