Merge branch 'master' into coq-prelude-update

GaloisInc · Sep 8, 2021 · 4944043 · 4944043
2 parents 8f084ac + ce2dd0f
commit 4944043
Show file tree

Hide file tree

Showing 57 changed files with 1,397 additions and 259 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -62,6 +62,9 @@ jobs:
       matrix:
         os: [ubuntu-18.04, macos-latest, windows-latest]
         ghc: ["8.8.4", "8.10.3"]
+        exclude:
+          - os: windows-latest
+            ghc: "8.8.4"
     outputs:
       cabal-test-suites-json: ${{ steps.cabal-test-suites.outputs.targets-json }}
     steps:
@@ -119,15 +122,15 @@ jobs:
           dest: dist-tests
 
       - if: |
-          matrix.ghc == '8.8.4' &&
+          matrix.ghc == '8.10.3' &&
           runner.os != 'Windows'
         uses: actions/upload-artifact@v2
         with:
           path: ${{ steps.abc.outputs.path }}
           name: abc-${{ runner.os }}
 
       - uses: actions/upload-artifact@v2
-        if: "matrix.ghc == '8.8.4'"
+        if: "matrix.ghc == '8.10.3'"
         with:
           path: dist-tests
           name: dist-tests-${{ matrix.os }}
@@ -141,22 +144,22 @@ jobs:
       - shell: bash
         run: .github/ci.sh zip_dist $NAME
 
-      - if: matrix.ghc == '8.8.4' && needs.config.outputs.release == 'true'
+      - if: matrix.ghc == '8.10.3' && needs.config.outputs.release == 'true'
         shell: bash
         env:
           SIGNING_PASSPHRASE: ${{ secrets.SIGNING_PASSPHRASE }}
           SIGNING_KEY: ${{ secrets.SIGNING_KEY }}
         run: .github/ci.sh sign $NAME.tar.gz
 
-      - if: matrix.ghc == '8.8.4'
+      - if: matrix.ghc == '8.10.3'
         uses: actions/upload-artifact@v2
         with:
           name: ${{ steps.config.outputs.name }} (GHC ${{ matrix.ghc }})
           path: "${{ steps.config.outputs.name }}.tar.gz*"
           if-no-files-found: error
           retention-days: ${{ needs.config.outputs.retention-days }}
 
-      - if: "matrix.ghc == '8.8.4'"
+      - if: "matrix.ghc == '8.10.3'"
         uses: actions/upload-artifact@v2
         with:
           path: dist/bin
@@ -506,7 +509,6 @@ jobs:
       - heapster-tests
       - saw-remote-api-tests
       - cabal-test
-      - build-push-image
       - s2n-tests
     steps:
       - run: "true"
diff --git a/cabal.GHC-8.10.3.config b/cabal.GHC-8.10.3.config
@@ -298,7 +298,7 @@ constraints: any.Cabal ==3.2.1.0,
              any.text-short ==0.1.3,
              text-short -asserts,
              any.tf-random ==0.5,
-             any.th-abstraction ==0.3.2.0,
+             any.th-abstraction ==0.4.2.0,
              any.th-compat ==0.1.1,
              any.th-expand-syns ==0.4.6.0,
              any.th-lift ==0.8.2,

diff --git a/cabal.GHC-8.8.4.config b/cabal.GHC-8.8.4.config
@@ -300,7 +300,7 @@ constraints: any.Cabal ==3.0.1.0,
              any.text-short ==0.1.3,
              text-short -asserts,
              any.tf-random ==0.5,
-             any.th-abstraction ==0.3.2.0,
+             any.th-abstraction ==0.4.2.0,
              any.th-compat ==0.1.1,
              any.th-expand-syns ==0.4.6.0,
              any.th-lift ==0.8.2,

diff --git a/cabal.project b/cabal.project
@@ -22,6 +22,7 @@ packages:
     deps/crucible/crucible-jvm
     deps/crucible/crucible-llvm
     deps/crucible/crucible-saw
