Skip to content

Fix side-effect check on loop invariants #5942

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 2 commits into from
May 14, 2021
Merged

Fix side-effect check on loop invariants #5942

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9860129
Minor refactor and cleanup on code contracts
SaswatPadhi May 12, 2021
1debdc7
Fix side-effect check on loop invariants
SaswatPadhi May 12, 2021
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
16 changes: 16 additions & 0 deletions regression/contracts/invariant_side_effects/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
#include <assert.h>
#include <stdlib.h>

int main()
{
unsigned N, *a = malloc(sizeof(unsigned int));

*a = 0;
while(*a < N)
__CPROVER_loop_invariant((0 <= *a) && (*a <= N))
{
++(*a);
}

assert(*a == N);
}
12 changes: 12 additions & 0 deletions regression/contracts/invariant_side_effects/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
CORE
main.c
--enforce-all-contracts
^EXIT=0$
^SIGNAL=0$
^\[main.1\] .* Check loop invariant before entry: SUCCESS$
^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
^\[main.assertion.1\] .* assertion \*a == N: SUCCESS$
^VERIFICATION SUCCESSFUL$
--
This test checks that C expressions are correctly converted to logic
when enforcing loop invariant annotations.
89 changes: 46 additions & 43 deletions src/goto-instrument/code_contracts.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,6 @@ Date: February 2016

#include <ansi-c/c_expr.h>

#include <goto-programs/goto_convert_class.h>
#include <goto-programs/remove_skip.h>

#include <util/arith_tools.h>
Expand All @@ -34,8 +33,6 @@ Date: February 2016
#include <util/pointer_predicates.h>
#include <util/replace_symbol.h>

#include "loop_utils.h"

/// Predicate to be used with the exprt::visit() function. The function
/// found_return_value() will return `true` iff this predicate is called on an
/// expr that contains `__CPROVER_return_value`.
Expand Down Expand Up @@ -74,11 +71,12 @@ exprt get_size(const typet &type, const namespacet &ns, messaget &log)
return result;
}

