Checker Nullness

belongs to group Advanced
Identify where null might be dereferenced or passed to a library

Frameworks supported by this checker

  • java up to 11
  • android up to API level 28
  • dotnet

Warnings generated by this checker

  • ActualInnerNullWarning: an actual parameter passed to a method is an array or collection possibly containing null [ CWE476 ]
  • ActualNullWarning: an actual parameter passed to a method might be null [ CWE476 ]
  • ArrayLengthOfNullWarning: the length of a possibly null array is computed [ CWE476 ]
  • ArrayLoadFromNullWarning: an element of a possibly null array is read [ CWE476 ]
  • ArrayStoreIntoNullWarning: an element of a possibly null array is written [ CWE476 ]
  • CallOnNullWarning: a method call might occur on a null receiver [ CWE476 ]
  • FieldInnerNullWarning: a field holds an array or collection possibly containing null [ CWE476 ]
  • FieldNullWarning: a field might hold null [ CWE476 ]
  • FormalInnerNullWarning: a formal parameter of a method or constructor is an array or collection possibly containing null [ CWE476 ]
  • FormalNullWarning: a formal parameter of a method or constructor might hold null [ CWE476 ]
  • GetFieldFromNullWarning: a field is read from a possibly null receiver [ CWE476 ]
  • MethodReturnsInnerNullWarning: a method returns an array or collection possibly containing null [ CWE476 ]
  • MethodReturnsNullWarning: a method might return null [ CWE476 ]
  • PutFieldIntoNullWarning: a field is written into a possibly null receiver [ CWE476 ]
  • SynchronizationOnNullWarning: a synchronization might occur on null [ CWE476 ]
  • ThrowOfNullWarning: a throw command might throw null [ CWE476 ]
  • UselessNullnessTestOfFieldWarning: a comparison of a field against null is always true or always false [ CWE398 ]
  • UselessNullnessTestOfFormalWarning: a comparison of a formal parameter against null is always true or always false [ CWE398 ]
  • UselessNullnessTestOfMethodReturnWarning: a comparison of the return value of a method against null is always true or always false [ CWE253 ]
  • UselessNullnessTestWarning: a comparison of a value against null is always true or always false [ CWE398 ]

