Skip to content

Unroll enumeration values() loops #2651

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
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
Binary file not shown.
Binary file not shown.
16 changes: 16 additions & 0 deletions jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
package com.diffblue.regression;

public class Foo {
public int foo(MyEnum e) {
if (e == null) return 0;
switch (e) {
case A:
return 1;
case B:
return 2;
case C:
return 3;
}
return 5;
}
}
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
package com.diffblue.regression;

enum MyEnum {
A, B, C, D;
}
10 changes: 10 additions & 0 deletions jbmc/regression/jbmc/enum_switch/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE symex-driven-lazy-loading-expected-failure
com/diffblue/regression/Foo.class
--trace --cover location --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 10 --function "com.diffblue.regression.Foo.foo" --java-unwind-enum-static
line 8.*SATISFIED
line 10.*SATISFIED
line 12.*SATISFIED
line 14.*SATISFIED
^EXIT=0$
^SIGNAL=0$
--
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
package com.diffblue.regression;
public class EnumIter {
int f() {
MyEnum[] a = MyEnum.values();
int num = a[2].ordinal() + a[3].ordinal();
return num ;
}
}
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
package com.diffblue.regression;

enum MyEnum {
A, B, C, D;
}
7 changes: 7 additions & 0 deletions jbmc/regression/jbmc/enum_values_clone/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
CORE symex-driven-lazy-loading-expected-failure
com/diffblue/regression/EnumIter.class
--trace --cover location --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static
\d+ of \d+ covered \(100\.0%\)
^EXIT=0$
^SIGNAL=0$
--
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
package com.diffblue.regression;
public class EnumIter {
String f() {
MyEnum[] a = MyEnum.values();
return a[2].name() + a[3].name();
}
}
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
package com.diffblue.regression;

