[TG-2755] Fix nondet-static option for static initializers

jbmc/regression/jbmc/nondet-static/My.java

@@ -0,0 +1,238 @@
+public class My {
+  public static int val() { return 3; }
+
+  public static int p1;
+  public static int p2 = 1;
+  public static int p3;
+  static { p3 = 2; }
+  public static int p4 = val();
+  public static Integer p5 = new Integer(5);
+
+  public static final int pf1 = 1;
+  public static final int pf2;
+  static { pf2 = 2; }
+  public static final int pf3 = val();
+  public static final Integer pf4 = new Integer(4);
+
+  private static int pr1;
+  private static int pr2 = 1;
+  private static int pr3;
+  static { pr3 = 2; }
+  private static int pr4 = val();
+  private static Integer pr5 = new Integer(5);
+
+  private static final int prf1 = 1;
+  private static final int prf2;
+  static { prf2 = 2; }
+  private static final int prf3 = val();
+  private static final Integer prf4 = new Integer(4);
+
+  // for inner classes, the missing cases of the above fields do not compile
+  public class PInner {
+    public static final int pf1 = 1;
+
+    private static final int prf1 = 1;
+  }
+
+  public static class PSInner {
+    public static int p1;
+    public static int p2 = 1;
+    public static int p3;
+    static { p3 = 2; }
+    public static int p4 = val();
+    public static Integer p5 = new Integer(5);
+
+    public static final int pf1 = 1;
+    public static final int pf2;
+    static { pf2 = 2; }
+    public static final int pf3 = val();
+    public static final Integer pf4 = new Integer(4);
+
+    private static int pr1;
+    private static int pr2 = 1;
+    private static int pr3;
+    static { pr3 = 2; }
+    private static int pr4 = val();
+    private static Integer pr5 = new Integer(5);
+
+    private static final int prf1 = 1;
+    private static final int prf2;
+    static { prf2 = 2; }
+    private static final int prf3 = val();
+    private static final Integer prf4 = new Integer(4);
+  }
+
+  private class PrInner {
+    public static final int pf1 = 1;
+
+    private static final int prf1 = 1;
+  }
+
+  private static class PrSInner {
+    public static int p1;
+    public static int p2 = 1;
+    public static int p3;
+    static { p3 = 2; }
+    public static int p4 = val();
+    public static Integer p5 = new Integer(5);
+
+    public static final int pf1 = 1;
+    public static final int pf2;
+    static { pf2 = 2; }
+    public static final int pf3 = val();
+    public static final Integer pf4 = new Integer(4);
+
+    private static int pr1;
+    private static int pr2 = 1;
+    private static int pr3;
+    static { pr3 = 2; }
+    private static int pr4 = val();
+    private static Integer pr5 = new Integer(5);
+
+    private static final int prf1 = 1;
+    private static final int prf2;
+    static { prf2 = 2; }
+    private static final int prf3 = val();
+    private static final Integer prf4 = new Integer(4);
+  }
+
+  public int field;
+  public My(int i) {
+    String s = "bla";
+    field = i;
+    if (p1 != 0)
+      field = 108; // this line can only be covered with nondet-static
+    if (p2 != 1)
+      field = 108; // this line can only be covered with nondet-static
+    if (p3 != 2)
+      field = 108; // this line can only be covered with nondet-static
+    if (p4 != 3)
+      field = 108; // this line can only be covered with nondet-static
+    if (!p5.equals(5))
+      field = 108; // this line can only be covered with nondet-static
+
+    if (pf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (pf2 != 2)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (pf3 != 3)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (!pf4.equals(4))
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (pr1 != 0)
+      field = 108; // this line can only be covered with nondet-static
+    if (pr2 != 1)
+      field = 108; // this line can only be covered with nondet-static
+    if (pr3 != 2)
+      field = 108; // this line can only be covered with nondet-static
+    if (pr4 != 3)
+      field = 108; // this line can only be covered with nondet-static
+    if (!pr5.equals(5))
+      field = 108; // this line can only be covered with nondet-static
+
+    if (prf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (prf2 != 2)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (prf3 != 3)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (!prf4.equals(4))
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PInner.pf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PInner.prf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PSInner.p1 != 0)
+      field = 108; // this line can only be covered with nondet-static
+    if (PSInner.p2 != 1)
+      field = 108; // this line can only be covered with nondet-static
+    if (PSInner.p3 != 2)
+      field = 108; // this line can only be covered with nondet-static
+    if (PSInner.p4 != 3)
+      field = 108; // this line can only be covered with nondet-static
+    if (!PSInner.p5.equals(5))
+      field = 108; // this line can only be covered with nondet-static
+
+    if (PSInner.pf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PSInner.pf2 != 2)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PSInner.pf3 != 3)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (!PSInner.pf4.equals(4))
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PSInner.pr1 != 0)
+      field = 108; // this line can only be covered with nondet-static
+    if (PSInner.pr2 != 1)
+      field = 108; // this line can only be covered with nondet-static
+    if (PSInner.pr3 != 2)
+      field = 108; // this line can only be covered with nondet-static
+    if (PSInner.pr4 != 3)
+      field = 108; // this line can only be covered with nondet-static
+    if (!PSInner.pr5.equals(5))
+      field = 108; // this line can only be covered with nondet-static
+
+    if (PSInner.prf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PSInner.prf2 != 2)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PSInner.prf3 != 3)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (!PSInner.prf4.equals(4))
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PrInner.pf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PrInner.prf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PrSInner.p1 != 0)
+      field = 108; // this line can only be covered with nondet-static
+    if (PrSInner.p2 != 1)
+      field = 108; // this line can only be covered with nondet-static
+    if (PrSInner.p3 != 2)
+      field = 108; // this line can only be covered with nondet-static
+    if (PrSInner.p4 != 3)
+      field = 108; // this line can only be covered with nondet-static
+    if (!PrSInner.p5.equals(5))
+      field = 108; // this line can only be covered with nondet-static
+
+    if (PrSInner.pf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PrSInner.pf2 != 2)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PrSInner.pf3 != 3)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (!PrSInner.pf4.equals(4))
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (PrSInner.pr1 != 0)
+      field = 108; // this line can only be covered with nondet-static
+    if (PrSInner.pr2 != 1)
+      field = 108; // this line can only be covered with nondet-static
+    if (PrSInner.pr3 != 2)
+      field = 108; // this line can only be covered with nondet-static
+    if (PrSInner.pr4 != 3)
+      field = 108; // this line can only be covered with nondet-static
+    if (!PrSInner.pr5.equals(5))
+      field = 108; // this line can only be covered with nondet-static
+
+    if (PrSInner.prf1 != 1)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PrSInner.prf2 != 2)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (PrSInner.prf3 != 3)
+      field = 108; // this line cannot be covered even with nondet-static
+    if (!PSInner.prf4.equals(4))
+      field = 108; // this line cannot be covered even with nondet-static
+
+    if (s != "bla")
+      field = 108; // this line cannot be covered even with nondet-static
+  }
+}

