Skip to content

Optimize remove_level_2 #3559

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 6 commits into from
Dec 14, 2018
Merged

Optimize remove_level_2 #3559

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
9157f0f
Move update_identifier definition to cpp file
romainbrenguier Dec 12, 2018
5f9fd35
Remove build_identifier from the public_interface
romainbrenguier Dec 12, 2018
8bd5402
Document build_ssa_identifier_rec
romainbrenguier Dec 12, 2018
75f7c77
Hide get_l1_name from interface
romainbrenguier Dec 12, 2018
7efc7b8
Inline get_l1_name
romainbrenguier Dec 12, 2018
7114c57
Optimize remove_level_2
romainbrenguier Dec 13, 2018
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
6 changes: 4 additions & 2 deletions src/goto-symex/goto_symex_state.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,8 @@ Author: Daniel Kroening, [email protected]

#include <analyses/dirty.h>

static void get_l1_name(exprt &expr);

goto_symex_statet::goto_symex_statet()
: depth(0),
symex_target(nullptr),
Expand Down Expand Up @@ -220,7 +222,7 @@ void goto_symex_statet::assignment(
get_l1_name(l1_rhs);

ssa_exprt l1_lhs(lhs);
get_l1_name(l1_lhs);
l1_lhs.remove_level_2();

if(run_validation_checks)
{
Expand Down Expand Up @@ -750,7 +752,7 @@ void goto_symex_statet::get_original_name(typet &type) const
}
}

void goto_symex_statet::get_l1_name(exprt &expr) const
static void get_l1_name(exprt &expr)
{
// do not reset the type !

Expand Down
3 changes: 0 additions & 3 deletions src/goto-symex/goto_symex_state.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,9 +97,6 @@ class goto_symex_statet final
void set_l1_indices(ssa_exprt &expr, const namespacet &ns);
void set_l2_indices(ssa_exprt &expr, const namespacet &ns);

// only required for value_set.assign
void get_l1_name(exprt &expr) const;

// this maps L1 names to (L2) types
typedef std::unordered_map<irep_idt, typet> l1_typest;
l1_typest l1_types;
Expand Down
17 changes: 16 additions & 1 deletion src/util/ssa_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,10 @@ Author: Daniel Kroening, [email protected]

#include <util/arith_tools.h>

/// If \p expr is a symbol "s" add to \p os "s!l0@l1#l2" and to \p l1_object_os
/// "s!l0@l1".
/// If \p expr is a member or index expression, recursively apply the procedure
/// and add ".component_name" or "[index]" to \p os.
static void build_ssa_identifier_rec(
const exprt &expr,
const irep_idt &l0,
Expand Down Expand Up @@ -82,7 +86,7 @@ bool ssa_exprt::can_build_identifier(const exprt &expr)
return false;
Copy link
Contributor

Choose a reason for hiding this comment

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

Commit message typo: "and probably shouldn't." -> "and probably shouldn't be part of it."

}

std::pair<irep_idt, irep_idt> ssa_exprt::build_identifier(
static std::pair<irep_idt, irep_idt> build_identifier(
const exprt &expr,
const irep_idt &l0,
const irep_idt &l1,
Expand All @@ -95,3 +99,14 @@ std::pair<irep_idt, irep_idt> ssa_exprt::build_identifier(

return std::make_pair(irep_idt(oss.str()), irep_idt(l1_object_oss.str()));
}

void ssa_exprt::update_identifier()
{
const irep_idt &l0 = get_level_0();
const irep_idt &l1 = get_level_1();
const irep_idt &l2 = get_level_2();

auto idpair = build_identifier(get_original_expr(), l0, l1, l2);
set_identifier(idpair.first);
set(ID_L1_object_identifier, idpair.second);
}
19 changes: 2 additions & 17 deletions src/util/ssa_expr.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -101,7 +101,7 @@ class ssa_exprt:public symbol_exprt
void remove_level_2()
{
remove(ID_L2);
update_identifier();
set_identifier(get_l1_object_identifier());
}

const irep_idt get_level_0() const
Expand All @@ -119,22 +119,7 @@ class ssa_exprt:public symbol_exprt
return get(ID_L2);
}

void update_identifier()
{
const irep_idt &l0=get_level_0();
const irep_idt &l1=get_level_1();
const irep_idt &l2=get_level_2();

auto idpair=build_identifier(get_original_expr(), l0, l1, l2);
set_identifier(idpair.first);
set(ID_L1_object_identifier, idpair.second);
}

static std::pair<irep_idt, irep_idt> build_identifier(
const exprt &src,
const irep_idt &l0,
const irep_idt &l1,
const irep_idt &l2);
void update_identifier();

/* Used to determine whether or not an identifier can be built
* before trying and getting an exception */
Expand Down