-
Notifications
You must be signed in to change notification settings - Fork 274
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
Changes from all commits
714de0d
6270968
361469b
a985eae
c9a53f9
4f158a3
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
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; | ||
} | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
package com.diffblue.regression; | ||
|
||
enum MyEnum { | ||
A, B, C, D; | ||
} |
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$ | ||
-- |
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 ; | ||
} | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
package com.diffblue.regression; | ||
|
||
enum MyEnum { | ||
A, B, C, D; | ||
} |
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$ | ||
-- |
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(); | ||
} | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
package com.diffblue.regression; | ||
|
||
enum MyEnum { | ||
A, B, C, D; | ||
} |
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$ | ||
-- |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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 ¤t_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) | ||
return clone_caller; | ||
else | ||
return irep_idt(); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. maybe better use an |
||
} | ||
else if(has_suffix(id2string(current_function), ".<clinit>:()V")) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. how do we know this is an enum's There was a problem hiding this comment. Choose a reason for hiding this commentThe 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 | ||
|
@@ -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"); | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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, | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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> | ||
|
@@ -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()) | ||
{ | ||
|
There was a problem hiding this comment.
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 ?