Loading...

Searching...

No Matches

java_enum_static_init_unwind_handler.cpp File Reference

Unwind loops in static initializers. More...

#include "java_enum_static_init_unwind_handler.h"
#include <util/invariant.h>
#include <util/ssa_expr.h>
#include <util/suffix.h>
#include <goto-symex/call_stack.h>
#include "java_utils.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).

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.

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 32 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 70 of file java_enum_static_init_unwind_handler.cpp.