Skip to content

L1 renaming at each declaration #3980

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 2 commits into from
Mar 7, 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
4 changes: 2 additions & 2 deletions regression/cbmc-cover/pointer-function-parameters/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,8 @@ main.c
^\*\* 5 of 5 covered \(100\.0%\)$
^Test suite:$
^(tmp(\$\d+)?=[^,]*, a=\(\(signed int \*\)NULL\))|(a=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*)$
^(a=&tmp(\$\d+)?!0, tmp(\$\d+)?=4)|(tmp(\$\d+)?=4, a=&tmp(\$\d+)?!0)$
^(a=&tmp(\$\d+)?!0, tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+))|(tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+), a=&tmp(\$\d+)?!0)$
^(a=&tmp(\$\d+)?!0@1, tmp(\$\d+)?=4)|(tmp(\$\d+)?=4, a=&tmp(\$\d+)?!0@1)$
^(a=&tmp(\$\d+)?!0@1, tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+))|(tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+), a=&tmp(\$\d+)?!0@1)$
^EXIT=0$
^SIGNAL=0$
--
Expand Down
10 changes: 10 additions & 0 deletions regression/cbmc/Local_out_of_scope4/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
int g;

int main()
{
for(int i = 0; i < 4; ++i)
{
int *x;
*&x = &g;
}
}
8 changes: 8 additions & 0 deletions regression/cbmc/Local_out_of_scope4/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
main.c
--pointer-check
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
3 changes: 1 addition & 2 deletions regression/cbmc/vla3/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -7,5 +7,4 @@ main.c
--
^warning: ignoring
--
Renaming is inconsistent across loop iterations as we map L1 names to types, but
do not actually introduce new L1 ids each time we declare an object.
The array decision procedure does not yet handle member expressions.
3 changes: 2 additions & 1 deletion src/goto-programs/goto_clean_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,8 @@ symbol_exprt goto_convertt::make_compound_literal(

// The lifetime of compound literals is really that of
// the block they are in.
copy(code_declt(result), DECL, dest);
if(!new_symbol.is_static_lifetime)
copy(code_declt(result), DECL, dest);

code_assignt code_assign(result, expr);
code_assign.add_source_location()=source_location;
Expand Down
26 changes: 26 additions & 0 deletions src/goto-symex/goto_symex_state.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -766,3 +766,29 @@ void goto_symex_statet::print_backtrace(std::ostream &out) const
<< frame.calling_location.pc->location_number << "\n";
}
}

void goto_symex_statet::add_object(
ssa_exprt &ssa,
std::size_t l1_index,
const namespacet &ns)
{
framet &frame = call_stack().top();

const irep_idt l0_name = ssa.get_identifier();

// save old L1 name, if any
auto existing_or_new_entry = level1.current_names.emplace(
std::piecewise_construct,
std::forward_as_tuple(l0_name),
std::forward_as_tuple(ssa, l1_index));

if(!existing_or_new_entry.second)
{
frame.old_level1.emplace(l0_name, existing_or_new_entry.first->second);
existing_or_new_entry.first->second = std::make_pair(ssa, l1_index);
}

ssa = rename_ssa<L1>(std::move(ssa), ns);
const bool inserted = frame.local_objects.insert(ssa.get_identifier()).second;
INVARIANT(inserted, "l1_name expected to be unique by construction");
}
8 changes: 5 additions & 3 deletions src/goto-symex/goto_symex_state.h
Original file line number Diff line number Diff line change
Expand Up @@ -60,9 +60,6 @@ class goto_symex_statet final : public goto_statet

symex_target_equationt *symex_target;

// we remember all L1 renamings
std::set<irep_idt> l1_history;

symex_level0t level0;
symex_level1t level1;

Expand Down Expand Up @@ -141,6 +138,11 @@ class goto_symex_statet final : public goto_statet
return threads[source.thread_nr].call_stack;
}

/// Create a new instance of the L0-renamed object \p ssa. As part of this,
/// turn \p ssa into an L1-renamed SSA expression. When doing so, use
/// \p l1_index as the L1 index, which must not previously have been used.
void add_object(ssa_exprt &ssa, std::size_t l1_index, const namespacet &ns);

void print_backtrace(std::ostream &) const;

