diff --git a/.github/ci.sh b/.github/ci.sh
index d3f9f7334a..71d46a181f 100755
--- a/.github/ci.sh
+++ b/.github/ci.sh
@@ -45,6 +45,7 @@ setup_dist_bins() {
extract_exe "saw-remote-api" "dist/bin"
fi
extract_exe "saw" "dist/bin"
+ extract_exe "cryptol" "dist/bin"
export PATH=$PWD/dist/bin:$PATH
echo "$PWD/dist/bin" >> "$GITHUB_PATH"
strip dist/bin/saw* || echo "Strip failed: Ignoring harmless error"
@@ -83,18 +84,16 @@ install_system_deps() {
}
build_cryptol() {
- is_exe "dist/bin" "cryptol" && return
- (cd deps/cryptol &&
- git submodule update --init &&
- .github/ci.sh build)
+ cabal build exe:cryptol
}
bundle_files() {
- mkdir -p dist dist/{bin,doc,examples,include,lib}
+ mkdir -p dist dist/{bin,deps,doc,examples,include,lib}
cp LICENSE README.md dist/
$IS_WIN || chmod +x dist/bin/*
+ (cd deps/cryptol-specs && git archive --prefix=cryptol-specs/ --format=tar HEAD) | (cd dist/deps && tar x)
cp doc/extcore.md dist/doc
cp doc/tutorial/sawScriptTutorial.pdf dist/doc/tutorial.pdf
cp doc/manual/manual.pdf dist/doc/manual.pdf
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 770fc5c8c2..1b67c9b4c1 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -111,6 +111,11 @@ jobs:
- shell: bash
run: .github/ci.sh build
+ - shell: bash
+ env:
+ RELEASE: ${{ needs.config.outputs.release }}
+ run: .github/ci.sh build_cryptol
+
- uses: GaloisInc/.github/actions/cabal-collect-bins@v1
id: cabal-test-suites
with:
@@ -348,7 +353,7 @@ jobs:
build-push-image:
runs-on: ubuntu-latest
needs: [config]
- if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
+ if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch' || needs.config.outputs.release == 'true'
strategy:
fail-fast: false
matrix:
diff --git a/CHANGES.md b/CHANGES.md
index 99380cb3f7..c15604d362 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,4 +1,4 @@
-# Unreleased version
+# Version 0.9
## New Features
@@ -20,6 +20,8 @@ Several improvements have been made to JVM verification:
"current" status, so that `enable_experimental` is no longer
necessary for JVM verification.
+* The RPC API now includes methods for Java verification, as described [here](https://github.com/GaloisInc/saw-script/blob/master/saw-remote-api/docs/SAW.rst#sawjvmload-class-command).
+
A new `enable_lax_pointer_ordering` function exists, which relaxes the
restrictions that Crucible imposes on comparisons between pointers from
different allocation blocks.
@@ -27,6 +29,22 @@ different allocation blocks.
A SAW value of type `Bool` can now be brought into scope in Cryptol expressions
as a value of type `Bit`.
+A new `hoist_ifs_in_goal` proof tactic works like `hoist_ifs` but on the
+current goal in a proof script.
+
+The verification summaries produced when specifying the `-s` flag now
+contain much more detailed information. When producing JSON output (`-f
+json`), the tool in the `verif-viewer` directory can be used to
+translate it to GraphViz format.
+
+Two new experimental functions can evaluate SAWCore terms into simpler
+forms. The `normalize_term` function simplifies the given term by fully
+evaluating it with the SAWCore symbolic simulator but keeping it in
+SAWCore format. The `extract_uninterp` function allows certain
+uninterpreted functions to be replaced with extra inputs and constraints
+on those inputs, allowing propositional solvers to prove goals involving
+uninterpreted functions.
+
## Changes
* The linked-in version of ABC (based on the Haskell `abcBridge`
@@ -52,6 +70,42 @@ as a value of type `Bit`.
[issues](https://github.com/galoisinc/saw-script/issues) for
performance regressions you encounter!
+ The removal of the linked-in ABC version means that the `abc` tactic
+ now requires an external `abc` executable. You can get this by
+ downloading a `with-solvers` package from the releases page, by
+ downloading a solver package from the [`what4-solvers`
+ repository](https://github.com/GaloisInc/what4-solvers), or by
+ building it yourself from the [ABC
+ repository](https://github.com/berkeley-abc/abc).
+
+* The LLVM bitcode reader now should support files from any LLVM version
+ between 3.6 and 12.
+
+## Bug Fixes
+
+* Overall, closed issues #109, #120, #128, #156, #233, #316, #320, #324,
+ #523, #561, #624, #689, #722, #727, #746, #869, #872, #900, #975,
+ #982, #1033, #1035, #1045, #1066, #1098, #1120, #1135, #1140, #1144,
+ #1147, #1148, #1152, #1166, #1171, #1175, #1182, #1184, #1186, #1211,
+ #1224, #1226, #1230, #1256, #1260, #1263, #1269, #1280, #1285, #1299,
+ #1307, #1308, #1311, #1318, #1341, #1355, #1367, #1375, #1381, #1388,
+ #1389, #1390, #1404, #1411, #1420, #1430, and #1438.
+
+* Overall, merged pull requests #942, #1117, #1185, #1191, #1204, #1205,
+ #1206, #1207, #1208, #1209, #1212, #1213, #1214, #1216, #1218, #1219,
+ #1267, #1270, #1272, #1274, #1275, #1276, #1278, #1279, #1281, #1282,
+ #1283, #1284, #1286, #1288, #1289, #1290, #1292, #1293, #1294, #1295,
+ #1297, #1298, #1300, #1309, #1310, #1313, #1315, #1317, #1319, #1320,
+ #1321, #1323, #1325, #1327, #1328, #1329, #1330, #1331, #1332, #1334,
+ #1335, #1336, #1337, #1342, #1343, #1345, #1346, #1349, #1351, #1356,
+ #1357, #1364, #1365, #1366, #1368, #1369, #1370, #1371, #1373, #1374,
+ #1378, #1379, #1380, #1384, #1385, #1391, #1392, #1393, #1394, #1396,
+ #1397, #1398, #1399, #1401, #1402, #1403, #1405, #1406, #1410, #1413,
+ #1414, #1415, #1416, #1422, #1423, #1424, #1426, #1427, #1428, #1429,
+ #1431, #1432, #1433, #1434, #1435, #1437, #1439, #1440, #1441, #1443,
+ #1444, #1445, #1446, #1448, #1449, #1450, #1451, #1453, #1454, #1455,
+ #1456, #1457, #1458, #1459, #1463, #1464, #1465, #1466, and #1468.
+
# Version 0.8
## New Features
diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md
new file mode 100644
index 0000000000..d224e70553
--- /dev/null
+++ b/CODE_OF_CONDUCT.md
@@ -0,0 +1,86 @@
+# Code of Conduct
+
+## Our Pledge
+
+We as members, contributors, and leaders pledge to make participation in our
+community a harassment-free experience for everyone, regardless of age, body
+size, visible or invisible disability, ethnicity, sex characteristics, gender
+identity and expression, level of experience, education, socio-economic status,
+nationality, personal appearance, race, caste, color, religion, or sexual identity
+and orientation.
+
+We pledge to act and interact in ways that contribute to an open, welcoming,
+diverse, inclusive, and healthy community.
+
+## Our Standards
+
+Examples of behavior that contributes to a positive environment for our
+community include:
+
+* Demonstrating empathy and kindness toward other people
+* Being respectful of differing opinions, viewpoints, and experiences
+* Giving and gracefully accepting constructive feedback
+* Accepting responsibility and apologizing to those affected by our mistakes,
+ and learning from the experience
+* Focusing on what is best not just for us as individuals, but for the
+ overall community
+
+Examples of unacceptable behavior include:
+
+* The use of sexualized language or imagery, and sexual attention or
+ advances of any kind
+* Trolling, insulting or derogatory comments, and personal or political attacks
+* Public or private harassment
+* Publishing others' private information, such as a physical or email
+ address, without their explicit permission
+* Other conduct which could reasonably be considered inappropriate in a
+ professional setting
+
+## Enforcement Responsibilities
+
+Project maintainers are responsible for clarifying and enforcing our standards of
+acceptable behavior and will take appropriate and fair corrective action in
+response to any behavior that they deem inappropriate, threatening, offensive,
+or harmful.
+
+Project maintainers have the right and responsibility to remove, edit, or reject
+comments, commits, code, wiki edits, issues, and other contributions that are
+not aligned to this Code of Conduct, and will communicate reasons for moderation
+decisions when appropriate.
+
+## Scope
+
+This Code of Conduct applies within all community spaces, and also applies when
+an individual is officially representing the community in public spaces.
+Examples of representing our community include using an official e-mail address,
+posting via an official social media account, or acting as an appointed
+representative at an online or offline event.
+
+## Enforcement
+
+Instances of abusive, harassing, or otherwise unacceptable behavior may
+be reported to the project maintainers responsible for enforcement at
+[saw@galois.com](mailto:cryptol@galois.com). All complaints will be
+reviewed and investigated promptly and fairly.
+
+All project maintainers are obligated to respect the privacy and security of the
+reporter of any incident.
+
+## Attribution
+
+This Code of Conduct is adapted from the [Contributor Covenant][homepage],
+version 2.1, available at
+[https://www.contributor-covenant.org/version/2/1/code_of_conduct.html][v2.1].
+
+Community Impact Guidelines were inspired by
+[Mozilla's code of conduct enforcement ladder][Mozilla CoC].
+
+For answers to common questions about this code of conduct, see the FAQ at
+[https://www.contributor-covenant.org/faq][FAQ]. Translations are available
+at [https://www.contributor-covenant.org/translations][translations].
+
+[homepage]: https://www.contributor-covenant.org
+[v2.1]: https://www.contributor-covenant.org/version/2/1/code_of_conduct.html
+[Mozilla CoC]: https://github.com/mozilla/diversity
+[FAQ]: https://www.contributor-covenant.org/faq
+[translations]: https://www.contributor-covenant.org/translations
diff --git a/README.md b/README.md
index fb1102a795..2b4f7cf1fb 100644
--- a/README.md
+++ b/README.md
@@ -41,7 +41,8 @@ To build SAWScript and related utilities from source:
* Ensure that you have the `cabal` and `ghc` executables in your
`PATH`. If you don't already have them, we recommend using `ghcup`
- to install them:
+ to install them: . We recommend
+ Cabal 3.4 or newer, and GHC 8.8 or 8.10.
* Ensure that you have the C libraries and header files for
`terminfo`, which generally comes as part of `ncurses` on most
@@ -70,7 +71,7 @@ SAW can analyze LLVM programs (usually derived from C, but potentially
for other languages). The only tool strictly required for this is a
compiler that can generate LLVM bitcode, such as `clang`. However,
having the full LLVM tool suite available can be useful. We have tested
-SAW with LLVM and `clang` versions from 3.5 to 11.0, as well as the
+SAW with LLVM and `clang` versions from 3.5 to 12.0, as well as the
version of `clang` bundled with Apple Xcode. We welcome bug reports on
any failure to parse bitcode from LLVM versions in that range.
@@ -79,6 +80,11 @@ will be possible for all language constructs. There are various
instructions that are not supported during verification. However,
any failure during `llvm_load_module` should be considered a bug.
+## Notes on Windows
+
+If you have trouble loading the SAW REPL on Windows, try invoking it
+with the `--no-color` option.
+
## Related Packages
Many dependencies are automatically downloaded into `deps/` when you
diff --git a/deps/crucible b/deps/crucible
index 9824efe038..05a4e082e6 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit 9824efe038d6045f2040eb2cd7ecfb7f2e34dade
+Subproject commit 05a4e082e6a29e81d75babba9f5918863c5f65ee
diff --git a/deps/cryptol b/deps/cryptol
index cb240cdd31..f315ae9f4a 160000
--- a/deps/cryptol
+++ b/deps/cryptol
@@ -1 +1 @@
-Subproject commit cb240cdd31c864b298f181c0dac660e2f4e32aa5
+Subproject commit f315ae9f4a123e7e735902af79814762537c8053
diff --git a/heapster-saw/examples/Makefile b/heapster-saw/examples/Makefile
index a6dbb8cd07..dee6e52df7 100644
--- a/heapster-saw/examples/Makefile
+++ b/heapster-saw/examples/Makefile
@@ -16,8 +16,10 @@ ifeq ($(SAW),)
endif
endif
-%.bc: %.c
+ifeq ($(CI),)
+ %.bc: %.c
clang -emit-llvm -g -c $<
+endif
%_gen.v: %.saw %.bc
$(SAW) $<
diff --git a/saw-remote-api/Dockerfile b/saw-remote-api/Dockerfile
index b174492277..04603babc5 100644
--- a/saw-remote-api/Dockerfile
+++ b/saw-remote-api/Dockerfile
@@ -1,48 +1,6 @@
-FROM debian:buster AS solvers
-
-# Install needed packages for building
-RUN apt-get update \
- && apt-get install -y curl cmake gcc g++ git libreadline-dev unzip
-RUN useradd -m user
-RUN install -d -o user -g user /solvers
-USER user
-WORKDIR /solvers
-RUN mkdir -p rootfs/usr/local/bin
-
-# Get Z3 4.8.10 from GitHub
-RUN curl -L https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-ubuntu-18.04.zip --output z3.zip
-RUN unzip z3.zip
-RUN mv z3-*/bin/z3 rootfs/usr/local/bin
-
-# Build abc from GitHub. (Latest version.)
-RUN git clone https://github.com/berkeley-abc/abc.git
-RUN cd abc && make -j$(nproc)
-RUN cp abc/abc rootfs/usr/local/bin
-
-# Build Boolector release 3.2.1 from source
-RUN curl -L https://github.com/Boolector/boolector/archive/3.2.1.tar.gz | tar xz
-RUN cd boolector* && ./contrib/setup-lingeling.sh && ./contrib/setup-btor2tools.sh && ./configure.sh && cd build && make -j$(nproc)
-RUN cp boolector*/build/bin/boolector rootfs/usr/local/bin
-
-# Install Yices 2.6.2
-RUN curl -L https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-x86_64-pc-linux-gnu-static-gmp.tar.gz | tar xz
-RUN cp yices*/bin/yices-smt2 rootfs/usr/local/bin \
- && cp yices*/bin/yices rootfs/usr/local/bin
-
-# Install CVC4 1.8
-RUN curl -L https://github.com/CVC4/CVC4/releases/download/1.8/cvc4-1.8-x86_64-linux-opt --output rootfs/usr/local/bin/cvc4
-
-# Install MathSAT 5.6.3 - Uncomment if you are in compliance with MathSAT's license.
-# RUN curl -L https://mathsat.fbk.eu/download.php?file=mathsat-5.6.3-linux-x86_64.tar.gz | tar xz
-# RUN cp mathsat-5.6.3-linux-x86_64/bin/mathsat rootfs/usr/local/bin
-
-# Set executable and run tests
-RUN chmod +x rootfs/usr/local/bin/*
-
FROM haskell:8.8.4 AS build
USER root
RUN apt-get update && apt-get install -y wget libncurses-dev unzip
-COPY --from=solvers /solvers/rootfs /
RUN useradd -m saw
COPY --chown=saw:saw . /home/saw
USER saw
@@ -53,7 +11,9 @@ COPY cabal.GHC-8.8.4.config cabal.project.freeze
RUN cabal v2-update && cabal v2-build -j exe:saw-remote-api
RUN mkdir -p /home/saw/rootfs/usr/local/bin
RUN cp $(cabal v2-exec which saw-remote-api) /home/saw/rootfs/usr/local/bin/saw-remote-api
-WORKDIR /home/saw
+WORKDIR /home/saw//rootfs/usr/local/bin
+RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20210917/ubuntu-18.04-bin.zip"
+RUN unzip solvers.zip && rm solvers.zip && chmod +x *
USER root
RUN chown -R root:root /home/saw/rootfs
@@ -61,7 +21,6 @@ FROM debian:buster-slim
RUN apt-get update \
&& apt-get install -y libgmp10 libgomp1 libffi6 wget libncurses5 unzip openjdk-11-jdk-headless
COPY --from=build /home/saw/rootfs /
-COPY --from=solvers /solvers/rootfs /
RUN useradd -m saw && chown -R saw:saw /home/saw
USER saw
ENV LANG=C.UTF-8 \
diff --git a/saw-remote-api/python/saw_client/commands.py b/saw-remote-api/python/saw_client/commands.py
index 89542c70c9..257d2b86c5 100644
--- a/saw-remote-api/python/saw_client/commands.py
+++ b/saw-remote-api/python/saw_client/commands.py
@@ -12,34 +12,44 @@ def process_error(self, ae : argo.ArgoException) -> Exception:
return exceptions.make_saw_exception(ae)
class CryptolLoadFile(SAWCommand):
- def __init__(self, connection : argo.HasProtocolState, filename : str) -> None:
+ def __init__(self, connection : argo.HasProtocolState,
+ filename : str,
+ timeout : Optional[float]) -> None:
super(CryptolLoadFile, self).__init__(
'SAW/Cryptol/load file',
{'file': filename},
- connection
+ connection,
+ timeout=timeout
)
def process_result(self, _res : Any) -> Any:
return None
class CryptolLoadModule(SAWCommand):
- def __init__(self, connection : argo.HasProtocolState, module_name : str) -> None:
+ def __init__(self, connection : argo.HasProtocolState,
+ module_name : str,
+ timeout : Optional[float]) -> None:
super(CryptolLoadModule, self).__init__(
'SAW/Cryptol/load module',
{'module': module_name},
- connection
+ connection,
+ timeout=timeout
)
def process_result(self, _res : Any) -> Any:
return None
class CreateGhostVariable(SAWCommand):
- def __init__(self, connection : argo.HasProtocolState, name : str, server_name : str) -> None:
+ def __init__(self, connection : argo.HasProtocolState,
+ name : str,
+ server_name : str,
+ timeout : Optional[float]) -> None:
super(CreateGhostVariable, self).__init__(
'SAW/create ghost variable',
{'display name': name,
'server name': server_name},
- connection
+ connection,
+ timeout=timeout
)
def process_result(self, _res : Any) -> Any:
@@ -48,11 +58,13 @@ def process_result(self, _res : Any) -> Any:
class LLVMLoadModule(SAWCommand):
def __init__(self, connection : argo.HasProtocolState,
name : str,
- bitcode_file : str) -> None:
+ bitcode_file : str,
+ timeout : Optional[float]) -> None:
super(LLVMLoadModule, self).__init__(
'SAW/LLVM/load module',
{'name': name, 'bitcode file': bitcode_file},
- connection
+ connection,
+ timeout=timeout
)
def process_result(self, res : Any) -> Any:
@@ -65,12 +77,13 @@ def __init__(
module : str,
function : str,
setup : Any,
- lemma_name : str) -> None:
+ lemma_name : str,
+ timeout : Optional[float]) -> None:
params = {'module': module,
'function': function,
'contract': setup,
'lemma name': lemma_name}
- super(LLVMAssume, self).__init__('SAW/LLVM/assume', params, connection)
+ super(LLVMAssume, self).__init__('SAW/LLVM/assume', params, connection, timeout=timeout)
def process_result(self, _res : Any) -> Any:
return None
@@ -85,7 +98,8 @@ def __init__(
check_sat : bool,
setup : Any,
script : ProofScript,
- lemma_name : str) -> None:
+ lemma_name : str,
+ timeout : Optional[float]) -> None:
params = {'module': module,
'function': function,
'lemmas': lemmas,
@@ -93,7 +107,7 @@ def __init__(
'contract': setup,
'script': script,
'lemma name': lemma_name}
- super(LLVMVerify, self).__init__('SAW/LLVM/verify', params, connection)
+ super(LLVMVerify, self).__init__('SAW/LLVM/verify', params, connection, timeout=timeout)
def process_result(self, res : Any) -> Any:
return res
@@ -101,11 +115,13 @@ def process_result(self, res : Any) -> Any:
class JVMLoadClass(SAWCommand):
def __init__(self, connection : argo.HasProtocolState,
name : str,
- class_name : str) -> None:
+ class_name : str,
+ timeout : Optional[float]) -> None:
super(JVMLoadClass, self).__init__(
'SAW/JVM/load class',
{'name': name, 'class name': class_name},
- connection
+ connection,
+ timeout=timeout
)
def process_result(self, res : Any) -> Any:
@@ -118,12 +134,13 @@ def __init__(
module : str,
function : str,
setup : Any,
- lemma_name : str) -> None:
+ lemma_name : str,
+ timeout : Optional[float]) -> None:
params = {'module': module,
'function': function,
'contract': setup,
'lemma name': lemma_name}
- super(JVMAssume, self).__init__('SAW/JVM/assume', params, connection)
+ super(JVMAssume, self).__init__('SAW/JVM/assume', params, connection, timeout=timeout)
def process_result(self, _res : Any) -> Any:
return None
@@ -138,7 +155,8 @@ def __init__(
check_sat : bool,
setup : Any,
script : ProofScript,
- lemma_name : str) -> None:
+ lemma_name : str,
+ timeout : Optional[float]) -> None:
params = {'module': class_name,
'function': method_name,
'lemmas': lemmas,
@@ -146,7 +164,7 @@ def __init__(
'contract': setup,
'script': script,
'lemma name': lemma_name}
- super(JVMVerify, self).__init__('SAW/JVM/verify', params, connection)
+ super(JVMVerify, self).__init__('SAW/JVM/verify', params, connection, timeout=timeout)
def process_result(self, res : Any) -> Any:
return res
@@ -156,10 +174,11 @@ def __init__(
self,
connection : argo.HasProtocolState,
goal : cryptoltypes.CryptolJSON,
- script : ProofScript) -> None:
+ script : ProofScript,
+ timeout : Optional[float]) -> None:
params = {'goal': goal,
'script': script}
- super(Prove, self).__init__('SAW/prove', params, connection)
+ super(Prove, self).__init__('SAW/prove', params, connection, timeout=timeout)
def process_result(self, res : Any) -> Any:
return res
diff --git a/saw-remote-api/python/saw_client/connection.py b/saw-remote-api/python/saw_client/connection.py
index 91d651110d..8ce464b7a0 100644
--- a/saw-remote-api/python/saw_client/connection.py
+++ b/saw-remote-api/python/saw_client/connection.py
@@ -146,24 +146,24 @@ def protocol_state(self) -> Any:
return self.most_recent_result.state()
# Protocol messages
- def cryptol_load_file(self, filename: str) -> Command:
- self.most_recent_result = CryptolLoadFile(self, filename)
+ def cryptol_load_file(self, filename: str, timeout : Optional[float] = None) -> Command:
+ self.most_recent_result = CryptolLoadFile(self, filename, timeout)
return self.most_recent_result
- def create_ghost_variable(self, name: str, server_name: str) -> Command:
+ def create_ghost_variable(self, name: str, server_name: str, timeout : Optional[float] = None) -> Command:
"""Create an instance of the `CreateGhostVariable` command. Documentation on
the purpose and use of this command is associated with the top-level
`create_ghost_variable` function.
"""
- self.most_recent_result = CreateGhostVariable(self, name, server_name)
+ self.most_recent_result = CreateGhostVariable(self, name, server_name, timeout)
return self.most_recent_result
- def jvm_load_class(self, name: str, class_name: str) -> Command:
+ def jvm_load_class(self, name: str, class_name: str, timeout : Optional[float] = None) -> Command:
"""Create an instance of the `JVMLoadClass` command. Documentation on the purpose
and use of this command is associated with the top-level `jvm_load_class`
function.
"""
- self.most_recent_result = JVMLoadClass(self, name, class_name)
+ self.most_recent_result = JVMLoadClass(self, name, class_name, timeout)
return self.most_recent_result
def jvm_verify(self,
@@ -173,30 +173,32 @@ def jvm_verify(self,
check_sat: bool,
contract: Any,
script: ProofScript,
- lemma_name: str) -> Command:
+ lemma_name: str,
+ timeout : Optional[float] = None) -> Command:
"""Create an instance of the `JVMVerify` command. Documentation on the purpose
and use of this command is associated with the top-level `jvm_assume`
function.
"""
self.most_recent_result = \
- JVMVerify(self, class_name, method_name, lemmas, check_sat, contract, script, lemma_name)
+ JVMVerify(self, class_name, method_name, lemmas, check_sat, contract, script, lemma_name, timeout)
return self.most_recent_result
def jvm_assume(self,
class_name: str,
method_name: str,
contract: Any,
- lemma_name: str) -> Command:
+ lemma_name: str,
+ timeout : Optional[float] = None) -> Command:
"""Create an instance of the `JVMAssume` command. Documentation on the purpose
and use of this command is associated with the top-level `jvm_assume`
function.
"""
self.most_recent_result = \
- JVMAssume(self, class_name, method_name, contract, lemma_name)
+ JVMAssume(self, class_name, method_name, contract, lemma_name, timeout)
return self.most_recent_result
- def llvm_load_module(self, name: str, bitcode_file: str) -> Command:
- self.most_recent_result = LLVMLoadModule(self, name, bitcode_file)
+ def llvm_load_module(self, name: str, bitcode_file: str, timeout : Optional[float] = None) -> Command:
+ self.most_recent_result = LLVMLoadModule(self, name, bitcode_file, timeout)
return self.most_recent_result
def llvm_verify(self,
@@ -206,29 +208,32 @@ def llvm_verify(self,
check_sat: bool,
contract: Any,
script: ProofScript,
- lemma_name: str) -> Command:
+ lemma_name: str,
+ timeout : Optional[float] = None) -> Command:
self.most_recent_result = \
- LLVMVerify(self, module, function, lemmas, check_sat, contract, script, lemma_name)
+ LLVMVerify(self, module, function, lemmas, check_sat, contract, script, lemma_name, timeout)
return self.most_recent_result
def llvm_assume(self,
module: str,
function: str,
contract: Any,
- lemma_name: str) -> Command:
+ lemma_name: str,
+ timeout : Optional[float] = None) -> Command:
"""Create an instance of the `LLVMAssume` command. Documentation on the purpose
and use of this command is associated with the top-level `llvm_assume`
function.
"""
self.most_recent_result = \
- LLVMAssume(self, module, function, contract, lemma_name)
+ LLVMAssume(self, module, function, contract, lemma_name, timeout)
return self.most_recent_result
def prove(self,
goal: cryptoltypes.CryptolJSON,
- proof_script: ProofScript) -> Command:
+ proof_script: ProofScript,
+ timeout : Optional[float] = None) -> Command:
"""Create an instance of the `Prove` command. Documentation on the purpose and
use of this command is associated with the top-level `prove` function.
"""
- self.most_recent_result = Prove(self, goal, proof_script)
+ self.most_recent_result = Prove(self, goal, proof_script, timeout)
return self.most_recent_result
diff --git a/saw/Dockerfile b/saw/Dockerfile
index 345bd48e2b..1ea90c4aaf 100644
--- a/saw/Dockerfile
+++ b/saw/Dockerfile
@@ -1,48 +1,6 @@
-FROM debian:buster AS solvers
-
-# Install needed packages for building
-RUN apt-get update \
- && apt-get install -y curl cmake gcc g++ git libreadline-dev unzip
-RUN useradd -m user
-RUN install -d -o user -g user /solvers
-USER user
-WORKDIR /solvers
-RUN mkdir -p rootfs/usr/local/bin
-
-# Get Z3 4.8.10 from GitHub
-RUN curl -L https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-ubuntu-18.04.zip --output z3.zip
-RUN unzip z3.zip
-RUN mv z3-*/bin/z3 rootfs/usr/local/bin
-
-# Build abc from GitHub. (Latest version.)
-RUN git clone https://github.com/berkeley-abc/abc.git
-RUN cd abc && make -j$(nproc)
-RUN cp abc/abc rootfs/usr/local/bin
-
-# Build Boolector release 3.2.1 from source
-RUN curl -L https://github.com/Boolector/boolector/archive/3.2.1.tar.gz | tar xz
-RUN cd boolector* && ./contrib/setup-lingeling.sh && ./contrib/setup-btor2tools.sh && ./configure.sh && cd build && make -j$(nproc)
-RUN cp boolector*/build/bin/boolector rootfs/usr/local/bin
-
-# Install Yices 2.6.2
-RUN curl -L https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-x86_64-pc-linux-gnu-static-gmp.tar.gz | tar xz
-RUN cp yices*/bin/yices-smt2 rootfs/usr/local/bin \
- && cp yices*/bin/yices rootfs/usr/local/bin
-
-# Install CVC4 1.8
-RUN curl -L https://github.com/CVC4/CVC4/releases/download/1.8/cvc4-1.8-x86_64-linux-opt --output rootfs/usr/local/bin/cvc4
-
-# Install MathSAT 5.6.3 - Uncomment if you are in compliance with MathSAT's license.
-# RUN curl -L https://mathsat.fbk.eu/download.php?file=mathsat-5.6.3-linux-x86_64.tar.gz | tar xz
-# RUN cp mathsat-5.6.3-linux-x86_64/bin/mathsat rootfs/usr/local/bin
-
-# Set executable and run tests
-RUN chmod +x rootfs/usr/local/bin/*
-
FROM haskell:8.8.4 AS build
USER root
RUN apt-get update && apt-get install -y wget libncurses-dev unzip
-COPY --from=solvers /solvers/rootfs /
RUN useradd -m saw
COPY --chown=saw:saw . /home/saw
USER saw
@@ -54,7 +12,9 @@ RUN cabal v2-update
RUN cabal v2-build
RUN mkdir -p /home/saw/rootfs/usr/local/bin
RUN cp $(cabal v2-exec which saw) /home/saw/rootfs/usr/local/bin/saw
-WORKDIR /home/saw
+WORKDIR /home/saw//rootfs/usr/local/bin
+RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20210917/ubuntu-18.04-bin.zip"
+RUN unzip solvers.zip && rm solvers.zip && chmod +x *
USER root
RUN chown -R root:root /home/saw/rootfs
@@ -62,7 +22,6 @@ FROM debian:buster-slim
RUN apt-get update \
&& apt-get install -y libgmp10 libgomp1 libffi6 wget libncurses5 libreadline-dev unzip
COPY --from=build /home/saw/rootfs /
-COPY --from=solvers /solvers/rootfs /
RUN useradd -m saw && chown -R saw:saw /home/saw
USER saw
ENV LANG=C.UTF-8 \