aboutsummaryrefslogtreecommitdiffhomepage
path: root/include
diff options
context:
space:
mode:
Diffstat (limited to 'include')
-rw-r--r--include/klee/Expr.h308
1 files changed, 151 insertions, 157 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 2f24ffa4..9ad1b49a 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -324,163 +324,6 @@ inline std::stringstream &operator<<(std::stringstream &os, const Expr::Kind kin
return os;
}
-// Terminal Exprs
-
-class ConstantExpr : public Expr {
-public:
- static const Kind kind = Constant;
- static const unsigned numKids = 0;
-
-private:
- llvm::APInt value;
-
- ConstantExpr(const llvm::APInt &v) : value(v) {}
-
-public:
- ~ConstantExpr() {}
-
- Width getWidth() const { return value.getBitWidth(); }
- Kind getKind() const { return Constant; }
-
- unsigned getNumKids() const { return 0; }
- ref<Expr> getKid(unsigned i) const { return 0; }
-
- /// getAPValue - Return the arbitrary precision value directly.
- ///
- /// Clients should generally not use the APInt value directly and instead use
- /// native ConstantExpr APIs.
- const llvm::APInt &getAPValue() const { return value; }
-
- /// getZExtValue - Returns the constant value zero extended to the
- /// return type of this method.
- ///
- ///\param bits - optional parameter that can be used to check that the
- ///number of bits used by this constant is <= to the parameter
- ///value. This is useful for checking that type casts won't truncate
- ///useful bits.
- ///
- /// Example: unit8_t byte= (unit8_t) constant->getZExtValue(8);
- uint64_t getZExtValue(unsigned bits = 64) const {
- assert(getWidth() <= bits && "Value may be out of range!");
- return value.getZExtValue();
- }
-
- /// getLimitedValue - If this value is smaller than the specified limit,
- /// return it, otherwise return the limit value.
- uint64_t getLimitedValue(uint64_t Limit = ~0ULL) const {
- return value.getLimitedValue(Limit);
- }
-
- /// toString - Return the constant value as a string
- /// \param Res specifies the string for the result to be placed in
- /// \param radix specifies the base (e.g. 2,10,16). The default is base 10
- void toString(std::string &Res, unsigned radix=10) const;
-
-
-
- int compareContents(const Expr &b) const {
- const ConstantExpr &cb = static_cast<const ConstantExpr&>(b);
- if (getWidth() != cb.getWidth())
- return getWidth() < cb.getWidth() ? -1 : 1;
- if (value == cb.value)
- return 0;
- return value.ult(cb.value) ? -1 : 1;
- }
-
- virtual ref<Expr> rebuild(ref<Expr> kids[]) const {
- assert(0 && "rebuild() on ConstantExpr");
- return const_cast<ConstantExpr*>(this);
- }
-
- virtual unsigned computeHash();
-
- static ref<Expr> fromMemory(void *address, Width w);
- void toMemory(void *address);
-
- static ref<ConstantExpr> alloc(const llvm::APInt &v) {
- ref<ConstantExpr> r(new ConstantExpr(v));
- r->computeHash();
- return r;
- }
-
- static ref<ConstantExpr> alloc(const llvm::APFloat &f) {
- return alloc(f.bitcastToAPInt());
- }
-
- static ref<ConstantExpr> alloc(uint64_t v, Width w) {
- return alloc(llvm::APInt(w, v));
- }
-
- static ref<ConstantExpr> create(uint64_t v, Width w) {
- assert(v == bits64::truncateToNBits(v, w) &&
- "invalid constant");
- return alloc(v, w);
- }
-
- static bool classof(const Expr *E) {
- return E->getKind() == Expr::Constant;
- }
- static bool classof(const ConstantExpr *) { return true; }
-
- /* Utility Functions */
-
- /// isZero - Is this a constant zero.
- bool isZero() const { return getAPValue().isMinValue(); }
-
- /// isOne - Is this a constant one.
- bool isOne() const { return getLimitedValue() == 1; }
-
- /// isTrue - Is this the true expression.
- bool isTrue() const {
- return (getWidth() == Expr::Bool && value.getBoolValue()==true);
- }
-
- /// isFalse - Is this the false expression.
- bool isFalse() const {
- return (getWidth() == Expr::Bool && value.getBoolValue()==false);
- }
-
- /// isAllOnes - Is this constant all ones.
- bool isAllOnes() const { return getAPValue().isAllOnesValue(); }
-
- /* Constant Operations */
-
- ref<ConstantExpr> Concat(const ref<ConstantExpr> &RHS);
- ref<ConstantExpr> Extract(unsigned offset, Width W);
- ref<ConstantExpr> ZExt(Width W);
- ref<ConstantExpr> SExt(Width W);
- ref<ConstantExpr> Add(const ref<ConstantExpr> &RHS);
- ref<ConstantExpr> Sub(const ref<ConstantExpr> &RHS);
- ref<ConstantExpr> Mul(const ref<ConstantExpr> &RHS);
- ref<ConstantExpr> UDiv(const ref<ConstantExpr> &RHS);
- ref<ConstantExpr> SDiv(const ref<ConstantExpr> &RHS);
- ref<ConstantExpr> URem(const ref<ConstantExpr> &RHS);
- ref<ConstantExpr> SRem(const ref<ConstantExpr> &RHS);
- ref<ConstantExpr> And(const ref<ConstantExpr> &RHS);
- ref<ConstantExpr> Or(const ref<ConstantExpr> &RHS);
- ref<ConstantExpr> Xor(const ref<ConstantExpr> &RHS);
- ref<ConstantExpr> Shl(const ref<ConstantExpr> &RHS);
- ref<ConstantExpr> LShr(const ref<ConstantExpr> &RHS);
- ref<ConstantExpr> AShr(const ref<ConstantExpr> &RHS);
-
- // Comparisons return a constant expression of width 1.
-
- ref<ConstantExpr> Eq(const ref<ConstantExpr> &RHS);
- ref<ConstantExpr> Ne(const ref<ConstantExpr> &RHS);
- ref<ConstantExpr> Ult(const ref<ConstantExpr> &RHS);
- ref<ConstantExpr> Ule(const ref<ConstantExpr> &RHS);
- ref<ConstantExpr> Ugt(const ref<ConstantExpr> &RHS);
- ref<ConstantExpr> Uge(const ref<ConstantExpr> &RHS);
- ref<ConstantExpr> Slt(const ref<ConstantExpr> &RHS);
- ref<ConstantExpr> Sle(const ref<ConstantExpr> &RHS);
- ref<ConstantExpr> Sgt(const ref<ConstantExpr> &RHS);
- ref<ConstantExpr> Sge(const ref<ConstantExpr> &RHS);
-
- ref<ConstantExpr> Neg();
- ref<ConstantExpr> Not();
-};
-
-
// Utility classes
class NonConstantExpr : public Expr {
@@ -1089,6 +932,157 @@ COMPARISON_EXPR_CLASS(Sle)
COMPARISON_EXPR_CLASS(Sgt)
COMPARISON_EXPR_CLASS(Sge)
+// Terminal Exprs
+
+class ConstantExpr : public Expr {
+public:
+ static const Kind kind = Constant;
+ static const unsigned numKids = 0;
+
+private:
+ llvm::APInt value;
+
+ ConstantExpr(const llvm::APInt &v) : value(v) {}
+
+public:
+ ~ConstantExpr() {}
+
+ Width getWidth() const { return value.getBitWidth(); }
+ Kind getKind() const { return Constant; }
+
+ unsigned getNumKids() const { return 0; }
+ ref<Expr> getKid(unsigned i) const { return 0; }
+
+ /// getAPValue - Return the arbitrary precision value directly.
+ ///
+ /// Clients should generally not use the APInt value directly and instead use
+ /// native ConstantExpr APIs.
+ const llvm::APInt &getAPValue() const { return value; }
+
+ /// getZExtValue - Returns the constant value zero extended to the
+ /// return type of this method.
+ ///
+ ///\param bits - optional parameter that can be used to check that the
+ /// number of bits used by this constant is <= to the parameter
+ /// value. This is useful for checking that type casts won't truncate
+ /// useful bits.
+ ///
+ /// Example: unit8_t byte= (unit8_t) constant->getZExtValue(8);
+ uint64_t getZExtValue(unsigned bits = 64) const {
+ assert(getWidth() <= bits && "Value may be out of range!");
+ return value.getZExtValue();
+ }
+
+ /// getLimitedValue - If this value is smaller than the specified limit,
+ /// return it, otherwise return the limit value.
+ uint64_t getLimitedValue(uint64_t Limit = ~0ULL) const {
+ return value.getLimitedValue(Limit);
+ }
+
+ /// toString - Return the constant value as a string
+ /// \param Res specifies the string for the result to be placed in
+ /// \param radix specifies the base (e.g. 2,10,16). The default is base 10
+ void toString(std::string &Res, unsigned radix = 10) const;
+
+ int compareContents(const Expr &b) const {
+ const ConstantExpr &cb = static_cast<const ConstantExpr &>(b);
+ if (getWidth() != cb.getWidth())
+ return getWidth() < cb.getWidth() ? -1 : 1;
+ if (value == cb.value)
+ return 0;
+ return value.ult(cb.value) ? -1 : 1;
+ }
+
+ virtual ref<Expr> rebuild(ref<Expr> kids[]) const {
+ assert(0 && "rebuild() on ConstantExpr");
+ return const_cast<ConstantExpr *>(this);
+ }
+
+ virtual unsigned computeHash();
+
+ static ref<Expr> fromMemory(void *address, Width w);
+ void toMemory(void *address);
+
+ static ref<ConstantExpr> alloc(const llvm::APInt &v) {
+ ref<ConstantExpr> r(new ConstantExpr(v));
+ r->computeHash();
+ return r;
+ }
+
+ static ref<ConstantExpr> alloc(const llvm::APFloat &f) {
+ return alloc(f.bitcastToAPInt());
+ }
+
+ static ref<ConstantExpr> alloc(uint64_t v, Width w) {
+ return alloc(llvm::APInt(w, v));
+ }
+
+ static ref<ConstantExpr> create(uint64_t v, Width w) {
+ assert(v == bits64::truncateToNBits(v, w) && "invalid constant");
+ return alloc(v, w);
+ }
+
+ static bool classof(const Expr *E) { return E->getKind() == Expr::Constant; }
+ static bool classof(const ConstantExpr *) { return true; }
+
+ /* Utility Functions */
+
+ /// isZero - Is this a constant zero.
+ bool isZero() const { return getAPValue().isMinValue(); }
+
+ /// isOne - Is this a constant one.
+ bool isOne() const { return getLimitedValue() == 1; }
+
+ /// isTrue - Is this the true expression.
+ bool isTrue() const {
+ return (getWidth() == Expr::Bool && value.getBoolValue() == true);
+ }
+
+ /// isFalse - Is this the false expression.
+ bool isFalse() const {
+ return (getWidth() == Expr::Bool && value.getBoolValue() == false);
+ }
+
+ /// isAllOnes - Is this constant all ones.
+ bool isAllOnes() const { return getAPValue().isAllOnesValue(); }
+
+ /* Constant Operations */
+
+ ref<ConstantExpr> Concat(const ref<ConstantExpr> &RHS);
+ ref<ConstantExpr> Extract(unsigned offset, Width W);
+ ref<ConstantExpr> ZExt(Width W);
+ ref<ConstantExpr> SExt(Width W);
+ ref<ConstantExpr> Add(const ref<ConstantExpr> &RHS);
+ ref<ConstantExpr> Sub(const ref<ConstantExpr> &RHS);
+ ref<ConstantExpr> Mul(const ref<ConstantExpr> &RHS);
+ ref<ConstantExpr> UDiv(const ref<ConstantExpr> &RHS);
+ ref<ConstantExpr> SDiv(const ref<ConstantExpr> &RHS);
+ ref<ConstantExpr> URem(const ref<ConstantExpr> &RHS);
+ ref<ConstantExpr> SRem(const ref<ConstantExpr> &RHS);
+ ref<ConstantExpr> And(const ref<ConstantExpr> &RHS);
+ ref<ConstantExpr> Or(const ref<ConstantExpr> &RHS);
+ ref<ConstantExpr> Xor(const ref<ConstantExpr> &RHS);
+ ref<ConstantExpr> Shl(const ref<ConstantExpr> &RHS);
+ ref<ConstantExpr> LShr(const ref<ConstantExpr> &RHS);
+ ref<ConstantExpr> AShr(const ref<ConstantExpr> &RHS);
+
+ // Comparisons return a constant expression of width 1.
+
+ ref<ConstantExpr> Eq(const ref<ConstantExpr> &RHS);
+ ref<ConstantExpr> Ne(const ref<ConstantExpr> &RHS);
+ ref<ConstantExpr> Ult(const ref<ConstantExpr> &RHS);
+ ref<ConstantExpr> Ule(const ref<ConstantExpr> &RHS);
+ ref<ConstantExpr> Ugt(const ref<ConstantExpr> &RHS);
+ ref<ConstantExpr> Uge(const ref<ConstantExpr> &RHS);
+ ref<ConstantExpr> Slt(const ref<ConstantExpr> &RHS);
+ ref<ConstantExpr> Sle(const ref<ConstantExpr> &RHS);
+ ref<ConstantExpr> Sgt(const ref<ConstantExpr> &RHS);
+ ref<ConstantExpr> Sge(const ref<ConstantExpr> &RHS);
+
+ ref<ConstantExpr> Neg();
+ ref<ConstantExpr> Not();
+};
+
// Implementations
inline bool Expr::isZero() const {
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-24 18:27:39 +0000