From 7c97f783935ec122fbf0d7d070c00804738abd6a Mon Sep 17 00:00:00 2001 From: ZyX Date: Mon, 11 Sep 2017 01:27:46 +0300 Subject: 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. --- test/symbolic/klee/viml_expressions_lexer.c | 86 +++++++++++++++++++++++++++++ 1 file changed, 86 insertions(+) create mode 100644 test/symbolic/klee/viml_expressions_lexer.c (limited to 'test/symbolic/klee/viml_expressions_lexer.c') 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 +#else +# include +#endif +#include +#include +#include + +#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)); +} -- cgit From 9fa8f7fc0a24371f7956450d840bdae8a2fc9a51 Mon Sep 17 00:00:00 2001 From: ZyX Date: Thu, 28 Sep 2017 00:40:25 +0300 Subject: viml/parser/expressions: Add a way to adjust lexer It also adds support for kExprLexOr which for some reason was forgotten. It was only made sure that KLEE test compiles in non-KLEE mode, not that something works or that KLEE is able to run tests. --- test/symbolic/klee/viml_expressions_lexer.c | 24 +++++++++++++++++++----- 1 file changed, 19 insertions(+), 5 deletions(-) (limited to 'test/symbolic/klee/viml_expressions_lexer.c') diff --git a/test/symbolic/klee/viml_expressions_lexer.c b/test/symbolic/klee/viml_expressions_lexer.c index e3b5aa80cc..67f3eb7faa 100644 --- a/test/symbolic/klee/viml_expressions_lexer.c +++ b/test/symbolic/klee/viml_expressions_lexer.c @@ -34,13 +34,20 @@ int main(const int argc, const char *const *const argv, { char input[INPUT_SIZE]; uint8_t shift; - const bool peek = false; + 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[] = { @@ -79,8 +86,15 @@ int main(const int argc, const char *const *const argv, }; 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)); + 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); } -- cgit From 163792e9b9854fe046ada3233dec0fd0f6c55737 Mon Sep 17 00:00:00 2001 From: ZyX Date: Fri, 6 Oct 2017 01:19:43 +0300 Subject: viml/parser/expressions: Make lexer parse numbers, support non-decimal --- test/symbolic/klee/viml_expressions_lexer.c | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'test/symbolic/klee/viml_expressions_lexer.c') diff --git a/test/symbolic/klee/viml_expressions_lexer.c b/test/symbolic/klee/viml_expressions_lexer.c index 67f3eb7faa..cddc1cb2f1 100644 --- a/test/symbolic/klee/viml_expressions_lexer.c +++ b/test/symbolic/klee/viml_expressions_lexer.c @@ -2,6 +2,7 @@ # include #else # include +# include #endif #include #include @@ -56,7 +57,7 @@ int main(const int argc, const char *const *const argv, .data = &input[shift], .size = sizeof(input) - shift, #else - .data = (const char *)&argv[1], + .data = (const char *)argv[1], .size = strlen(argv[1]), #endif .allocated = false, @@ -97,4 +98,7 @@ int main(const int argc, const char *const *const argv, } 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 } -- cgit From fa3cfc0dd54df125a1dbabccda47a5f45dc483ae Mon Sep 17 00:00:00 2001 From: ZyX Date: Mon, 9 Oct 2017 02:55:56 +0300 Subject: viml/parser/expressions: Finish parser MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Note: formatc.lua was unable to swallow some newer additions to ExprASTNodeType (specifically `kExprNodeOr = '|'` and probably something else), so all `= …` were dropped: in any case they only were there in order to not bother updating viml_pexpr_debug_print_ast_node and since it is now known all nodes which will be present it is not much of an issue. --- test/symbolic/klee/viml_expressions_lexer.c | 1 + 1 file changed, 1 insertion(+) (limited to 'test/symbolic/klee/viml_expressions_lexer.c') diff --git a/test/symbolic/klee/viml_expressions_lexer.c b/test/symbolic/klee/viml_expressions_lexer.c index cddc1cb2f1..ee7dc312e9 100644 --- a/test/symbolic/klee/viml_expressions_lexer.c +++ b/test/symbolic/klee/viml_expressions_lexer.c @@ -17,6 +17,7 @@ #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 -- cgit