read failed: getstatic

[weaversa]

This error feels like saw is not properly handling (allocating and filling) static final private (global) arrays for Java programs.

Loading file "mock.saw"
registering standard overrides
registering use-provided overrides
registering assumptions
simulating function
...Stack trace:
"jym_verify" (mock.saw:3:6-3:16):
Symbolic execution failed.
Abort due to false assumption:
  internal: error: in mock.getMask
  read failed: getstatic mock.mask

public class mock {
  static final private int mask[] = {1, 2, 3};
  public static final in getMask(int pos) {
    return mask[pos];
  }
}

import mock;
public class mock2 {
  public in getval() {
    return mock.getMask(2);
  }
}

c <- java_load_class "mock2";
p <- jvm_verify c "getval" [] false
  do {
    this <- jvm_alloc_object "mock2";
    jvm_execute_func [this];
    jvm_return (jvm_term {{ 3 : [32] }});}
  z3;

[brianhuffman]

We just never implemented this functionality to automatically initialize static final fields. As a workaround, you can specify the contents of the static fields explicitly, like this:

c <- java_load_class "mock2";

let mask_setup =
  do {
    mask <- jvm_alloc_array 3 java_int;
    jvm_array_is mask {{ [1, 2, 3] : [3][32] }};
    jvm_static_field_is "mock.mask" mask;
  };

p <- jvm_verify c "getval" [] false
  do {
    this <- jvm_alloc_object "mock2";
    mask_setup;
    jvm_execute_func [this];
    jvm_return (jvm_term {{ 3 : [32] }});}
  z3;

Implementing this automatic initialization might be a bit tricky, because apparently the values of static final fields like this are not stored as values in the class file, they are stored as code. Here's the output of running javap -p -c mock.class:

Compiled from "mock.java"
public class mock {
  private static final int[] mask;

  public mock();
    Code:
       0: aload_0
       1: invokespecial #1                  // Method java/lang/Object."<init>":()V
       4: return

  public static final int getMask(int);
    Code:
       0: getstatic     #2                  // Field mask:[I
       3: iload_0
       4: iaload
       5: ireturn

  static {};
    Code:
       0: iconst_3
       1: newarray       int
       3: dup
       4: iconst_0
       5: iconst_1
       6: iastore
       7: dup
       8: iconst_1
       9: iconst_2
      10: iastore
      11: dup
      12: iconst_2
      13: iconst_3
      14: iastore
      15: putstatic     #2                  // Field mask:[I
      18: return
}

Basically I guess we'd just have to run the code from this no-name static {} method block before performing any verification. If arbitrary code is allowed in blocks like this (such as calling other constructor methods or class initializers) then that might get a bit tricky, especially if that code is sensitive to which other classes or fields have been initialized already. (See also #916.)

Another challenge will be how to deal with final static fields when executing overrides. When we run the spec for getval as an override, it should really be checking as an explicit precondition that the mask field contains the expected array value. But because the expected value is only expressed as code in the class file, we'll have to somehow derive the form of that precondition from the code. Again, this might get tricky if the code in that initializer does anything weird.

[michaelabernardo]

Using your workaround, we get the following error:

Stack trace: "jvm_verify" (mock.saw:10:6-10:16):
jvm_static_field_is: JVM field resolution failed:
Values with type 'mock' do not contain field named mock.mask.
Available fields:
mask

[brianhuffman]

The behavior of static field name parsing and resolution has been modified in the not-too-distant past. You might be using a slightly different version than me. You might try changing jvm_static_field_is "mock.mask" mask to jvm_static_field_is "mask" mask.

[sauclovian-g]

This at least should be fixed to have reasonable error reporting.