klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
SeedInfo.cpp
Go to the documentation of this file.
1 //===-- SeedInfo.cpp ------------------------------------------------------===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 
10 #include "Common.h"
11 
12 #include "Memory.h"
13 #include "SeedInfo.h"
14 #include "TimingSolver.h"
15 
16 #include "klee/ExecutionState.h"
17 #include "klee/Expr.h"
18 #include "klee/util/ExprUtil.h"
20 
21 using namespace klee;
22 
24  bool byName) {
25  if (byName) {
26  unsigned i;
27 
28  for (i=0; i<input->numObjects; ++i) {
29  KTestObject *obj = &input->objects[i];
30  if (std::string(obj->name) == mo->name)
31  if (used.insert(obj).second)
32  return obj;
33  }
34 
35  // If first unused input matches in size then accept that as
36  // well.
37  for (i=0; i<input->numObjects; ++i)
38  if (!used.count(&input->objects[i]))
39  break;
40  if (i<input->numObjects) {
41  KTestObject *obj = &input->objects[i];
42  if (obj->numBytes == mo->size) {
43  used.insert(obj);
44  klee_warning_once(mo, "using seed input %s[%d] for: %s (no name match)",
45  obj->name, obj->numBytes, mo->name.c_str());
46  return obj;
47  }
48  }
49 
50  klee_warning_once(mo, "no seed input for: %s", mo->name.c_str());
51  return 0;
52  } else {
53  if (inputPosition >= input->numObjects) {
54  return 0;
55  } else {
56  return &input->objects[inputPosition++];
57  }
58  }
59 }
60 
62  ref<Expr> condition,
63  TimingSolver *solver) {
64  std::vector< ref<Expr> > required(state.constraints.begin(),
65  state.constraints.end());
66  ExecutionState tmp(required);
67  tmp.addConstraint(condition);
68 
69  // Try and patch direct reads first, this is likely to resolve the
70  // problem quickly and avoids long traversal of all seed
71  // values. There are other smart ways to do this, the nicest is if
72  // we got a minimal counterexample from STP, in which case we would
73  // just inject those values back into the seed.
74  std::set< std::pair<const Array*, unsigned> > directReads;
75  std::vector< ref<ReadExpr> > reads;
76  findReads(condition, false, reads);
77  for (std::vector< ref<ReadExpr> >::iterator it = reads.begin(),
78  ie = reads.end(); it != ie; ++it) {
79  ReadExpr *re = it->get();
80  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
81  directReads.insert(std::make_pair(re->updates.root,
82  (unsigned) CE->getZExtValue(32)));
83  }
84  }
85 
86  for (std::set< std::pair<const Array*, unsigned> >::iterator
87  it = directReads.begin(), ie = directReads.end(); it != ie; ++it) {
88  const Array *array = it->first;
89  unsigned i = it->second;
90  ref<Expr> read = ReadExpr::create(UpdateList(array, 0),
92 
93  // If not in bindings then this can't be a violation?
94  Assignment::bindings_ty::iterator it2 = assignment.bindings.find(array);
95  if (it2 != assignment.bindings.end()) {
96  ref<Expr> isSeed = EqExpr::create(read,
97  ConstantExpr::alloc(it2->second[i],
98  Expr::Int8));
99  bool res;
100  bool success = solver->mustBeFalse(tmp, isSeed, res);
101  assert(success && "FIXME: Unhandled solver failure");
102  (void) success;
103  if (res) {
104  ref<ConstantExpr> value;
105  bool success = solver->getValue(tmp, read, value);
106  assert(success && "FIXME: Unhandled solver failure");
107  (void) success;
108  it2->second[i] = value->getZExtValue(8);
109  tmp.addConstraint(EqExpr::create(read,
110  ConstantExpr::alloc(it2->second[i],
111  Expr::Int8)));
112  } else {
113  tmp.addConstraint(isSeed);
114  }
115  }
116  }
117 
118  bool res;
119  bool success = solver->mayBeTrue(state, assignment.evaluate(condition), res);
120  assert(success && "FIXME: Unhandled solver failure");
121  (void) success;
122  if (res)
123  return;
124 
125  // We could still do a lot better than this, for example by looking at
126  // independence. But really, this shouldn't be happening often.
127  for (Assignment::bindings_ty::iterator it = assignment.bindings.begin(),
128  ie = assignment.bindings.end(); it != ie; ++it) {
129  const Array *array = it->first;
130  for (unsigned i=0; i<array->size; ++i) {
131  ref<Expr> read = ReadExpr::create(UpdateList(array, 0),
133  ref<Expr> isSeed = EqExpr::create(read,
134  ConstantExpr::alloc(it->second[i],
135  Expr::Int8));
136  bool res;
137  bool success = solver->mustBeFalse(tmp, isSeed, res);
138  assert(success && "FIXME: Unhandled solver failure");
139  (void) success;
140  if (res) {
141  ref<ConstantExpr> value;
142  bool success = solver->getValue(tmp, read, value);
143  assert(success && "FIXME: Unhandled solver failure");
144  (void) success;
145  it->second[i] = value->getZExtValue(8);
146  tmp.addConstraint(EqExpr::create(read,
147  ConstantExpr::alloc(it->second[i],
148  Expr::Int8)));
149  } else {
150  tmp.addConstraint(isSeed);
151  }
152  }
153  }
154 
155 #ifndef NDEBUG
156  {
157  bool res;
158  bool success =
159  solver->mayBeTrue(state, assignment.evaluate(condition), res);
160  assert(success && "FIXME: Unhandled solver failure");
161  (void) success;
162  assert(res && "seed patching failed");
163  }
164 #endif
165 }
KTest * input
Definition: SeedInfo.h:27
void void void void klee_warning_once(const void *id, const char *msg,...) __attribute__((format(printf
Definition: Common.cpp:90
constraint_iterator end() const
Definition: Constraints.h:57
unsigned size
Definition: Expr.h:605
static ref< Expr > create(const UpdateList &updates, ref< Expr > i)
Definition: Expr.cpp:499
unsigned numBytes
Definition: KTest.h:21
ref< Expr > evaluate(const Array *mo, unsigned index) const
Definition: Assignment.h:68
Class representing a complete list of updates into an array.
Definition: Expr.h:655
std::set< struct KTestObject * > used
Definition: SeedInfo.h:29
UpdateList updates
Definition: Expr.h:687
uint64_t getZExtValue(unsigned bits=64) const
Definition: Expr.h:361
std::string name
Definition: Memory.h:46
unsigned numObjects
Definition: KTest.h:36
static const Width Int32
Definition: Expr.h:100
unsigned size
size in bytes
Definition: Memory.h:45
static const Width Int8
Definition: Expr.h:98
bindings_ty bindings
Definition: Assignment.h:27
void patchSeed(const ExecutionState &state, ref< Expr > condition, TimingSolver *solver)
Definition: SeedInfo.cpp:61
void findReads(ref< Expr > e, bool visitUpdates, std::vector< ref< ReadExpr > > &result)
Definition: ExprUtil.cpp:21
constraint_iterator begin() const
Definition: Constraints.h:54
bool mayBeTrue(const ExecutionState &, ref< Expr >, bool &result)
KTestObject * objects
Definition: KTest.h:37
bool mustBeFalse(const ExecutionState &, ref< Expr >, bool &result)
char * name
Definition: KTest.h:20
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:398
Assignment assignment
Definition: SeedInfo.h:26
ConstraintManager constraints
const Array * root
Definition: Expr.h:659
Class representing a one byte read from an array.
Definition: Expr.h:681
unsigned inputPosition
Definition: SeedInfo.h:28
ref< Expr > index
Definition: Expr.h:688
KTestObject * getNextInput(const MemoryObject *mo, bool byName)
Definition: SeedInfo.cpp:23
bool getValue(const ExecutionState &, ref< Expr > expr, ref< ConstantExpr > &result)