Skip to content

Value-set analysis: templatise and virtualise to facilitate customisation #1413

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 4 commits into from
Oct 13, 2017
Merged

Value-set analysis: templatise and virtualise to facilitate customisation #1413

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
a2c1685
Templatize and virtualize value-set analysis
smowton Mar 8, 2017
9465771
Value-set analysis: ignore DEAD statements
smowton Sep 22, 2017
e669c12
Add unit tests for value-set-analysis customisation
smowton Sep 14, 2017
a99b254
Indirect value_set_domaint -> value_sett operations via non-member fu…
smowton Oct 13, 2017
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
2 changes: 1 addition & 1 deletion src/goto-symex/postcondition.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -174,7 +174,7 @@ bool postconditiont::is_used(
// aliasing may happen here

value_setst::valuest expr_set;
value_set.get_value_set(expr.op0(), expr_set, ns);
value_set.read_value_set(expr.op0(), expr_set, ns);
std::unordered_set<irep_idt, irep_id_hash> symbols;

for(value_setst::valuest::const_iterator
Expand Down
2 changes: 1 addition & 1 deletion src/goto-symex/symex_dereference_state.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,7 @@ void symex_dereference_statet::get_value_set(
const exprt &expr,
value_setst::valuest &value_set)
{
state.value_set.get_value_set(expr, value_set, goto_symex.ns);
state.value_set.read_value_set(expr, value_set, goto_symex.ns);

#if 0
std::cout << "**************************\n";
Expand Down
1 change: 0 additions & 1 deletion src/pointer-analysis/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,6 @@ SRC = add_failed_symbols.cpp \
value_set_analysis_fivr.cpp \
value_set_analysis_fivrns.cpp \
value_set_dereference.cpp \
value_set_domain.cpp \
value_set_domain_fi.cpp \
value_set_domain_fivr.cpp \
value_set_domain_fivrns.cpp \
Expand Down
2 changes: 1 addition & 1 deletion src/pointer-analysis/show_value_sets.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,10 +12,10 @@ Author: Daniel Kroening, [email protected]
#ifndef CPROVER_POINTER_ANALYSIS_SHOW_VALUE_SETS_H
#define CPROVER_POINTER_ANALYSIS_SHOW_VALUE_SETS_H

#include <pointer-analysis/value_set_analysis.h>
Copy link
Contributor

Choose a reason for hiding this comment

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

Why swap this to a full include when forward declaration was sufficient?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

value_set_analysist is a template specialisation now; class value_set_analysist won't work as the forward-decl will clash with the actual definition. There might be a way around this but I don't know it.

#include <util/ui_message.h>

class goto_modelt;
class value_set_analysist;

void show_value_sets(
ui_message_handlert::uit,
Expand Down
25 changes: 19 additions & 6 deletions src/pointer-analysis/value_set.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -311,7 +311,7 @@ bool value_sett::eval_pointer_offset(
return mod;
}

void value_sett::get_value_set(
void value_sett::read_value_set(
const exprt &expr,
value_setst::valuest &dest,
const namespacet &ns) const
Expand Down Expand Up @@ -340,7 +340,7 @@ void value_sett::get_value_set(
{
exprt tmp(expr);
if(!is_simplified)
simplify(tmp, ns);
simplifier(tmp, ns);

get_value_set_rec(tmp, dest, "", tmp.type(), ns);
}
Expand Down Expand Up @@ -809,7 +809,7 @@ void value_sett::get_value_set_rec(

exprt op1=expr.op1();
if(eval_pointer_offset(op1, ns))
simplify(op1, ns);
simplifier(op1, ns);

mp_integer op1_offset;
const typet &op0_type=ns.follow(expr.op0().type());
Expand Down Expand Up @@ -908,7 +908,7 @@ void value_sett::dereference_rec(
dest=src;
}

void value_sett::get_reference_set(
void value_sett::read_reference_set(
const exprt &expr,
value_setst::valuest &dest,
const namespacet &ns) const
Expand Down Expand Up @@ -1205,6 +1205,12 @@ void value_sett::assign(
object_mapt values_rhs;
get_value_set(rhs, values_rhs, ns, is_simplified);

// Permit custom subclass to alter the read values prior to write:
adjust_assign_rhs_values(rhs, ns, values_rhs);

// Permit custom subclass to perform global side-effects prior to write:
apply_assign_side_effects(lhs, rhs, ns);

assign_rec(lhs, values_rhs, "", ns, add_to_sets);
}
}
Expand Down Expand Up @@ -1482,7 +1488,7 @@ void value_sett::do_end_function(
assign(lhs, rhs, ns, false, false);
}

void value_sett::apply_code(
void value_sett::apply_code_rec(
const codet &code,
const namespacet &ns)
{
Expand All @@ -1491,7 +1497,7 @@ void value_sett::apply_code(
if(statement==ID_block)
{
forall_operands(it, code)
apply_code(to_code(*it), ns);
apply_code_rec(to_code(*it), ns);
}
else if(statement==ID_function_call)
{
Expand Down Expand Up @@ -1609,6 +1615,10 @@ void value_sett::apply_code(
{
// doesn't do anything
}
else if(statement==ID_dead)
{
// ignore (could potentially prune value set in future)
}
else
{
// std::cerr << code.pretty() << '\n';
Expand Down Expand Up @@ -1694,3 +1704,6 @@ exprt value_sett::make_member(

return member_expr;
}

value_sett::expr_simplifiert value_sett::default_simplifier=
[](exprt &e, const namespacet &ns) { simplify(e, ns); };
98 changes: 80 additions & 18 deletions src/pointer-analysis/value_set.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,8 +24,20 @@ class namespacet;

class value_sett
{
typedef std::function<void(exprt &, const namespacet &)> expr_simplifiert;

static expr_simplifiert default_simplifier;

public:
value_sett():location_number(0)
value_sett():
location_number(0),
simplifier(default_simplifier)
{
}

explicit value_sett(expr_simplifiert simplifier):
location_number(0),
simplifier(std::move(simplifier))
{
}

Expand Down Expand Up @@ -166,7 +178,7 @@ class value_sett
typedef std::unordered_map<idt, entryt, string_hash> valuest;
#endif

void get_value_set(
void read_value_set(
const exprt &expr,
value_setst::valuest &dest,
const namespacet &ns) const;
Expand Down Expand Up @@ -213,7 +225,10 @@ class value_sett

void apply_code(
const codet &code,
const namespacet &ns);
const namespacet &ns)
{
apply_code_rec(code, ns);
}

void assign(
const exprt &lhs,
Expand All @@ -232,7 +247,7 @@ class value_sett
const exprt &lhs,
const namespacet &ns);

void get_reference_set(
void read_reference_set(
const exprt &expr,
value_setst::valuest &dest,
const namespacet &ns) const;
Expand All @@ -242,13 +257,6 @@ class value_sett
const namespacet &ns) const;

protected:
Copy link
Contributor

Choose a reason for hiding this comment

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

Prefer to make these private if at all possible.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

The virtual override points definitely need defer-to-base I'm afraid

void get_value_set_rec(
const exprt &expr,
object_mapt &dest,
const std::string &suffix,
const typet &original_type,
const namespacet &ns) const;

void get_value_set(
const exprt &expr,
object_mapt &dest,
Expand All @@ -272,13 +280,6 @@ class value_sett
const exprt &src,
exprt &dest) const;

void assign_rec(
const exprt &lhs,
const object_mapt &values_rhs,
const std::string &suffix,
const namespacet &ns,
bool add_to_sets);

void do_free(
const exprt &op,
const namespacet &ns);
Expand All @@ -287,6 +288,67 @@ class value_sett
const exprt &src,
const irep_idt &component_name,
const namespacet &ns);

// Expression simplification:

private:
/// Expression simplification function; by default, plain old
/// util/simplify_expr, but can be customised by subclass.
expr_simplifiert simplifier;

protected:
/// Run registered expression simplifier
void run_simplifier(exprt &e, const namespacet &ns)
{
simplifier(e, ns);
}

// Subclass customisation points:

protected:
/// Subclass customisation point for recursion over RHS expression:
virtual void get_value_set_rec(
const exprt &expr,
object_mapt &dest,
const std::string &suffix,
const typet &original_type,
const namespacet &ns) const;

/// Subclass customisation point for recursion over LHS expression:
virtual void assign_rec(
const exprt &lhs,
const object_mapt &values_rhs,
const std::string &suffix,
const namespacet &ns,
bool add_to_sets);

/// Subclass customisation point for applying code to this domain:
virtual void apply_code_rec(
const codet &code,
const namespacet &ns);

private:
/// Subclass customisation point to filter or otherwise alter the value-set
/// returned from get_value_set before it is passed into assign. For example,
/// this is used in one subclass to tag and thus differentiate values that
/// originated in a particular place, vs. those that have been copied.
virtual void adjust_assign_rhs_values(
const exprt &rhs,
const namespacet &ns,
object_mapt &rhs_values) const
{
}

/// Subclass customisation point to apply global side-effects to this domain,
/// after RHS values are read but before they are written. For example, this
/// is used in a recency-analysis plugin to demote existing most-recent
/// objects to general case ones.
virtual void apply_assign_side_effects(
const exprt &lhs,
const exprt &rhs,
const namespacet &ns)
{
}
};

#endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_H
65 changes: 0 additions & 65 deletions src/pointer-analysis/value_set_analysis.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,74 +13,9 @@ Author: Daniel Kroening, [email protected]

#include <util/prefix.h>
#include <util/cprover_prefix.h>
#include <util/xml_expr.h>
#include <util/xml.h>

#include <langapi/language_util.h>

void value_set_analysist::initialize(
const goto_programt &goto_program)
{
baset::initialize(goto_program);
}

void value_set_analysist::initialize(
const goto_functionst &goto_functions)
{
baset::initialize(goto_functions);
}

void value_set_analysist::convert(
const goto_programt &goto_program,
const irep_idt &identifier,
xmlt &dest) const
{
source_locationt previous_location;

forall_goto_program_instructions(i_it, goto_program)
{
const source_locationt &location=i_it->source_location;

if(location==previous_location)
continue;

if(location.is_nil() || location.get_file().empty())
continue;

// find value set
const value_sett &value_set=(*this)[i_it].value_set;

xmlt &i=dest.new_element("instruction");
i.new_element()=::xml(location);

for(value_sett::valuest::const_iterator
v_it=value_set.values.begin();
v_it!=value_set.values.end();
v_it++)
{
xmlt &var=i.new_element("variable");
var.new_element("identifier").data=
id2string(v_it->first);

#if 0
const value_sett::expr_sett &expr_set=
v_it->second.expr_set();

for(value_sett::expr_sett::const_iterator
e_it=expr_set.begin();
e_it!=expr_set.end();
e_it++)
{
std::string value_str=
from_expr(ns, identifier, *e_it);

var.new_element("value").data=
xmlt::escape(value_str);
}
#endif
}
}
}
void convert(
const goto_functionst &goto_functions,
const value_set_analysist &value_set_analysis,
Expand Down
Loading