From 233700390b9fe2d5e5cb8988163c3b22c416788f Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 19 Mar 2019 12:02:07 +0000 Subject: [PATCH 1/2] StringToLowerCase: Reduce string length limit The string solver was consuming a very large amount of memory with the limit set to 10000; this appears to be pure chance whether the solver picks a solution requiring universals to be instantiated a large number of times. The other tests in this directory are already set to limit string length to 1000, so I just do the same thing here. --- .../jbmc-strings/StringToLowerCase/test_dependency.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jbmc/regression/jbmc-strings/StringToLowerCase/test_dependency.desc b/jbmc/regression/jbmc-strings/StringToLowerCase/test_dependency.desc index 2ec32e7ce9..b93fb7882c 100644 --- a/jbmc/regression/jbmc-strings/StringToLowerCase/test_dependency.desc +++ b/jbmc/regression/jbmc-strings/StringToLowerCase/test_dependency.desc @@ -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 From d201bad22dbd47e01e6f04ca77ddfcc6028f31c0 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 19 Mar 2019 12:27:31 +0000 Subject: [PATCH 2/2] Always use L2 generation 0 for dead variables This means that merge_goto's special merge logic for generation zero works on both dead local variables and on #return_value global variables defined for the second and subsequent times, discounting the control-flow where the variable is dead. --- .../jbmc/throwing-function-return-value/test.desc | 5 +++++ src/goto-symex/goto_symex_state.cpp | 13 ------------- src/goto-symex/goto_symex_state.h | 10 ++++++---- src/goto-symex/symex_dead.cpp | 9 ++++++--- 4 files changed, 17 insertions(+), 20 deletions(-) diff --git a/jbmc/regression/jbmc/throwing-function-return-value/test.desc b/jbmc/regression/jbmc/throwing-function-return-value/test.desc index 4246e18eff..4bebe0b119 100644 --- a/jbmc/regression/jbmc/throwing-function-return-value/test.desc +++ b/jbmc/regression/jbmc/throwing-function-return-value/test.desc @@ -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 @@ -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). diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 772256dd63..09f0d87f9a 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -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 diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index 9fb65bf5bc..ab0ec52a1a 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -223,16 +223,18 @@ public: 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); + } + std::function get_l2_name_provider() const { return fresh_l2_name_provider; diff --git a/src/goto-symex/symex_dead.cpp b/src/goto-symex/symex_dead.cpp index 898dd28027..f06b3b0167 100644 --- a/src/goto-symex/symex_dead.cpp +++ b/src/goto-symex/symex_dead.cpp @@ -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); }