From 3e006dbfacd06e12818d97ae5aab1960324b27f9 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Tue, 14 Nov 2023 15:06:06 +0000 Subject: Add checks to the seed concretization tests about the expected number of queries --- test/Feature/SeedConcretizeExtendFP.c | 4 ++++ test/Feature/SeedConcretizeExternalCall.c | 4 ++++ test/Feature/SeedConcretizeFP.c | 4 ++++ test/Feature/SeedConcretizeMalloc.c | 8 ++++++-- 4 files changed, 18 insertions(+), 2 deletions(-) diff --git a/test/Feature/SeedConcretizeExtendFP.c b/test/Feature/SeedConcretizeExtendFP.c index 6a8de589..3ecd3bc3 100644 --- a/test/Feature/SeedConcretizeExtendFP.c +++ b/test/Feature/SeedConcretizeExtendFP.c @@ -8,6 +8,7 @@ // RUN: rm -rf %t.klee-out-2 // RUN: %klee --exit-on-error --output-dir=%t.klee-out-2 --seed-file %t.klee-out/test000001.ktest --allow-seed-extension %t.bc 2>&1 | FileCheck %s +// RUN: %klee-stats --print-columns 'SolverQueries' --table-format=csv %t.klee-out-2 | FileCheck --check-prefix=CHECK-STATS %s #include "klee/klee.h" @@ -30,4 +31,7 @@ int main() { // CHECK: concretizing (reason: floating point) assert((unsigned) d < 5001); } + + // CHECK-STATS: 3 + // These is similar to SeedConcretizeFP.c (1 query) plus the extra queries due to an incomplete seed } diff --git a/test/Feature/SeedConcretizeExternalCall.c b/test/Feature/SeedConcretizeExternalCall.c index 7eb69698..afc7fb6a 100644 --- a/test/Feature/SeedConcretizeExternalCall.c +++ b/test/Feature/SeedConcretizeExternalCall.c @@ -6,6 +6,7 @@ // RUN: rm -rf %t.klee-out-2 // RUN: %klee --external-calls=all --exit-on-error --output-dir=%t.klee-out-2 --seed-file %t.klee-out/test000001.ktest %t.bc +// RUN: %klee-stats --print-columns 'SolverQueries' --table-format=csv %t.klee-out-2 | FileCheck --check-prefix=CHECK-STATS %s #include "klee/klee.h" @@ -22,4 +23,7 @@ int main() { int x; klee_make_symbolic(&x, sizeof(x), "x"); assert(abs(x) == 12345678); + + // CHECK-STATS: 0 + // No queries, but this will change once https://github.com/klee/klee/pull/1520 is merged } diff --git a/test/Feature/SeedConcretizeFP.c b/test/Feature/SeedConcretizeFP.c index bc5246ad..bde6b329 100644 --- a/test/Feature/SeedConcretizeFP.c +++ b/test/Feature/SeedConcretizeFP.c @@ -6,6 +6,7 @@ // RUN: rm -rf %t.klee-out-2 // RUN: %klee --exit-on-error --output-dir=%t.klee-out-2 --seed-file %t.klee-out/test000001.ktest %t.bc 2>&1 | FileCheck %s +// RUN: %klee-stats --print-columns 'SolverQueries' --table-format=csv %t.klee-out-2 | FileCheck --check-prefix=CHECK-STATS %s #include "klee/klee.h" @@ -24,4 +25,7 @@ int main() { double d = i; // CHECK: concretizing (reason: floating point) assert((unsigned) d == 12345678); + + // CHECK-STATS: 1 + // This one query involves the constraint that i == 12345678 } diff --git a/test/Feature/SeedConcretizeMalloc.c b/test/Feature/SeedConcretizeMalloc.c index 1f916723..87748846 100644 --- a/test/Feature/SeedConcretizeMalloc.c +++ b/test/Feature/SeedConcretizeMalloc.c @@ -6,6 +6,7 @@ // RUN: rm -rf %t.klee-out-2 // RUN: %klee --output-dir=%t.klee-out-2 --seed-file %t.klee-out/test000001.ktest %t.bc | FileCheck --allow-empty %s +// RUN: %klee-stats --print-columns 'SolverQueries' --table-format=csv %t.klee-out-2 | FileCheck --check-prefix=CHECK-STATS %s #include "klee/klee.h" @@ -14,13 +15,13 @@ #include void SeedGen() { - unsigned x; + size_t x; klee_make_symbolic(&x, sizeof(x), "x"); klee_assume(x == 100); } int main(int argc, char **argv) { - unsigned s; + size_t s; klee_make_symbolic(&s, sizeof(s), "size"); char *p = (char *)malloc(s); if (!p) @@ -29,4 +30,7 @@ int main(int argc, char **argv) { if (s != 100) printf("Error\n"); // CHECK-NOT: Error + + // CHECK-STATS: 4 + // These queries are due to the explicit constraint asserting that s is 100 and the implicit one checking if we have a huge malloc } -- cgit 1.4.1