Merge pull request #1171 from GaloisInc/crux-0.8-forward-port

Forward-port Crux 0.8 changes to `master` branch
GaloisInc · Feb 6, 2024 · 87fc19c · 87fc19c
2 parents 6157bbe + 3633bd7
commit 87fc19c
Show file tree

Hide file tree

Showing 34 changed files with 194 additions and 66 deletions.
diff --git a/.github/workflows/crux-llvm-build.yml b/.github/workflows/crux-llvm-build.yml
@@ -31,7 +31,7 @@ jobs:
       event-tag: ${{ steps.config.outputs.tag }}
       event-schedule: ${{ steps.config.outputs.schedule }}
       publish: ${{ steps.config.outputs.publish }}
-      release: ${{ steps.env.outputs.release }}
+      release: ${{ steps.config.outputs.release }}
       retention-days: ${{ steps.config.outputs.retention-days }}
     steps:
       - uses: actions/checkout@v2
@@ -52,7 +52,7 @@ jobs:
           .github/ci.sh output tag $EVENT_TAG
           .github/ci.sh output schedule $EVENT_SCHEDULE
           .github/ci.sh output publish $({ $EVENT_TAG || $EVENT_SCHEDULE; } && echo true || echo false)
-          .github/ci.sh output release $([[ "refs/heads/release-$(.github/ci.sh crux_llvm_ver)" == "${{ github.event.ref }}" ]] && echo true || echo false)
+          .github/ci.sh output release $([[ "refs/heads/release-crux-$(.github/ci.sh crux_llvm_ver)" == "${{ github.event.ref }}" ]] && echo true || echo false)
           .github/ci.sh output retention-days $($RELEASE && echo 90 || echo 5)
 
   build:
@@ -369,9 +369,9 @@ jobs:
           docker push ${{ matrix.image }}:nightly
 
       - if: needs.config.outputs.release == 'true'
-        name: ${{ matrix.image }}:${{ needs.config.outputs.version }}
+        name: ${{ matrix.image }}:${{ needs.config.outputs.crux-llvm-version }}
         run: |
-          docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:${{ needs.config.outputs.version }}
-          docker push ${{ matrix.image }}:${{ needs.config.outputs.version }}
+          docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:${{ needs.config.outputs.crux-llvm-version }}
+          docker push ${{ matrix.image }}:${{ needs.config.outputs.crux-llvm-version }}
           docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:latest
           docker push ${{ matrix.image }}:latest
diff --git a/.github/workflows/crux-mir-build.yml b/.github/workflows/crux-mir-build.yml
@@ -33,7 +33,7 @@ jobs:
       event-tag: ${{ steps.config.outputs.tag }}
       event-schedule: ${{ steps.config.outputs.schedule }}
       publish: ${{ steps.config.outputs.publish }}
-      release: ${{ steps.env.outputs.release }}
+      release: ${{ steps.config.outputs.release }}
       retention-days: ${{ steps.config.outputs.retention-days }}
     steps:
       - uses: actions/checkout@v2
@@ -54,7 +54,7 @@ jobs:
           .github/ci.sh output tag $EVENT_TAG
           .github/ci.sh output schedule $EVENT_SCHEDULE
           .github/ci.sh output publish $({ $EVENT_TAG || $EVENT_SCHEDULE; } && echo true || echo false)
-          .github/ci.sh output release $([[ "refs/heads/release-$(.github/ci.sh crux_mir_ver)" == "${{ github.event.ref }}" ]] && echo true || echo false)
+          .github/ci.sh output release $([[ "refs/heads/release-crux-$(.github/ci.sh crux_mir_ver)" == "${{ github.event.ref }}" ]] && echo true || echo false)
           .github/ci.sh output retention-days $($RELEASE && echo 90 || echo 5)
 
   build:
@@ -276,9 +276,9 @@ jobs:
           docker push ${{ matrix.image }}:nightly
 
       - if: needs.config.outputs.release == 'true'
