klee
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_ASSIGNMENT_H
11#define KLEE_ASSIGNMENT_H
12
15
16#include <map>
17
18namespace klee {
19 class Array;
20
21 class Assignment {
22 public:
23 typedef std::map<const Array*, std::vector<unsigned char> > bindings_ty;
24
27
28 public:
29 Assignment(bool _allowFreeValues=false)
30 : allowFreeValues(_allowFreeValues) {}
31 Assignment(const std::vector<const Array*> &objects,
32 std::vector< std::vector<unsigned char> > &values,
33 bool _allowFreeValues=false)
34 : allowFreeValues(_allowFreeValues){
35 std::vector< std::vector<unsigned char> >::iterator valIt =
36 values.begin();
37 for (std::vector<const Array*>::const_iterator it = objects.begin(),
38 ie = objects.end(); it != ie; ++it) {
39 const Array *os = *it;
40 std::vector<unsigned char> &arr = *valIt;
41 bindings.insert(std::make_pair(os, arr));
42 ++valIt;
43 }
44 }
45
46 ref<Expr> evaluate(const Array *mo, unsigned index) const;
49
50 template<typename InputIterator>
51 bool satisfies(InputIterator begin, InputIterator end);
52 void dump();
53 };
54
56 const Assignment &a;
57
58 protected:
59 ref<Expr> getInitialValue(const Array &mo, unsigned index) {
60 return a.evaluate(&mo, index);
61 }
62
63 public:
64 AssignmentEvaluator(const Assignment &_a) : a(_a) {}
65 };
66
67 /***/
68
69 inline ref<Expr> Assignment::evaluate(const Array *array,
70 unsigned index) const {
71 assert(array);
72 bindings_ty::const_iterator it = bindings.find(array);
73 if (it!=bindings.end() && index<it->second.size()) {
74 return ConstantExpr::alloc(it->second[index], array->getRange());
75 } else {
76 if (allowFreeValues) {
77 return ReadExpr::create(UpdateList(array, ref<UpdateNode>(nullptr)),
78 ConstantExpr::alloc(index, array->getDomain()));
79 } else {
80 return ConstantExpr::alloc(0, array->getRange());
81 }
82 }
83 }
84
86 AssignmentEvaluator v(*this);
87 return v.visit(e);
88 }
89
90 template<typename InputIterator>
91 inline bool Assignment::satisfies(InputIterator begin, InputIterator end) {
92 AssignmentEvaluator v(*this);
93 for (; begin!=end; ++begin)
94 if (!v.visit(*begin)->isTrue())
95 return false;
96 return true;
97 }
98}
99
100#endif /* KLEE_ASSIGNMENT_H */
Expr::Width getRange() const
Definition: Expr.h:530
Expr::Width getDomain() const
Definition: Expr.h:529
AssignmentEvaluator(const Assignment &_a)
Definition: Assignment.h:64
ref< Expr > getInitialValue(const Array &mo, unsigned index)
Definition: Assignment.h:59
const Assignment & a
Definition: Assignment.h:56
bool satisfies(InputIterator begin, InputIterator end)
Definition: Assignment.h:91
bool allowFreeValues
Definition: Assignment.h:25
std::map< const Array *, std::vector< unsigned char > > bindings_ty
Definition: Assignment.h:23
ref< Expr > evaluate(const Array *mo, unsigned index) const
Definition: Assignment.h:69
Assignment(bool _allowFreeValues=false)
Definition: Assignment.h:29
ConstraintSet createConstraintsFromAssignment() const
Definition: Assignment.cpp:28
bindings_ty bindings
Definition: Assignment.h:26
Assignment(const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool _allowFreeValues=false)
Definition: Assignment.h:31
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:1065
ref< Expr > visit(const ref< Expr > &e)
Definition: ExprVisitor.cpp:26
bool isTrue() const
isTrue - Is this the true expression.
Definition: Expr.h:1156
static ref< Expr > create(const UpdateList &updates, ref< Expr > i)
Definition: Expr.cpp:538
Class representing a complete list of updates into an array.
Definition: Expr.h:539
Definition: main.cpp:291