GaloisInc · mergify · Feb 6, 2024 · Feb 1, 2024 · Feb 1, 2024 · Feb 1, 2024
diff --git a/CHANGES.md b/CHANGES.md
@@ -1,4 +1,4 @@
-# Nightly -- ????-??-??
+# Version 1.1 -- 2024-02-05
 
 ## New Features
 * SAW now supports loading and reasoning about Cryptol declarations that make use of numeric constraint guards.  For more information on numeric constraint guards, see the [relavent section of the Cryptol reference manual](https://galoisinc.github.io/cryptol/master/BasicSyntax.html#numeric-constraint-guards).
@@ -24,6 +24,42 @@
   * Add `jvm_ghost_value` and `mir_ghost_value` commands in addition to the
     existing `llvm_ghost_value` command.
 
+* SAW now includes an experimental `set_solver_cache_path` command, which
+  caches the results of tactics which call out to automated provers. This can
+  save a considerable amount of time when repeatedly running proof scripts. For
+  more information, see the
+  [manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md#caching-solver-results).
+
+* Add experimental support for verifying hardware circuits via VHDL and Yosys.
+  There is now a family of experimental `yosys_*` commands that support this.
+  For more information, see the
+  [manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md#analyzing-hardware-circuits-using-yosys).
+
+* Extend `llvm_verify_x86` in order to handle x86 functions that spill arguments
+  to the stack.
+
+## Bug fixes
+
+* Fix a bug in which SAW failed to expand type synonyms used in the definition
+  of another type synonym.
+
+* Fix a bug in which SAW would fail to load LLVM bitcode files produced by Apple
+  Clang on macOS.
+
+* Overall, closed issues #1818, #1822, #1824, #1828, #1834, #1839, #1842,
+  #1843, #1847, #1852, #1854, #1856, 1857, #1859, #1864, #1870, #1875, #1883,
+  #1884, #1888, #1892, #1894, #1897, #1900, #1909, #1914, #1917, #1923, #1927,
+  #1929, #1932, #1938, #1942, #1945, #1961, #1968, #1970, #1973, #1985, #2003,
+  and #2005.
+
+* Overall, merged pull requests #1882, #1885, #1889, #1890, #1891, #1893,
+  #1898, #1899, #1904, #1905, #1907, #1908, #1911, #1913, #1915, #1916, #1919,
+  #1920, #1921, #1922, #1924, #1925, #1928, #1930, #1931, #1933, #1934, #1935,
+  #1936, #1937, #1939, #1940, #1941, #1943, #1947, #1948, #1949, #1950, #1951,
+  #1952, #1955, #1958, #1959, #1962, #1963, #1969, #1971, #1972, #1974, #1986,
+  #1986, #1987, #1991, #1992, #1993, #2001, #2004, #2006, #2007, #2008, #2009,
+  #2010, #2011, #2012, #2013, #2014, #2015, #2020, #2021, #2022, and #2024.
+
 # Version 1.0 -- 2023-06-26
 
 ## New Features

diff --git a/cabal.GHC-9.2.8.config b/cabal.GHC-9.2.8.config
@@ -40,7 +40,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              attoparsec -developer,
              any.attoparsec-aeson ==2.1.0.0,
              any.auto-update ==0.1.6,
-             any.barbies ==2.0.5.0,
+             any.barbies ==2.1.1.0,
              any.base ==4.16.4.0,
              any.base-compat ==0.12.3,
              any.base-compat-batteries ==0.12.3,
@@ -293,7 +293,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.quickcheck-instances ==0.3.30,
              quickcheck-instances -bytestring-builder,
              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.recv ==0.1.0,
              any.reflection ==2.1.7,
@@ -306,7 +306,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.sbv ==10.2,
              any.scientific ==0.3.7.0,
@@ -336,7 +336,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,
@@ -410,7 +410,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.vector-binary-instances ==0.2.5.2,
              any.vector-stream ==0.1.0.1,
              any.vector-th-unbox ==0.2.2,
-             any.versions ==6.0.4,
+             any.versions ==6.0.5,
              any.void ==0.7.3,
              void -safe,
              any.wai ==3.2.4,
@@ -419,7 +419,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.wai-logger ==2.4.0,
              any.warp ==3.3.31,
              warp +allow-sendfilefd -network-bytestring -warp-debug +x509,
-             any.warp-tls ==3.4.3,
+             any.warp-tls ==3.4.4,
              any.weigh ==0.0.17,
              what4 -drealtestdisable -solvertests -stptestdisable,
              any.witherable ==0.4.2,
@@ -433,4 +433,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.8.config b/cabal.GHC-9.4.8.config
@@ -41,7 +41,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              attoparsec -developer,
              any.attoparsec-aeson ==2.1.0.0,
              any.auto-update ==0.1.6,
-             any.barbies ==2.0.5.0,
+             any.barbies ==2.1.1.0,
              any.base ==4.17.2.1,
              any.base-compat ==0.12.3,
              any.base-compat-batteries ==0.12.3,
@@ -293,7 +293,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.quickcheck-instances ==0.3.30,
              quickcheck-instances -bytestring-builder,
              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.recv ==0.1.0,
              any.reflection ==2.1.7,
@@ -306,7 +306,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.sbv ==10.2,
              any.scientific ==0.3.7.0,
@@ -336,7 +336,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,
@@ -410,7 +410,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.vector-binary-instances ==0.2.5.2,
              any.vector-stream ==0.1.0.1,
              any.vector-th-unbox ==0.2.2,
-             any.versions ==6.0.4,
+             any.versions ==6.0.5,
              any.void ==0.7.3,
              void -safe,
              any.wai ==3.2.4,
@@ -419,7 +419,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.wai-logger ==2.4.0,
              any.warp ==3.3.31,
              warp +allow-sendfilefd -network-bytestring -warp-debug +x509,
-             any.warp-tls ==3.4.3,
+             any.warp-tls ==3.4.4,
              any.weigh ==0.0.17,
              what4 -drealtestdisable -solvertests -stptestdisable,
              any.witherable ==0.4.2,
@@ -433,4 +433,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.3.config b/cabal.GHC-9.6.3.config
@@ -41,7 +41,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              attoparsec -developer,
              any.attoparsec-aeson ==2.1.0.0,
              any.auto-update ==0.1.6,
-             any.barbies ==2.0.5.0,
+             any.barbies ==2.1.1.0,
              any.base ==4.18.1.0,
              any.base-compat ==0.12.3,
              any.base-compat-batteries ==0.12.3,
@@ -291,7 +291,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.quickcheck-instances ==0.3.30,
              quickcheck-instances -bytestring-builder,
              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.recv ==0.1.0,
              any.reflection ==2.1.7,
@@ -304,7 +304,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.sbv ==10.2,
              any.scientific ==0.3.7.0,
@@ -334,7 +334,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,
@@ -408,7 +408,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.vector-binary-instances ==0.2.5.2,
              any.vector-stream ==0.1.0.1,
              any.vector-th-unbox ==0.2.2,
-             any.versions ==6.0.4,
+             any.versions ==6.0.5,
              any.void ==0.7.3,
              void -safe,
              any.wai ==3.2.4,
@@ -417,7 +417,7 @@ constraints: any.BoundedChan ==1.0.3.0,
              any.wai-logger ==2.4.0,
              any.warp ==3.3.31,
              warp +allow-sendfilefd -network-bytestring -warp-debug +x509,
-             any.warp-tls ==3.4.3,
+             any.warp-tls ==3.4.4,
              any.weigh ==0.0.17,
              what4 -drealtestdisable -solvertests -stptestdisable,
              any.witherable ==0.4.2,
@@ -431,4 +431,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/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/saw-remote-api/CHANGELOG.md b/saw-remote-api/CHANGELOG.md
@@ -1,6 +1,6 @@
 # Revision history for saw-remote-api
 
-## next -- TBA
+## 1.1.0 -- 2024-02-05
 
 * Add remote API support for SAW's experimental MIR verification support:
 

diff --git a/saw-remote-api/python/CHANGELOG.md b/saw-remote-api/python/CHANGELOG.md
@@ -1,6 +1,6 @@
 # Revision history for saw-client
 
-## next -- TBA
+## 1.1.0 -- 2024-02-05
 
 * Add Python bindings for SAW's experimental MIR verification support:
 

diff --git a/saw-remote-api/python/poetry.lock b/saw-remote-api/python/poetry.lock
diff --git a/saw-remote-api/python/pyproject.toml b/saw-remote-api/python/pyproject.toml
@@ -1,6 +1,6 @@
 [tool.poetry]
 name = "saw-client"
-version = "1.0.0"
+version = "1.1.0.99"
 readme = "README.md"
 description = "SAW client for the SAW RPC server"
 authors = ["Galois, Inc. <[email protected]>"]
@@ -14,7 +14,7 @@ include = [
 python = "^3.8"
 requests = "^2.25.1"
 BitVector = "^3.4.9"
-cryptol = "3.0.0" # { path = "../../deps/cryptol/cryptol-remote-api/python/", develop = true }
+cryptol = "3.1.0" # { path = "../../deps/cryptol/cryptol-remote-api/python/", develop = true }
 argo-client = "0.0.11"
 lmdb = "^1.4.1"
 cbor2 = "^5.4.6"

diff --git a/saw-remote-api/saw-remote-api.cabal b/saw-remote-api/saw-remote-api.cabal
@@ -4,7 +4,7 @@ cabal-version:       2.4
 -- http://haskell.org/cabal/users-guide/
 
 name:                saw-remote-api
-version:             1.0.0
+version:             1.1.0.99
 -- synopsis:
 -- description:
 -- bug-reports:

diff --git a/saw-script.cabal b/saw-script.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.4
 Name:          saw-script
-Version:       1.0.0.99
+Version:       1.1.0.99
 Author:        Galois Inc.
 Maintainer:    [email protected]
 Build-type:    Custom
+55 −55		cabal.GHC-8.10.7.config
+56 −56		cabal.GHC-9.2.8.config
+56 −56		cabal.GHC-9.4.5.config
+56 −56		cabal.GHC-9.6.2.config
+3 −0		crucible-cli/CHANGELOG.md
+1 −1		crucible-cli/crucible-cli.cabal
+1 −1		crucible-concurrency/crucible-concurrency.cabal
+3 −2		crucible-go/CHANGELOG.md
+1 −1		crucible-go/crucible-go.cabal
+3 −2		crucible-jvm/CHANGELOG.md
+3 −0		crucible-llvm-cli/CHANGELOG.md
+1 −1		crucible-llvm-cli/crucible-llvm-cli.cabal
+3 −0		crucible-llvm-syntax/CHANGELOG.md
+1 −1		crucible-llvm-syntax/crucible-llvm-syntax.cabal
+12 −1		crucible-llvm/CHANGELOG.md
+9 −4		crucible-llvm/crucible-llvm.cabal
+38 −1		crucible-mir/CHANGELOG.md
+1 −1		crucible-mir/crucible-mir.cabal
+1 −1		crucible-symio/CHANGELOG.md
+9 −2		crucible-symio/crucible-symio.cabal
+11 −1		crucible-syntax/CHANGELOG.md
+1 −1		crucible-syntax/crucible-syntax.cabal
+9 −0		crucible/CHANGELOG.md
+8 −3		crucible/crucible.cabal
+4 −0		crux-llvm/CHANGELOG.md
+7 −2		crux-llvm/crux-llvm.cabal
+14 −0		crux-mir/CHANGELOG.md
+1 −1		crux-mir/crux-mir.cabal
+5 −0		crux/CHANGELOG.md
+7 −2		crux/crux.cabal
+1 −1		dependencies/llvm-pretty
+1 −1		dependencies/llvm-pretty-bc-parser
+14 −4		CHANGES.md
+3 −2		cryptol-remote-api/CHANGELOG.md
+1 −1		cryptol-remote-api/cryptol-remote-api.cabal
+3 −2		cryptol-remote-api/python/CHANGELOG.md
+1 −1		cryptol-remote-api/python/pyproject.toml
+2 −2		cryptol.cabal
+20 −0		CHANGELOG.md
+7 −0		disasm-test/tests/T266-constant-icmp.ll
+7 −0		disasm-test/tests/T266-constant-icmp.pre-llvm15.ll
+3 −3		flake.lock
+1 −1		llvm-pretty
+3 −3		llvm-pretty-bc-parser.cabal
+6 −4		src/Data/LLVM/BitCode/IR/Constants.hs
+0 −18		src/Data/LLVM/BitCode/IR/Values.hs