From 9157f0f2324cc35e17ad1f2ac1ebe78abfe5ff2f Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 12 Dec 2018 10:49:14 +0000 Subject: [PATCH 1/6] Move update_identifier definition to cpp file To lighten the header. --- src/util/ssa_expr.cpp | 11 +++++++++++ src/util/ssa_expr.h | 11 +---------- 2 files changed, 12 insertions(+), 10 deletions(-) diff --git a/src/util/ssa_expr.cpp b/src/util/ssa_expr.cpp index ce3b2527f51..4fa14269c8b 100644 --- a/src/util/ssa_expr.cpp +++ b/src/util/ssa_expr.cpp @@ -95,3 +95,14 @@ std::pair 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); +} diff --git a/src/util/ssa_expr.h b/src/util/ssa_expr.h index 56d4f627d8a..ada1e40dc35 100644 --- a/src/util/ssa_expr.h +++ b/src/util/ssa_expr.h @@ -119,16 +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); - } + void update_identifier(); static std::pair build_identifier( const exprt &src, From 5f9fd353656910c2ab7c5e7a70399e21a5ffd6b2 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 12 Dec 2018 10:52:40 +0000 Subject: [PATCH 2/6] Remove build_identifier from the public_interface This is not used outside of the ssa_exprt class and shouldn't be part of the public interface. --- src/util/ssa_expr.cpp | 2 +- src/util/ssa_expr.h | 6 ------ 2 files changed, 1 insertion(+), 7 deletions(-) diff --git a/src/util/ssa_expr.cpp b/src/util/ssa_expr.cpp index 4fa14269c8b..8a3e56fcb34 100644 --- a/src/util/ssa_expr.cpp +++ b/src/util/ssa_expr.cpp @@ -82,7 +82,7 @@ bool ssa_exprt::can_build_identifier(const exprt &expr) return false; } -std::pair ssa_exprt::build_identifier( +static std::pair build_identifier( const exprt &expr, const irep_idt &l0, const irep_idt &l1, diff --git a/src/util/ssa_expr.h b/src/util/ssa_expr.h index ada1e40dc35..022d6167095 100644 --- a/src/util/ssa_expr.h +++ b/src/util/ssa_expr.h @@ -121,12 +121,6 @@ class ssa_exprt:public symbol_exprt void update_identifier(); - static std::pair build_identifier( - const exprt &src, - const irep_idt &l0, - const irep_idt &l1, - const irep_idt &l2); - /* Used to determine whether or not an identifier can be built * before trying and getting an exception */ static bool can_build_identifier(const exprt &src); From 8bd5402c87207eb981f5dd6fbaaee72c4a3b86d3 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 12 Dec 2018 11:01:23 +0000 Subject: [PATCH 3/6] Document build_ssa_identifier_rec --- src/util/ssa_expr.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/util/ssa_expr.cpp b/src/util/ssa_expr.cpp index 8a3e56fcb34..3d25ae8c328 100644 --- a/src/util/ssa_expr.cpp +++ b/src/util/ssa_expr.cpp @@ -13,6 +13,10 @@ Author: Daniel Kroening, kroening@kroening.com #include +/// 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, From 75f7c777b1aac9f1568f264e432a7c8a20525c41 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 12 Dec 2018 11:09:04 +0000 Subject: [PATCH 4/6] Hide get_l1_name from interface This is only used in one function. --- src/goto-symex/goto_symex_state.cpp | 4 +++- src/goto-symex/goto_symex_state.h | 3 --- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 0b99d2434f0..eee56bea977 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -25,6 +25,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +static void get_l1_name(exprt &expr); + goto_symex_statet::goto_symex_statet() : depth(0), symex_target(nullptr), @@ -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 ! diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index b2dcd4741dc..83923692de5 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -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 l1_typest; l1_typest l1_types; From 7efc7b8fde6d370a2b571ab4d2ff655e577ca1da Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 12 Dec 2018 11:12:57 +0000 Subject: [PATCH 5/6] Inline get_l1_name For ssa_exprt's this always remove_level_2 --- src/goto-symex/goto_symex_state.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index eee56bea977..6bba6a2ead0 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -222,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) { From 7114c571611e9ab17b8e7bec13e1a8b55248b4e5 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 13 Dec 2018 11:28:39 +0000 Subject: [PATCH 6/6] Optimize remove_level_2 To reset the identifier we can just used the l1_object_identifier which is a cached version of the level1 identifier. --- src/util/ssa_expr.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/ssa_expr.h b/src/util/ssa_expr.h index 022d6167095..136065fcfe5 100644 --- a/src/util/ssa_expr.h +++ b/src/util/ssa_expr.h @@ -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