// threads
Expand Down
14 changes: 14 additions & 0 deletions src/goto-symex/path_storage.h
Original file line number Diff line number Diff line change
Expand Up @@ -98,11 +98,25 @@ class path_storaget
/// error-handling paths.
std::unordered_map<irep_idt, local_safe_pointerst> safe_pointers;

/// Provide a unique index for a given \p id, starting from \p minimum_index.
std::size_t get_unique_index(const irep_idt &id, std::size_t minimum_index)
{
auto entry = unique_index_map.emplace(id, minimum_index);

if(!entry.second)
entry.first->second = std::max(entry.first->second + 1, minimum_index);
Copy link
Contributor

Choose a reason for hiding this comment

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

It looks like we could avoid the if condition if the function is always called with the same minimum index, I don't know if that's always the case.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

No, even right now we (intentionally) use 0 for L1 indices when setting up new threads, but elsewhere use 1. And also that facility is rather general, we could as well use it for non-det counters any maybe others.


return entry.first->second;
}

private:
// Derived classes should override these methods, allowing the base class to
// enforce preconditions.
virtual patht &private_peek() = 0;
virtual void private_pop() = 0;

/// Storage used by \ref get_unique_index.
std::unordered_map<irep_idt, std::size_t> unique_index_map;
};

/// \brief LIFO save queue: depth-first search, try to finish paths
Expand Down
14 changes: 6 additions & 8 deletions src/goto-symex/symex_dead.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,8 +11,6 @@ Author: Daniel Kroening, [email protected]

#include "goto_symex.h"

#include <cassert>

#include <util/std_expr.h>

#include <pointer-analysis/add_failed_symbols.h>
Expand All @@ -23,9 +21,6 @@ void goto_symext::symex_dead(statet &state)

const code_deadt &code = instruction.get_dead();

// We increase the L2 renaming to make these non-deterministic.
// We also prevent propagation of old values.

ssa_exprt ssa = state.rename_ssa<L1>(ssa_exprt{code.symbol()}, ns);

// in case of pointers, put something into the value set
Expand All @@ -43,10 +38,13 @@ void goto_symext::symex_dead(statet &state)

const irep_idt &l1_identifier = ssa.get_identifier();

// prevent propagation
// we cannot remove the object from the L1 renaming map, because L1 renaming
// information is not local to a path, but removing it from the propagation
// map is safe as 1) it is local to a path and 2) this instance can no longer
// appear
state.propagation.erase(l1_identifier);

// L2 renaming
// increment the L2 index to ensure a merge on join points will propagate the
// value for branches that are still live
auto level2_it = state.level2.current_names.find(l1_identifier);
if(level2_it != state.level2.current_names.end())
symex_renaming_levelt::increase_counter(level2_it);
Expand Down
27 changes: 14 additions & 13 deletions src/goto-symex/symex_decl.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -34,10 +34,16 @@ void goto_symext::symex_decl(statet &state)

void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
{
// We increase the L2 renaming to make these non-deterministic.
// We also prevent propagation of old values.

ssa_exprt ssa = state.rename_ssa<L1>(ssa_exprt{expr}, ns);
// each declaration introduces a new object, which we record as a fresh L1
// index

ssa_exprt ssa = state.rename_ssa<L0>(ssa_exprt{expr}, ns);
// We use "1" as the first level-1 index, which is in line with doing so for
// level-2 indices (but it's an arbitrary choice, we have just always been
// doing it this way).
const std::size_t fresh_l1_index =
path_storage.get_unique_index(ssa.get_identifier(), 1);
state.add_object(ssa, fresh_l1_index, ns);
const irep_idt &l1_identifier = ssa.get_identifier();

// rename type to L2
Expand All @@ -57,16 +63,11 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
state.value_set.assign(ssa, l1_rhs, ns, true, false);
}

// prevent propagation
state.propagation.erase(l1_identifier);

