diff --git a/CHANGES.md b/CHANGES.md index d7a684c57e..42e984f0a1 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,4 +1,4 @@ -# Unreleased version +# Version 0.8 ## New Features @@ -15,17 +15,130 @@ When the path to Java is known, SAW can automatically add system-related JAR files to the JAR path, which eliminates the need to manually specify these files with `-j`. -SAWScript includes two new functions, `llvm_struct_type` and -`llvm_packed_struct_type`, for constructing an LLVM struct type from a list -of other LLVM types. This is not to be confused with the existing `llvm_struct` -function, which takes a string as an argument and returns the corresponding -alias type (which is often, but not necessarily, defined as a struct type). -To avoid confusion, a new `llvm_alias` function has been introduced, and -`llvm_struct` is now a synonym for `llvm_alias`. The `llvm_struct` function -continues to be available for now. - -SAWScript includes a new `llvm_pointer : LLVMType -> LLVMType` function for -constructing LLVM pointer types. +The Crucible-based interface to Java verification is now strictly an +improvement over the older code base, with the addition of several +features: + +* Performance of JVM verification is significantly better, as a result + of removing some unnecessary instances of rewriting. This improves + performance of LLVM verification, as well. + +* The new `jvm_static_field_is` function allows describing the contents + of static variables in method specifications. + +* The verification code initializes all JVM classes at the start so that + initializers don't run at arbitrary intermediate points and clobber + static field values specified in preconditions. This means, however, + that any proofs about Java code are under the assumption that all + class initializers have run before the method under analysis executes. + +Now that the Crucible-based verification infrastructure is sufficiently +expressive and performant, we have removed all dependencies on the old +`jvm-verifier` library. + +On the LLVM side, SAWScript includes a variety of new functions for +writing specification blocks: + +* The `llvm_struct_type` and `llvm_packed_struct_type` functions each + construct an LLVM struct type from a list of other LLVM types. This is + not to be confused with the existing `llvm_struct` function, which + takes a string as an argument and returns the corresponding alias type + (which is often, but not necessarily, defined as a struct type). + +* To avoid confusion, a new `llvm_alias` function now exists, and + `llvm_struct` is now a synonym for `llvm_alias`. The `llvm_struct` + function continues to be available for now. + +* The `llvm_pointer : LLVMType -> LLVMType` function allows construction + of arbitrary LLVM pointer types. + +* Two new functions, `llvm_points_to_at_type` and + `llvm_conditional_points_to_at_type`, mirror `llvm_points_to` and + `llvm_conditional_points_to`, but cast the pointer to a different + type. This may be useful when reading or writing a prefix of a larger + array, for example. + +* Support for using ABC as an external process is more complete: + + * SAW can now generate Verilog with multiple outputs (from `Term` + values that have tuple or vector result types, for example). + + * The new commands `write_aig_external` and `write_cnf_external` + generate AIG and CNF files, respectively, by first writing Verilog + and then using the available `abc` executable to bit-blast to the + lower-level representation. Corresponding proof tactics, + `offline_aig_external` and `offline_cnf_external` also exist. + +These changes are in preparation for removing the linked-in copy of ABC +in a future release. + +The `saw-remote-api` RPC server and associated Python client now have +more complete support for LLVM verification, including: + +* More complete points-to declarations, matching what is currently + available in SAWScript. + +* Support for more provers, including the full range of SBV-based and + What4-based provers available in SAWScript. + +* Support for ghost variables. + +* Support for assuming LLVM contracts directly (rather than the previous + behavior which would temporarily assume that failed verifications + succeeded to determine whether higher-level verifications would still + succeed). + +* Support for global variables and initializers. + +* Support for null pointers. + +* Support for array value literals. + +* Support for specifying the value of individual struct fields and array + elements. + +* 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/). + +## Changes + +The proof management infrastructure in SAWScript is simpler and more +consistent than before. Many of these changes are internal, to make the +code less error-prone and easier to maintain in the future. Several are +user-facing, though: + +* The `caseProofResult` command now passes a `Theorem` argument to the + first function argument, allowing its use as a rewrite rule, for + example. + +* A new `admit` tactic exists, which takes a `String` argument + describing why the user has decided omit proof of the goal. This + replaces the `assume_unsat` and `assume_valid` tactics, which we now + recommend against. They will be officially deprecated in a future + release, and removed after that. + +* Prover tactics (e.g., `yices`) now return `ProofScript ()` instead of + `ProofScript SatResult`. + +## Bug Fixes + +* Verilog generated from rotation operations is now in correct Verilog + syntax. + +* Closed issues #9, #25, #39, #41, #54, #55, #69, #81, #90, #92, #124, + #136, #144, #149, #152, #159, #271, #285, #323, #353, #377, #382, + #431, #446, #631, #652, #739, #740, #861, #901, #908, #924, #930, + #951, #962, #971, #985, #991, #993, #994, #995, #996, #1003, #1006, + #1009, #1021, #1022, #1023, #1031, #1032, #1050, #1051, #1052, #1055, + #1056, #1058, #1061, #1062, #1067, #1073, #1083, #1085, #1090, #1091, + #1096, #1099, #1101, #1119, #1122, #1123, #1127, #1128, #1132, #1163, + and #1164. # Version 0.7 diff --git a/README.md b/README.md index 20755a2334..0ce5a1b4d9 100644 --- a/README.md +++ b/README.md @@ -17,7 +17,9 @@ describes the breadth of SAWScript's features. ## Precompiled Binaries -Precompiled SAWScript binaries for a variety of platforms are available on the [releases page](https://github.com/GaloisInc/saw-script/releases). +Precompiled SAWScript binaries for a variety of platforms are available +on the [releases +page](https://github.com/GaloisInc/saw-script/releases). ## Getting Z3 @@ -27,7 +29,7 @@ solver](https://github.com/Z3Prover/z3) installed. You can download Z3 binaries for a variety of platforms from their [releases page](https://github.com/Z3Prover/z3/releases). -We currently recommend Z3 4.8.7. If you plan to use path satisfiability +We currently recommend Z3 4.8.10. If you plan to use path satisfiability checking, you'll also need Yices version 2.6.1 or newer. After installation, make sure that `z3` (or `z3.exe` on Windows) @@ -68,7 +70,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 9.0, as well as the +SAW with LLVM and `clang` versions from 3.5 to 11.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. diff --git a/intTests/test_external_abc/test.saw b/intTests/test_external_abc/test.saw index bb6c3c8c57..256f708df2 100644 --- a/intTests/test_external_abc/test.saw +++ b/intTests/test_external_abc/test.saw @@ -8,18 +8,24 @@ prove_print w4_abc_smtlib2 t; prove_print w4_abc_verilog t; prove_print (offline_verilog "offline_verilog") t; prove_print (w4_offline_smtlib2 "w4_offline_smtlib2") t; +prove_print (offline_aig_external "offline_aig") t; +prove_print (offline_cnf_external "offline_cnf") t; // A formula that is unsatisfiable. let q_unsat = {{ \(x:[8]) -> x != 0 /\ x+x == x }}; write_verilog "write_verilog_unsat.v" q_unsat; write_smtlib2_w4 "write_smtlib2_w4_unsat.smt2" q_unsat; +write_aig_external "write_aig_external_unsat.aig" q_unsat; +write_cnf_external "write_aig_external_unsat.cnf" q_unsat; // A formula that is satisfiable. let q_sat = {{ \(x:[8]) -> x+x == x }}; write_verilog "write_verilog_sat.v" q_sat; write_smtlib2_w4 "write_smtlib2_w4_sat.smt2" q_sat; +write_aig_external "write_aig_external_sat.aig" q_sat; +write_cnf_external "write_aig_external_sat.cnf" q_sat; fails (prove_print sbv_abc q_sat); fails (prove_print w4_abc_smtlib2 q_sat); diff --git a/intTests/test_external_abc/test.sh b/intTests/test_external_abc/test.sh index 117c16e4cc..31b030f163 100755 --- a/intTests/test_external_abc/test.sh +++ b/intTests/test_external_abc/test.sh @@ -14,6 +14,15 @@ abc -q "%read write_verilog_unsat.v; $SCRIPT" || true; abc -q "%read write_verilog_sat.v; $SCRIPT" || true; [ -s ${CEX} ] +rm -f ${CEX} + +abc -q "&read offline_aig.prove0.aig; &cec -m; write_aiger_cex $CEX" || true; +[ ! -f ${CEX} ] +abc -q "&read write_aig_external_unsat.aig; &cec -m; write_aiger_cex $CEX" || true; +[ ! -f ${CEX} ] +abc -q "&read write_aig_external_sat.aig; &cec -m; write_aiger_cex $CEX" || true; +[ -s ${CEX} ] + z3 w4_offline_smtlib2.prove0.smt2 | grep "^unsat$" z3 write_smtlib2_w4_sat.smt2 | grep "^sat$" z3 write_smtlib2_w4_unsat.smt2 | grep "^unsat$" @@ -23,4 +32,4 @@ abc -q "%read write_verilog_tupt.v; %blast; &write tupt.aig" abc -q "cec seqt.aig tupt.aig" rm -f ${CEX} -rm -f *.v *.aig *.smt2 +rm -f *.v *.aig *.smt2 *.cnf diff --git a/intTests/test_llvm_x86_07/test b/intTests/test_llvm_x86_07/test new file mode 100755 index 0000000000..98ee15353a Binary files /dev/null and b/intTests/test_llvm_x86_07/test differ diff --git a/intTests/test_llvm_x86_07/test.S b/intTests/test_llvm_x86_07/test.S new file mode 100644 index 0000000000..219e776c36 --- /dev/null +++ b/intTests/test_llvm_x86_07/test.S @@ -0,0 +1,10 @@ +section .bss +section .text +global precondtest +precondtest: + mov rax, rdi + ret +global _start +_start: + mov rax, 60 + syscall diff --git a/intTests/test_llvm_x86_07/test.c b/intTests/test_llvm_x86_07/test.c new file mode 100644 index 0000000000..ed199b2e65 --- /dev/null +++ b/intTests/test_llvm_x86_07/test.c @@ -0,0 +1,8 @@ +#include +#include + +extern uint64_t precondtest(uint64_t x); + +void test() { + precondtest(1); +}; diff --git a/intTests/test_llvm_x86_07/test.saw b/intTests/test_llvm_x86_07/test.saw new file mode 100644 index 0000000000..f1a3013471 --- /dev/null +++ b/intTests/test_llvm_x86_07/test.saw @@ -0,0 +1,14 @@ +enable_experimental; + +m <- llvm_load_module "test.bc"; + +let precondtest_setup = do { + x <- crucible_fresh_var "x" (llvm_int 64); + crucible_precond {{ x < 10 }}; + llvm_execute_func [crucible_term x]; + x' <- crucible_fresh_var "x'" (llvm_int 64); + crucible_return (crucible_term x'); + crucible_postcond {{ x' < 10 }}; +}; + +llvm_verify_x86 m "./test" "precondtest" [] false precondtest_setup w4; \ No newline at end of file diff --git a/intTests/test_llvm_x86_07/test.sh b/intTests/test_llvm_x86_07/test.sh new file mode 100755 index 0000000000..72b10f2497 --- /dev/null +++ b/intTests/test_llvm_x86_07/test.sh @@ -0,0 +1,7 @@ +#!/bin/sh +set -e + +# yasm -felf64 test.S +# ld test.o -o test +clang -c -emit-llvm test.c +$SAW test.saw diff --git a/saw-remote-api/docs/SAW.rst b/saw-remote-api/docs/SAW.rst index 0fda9b34ed..aee4ed507f 100644 --- a/saw-remote-api/docs/SAW.rst +++ b/saw-remote-api/docs/SAW.rst @@ -238,6 +238,22 @@ SAW/LLVM/assume (command) Assume the function meets its specification. +SAW/create ghost variable (command) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + + +``display name`` + The name to assign to the ghost variable for display. + + + +``server name`` + The server name to use to access the ghost variable later. + + +Create a ghost global variable to represent proof-specific program state. + + SAW/make simpset (command) ~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/saw-remote-api/python/poetry.lock b/saw-remote-api/python/poetry.lock index 80b408e562..53ddf89654 100644 --- a/saw-remote-api/python/poetry.lock +++ b/saw-remote-api/python/poetry.lock @@ -36,22 +36,17 @@ python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*, !=3.4.*" [[package]] name = "cryptol" -version = "0.0.2" -description = "Cryptol client" +version = "2.11.0" +description = "Cryptol client for the Cryptol 2.11 RPC server" category = "main" optional = false -python-versions = "^3.8" -develop = true +python-versions = ">=3.8,<4.0" [package.dependencies] argo-client = "0.0.4" BitVector = "^3.4.9" requests = "^2.25.1" -[package.source] -type = "directory" -url = "../../deps/cryptol/cryptol-remote-api/python" - [[package]] name = "idna" version = "2.10" @@ -152,7 +147,10 @@ chardet = [ {file = "chardet-4.0.0-py2.py3-none-any.whl", hash = "sha256:f864054d66fd9118f2e67044ac8981a54775ec5b67aed0441892edb553d21da5"}, {file = "chardet-4.0.0.tar.gz", hash = "sha256:0d6f53a15db4120f2b08c94f11e7d93d2c911ee118b6b30a04ec3ee8310179fa"}, ] -cryptol = [] +cryptol = [ + {file = "cryptol-2.11.0-py3-none-any.whl", hash = "sha256:60c16ddef674bd7f9bf27b4962c72a696ff10c8ded5d18ba9f73b797897e3494"}, + {file = "cryptol-2.11.0.tar.gz", hash = "sha256:e252f95cea05268c895ae779701947fea34d43f2715dd3444692a35663b029f3"}, +] idna = [ {file = "idna-2.10-py2.py3-none-any.whl", hash = "sha256:b97d804b1e9b523befed77c48dacec60e6dcb0b5391d57af6a65a312a90648c0"}, {file = "idna-2.10.tar.gz", hash = "sha256:b307872f855b18632ce0c21c5e45be78c0ea7ae4c15c828c20788b26921eb3f6"}, diff --git a/saw-remote-api/python/pyproject.toml b/saw-remote-api/python/pyproject.toml index 83f5a888d9..b8efa596f5 100644 --- a/saw-remote-api/python/pyproject.toml +++ b/saw-remote-api/python/pyproject.toml @@ -8,7 +8,7 @@ authors = ["Andrew Kent ", "Aaron Tomb "] python = "^3.8" requests = "^2.25.1" BitVector = "^3.4.9" -cryptol = { path = "../../deps/cryptol/cryptol-remote-api/python/", develop = true } +cryptol = "2.11.0" argo-client = "0.0.4" [tool.poetry.dev-dependencies] diff --git a/saw-remote-api/python/saw/__init__.py b/saw-remote-api/python/saw/__init__.py index a9d0833f79..320b786ed3 100644 --- a/saw-remote-api/python/saw/__init__.py +++ b/saw-remote-api/python/saw/__init__.py @@ -2,9 +2,8 @@ from dataclasses import dataclass from typing import List, Optional, Set, Union, Tuple, Any, IO import uuid -import os import sys -import signal +import time import atexit from distutils.spawn import find_executable @@ -115,6 +114,19 @@ def is_success(self) -> bool: return False +@dataclass +class AssumptionSucceeded(VerificationSucceeded): + def __init__(self, + server_name: str, + contract: llvm.Contract, + stdout: str, + stderr: str) -> None: + super().__init__(server_name, + [], + contract, + stdout, + stderr) + @dataclass class AssumptionFailed(VerificationFailed): def __init__(self, @@ -129,7 +141,7 @@ def __init__(self, # FIXME cryptol_path isn't always used...? def connect(command: Union[str, ServerConnection, None] = None, - *, + *, cryptol_path: Optional[str] = None, persist: bool = False, url : Optional[str] = None, @@ -189,11 +201,12 @@ def print_if_still_running() -> None: except ProcessLookupError: pass atexit.register(print_if_still_running) + time.sleep(0.1) def reset() -> None: """Reset the current SAW connection to the initial state. - + If the connection is inactive, ``connect()`` is called to initialize it.""" if __designated_connection is not None: __designated_connection.reset() @@ -202,7 +215,7 @@ def reset() -> None: def reset_server() -> None: """Reset the SAW server, clearing all states. - + If the connection is inactive, ``connect()`` is called to initialize it.""" if __designated_connection is not None: __designated_connection.reset_server() @@ -343,9 +356,19 @@ def view(v: View) -> None: def cryptol_load_file(filename: str) -> None: - __get_designated_connection().cryptol_load_file(filename) + __get_designated_connection().cryptol_load_file(filename).result() return None +def create_ghost_variable(name: str) -> llvm.GhostVariable: + """Create a ghost variable that can be used to invent state useful to + verification but that doesn't exist in the concrete state of the program. + This state can be referred to using the `c.ghost_value` method for some + `Contract` object `c`. + """ + server_name = __fresh_server_name(name) + __get_designated_connection().create_ghost_variable(name, server_name) + return llvm.GhostVariable(name, server_name) + @dataclass class LLVMModule: @@ -359,6 +382,45 @@ def llvm_load_module(bitcode_file: str) -> LLVMModule: return LLVMModule(bitcode_file, name) +def llvm_assume(module: LLVMModule, + function: str, + contract: llvm.Contract, + lemma_name_hint: Optional[str] = None) -> VerificationResult: + """Assume that the given function satisfies the given contract. Returns an + override linking the function and contract that can be passed as an + argument in calls to `llvm_verify` + """ + if lemma_name_hint is None: + lemma_name_hint = contract.__class__.__name__ + "_" + function + name = __fresh_server_name(lemma_name_hint) + + result: VerificationResult + try: + conn = __get_designated_connection() + res = conn.llvm_assume(module.server_name, + function, + contract.to_json(), + name) + result = AssumptionSucceeded(server_name=name, + contract=contract, + stdout=res.stdout(), + stderr=res.stderr()) + __global_success = True + # If something stopped us from even **assuming**... + except exceptions.VerificationError as err: + __global_success = False + result = AssumptionFailed(server_name=name, + assumptions=[], + contract=contract, + exception=err) + except Exception as err: + __global_success = False + for view in __designated_views: + view.on_python_exception(err) + raise err from None + + return result + def llvm_verify(module: LLVMModule, function: str, contract: llvm.Contract, @@ -371,18 +433,17 @@ def llvm_verify(module: LLVMModule, lemmas = [] if script is None: script = proofscript.ProofScript([proofscript.abc]) + if lemma_name_hint is None: + lemma_name_hint = contract.__class__.__name__ + "_" + function - lemma_name_hint = contract.__class__.__name__ + "_" + function - name = llvm.uniquify(lemma_name_hint, __used_server_names) - __used_server_names.add(name) + name = __fresh_server_name(lemma_name_hint) result: VerificationResult conn = __get_designated_connection() - conn_snapshot = conn.snapshot() global __global_success global __designated_views - + try: res = conn.llvm_verify(module.server_name, function, @@ -391,6 +452,7 @@ def llvm_verify(module: LLVMModule, contract.to_json(), script.to_json(), name) + stdout = res.stdout() stderr = res.stderr() result = VerificationSucceeded(server_name=name, @@ -400,27 +462,11 @@ def llvm_verify(module: LLVMModule, stderr=stderr) # If the verification did not succeed... except exceptions.VerificationError as err: - # roll back to snapshot because the current connection's - # latest result is now a verification exception! - __set_designated_connection(conn_snapshot) - conn = __get_designated_connection() - # Assume the verification succeeded - try: - conn.llvm_assume(module.server_name, - function, - contract.to_json(), - name).result() - result = VerificationFailed(server_name=name, - assumptions=lemmas, - contract=contract, - exception=err) - # If something stopped us from even **assuming**... - except exceptions.VerificationError as err: - __set_designated_connection(conn_snapshot) - result = AssumptionFailed(server_name=name, - assumptions=lemmas, - contract=contract, - exception=err) + # FIXME add the goal as an assumption if it failed...? + result = VerificationFailed(server_name=name, + assumptions=lemmas, + contract=contract, + exception=err) # If something else went wrong... except Exception as err: __global_success = False diff --git a/saw-remote-api/python/saw/commands.py b/saw-remote-api/python/saw/commands.py index c00808b6ba..7dd0d92a47 100644 --- a/saw-remote-api/python/saw/commands.py +++ b/saw-remote-api/python/saw/commands.py @@ -33,6 +33,18 @@ def __init__(self, connection : argo.HasProtocolState, module_name : str) -> Non def process_result(self, _res : Any) -> Any: return None +class CreateGhostVariable(SAWCommand): + def __init__(self, connection : argo.HasProtocolState, name : str, server_name : str) -> None: + super(CreateGhostVariable, self).__init__( + 'SAW/create ghost variable', + {'display name': name, + 'server name': server_name}, + connection + ) + + def process_result(self, _res : Any) -> Any: + return None + class LLVMLoadModule(SAWCommand): def __init__(self, connection : argo.HasProtocolState, name : str, @@ -43,8 +55,8 @@ def __init__(self, connection : argo.HasProtocolState, connection ) - def process_result(self, _res : Any) -> Any: - return None + def process_result(self, res : Any) -> Any: + return res class LLVMAssume(SAWCommand): def __init__( @@ -83,8 +95,8 @@ def __init__( 'lemma name': lemma_name} super(LLVMVerify, self).__init__('SAW/LLVM/verify', params, connection) - def process_result(self, _res : Any) -> Any: - return None + def process_result(self, res : Any) -> Any: + return res class Prove(SAWCommand): def __init__( diff --git a/saw-remote-api/python/saw/connection.py b/saw-remote-api/python/saw/connection.py index 7bf5b9ff78..cabfba9022 100644 --- a/saw-remote-api/python/saw/connection.py +++ b/saw-remote-api/python/saw/connection.py @@ -5,7 +5,6 @@ from argo_client.connection import ServerConnection, DynamicSocketProcess, HttpProcess, ManagedProcess from argo_client.interaction import Interaction, Command from .commands import * - from typing import Optional, Union, Any, List # FIXME cryptol_path isn't always used...? @@ -88,7 +87,7 @@ def __init__(self, def reset(self) -> None: """Resets the connection, causing its unique state on the server to be freed (if applicable). - + After a reset a connection may be treated as if it were a fresh connection with the server if desired.""" SAWReset(self) self.most_recent_result = None @@ -102,10 +101,10 @@ def disconnect(self) -> None: """Clears the state from the server and closes any underlying server/connection process launched by this object.""" self.reset() - if not self.persist: - if self.proc and (pid := self.proc.pid()): - os.killpg(os.getpgid(pid), signal.SIGKILL) - self.proc = None + if not self.persist and self.proc and (pid := self.proc.pid()): + pgid = os.getpgid(pid) + os.kill(pgid, signal.SIGKILL) + self.proc = None def __del__(self) -> None: @@ -115,7 +114,7 @@ def __del__(self) -> None: if not self.persist: if self.proc and (pid := self.proc.pid()): os.killpg(os.getpgid(pid), signal.SIGKILL) - + def pid(self) -> Optional[int]: """Return the PID of the running server process.""" @@ -131,15 +130,6 @@ def running(self) -> bool: else: return False - def snapshot(self) -> SAWConnection: - """Return a ``SAWConnection`` that has the same process and state as - the current connection. The new connection's state will be - independent of the current state. - """ - copy = SAWConnection(self.server_connection) - copy.most_recent_result = self.most_recent_result - return copy - def protocol_state(self) -> Any: if self.most_recent_result is None: return None @@ -151,6 +141,14 @@ def cryptol_load_file(self, filename: str) -> Command: self.most_recent_result = CryptolLoadFile(self, filename) return self.most_recent_result + def create_ghost_variable(self, name: str, server_name: str) -> 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) + 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) return self.most_recent_result @@ -172,6 +170,10 @@ def llvm_assume(self, function: str, contract: Any, lemma_name: str) -> 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) return self.most_recent_result @@ -179,10 +181,8 @@ def llvm_assume(self, def prove(self, goal: cryptoltypes.CryptolJSON, proof_script: ProofScript) -> Command: - """Atempts to prove that the expression given as the first argument, @goal@, is - true for all possible values of free symbolic variables. Uses the proof - script (potentially specifying an automated prover) provided by the - second argument. + """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) return self.most_recent_result diff --git a/saw-remote-api/python/saw/llvm.py b/saw-remote-api/python/saw/llvm.py index 30ede26be8..2715ded078 100644 --- a/saw-remote-api/python/saw/llvm.py +++ b/saw-remote-api/python/saw/llvm.py @@ -268,6 +268,22 @@ def to_json(self) -> Any: "check points to type": check_target_type_json, "condition": self.condition.to_json() if self.condition is not None else self.condition} +@dataclass +class GhostVariable: + name: str + server_name: str + +class GhostValue: + """A class containing the statement that a given ghost variable should have the + value given by a Cryptol expression. + """ + def __init__(self, name: str, value: CryptolTerm) -> None: + self.name = name + self.value = value + + def to_json(self) -> Any: + return {"server name": self.name, + "value": cryptoltypes.to_cryptol(self.value)} @dataclass class State: @@ -276,12 +292,14 @@ class State: conditions : List[Condition] = dataclasses.field(default_factory=list) allocated : List[Allocated] = dataclasses.field(default_factory=list) points_to : List[PointsTo] = dataclasses.field(default_factory=list) + ghost_values : List[GhostValue] = dataclasses.field(default_factory=list) def to_json(self) -> Any: return {'variables': [v.to_init_json() for v in self.fresh], 'conditions': [c.to_json() for c in self.conditions], 'allocated': [a.to_init_json() for a in self.allocated], - 'points to': [p.to_json() for p in self.points_to] + 'points to': [p.to_json() for p in self.points_to], + 'ghost values': [g.to_json() for g in self.ghost_values] } ContractState = \ @@ -426,6 +444,19 @@ def points_to(self, pointer : SetupVal, target : SetupVal, *, else: raise Exception("wrong state") + def ghost_value(self, var: GhostVariable, value: CryptolTerm) -> None: + """Declare that the given ghost variable should have a value specified by the given Cryptol expression. + + Usable either before or after `execute_func`. + """ + gv = GhostValue(var.name, value) + if self.__state == 'pre': + self.__pre_state.ghost_values.append(gv) + elif self.__state == 'post': + self.__post_state.ghost_values.append(gv) + else: + raise Exception("wrong state") + @deprecated def proclaim(self, proposition : Union[str, CryptolTerm, cryptoltypes.CryptolJSON]) -> None: """DEPRECATED: Use ``precondition`` or ``postcondition`` instead. This method will @@ -515,11 +546,13 @@ def to_json(self) -> Any: {'pre vars': [v.to_init_json() for v in self.__pre_state.fresh], 'pre conds': [c.to_json() for c in self.__pre_state.conditions], 'pre allocated': [a.to_init_json() for a in self.__pre_state.allocated], + 'pre ghost values': [g.to_json() for g in self.__pre_state.ghost_values], 'pre points tos': [pt.to_json() for pt in self.__pre_state.points_to], 'argument vals': [a.to_json() for a in self.__arguments] if self.__arguments is not None else [], 'post vars': [v.to_init_json() for v in self.__post_state.fresh], 'post conds': [c.to_json() for c in self.__post_state.conditions], 'post allocated': [a.to_init_json() for a in self.__post_state.allocated], + 'post ghost values': [g.to_json() for g in self.__post_state.ghost_values], 'post points tos': [pt.to_json() for pt in self.__post_state.points_to], 'return val': self.__returns.to_json()} diff --git a/saw-remote-api/python/tests/saw/test-files/ghost.bc b/saw-remote-api/python/tests/saw/test-files/ghost.bc new file mode 100644 index 0000000000..c3bd8b7dec Binary files /dev/null and b/saw-remote-api/python/tests/saw/test-files/ghost.bc differ diff --git a/saw-remote-api/python/tests/saw/test-files/ghost.c b/saw-remote-api/python/tests/saw/test-files/ghost.c new file mode 100644 index 0000000000..bdb95e759a --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/ghost.c @@ -0,0 +1,3 @@ +extern int get_and_increment(); + +int f(int i) { return i * get_and_increment(); } diff --git a/saw-remote-api/python/tests/saw/test-files/test.bc b/saw-remote-api/python/tests/saw/test-files/test.bc new file mode 100644 index 0000000000..c3bd8b7dec Binary files /dev/null and b/saw-remote-api/python/tests/saw/test-files/test.bc differ diff --git a/saw-remote-api/python/tests/saw/test-files/test.c b/saw-remote-api/python/tests/saw/test-files/test.c new file mode 100644 index 0000000000..bdb95e759a --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/test.c @@ -0,0 +1,3 @@ +extern int get_and_increment(); + +int f(int i) { return i * get_and_increment(); } 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 2487c402a1..6baa5c9935 100644 --- a/saw-remote-api/python/tests/saw/test_alloc_aligned.py +++ b/saw-remote-api/python/tests/saw/test_alloc_aligned.py @@ -61,16 +61,8 @@ def specification(self) -> None: class LLVMNestedStructTest(unittest.TestCase): - - @classmethod - def setUpClass(self): - connect(reset_server=True) - - @classmethod - def tearDownClass(self): - disconnect() - def test_llvm_struct(self): + connect(reset_server=True) if __name__ == "__main__": view(LogResults()) bcname = str(Path('tests','saw','test-files', 'alloc_aligned.bc')) diff --git a/saw-remote-api/python/tests/saw/test_ghost.py b/saw-remote-api/python/tests/saw/test_ghost.py new file mode 100644 index 0000000000..aed3c62522 --- /dev/null +++ b/saw-remote-api/python/tests/saw/test_ghost.py @@ -0,0 +1,57 @@ +import saw +from saw.llvm import Contract, CryptolTerm, cryptol, void, i32, GhostVariable + +import unittest +from pathlib import Path + +def pre_counter(contract: Contract, counter: GhostVariable): + n = contract.fresh_var(i32, "n") + contract.precondition(n < cryptol("128")) + contract.ghost_value(counter, n) + return n + +def post_counter(contract: Contract, counter: GhostVariable, n: CryptolTerm): + contract.ghost_value(counter, cryptol("(+)")(n, cryptol("1"))) + +class GetAndIncrementContract(Contract): + def __init__(self, counter: str) -> None: + super().__init__() + self.counter = counter + + def specification(self) -> None: + n = pre_counter(self, self.counter) + self.execute_func() + post_counter(self, self.counter, n) + self.returns(n) + +class FContract(Contract): + def __init__(self, counter: str) -> None: + super().__init__() + self.counter = counter + + def specification(self) -> None: + n = pre_counter(self, self.counter) + i = self.fresh_var(i32, "i") + self.precondition(i < cryptol("512")) + self.execute_func(i) + post_counter(self, self.counter, n) + self.returns(cryptol("(*)")(i, n)) + +class GhostTest(unittest.TestCase): + + def test_ghost(self): + + saw.connect(reset_server=True) + if __name__ == "__main__": saw.view(saw.LogResults()) + ghost_bc = str(Path('tests','saw','test-files', 'ghost.bc')) + + mod = saw.llvm_load_module(ghost_bc) + + counter = saw.create_ghost_variable('counter'); + get_and_increment_ov = saw.llvm_assume(mod, 'get_and_increment', GetAndIncrementContract(counter)) + self.assertIs(get_and_increment_ov.is_success(), True) + f_ov = saw.llvm_verify(mod, 'f', FContract(counter), lemmas=[get_and_increment_ov]) + self.assertIs(f_ov.is_success(), True) + +if __name__ == "__main__": + unittest.main() 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 8127fc9004..8586e6dddf 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 @@ -19,16 +19,8 @@ def specification(self): class LLVMArraySwapTest(unittest.TestCase): - - @classmethod - def setUpClass(self): - connect(reset_server=True) - - @classmethod - def tearDownClass(self): - disconnect() - def test_llvm_array_swap(self): + connect(reset_server=True) if __name__ == "__main__": view(LogResults()) bcname = str(Path('tests','saw','test-files', 'llvm_array_swap.bc')) mod = llvm_load_module(bcname) 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 9f66a12991..23fa5bf983 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 @@ -21,16 +21,8 @@ def specification(self): class LLVMAssertNullTest(unittest.TestCase): - - @classmethod - def setUpClass(self): - connect(reset_server=True) - - @classmethod - def tearDownClass(self): - disconnect() - def test_llvm_assert_null(self): + connect(reset_server=True) if __name__ == "__main__": view(LogResults()) bcname = str(Path('tests','saw','test-files', 'llvm_assert_null.bc')) mod = llvm_load_module(bcname) 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 6fe8e4ad3e..298283d58b 100644 --- a/saw-remote-api/python/tests/saw/test_llvm_global.py +++ b/saw-remote-api/python/tests/saw/test_llvm_global.py @@ -15,16 +15,8 @@ def specification(self): class LLVMGlobalTest(unittest.TestCase): - - @classmethod - def setUpClass(self): - connect(reset_server=True) - - @classmethod - def tearDownClass(self): - disconnect() - def test_llvm_global(self): + connect(reset_server=True) if __name__ == "__main__": view(LogResults()) bcname = str(Path('tests','saw','test-files', 'llvm_global.bc')) mod = llvm_load_module(bcname) 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 e87b370f6a..fab7970da9 100644 --- a/saw-remote-api/python/tests/saw/test_llvm_pointer.py +++ b/saw-remote-api/python/tests/saw/test_llvm_pointer.py @@ -18,15 +18,8 @@ def specification(self): class LLVMPointerTest(unittest.TestCase): - @classmethod - def setUpClass(self): - connect(reset_server=True) - - @classmethod - def tearDownClass(self): - disconnect() - def test_llvm_pointer(self): + connect(reset_server=True) if __name__ == "__main__": view(LogResults()) bcname = str(Path('tests','saw','test-files', 'llvm_pointer.bc')) mod = llvm_load_module(bcname) 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 c209339354..3463a34664 100644 --- a/saw-remote-api/python/tests/saw/test_llvm_struct.py +++ b/saw-remote-api/python/tests/saw/test_llvm_struct.py @@ -47,17 +47,8 @@ def specification(self): class LLVMStructTest(unittest.TestCase): - - @classmethod - def setUpClass(self): - connect(reset_server=True) - - @classmethod - def tearDownClass(self): - disconnect() - - def test_llvm_struct(self): + connect(reset_server=True) if __name__ == "__main__": view(LogResults()) bcname = str(Path('tests','saw','test-files', 'llvm_struct.bc')) mod = llvm_load_module(bcname) 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 9126844905..b6c2d8b5d2 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 @@ -17,16 +17,8 @@ def specification(self): class LLVMStructTest(unittest.TestCase): - - @classmethod - def setUpClass(self): - connect(reset_server=True) - - @classmethod - def tearDownClass(self): - disconnect() - def test_llvm_struct(self): + connect(reset_server=True) if __name__ == "__main__": view(LogResults()) bcname = str(Path('tests','saw','test-files', 'llvm_struct_type.bc')) mod = llvm_load_module(bcname) 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 1dd7d8a89e..f3e5d89287 100644 --- a/saw-remote-api/python/tests/saw/test_nested_struct.py +++ b/saw-remote-api/python/tests/saw/test_nested_struct.py @@ -24,16 +24,8 @@ def specification(self): self.returns(b) class LLVMNestedStructTest(unittest.TestCase): - - @classmethod - def setUpClass(self): - connect(reset_server=True) - - @classmethod - def tearDownClass(self): - disconnect() - def test_llvm_struct(self): + connect(reset_server=True) if __name__ == "__main__": view(LogResults()) bcname = str(Path('tests','saw','test-files', 'nested_struct.bc')) 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 a21a2af96d..bc2910b497 100644 --- a/saw-remote-api/python/tests/saw/test_nested_struct2.py +++ b/saw-remote-api/python/tests/saw/test_nested_struct2.py @@ -26,16 +26,8 @@ def specification(self): self.returns(b) class LLVMNestedStructTest(unittest.TestCase): - - @classmethod - def setUpClass(self): - connect(reset_server=True) - - @classmethod - def tearDownClass(self): - disconnect() - def test_llvm_struct(self): + connect(reset_server=True) if __name__ == "__main__": view(LogResults()) bcname = str(Path('tests','saw','test-files', 'nested_struct.bc')) 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 3b719fa8f7..e223a1c0c0 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 @@ -23,16 +23,8 @@ def specification(self) -> None: class PointsToAtTypeTest(unittest.TestCase): - - @classmethod - def setUpClass(self): - connect(reset_server=True) - - @classmethod - def tearDownClass(self): - disconnect() - def test_points_to_at_type(self): + connect(reset_server=True) if __name__ == "__main__": view(LogResults()) bcname = str(Path('tests','saw','test-files', 'points_to_at_type.bc')) mod = llvm_load_module(bcname) diff --git a/saw-remote-api/python/tests/saw/test_salsa20.py b/saw-remote-api/python/tests/saw/test_salsa20.py index 46c822f16d..f2a226b309 100644 --- a/saw-remote-api/python/tests/saw/test_salsa20.py +++ b/saw-remote-api/python/tests/saw/test_salsa20.py @@ -121,16 +121,8 @@ def specification(self): self.points_to(m_p, cryptol("Salsa20_encrypt")((k, v, m))) class Salsa20EasyTest(unittest.TestCase): - - @classmethod - def setUpClass(self): - connect(reset_server=True) - - @classmethod - def tearDownClass(self): - disconnect() - def test_salsa20(self): + connect(reset_server=True) if __name__ == "__main__": view(LogResults()) bcname = str(Path('tests','saw','test-files', 'salsa20.bc')) diff --git a/saw-remote-api/python/tests/saw/test_swap.py b/saw-remote-api/python/tests/saw/test_swap.py index 733181918d..50592e4dcb 100644 --- a/saw-remote-api/python/tests/saw/test_swap.py +++ b/saw-remote-api/python/tests/saw/test_swap.py @@ -23,17 +23,8 @@ def specification(self) -> None: class SwapEasyTest(unittest.TestCase): - - @classmethod - def setUpClass(self): - saw.connect(reset_server=True) - - @classmethod - def tearDownClass(self): - saw.reset_server() - saw.disconnect() - def test_swap(self): + saw.connect(reset_server=True) if __name__ == "__main__": saw.view(saw.LogResults()) swap_bc = str(Path('tests','saw','test-files', 'swap.bc')) 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 40e55c924c..5e6dbed7fd 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 @@ -2,10 +2,10 @@ import saw from saw.proofscript import * import unittest +import sys class LLVMAssumeTest(unittest.TestCase): - def test_llvm_assume(self): c = saw.connection.connect(reset_server=True) if __name__ == "__main__": saw.view(saw.LogResults()) @@ -43,8 +43,7 @@ def test_llvm_assume(self): prover = ProofScript([abc]).to_json() c.llvm_assume('m', 'seven', seven_contract, 'seven_ov').result() c.llvm_verify('m', 'addone', ['seven_ov'], False, addone_contract, prover, 'addone_ov').result() - c.reset_server() - c.disconnect() + if __name__ == "__main__": unittest.main() 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 3cfad443f8..a42160b21a 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 @@ -10,6 +10,7 @@ class Salsa20LowLevelTest(unittest.TestCase): def test_salsa20(self): c = saw.connection.connect(reset_server=True) + if __name__ == "__main__": saw.view(saw.LogResults()) bcname = str(Path('tests','saw','test-files', 'salsa20.bc')) @@ -215,7 +216,6 @@ def crypt_contract(size : int): c.llvm_verify('m', 's20_hash', ['dr_ov'], False, hash_contract, prover, 'hash_ov').result() c.llvm_verify('m', 's20_expand32', ['hash_ov'], False, expand_contract, prover, 'expand_ov').result() c.llvm_verify('m', 's20_crypt32', ['expand_ov'], False, crypt_contract(63), prover, 'crypt_ov').result() - c.disconnect() if __name__ == "__main__": unittest.main() 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 f62cae2349..e89527a0a5 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 @@ -5,9 +5,7 @@ class SevenTest(unittest.TestCase): def test_seven(self): - c = saw.connection.connect(reset_server=True) - c.reset() if __name__ == "__main__": saw.view(saw.LogResults()) seven_bc = str(Path('tests','saw','test-files', 'seven.bc')) @@ -29,7 +27,6 @@ def test_seven(self): prover = ProofScript([abc]).to_json() c.llvm_verify('m', 'seven', [], False, contract, prover, 'ok').result() - c.disconnect() if __name__ == "__main__": unittest.main() 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 a11375c48b..f38fdb160f 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 @@ -6,9 +6,7 @@ class SwapLowLevelTest(unittest.TestCase): def test_swap(self): - c = saw.connection.connect(reset_server=True) - c.reset_server() if __name__ == "__main__": saw.view(saw.LogResults()) swap_bc = str(Path('tests','saw','test-files', 'swap.bc')) @@ -56,7 +54,6 @@ def test_swap(self): prover = ProofScript([abc]).to_json() c.llvm_verify('m', 'swap', [], False, contract, prover, 'ok').result() - c.disconnect() if __name__ == "__main__": 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 b5eec3ecf6..90e9874637 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 @@ -6,7 +6,6 @@ class TrivialTest(unittest.TestCase): def test_trivial(self): - c = saw.connection.connect(reset_server=True) if __name__ == "__main__": saw.view(saw.LogResults()) @@ -33,7 +32,6 @@ def test_trivial(self): prover = ProofScript([abc]).to_json() c.llvm_verify('m', 'always_null', [], False, contract, prover, 'ok').result() - c.disconnect() if __name__ == "__main__": diff --git a/saw-remote-api/saw-remote-api.cabal b/saw-remote-api/saw-remote-api.cabal index bc5aa5f67e..51357acb7d 100644 --- a/saw-remote-api/saw-remote-api.cabal +++ b/saw-remote-api/saw-remote-api.cabal @@ -79,6 +79,7 @@ library SAWServer.Data.LLVMType, SAWServer.Data.SetupValue, SAWServer.Exceptions, + SAWServer.Ghost, SAWServer.JVMCrucibleSetup, SAWServer.JVMVerify, SAWServer.LLVMCrucibleSetup, diff --git a/saw-remote-api/saw-remote-api/Main.hs b/saw-remote-api/saw-remote-api/Main.hs index d401dafc24..0b25d4b819 100644 --- a/saw-remote-api/saw-remote-api/Main.hs +++ b/saw-remote-api/saw-remote-api/Main.hs @@ -16,6 +16,9 @@ import SAWServer.CryptolSetup cryptolLoadModule, cryptolLoadFileDescr, cryptolLoadFile ) +import SAWServer.Ghost + ( createGhostVariableDescr, + createGhostVariable ) --import SAWServer.JVMCrucibleSetup --import SAWServer.JVMVerify import SAWServer.LLVMCrucibleSetup @@ -94,6 +97,10 @@ sawMethods = llvmAssumeDescr llvmAssume -- General + , Argo.command + "SAW/create ghost variable" + createGhostVariableDescr + createGhostVariable , Argo.command "SAW/make simpset" makeSimpsetDescr diff --git a/saw-remote-api/scripts/run_rpc_tests.sh b/saw-remote-api/scripts/run_rpc_tests.sh index 3d59b34065..e77670daad 100755 --- a/saw-remote-api/scripts/run_rpc_tests.sh +++ b/saw-remote-api/scripts/run_rpc_tests.sh @@ -19,8 +19,11 @@ run_test poetry run mypy saw/ export SAW_SERVER=$(which saw-remote-api) if [[ ! -x "$SAW_SERVER" ]]; then - echo "could not locate saw-remote-api executable - try executing with cabal v2-exec" - exit 1 + export SAW_SERVER=$(cabal v2-exec which saw-remote-api) + if [[ ! -x "$SAW_SERVER" ]]; then + echo "could not locate saw-remote-api executable" + exit 1 + fi fi echo "Running saw-remote-api tests..." diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs index b69032d9f8..57a910e2db 100644 --- a/saw-remote-api/src/SAWServer.hs +++ b/saw-remote-api/src/SAWServer.hs @@ -37,7 +37,6 @@ import qualified Data.AIG as AIG #endif import qualified Lang.Crucible.FunctionHandle as Crucible (HandleAllocator, newHandleAllocator) import qualified Lang.Crucible.JVM as CJ -import qualified Text.LLVM.AST as LLVM import qualified Lang.JVM.Codebase as JSS import qualified Verifier.SAW.CryptolEnv as CryptolEnv import Verifier.SAW.Module (emptyModule) @@ -46,11 +45,10 @@ import Verifier.SAW.Term.Functor (mkModuleName) import Verifier.SAW.TypedTerm (TypedTerm, CryptolModule) -import qualified SAWScript.Crucible.Common.MethodSpec as CMS (CrucibleMethodSpecIR) import SAWScript.Crucible.LLVM.Builtins (CheckPointsToType) import SAWScript.Crucible.LLVM.X86 (defaultStackBaseAlign) +import qualified SAWScript.Crucible.Common.MethodSpec as CMS (CrucibleMethodSpecIR, GhostGlobal) import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMS (SomeLLVM, LLVMModule) -import SAWScript.JavaExpr (JavaType(..)) import SAWScript.Options (defaultOptions) import SAWScript.Position (Pos(..)) import SAWScript.Prover.Rewrite (basic_ss) @@ -78,13 +76,13 @@ type CryptolAST = P.Expr P.PName data SAWTask = ProofScriptTask - | LLVMCrucibleSetup ServerName [SetupStep LLVM.Type] - | JVMSetup ServerName [SetupStep JavaType] + | LLVMCrucibleSetup ServerName + | JVMSetup ServerName instance Show SAWTask where show ProofScriptTask = "ProofScript" - show (LLVMCrucibleSetup n steps) = "(LLVMCrucibleSetup" ++ show n ++ " " ++ show steps ++ ")" - show (JVMSetup n steps) = "(JVMSetup" ++ show n ++ " " ++ show steps ++ ")" + show (LLVMCrucibleSetup n) = "(LLVMCrucibleSetup" ++ show n ++ ")" + show (JVMSetup n) = "(JVMSetup" ++ show n ++ ")" data CrucibleSetupVal e @@ -104,6 +102,7 @@ data SetupStep ty = SetupReturn (CrucibleSetupVal CryptolAST) -- ^ The return value | SetupFresh ServerName Text ty -- ^ Server name to save in, debug name, fresh variable type | SetupAlloc ServerName ty Bool (Maybe Int) -- ^ Server name to save in, type of allocation, mutability, alignment + | SetupGhostValue ServerName Text CryptolAST -- ^ Variable, term | SetupPointsTo (CrucibleSetupVal CryptolAST) (CrucibleSetupVal CryptolAST) (Maybe (CheckPointsToType ty)) @@ -285,6 +284,7 @@ data ServerVal | VLLVMModule (Some CMS.LLVMModule) | VJVMMethodSpecIR (CMS.CrucibleMethodSpecIR CJ.JVM) | VLLVMMethodSpecIR (CMS.SomeLLVM CMS.CrucibleMethodSpecIR) + | VGhostVar CMS.GhostGlobal instance Show ServerVal where show (VTerm t) = "(VTerm " ++ show t ++ ")" @@ -297,6 +297,7 @@ instance Show ServerVal where show (VLLVMModule (Some _)) = "VLLVMModule" show (VLLVMMethodSpecIR _) = "VLLVMMethodSpecIR" show (VJVMMethodSpecIR _) = "VJVMMethodSpecIR" + show (VGhostVar x) = "(VGhostVar " ++ show x ++ ")" class IsServerVal a where toServerVal :: a -> ServerVal @@ -322,6 +323,9 @@ instance IsServerVal (CMS.SomeLLVM CMS.CrucibleMethodSpecIR) where instance IsServerVal JSS.Class where toServerVal = VJVMClass +instance IsServerVal CMS.GhostGlobal where + toServerVal = VGhostVar + class KnownCrucibleSetupType a where knownCrucibleSetupRepr :: CrucibleSetupTypeRepr a @@ -411,3 +415,15 @@ getTerm n = case v of VTerm t -> return t _other -> Argo.raise (notATerm n) + +getGhost :: ServerName -> Argo.Command SAWState CMS.GhostGlobal +getGhost n = + do v <- getServerVal n + case v of + VGhostVar x -> return x + _other -> error "TODO" -- raise (notAGhostVariable n) -- TODO + +getGhosts :: Argo.Command SAWState [(ServerName, CMS.GhostGlobal)] +getGhosts = + do SAWEnv serverEnv <- view sawEnv <$> Argo.getState + return [ (n, g) | (n, VGhostVar g) <- M.toList serverEnv ] diff --git a/saw-remote-api/src/SAWServer/Data/Contract.hs b/saw-remote-api/src/SAWServer/Data/Contract.hs index d3a8bcc4e4..d3647de328 100644 --- a/saw-remote-api/src/SAWServer/Data/Contract.hs +++ b/saw-remote-api/src/SAWServer/Data/Contract.hs @@ -9,11 +9,12 @@ module SAWServer.Data.Contract , Contract(..) , ContractVar(..) , Allocated(..) + , GhostValue(..) , PointsTo(..) ) where import Control.Applicative -import Data.Aeson (FromJSON(..), withObject, withText, (.:), (.:?)) +import Data.Aeson (FromJSON(..), withObject, withText, (.:), (.:?), (.!=)) import Data.Text (Text) import SAWScript.Crucible.LLVM.Builtins (CheckPointsToType(..)) @@ -31,11 +32,13 @@ data Contract ty cryptolExpr = { preVars :: [ContractVar ty] , preConds :: [cryptolExpr] , preAllocated :: [Allocated ty] + , preGhostValues :: [GhostValue cryptolExpr] , prePointsTos :: [PointsTo ty cryptolExpr] , argumentVals :: [CrucibleSetupVal cryptolExpr] , postVars :: [ContractVar ty] , postConds :: [cryptolExpr] , postAllocated :: [Allocated ty] + , postGhostValues :: [GhostValue cryptolExpr] , postPointsTos :: [PointsTo ty cryptolExpr] , returnVal :: Maybe (CrucibleSetupVal cryptolExpr) } @@ -68,6 +71,13 @@ data CheckAgainstTag = TagCheckAgainstPointerType | TagCheckAgainstCastedType + +data GhostValue cryptolExpr = + GhostValue + { ghostVarName :: ServerName + , ghostValue :: cryptolExpr + } deriving stock (Functor, Foldable, Traversable) + instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (PointsTo ty cryptolExpr) where parseJSON = withObject "Points-to relationship" $ \o -> @@ -76,6 +86,12 @@ instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (PointsTo ty cryptolExp <*> o .:? "check points to type" <*> o .:? "condition" +instance FromJSON cryptolExpr => FromJSON (GhostValue cryptolExpr) where + parseJSON = + withObject "ghost variable value" $ \o -> + GhostValue <$> o .: "server name" + <*> o .: "value" + instance FromJSON ty => FromJSON (Allocated ty) where parseJSON = withObject "allocated thing" $ \o -> @@ -97,11 +113,13 @@ instance (FromJSON ty, FromJSON e) => FromJSON (Contract ty e) where Contract <$> o .: "pre vars" <*> o .: "pre conds" <*> o .: "pre allocated" + <*> o .:? "pre ghost values" .!= [] <*> o .: "pre points tos" <*> o .: "argument vals" <*> o .: "post vars" <*> o .: "post conds" <*> o .: "post allocated" + <*> o .:? "post ghost values" .!= [] <*> o .: "post points tos" <*> o .:? "return val" diff --git a/saw-remote-api/src/SAWServer/Ghost.hs b/saw-remote-api/src/SAWServer/Ghost.hs new file mode 100644 index 0000000000..9df1d65b68 --- /dev/null +++ b/saw-remote-api/src/SAWServer/Ghost.hs @@ -0,0 +1,49 @@ +{-# LANGUAGE OverloadedStrings #-} +module SAWServer.Ghost + ( createGhostVariable + , createGhostVariableDescr + ) where + +import Data.Aeson (FromJSON(..), withObject, (.:)) + +import Argo +import qualified Argo.Doc as Doc +import Data.Text (Text) +import Control.Monad.State +import Data.Parameterized.Classes (knownRepr) + +import Lang.Crucible.CFG.Common (freshGlobalVar) +import SAWScript.Crucible.Common.MethodSpec (GhostGlobal) + +import SAWServer +import SAWServer.OK + +createGhostVariableDescr :: Doc.Block +createGhostVariableDescr = + Doc.Paragraph [Doc.Text "Create a ghost global variable to represent proof-specific program state."] + +freshGhost :: Text -> Command SAWState GhostGlobal +freshGhost name = + do allocator <- getHandleAlloc + liftIO (freshGlobalVar allocator name knownRepr) + +createGhostVariable :: CreateGhostParams -> Command SAWState OK +createGhostVariable (CreateGhostParams displayName serverName) = + do setServerVal serverName =<< freshGhost displayName + ok + +data CreateGhostParams + = CreateGhostParams Text ServerName + +instance FromJSON CreateGhostParams where + parseJSON = + withObject "parameters for creating a ghost variable" $ \o -> + CreateGhostParams <$> o .: "display name" <*> o.: "server name" + +instance Doc.DescribedParams CreateGhostParams where + parameterFieldDescription = + [ ("display name", + Doc.Paragraph [Doc.Text "The name to assign to the ghost variable for display."]) + , ("server name", + Doc.Paragraph [Doc.Text "The server name to use to access the ghost variable later."]) + ] diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs index 629a989b9c..e300be4e36 100644 --- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs @@ -8,8 +8,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE PartialTypeSignatures #-} module SAWServer.JVMCrucibleSetup - ( startJVMSetup - , jvmLoadClass + ( jvmLoadClass , compileJVMContract ) where @@ -55,12 +54,11 @@ import SAWServer SAWState, SetupStep(..), CrucibleSetupVal(CryptolExpr, NullValue, NamedValue), - SAWTask(JVMSetup), sawTask, - pushTask, setServerVal ) import SAWServer.Data.Contract ( PointsTo(PointsTo), + GhostValue(..), Allocated(Allocated), ContractVar(ContractVar), Contract(preVars, preConds, preAllocated, prePointsTos, @@ -72,11 +70,6 @@ import SAWServer.Exceptions ( notAtTopLevel ) import SAWServer.OK ( OK, ok ) import SAWServer.TopLevel ( tl ) -startJVMSetup :: StartJVMSetupParams -> Argo.Command SAWState OK -startJVMSetup (StartJVMSetupParams n) = - do pushTask (JVMSetup n []) - ok - newtype StartJVMSetupParams = StartJVMSetupParams ServerName @@ -139,6 +132,8 @@ interpretJVMSetup fileReader bic cenv0 ss = evalStateT (traverse_ go ss) (mempty lift (jvm_alloc_object c) >>= save name . Val go (SetupAlloc _ ty _ Nothing) = error $ "cannot allocate type: " ++ show ty + go (SetupGhostValue _serverName _displayName _v) = get >>= \env -> lift $ + error "nyi: ghost points-to" go (SetupPointsTo src tgt _chkTgt _cond) = get >>= \env -> lift $ do _ptr <- getSetupVal env src _tgt' <- getSetupVal env tgt diff --git a/saw-remote-api/src/SAWServer/JVMVerify.hs b/saw-remote-api/src/SAWServer/JVMVerify.hs index 82eeb6f126..3e64fedfbf 100644 --- a/saw-remote-api/src/SAWServer/JVMVerify.hs +++ b/saw-remote-api/src/SAWServer/JVMVerify.hs @@ -42,7 +42,7 @@ jvmVerifyAssume mode (VerifyParams className fun lemmaNames checkSat contract sc case tasks of (_:_) -> Argo.raise $ notAtTopLevel $ map fst tasks [] -> - do pushTask (JVMSetup lemmaName []) + do pushTask (JVMSetup lemmaName) state <- Argo.getState cls <- getJVMClass className let bic = view sawBIC state diff --git a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs index 1e5a3e21ff..8f38d952f8 100644 --- a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs @@ -7,9 +7,9 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE PartialTypeSignatures #-} +{-# LANGUAGE TupleSections #-} module SAWServer.LLVMCrucibleSetup - ( startLLVMCrucibleSetup - , llvmLoadModule + ( llvmLoadModule , llvmLoadModuleDescr , Contract(..) , ContractVar(..) @@ -20,23 +20,15 @@ module SAWServer.LLVMCrucibleSetup import Control.Exception (throw) import Control.Lens ( view ) -import Control.Monad.State - ( evalStateT, - MonadIO(liftIO), - MonadState(get, put), - MonadTrans(lift), - modify' ) +import Control.Monad.IO.Class import Data.Aeson (FromJSON(..), withObject, (.:)) import Data.ByteString (ByteString) -import Data.Foldable ( traverse_ ) import Data.Map (Map) import qualified Data.Map as Map -import Data.Maybe ( maybeToList ) import qualified Data.Text as T import qualified Cryptol.Parser.AST as P import Cryptol.Utils.Ident (mkIdent) -import qualified Text.LLVM.AST as LLVM import qualified Data.LLVM.BitCode as LLVM import qualified SAWScript.Crucible.Common.MethodSpec as MS (SetupValue(..)) import SAWScript.Crucible.LLVM.Builtins @@ -47,10 +39,12 @@ import SAWScript.Crucible.LLVM.Builtins , llvm_execute_func , llvm_fresh_var , llvm_points_to_internal + , llvm_ghost_value , llvm_return , llvm_precond , llvm_postcond ) import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMS +import qualified SAWScript.Crucible.Common.MethodSpec as CMS (GhostGlobal) import SAWScript.Value (BuiltinContext, LLVMCrucibleSetupM(..), biSharedContext) import qualified Verifier.SAW.CryptolEnv as CEnv import Verifier.SAW.CryptolEnv (CryptolEnv) @@ -61,15 +55,12 @@ import qualified Argo.Doc as Doc import SAWServer as Server ( ServerName(..), SAWState, - SetupStep(..), CrucibleSetupVal(..), - SAWTask(LLVMCrucibleSetup), sawTask, - pushTask, getHandleAlloc, setServerVal ) import SAWServer.Data.Contract - ( PointsTo(..), Allocated(..), ContractVar(..), Contract(..) ) + ( PointsTo(..), GhostValue(..), Allocated(..), ContractVar(..), Contract(..) ) import SAWServer.Data.LLVMType (JSONLLVMType, llvmType) import SAWServer.Data.SetupValue () import SAWServer.CryptolExpression (CryptolModuleException(..), getTypedTermOfCExp) @@ -77,11 +68,6 @@ import SAWServer.Exceptions ( notAtTopLevel, cantLoadLLVMModule ) import SAWServer.OK ( OK, ok ) import SAWServer.TrackFile ( trackFile ) -startLLVMCrucibleSetup :: StartLLVMCrucibleSetupParams -> Argo.Command SAWState OK -startLLVMCrucibleSetup (StartLLVMCrucibleSetupParams n) = - do pushTask (LLVMCrucibleSetup n []) - ok - newtype StartLLVMCrucibleSetupParams = StartLLVMCrucibleSetupParams ServerName @@ -92,68 +78,81 @@ instance FromJSON StartLLVMCrucibleSetupParams where newtype ServerSetupVal = Val (CMS.AllLLVM MS.SetupValue) --- TODO: this is an extra layer of indirection that could be collapsed, but is easy to implement for now. compileLLVMContract :: (FilePath -> IO ByteString) -> BuiltinContext -> + Map ServerName CMS.GhostGlobal -> CryptolEnv -> Contract JSONLLVMType (P.Expr P.PName) -> LLVMCrucibleSetupM () -compileLLVMContract fileReader bic cenv c = - interpretLLVMSetup fileReader bic cenv steps - where - setupFresh (ContractVar n dn ty) = SetupFresh n dn (llvmType ty) - setupAlloc (Allocated n ty mut align) = SetupAlloc n (llvmType ty) mut align - steps = - map setupFresh (preVars c) ++ - map SetupPrecond (preConds c) ++ - map setupAlloc (preAllocated c) ++ - map (\(PointsTo p v chkV cond) -> SetupPointsTo p v (fmap (fmap llvmType) chkV) cond) (prePointsTos c) ++ - [ SetupExecuteFunction (argumentVals c) ] ++ - map setupFresh (postVars c) ++ - map SetupPostcond (postConds c) ++ - map setupAlloc (postAllocated c) ++ - map (\(PointsTo p v chkV cond) -> SetupPointsTo p v (fmap (fmap llvmType) chkV) cond) (postPointsTos c) ++ - [ SetupReturn v | v <- maybeToList (returnVal c) ] - -interpretLLVMSetup :: - (FilePath -> IO ByteString) -> - BuiltinContext -> - CryptolEnv -> - [SetupStep LLVM.Type] -> - LLVMCrucibleSetupM () -interpretLLVMSetup fileReader bic cenv0 ss = - evalStateT (traverse_ go ss) (mempty, cenv0) +compileLLVMContract fileReader bic ghostEnv cenv0 c = + do allocsPre <- mapM setupAlloc (preAllocated c) + (envPre, cenvPre) <- setupState allocsPre (Map.empty, cenv0) (preVars c) + mapM_ (\p -> getTypedTerm cenvPre p >>= llvm_precond) (preConds c) + mapM_ (setupPointsTo (envPre, cenvPre)) (prePointsTos c) + mapM_ (setupGhostValue ghostEnv cenvPre) (preGhostValues c) + traverse (getSetupVal (envPre, cenvPre)) (argumentVals c) >>= llvm_execute_func + allocsPost <- mapM setupAlloc (postAllocated c) + (envPost, cenvPost) <- setupState (allocsPre ++ allocsPost) (envPre, cenvPre) (postVars c) + mapM_ (\p -> getTypedTerm cenvPost p >>= llvm_postcond) (postConds c) + mapM_ (setupPointsTo (envPost, cenvPost)) (postPointsTos c) + mapM_ (setupGhostValue ghostEnv cenvPost) (postGhostValues c) + case returnVal c of + Just v -> getSetupVal (envPost, cenvPost) v >>= llvm_return + Nothing -> return () where - go (SetupReturn v) = get >>= \env -> lift $ getSetupVal env v >>= llvm_return - -- TODO: do we really want two names here? - go (SetupFresh name@(ServerName n) debugName ty) = - do t <- lift $ llvm_fresh_var (T.unpack debugName) ty - (env, cenv) <- get - put (env, CEnv.bindTypedTerm (mkIdent n, t) cenv) - save name (Val (CMS.anySetupTerm t)) - go (SetupAlloc name ty True Nothing) = - lift (llvm_alloc ty) >>= save name . Val - go (SetupAlloc name ty False Nothing) = - lift (llvm_alloc_readonly ty) >>= save name . Val - go (SetupAlloc name ty True (Just align)) = - lift (llvm_alloc_aligned align ty) >>= save name . Val - go (SetupAlloc name ty False (Just align)) = - lift (llvm_alloc_readonly_aligned align ty) >>= save name . Val - go (SetupPointsTo src tgt chkTgt cond) = get >>= \env -> lift $ - do ptr <- getSetupVal env src - tgt' <- getSetupVal env tgt - cond' <- traverse (getTypedTerm env) cond - llvm_points_to_internal chkTgt cond' ptr tgt' - go (SetupExecuteFunction args) = - get >>= \env -> - lift $ traverse (getSetupVal env) args >>= llvm_execute_func - go (SetupPrecond p) = get >>= \env -> lift $ - getTypedTerm env p >>= llvm_precond - go (SetupPostcond p) = get >>= \env -> lift $ - getTypedTerm env p >>= llvm_postcond - - save name val = modify' (\(env, cenv) -> (Map.insert name val env, cenv)) + setupFresh (ContractVar n dn ty) = + do t <- llvm_fresh_var (T.unpack dn) (llvmType ty) + return (n, t) + + setupState allocs (env, cenv) vars = + do freshTerms <- mapM setupFresh vars + let cenv' = foldr (\(ServerName n, t) -> CEnv.bindTypedTerm (mkIdent n, t)) cenv freshTerms + let env' = Map.union env $ Map.fromList $ + [ (n, Val (CMS.anySetupTerm t)) | (n, t) <- freshTerms ] ++ + [ (n, Val v) | (n, v) <- allocs ] + return (env', cenv') + + setupAlloc (Allocated n ty mut malign) = + case (mut, malign) of + (True, Nothing) -> (n,) <$> llvm_alloc ty' + (False, Nothing) -> (n,) <$> llvm_alloc_readonly ty' + (True, (Just align)) -> (n,) <$> llvm_alloc_aligned align ty' + (False, (Just align)) -> (n,) <$> llvm_alloc_readonly_aligned align ty' + where + ty' = llvmType ty + + setupPointsTo env (PointsTo p v chkTgt cond) = + do ptr <- getSetupVal env p + val <- getSetupVal env v + cond' <- traverse (getTypedTerm (snd env)) cond + let chkTgt' = fmap (fmap llvmType) chkTgt + llvm_points_to_internal chkTgt' cond' ptr val + + setupGhostValue genv cenv (GhostValue serverName e) = + do g <- resolve genv serverName + t <- getTypedTerm cenv e + llvm_ghost_value g t + + resolve :: Map ServerName a -> ServerName -> LLVMCrucibleSetupM a + resolve env name = + LLVMCrucibleSetupM $ + case Map.lookup name env of + Just v -> return v + Nothing -> fail $ unlines + [ "Server value " ++ show name ++ " not found - impossible!" -- rule out elsewhere + , show (Map.keys env) + ] + + getTypedTerm :: + CryptolEnv -> + P.Expr P.PName -> + LLVMCrucibleSetupM TypedTerm + getTypedTerm cenv expr = LLVMCrucibleSetupM $ + do (res, warnings) <- liftIO $ getTypedTermOfCExp fileReader (biSharedContext bic) cenv expr + case res of + Right (t, _) -> return t + Left err -> throw $ CryptolModuleException err warnings getSetupVal :: (Map ServerName ServerSetupVal, CryptolEnv) -> @@ -176,30 +175,10 @@ interpretLLVMSetup fileReader bic cenv0 ss = LLVMCrucibleSetupM $ return $ CMS.anySetupGlobalInitializer name getSetupVal _ (GlobalLValue name) = LLVMCrucibleSetupM $ return $ CMS.anySetupGlobal name - getSetupVal (env, _) (NamedValue n) = LLVMCrucibleSetupM $ - resolve env n >>= - \case - Val x -> return x -- TODO add cases for the named server values that - -- are not coming from the setup monad - -- (e.g. surrounding context) - getSetupVal env (CryptolExpr expr) = - do t <- getTypedTerm env expr - return (CMS.anySetupTerm t) - - getTypedTerm :: - (Map ServerName ServerSetupVal, CryptolEnv) -> - P.Expr P.PName -> - LLVMCrucibleSetupM TypedTerm - getTypedTerm (_, cenv) expr = LLVMCrucibleSetupM $ liftIO $ - do (res, warnings) <- getTypedTermOfCExp fileReader (biSharedContext bic) cenv expr - case res of - Right (t, _) -> return t -- TODO: report warnings - Left err -> throw $ CryptolModuleException err warnings - - resolve env name = - case Map.lookup name env of - Just v -> return v - Nothing -> error "Server value not found - impossible!" -- rule out elsewhere + getSetupVal (env, _) (NamedValue n) = + resolve env n >>= \case Val x -> return x + getSetupVal (_, cenv) (CryptolExpr expr) = + CMS.anySetupTerm <$> getTypedTerm cenv expr data LLVMLoadModuleParams = LLVMLoadModuleParams ServerName FilePath diff --git a/saw-remote-api/src/SAWServer/LLVMVerify.hs b/saw-remote-api/src/SAWServer/LLVMVerify.hs index 36247f2d86..699943f2dc 100644 --- a/saw-remote-api/src/SAWServer/LLVMVerify.hs +++ b/saw-remote-api/src/SAWServer/LLVMVerify.hs @@ -11,6 +11,7 @@ module SAWServer.LLVMVerify import Prelude hiding (mod) import Control.Lens ( view ) +import qualified Data.Map as Map import SAWScript.Crucible.LLVM.Builtins ( llvm_unsafe_assume_spec, llvm_verify ) @@ -28,6 +29,7 @@ import SAWServer pushTask, dropTask, setServerVal, + getGhosts, getLLVMModule, getLLVMMethodSpecIR ) import SAWServer.CryptolExpression (getCryptolExpr) @@ -51,13 +53,15 @@ llvmVerifyAssume mode (VerifyParams modName fun lemmaNames checkSat contract scr case tasks of (_:_) -> Argo.raise $ notAtTopLevel $ map fst tasks [] -> - do pushTask (LLVMCrucibleSetup lemmaName []) + do pushTask (LLVMCrucibleSetup lemmaName) state <- Argo.getState mod <- getLLVMModule modName let bic = view sawBIC state cenv = rwCryptol (view sawTopLevelRW state) fileReader <- Argo.getFileReader - setup <- compileLLVMContract fileReader bic cenv <$> traverse getCryptolExpr contract + ghostEnv <- Map.fromList <$> getGhosts + setup <- compileLLVMContract fileReader bic ghostEnv cenv <$> + traverse getCryptolExpr contract res <- case mode of VerifyContract -> do lemmas <- mapM getLLVMMethodSpecIR lemmaNames @@ -105,7 +109,7 @@ llvmVerifyX86 (X86VerifyParams modName objName fun globals _lemmaNames checkSat case tasks of (_:_) -> Argo.raise $ notAtTopLevel $ map fst tasks [] -> - do pushTask (LLVMCrucibleSetup lemmaName []) + do pushTask (LLVMCrucibleSetup lemmaName) state <- Argo.getState mod <- getLLVMModule modName let bic = view sawBIC state @@ -113,7 +117,9 @@ llvmVerifyX86 (X86VerifyParams modName objName fun globals _lemmaNames checkSat allocs = map (\(X86Alloc name size) -> (name, size)) globals proofScript <- interpretProofScript script fileReader <- Argo.getFileReader - setup <- compileLLVMContract fileReader bic cenv <$> traverse getCryptolExpr contract + ghostEnv <- Map.fromList <$> getGhosts + setup <- compileLLVMContract fileReader bic ghostEnv cenv <$> + traverse getCryptolExpr contract res <- tl $ llvm_verify_x86 mod objName fun allocs checkSat setup proofScript dropTask setServerVal lemmaName res diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 39f6575958..bf191a09ba 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -762,11 +762,19 @@ offline_aig path = do SV.AIGProxy proxy <- SV.scriptTopLevel SV.getProxy proveWithSATExporter (Prover.writeAIG_SAT proxy) mempty path "." ".aig" +offline_aig_external :: FilePath -> ProofScript () +offline_aig_external path = + proveWithSATExporter Prover.writeAIG_SATviaVerilog mempty path "." ".aig" + offline_cnf :: FilePath -> ProofScript () offline_cnf path = do SV.AIGProxy proxy <- SV.scriptTopLevel SV.getProxy proveWithSATExporter (Prover.writeCNF proxy) mempty path "." ".cnf" +offline_cnf_external :: FilePath -> ProofScript () +offline_cnf_external path = + proveWithSATExporter Prover.writeCNF_SATviaVerilog mempty path "." ".cnf" + offline_coq :: FilePath -> ProofScript () offline_coq path = proveWithPropExporter (const (Prover.writeCoqProp "goal" [] [])) path "_" ".v" diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index b62e2bd229..85fae2d9fa 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -38,6 +38,7 @@ module SAWScript.Crucible.LLVM.Override , learnCond , learnSetupCondition + , executeSetupCondition , matchArg , assertTermEqualities , methodSpecHandler diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 1d7d1933dd..6d1eafd3af 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -72,6 +72,7 @@ import SAWScript.X86 hiding (Options) import SAWScript.X86Spec import SAWScript.Crucible.Common +import qualified SAWScript.Crucible.Common as Common import qualified SAWScript.Crucible.Common.MethodSpec as MS import qualified SAWScript.Crucible.Common.Override as O import qualified SAWScript.Crucible.Common.Setup.Type as Setup @@ -320,7 +321,7 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se liftIO $ sawRegisterSymFunInterp sawst (Macaw.fnShaMaj sfs) $ cryptolUninterpreted cenv "Maj" let preserved = Set.fromList . catMaybes $ stringToReg . Text.toLower . Text.pack <$> rwPreservedRegs rw - (C.SomeCFG cfg, elf, relf, addr, cfgs) <- liftIO $ buildCFG opts halloc preserved path nm + (C.SomeCFG cfg, elf, relf, addr, cfgs) <- io $ buildCFG opts halloc preserved path nm addrInt <- if Macaw.segmentBase (Macaw.segoffSegment addr) == 0 then pure . toInteger $ Macaw.segmentOffset (Macaw.segoffSegment addr) + Macaw.segoffOffset addr else fail $ mconcat ["Address of \"", nm, "\" is not an absolute address"] @@ -351,9 +352,9 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se let ?lc = modTrans llvmModule ^. C.LLVM.transContext . C.LLVM.llvmTypeCtx - emptyState <- liftIO $ initialState sym opts sc cc elf relf methodSpec globsyms maxAddr + emptyState <- io $ initialState sym opts sc cc elf relf methodSpec globsyms maxAddr balign <- integerToAlignment $ rwStackBaseAlign rw - (env, preState) <- liftIO . runX86Sim emptyState $ setupMemory globsyms balign + (env, preState) <- io . runX86Sim emptyState $ setupMemory globsyms balign let funcLookup = Macaw.LookupFunctionHandle $ \st _mem regs -> do @@ -437,7 +438,15 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se liftIO $ C.executeCrucible execFeatures initial >>= \case C.FinishedResult{} -> pure () - C.AbortedResult{} -> printOutLn opts Warn "Warning: function never returns" + C.AbortedResult _ ar -> do + printOutLn opts Warn "Warning: function never returns" + print $ Common.ppAbortedResult + ( \gp -> + case C.lookupGlobal mvar $ gp ^. C.gpGlobals of + Nothing -> "LLVM memory global variable not initialized" + Just mem -> C.LLVM.ppMem $ C.LLVM.memImplHeap mem + ) + ar C.TimeoutResult{} -> fail "Execution timed out" stats <- checkGoals sym opts sc tactic @@ -870,7 +879,10 @@ assertPost globals env premem preregs = do pointsToMatches <- forM (ms ^. MS.csPostState . MS.csPointsTos) $ assertPointsTo env tyenv nameEnv - let setupConditionMatches = fmap + let setupConditionMatchesPre = fmap -- assume preconditions + (LO.executeSetupCondition opts sc cc ms) + $ ms ^. MS.csPreState . MS.csConditions + let setupConditionMatchesPost = fmap -- assert postconditions (LO.learnSetupCondition opts sc cc ms MS.PostState) $ ms ^. MS.csPostState . MS.csConditions @@ -889,12 +901,15 @@ assertPost globals env premem preregs = do . sequence_ $ mconcat [ returnMatches , pointsToMatches - , setupConditionMatches + , setupConditionMatchesPre + , setupConditionMatchesPost , [LO.assertTermEqualities sc cc] ] st <- case result of Left err -> throwX86 $ show err Right (_, st) -> pure st + liftIO . forM_ (view O.osAssumes st) $ \p -> + C.addAssumption sym . C.LabeledPred p $ C.AssumptionReason (st ^. O.osLocation) "precondition" liftIO . forM_ (view LO.osAsserts st) $ \(W4.LabeledPred p r) -> C.addAssertion sym $ C.LabeledPred p r diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 932b5d616c..88ff31e39c 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -992,6 +992,15 @@ primitives = Map.fromList , "bits to a finite number of bits." ] + , prim "write_aig_external" "String -> Term -> TopLevel ()" + (scVal writeAIGviaVerilog) + Current + [ "Write out a representation of a term in binary AIGER format. The" + , "term must be representable as a function from a finite number of" + , "bits to a finite number of bits. Uses ABC to convert an intermediate" + , "Verilog file." + ] + , prim "write_saig" "String -> Term -> TopLevel ()" (pureVal writeSAIGPrim) Current @@ -1026,6 +1035,11 @@ primitives = Map.fromList Current [ "Write the given term to the named file in CNF format." ] + , prim "write_cnf_external" "String -> Term -> TopLevel ()" + (scVal write_cnf_external) + Current + [ "Write the given term to the named file in CNF format." ] + , prim "write_smtlib2" "String -> Term -> TopLevel ()" (scVal write_smtlib2) Current @@ -1396,11 +1410,25 @@ primitives = Map.fromList Current [ "Write the current goal to the given file in AIGER format." ] + , prim "offline_aig_external" "String -> ProofScript ()" + (pureVal offline_aig_external) + Current + [ "Write the current goal to the given file in AIGER format." + , "Uses ABC and an intermediate Verilog file." + ] + , prim "offline_cnf" "String -> ProofScript ()" (pureVal offline_cnf) Current [ "Write the current goal to the given file in CNF format." ] + , prim "offline_cnf_external" "String -> ProofScript ()" + (pureVal offline_cnf_external) + Current + [ "Write the current goal to the given file in CNF format." + , "Uses ABC and an intermediate Verilog file." + ] + , prim "offline_extcore" "String -> ProofScript ()" (pureVal offline_extcore) Current diff --git a/src/SAWScript/Prover/Exporter.hs b/src/SAWScript/Prover/Exporter.hs index 7067c25f88..e13b448fc4 100644 --- a/src/SAWScript/Prover/Exporter.hs +++ b/src/SAWScript/Prover/Exporter.hs @@ -12,12 +12,17 @@ module SAWScript.Prover.Exporter -- * External formats , writeAIG + , writeAIGviaVerilog + , writeAIG_SATviaVerilog , writeAIG_SAT , writeSAIG , writeSAIGInferLatches , writeAIGComputedLatches , writeCNF + , writeCNFviaVerilog + , writeCNF_SATviaVerilog , write_cnf + , write_cnf_external , writeSMTLib2 , writeSMTLib2What4 , write_smtlib2 @@ -39,6 +44,7 @@ module SAWScript.Prover.Exporter import Data.Foldable(toList) +import Control.Monad (unless) import Control.Monad.Except (runExceptT) import Control.Monad.IO.Class (liftIO, MonadIO) import qualified Data.AIG as AIG @@ -47,11 +53,14 @@ import Data.Parameterized.Nonce (globalNonceGenerator) import Data.Parameterized.Some (Some(..)) import Data.Set (Set) import qualified Data.SBV.Dynamic as SBV +import System.Directory (removeFile) import System.IO +import System.IO.Temp(emptySystemTempFile) import Data.Text.Prettyprint.Doc.Render.Text import Prettyprinter (vcat) import Cryptol.Utils.PP(pretty) +import Lang.JVM.ProcessUtils (readProcessExitIfFailure) import Verifier.SAW.CryptolEnv (initCryptolEnv, loadCryptolModule) import Verifier.SAW.Cryptol.Prelude (cryptolModule, scLoadPreludeModule, scLoadCryptolModule) @@ -125,6 +134,42 @@ writeAIG proxy sc f t = do aig <- bitblastPrim proxy sc t AIG.writeAiger f aig +withABCVerilog :: SharedContext -> FilePath -> Term -> (FilePath -> String) -> TopLevel () +withABCVerilog sc baseName t buildCmd = + do verilogFile <- liftIO $ emptySystemTempFile (baseName ++ ".v") + write_verilog sc verilogFile t + liftIO $ + do (out, err) <- readProcessExitIfFailure "abc" ["-q", buildCmd verilogFile] + unless (null out) $ putStrLn "ABC output:" >> putStrLn out + unless (null err) $ putStrLn "ABC errors:" >> putStrLn err + removeFile verilogFile + +-- | Write a @SATQuery@ to an AIG file by using ABC to convert a Verilog +-- file. +writeAIG_SATviaVerilog :: SharedContext -> FilePath -> SATQuery -> TopLevel () +writeAIG_SATviaVerilog sc f query = + writeAIGviaVerilog sc f =<< liftIO (satQueryAsTerm sc query) + +-- | Write a @Term@ representing a an arbitrary function to an AIG file +-- by using ABC to convert a Verilog file. +writeAIGviaVerilog :: SharedContext -> FilePath -> Term -> TopLevel () +writeAIGviaVerilog sc aigFile t = + withABCVerilog sc aigFile t $ + \verilogFile -> "%read " ++ verilogFile ++ "; %blast; &write " ++ aigFile + +-- | Write a @SATQuery@ to a CNF file by using ABC to convert a Verilog +-- file. +writeCNF_SATviaVerilog :: SharedContext -> FilePath -> SATQuery -> TopLevel () +writeCNF_SATviaVerilog sc f query = + writeCNFviaVerilog sc f =<< liftIO (satQueryAsTerm sc query) + +-- | Write a @Term@ representing a an arbitrary function to a CNF file +-- by using ABC to convert a Verilog file. +writeCNFviaVerilog :: SharedContext -> FilePath -> Term -> TopLevel () +writeCNFviaVerilog sc cnfFile t = + withABCVerilog sc cnfFile t $ + \verilogFile -> "%read " ++ verilogFile ++ "; %blast; &write_cnf " ++ cnfFile + -- | Like @writeAIG@, but takes an additional 'Integer' argument -- specifying the number of input and output bits to be interpreted as -- latches. Used to implement more friendly SAIG writers @@ -192,6 +237,11 @@ write_cnf sc f (TypedTerm schema t) = do satq <- io (predicateToSATQuery sc mempty t) writeCNF proxy sc f satq +write_cnf_external :: SharedContext -> FilePath -> TypedTerm -> TopLevel () +write_cnf_external sc f (TypedTerm schema t) = do + liftIO $ checkBooleanSchema schema + writeCNFviaVerilog sc f t + -- | Write a @Term@ representing a predicate (i.e. a monomorphic -- function returning a boolean) to an SMT-Lib version 2 file. The goal -- is to pass the term through as directly as possible, so we interpret diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index 78db76a374..a237221cbe 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -37,7 +37,8 @@ import Control.Applicative (Applicative) #endif import Control.Lens import Control.Monad.Fail (MonadFail(..)) -import Control.Monad.Catch (MonadThrow(..), MonadMask(..), MonadCatch(..)) +import Control.Monad.Catch (MonadThrow(..), MonadMask(..), + MonadCatch(..), catches, Handler(..)) import Control.Monad.Except (ExceptT(..), runExceptT, MonadError(..)) import Control.Monad.Reader (MonadReader) import qualified Control.Exception as X @@ -75,6 +76,7 @@ import SAWScript.Options (Options(printOutFn),printOutLn,Verbosity) import SAWScript.Proof import SAWScript.Prover.SolverStats import SAWScript.Crucible.LLVM.Skeleton +import SAWScript.X86 (X86Unsupported(..), X86Error(..)) import Verifier.SAW.Name (toShortName) import Verifier.SAW.CryptolEnv as CEnv @@ -423,7 +425,16 @@ runTopLevel :: TopLevel a -> TopLevelRO -> TopLevelRW -> IO (a, TopLevelRW) runTopLevel (TopLevel m) ro rw = runStateT (runReaderT m ro) rw io :: IO a -> TopLevel a -io = liftIO +io f = liftIO f + `catches` + [ Handler (\(ex :: X86Unsupported) -> handleX86Unsupported ex) + , Handler (\(ex :: X86Error) -> handleX86Error ex) + ] + where + handleX86Unsupported (X86Unsupported s) = + throwTopLevel $ "Unsupported x86 feature: " ++ s + handleX86Error (X86Error s) = + throwTopLevel $ "Error in x86 code: " ++ s throwTopLevel :: String -> TopLevel a throwTopLevel msg = do diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs index f2a970d502..940ff8fbb0 100644 --- a/src/SAWScript/X86.hs +++ b/src/SAWScript/X86.hs @@ -264,8 +264,11 @@ getElf path = Right (Elf.SomeElf hdr) | Elf.ELFCLASS64 <- Elf.headerClass (Elf.header hdr) -> pure hdr | otherwise -> unsupported "32-bit ELF format" - Left _ -> malformed "Invalid ELF header" - + Left (off, msg) -> malformed $ mconcat [ "Invalid ELF header at offset " + , show off + , ": " + , msg + ] -- | Extract a Macaw "memory" from an ELF file and resolve symbols.