diff --git a/.github/workflows/deploy.yml b/.github/workflows/deploy.yml index 3335de128..0c61c4033 100644 --- a/.github/workflows/deploy.yml +++ b/.github/workflows/deploy.yml @@ -38,6 +38,7 @@ jobs: nix-shell --run " dune build @doc && + rm -rf doc/api && mv _build/default/_doc/_html doc/api && BISECT_FILE=\$(pwd)/bisect dune runtest --force --instrument-with bisect_ppx && bisect-ppx-report html -o doc/coverage && diff --git a/HACKING.md b/HACKING.md new file mode 100644 index 000000000..da9b32bad --- /dev/null +++ b/HACKING.md @@ -0,0 +1,103 @@ +# Hacking on Owi + +## Development setup + +To get a proper development setup: + +```shell-session +$ git clone git@github.com:OCamlPro/owi.git +$ cd owi +$ opam install . --deps-only --with-test --with-doc --with-dev-setup +$ git submodule update --init --recursive +$ dune build @all +``` + +## Coding Guidelines + +### The `prelude` library + +We use the [`prelude`](https://forge.kumikode.org/kumikode/prelude) library to **hide dangerous functions** from the standard library. +It is automatically opened in the whole project. +More than dangerous functions, this library also hide some modules for which better alternatives exists. +For instance, all system interactions are done using [`Bos`](https://erratique.ch/software/bos/doc/) and all the formatting is done with [`Fmt`](https://erratique.ch/software/fmt/doc/). + +### Printing + +Read the [Logs basics](https://erratique.ch/software/logs/doc/Logs/index.html#basics) and in particular, the [usage conventions](https://erratique.ch/software/logs/doc/Logs/index.html#usage). + +## Documentation + +### API + +You can build the documentation with: + +```shell-session +$ dune build @doc +$ xdg-open _build/default/doc/index.html +``` + +### User Manual + +```shell-session +$ cd ./doc +$ mdbook serve +``` + +## Testing + +### Unit tests + +Tests are mostly written using [Cram Tests]. +The ones that are integrated into documentation are using [MDX]. +You can run them as follow: + +```shell-session +$ dune runtest +``` + +If you made some changes and the output of some tests is changing, the diff will be displayed. +If you want to automatically accept the diff as being the new expected output, you can run: + +```shell-session +$ dune promote +``` + +### Code coverage + +You can generate the code coverage report with: + +```shell-session +BISECT_FILE=$(pwd)/bisect dune runtest --force --instrument-with bisect_ppx +bisect-ppx-report html -o _coverage +xdg-open _coverage/index.html +``` + +### Fuzzing + +See [test/fuzz]. + +[Cram Tests]: https://dune.readthedocs.io/en/latest/reference/cram.html +[MDX]: https://github.com/realworldocaml/mdx +[test/fuzz]: ./test/fuzz + +## Diagnostic + +### Profiling + +#### Landmarks + +```shell-session +OCAML_LANDMARKS=on dune exec --instrument-with landmarks --profile release -- owi run test/run/binary_loop.wasm +``` + +See the discussion in [#871] to understand landmarks limitations in Owi. + +### Benchmarking + +#### Test-comp + +See [Symbocalypse]. + +[#871]: https://github.com/OCamlPro/owi/pull/871 +[Symbocalypse]: https://github.com/OCamlPro/symbocalypse + diff --git a/README.md b/README.md index 012fbe749..2addbb796 100644 --- a/README.md +++ b/README.md @@ -9,7 +9,7 @@

