java_enum_static_init_unwind_handler.cpp File Reference

#include "java_enum_static_init_unwind_handler.h"
#include "java_utils.h"
#include <util/invariant.h>
#include <util/ssa_expr.h>
#include <util/suffix.h>
#include <goto-symex/call_stack.h>

Include dependency graph for java_enum_static_init_unwind_handler.cpp:

Go to the source code of this file.

Functions
static irep_idt	find_enum_function_on_stack (const call_stackt &context)
	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). More...
tvt	java_enum_static_init_unwind_handler (const call_stackt &context, unsigned loop_number, unsigned unwind_count, unsigned &unwind_max, const symbol_tablet &symbol_table)
	Unwind handler that special-cases the clinit (static initializer) functions of enumeration classes, and VALUES array cloning in their values() methods. More...

Detailed Description

Unwind loops in static initializers

Definition in file java_enum_static_init_unwind_handler.cpp.

Function Documentation

find_enum_function_on_stack()

static irep_idt find_enum_function_on_stack ( const call_stackt &  context )

static

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

  Parameters

  context

  the current call stack

  Returns

  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.

Definition at line 31 of file java_enum_static_init_unwind_handler.cpp.

java_enum_static_init_unwind_handler()

tvt java_enum_static_init_unwind_handler	(	const call_stackt &	context,
		unsigned	loop_number,
		unsigned	unwind_count,
		unsigned &	unwind_max,
		const symbol_tablet &	symbol_table
	)

Unwind handler that special-cases the clinit (static initializer) functions 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 / copying of the enumeration's value array.

Parameters

	context	call stack when the loop back-edge was taken
	loop_number	ordinal number of the loop (ignored)
	unwind_count	iteration count that is about to begin
[out]	unwind_max	may be set to an advisory (unenforced) maximum when we know the total iteration count
	symbol_table	global symbol table

Returns

false if loop_id belongs to an enumeration's static initializer and unwind_count is <= the enumeration size, or unknown (defer / no decision) otherwise.

Definition at line 69 of file java_enum_static_init_unwind_handler.cpp.