Java frontend requires --simplify for constant casts

[smowton]

The Java frontend synthesises expressions like (signedbv_typet(32)) (integer_typet(50)), for example due to the bytecode op bipush 50, for which the parser makes an integer-typed constant for the 50 and then wraps it in a typecast for the bipush (see https://github.com/diffblue/cbmc/blob/master/src/java_bytecode/java_bytecode_convert_method.cpp#L1416)

Problem is, only simplify_expr actually understands that construct (at https://github.com/diffblue/cbmc/blob/master/src/util/simplify_expr.cpp#L451); in particular boolbvt::convert_typecast does not, and for input:

public class test {
  public void f() {
    int x = 50;
  }
}

with command line: cbmc test.class --no-simplify --function test.f --cover location

We get the predictable error:

warning: ignoring typecast
  * type: signedbv
      * width: 32
      * #c_type: signed_int
  0: constant
      * type: integer
      * value: 50

Therefore I say the Java frontend should forcibly simplify that expression immediately upon generating it, rather than hope for optional downstream passes to fix it up.

[martin-cs]

On Thu, 2017-06-15 at 01:43 -0700, Chris Smowton wrote: The Java frontend synthesises expressions like `(signedbv_typet(32)) (integer_typet(50))`, for example due to the bytecode op `bipush 50`, for which the parser makes an integer-typed constant for the `50` and then wraps it in a typecast for the `bipush` (see https://github.com/diffblue/cbmc/blob/master/src/java_bytecode/java_bytecode_convert_method.cpp#L1416) Problem is, only `simplify_expr` actually understands that construct (at https://github.com/diffblue/cbmc/blob/master/src/util/simplify_expr.cpp#L451); in particular `boolbvt::convert_typecast` does not, and for input: ``` public class test { public void f() { int x = 50; } } ``` with command line: `cbmc test.class --no-simplify --function test.f --cover location`

Note that --no-simplify is intended more as a testing option than a feature / user accessible thing. May I ask why you want this to work?

We get the predictable error: ``` warning: ignoring typecast * type: signedbv * width: 32 * #c_type: signed_int 0: constant * type: integer * value: 50 ```

This is a bit expected. The integer type is intended to be mathematical integers (i.e. \Z) so them not being supported by the bit-blaster (or at least requiring an extra layer with abstraction) is not wrong as such.

Therefore I say the Java frontend should forcibly simplify that expression immediately upon generating it, rather than hope for optional downstream passes to fix it up.

Maybe. The general policy has been to only simplify / transform code when needed as doing it earlier can result in building up some complex and technical debt heavy constraints on the system. For example if we ever wanted to actually do something smart with complex or vector we could be in with a big job. For me it comes down to a question of what the semantics of bipush are. Is it "it creates a(n| mathematical) integer constant and casts it to the appropriate type" or is it "it creates an constant of the right type". If it's the first one, so that the cast could fail / raise exceptions / etc. then we shouldn't simplify it. If it's the second then yes, simplify at that point, but not necessarily more generally. HTH

[smowton]

The use case was "trying to create a new driver program, failing to set 'simplify', wondering why the Java frontend produces illegal expressions"

[smowton]

And bipush semantics are to push a constant int -- the existence of the cast at all is just a convenience thing for the parser.

[smowton]

To phrase this another way, surely simplify should be doing what it says -- simplifying, making a downstream task easier rather than possible -- rather than eliminating certain expression forms that other passes fail to cover?

[tautschnig]

To phrase this another way, surely simplify should be doing what it says -- simplifying, making a downstream task easier rather than possible -- rather than eliminating certain expression forms that other passes fail to cover?

Yes, but as just said in #1016 (comment) I am wondering whether those expressions should exist in the first place?!

[martin-cs]

On Thu, 2017-06-15 at 03:38 -0700, Chris Smowton wrote: And `bipush` semantics are to push a constant `int` -- the existence of the cast at all is just a convenience thing for the parser.

Assuming that 'int' is a machine integer then, yes, the simplifier should be called when the cast has been created.

[martin-cs]

On Thu, 2017-06-15 at 03:42 -0700, Chris Smowton wrote: To phrase this another way, surely simplify should be doing what it says -- simplifying, making a downstream task *easier* rather than *possible* -- rather than eliminating certain expression forms that other passes fail to cover?

Sort of. The simplify / no-simplify options are about one specific case which is (context-free) expression simplification during symbolic execution. It isn't more general than that and critically, it is a back-end option rather than anything front-end. A consequence of this can be eliminating problematic constructs, which may mean that more basic analyzers / back-ends / solvers may be able to address some problems but this is a side effect, not the design. So perhaps the bigger question is; does the semantics of Java require mathematical integers? If not and it's just convenience in the front-end (which seems like the case) then it should simplify the casts when built and none of this is a problem.

[smowton]

I don't think the semantics require them; the contexts where they're used already specify a byte or half-word or similar rather than an arbitrary integer, so going via a universal integer intermediate format is purely a convenience. Simplify-when-built: the attached PR does this.