Skip to content

Symex code_deadt: always use L2 generation zero #4407

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
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
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
Test.class
--function Test.withDependency --max-nondet-string-length 10000
--function Test.withDependency --max-nondet-string-length 1000
^EXIT=10$
^SIGNAL=0$
assertion at file Test.java line 48 .*: SUCCESS
Expand Down
5 changes: 5 additions & 0 deletions jbmc/regression/jbmc/throwing-function-return-value/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,13 @@ Test.class
--function Test.main --show-vcc
java::Test\.main:\(Z\)V::14::t1!0@1#\d+ = address_of\(symex_dynamic::dynamic_object\d+\)
java::Test\.main:\(Z\)V::9::x!0@1#\d+ = 5 \+ java::Test\.main:\(Z\)V::9::x!0@1#\d+
java::Test\.g:\(\)I#return_value!0#[0-9]+ = 5
^EXIT=0$
^SIGNAL=0$
--
return_value!0#0
java::Sub\.g:\(\)
java::Test\.g:\(\)I#return_value!0#[0-9]+ = [^5]
--
This checks that when a function may throw, we can nonetheless constant-propagate
and populate the value-set for the normal-return path. In particular we don't
Expand All @@ -16,3 +18,6 @@ reading the return-value when not defined), nor do we expect to see any code
from the Sub class, which is not accessible and can only be reached when
constant propagation has lost information to the point we're not sure which type
virtual calls against Test may find.
The final check ensures there is no uncertainty about whether Test.g() may throw,
which would result in a nondet return-value (corresponding to the hypothetical
throwing path).
13 changes: 0 additions & 13 deletions src/goto-symex/goto_symex_state.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -459,19 +459,6 @@ bool goto_symex_statet::l2_thread_read_encoding(
return true;
}

/// Allocates a fresh L2 name for the given L1 identifier, and makes it the
/// latest generation on this path. Does nothing if there isn't an expression
/// keyed by the l1 identifier.
void goto_symex_statet::increase_generation_if_exists(const irep_idt identifier)
{
// If we can't find the name in the local scope, this is a no-op.
auto current_names_iter = level2.current_names.find(identifier);
if(current_names_iter == level2.current_names.end())
return;

current_names_iter->second.second = fresh_l2_name_provider(identifier);
}

goto_symex_statet::write_is_shared_resultt goto_symex_statet::write_is_shared(
const ssa_exprt &expr,
const namespacet &ns) const
Expand Down
10 changes: 6 additions & 4 deletions src/goto-symex/goto_symex_state.h
Original file line number Diff line number Diff line change
Expand Up @@ -223,16 +223,18 @@ class goto_symex_statet final : public goto_statet
l1_identifier, lhs, fresh_l2_name_provider);
}

/// Increases the generation of the L1 identifier. Does nothing if there
/// isn't an expression keyed by it.
void increase_generation_if_exists(const irep_idt identifier);

/// Drops an L1 name from the local L2 map
void drop_l1_name(symex_renaming_levelt::current_namest::const_iterator it)
{
level2.current_names.erase(it);
}

/// Drops an L1 name from the local L2 map
void drop_l1_name(const irep_idt &l1_identifier)
{
level2.current_names.erase(l1_identifier);
Copy link
Contributor

Choose a reason for hiding this comment

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

I would think these methods should belong to the symex_level2t class

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I'll keep it alongside its close cousin increase_generation for now; if we want to refactor we should do them together (I don't mind either way)

}

std::function<std::size_t(const irep_idt &)> get_l2_name_provider() const
{
return fresh_l2_name_provider;
Expand Down
9 changes: 6 additions & 3 deletions src/goto-symex/symex_dead.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,10 @@ void goto_symext::symex_dead(statet &state)
// can no longer appear
state.value_set.values.erase(l1_identifier);
state.propagation.erase(l1_identifier);
// increment the L2 index to ensure a merge on join points will propagate the
// value for branches that are still live
state.increase_generation_if_exists(l1_identifier);
// Remove from the local L2 renaming map; this means any reads from the dead
// identifier will use generation 0 (e.g. x!N@M#0, where N and M are positive
// integers), which is never defined by any write, and will be dropped by
// `goto_symext::merge_goto` on merging with branches where the identifier
// is still live.
state.drop_l1_name(l1_identifier);
}