From 19e5bba532b051adc52336daaefa2d5e62ddafcd Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 21 Mar 2018 11:36:33 +0000 Subject: [PATCH] Document synthetic methods generated by the Java frontend --- src/java_bytecode/java_bytecode_language.h | 4 ++++ src/java_bytecode/synthetic_methods_map.h | 21 ++++++++++++++++++++- 2 files changed, 24 insertions(+), 1 deletion(-) diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index dc708eef744..e1f78f52212 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/src/java_bytecode/java_bytecode_language.h @@ -172,6 +172,10 @@ class java_bytecode_languaget:public languaget private: const std::unique_ptr pointer_type_selector; + + /// Maps synthetic method names on to the particular type of synthetic method + /// (static initializer, initializer wrapper, etc). For full documentation see + /// synthetic_method_map.h synthetic_methods_mapt synthetic_methods; stub_global_initializer_factoryt stub_global_initializer_factory; class_hierarchyt class_hierarchy; diff --git a/src/java_bytecode/synthetic_methods_map.h b/src/java_bytecode/synthetic_methods_map.h index 86f12e2506b..2fe258524f1 100644 --- a/src/java_bytecode/synthetic_methods_map.h +++ b/src/java_bytecode/synthetic_methods_map.h @@ -1,6 +1,6 @@ /*******************************************************************\ -Module: Java Static Initializers +Module: Synthetic methods map Author: Chris Smowton, chris.smowton@diffblue.com @@ -9,12 +9,31 @@ Author: Chris Smowton, chris.smowton@diffblue.com #ifndef CPROVER_JAVA_BYTECODE_SYNTHETIC_METHODS_MAP_H #define CPROVER_JAVA_BYTECODE_SYNTHETIC_METHODS_MAP_H +/// \file +/// Synthetic methods are particular methods internally generated by the +/// Java frontend, including thunks to ensure static initializers are run once +/// and initializers created for unknown / stub types. Compare normal methods, +/// which are translated from Java bytecode. This file provides an +/// enumeration specifying the kind of a particular synthetic method and a +/// common type of a map giving a collection of synthetic methods. +/// Functions stubs and array.clone() functions are also generated by the Java +/// frontend but are not recorded using this framework, but may be in future. + +/// Synthetic method kinds. enum class synthetic_method_typet { + /// A static initializer wrapper + /// (code of the form `if(!already_run) clinit(); already_run = true;`) + /// These are generated for both user and stub types, to ensure the actual + /// static initializer is only run once on any given path. STATIC_INITIALIZER_WRAPPER, + /// A generated (synthetic) static initializer function for a stub type. + /// Because we don't have the bytecode for a stub type (by definition), we + /// generate a static initializer function to initialize its static fields. STUB_CLASS_STATIC_INITIALIZER }; +/// Maps method names on to a synthetic method kind. typedef std::unordered_map synthetic_methods_mapt;