From 26f0976f72a25f0e2a26f326870d396e4e7b5c18 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Sun, 5 Feb 2017 13:25:23 +0100 Subject: [PATCH] ignore non-Java files in enum static init unwind To correctly unwind static inits of Java enums, one first has to check whether the function is actually a Java function. This patch also adds a first regression test for static loop unwinding. Fixes: b49a7fc3a32bcc3e883c81ee4bec6f085a074bfa --- regression/cbmc-java/enum1/enum1.class | Bin 0 -> 1399 bytes regression/cbmc-java/enum1/enum1.java | 16 ++++++++++ regression/cbmc-java/enum1/test.desc | 8 +++++ src/cbmc/cbmc_parse_options.cpp | 2 ++ .../remove_static_init_loops.cpp | 30 ++++++++---------- 5 files changed, 40 insertions(+), 16 deletions(-) create mode 100644 regression/cbmc-java/enum1/enum1.class create mode 100644 regression/cbmc-java/enum1/enum1.java create mode 100644 regression/cbmc-java/enum1/test.desc diff --git a/regression/cbmc-java/enum1/enum1.class b/regression/cbmc-java/enum1/enum1.class new file mode 100644 index 0000000000000000000000000000000000000000..25433918f32a04d37d06b547950c54302a0bb0b0 GIT binary patch literal 1399 zcmZuxT~iZh6n@_9Cc9ae5Cd2O5&S?+LXm>f))Fa*_)#NhS7}qPmat{khK=29nCX2l zde8E% zSCY7jYZk8K3j;R<^!26kjDS)0g68(jd|NTwX6M@Me4EYDYl7Z)R~!NJUMFB+!fiCX zF!Jj`ESt76gvG$L)GyT_EZBTY(!jLuS?TQloFXejp?6 zy(cs6eNN<7zq{!^P`wazj##SJ4hm&^f>wxA>7bVd;$=DYW?1#E_;LhGp?Fp{Z{wKU z-fnDos3O`G?fRFvTKgF?~?v8Z|NMM_PP+TQDCXGs(x_aOf$Lm3>%$ z%RDjFWJ;y)BP=Nb(~pm6F(Ljz*1!y(W|_M^>P!0QwEmLO_i*SD4E-^5Z5QTK=#`AE z?W1oODJAslN=Pf=a9jx)B@85#FsOtfLkWiY7c*!rq@0T0LfWasTgW(-L<@sX#bD>o zF2oZYxlw#p(k|vkf5l)iH@n)x2UB|({xK#V|NE*t(HIPN$&=z_x5;<7h@Uvg&*Tqb esR`52?M3kh-y6_`c#R>V(MIwdKeQ5?x&Hv{^%LX( literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/enum1/enum1.java b/regression/cbmc-java/enum1/enum1.java new file mode 100644 index 00000000000..40838ccdc0d --- /dev/null +++ b/regression/cbmc-java/enum1/enum1.java @@ -0,0 +1,16 @@ +public enum enum1 +{ + VAL1, VAL2, VAL3, VAL4, VAL5; + static + { + for(enum1 e : enum1.values()) + { + System.out.println(e); + } + } + public static void main(String[] args) + { + enum1 e=VAL5; + assert(e==VAL5); + } +} diff --git a/regression/cbmc-java/enum1/test.desc b/regression/cbmc-java/enum1/test.desc new file mode 100644 index 00000000000..8a395386017 --- /dev/null +++ b/regression/cbmc-java/enum1/test.desc @@ -0,0 +1,8 @@ +CORE +enum1.class +--java-unwind-enum-static --unwind 3 +^EXIT=10$ +^SIGNAL=0$ +^Unwinding loop java::enum1.:()V.0 iteration 5 (6 max) file enum1.java line 6 function java::enum1.:()V bytecode_index 78 thread 0$ +-- +^warning: ignoring diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index d09b544c678..4d839835824 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -550,6 +550,8 @@ int cbmc_parse_optionst::doit() if(set_properties(goto_functions)) return 7; // should contemplate EX_USAGE from sysexits.h + // unwinds loops to number of enum elements + // side effect: add this as explicit unwind to unwind set if(options.get_bool_option("java-unwind-enum-static")) remove_static_init_loops(symbol_table, goto_functions, options); diff --git a/src/goto-programs/remove_static_init_loops.cpp b/src/goto-programs/remove_static_init_loops.cpp index 25d48ccf654..f1084d6ca53 100644 --- a/src/goto-programs/remove_static_init_loops.cpp +++ b/src/goto-programs/remove_static_init_loops.cpp @@ -7,6 +7,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include +#include #include #include "remove_static_init_loops.h" @@ -56,6 +57,10 @@ void remove_static_init_loopst::unwind_enum_static( const std::string java_clinit=":()V"; const std::string &fname=id2string(ins.function); size_t class_prefix_length=fname.find_last_of('.'); + // is Java function and static init? + const symbolt &function_name=symbol_table.lookup(ins.function); + if(!(function_name.mode==ID_java && has_suffix(fname, java_clinit))) + continue; assert( class_prefix_length!=std::string::npos && "could not identify class name"); @@ -65,23 +70,16 @@ void remove_static_init_loopst::unwind_enum_static( size_t unwinds=class_type.get_size_t(ID_java_enum_static_unwind); unwind_max=std::max(unwind_max, unwinds); - if(fname.length()>java_clinit.length()) + if(unwinds>0) { - // extend unwindset with unwinds for of enum - if(fname.compare( - fname.length()-java_clinit.length(), - java_clinit.length(), - java_clinit)==0 && unwinds>0) - { - const std::string &set=options.get_option("unwindset"); - std::string newset; - if(set!="") - newset=","; - newset+= - id2string(ins.function)+"."+std::to_string(loop_id)+":"+ - std::to_string(unwinds); - options.set_option("unwindset", set+newset); - } + const std::string &set=options.get_option("unwindset"); + std::string newset; + if(set!="") + newset=","; + newset+= + id2string(ins.function)+"."+std::to_string(loop_id)+":"+ + std::to_string(unwinds); + options.set_option("unwindset", set+newset); } } }