Skip to content

Latest commit

 

History

History
503 lines (376 loc) · 19.4 KB

CONTRIBUTING.md

File metadata and controls

503 lines (376 loc) · 19.4 KB

SAW development

This document explains our standards for developing SAW. Our goals are to have a development process that:

  • consistently yields reliable software artifacts,
  • quickly incorporates improvements and gets them into user hands, and
  • allows new contributors to have an immediate impact.

It describes our methods and practices for:

  • testing and continuous integration;
  • issue tracking;
  • organizing, branching, and merging this repository;
  • producing and publishing release artifacts; and
  • feature and release planning.

This is a living document that is not (and possibly cannot be) comprehensive. If something is missing or unclear, or if you have suggestions for improving our processes, please file an issue or open a pull request.

Building

See guidance in README.md for information on building SAW.

Testing

The core test suite for SAW consists of a collection of integration tests, in subdirectories of the intTest directory. A Cabal test suite called integration_tests is responsible for invoking these tests.

Dependency freezing

To ensure repeatable test results, our CI system uses cabal.project.freeze files to fix the version of all dependencies prior to building. It uses one of several version freezing files, each named cabal.GHC-<VER>.config, for GHC version <VER>.

We recommend building and testing using these files unless your explicit goal is to assess compatibility with different library versions. To do so, run the following before building or testing:

ln -s cabal.GHC-<VER>.config cabal.project.freeze

Running and Creating Tests

For more information on running and creating tests, see the README.md file in the intTests directory.

Other Tests in CI

Although individual developers typically run just the core integration tests, our CI system (GitHub Actions) runs several other tests on every pull request. These include ensuring that a variety of large proof developments, many for the s2n TLS library, continue to succeed. The scripts for running these tests are located in the s2nTests directory.

Issue tracking

We use the GitHub issue tracker in the saw-script repository to manage bug reports and other tickets. When filing an issue please search quickly to see if the same issue has already been reported. (There is no need to search exhaustively or spend a lot of time checking old issues, but please do make a quick check.) If feasible please label your issues. The available issue labels are documented below. This helps make sure the right people see them quickly.

Issue labels

The issue labels for saw-script are grouped by color into categories. Administrative labels use warm colors and technical labels use cool colors.

Issue labels should be used to reflect the current state of the issue. For complex issues, the label set should be updated as understanding changes and/or partial fixes are put in place. The primary purpose of labels is to improve search and discovery as issues are worked on; statistics and analysis (for which one would want to leave certain labels in place even when they no longer apply) is at most a secondary application. In principle, when closing a complex issue whose labeling has changed over time, it's nice to update the label set with all the labels that have been relevant; this improves discoverability for closed issues, which is useful not just for analytics but also for investigating regressions. However, we shouldn't assume this will get done.

If reopening an issue because the changes that fixed it needed to be reverted, or because it has regressed, check and update the label set.

The categories and their labels follow.

Primary issue properties (red)

  • breaking - marks changes that will break backwards compatibility. Use this label to help ensure that concerns relative to such changes (documentation, migration path, etc.) are attended to.

  • easy - marks issues that we expect to be easy to resolve. These are likely to be good starting points for new contributors.

  • maybe fixed - marks issues where there's some reason to suppose the issue might be resolved, but that requires further investigation or confirmation. If the fix is confirmed, please remove the label before closing the issue. For obvious reasons, generally should not be applied to new issues.

  • missing cryptol features - marks issues related to features in Cryptol that don't work in SAW.

  • needs administrative review - marks issues that need administrative (rather than purely technical) review, e.g. to assess relevance, priorities, or strategic planning. Should be removed once this review has happened and administrative questions have been answered.

  • needs design - marks issues that need (technical) design work to resolve. For example, something needs to be done but it isn't yet clear how to accomplish it, or it has interactions with other things that need to be clarified before work begins. Also should be used when we haven't yet established requirements. Should be removed once stakeholders have aligned on the needed plans.

  • needs test - issues for which we should add a regression test. In principle this label can be removed once there's a pull request that includes such a test (and re-added if that pull request is abandoned, the test backed out, etc.) or failing that when such a pull request is merged. Also in principle this should never appear on closed issues; if a test is needed it should be added before the issue is closed, or failing that a new issue should be added covering just the test. However, we shouldn't assume these updates will get done and in particular searching for closed issues with this label is not expected to be useful.

  • obsolete - marks issues that involve or depend on deprecated code such that they are not worth pursuing. For example, if there's a bug in a deprecated command such that it sometimes crashes, in general the correct response for anyone seeing the bug is to move away from the deprecated command and the bug itself isn't worth fixing. (This is not always the case; if it's not the case, don't use this label.) The issue should be left open until the deprecated code in question is ultimately removed; this makes it easier to find if/when someone else sees the problem.

  • priority - marks issues that are currently high priority for whatever reason.

  • regression - marks issues that describe regressions, that is, things that used to work but no longer do. If a previous (now closed) issue regresses and a new issue comes in documenting that, mark the new issue a regression and link it to the previous manifestation. If a previous (now closed) issue is found to have regressed without a new issue having been filed, it may make sense to reopen it rather than filing a new issue. In that case, when reopening the previous issue, mark it as a regression.

  • unsoundness - marks issues that can lead to unsoundness or incorrect verifications. Please be sure before applying this label, but please also don't hesitate to use it when it's warranted.

  • usability - marks issues that get in the way of using SAW effectively.

  • wontfix - marks issues that have not been fixed and aren't going to be fixed. This should only be applied to closed issues (that is, if applying it, apply it when the issue is closed) and should only be used for issues that are still relevant; that is, the issue is still valid but isn't worth fixing for whatever reason. Issues that aren't valid, turned out not to be bugs, stopped happening on their own, were in code that was later deleted, etc. should not use this label. The purpose is to be able to retrieve these issues again from the otherwise large and poorly-indexed body of closed issues.

