Merge pull request #992 from GaloisInc/update-deps

Update deps
GaloisInc · Jan 7, 2021 · 898e663 · 898e663
2 parents c0d8419 + 00db441
commit 898e663
Show file tree

Hide file tree

Showing 13 changed files with 14 additions and 23 deletions.
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 ->