aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile2
-rw-r--r--include/klee/Expr.h6
-rw-r--r--include/klee/Internal/Support/QueryLog.h2
-rw-r--r--include/klee/Solver.h2
-rw-r--r--include/klee/util/Assignment.h6
-rw-r--r--include/klee/util/Ref.h61
-rw-r--r--lib/Core/ExecutionState.cpp3
-rw-r--r--lib/Core/Executor.cpp58
-rw-r--r--lib/Core/ExecutorUtil.cpp4
-rw-r--r--lib/Core/ImpliedValue.cpp5
-rw-r--r--lib/Core/Memory.h6
-rw-r--r--lib/Core/SeedInfo.cpp12
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp2
-rw-r--r--lib/Core/TimingSolver.cpp2
-rw-r--r--lib/Expr/Constraints.cpp4
-rw-r--r--lib/Expr/Expr.cpp44
-rw-r--r--lib/Expr/ExprEvaluator.cpp2
-rw-r--r--lib/Expr/ExprPPrinter.cpp7
-rw-r--r--lib/Expr/Parser.cpp61
-rw-r--r--lib/Solver/FastCexSolver.cpp4
-rw-r--r--lib/Solver/Solver.cpp6
-rw-r--r--unittests/Expr/ExprTest.cpp6
22 files changed, 133 insertions, 172 deletions
diff --git a/Makefile b/Makefile
index db11c416..2c3ab72b 100644
--- a/Makefile
+++ b/Makefile
@@ -33,7 +33,7 @@ doxygen:
.PHONY: cscope.files
cscope.files:
find \
- lib include stp tools runtime examples unittests test www/code-examples \
+ lib include stp tools runtime examples unittests test \
-name Makefile -or \
-name \*.in -or \
-name \*.c -or \
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index d16a09bf..cb5423e0 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -238,7 +238,7 @@ struct Expr::CreateArg {
ref<Expr> expr;
Width width;
- CreateArg(Width w = Bool) : expr(0, Expr::Bool), width(w) {}
+ CreateArg(Width w = Bool) : expr(0), width(w) {}
CreateArg(ref<Expr> e) : expr(e), width(Expr::InvalidWidth) {}
bool isExpr() { return !isWidth(); }
@@ -328,12 +328,12 @@ public:
static ref<ConstantExpr> fromMemory(void *address, Width w);
void toMemory(void *address);
- static ref<ConstantExpr> alloc(uint64_t v, Width w) {
+ static ref<Expr> alloc(uint64_t v, Width w) {
// constructs an "optimized" ConstantExpr
return ref<ConstantExpr>(v, w);
}
- static ref<ConstantExpr> create(uint64_t v, Width w) {
+ static ref<Expr> create(uint64_t v, Width w) {
assert(v == bits64::truncateToNBits(v, w) &&
"invalid constant");
return alloc(v, w);
diff --git a/include/klee/Internal/Support/QueryLog.h b/include/klee/Internal/Support/QueryLog.h
index b090d2d9..212ab760 100644
--- a/include/klee/Internal/Support/QueryLog.h
+++ b/include/klee/Internal/Support/QueryLog.h
@@ -35,7 +35,7 @@ namespace klee {
std::vector<const Array*> objects;
public:
- QueryLogEntry() : query(0,Expr::Bool) {}
+ QueryLogEntry() : query(ConstantExpr::alloc(0,Expr::Bool)) {}
QueryLogEntry(const QueryLogEntry &b);
QueryLogEntry(const Query &_query,
Type _type,
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index a053050d..1ed8c175 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -35,7 +35,7 @@ namespace klee {
/// withFalse - Return a copy of the query with a false expression.
Query withFalse() const {
- return Query(constraints, ref<Expr>(0, Expr::Bool));
+ return Query(constraints, ConstantExpr::alloc(0, Expr::Bool));
}
/// negateExpr - Return a copy of the query with the expression negated.
diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h
index 19f89a03..cb001415 100644
--- a/include/klee/util/Assignment.h
+++ b/include/klee/util/Assignment.h
@@ -69,13 +69,13 @@ namespace klee {
unsigned index) const {
bindings_ty::const_iterator it = bindings.find(array);
if (it!=bindings.end() && index<it->second.size()) {
- return ref<Expr>(it->second[index], Expr::Int8);
+ return ConstantExpr::alloc(it->second[index], Expr::Int8);
} else {
if (allowFreeValues) {
return ReadExpr::create(UpdateList(array, true, 0),
- ref<Expr>(index, Expr::Int32));
+ ConstantExpr::alloc(index, Expr::Int32));
} else {
- return ref<Expr>(0, Expr::Int8);
+ return ConstantExpr::alloc(0, Expr::Int8);
}
}
}
diff --git a/include/klee/util/Ref.h b/include/klee/util/Ref.h
index a70b09cf..f900f137 100644
--- a/include/klee/util/Ref.h
+++ b/include/klee/util/Ref.h
@@ -13,48 +13,11 @@
#include <assert.h>
class Expr;
-class BinaryExpr;
-class CastExpr;
-class CmpExpr;
-
class ConstantExpr;
-class ReadExpr;
-class UpdateNode;
-class NotOptimizedExpr;
-class ReadExpr;
-class SelectExpr;
-class ConcatExpr;
-class ExtractExpr;
-class ZExtExpr;
-class SExtExpr;
-class AddExpr;
-class SubExpr;
-class MulExpr;
-class UDivExpr;
-class SDivExpr;
-class URemExpr;
-class SRemExpr;
-class AndExpr;
-class OrExpr;
-class XorExpr;
-class ShlExpr;
-class LShrExpr;
-class AShrExpr;
-class EqExpr;
-class NeExpr;
-class UltExpr;
-class UleExpr;
-class UgtExpr;
-class UgeExpr;
-class SltExpr;
-class SleExpr;
-class SgtExpr;
-class SgeExpr;
-class KModule;
-
- class ExprVisitor;
- class StackFrame;
- class ObjectState;
+
+class ExprVisitor;
+class StackFrame;
+class ObjectState;
template<class T>
class ref {
@@ -91,9 +54,12 @@ private:
}
friend class ExprVisitor;
- friend class Cell;
- friend class ObjectState;
- friend class KModule;
+ friend class ConstantExpr;
+
+ // construct from constant
+ ref(uint64_t val, Expr::Width w) : constantWidth(w) {
+ contents.val = val;
+ }
public:
template<class U> friend class ref;
@@ -107,14 +73,9 @@ public:
contents.ptr = p;
inc();
}
-
- // construct from constant
- ref(uint64_t val, Expr::Width w) : constantWidth(w) {
- contents.val = val;
- }
// normal copy constructor
- ref (const ref<T> &r)
+ ref(const ref<T> &r)
: constantWidth(r.constantWidth), contents(r.contents) {
inc();
}
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index dd6d4647..d07b6490 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -247,7 +247,8 @@ bool ExecutionState::merge(const ExecutionState &b) {
// merge stack
- ref<Expr> inA(1, Expr::Bool), inB(1, Expr::Bool);
+ ref<Expr> inA = ConstantExpr::alloc(1, Expr::Bool);
+ ref<Expr> inB = ConstantExpr::alloc(1, Expr::Bool);
for (std::set< ref<Expr> >::iterator it = aSuffix.begin(),
ie = aSuffix.end(); it != ie; ++it)
inA = AndExpr::create(inA, *it);
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 9c6d84cd..c3d2fcb4 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -902,7 +902,7 @@ void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
state.addConstraint(condition);
if (ivcEnabled)
- doImpliedValueConcretization(state, condition, ref<Expr>(1, Expr::Bool));
+ doImpliedValueConcretization(state, condition, ConstantExpr::alloc(1, Expr::Bool));
}
ref<Expr> Executor::evalConstant(Constant *c) {
@@ -1268,7 +1268,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
KInstIterator kcaller = state.stack.back().caller;
Instruction *caller = kcaller ? kcaller->inst : 0;
bool isVoidReturn = (ri->getNumOperands() == 0);
- ref<Expr> result(0,Expr::Bool);
+ ref<Expr> result = ConstantExpr::alloc(0, Expr::Bool);
if (WriteTraces) {
state.exeTraceMgr.addEvent(new FunctionReturnTraceEvent(state, ki));
@@ -1402,7 +1402,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
transferToBasicBlock(si->getSuccessor(index), si->getParent(), state);
} else {
std::map<BasicBlock*, ref<Expr> > targets;
- ref<Expr> isDefault(1,Expr::Bool);
+ ref<Expr> isDefault = ConstantExpr::alloc(1, Expr::Bool);
for (unsigned i=1; i<cases; ++i) {
ref<Expr> value = evalConstant(si->getCaseValue(i));
ref<Expr> match = EqExpr::create(cond, value);
@@ -1413,7 +1413,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
if (result) {
std::map<BasicBlock*, ref<Expr> >::iterator it =
targets.insert(std::make_pair(si->getSuccessor(i),
- ref<Expr>(0,Expr::Bool))).first;
+ ConstantExpr::alloc(0, Expr::Bool))).first;
it->second = OrExpr::create(match, it->second);
}
}
@@ -1587,9 +1587,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
// Arithmetic / logical
#define FP_CONSTANT_BINOP(op, type, l, r, target, state) \
bindLocal(target, state, \
- ref<Expr>(op(toConstant(state, l, "floating point").getConstantValue(), \
- toConstant(state, r, "floating point").getConstantValue(), \
- type), type))
+ ConstantExpr::alloc(op(toConstant(state, l, "floating point").getConstantValue(), \
+ toConstant(state, r, "floating point").getConstantValue(), \
+ type), type))
case Instruction::Add: {
BinaryOperator *bi = cast<BinaryOperator>(i);
ref<Expr> left = eval(ki, 0, state).value;
@@ -1915,8 +1915,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
uint64_t value = floats::trunc(arg.getConstantValue(),
resultType,
arg.getWidth());
- ref<Expr> result(value, resultType);
- bindLocal(ki, state, result);
+ bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
break;
}
@@ -1928,8 +1927,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
uint64_t value = floats::ext(arg.getConstantValue(),
resultType,
arg.getWidth());
- ref<Expr> result(value, resultType);
- bindLocal(ki, state, result);
+ bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
break;
}
@@ -1941,8 +1939,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
uint64_t value = floats::toUnsignedInt(arg.getConstantValue(),
resultType,
arg.getWidth());
- ref<Expr> result(value, resultType);
- bindLocal(ki, state, result);
+ bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
break;
}
@@ -1954,8 +1951,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
uint64_t value = floats::toSignedInt(arg.getConstantValue(),
resultType,
arg.getWidth());
- ref<Expr> result(value, resultType);
- bindLocal(ki, state, result);
+ bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
break;
}
@@ -1966,8 +1962,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
"floating point");
uint64_t value = floats::UnsignedIntToFP(arg.getConstantValue(),
resultType);
- ref<Expr> result(value, resultType);
- bindLocal(ki, state, result);
+ bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
break;
}
@@ -1979,8 +1974,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
uint64_t value = floats::SignedIntToFP(arg.getConstantValue(),
resultType,
arg.getWidth());
- ref<Expr> result(value, resultType);
- bindLocal(ki, state, result);
+ bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
break;
}
@@ -2088,8 +2082,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
}
}
- ref<Expr> result(ret, resultType);
- bindLocal(ki, state, result);
+ bindLocal(ki, state, ConstantExpr::alloc(ret, resultType));
break;
}
@@ -2630,7 +2623,7 @@ void Executor::executeAlloc(ExecutionState &state,
MemoryObject *mo = memory->allocate(size.getConstantValue(), isLocal, false,
state.prevPC->inst);
if (!mo) {
- bindLocal(target, state, ref<Expr>(0, kMachinePointerType));
+ bindLocal(target, state, ConstantExpr::alloc(0, kMachinePointerType));
} else {
ObjectState *os = bindObjectInState(state, mo, isLocal);
if (zeroMemory) {
@@ -2665,8 +2658,8 @@ void Executor::executeAlloc(ExecutionState &state,
// Try and start with a small example
while (example.getConstantValue()>128) {
- ref<Expr> tmp = ref<Expr>(example.getConstantValue() >> 1,
- example.getWidth());
+ ref<Expr> tmp = ConstantExpr::alloc(example.getConstantValue() >> 1,
+ example.getWidth());
bool res;
bool success = solver->mayBeTrue(state, EqExpr::create(tmp, size), res);
assert(success && "FIXME: Unhandled solver failure");
@@ -2693,12 +2686,15 @@ void Executor::executeAlloc(ExecutionState &state,
} else {
// See if a *really* big value is possible. If so assume
// malloc will fail for it, so lets fork and return 0.
- StatePair hugeSize = fork(*fixedSize.second,
- UltExpr::create(ref<Expr>(1<<31, Expr::Int32), size),
- true);
+ StatePair hugeSize =
+ fork(*fixedSize.second,
+ UltExpr::create(ConstantExpr::alloc(1<<31, Expr::Int32),
+ size),
+ true);
if (hugeSize.first) {
klee_message("NOTE: found huge malloc, returing 0");
- bindLocal(target, *hugeSize.first, ref<Expr>(0,kMachinePointerType));
+ bindLocal(target, *hugeSize.first,
+ ConstantExpr::alloc(0, kMachinePointerType));
}
if (hugeSize.second) {
@@ -3011,7 +3007,7 @@ void Executor::runFunctionAsMain(Function *f,
assert(kf);
Function::arg_iterator ai = f->arg_begin(), ae = f->arg_end();
if (ai!=ae) {
- arguments.push_back(ref<Expr>(argc, Expr::Int32));
+ arguments.push_back(ConstantExpr::alloc(argc, Expr::Int32));
if (++ai!=ae) {
argvMO = memory->allocate((argc+1+envc+1+1) * kMachinePointerSize, false, true,
@@ -3108,7 +3104,7 @@ void Executor::getConstraintLog(const ExecutionState &state,
std::string &res,
bool asCVC) {
if (asCVC) {
- Query query(state.constraints, ref<Expr>(0, Expr::Bool));
+ Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool));
char *log = solver->stpSolver->getConstraintLog(query);
res = std::string(log);
free(log);
@@ -3155,7 +3151,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state,
klee_warning("unable to compute initial values (invalid constraints?)!");
ExprPPrinter::printQuery(std::cerr,
state.constraints,
- ref<Expr>(0,Expr::Bool));
+ ConstantExpr::alloc(0, Expr::Bool));
return false;
}
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 3b11dd42..62aa45db 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -37,7 +37,7 @@ ref<Expr>
Executor::evalConstantExpr(llvm::ConstantExpr *ce) {
const llvm::Type *type = ce->getType();
- ref<Expr> op1(0,Expr::Bool), op2(0,Expr::Bool), op3(0,Expr::Bool);
+ ref<Expr> op1(0), op2(0), op3(0);
int numOperands = ce->getNumOperands();
if (numOperands > 0) op1 = evalConstant(ce->getOperand(0));
@@ -80,7 +80,7 @@ Executor::evalConstantExpr(llvm::ConstantExpr *ce) {
for (gep_type_iterator ii = gep_type_begin(ce), ie = gep_type_end(ce);
ii != ie; ++ii) {
- ref<Expr> addend(0, kMachinePointerType);
+ ref<Expr> addend = ConstantExpr::alloc(0, kMachinePointerType);
if (const StructType *st = dyn_cast<StructType>(*ii)) {
const StructLayout *sl = kmodule->targetData->getStructLayout(st);
diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp
index 386c8d80..1de47d0c 100644
--- a/lib/Core/ImpliedValue.cpp
+++ b/lib/Core/ImpliedValue.cpp
@@ -239,8 +239,9 @@ void ImpliedValue::checkForImpliedValues(Solver *S, ref<Expr> e,
for (std::vector< ref<ReadExpr> >::iterator i = reads.begin(),
ie = reads.end(); i != ie; ++i) {
ReadExpr *re = i->get();
- ref<Expr> size = ref<Expr>(re->updates.root->size, kMachinePointerType);
- assumption.push_back(UltExpr::create(re->index, size));
+ assumption.push_back(UltExpr::create(re->index,
+ ConstantExpr::alloc(re->updates.root->size,
+ kMachinePointerType)));
}
ConstraintManager assume(assumption);
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index 0f09b162..cfb4ab43 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -118,7 +118,7 @@ public:
ref<Expr> getBoundsCheckOffset(ref<Expr> offset) const {
if (size==0) {
- return EqExpr::create(offset, ref<Expr>(0, kMachinePointerType));
+ return EqExpr::create(offset, ConstantExpr::alloc(0, kMachinePointerType));
} else {
return UltExpr::create(offset, getSizeExpr());
}
@@ -126,9 +126,9 @@ public:
ref<Expr> getBoundsCheckOffset(ref<Expr> offset, unsigned bytes) const {
if (bytes<=size) {
return UltExpr::create(offset,
- ref<Expr>(size - bytes + 1, kMachinePointerType));
+ ConstantExpr::alloc(size - bytes + 1, kMachinePointerType));
} else {
- return ref<Expr>(0, Expr::Bool);
+ return ConstantExpr::alloc(0, Expr::Bool);
}
}
};
diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp
index e6d88bac..9369dcbc 100644
--- a/lib/Core/SeedInfo.cpp
+++ b/lib/Core/SeedInfo.cpp
@@ -88,12 +88,12 @@ void SeedInfo::patchSeed(const ExecutionState &state,
const Array *array = it->first;
unsigned i = it->second;
ref<Expr> read = ReadExpr::create(UpdateList(array, true, 0),
- ref<Expr>(i, Expr::Int32));
+ ConstantExpr::alloc(i, Expr::Int32));
// If not in bindings then this can't be a violation?
Assignment::bindings_ty::iterator it2 = assignment.bindings.find(array);
if (it2 != assignment.bindings.end()) {
- ref<Expr> isSeed = EqExpr::create(read, ref<Expr>(it2->second[i], Expr::Int8));
+ ref<Expr> isSeed = EqExpr::create(read, ConstantExpr::alloc(it2->second[i], Expr::Int8));
bool res;
bool success = solver->mustBeFalse(tmp, isSeed, res);
assert(success && "FIXME: Unhandled solver failure");
@@ -102,7 +102,7 @@ void SeedInfo::patchSeed(const ExecutionState &state,
bool success = solver->getValue(tmp, read, value);
assert(success && "FIXME: Unhandled solver failure");
it2->second[i] = value.getConstantValue();
- tmp.addConstraint(EqExpr::create(read, ref<Expr>(it2->second[i], Expr::Int8)));
+ tmp.addConstraint(EqExpr::create(read, ConstantExpr::alloc(it2->second[i], Expr::Int8)));
} else {
tmp.addConstraint(isSeed);
}
@@ -122,8 +122,8 @@ void SeedInfo::patchSeed(const ExecutionState &state,
const Array *array = it->first;
for (unsigned i=0; i<array->size; ++i) {
ref<Expr> read = ReadExpr::create(UpdateList(array, true, 0),
- ref<Expr>(i, Expr::Int32));
- ref<Expr> isSeed = EqExpr::create(read, ref<Expr>(it->second[i], Expr::Int8));
+ ConstantExpr::alloc(i, Expr::Int32));
+ ref<Expr> isSeed = EqExpr::create(read, ConstantExpr::alloc(it->second[i], Expr::Int8));
bool res;
bool success = solver->mustBeFalse(tmp, isSeed, res);
assert(success && "FIXME: Unhandled solver failure");
@@ -132,7 +132,7 @@ void SeedInfo::patchSeed(const ExecutionState &state,
bool success = solver->getValue(tmp, read, value);
assert(success && "FIXME: Unhandled solver failure");
it->second[i] = value.getConstantValue();
- tmp.addConstraint(EqExpr::create(read, ref<Expr>(it->second[i], Expr::Int8)));
+ tmp.addConstraint(EqExpr::create(read, ConstantExpr::alloc(it->second[i], Expr::Int8)));
} else {
tmp.addConstraint(isSeed);
}
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 3f7c442e..9f5a2347 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -386,7 +386,7 @@ void SpecialFunctionHandler::handlePreferCex(ExecutionState &state,
ref<Expr> cond = arguments[1];
if (cond.getWidth() != Expr::Bool)
- cond = NeExpr::create(cond, ref<Expr>(0, cond.getWidth()));
+ cond = NeExpr::create(cond, ConstantExpr::alloc(0, cond.getWidth()));
Executor::ExactResolutionList rl;
executor.resolveExact(state, arguments[0], rl, "prefex_cex");
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index 70e42836..4c09a1aa 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -130,7 +130,7 @@ TimingSolver::getInitialValues(const ExecutionState& state,
sys::Process::GetTimeUsage(now,user,sys);
bool success = solver->getInitialValues(Query(state.constraints,
- ref<Expr>(0, Expr::Bool)),
+ ConstantExpr::alloc(0, Expr::Bool)),
objects, result);
sys::Process::GetTimeUsage(delta,user,sys);
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
index e9c376f4..4c18a3b3 100644
--- a/lib/Expr/Constraints.cpp
+++ b/lib/Expr/Constraints.cpp
@@ -100,11 +100,11 @@ ref<Expr> ConstraintManager::simplifyExpr(ref<Expr> e) const {
ee->left));
} else {
equalities.insert(std::make_pair(*it,
- ref<Expr>(1,Expr::Bool)));
+ ConstantExpr::alloc(1, Expr::Bool)));
}
} else {
equalities.insert(std::make_pair(*it,
- ref<Expr>(1,Expr::Bool)));
+ ConstantExpr::alloc(1, Expr::Bool)));
}
}
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 55b9a0a4..7f20e3fc 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -43,42 +43,42 @@ ref<Expr> Expr::createTempRead(const Array *array, Expr::Width w) {
switch (w) {
case Expr::Bool:
return ZExtExpr::create(ReadExpr::create(ul,
- ref<Expr>(0,kMachinePointerType)),
+ ConstantExpr::alloc(0,kMachinePointerType)),
Expr::Bool);
case Expr::Int8:
return ReadExpr::create(ul,
- ref<Expr>(0,kMachinePointerType));
+ ConstantExpr::alloc(0,kMachinePointerType));
case Expr::Int16:
return ConcatExpr::create(ReadExpr::create(ul,
- ref<Expr>(1,kMachinePointerType)),
+ ConstantExpr::alloc(1,kMachinePointerType)),
ReadExpr::create(ul,
- ref<Expr>(0,kMachinePointerType)));
+ ConstantExpr::alloc(0,kMachinePointerType)));
case Expr::Int32:
return ConcatExpr::create4(ReadExpr::create(ul,
- ref<Expr>(3,kMachinePointerType)),
+ ConstantExpr::alloc(3,kMachinePointerType)),
ReadExpr::create(ul,
- ref<Expr>(2,kMachinePointerType)),
+ ConstantExpr::alloc(2,kMachinePointerType)),
ReadExpr::create(ul,
- ref<Expr>(1,kMachinePointerType)),
+ ConstantExpr::alloc(1,kMachinePointerType)),
ReadExpr::create(ul,
- ref<Expr>(0,kMachinePointerType)));
+ ConstantExpr::alloc(0,kMachinePointerType)));
case Expr::Int64:
return ConcatExpr::create8(ReadExpr::create(ul,
- ref<Expr>(7,kMachinePointerType)),
+ ConstantExpr::alloc(7,kMachinePointerType)),
ReadExpr::create(ul,
- ref<Expr>(6,kMachinePointerType)),
+ ConstantExpr::alloc(6,kMachinePointerType)),
ReadExpr::create(ul,
- ref<Expr>(5,kMachinePointerType)),
+ ConstantExpr::alloc(5,kMachinePointerType)),
ReadExpr::create(ul,
- ref<Expr>(4,kMachinePointerType)),
+ ConstantExpr::alloc(4,kMachinePointerType)),
ReadExpr::create(ul,
- ref<Expr>(3,kMachinePointerType)),
+ ConstantExpr::alloc(3,kMachinePointerType)),
ReadExpr::create(ul,
- ref<Expr>(2,kMachinePointerType)),
+ ConstantExpr::alloc(2,kMachinePointerType)),
ReadExpr::create(ul,
- ref<Expr>(1,kMachinePointerType)),
+ ConstantExpr::alloc(1,kMachinePointerType)),
ReadExpr::create(ul,
- ref<Expr>(0,kMachinePointerType)));
+ ConstantExpr::alloc(0,kMachinePointerType)));
default: assert(0 && "invalid width");
}
}
@@ -639,7 +639,7 @@ static ref<Expr> SubExpr_create(Expr *l, Expr *r) {
if (type == Expr::Bool) {
return XorExpr_create(l, r);
} else if (*l==*r) {
- return ref<Expr>(0, type);
+ return ConstantExpr::alloc(0, type);
} else {
Expr::Kind lk = l->getKind(), rk = r->getKind();
if (lk==Expr::Add && l->getKid(0).isConstant()) { // (k+a)-b = k+(a-b)
@@ -891,7 +891,7 @@ ref<Expr> _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) { \
static ref<Expr> EqExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
if (l == r) {
- return ref<Expr>(1, Expr::Bool);
+ return ConstantExpr::alloc(1, Expr::Bool);
} else {
return EqExpr::alloc(l, r);
}
@@ -952,7 +952,7 @@ static ref<Expr> TryConstArrayOpt(const ref<Expr> &cl,
//llvm::cerr << "\n\n=== Applying const array optimization ===\n\n";
if (matches == 0)
- return ref<Expr>(0, Expr::Bool);
+ return ConstantExpr::alloc(0, Expr::Bool);
ref<Expr> res = EqExpr::create(first_idx_match, rd->index);
if (matches == 1)
@@ -1079,11 +1079,11 @@ static ref<Expr> UltExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
if (r.isConstant()) {
uint64_t value = r.getConstantValue();
if (value <= 8) {
- ref<Expr> res(0,Expr::Bool);
+ ref<Expr> res = ConstantExpr::alloc(0, Expr::Bool);
for (unsigned i=0; i<value; i++) {
- res = OrExpr::create(EqExpr::create(l, ref<Expr>(i,t)), res);
+ res = OrExpr::create(EqExpr::create(l,
+ ConstantExpr::alloc(i, t)), res);
}
- // llvm::cerr << l << "<" << r << " <=> " << res << "\n";
return res;
}
}
diff --git a/lib/Expr/ExprEvaluator.cpp b/lib/Expr/ExprEvaluator.cpp
index 102387e1..cf901f0e 100644
--- a/lib/Expr/ExprEvaluator.cpp
+++ b/lib/Expr/ExprEvaluator.cpp
@@ -26,7 +26,7 @@ ExprVisitor::Action ExprEvaluator::evalRead(const UpdateList &ul,
UpdateList fwd(ul.root, un, 0);
return Action::changeTo(ReadExpr::create(fwd,
- ref<Expr>(index,Expr::Int32)));
+ ConstantExpr::alloc(index, Expr::Int32)));
}
}
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index dc7f4f64..fd367f23 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -240,7 +240,8 @@ class PPrinter : public ExprPPrinter {
// Get stride expr in proper index width.
Expr::Width idxWidth = base->index.getWidth();
- ref<Expr> strideExpr(stride, idxWidth), offset(0, idxWidth);
+ ref<Expr> strideExpr = ConstantExpr::alloc(stride, idxWidth);
+ ref<Expr> offset = ConstantExpr::alloc(0, idxWidth);
for (unsigned i=1; i<ep->getNumKids(); ++i) {
const ReadExpr *re = dyn_ref_cast<ReadExpr>(ep->getKid(i));
if (!re)
@@ -357,7 +358,7 @@ public:
// Detect Not.
// FIXME: This should be in common code.
if (const EqExpr *ee = dyn_ref_cast<EqExpr>(e)) {
- if (ee->left == ref<Expr>(false, Expr::Bool)) {
+ if (ee->left == ConstantExpr::alloc(false, Expr::Bool)) {
PC << "(Not";
printWidth(PC, e);
PC << ' ';
@@ -443,7 +444,7 @@ void ExprPPrinter::printOne(std::ostream &os,
void ExprPPrinter::printConstraints(std::ostream &os,
const ConstraintManager &constraints) {
- printQuery(os, constraints, ref<Expr>(false, Expr::Bool));
+ printQuery(os, constraints, ConstantExpr::alloc(false, Expr::Bool));
}
void ExprPPrinter::printQuery(std::ostream &os,
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index dba089a5..a8ea0a6b 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -398,7 +398,7 @@ DeclResult ParserImpl::ParseQueryCommand() {
if (Tok.kind == Token::EndOfFile) {
Error("unexpected end of file.");
return new QueryCommand(Constraints.begin(), Constraints.end(),
- ref<Expr>(false, Expr::Bool));
+ ConstantExpr::alloc(false, Expr::Bool));
}
ExprResult Res = ParseExpr(TypeResult(Expr::Bool));
@@ -410,7 +410,7 @@ DeclResult ParserImpl::ParseQueryCommand() {
ExprResult Res = ParseExpr(TypeResult());
if (!Res.isValid()) // Error emitted by ParseExpr.
- Res = ExprResult(ref<Expr>(0, Expr::Bool));
+ Res = ExprResult(ConstantExpr::alloc(0, Expr::Bool));
ExpectRParen("unexpected argument to 'query'.");
return new QueryCommand(Constraints.begin(), Constraints.end(),
@@ -447,7 +447,7 @@ ExprResult ParserImpl::ParseExpr(TypeResult ExpectedType) {
if (Tok.kind == Token::KWFalse || Tok.kind == Token::KWTrue) {
bool Value = Tok.kind == Token::KWTrue;
ConsumeToken();
- return ExprResult(ref<Expr>(Value, Expr::Bool));
+ return ExprResult(ConstantExpr::alloc(Value, Expr::Bool));
}
if (Tok.kind == Token::Number) {
@@ -491,9 +491,10 @@ ExprResult ParserImpl::ParseExpr(TypeResult ExpectedType) {
// use-of-undef errors.
// FIXME: Maybe we should let the symbol table map to invalid
// entries?
- if (Label && ExpectedType.isValid())
- ExprSymTab.insert(std::make_pair(Label,
- ref<Expr>(0, ExpectedType.get())));
+ if (Label && ExpectedType.isValid()) {
+ ref<Expr> Value = ConstantExpr::alloc(0, ExpectedType.get());
+ ExprSymTab.insert(std::make_pair(Label, Value));
+ }
return Res;
} else if (ExpectedType.isValid()) {
// Type check result.
@@ -716,7 +717,7 @@ ExprResult ParserImpl::ParseParenExpr(TypeResult FIXME_UNUSED) {
default:
Error("internal error, unimplemented special form.", Name);
SkipUntilRParen();
- return ExprResult(ref<Expr>(0, ResTy));
+ return ExprResult(ConstantExpr::alloc(0, ResTy));
}
}
@@ -740,20 +741,20 @@ ExprResult ParserImpl::ParseUnaryParenExpr(const Token &Name,
if (Tok.kind == Token::RParen) {
Error("unexpected end of arguments.", Name);
ConsumeRParen();
- return ref<Expr>(0, ResTy);
+ return ConstantExpr::alloc(0, ResTy);
}
ExprResult Arg = ParseExpr(IsFixed ? ResTy : TypeResult());
if (!Arg.isValid())
- Arg = ref<Expr>(0, ResTy);
+ Arg = ConstantExpr::alloc(0, ResTy);
ExpectRParen("unexpected argument in unary expression.");
ExprHandle E = Arg.get();
switch (Kind) {
case eMacroKind_Not:
- return EqExpr::alloc(ref<Expr>(0, E.getWidth()), E);
+ return EqExpr::alloc(ConstantExpr::alloc(0, E.getWidth()), E);
case eMacroKind_Neg:
- return SubExpr::alloc(ref<Expr>(0, E.getWidth()), E);
+ return SubExpr::alloc(ConstantExpr::alloc(0, E.getWidth()), E);
case Expr::SExt:
// FIXME: Type check arguments.
return SExtExpr::alloc(E, ResTy);
@@ -762,7 +763,7 @@ ExprResult ParserImpl::ParseUnaryParenExpr(const Token &Name,
return ZExtExpr::alloc(E, ResTy);
default:
Error("internal error, unhandled kind.", Name);
- return ref<Expr>(0, ResTy);
+ return ConstantExpr::alloc(0, ResTy);
}
}
@@ -831,7 +832,7 @@ ExprResult ParserImpl::ParseBinaryParenExpr(const Token &Name,
ParseMatchedBinaryArgs(Name, IsFixed ? TypeResult(ResTy) : TypeResult(),
LHS, RHS);
if (!LHS.isValid() || !RHS.isValid())
- return ref<Expr>(0, ResTy);
+ return ConstantExpr::alloc(0, ResTy);
ref<Expr> LHS_E = LHS.get(), RHS_E = RHS.get();
assert(LHS_E.getWidth() == RHS_E.getWidth() && "Mismatched types!");
@@ -865,7 +866,7 @@ ExprResult ParserImpl::ParseBinaryParenExpr(const Token &Name,
case Expr::Sge: return SgeExpr::alloc(LHS_E, RHS_E);
default:
Error("FIXME: unhandled kind.", Name);
- return ref<Expr>(0, ResTy);
+ return ConstantExpr::alloc(0, ResTy);
}
}
@@ -875,14 +876,14 @@ ExprResult ParserImpl::ParseSelectParenExpr(const Token &Name,
if (Tok.kind == Token::RParen) {
Error("unexpected end of arguments.", Name);
ConsumeRParen();
- return ref<Expr>(0, ResTy);
+ return ConstantExpr::alloc(0, ResTy);
}
ExprResult Cond = ParseExpr(Expr::Bool);
ExprResult LHS, RHS;
ParseMatchedBinaryArgs(Name, ResTy, LHS, RHS);
if (!Cond.isValid() || !LHS.isValid() || !RHS.isValid())
- return ref<Expr>(0, ResTy);
+ return ConstantExpr::alloc(0, ResTy);
return SelectExpr::alloc(Cond.get(), LHS.get(), RHS.get());
}
@@ -900,7 +901,7 @@ ExprResult ParserImpl::ParseConcatParenExpr(const Token &Name,
// Skip to end of expr on error.
if (!E.isValid()) {
SkipUntilRParen();
- return ref<Expr>(0, ResTy);
+ return ConstantExpr::alloc(0, ResTy);
}
Kids.push_back(E.get());
@@ -911,7 +912,7 @@ ExprResult ParserImpl::ParseConcatParenExpr(const Token &Name,
if (Width != ResTy) {
Error("concat does not match expected result size.");
- return ref<Expr>(0, ResTy);
+ return ConstantExpr::alloc(0, ResTy);
}
return ConcatExpr::createN(Kids.size(), &Kids[0]);
@@ -926,14 +927,14 @@ ExprResult ParserImpl::ParseExtractParenExpr(const Token &Name,
ExpectRParen("unexpected argument to expression.");
if (!OffsetExpr.isValid() || !Child.isValid())
- return ref<Expr>(0, ResTy);
+ return ConstantExpr::alloc(0, ResTy);
assert(OffsetExpr.get().isConstant() && "ParseNumber returned non-constant.");
unsigned Offset = (unsigned) OffsetExpr.get().getConstantValue();
if (Offset + ResTy > Child.get().getWidth()) {
Error("extract out-of-range of child expression.", Name);
- return ref<Expr>(0, ResTy);
+ return ConstantExpr::alloc(0, ResTy);
}
return ExtractExpr::alloc(Child.get(), Offset, ResTy);
@@ -947,7 +948,7 @@ ExprResult ParserImpl::ParseAnyReadParenExpr(const Token &Name,
ExpectRParen("unexpected argument in read expression.");
if (!Array.isValid())
- return ref<Expr>(0, ResTy);
+ return ConstantExpr::alloc(0, ResTy);
// FIXME: Need generic way to get array width. Needs to work with
// anonymous arrays.
@@ -962,10 +963,10 @@ ExprResult ParserImpl::ParseAnyReadParenExpr(const Token &Name,
IndexExpr = Index.getExpr();
if (!IndexExpr.isValid())
- return ref<Expr>(0, ResTy);
+ return ConstantExpr::alloc(0, ResTy);
else if (IndexExpr.get().getWidth() != ArrayDomainType) {
Error("index width does not match array domain.");
- return ref<Expr>(0, ResTy);
+ return ConstantExpr::alloc(0, ResTy);
}
// FIXME: Check range width.
@@ -973,13 +974,13 @@ ExprResult ParserImpl::ParseAnyReadParenExpr(const Token &Name,
switch (Kind) {
default:
assert(0 && "Invalid kind.");
- return ref<Expr>(0, ResTy);
+ return ConstantExpr::alloc(0, ResTy);
case eMacroKind_ReadLSB:
case eMacroKind_ReadMSB: {
unsigned NumReads = ResTy / ArrayRangeType;
if (ResTy != NumReads*ArrayRangeType) {
Error("invalid ordered read (not multiple of range type).", Name);
- return ref<Expr>(0, ResTy);
+ return ConstantExpr::alloc(0, ResTy);
}
std::vector<ExprHandle> Kids;
Kids.reserve(NumReads);
@@ -987,7 +988,7 @@ ExprResult ParserImpl::ParseAnyReadParenExpr(const Token &Name,
for (unsigned i=0; i<NumReads; ++i) {
// FIXME: using folding here
ExprHandle OffsetIndex = AddExpr::create(IndexExpr.get(),
- ref<Expr>(i, ArrayDomainType));
+ ConstantExpr::alloc(i, ArrayDomainType));
Kids.push_back(ReadExpr::alloc(Array.get(), OffsetIndex));
}
if (Kind == eMacroKind_ReadLSB)
@@ -1185,7 +1186,7 @@ ExprResult ParserImpl::ParseNumberToken(Expr::Width Type, const Token &Tok) {
// Diagnose 0[box] with no trailing digits.
if (!N) {
Error("invalid numeric token (no digits).", Tok);
- return ref<Expr>(0, Type);
+ return ConstantExpr::alloc(0, Type);
}
}
@@ -1207,12 +1208,12 @@ ExprResult ParserImpl::ParseNumberToken(Expr::Width Type, const Token &Tok) {
Digit = Char - 'A' + 10;
else {
Error("invalid character in numeric token.", Tok);
- return ref<Expr>(0, Type);
+ return ConstantExpr::alloc(0, Type);
}
if (Digit >= Radix) {
Error("invalid character in numeric token (out of range).", Tok);
- return ref<Expr>(0, Type);
+ return ConstantExpr::alloc(0, Type);
}
DigitVal = Digit;
@@ -1223,7 +1224,7 @@ ExprResult ParserImpl::ParseNumberToken(Expr::Width Type, const Token &Tok) {
if (HasMinus)
Val = -Val;
- return ExprResult(ref<Expr>(Val.trunc(Type).getZExtValue(), Type));
+ return ExprResult(ConstantExpr::alloc(Val.trunc(Type).getZExtValue(), Type));
}
/// ParseTypeSpecifier - Parse a type specifier.
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index d2bc27c6..b6f676aa 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -358,11 +358,11 @@ protected:
if (index >= cod.size) {
return ReadExpr::create(UpdateList(&array, true, 0),
- ref<Expr>(index, Expr::Int32));
+ ConstantExpr::alloc(index, Expr::Int32));
} else {
CexValueData &cvd = cod.values[index];
assert(cvd.min() == cvd.max() && "value is not fixed");
- return ref<Expr>(cvd.min(), Expr::Int8);
+ return ConstantExpr::alloc(cvd.min(), Expr::Int8);
}
}
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 2a50ae0c..ae378ac1 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -327,8 +327,8 @@ ValidatingSolver::computeInitialValues(const Query& query,
unsigned char value = values[i][j];
bindings.push_back(EqExpr::create(ReadExpr::create(UpdateList(array,
true, 0),
- ref<Expr>(j, Expr::Int32)),
- ref<Expr>(value, Expr::Int8)));
+ ConstantExpr::alloc(j, Expr::Int32)),
+ ConstantExpr::alloc(value, Expr::Int8)));
}
}
ConstraintManager tmp(bindings);
@@ -439,7 +439,7 @@ char *STPSolverImpl::getConstraintLog(const Query &query) {
for (std::vector< ref<Expr> >::const_iterator it = query.constraints.begin(),
ie = query.constraints.end(); it != ie; ++it)
vc_assertFormula(vc, builder->construct(*it));
- assert(query.expr == ref<Expr>(0, Expr::Bool) &&
+ assert(query.expr == ConstantExpr::alloc(0, Expr::Bool) &&
"Unexpected expression in query!");
char *buffer;
diff --git a/unittests/Expr/ExprTest.cpp b/unittests/Expr/ExprTest.cpp
index 9220c53e..72b37ab2 100644
--- a/unittests/Expr/ExprTest.cpp
+++ b/unittests/Expr/ExprTest.cpp
@@ -22,9 +22,9 @@ ref<Expr> getConstant(int value, Expr::Width width) {
}
TEST(ExprTest, BasicConstruction) {
- EXPECT_EQ(ref<Expr>(0, 32),
- SubExpr::create(ref<Expr>(10, 32),
- ref<Expr>(10, 32)));
+ EXPECT_EQ(ConstantExpr::alloc(0, 32),
+ SubExpr::create(ConstantExpr::alloc(10, 32),
+ ConstantExpr::alloc(10, 32)));
}
TEST(ExprTest, ConcatExtract) {
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-25 11:32:34 +0000