change java bool type representation

[mgudemann]

The JVM does not fully support a Boolean type. Instead, it uses an
32-bit integral type with value 0 for false and 1 for true (cf. 2.3.4 of
the JVM Spec). In particular, the bytecodes iconst_0 and iconst_1 are
used for false and true.

[mgudemann]

Ok, unsuprisingly this isn't so easy. Now a non-deterministic boolean can be any int. There should be a restriction to set only the LSB.

In particular what does not work is something like this:

    public void doIt(boolean a, int div) {
      if (a == true) {
        return;
      }
      if (a == false) {
        return;
      }
      int d = 5 / div;
    }

while this is ok:

    public void doIt3(boolean a, int div) {
      if (a) {
        return;
      }
      if (!a) {
        return;
      }
      int d = 5 / div;
    }

[kroening]

We do have c_bool, which has the semantics that it can only be 0 or 1. It can have an arbitrary number of bits in it.

[mgudemann]

When using c_bool_typet(32) for example on the function java::BoolType.boolTest:(Z)V of

public class BoolType {
  public boolean negate(boolean a) {
    return !a;
  }
  public void boolTest() {
    boolean b = negate(true);
    assert !b;
  }
}

on gets the error

function call: parameter "java::BoolType.negate:(Z)Z::arg1a" type mismatch: got signedbv
  * width: 32, expected c_bool
  * width: 32

because of the internal signedbv type of the constant true which ist encoded as iconst_1 in the bytecode

  public void boolTest();
    Code:
       0: aload_0       
       1: iconst_1      
       2: invokevirtual #2                  // Method negate:(Z)Z

[mgudemann]

Using c_bool_typet(8/32) also fails on division by zero on this:

public class BoolType {
  public void doIt(boolean a, int div) {
    if (a == true || a == false) {
      return;
    }
    int d = 5 / div;
  }
}

presumably because of a related reason.

[kroening]

2675a17 adds a test for this.