Secondary issue properties (black)

  • better-in-python - marks issues that can be resolved by switching to the Python-based interface.

  • better-when-documented - marks issues whose root causes include missing or wrong documentation. Use this for any issue where that's true, regardless of whether it is primarily a documentation issue or not. Do not close the issue until the documentation issues have been handled.

  • documentation debt - marks issues that involve previously deferred, unhandled, postponed, or unfinished documentation tasks; technical debt in documentation.

  • performance - marks issues that affect performance or include performance problems.

  • tech debt - marks issues that involve previously incurred technical debt.

The distinction between primary and secondary issue priorities is specifically which ones we want to have stand out when looking at the label set.

Type of issue (orange)

  • type: bug - marks issues that report unexpected/unwanted behavior or other problems.

  • type: enhancement - marks issues that describe improvements to existing capabilities. Issues describing new capabilities are feature requests.

  • type: feature request - marks issues that describe desired new capabilities. Issues describing improvements to existing capabilities are enhancements.

  • type: question - marks issues that are primarily asking questions. The difference between a question and a more generic support request is that a question is resolved once an answer's been found. Questions will sometimes progress to more general support requests. Sometimes they will also be of the form "is this behavior a bug?" in which case the answer is often "yes" and the issue then becomes a bug report. Update the type label when these things happen.

  • type: support - marks issues that ask for help or support. Not infrequently these will progress to be bug reports; at that point change the type label.

These labels have a common text prefix so they sort together. Issues should ordinarily have exactly one type label.

Issue state (yellow)

We are currently not using issue state labels.

Technical topics (pale green)

In general apply these if they appear relevant; the purpose of these labels is to attract the attention of people who know about the topics in question, and it's better to have the occasional false alarm than to miss things.

  • topics: bitfields - marks issues that relate to SAW's support for bitfields.

  • topics: error handling - marks issues that involve the way SAW responds to an error condition. It is common, but not universal, for issues that involve error handling to also involve the messages printed as a result; use the topics: error messages label as well for these.

  • topics: error messages - marks issues that involve the messages SAW produces when an error occurs. (Use this label for warning and notice messages as well, if applicable.)

  • topics: memory model - marks issues related to the LLVM and/or Crucible model of pointers and memory blocks.

  • topics: saw-core names - marks issues related to the URI-based saw-core names.

These labels have a common text prefix so they sort together. Use all that apply.

Artefact type (dark turquoise)

  • documentation - marks issues involving documentation. Don't forget to also select an issue type (typically bug, but sometimes enhancement or feature request). The better-when-documented label is for issues where someone ran into problems because of bad or missing documentation; the documentation debt label is for issues where necessary documentation changes got left off or forgotten in the past. None of these are mutually exclusive.

  • test assets - marks issues involving test programs and/or other test assets. This includes, for example, bugs in test programs, and test programs that don't behave deterministically. Use tooling: test infrastructure to label bugs in test infrastructure. Use the CI label for issues involving the CI infrastructure, including running tests in the CI system.

Project tooling (lime green)

  • tooling: build system - issues involving SAW's build system.

  • tooling: CI - issues involving the CI/CD scripts or processes. For test or testing problems, use this label only if the CI mechanisms are involved; otherwise use tooling: test infrastructure for infrastructure issues and test assets problems with individual tests.

  • tooling: test infrastructure - issues involving test infrastructure, test execution, or making SAW more testable. Use test assets instead for problems with individual tests.

  • tooling: release engineering - issues involving releases, release processes, making releases, or other release engineering concerns. This includes processes related to snapshots and nightlies.

