diff --git a/docs/eval_modes/options.md b/docs/eval_modes/options.md index d9665c62..c7553d7c 100644 --- a/docs/eval_modes/options.md +++ b/docs/eval_modes/options.md @@ -8,11 +8,11 @@ nav_order: 1 # Options and System Properties Formulog evaluation is controlled by options and system properties. -For example, to interpret the test program with SMT debug information (the `debugSmt` property) and 2 -threads (the `-j 2` option), use +For example, to interpret the test program with SMT logging and 2 +threads, use the `debugSmt` property and `-j 2` option: ``` -java -DdebugSmt -jar formulog.jar greeting.flg -j 2 +java -DdebugSmt -jar formulog.jar example/greeting.flg -j 2 ``` ## Options diff --git a/docs/eval_modes/smt.md b/docs/eval_modes/smt.md index cd87b498..60c946a0 100644 --- a/docs/eval_modes/smt.md +++ b/docs/eval_modes/smt.md @@ -23,7 +23,7 @@ SMT solving). - `push-pop`: try to use incremental SMT solving via the `push` and `pop` SMT commands. This can work well when query `y` extends query `x`; e.g., `y = c :: x`, where `c` is an additional conjunct; this situation most commonly occurs -when using [eager evaluation]({{ site.baseurl }}{% link eval_modes/eager.md %}). +when using [eager evaluation]({{ site.base_url }}{% link eval_modes/eager.md %}). - `check-sat-assuming`: try to use incremental SMT solving via the `check-sat-assuming` SMT command. This caches conjuncts in the SMT solver in a way such that they can be enabled or disabled per SMT query, and works well if diff --git a/docs/lang_ref/goal_directed_eval.md b/docs/lang_ref/goal_directed_eval.md index cdf99261..b00c99b2 100644 --- a/docs/lang_ref/goal_directed_eval.md +++ b/docs/lang_ref/goal_directed_eval.md @@ -49,7 +49,7 @@ predicates that are "invoked" from the functional fragment of Formulog. Queries are in the form `:- A.` where `A` is a positive (non-negated) atom. The typical rules about variable usage apply (see the "Anonymous variables" section -of the [Program Safety page]({{ site.baseurl }}{% link lang_ref/program_safety.md %})). If you want to have a query consisting of +of the [Program Safety page]({{ site.base_url }}{% link lang_ref/program_safety.md %})). If you want to have a query consisting of multiple atoms, write a rule defining a new relation and then query that relation. For example, the hypothetical query `:- A, B.` could be rewritten as the rule `R :- A, B.` and query `:- R.`. There can be only one query per diff --git a/docs/lang_ref/lang_basics.md b/docs/lang_ref/lang_basics.md index 40fd908f..c193d7ab 100644 --- a/docs/lang_ref/lang_basics.md +++ b/docs/lang_ref/lang_basics.md @@ -53,7 +53,7 @@ type cmp = ``` It also has built-in types representing logical formulas, but a discussion of -these is delayed until the [section on logical formulas]({{ site.baseurl }}{% link lang_ref/logical_formulas.md %}). +these is delayed until the [section on logical formulas]({{ site.base_url }}{% link lang_ref/logical_formulas.md %}). #### List Notation @@ -421,7 +421,7 @@ with manipulating primitives): respectively. The string should either be a decimal integer preceded optionally by `-` or `+`, or a hexadecimal integer preceded by `0x`. The operations return `none` if the string is not in the proper format or - represents an integer too large to fit in 32/64 bits. + represents an integer of too great magnitude to fit in 32/64 bits. Standard arithmetic notation can be used for signed `i32` operations. For example, `38 + 12 / 3` is shorthand for `i32_add(38, i32_sdiv(12, 3))`. diff --git a/docs/lang_ref/logical_formulas.md b/docs/lang_ref/logical_formulas.md index f215217d..359773aa 100644 --- a/docs/lang_ref/logical_formulas.md +++ b/docs/lang_ref/logical_formulas.md @@ -467,4 +467,4 @@ finds one in time; it returns `none` otherwise. Variables in a model can be inspected using `query_model`, which will return `none` if a variable is not present in the model or if it is of a type that cannot be concretely represented in Formulog (for example, Formulog does not -have a concrete representation of a 13-bit bit vector). +have a concrete representation of a 13-bit vector). diff --git a/docs/starting.md b/docs/starting.md index c9867964..84802a60 100644 --- a/docs/starting.md +++ b/docs/starting.md @@ -9,7 +9,7 @@ nav_order: 2 Thank you for your interest in Formulog! This page describes how to set up Formulog and provides some pointers on writing Formulog programs. -## Seting up Formulog +## Setting up Formulog There are three main ways to set up Formulog (listed in increasing order of number of dependencies): @@ -100,7 +100,7 @@ greeting("Hello, World") Now that you have Formulog set up, the fun part starts: writing Formulog programs! -Check out our [tutorial]({{ site.baseurl }}{% link tutorial/index.md %}) for a walk-through of how to encode a refinement type system in Formulog. +Check out our [tutorial]({{ site.base_url }}{% link tutorial/index.md %}) for a walk-through of how to encode a refinement type system in Formulog. Additional short-ish example programs can be found in the `examples/` directory (in the Docker image or repository base directory). For examples of larger developments, see the case studies we have used in publications: @@ -108,7 +108,7 @@ For examples of larger developments, see the case studies we have used in public - [a bottom-up points-to analysis for Java](https://github.com/aaronbembenek/making-formulog-fast/blob/main/benchmarks/scuba/bench.flg) - [a symbolic executor an LLVM fragment](https://github.com/aaronbembenek/making-formulog-fast/blob/main/benchmarks/symex/bench.flg) -See the [language reference]({{ site.baseurl }}{% link lang_ref/index.md %}) for details about Formulog constructs. +See the [language reference]({{ site.base_url }}{% link lang_ref/index.md %}) for details about Formulog constructs. Syntax highlighting is available for Visual Studio Code (follow instructions [here](https://github.com/HarvardPL/formulog-syntax)) and Vim (install [misc/flg.vim](https://github.com/HarvardPL/formulog/blob/master/misc/flg.vim)). diff --git a/docs/tutorial/index.md b/docs/tutorial/index.md index a646b12a..785c0b9c 100644 --- a/docs/tutorial/index.md +++ b/docs/tutorial/index.md @@ -7,7 +7,7 @@ nav_order: 3 # Tutorial: Building a Refinement Type Checker In this tutorial, we'll implement a type checker for a small (but still interesting) refinement type system in Formulog. -In particular, we'll implement the declarative, bidirectional type checking rules for the first system in the article [Refinement Types: A Tutorial](https://arxiv.org/abs/2010.07763) by Ranjit Jhala and Niki Vazou [1]. +In particular, we'll implement the declarative, bidirectional type checking rules for the first system in the article [Refinement Types: A Tutorial](https://arxiv.org/abs/2010.07763v1) by Ranjit Jhala and Niki Vazou [1]. Our hope is that our tutorial gives a good overview of many Formulog features, and a flavor of what it is like to program a nontrivial analysis in Formulog. ### Intended Audience @@ -24,7 +24,7 @@ If you have a question about the content of this tutorial, a suggestion for impr ### Attribution -This tutorial includes figures from the article [Refinement Types: A Tutorial](https://arxiv.org/abs/2010.07763) (v1) by Ranjit Jhala and Niki Vazou [1], which has been published under a [CC BY 4.0 license](https://creativecommons.org/licenses/by/4.0/). +This tutorial includes figures from the article [Refinement Types: A Tutorial](https://arxiv.org/abs/2010.07763v1) by Ranjit Jhala and Niki Vazou [1], which has been published under a [CC BY 4.0 license](https://creativecommons.org/licenses/by/4.0/). We will refer to this article as "JV" for short. ## General Approach @@ -35,7 +35,7 @@ Our typical approach when implementing an analysis in Formulog is thus to try to This is the approach we will follow in this tutorial: directly translate the formalism of JV as we encounter it, and then go back to patch our implementation as necessary. Concretely, we will work our way through JV Sections 3.1 and 3.2. -For the full, final code, see [tutorial.flg](tutorial.flg). +For the full, final code, see [tutorial.flg](https://github.com/HarvardPL/formulog/blob/master/docs/tutorial/tutorial.flg). ## Definitions @@ -600,7 +600,7 @@ ent((X, t_refined(B, Y, P)) :: G, C) :- ``` Now the type checker works on this example! -(This isn't the most general solution: a better technique would be to create a fresh variable and substitute it with `Y` in `P` and `X` in `C`; however, this is good enough for now.) +(This isn't the most general solution: a better technique would be to create a fresh variable and substitute it for `Y` in `P` and `X` in `C`; however, this is good enough for now.) ### Checking Functions @@ -772,10 +772,10 @@ As we mentioned earlier, please raise a [GitHub issue](https://github.com/Harvar ## References -[1] Ranjit Jhala and Niki Vazou. 2020. Refinement Types: A Tutorial. arXiv:2010.07763. https://arxiv.org/abs/2010.07763 +[1] Ranjit Jhala and Niki Vazou. 2020. Refinement Types: A Tutorial. arXiv:2010.07763v1. -[2] Gavin M. Bierman, Andrew D. Gordon, Cătălin Hriţcu, and David Langworthy. 2012. Semantic Subtyping with an SMT Solver. Journal of Functional Programming 22, 1 (2012), 31–105. https://doi.org/10.1145/1863543.1863560 +[2] Gavin M. Bierman, Andrew D. Gordon, Cătălin Hriţcu, and David Langworthy. 2012. Semantic Subtyping with an SMT Solver. Journal of Functional Programming 22, 1 (2012), 31–105. -[3] Yu Feng, Xinyu Wang, Isil Dillig, and Thomas Dillig. 2015. Bottom-up Context-Sensitive Pointer Analysis for Java. In Proceedings of the 13th Asian Symposium on Programming Languages and Systems. 465–484. https://doi.org/10.1007/978-3-319-26529-2_25 +[3] Yu Feng, Xinyu Wang, Isil Dillig, and Thomas Dillig. 2015. Bottom-up Context-Sensitive Pointer Analysis for Java. In Proceedings of the 13th Asian Symposium on Programming Languages and Systems. 465–484. -[4] Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. 209–224. https://www.usenix.org/legacy/event/osdi08/tech/full_papers/cadar/cadar.pdf +[4] Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. 209–224. diff --git a/docs/tutorial/tutorial.flg b/docs/tutorial/tutorial.flg index 8d700dbd..fe65cd34 100644 --- a/docs/tutorial/tutorial.flg +++ b/docs/tutorial/tutorial.flg @@ -2,7 +2,7 @@ DEFINITIONS *******************************************************************************) -(* An algebraic data type with a single variant *) +(* An algebraic data type with two variants *) type basic_typ = | b_int | b_bool @@ -39,7 +39,7 @@ type kind = | k_base | k_star -(* Tuples and lists are built-in type *) +(* Tuples and lists are built-in types *) type env = (var * typ) list type expr =