From f325b512138163daba0b27deb7b1c54969594cdf Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Fri, 22 Jul 2016 16:49:50 +0200 Subject: [PATCH 1/2] Java API: In fromInt() methods of enums fail on invalid value. The existing code just returns one of the enum values if an unknown int value is passed, silently hiding bugs. --- scripts/mk_genfile_common.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index b8d6ac5e1..51d68f56c 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -345,7 +345,7 @@ def mk_z3consts_java_internal(api_files, package_name, output_dir): efile.write(' public static final %s fromInt(int v) {\n' % name) efile.write(' for (%s k: values()) \n' % name) efile.write(' if (k.intValue == v) return k;\n') - efile.write(' return values()[0];\n') + efile.write(' throw new IllegalArgumentException("Illegal value " + v + " for %s");\n' % name) efile.write(' }\n\n') efile.write(' public final int toInt() { return this.intValue; }\n') # efile.write(';\n %s(int v) {}\n' % name) From c3b8c15f35d1b2996517e8c2097d71996ab8e667 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Fri, 22 Jul 2016 17:28:40 +0200 Subject: [PATCH 2/2] Java API: Make enum lookup more efficient. The existing code causes an allocation of an array with all enum values on every method call (inside the values() method), and loops over all enum entries. --- scripts/mk_genfile_common.py | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 51d68f56c..cbeb8a82d 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -323,6 +323,9 @@ def mk_z3consts_java_internal(api_files, package_name, output_dir): generated_enumeration_files.append(efile.name) efile.write('/**\n * Automatically generated file\n **/\n\n') efile.write('package %s.enumerations;\n\n' % package_name) + efile.write('import java.util.HashMap;\n') + efile.write('import java.util.Map;\n') + efile.write('\n') efile.write('/**\n') efile.write(' * %s\n' % name) @@ -342,9 +345,18 @@ def mk_z3consts_java_internal(api_files, package_name, output_dir): efile.write(' %s(int v) {\n' % name) efile.write(' this.intValue = v;\n') efile.write(' }\n\n') + efile.write(' // Cannot initialize map in constructor, so need to do it lazily.\n') + efile.write(' // Easiest thread-safe way is the initialization-on-demand holder pattern.\n') + efile.write(' private static class %s_MappingHolder {\n' % name) + efile.write(' private static final Map intMapping = new HashMap<>();\n' % name) + efile.write(' static {\n') + efile.write(' for (%s k : %s.values())\n' % (name, name)) + efile.write(' intMapping.put(k.toInt(), k);\n') + efile.write(' }\n') + efile.write(' }\n\n') efile.write(' public static final %s fromInt(int v) {\n' % name) - efile.write(' for (%s k: values()) \n' % name) - efile.write(' if (k.intValue == v) return k;\n') + efile.write(' %s k = %s_MappingHolder.intMapping.get(v);\n' % (name, name)) + efile.write(' if (k != null) return k;\n') efile.write(' throw new IllegalArgumentException("Illegal value " + v + " for %s");\n' % name) efile.write(' }\n\n') efile.write(' public final int toInt() { return this.intValue; }\n')