-        name: ${{ matrix.image }}:${{ needs.config.outputs.version }}
+        name: ${{ matrix.image }}:${{ needs.config.outputs.crux-mir-version }}
         run: |
-          docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:${{ needs.config.outputs.version }}
-          docker push ${{ matrix.image }}:${{ needs.config.outputs.version }}
+          docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:${{ needs.config.outputs.crux-mir-version }}
+          docker push ${{ matrix.image }}:${{ needs.config.outputs.crux-mir-version }}
           docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:latest
           docker push ${{ matrix.image }}:latest
diff --git a/cabal.GHC-8.10.7.config b/cabal.GHC-8.10.7.config
@@ -26,7 +26,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              atomic-primops -debug,
              any.attoparsec ==0.14.4,
              attoparsec -developer,
-             any.barbies ==2.0.5.0,
+             any.barbies ==2.1.1.0,
              any.base ==4.14.3.0,
              any.base-compat ==0.13.1,
              any.base-compat-batteries ==0.13.1,
@@ -179,7 +179,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.profunctors ==5.6.2,
              any.pvar ==1.0.0.0,
              any.quickcheck-io ==0.2.0,
-             any.random ==1.2.1.1,
+             any.random ==1.2.1.2,
              any.raw-strings-qq ==1.1,
              any.reflection ==2.1.7,
              reflection -slow +template-haskell,
@@ -191,7 +191,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.rts ==1.0.1,
              any.s-cargot ==0.1.6.0,
              s-cargot -build-example,
-             any.safe ==0.3.20,
+             any.safe ==0.3.21,
              any.safe-exceptions ==0.1.7.4,
              any.scheduler ==2.0.0.1,
              any.scientific ==0.3.7.0,
@@ -211,7 +211,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.streaming-commons ==0.2.2.6,
              streaming-commons -use-bytestring-builder,
              any.strict ==0.5,
-             any.string-interpolate ==0.3.2.1,
+             any.string-interpolate ==0.3.3.0,
              string-interpolate -bytestring-builder -extended-benchmarks -text-builder,
              any.syb ==0.7.2.4,
              any.tagged ==0.8.8,
@@ -271,7 +271,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.vector-algorithms ==0.9.0.1,
              vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks,
              any.vector-stream ==0.1.0.1,
-             any.versions ==6.0.4,
+             any.versions ==6.0.5,
              any.void ==0.7.3,
              void -safe,
              any.websockets ==0.13.0.0,
@@ -286,4 +286,4 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.zlib ==0.6.3.0,
              zlib -bundled-c-zlib -non-blocking-ffi -pkg-config,
              any.zlib-bindings ==0.1.1.5
-index-state: hackage.haskell.org 2024-01-15T23:27:26Z
+index-state: hackage.haskell.org 2024-02-05T11:57:43Z
diff --git a/cabal.GHC-9.2.8.config b/cabal.GHC-9.2.8.config
@@ -26,7 +26,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              atomic-primops -debug,
              any.attoparsec ==0.14.4,
              attoparsec -developer,
-             any.barbies ==2.0.5.0,
+             any.barbies ==2.1.1.0,
              any.base ==4.16.4.0,
              any.base-compat ==0.13.1,
              any.base-compat-batteries ==0.13.1,
@@ -179,7 +179,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.profunctors ==5.6.2,
              any.pvar ==1.0.0.0,
              any.quickcheck-io ==0.2.0,
-             any.random ==1.2.1.1,
+             any.random ==1.2.1.2,
              any.raw-strings-qq ==1.1,
              any.reflection ==2.1.7,
              reflection -slow +template-haskell,
@@ -191,7 +191,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.rts ==1.0.2,
              any.s-cargot ==0.1.6.0,
              s-cargot -build-example,
-             any.safe ==0.3.20,
+             any.safe ==0.3.21,
              any.safe-exceptions ==0.1.7.4,
              any.scheduler ==2.0.0.1,
              any.scientific ==0.3.7.0,
@@ -211,7 +211,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.streaming-commons ==0.2.2.6,
              streaming-commons -use-bytestring-builder,
              any.strict ==0.5,
