Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

updates from release 0.8 to master #1208

Merged
merged 17 commits into from
Apr 22, 2021
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 5 additions & 17 deletions .github/ci.sh
Original file line number Diff line number Diff line change
@@ -105,28 +105,20 @@ install_yices() {
rm -rf "yices$ext" "yices-$YICES_VERSION"
}

install_yasm() {
is_exe "$BIN" "yasm" && return
case "$RUNNER_OS" in
Linux) sudo apt-get update -q && sudo apt-get install -y yasm ;;
macOS) brew install yasm ;;
Windows) choco install yasm ;;
esac
}

build() {
ghc_ver="$(ghc --numeric-version)"
cp cabal.GHC-"$ghc_ver".config cabal.project.freeze
cabal v2-update
cabal v2-configure -j --enable-tests
git status --porcelain
pkgs=(saw)
if $IS_WIN; then
echo "flags: -builtin-abc" >> cabal.project.local
echo "constraints: cryptol-saw-core -build-css" >> cabal.project.local
else
pkgs+=(saw-remote-api)
fi
tee -a cabal.project > /dev/null < cabal.project.ci
tee -a cabal.project.local > /dev/null < cabal.project.ci
if ! retry cabal v2-build "$@" "${pkgs[@]}"; then
if [[ "$RUNNER_OS" == "macOS" ]]; then
echo "Working around a dylib issue on macos by removing the cache and trying again"
@@ -155,11 +147,10 @@ install_system_deps() {
install_z3 &
install_cvc4 &
install_yices &
install_yasm &
wait
export PATH="$BIN:$PATH"
echo "$BIN" >> "$GITHUB_PATH"
is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" yices && is_exe "$BIN" yasm
is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" yices
}

build_cryptol() {
@@ -193,12 +184,9 @@ sign() {
}

zip_dist() {
: "${VERSION?VERSION is required as an environment variable}"
name="${name:-"saw-$VERSION-$RUNNER_OS-x86_64"}"
mv dist "$name"
name="$1"
cp -r dist "$name"
tar -czf "$name".tar.gz "$name"
sign "$name".tar.gz
[[ -f "$name".tar.gz.sig ]] && [[ -f "$name".tar.gz ]]
}

output() { echo "::set-output name=$1::$2"; }
276 changes: 162 additions & 114 deletions .github/workflows/build.yml → .github/workflows/ci.yml

Large diffs are not rendered by default.

45 changes: 0 additions & 45 deletions .github/workflows/docker.yml

This file was deleted.

132 changes: 0 additions & 132 deletions .github/workflows/nightly.yml

This file was deleted.

3 changes: 0 additions & 3 deletions CHANGES.md
Original file line number Diff line number Diff line change
@@ -99,9 +99,6 @@ more complete support for LLVM verification, including:

* Support for specifying the alignment of allocations.

The most recent version of the Python client is now in the `saw-script`
repository and available from `PyPI` with `pip install saw`.

Docker images for SAW are now located on
[GitHub](https://github.com/orgs/galoisinc/packages/container/package/saw)
instead of [DockerHub](https://hub.docker.com/r/galoisinc/saw/).
18 changes: 9 additions & 9 deletions saw-remote-api/python/README.md
Original file line number Diff line number Diff line change
@@ -23,7 +23,7 @@ git submodule update --init
cd saw-remote-api/python
```
5. Install and setup some version of the `saw-remote-api` server and update any
relevant environment variables as needed (see `saw.connect()` documentation
relevant environment variables as needed (see `saw_client.connect()` documentation
for the various ways a server can be connected to).
E.g., here is how the docker image of the server might be used:
```
@@ -72,11 +72,11 @@ either as a local executable or running in docker image listening on a port.

## Connecting with a server in a script

Connecting to a server in a Python script is accomplished via the `saw.connect`
Connecting to a server in a Python script is accomplished via the `saw_client.connect`
method. Its accompanying Python doc strings describe the various ways it can be
used. Below is a brief summary:

`saw.connect()`, when provided no arguments, will attempt the following in order:
`saw_client.connect()`, when provided no arguments, will attempt the following in order:

1. If the environment variable ``SAW_SERVER`` is set and refers to an
executable, it is assumed to be a `saw-remote-api` executable and will be
@@ -91,7 +91,7 @@ Additional arguments and options are documented with the function.

Notable, the `reset_server` keyword can be used to connect to a running server
and reset it, ensuring states from previous scrips have been cleared. E.g.,
`saw.connect(reset_server=True)`.
`saw_client.connect(reset_server=True)`.


## Acquiring a SAW Server
@@ -116,7 +116,7 @@ find...)

### Server docker images

Docker images for the saw server are currently uploaded to
Docker images for the SAW server are currently uploaded to
[DockerHub](https://hub.docker.com/r/galoisinc/saw-remote-api).

These images are set up to run as HTTP `saw-remote-api` servers, e.g.:
@@ -174,15 +174,15 @@ If leveraging environment variables is undesirable, the scripts themselves can
specify a command to launch the server, e.g.:

```
saw.connect(COMMAND)
saw_client.connect(COMMAND)
```

where `COMMAND` is a command to launch a new SAW server in socket mode.

Or a server URL can be specified directly in the script, e.g.:

```
saw.connect(url=URL)
saw_client.connect(url=URL)
```

where `URL` is a URL for a running SAW server in HTTP mode.
@@ -191,10 +191,10 @@ where `URL` is a URL for a running SAW server in HTTP mode.

To ensure any previous server state is cleared when running a SAW Python script
against a persistent server (e.g., one running in HTTP mode in a different process),
the `reset_server` keyword can be passed to `saw.connect()`. E.g.,
the `reset_server` keyword can be passed to `saw_client.connect()`. E.g.,

```
saw.connect(url="http://localhost:8080/", reset_server=True)
saw_client.connect(url="http://localhost:8080/", reset_server=True)
```

will connect to a SAW server running at `http://localhost:8080/` and will
14 changes: 10 additions & 4 deletions saw-remote-api/python/pyproject.toml
Original file line number Diff line number Diff line change
@@ -1,14 +1,20 @@
[tool.poetry]
name = "saw"
version = "0.0.1"
description = "SAW client"
name = "saw-client"
version = "0.8.1"
readme = "README.md"
description = "SAW client for the SAW 0.8 RPC server"
authors = ["Andrew Kent <andrew@galois.com>", "Aaron Tomb <atomb@galois.com>"]
license = "BSD License"
include = [
"LICENSE",
"mypy.ini",
]

[tool.poetry.dependencies]
python = "^3.8"
requests = "^2.25.1"
BitVector = "^3.4.9"
cryptol = "2.11.0"
cryptol = { path = "../../deps/cryptol/cryptol-remote-api/python/", develop = true }
argo-client = "0.0.4"

[tool.poetry.dev-dependencies]
114 changes: 84 additions & 30 deletions saw-remote-api/python/requirements.txt
Original file line number Diff line number Diff line change
@@ -1,30 +1,84 @@
alabaster==0.7.12
argo-client==0.0.4
Babel==2.8.0
BitVector==3.4.9
certifi==2020.6.20
chardet==3.0.4
docutils==0.16
idna==2.10
imagesize==1.2.0
Jinja2==2.11.3
MarkupSafe==1.1.1
mypy==0.812
mypy-extensions==0.4.3
packaging==20.4
Pygments==2.7.4
pyparsing==2.4.7
pytz==2020.1
requests==2.24.0
six==1.15.0
snowballstemmer==2.0.0
Sphinx==3.2.1
sphinxcontrib-applehelp==1.0.2
sphinxcontrib-devhelp==1.0.2
sphinxcontrib-htmlhelp==1.0.3
sphinxcontrib-jsmath==1.0.1
sphinxcontrib-qthelp==1.0.3
sphinxcontrib-serializinghtml==1.1.4
typed-ast==1.4.2
typing-extensions==3.7.4.3
urllib3==1.25.10
argo-client==0.0.4; python_version >= "3.7" \
--hash=sha256:1ce6af1cbc738d08348dcb62d573968da58e2382cb4ea753cc061aa16d45ff6a \
--hash=sha256:74c13e9f3bf5a48eeda847af343bdaf54a950c100496ed3c342a51f5406cf568
bitvector==3.4.9 \
--hash=sha256:a5e94cbb4804213b1f0c32d84517cd8f0bb8c689b5eb8055d351632e220a5edd
certifi==2020.12.5; python_version >= "3.8" and python_full_version < "3.0.0" and python_version < "4.0" or python_version >= "3.8" and python_version < "4.0" and python_full_version >= "3.5.0" \
--hash=sha256:719a74fb9e33b9bd44cc7f3a8d94bc35e4049deebe19ba7d8e108280cfd59830 \
--hash=sha256:1a4995114262bffbc2413b159f2a1a480c969de6e6eb13ee966d470af86af59c
chardet==4.0.0; python_version >= "3.8" and python_full_version < "3.0.0" and python_version < "4.0" or python_version >= "3.8" and python_version < "4.0" and python_full_version >= "3.5.0" \
--hash=sha256:f864054d66fd9118f2e67044ac8981a54775ec5b67aed0441892edb553d21da5 \
--hash=sha256:0d6f53a15db4120f2b08c94f11e7d93d2c911ee118b6b30a04ec3ee8310179fa
cryptol==2.11.0; python_version >= "3.8" and python_version < "4.0" \
--hash=sha256:60c16ddef674bd7f9bf27b4962c72a696ff10c8ded5d18ba9f73b797897e3494 \
--hash=sha256:e252f95cea05268c895ae779701947fea34d43f2715dd3444692a35663b029f3
idna==2.10; python_version >= "3.8" and python_full_version < "3.0.0" and python_version < "4.0" or python_version >= "3.8" and python_version < "4.0" and python_full_version >= "3.5.0" \
--hash=sha256:b97d804b1e9b523befed77c48dacec60e6dcb0b5391d57af6a65a312a90648c0 \
--hash=sha256:b307872f855b18632ce0c21c5e45be78c0ea7ae4c15c828c20788b26921eb3f6
mypy-extensions==0.4.3; python_version >= "3.8" and python_version < "4.0" \
--hash=sha256:090fedd75945a69ae91ce1303b5824f428daf5a028d2f6ab8a299250a846f15d \
--hash=sha256:2d82818f5bb3e369420cb3c4060a7970edba416647068eb4c5343488a6c604a8
mypy==0.812; python_version >= "3.5" \
--hash=sha256:a26f8ec704e5a7423c8824d425086705e381b4f1dfdef6e3a1edab7ba174ec49 \
--hash=sha256:28fb5479c494b1bab244620685e2eb3c3f988d71fd5d64cc753195e8ed53df7c \
--hash=sha256:9743c91088d396c1a5a3c9978354b61b0382b4e3c440ce83cf77994a43e8c521 \
--hash=sha256:d7da2e1d5f558c37d6e8c1246f1aec1e7349e4913d8fb3cb289a35de573fe2eb \
--hash=sha256:4eec37370483331d13514c3f55f446fc5248d6373e7029a29ecb7b7494851e7a \
--hash=sha256:d65cc1df038ef55a99e617431f0553cd77763869eebdf9042403e16089fe746c \
--hash=sha256:61a3d5b97955422964be6b3baf05ff2ce7f26f52c85dd88db11d5e03e146a3a6 \
--hash=sha256:25adde9b862f8f9aac9d2d11971f226bd4c8fbaa89fb76bdadb267ef22d10064 \
--hash=sha256:552a815579aa1e995f39fd05dde6cd378e191b063f031f2acfe73ce9fb7f9e56 \
--hash=sha256:499c798053cdebcaa916eef8cd733e5584b5909f789de856b482cd7d069bdad8 \
--hash=sha256:5873888fff1c7cf5b71efbe80e0e73153fe9212fafdf8e44adfe4c20ec9f82d7 \
--hash=sha256:9f94aac67a2045ec719ffe6111df543bac7874cee01f41928f6969756e030564 \
--hash=sha256:d23e0ea196702d918b60c8288561e722bf437d82cb7ef2edcd98cfa38905d506 \
--hash=sha256:674e822aa665b9fd75130c6c5f5ed9564a38c6cea6a6432ce47eafb68ee578c5 \
--hash=sha256:abf7e0c3cf117c44d9285cc6128856106183938c68fd4944763003decdcfeb66 \
--hash=sha256:0d0a87c0e7e3a9becdfbe936c981d32e5ee0ccda3e0f07e1ef2c3d1a817cf73e \
--hash=sha256:7ce3175801d0ae5fdfa79b4f0cfed08807af4d075b402b7e294e6aa72af9aa2a \
--hash=sha256:b09669bcda124e83708f34a94606e01b614fa71931d356c1f1a5297ba11f110a \
--hash=sha256:33f159443db0829d16f0a8d83d94df3109bb6dd801975fe86bacb9bf71628e97 \
--hash=sha256:3f2aca7f68580dc2508289c729bd49ee929a436208d2b2b6aab15745a70a57df \
--hash=sha256:2f9b3407c58347a452fc0736861593e105139b905cca7d097e413453a1d650b4 \
--hash=sha256:cd07039aa5df222037005b08fbbfd69b3ab0b0bd7a07d7906de75ae52c4e3119
requests==2.25.1; (python_version >= "2.7" and python_full_version < "3.0.0") or (python_full_version >= "3.5.0") \
--hash=sha256:c210084e36a42ae6b9219e00e48287def368a26d03a048ddad7bfee44f75871e \
--hash=sha256:27973dd4a904a4f13b263a19c866c13b92a39ed1c964655f025f3f8d3d75b804
typed-ast==1.4.3; python_version >= "3.8" and python_version < "4.0" \
--hash=sha256:2068531575a125b87a41802130fa7e29f26c09a2833fea68d9a40cf33902eba6 \
--hash=sha256:c907f561b1e83e93fad565bac5ba9c22d96a54e7ea0267c708bffe863cbe4075 \
--hash=sha256:1b3ead4a96c9101bef08f9f7d1217c096f31667617b58de957f690c92378b528 \
--hash=sha256:dde816ca9dac1d9c01dd504ea5967821606f02e510438120091b84e852367428 \
--hash=sha256:777a26c84bea6cd934422ac2e3b78863a37017618b6e5c08f92ef69853e765d3 \
--hash=sha256:f8afcf15cc511ada719a88e013cec87c11aff7b91f019295eb4530f96fe5ef2f \
--hash=sha256:52b1eb8c83f178ab787f3a4283f68258525f8d70f778a2f6dd54d3b5e5fb4341 \
--hash=sha256:01ae5f73431d21eead5015997ab41afa53aa1fbe252f9da060be5dad2c730ace \
--hash=sha256:c190f0899e9f9f8b6b7863debfb739abcb21a5c054f911ca3596d12b8a4c4c7f \
--hash=sha256:398e44cd480f4d2b7ee8d98385ca104e35c81525dd98c519acff1b79bdaac363 \
--hash=sha256:bff6ad71c81b3bba8fa35f0f1921fb24ff4476235a6e94a26ada2e54370e6da7 \
--hash=sha256:0fb71b8c643187d7492c1f8352f2c15b4c4af3f6338f21681d3681b3dc31a266 \
--hash=sha256:760ad187b1041a154f0e4d0f6aae3e40fdb51d6de16e5c99aedadd9246450e9e \
--hash=sha256:5feca99c17af94057417d744607b82dd0a664fd5e4ca98061480fd8b14b18d04 \
--hash=sha256:95431a26309a21874005845c21118c83991c63ea800dd44843e42a916aec5899 \
--hash=sha256:aee0c1256be6c07bd3e1263ff920c325b59849dc95392a05f258bb9b259cf39c \
--hash=sha256:9ad2c92ec681e02baf81fdfa056fe0d818645efa9af1f1cd5fd6f1bd2bdfd805 \
--hash=sha256:b36b4f3920103a25e1d5d024d155c504080959582b928e91cb608a65c3a49e1a \
--hash=sha256:067a74454df670dcaa4e59349a2e5c81e567d8d65458d480a5b3dfecec08c5ff \
--hash=sha256:7538e495704e2ccda9b234b82423a4038f324f3a10c43bc088a1636180f11a41 \
--hash=sha256:af3d4a73793725138d6b334d9d247ce7e5f084d96284ed23f22ee626a7b88e39 \
--hash=sha256:f2362f3cb0f3172c42938946dbc5b7843c2a28aec307c49100c8b38764eb6927 \
--hash=sha256:dd4a21253f42b8d2b48410cb31fe501d32f8b9fbeb1f55063ad102fe9c425e40 \
--hash=sha256:f328adcfebed9f11301eaedfa48e15bdece9b519fb27e6a8c01aa52a17ec31b3 \
--hash=sha256:2c726c276d09fc5c414693a2de063f521052d9ea7c240ce553316f70656c84d4 \
--hash=sha256:cae53c389825d3b46fb37538441f75d6aecc4174f615d048321b716df2757fb0 \
--hash=sha256:b9574c6f03f685070d859e75c7f9eeca02d6933273b5e69572e5ff9d5e3931c3 \
--hash=sha256:209596a4ec71d990d71d5e0d312ac935d86930e6eecff6ccc7007fe54d703808 \
--hash=sha256:9c6d1a54552b5330bc657b7ef0eae25d00ba7ffe85d9ea8ae6540d2197a3788c \
--hash=sha256:fb1bbeac803adea29cedd70781399c99138358c26d05fcbd23c13016b7f5ec65
typing-extensions==3.7.4.3; python_version >= "3.8" and python_version < "4.0" \
--hash=sha256:dafc7639cde7f1b6e1acc0f457842a83e722ccca8eef5270af2d74792619a89f \
--hash=sha256:7cb407020f00f7bfc3cb3e7881628838e69d8f3fcab2f64742a5e76b2f841918 \
--hash=sha256:99d4073b617d30288f569d3f13d2bd7548c3a7e4c8de87db09a9d29bb3a4a60c
urllib3==1.26.4; python_version >= "3.8" and python_full_version < "3.0.0" and python_version < "4.0" or python_full_version >= "3.5.0" and python_version < "4" and python_version >= "3.8" \
--hash=sha256:2f4da4594db7e1e110a944bb1b551fdf4e6c136ad42e4234131391e21eb5b0df \
--hash=sha256:e7b021f7241115872f92f43c6508082facffbd1c048e3c6e2bb9c2a157e28937
File renamed without changes.
Original file line number Diff line number Diff line change
@@ -3,7 +3,7 @@

from cryptol import cryptoltypes
from . import exceptions
from saw.proofscript import *
from .proofscript import *

from typing import Any, List

File renamed without changes.
File renamed without changes.
File renamed without changes.
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
from abc import ABCMeta, abstractmethod
from cryptol import cryptoltypes
from saw.utils import deprecated
from .utils import deprecated
from dataclasses import dataclass
import dataclasses
import re
File renamed without changes.
File renamed without changes.
File renamed without changes.
44 changes: 0 additions & 44 deletions saw-remote-api/python/setup.py

This file was deleted.

4 changes: 2 additions & 2 deletions saw-remote-api/python/tests/saw/test_alloc_aligned.py
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
from pathlib import Path
import unittest
from saw import *
from saw.llvm import Contract, FreshVar, SetupVal, cryptol, struct, LLVMType, array_ty, i8, i64
from saw_client import *
from saw_client.llvm import Contract, FreshVar, SetupVal, cryptol, struct, LLVMType, array_ty, i8, i64
from typing import Tuple


4 changes: 2 additions & 2 deletions saw-remote-api/python/tests/saw/test_ghost.py
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import saw
from saw.llvm import Contract, CryptolTerm, cryptol, void, i32, GhostVariable
import saw_client as saw
from saw_client.llvm import Contract, CryptolTerm, cryptol, void, i32, GhostVariable

import unittest
from pathlib import Path
4 changes: 2 additions & 2 deletions saw-remote-api/python/tests/saw/test_llvm_array_swap.py
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
from pathlib import Path
import unittest
from saw import *
from saw.llvm import Contract, array, array_ty, void, i32
from saw_client import *
from saw_client.llvm import Contract, array, array_ty, void, i32


class ArraySwapContract(Contract):
4 changes: 2 additions & 2 deletions saw-remote-api/python/tests/saw/test_llvm_assert_null.py
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
from pathlib import Path
import unittest
from saw import *
from saw.llvm import Contract, cryptol, null, i32
from saw_client import *
from saw_client.llvm import Contract, cryptol, null, i32


class FContract1(Contract):
4 changes: 2 additions & 2 deletions saw-remote-api/python/tests/saw/test_llvm_global.py
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
from pathlib import Path
import unittest
from saw import *
from saw.llvm import Contract, global_initializer, global_var
from saw_client import *
from saw_client.llvm import Contract, global_initializer, global_var


class FContract(Contract):
4 changes: 2 additions & 2 deletions saw-remote-api/python/tests/saw/test_llvm_pointer.py
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
from pathlib import Path
import unittest
from saw import *
from saw.llvm import Contract, cryptol, void, i8, ptr_ty
from saw_client import *
from saw_client.llvm import Contract, cryptol, void, i8, ptr_ty


class FContract(Contract):
4 changes: 2 additions & 2 deletions saw-remote-api/python/tests/saw/test_llvm_struct.py
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
from pathlib import Path
import unittest
from saw import *
from saw.llvm import Contract, SetupVal, FreshVar, cryptol, struct, LLVMType, void, array_ty, i32, alias_ty
from saw_client import *
from saw_client.llvm import Contract, SetupVal, FreshVar, cryptol, struct, LLVMType, void, array_ty, i32, alias_ty


def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None) -> Tuple[FreshVar, SetupVal]:
4 changes: 2 additions & 2 deletions saw-remote-api/python/tests/saw/test_llvm_struct_type.py
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
from pathlib import Path
import unittest
from saw import *
from saw.llvm import Contract, cryptol, struct, void, i32, array_ty, struct_ty
from saw_client import *
from saw_client.llvm import Contract, cryptol, struct, void, i32, array_ty, struct_ty


class FContract(Contract):
4 changes: 2 additions & 2 deletions saw-remote-api/python/tests/saw/test_nested_struct.py
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
from pathlib import Path
import unittest
from saw import *
from saw.llvm import Contract, elem, field, i32, alias_ty
from saw_client import *
from saw_client.llvm import Contract, elem, field, i32, alias_ty

class FContract1(Contract):
def specification(self):
4 changes: 2 additions & 2 deletions saw-remote-api/python/tests/saw/test_nested_struct2.py
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
from pathlib import Path
import unittest
from saw import *
from saw.llvm import Contract, elem, field, i32, alias_ty
from saw_client import *
from saw_client.llvm import Contract, elem, field, i32, alias_ty

# like test_nested_struct.py but using cute __getitem__ indexing on SetupVals

6 changes: 3 additions & 3 deletions saw-remote-api/python/tests/saw/test_points_to_at_type.py
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
from pathlib import Path
import unittest
from saw import *
from saw.exceptions import VerificationError
from saw.llvm import Contract, LLVMType, PointerType, cryptol, void, i32, array_ty
from saw_client import *
from saw_client.exceptions import VerificationError
from saw_client.llvm import Contract, LLVMType, PointerType, cryptol, void, i32, array_ty
from typing import Union


14 changes: 3 additions & 11 deletions saw-remote-api/python/tests/saw/test_provers.py
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
from cryptol import cryptoltypes
from cryptol.bitvector import BV
import saw
from saw.proofscript import *
import saw_client as saw
from saw_client.proofscript import *

import unittest
from pathlib import Path
@@ -12,16 +12,8 @@ def cry(exp):

class ProverTest(unittest.TestCase):

@classmethod
def setUpClass(self):
saw.connect(reset_server=True)

@classmethod
def tearDownClass(self):
saw.reset_server()
saw.disconnect()

def test_provers(self):
saw.connect(reset_server=True)

if __name__ == "__main__": saw.view(saw.LogResults())

4 changes: 2 additions & 2 deletions saw-remote-api/python/tests/saw/test_salsa20.py
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
from pathlib import Path
import unittest
from cryptol.cryptoltypes import to_cryptol
from saw import *
from saw.llvm import Contract, void, SetupVal, FreshVar, cryptol, i8, i32, LLVMType, LLVMArrayType
from saw_client import *
from saw_client.llvm import Contract, void, SetupVal, FreshVar, cryptol, i8, i32, LLVMType, LLVMArrayType


def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None) -> Tuple[FreshVar, SetupVal]:
4 changes: 2 additions & 2 deletions saw-remote-api/python/tests/saw/test_swap.py
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import saw
from saw.llvm import Contract, void, i32
import saw_client as saw
from saw_client.llvm import Contract, void, i32

import unittest
from pathlib import Path
4 changes: 2 additions & 2 deletions saw-remote-api/python/tests/saw_low_level/test_llvm_assume.py
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
from pathlib import Path
import saw
from saw.proofscript import *
import saw_client as saw
from saw_client.proofscript import *
import unittest
import sys

Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
from pathlib import Path
import unittest
import saw
from saw.llvm import *
from saw.proofscript import *
import saw_client as saw
from saw_client.llvm import *
from saw_client.proofscript import *



4 changes: 2 additions & 2 deletions saw-remote-api/python/tests/saw_low_level/test_seven.py
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
from pathlib import Path
import unittest
import saw
from saw.proofscript import *
import saw_client as saw
from saw_client.proofscript import *

class SevenTest(unittest.TestCase):
def test_seven(self):
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
from pathlib import Path
import unittest
import saw
from saw.proofscript import *
import saw_client as saw
from saw_client.proofscript import *


class SwapLowLevelTest(unittest.TestCase):
4 changes: 2 additions & 2 deletions saw-remote-api/python/tests/saw_low_level/test_trivial.py
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
from pathlib import Path
import unittest
import saw
from saw.proofscript import *
import saw_client as saw
from saw_client.proofscript import *


class TrivialTest(unittest.TestCase):
2 changes: 1 addition & 1 deletion saw-remote-api/scripts/run_rpc_tests.sh
Original file line number Diff line number Diff line change
@@ -15,7 +15,7 @@ poetry install

echo "Typechecking code with mypy..."
# Don't run mypy on tests/ yet, as it doesn't play well with mypy. See #1125.
run_test poetry run mypy saw/
run_test poetry run mypy saw_client/

export SAW_SERVER=$(which saw-remote-api)
if [[ ! -x "$SAW_SERVER" ]]; then
Original file line number Diff line number Diff line change
@@ -1,20 +1,17 @@
#!/bin/bash

echo "Building and testing saw-remote-api docker image..."
echo "Testing saw-remote-api docker image..."

DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"

pushd $DIR/../..

docker build -t saw-remote-api --file saw-remote-api/Dockerfile .
popd
TAG=${1:-saw-remote-api}

pushd $DIR/..

docker run --name=saw-remote-api -d \
-v $PWD/python/tests/saw/test-files:/home/saw/tests/saw/test-files \
-p 8080:8080 \
saw-remote-api
"$TAG"

if (( $? != 0 )); then
echo "Failed to launch docker container"
2 changes: 1 addition & 1 deletion saw-script.cabal
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
Name: saw-script
Version: 0.7.0.99
Version: 0.8.0.99
Author: Galois Inc.
Maintainer: atomb@galois.com
Build-type: Custom