Project subsystems (cornflower blue)

  • subsystem: crucible-jvm - issues related to Java verification using the crucible-jvm tooling.

  • subsystem: crucible-llvm - issues related to LLVM bitcode verification using the crucible-llvm tooling.

  • subsystem: crucible-mir - issues related to Rust verification using the crucible-mir and mir-json tooling.

  • subsystem: crucible-mir-comp - issues related to Rust verification and composition with crucible-mir-comp or crux-mir-comp.

  • subsystem: cryptol-saw-core - issues related to the Cryptol-to-saw-core translation in the cryptol-saw-core package.

  • subsystem: hardware - issues related to verification of hardware.

  • subsystem: heapster - issues related to memory verification using Heapster.

  • subsystem: MRSolver - issues related to the Mr. Solver monadic-recursive solver in Heapster.

  • subsystem: saw-core - issues related to the saw-core representation or the saw-core subsystem.

  • subsystem: saw-core-coq - issues related to converting saw-core to Gallina for use with the Coq/Rocq theorem prover.

  • subsystem: saw-python - issues related to the Python bindings for the RPC SAW server.

  • subsystem: saw-remote-api - issues related to the SAW server and its RPC bindings.

  • subsystem: x86 - issues related to verifying x86 binaries via Macaw.

  • subproject - issues involving one of the various subprojects SAW depends on. Note that this intentionally does not have the "subsystem:" prefix as the string "subsystem: subproject" is confusing.

Pull request labels

On GitHub pull requests use the same label set as issues. The labels defined in the previous section should be used only for issues, not pull requests. There is no need to mirror the labels on an issue into a pull request meant to address it. (However, if making a pull request without an issue, then please do apply any relevant issue labels; this improves later discoverability.)

Also please remember to add any pull request properties that apply.

There is one category of pull request labels.

Pull request properties

  • PR: dependency bump - use this to mark pull requests that adjust dependency constraints. (Other than via git submodules; use PR: submodule bump for those.)

  • PR: keep updated - add this label to ask Mergify to merge the trunk into your pull request branch for you when the trunk updates. Because of the assorted risks associated with more than one party applying changes to the same git branch, this should generally be used only for branches that are not currently under active development.

  • PR: ready to merge - this label asks Mergify to merge your pull request as soon as there's both an approval and a successful CI run. We are no longer using this Mergify feature and expect to remove support for it in the near future.

  • PR: submodule bump - use this to mark pull requests that change git submodule references. (Changes that involve other version bumps should use PR: dependency bump.)

Adding labels

In order to keep this documentation up to date, if proposing new labels (or changes to the existing labels), please include a pull request that updates this file.

Repository organization and practices

The top-level repository directories are:

  • src - Source code for the SAWScript interpreter library.

  • saw - Source for the saw executable interpreter for SAWScript.

  • doc - A manual and tutorials for SAWScript.

  • examples - Various examples of using SAWScript.

  • intTests - The central test suite for SAWScript.

  • s2nTests - Additional tests for SAWScript, confirming that verifications involving the s2n library continue to work.

  • saw-remote-api - Source for a server that provides a remote API to SAW based on JSON-RPC, and a Python client for that API.

  • saw-core - Source code for the SAWCore intermediate language used within SAW.

  • saw-core-aig - A library for translating SAWCore to And-Inverter Graphs.

  • saw-core-coq - A library for translating SAWCore to Coq's Gallina language.

  • saw-core-sbv - A library for translating SAWCore predicates to SMT queries using the SBV library.

  • saw-core-what4 - A library for translating SAWCore predicates to solver queries using the What4 library.

  • cryptol-saw-core - A library for translating Cryptol code into SAWCore.

  • rme - A library implementing a Reed-Muller Expansion datatype for representing Boolean formulas.

  • deps - A location for other dependencies included as Git submodules.

  • crux-mir-comp - A version of Crux that can perform modular analysis of Rust code using a form of contracts.

Branching and merging

Within the GaloisInc/saw-script repository, we use a variation on the git-flow model for branches and merging with they key difference that our master (rather than develop) branch serves as the cutting edge development branch, and our release-* (rather than master) branches are where only pristine, tagged releases are committed.

In short:

  • All changes should be developed on branches and then merged into master when completed.

  • When we reach a feature freeze for a release, we create a new branch prefixed with release-, for example release-0.3. When the release is made, we merge those changes back into master and tag the HEAD of the release branch.

  • If a critical bug emerges in already-released software, we create a branch off of the relevant release branch. When the hotfix is complete, we merge those changes back into master and add a tag on the release branch.

  • Merging PRs requires a review from at least one other committer, and requires successful completion of a CI workflow including a wide variety of tests. Branches must be up-to-date with master before merging.

  • A PR is normally merged by the author of the PR following a review acceptance and valid CI completion. This allows the author to determine when they are fully ready for the merge to be performed. We suggest the use of Mergify (see below) although the merge can also be performed manually, and if you as an author do not have merge permissions, please indicate this in a comment when asking for reviews.

Using Mergify

Due to the requirement that PRs pass CI and code review and are up-to-date with master before merging, it can be time-consuming to manually manage a large queue of changes to be merged. To help reduce this burden we use the Mergify tool. It automatically queues up CI runs and merges PRs once CI and code review have succeeded. To indicate that a PR is ready for Mergify to merge, add the ready-to-merge label.

Copyright and License

Copyright 2011-2021 Galois, Inc.

Licensed under the BSD 3-Clause License; you may not use this work except in compliance with the License. A copy of the License is included in the LICENSE file.