Fix Java integers when --no-simplify is set #1016
Conversation
These are otherwise illegal expressions (at least to boolbvt), and so get ignored. This problem usually doesn't show up as it requires --no-simplify to escape subsequent incidental simplification.
| // Force a simplify here in case we have --no-simplify | ||
| // because the simplifier is the only pass that knows how to | ||
| // deal with this cast from integer_typet: | ||
| results[0]=simplify_expr(typecast_exprt(arg0, java_int_type()), ns); |
There was a problem hiding this comment.
Why is an integer_typet being used in the first place? Does the Java standard state that these should be unbounded integers? Please clarify.
There was a problem hiding this comment.
Nothing to do with me, that code predates Github, but basically it's just a parser simplicity thing-- the integer in the constant pool turns into a "universal" integer, then using it in an ipush instruction clarifies it ought to be considered an int32 or whatever
There was a problem hiding this comment.
I fully understand that this isn't a problem you had introduced - but I am questioning the fix. Looking at http://docs.oracle.com/javase/specs/jls/se7/html/jls-3.html#jls-3.10.1 the introduction of that integer_typet is just wrong and that is what ought to be fixed, instead of introducing the simplify_expr here.
There was a problem hiding this comment.
That's not quite the right bit of the language spec--- I think that concerns literals in the source, whereas this is a literal in bytecode (e.g. https://cs.au.dk/~mis/dOvs/jvmspec/ref-_bipush.html). At any rate converting the int8_t in the bytecode to an integer doesn't seem wrong, since it doesn't lose any information?
There was a problem hiding this comment.
Ah, my Java knowledge is rather limited -- I had assumed what was true in the source was also true of bytecode. Well, in fact the bytecode should have the bit width sorted out already, or at least your statement mentioning int8_t hints at that?
Yes, converting int8_t to integer shouldn't lose information, but it yields an expression that the backend cannot deal with.
There was a problem hiding this comment.
Indeed. Either convert it back to a bitvector in the frontend (i.e. merge this PR) or have the parser create a bitvector to begin with (in which case I'll rewrite this Monday)
There was a problem hiding this comment.
I would strongly vouch for creating a bitvector to begin with - the current approach is a very effective way of shooting oneself in the foot...
My apologies that you are getting all the backlash for code you haven't even written in the first place. I'll try to make up for that by contributing patches (it seems necessary to do a git grep integer_typet).
There was a problem hiding this comment.
Pushed an amended version that creates an integer directly in bytecode-convert-method. I didn't do it in the parser because that uses integer_typet everywhere, and making particular exceptions seemed uglier. Rather let's say the parser turns the bytecode format into a tree where integer members are represented as mp_integers (effectively), then convert-method produces valid codet expressions (and typecast-integer-to-bitvector is specifically not one).
There was a problem hiding this comment.
I'll take a look; I have started to clear out most uses of integer_typet (in java_bytecode and elsewhere).
See issue cbmc#1015 for detail.
smowton
force-pushed
the
smowton/fix/java_integers_without_simplify
branch
from
00f63e6 to
e2e2360
Compare
Fixes #1015