+    deps/crucible/crucible-symio
     deps/crucible/crucible-syntax
     deps/crucible/crux
     deps/crucible/crux-mir
@@ -42,4 +43,4 @@ packages:
 source-repository-package
     type: git
     location: https://github.com/eddywestbrook/hobbits.git
-    tag: e5918895396b6bcee2fc39f6bd0d77a90a52ba5f
+    tag: 20b6d18758312deaf6a544d474483e537d5f018f
diff --git a/cryptol-saw-core/saw/Cryptol.sawcore b/cryptol-saw-core/saw/Cryptol.sawcore
@@ -1741,6 +1741,15 @@ ecArrayLookup = arrayLookup;
 ecArrayUpdate : (a b : sort 0) -> (Array a b) -> a -> b -> (Array a b);
 ecArrayUpdate = arrayUpdate;
 
+ecArrayCopy : (n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> Array (seq n Bool) a -> seq n Bool -> seq n Bool -> Array (seq n Bool) a;
+ecArrayCopy = finNumRec (\(n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> Array (seq n Bool) a -> seq n Bool -> seq n Bool -> Array (seq n Bool) a) arrayCopy;
+
+ecArraySet : (n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> a -> seq n Bool -> Array (seq n Bool) a;
+ecArraySet = finNumRec (\(n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> a -> seq n Bool -> Array (seq n Bool) a) arraySet;
+
+ecArrayRangeEq : (n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> Array (seq n Bool) a -> seq n Bool -> seq n Bool -> Bool;
+ecArrayRangeEq = finNumRec (\(n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> Array (seq n Bool) a -> seq n Bool -> seq n Bool -> Bool) arrayRangeEq;
+
 --------------------------------------------------------------------------------
 -- Suite-B Primitives
 

diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
@@ -809,6 +809,9 @@ arrayPrims =
   [ ("arrayConstant", flip scGlobalDef "Cryptol.ecArrayConstant") -- {a,b} b -> Array a b
   , ("arrayLookup",   flip scGlobalDef "Cryptol.ecArrayLookup") -- {a,b} Array a b -> a -> b
   , ("arrayUpdate",   flip scGlobalDef "Cryptol.ecArrayUpdate") -- {a,b} Array a b -> a -> b -> Array a b
+  , ("arrayCopy", flip scGlobalDef "Cryptol.ecArrayCopy") -- {n,a} Array [n] a -> [n] -> Array [n] a -> [n] -> [n] -> Array [n] a
+  , ("arraySet", flip scGlobalDef "Cryptol.ecArraySet") -- {n,a} Array [n] a -> [n] -> a -> [n] -> Array [n] a
+  , ("arrayRangeEqual", flip scGlobalDef "Cryptol.ecArrayRangeEq") -- {n,a} Array [n] a -> [n] -> Array [n] a -> [n] -> [n] -> Bit
   ]
 
 floatPrims :: Map C.PrimIdent (SharedContext -> IO Term)

diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
@@ -83,7 +83,7 @@ import qualified Cryptol.ModuleSystem.Renamer as MR
 
 import qualified Cryptol.Utils.Ident as C
 
-import Cryptol.Utils.PP
+import Cryptol.Utils.PP hiding ((</>))
 import Cryptol.Utils.Ident (Ident, preludeName, preludeReferenceName
                            , packIdent, interactiveName, identText
                            , packModName, textToModName, modNameChunks

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/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/what4 b/deps/what4
+1 −1		.github/workflows/ci.yml
+0 −0		.gitmodules
+3 −1		argo/argo.cabal
+303 −110		argo/src/Argo.hs
+53 −16		argo/src/Argo/DefaultMain.hs
+73 −15		argo/src/Argo/ServerState.hs
+2 −1		file-echo-api/file-echo-api.cabal
+4 −0		file-echo-api/file-echo-api/Main.hs
+3 −0		file-echo-api/mutable-file-echo-api/Main.hs
+91 −0		file-echo-api/src/FileEchoServer.hs
+77 −0		file-echo-api/src/MutableFileEchoServer.hs
+18 −2		python/CHANGELOG.md
+43 −10		python/argo_client/connection.py
+12 −4		python/argo_client/interaction.py
+1 −1		python/setup.py
+375 −54		python/tests/test_file_echo_api.py
+63 −1		python/tests/test_file_echo_interaction.py
+133 −26		python/tests/test_mutable_file_echo_api.py
+0 −61		stack.yaml
+1 −0		.github/workflows/ci.yml
+6 −0		cryptol-remote-api/python/CHANGELOG.md
+1 −1		cryptol-remote-api/python/cryptol/commands.py
+7 −7		cryptol-remote-api/python/poetry.lock
+2 −2		cryptol-remote-api/python/pyproject.toml
+25 −0		cryptol-remote-api/python/tests/cryptol/test-files/Types.cry
+2 −2		cryptol-remote-api/python/tests/cryptol/test_AES.py
+1 −1		cryptol-remote-api/python/tests/cryptol/test_DES.py
+32 −0		cryptol-remote-api/python/tests/cryptol/test_error_recovery.py
+45 −0		cryptol-remote-api/python/tests/cryptol/test_types.py
+2 −2		cryptol.cabal
+1 −1		cryptol/REPL/Haskeline.hs
+1 −1		deps/argo
+ −		docs/ProgrammingCryptol.pdf
+5 −5		docs/ProgrammingCryptol/crashCourse/CrashCourse.tex
+ −		docs/Semantics.pdf
+44 −0		lib/Array.cry
+1 −1		src/Cryptol/Backend/Concrete.hs
+1 −1		src/Cryptol/Eval/Concrete.hs
+3 −4		src/Cryptol/Eval/Reference.lhs
+6 −9		src/Cryptol/Eval/Value.hs
+1 −1		src/Cryptol/ModuleSystem/Monad.hs
+1 −1		src/Cryptol/ModuleSystem/NamingEnv.hs
+14 −14		src/Cryptol/ModuleSystem/Renamer/Error.hs
+39 −35		src/Cryptol/Parser/AST.hs
+2 −2		src/Cryptol/Parser/Name.hs
+1 −1		src/Cryptol/Parser/NoInclude.hs
+9 −9		src/Cryptol/Parser/ParserUtils.hs
+5 −5		src/Cryptol/Parser/Selector.hs
+25 −25		src/Cryptol/REPL/Browse.hs
+25 −24		src/Cryptol/REPL/Command.hs
+3 −3		src/Cryptol/REPL/Monad.hs
+3 −3		src/Cryptol/Symbolic.hs
+4 −6		src/Cryptol/TypeCheck.hs
+23 −22		src/Cryptol/TypeCheck/AST.hs
+49 −49		src/Cryptol/TypeCheck/Error.hs
+26 −24		src/Cryptol/TypeCheck/InferTypes.hs
+20 −8		src/Cryptol/TypeCheck/Parseable.hs
+1 −2		src/Cryptol/TypeCheck/SimpleSolver.hs
+1 −1		src/Cryptol/TypeCheck/Solver/SMT.hs
+26 −25		src/Cryptol/TypeCheck/Type.hs
+1 −1		src/Cryptol/TypeCheck/TypeOf.hs
+77 −63		src/Cryptol/Utils/PP.hs
+2 −1		tests/examples/allexamples.icry.stdout
+10 −5		tests/issues/issue1024.icry.stdout
+3 −3		tests/issues/issue152.icry.stdout
+25 −31		tests/issues/issue226.icry.stdout
+6 −6		tests/issues/issue268.icry.stdout
+3 −4		tests/issues/issue407.icry.stdout
+3 −7		tests/issues/issue410.icry.stdout
+1 −2		tests/issues/issue494.icry.stdout
+10 −9		tests/issues/issue513.icry.stdout
+4 −2		tests/issues/issue702.icry.stdout
+2 −1		tests/issues/issue894.icry.stdout
+2 −2		tests/issues/padding.icry.stdout
+2 −1		tests/modsys/nested/T1.icry.stdout
+8 −4		tests/modsys/nested/T2.icry.stdout
+16 −16		tests/mono-binds/test01.icry.stdout
+20 −20		tests/mono-binds/test02.icry.stdout
+16 −16		tests/mono-binds/test03.icry.stdout
+8 −8		tests/mono-binds/test04.icry.stdout
+25 −24		tests/mono-binds/test05.icry.stdout
+24 −24		tests/mono-binds/test06.icry.stdout
+11 −0		tests/regression/array.icry.stdout
+1 −1		tests/regression/float.icry.stdout
+35 −44		tests/regression/instance.icry.stdout
+4 −4		tests/regression/rec-update.icry.stdout
+3 −3		tests/regression/repl-decls.icry.stdout
+2 −2		tests/regression/sort.icry.stdout
+25 −26		tests/regression/specialize.icry.stdout
+1 −2		tests/regression/superclass.icry.stdout
+1 −6		.github/workflows/build.yml
+3 −6		.github/workflows/llvm-quick-fuzz.yml
+0 −1		.gitignore
+3 −0		.gitmodules
+14 −0		disasm-test/tests/fneg.ll
+10 −26		doc/developing.md
+1 −0		llvm-pretty
+26 −0		src/Data/LLVM/BitCode/IR/Constants.hs
+85 −59		src/Data/LLVM/BitCode/IR/Function.hs
+3 −0		src/Data/LLVM/BitCode/IR/Module.hs
+9 −8		src/Data/LLVM/BitCode/Parse.hs
+1 −0		unit-test/Tests/Instances.hs
+1 −0		cabal.project.dist
+1 −1		deps/crucible
+1 −1		deps/macaw-loader
+1 −1		deps/semmc
+1 −0		macaw-aarch32-symbolic/macaw-aarch32-symbolic.cabal
+3 −0		macaw-aarch32-symbolic/tests/Main.hs
+1 −0		macaw-ppc-symbolic/macaw-ppc-symbolic.cabal
+3 −0		macaw-ppc-symbolic/tests/Main.hs
+5 −7		macaw-ppc/src/Data/Macaw/PPC.hs
+29 −1		macaw-ppc/src/Data/Macaw/PPC/Arch.hs
+7 −8		macaw-ppc/src/Data/Macaw/PPC/Eval.hs
+2 −1		refinement/macaw-refinement.cabal
+7 −0		refinement/src/Data/Macaw/Refinement.hs
+2 −0		refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
+7 −0		refinement/src/Data/Macaw/Refinement/UnknownTransfer.hs
+3 −2		refinement/tests/RefinementTests.hs
+4 −1		refinement/tools/Initialization.hs
+3 −0		refinement/tools/run-refinement.hs
+8 −5		symbolic/src/Data/Macaw/Symbolic.hs
+2 −2		symbolic/src/Data/Macaw/Symbolic/MemOps.hs
+1 −0		symbolic/src/Data/Macaw/Symbolic/Memory.hs
+2 −0		symbolic/src/Data/Macaw/Symbolic/Testing.hs
+3 −1		x86_symbolic/src/Data/Macaw/X86/Crucible.hs
+3 −2		x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
+3 −0		x86_symbolic/tests/Main.hs
+2 −2		what4/README.md
+72 −0		what4/src/What4/Expr/App.hs
+4 −1		what4/src/What4/Expr/AppTheory.hs
+161 −7		what4/src/What4/Expr/Builder.hs
+77 −22		what4/src/What4/Expr/GroundEval.hs
+18 −17		what4/src/What4/Expr/VarIdentification.hs
+57 −0		what4/src/What4/Interface.hs
+64 −0		what4/src/What4/Protocol/SMTWriter.hs
+3 −0		what4/src/What4/Protocol/VerilogWriter/Backend.hs
+1 −1		what4/src/What4/Solver/Boolector.hs
+75 −0		what4/test/ExprBuilderSMTLib2.hs