sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

better treatment of cases where array out of bounds accesses occurr

tempestpy_adaptions
TimQu 6 years ago
parent
7bae50d0ba
commit
bdeacf8669
1 changed files with 159 additions and 121 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 190
      src/storm/storage/jani/ArrayEliminator.cpp

190
src/storm/storage/jani/ArrayEliminator.cpp
View File

@ -128,94 +128,119 @@ namespace storm {
class ArrayExpressionEliminationVisitor : public storm::expressions::ExpressionVisitor, public storm::expressions::JaniExpressionVisitor {
public:
typedef std::shared_ptr<storm::expressions::BaseExpression const> BaseExprPtr;
class ResultType {
public:
ResultType(ResultType const& other) = default;
ResultType(BaseExprPtr expression) : expression(expression), arrayOutOfBoundsMessage("") {}
ResultType(std::string arrayOutOfBoundsMessage) : expression(nullptr), arrayOutOfBoundsMessage(arrayOutOfBoundsMessage) {}
BaseExprPtr& expr() {
STORM_LOG_ASSERT(!isArrayOutOfBounds(), "Tried to get the result expression, but " << arrayOutOfBoundsMessage);
return expression;
};
bool isArrayOutOfBounds() { return arrayOutOfBoundsMessage != ""; };
std::string const& outOfBoundsMessage() const { return arrayOutOfBoundsMessage; }
private:
BaseExprPtr expression;
std::string arrayOutOfBoundsMessage;
};
ArrayExpressionEliminationVisitor(std::unordered_map<storm::expressions::Variable, std::vector<storm::jani::Variable const*>> const& replacements, std::unordered_map<storm::expressions::Variable, std::size_t> const& sizes) : replacements(replacements), arraySizes(sizes) {}
virtual ~ArrayExpressionEliminationVisitor() = default;
storm::expressions::Expression eliminate(storm::expressions::Expression const& expression) {
// here, data is the accessed index of the most recent array access expression. Initially, there is none.
auto res = storm::expressions::Expression(boost::any_cast<BaseExprPtr>(expression.accept(*this, boost::any())));
STORM_LOG_ASSERT(!containsArrayExpression(res), "Expression still contains array expressions. Before: " << std::endl << expression << std::endl << "After:" << std::endl << res);
return res.simplify();
auto res = boost::any_cast<ResultType>(expression.accept(*this, boost::any()));
STORM_LOG_THROW(!res.isArrayOutOfBounds(), storm::exceptions::OutOfRangeException, res.outOfBoundsMessage());
STORM_LOG_ASSERT(!containsArrayExpression(res.expr()->toExpression()), "Expression still contains array expressions. Before: " << std::endl << expression << std::endl << "After:" << std::endl << res.expr()->toExpression());
return res.expr()->simplify();
}
virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) override {
BaseExprPtr thenExpression, elseExpression;
// We need to handle expressions of the kind '42<size : A[42] : 0', where size is a variable.
// If an out of range exception occurrs in the 'then' or the 'else' branch, we assume that the this expression represents the other branch.
// TODO: Make this more reliable
bool thenOutOfRange(false), elseOutOfRange(false);
try {
thenExpression = boost::any_cast<BaseExprPtr>(expression.getThenExpression()->accept(*this, data));
} catch (storm::exceptions::OutOfRangeException const&) {
thenOutOfRange = true;
}
try {
elseExpression = boost::any_cast<BaseExprPtr>(expression.getElseExpression()->accept(*this, data));
} catch (storm::exceptions::OutOfRangeException const& e) {
if (thenOutOfRange) {
throw e;
} else {
elseOutOfRange = true;
}
// for the condition expression, outer array accesses should not matter.
ResultType conditionResult = boost::any_cast<ResultType>(expression.getCondition()->accept(*this, boost::any()));
if (conditionResult.isArrayOutOfBounds()) {
return conditionResult;
}
if (thenOutOfRange) {
assert(!elseOutOfRange);
return elseExpression;
} else if (elseOutOfRange) {
return thenExpression;
// We need to handle expressions of the kind '42<size : A[42] : 0', where size is a variable and A[42] might be out of bounds.
ResultType thenResult = boost::any_cast<ResultType>(expression.getThenExpression()->accept(*this, data));
ResultType elseResult = boost::any_cast<ResultType>(expression.getElseExpression()->accept(*this, data));
if (thenResult.isArrayOutOfBounds()) {
if (elseResult.isArrayOutOfBounds()) {
return ResultType(thenResult.outOfBoundsMessage() + " and " + elseResult.outOfBoundsMessage());
} else {
// Assume the else expression
return elseResult;
}
// for the condition expression, outer array accesses should not matter.
BaseExprPtr conditionExpression = boost::any_cast<BaseExprPtr>(expression.getCondition()->accept(*this, boost::any()));
} else if (elseResult.isArrayOutOfBounds()) {
// Assume the then expression
return thenResult;
} else {
// If the arguments did not change, we simply push the expression itself.
if (conditionExpression.get() == expression.getCondition().get() && thenExpression.get() == expression.getThenExpression().get() && elseExpression.get() == expression.getElseExpression().get()) {
return expression.getSharedPointer();
if (conditionResult.expr().get() == expression.getCondition().get() && thenResult.expr().get() == expression.getThenExpression().get() && elseResult.expr().get() == expression.getElseExpression().get()) {
return ResultType(expression.getSharedPointer());
} else {
return std::const_pointer_cast<storm::expressions::BaseExpression const>(std::shared_ptr<storm::expressions::BaseExpression>(new storm::expressions::IfThenElseExpression(expression.getManager(), thenExpression->getType(), conditionExpression, thenExpression, elseExpression)));
return ResultType(std::const_pointer_cast<storm::expressions::BaseExpression const>(std::shared_ptr<storm::expressions::BaseExpression>(new storm::expressions::IfThenElseExpression(expression.getManager(), thenResult.expr()->getType(), conditionResult.expr(), thenResult.expr(), elseResult.expr()))));
}
}
}
virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data) override {
STORM_LOG_ASSERT(data.empty(), "BinaryBooleanFunctionExpressions should not be direct subexpressions of array access expressions. However, the expression " << expression << " is.");
BaseExprPtr firstExpression = boost::any_cast<BaseExprPtr>(expression.getFirstOperand()->accept(*this, data));
BaseExprPtr secondExpression = boost::any_cast<BaseExprPtr>(expression.getSecondOperand()->accept(*this, data));
ResultType firstResult = boost::any_cast<ResultType>(expression.getFirstOperand()->accept(*this, data));
ResultType secondResult = boost::any_cast<ResultType>(expression.getSecondOperand()->accept(*this, data));
if (firstResult.isArrayOutOfBounds()) {
return firstResult;
} else if (secondResult.isArrayOutOfBounds()) {
return secondResult;
}
// If the arguments did not change, we simply push the expression itself.
if (firstExpression.get() == expression.getFirstOperand().get() && secondExpression.get() == expression.getSecondOperand().get()) {
return expression.getSharedPointer();
if (firstResult.expr().get() == expression.getFirstOperand().get() && secondResult.expr().get() == expression.getSecondOperand().get()) {
return ResultType(expression.getSharedPointer());
} else {
return std::const_pointer_cast<storm::expressions::BaseExpression const>(std::shared_ptr<storm::expressions::BaseExpression>(new storm::expressions::BinaryBooleanFunctionExpression(expression.getManager(), expression.getType(), firstExpression, secondExpression, expression.getOperatorType())));
return ResultType(std::const_pointer_cast<storm::expressions::BaseExpression const>(std::shared_ptr<storm::expressions::BaseExpression>(new storm::expressions::BinaryBooleanFunctionExpression(expression.getManager(), expression.getType(), firstResult.expr(), secondResult.expr(), expression.getOperatorType()))));
}
}
virtual boost::any visit(storm::expressions::BinaryNumericalFunctionExpression const& expression, boost::any const& data) override {
STORM_LOG_ASSERT(data.empty(), "BinaryNumericalFunctionExpression should not be direct subexpressions of array access expressions. However, the expression " << expression << " is.");
BaseExprPtr firstExpression = boost::any_cast<BaseExprPtr>(expression.getFirstOperand()->accept(*this, data));
BaseExprPtr secondExpression = boost::any_cast<BaseExprPtr>(expression.getSecondOperand()->accept(*this, data));
ResultType firstResult = boost::any_cast<ResultType>(expression.getFirstOperand()->accept(*this, data));
ResultType secondResult = boost::any_cast<ResultType>(expression.getSecondOperand()->accept(*this, data));
if (firstResult.isArrayOutOfBounds()) {
return firstResult;
} else if (secondResult.isArrayOutOfBounds()) {
return secondResult;
}
// If the arguments did not change, we simply push the expression itself.
if (firstExpression.get() == expression.getFirstOperand().get() && secondExpression.get() == expression.getSecondOperand().get()) {
return expression.getSharedPointer();
if (firstResult.expr().get() == expression.getFirstOperand().get() && secondResult.expr().get() == expression.getSecondOperand().get()) {
return ResultType(expression.getSharedPointer());
} else {
return std::const_pointer_cast<storm::expressions::BaseExpression const>(std::shared_ptr<storm::expressions::BaseExpression>(new storm::expressions::BinaryNumericalFunctionExpression(expression.getManager(), expression.getType(), firstExpression, secondExpression, expression.getOperatorType())));
return ResultType(std::const_pointer_cast<storm::expressions::BaseExpression const>(std::shared_ptr<storm::expressions::BaseExpression>(new storm::expressions::BinaryNumericalFunctionExpression(expression.getManager(), expression.getType(), firstResult.expr(), secondResult.expr(), expression.getOperatorType()))));
}
}
virtual boost::any visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data) override {
STORM_LOG_ASSERT(data.empty(), "BinaryRelationExpression should not be direct subexpressions of array access expressions. However, the expression " << expression << " is.");
BaseExprPtr firstExpression = boost::any_cast<BaseExprPtr>(expression.getFirstOperand()->accept(*this, data));
BaseExprPtr secondExpression = boost::any_cast<BaseExprPtr>(expression.getSecondOperand()->accept(*this, data));
ResultType firstResult = boost::any_cast<ResultType>(expression.getFirstOperand()->accept(*this, data));
ResultType secondResult = boost::any_cast<ResultType>(expression.getSecondOperand()->accept(*this, data));
if (firstResult.isArrayOutOfBounds()) {
return firstResult;
} else if (secondResult.isArrayOutOfBounds()) {
return secondResult;
}
// If the arguments did not change, we simply push the expression itself.
if (firstExpression.get() == expression.getFirstOperand().get() && secondExpression.get() == expression.getSecondOperand().get()) {
return expression.getSharedPointer();
if (firstResult.expr().get() == expression.getFirstOperand().get() && secondResult.expr().get() == expression.getSecondOperand().get()) {
return ResultType(expression.getSharedPointer());
} else {
return std::const_pointer_cast<storm::expressions::BaseExpression const>(std::shared_ptr<storm::expressions::BaseExpression>(new storm::expressions::BinaryRelationExpression(expression.getManager(), expression.getType(), firstExpression, secondExpression, expression.getRelationType())));
return ResultType(std::const_pointer_cast<storm::expressions::BaseExpression const>(std::shared_ptr<storm::expressions::BaseExpression>(new storm::expressions::BinaryRelationExpression(expression.getManager(), expression.getType(), firstResult.expr(), secondResult.expr(), expression.getRelationType()))));
}
}
@ -225,59 +250,69 @@ namespace storm {
uint64_t index = boost::any_cast<uint64_t>(data);
STORM_LOG_ASSERT(replacements.find(expression.getVariable()) != replacements.end(), "Unable to find array variable " << expression << " in array replacements.");
auto const& arrayVarReplacements = replacements.at(expression.getVariable());
if (index >= arrayVarReplacements.size()) throw storm::exceptions::OutOfRangeException();
//STORM_LOG_THROW(index < arrayVarReplacements.size(), storm::exceptions::OutOfRangeException, "Array index " << index << " for variable " << expression << " is out of bounds.");
return arrayVarReplacements[index]->getExpressionVariable().getExpression().getBaseExpressionPointer();
if (index >= arrayVarReplacements.size()) {
return ResultType("Array index " + std::to_string(index) + " for variable " + expression.getVariableName() + " is out of bounds.");
}
return ResultType(arrayVarReplacements[index]->getExpressionVariable().getExpression().getBaseExpressionPointer());
} else {
STORM_LOG_ASSERT(data.empty(), "VariableExpression of non-array variable should not be a subexpressions of array access expressions. However, the expression " << expression << " is.");
return expression.getSharedPointer();
return ResultType(expression.getSharedPointer());
}
}
virtual boost::any visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data) override {
STORM_LOG_ASSERT(data.empty(), "UnaryBooleanFunctionExpression should not be direct subexpressions of array access expressions. However, the expression " << expression << " is.");
BaseExprPtr operandExpression = boost::any_cast<BaseExprPtr>(expression.getOperand()->accept(*this, data));
ResultType operandResult = boost::any_cast<ResultType>(expression.getOperand()->accept(*this, data));
if (operandResult.isArrayOutOfBounds()) {
return operandResult;
}
// If the argument did not change, we simply push the expression itself.
if (operandExpression.get() == expression.getOperand().get()) {
return expression.getSharedPointer();
if (operandResult.expr().get() == expression.getOperand().get()) {
return ResultType(expression.getSharedPointer());
} else {
return std::const_pointer_cast<storm::expressions::BaseExpression const>(std::shared_ptr<storm::expressions::BaseExpression>(new storm::expressions::UnaryBooleanFunctionExpression(expression.getManager(), expression.getType(), operandExpression, expression.getOperatorType())));
return ResultType(std::const_pointer_cast<storm::expressions::BaseExpression const>(std::shared_ptr<storm::expressions::BaseExpression>(new storm::expressions::UnaryBooleanFunctionExpression(expression.getManager(), expression.getType(), operandResult.expr(), expression.getOperatorType()))));
}
}
virtual boost::any visit(storm::expressions::UnaryNumericalFunctionExpression const& expression, boost::any const& data) override {
STORM_LOG_ASSERT(data.empty(), "UnaryBooleanFunctionExpression should not be direct subexpressions of array access expressions. However, the expression " << expression << " is.");
BaseExprPtr operandExpression = boost::any_cast<BaseExprPtr>(expression.getOperand()->accept(*this, data));
ResultType operandResult = boost::any_cast<ResultType>(expression.getOperand()->accept(*this, data));
if (operandResult.isArrayOutOfBounds()) {
return operandResult;
}
// If the argument did not change, we simply push the expression itself.
if (operandExpression.get() == expression.getOperand().get()) {
return expression.getSharedPointer();
if (operandResult.expr().get() == expression.getOperand().get()) {
return ResultType(expression.getSharedPointer());
} else {
return std::const_pointer_cast<storm::expressions::BaseExpression const>(std::shared_ptr<storm::expressions::BaseExpression>(new storm::expressions::UnaryNumericalFunctionExpression(expression.getManager(), expression.getType(), operandExpression, expression.getOperatorType())));
return ResultType(std::const_pointer_cast<storm::expressions::BaseExpression const>(std::shared_ptr<storm::expressions::BaseExpression>(new storm::expressions::UnaryNumericalFunctionExpression(expression.getManager(), expression.getType(), operandResult.expr(), expression.getOperatorType()))));
}
}
virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const&) override {
return expression.getSharedPointer();
return ResultType(expression.getSharedPointer());
}
virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const&) override {
return expression.getSharedPointer();
return ResultType(expression.getSharedPointer());
}
virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const&) override {
return expression.getSharedPointer();
return ResultType(expression.getSharedPointer());
}
virtual boost::any visit(storm::expressions::ValueArrayExpression const& expression, boost::any const& data) override {
STORM_LOG_THROW(!data.empty(), storm::exceptions::NotSupportedException, "Unable to translate ValueArrayExpression to element expression since it does not seem to be within an array access expression.");
uint64_t index = boost::any_cast<uint64_t>(data);
STORM_LOG_ASSERT(expression.size()->isIntegerLiteralExpression(), "unexpected kind of size expression of ValueArrayExpression (" << expression.size()->toExpression() << ").");
if (index >= static_cast<uint64_t>(expression.size()->evaluateAsInt())) throw storm::exceptions::OutOfRangeException();
// STORM_LOG_THROW(index < static_cast<uint64_t>(expression.size()->evaluateAsInt()), storm::exceptions::OutOfRangeException, "Out of bounds array access occured while accessing index " << index << " of expression " << expression);
return boost::any_cast<BaseExprPtr>(expression.at(index)->accept(*this, boost::any()));
if (index >= static_cast<uint64_t>(expression.size()->evaluateAsInt())) {
return ResultType("Array index " + std::to_string(index) + " for ValueArrayExpression " + expression.toExpression().toString() + " is out of bounds.");
}
return ResultType(boost::any_cast<ResultType>(expression.at(index)->accept(*this, boost::any())));
}
virtual boost::any visit(storm::expressions::ConstructorArrayExpression const& expression, boost::any const& data) override {
@ -286,10 +321,11 @@ namespace storm {
if (expression.size()->containsVariables()) {
STORM_LOG_WARN("Ignoring length of constructorArrayExpression " << expression << " as it still contains variables.");
} else {
if (index >= static_cast<uint64_t>(expression.size()->evaluateAsInt())) throw storm::exceptions::OutOfRangeException();
// STORM_LOG_THROW(index < static_cast<uint64_t>(expression.size()->evaluateAsInt()), storm::exceptions::OutOfRangeException, "Out of bounds array access occured while accessing index " << index << " of expression " << expression);
if (index >= static_cast<uint64_t>(expression.size()->evaluateAsInt())) {
return ResultType("Array index " + std::to_string(index) + " for ConstructorArrayExpression " + expression.toExpression().toString() + " is out of bounds.");
}
}
return boost::any_cast<BaseExprPtr>(expression.at(index)->accept(*this, boost::any()));
return ResultType(boost::any_cast<ResultType>(expression.at(index)->accept(*this, boost::any())));
}
virtual boost::any visit(storm::expressions::ArrayAccessExpression const& expression, boost::any const& data) override {
@ -298,19 +334,18 @@ namespace storm {
uint64_t size = MaxArraySizeExpressionVisitor().getMaxSize(expression.getFirstOperand()->toExpression(), arraySizes);
STORM_LOG_THROW(size > 0, storm::exceptions::NotSupportedException, "Unable to get size of array expression for array access " << expression << ".");
uint64_t index = size - 1;
storm::expressions::Expression result = boost::any_cast<BaseExprPtr>(expression.getFirstOperand()->accept(*this, index))->toExpression();
storm::expressions::Expression result = boost::any_cast<ResultType>(expression.getFirstOperand()->accept(*this, index)).expr()->toExpression();
while (index > 0) {
--index;
storm::expressions::Expression isCurrentIndex = boost::any_cast<BaseExprPtr>(expression.getSecondOperand()->accept(*this, boost::any()))->toExpression() == expression.getManager().integer(index);
storm::expressions::Expression isCurrentIndex = boost::any_cast<ResultType>(expression.getSecondOperand()->accept(*this, boost::any())).expr()->toExpression() == expression.getManager().integer(index);
result = storm::expressions::ite(isCurrentIndex,
boost::any_cast<BaseExprPtr>(expression.getFirstOperand()->accept(*this, index))->toExpression(),
boost::any_cast<ResultType>(expression.getFirstOperand()->accept(*this, index)).expr()->toExpression(),
result);
}
return result.getBaseExpressionPointer();
return ResultType(result.getBaseExpressionPointer());
} else {
uint64_t index = expression.getSecondOperand()->evaluateAsInt();
auto result = boost::any_cast<BaseExprPtr>(expression.getFirstOperand()->accept(*this, index));
return result;
return boost::any_cast<ResultType>(expression.getFirstOperand()->accept(*this, index));
}
}
@ -468,6 +503,8 @@ namespace storm {
// Replace array occurrences in LValues and assigned expressions.
std::vector<Assignment> newAssignments;
if (!orderedAssignments.empty()) {
int64_t level = orderedAssignments.getLowestLevel();
std::unordered_map<storm::expressions::Variable, std::vector<Assignment const*>> collectedArrayAccessAssignments;
for (Assignment const& assignment : orderedAssignments) {
@ -520,6 +557,7 @@ namespace storm {
orderedAssignments.add(assignment);
}
}
}
private:

Write Preview
Loading…
Cancel
Save