-[![build-badge]][build status] [![coverage-badge]][code coverage] [📘 documentation] [💬 zulip] +[![build-badge]][build status] [![coverage-badge]][code coverage]
@@ -19,12 +19,98 @@ ### Key resources -
- 📘 Documentation → Read the documentation
- 💬 Zulip community → Ask questions and collaborate
-
+- 📘 [User Manual](https://ocamlpro.github.io/owi) + - [Install Owi](https://ocamlpro.github.io/owi/installation.html) + - [Quickstart](https://ocamlpro.github.io/owi/symex/quickstart.html) +- 💬 [Zulip community](https://owi.zulipchat.com) +- [List of supported Wasm proposals](https://webassembly.org/features) +- [Changelog](./CHANGES.md) +- [Hacking on Owi](./HACKING.md) + +### Explanations + +
+ + List of talks + +- [september 2023]: [ICFP OCaml track] @ The Westin Seattle - Seattle +- [october 2023]: Wasm Research Day organized by the [WebAssembly Research Center] @ Google - Munich +- april 2024: [OUPS (OCaml UserS in Paris)] @ Sorbonne Université - Paris +- [november 2024]: [LVP working group] day of the [GdR GPL] @ Université Paris-Cité - Paris +- [december 2024]: Léo Andrès' PhD defense @ Université Paris-Saclay - Gif-sur-Yvette +- january 2025: [JFLA 2025] @ Domaine de Roiffé - Roiffé +- [february 2025]: [Wasm Research Day 2025] (remote) @ Fastly - San Francisco +- february 2025: [PPS Seminar] @ Université Paris-Cité - Paris +- may 2025: [15th MirageOS hack retreat] @ Priscilla Queen of the Medina - Marrakech +- june 2025: [\ 2025] @ Faculty of Mathematics and Physics, Charles University - Prague +- june 2025: [Dagstuhl Seminar 25241 - Utilising and Scaling the WebAssembly Semantics] @ Leibniz-Zentrum für Informatik - Dagstuhl +- october 2025: [Wasm Research Day October 2025] @ Google - Munich + +
+ +
+ + List of publications + +- [Owi: Performant Parallel Symbolic Execution Made Easy, an Application to WebAssembly], 2024 +- [Exécution symbolique pour tous ou Compilation d'OCaml vers WebAssembly], 2024 +- [Cross-Language Symbolic Runtime Annotation Checking], 2025 +- [Exécution symbolique pour la génération de tests ciblant des labels], 2026 + +[Cross-Language Symbolic Runtime Annotation Checking]: https://inria.hal.science/hal-04798756/file/cross_language_symbolic_runtime_annotation_checking.pdf +[Exécution symbolique pour la génération de tests ciblant des labels]: https://hal.science/hal-05427949 +[Exécution symbolique pour tous ou Compilation d'OCaml vers WebAssembly]: https://fs.zapashcanon.fr/pdf/manuscrit_these_leo_andres.pdf +[Owi: Performant Parallel Symbolic Execution Made Easy, an Application to WebAssembly]: https://hal.science/hal-04627413 + +[september 2023]: https://youtu.be/IM76cMP3Eqo +[october 2023]: https://youtu.be/os_pknmiqmU +[november 2024]: https://groupes.renater.fr/wiki/lvp/public/journee_lvp_novembre2024 +[december 2024]: https://fs.zapashcanon.fr/mp4/phd_defense.mp4 +[february 2025]: https://youtu.be/x6V-NJ9agjg + +[15th MirageOS hack retreat]: https://retreat.mirage.io +[Dagstuhl Seminar 25241 - Utilising and Scaling the WebAssembly Semantics]: https://www.dagstuhl.de/seminars/seminar-calendar/seminar-details/25241 +[JFLA 2025]: https://jfla.inria.fr/jfla2025.html +[GdR GPL]: https://gdr-gpl.cnrs.fr/ +[ICFP OCaml track]: https://icfp23.sigplan.org/home/ocaml-2023 +[LVP working group]: https://gdrgpl.myxwiki.org/xwiki/bin/view/Main/GTs/GT%20Langages%20et%20v%C3%A9rification%20de%20programmes%20(LVP) +[OUPS (OCaml UserS in Paris)]: https://oups.frama.io +[PPS Seminar]: https://www.irif.fr/seminaires/pps/index +[\ 2025]: https://2025.programming-conference.org +[WebAssembly Research Center]: https://www.cs.cmu.edu/wrc +[Wasm Research Day 2025]: https://www.cs.cmu.edu/~wasm/wasm-research-day-2025.html +[Wasm Research Day October 2025]: https://www.cs.cmu.edu/~wasm/wasm-research-day-2025b.html + +
+ +### References + +- TODO: man pages (see [here](https://ocamlpro.github.io/owi/manpages/owi.html#owi) for now) +- TODO: high-level API for each language +- TODO: Wasm API + +### About + +#### Fundings & Sponsors + +This project was partly funded through the [NGI0 Core] Fund, a fund established by [NLnet] with financial support from the European Commission's [Next Generation Internet] program : + +1. [First grant]. +2. [Second grant]. + +[Next Generation Internet]: https://ngi.eu +[NGI0 Core]: https://nlnet.nl/core +[NLnet]: https://nlnet.nl +[First grant]: https://nlnet.nl/project/OWI +[Second grant]: https://nlnet.nl/project/OWI-2/ + +#### Spelling and pronunciation + +Although the name Owi comes from an acronym (OCaml WebAssembly Interpreter), it must be written as a proper noun and only the first letter must be capitalized. It is possible to write the name in full lowercase when referring to the opam package or to the name of the binary. + +The reason we chose this spelling rather than the fully capitalized version is that in French, Owi is pronounced [o’wi(ʃ)] which sounds like "Oh oui !" which means "Oh yes!". Thus it should be pronounced this way and not by spelling the three letters it is made of. -### License +#### License Owi Copyright (C) 2021-2024 OCamlPro @@ -56,5 +142,3 @@ Some code has been taken from the E-ACSL plugin of Frama-C. It is licensed under [build status]: https://github.com/ocamlpro/owi/actions [coverage-badge]: https://raw.githubusercontent.com/ocamlpro/owi/gh-pages/coverage/badge.svg [code coverage]: https://ocamlpro.github.io/owi/coverage -[📘 documentation]: https://ocamlpro.github.io/owi -[💬 zulip]: https://owi.zulipchat.com diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index ef6796765..d811244a1 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -2,13 +2,8 @@ [Home](index.md) [Installation](installation.md) -[Supported Wasm proposals](proposals.md) [Comparison with other tools](comparison.md) - -# Symbolic Execution Engine - -- [Symbolic Execution 101](symex/symbolic-execution-101.md) -- [Quickstart](symex/quickstart.md) +[Quickstart](symex/quickstart.md) # Bug-Finding, Testing & Pen-testing @@ -32,12 +27,6 @@ - [How to Speed it Up](sap/optimizations.md) - [Comparison to Rosette, Prolog, etc.](sap/comparison.md) -# Going Further - -- [Talks and Papers](further/talks-papers.md) -- [Commands and Options](further/commands.md) -- [API: Symbols and Helpers](further/api.md) - # WebAssembly Toolkit - [Overview](wasm-toolkit/overview.md) - [Comparison with Other Tools](wasm-toolkit/comparison.md) @@ -65,18 +54,3 @@ - [Overview](ocaml-api/overview.md) - [How to Define Custom Functions](ocaml-api/custom-functions.md) - [Generated API Documentation](ocaml-api/odoc.md) - -# Hacking -- [Development Setup](hacking/setup.md) -- [Coding Guidelines](hacking/guidelines.md) -- [Documentation](hacking/doc.md) -- [Testing](hacking/testing.md) -- [Benchmarking](hacking/benchmarking.md) - -# About -- [History of Owi](about/history.md) -- [Authors and Contributors](about/authors.md) -- [License](about/license.md) -- [Funding](about/fundings.md) -- [Changelog](about/changelog.md) -- [Projects and People Using Owi](about/users.md) diff --git a/doc/src/about/authors.md b/doc/src/about/authors.md deleted file mode 100644 index 103cd7bab..000000000 --- a/doc/src/about/authors.md +++ /dev/null @@ -1 +0,0 @@ -# Authors and Contributors diff --git a/doc/src/about/changelog.md b/doc/src/about/changelog.md deleted file mode 100644 index 6355bdffc..000000000 --- a/doc/src/about/changelog.md +++ /dev/null @@ -1,5 +0,0 @@ -# Changelog - -See [CHANGELOG]. - -[CHANGELOG]: https://github.com/OCamlPro/owi/blob/main/CHANGES.md diff --git a/doc/src/about/fundings.md b/doc/src/about/fundings.md deleted file mode 100644 index f4a164311..000000000 --- a/doc/src/about/fundings.md +++ /dev/null @@ -1,8 +0,0 @@ -# Funding - -This project was partly funded through the [NGI0 Core] Fund, a fund established by [NLnet] with financial support from the European Commission's [Next Generation Internet] programme. See [Owi project on NLnet]. - -[Next Generation Internet]: https://ngi.eu -[NGI0 Core]: https://nlnet.nl/core -[NLnet]: https://nlnet.nl -[Owi project on NLnet]: https://nlnet.nl/project/OWI diff --git a/doc/src/about/history.md b/doc/src/about/history.md deleted file mode 100644 index 24a319110..000000000 --- a/doc/src/about/history.md +++ /dev/null @@ -1,8 +0,0 @@ -# History of Owi - -### Spelling and pronunciation - -Although the name Owi comes from an acronym (OCaml WebAssembly Interpreter), it must be written as a proper noun and only the first letter must be capitalized. It is possible to write the name in full lowercase when referring to the opam package or to the name of the binary. - -The reason we chose this spelling rather than the fully capitalized version is that in French, Owi is pronounced [o’wi(ʃ)] which sounds like "Oh oui !" which means "Oh yes!". Thus it should be pronounced this way and not by spelling the three letters it is made of. - diff --git a/doc/src/about/license.md b/doc/src/about/license.md deleted file mode 100644 index 165252d0b..000000000 --- a/doc/src/about/license.md +++ /dev/null @@ -1,27 +0,0 @@ -# License - - Owi - Copyright (C) 2021-2024 OCamlPro - - This program is free software: you can redistribute it and/or modify - it under the terms of the GNU Affero General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - This program is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU Affero General Public License for more details. - - You should have received a copy of the GNU Affero General Public License - along with this program. If not, see . - -See [LICENSE]. - -A few files have been taken from the WebAssembly reference interpreter. They are licensed under the Apache License 2.0 and have a different copyright which is stated in the header of the files. - -Some code has been taken from the `base` library from Jane Street. It is licensed under the MIT License and have a different copyright which is stated in the header of the files. - -Some code has been taken from the E-ACSL plugin of Frama-C. It is licensed under the GNU Lesser General Public License 2.1 and have a different copyright which is stated in the header of the files. - -[LICENSE]: https://github.com/OCamlPro/owi/blob/main/LICENSE.md diff --git a/doc/src/about/users.md b/doc/src/about/users.md deleted file mode 100644 index 328a8ccbd..000000000 --- a/doc/src/about/users.md +++ /dev/null @@ -1 +0,0 @@ -# Projects and People Using Owi diff --git a/doc/src/further/api.md b/doc/src/further/api.md deleted file mode 100644 index c3694b7cd..000000000 --- a/doc/src/further/api.md +++ /dev/null @@ -1 +0,0 @@ -# API: Symbols and Helpers diff --git a/doc/src/further/commands.md b/doc/src/further/commands.md deleted file mode 100644 index 41152bfac..000000000 --- a/doc/src/further/commands.md +++ /dev/null @@ -1 +0,0 @@ -# Commands and Options diff --git a/doc/src/further/talks-papers.md b/doc/src/further/talks-papers.md deleted file mode 100644 index aa08f59fd..000000000 --- a/doc/src/further/talks-papers.md +++ /dev/null @@ -1,45 +0,0 @@ -# Talks and Papers - -## Publications - -- [Owi: Performant Parallel Symbolic Execution Made Easy, an Application to WebAssembly], 2024 -- [Exécution symbolique pour tous ou Compilation d'OCaml vers WebAssembly], 2024 -- [Cross-Language Symbolic Runtime Annotation Checking], 2025 - -## Talks - -- [september 2023]: [ICFP OCaml track] @ The Westin Seattle - Seattle -- [october 2023]: Wasm Research Day organized by the [WebAssembly Research Center] @ Google - Munich -- april 2024: [OUPS (OCaml UserS in Paris)] @ Sorbonne Université - Paris -- [november 2024]: [LVP working group] day of the [GdR GPL] @ Université Paris-Cité - Paris -- [december 2024]: Léo Andrès' PhD defense @ Université Paris-Saclay - Gif-sur-Yvette -- january 2025: [JFLA 2025] @ Domaine de Roiffé - Roiffé -- [february 2025]: [Wasm Research Day 2025] (remote) @ Fastly - San Francisco -- february 2025: [PPS Seminar] @ Université Paris-Cité - Paris -- may 2025: [15th MirageOS hack retreat] @ Priscilla Queen of the Medina - Marrakech -- june 2025: [\ 2025] @ Faculty of Mathematics and Physics, Charles University - Prague -- june 2025: [Dagstuhl Seminar 25241 - Utilising and Scaling the WebAssembly Semantics] @ Leibniz-Zentrum für Informatik - Dagstuhl -- october 2025: [Wasm Research Day October 2025] @ Google - Munich - -[Cross-Language Symbolic Runtime Annotation Checking]: https://inria.hal.science/hal-04798756/file/cross_language_symbolic_runtime_annotation_checking.pdf -[Exécution symbolique pour tous ou Compilation d'OCaml vers WebAssembly]: https://fs.zapashcanon.fr/pdf/manuscrit_these_leo_andres.pdf -[Owi: Performant Parallel Symbolic Execution Made Easy, an Application to WebAssembly]: https://hal.science/hal-04627413 - -[september 2023]: https://youtu.be/IM76cMP3Eqo -[october 2023]: https://youtu.be/os_pknmiqmU -[november 2024]: https://groupes.renater.fr/wiki/lvp/public/journee_lvp_novembre2024 -[december 2024]: https://fs.zapashcanon.fr/mp4/phd_defense.mp4 -[february 2025]: https://youtu.be/x6V-NJ9agjg - -[15th MirageOS hack retreat]: https://retreat.mirage.io -[Dagstuhl Seminar 25241 - Utilising and Scaling the WebAssembly Semantics]: https://www.dagstuhl.de/seminars/seminar-calendar/seminar-details/25241 -[JFLA 2025]: https://jfla.inria.fr/jfla2025.html -[GdR GPL]: https://gdr-gpl.cnrs.fr/ -[ICFP OCaml track]: https://icfp23.sigplan.org/home/ocaml-2023 -[LVP working group]: https://gdrgpl.myxwiki.org/xwiki/bin/view/Main/GTs/GT%20Langages%20et%20v%C3%A9rification%20de%20programmes%20(LVP) -[OUPS (OCaml UserS in Paris)]: https://oups.frama.io -[PPS Seminar]: https://www.irif.fr/seminaires/pps/index -[\ 2025]: https://2025.programming-conference.org -[WebAssembly Research Center]: https://www.cs.cmu.edu/wrc -[Wasm Research Day 2025]: https://www.cs.cmu.edu/~wasm/wasm-research-day-2025.html -[Wasm Research Day October 2025]: https://www.cs.cmu.edu/~wasm/wasm-research-day-2025b.html diff --git a/doc/src/hacking/benchmarking.md b/doc/src/hacking/benchmarking.md deleted file mode 100644 index 0d7e06392..000000000 --- a/doc/src/hacking/benchmarking.md +++ /dev/null @@ -1,16 +0,0 @@ -# Benchmarking - -## Landmarks - -```shell-session -OCAML_LANDMARKS=on dune exec --instrument-with landmarks --profile release -- owi run test/run/binary_loop.wasm -``` - -See the discussion in [#871] to understand landmarks limitations in Owi. - -## Test-comp - -See [Symbocalypse]. - -[#871]: https://github.com/OCamlPro/owi/pull/871 -[Symbocalypse]: https://github.com/OCamlPro/symbocalypse diff --git a/doc/src/hacking/doc.md b/doc/src/hacking/doc.md deleted file mode 100644 index 9e94c4c43..000000000 --- a/doc/src/hacking/doc.md +++ /dev/null @@ -1,17 +0,0 @@ -# Documentation - -## API - -You can build the documentation with: - -```shell-session -$ dune build @doc -$ xdg-open _build/default/doc/index.html -``` - -## Full documentation - -```shell-session -$ cd ./doc -$ mdbook serve -``` diff --git a/doc/src/hacking/guidelines.md b/doc/src/hacking/guidelines.md deleted file mode 100644 index d9d653aa8..000000000 --- a/doc/src/hacking/guidelines.md +++ /dev/null @@ -1,12 +0,0 @@ -# Coding Guidelines - -## The `prelude` library - -We use the [`prelude`](https://git.zapashcanon.fr/zapashcanon/prelude) library to **hide dangerous functions** from the standard library. -It is automatically opened in the whole project. -More than dangerous functions, this library also hide some modules for which better alternatives exists. -For instance, all system interactions are done using [`Bos`](https://erratique.ch/software/bos/doc/) and all the formatting is done with [`Fmt`](https://erratique.ch/software/fmt/doc/). - -## Printing - -Read the [Logs basics](https://erratique.ch/software/logs/doc/Logs/index.html#basics) and in particular, the [usage conventions](https://erratique.ch/software/logs/doc/Logs/index.html#usage). diff --git a/doc/src/hacking/setup.md b/doc/src/hacking/setup.md deleted file mode 100644 index 39a568fbb..000000000 --- a/doc/src/hacking/setup.md +++ /dev/null @@ -1,11 +0,0 @@ -# Development Setup - -To get a proper development setup: - -```shell-session -$ git clone git@github.com:OCamlPro/owi.git -$ cd owi -$ opam install . --deps-only --with-test --with-doc --with-dev-setup -$ git submodule update --init --recursive -$ dune build @all -``` diff --git a/doc/src/hacking/testing.md b/doc/src/hacking/testing.md deleted file mode 100644 index 7d8df28ea..000000000 --- a/doc/src/hacking/testing.md +++ /dev/null @@ -1,36 +0,0 @@ -# Testing - -## Unit tests - -Tests are mostly written using [Cram Tests]. -The ones that are integrated into documentation are using [MDX]. -You can run them as follow: - -```shell-session -$ dune runtest -``` - -If you made some changes and the output of some tests is changing, the diff will be displayed. -If you want to automatically accept the diff as being the new expected output, you can run: - -```shell-session -$ dune promote -``` - -## Code coverage - -You can generate the code coverage report with: - -```shell-session -BISECT_FILE=$(pwd)/bisect odune runtest --force --instrument-with bisect_ppx -bisect-ppx-report html -o _coverage -xdg-open _coverage/index.html -``` - -## Fuzzing - -See [test/fuzz]. - -[Cram Tests]: https://dune.readthedocs.io/en/latest/reference/cram.html -[MDX]: https://github.com/realworldocaml/mdx -[test/fuzz]: https://github.com/OCamlPro/owi/tree/main/test/fuzz diff --git a/doc/src/proposals.md b/doc/src/proposals.md deleted file mode 100644 index fabb06653..000000000 --- a/doc/src/proposals.md +++ /dev/null @@ -1,5 +0,0 @@ -# Supported Wasm proposals - -See the [WebAssembly features] page. - -[WebAssembly features]: https://webassembly.org/features