aboutsummaryrefslogtreecommitdiff
path: root/test/symbolic/klee
diff options
context:
space:
mode:
Diffstat (limited to 'test/symbolic/klee')
-rw-r--r--test/symbolic/klee/nvim/charset.c172
-rw-r--r--test/symbolic/klee/nvim/garray.c195
-rw-r--r--test/symbolic/klee/nvim/gettext.c4
-rw-r--r--test/symbolic/klee/nvim/keymap.c539
-rw-r--r--test/symbolic/klee/nvim/mbyte.c266
-rw-r--r--test/symbolic/klee/nvim/memory.c101
-rwxr-xr-xtest/symbolic/klee/run.sh102
-rw-r--r--test/symbolic/klee/viml_expressions_lexer.c105
-rw-r--r--test/symbolic/klee/viml_expressions_parser.c117
9 files changed, 1601 insertions, 0 deletions
diff --git a/test/symbolic/klee/nvim/charset.c b/test/symbolic/klee/nvim/charset.c
new file mode 100644
index 0000000000..95853a6834
--- /dev/null
+++ b/test/symbolic/klee/nvim/charset.c
@@ -0,0 +1,172 @@
+#include <stdbool.h>
+
+#include "nvim/ascii.h"
+#include "nvim/macros.h"
+#include "nvim/charset.h"
+#include "nvim/eval/typval.h"
+#include "nvim/vim.h"
+
+int hex2nr(int c)
+{
+ if ((c >= 'a') && (c <= 'f')) {
+ return c - 'a' + 10;
+ }
+
+ if ((c >= 'A') && (c <= 'F')) {
+ return c - 'A' + 10;
+ }
+ return c - '0';
+}
+
+void vim_str2nr(const char_u *const start, int *const prep, int *const len,
+ const int what, varnumber_T *const nptr,
+ uvarnumber_T *const unptr, const int maxlen)
+{
+ const char *ptr = (const char *)start;
+#define STRING_ENDED(ptr) \
+ (!(maxlen == 0 || (int)((ptr) - (const char *)start) < maxlen))
+ int pre = 0; // default is decimal
+ const bool negative = (ptr[0] == '-');
+ uvarnumber_T un = 0;
+
+ if (negative) {
+ ptr++;
+ }
+
+ if (what & STR2NR_FORCE) {
+ // When forcing main consideration is skipping the prefix. Octal and decimal
+ // numbers have no prefixes to skip. pre is not set.
+ switch ((unsigned)what & (~(unsigned)STR2NR_FORCE)) {
+ case STR2NR_HEX: {
+ if (!STRING_ENDED(ptr + 2)
+ && ptr[0] == '0'
+ && (ptr[1] == 'x' || ptr[1] == 'X')
+ && ascii_isxdigit(ptr[2])) {
+ ptr += 2;
+ }
+ goto vim_str2nr_hex;
+ }
+ case STR2NR_BIN: {
+ if (!STRING_ENDED(ptr + 2)
+ && ptr[0] == '0'
+ && (ptr[1] == 'b' || ptr[1] == 'B')
+ && ascii_isbdigit(ptr[2])) {
+ ptr += 2;
+ }
+ goto vim_str2nr_bin;
+ }
+ case STR2NR_OCT: {
+ goto vim_str2nr_oct;
+ }
+ case 0: {
+ goto vim_str2nr_dec;
+ }
+ default: {
+ assert(false);
+ }
+ }
+ } else if ((what & (STR2NR_HEX|STR2NR_OCT|STR2NR_BIN))
+ && !STRING_ENDED(ptr + 1)
+ && ptr[0] == '0' && ptr[1] != '8' && ptr[1] != '9') {
+ pre = ptr[1];
+ // Detect hexadecimal: 0x or 0X follwed by hex digit
+ if ((what & STR2NR_HEX)
+ && !STRING_ENDED(ptr + 2)
+ && (pre == 'X' || pre == 'x')
+ && ascii_isxdigit(ptr[2])) {
+ ptr += 2;
+ goto vim_str2nr_hex;
+ }
+ // Detect binary: 0b or 0B follwed by 0 or 1
+ if ((what & STR2NR_BIN)
+ && !STRING_ENDED(ptr + 2)
+ && (pre == 'B' || pre == 'b')
+ && ascii_isbdigit(ptr[2])) {
+ ptr += 2;
+ goto vim_str2nr_bin;
+ }
+ // Detect octal number: zero followed by octal digits without '8' or '9'
+ pre = 0;
+ if (!(what & STR2NR_OCT)) {
+ goto vim_str2nr_dec;
+ }
+ for (int i = 2; !STRING_ENDED(ptr + i) && ascii_isdigit(ptr[i]); i++) {
+ if (ptr[i] > '7') {
+ goto vim_str2nr_dec;
+ }
+ }
+ pre = '0';
+ goto vim_str2nr_oct;
+ } else {
+ goto vim_str2nr_dec;
+ }
+
+ // Do the string-to-numeric conversion "manually" to avoid sscanf quirks.
+ assert(false); // Should’ve used goto earlier.
+#define PARSE_NUMBER(base, cond, conv) \
+ do { \
+ while (!STRING_ENDED(ptr) && (cond)) { \
+ /* avoid ubsan error for overflow */ \
+ if (un < UVARNUMBER_MAX / base) { \
+ un = base * un + (uvarnumber_T)(conv); \
+ } else { \
+ un = UVARNUMBER_MAX; \
+ } \
+ ptr++; \
+ } \
+ } while (0)
+ switch (pre) {
+ case 'b':
+ case 'B': {
+vim_str2nr_bin:
+ PARSE_NUMBER(2, (*ptr == '0' || *ptr == '1'), (*ptr - '0'));
+ break;
+ }
+ case '0': {
+vim_str2nr_oct:
+ PARSE_NUMBER(8, ('0' <= *ptr && *ptr <= '7'), (*ptr - '0'));
+ break;
+ }
+ case 0: {
+vim_str2nr_dec:
+ PARSE_NUMBER(10, (ascii_isdigit(*ptr)), (*ptr - '0'));
+ break;
+ }
+ case 'x':
+ case 'X': {
+vim_str2nr_hex:
+ PARSE_NUMBER(16, (ascii_isxdigit(*ptr)), (hex2nr(*ptr)));
+ break;
+ }
+ }
+#undef PARSE_NUMBER
+
+ if (prep != NULL) {
+ *prep = pre;
+ }
+
+ if (len != NULL) {
+ *len = (int)(ptr - (const char *)start);
+ }
+
+ if (nptr != NULL) {
+ if (negative) { // account for leading '-' for decimal numbers
+ // avoid ubsan error for overflow
+ if (un > VARNUMBER_MAX) {
+ *nptr = VARNUMBER_MIN;
+ } else {
+ *nptr = -(varnumber_T)un;
+ }
+ } else {
+ if (un > VARNUMBER_MAX) {
+ un = VARNUMBER_MAX;
+ }
+ *nptr = (varnumber_T)un;
+ }
+ }
+
+ if (unptr != NULL) {
+ *unptr = un;
+ }
+#undef STRING_ENDED
+}
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/keymap.c b/test/symbolic/klee/nvim/keymap.c
new file mode 100644
index 0000000000..a341a73689
--- /dev/null
+++ b/test/symbolic/klee/nvim/keymap.c
@@ -0,0 +1,539 @@
+#include <stdbool.h>
+
+#include "nvim/types.h"
+#include "nvim/keymap.h"
+#include "nvim/ascii.h"
+#include "nvim/eval/typval.h"
+
+#define MOD_KEYS_ENTRY_SIZE 5
+
+static char_u modifier_keys_table[] =
+{
+ MOD_MASK_SHIFT, '&', '9', '@', '1',
+ MOD_MASK_SHIFT, '&', '0', '@', '2',
+ MOD_MASK_SHIFT, '*', '1', '@', '4',
+ MOD_MASK_SHIFT, '*', '2', '@', '5',
+ MOD_MASK_SHIFT, '*', '3', '@', '6',
+ MOD_MASK_SHIFT, '*', '4', 'k', 'D',
+ MOD_MASK_SHIFT, '*', '5', 'k', 'L',
+ MOD_MASK_SHIFT, '*', '7', '@', '7',
+ MOD_MASK_CTRL, KS_EXTRA, (int)KE_C_END, '@', '7',
+ MOD_MASK_SHIFT, '*', '9', '@', '9',
+ MOD_MASK_SHIFT, '*', '0', '@', '0',
+ MOD_MASK_SHIFT, '#', '1', '%', '1',
+ MOD_MASK_SHIFT, '#', '2', 'k', 'h',
+ MOD_MASK_CTRL, KS_EXTRA, (int)KE_C_HOME, 'k', 'h',
+ MOD_MASK_SHIFT, '#', '3', 'k', 'I',
+ MOD_MASK_SHIFT, '#', '4', 'k', 'l',
+ MOD_MASK_CTRL, KS_EXTRA, (int)KE_C_LEFT, 'k', 'l',
+ MOD_MASK_SHIFT, '%', 'a', '%', '3',
+ MOD_MASK_SHIFT, '%', 'b', '%', '4',
+ MOD_MASK_SHIFT, '%', 'c', '%', '5',
+ MOD_MASK_SHIFT, '%', 'd', '%', '7',
+ MOD_MASK_SHIFT, '%', 'e', '%', '8',
+ MOD_MASK_SHIFT, '%', 'f', '%', '9',
+ MOD_MASK_SHIFT, '%', 'g', '%', '0',
+ MOD_MASK_SHIFT, '%', 'h', '&', '3',
+ MOD_MASK_SHIFT, '%', 'i', 'k', 'r',
+ MOD_MASK_CTRL, KS_EXTRA, (int)KE_C_RIGHT, 'k', 'r',
+ MOD_MASK_SHIFT, '%', 'j', '&', '5',
+ MOD_MASK_SHIFT, '!', '1', '&', '6',
+ MOD_MASK_SHIFT, '!', '2', '&', '7',
+ MOD_MASK_SHIFT, '!', '3', '&', '8',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_UP, 'k', 'u',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_DOWN, 'k', 'd',
+
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_XF1, KS_EXTRA, (int)KE_XF1,
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_XF2, KS_EXTRA, (int)KE_XF2,
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_XF3, KS_EXTRA, (int)KE_XF3,
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_XF4, KS_EXTRA, (int)KE_XF4,
+
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F1, 'k', '1',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F2, 'k', '2',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F3, 'k', '3',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F4, 'k', '4',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F5, 'k', '5',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F6, 'k', '6',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F7, 'k', '7',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F8, 'k', '8',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F9, 'k', '9',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F10, 'k', ';',
+
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F11, 'F', '1',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F12, 'F', '2',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F13, 'F', '3',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F14, 'F', '4',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F15, 'F', '5',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F16, 'F', '6',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F17, 'F', '7',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F18, 'F', '8',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F19, 'F', '9',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F20, 'F', 'A',
+
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F21, 'F', 'B',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F22, 'F', 'C',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F23, 'F', 'D',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F24, 'F', 'E',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F25, 'F', 'F',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F26, 'F', 'G',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F27, 'F', 'H',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F28, 'F', 'I',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F29, 'F', 'J',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F30, 'F', 'K',
+
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F31, 'F', 'L',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F32, 'F', 'M',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F33, 'F', 'N',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F34, 'F', 'O',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F35, 'F', 'P',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F36, 'F', 'Q',
+ MOD_MASK_SHIFT, KS_EXTRA, (int)KE_S_F37, 'F', 'R',
+
+ MOD_MASK_SHIFT, 'k', 'B', KS_EXTRA, (int)KE_TAB,
+
+ NUL
+};
+
+int simplify_key(const int key, int *modifiers)
+{
+ if (*modifiers & (MOD_MASK_SHIFT | MOD_MASK_CTRL | MOD_MASK_ALT)) {
+ // TAB is a special case.
+ if (key == TAB && (*modifiers & MOD_MASK_SHIFT)) {
+ *modifiers &= ~MOD_MASK_SHIFT;
+ return K_S_TAB;
+ }
+ const int key0 = KEY2TERMCAP0(key);
+ const int key1 = KEY2TERMCAP1(key);
+ for (int i = 0; modifier_keys_table[i] != NUL; i += MOD_KEYS_ENTRY_SIZE) {
+ if (key0 == modifier_keys_table[i + 3]
+ && key1 == modifier_keys_table[i + 4]
+ && (*modifiers & modifier_keys_table[i])) {
+ *modifiers &= ~modifier_keys_table[i];
+ return TERMCAP2KEY(modifier_keys_table[i + 1],
+ modifier_keys_table[i + 2]);
+ }
+ }
+ }
+ return key;
+}
+
+int handle_x_keys(const int key)
+ FUNC_ATTR_CONST FUNC_ATTR_WARN_UNUSED_RESULT
+{
+ switch (key) {
+ case K_XUP: return K_UP;
+ case K_XDOWN: return K_DOWN;
+ case K_XLEFT: return K_LEFT;
+ case K_XRIGHT: return K_RIGHT;
+ case K_XHOME: return K_HOME;
+ case K_ZHOME: return K_HOME;
+ case K_XEND: return K_END;
+ case K_ZEND: return K_END;
+ case K_XF1: return K_F1;
+ case K_XF2: return K_F2;
+ case K_XF3: return K_F3;
+ case K_XF4: return K_F4;
+ case K_S_XF1: return K_S_F1;
+ case K_S_XF2: return K_S_F2;
+ case K_S_XF3: return K_S_F3;
+ case K_S_XF4: return K_S_F4;
+ }
+ return key;
+}
+
+static const struct key_name_entry {
+ int key; // Special key code or ascii value
+ const char *name; // Name of key
+} key_names_table[] = {
+ { ' ', "Space" },
+ { TAB, "Tab" },
+ { K_TAB, "Tab" },
+ { NL, "NL" },
+ { NL, "NewLine" }, // Alternative name
+ { NL, "LineFeed" }, // Alternative name
+ { NL, "LF" }, // Alternative name
+ { CAR, "CR" },
+ { CAR, "Return" }, // Alternative name
+ { CAR, "Enter" }, // Alternative name
+ { K_BS, "BS" },
+ { K_BS, "BackSpace" }, // Alternative name
+ { ESC, "Esc" },
+ { CSI, "CSI" },
+ { K_CSI, "xCSI" },
+ { '|', "Bar" },
+ { '\\', "Bslash" },
+ { K_DEL, "Del" },
+ { K_DEL, "Delete" }, // Alternative name
+ { K_KDEL, "kDel" },
+ { K_UP, "Up" },
+ { K_DOWN, "Down" },
+ { K_LEFT, "Left" },
+ { K_RIGHT, "Right" },
+ { K_XUP, "xUp" },
+ { K_XDOWN, "xDown" },
+ { K_XLEFT, "xLeft" },
+ { K_XRIGHT, "xRight" },
+
+ { K_F1, "F1" },
+ { K_F2, "F2" },
+ { K_F3, "F3" },
+ { K_F4, "F4" },
+ { K_F5, "F5" },
+ { K_F6, "F6" },
+ { K_F7, "F7" },
+ { K_F8, "F8" },
+ { K_F9, "F9" },
+ { K_F10, "F10" },
+
+ { K_F11, "F11" },
+ { K_F12, "F12" },
+ { K_F13, "F13" },
+ { K_F14, "F14" },
+ { K_F15, "F15" },
+ { K_F16, "F16" },
+ { K_F17, "F17" },
+ { K_F18, "F18" },
+ { K_F19, "F19" },
+ { K_F20, "F20" },
+
+ { K_F21, "F21" },
+ { K_F22, "F22" },
+ { K_F23, "F23" },
+ { K_F24, "F24" },
+ { K_F25, "F25" },
+ { K_F26, "F26" },
+ { K_F27, "F27" },
+ { K_F28, "F28" },
+ { K_F29, "F29" },
+ { K_F30, "F30" },
+
+ { K_F31, "F31" },
+ { K_F32, "F32" },
+ { K_F33, "F33" },
+ { K_F34, "F34" },
+ { K_F35, "F35" },
+ { K_F36, "F36" },
+ { K_F37, "F37" },
+
+ { K_XF1, "xF1" },
+ { K_XF2, "xF2" },
+ { K_XF3, "xF3" },
+ { K_XF4, "xF4" },
+
+ { K_HELP, "Help" },
+ { K_UNDO, "Undo" },
+ { K_INS, "Insert" },
+ { K_INS, "Ins" }, // Alternative name
+ { K_KINS, "kInsert" },
+ { K_HOME, "Home" },
+ { K_KHOME, "kHome" },
+ { K_XHOME, "xHome" },
+ { K_ZHOME, "zHome" },
+ { K_END, "End" },
+ { K_KEND, "kEnd" },
+ { K_XEND, "xEnd" },
+ { K_ZEND, "zEnd" },
+ { K_PAGEUP, "PageUp" },
+ { K_PAGEDOWN, "PageDown" },
+ { K_KPAGEUP, "kPageUp" },
+ { K_KPAGEDOWN, "kPageDown" },
+
+ { K_KPLUS, "kPlus" },
+ { K_KMINUS, "kMinus" },
+ { K_KDIVIDE, "kDivide" },
+ { K_KMULTIPLY, "kMultiply" },
+ { K_KENTER, "kEnter" },
+ { K_KPOINT, "kPoint" },
+
+ { K_K0, "k0" },
+ { K_K1, "k1" },
+ { K_K2, "k2" },
+ { K_K3, "k3" },
+ { K_K4, "k4" },
+ { K_K5, "k5" },
+ { K_K6, "k6" },
+ { K_K7, "k7" },
+ { K_K8, "k8" },
+ { K_K9, "k9" },
+
+ { '<', "lt" },
+
+ { K_MOUSE, "Mouse" },
+ { K_LEFTMOUSE, "LeftMouse" },
+ { K_LEFTMOUSE_NM, "LeftMouseNM" },
+ { K_LEFTDRAG, "LeftDrag" },
+ { K_LEFTRELEASE, "LeftRelease" },
+ { K_LEFTRELEASE_NM, "LeftReleaseNM" },
+ { K_MIDDLEMOUSE, "MiddleMouse" },
+ { K_MIDDLEDRAG, "MiddleDrag" },
+ { K_MIDDLERELEASE, "MiddleRelease" },
+ { K_RIGHTMOUSE, "RightMouse" },
+ { K_RIGHTDRAG, "RightDrag" },
+ { K_RIGHTRELEASE, "RightRelease" },
+ { K_MOUSEDOWN, "ScrollWheelUp" },
+ { K_MOUSEUP, "ScrollWheelDown" },
+ { K_MOUSELEFT, "ScrollWheelRight" },
+ { K_MOUSERIGHT, "ScrollWheelLeft" },
+ { K_MOUSEDOWN, "MouseDown" }, // OBSOLETE: Use
+ { K_MOUSEUP, "MouseUp" }, // ScrollWheelXXX instead
+ { K_X1MOUSE, "X1Mouse" },
+ { K_X1DRAG, "X1Drag" },
+ { K_X1RELEASE, "X1Release" },
+ { K_X2MOUSE, "X2Mouse" },
+ { K_X2DRAG, "X2Drag" },
+ { K_X2RELEASE, "X2Release" },
+ { K_DROP, "Drop" },
+ { K_ZERO, "Nul" },
+ { K_SNR, "SNR" },
+ { K_PLUG, "Plug" },
+ { K_PASTE, "Paste" },
+ { 0, NULL }
+};
+
+int get_special_key_code(const char_u *name)
+{
+ for (int i = 0; key_names_table[i].name != NULL; i++) {
+ const char *const table_name = key_names_table[i].name;
+ int j;
+ for (j = 0; ascii_isident(name[j]) && table_name[j] != NUL; j++) {
+ if (TOLOWER_ASC(table_name[j]) != TOLOWER_ASC(name[j])) {
+ break;
+ }
+ }
+ if (!ascii_isident(name[j]) && table_name[j] == NUL) {
+ return key_names_table[i].key;
+ }
+ }
+
+ return 0;
+}
+
+
+static const struct modmasktable {
+ short mod_mask; ///< Bit-mask for particular key modifier.
+ short mod_flag; ///< Bit(s) for particular key modifier.
+ char_u name; ///< Single letter name of modifier.
+} mod_mask_table[] = {
+ {MOD_MASK_ALT, MOD_MASK_ALT, (char_u)'M'},
+ {MOD_MASK_META, MOD_MASK_META, (char_u)'T'},
+ {MOD_MASK_CTRL, MOD_MASK_CTRL, (char_u)'C'},
+ {MOD_MASK_SHIFT, MOD_MASK_SHIFT, (char_u)'S'},
+ {MOD_MASK_MULTI_CLICK, MOD_MASK_2CLICK, (char_u)'2'},
+ {MOD_MASK_MULTI_CLICK, MOD_MASK_3CLICK, (char_u)'3'},
+ {MOD_MASK_MULTI_CLICK, MOD_MASK_4CLICK, (char_u)'4'},
+ {MOD_MASK_CMD, MOD_MASK_CMD, (char_u)'D'},
+ // 'A' must be the last one
+ {MOD_MASK_ALT, MOD_MASK_ALT, (char_u)'A'},
+ {0, 0, NUL}
+};
+
+int name_to_mod_mask(int c)
+{
+ c = TOUPPER_ASC(c);
+ for (size_t i = 0; mod_mask_table[i].mod_mask != 0; i++) {
+ if (c == mod_mask_table[i].name) {
+ return mod_mask_table[i].mod_flag;
+ }
+ }
+ return 0;
+}
+
+static int extract_modifiers(int key, int *modp)
+{
+ int modifiers = *modp;
+
+ if (!(modifiers & MOD_MASK_CMD)) { // Command-key is special
+ if ((modifiers & MOD_MASK_SHIFT) && ASCII_ISALPHA(key)) {
+ key = TOUPPER_ASC(key);
+ modifiers &= ~MOD_MASK_SHIFT;
+ }
+ }
+ if ((modifiers & MOD_MASK_CTRL)
+ && ((key >= '?' && key <= '_') || ASCII_ISALPHA(key))) {
+ key = Ctrl_chr(key);
+ modifiers &= ~MOD_MASK_CTRL;
+ if (key == 0) { // <C-@> is <Nul>
+ key = K_ZERO;
+ }
+ }
+
+ *modp = modifiers;
+ return key;
+}
+
+int find_special_key(const char_u **srcp, const size_t src_len, int *const modp,
+ const bool keycode, const bool keep_x_key,
+ const bool in_string)
+{
+ const char_u *last_dash;
+ const char_u *end_of_name;
+ const char_u *src;
+ const char_u *bp;
+ const char_u *const end = *srcp + src_len - 1;
+ int modifiers;
+ int bit;
+ int key;
+ uvarnumber_T n;
+ int l;
+
+ if (src_len == 0) {
+ return 0;
+ }
+
+ src = *srcp;
+ if (src[0] != '<') {
+ return 0;
+ }
+
+ // Find end of modifier list
+ last_dash = src;
+ for (bp = src + 1; bp <= end && (*bp == '-' || ascii_isident(*bp)); bp++) {
+ if (*bp == '-') {
+ last_dash = bp;
+ if (bp + 1 <= end) {
+ l = utfc_ptr2len_len(bp + 1, (int)(end - bp) + 1);
+ // Anything accepted, like <C-?>.
+ // <C-"> or <M-"> are not special in strings as " is
+ // the string delimiter. With a backslash it works: <M-\">
+ if (end - bp > l && !(in_string && bp[1] == '"') && bp[2] == '>') {
+ bp += l;
+ } else if (end - bp > 2 && in_string && bp[1] == '\\'
+ && bp[2] == '"' && bp[3] == '>') {
+ bp += 2;
+ }
+ }
+ }
+ if (end - bp > 3 && bp[0] == 't' && bp[1] == '_') {
+ bp += 3; // skip t_xx, xx may be '-' or '>'
+ } else if (end - bp > 4 && STRNICMP(bp, "char-", 5) == 0) {
+ vim_str2nr(bp + 5, NULL, &l, STR2NR_ALL, NULL, NULL, 0);
+ bp += l + 5;
+ break;
+ }
+ }
+
+ if (bp <= end && *bp == '>') { // found matching '>'
+ end_of_name = bp + 1;
+
+ /* Which modifiers are given? */
+ modifiers = 0x0;
+ for (bp = src + 1; bp < last_dash; bp++) {
+ if (*bp != '-') {
+ bit = name_to_mod_mask(*bp);
+ if (bit == 0x0) {
+ break; // Illegal modifier name
+ }
+ modifiers |= bit;
+ }
+ }
+
+ // Legal modifier name.
+ if (bp >= last_dash) {
+ if (STRNICMP(last_dash + 1, "char-", 5) == 0
+ && ascii_isdigit(last_dash[6])) {
+ // <Char-123> or <Char-033> or <Char-0x33>
+ vim_str2nr(last_dash + 6, NULL, NULL, STR2NR_ALL, NULL, &n, 0);
+ key = (int)n;
+ } else {
+ int off = 1;
+
+ // Modifier with single letter, or special key name.
+ if (in_string && last_dash[1] == '\\' && last_dash[2] == '"') {
+ off = 2;
+ }
+ l = mb_ptr2len(last_dash + 1);
+ if (modifiers != 0 && last_dash[l + 1] == '>') {
+ key = PTR2CHAR(last_dash + off);
+ } else {
+ key = get_special_key_code(last_dash + off);
+ if (!keep_x_key) {
+ key = handle_x_keys(key);
+ }
+ }
+ }
+
+ // get_special_key_code() may return NUL for invalid
+ // special key name.
+ if (key != NUL) {
+ // Only use a modifier when there is no special key code that
+ // includes the modifier.
+ key = simplify_key(key, &modifiers);
+
+ if (!keycode) {
+ // don't want keycode, use single byte code
+ if (key == K_BS) {
+ key = BS;
+ } else if (key == K_DEL || key == K_KDEL) {
+ key = DEL;
+ }
+ }
+
+ // Normal Key with modifier:
+ // Try to make a single byte code (except for Alt/Meta modifiers).
+ if (!IS_SPECIAL(key)) {
+ key = extract_modifiers(key, &modifiers);
+ }
+
+ *modp = modifiers;
+ *srcp = end_of_name;
+ return key;
+ }
+ }
+ }
+ return 0;
+}
+
+char_u *add_char2buf(int c, char_u *s)
+{
+ char_u temp[MB_MAXBYTES + 1];
+ const int len = utf_char2bytes(c, temp);
+ for (int i = 0; i < len; ++i) {
+ c = temp[i];
+ // Need to escape K_SPECIAL and CSI like in the typeahead buffer.
+ if (c == K_SPECIAL) {
+ *s++ = K_SPECIAL;
+ *s++ = KS_SPECIAL;
+ *s++ = KE_FILLER;
+ } else {
+ *s++ = c;
+ }
+ }
+ return s;
+}
+
+unsigned int trans_special(const char_u **srcp, const size_t src_len,
+ char_u *const dst, const bool keycode,
+ const bool in_string)
+{
+ int modifiers = 0;
+ int key;
+ unsigned int dlen = 0;
+
+ key = find_special_key(srcp, src_len, &modifiers, keycode, false, in_string);
+ if (key == 0) {
+ return 0;
+ }
+
+ // Put the appropriate modifier in a string.
+ if (modifiers != 0) {
+ dst[dlen++] = K_SPECIAL;
+ dst[dlen++] = KS_MODIFIER;
+ dst[dlen++] = (char_u)modifiers;
+ }
+
+ if (IS_SPECIAL(key)) {
+ dst[dlen++] = K_SPECIAL;
+ dst[dlen++] = (char_u)KEY2TERMCAP0(key);
+ dst[dlen++] = KEY2TERMCAP1(key);
+ } else if (has_mbyte && !keycode) {
+ dlen += (unsigned int)(*mb_char2bytes)(key, dst + dlen);
+ } else if (keycode) {
+ char_u *after = add_char2buf(key, dst + dlen);
+ assert(after >= dst && (uintmax_t)(after - dst) <= UINT_MAX);
+ dlen = (unsigned int)(after - dst);
+ } else {
+ dst[dlen++] = (char_u)key;
+ }
+
+ return dlen;
+}
diff --git a/test/symbolic/klee/nvim/mbyte.c b/test/symbolic/klee/nvim/mbyte.c
new file mode 100644
index 0000000000..f98a531206
--- /dev/null
+++ b/test/symbolic/klee/nvim/mbyte.c
@@ -0,0 +1,266 @@
+#include <stddef.h>
+#include <inttypes.h>
+#include <assert.h>
+#include <stdbool.h>
+
+#include "nvim/types.h"
+#include "nvim/mbyte.h"
+#include "nvim/ascii.h"
+
+const uint8_t utf8len_tab_zero[] = {
+ //1 2 3 4 5 6 7 8 9 A B C D E F 0 1 2 3 4 5 6 7 8 9 A B C D E F
+ 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, // 0
+ 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, // 2
+ 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, // 4
+ 1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1, // 6
+ 0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0, // 8
+ 0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0, // A
+ 2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2, // C
+ 3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,4,4,4,4,4,4,4,4,5,5,5,5,6,6,0,0, // E
+};
+
+const uint8_t utf8len_tab[] = {
+ // ?1 ?2 ?3 ?4 ?5 ?6 ?7 ?8 ?9 ?A ?B ?C ?D ?E ?F
+ 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, // 0?
+ 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, // 1?
+ 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, // 2?
+ 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, // 3?
+ 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, // 4?
+ 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, // 5?
+ 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, // 6?
+ 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, // 7?
+ 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, // 8?
+ 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, // 9?
+ 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, // A?
+ 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, // B?
+ 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, // C?
+ 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, // D?
+ 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, // E?
+ 4, 4, 4, 4, 4, 4, 4, 4, 5, 5, 5, 5, 6, 6, 1, 1, // F?
+};
+
+int utf_ptr2char(const char_u *const p)
+{
+ if (p[0] < 0x80) { // Be quick for ASCII.
+ return p[0];
+ }
+
+ const uint8_t len = utf8len_tab_zero[p[0]];
+ if (len > 1 && (p[1] & 0xc0) == 0x80) {
+ if (len == 2) {
+ return ((p[0] & 0x1f) << 6) + (p[1] & 0x3f);
+ }
+ if ((p[2] & 0xc0) == 0x80) {
+ if (len == 3) {
+ return (((p[0] & 0x0f) << 12) + ((p[1] & 0x3f) << 6)
+ + (p[2] & 0x3f));
+ }
+ if ((p[3] & 0xc0) == 0x80) {
+ if (len == 4) {
+ return (((p[0] & 0x07) << 18) + ((p[1] & 0x3f) << 12)
+ + ((p[2] & 0x3f) << 6) + (p[3] & 0x3f));
+ }
+ if ((p[4] & 0xc0) == 0x80) {
+ if (len == 5) {
+ return (((p[0] & 0x03) << 24) + ((p[1] & 0x3f) << 18)
+ + ((p[2] & 0x3f) << 12) + ((p[3] & 0x3f) << 6)
+ + (p[4] & 0x3f));
+ }
+ if ((p[5] & 0xc0) == 0x80 && len == 6) {
+ return (((p[0] & 0x01) << 30) + ((p[1] & 0x3f) << 24)
+ + ((p[2] & 0x3f) << 18) + ((p[3] & 0x3f) << 12)
+ + ((p[4] & 0x3f) << 6) + (p[5] & 0x3f));
+ }
+ }
+ }
+ }
+ }
+ // Illegal value: just return the first byte.
+ return p[0];
+}
+
+bool utf_composinglike(const char_u *p1, const char_u *p2)
+{
+ return false;
+}
+
+char_u *string_convert(const vimconv_T *conv, char_u *data, size_t *size)
+{
+ return NULL;
+}
+
+int utf_ptr2len_len(const char_u *p, int size)
+{
+ int len;
+ int i;
+ int m;
+
+ len = utf8len_tab[*p];
+ if (len == 1)
+ return 1; /* NUL, ascii or illegal lead byte */
+ if (len > size)
+ m = size; /* incomplete byte sequence. */
+ else
+ m = len;
+ for (i = 1; i < m; ++i)
+ if ((p[i] & 0xc0) != 0x80)
+ return 1;
+ return len;
+}
+
+int utfc_ptr2len_len(const char_u *p, int size)
+{
+ int len;
+ int prevlen;
+
+ if (size < 1 || *p == NUL)
+ return 0;
+ if (p[0] < 0x80 && (size == 1 || p[1] < 0x80)) /* be quick for ASCII */
+ return 1;
+
+ /* Skip over first UTF-8 char, stopping at a NUL byte. */
+ len = utf_ptr2len_len(p, size);
+
+ /* Check for illegal byte and incomplete byte sequence. */
+ if ((len == 1 && p[0] >= 0x80) || len > size)
+ return 1;
+
+ /*
+ * Check for composing characters. We can handle only the first six, but
+ * skip all of them (otherwise the cursor would get stuck).
+ */
+ prevlen = 0;
+ while (len < size) {
+ int len_next_char;
+
+ if (p[len] < 0x80)
+ break;
+
+ /*
+ * Next character length should not go beyond size to ensure that
+ * UTF_COMPOSINGLIKE(...) does not read beyond size.
+ */
+ len_next_char = utf_ptr2len_len(p + len, size - len);
+ if (len_next_char > size - len)
+ break;
+
+ if (!UTF_COMPOSINGLIKE(p + prevlen, p + len))
+ break;
+
+ /* Skip over composing char */
+ prevlen = len;
+ len += len_next_char;
+ }
+ return len;
+}
+
+int utf_char2len(const int c)
+{
+ if (c < 0x80) {
+ return 1;
+ } else if (c < 0x800) {
+ return 2;
+ } else if (c < 0x10000) {
+ return 3;
+ } else if (c < 0x200000) {
+ return 4;
+ } else if (c < 0x4000000) {
+ return 5;
+ } else {
+ return 6;
+ }
+}
+
+int utf_char2bytes(const int c, char_u *const buf)
+{
+ if (c < 0x80) { // 7 bits
+ buf[0] = c;
+ return 1;
+ } else if (c < 0x800) { // 11 bits
+ buf[0] = 0xc0 + ((unsigned)c >> 6);
+ buf[1] = 0x80 + (c & 0x3f);
+ return 2;
+ } else if (c < 0x10000) { // 16 bits
+ buf[0] = 0xe0 + ((unsigned)c >> 12);
+ buf[1] = 0x80 + (((unsigned)c >> 6) & 0x3f);
+ buf[2] = 0x80 + (c & 0x3f);
+ return 3;
+ } else if (c < 0x200000) { // 21 bits
+ buf[0] = 0xf0 + ((unsigned)c >> 18);
+ buf[1] = 0x80 + (((unsigned)c >> 12) & 0x3f);
+ buf[2] = 0x80 + (((unsigned)c >> 6) & 0x3f);
+ buf[3] = 0x80 + (c & 0x3f);
+ return 4;
+ } else if (c < 0x4000000) { // 26 bits
+ buf[0] = 0xf8 + ((unsigned)c >> 24);
+ buf[1] = 0x80 + (((unsigned)c >> 18) & 0x3f);
+ buf[2] = 0x80 + (((unsigned)c >> 12) & 0x3f);
+ buf[3] = 0x80 + (((unsigned)c >> 6) & 0x3f);
+ buf[4] = 0x80 + (c & 0x3f);
+ return 5;
+ } else { // 31 bits
+ buf[0] = 0xfc + ((unsigned)c >> 30);
+ buf[1] = 0x80 + (((unsigned)c >> 24) & 0x3f);
+ buf[2] = 0x80 + (((unsigned)c >> 18) & 0x3f);
+ buf[3] = 0x80 + (((unsigned)c >> 12) & 0x3f);
+ buf[4] = 0x80 + (((unsigned)c >> 6) & 0x3f);
+ buf[5] = 0x80 + (c & 0x3f);
+ return 6;
+ }
+}
+
+int utf_ptr2len(const char_u *const p)
+{
+ if (*p == NUL) {
+ return 0;
+ }
+ const int len = utf8len_tab[*p];
+ for (int i = 1; i < len; i++) {
+ if ((p[i] & 0xc0) != 0x80) {
+ return 1;
+ }
+ }
+ return len;
+}
+
+int utfc_ptr2len(const char_u *const p)
+{
+ uint8_t b0 = (uint8_t)(*p);
+
+ if (b0 == NUL) {
+ return 0;
+ }
+ if (b0 < 0x80 && p[1] < 0x80) { // be quick for ASCII
+ return 1;
+ }
+
+ // Skip over first UTF-8 char, stopping at a NUL byte.
+ int len = utf_ptr2len(p);
+
+ // Check for illegal byte.
+ if (len == 1 && b0 >= 0x80) {
+ return 1;
+ }
+
+ // Check for composing characters. We can handle only the first six, but
+ // skip all of them (otherwise the cursor would get stuck).
+ int prevlen = 0;
+ for (;;) {
+ if (p[len] < 0x80 || !UTF_COMPOSINGLIKE(p + prevlen, p + len)) {
+ return len;
+ }
+
+ // Skip over composing char.
+ prevlen = len;
+ len += utf_ptr2len(p + len);
+ }
+}
+
+void mb_copy_char(const char_u **fp, char_u **tp)
+{
+ const size_t l = utfc_ptr2len(*fp);
+
+ memmove(*tp, *fp, (size_t)l);
+ *tp += l;
+ *fp += l;
+}
diff --git a/test/symbolic/klee/nvim/memory.c b/test/symbolic/klee/nvim/memory.c
new file mode 100644
index 0000000000..df422cea3e
--- /dev/null
+++ b/test/symbolic/klee/nvim/memory.c
@@ -0,0 +1,101 @@
+#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;
+size_t ever_allocated_memory = 0;
+
+size_t allocated_memory_limit = SIZE_MAX;
+
+void *xmalloc(const size_t size)
+{
+ void *ret = malloc(size);
+ allocated_memory += size;
+ ever_allocated_memory += size;
+ assert(allocated_memory <= allocated_memory_limit);
+ assert(arecs_rb_length(&arecs) < RB_SIZE);
+ arecs_rb_push(&arecs, (AllocRecord) {
+ .ptr = ret,
+ .size = size,
+ });
+ return ret;
+}
+
+void xfree(void *const p)
+{
+ if (p == NULL) {
+ return;
+ }
+ 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;
+ if (new_size > arec->size) {
+ ever_allocated_memory += (new_size - arec->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..0234a935b5
--- /dev/null
+++ b/test/symbolic/klee/run.sh
@@ -0,0 +1,102 @@
+#!/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"
+
+help() {
+ echo "Usage:"
+ echo
+ echo " $0 -c fname"
+ echo " $0 fname"
+ echo " $0 -s"
+ echo
+ echo "First form compiles executable out of test/symbolic/klee/{fname}.c."
+ echo "Compiled executable is placed into build/klee/{fname}. Must first"
+ echo "successfully compile Neovim in order to generate declarations."
+ echo
+ echo "Second form runs KLEE in a docker container using file "
+ echo "test/symbolic/klee/{fname.c}. Bitcode is placed into build/klee/a.bc,"
+ echo "results are placed into build/klee/out/. The latter is first deleted if"
+ echo "it exists."
+ echo
+ echo "Third form runs ktest-tool which prints errors found by KLEE via "
+ echo "the same container used to run KLEE."
+}
+
+main() {
+ local compile=
+ local print_errs=
+ if test "$1" = "--help" ; then
+ help
+ return
+ fi
+ if test "$1" = "-s" ; then
+ print_errs=1
+ shift
+ elif test "$1" = "-c" ; then
+ compile=1
+ shift
+ fi
+ if test -z "$print_errs" ; then
+ local test="$1" ; shift
+ fi
+
+ 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
+ local line1='cd /image'
+ if test -z "$print_errs" ; then
+ test -d "$KLEE_OUT_DIR" && rm -r "$KLEE_OUT_DIR"
+
+ 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'"
+ fi
+ local line2="for t in '$KLEE_OUT_DIR'/*.err"
+ line2="$line2 ; do ktest-tool --write-ints"
+ line2="$line2 \"\$(printf '%s' \"\$t\" | sed -e 's@\\.[^/]*\$@.ktest@')\""
+ 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..ee7dc312e9
--- /dev/null
+++ b/test/symbolic/klee/viml_expressions_lexer.c
@@ -0,0 +1,105 @@
+#ifdef USE_KLEE
+# include <klee/klee.h>
+#else
+# include <string.h>
+# include <stdio.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/keymap.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;
+ int flags;
+ 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 <= (kELFlagPeek|kELFlagAllowFloat|kELFlagForbidEOC
+ |kELFlagForbidScope|kELFlagIsNotCmp));
+#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);
+
+ allocated_memory_limit = 0;
+ LexExprToken token = viml_pexpr_next_token(&pstate, flags);
+ if (flags & kELFlagPeek) {
+ assert(pstate.pos.line == 0 && pstate.pos.col == 0);
+ } else {
+ assert((pstate.pos.line == 0)
+ ? (pstate.pos.col > 0)
+ : (pstate.pos.line == 1 && pstate.pos.col == 0));
+ }
+ assert(allocated_memory == 0);
+ assert(ever_allocated_memory == 0);
+#ifndef USE_KLEE
+ fprintf(stderr, "tkn: %s\n", viml_pexpr_repr_token(&pstate, token, NULL));
+#endif
+}
diff --git a/test/symbolic/klee/viml_expressions_parser.c b/test/symbolic/klee/viml_expressions_parser.c
new file mode 100644
index 0000000000..9a876ed3fa
--- /dev/null
+++ b/test/symbolic/klee/viml_expressions_parser.c
@@ -0,0 +1,117 @@
+#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"
+#include "nvim/keymap.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;
+ unsigned 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|kExprFlagsParseLet));
+#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];
+
+ ParserHighlight colors;
+ kvi_init(colors);
+
+ ParserState pstate = {
+ .reader = {
+ .get_line = simple_get_line,
+ .cookie = &cur_pline,
+ .lines = KV_INITIAL_VALUE,
+ .conv.vc_type = CONV_NONE,
+ },
+ .pos = { 0, 0 },
+ .colors = &colors,
+ .can_continuate = false,
+ };
+ kvi_init(pstate.reader.lines);
+
+ const ExprAST ast = viml_pexpr_parse(&pstate, (int)flags);
+ assert(ast.root != NULL || ast.err.msg);
+ if (flags & kExprFlagsParseLet) {
+ assert(ast.err.msg != NULL
+ || ast.root->type == kExprNodeAssignment
+ || (ast.root->type == kExprNodeListLiteral
+ && ast.root->children != NULL)
+ || ast.root->type == kExprNodeComplexIdentifier
+ || ast.root->type == kExprNodeCurlyBracesIdentifier
+ || ast.root->type == kExprNodePlainIdentifier
+ || ast.root->type == kExprNodeRegister
+ || ast.root->type == kExprNodeEnvironment
+ || ast.root->type == kExprNodeOption
+ || ast.root->type == kExprNodeSubscript
+ || ast.root->type == kExprNodeConcatOrSubscript);
+ }
+ // Can’t possibly have more highlight tokens then there are bytes in string.
+ assert(kv_size(colors) <= INPUT_SIZE - shift);
+ kvi_destroy(colors);
+ // Not destroying pstate.reader.lines because there is no way it could exceed
+ // its limits in the current circumstances.
+ viml_pexpr_free_ast(ast);
+ assert(allocated_memory == 0);
+}
generated by cgit (git 2.34.1) at 2025-08-07 08:08:15 +0000