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

4 files changed, 103 insertions, 0 deletions

diff --git a/drnim/tests/config.nims b/drnim/tests/config.nims
new file mode 100644
index 000000000..cd4ee4b08
--- /dev/null
+++ b/drnim/tests/config.nims
@@ -0,0 +1,7 @@
+switch("path", "$nim/testament/lib") # so we can `import stdtest/foo` in this dir
+
+## prevent common user config settings to interfere with testament expectations
+## Indifidual tests can override this if needed to test for these options.
+switch("colors", "off")
+switch("listFullPaths", "off")
+switch("excessiveStackTrace", "off")
diff --git a/drnim/tests/tbasic_array_index.nim b/drnim/tests/tbasic_array_index.nim
new file mode 100644
index 000000000..3f24ed3bd
--- /dev/null
+++ b/drnim/tests/tbasic_array_index.nim
@@ -0,0 +1,43 @@
+discard """
+  nimout: '''tbasic_array_index.nim(26, 17) Warning: cannot prove: 0 <= len(a) - 4; counter example: a.len -> 0 [IndexCheck]
+tbasic_array_index.nim(32, 5) Warning: cannot prove: 4.0 <= 1.0 [IndexCheck]
+tbasic_array_index.nim(38, 36) Warning: cannot prove: a <= 10'u32; counter example: a -> #x000000000000000b
+'''
+  cmd: "drnim $file"
+  action: "compile"
+"""
+
+{.push staticBoundChecks: defined(nimDrNim).}
+
+proc takeNat(n: Natural) =
+  discard
+
+proc p(a, b: openArray[int]) =
+  if a.len > 0:
+    echo a[0]
+
+  for i in 0..a.len-8:
+    #{.invariant: i < a.len.}
+    echo a[i]
+
+  for i in 0..min(a.len, b.len)-1:
+    echo a[i], " ", b[i]
+
+  takeNat(a.len - 4)
+
+proc r(x: range[0.0..1.0]) = echo x
+
+proc sum() =
+  r 1.0
+  r 4.0
+
+proc ru(x: range[1u32..10u32]) = echo x
+
+proc xu(a: uint) =
+  if a >= 4u:
+    let chunk = range[1u32..10u32](a)
+    ru chunk
+
+{.pop.}
+
+p([1, 2, 3], [4, 5])
diff --git a/drnim/tests/tensures.nim b/drnim/tests/tensures.nim
new file mode 100644
index 000000000..1283b493b
--- /dev/null
+++ b/drnim/tests/tensures.nim
@@ -0,0 +1,31 @@
+discard """
+  nimout: '''tensures.nim(11, 10) Warning: BEGIN [User]
+tensures.nim(20, 5) Warning: cannot prove:
+0 < n [IndexCheck]
+tensures.nim(30, 10) Warning: END [User]'''
+  cmd: "drnim $file"
+  action: "compile"
+"""
+
+{.push staticBoundChecks: defined(nimDrNim).}
+{.warning: "BEGIN".}
+
+proc fac(n: int) {.requires: n > 0.} =
+  discard
+
+proc g(): int {.ensures: result > 0.} =
+  result = 10
+
+fac 7 # fine
+fac -45 # wrong
+
+fac g() # fine
+
+proc main =
+  var x = g()
+  fac x
+
+main()
+
+{.warning: "END".}
+{.pop.}
diff --git a/drnim/tests/tsetlen_invalidates.nim b/drnim/tests/tsetlen_invalidates.nim
new file mode 100644
index 000000000..03620af10
--- /dev/null
+++ b/drnim/tests/tsetlen_invalidates.nim
@@ -0,0 +1,22 @@
+discard """
+  nimout: '''
+tsetlen_invalidates.nim(15, 12) Warning: cannot prove: 0 <= len(a) + -1; counter example: a.len -> 0 [IndexCheck]
+'''
+  cmd: "drnim $file"
+  action: "compile"
+"""
+
+{.push staticBoundChecks: defined(nimDrNim).}
+
+proc p() =
+  var a = newSeq[int](3)
+  if a.len > 0:
+    a.setLen 0
+    echo a[0]
+
+  if a.len > 0:
+    echo a[0]
+
+{.pop.}
+
+p()