// L2 renaming
// inlining may yield multiple declarations of the same identifier
// within the same L1 context
const auto level2_it =
state.level2.current_names.emplace(l1_identifier, std::make_pair(ssa, 0))
.first;
symex_renaming_levelt::increase_counter(level2_it);
bool is_new =
state.level2.current_names.emplace(l1_identifier, std::make_pair(ssa, 1))
.second;
CHECK_RETURN(is_new);
const bool record_events=state.record_events;
state.record_events=false;
exprt expr_l2 = state.rename(std::move(ssa), ns);
Expand Down
60 changes: 10 additions & 50 deletions src/goto-symex/symex_function_call.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]
static void locality(
const irep_idt &function_identifier,
goto_symext::statet &state,
path_storaget &path_storage,
const goto_functionst::goto_functiont &goto_function,
const namespacet &ns);

Expand Down Expand Up @@ -307,7 +308,7 @@ void goto_symext::symex_function_call_code(
framet &frame = state.call_stack().new_frame(state.source);

// preserve locality of local variables
locality(identifier, state, goto_function, ns);
locality(identifier, state, path_storage, goto_function, ns);

// assign actuals to formal parameters
parameter_assignments(identifier, goto_function, state, arguments);
Expand Down Expand Up @@ -383,68 +384,27 @@ void goto_symext::symex_end_of_function(statet &state)
pop_frame(state);
}

/// preserves locality of local variables of a given function by applying L1
/// renaming to the local identifiers
/// Preserves locality of parameters of a given function by applying L1
/// renaming to them.
static void locality(
const irep_idt &function_identifier,
goto_symext::statet &state,
path_storaget &path_storage,
const goto_functionst::goto_functiont &goto_function,
const namespacet &ns)
{
unsigned &frame_nr=
state.threads[state.source.thread_nr].function_frame[function_identifier];
frame_nr++;

std::set<irep_idt> local_identifiers;

get_local_identifiers(goto_function, local_identifiers);

framet &frame = state.call_stack().top();

for(std::set<irep_idt>::const_iterator
it=local_identifiers.begin();
it!=local_identifiers.end();
it++)
for(const auto &param : goto_function.parameter_identifiers)
{
// get L0 name
ssa_exprt ssa =
state.rename_ssa<L0>(ssa_exprt{ns.lookup(*it).symbol_expr()}, ns);
const irep_idt l0_name=ssa.get_identifier();

// save old L1 name for popping the frame
auto c_it = state.level1.current_names.find(l0_name);

if(c_it != state.level1.current_names.end())
{
frame.old_level1.emplace(l0_name, c_it->second);
c_it->second = std::make_pair(ssa, frame_nr);
}
else
{
c_it = state.level1.current_names
.emplace(l0_name, std::make_pair(ssa, frame_nr))
.first;
}

// do L1 renaming -- these need not be unique, as
// identifiers may be shared among functions
// (e.g., due to inlining or other code restructuring)

ssa_exprt ssa_l1 = state.rename_ssa<L1>(std::move(ssa), ns);

irep_idt l1_name = ssa_l1.get_identifier();
unsigned offset=0;

while(state.l1_history.find(l1_name)!=state.l1_history.end())
{
symex_renaming_levelt::increase_counter(c_it);
++offset;
ssa_l1.set_level_1(frame_nr + offset);
l1_name = ssa_l1.get_identifier();
}
state.rename_ssa<L0>(ssa_exprt{ns.lookup(param).symbol_expr()}, ns);

// now unique -- store
frame.local_objects.insert(l1_name);
state.l1_history.insert(l1_name);
const std::size_t fresh_l1_index =
path_storage.get_unique_index(ssa.get_identifier(), frame_nr);
state.add_object(ssa, fresh_l1_index, ns);
}
}
4 changes: 3 additions & 1 deletion src/goto-symex/symex_start_thread.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -66,6 +66,9 @@ void goto_symext::symex_start_thread(statet &state)

// get L0 name for current thread
lhs.set_level_0(t);
const irep_idt &l0_name = lhs.get_identifier();
std::size_t l1_index = path_storage.get_unique_index(l0_name, 0);
CHECK_RETURN(l1_index == 0);

// set up L1 name
auto emplace_result = state.level1.current_names.emplace(
Expand All @@ -76,7 +79,6 @@ void goto_symext::symex_start_thread(statet &state)
const ssa_exprt lhs_l1 = state.rename_ssa<L1>(std::move(lhs), ns);
const irep_idt l1_name = lhs_l1.get_l1_object_identifier();
// store it
state.l1_history.insert(l1_name);
new_thread.call_stack.back().local_objects.insert(l1_name);

// make copy
Expand Down