aboutsummaryrefslogtreecommitdiff
path: root/test/symbolic/klee/viml_expressions_parser.c
diff options
context:
space:
mode:
authorZyX <kp-pav@yandex.ru>2017-09-11 01:27:46 +0300
committerZyX <kp-pav@yandex.ru>2017-10-08 22:25:05 +0300
commit7c97f783935ec122fbf0d7d070c00804738abd6a (patch)
tree0ad3a1c319c04c02686c32b27ec725f4f7ded076 /test/symbolic/klee/viml_expressions_parser.c
parent430e516d3ac1235c1ee3009a8a36089bf278440e (diff)
downloadrneovim-7c97f783935ec122fbf0d7d070c00804738abd6a.tar.gz
rneovim-7c97f783935ec122fbf0d7d070c00804738abd6a.tar.bz2
rneovim-7c97f783935ec122fbf0d7d070c00804738abd6a.zip
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.
Diffstat (limited to 'test/symbolic/klee/viml_expressions_parser.c')
-rw-r--r--test/symbolic/klee/viml_expressions_parser.c102
1 files changed, 102 insertions, 0 deletions
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
+}