Skip to content

Commit

Permalink
Merge pull request #2023 from GaloisInc/release-1.1-prep
Browse files Browse the repository at this point in the history 
Prepare for 1.1 release
  • Loading branch information
@mergify
mergify[bot] authored Feb 6, 2024
2 parents 9919afe + 00f7ee0 commit 3dc551c
Show file tree
Hide file tree
Showing 14 changed files with 74 additions and 38 deletions.
38 changes: 37 additions & 1 deletion CHANGES.md
View file
Original file line number Diff line number Diff line change
@@ -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).
Expand All @@ -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
Expand Down
14 changes: 7 additions & 7 deletions cabal.GHC-9.2.8.config
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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,
Expand All @@ -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,
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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,
Expand All @@ -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,
Expand All @@ -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
14 changes: 7 additions & 7 deletions cabal.GHC-9.4.8.config
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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,
Expand All @@ -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,
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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,
Expand All @@ -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,
Expand All @@ -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
14 changes: 7 additions & 7 deletions cabal.GHC-9.6.3.config
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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,
Expand All @@ -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,
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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,
Expand All @@ -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,
Expand All @@ -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
2 changes: 1 addition & 1 deletion deps/crucible
Submodule crucible updated 32 files
+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
2 changes: 1 addition & 1 deletion deps/cryptol
Submodule cryptol updated 6 files
+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
2 changes: 1 addition & 1 deletion deps/llvm-pretty
Submodule llvm-pretty updated from 34cf64 to 780e7c
2 changes: 1 addition & 1 deletion deps/llvm-pretty-bc-parser
Submodule llvm-pretty-bc-parser updated 8 files
+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
2 changes: 1 addition & 1 deletion saw-remote-api/CHANGELOG.md
View file
Original file line number Diff line number Diff line change
@@ -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:

Expand Down
2 changes: 1 addition & 1 deletion saw-remote-api/python/CHANGELOG.md
View file
Original file line number Diff line number Diff line change
@@ -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:

Expand Down
12 changes: 6 additions & 6 deletions saw-remote-api/python/poetry.lock
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 2 additions & 2 deletions saw-remote-api/python/pyproject.toml
View file
Original file line number Diff line number Diff line change
@@ -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]>"]
Expand All @@ -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"
Expand Down
2 changes: 1 addition & 1 deletion saw-remote-api/saw-remote-api.cabal
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
2 changes: 1 addition & 1 deletion saw-script.cabal
View file
Original file line number Diff line number Diff line change
@@ -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
Expand Down

0 comments on commit 3dc551c

Please sign in to comment.