Aggregated RISCV64 + CI work #8
Draft
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shed@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
A lot of hacks Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shed@data61.csiro.au>
Use -a armv7 or -a rv64 to specify the architecture. Use tab as indents in chronos/emitter.py Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
The parser is used to generate RISC-V input file for Chronos. It is based on the Armv7 version. The commit is a checkpoint for on-going work. Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Note that the code is really simple. Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Yanyan Shen <yanyan.shen@data61.csiro.au>
Signed-off-by: Zoltan Kocsis <zoltan.kocsis@data61.csiro.au>
Signed-off-by: Zoltan Kocsis <zoltan.kocsis@data61.csiro.au>
Previously, `start_prove_task_with_solver` passed its `model` argument around directly. The correctness of this behavior depends upon the implementation details of `solver.Solver.check_model_iteration` to ensure that such a model is not updated directly. We change the behavior, so that we pass separate copies of the `model` instead, which results in correct behavior independly of `check_model_iteration`. Signed-off-by: Zoltan Kocsis <zoltan.kocsis@data61.csiro.au>
Signed-off-by: Zoltan Kocsis <zoltan.kocsis@data61.csiro.au>
Signed-off-by: Zoltan Kocsis <zoltan.kocsis@data61.csiro.au>
This adds a configuration for calculating bounds on stack usage for RISC-V kernels compiled with a subset of `-O2` optimisation (with `-fno-partial-inlining -fno-ipa-cp -fno-ipa-sra`). Co-authored-by: Zoltan Kocsis <zoltan.kocsis@data61.csiro.au> Signed-off-by: Zoltan Kocsis <zoltan.kocsis@data61.csiro.au> Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
We implement a shell script that performs end-to-end binary verification of seL4, including setting up HOL4 and the required SMT solvers. Run using `./seL4-example/run_proofs_riscv_mcs.sh`. Set USE_SONOLAR to true to use the SONOLAR SMT solver (faster proofs, but requires a license for commercial purposes). Signed-off-by: Zoltan Kocsis <koc034@nascar-ev.nexus.csiro.au>
We add two template solverlists that our scripts can use to generate solverlists appropriate for `seL4-example`. Signed-off-by: Zoltan Kocsis <zoltan.kocsis@data61.csiro.au>
The functionality of some of the removed scripts will be replaced in subsequent commits. Signed-off-by: Matthew Brecknell <matt@kry10.com>
Signed-off-by: Matthew Brecknell <matt@kry10.com>
Signed-off-by: Matthew Brecknell <matt@kry10.com>
Signed-off-by: Matthew Brecknell <matt@kry10.com>
If set, search for the solverlist from the directory given by the `GRAPH_REFINE_SOLVERLIST_DIR` environment variable. If not set, search from the current directory (to match previous behaviour). Signed-off-by: Matthew Brecknell <matt@kry10.com>
Allow version information to be passed via the environment, if graph-refine is run from outside a git checkout. Signed-off-by: Matthew Brecknell <matt@kry10.com>
Add `GRAPH_REFINE_SMT2_DIR` environment variable to specify where STM problems should be written. If not specified, defaults to a subdirectory of the target directory. Signed-off-by: Matthew Brecknell <matt@kry10.com>
Add scripts supporting various methods of obtaining and running the decompiler. Also package the decompiler as a Nix derivation, and allow building a Docker image. Signed-off-by: Matthew Brecknell <matt@kry10.com>
Package graph-refine with a solver configuration as a Nix derivation, and also allow building a Docker image. Signed-off-by: Matthew Brecknell <matt@kry10.com>
Add a GitHub workflow that builds Docker images for the decompiler and graph-refine. Signed-off-by: Matthew Brecknell <matt@kry10.com>
Provides a nix-shell environment containing the tools needed to run graph-refine on the command-line, including a solver configuration. Signed-off-by: Matthew Brecknell <matt@kry10.com>
Supports ARM and non-MCS -O2 builds. Also allows passing `L4V_ARCH` via the environment, for better integration with seL4-example/Makefile. Signed-off-by: Matthew Brecknell <matt@kry10.com>
- Remove some obsolete code. - Add some missing dependencies. - Use the decompiler installed by setup-decompiler.py. - Add a convenience target for GitHub CI. Signed-off-by: Matthew Brecknell <matt@kry10.com>
We will use this to uniquely identify graph-refine jobs in CI. Signed-off-by: Matthew Brecknell <matt@kry10.com>
We will use this to drive parallel execution of graph-refine. Signed-off-by: Matthew Brecknell <matt@kry10.com>
The `ci-submit` script is intended to run in GitHub CI. It sends a graph-refine job over SSH to a host that is configured to receive it using `ci-receive`. Signed-off-by: Matthew Brecknell <matt@kry10.com>
Add a simple graph-refine job queue that runs jobs serially, but runs functions within a job in parallel. In the Nix/Docker build, add support for dispatching to different graph-refine versions for different architectures. This is a temporary measure while the ARM and RISCV64 branches are not yet integrated. Also modify the `build` workflow to build graph-refine Docker images including both ARM and RISCV64 versions. Signed-off-by: Matthew Brecknell <matt@kry10.com>
Assumes the same work directory layout as the worker, and a web server serving the work directory as a static website. Signed-off-by: Matthew Brecknell <matt@kry10.com>
This is a significant overhaul of the support scripts that can be used to run various stages of the binary verification (BV) pipeline, especially for the seL4 kernel. For both continuous integration (CI) and interactive use, we support running all of the "back end" of BV (parts other than the l4v Isabelle proofs) using either Nix or containers. In particular, for running BV in CI, the only dependencies are `bash`, and either Docker or Podman (including rootless). Major improvements: - Add Nix and Docker support for running the remaining parts of the BV "back end" for seL4. We combine decompilation with stack usage analysis, and optionally with compilation. This is designed to work with the `export-kernel-builds.py` script added to l4v. - Combine stack bounds analysis and other graph-refine input preprocessing, so that we only parse graph-lang and ELF dumps once. Also rework RISCV64 fixups to be more precise. - Add a GitHub workflow that performs decompilation and stack usage analysis. It is intended to be triggered by an l4v proof workflow run, which should have already performed kernel compilation and C graph-lang export. This workflow can also be manually triggered. At its conclusion, this workflow submits a job to a custom back end which performs the final stage of binary verification (graph refinement). Minor improvements to the decompiler support scripts: - Support podman. - Show progress when installing a decompiler using setup-decompiler.py. Minor improvements to Nix scripts: - Use qualified references, to avoid namespace pollution. - Use pinned versions of components. - Refactor some utility functions. - Fix Docker image entry points, for compatibility with podman. - Restrict the use of sonolar to its supported platform (x86_64-linux). - Remove L4V_ARCH dispatch mechanism. This never worked properly, and will be obsolete as soon as branches are integrated. Signed-off-by: Matthew Brecknell <matt@kry10.com>
This can be used to expose results generated by the graph-refine backend, using a simple static web server configuration. The backend generates and updates JSON data files as it works, and the web view loads them from the browser using JavaScript.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This pull request aggregates a lot of work that has not yet been merged to the main branch, including:
As we go through clean-up and review, we might split this into multiple pull requests.