Skip to content

Commit 880b61b

Browse files
blishkoblishko
committed
SMTChecker: Refactor handling of ConstantCondition verification target
1 parent 2ab62d7 commit 880b61b

File tree

2 files changed

+90
-89
lines changed

2 files changed

+90
-89
lines changed

‎libsolidity/formal/BMC.cpp‎

Lines changed: 69 additions & 80 deletions
Original file line numberDiff line numberDiff line change
@@ -247,14 +247,8 @@ bool BMC::visit(IfStatement const& _node)
247247
m_context.pushSolver();
248248
_node.condition().accept(*this);
249249

250-
// We ignore called functions here because they have
251-
// specific input values.
252-
if (isRootFunction() && !isInsideLoop())
253-
addVerificationTarget(
254-
VerificationTargetType::ConstantCondition,
255-
expr(_node.condition()),
256-
&_node.condition()
257-
);
250+
checkIfConditionIsConstant(_node.condition());
251+
258252
m_context.popSolver();
259253
resetVariableIndices(std::move(indicesBeforePush));
260254

@@ -283,13 +277,7 @@ bool BMC::visit(Conditional const& _op)
283277
auto indicesBeforePush = copyVariableIndices();
284278
m_context.pushSolver();
285279
_op.condition().accept(*this);
286-
287-
if (isRootFunction() && !isInsideLoop())
288-
addVerificationTarget(
289-
VerificationTargetType::ConstantCondition,
290-
expr(_op.condition()),
291-
&_op.condition()
292-
);
280+
checkIfConditionIsConstant(_op.condition());
293281
m_context.popSolver();
294282
resetVariableIndices(std::move(indicesBeforePush));
295283

@@ -690,12 +678,7 @@ void BMC::visitRequire(FunctionCall const& _funCall)
690678
auto const& args = _funCall.arguments();
691679
solAssert(args.size() >= 1, "");
692680
solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
693-
if (isRootFunction() && !isInsideLoop())
694-
addVerificationTarget(
695-
VerificationTargetType::ConstantCondition,
696-
expr(*args.front()),
697-
args.front().get()
698-
);
681+
checkIfConditionIsConstant(*args.front());
699682
}
700683

701684
void BMC::visitAddMulMod(FunctionCall const& _funCall)
@@ -933,9 +916,6 @@ void BMC::checkVerificationTarget(BMCVerificationTarget& _target)
933916

934917
switch (_target.type)
935918
{
936-
case VerificationTargetType::ConstantCondition:
937-
checkConstantCondition(_target);
938-
break;
939919
case VerificationTargetType::Underflow:
940920
checkUnderflow(_target);
941921
break;
@@ -951,19 +931,70 @@ void BMC::checkVerificationTarget(BMCVerificationTarget& _target)
951931
case VerificationTargetType::Assert:
952932
checkAssert(_target);
953933
break;
934+
case VerificationTargetType::ConstantCondition:
935+
solAssert(false, "Checks for constant condition are handled separately");
954936
default:
955937
solAssert(false, "");
956938
}
957939
}
958940

