 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
14.8% |
8 / 54 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
22.2% |
12 / 54 |
| |
|
Line Coverage: |
11.6% |
8 / 69 |
| |
 |
|
 |
1 : /* -*- mode: c++; c-basic-offset: 2; -*- */
2 :
3 : #include "Common.h"
4 :
5 : #include "SeedInfo.h"
6 : #include "TimingSolver.h"
7 :
8 : #include "klee/ExecutionState.h"
9 : #include "klee/Expr.h"
10 : #include "klee/Memory.h"
11 : #include "klee/util/ExprUtil.h"
12 : #include "klee/Internal/ADT/BOut.h"
13 :
14 : #include "klee/Internal/FIXME/sugar.h"
15 :
16 : using namespace klee;
17 :
18 : BOutObject *SeedInfo::getNextInput(const MemoryObject *mo,
19 4: bool byName) {
4: branch 0 taken
0: branch 1 not taken
20 4: if (byName) {
21 : unsigned i;
22 :
10: branch 0 taken
0: branch 1 not taken
23 10: for (i=0; i<input->numObjects; ++i) {
24 10: BOutObject *obj = &input->objects[i];
5: branch 2 taken
5: branch 3 taken
25 40: if (std::string(obj->name) == mo->name)
4: branch 1 taken
1: branch 2 taken
26 5: if (used.insert(obj).second)
27 4: return obj;
28 : }
29 :
30 : // If first unused input matches in size then accept that as
31 : // well.
0: branch 0 not taken
0: branch 1 not taken
32 0: for (i=0; i<input->numObjects; ++i)
0: branch 0 not taken
0: branch 1 not taken
33 0: if (!used.count(&input->objects[i]))
34 0: break;
0: branch 0 not taken
0: branch 1 not taken
35 0: if (i<input->numObjects) {
36 0: BOutObject *obj = &input->objects[i];
0: branch 0 not taken
0: branch 1 not taken
37 0: if (obj->numBytes == mo->size) {
38 0: used.insert(obj);
39 : klee_warning_once(mo, "using seed input %s[%d] for: %s (no name match)",
40 0: obj->name, obj->numBytes, mo->name.c_str());
41 0: return obj;
42 : }
43 : }
44 :
45 0: klee_warning_once(mo, "no seed input for: %s", mo->name.c_str());
46 0: return 0;
47 : } else {
0: branch 0 not taken
0: branch 1 not taken
48 0: if (inputPosition >= input->numObjects) {
49 0: return 0;
50 : } else {
51 0: return &input->objects[inputPosition++];
52 : }
53 : }
54 : }
55 :
56 : void SeedInfo::patchSeed(const ExecutionState &state,
57 : ref<Expr> condition,
58 0: TimingSolver *solver) {
59 : std::vector< ref<Expr> > required(state.constraints.begin(),
60 0: state.constraints.end());
61 0: ExecutionState tmp(required);
62 0: tmp.addConstraint(condition);
63 :
64 : // Try and patch direct reads first, this is likely to resolve the
65 : // problem quickly and avoids long traversal of all seed
66 : // values. There are other smart ways to do this, the nicest is if
67 : // we got a minimal counterexample from STP, in which case we would
68 : // just inject those values back into the seed.
69 : std::set< std::pair<const MemoryObject *, unsigned> > directReads;
70 : std::vector< ref<ReadExpr> > reads;
71 0: findReads(condition, false, reads);
0: branch 0 not taken
0: branch 1 not taken
72 0: foreach(it, reads.begin(), reads.end()) {
73 0: ReadExpr *re = it->get();
0: branch 0 not taken
0: branch 1 not taken
74 0: if (re->index.isConstant()) {
75 0: unsigned index = (unsigned) re->index.getConstantValue();
76 0: directReads.insert(std::make_pair(re->updates.root, index));
77 : }
78 : }
79 :
0: branch 1 not taken
0: branch 2 not taken
80 0: foreach(it, directReads.begin(), directReads.end()) {
81 0: const MemoryObject *mo = it->first;
82 0: unsigned i = it->second;
83 : ref<Expr> read = ReadExpr::create(UpdateList(mo, true, 0),
84 0: ref<Expr>(i, Expr::Int32));
85 0: let(it2, assignment.bindings.find(mo));
86 :
87 : // If not in bindings then this can't be a violation?
0: branch 0 not taken
0: branch 1 not taken
88 0: if (it2 != assignment.bindings.end()) {
89 0: ref<Expr> isSeed = EqExpr::create(read, ref<Expr>(it2->second[i], Expr::Int8));
90 : bool res;
91 0: bool success = solver->mustBeFalse(tmp, isSeed, res);
0: branch 0 not taken
0: branch 1 not taken
92 0: assert(success && "FIXME: Unhandled solver failure");
0: branch 0 not taken
0: branch 1 not taken
93 0: if (res) {
94 : ref<Expr> value;
95 0: bool success = solver->getValue(tmp, read, value);
0: branch 0 not taken
0: branch 1 not taken
96 0: assert(success && "FIXME: Unhandled solver failure");
97 0: it2->second[i] = value.getConstantValue();
98 0: tmp.addConstraint(EqExpr::create(read, ref<Expr>(it2->second[i], Expr::Int8)));
99 : } else {
100 0: tmp.addConstraint(isSeed);
101 0: }
102 : }
103 : }
104 :
105 : bool res;
106 0: bool success = solver->mayBeTrue(state, assignment.evaluate(condition), res);
0: branch 0 not taken
0: branch 1 not taken
107 0: assert(success && "FIXME: Unhandled solver failure");
0: branch 0 not taken
0: branch 1 not taken
108 0: if (res)
109 0: return;
110 :
111 : // We could still do a lot better than this, for example by looking at
112 : // independence. But really, this shouldn't be happening often.
0: branch 0 not taken
0: branch 1 not taken
113 0: foreach(it, assignment.bindings.begin(), assignment.bindings.end()) {
114 0: const MemoryObject *mo = it->first;
0: branch 2 not taken
0: branch 3 not taken
115 0: for (unsigned i=0; i<mo->size; ++i) {
116 : ref<Expr> read = ReadExpr::create(UpdateList(mo, true, 0),
117 0: ref<Expr>(i, Expr::Int32));
118 0: ref<Expr> isSeed = EqExpr::create(read, ref<Expr>(it->second[i], Expr::Int8));
119 : bool res;
120 0: bool success = solver->mustBeFalse(tmp, isSeed, res);
0: branch 0 not taken
0: branch 1 not taken
121 0: assert(success && "FIXME: Unhandled solver failure");
0: branch 0 not taken
0: branch 1 not taken
122 0: if (res) {
123 : ref<Expr> value;
124 0: bool success = solver->getValue(tmp, read, value);
0: branch 0 not taken
0: branch 1 not taken
125 0: assert(success && "FIXME: Unhandled solver failure");
126 0: it->second[i] = value.getConstantValue();
127 0: tmp.addConstraint(EqExpr::create(read, ref<Expr>(it->second[i], Expr::Int8)));
128 : } else {
129 0: tmp.addConstraint(isSeed);
130 : }
131 : }
132 : }
133 :
134 : #ifndef NDEBUG
135 : {
136 : bool res;
137 : bool success =
138 0: solver->mayBeTrue(state, assignment.evaluate(condition), res);
0: branch 0 not taken
0: branch 1 not taken
139 0: assert(success && "FIXME: Unhandled solver failure");
0: branch 0 not taken
0: branch 1 not taken
140 0: assert(res && "seed patching failed");
141 0: }
142 : #endif
103: branch 0 taken
0: branch 1 not taken
103: branch 2 taken
0: branch 3 not taken
143 206: }
Generated: 2009-05-17 22:47 by zcov