-             any.string-interpolate ==0.3.2.1,
+             any.string-interpolate ==0.3.3.0,
              string-interpolate -bytestring-builder -extended-benchmarks -text-builder,
              any.syb ==0.7.2.4,
              any.tagged ==0.8.8,
@@ -271,7 +271,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.vector-algorithms ==0.9.0.1,
              vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks,
              any.vector-stream ==0.1.0.1,
-             any.versions ==6.0.4,
+             any.versions ==6.0.5,
              any.void ==0.7.3,
              void -safe,
              any.websockets ==0.13.0.0,
@@ -286,4 +286,4 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.zlib ==0.6.3.0,
              zlib -bundled-c-zlib -non-blocking-ffi -pkg-config,
              any.zlib-bindings ==0.1.1.5
-index-state: hackage.haskell.org 2024-01-15T23:27:26Z
+index-state: hackage.haskell.org 2024-02-05T11:57:43Z
diff --git a/cabal.GHC-9.4.5.config b/cabal.GHC-9.4.5.config
@@ -27,7 +27,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              atomic-primops -debug,
              any.attoparsec ==0.14.4,
              attoparsec -developer,
-             any.barbies ==2.0.5.0,
+             any.barbies ==2.1.1.0,
              any.base ==4.17.1.0,
              any.base-compat ==0.13.1,
              any.base-compat-batteries ==0.13.1,
@@ -179,7 +179,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.profunctors ==5.6.2,
              any.pvar ==1.0.0.0,
              any.quickcheck-io ==0.2.0,
-             any.random ==1.2.1.1,
+             any.random ==1.2.1.2,
              any.raw-strings-qq ==1.1,
              any.reflection ==2.1.7,
              reflection -slow +template-haskell,
@@ -191,7 +191,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.rts ==1.0.2,
              any.s-cargot ==0.1.6.0,
              s-cargot -build-example,
-             any.safe ==0.3.20,
+             any.safe ==0.3.21,
              any.safe-exceptions ==0.1.7.4,
              any.scheduler ==2.0.0.1,
              any.scientific ==0.3.7.0,
@@ -211,7 +211,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.streaming-commons ==0.2.2.6,
              streaming-commons -use-bytestring-builder,
              any.strict ==0.5,
-             any.string-interpolate ==0.3.2.1,
+             any.string-interpolate ==0.3.3.0,
              string-interpolate -bytestring-builder -extended-benchmarks -text-builder,
              any.syb ==0.7.2.4,
              any.tagged ==0.8.8,
@@ -271,7 +271,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.vector-algorithms ==0.9.0.1,
              vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks,
              any.vector-stream ==0.1.0.1,
-             any.versions ==6.0.4,
+             any.versions ==6.0.5,
              any.void ==0.7.3,
              void -safe,
              any.websockets ==0.13.0.0,
@@ -286,4 +286,4 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.zlib ==0.6.3.0,
              zlib -bundled-c-zlib -non-blocking-ffi -pkg-config,
              any.zlib-bindings ==0.1.1.5
-index-state: hackage.haskell.org 2024-01-15T23:27:26Z
+index-state: hackage.haskell.org 2024-02-05T11:57:43Z
diff --git a/cabal.GHC-9.6.2.config b/cabal.GHC-9.6.2.config
@@ -27,7 +27,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              atomic-primops -debug,
              any.attoparsec ==0.14.4,
              attoparsec -developer,
-             any.barbies ==2.0.5.0,
+             any.barbies ==2.1.1.0,
              any.base ==4.18.0.0,
              any.base-compat ==0.13.1,
              any.base-compat-batteries ==0.13.1,
@@ -177,7 +177,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.profunctors ==5.6.2,
              any.pvar ==1.0.0.0,
              any.quickcheck-io ==0.2.0,
-             any.random ==1.2.1.1,
+             any.random ==1.2.1.2,
              any.raw-strings-qq ==1.1,
              any.reflection ==2.1.7,
              reflection -slow +template-haskell,