Options accepted by this checker

  • annotationPackage: specify the package for the annotations used in the jaif file
    This option specifies which package must be used in the jaif file to identify the nullness annotations. If it is not used, the default Julia package for those annotations is used
  • dumpAnalysis: dump the nullness analysis at the end of its computation
    This option prints the nullness invariants inferred at each bytecode (locals and stack elements that are definitely null or non-null). This can be a huge printout. Useful for debugging
  • dumpDotWithInvariants: dump the analysed code in dot format, with nullness information
    This option dumps a dot file for each method or constructor that is reachable from the entry points of the analysis. At the beginning of each code, a nullness invariant is reported
  • dumpSelectedAnalysis: dump the nullness analysis of selected places at the end of its computation
    This option prints the nullness invariants inferred at each bytecode of methods or constructors that have at least a parameter or the return value annotated as @com.juliasoft.julia.checkers.Print
  • entriesReceiveNonNull: assume that entries to the program are called with non-null parameters from outside the application
    This can be useful to reduce the number of spurious nullness warnings during the analysis of libraries. However, this assumption should be true or the results might be unsound
  • fullJaif: dump a jaif file with the nullness and non-nullness information of the program
    The generated jaif file is a compact report of the program places that might contain a null value. Differently from the -jaif option, this generates explicit information for the places that contain a non-null value as well and is hence a more verbose version of the same information
  • fullyQualifiedNames: use fully qualified class names in the jaif files
    The generated jaif file is a compact report of the program places that might contain a null value. This option forces the use of fully qualified class names in the jaif file, also when referring to classes in the same package that is being reported
  • init: perform a preliminary class initialization analysis that simplifies the code
    A class initialization analysis determines where a class is already initialized, and hence its static initializer will never be called again. This option allows one to simplify the code before the actual nullness analysis and can sometimes improve its precision. However, it increases the total cost of the analysis
  • jaif: dump a jaif file with the nullness information of the program
    A jaif file is a compact report of the program places that might contain a null value. It can be used for reference and documentation, but can also be imported in the source code of the program by using the annotation file utilities (see http://types.cs.washington.edu/annotation-file-utilities)
  • list: list the program points where null might be dereferenced or passed to a library
    In most cases, this option will be selected. The only reason to leave this option unselected is to apply the nullness checker only to generate a jaif file or modify the program by removing exceptional execution paths that will never be followed at run-time. For instance, if nullness analysis is only used to support and simplify the code for a subsequent static analysis
  • mergeCreations: merge the creation points for the same type inside the same class
    This enhances the efficiency of the creation points analysis performed as part of nullness analysis but, in general, reduces the precision of the analyzer. However, it can be an important option to select for the analysis of very large applications and in library mode, when the creation points analysis takes too long to complete. This option is automatically selected for large programs
  • noArrays: do not prove that arrays contain non-null elements
    Proving that the elements of an array are non-null when they are accessed is an important aspect for the precision of the nullness analysis, but is also difficult in most cases. This option disables that proof. Mainly useful for profiling and statistics
  • noCollections: do not prove that collections contain non-null elements
    Proving that the elements of a collection are non-null when they are accessed is an important aspect for the precision of the nullness analysis, but is also difficult in most cases. This option disables that proof. Mainly useful for profiling and statistics
  • noExpNonNullness: do not perform the expression non-nullness analysis
    This reduces the precision of the analysis, since Julia will not try to prove anymore that specific expressions hold a non-null value at specific program points. Mainly useful for profiling and statistics
  • noFieldNullness: do not perform the field nullness analysis
    This reduces the precision of the analysis, since Julia will not track anymore the fields that might contain a null-value at specific program points. Mainly useful for profiling and statistics
  • noOracle: do not use an oracle semantics for the fields
    This largely reduces the precision of the analysis, since Julia will not track anymore the fields that are definitely initialized to a non-null value before being accessed. Mainly useful for profiling and statistics
  • noRawness: do not perform the rawness analysis for the jaif file
    Rawness analysis identifies objects that are not yet completely initialized. This information is reported in the jaif file, if the -jaif or -fullJaif options are selected. By unselecting this option, no rawness information is reported in those files
  • noReachability: do not perform reachability analysis
    This option reduces the precision of the analyzer. Only useful for statistics
  • noTrackBooleans: do not approximate Booleans during the analysis
    By selecting this option, Julia does not reason anymore on the value of Boolean variables. In rare cases, this reduces the precision of the analysis, but in general increases the efficiency and reduces the memory footprint of the analyzer
  • noUnreachable: do not dump information on unreachable code
    By selecting this option, the jaif files become smaller
  • noUselessChecks: do not warn when a nullness check is useless
    By selecting this option, useless checks against null are not reported with a warning
  • openCallsReturnNonNull: assume that calls to unknown code return a non-null value, unless that value is later compared against null.
    This can be useful to reduce the number of spurious nullness warnings during the analysis of incomplete code. However, this assumption might make the analysis unsound
  • reachabilityVsSharing: show the precision of sharing analysis wrt reachability information
    Reachability information can be computed from sharing information, but in general the result is less precise than by computing reachability information explicitly with its own analysis. This option is only useful for statistics, by comparing the precision of the resulting reachability information
  • reportLocals: dump information on local variables
    By selecting this option, the jaif file contains information on local variables as well and consequently becomes larger
  • reportSideEffects: annotate the side-effect free methods and constructors in the jaif file
    The generated jaif file is a compact report of the program places that might contain a null value. This option, when used in conjunction with -jaif or -jaifFull, uses also an extra annotation for the methods and constructors that have no side-effect
  • simplify: simplify the program in memory after the analysis, by removing useless exception handlers
    This option applies a simplification to the program in memory, by using the results of the nullness analysis. Namely, if an instruction has been proved to never throw an exception, then its branches to exceptional handlers can be removed. This option is useful only for optimizing subsequent analyses
  • stub: dump a stub file with the nullness information of the program
    A stub file reports the nullable methods parameters and the nullable fields. Consider using the richer jaif file generated through the -jaif option instead
  • synchroniseExpAliasing: wait for the supporting analyses before starting the expression aliasing analysis
    This option allows one to compute the exact time needed for the expression aliasing analysis. Only useful for statistics
  • synchroniseReachability: wait for the supporting analyses before starting the reachability analysis
    This option allows one to compute the exact time needed for the reachability analysis. Only useful for statistics
  • synchroniseSharing: wait for the supporting analyses before starting the sharing analysis
    This option allows one to compute the exact time needed for the sharing analysis. Only useful for statistics
  • unwrittenFieldsHoldNull: Assume that fields never assigned hold null. This might be unsound for fields assigned by reflection
    This can improve the precision of the analysis in the rare case when fields are accessed but never assigned. However, it is highly likely that those fields are assigned by reflection, so we suggest not to use this option
  • warnIfExpected: issues null-pointer warnings also where the exception might be expected
    The programmer sometime expects a NullPointerException, for instance if the code catches that exception explicitly or if a JUnit test is annotated as expecting that exception to be thrown. By disabling this option, a warning is not generated in those cases

Annotations understood by this checker

  • @com.juliasoft.julia.checkers.nullness.NonNull
  • @com.juliasoft.julia.checkers.nullness.Nullable


Description

This checker looks for program points where, at runtime, a null pointer might be dereferenced and the execution stopped with a NullPointerException. It also looks for calls to library methods where null, or a collection or array containing a null element, might be passed as a parameter in a place where this is not allowed.

Action: check if the value is actually null and modify the program in such a way to be sure that it is never null again. In most cases, a nullness bug is the consequence of a more complex bug, where some field is not always initialized before being used. Try to define as many as possible of your fields as final. Do not use null as a special value returned by a method.

Since nullness is undecidable, it is impossible to find all and only the nullness bugs, without any false positive. As a consequence, Julia will often issue spurious warnings, where a fake bug is signalled because the analyzer is not clever enough to understand that some value in never actually null. However, Julia is currently the only analyzer that does not miss nullness bugs: if there is a real bug, it will be signalled. If the number of false alarms is too high and soundness is not paramount, it is also possible to use the faster BasicNullness checker, which is unsound but yields its results much more quickly and with fewer false alarms than Nullness.

Manually-provided Annotations

In order to reduce the number of false positives, you can instruct the analyzer with nullness annotations, placed in the code that you analyze. Usually, one performs a first nullness analysis and gets many fake warnings (false positives), but most of them have the same origin: a field that Julia does not identify as non-null or a method that Julia does not identify as always returning a non-null value. Hence, you can use this first analysis to place annotations in your code and then start the analysis again. In particular, Julia can be helped by putting the following annotations in the code under analysis:

  • @NonNull for fields and return values: states that the field is never null when it is read, or that the method always returns a non-null value;
  • @Inner0NonNull for fields and return values of generic type: states that the first generic type variable of the values held in the field or returned by the method is non-null. For instance, this allows one to state that a set bound to a field contains non-null elements only or that a method returns a map whose keys are all non-null;
  • @Inner1NonNull for fields and return values of generic type: as in the case above, but predicates over the second generic type variable. For instance, this allows one to state that the values of a map held in a field are all non-null.
  • @Nullable for the formal parameters of a method or constructor in a library: it states that it is allowed to pass null for that parameter.

It is also possible to state that a given expression is non-null at a specific program point. For that, use NullnessAssertions.assertNonNull(expression). Note that the fact that a variable is non-null at a program point does not prevent it from holding null later.

Jaif Annotation File

If the jaif option of this checker is enabled, a jaif file is generated. It is a text file that contains nullness annotations for fields, constructor and method parameters and the return value of the methods. In this sense, it is a compact representation of the information inferred by this checker. The default annotation is @NonNull, hence the latter is never explicitly reported in the file.

This checker looks for program points where, at runtime, a null pointer might be dereferenced and the execution stopped with a NullReferenceException. It also looks for calls to library methods where null, or a collection or array containing a null element, might be passed as a parameter in a place where this is not allowed.

Action: check if the value is actually null and modify the program in such a way to be sure that it is never null again. In most cases, a nullness bug is the consequence of a more complex bug, where some field is not always initialized before being used. Try to define as many as possible of your fields as final. Do not use null as a special value returned by a method.

Since nullness is undecidable, it is impossible to find all and only the nullness bugs, without any false positive. As a consequence, Julia will often issue spurious warnings, where a fake bug is signalled because the analyzer is not clever enough to understand that some value in never actually null. However, Julia is currently the only analyzer that does not miss nullness bugs: if there is a real bug, it will be signalled. If the number of false alarms is too high and soundness is not paramount, it is also possible to use the faster BasicNullness checker, which is unsound but yields its results much more quickly and with fewer false alarms than Nullness.

Manually-provided Annotations

In order to reduce the number of false positives, you can instruct the analyzer with nullness annotations, placed in the code that you analyze. Usually, one performs a first nullness analysis and gets many fake warnings (false positives), but most of them have the same origin: a field that Julia does not identify as non-null or a method that Julia does not identify as always returning a non-null value. Hence, you can use this first analysis to place annotations in your code and then start the analysis again. In particular, Julia can be helped by putting the following annotations in the code under analysis:

  • [NonNull] for fields and return values: states that the field is never null when it is read, or that the method always returns a non-null value;
  • [Inner0NonNull] for fields and return values of generic type: states that the first generic type variable of the values held in the field or returned by the method is non-null. For instance, this allows one to state that a set bound to a field contains non-null elements only or that a method returns a map whose keys are all non-null;
  • [Inner1NonNull] for fields and return values of generic type: as in the case above, but predicates over the second generic type variable. For instance, this allows one to state that the values of a map held in a field are all non-null.
  • [Nullable] for the formal parameters of a method or constructor in a library: it states that it is allowed to pass null for that parameter.

It is also possible to state that a given expression is non-null at a specific program point, but note that the fact that a variable is non-null at a program point does not prevent it from holding null later.

Jaif Annotation File

If the jaif option of this checker is enabled, a jaif file is generated. It is a text file that contains nullness annotations for fields, constructor and method parameters and the return value of the methods. In this sense, it is a compact representation of the information inferred by this checker. The default annotation is [NonNull], hence the latter is never explicitly reported in the file.


Examples

Consider the following fragment of code, taken from the BluetoothChat sample application by Google, distributed with its ADT:

  // Read from the InputStream
  int bytes = this.mmInStream.read(buffer);

This checker issues the following warning (the exact line depends on the version of the sample application):

com/example/android/BluetoothChat/BluetoothChatService.java:2: [Nullness: FieldNullWarning] is the value of field mmInStream non-null?

This means that, according to Julia, it seems possible that field mmInStream might hold null there and a runtime NullPointerException might be thrown. A similar warning is signalled about field mmOutStream as well. Those fields are initialized inside the constructor:

  private class ConnectedThread extends Thread {
    private final BluetoothSocket mmSocket;
    private final InputStream mmInStream;
    private final OutputStream mmOutStream;

    public ConnectedThread(BluetoothSocket socket, String socketType) {
      Log.d(TAG, "create ConnectedThread: " + socketType);
      mmSocket = socket;
      InputStream tmpIn = null;
      OutputStream tmpOut = null;

      // Get the BluetoothSocket input and output streams
      try {
        tmpIn = socket.getInputStream();
        tmpOut = socket.getOutputStream();
      } catch (IOException e) {
        Log.e(TAG, "temp sockets not created", e);
      }

      mmInStream = tmpIn;
      mmOutStream = tmpOut;
    }
  }

However, if the input or output streams of the bluetooth socket cannot be opened (for instance, if the mobile device has no bluetooth hardware interface or has that interface turned off or broken), an IOException is thrown at line 14, variables tmpIn and tmpOut keep their initial value null from lines 9 and 10 and fields mmInStream and mmOutStream get assigned null at lines 20 and 21. Hence, Julia is right: there might be a NullPointerException at BluetoothChatService.java:2 because those two fields might actually hold null.

To fix that bug, when the streams cannot be opened, the construction of the object should abort with an exception:

 private class ConnectedThread extends Thread {
    private final BluetoothSocket mmSocket;
    private final InputStream mmInStream;
    private final OutputStream mmOutStream;

    public ConnectedThread(BluetoothSocket socket, String socketType) throws IOException {
      Log.d(TAG, "create ConnectedThread: " + socketType);
      mmSocket = socket;
      InputStream tmpIn = null;
      OutputStream tmpOut = null;

      // Get the BluetoothSocket input and output streams
      try {
        tmpIn = socket.getInputStream();
        tmpOut = socket.getOutputStream();
      } catch (IOException e) {
        Log.e(TAG, "temp sockets not created", e);
        throw e;
      }

      mmInStream = tmpIn;
      mmOutStream = tmpOut;
    }
  }

With these changes, Julia does not issue anymore a warning about the possible nullness of fields mmInStream and mmOutStream, since it can now prove them non-null.

Consider now the following program:

import java.util.Set;
import java.util.HashSet;

public class Nullness {
  public static void main(String[] args) {
    Set<Object> set = new HashSet<>();
    Set<String> set2 = new HashSet<>();

    for (String s: args)
      set2.add(s);

    if (System.currentTimeMillis() % 2 == 0)
      set2.add(null);

    set.add("hello");
    set.add(new Object());

    for (Object o: set)
      o.toString();

    for (String s: set2)
      s.toString();

    for (String s: set2) {
      System.out.println(s);
      System.getProperty(s);
    }
  }
}

The HashSet set contains non-null elements only, while the HashSet set2 might contain null among its elements, because of line 13. Julia understands this fact and this checker issues the following warnings:

Nullness.java:22: [Nullness: CallOnNullWarning] is the receiver of "toString" non-null?
Nullness.java:26: [Nullness: ActualNullWarning] is parameter "key" of "getProperty" non-null?

That is, Julia finds that method toString() might be called on a null receiver at line 22, which would raise a NullPointerException. Moreover, null might be passed as actual parameter to the getProperty() method at line 26, which is illegal and would raise a NullPointerException as well. It is interesting to observe that Julia does not issue any warning about the fact that null might be passed as actual parameter to the println() method at line 25. This is because that method allows null as its argument, in which case it prints the string "null" and does not throw any exception.

Consider the following program:

using System;
using System.Collections.Generic;

namespace Nullness
{
	public class Nullness
    {
        public static void Main(string[] args)
        {
            HashSet<object> set = new HashSet<object>();
            HashSet<string> set2 = new HashSet<string>();
            foreach (string s in args)
                set2.Add(s);
            if (DateTime.Now.Millisecond % 2 == 0)
                set2.Add(null);
            set.Add("hello");
            set.Add(new object());
            foreach (object o in set)
                o.ToString();
            foreach (string s in set2)
                s.ToString();
            foreach (string s in set2)
            {
                Console.WriteLine(s);
                Environment.GetEnvironmentVariable(s);
            }
        }
    }
}

The HashSet set contains non-null elements only, while the HashSet set2 might contain null among its elements, because of line 15. Julia understands this fact and this checker issues the following warnings:

Nullness.java:21: [Nullness: CallOnNullWarning] is the receiver of "ToString" non-null?
Nullness.java:25: [Nullness: ActualNullWarning] is parameter "variable" of "GetEnvironmentVariable" non-null?

That is, Julia finds that method ToString() might be called on a null receiver at line 21, which would raise a NullReferenceException. Moreover, null might be passed as actual parameter to the GetEnvironmentVariable() method at line 25, which is illegal and would raise a NullReferenceException as well. It is interesting to observe that Julia does not issue any warning about the fact that null might be passed as actual parameter to the WriteLine() method at line 24. This is because that method allows null as its argument, in which case it prints the string "null" and does not throw any exception.