DrNim (Nim compiler with Z3 integration) (#13743)

* code cleanups and feature additions
* added basic test and koch/CI integration
* make it build on Unix
* DrNim: now buildable on Unix, only takes 10 minutes, enjoy
* added basic documentation for DrNim which can also be seen as the RFC we're following
* drnim: change the build setup so that drnim.exe ends up in bin/
* makes simple floating point ranges work
* added basic float range check
* drnim: teach Z3 about Nim's range types plus code refactoring
* drnim: make unsigned numbers work
* added and fixed index checking under setLen
* first implementation of .ensures, .invariant and .assume (.requires still missing and so is proc type compatibility checking
* drnim: .requires checking implemented
* drnim: implemented .ensures properly
* more impressive test involving min()
* drnim: check for proc type compatibility and base method compatibility wrt .requires and .ensures
* testament: support for 'pattern <directory>
* koch: uses new <directory> feature of testament
* drnim: added tiny musings about 'old'
* Make testament work with old SSL versions
* koch: add support for 'koch drnim -d:release'
* drnim: preparations for the param.old notation

1 files changed, 203 insertions, 0 deletions

diff --git a/doc/drnim.rst b/doc/drnim.rst
new file mode 100644
index 000000000..a9ae9baeb
--- /dev/null
+++ b/doc/drnim.rst
@@ -0,0 +1,203 @@
+===================================
+   DrNim User Guide
+===================================
+
+:Author: Andreas Rumpf
+:Version: |nimversion|
+
+.. contents::
+
+
+Introduction
+============
+
+This document describes the usage of the *DrNim* tool. DrNim combines
+the Nim frontend with the `Z3 <https://github.com/Z3Prover/z3>`_ proof
+engine in order to allow verify / validate software written in Nim.
+DrNim's command line options are the same as the Nim compiler's.
+
+
+DrNim currently only checks the sections of your code that are marked
+via ``staticBoundChecks: on``:
+
+.. code-block:: nim
+
+  {.push staticBoundChecks: on.}
+  # <--- code section here ---->
+  {.pop.}
+
+DrNim currently only tries to prove array indexing or subrange checks,
+overflow errors are *not* prevented. Overflows will be checked for in
+the future.
+
+Later versions of the **Nim compiler** will **assume** that the checks inside
+the ``staticBoundChecks: on`` environment have been proven correct and so
+it will **omit** the runtime checks. If you do not want this behavior, use
+instead ``{.push staticBoundChecks: defined(nimDrNim).}``. This way the
+Nim compiler remains unaware of the performed proofs but DrNim will prove
+your code.
+
+
+Installation
+============
+
+Run ``koch drnim``, the executable will afterwards be in ``$nim/bin/drnim``.
+
+
+Motivating Example
+==================
+
+The follow example highlights what DrNim can easily do, even
+without additional annotations:
+
+.. code-block:: nim
+
+  {.push staticBoundChecks: on.}
+
+  proc sum(a: openArray[int]): int =
+    for i in 0..a.len:
+      result += a[i]
+
+  {.pop.}
+
+  echo sum([1, 2, 3])
+
+This program contains a famous "index out of bounds" bug. DrNim
+detects it and produces the following error message::
+
+  cannot prove: i <= len(a) + -1; counter example: i -> 0 a.len -> 0 [IndexCheck]
+
+In other words for ``i == 0`` and ``a.len == 0`` (for example!) there would be
+an index out of bounds error.
+
+
+Pre-, postconditions and invariants
+===================================
+
+DrNim adds 4 additional annotations (pragmas) to Nim:
+
+- `requires`:idx:
+- `ensures`:idx:
+- `invariant`:idx:
+- `assume`:idx:
+
+These pragmas are ignored by the Nim compiler so that they don't have to
+be disabled via ``when defined(nimDrNim)``.
+
+
+Invariant
+---------
+
+An ``invariant`` is a proposition that must be true after every loop
+iteration, it's tied to the loop body it's part of.
+
+
+Requires
+--------
+
+A ``requires`` annotation describes what the function expects to be true
+before it's called so that it can perform its operation. A ``requires``
+annotation is also called a `precondition`:idx:.
+
+
+Ensures
+-------
+
+An ``ensures`` annotation describes what will be true after the function
+call. An ``ensures`` annotation is also called a `postcondition`:idx:.
+
+
+Assume
+------
+
+An ``assume`` annotation describes what DrNim should **assume** to be true
+in this section of the program. It is an unsafe escape mechanism comparable
+to Nim's ``cast`` statement. Use it only when you really know better
+than DrNim. You should add a comment to a paper that proves the proposition
+you assume.
+
+
+Example: insertionSort
+======================
+
+**Note**: This example does not yet work with DrNim. ``forall`` and ``exists``
+are not implemented.
+
+.. code-block:: nim
+
+  import std / logic
+
+  proc insertionSort(a: var openArray[int]) {.
+      ensures: forall(i in 1..<a.len, a[i-1] <= a[i]).} =
+
+    for k in 1 ..< a.len:
+      {.invariant: 1 <= k and k <= a.len.}
+      {.invariant: forall(j in 1..<k, i in 0..<j, a[i] <= a[j]).}
+      var t = k
+      while t > 0 and a[t-1] > a[t]:
+        {.invariant: k < a.len.}
+        {.invariant: 0 <= t and t <= k.}
+        {.invariant: forall(j in 1..k, i in 0..<j, j == t or a[i] <= a[j]).}
+        swap a[t], a[t-1]
+        dec t
+
+Unfortunately the invariants required to prove this code correct take more
+code than the imperative instructions. However this effort can be compensated
+by the fact that the result needs very little testing. Be aware though that
+DrNim only proves that after ``insertionSort`` this condition holds::
+
+  forall(i in 1..<a.len, a[i-1] <= a[i])
+
+
+This is required, but not sufficient to describe that a ``sort`` operation
+was performed. For example, the same postcondition is true for this proc
+which doesn't sort at all:
+
+.. code-block:: nim
+
+  import std / logic
+
+  proc insertionSort(a: var openArray[int]) {.
+      ensures: forall(i in 1..<a.len, a[i-1] <= a[i]).} =
+    # does not sort, overwrites `a`'s contents!
+    for i in 0..<a.len: a[i] = i
+
+
+
+Syntax of propositions
+======================
+
+The basic syntax is ``ensures|requires|invariant: <prop>``.
+A ``prop`` is either a comparison or a compound::
+
+  prop = nim_bool_expression
+       | prop 'and' prop
+       | prop 'or' prop
+       | prop '->' prop # implication
+       | prop '<->' prop
+       | 'not' prop
+       | '(' prop ')' # you can group props via ()
+       | forallProp
+       | existsProp
+
+  forallProp = 'forall' '(' quantifierList ',' prop ')'
+  existsProp = 'exists' '(' quantifierList ',' prop ')'
+
+  quantifierList = quantifier (',' quantifier)*
+  quantifier = <new identifier> 'in' nim_iteration_expression
+
+
+``nim_iteration_expression`` here is an ordinary expression of Nim code
+that describes an iteration space, for example ``1..4`` or ``1..<a.len``.
+
+``nim_bool_expression`` here is an ordinary expression of Nim code of
+type ``bool`` like ``a == 3`` or ``23 > a.len``.
+
+The supported subset of Nim code that can be used in these expressions
+is currently underspecified but ``let`` variables, function parameters
+and ``result`` (which represents the function's final result) are amenable
+for verification. The expressions must not have any side-effects and must
+terminate.
+
+The operators ``forall``, ``exists``, ``->``, ``<->`` have to imported
+from ``std / logic``.