959-
void BMC::checkConstantCondition(BMCVerificationTarget& _target)
941+
void BMC::checkIfConditionIsConstant(Expression const& _condition)
960942
{
961-
checkBooleanNotConstant(
962-
*_target.expression,
963-
_target.constraints,
964-
_target.value,
965-
_target.callStack
966-
);
943+
if (
944+
!m_settings.targets.has(VerificationTargetType::ConstantCondition) ||
945+
(m_currentContract && !shouldEncode(*m_currentContract))
946+
)
947+
return;
948+
949+
// We ignore called functions here because they have specific input values.
950+
// Also, expressions inside loop can have different values in different iterations.
951+
if (!isRootFunction() || isInsideLoop())
952+
return;
953+
954+
// Do not check for const-ness if this is a literal.
955+
if (dynamic_cast<Literal const*>(&_condition))
956+
return;
957+
958+
auto [canBeTrue, canBeFalse] = checkBooleanNotConstant(currentPathConditions() && m_context.assertions(), expr(_condition));
959+
960+
// Report based on the result of the checks
961+
if (canBeTrue == CheckResult::ERROR || canBeFalse == CheckResult::ERROR)
962+
m_errorReporter.warning(8592_error, _condition.location(), "BMC: Error trying to invoke SMT solver.");
963+
else if (canBeTrue == CheckResult::CONFLICTING || canBeFalse == CheckResult::CONFLICTING)
964+
m_errorReporter.warning(3356_error, _condition.location(), "BMC: At least two SMT solvers provided conflicting answers. Results might not be sound.");
965+
else if (canBeTrue == CheckResult::UNKNOWN || canBeFalse == CheckResult::UNKNOWN)
966+
{
967+
// Not enough information to make definite claims.
968+
}
969+
else if (canBeTrue == CheckResult::SATISFIABLE && canBeFalse == CheckResult::SATISFIABLE)
970+
{
971+
// Condition can be both true and false for some program runs.
972+
}
973+
974+
else if (canBeTrue == CheckResult::UNSATISFIABLE && canBeFalse == CheckResult::UNSATISFIABLE)
975+
m_errorReporter.warning(2512_error, _condition.location(), "BMC: Condition unreachable.", SMTEncoder::callStackMessage(m_callStack));
976+
else
977+
{
978+
std::string description;
979+
if (canBeFalse == smtutil::CheckResult::UNSATISFIABLE)
980+
{
981+
smtAssert(canBeTrue == smtutil::CheckResult::SATISFIABLE);
982+
description = "BMC: Condition is always true.";
983+
}
984+
else
985+
{
986+
smtAssert(canBeTrue == smtutil::CheckResult::UNSATISFIABLE);
987+
smtAssert(canBeFalse == smtutil::CheckResult::SATISFIABLE);
988+
description = "BMC: Condition is always false.";
989+
}
990+
m_errorReporter.warning(
991+
6838_error,
992+
_condition.location(),
993+
description,
994+
SMTEncoder::callStackMessage(m_callStack)
995+
);
996+
}
997+
967998
}
968999

9691000
void BMC::checkUnderflow(BMCVerificationTarget& _target)
@@ -1068,6 +1099,7 @@ void BMC::addVerificationTarget(
10681099
Expression const* _expression
10691100
)
10701101
{
1102+
smtAssert(_type != VerificationTargetType::ConstantCondition, "Checks for constant condition are handled separately");
10711103
if (!m_settings.targets.has(_type) || (m_currentContract && !shouldAnalyzeVerificationTargetsFor(*m_currentContract)))
10721104
return;
10731105

@@ -1081,10 +1113,7 @@ void BMC::addVerificationTarget(
10811113
m_callStack,
10821114
modelExpressions()
10831115
};
1084-
if (_type == VerificationTargetType::ConstantCondition)
1085-
checkVerificationTarget(target);
1086-
else
1087-
m_verificationTargets.emplace_back(std::move(target));
1116+
m_verificationTargets.emplace_back(std::move(target));
10881117
}
10891118

10901119
/// Solving.
@@ -1188,62 +1217,22 @@ void BMC::checkCondition(
11881217
m_interface->pop();
11891218
}
11901219

