klee: Start preparing for klee tests

First stage: something compiling without klee, but with a buch of dirty
hacks - done.
Second stage: something running under klee, able to emit useful results,
but still using dirty hacks - done.

Third stage: make CMake care about clang argumnets - not done, may be
omitted if proves to be too hard. Not that klee can be run on CI in any
case.

9 files changed, 601 insertions, 0 deletions

diff --git a/src/nvim/lib/ringbuf.h b/src/nvim/lib/ringbuf.h
index 12b75ec65a..e63eae70b0 100644
--- a/src/nvim/lib/ringbuf.h
+++ b/src/nvim/lib/ringbuf.h
@@ -15,6 +15,7 @@
 #ifndef NVIM_LIB_RINGBUF_H
 #define NVIM_LIB_RINGBUF_H
 
+#include <stddef.h>
 #include <string.h>
 #include <assert.h>
 #include <stdint.h>
@@ -73,6 +74,32 @@ typedef struct { \
   RBType *buf_end; \
 } TypeName##RingBuffer;
 
+/// Dummy item free macros, for use in RINGBUF_INIT
+///
+/// This macros actually does nothing.
+///
+/// @param[in]  item  Item to be freed.
+#define RINGBUF_DUMMY_FREE(item)
+
+/// Static ring buffer
+///
+/// @warning Ring buffers created with this macros must neither be freed nor
+///          deallocated.
+///
+/// @param  scope  Ring buffer scope.
+/// @param  TypeName  Ring buffer type name.
+/// @param  RBType  Type of the single ring buffer element.
+/// @param  varname  Variable name.
+/// @param  rbsize  Ring buffer size.
+#define RINGBUF_STATIC(scope, TypeName, RBType, varname, rbsize) \
+static RBType _##varname##_buf[rbsize]; \
+scope TypeName##RingBuffer varname = { \
+  .buf = _##varname##_buf, \
+  .next = _##varname##_buf, \
+  .first = NULL, \
+  .buf_end = _##varname##_buf + rbsize - 1, \
+};
+
 /// Initialize a new ring buffer
 ///
 /// @param TypeName    Ring buffer type name. Actual type name will be