static void check_apply_invariants(
void code_contractst::check_apply_invariants(
goto_functionst::goto_functiont &goto_function,
const local_may_aliast &local_may_alias,
const goto_programt::targett loop_head,
const loopt &loop)
const loopt &loop,
const irep_idt &mode)
{
PRECONDITION(!loop.empty());

Expand All @@ -96,16 +94,18 @@ static void check_apply_invariants(
if(invariant.is_nil())
return;

// change H: loop; E: ...
// change
// H: loop;
// E: ...
// to
// H: assert(invariant);
// havoc;
// assume(invariant);
// if(guard) goto E:
// loop;
// assert(invariant);
// assume(false);
// E: ...
// H: assert(invariant);
// havoc;
// assume(invariant);
// if(guard) goto E:
// loop;
// assert(invariant);
// assume(false);
// E: ...

// find out what can get changed in the loop
modifiest modifies;
Expand All @@ -116,17 +116,20 @@ static void check_apply_invariants(

// assert the invariant
{
goto_programt::targett a = havoc_code.add(
goto_programt::make_assertion(invariant, loop_head->source_location));
a->source_location.set_comment("Check loop invariant before entry");
code_assertt assertion{invariant};
assertion.add_source_location() = loop_head->source_location;
converter.goto_convert(assertion, havoc_code, mode);
havoc_code.instructions.back().source_location.set_comment(
"Check loop invariant before entry");
}

// havoc variables being written to
build_havoc_code(loop_head, modifies, havoc_code);

// assume the invariant
havoc_code.add(
goto_programt::make_assumption(invariant, loop_head->source_location));
code_assumet assumption{invariant};
assumption.add_source_location() = loop_head->source_location;
converter.goto_convert(assumption, havoc_code, mode);

// non-deterministically skip the loop if it is a do-while loop
if(!loop_head->is_goto())
Expand All @@ -142,11 +145,14 @@ static void check_apply_invariants(

// assert the invariant at the end of the loop body
{
goto_programt::instructiont a =
goto_programt::make_assertion(invariant, loop_end->source_location);
a.source_location.set_comment("Check that loop invariant is preserved");
goto_function.body.insert_before_swap(loop_end, a);
++loop_end;
code_assertt assertion{invariant};
assertion.add_source_location() = loop_end->source_location;
converter.goto_convert(assertion, havoc_code, mode);
havoc_code.instructions.back().source_location.set_comment(
"Check that loop invariant is preserved");
auto offset = havoc_code.instructions.size();
goto_function.body.insert_before_swap(loop_end, havoc_code);
std::advance(loop_end, offset);
}

// change the back edge into assume(false) or assume(guard)
Expand All @@ -158,15 +164,6 @@ static void check_apply_invariants(
loop_end->set_condition(boolean_negate(loop_end->get_condition()));
}

void code_contractst::convert_to_goto(
const codet &code,
const irep_idt &mode,
goto_programt &program)
{
goto_convertt converter(symbol_table, log.get_message_handler());
converter.goto_convert(code, program, mode);
}

bool code_contractst::has_contract(const irep_idt fun_name)
{
const symbolt &function_symbol = ns.lookup(fun_name);
Expand Down Expand Up @@ -322,7 +319,7 @@ code_contractst::create_ensures_instruction(

// Create instructions corresponding to the ensures clause
goto_programt ensures_program;
convert_to_goto(expression, mode, ensures_program);
converter.goto_convert(expression, ensures_program, mode);

// return a pair containing:
// 1. instructions corresponding to the ensures clause
Expand Down Expand Up @@ -424,10 +421,10 @@ bool code_contractst::apply_function_contract(
if(requires.is_not_nil())
{
goto_programt assertion;
convert_to_goto(
converter.goto_convert(
code_assertt(requires),
symbol_table.lookup_ref(function).mode,
assertion);
assertion,
symbol_table.lookup_ref(function).mode);
auto lines_to_iterate = assertion.instructions.size();
goto_program.insert_before_swap(target, assertion);
std::advance(target, lines_to_iterate);
Expand Down Expand Up @@ -483,15 +480,21 @@ bool code_contractst::apply_function_contract(
}

void code_contractst::apply_loop_contract(
const irep_idt &function_name,
goto_functionst::goto_functiont &goto_function)
{
local_may_aliast local_may_alias(goto_function);
natural_loops_mutablet natural_loops(goto_function.body);

// iterate over the (natural) loops in the function
// Iterate over the (natural) loops in the function,
// and apply any invariant annotations that we find.
for(const auto &loop : natural_loops.loop_map)
check_apply_invariants(
goto_function, local_may_alias, loop.first, loop.second);
goto_function,
local_may_alias,
loop.first,
loop.second,
symbol_table.lookup_ref(function_name).mode);
}

const symbolt &code_contractst::new_tmp_symbol(
Expand Down Expand Up @@ -966,8 +969,8 @@ void code_contractst::add_contract_check(
replace(requires_cond);

goto_programt assumption;
convert_to_goto(
code_assumet(requires_cond), function_symbol.mode, assumption);
converter.goto_convert(
code_assumet(requires_cond), assumption, function_symbol.mode);
check.destructive_append(assumption);
}

Expand Down Expand Up @@ -1078,7 +1081,7 @@ bool code_contractst::enforce_contracts()
if(has_contract(goto_function.first))
funs_to_enforce.insert(id2string(goto_function.first));
else
apply_loop_contract(goto_function.second);
apply_loop_contract(goto_function.first, goto_function.second);
}
return enforce_contracts(funs_to_enforce);
}
Expand All @@ -1098,7 +1101,7 @@ bool code_contractst::enforce_contracts(
<< messaget::eom;
continue;
}
apply_loop_contract(goto_function->second);
apply_loop_contract(goto_function->first, goto_function->second);

if(!has_contract(fun))
{
Expand Down
28 changes: 18 additions & 10 deletions src/goto-instrument/code_contracts.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,14 +19,18 @@ Date: February 2016
#include <string>
#include <unordered_set>

#include <goto-programs/goto_convert_class.h>
#include <goto-programs/goto_functions.h>
#include <goto-programs/goto_model.h>

#include <util/message.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>

#include "loop_utils.h"
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wouldn't forward declarations do the trick?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry, resolved this comment by mistake without addressing it.

I #included this header file for the loopt type, which is typedefed as:

typedef const natural_loops_mutablet::natural_loopt loopt;

Could I forward declare it here somehow? I wasn't sure how to.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I believe one of typename loopt; or class loopt; might still work, and likely the compiler will telly you if it doesn't :-) Not high priority, though.


class assigns_clauset;
class local_may_aliast;
class replace_symbolt;

class code_contractst
Expand All @@ -36,8 +40,9 @@ class code_contractst
: ns(goto_model.symbol_table),
symbol_table(goto_model.symbol_table),
goto_functions(goto_model.goto_functions),
temporary_counter(0),
log(log)
log(log),
converter(symbol_table, log.get_message_handler())

{
}

Expand Down Expand Up @@ -89,26 +94,27 @@ class code_contractst
const irep_idt &function_id,
const irep_idt &mode);

void check_apply_invariants(
goto_functionst::goto_functiont &goto_function,
const local_may_aliast &local_may_alias,
const goto_programt::targett loop_head,
const loopt &loop,
const irep_idt &mode);

namespacet ns;

protected:
symbol_tablet &symbol_table;
goto_functionst &goto_functions;

unsigned temporary_counter;
messaget &log;
goto_convertt converter;

std::unordered_set<irep_idt> summarized;

/// \brief Enforce contract of a single function
bool enforce_contract(const std::string &);

/// \brief Create goto instructions based on code and add them to program.
void convert_to_goto(
const codet &code,
const irep_idt &mode,
goto_programt &program);

/// Insert assertion statements into the goto program to ensure that
/// assigned memory is within the assignable memory frame.
bool add_pointer_checks(const std::string &);
Expand Down Expand Up @@ -159,7 +165,9 @@ class code_contractst
const exprt &lhs,
std::vector<exprt> &aliasable_references);

void apply_loop_contract(goto_functionst::goto_functiont &goto_function);
void apply_loop_contract(
const irep_idt &function_name,
goto_functionst::goto_functiont &goto_function);

/// \brief Does the named function have a contract?
bool has_contract(const irep_idt);
Expand Down
12 changes: 5 additions & 7 deletions src/goto-programs/goto_convert.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -868,13 +868,11 @@ void goto_convertt::convert_loop_invariant(
if(invariant.is_nil())
return;

goto_programt no_sideeffects;
clean_expr(invariant, no_sideeffects, mode);

INVARIANT_WITH_DIAGNOSTICS(
no_sideeffects.instructions.empty(),
"loop invariant is not side-effect free",
code.find_source_location());
if(has_subexpr(invariant, ID_side_effect))
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As I recall, this was the really contentious part last time around. This seems much less disruptive.

I think throwing the exception is correct because the user can trigger this even if the tool is non-buggy. I wonder if it would be more user-friendly to check this earlier but ... I guess we need to check it here as well.

I wonder if this might still be a bit too conservative but, if it works for you then fine.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you, yes earlier I had removed this part entirely and was doing some checking in goto-instrument instead. Now this check is performed at goto-cc compilation.

I wonder if this might still be a bit too conservative but, if it works for you then fine.

I completely agree with you. And it's on our roadmap to allow function calls within contracts, if those functions have an empty assigns clause (so no side effects).

{
throw incorrect_goto_program_exceptiont(
"Loop invariant is not side-effect free.", code.find_source_location());
}

PRECONDITION(loop->is_goto());
loop->guard.add(ID_C_spec_loop_invariant).swap(invariant);
Expand Down
1 change: 0 additions & 1 deletion src/goto-programs/goto_convert_class.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,7 +97,6 @@ class goto_convertt:public messaget

void rewrite_boolean(exprt &dest);

static bool has_sideeffect(const exprt &expr);
static bool has_function_call(const exprt &expr);

void remove_side_effect(
Expand Down