diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 6185e98e5e..c5dc81f2f5 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1460,9 +1460,9 @@ void Executor::addConstraint(ExecutionState &state, ref condition) { if (!concretization.isEmpty()) { // Update memory objects if arrays have affected them. + updateStateWithSymcretes(state, concretization); Assignment delta = state.constraints.cs().concretization().diffWith(concretization); - updateStateWithSymcretes(state, delta); state.addConstraint(condition, delta); } else { state.addConstraint(condition, {}); @@ -6490,7 +6490,7 @@ void Executor::updateStateWithSymcretes(ExecutionState &state, * assign. We want to update only objects, whose size were changed. */ std::vector> updatedSizeSymcretes; - const Assignment &diffAssignment = + Assignment diffAssignment = state.constraints.cs().concretization().diffWith(assignment); for (const ref &symcrete : state.constraints.cs().symcretes()) { diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index d349c9d0b2..17ae8e50bc 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -209,7 +209,7 @@ ConstraintSet::ConstraintSet() {} void ConstraintSet::addConstraint(ref e, const Assignment &delta) { _constraints.insert(e); // Update bindings - for (auto i : delta.bindings) { + for (auto &i : delta.bindings) { _concretization.bindings.replace({i.first, i.second}); } _independentElements.updateConcretization(delta); diff --git a/lib/Expr/IndependentSet.cpp b/lib/Expr/IndependentSet.cpp index feb3d26583..d01b234f17 100644 --- a/lib/Expr/IndependentSet.cpp +++ b/lib/Expr/IndependentSet.cpp @@ -23,7 +23,7 @@ IndependentConstraintSet::updateConcretization( if (delta.bindings.size() == 0) { return ics; } - for (auto i : delta.bindings) { + for (auto &i : delta.bindings) { ics->concretization.bindings.replace({i.first, i.second}); } InnerSetUnion DSU; @@ -45,6 +45,15 @@ IndependentConstraintSet::updateConcretization( } DSU.addValue(new ExprEitherSymcrete::left(e)); } + auto concretizationConstraints = + ics->concretization.createConstraintsFromAssignment(); + for (ref e : concretizationConstraints) { + if (auto ce = dyn_cast(e)) { + assert(ce->isTrue() && "Attempt to add invalid constraint"); + continue; + } + DSU.addValue(new ExprEitherSymcrete::left(e)); + } ics->concretizedSets = DSU; return ics; } @@ -56,7 +65,7 @@ IndependentConstraintSet::removeConcretization( if (delta.bindings.size() == 0) { return ics; } - for (auto i : delta.bindings) { + for (auto &i : delta.bindings) { ics->concretization.bindings.remove(i.first); } InnerSetUnion DSU; @@ -78,6 +87,15 @@ IndependentConstraintSet::removeConcretization( } DSU.addValue(new ExprEitherSymcrete::left(e)); } + auto concretizationConstraints = + ics->concretization.createConstraintsFromAssignment(); + for (ref e : concretizationConstraints) { + if (auto ce = dyn_cast(e)) { + assert(ce->isTrue() && "Attempt to add invalid constraint"); + continue; + } + DSU.addValue(new ExprEitherSymcrete::left(e)); + } ics->concretizedSets = DSU; return ics; @@ -343,6 +361,15 @@ IndependentConstraintSet::merge(ref A, } DSU.addValue(new ExprEitherSymcrete::left(e)); } + auto concretizationConstraints = + a->concretization.createConstraintsFromAssignment(); + for (ref e : concretizationConstraints) { + if (auto ce = dyn_cast(e)) { + assert(ce->isTrue() && "Attempt to add invalid constraint"); + continue; + } + DSU.addValue(new ExprEitherSymcrete::left(e)); + } a->concretizedSets = DSU; } diff --git a/scripts/kleef b/scripts/kleef index 86a250c171..c98a94114a 100755 --- a/scripts/kleef +++ b/scripts/kleef @@ -92,6 +92,7 @@ def klee_options( "--track-coverage=all", # Only branches and only instructions are wrong in real life. E.g., ternary operators are sometimes counted as different branches, while we stick to look at them as a single instruction from a single branch "--use-iterative-deepening-search=max-cycles", f"--max-solver-time={MAX_SOLVER_TIME}s", + "--max-cycles-before-stuck=15", # "--tc-type=cov", "--only-output-states-covering-new", # Don't generate all test cases "--dump-states-on-halt=true", # Check in case we missed some oncovered instructions diff --git a/test/Industry/CoverageBranches/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c b/test/Industry/CoverageBranches/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c index b0efaf937e..99f638327a 100644 --- a/test/Industry/CoverageBranches/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c +++ b/test/Industry/CoverageBranches/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c @@ -9,7 +9,7 @@ // RUN: FileCheck --input-file=%t.cov.log --check-prefix=CHECK-COV %s -// Branch coverage 100%, the number of branches is 1: +// Branch coverage 100%, the number of branches is 2: // CHECK-COV: Lines executed:100.00% of 11 // CHECK-COV-NEXT: Branches executed:100.00% of 2 // CHECK-COV-NEXT: Taken at least once:100.00% of 2 diff --git a/test/Industry/CoverageBranches/CostasArray-17.c b/test/Industry/CoverageBranches/CostasArray-17.c index 6f326016af..088a33fbb0 100644 --- a/test/Industry/CoverageBranches/CostasArray-17.c +++ b/test/Industry/CoverageBranches/CostasArray-17.c @@ -19,7 +19,7 @@ // RUN: FileCheck --input-file=%t.cov.log --check-prefix=CHECK %s -// Branch coverage 100%, the number of branches is 1: +// Branch coverage 100%, the number of branches is 2: // CHECK: Lines executed:{{(0\.7[0-9])}}% of 1545 // CHECK-NEXT: Branches executed:100.00% of 2 // CHECK-NEXT: Taken at least once:100.00% of 2 diff --git a/test/Industry/CoverageBranches/egcd3-ll_valuebound10.c b/test/Industry/CoverageBranches/egcd3-ll_valuebound10.c index 72396f861a..d5405512d8 100644 --- a/test/Industry/CoverageBranches/egcd3-ll_valuebound10.c +++ b/test/Industry/CoverageBranches/egcd3-ll_valuebound10.c @@ -9,7 +9,6 @@ // RUN: FileCheck --input-file=%t.cov.log --check-prefix=CHECK %s -// Branch coverage 100%, the number of branches is 1: // CHECK: Lines executed:87.93% of 58 // CHECK-NEXT: Branches executed:100.00% of 18 // CHECK-NEXT: Taken at least once:83.33% of 18 diff --git a/test/Industry/CoverageBranches/matrix-2-2.c b/test/Industry/CoverageBranches/matrix-2-2.c new file mode 100644 index 0000000000..d25bd92255 --- /dev/null +++ b/test/Industry/CoverageBranches/matrix-2-2.c @@ -0,0 +1,68 @@ +// RUN: %clang -Wno-everything %s -emit-llvm %O0opt -g -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=all --max-cycles=2 --optimize=true --emit-all-errors --delete-dead-loops=false --use-forked-solver=false -max-memory=6008 --cex-cache-validity-cores --only-output-states-covering-new=true --dump-states-on-halt=true --use-sym-size-alloc=true --symbolic-allocation-threshold=8192 %t1.bc 2>&1 + +// RUN: rm -f %t*.gcda %t*.gcno %t*.gcov +// RUN: %cc -DGCOV %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner --coverage +// RUN: %replay %t.klee-out %t_runner +// RUN: gcov -b %t_runner-%basename_t > %t.cov.log + +// RUN: FileCheck --input-file=%t.cov.log --check-prefix=CHECK-COV %s + +// Branch coverage is greater 80%: +// CHECK-COV: Lines executed:9{{([0-9]\.[0-9][0-9])}}% of 24 +// CHECK-COV-NEXT: Branches executed:100.00% of 16 +// CHECK-COV-NEXT: Taken at least once:{{([8-9][0-9]\.[0-9][0-9])}}% of 16 + +#include "klee-test-comp.c" + +extern void exit(int); +extern void abort(void); +#ifdef GCOV +extern void __gcov_dump(void); +#endif + +void dump() { +#ifdef GCOV + __gcov_dump(); + exit(0); +#endif +} + +extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); +void reach_error() { dump(); __assert_fail("0", "matrix-2-2.c", 3, "reach_error"); } + +void __VERIFIER_assert(int cond) { + if (!(cond)) { + ERROR: {reach_error();abort();} + } + return; +} +extern unsigned int __VERIFIER_nondet_uint(); +extern int __VERIFIER_nondet_int(); + +int main() +{ + unsigned int N_LIN=__VERIFIER_nondet_uint(); + unsigned int N_COL=__VERIFIER_nondet_uint(); + if (N_LIN >= 4000000000 / sizeof(int) || N_COL >= 4000000000 / sizeof(int)) { + return 0; + } + unsigned int j,k; + int matriz[N_COL][N_LIN], maior; + + maior = __VERIFIER_nondet_int(); + for(j=0;jmaior) + maior = matriz[j][k]; + } + + for(j=0;j