From c7ad88561f02fc779b0f2da05d69002f73d19b77 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 1 Feb 2019 17:31:29 +0000 Subject: [PATCH 1/3] Java frontend: get qualified generic types of static fields Before it would unintentionally erase SomeClass.field from A to just the unqualified A type. --- .../java_bytecode_convert_method.cpp | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index d93cc7fb1c2..a51541455e0 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -1529,12 +1529,10 @@ code_blockt java_bytecode_convert_methodt::convert_instructions( const bool is_assertions_disabled_field= field_name.find("$assertionsDisabled")!=std::string::npos; + const irep_idt field_id( + get_static_field(arg0.get_string(ID_class), field_name)); const symbol_exprt symbol_expr( - get_static_field(arg0.get_string(ID_class), field_name), arg0.type()); - - INVARIANT( - symbol_table.has_symbol(symbol_expr.get_identifier()), - "getstatic symbol should have been created before method conversion"); + symbol_table.lookup_ref(field_id).symbol_expr()); convert_getstatic( arg0, symbol_expr, is_assertions_disabled_field, c, results); @@ -1549,12 +1547,10 @@ code_blockt java_bytecode_convert_methodt::convert_instructions( PRECONDITION(op.size() == 1 && results.empty()); const auto &field_name=arg0.get_string(ID_component_name); + const irep_idt field_id( + get_static_field(arg0.get_string(ID_class), field_name)); const symbol_exprt symbol_expr( - get_static_field(arg0.get_string(ID_class), field_name), arg0.type()); - - INVARIANT( - symbol_table.has_symbol(symbol_expr.get_identifier()), - "putstatic symbol should have been created before method conversion"); + symbol_table.lookup_ref(field_id).symbol_expr()); c = convert_putstatic(i_it->source_location, arg0, op, symbol_expr); } From a208cce75f4a8a72ad7138d879c8e6317c62b051 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 12 Feb 2019 12:17:32 +0000 Subject: [PATCH 2/3] Add test for generic static field type consistency --- .../jbmc/generic_static_field/Test.class | Bin 0 -> 528 bytes .../jbmc/generic_static_field/Test.java | 12 ++++++++++++ .../jbmc/generic_static_field/test.desc | 15 +++++++++++++++ 3 files changed, 27 insertions(+) create mode 100644 jbmc/regression/jbmc/generic_static_field/Test.class create mode 100644 jbmc/regression/jbmc/generic_static_field/Test.java create mode 100644 jbmc/regression/jbmc/generic_static_field/test.desc diff --git a/jbmc/regression/jbmc/generic_static_field/Test.class b/jbmc/regression/jbmc/generic_static_field/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..b40e9fc5e63799a993498af583007d1fd1bf9ec4 GIT binary patch literal 528 zcmZ`$%TB^T6g@-BqooR>;saf{D=uW?N(hNDF)?X$LBrNe%UFk$V%ovPzfw0QF8lyL z%6NxDlo%ItALpKX=gghYulElCr)b$Qv17r&ZW()J>@zr-;!1|McT&V7hLY!tOm!Ko zfs7KaW~pFk&B2~G=8wD+^CaqAB}zmh?e>XT>d8c^K7--5hYaS$bVNNhPbT7eHVH)P z^B^Xq;Y~vx4|ytez5q>iFEfVbYVGM^S+C|-`~LhYQ;|4^irZewJY0nTiF14Y*)QEU z!B~W<+y4tO*n{aT4aKF@VlBOf6a8QZ7HkJal;~|5WvKrwA|Hq&TB%7Zrbf*qU#6^p z3LTBvWUGXnlV{|M$8TUS6c}*G>IO|;BkSY@tP={ { + + public static Test static_field; + + public static Test test() { + + return static_field; + + } + +} diff --git a/jbmc/regression/jbmc/generic_static_field/test.desc b/jbmc/regression/jbmc/generic_static_field/test.desc new file mode 100644 index 00000000000..f341a759e93 --- /dev/null +++ b/jbmc/regression/jbmc/generic_static_field/test.desc @@ -0,0 +1,15 @@ +CORE +Test.class +--function Test.test --validate-goto-model --show-goto-functions +^EXIT=0$ +^SIGNAL=0$ +Test\.test:\(\)LTest;#return_value = static_field; +-- +^warning: ignoring +-- +This checks that the return value type matches the static field -- if it didn't, +either --validate-goto-model would throw because of a mismatching assignment, or +a cast would be used to adjust the type. + +The original motivation for this test was that generic field references could +accidentally omit generic arguments that were present in function types. From 35213c49f35691285d2af9771da5c9e2de0cd8ba Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 12 Feb 2019 13:58:47 +0000 Subject: [PATCH 3/3] Comment that static field symbols should exist Avoid the suggestion that `get_static_field` might be expected to create them -- it doesn't, java_bytecode_convert_class does and we should be able to safely assume they exist during convert_method. --- jbmc/src/java_bytecode/java_bytecode_convert_method.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index a51541455e0..4c375214507 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -1531,6 +1531,8 @@ code_blockt java_bytecode_convert_methodt::convert_instructions( const irep_idt field_id( get_static_field(arg0.get_string(ID_class), field_name)); + + // Symbol should have been populated by java_bytecode_convert_class: const symbol_exprt symbol_expr( symbol_table.lookup_ref(field_id).symbol_expr()); @@ -1549,6 +1551,8 @@ code_blockt java_bytecode_convert_methodt::convert_instructions( const irep_idt field_id( get_static_field(arg0.get_string(ID_class), field_name)); + + // Symbol should have been populated by java_bytecode_convert_class: const symbol_exprt symbol_expr( symbol_table.lookup_ref(field_id).symbol_expr());