diff --git a/saw-remote-api/python/README.md b/saw-remote-api/python/README.md index 268403adb3..869fa77c44 100644 --- a/saw-remote-api/python/README.md +++ b/saw-remote-api/python/README.md @@ -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,7 +174,7 @@ 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. @@ -182,7 +182,7 @@ 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 diff --git a/saw-remote-api/python/pyproject.toml b/saw-remote-api/python/pyproject.toml index b8efa596f5..9a6a056b5d 100644 --- a/saw-remote-api/python/pyproject.toml +++ b/saw-remote-api/python/pyproject.toml @@ -1,8 +1,14 @@ [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 ", "Aaron Tomb "] +license = "BSD License" +include = [ + "LICENSE", + "mypy.ini", +] [tool.poetry.dependencies] python = "^3.8" diff --git a/saw-remote-api/python/requirements.txt b/saw-remote-api/python/requirements.txt index e3f314de7c..8fdf3541b9 100644 --- a/saw-remote-api/python/requirements.txt +++ b/saw-remote-api/python/requirements.txt @@ -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 diff --git a/saw-remote-api/python/saw/__init__.py b/saw-remote-api/python/saw_client/__init__.py similarity index 100% rename from saw-remote-api/python/saw/__init__.py rename to saw-remote-api/python/saw_client/__init__.py diff --git a/saw-remote-api/python/saw/commands.py b/saw-remote-api/python/saw_client/commands.py similarity index 99% rename from saw-remote-api/python/saw/commands.py rename to saw-remote-api/python/saw_client/commands.py index 7dd0d92a47..c6381186f5 100644 --- a/saw-remote-api/python/saw/commands.py +++ b/saw-remote-api/python/saw_client/commands.py @@ -3,7 +3,7 @@ from cryptol import cryptoltypes from . import exceptions -from saw.proofscript import * +from .proofscript import * from typing import Any, List diff --git a/saw-remote-api/python/saw/connection.py b/saw-remote-api/python/saw_client/connection.py similarity index 100% rename from saw-remote-api/python/saw/connection.py rename to saw-remote-api/python/saw_client/connection.py diff --git a/saw-remote-api/python/saw/dashboard.py b/saw-remote-api/python/saw_client/dashboard.py similarity index 100% rename from saw-remote-api/python/saw/dashboard.py rename to saw-remote-api/python/saw_client/dashboard.py diff --git a/saw-remote-api/python/saw/exceptions.py b/saw-remote-api/python/saw_client/exceptions.py similarity index 100% rename from saw-remote-api/python/saw/exceptions.py rename to saw-remote-api/python/saw_client/exceptions.py diff --git a/saw-remote-api/python/saw/llvm.py b/saw-remote-api/python/saw_client/llvm.py similarity index 99% rename from saw-remote-api/python/saw/llvm.py rename to saw-remote-api/python/saw_client/llvm.py index 2715ded078..725e72268d 100644 --- a/saw-remote-api/python/saw/llvm.py +++ b/saw-remote-api/python/saw_client/llvm.py @@ -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 diff --git a/saw-remote-api/python/saw/proofscript.py b/saw-remote-api/python/saw_client/proofscript.py similarity index 100% rename from saw-remote-api/python/saw/proofscript.py rename to saw-remote-api/python/saw_client/proofscript.py diff --git a/saw-remote-api/python/saw/py.typed b/saw-remote-api/python/saw_client/py.typed similarity index 100% rename from saw-remote-api/python/saw/py.typed rename to saw-remote-api/python/saw_client/py.typed diff --git a/saw-remote-api/python/saw/utils.py b/saw-remote-api/python/saw_client/utils.py similarity index 100% rename from saw-remote-api/python/saw/utils.py rename to saw-remote-api/python/saw_client/utils.py diff --git a/saw-remote-api/python/setup.py b/saw-remote-api/python/setup.py deleted file mode 100644 index 5f088f858a..0000000000 --- a/saw-remote-api/python/setup.py +++ /dev/null @@ -1,44 +0,0 @@ -#!/usr/bin/env python -# -*- coding: utf-8 -*- - -from setuptools import setup - -def get_README(): - content = "" - with open("README.md") as f: - content += f.read() - return content - -setup( - name="saw", - python_requires=">=3.7", - version="0.0.1", - url="https://github.com/GaloisInc/saw-script", - project_urls={ - "Source": "https://github.com/GaloisInc/saw/tree/main/saw-remote-api/python", - "Bug Tracker": "https://github.com/GaloisInc/saw/issues" - }, - license="BSD", - description="A scripting library for interacting with the SAW RPC server.", - long_description=get_README(), - long_description_content_type="text/markdown", - author="Galois, Inc.", - author_email="andrew@galois.com", - packages=["saw"], - package_data={"saw": ["py.typed"]}, - zip_safe=False, - install_requires=[ - "BitVector==3.4.9", - "mypy==0.812", - "mypy-extensions==0.4.3", - "argo-client==0.0.4", - ], - classifiers=[ - "Development Status :: 3 - Alpha", - "License :: OSI Approved :: BSD License", - "Operating System :: OS Independent", - "Programming Language :: Python :: 3.7", - "Programming Language :: Python :: 3.8", - "Programming Language :: Python :: 3.9" - ], -) diff --git a/saw-remote-api/python/tests/saw/test_alloc_aligned.py b/saw-remote-api/python/tests/saw/test_alloc_aligned.py index 6baa5c9935..a82212b21f 100644 --- a/saw-remote-api/python/tests/saw/test_alloc_aligned.py +++ b/saw-remote-api/python/tests/saw/test_alloc_aligned.py @@ -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 diff --git a/saw-remote-api/python/tests/saw/test_ghost.py b/saw-remote-api/python/tests/saw/test_ghost.py index aed3c62522..be831b47de 100644 --- a/saw-remote-api/python/tests/saw/test_ghost.py +++ b/saw-remote-api/python/tests/saw/test_ghost.py @@ -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 diff --git a/saw-remote-api/python/tests/saw/test_llvm_array_swap.py b/saw-remote-api/python/tests/saw/test_llvm_array_swap.py index 8586e6dddf..7904bc1044 100644 --- a/saw-remote-api/python/tests/saw/test_llvm_array_swap.py +++ b/saw-remote-api/python/tests/saw/test_llvm_array_swap.py @@ -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): diff --git a/saw-remote-api/python/tests/saw/test_llvm_assert_null.py b/saw-remote-api/python/tests/saw/test_llvm_assert_null.py index 23fa5bf983..99b613612f 100644 --- a/saw-remote-api/python/tests/saw/test_llvm_assert_null.py +++ b/saw-remote-api/python/tests/saw/test_llvm_assert_null.py @@ -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): diff --git a/saw-remote-api/python/tests/saw/test_llvm_global.py b/saw-remote-api/python/tests/saw/test_llvm_global.py index 298283d58b..2a681a8de0 100644 --- a/saw-remote-api/python/tests/saw/test_llvm_global.py +++ b/saw-remote-api/python/tests/saw/test_llvm_global.py @@ -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): diff --git a/saw-remote-api/python/tests/saw/test_llvm_pointer.py b/saw-remote-api/python/tests/saw/test_llvm_pointer.py index fab7970da9..a1a80aabbd 100644 --- a/saw-remote-api/python/tests/saw/test_llvm_pointer.py +++ b/saw-remote-api/python/tests/saw/test_llvm_pointer.py @@ -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): diff --git a/saw-remote-api/python/tests/saw/test_llvm_struct.py b/saw-remote-api/python/tests/saw/test_llvm_struct.py index 3463a34664..ff583ea03d 100644 --- a/saw-remote-api/python/tests/saw/test_llvm_struct.py +++ b/saw-remote-api/python/tests/saw/test_llvm_struct.py @@ -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]: diff --git a/saw-remote-api/python/tests/saw/test_llvm_struct_type.py b/saw-remote-api/python/tests/saw/test_llvm_struct_type.py index b6c2d8b5d2..86feb33502 100644 --- a/saw-remote-api/python/tests/saw/test_llvm_struct_type.py +++ b/saw-remote-api/python/tests/saw/test_llvm_struct_type.py @@ -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): diff --git a/saw-remote-api/python/tests/saw/test_nested_struct.py b/saw-remote-api/python/tests/saw/test_nested_struct.py index f3e5d89287..fa76ef2c56 100644 --- a/saw-remote-api/python/tests/saw/test_nested_struct.py +++ b/saw-remote-api/python/tests/saw/test_nested_struct.py @@ -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): diff --git a/saw-remote-api/python/tests/saw/test_nested_struct2.py b/saw-remote-api/python/tests/saw/test_nested_struct2.py index bc2910b497..795d7d894f 100644 --- a/saw-remote-api/python/tests/saw/test_nested_struct2.py +++ b/saw-remote-api/python/tests/saw/test_nested_struct2.py @@ -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 diff --git a/saw-remote-api/python/tests/saw/test_points_to_at_type.py b/saw-remote-api/python/tests/saw/test_points_to_at_type.py index e223a1c0c0..6991a31114 100644 --- a/saw-remote-api/python/tests/saw/test_points_to_at_type.py +++ b/saw-remote-api/python/tests/saw/test_points_to_at_type.py @@ -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 diff --git a/saw-remote-api/python/tests/saw/test_provers.py b/saw-remote-api/python/tests/saw/test_provers.py index 06bcc417d4..f593acde91 100644 --- a/saw-remote-api/python/tests/saw/test_provers.py +++ b/saw-remote-api/python/tests/saw/test_provers.py @@ -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()) diff --git a/saw-remote-api/python/tests/saw/test_salsa20.py b/saw-remote-api/python/tests/saw/test_salsa20.py index f2a226b309..c8cfd2389c 100644 --- a/saw-remote-api/python/tests/saw/test_salsa20.py +++ b/saw-remote-api/python/tests/saw/test_salsa20.py @@ -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]: diff --git a/saw-remote-api/python/tests/saw/test_swap.py b/saw-remote-api/python/tests/saw/test_swap.py index 50592e4dcb..e6a4549d4b 100644 --- a/saw-remote-api/python/tests/saw/test_swap.py +++ b/saw-remote-api/python/tests/saw/test_swap.py @@ -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 diff --git a/saw-remote-api/python/tests/saw_low_level/test_llvm_assume.py b/saw-remote-api/python/tests/saw_low_level/test_llvm_assume.py index 5e6dbed7fd..ff4c27a1e9 100644 --- a/saw-remote-api/python/tests/saw_low_level/test_llvm_assume.py +++ b/saw-remote-api/python/tests/saw_low_level/test_llvm_assume.py @@ -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 diff --git a/saw-remote-api/python/tests/saw_low_level/test_salsa20_low_level.py b/saw-remote-api/python/tests/saw_low_level/test_salsa20_low_level.py index a42160b21a..66368c2eaf 100755 --- a/saw-remote-api/python/tests/saw_low_level/test_salsa20_low_level.py +++ b/saw-remote-api/python/tests/saw_low_level/test_salsa20_low_level.py @@ -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 * diff --git a/saw-remote-api/python/tests/saw_low_level/test_seven.py b/saw-remote-api/python/tests/saw_low_level/test_seven.py index e89527a0a5..041ffd66b4 100644 --- a/saw-remote-api/python/tests/saw_low_level/test_seven.py +++ b/saw-remote-api/python/tests/saw_low_level/test_seven.py @@ -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): diff --git a/saw-remote-api/python/tests/saw_low_level/test_swap_low_level.py b/saw-remote-api/python/tests/saw_low_level/test_swap_low_level.py index f38fdb160f..6c0891425f 100644 --- a/saw-remote-api/python/tests/saw_low_level/test_swap_low_level.py +++ b/saw-remote-api/python/tests/saw_low_level/test_swap_low_level.py @@ -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): diff --git a/saw-remote-api/python/tests/saw_low_level/test_trivial.py b/saw-remote-api/python/tests/saw_low_level/test_trivial.py index 90e9874637..335b121041 100644 --- a/saw-remote-api/python/tests/saw_low_level/test_trivial.py +++ b/saw-remote-api/python/tests/saw_low_level/test_trivial.py @@ -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): diff --git a/saw-remote-api/scripts/run_rpc_tests.sh b/saw-remote-api/scripts/run_rpc_tests.sh index e77670daad..fab3445afc 100755 --- a/saw-remote-api/scripts/run_rpc_tests.sh +++ b/saw-remote-api/scripts/run_rpc_tests.sh @@ -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