1191-
void BMC::checkBooleanNotConstant(
1192-
Expression const& _condition,
1220+
BMC::ConstantExpressionCheckResult BMC::checkBooleanNotConstant(
11931221
smtutil::Expression const& _constraints,
1194-
smtutil::Expression const& _value,
1195-
std::vector<SMTEncoder::CallStackEntry> const& _callStack
1222+
smtutil::Expression const& _condition
11961223
)
11971224
{
1198-
// Do not check for const-ness if this is a constant.
1199-
if (dynamic_cast<Literal const*>(&_condition))
1200-
return;
1201-
12021225
m_interface->push();
1203-
m_interface->addAssertion(_constraints && _value);
1226+
m_interface->addAssertion(_constraints && _condition);
12041227
auto positiveResult = checkSatisfiable();
12051228
m_interface->pop();
12061229

12071230
m_interface->push();
1208-
m_interface->addAssertion(_constraints && !_value);
1231+
m_interface->addAssertion(_constraints && !_condition);
12091232
auto negatedResult = checkSatisfiable();
12101233
m_interface->pop();
12111234

1212-
if (positiveResult == smtutil::CheckResult::ERROR || negatedResult == smtutil::CheckResult::ERROR)
1213-
m_errorReporter.warning(8592_error, _condition.location(), "BMC: Error trying to invoke SMT solver.");
1214-
else if (positiveResult == smtutil::CheckResult::CONFLICTING || negatedResult == smtutil::CheckResult::CONFLICTING)
1215-
m_errorReporter.warning(3356_error, _condition.location(), "BMC: At least two SMT solvers provided conflicting answers. Results might not be sound.");
1216-
else if (positiveResult == smtutil::CheckResult::SATISFIABLE && negatedResult == smtutil::CheckResult::SATISFIABLE)
1217-
{
1218-
// everything fine.
1219-
}
1220-
else if (positiveResult == smtutil::CheckResult::UNKNOWN || negatedResult == smtutil::CheckResult::UNKNOWN)
1221-
{
1222-
// can't do anything.
1223-
}
1224-
else if (positiveResult == smtutil::CheckResult::UNSATISFIABLE && negatedResult == smtutil::CheckResult::UNSATISFIABLE)
1225-
m_errorReporter.warning(2512_error, _condition.location(), "BMC: Condition unreachable.", SMTEncoder::callStackMessage(_callStack));
1226-
else
1227-
{
1228-
std::string description;
1229-
if (positiveResult == smtutil::CheckResult::SATISFIABLE)
1230-
{
1231-
solAssert(negatedResult == smtutil::CheckResult::UNSATISFIABLE, "");
1232-
description = "BMC: Condition is always true.";
1233-
}
1234-
else
1235-
{
1236-
solAssert(positiveResult == smtutil::CheckResult::UNSATISFIABLE, "");
1237-
solAssert(negatedResult == smtutil::CheckResult::SATISFIABLE, "");
1238-
description = "BMC: Condition is always false.";
1239-
}
1240-
m_errorReporter.warning(
1241-
6838_error,
1242-
_condition.location(),
1243-
description,
1244-
SMTEncoder::callStackMessage(_callStack)
1245-
);
1246-
}
1235+
return {.canBeTrue = positiveResult, .canBeFalse = negatedResult};
12471236
}
12481237

12491238
std::pair<smtutil::CheckResult, std::vector<std::string>>

‎libsolidity/formal/BMC.h‎

Lines changed: 21 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -161,7 +161,6 @@ class BMC: public SMTEncoder
161161

162162
void checkVerificationTargets();
163163
void checkVerificationTarget(BMCVerificationTarget& _target);
164-
void checkConstantCondition(BMCVerificationTarget& _target);
165164
void checkUnderflow(BMCVerificationTarget& _target);
166165
void checkOverflow(BMCVerificationTarget& _target);
167166
void checkDivByZero(BMCVerificationTarget& _target);
@@ -172,8 +171,13 @@ class BMC: public SMTEncoder
172171
smtutil::Expression const& _value,
173172
Expression const* _expression
174173
);
174+
/// Special handling of ConstantCondition verification target.
175+
/// The target is checked immediately, unlike the other targets that are queued for checking at the end of analysis.
176+
void checkIfConditionIsConstant(Expression const& _condition);
175177
//@}
176178

179+
180+
177181
/// Solver related.
178182
//@{
179183
/// Check that a condition can be satisfied.
@@ -188,13 +192,18 @@ class BMC: public SMTEncoder
188192
std::string const& _additionalValueName = "",
189193
smtutil::Expression const* _additionalValue = nullptr
190194
);
191-
/// Checks that a boolean condition is not constant. Do not warn if the expression
192-
/// is a literal constant.
193-
void checkBooleanNotConstant(
194-
Expression const& _condition,
195+
196+
struct ConstantExpressionCheckResult
197+
{
198+
smtutil::CheckResult canBeTrue;
199+
smtutil::CheckResult canBeFalse;
200+
};
201+
202+
/// Checks whether the given boolean condition is either true or always false under given constraints.
203+
/// Returns the results from the solver for these two checks.
204+
ConstantExpressionCheckResult checkBooleanNotConstant(
195205
smtutil::Expression const& _constraints,
196-
smtutil::Expression const& _value,
197-
std::vector<CallStackEntry> const& _callStack
206+
smtutil::Expression const& _condition
198207
);
199208
std::pair<smtutil::CheckResult, std::vector<std::string>>
200209
checkSatisfiableAndGenerateModel(std::vector<smtutil::Expression> const& _expressionsToEvaluate);
@@ -222,20 +231,23 @@ class BMC: public SMTEncoder
222231
/// Number of verification conditions that could not be proved.
223232
size_t m_unprovedAmt = 0;
224233

234+
/// Loop analysis
235+
//@{
225236
enum class LoopControlKind
226237
{
227238
Continue,
228239
Break
229240
};
230241

231-
// Current path conditions and SSA indices for break or continue statement
242+
/// Current path conditions and SSA indices for break or continue statement
232243
struct LoopControl {
233244
LoopControlKind kind;
234245
smtutil::Expression pathConditions;
235246
VariableIndices variableIndices;
236247
};
237248

238-
// Loop control statements for every loop
249+
/// Loop control statements for every loop
239250
std::stack<std::vector<LoopControl>> m_loopCheckpoints;
251+
//@}
240252
};
241253
}

0 commit comments

Comments
 (0)