diff --git a/test/symbolic/klee/nvim/charset.c b/test/symbolic/klee/nvim/charset.c
new file mode 100644
index 0000000000..a40488920e
--- /dev/null
+++ b/test/symbolic/klee/nvim/charset.c
@@ -0,0 +1,10 @@
+#include <stdbool.h>
+
+#include "nvim/ascii.h"
+#include "nvim/macros.h"
+#include "nvim/charset.h"
+
+bool vim_isIDc(int c)
+{
+  return ASCII_ISALNUM(c);
+}
diff --git a/test/symbolic/klee/nvim/garray.c b/test/symbolic/klee/nvim/garray.c
new file mode 100644
index 0000000000..260870c3c2
--- /dev/null
+++ b/test/symbolic/klee/nvim/garray.c
@@ -0,0 +1,195 @@
+// This is an open source non-commercial project. Dear PVS-Studio, please check
+// it. PVS-Studio Static Code Analyzer for C, C++ and C#: http://www.viva64.com
+
+/// @file garray.c
+///
+/// Functions for handling growing arrays.
+
+#include <string.h>
+#include <inttypes.h>
+
+#include "nvim/vim.h"
+#include "nvim/ascii.h"
+#include "nvim/log.h"
+#include "nvim/memory.h"
+#include "nvim/path.h"
+#include "nvim/garray.h"
+#include "nvim/strings.h"
+
+// #include "nvim/globals.h"
+#include "nvim/memline.h"
+
+#ifdef INCLUDE_GENERATED_DECLARATIONS
+# include "garray.c.generated.h"
+#endif
+
+/// Clear an allocated growing array.
+void ga_clear(garray_T *gap)
+{
+  xfree(gap->ga_data);
+
+  // Initialize growing array without resetting itemsize or growsize
+  gap->ga_data = NULL;
+  gap->ga_maxlen = 0;
+  gap->ga_len = 0;
+}
+
+/// Clear a growing array that contains a list of strings.
+///
+/// @param gap
+void ga_clear_strings(garray_T *gap)
+{
+  GA_DEEP_CLEAR_PTR(gap);
+}
+
+/// Initialize a growing array.
+///
+/// @param gap
+/// @param itemsize
+/// @param growsize
+void ga_init(garray_T *gap, int itemsize, int growsize)
+{
+  gap->ga_data = NULL;
+  gap->ga_maxlen = 0;
+  gap->ga_len = 0;
+  gap->ga_itemsize = itemsize;
+  ga_set_growsize(gap, growsize);
+}
+
+/// A setter for the growsize that guarantees it will be at least 1.
+///
+/// @param gap
+/// @param growsize
+void ga_set_growsize(garray_T *gap, int growsize)
+{
+  if (growsize < 1) {
+    WLOG("trying to set an invalid ga_growsize: %d", growsize);
+    gap->ga_growsize = 1;
+  } else {
+    gap->ga_growsize = growsize;
+  }
+}
+
+/// Make room in growing array "gap" for at least "n" items.
+///
+/// @param gap
+/// @param n
+void ga_grow(garray_T *gap, int n)
+{
+  if (gap->ga_maxlen - gap->ga_len >= n) {
+    // the garray still has enough space, do nothing
+    return;
+  }
+
+  if (gap->ga_growsize < 1) {
+    WLOG("ga_growsize(%d) is less than 1", gap->ga_growsize);
+  }
+
+  // the garray grows by at least growsize
+  if (n < gap->ga_growsize) {
+    n = gap->ga_growsize;
+  }
+  int new_maxlen = gap->ga_len + n;
+
+  size_t new_size = (size_t)(gap->ga_itemsize * new_maxlen);
+  size_t old_size = (size_t)(gap->ga_itemsize * gap->ga_maxlen);
+
+  // reallocate and clear the new memory
+  char *pp = xrealloc(gap->ga_data, new_size);
+  memset(pp + old_size, 0, new_size - old_size);
+
+  gap->ga_maxlen = new_maxlen;
+  gap->ga_data = pp;
+}
+
+/// For a growing array that contains a list of strings: concatenate all the
+/// strings with sep as separator.
+///
+/// @param gap
+/// @param sep
+///
+/// @returns the concatenated strings
+char_u *ga_concat_strings_sep(const garray_T *gap, const char *sep)
+  FUNC_ATTR_NONNULL_RET
+{
+  const size_t nelem = (size_t) gap->ga_len;
+  const char **strings = gap->ga_data;
+
+  if (nelem == 0) {
+    return (char_u *) xstrdup("");
+  }
+
+  size_t len = 0;
+  for (size_t i = 0; i < nelem; i++) {
+    len += strlen(strings[i]);
+  }
+
+  // add some space for the (num - 1) separators
+  len += (nelem - 1) * strlen(sep);
+  char *const ret = xmallocz(len);
+
+  char *s = ret;
+  for (size_t i = 0; i < nelem - 1; i++) {
+    s = xstpcpy(s, strings[i]);
+    s = xstpcpy(s, sep);
+  }
+  strcpy(s, strings[nelem - 1]);
+
+  return (char_u *) ret;
+}
+
+/// For a growing array that contains a list of strings: concatenate all the
+/// strings with a separating comma.
+///
+/// @param gap
+///
+/// @returns the concatenated strings
+char_u* ga_concat_strings(const garray_T *gap) FUNC_ATTR_NONNULL_RET
+{
+  return ga_concat_strings_sep(gap, ",");
+}
+
+/// Concatenate a string to a growarray which contains characters.
+/// When "s" is NULL does not do anything.
+///
+/// WARNING:
+/// - Does NOT copy the NUL at the end!
+/// - The parameter may not overlap with the growing array
+///
+/// @param gap
+/// @param s
+void ga_concat(garray_T *gap, const char_u *restrict s)
+{
+  if (s == NULL) {
+    return;
+  }
+
+  ga_concat_len(gap, (const char *restrict) s, strlen((char *) s));
+}
+
+/// Concatenate a string to a growarray which contains characters
+///
+/// @param[out]  gap  Growarray to modify.
+/// @param[in]  s  String to concatenate.
+/// @param[in]  len  String length.
+void ga_concat_len(garray_T *const gap, const char *restrict s,
+                   const size_t len)
+  FUNC_ATTR_NONNULL_ALL
+{
+  if (len) {
+    ga_grow(gap, (int) len);
+    char *data = gap->ga_data;
+    memcpy(data + gap->ga_len, s, len);
+    gap->ga_len += (int) len;
+  }
+}
+
+/// Append one byte to a growarray which contains bytes.
+///
+/// @param gap
+/// @param c
+void ga_append(garray_T *gap, char c)
+{
+  GA_APPEND(char, gap, c);
+}
+
diff --git a/test/symbolic/klee/nvim/gettext.c b/test/symbolic/klee/nvim/gettext.c
new file mode 100644
index 0000000000..b9cc98d770
--- /dev/null
+++ b/test/symbolic/klee/nvim/gettext.c
@@ -0,0 +1,4 @@
+char *gettext(const char *s)
+{
+  return (char *)s;
+}
diff --git a/test/symbolic/klee/nvim/mbyte.c b/test/symbolic/klee/nvim/mbyte.c
new file mode 100644
index 0000000000..394d17b700
--- /dev/null
+++ b/test/symbolic/klee/nvim/mbyte.c
@@ -0,0 +1,18 @@
+#include <stddef.h>
+
+#include "nvim/types.h"
+#include "nvim/mbyte.h"
+#include "nvim/ascii.h"
+
+char_u *string_convert(const vimconv_T *conv, char_u *data, size_t *size)
+{
+  return NULL;
+}
+
+int utfc_ptr2len_len(const char_u *p, int size)
+{
+  if (size < 1 || *p == NUL) {
+    return 0;
+  }
+  return 1;
+}
diff --git a/test/symbolic/klee/nvim/memory.c b/test/symbolic/klee/nvim/memory.c
new file mode 100644
index 0000000000..7e924a410a
--- /dev/null
+++ b/test/symbolic/klee/nvim/memory.c
@@ -0,0 +1,90 @@
+#include <stdlib.h>
+#include <assert.h>
+
+#include "nvim/lib/ringbuf.h"
+
+enum { RB_SIZE = 1024 };
+
+typedef struct {
+  void *ptr;
+  size_t size;
+} AllocRecord;
+
+RINGBUF_TYPEDEF(AllocRecords, AllocRecord)
+RINGBUF_INIT(AllocRecords, arecs, AllocRecord, RINGBUF_DUMMY_FREE)
+RINGBUF_STATIC(static, AllocRecords, AllocRecord, arecs, RB_SIZE)
+
+size_t allocated_memory = 0;
+
+void *xmalloc(const size_t size)
+{
+  void *ret = malloc(size);
+  allocated_memory += size;
+  assert(arecs_rb_length(&arecs) < RB_SIZE);
+  arecs_rb_push(&arecs, (AllocRecord) {
+    .ptr = ret,
+    .size = size,
+  });
+  return ret;
+}
+
+void xfree(void *const p)
+{
+  RINGBUF_FORALL(&arecs, AllocRecord, arec) {
+    if (arec->ptr == p) {
+      allocated_memory -= arec->size;
+      arecs_rb_remove(&arecs, arecs_rb_find_idx(&arecs, arec));
+      return;
+    }
+  }
+  assert(false);
+}
+
+void *xrealloc(void *const p, size_t new_size)
+{
+  void *ret = realloc(p, new_size);
+  RINGBUF_FORALL(&arecs, AllocRecord, arec) {
+    if (arec->ptr == p) {
+      allocated_memory -= arec->size;
+      allocated_memory += new_size;
+      arec->ptr = ret;
+      arec->size = new_size;
+      return ret;
+    }
+  }
+  assert(false);
+  return (void *)(intptr_t)1;
+}
+
+char *xstrdup(const char *str)
+  FUNC_ATTR_MALLOC FUNC_ATTR_WARN_UNUSED_RESULT FUNC_ATTR_NONNULL_RET
+  FUNC_ATTR_NONNULL_ALL
+{
+  return xmemdupz(str, strlen(str));
+}
+
+void *xmallocz(size_t size)
+  FUNC_ATTR_MALLOC FUNC_ATTR_NONNULL_RET FUNC_ATTR_WARN_UNUSED_RESULT
+{
+  size_t total_size = size + 1;
+  assert(total_size > size);
+
+  void *ret = xmalloc(total_size);
+  ((char *)ret)[size] = 0;
+
+  return ret;
+}
+
+char *xstpcpy(char *restrict dst, const char *restrict src)
+  FUNC_ATTR_NONNULL_RET FUNC_ATTR_WARN_UNUSED_RESULT FUNC_ATTR_NONNULL_ALL
+{
+  const size_t len = strlen(src);
+  return (char *)memcpy(dst, src, len + 1) + len;
+}
+
+void *xmemdupz(const void *data, size_t len)
+  FUNC_ATTR_MALLOC FUNC_ATTR_NONNULL_RET FUNC_ATTR_WARN_UNUSED_RESULT
+  FUNC_ATTR_NONNULL_ALL
+{
+  return memcpy(xmallocz(len), data, len);
+}
diff --git a/test/symbolic/klee/run.sh b/test/symbolic/klee/run.sh
new file mode 100755
index 0000000000..388903c234
--- /dev/null
+++ b/test/symbolic/klee/run.sh
@@ -0,0 +1,69 @@
+#!/bin/sh
+
+set -e
+set -x
+test -z "$POSH_VERSION" && set -u
+
+PROJECT_SOURCE_DIR=.
+PROJECT_BINARY_DIR="$PROJECT_SOURCE_DIR/build"
+KLEE_TEST_DIR="$PROJECT_SOURCE_DIR/test/symbolic/klee"
+KLEE_BIN_DIR="$PROJECT_BINARY_DIR/klee"
+KLEE_OUT_DIR="$KLEE_BIN_DIR/out"
+
+main() {
+  local compile=
+  if test "$1" = "-c" ; then
+    compile=1
+    shift
+  fi
+  local test="$1" ; shift
+
+  local includes=
+  includes="$includes -I$KLEE_TEST_DIR"
+  includes="$includes -I/home/klee/klee_src/include"
+  includes="$includes -I$PROJECT_SOURCE_DIR/src"
+  includes="$includes -I$PROJECT_BINARY_DIR/src/nvim/auto"
+  includes="$includes -I$PROJECT_BINARY_DIR/include"
+  includes="$includes -I$PROJECT_BINARY_DIR/config"
+  includes="$includes -I/host-includes"
+
+  local defines=
+  defines="$defines -DMIN_LOG_LEVEL=9999"
+  defines="$defines -DINCLUDE_GENERATED_DECLARATIONS"
+
+  test -z "$compile" && defines="$defines -DUSE_KLEE"
+
+  test -d "$KLEE_BIN_DIR" || mkdir -p "$KLEE_BIN_DIR"
+
+  if test -z "$compile" ; then
+    test -d "$KLEE_OUT_DIR" && rm -r "$KLEE_OUT_DIR"
+    local line1='cd /image'
+    line1="$line1 && $(echo clang \
+      $includes $defines \
+      -o "$KLEE_BIN_DIR/a.bc" -emit-llvm -g -c \
+      "$KLEE_TEST_DIR/$test.c")"
+    line1="$line1 && klee --libc=uclibc --posix-runtime "
+    line1="$line1 '--output-dir=$KLEE_OUT_DIR' '$KLEE_BIN_DIR/a.bc'"
+    local line2="for t in '$KLEE_OUT_DIR'/*.err"
+    line2="$line2 ; do ktest-tool --write-ints"
+    line2="$line2 \"\$(printf '%s' \"\$t\" | sed -e 's@.[^/]*\$@.out@')\""
+    line2="$line2 ; done"
+    printf '%s\n%s\n' "$line1" "$line2" | \
+      docker run \
+        --volume "$(cd "$PROJECT_SOURCE_DIR" && pwd)":/image \
+        --volume "/usr/include":/host-includes \
+        --interactive \
+        --rm \
+        --ulimit='stack=-1:-1' \
+        klee/klee \
+        /bin/sh -x
+  else
+    clang \
+      $includes $defines \
+      -o "$KLEE_BIN_DIR/$test" \
+      -O0 -g \
+      "$KLEE_TEST_DIR/$test.c"
+  fi
+}
+
+main "$@"
diff --git a/test/symbolic/klee/viml_expressions_lexer.c b/test/symbolic/klee/viml_expressions_lexer.c
new file mode 100644
index 0000000000..e3b5aa80cc
--- /dev/null
+++ b/test/symbolic/klee/viml_expressions_lexer.c
@@ -0,0 +1,86 @@
+#ifdef USE_KLEE
+# include <klee/klee.h>
+#else
+# include <string.h>
+#endif
+#include <stddef.h>
+#include <stdint.h>
+#include <assert.h>
+
+#include "nvim/viml/parser/expressions.h"
+#include "nvim/viml/parser/parser.h"
+#include "nvim/mbyte.h"
+
+#include "nvim/memory.c"
+#include "nvim/mbyte.c"
+#include "nvim/charset.c"
+#include "nvim/garray.c"
+#include "nvim/gettext.c"
+#include "nvim/viml/parser/expressions.c"
+
+#define INPUT_SIZE 7
+
+uint8_t avoid_optimizing_out;
+
+void simple_get_line(void *cookie, ParserLine *ret_pline)
+{
+  ParserLine **plines_p = (ParserLine **)cookie;
+  *ret_pline = **plines_p;
+  (*plines_p)++;
+}
+
+int main(const int argc, const char *const *const argv,
+         const char *const *const environ)
+{
+  char input[INPUT_SIZE];
+  uint8_t shift;
+  const bool peek = false;
+  avoid_optimizing_out = argc;
+
+#ifdef USE_KLEE
+  klee_make_symbolic(input, sizeof(input), "input");
+  klee_make_symbolic(&shift, sizeof(shift), "shift");
+  klee_assume(shift < INPUT_SIZE);
+#endif
+
+  ParserLine plines[] = {
+    {
+#ifdef USE_KLEE
+      .data = &input[shift],
+      .size = sizeof(input) - shift,
+#else
+      .data = (const char *)&argv[1],
+      .size = strlen(argv[1]),
+#endif
+      .allocated = false,
+    },
+    {
+      .data = NULL,
+      .size = 0,
+      .allocated = false,
+    },
+  };
+#ifdef USE_KLEE
+  assert(plines[0].size <= INPUT_SIZE);
+  assert((plines[0].data[0] != 5) | (plines[0].data[0] != argc));
+#endif
+  ParserLine *cur_pline = &plines[0];
+
+  ParserState pstate = {
+    .reader = {
+      .get_line = simple_get_line,
+      .cookie = &cur_pline,
+      .lines = KV_INITIAL_VALUE,
+      .conv.vc_type = CONV_NONE,
+    },
+    .pos = { 0, 0 },
+    .colors = NULL,
+    .can_continuate = false,
+  };
+  kvi_init(pstate.reader.lines);
+
+  LexExprToken token = viml_pexpr_next_token(&pstate, peek);
+  assert((pstate.pos.line == 0)
+         ? (pstate.pos.col > 0)
+         : (pstate.pos.line == 1 && pstate.pos.col == 0));
+}
diff --git a/test/symbolic/klee/viml_expressions_parser.c b/test/symbolic/klee/viml_expressions_parser.c
new file mode 100644
index 0000000000..2bad1adc53
--- /dev/null
+++ b/test/symbolic/klee/viml_expressions_parser.c
@@ -0,0 +1,102 @@
+#ifdef USE_KLEE
+# error UNFINISHED
+# include <klee/klee.h>
+#else
+# include <string.h>
+#endif
+#include <stddef.h>
+#include <stdint.h>
+#include <assert.h>
+
+#include "nvim/viml/parser/expressions.h"
+#include "nvim/viml/parser/parser.h"
+#include "nvim/mbyte.h"
+
+#include "nvim/memory.c"
+#include "nvim/mbyte.c"
+#include "nvim/charset.c"
+#include "nvim/garray.c"
+#include "nvim/gettext.c"
+#include "nvim/viml/parser/expressions.c"
+
+#define INPUT_SIZE 50
+
+uint8_t avoid_optimizing_out;
+
+void simple_get_line(void *cookie, ParserLine *ret_pline)
+{
+  ParserLine **plines_p = (ParserLine **)cookie;
+  *ret_pline = **plines_p;
+  (*plines_p)++;
+}
+
+int main(const int argc, const char *const *const argv,
+         const char *const *const environ)
+{
+  char input[INPUT_SIZE];
+  uint8_t shift;
+  int flags;
+  const bool peek = false;
+  avoid_optimizing_out = argc;
+
+#ifndef USE_KLEE
+  sscanf(argv[2], "%d", &flags);
+#endif
+
+#ifdef USE_KLEE
+  klee_make_symbolic(input, sizeof(input), "input");
+  klee_make_symbolic(&shift, sizeof(shift), "shift");
+  klee_make_symbolic(&flags, sizeof{flags}, "flags");
+  klee_assume(shift < INPUT_SIZE);
+  klee_assume(
+      flags <= kExprFlagsMulti|kExprFlagsDisallowEOC|kExprFlagsPrintError);
+#endif
+
+  ParserLine plines[] = {
+    {
+#ifdef USE_KLEE
+      .data = &input[shift],
+      .size = sizeof(input) - shift,
+#else
+      .data = argv[1],
+      .size = strlen(argv[1]),
+#endif
+      .allocated = false,
+    },
+    {
+      .data = NULL,
+      .size = 0,
+      .allocated = false,
+    },
+  };
+#ifdef USE_KLEE
+  assert(plines[0].size <= INPUT_SIZE);
+  assert((plines[0].data[0] != 5) | (plines[0].data[0] != argc));
+#endif
+  ParserLine *cur_pline = &plines[0];
+
+  ParserState pstate = {
+    .reader = {
+      .get_line = simple_get_line,
+      .cookie = &cur_pline,
+      .lines = KV_INITIAL_VALUE,
+      .conv.vc_type = CONV_NONE,
+    },
+    .pos = { 0, 0 },
+    .colors = NULL,
+    .can_continuate = false,
+  };
+  kvi_init(pstate.reader.lines);
+
+  const ExprAST ast = viml_pexpr_parse(&pstate, flags);
+  assert(ast.root != NULL
+         || plines[0].size == 0);
+  assert(ast.root != NULL || !ast.correct);
+  assert(ast.correct
+         || (ast.err.msg != NULL
+             && ast.err.arg != NULL
+             && ast.err.arg >= plines[0].data
+             && ((size_t)(ast.err.arg - plines[0].data) + ast.err.arg_len
+                 <= plines[0].size)));
+  // FIXME: free memory and assert no memory leaks
+}