jbmc/regression/jbmc/nondet-static/test.desc

@@ -0,0 +1,70 @@
+CORE symex-driven-lazy-loading-expected-failure
+My.class
+--function "My.<init>" --cover location --nondet-static --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+file My\.java line 104 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 106 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 108 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 110 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 112 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 117 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 119 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 121 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 124 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 126 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 128 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 130 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 132 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 137 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 139 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 141 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 150 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 152 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 154 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 156 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 158 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 163 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 165 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 167 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 170 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 172 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 174 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 176 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 178 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 183 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 185 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 187 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 196 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 198 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 200 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 202 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 204 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 209 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 211 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 213 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 216 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 218 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 220 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 222 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 224 function java::My\.\<init\>:\(I\)V.*SATISFIED$
+file My\.java line 229 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 231 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 233 function java::My\.\<init\>:\(I\)V.*FAILED$
+file My\.java line 236 function java::My\.\<init\>:\(I\)V.*FAILED$
+--
+file My\.java line 115 function java::My\.\<init\>:\(I\)V
+file My\.java line 135 function java::My\.\<init\>:\(I\)V
+file My\.java line 144 function java::My\.\<init\>:\(I\)V
+file My\.java line 147 function java::My\.\<init\>:\(I\)V
+file My\.java line 161 function java::My\.\<init\>:\(I\)V
+file My\.java line 181 function java::My\.\<init\>:\(I\)V
+file My\.java line 190 function java::My\.\<init\>:\(I\)V
+file My\.java line 193 function java::My\.\<init\>:\(I\)V
+file My\.java line 207 function java::My\.\<init\>:\(I\)V
+file My\.java line 227 function java::My\.\<init\>:\(I\)V
+--
+This tests nondet-static option
+
+This fails under symex-driven lazy loading because nondet-static cannot be used
+with it

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -645,6 +645,8 @@ void java_bytecode_convert_classt::convert(
     // link matches the method used by java_bytecode_convert_method::convert
     // for methods.
     new_symbol.type.set(ID_C_class, class_symbol.name);
+    new_symbol.type.set(ID_C_field, f.name);
+    new_symbol.type.set(ID_C_constant, f.is_final);
     new_symbol.pretty_name=id2string(class_symbol.pretty_name)+
       "."+id2string(f.name);
     new_symbol.mode=ID_java;

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -157,6 +157,8 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
   else
     java_cp_include_files=".*";
 
+  nondet_static = cmd.isset("nondet-static");
+
   language_options_initialized=true;
 }
 
@@ -1029,9 +1031,18 @@ bool java_bytecode_languaget::convert_single_method(
     case synthetic_method_typet::STATIC_INITIALIZER_WRAPPER:
       if(threading_support)
         symbol.value = get_thread_safe_clinit_wrapper_body(
-          function_id, symbol_table);
+          function_id,
+          symbol_table,
+          nondet_static,
+          object_factory_parameters,
+          get_pointer_type_selector());
       else
-        symbol.value = get_clinit_wrapper_body(function_id, symbol_table);
+        symbol.value = get_clinit_wrapper_body(
+          function_id,
+          symbol_table,
+          nondet_static,
+          object_factory_parameters,
+          get_pointer_type_selector());
       break;
     case synthetic_method_typet::STUB_CLASS_STATIC_INITIALIZER:
       symbol.value =

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -192,6 +192,7 @@ class java_bytecode_languaget:public languaget
   bool throw_assertion_error;
   java_string_library_preprocesst string_preprocess;
   std::string java_cp_include_files;
+  bool nondet_static;
 
   // list of classes to force load even without reference from the entry point
   std::vector<irep_idt> java_load_classes;