aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/Executor.cpp12
-rw-r--r--lib/Core/TimingSolver.cpp2
-rw-r--r--lib/Expr/Expr.cpp26
-rw-r--r--lib/Expr/ExprPPrinter.cpp4
-rw-r--r--lib/Expr/Parser.cpp9
-rw-r--r--lib/Solver/CachingSolver.cpp2
-rw-r--r--lib/Solver/CexCachingSolver.cpp4
-rw-r--r--lib/Solver/Solver.cpp2
8 files changed, 29 insertions, 32 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 79b2040b..62f033be 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -728,7 +728,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
addConstraint(current, condition);
} else {
res = Solver::False;
- addConstraint(current, Expr::createNot(condition));
+ addConstraint(current, Expr::createIsZero(condition));
}
}
} else if (res==Solver::Unknown) {
@@ -753,7 +753,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
addConstraint(current, condition);
res = Solver::True;
} else {
- addConstraint(current, Expr::createNot(condition));
+ addConstraint(current, Expr::createIsZero(condition));
res = Solver::False;
}
}
@@ -786,7 +786,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
assert(trueSeed || falseSeed);
res = trueSeed ? Solver::True : Solver::False;
- addConstraint(current, trueSeed ? condition : Expr::createNot(condition));
+ addConstraint(current, trueSeed ? condition : Expr::createIsZero(condition));
}
}
@@ -880,7 +880,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
}
addConstraint(*trueState, condition);
- addConstraint(*falseState, Expr::createNot(condition));
+ addConstraint(*falseState, Expr::createIsZero(condition));
// Kinda gross, do we even really still want this option?
if (MaxDepth && MaxDepth<=trueState->depth) {
@@ -1389,7 +1389,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
for (unsigned i=1; i<cases; ++i) {
ref<Expr> value = evalConstant(si->getCaseValue(i));
ref<Expr> match = EqExpr::create(cond, value);
- isDefault = AndExpr::create(isDefault, Expr::createNot(match));
+ isDefault = AndExpr::create(isDefault, Expr::createIsZero(match));
bool result;
bool success = solver->mayBeTrue(state, match, result);
assert(success && "FIXME: Unhandled solver failure");
@@ -3119,7 +3119,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state,
mo->cexPreferences.begin(), pie = mo->cexPreferences.end();
for (; pi != pie; ++pi) {
bool mustBeTrue;
- bool success = solver->mustBeTrue(tmp, Expr::createNot(*pi),
+ bool success = solver->mustBeTrue(tmp, Expr::createIsZero(*pi),
mustBeTrue);
if (!success) break;
if (!mustBeTrue) tmp.addConstraint(*pi);
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index 0154ddcf..542a3c8e 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -72,7 +72,7 @@ bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr,
bool TimingSolver::mustBeFalse(const ExecutionState& state, ref<Expr> expr,
bool &result) {
- return mustBeTrue(state, Expr::createNot(expr), result);
+ return mustBeTrue(state, Expr::createIsZero(expr), result);
}
bool TimingSolver::mayBeTrue(const ExecutionState& state, ref<Expr> expr,
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index fc450d76..2f9e04a0 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -289,7 +289,7 @@ Expr::Width Expr::getWidthForLLVMType(const llvm::Type *t) {
}
ref<Expr> Expr::createImplies(ref<Expr> hyp, ref<Expr> conc) {
- return OrExpr::create(Expr::createNot(hyp), conc);
+ return OrExpr::create(Expr::createIsZero(hyp), conc);
}
ref<Expr> Expr::createIsZero(ref<Expr> e) {
@@ -300,10 +300,6 @@ ref<Expr> Expr::createCoerceToPointerType(ref<Expr> e) {
return ZExtExpr::create(e, kMachinePointerType);
}
-ref<Expr> Expr::createNot(ref<Expr> e) {
- return createIsZero(e);
-}
-
ref<ConstantExpr> Expr::createPointer(uint64_t v) {
return ConstantExpr::create(v, kMachinePointerType);
}
@@ -527,11 +523,11 @@ ref<Expr> SelectExpr::create(ref<Expr> c, ref<Expr> t, ref<Expr> f) {
if (CE->isTrue()) {
return OrExpr::create(c, f);
} else {
- return AndExpr::create(Expr::createNot(c), f);
+ return AndExpr::create(Expr::createIsZero(c), f);
}
} else if (ConstantExpr *CE = dyn_cast<ConstantExpr>(f)) {
if (CE->isTrue()) {
- return OrExpr::create(Expr::createNot(c), t);
+ return OrExpr::create(Expr::createIsZero(c), t);
} else {
return AndExpr::create(c, t);
}
@@ -868,7 +864,7 @@ static ref<Expr> SRemExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
static ref<Expr> ShlExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
if (l->getWidth() == Expr::Bool) { // l & !r
- return AndExpr::create(l, Expr::createNot(r));
+ return AndExpr::create(l, Expr::createIsZero(r));
} else{
return ShlExpr::alloc(l, r);
}
@@ -876,7 +872,7 @@ static ref<Expr> ShlExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
static ref<Expr> LShrExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
if (l->getWidth() == Expr::Bool) { // l & !r
- return AndExpr::create(l, Expr::createNot(r));
+ return AndExpr::create(l, Expr::createIsZero(r));
} else{
return LShrExpr::alloc(l, r);
}
@@ -1014,8 +1010,8 @@ static ref<Expr> EqExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {
const OrExpr *roe = cast<OrExpr>(r);
// transform not(or(a,b)) to and(not a, not b)
- return AndExpr::create(Expr::createNot(roe->left),
- Expr::createNot(roe->right));
+ return AndExpr::create(Expr::createIsZero(roe->left),
+ Expr::createIsZero(roe->right));
}
}
} else if (rk == Expr::SExt) {
@@ -1093,7 +1089,7 @@ ref<Expr> SgeExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
static ref<Expr> UltExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
Expr::Width t = l->getWidth();
if (t == Expr::Bool) { // !l && r
- return AndExpr::create(Expr::createNot(l), r);
+ return AndExpr::create(Expr::createIsZero(l), r);
} else {
return UltExpr::alloc(l, r);
}
@@ -1101,7 +1097,7 @@ static ref<Expr> UltExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
static ref<Expr> UleExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
if (l->getWidth() == Expr::Bool) { // !(l && !r)
- return OrExpr::create(Expr::createNot(l), r);
+ return OrExpr::create(Expr::createIsZero(l), r);
} else {
return UleExpr::alloc(l, r);
}
@@ -1109,7 +1105,7 @@ static ref<Expr> UleExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
static ref<Expr> SltExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
if (l->getWidth() == Expr::Bool) { // l && !r
- return AndExpr::create(l, Expr::createNot(r));
+ return AndExpr::create(l, Expr::createIsZero(r));
} else {
return SltExpr::alloc(l, r);
}
@@ -1117,7 +1113,7 @@ static ref<Expr> SltExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
static ref<Expr> SleExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
if (l->getWidth() == Expr::Bool) { // !(!l && r)
- return OrExpr::create(l, Expr::createNot(r));
+ return OrExpr::create(l, Expr::createIsZero(r));
} else {
return SleExpr::alloc(l, r);
}
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index 6eb15c7c..691ccd89 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -408,11 +408,11 @@ public:
bindings.insert(std::make_pair(e, counter++));
}
- // Detect Not.
+ // Detect Nz
// FIXME: This should be in common code.
if (const EqExpr *ee = dyn_cast<EqExpr>(e)) {
if (ee->left == ConstantExpr::alloc(false, Expr::Bool)) {
- PC << "(Not";
+ PC << "(Nz";
printWidth(PC, e);
PC << ' ';
print(ee->right, PC);
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index 42e8af03..52fba4a6 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -776,7 +776,7 @@ ExprResult ParserImpl::ParseExpr(TypeResult ExpectedType) {
// Additional kinds for macro forms.
enum MacroKind {
- eMacroKind_Not = Expr::LastKind + 1, // false == x
+ eMacroKind_Nz = Expr::LastKind + 1, // false == x
eMacroKind_Neg, // 0 - x
eMacroKind_ReadLSB, // Multibyte read
eMacroKind_ReadMSB, // Multibyte write
@@ -806,6 +806,9 @@ static bool LookupExprInfo(const Token &Tok, unsigned &Kind,
return SetOK(Expr::Eq, false, 2);
if (memcmp(Tok.start, "Ne", 2) == 0)
return SetOK(Expr::Ne, false, 2);
+
+ if (memcmp(Tok.start, "Nz", 2) == 0)
+ return SetOK(eMacroKind_Nz, true, 1);
if (memcmp(Tok.start, "Or", 2) == 0)
return SetOK(Expr::Or, true, 2);
@@ -826,8 +829,6 @@ static bool LookupExprInfo(const Token &Tok, unsigned &Kind,
if (memcmp(Tok.start, "Xor", 3) == 0)
return SetOK(Expr::Xor, true, 2);
- if (memcmp(Tok.start, "Not", 3) == 0)
- return SetOK(eMacroKind_Not, true, 1);
if (memcmp(Tok.start, "Neg", 3) == 0)
return SetOK(eMacroKind_Neg, true, 1);
if (memcmp(Tok.start, "Ult", 3) == 0)
@@ -1015,7 +1016,7 @@ ExprResult ParserImpl::ParseUnaryParenExpr(const Token &Name,
ExpectRParen("unexpected argument in unary expression.");
ExprHandle E = Arg.get();
switch (Kind) {
- case eMacroKind_Not:
+ case eMacroKind_Nz:
return Builder->Eq(Builder->Constant(0, E->getWidth()), E);
case eMacroKind_Neg:
return Builder->Sub(Builder->Constant(0, E->getWidth()), E);
diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp
index d353e485..c0b77429 100644
--- a/lib/Solver/CachingSolver.cpp
+++ b/lib/Solver/CachingSolver.cpp
@@ -89,7 +89,7 @@ public:
the canonicalization process. */
ref<Expr> CachingSolver::canonicalizeQuery(ref<Expr> originalQuery,
bool &negationUsed) {
- ref<Expr> negatedQuery = Expr::createNot(originalQuery);
+ ref<Expr> negatedQuery = Expr::createIsZero(originalQuery);
// select the "smaller" query to the be canonical representation
if (originalQuery.compare(negatedQuery) < 0) {
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index 373f42d9..2bdc7418 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -137,7 +137,7 @@ bool CexCachingSolver::searchForAssignment(KeyType &key, Assignment *&result) {
bool CexCachingSolver::lookupAssignment(const Query &query,
Assignment *&result) {
KeyType key(query.constraints.begin(), query.constraints.end());
- ref<Expr> neg = Expr::createNot(query.expr);
+ ref<Expr> neg = Expr::createIsZero(query.expr);
if (ConstantExpr *CE = dyn_cast<ConstantExpr>(neg)) {
if (CE->isFalse()) {
result = (Assignment*) 0;
@@ -152,7 +152,7 @@ bool CexCachingSolver::lookupAssignment(const Query &query,
bool CexCachingSolver::getAssignment(const Query& query, Assignment *&result) {
KeyType key(query.constraints.begin(), query.constraints.end());
- ref<Expr> neg = Expr::createNot(query.expr);
+ ref<Expr> neg = Expr::createIsZero(query.expr);
if (ConstantExpr *CE = dyn_cast<ConstantExpr>(neg)) {
if (CE->isFalse()) {
result = (Assignment*) 0;
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index f8f9d690..abff5743 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -349,7 +349,7 @@ ValidatingSolver::computeInitialValues(const Query& query,
}
}
ConstraintManager tmp(bindings);
- ref<Expr> constraints = Expr::createNot(query.expr);
+ ref<Expr> constraints = Expr::createIsZero(query.expr);
for (ConstraintManager::const_iterator it = query.constraints.begin(),
ie = query.constraints.end(); it != ie; ++it)
constraints = AndExpr::create(constraints, *it);
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-22 23:31:36 +0000