enum MyEnum {
A, B, C, D;
}
7 changes: 7 additions & 0 deletions jbmc/regression/jbmc/enum_values_clone_name/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
CORE symex-driven-lazy-loading-expected-failure
com/diffblue/regression/EnumIter.class
--trace --cover location --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static
\d+ of \d+ covered \(100\.0%\)
^EXIT=0$
^SIGNAL=0$
--
7 changes: 5 additions & 2 deletions jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1959,9 +1959,12 @@ codet java_bytecode_convert_methodt::convert_switch(
mp_integer number;
bool ret = to_integer(to_constant_expr(*a_it), number);
DATA_INVARIANT(!ret, "case label expected to be integer");
// The switch case does not contain any code, it just branches via a GOTO
// to the jump target of the tableswitch/lookupswitch case at
// hand. Therefore we consider this code to belong to the source bytecode
// instruction and not the target instruction.
code_case.code() = code_gotot(label(integer2string(number)));
code_case.code().add_source_location() =
address_map.at(integer2unsigned(number)).source->source_location;
code_case.code().add_source_location() = location;

if(a_it == args.begin())
code_case.set_default();
Expand Down
49 changes: 42 additions & 7 deletions jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -14,12 +14,47 @@ Author: Chris Smowton, [email protected]
#include <util/invariant.h>
#include <util/suffix.h>

/// Check if we may be in a function that loops over the cases of an
/// enumeration (note we return a candidate function that matches a pattern;
/// our caller must verify it really belongs to an enumeration).
/// At the moment we know of two cases that definitely do so:
/// * An enumeration type's static initialiser
/// * The array[reference].clone() method when called from an enumeration type's
/// 'values()' method
/// \param context: the current call stack
/// \return the name of an enclosing function that may be defined on the
/// relevant enum type, or an empty string if we don't find one.
static irep_idt
find_enum_function_on_stack(const goto_symex_statet::call_stackt &context)
{
static irep_idt reference_array_clone_id =
"java::array[reference].clone:()Ljava/lang/Object;";

PRECONDITION(!context.empty());
const irep_idt &current_function = context.back().function_identifier;

if(context.size() >= 2 && current_function == reference_array_clone_id)
{
const irep_idt &clone_caller =
context.at(context.size() - 2).function_identifier;
if(id2string(clone_caller).find(".values:()[L") != std::string::npos)
Copy link
Contributor

Choose a reason for hiding this comment

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

are we sure that it will always be for an enum type's .values method ?

return clone_caller;
else
return irep_idt();
Copy link
Contributor

Choose a reason for hiding this comment

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

maybe better use an optionalt<irep_idt> as return value

}
else if(has_suffix(id2string(current_function), ".<clinit>:()V"))
Copy link
Contributor

Choose a reason for hiding this comment

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

how do we know this is an enum's <clinit> ?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

We don't -- this function returns a candidate, which its caller checks further.

return current_function;
else
return irep_idt();
}

/// Unwind handler that special-cases the clinit (static initializer) functions
/// of enumeration classes. When java_bytecode_convert_classt has annotated them
/// of enumeration classes, and VALUES array cloning in their values() methods.
/// When java_bytecode_convert_classt has annotated them
/// with a size of the enumeration type, this forces unwinding of any loop in
/// the static initializer to at least that many iterations, with intent to
/// permit population of the enumeration's value array.
/// \param function_id: function the loop is in
/// permit population / copying of the enumeration's value array.
/// \param context: call stack when the loop back-edge was taken
/// \param loop_number: ordinal number of the loop (ignored)
/// \param unwind_count: iteration count that is about to begin
/// \param [out] unwind_max: may be set to an advisory (unenforced) maximum when
Expand All @@ -29,17 +64,17 @@ Author: Chris Smowton, [email protected]
/// unwind_count is <= the enumeration size, or unknown (defer / no decision)
/// otherwise.
tvt java_enum_static_init_unwind_handler(
const irep_idt &function_id,
const goto_symex_statet::call_stackt &context,
unsigned loop_number,
unsigned unwind_count,
unsigned &unwind_max,
const symbol_tablet &symbol_table)
{
const std::string &function_str = id2string(function_id);
if(!has_suffix(function_str, ".<clinit>:()V"))
const irep_idt enum_function_id = find_enum_function_on_stack(context);
if(enum_function_id.empty())
return tvt::unknown();

const symbolt &function_symbol = symbol_table.lookup_ref(function_str);
const symbolt &function_symbol = symbol_table.lookup_ref(enum_function_id);
irep_idt class_id = function_symbol.type.get(ID_C_class);
INVARIANT(
!class_id.empty(), "functions should have their defining class annotated");
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -12,11 +12,13 @@ Author: Chris Smowton, [email protected]
#ifndef CPROVER_JAVA_BYTECODE_JAVA_ENUM_STATIC_INIT_UNWIND_HANDLER_H
#define CPROVER_JAVA_BYTECODE_JAVA_ENUM_STATIC_INIT_UNWIND_HANDLER_H

#include <goto-symex/goto_symex_state.h>

#include <util/symbol_table.h>
#include <util/threeval.h>

tvt java_enum_static_init_unwind_handler(
const irep_idt &function_id,
const goto_symex_statet::call_stackt &context,
unsigned loop_number,
unsigned unwind_count,
unsigned &unwind_max,
Expand Down
8 changes: 2 additions & 6 deletions jbmc/src/jbmc/jbmc_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -479,16 +479,12 @@ int jbmc_parse_optionst::doit()
configure_bmc = [](bmct &bmc, const symbol_tablet &symbol_table) {
bmc.add_loop_unwind_handler(
[&symbol_table](
const irep_idt &function_id,
const goto_symex_statet::call_stackt &context,
unsigned loop_number,
unsigned unwind,
unsigned &max_unwind) {
return java_enum_static_init_unwind_handler(
function_id,
loop_number,
unwind,
max_unwind,
symbol_table);
context, loop_number, unwind, max_unwind, symbol_table);
});
};
}
Expand Down
7 changes: 2 additions & 5 deletions src/cbmc/symex_bmc.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -106,6 +106,7 @@ void symex_bmct::merge_goto(

bool symex_bmct::get_unwind(
const symex_targett::sourcet &source,
const goto_symex_statet::call_stackt &context,
unsigned unwind)
{
const irep_idt id=goto_programt::loop_id(*source.pc);
Expand All @@ -116,11 +117,7 @@ bool symex_bmct::get_unwind(
for(auto handler : loop_unwind_handlers)
{
abort_unwind_decision =
handler(
source.pc->function,
source.pc->loop_number,
unwind,
this_loop_limit);
handler(context, source.pc->loop_number, unwind, this_loop_limit);
if(abort_unwind_decision.is_known())
break;
}
Expand Down
16 changes: 9 additions & 7 deletions src/cbmc/symex_bmc.h
Original file line number Diff line number Diff line change
Expand Up @@ -35,14 +35,15 @@ class symex_bmct: public goto_symext
// To show progress
source_locationt last_source_location;

/// Loop unwind handlers take the function ID and loop number, the unwind
/// count so far, and an out-parameter specifying an advisory maximum, which
/// they may set. If set the advisory maximum is set it is *only* used to
/// print useful information for the user (e.g. "unwinding iteration N, max
/// M"), and is not enforced. They return true to halt unwinding, false to
/// authorise unwinding, or Unknown to indicate they have no opinion.
/// Loop unwind handlers take the call stack, loop number, the unwind count so
/// far, and an out-parameter specifying an advisory maximum, which they may
/// set. If set the advisory maximum is set it is *only* used to print useful
/// information for the user (e.g. "unwinding iteration N, max M"), and is not
/// enforced. They return true to halt unwinding, false to authorise
/// unwinding, or Unknown to indicate they have no opinion.
typedef
std::function<tvt(const irep_idt &, unsigned, unsigned, unsigned &)>
std::function<tvt(
const goto_symex_statet::call_stackt &, unsigned, unsigned, unsigned &)>
loop_unwind_handlert;

/// Recursion unwind handlers take the function ID, the unwind count so far,
Expand Down Expand Up @@ -105,6 +106,7 @@ class symex_bmct: public goto_symext
// for loop unwinding
virtual bool get_unwind(
const symex_targett::sourcet &source,
const goto_symex_statet::call_stackt &context,
unsigned unwind);

virtual bool get_unwind_recursion(
Expand Down
69 changes: 28 additions & 41 deletions src/goto-programs/interpreter_evaluate.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
#include <util/fixedbv.h>
#include <util/ieee_float.h>
#include <util/pointer_offset_size.h>
#include <util/simplify_expr.h>
#include <util/string_container.h>

#include <langapi/language_util.h>
Expand Down Expand Up @@ -894,52 +895,38 @@ void interpretert::evaluate(
mp_integer address=evaluate_address(
expr,
true); // fail quietly
if(address.is_zero() && expr.id()==ID_index)
if(address.is_zero())
{
// Try reading from a constant array:
mp_vectort idx;
evaluate(expr.op1(), idx);
if(idx.size()==1)
exprt simplified;
// In case of being an indexed access, try to evaluate the index, then
// simplify.
if(expr.id() == ID_index)
{
mp_integer read_from_index=idx[0];
if(expr.op0().id()==ID_array)
exprt evaluated_index = expr;
mp_vectort idx;
evaluate(expr.op1(), idx);
if(idx.size() == 1)
{
const auto &ops=expr.op0().operands();
DATA_INVARIANT(read_from_index.is_long(), "index is too large");
if(read_from_index>=0 && read_from_index<ops.size())
{
evaluate(ops[read_from_index.to_long()], dest);
if(dest.size()!=0)
return;
}
}
else if(expr.op0().id() == ID_array_list)
{
// This sort of construct comes from boolbv_get, but doesn't seem
// to have an exprt yet. Its operands are a list of key-value pairs.
const auto &ops=expr.op0().operands();
DATA_INVARIANT(
ops.size()%2==0,
"array-list has odd number of operands");
for(size_t listidx=0; listidx!=ops.size(); listidx+=2)
{
mp_vectort elem_idx;
evaluate(ops[listidx], elem_idx);
CHECK_RETURN(elem_idx.size()==1);
if(elem_idx[0]==read_from_index)
{
evaluate(ops[listidx+1], dest);
if(dest.size()!=0)
return;
else
break;
}
}
// If we fall out the end of this loop then the constant array-list
// didn't define an element matching the index we're looking for.
evaluated_index.op1() =
constant_exprt(integer2string(idx[0]), expr.op1().type());
}
simplified = simplify_expr(evaluated_index, ns);
}
else
{
// Try reading from a constant -- simplify_expr has all the relevant
// cases (index-of-constant-array, member-of-constant-struct and so on)
// Note we complain of a problem even if simplify did *something* but
// still left us with an unresolved index, member, etc.
simplified = simplify_expr(expr, ns);
}
if(simplified.id() == expr.id())
evaluate_address(expr); // Evaluate again to print error message.
else
{
evaluate(simplified, dest);
return;
}
evaluate_address(expr); // Evaluate again to print error message.
}
else if(!address.is_zero())
{
Expand Down
1 change: 1 addition & 0 deletions src/goto-symex/goto_symex.h
Original file line number Diff line number Diff line change
Expand Up @@ -328,6 +328,7 @@ class goto_symext
// with false we continue.
virtual bool get_unwind(
const symex_targett::sourcet &source,
const goto_symex_statet::call_stackt &context,
unsigned unwind);

virtual void loop_bound_exceeded(statet &, const exprt &guard);
Expand Down
3 changes: 2 additions & 1 deletion src/goto-symex/symex_goto.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@ void goto_symext::symex_goto(statet &state)
unwind++;

// continue unwinding?
if(get_unwind(state.source, unwind))
if(get_unwind(state.source, state.call_stack(), unwind))
{
// no!
loop_bound_exceeded(state, new_guard);
Expand Down Expand Up @@ -540,6 +540,7 @@ void goto_symext::loop_bound_exceeded(

bool goto_symext::get_unwind(
const symex_targett::sourcet &source,
const goto_symex_statet::call_stackt &context,
unsigned unwind)
{
// by default, we keep going
Expand Down