Skip to content

Make dirtyt traverse operands of OTHER instructions #7106

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
Sep 7, 2022
Merged

Make dirtyt traverse operands of OTHER instructions #7106

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
57 changes: 46 additions & 11 deletions src/analyses/dirty.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,14 +19,49 @@ Date: March 2013
void dirtyt::build(const goto_functiont &goto_function)
{
for(const auto &i : goto_function.body.instructions)
i.apply([this](const exprt &e) { find_dirty(e); });
{
if(i.is_other())
{
search_other(i);
}
else
{
i.apply([this](const exprt &e) { find_dirty(e); });
}
}
}

void dirtyt::search_other(const goto_programt::instructiont &instruction)
{
INVARIANT(instruction.is_other(), "instruction type must be OTHER");
Copy link
Collaborator

Choose a reason for hiding this comment

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

Pedantry but I would PRECONDITION this because it is the caller's responsibility rather than a property of the algorithm.

if(instruction.get_other().id() == ID_code)
{
const codet &code = instruction.get_other();
const irep_idt &statement = code.get_statement();
if(
statement == ID_expression || statement == ID_array_set ||
statement == ID_array_equal || statement == ID_array_copy ||
statement == ID_array_replace || statement == ID_havoc_object ||
statement == ID_input || statement == ID_output)
{
forall_operands(it, code)
find_dirty(*it);
}
// other possible cases according to goto_programt::instructiont::output
// and goto_symext::symex_other:
// statement == ID_fence ||
// statement == ID_user_specified_predicate ||
// statement == ID_user_specified_parameter_predicates ||
// statement == ID_user_specified_return_predicates ||
// statement == ID_decl || statement == ID_nondet || statement == ID_asm)
}
}

void dirtyt::find_dirty(const exprt &expr)
{
if(expr.id()==ID_address_of)
if(expr.id() == ID_address_of)
Copy link
Collaborator

Choose a reason for hiding this comment

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

Don't change it on this PR but in general it is good to have refactoring in a separate commit to make reviewing and bisecting for regressions easier.

{
const address_of_exprt &address_of_expr=to_address_of_expr(expr);
const address_of_exprt &address_of_expr = to_address_of_expr(expr);
find_dirty_address_of(address_of_expr.object());
return;
}
Expand All @@ -37,27 +72,26 @@ void dirtyt::find_dirty(const exprt &expr)

void dirtyt::find_dirty_address_of(const exprt &expr)
{
if(expr.id()==ID_symbol)
if(expr.id() == ID_symbol)
{
const irep_idt &identifier=
to_symbol_expr(expr).get_identifier();
const irep_idt &identifier = to_symbol_expr(expr).get_identifier();

dirty.insert(identifier);
}
else if(expr.id()==ID_member)
else if(expr.id() == ID_member)
{
find_dirty_address_of(to_member_expr(expr).struct_op());
}
else if(expr.id()==ID_index)
else if(expr.id() == ID_index)
{
find_dirty_address_of(to_index_expr(expr).array());
find_dirty(to_index_expr(expr).index());
}
else if(expr.id()==ID_dereference)
else if(expr.id() == ID_dereference)
{
find_dirty(to_dereference_expr(expr).pointer());
}
else if(expr.id()==ID_if)
else if(expr.id() == ID_if)
{
find_dirty_address_of(to_if_expr(expr).true_case());
find_dirty_address_of(to_if_expr(expr).false_case());
Expand All @@ -76,7 +110,8 @@ void dirtyt::output(std::ostream &out) const
/// \param id: function id to analyse
/// \param function: function to analyse
void incremental_dirtyt::populate_dirty_for_function(
const irep_idt &id, const goto_functionst::goto_functiont &function)
const irep_idt &id,
const goto_functionst::goto_functiont &function)
{
auto insert_result = dirty_processed_functions.insert(id);
if(insert_result.second)
Expand Down
18 changes: 9 additions & 9 deletions src/analyses/dirty.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,12 +14,13 @@ Date: March 2013
#ifndef CPROVER_ANALYSES_DIRTY_H
#define CPROVER_ANALYSES_DIRTY_H

#include <unordered_set>

#include <util/std_expr.h>
#include <util/invariant.h>
#include <util/std_expr.h>

#include <goto-programs/goto_functions.h>

#include <unordered_set>

/// Dirty variables are ones which have their address taken so we can't
/// reliably work out where they may be assigned and are also considered shared
/// state in the presence of multi-threading.
Expand Down Expand Up @@ -65,7 +66,7 @@ class dirtyt
bool operator()(const irep_idt &id) const
{
die_if_uninitialized();
return dirty.find(id)!=dirty.end();
return dirty.find(id) != dirty.end();
}

bool operator()(const symbol_exprt &expr) const
Expand Down Expand Up @@ -100,14 +101,12 @@ class dirtyt

// variables whose address is taken
std::unordered_set<irep_idt> dirty;

void search_other(const goto_programt::instructiont &instruction);
void find_dirty(const exprt &expr);
void find_dirty_address_of(const exprt &expr);
};

inline std::ostream &operator<<(
std::ostream &out,
const dirtyt &dirty)
inline std::ostream &operator<<(std::ostream &out, const dirtyt &dirty)
{
dirty.output(out);
return out;
Expand All @@ -119,7 +118,8 @@ class incremental_dirtyt
{
public:
void populate_dirty_for_function(
const irep_idt &id, const goto_functionst::goto_functiont &function);
const irep_idt &id,
const goto_functionst::goto_functiont &function);

bool operator()(const irep_idt &id) const
{
Expand Down
49 changes: 2 additions & 47 deletions src/goto-instrument/contracts/cfg_info.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,51 +31,6 @@ Date: June 2022
#include <set>
#include <vector>

/// Work around the fact that dirtyt does not look into
/// OTHER instructions
class dirty_altt : public dirtyt
{
public:
dirty_altt() : dirtyt()
{
}

explicit dirty_altt(const goto_functiont &goto_function)
: dirtyt(goto_function)
{
collect_other(goto_function);
}

explicit dirty_altt(const goto_functionst &goto_functions)
: dirtyt(goto_functions)
{
for(const auto &gf_entry : goto_functions.function_map)
collect_other(gf_entry.second);
}

protected:
void collect_other(const goto_functiont &goto_function)
{
for(const auto &i : goto_function.body.instructions)
{
if(i.is_other())
{
auto &statement = i.get_other().get_statement();
if(
statement == ID_array_set || statement == ID_array_copy ||
statement == ID_array_replace || statement == ID_array_equal ||
statement == ID_havoc_object)
{
for(const auto &op : i.get_other().operands())
{
find_dirty(op);
}
}
}
}
}
};

/// Stores information about a goto function computed from its CFG.
///
/// The methods of this class provide information about identifiers
Expand Down Expand Up @@ -177,7 +132,7 @@ class function_cfg_infot : public cfg_infot
}

private:
const dirty_altt is_dirty;
const dirtyt is_dirty;
const localst locals;
std::unordered_set<irep_idt> parameters;
};
Expand Down Expand Up @@ -230,7 +185,7 @@ class loop_cfg_infot : public cfg_infot
}

private:
const dirty_altt is_dirty;
const dirtyt is_dirty;
std::unordered_set<irep_idt> locals;
};
#endif