diff --git a/deps/argo b/deps/argo index 5ffd2818f7..5217d1da92 160000 --- a/deps/argo +++ b/deps/argo @@ -1 +1 @@ -Subproject commit 5ffd2818f769f118a15d0e86a1fdb0c99893c444 +Subproject commit 5217d1da928a5d1902186db991dacb047d1da5d7 diff --git a/deps/cryptol b/deps/cryptol index d08cec6484..a506732dc6 160000 --- a/deps/cryptol +++ b/deps/cryptol @@ -1 +1 @@ -Subproject commit d08cec6484515e6949384a09855c10edf3933773 +Subproject commit a506732dc63cf5bd78f18ac7ac525926c805a2b6 diff --git a/saw-remote-api/docs/.gitignore b/saw-remote-api/docs/.gitignore new file mode 100644 index 0000000000..69fa449dd9 --- /dev/null +++ b/saw-remote-api/docs/.gitignore @@ -0,0 +1 @@ +_build/ diff --git a/saw-remote-api/docs/Makefile b/saw-remote-api/docs/Makefile new file mode 100644 index 0000000000..79b2d51c4b --- /dev/null +++ b/saw-remote-api/docs/Makefile @@ -0,0 +1,35 @@ +# Minimal makefile for Sphinx documentation +# + +# You can set these variables from the command line, and also +# from the environment for the first two. +SPHINXOPTS ?= +SPHINXBUILD ?= sphinx-build +SOURCEDIR = . +BUILDDIR = _build + +# Documentation taken from Argo +# Edit ARGODOCS if the dependency path changes; add reST files to ARGODEPS +# that live in Argo but are needed here +ARGODOCS = ../../deps/argo/docs +ARGODEPS = Protocol.rst + +# Documentation taken from Cryptol Remote API +# Edit CRYPTOLDOCS if the dependency path changes; add reST files to +# CRYPTOLDEPS that live in Cryptol but are needed here +CRYPTOLDOCS = ../../deps/cryptol/cryptol-remote-api/docs +CRYPTOLDEPS = Cryptol.rst Errors.rst + +# Put it first so that "make" without argument is like "make help". +help: + @$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O) + +.PHONY: help Makefile + +# Catch-all target: route all unknown targets to Sphinx using the new +# "make mode" option. $(O) is meant as a shortcut for $(SPHINXOPTS). +%: Makefile + cp $(foreach d,$(ARGODEPS),$(ARGODOCS)/$(d)) . + cp $(foreach d,$(CRYPTOLDEPS),$(CRYPTOLDOCS)/$(d)) . + @$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O) + rm $(ARGODEPS) $(CRYPTOLDEPS) diff --git a/saw-remote-api/docs/SAW.rst b/saw-remote-api/docs/SAW.rst new file mode 100644 index 0000000000..55da3e6462 --- /dev/null +++ b/saw-remote-api/docs/SAW.rst @@ -0,0 +1,424 @@ +================ +SAW Verification +================ + +Note: The SAW API is still in flux and is not yet fully documented. + +As with the Cryptol methods, server state is propagated as described in the +protocol overview. + +Methods implemented against the SAW API may throw :ref:`a variety of SAW-related +errors `, with codes in the range of ``10000``-``19999``. +Additionally, SAW verification relies on Cryptol, and some SAW methods may throw +:ref:`Cryptol server errors ` when appropriate. + +Cryptol Module Management +========================= + +Loading Modules +--------------- + +:Method name: + ``SAW/Cryptol/load module`` +:Parameters: + - ``module name``: The name of the Cryptol module to be loaded. + +Loading Files +------------- + +:Method name: + ``SAW/Cryptol/load file`` +:Parameters: + - ``file``: The name of the Cryptol source file to be loaded. + +Saving Terms +------------ + +:Method name: + ``SAW/Cryptol/save term`` +:Parameters: + - ``name``: The name to bind the value of ``expression`` to on the server. + - ``expression``: The Cryptol expression to bind the value of ``name`` to on the server. + +JVM Verification +================ + +NOTE: The following represents an aspirational view of the JVM-specific protocol; currently, +the code underlying these methods is incomplete and does not work. + +Loading Classes +--------------- + +:Method name: + ``SAW/JVM/load class`` +:Parameters: + - ``name``: The name to bind the loaded class to on the server. + - ``class``: The name of the class to load and bind the value of ``name`` to on the server. + +Verifying +--------- + +:Method name: + ``SAW/JVM/verify`` +:Parameters: + - ``module``: The name of the (previously loaded) *class* containing the function/method to verify. + - ``function``: The name of the function/method to verify. + - ``lemmas``: A list containing the names of previously proved lemmas to be used in compositional verification. + - ``check sat``: A Boolean value indicating whether or not to perform path satisfiability checking. + - ``contract``: The :ref:`specification` to perform verification against. + - ``script``: The :ref:`proof script` to use for verification. + - ``lemma name``: The name to bind the result of verification to on the server. + +Assuming +-------- + +:Method name: + ``SAW/JVM/assume`` +:Parameters: + - ``module``: The name of the (previously loaded) *class* containing the function/method to assume verified. + - ``function``: The name of the function/method to assume verified. + - ``contract``: The :ref:`specification` to assume for the given function/method. + - ``lemma name``: The name to bind the result of verification to on the server. + +LLVM Verification +================= + +Loading Modules +--------------- + +:Method name: + ``SAW/LLVM/load module`` +:Parameters: + - ``name``: The name to bind the loaded bitcode file to on the server. + - ``bitcode file``: The path to the bitcode file to load and bind to ``name`` on the server. + +Verifying (LLVM Implementations) +-------------------------------- + +:Method name: + ``SAW/LLVM/verify`` +:Parameters: + - ``module``: The name of the (previously loaded) module containing the function to verify. + - ``function``: The name of the function to verify. + - ``lemmas``: A list containing the names of previously proved lemmas to be used in compositional verification. + - ``check sat``: A Boolean value indicating whether or not to perform path satisfiability checking. + - ``contract``: The :ref:`specification` to perform verification against. + - ``script``: The :ref:`proof script` to use for verification. + - ``lemma name``: The name to bind the result of verification to on the server. + +Verifying (x86 Implementations) +------------------------------- + +:Method name: + ``SAW/LLVM/verify x86`` +:Parameters: + - ``module``: The name of the (previously loaded) module containing the type of the function to verify. + - ``object file``: The path to the x86 object file containing the implementation of the function to verify. + - ``function``: The name of the function to verify. + - ``globals``: A list containing the global allocations needed for the verification task. + - ``lemmas``: A list containing the names of previously proved lemmas to be used in compositional verification. + - ``check sat``: A Boolean value indicating whether or not to perform path satisfiability checking. + - ``contract``: The :ref:`specification` to perform verification against. + - ``script``: The :ref:`proof script` to use for verification. + - ``lemma name``: The name to bind the result of verification to on the server. + +Assuming +-------- + +:Method name: + ``SAW/LLVM/assume`` +:Parameters: + - ``module``: The name of the (previously loaded) *class* containing the function/method to assume verified. + - ``function``: The name of the function/method to assume verified. + - ``contract``: The :ref:`specification` to assume for the given function/method. + - ``lemma name``: The name to bind the result of verification to on the server. + +Proof Management +================ + +Making Simpsets +--------------- + +:Method name: + ``SAW/make simpset`` +:Parameters: + - ``elements``: A list of names bound to terms to add to the simpset. + - ``result``: The name to bind the simpset to on the server. + +Running Proof Scripts +--------------------- + +:Method name: + ``SAW/prove`` +:Parameters: + - ``script``: The :ref:`proof script` to run. + - ``term``: The name of a term bound on the server to run the proof script against. +:Return fields: + - ``status``: A string (either ``valid`` or ``invalid``) indicating whether the proof went through successfully or not. + +Setting Options +--------------- + +:Method name: + ``SAW/set option`` +:Parameters: + - ``option``: The name of the option to set. This is one of: + + * ``lax arithmetic`` + * ``SMT array memory model`` + * ``What4 hash consing`` + + - ``value``: A Boolean value indicating whether to enable/disable the feature named by ``option``. + +.. _specifications: + +Specifications +============== + +SAW verification relies on the provision of specifications to verify against. In the API, +these specifications are represented by a JSON object with the following fields: + +``pre vars`` + A list of symbolic variables introduced in the initial state section of the specification. These variables + are represented by a JSON object containing three fields: + +.. _contract-vars: + + - ``server name``: The name of the variable on the server. + - ``name``: The "display name" of the variable, used in debugging output. + - ``type``: The :ref:`LLVM` or :ref:`JVM` type of this variable. + +``pre conds`` + A list of the specification's preconditions, as :ref:`Cryptol terms`. + +``pre allocated`` + A list of allocations in the initial state section of the specification. In preconditions, + allocations specify that the function being verified expects a pointer to the allocated memory + to exist. An allocation is a JSON object containing four fields, one of which is optional: + +.. _allocation: + + - ``server name``: The name by which the allocation is referred to on the server. + - ``type``: The :ref:`LLVM` or :ref:`JVM` type of the data for which space is being allocated. + - ``mutable``: A Boolean value indicating whether the allocated memory is mutable or not. + - ``alignment``: An integer value indicating where the start of the allocated memory should + be aligned. This value must be a power of two, and the allocated memory may be aligned at + any multiple of it. The field *must* be ``null`` in JVM specifications, and *may* be ``null`` + in LLVM specifications. + +``pre points to`` + A list of 'points-to' relationships in the initial state section of the specification. These + relationships are captured in a JSON object containing two fields: + +.. _points-to: + + - ``pointer``: A :ref:`Crucible Setup value` representing the pointer. + - ``points to``: A :ref:`Crucible Setup value` representing the referent of ``pointer``. + +``argument vals`` + A list of :ref:`Crucible Setup values` representing the arguments to the function being verified. + +``post vars`` + A list of variables in the final state section of the specification. While in many cases this + list will be empty, it is sometimes useful to specify that functions return arbitrary values. + These variables are represented in the same way as :ref:`above`. + +``post conds`` + A list of the specification's postconditions, as :ref:`Cryptol terms`. + +``post allocated`` + A list of allocations in the final state section of the specification. In postconditions, + allocations specify that the function being verified allocated memory. An allocation is + represented in the same was as :ref:`above`. + +``post points tos`` + A list of 'points-to' relationships in the final state section of the specification. These + relationships are represented in the same was as :ref:`above`. + + +``return val`` + An optional :ref:`Crucible Setup value` specifying the expected return value of the function being verified. + +.. _proof-scripts: + +Proof Scripts +============= + +SAW allows one to direct a verification task using a proof script, which is simply a sequence of proof +tactics to apply. Very commonly, the proof script provided in a verification task is simply an instruction +to use an external SAT/SMT solver such as ABC, Yices, or Z3. + +A proof script is represented as a JSON object with a single field: + +``tactics`` + A list of proof tactics to apply to the context/goal. A proof tactic is represented as a JSON object + containing a tag named ``tactic``, with any further fields determined by this tag. These tag values can be: + + ``use prover`` + Apply an external prover to the goal. There is an additional field ``prover`` which is a JSON object + with a field ``name`` specifying what prover to use (one of ``abc``, ``cvc4``, ``rme``, ``yices``, or ``z3``), + and a field ``uninterpreted functions`` when ``name`` is one of ``cvc4``, ``yices``, or ``z3``. This + field is a list of names of functions taken as uninterpreted/abstract. + + ``unfold`` + Unfold terms in the context/goal. There is an additional field ``names``, a list of the names bound on + the server to unfold. + + ``beta reduce goal`` + Perform a single beta reduction on the proof goal. + + ``evaluate goal`` + Fully evaluate the proof goal. There is an additional field ``uninterpreted functions``, a list of names + of functions taken as uninterpreted/abstract. + + ``simplify`` + Simplify the context/goal. There is an additional field ``rules``, a name bound to a simpset on the server. + + ``assume unsat`` + Assume the goal is unsatisfiable, which in the current implementation of SAW should be interpreted as + assuming the property being checked to be true. This is likely to change in the future. + + ``trivial`` + States that the goal should be trivially true (either the constant ``True`` or a function that immediately + returns ``True``. This tactic fails if that is not the case. + +.. _setup-values: + +Crucible Setup Values +===================== + +Setup Values encompass all values that can occur during symbolic execution, including Cryptol terms, +pointers, arrays, and structures. They are used extensively when writing the specifications provided to the +``verify`` commands. Setup Values are represented as JSON objects containing a tag field, ``setup value``, +that determines the other fields. This tag value can be: + +``saved`` + A term previously saved on the server. There is an additional field ``name`` giving the name bound to the + term on the server. + +``null value`` + A null/empty value. + +``Cryptol`` + A Cryptol term. There is an additional field ``expression`` containing a Cryptol expression. + +``array value`` + An array value. There is an additional field ``elements`` which is a list of :ref:`Crucible Setup values` + to populate the array with. + +``field lvalue`` + A field of a struct. There are two additional fields: + + - ``base``: A :ref:`Crucible Setup value`, the structure containing the field to assign to. + - ``field``: The name of the field to assign to. + +``element lvalue`` + An element of an array. Theer are two additional fields: + + - ``base``: A :ref:`Crucible Setup value`, the array to be indexed for assignment. + - ``index``: An integer giving the index into the array to be assigned to. + +``global initializer`` + A constant global initializer value. There is an additional field ``name`` giving the name of the + global variable on the server to access the initializer of. + +``global lvalue`` + A global variable to be assigned to. There is an additional field ``name`` giving the name of the global + variable on the server that is to be assigned to. + +.. _llvm-types: + +LLVM Types +========== + +For most commands involving the introduction of variables or the allocation of space, the type of data to +be stored must be provided. Since SAW supports both LLVM and JVM verification, the types from these +respective architectures must have JSON representations. Both LLVM and JVM types are represented as JSON +objects with a tag field to indicate any additional information that must/might be present. + +The tag field is named ``type``. This tag value can be: + +``primitive type`` + An LLVM primitive type. This is an additional field ``primitive`` which can be any of the following: + + - ``label``: An LLVM label. + - ``void``: The LLVM void type. + - ``integer``: An LLVM integer. There is an additional field ``size``, an integer giving the number of + bytes in the integer type. + - ``float``: An LLVM float. There is an additional field ``float type`` which can be any of the following: + + + ``half`` + + ``float`` + + ``double`` + + ``fp128`` + + ``x86_fp80`` + + ``PPC_fp128`` + + - ``X86mmx``: An x86 SIMD instruction. + - ``metadata``: LLVM metadata. + +``type alias`` + A type alias. There is an additional field ``alias of``, which identifies the type being aliased by name. + +``array`` + An LLVM array. There are two additional fields: + + - ``size``: An integer giving the length of the array. + - ``element type``: An :ref:`LLVM type` describing the array elements. + +``function`` + A function type. There are three additional fields: + + - ``return type``: An :ref:`LLVM type` describing the return type of the function. + - ``argument types``: A list of :ref:`LLVM types` describing the arguments of the function. + - ``varargs``: A Boolean indicating whether this function takes a variable number of arguments. + +``pointer`` + A pointer type. There is an additional field ``to type``, an :ref:`LLVM type` describing the + referent type of the pointer. + +``struct`` + A structure type. There is an additional field ``fields``, a list of :ref:`LLVM types` describing + the structure fields. + +``packed struct`` + A packed structure type. There is an additional field ``fields``, a list of :ref:`LLVM types` describing + the structure fields. + +``vector`` + An LLVM vector. There are two additional fields: + + - ``size``: An integer giving the length of the array. + - ``element type``: An :ref:`LLVM type` describing the array elements. + +``opaque`` + An opaque structure type. + +.. _jvm-types: + +JVM Types +========= + +As with LLVM types, there is a tag field named ``type``. This tag value can be: + +``primitive type`` + A JVM primitive type. There is an additional field ``primitive`` which can be any of the following: + + - ``boolean``: A JVM Boolean. + - ``byte``: A JVM byte. + - ``char``: A JVM character. + - ``double``: A JVM double-precision float. + - ``float``: A JVM single-precsion float. + - ``int``: A JVM integer. + - ``long``: A JVM long integer. + - ``short``: A JVM short integer. + +``array type`` + A JVM array. There are two additional fields: + + - ``size``: An integer giving the length of the array. + - ``element type``: An :ref:`JVM type` describing the array elements. + +``class type`` + A JVM class. There is an additional field ``class name`` which identifies the class. + Class names are encoded using dots. diff --git a/saw-remote-api/docs/conf.py b/saw-remote-api/docs/conf.py new file mode 100644 index 0000000000..6514bb931a --- /dev/null +++ b/saw-remote-api/docs/conf.py @@ -0,0 +1,169 @@ +# Configuration file for the Sphinx documentation builder. +# +# This file only contains a selection of the most common options. For a full +# list see the documentation: +# https://www.sphinx-doc.org/en/master/usage/configuration.html + +# -- Path setup -------------------------------------------------------------- + +# If extensions (or modules to document with autodoc) are in another directory, +# add these directories to sys.path here. If the directory is relative to the +# documentation root, use os.path.abspath to make it absolute, like shown here. +# +# import os +# import sys +# sys.path.insert(0, os.path.abspath('.')) + + +# -- Project information ----------------------------------------------------- + +project = 'SAW Remote API' +copyright = '2020, Galois, Inc.' +author = 'Galois, Inc.' + + +# -- General configuration --------------------------------------------------- + +# Add any Sphinx extension module names here, as strings. They can be +# extensions coming with Sphinx (named 'sphinx.ext.*') or your custom +# ones. +extensions = [ + 'sphinx.ext.autodoc', + 'sphinx.ext.doctest', + 'sphinx.ext.coverage', + 'sphinx.ext.mathjax', + 'sphinx.ext.viewcode', +] + +# Add any paths that contain templates here, relative to this directory. +templates_path = ['_templates'] + +# The suffix(es) of source filenames. +# You can specify multiple suffix as a list of string: +# +# source_suffix = ['.rst', '.md'] +source_suffix = '.rst' + +# The master toctree document. +master_doc = 'index' + +# The language for content autogenerated by Sphinx. Refer to documentation +# for a list of supported languages. +# +# This is also used if you do content translation via gettext catalogs. +# Usually you set "language" from the command line for these cases. +language = None + +# List of patterns, relative to source directory, that match files and +# directories to ignore when looking for source files. +# This pattern also affects html_static_path and html_extra_path. +exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store'] + +# The name of the Pygments (syntax highlighting) style to use. +pygments_style = None + +# -- Options for HTML output ------------------------------------------------- + +# The theme to use for HTML and HTML Help pages. See the documentation for +# a list of builtin themes. +# +html_theme = 'nature' + +# Theme options are theme-specific and customize the look and feel of a theme +# further. For a list of options available for each theme, see the +# documentation. +# +# html_theme_options = {} + +# Add any paths that contain custom static files (such as style sheets) here, +# relative to this directory. They are copied after the builtin static files, +# so a file named "default.css" will overwrite the builtin "default.css". +html_static_path = ['_static'] + +# Custom sidebar templates, must be a dictionary that maps document names +# to template names. +# +# The default sidebars (for documents that don't match any pattern) are +# defined by theme itself. Builtin themes are using these templates by +# default: ``['localtoc.html', 'relations.html', 'sourcelink.html', +# 'searchbox.html']``. +# +# html_sidebars = {} + + +# -- Options for HTMLHelp output --------------------------------------------- + +# Output file base name for HTML help builder. +htmlhelp_basename = 'SAWremotedoc' + + +# -- Options for LaTeX output ------------------------------------------------ + +latex_elements = { + # The paper size ('letterpaper' or 'a4paper'). + # + # 'papersize': 'letterpaper', + + # The font size ('10pt', '11pt' or '12pt'). + # + # 'pointsize': '10pt', + + # Additional stuff for the LaTeX preamble. + # + # 'preamble': '', + + # Latex figure (float) alignment + # + # 'figure_align': 'htbp', +} + +# Grouping the document tree into LaTeX files. List of tuples +# (source start file, target name, title, +# author, documentclass [howto, manual, or own class]). +latex_documents = [ + (master_doc, 'SAWRemote.tex', 'SAW Remote API Documentation', + 'Galois, Inc.', 'manual'), +] + + +# -- Options for manual page output ------------------------------------------ + +# One entry per manual page. List of tuples +# (source start file, name, description, authors, manual section). +man_pages = [ + (master_doc, 'saw-remote-api', 'SAW Remote API Documentation', + [author], 1) +] + + +# -- Options for Texinfo output ---------------------------------------------- + +# Grouping the document tree into Texinfo files. List of tuples +# (source start file, target name, title, author, +# dir menu entry, description, category) +texinfo_documents = [ + (master_doc, 'SAWRemote', 'SAW Remote API Documentation', + author, 'SAW Remote API', 'One line description of project.', + 'Miscellaneous'), +] + + +# -- Options for Epub output ------------------------------------------------- + +# Bibliographic Dublin Core info. +epub_title = project + +# The unique identifier of the text. This can be a ISBN number +# or the project homepage. +# +# epub_identifier = '' + +# A unique identification for the text. +# +# epub_uid = '' + +# A list of files that should not be packed into the epub file. +epub_exclude_files = ['search.html'] + + +# -- Extension configuration ------------------------------------------------- \ No newline at end of file diff --git a/saw-remote-api/docs/index.rst b/saw-remote-api/docs/index.rst new file mode 100644 index 0000000000..b6ef398fa3 --- /dev/null +++ b/saw-remote-api/docs/index.rst @@ -0,0 +1,24 @@ +.. SAW Remote API documentation master file, created by + sphinx-quickstart on Mon Nov 23 15:56:11 2020. + You can adapt this file completely to your liking, but it should at least + contain the root `toctree` directive. + +SAW Remote API +============== + +.. toctree:: + :maxdepth: 3 + :caption: Contents: + + Protocol Overview + Cryptol Evaluation + SAW Verification + Errors + + +Indices and tables +================== + +* :ref:`genindex` +* :ref:`modindex` +* :ref:`search`