Skip to content

CONTRACTS: do not rely on replace_symbol for bound variables [blocks: #6827] #6828

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Apr 25, 2022
Merged

CONTRACTS: do not rely on replace_symbol for bound variables [blocks: #6827] #6828

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
95 changes: 47 additions & 48 deletions src/goto-instrument/contracts/contracts.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -154,9 +154,9 @@ void code_contractst::check_apply_loop_contracts(
// at the start of and end of a loop body
std::vector<symbol_exprt> old_decreases_vars, new_decreases_vars;

replace_symbolt replace;
code_contractst::add_quantified_variable(invariant, replace, mode);
replace(invariant);
// replace bound variables by fresh instances
if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall))
add_quantified_variable(invariant, mode);

// instrument
//
Expand Down Expand Up @@ -567,68 +567,73 @@ void code_contractst::check_apply_loop_contracts(
}

void code_contractst::add_quantified_variable(
const exprt &expression,
replace_symbolt &replace,
exprt &expression,
const irep_idt &mode)
{
if(expression.id() == ID_not || expression.id() == ID_typecast)
{
// For unary connectives, recursively check for
// nested quantified formulae in the term
const auto &unary_expression = to_unary_expr(expression);
add_quantified_variable(unary_expression.op(), replace, mode);
auto &unary_expression = to_unary_expr(expression);
add_quantified_variable(unary_expression.op(), mode);
}
if(expression.id() == ID_notequal || expression.id() == ID_implies)
{
// For binary connectives, recursively check for
// nested quantified formulae in the left and right terms
const auto &binary_expression = to_binary_expr(expression);
add_quantified_variable(binary_expression.lhs(), replace, mode);
add_quantified_variable(binary_expression.rhs(), replace, mode);
auto &binary_expression = to_binary_expr(expression);
add_quantified_variable(binary_expression.lhs(), mode);
add_quantified_variable(binary_expression.rhs(), mode);
}
if(expression.id() == ID_if)
{
// For ternary connectives, recursively check for
// nested quantified formulae in all three terms
const auto &if_expression = to_if_expr(expression);
add_quantified_variable(if_expression.cond(), replace, mode);
add_quantified_variable(if_expression.true_case(), replace, mode);
add_quantified_variable(if_expression.false_case(), replace, mode);
auto &if_expression = to_if_expr(expression);
add_quantified_variable(if_expression.cond(), mode);
add_quantified_variable(if_expression.true_case(), mode);
add_quantified_variable(if_expression.false_case(), mode);
}
if(expression.id() == ID_and || expression.id() == ID_or)
{
// For multi-ary connectives, recursively check for
// nested quantified formulae in all terms
const auto &multi_ary_expression = to_multi_ary_expr(expression);
for(const auto &operand : multi_ary_expression.operands())
auto &multi_ary_expression = to_multi_ary_expr(expression);
for(auto &operand : multi_ary_expression.operands())
{
add_quantified_variable(operand, replace, mode);
add_quantified_variable(operand, mode);
}
}
else if(expression.id() == ID_exists || expression.id() == ID_forall)
{
// When a quantifier expression is found,
// for each quantified variable ...
const auto &quantifier_expression = to_quantifier_expr(expression);
// When a quantifier expression is found, create a fresh symbol for each
// quantified variable and rewrite the expression to use those fresh
// symbols.
auto &quantifier_expression = to_quantifier_expr(expression);
std::vector<symbol_exprt> fresh_variables;
fresh_variables.reserve(quantifier_expression.variables().size());
for(const auto &quantified_variable : quantifier_expression.variables())
{
const auto &quantified_symbol = to_symbol_expr(quantified_variable);

// 1. create fresh symbol
symbolt new_symbol = new_tmp_symbol(
quantified_symbol.type(),
quantified_symbol.source_location(),
quantified_variable.type(),
quantified_variable.source_location(),
mode,
symbol_table);

// 2. add created fresh symbol to expression map
symbol_exprt q(
quantified_symbol.get_identifier(), quantified_symbol.type());
replace.insert(q, new_symbol.symbol_expr());

// 3. recursively check for nested quantified formulae
add_quantified_variable(quantifier_expression.where(), replace, mode);
fresh_variables.push_back(new_symbol.symbol_expr());
}

// use fresh symbols
exprt where = quantifier_expression.instantiate(fresh_variables);

// recursively check for nested quantified formulae
add_quantified_variable(where, mode);

// replace previous variables and body
quantifier_expression.variables() = fresh_variables;
quantifier_expression.where() = std::move(where);
}
}

Expand Down Expand Up @@ -831,9 +836,9 @@ void code_contractst::apply_function_contract(
// Insert assertion of the precondition immediately before the call site.
if(!requires.is_true())
{
replace_symbolt replace(common_replace);
code_contractst::add_quantified_variable(requires, replace, mode);
replace(requires);
if(has_subexpr(requires, ID_exists) || has_subexpr(requires, ID_forall))
add_quantified_variable(requires, mode);
common_replace(requires);

goto_programt assertion;
converter.goto_convert(code_assertt(requires), assertion, mode);
Expand All @@ -852,9 +857,9 @@ void code_contractst::apply_function_contract(
std::pair<goto_programt, goto_programt> ensures_pair;
if(!ensures.is_false())
{
replace_symbolt replace(common_replace);
code_contractst::add_quantified_variable(ensures, replace, mode);
replace(ensures);
if(has_subexpr(ensures, ID_exists) || has_subexpr(ensures, ID_forall))
add_quantified_variable(ensures, mode);
common_replace(ensures);

auto assumption = code_assumet(ensures);
ensures_pair =
Expand Down Expand Up @@ -1430,12 +1435,9 @@ void code_contractst::add_contract_check(
// Generate: assume(requires)
if(!requires.is_false())
{
// extend common_replace with quantified variables in REQUIRES,
// and then do the replacement
replace_symbolt replace(common_replace);
code_contractst::add_quantified_variable(
requires, replace, function_symbol.mode);
replace(requires);
if(has_subexpr(requires, ID_exists) || has_subexpr(requires, ID_forall))
add_quantified_variable(requires, function_symbol.mode);
common_replace(requires);

goto_programt assumption;
converter.goto_convert(
Expand All @@ -1450,12 +1452,9 @@ void code_contractst::add_contract_check(
// Generate: copies for history variables
if(!ensures.is_true())
{
// extend common_replace with quantified variables in ENSURES,
// and then do the replacement
replace_symbolt replace(common_replace);
code_contractst::add_quantified_variable(
ensures, replace, function_symbol.mode);
replace(ensures);
if(has_subexpr(ensures, ID_exists) || has_subexpr(ensures, ID_forall))
add_quantified_variable(ensures, function_symbol.mode);
common_replace(ensures);

// get all the relevant instructions related to history variables
auto assertion = code_assertt(ensures);
Expand Down
11 changes: 4 additions & 7 deletions src/goto-instrument/contracts/contracts.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -156,14 +156,11 @@ class code_contractst
const irep_idt &mangled_function,
goto_programt &dest);

/// This function recursively searches the expression to find nested or
/// This function recursively searches \p expression to find nested or
/// non-nested quantified expressions. When a quantified expression is found,
/// the quantified variable is added to the symbol table
/// and to the expression map.
void add_quantified_variable(
const exprt &expression,
replace_symbolt &replace,
const irep_idt &mode);
/// a fresh quantified variable is added to the symbol table and \p expression
/// is updated to use this fresh variable.
void add_quantified_variable(exprt &expression, const irep_idt &mode);

/// This function recursively identifies the "old" expressions within expr
/// and replaces them with correspoding history variables.
Expand Down