klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
STPBuilder.h
Go to the documentation of this file.
1 //===-- STPBuilder.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 __UTIL_STPBUILDER_H__
11 #define __UTIL_STPBUILDER_H__
12 
13 #include "klee/util/ExprHashMap.h"
15 #include "klee/Config/config.h"
16 
17 #include <vector>
18 
19 #define Expr VCExpr
20 #include <stp/c_interface.h>
21 
22 #if ENABLE_STPLOG == 1
23 #include "stp/stplog.h"
24 #endif
25 #undef Expr
26 
27 namespace klee {
28  class ExprHolder {
29  friend class ExprHandle;
30  ::VCExpr expr;
31  unsigned count;
32 
33  public:
34  ExprHolder(const ::VCExpr _expr) : expr(_expr), count(0) {}
36  if (expr) vc_DeleteExpr(expr);
37  }
38  };
39 
40  class ExprHandle {
42 
43  public:
44  ExprHandle() : H(new ExprHolder(0)) { H->count++; }
45  ExprHandle(::VCExpr _expr) : H(new ExprHolder(_expr)) { H->count++; }
46  ExprHandle(const ExprHandle &b) : H(b.H) { H->count++; }
47  ~ExprHandle() { if (--H->count == 0) delete H; }
48 
50  if (--H->count == 0) delete H;
51  H = b.H;
52  H->count++;
53  return *this;
54  }
55 
56  operator bool () { return H->expr; }
57  operator ::VCExpr () { return H->expr; }
58  };
59 
60  class STPArrayExprHash : public ArrayExprHash< ::VCExpr > {
61 
62  friend class STPBuilder;
63 
64  public:
66  virtual ~STPArrayExprHash();
67  };
68 
69 class STPBuilder {
70  ::VC vc;
73 
78 
80 
81 private:
82 
83  ExprHandle bvOne(unsigned width);
84  ExprHandle bvZero(unsigned width);
85  ExprHandle bvMinusOne(unsigned width);
86  ExprHandle bvConst32(unsigned width, uint32_t value);
87  ExprHandle bvConst64(unsigned width, uint64_t value);
88  ExprHandle bvZExtConst(unsigned width, uint64_t value);
89  ExprHandle bvSExtConst(unsigned width, uint64_t value);
90 
91  ExprHandle bvBoolExtract(ExprHandle expr, int bit);
92  ExprHandle bvExtract(ExprHandle expr, unsigned top, unsigned bottom);
94 
95  //logical left and right shift (not arithmetic)
96  ExprHandle bvLeftShift(ExprHandle expr, unsigned shift);
97  ExprHandle bvRightShift(ExprHandle expr, unsigned shift);
101 
102  ExprHandle constructAShrByConstant(ExprHandle expr, unsigned shift,
103  ExprHandle isSigned);
104  ExprHandle constructMulByConstant(ExprHandle expr, unsigned width, uint64_t x);
105  ExprHandle constructUDivByConstant(ExprHandle expr_n, unsigned width, uint64_t d);
106  ExprHandle constructSDivByConstant(ExprHandle expr_n, unsigned width, uint64_t d);
107 
108  ::VCExpr getInitialArray(const Array *os);
109  ::VCExpr getArrayForUpdate(const Array *root, const UpdateNode *un);
110 
111  ExprHandle constructActual(ref<Expr> e, int *width_out);
112  ExprHandle construct(ref<Expr> e, int *width_out);
113 
114  ::VCExpr buildVar(const char *name, unsigned width);
115  ::VCExpr buildArray(const char *name, unsigned indexWidth, unsigned valueWidth);
116 
117 public:
118  STPBuilder(::VC _vc, bool _optimizeDivides=true);
119  ~STPBuilder();
120 
124  ExprHandle getInitialRead(const Array *os, unsigned index);
125 
127  ExprHandle res = construct(e, 0);
128  constructed.clear();
129  return res;
130  }
131 };
132 
133 }
134 
135 #endif
ExprHandle getTrue()
Definition: STPBuilder.cpp:129
ExprHandle(::VCExpr _expr)
Definition: STPBuilder.h:45
::VCExpr expr
Definition: STPBuilder.h:30
::VCExpr buildVar(const char *name, unsigned width)
Definition: STPBuilder.cpp:99
STPArrayExprHash _arr_hash
Definition: STPBuilder.h:79
ExprHandle bvConst32(unsigned width, uint32_t value)
Definition: STPBuilder.cpp:144
ExprHandle bvZero(unsigned width)
Definition: STPBuilder.cpp:138
ExprHandle tempVars[4]
Definition: STPBuilder.h:71
ExprHolder * H
Definition: STPBuilder.h:41
ExprHandle getTempVar(Expr::Width w)
Definition: STPBuilder.cpp:119
ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle shift)
Definition: STPBuilder.cpp:229
ExprHandle eqExpr(ExprHandle a, ExprHandle b)
Definition: STPBuilder.cpp:171
ExprHandle construct(ref< Expr > e, int *width_out)
Definition: STPBuilder.cpp:491
ExprHandle constructMulByConstant(ExprHandle expr, unsigned width, uint64_t x)
Definition: STPBuilder.cpp:298
::VCExpr getInitialArray(const Array *os)
Definition: STPBuilder.cpp:426
::VCExpr buildArray(const char *name, unsigned indexWidth, unsigned valueWidth)
Definition: STPBuilder.cpp:107
ExprHandle bvMinusOne(unsigned width)
Definition: STPBuilder.cpp:141
::VCExpr getArrayForUpdate(const Array *root, const UpdateNode *un)
Definition: STPBuilder.cpp:466
ExprHandle bvExtract(ExprHandle expr, unsigned top, unsigned bottom)
Definition: STPBuilder.cpp:168
ExprHandle bvSExtConst(unsigned width, uint64_t value)
Definition: STPBuilder.cpp:159
ExprHolder(const ::VCExpr _expr)
Definition: STPBuilder.h:34
ExprHandle constructUDivByConstant(ExprHandle expr_n, unsigned width, uint64_t d)
Definition: STPBuilder.cpp:351
ExprHandle bvOne(unsigned width)
Definition: STPBuilder.cpp:135
ExprHandle bvZExtConst(unsigned width, uint64_t value)
Definition: STPBuilder.cpp:150
ExprHashMap< std::pair< ExprHandle, unsigned > > constructed
Definition: STPBuilder.h:72
ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle shift)
Definition: STPBuilder.cpp:208
ExprHandle constructAShrByConstant(ExprHandle expr, unsigned shift, ExprHandle isSigned)
Definition: STPBuilder.cpp:279
ExprHandle bvLeftShift(ExprHandle expr, unsigned shift)
Definition: STPBuilder.cpp:191
unsigned Width
The type of an expression is simply its width, in bits.
Definition: Expr.h:94
ExprHandle constructActual(ref< Expr > e, int *width_out)
Definition: STPBuilder.cpp:514
ExprHandle & operator=(const ExprHandle &b)
Definition: STPBuilder.h:49
virtual ~STPArrayExprHash()
Definition: STPBuilder.cpp:53
ExprHandle bvBoolExtract(ExprHandle expr, int bit)
Definition: STPBuilder.cpp:165
ExprHandle getFalse()
Definition: STPBuilder.cpp:132
ExprHandle constructSDivByConstant(ExprHandle expr_n, unsigned width, uint64_t d)
Definition: STPBuilder.cpp:388
Class representing a byte update of an array.
Definition: Expr.h:569
unsigned count
Definition: STPBuilder.h:31
ExprHandle bvRightShift(ExprHandle expr, unsigned shift)
Definition: STPBuilder.cpp:176
ExprHandle getInitialRead(const Array *os, unsigned index)
Definition: STPBuilder.cpp:462
ExprHandle construct(ref< Expr > e)
Definition: STPBuilder.h:126
ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle shift)
Definition: STPBuilder.cpp:250
STPBuilder(::VC _vc, bool _optimizeDivides=true)
Definition: STPBuilder.cpp:80
ExprHandle bvConst64(unsigned width, uint64_t value)
Definition: STPBuilder.cpp:147
void vc_DeleteExpr(void *)
ExprHandle(const ExprHandle &b)
Definition: STPBuilder.h:46
bool optimizeDivides
Definition: STPBuilder.h:77