@@ -189,7 +189,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.rts ==1.0.2,
              any.s-cargot ==0.1.6.0,
              s-cargot -build-example,
-             any.safe ==0.3.20,
+             any.safe ==0.3.21,
              any.safe-exceptions ==0.1.7.4,
              any.scheduler ==2.0.0.1,
              any.scientific ==0.3.7.0,
@@ -209,7 +209,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.streaming-commons ==0.2.2.6,
              streaming-commons -use-bytestring-builder,
              any.strict ==0.5,
-             any.string-interpolate ==0.3.2.1,
+             any.string-interpolate ==0.3.3.0,
              string-interpolate -bytestring-builder -extended-benchmarks -text-builder,
              any.syb ==0.7.2.4,
              any.tagged ==0.8.8,
@@ -269,7 +269,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.vector-algorithms ==0.9.0.1,
              vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks,
              any.vector-stream ==0.1.0.1,
-             any.versions ==6.0.4,
+             any.versions ==6.0.5,
              any.void ==0.7.3,
              void -safe,
              any.websockets ==0.13.0.0,
@@ -284,4 +284,4 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.zlib ==0.6.3.0,
              zlib -bundled-c-zlib -non-blocking-ffi -pkg-config,
              any.zlib-bindings ==0.1.1.5
-index-state: hackage.haskell.org 2024-01-15T23:27:26Z
+index-state: hackage.haskell.org 2024-02-05T11:57:43Z
diff --git a/crucible-cli/CHANGELOG.md b/crucible-cli/CHANGELOG.md
@@ -0,0 +1,3 @@
+# 0.1 -- 2024-02-05
+
+* Initial version. Split off from `crucible-syntax`.
diff --git a/crucible-cli/crucible-cli.cabal b/crucible-cli/crucible-cli.cabal
@@ -10,7 +10,7 @@ Category:      Language
 Synopsis:      A library for sharing code between Crucible CLI frontends
 -- Description:
 
-extra-doc-files: README.md
+extra-doc-files: CHANGELOG.md, README.md
 extra-source-files:
   test-data/**/*.cbl
   test-data/**/*.out.good

diff --git a/crucible-concurrency/crucible-concurrency.cabal b/crucible-concurrency/crucible-concurrency.cabal
@@ -3,7 +3,7 @@ cabal-version:       2.4
 --   For further documentation, see http://haskell.org/cabal/users-guide/
 
 name:                crucible-concurrency
-version:             0.1.0.0
+version:             0.1
 -- synopsis:
 -- description:
 -- bug-reports:

diff --git a/crucible-go/CHANGELOG.md b/crucible-go/CHANGELOG.md
@@ -1,3 +1,4 @@
-# next
+# 0.1 -- 2024-02-05
 
-* TODO: Describe API changes here
+* Change `SomeOverride`, as well as related functions in
+  `Lang.Crucible.Go.Overrides`, to use a `TypedOverride`.
diff --git a/crucible-go/crucible-go.cabal b/crucible-go/crucible-go.cabal
@@ -1,5 +1,5 @@
 name:                crucible-go
-version:             0.1.0.0
+version:             0.1
 synopsis:            A Go frontend for Crucible
 license:             BSD3
 license-file:        LICENSE

diff --git a/crucible-jvm/CHANGELOG.md b/crucible-jvm/CHANGELOG.md
@@ -1,3 +1,4 @@
-# next
+# 0.2 -- 2024-02-05
 
-* TODO: Describe API changes here
+* Change `jvmOverride_def` in `Lang.Crucible.JVM.Overrides` to use a
+  `TypedOverride`.
diff --git a/crucible-llvm-cli/CHANGELOG.md b/crucible-llvm-cli/CHANGELOG.md
@@ -0,0 +1,3 @@
+# 0.1 -- 2024-02-05
+
+* Initial version.
diff --git a/crucible-llvm-cli/crucible-llvm-cli.cabal b/crucible-llvm-cli/crucible-llvm-cli.cabal
@@ -10,7 +10,7 @@ Category:      Language
 Synopsis:      A Crucible CLI frontend for the LLVM language extension
 -- Description:
 
