Skip to content

Store goto_symex::\guard in a single place [blocks: #3619] #4017

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.

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
Feb 4, 2019
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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/auto_objects.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@ void goto_symext::trigger_auto_object(
const ssa_exprt &ssa_expr=to_ssa_expr(expr);
const irep_idt &obj_identifier=ssa_expr.get_object_name();

if(obj_identifier!="goto_symex::\\guard")
if(obj_identifier != statet::guard_identifier())
{
const symbolt &symbol=
ns.lookup(obj_identifier);
Expand Down
5 changes: 0 additions & 5 deletions src/goto-symex/goto_symex.h
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,6 @@ class goto_symext
target(_target),
atomic_section_counter(0),
log(mh),
guard_identifier("goto_symex::\\guard"),
path_storage(path_storage),
path_segment_vccs(0),
_total_vccs(std::numeric_limits<unsigned>::max()),
Expand Down Expand Up @@ -238,10 +237,6 @@ class goto_symext
guardt &,
bool keep_array);

// guards

const irep_idt guard_identifier;

virtual void symex_goto(statet &);
virtual void symex_start_thread(statet &);
virtual void symex_atomic_begin(statet &);
Expand Down
10 changes: 7 additions & 3 deletions src/goto-symex/goto_symex_state.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -180,7 +180,7 @@ void goto_symex_statet::assignment(

#if 0
PRECONDITION(l1_identifier != get_original_name(l1_identifier)
|| l1_identifier=="goto_symex::\\guard"
|| l1_identifier == guard_identifier()
|| ns.lookup(l1_identifier).is_shared()
|| has_prefix(id2string(l1_identifier), "symex::invalid_object")
|| has_prefix(id2string(l1_identifier), "symex_dynamic::dynamic_object"));
Expand Down Expand Up @@ -372,9 +372,11 @@ bool goto_symex_statet::l2_thread_read_encoding(
// is it a shared object?
const irep_idt &obj_identifier=expr.get_object_name();
if(
obj_identifier == "goto_symex::\\guard" ||
obj_identifier == guard_identifier() ||
(!ns.lookup(obj_identifier).is_shared() && !(dirty)(obj_identifier)))
{
return false;
}

ssa_exprt ssa_l1=expr;
ssa_l1.remove_level_2();
Expand Down Expand Up @@ -508,9 +510,11 @@ bool goto_symex_statet::l2_thread_write_encoding(
// is it a shared object?
const irep_idt &obj_identifier=expr.get_object_name();
if(
obj_identifier == "goto_symex::\\guard" ||
obj_identifier == guard_identifier() ||
(!ns.lookup(obj_identifier).is_shared() && !(dirty)(obj_identifier)))
{
return false; // not shared
}

// see whether we are within an atomic section
if(atomic_section_id!=0)
Expand Down
7 changes: 7 additions & 0 deletions src/goto-symex/goto_symex_state.h
Original file line number Diff line number Diff line change
Expand Up @@ -220,6 +220,13 @@ class goto_symex_statet final
typedef std::map<goto_programt::const_targett, goto_state_listt>
goto_state_mapt;

// guards
static irep_idt guard_identifier()
{
static irep_idt id = "goto_symex::\\guard";
return id;
}

// stack frames -- these are used for function calls and
// for exceptions
struct framet
Expand Down
4 changes: 3 additions & 1 deletion src/goto-symex/renaming_level.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,8 @@ Author: Romain Brenguier, [email protected]
#include <util/ssa_expr.h>
#include <util/symbol.h>

#include "goto_symex_state.h"

void symex_level0t::
operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr)
{
Expand All @@ -25,7 +27,7 @@ operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr)
const irep_idt &obj_identifier = ssa_expr.get_object_name();

// guards are not L0-renamed
if(obj_identifier == "goto_symex::\\guard")
if(obj_identifier == goto_symex_statet::guard_identifier())
return;

const symbolt *s;
Expand Down
9 changes: 3 additions & 6 deletions src/goto-symex/symex_goto.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -243,8 +243,8 @@ void goto_symext::symex_goto(statet &state)
}
else
{
symbol_exprt guard_symbol_expr=
symbol_exprt(guard_identifier, bool_typet());
symbol_exprt guard_symbol_expr =
symbol_exprt(statet::guard_identifier(), bool_typet());
exprt new_rhs = boolean_negate(new_guard);

ssa_exprt new_lhs(guard_symbol_expr);
Expand Down Expand Up @@ -394,7 +394,6 @@ static void for_each2(
/// \param [in, out] dest_state: second state
/// \param ns: namespace
/// \param diff_guard: difference between the guards of the two states
/// \param guard_identifier: prefix used for goto symex guards
/// \param [out] log: logger for debug messages
/// \param do_simplify: should the right-hand-side of the assignment that is
/// added to the target be simplified
Expand All @@ -408,7 +407,6 @@ static void merge_names(
goto_symext::statet &dest_state,
const namespacet &ns,
const guardt &diff_guard,
const irep_idt &guard_identifier,
messaget &log,
const bool do_simplify,
symex_target_equationt &target,
Expand All @@ -419,7 +417,7 @@ static void merge_names(
const irep_idt l1_identifier = ssa.get_identifier();
const irep_idt &obj_identifier = ssa.get_object_name();

if(obj_identifier == guard_identifier)
if(obj_identifier == goto_symext::statet::guard_identifier())
return; // just a guard, don't bother

if(goto_count == dest_count)
Expand Down Expand Up @@ -544,7 +542,6 @@ void goto_symext::phi_function(
dest_state,
ns,
diff_guard,
guard_identifier,
log,
symex_config.simplify_opt,
target,
Expand Down