Merge pull request #4802 from peterschrammel/assume-non-null

Add preconditions for Java NotNull annotations

Author: peterschrammel

jbmc/regression/jbmc/parameter-annotation-not-null/Main.class

@@ -0,0 +1,22 @@
+import javax.validation.constraints.NotNull;
+
+public class Main {
+  public static Integer test1(boolean y, Object z, String[] s)
+  {
+    return foo(1, y, z, s);
+  }
+  public static Integer test2(Integer x, boolean y, Object z)
+  {
+    return new Main().bar(x, y, z, new String[0]);
+  }
+  public static Integer test3(boolean y)
+  {
+    return foo(new Integer(1), y, null, new String[0]);
+  }
+  public static Integer foo(@NotNull Integer x, @NotNull boolean y, Object z, @NotNull String[] s) {
+    return x;
+  }
+  public Integer bar(@NotNull Integer x, @NotNull boolean y, Object z, @NotNull String[] s) {
+    return x;
+  }
+}

jbmc/regression/jbmc/parameter-annotation-not-null/Main.java

@@ -0,0 +1,10 @@
+CORE
+Main.class
+--function Main.test2 --classpath `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[not-null-annotation-check\.1\] line \d+ Not null annotation check: FAILURE
+\[not-null-annotation-check\.2\] line \d+ Not null annotation check: SUCCESS
+--
+^warning: ignoring

jbmc/regression/jbmc/parameter-annotation-not-null/test_array.desc

@@ -0,0 +1,10 @@
+CORE
+Main.class
+--function Main.test1 --classpath `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[not-null-annotation-check\.1\] line \d+ Not null annotation check: SUCCESS
+\[not-null-annotation-check\.2\] line \d+ Not null annotation check: FAILURE
+--
+^warning: ignoring

jbmc/regression/jbmc/parameter-annotation-not-null/test_object.desc

@@ -0,0 +1,10 @@
+CORE
+Main.class
+--function Main.test3 --classpath `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+\[not-null-annotation-check\.1\] line \d+ Not null annotation check: SUCCESS
+\[not-null-annotation-check\.2\] line \d+ Not null annotation check: SUCCESS
+--
+^warning: ignoring

jbmc/regression/jbmc/parameter-annotation-not-null/test_success.desc

@@ -585,9 +585,12 @@ void java_bytecode_convert_methodt::convert(
   current_method = method_symbol.name;
   method_has_this = method_type.has_this();
   if((!m.is_abstract) && (!m.is_native))
-    method_symbol.value = convert_instructions(
-      m,
-      to_java_class_type(class_symbol.type).lambda_method_handles());
+  {
+    code_blockt code(convert_parameter_annotations(m, method_type));
+    code.append(convert_instructions(
+      m, to_java_class_type(class_symbol.type).lambda_method_handles()));
+    method_symbol.value = std::move(code);
+  }
 }
 
 static irep_idt get_if_cmp_operator(const irep_idt &stmt)
@@ -966,6 +969,54 @@ static std::size_t get_bytecode_type_width(const typet &ty)
   return to_bitvector_type(ty).get_width();
 }
 
+code_blockt java_bytecode_convert_methodt::convert_parameter_annotations(
+  const methodt &method,
+  const java_method_typet &method_type)
+{
+  code_blockt code;
+
+  // Consider parameter annotations
+  const java_method_typet::parameterst &parameters(method_type.parameters());
+  std::size_t param_index = method_type.has_this() ? 1 : 0;
+  DATA_INVARIANT(
+    parameters.size() >= method.parameter_annotations.size() + param_index,
+    "parameters and parameter annotations mismatch");
+  for(const auto &param_annotations : method.parameter_annotations)
+  {
+    // NotNull annotations are not standardized. We support these:
+    if(
+      java_bytecode_parse_treet::find_annotation(
+        param_annotations, "java::javax.validation.constraints.NotNull") ||
+      java_bytecode_parse_treet::find_annotation(
+        param_annotations, "java::org.jetbrains.annotations.NotNull") ||
+      java_bytecode_parse_treet::find_annotation(
+        param_annotations, "org.eclipse.jdt.annotation.NonNull") ||
+      java_bytecode_parse_treet::find_annotation(
+        param_annotations, "java::edu.umd.cs.findbugs.annotations.NonNull"))
+    {
+      const irep_idt &param_identifier =
+        parameters[param_index].get_identifier();
+      const symbolt &param_symbol = symbol_table.lookup_ref(param_identifier);
+      const auto param_type =
+        type_try_dynamic_cast<pointer_typet>(param_symbol.type);
+      if(param_type)
+      {
+        code_assertt code_assert(notequal_exprt(
+          param_symbol.symbol_expr(), null_pointer_exprt(*param_type)));
+        source_locationt check_loc = method.source_location;
+        check_loc.set_comment("Not null annotation check");
+        check_loc.set_property_class("not-null-annotation-check");
+        code_assert.add_source_location() = check_loc;
+
+        code.add(std::move(code_assert));
+      }
+    }
+    ++param_index;
+  }
+
+  return code;
+}
+
 code_blockt java_bytecode_convert_methodt::convert_instructions(
   const methodt &method,
   const java_class_typet::java_lambda_method_handlest &lambda_method_handles)

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -300,6 +300,10 @@ class java_bytecode_convert_methodt:public messaget
   // conversion
   void convert(const symbolt &class_symbol, const methodt &);
 
+  code_blockt convert_parameter_annotations(
+    const methodt &method,
+    const java_method_typet &method_type);
+
   code_blockt convert_instructions(
     const methodt &,
     const java_class_typet::java_lambda_method_handlest &);

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -1276,7 +1276,7 @@ void java_bytecode_parsert::rmethod_attribute(methodt &method)
     attribute_name == "RuntimeVisibleParameterAnnotations")
   {
     u1 parameter_count = read_u1();
-    // There may be attributes for both runtime-visiible and rutime-invisible
+    // There may be attributes for both runtime-visible and runtime-invisible
     // annotations, the length of either array may be longer than the other as
     // trailing parameters without annotations are omitted.
     // Extend our parameter_annotations if this one is longer than the one