klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
Assignment.h
Go to the documentation of this file.
1 //===-- Assignment.h --------------------------------------------*- C++ -*-===//
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 #ifndef KLEE_UTIL_ASSIGNMENT_H
11 #define KLEE_UTIL_ASSIGNMENT_H
12 
13 #include <map>
14 
16 
17 // FIXME: Rename?
18 
19 namespace klee {
20  class Array;
21 
22  class Assignment {
23  public:
24  typedef std::map<const Array*, std::vector<unsigned char> > bindings_ty;
25 
28 
29  public:
30  Assignment(bool _allowFreeValues=false)
31  : allowFreeValues(_allowFreeValues) {}
32  Assignment(std::vector<const Array*> &objects,
33  std::vector< std::vector<unsigned char> > &values,
34  bool _allowFreeValues=false)
35  : allowFreeValues(_allowFreeValues){
36  std::vector< std::vector<unsigned char> >::iterator valIt =
37  values.begin();
38  for (std::vector<const Array*>::iterator it = objects.begin(),
39  ie = objects.end(); it != ie; ++it) {
40  const Array *os = *it;
41  std::vector<unsigned char> &arr = *valIt;
42  bindings.insert(std::make_pair(os, arr));
43  ++valIt;
44  }
45  }
46 
47  ref<Expr> evaluate(const Array *mo, unsigned index) const;
49 
50  template<typename InputIterator>
51  bool satisfies(InputIterator begin, InputIterator end);
52  };
53 
55  const Assignment &a;
56 
57  protected:
58  ref<Expr> getInitialValue(const Array &mo, unsigned index) {
59  return a.evaluate(&mo, index);
60  }
61 
62  public:
63  AssignmentEvaluator(const Assignment &_a) : a(_a) {}
64  };
65 
66  /***/
67 
68  inline ref<Expr> Assignment::evaluate(const Array *array,
69  unsigned index) const {
70  assert(array);
71  bindings_ty::const_iterator it = bindings.find(array);
72  if (it!=bindings.end() && index<it->second.size()) {
73  return ConstantExpr::alloc(it->second[index], array->getRange());
74  } else {
75  if (allowFreeValues) {
76  return ReadExpr::create(UpdateList(array, 0),
77  ConstantExpr::alloc(index, array->getDomain()));
78  } else {
79  return ConstantExpr::alloc(0, array->getRange());
80  }
81  }
82  }
83 
85  AssignmentEvaluator v(*this);
86  return v.visit(e);
87  }
88 
89  template<typename InputIterator>
90  inline bool Assignment::satisfies(InputIterator begin, InputIterator end) {
91  AssignmentEvaluator v(*this);
92  for (; begin!=end; ++begin)
93  if (!v.visit(*begin)->isTrue())
94  return false;
95  return true;
96  }
97 }
98 
99 #endif
static ref< Expr > create(const UpdateList &updates, ref< Expr > i)
Definition: Expr.cpp:499
bool allowFreeValues
Definition: Assignment.h:26
ref< Expr > evaluate(const Array *mo, unsigned index) const
Definition: Assignment.h:68
const Assignment & a
Definition: Assignment.h:55
Class representing a complete list of updates into an array.
Definition: Expr.h:655
bindings_ty bindings
Definition: Assignment.h:27
bool isTrue() const
isTrue - Is this the true expression.
Definition: Expr.h:1094
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:398
Expr::Width getRange() const
Definition: Expr.h:645
AssignmentEvaluator(const Assignment &_a)
Definition: Assignment.h:63
std::map< const Array *, std::vector< unsigned char > > bindings_ty
Definition: Assignment.h:24
Expr::Width getDomain() const
Definition: Expr.h:644
Assignment(bool _allowFreeValues=false)
Definition: Assignment.h:30
bool satisfies(InputIterator begin, InputIterator end)
Definition: Assignment.h:90
ref< Expr > getInitialValue(const Array &mo, unsigned index)
Definition: Assignment.h:58
Assignment(std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool _allowFreeValues=false)
Definition: Assignment.h:32
ref< Expr > visit(const ref< Expr > &e)
Definition: ExprVisitor.cpp:24