diff options
| -rw-r--r-- | include/expr/Parser.h | 5 | ||||
| -rw-r--r-- | lib/Expr/Parser.cpp | 37 | ||||
| -rw-r--r-- | runtime/POSIX/fd.h | 6 | ||||
| -rw-r--r-- | runtime/POSIX/fd_init.c | 10 | ||||
| -rw-r--r-- | runtime/POSIX/klee_init_env.c | 28 | ||||
| -rw-r--r-- | test/Runtime/POSIX/FD_Fail2.c | 5 | ||||
| -rw-r--r-- | test/Runtime/POSIX/Isatty.c | 2 | ||||
| -rw-r--r-- | test/Runtime/POSIX/Stdin.c | 2 | ||||
| -rw-r--r-- | test/Solver/2016-04-12-array-parsing-bug.kquery | 227 | ||||
| -rw-r--r-- | tools/kleaver/main.cpp | 13 |
10 files changed, 290 insertions, 45 deletions
diff --git a/include/expr/Parser.h b/include/expr/Parser.h index d2135f12..a9133e9d 100644 --- a/include/expr/Parser.h +++ b/include/expr/Parser.h @@ -228,9 +228,8 @@ namespace expr { /// \arg MB - The input data. /// \arg Builder - The expression builder to use for constructing /// expressions. - static Parser *Create(const std::string Name, - const llvm::MemoryBuffer *MB, - ExprBuilder *Builder); + static Parser *Create(const std::string Name, const llvm::MemoryBuffer *MB, + ExprBuilder *Builder, bool ClearArrayAfterQuery); }; } } diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index e914cb80..572b9572 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -111,6 +111,7 @@ namespace { const MemoryBuffer *TheMemoryBuffer; ExprBuilder *Builder; ArrayCache TheArrayCache; + bool ClearArrayAfterQuery; Lexer TheLexer; unsigned MaxErrors; @@ -322,14 +323,11 @@ namespace { void Error(const char *Message) { Error(Message, Tok); } public: - ParserImpl(const std::string _Filename, - const MemoryBuffer *MB, - ExprBuilder *_Builder) : Filename(_Filename), - TheMemoryBuffer(MB), - Builder(_Builder), - TheLexer(MB), - MaxErrors(~0u), - NumErrors(0) {} + ParserImpl(const std::string _Filename, const MemoryBuffer *MB, + ExprBuilder *_Builder, bool _ClearArrayAfterQuery) + : Filename(_Filename), TheMemoryBuffer(MB), Builder(_Builder), + ClearArrayAfterQuery(_ClearArrayAfterQuery), TheLexer(MB), + MaxErrors(~0u), NumErrors(0) {} virtual ~ParserImpl(); @@ -492,9 +490,9 @@ DeclResult ParserImpl::ParseArrayDecl() { Values.clear(); } - for (unsigned i = 0; i != Size.get(); ++i) { - // FIXME: Must be constant expression. - } + // for (unsigned i = 0; i != Size.get(); ++i) { + // TODO: Check: Must be constant expression. + //} } // FIXME: Validate that size makes sense for domain type. @@ -532,7 +530,7 @@ DeclResult ParserImpl::ParseArrayDecl() { ArrayDecl *AD = new ArrayDecl(Label, Size.get(), DomainType.get(), RangeType.get(), Root); - ArraySymTab.insert(std::make_pair(Label, AD)); + ArraySymTab[Label] = AD; // Create the initial version reference. VersionSymTab.insert(std::make_pair(Label, @@ -681,7 +679,13 @@ DeclResult ParserImpl::ParseQueryCommand() { exit: if (Tok.kind != Token::EndOfFile) - ExpectRParen("unexpected argument to 'query'."); + ExpectRParen("unexpected argument to 'query'."); + + // If we assume that the queries are independent, we clear the array + // table from the previous declarations + if (ClearArrayAfterQuery) + ArraySymTab.clear(); + return new QueryCommand(Constraints, Res.get(), Values, Objects); } @@ -1641,10 +1645,9 @@ Parser::Parser() { Parser::~Parser() { } -Parser *Parser::Create(const std::string Filename, - const MemoryBuffer *MB, - ExprBuilder *Builder) { - ParserImpl *P = new ParserImpl(Filename, MB, Builder); +Parser *Parser::Create(const std::string Filename, const MemoryBuffer *MB, + ExprBuilder *Builder, bool ClearArrayAfterQuery) { + ParserImpl *P = new ParserImpl(Filename, MB, Builder, ClearArrayAfterQuery); P->Initialize(); return P; } diff --git a/runtime/POSIX/fd.h b/runtime/POSIX/fd.h index cb86295c..4a6fbc15 100644 --- a/runtime/POSIX/fd.h +++ b/runtime/POSIX/fd.h @@ -71,9 +71,9 @@ typedef struct { extern exe_file_system_t __exe_fs; extern exe_sym_env_t __exe_env; -void klee_init_fds(unsigned n_files, unsigned file_length, - int sym_stdout_flag, int do_all_writes_flag, - unsigned max_failures); +void klee_init_fds(unsigned n_files, unsigned file_length, + unsigned stdin_length, int sym_stdout_flag, + int do_all_writes_flag, unsigned max_failures); void klee_init_env(int *argcPtr, char ***argvPtr); /* *** */ diff --git a/runtime/POSIX/fd_init.c b/runtime/POSIX/fd_init.c index 8b69fd04..9184b7ea 100644 --- a/runtime/POSIX/fd_init.c +++ b/runtime/POSIX/fd_init.c @@ -107,9 +107,9 @@ static unsigned __sym_uint32(const char *name) { writes past the initial file size are discarded (file offset is always incremented) max_failures: maximum number of system call failures */ -void klee_init_fds(unsigned n_files, unsigned file_length, - int sym_stdout_flag, int save_all_writes_flag, - unsigned max_failures) { +void klee_init_fds(unsigned n_files, unsigned file_length, + unsigned stdin_length, int sym_stdout_flag, + int save_all_writes_flag, unsigned max_failures) { unsigned k; char name[7] = "?-data"; struct stat64 s; @@ -124,9 +124,9 @@ void klee_init_fds(unsigned n_files, unsigned file_length, } /* setting symbolic stdin */ - if (file_length) { + if (stdin_length) { __exe_fs.sym_stdin = malloc(sizeof(*__exe_fs.sym_stdin)); - __create_new_dfile(__exe_fs.sym_stdin, file_length, "stdin", &s); + __create_new_dfile(__exe_fs.sym_stdin, stdin_length, "stdin", &s); __exe_env.fds[0].dfile = __exe_fs.sym_stdin; } else __exe_fs.sym_stdin = NULL; diff --git a/runtime/POSIX/klee_init_env.c b/runtime/POSIX/klee_init_env.c index cbcf31f4..7ac9804c 100644 --- a/runtime/POSIX/klee_init_env.c +++ b/runtime/POSIX/klee_init_env.c @@ -90,6 +90,7 @@ void klee_init_env(int* argcPtr, char*** argvPtr) { char* new_argv[1024]; unsigned max_len, min_argvs, max_argvs; unsigned sym_files = 0, sym_file_len = 0; + unsigned sym_stdin_len = 0; int sym_stdout_flag = 0; int save_all_writes_flag = 0; int fd_fail = 0; @@ -102,15 +103,16 @@ void klee_init_env(int* argcPtr, char*** argvPtr) { // Recognize --help when it is the sole argument. if (argc == 2 && __streq(argv[1], "--help")) { - __emit_error("klee_init_env\n\n\ + __emit_error("klee_init_env\n\n\ usage: (klee_init_env) [options] [program arguments]\n\ -sym-arg <N> - Replace by a symbolic argument with length N\n\ -sym-args <MIN> <MAX> <N> - Replace by at least MIN arguments and at most\n\ MAX arguments, each with maximum length N\n\ - -sym-files <NUM> <N> - Make stdin and up to NUM symbolic files, each\n\ - with maximum size N.\n\ + -sym-files <NUM> <N> - Make NUM symbolic files ('A', 'B', 'C', etc.),\n\ + each with size N\n\ + -sym-stdin <N> - Make stdin symbolic with size N.\n\ -sym-stdout - Make stdout symbolic.\n\ - -max-fail <N> - Allow up to <N> injected failures\n\ + -max-fail <N> - Allow up to N injected failures\n\ -fd-fail - Shortcut for '-max-fail 1'\n\n"); } @@ -156,8 +158,17 @@ usage: (klee_init_env) [options] [program arguments]\n\ sym_files = __str_to_int(argv[k++], msg); sym_file_len = __str_to_int(argv[k++], msg); - } - else if (__streq(argv[k], "--sym-stdout") || __streq(argv[k], "-sym-stdout")) { + } else if (__streq(argv[k], "--sym-stdin") || + __streq(argv[k], "-sym-stdin")) { + const char *msg = + "--sym-stdin expects one integer argument <sym-stdin-len>"; + + if (++k == argc) + __emit_error(msg); + + sym_stdin_len = __str_to_int(argv[k++], msg); + } else if (__streq(argv[k], "--sym-stdout") || + __streq(argv[k], "-sym-stdout")) { sym_stdout_flag = 1; k++; } @@ -190,8 +201,7 @@ usage: (klee_init_env) [options] [program arguments]\n\ *argcPtr = new_argc; *argvPtr = final_argv; - klee_init_fds(sym_files, sym_file_len, - sym_stdout_flag, save_all_writes_flag, - fd_fail); + klee_init_fds(sym_files, sym_file_len, sym_stdin_len, sym_stdout_flag, + save_all_writes_flag, fd_fail); } diff --git a/test/Runtime/POSIX/FD_Fail2.c b/test/Runtime/POSIX/FD_Fail2.c index c2e5596b..9d7e358f 100644 --- a/test/Runtime/POSIX/FD_Fail2.c +++ b/test/Runtime/POSIX/FD_Fail2.c @@ -18,7 +18,8 @@ #include <sys/types.h> #include <sys/stat.h> #include <fcntl.h> -#include <stdio.h> +#include <string.h> +#include <unistd.h> int main(int argc, char** argv) { char buf[1024]; @@ -28,7 +29,7 @@ int main(int argc, char** argv) { int r; - r = read(fd, buf, 1, 5); + r = read(fd, buf, 5); if (r != -1) printf("read() succeeded %u\n", fd); else printf("read() failed with error '%s'\n", strerror(errno)); diff --git a/test/Runtime/POSIX/Isatty.c b/test/Runtime/POSIX/Isatty.c index 241c5cbb..fdfc6ceb 100644 --- a/test/Runtime/POSIX/Isatty.c +++ b/test/Runtime/POSIX/Isatty.c @@ -1,6 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --libc=uclibc --posix-runtime %t.bc --sym-files 0 10 --sym-stdout > %t.log 2>&1 +// RUN: %klee --output-dir=%t.klee-out --libc=uclibc --posix-runtime %t.bc --sym-stdin 10 --sym-stdout > %t.log 2>&1 // RUN: test -f %t.klee-out/test000001.ktest // RUN: test -f %t.klee-out/test000002.ktest // RUN: test -f %t.klee-out/test000003.ktest diff --git a/test/Runtime/POSIX/Stdin.c b/test/Runtime/POSIX/Stdin.c index ebf16405..09eed6d2 100644 --- a/test/Runtime/POSIX/Stdin.c +++ b/test/Runtime/POSIX/Stdin.c @@ -1,6 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 0 4 > %t.log +// RUN: %klee --output-dir=%t.klee-out --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-stdin 4 > %t.log // RUN: grep "mode:file" %t.log // RUN: grep "mode:dir" %t.log // RUN: grep "mode:chr" %t.log diff --git a/test/Solver/2016-04-12-array-parsing-bug.kquery b/test/Solver/2016-04-12-array-parsing-bug.kquery new file mode 100644 index 00000000..d53fa35f --- /dev/null +++ b/test/Solver/2016-04-12-array-parsing-bug.kquery @@ -0,0 +1,227 @@ +# RUN: %kleaver %s > %t +# RUN: %kleaver --clear-array-decls-after-query %s > %t + +array A-data[8] : w32 -> w8 = symbolic +array A-data-stat[144] : w32 -> w8 = symbolic +array arg0[3] : w32 -> w8 = symbolic +array arg1[3] : w32 -> w8 = symbolic +array const_arr1[768] : w32 -> w8 = [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 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 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 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 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 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 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 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 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 3 32 2 32 2 32 2 32 2 32 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 1 96 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 8 216 8 216 8 216 8 216 8 216 8 216 8 216 8 216 8 216 8 216 4 192 4 192 4 192 4 192 4 192 4 192 4 192 8 213 8 213 8 213 8 213 8 213 8 213 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 4 192 4 192 4 192 4 192 4 192 4 192 8 214 8 214 8 214 8 214 8 214 8 214 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 4 192 4 192 4 192 4 192 2 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 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 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 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 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 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 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 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 0] +array const_arr8[277] : w32 -> w8 = [0 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 2 2 2 2 2 2 2 2 2 2 2 24 2 2 25 2 2 2 2 2 2 2 2 2 2 23 2 2 2 2 2 22 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 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 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 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 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 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 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21] +array model_version[4] : w32 -> w8 = symbolic +array n_args[4] : w32 -> w8 = symbolic +array n_args_1[4] : w32 -> w8 = symbolic +array stdin[8] : w32 -> w8 = symbolic +array stdin-stat[144] : w32 -> w8 = symbolic +array stdout[1024] : w32 -> w8 = symbolic +array stdout-stat[144] : w32 -> w8 = symbolic +(query [(Ult N0:(ReadLSB w32 0 n_args) + 2) + (Eq false (Slt 0 N0)) + (Ult N1:(ReadLSB w32 0 n_args_1) + 3) + (Slt 0 N1) + (Slt 1 N1) + (Eq false + (Eq 0 + (And w64 (ReadLSB w64 8 A-data-stat) + 2147483647))) + (Ult (ReadLSB w64 56 A-data-stat) + 65536) + (Eq false + (Eq 0 + (And w64 (ReadLSB w64 8 stdin-stat) + 2147483647))) + (Ult (ReadLSB w64 56 stdin-stat) + 65536) + (Eq false + (Eq 0 + (And w64 (ReadLSB w64 8 stdout-stat) + 2147483647))) + (Ult (ReadLSB w64 56 stdout-stat) + 65536) + (Eq 1 + (ReadLSB w32 0 model_version)) + (Eq 45 (Read w8 0 arg0)) + (Eq false + (Eq 0 N2:(Read w8 1 arg0))) + (Eq false (Eq 45 N2)) + (Eq 100 + (AShr w32 (Shl w32 (SExt w32 N2) 24) + 24)) + (Eq 0 + (And w16 (ReadLSB w16 N3:(Extract w32 0 (Add w64 256 + (Mul w64 2 + (ZExt w64 N4:(Read w8 0 arg1))))) const_arr1) + 8192)) + (Eq false (Eq 84 N4)) + (Eq false + (Ult (Add w64 18446744073664565360 + N5:(Select w64 (Eq 0 N4) 44986256 51741584)) + 2)) + (Eq false + (Ult (Add w32 4294967248 + (ZExt w32 N6:(Read w8 (Extract w32 0 (Add w64 18446744073657810032 N5)) + U0:[2=0] @ arg1))) + 10)) + (Eq false (Eq 45 N6)) + (Eq false (Eq 43 N6)) + (Eq 0 + (And w16 (ReadLSB w16 N7:(Extract w32 0 (Add w64 256 + (Mul w64 2 (ZExt w64 N6)))) const_arr1) + 1024)) + (Eq false (Eq 40 N6)) + (Eq false + (Slt N8:(SExt w32 N6) 1)) + (Ult 96 + (Add w32 4294967286 + (ZExt w32 (Read w8 (Extract w32 0 (SExt w64 N8)) + const_arr8)))) + (Eq 7 (Read w8 0 U0)) + (Eq 13 (Read w8 1 U0))] + false [] + [n_args + n_args_1 + arg0 + arg1 + A-data + A-data-stat + stdin + stdin-stat + stdout + stdout-stat + model_version]) + +array A-data[8] : w32 -> w8 = symbolic +array A-data-stat[144] : w32 -> w8 = symbolic +array arg0[11] : w32 -> w8 = symbolic +array arg1[3] : w32 -> w8 = symbolic +array model_version[4] : w32 -> w8 = symbolic +array n_args[4] : w32 -> w8 = symbolic +array n_args_1[4] : w32 -> w8 = symbolic +array stdin[8] : w32 -> w8 = symbolic +array stdin-stat[144] : w32 -> w8 = symbolic +array stdout[1024] : w32 -> w8 = symbolic +array stdout-stat[144] : w32 -> w8 = symbolic +(query [(Ult N0:(ReadLSB w32 0 n_args) + 2) + (Slt 0 N0) + (Ult N1:(ReadLSB w32 0 n_args_1) + 3) + (Slt 0 N1) + (Eq false (Slt 1 N1)) + (Eq false + (Eq 0 + (And w64 (ReadLSB w64 8 A-data-stat) + 2147483647))) + (Ult (ReadLSB w64 56 A-data-stat) + 65536) + (Eq false + (Eq 0 + (And w64 (ReadLSB w64 8 stdin-stat) + 2147483647))) + (Ult (ReadLSB w64 56 stdin-stat) + 65536) + (Eq false + (Eq 0 + (And w64 (ReadLSB w64 8 stdout-stat) + 2147483647))) + (Ult (ReadLSB w64 56 stdout-stat) + 65536) + (Eq 1 + (ReadLSB w32 0 model_version)) + (Eq 45 (Read w8 0 arg0)) + (Eq 45 (Read w8 1 arg0)) + (Eq 61 (Read w8 3 arg0)) + (Eq 116 (Read w8 2 arg0)) + (Eq false + (Eq 0 (Read w8 4 arg0))) + (Eq false + (Eq 0 + N2:(Read w8 7 U0:[10=0] @ arg0))) + (Eq 0 (Read w8 8 U0)) + (Eq 11 (Read w8 4 U0)) + (Eq 63 (Read w8 5 U0)) + (Eq 8 (Read w8 6 U0)) + (Eq false (Eq 39 N2)) + (Or (Eq 122 N2) + (Or (Eq 121 N2) + (Or (Eq 120 N2) + (Or (Eq 119 N2) + (Or (Eq 118 N2) + (Or (Eq 117 N2) + (Or (Eq 116 N2) + (Or (Eq 115 N2) + (Or (Eq 114 N2) + (Or (Eq 113 N2) + (Or (Eq 112 N2) + (Or (Eq 111 N2) + (Or (Eq 110 N2) + (Or (Eq 109 N2) + (Or (Eq 108 N2) + (Or (Eq 107 N2) + (Or (Eq 106 N2) + (Or (Eq 105 N2) + (Or (Eq 104 N2) + (Or (Eq 103 N2) + (Or (Eq 102 N2) + (Or (Eq 101 N2) + (Or (Eq 100 N2) + (Or (Eq 99 N2) + (Or (Eq 98 N2) + (Or (Eq 97 N2) + (Or (Eq 95 N2) + (Or (Eq 93 N2) + (Or (Eq 90 N2) + (Or (Eq 89 N2) + (Or (Eq 88 N2) + (Or (Eq 87 N2) + (Or (Eq 86 N2) + (Or (Eq 85 N2) + (Or (Eq 84 N2) + (Or (Eq 83 N2) + (Or (Eq 82 N2) + (Or (Eq 81 N2) + (Or (Eq 80 N2) + (Or (Eq 79 N2) + (Or (Eq 78 N2) + (Or (Eq 77 N2) + (Or (Eq 76 N2) + (Or (Eq 75 N2) + (Or (Eq 74 N2) + (Or (Eq 73 N2) + (Or (Eq 72 N2) + (Or (Eq 71 N2) + (Or (Eq 70 N2) + (Or (Eq 69 N2) + (Or (Eq 68 N2) + (Or (Eq 67 N2) + (Or (Eq 66 N2) + (Or (Eq 65 N2) + (Or (Eq 58 N2) + (Or (Eq 57 N2) + (Or (Eq 56 N2) + (Or (Eq 55 N2) + (Or (Eq 54 N2) + (Or (Eq 53 N2) + (Or (Eq 52 N2) + (Or (Eq 51 N2) + (Or (Eq 50 N2) + (Or (Eq 49 N2) + (Or (Eq 48 N2) + (Or (Eq 47 N2) + (Or (Eq 46 N2) + (Or (Eq 45 N2) + (Or (Eq 44 N2) + (Or (Eq 43 N2) (Eq 37 N2)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))] + false [] + [n_args + arg0 + n_args_1 + arg1 + A-data + A-data-stat + stdin + stdin-stat + stdout + stdout-stat + model_version]) \ No newline at end of file diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index 9c374eb8..a937d761 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -95,6 +95,11 @@ namespace { llvm::cl::opt<std::string> directoryToWriteQueryLogs("query-log-dir",llvm::cl::desc("The folder to write query logs to. Defaults is current working directory."), llvm::cl::init(".")); + llvm::cl::opt<bool> ClearArrayAfterQuery( + "clear-array-decls-after-query", + llvm::cl::desc("We discard the previous array declarations after a query " + "is performed. Default: false"), + llvm::cl::init(false)); } static std::string getQueryLogPath(const char filename[]) @@ -160,7 +165,7 @@ static bool PrintInputAST(const char *Filename, const MemoryBuffer *MB, ExprBuilder *Builder) { std::vector<Decl*> Decls; - Parser *P = Parser::Create(Filename, MB, Builder); + Parser *P = Parser::Create(Filename, MB, Builder, ClearArrayAfterQuery); P->SetMaxErrors(20); unsigned NumQueries = 0; @@ -193,7 +198,7 @@ static bool EvaluateInputAST(const char *Filename, const MemoryBuffer *MB, ExprBuilder *Builder) { std::vector<Decl*> Decls; - Parser *P = Parser::Create(Filename, MB, Builder); + Parser *P = Parser::Create(Filename, MB, Builder, ClearArrayAfterQuery); P->SetMaxErrors(20); while (Decl *D = P->ParseTopLevelDecl()) { Decls.push_back(D); @@ -327,8 +332,8 @@ static bool printInputAsSMTLIBv2(const char *Filename, { //Parse the input file std::vector<Decl*> Decls; - Parser *P = Parser::Create(Filename, MB, Builder); - P->SetMaxErrors(20); + Parser *P = Parser::Create(Filename, MB, Builder, ClearArrayAfterQuery); + P->SetMaxErrors(20); while (Decl *D = P->ParseTopLevelDecl()) { Decls.push_back(D); |