-extra-doc-files: README.md
+extra-doc-files: CHANGELOG.md, README.md
 extra-source-files:
   test-data/*.cbl
   test-data/*.out.good

diff --git a/crucible-llvm-syntax/CHANGELOG.md b/crucible-llvm-syntax/CHANGELOG.md
@@ -0,0 +1,3 @@
+# 0.1 -- 2024-02-05
+
+* Initial version.
diff --git a/crucible-llvm-syntax/crucible-llvm-syntax.cabal b/crucible-llvm-syntax/crucible-llvm-syntax.cabal
@@ -10,7 +10,7 @@ Category:      Language
 Synopsis:      A syntax for reading and writing Crucible-LLVM control-flow graphs
 -- Description:
 
-extra-doc-files: README.md
+extra-doc-files: CHANGELOG.md, README.md
 extra-source-files:
   test-data/*.cbl
   test-data/*.out.good

diff --git a/crucible-llvm/CHANGELOG.md b/crucible-llvm/CHANGELOG.md
@@ -1,7 +1,18 @@
-# next
+# 0.6 -- 2024-02-05
 
 * `bindLLVMFunPtr` now accepts an `Text.LLVM.AST.Symbol` rather than a whole `Declare`.
   Use `decName` to get a `Symbol` from a `Declare`.
+* Implement overrides for the LLVM `llvm.is.fpclass.f*` intrinsics.
+* Implement overrides for the `isinf`, `__isinf`, and `__isinff` C functions.
+* Implement overrides for the LLVM `llvm.fma.f*` and `llvm.fmuladd.f*`
+  intrinsics.
+* Implement overrides for the `fma` and `fmaf` C functions.
+* Add a `Lang.Crucible.LLVM.MemModel.CallStack.null` function.
+* Add a `ppLLVMLatest` function to `Lang.Crucible.LLVM.PrettyPrint`, which
+  pretty-prints an LLVM AST using the latest LLVM version that `llvm-pretty`
+  currently supports. Also add derived combinators (`ppDeclare`, `ppIdent`,
+  etc.) for calling the `llvm-pretty` functions of the same names in tandem
+  with `ppLLVMLatest`.
 
 # 0.5
 * Add `?memOpts :: MemOptions` constraints to the following functions:

diff --git a/crucible-llvm/crucible-llvm.cabal b/crucible-llvm/crucible-llvm.cabal
@@ -1,9 +1,9 @@
 Cabal-version: 2.2
 Name:          crucible-llvm
-Version:       0.5
+Version:       0.6.0.99
 Author:        Galois Inc.
 Copyright:     (c) Galois, Inc 2014-2022
-Maintainer:    rdockins@galois.com
+Maintainer:    [email protected], [email protected], langston@galois.com
 License:       BSD-3-Clause
 License-file:  LICENSE
 Build-type:    Simple
@@ -14,14 +14,19 @@ Description:
    for Crucible-based simulation and verification of LLVM-compiled applications.
 extra-source-files: CHANGELOG.md, README.md
 
+source-repository head
+  type:     git
+  location: https://github.com/GaloisInc/crucible
+  subdir:   crucible-llvm
+
 common bldflags
   ghc-options: -Wall
                -Werror=incomplete-patterns
                -Werror=missing-methods
                -Werror=overlapping-patterns
                -Wpartial-fields
                -Wincomplete-uni-patterns
-  ghc-prof-options: -O2 -fprof-auto-top
+  ghc-prof-options: -O2 -fprof-auto-exported
   default-language: Haskell2010
 
 
@@ -39,7 +44,7 @@ library
     extra,
     lens,
     itanium-abi >= 0.1.1.1 && < 0.2,
-    llvm-pretty >= 0.8 && < 0.12,
+    llvm-pretty >= 0.12 && < 0.13,
     mtl,
     parameterized-utils >= 2.1.5 && < 2.2,
     pretty,
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		# 0.1 -- 2024-02-05

		* Initial version. Split off from `crucible-syntax`.