diff --git a/deps/argo b/deps/argo index 5217d1da92..7d2c208502 160000 --- a/deps/argo +++ b/deps/argo @@ -1 +1 @@ -Subproject commit 5217d1da928a5d1902186db991dacb047d1da5d7 +Subproject commit 7d2c2085021825668412c62d31534568447d0fdc diff --git a/deps/crucible b/deps/crucible index c1da81f05e..b8c1b15fd4 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit c1da81f05e7a8ac80787e2f161ba341a312a6302 +Subproject commit b8c1b15fd4f3d11ea21bbf1ecaba320848e513d6 diff --git a/deps/cryptol b/deps/cryptol index a506732dc6..be24bfe260 160000 --- a/deps/cryptol +++ b/deps/cryptol @@ -1 +1 @@ -Subproject commit a506732dc63cf5bd78f18ac7ac525926c805a2b6 +Subproject commit be24bfe26058b3ad94bed2fda1065e0f801a7e9c diff --git a/deps/cryptol-specs b/deps/cryptol-specs index 0cc5e35b35..01acf50da7 160000 --- a/deps/cryptol-specs +++ b/deps/cryptol-specs @@ -1 +1 @@ -Subproject commit 0cc5e35b35eba6f30d163506a06afd8cfd4478e7 +Subproject commit 01acf50da70e39660afe1afd41cdab255137eca0 diff --git a/deps/elf-edit b/deps/elf-edit index fe018fbf6c..a440cefb13 160000 --- a/deps/elf-edit +++ b/deps/elf-edit @@ -1 +1 @@ -Subproject commit fe018fbf6c2df56fc3f565d2732780c064228f1b +Subproject commit a440cefb1317eaa198146469695e9a8fdc066b57 diff --git a/deps/llvm-pretty b/deps/llvm-pretty index cf5c931061..f5e0ff3f3f 160000 --- a/deps/llvm-pretty +++ b/deps/llvm-pretty @@ -1 +1 @@ -Subproject commit cf5c931061b48a4253e7eea15947eff7d9790f07 +Subproject commit f5e0ff3f3f6154842d3321031ca5a5031c91ecc6 diff --git a/deps/llvm-pretty-bc-parser b/deps/llvm-pretty-bc-parser index 3d0d549486..c38b86b8b4 160000 --- a/deps/llvm-pretty-bc-parser +++ b/deps/llvm-pretty-bc-parser @@ -1 +1 @@ -Subproject commit 3d0d549486ceb101c38af3423426f3ff07aa966d +Subproject commit c38b86b8b485c85181ab1bfc682fae194c8d4027 diff --git a/deps/macaw b/deps/macaw index 7761a6f6e1..2bd0633ba8 160000 --- a/deps/macaw +++ b/deps/macaw @@ -1 +1 @@ -Subproject commit 7761a6f6e1348e6479b2ad272ad47e59fb5a8fd7 +Subproject commit 2bd0633ba83a2bfb4fb6c7ca6f61d419bdae7565 diff --git a/deps/saw-core b/deps/saw-core index f61023ebbb..40da8772ca 160000 --- a/deps/saw-core +++ b/deps/saw-core @@ -1 +1 @@ -Subproject commit f61023ebbb34c2d6acbda9fc2eb2d0ba0884604c +Subproject commit 40da8772ca86cee7c762ac0e5847ba5e78d8fff4 diff --git a/deps/saw-core-coq b/deps/saw-core-coq index 8b4df2dc63..7978fdc139 160000 --- a/deps/saw-core-coq +++ b/deps/saw-core-coq @@ -1 +1 @@ -Subproject commit 8b4df2dc63dab5297126f264ae1ede788a722e04 +Subproject commit 7978fdc13901045f6758b66061120ce6e1a6417e diff --git a/s2nTests/docker/awslc.dockerfile b/s2nTests/docker/awslc.dockerfile index 0d2eb44133..a7eb8bd300 100644 --- 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 index 14cd9f8a05..4c7a6060af 100644 --- 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 index 21cb9b493b..4729cc1522 100644 --- 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 ->