Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Avoid using integer_typet where unsuitable #1035

Merged
merged 1 commit into from
Aug 4, 2017
Merged

Avoid using integer_typet where unsuitable #1035

merged 1 commit into from
Aug 4, 2017

Conversation

tautschnig
Copy link
Collaborator

The solver back end cannot necessarily handle unbounded integers. Do not use
them unless explicitly requested/supported.

Fixes: #1015

This is an alternative approach over #1016.

@tautschnig tautschnig requested a review from smowton June 19, 2017 12:59
@smowton
Copy link
Contributor

smowton commented Jun 19, 2017

Don't see anything obviously objectionable (although, test failures so clearly something broke), but I prefer #1016 because it causes less churn.

@tautschnig tautschnig mentioned this pull request Jun 19, 2017
Merged
@tautschnig
Copy link
Collaborator Author

Test failures addressed. Comments by @kroening, @pkesseli very much solicited (cf. #1016).

@tautschnig tautschnig force-pushed the no_integer_typet branch 2 times, most recently from d2cc0a2 to b3da32b Compare June 23, 2017 08:06
peterschrammel
peterschrammel reviewed Jun 25, 2017
View reviewed changes
src/java_bytecode/java_bytecode_convert_method.cpp Outdated
@@ -1413,40 +1423,46 @@ codet java_bytecode_convert_methodt::convert_instructions(
const bool is_double('d'==type_char);
const bool is_float('f'==type_char);

if(is_double || is_float)
if(is_double || is_float)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

weird indentation

src/java_bytecode/java_bytecode_convert_method.cpp Outdated
irep_idt number=to_constant_expr(arg).get_value();
mp_integer number;
if(to_integer(to_constant_expr(arg), number))
throw "failed to extract number";
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this a user-facing error or an invariant/precondition? (same question regarding other throws below)

src/java_bytecode/java_bytecode_convert_method.cpp Outdated
else
value.from_expr(to_constant_expr(arg0));

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This blank line actually adds to readability.

src/java_bytecode/java_bytecode_convert_method.cpp Outdated
bool ret=to_integer(to_constant_expr(arg0), int_value);
INVARIANT(!ret, "?ipush argument should be an integer");
results[0]=from_integer(int_value, java_int_type());
results[0]=arg0;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This seems to change assumptions on arg0 (need not be a constant nor of java_int_type). Please clarify.

@tautschnig
Copy link
Collaborator Author

@peterschrammel I hope to have addressed all comments.

@tautschnig tautschnig force-pushed the no_integer_typet branch 2 times, most recently from 25e9879 to b21e255 Compare June 29, 2017 08:41
@smowton
Copy link
Contributor

smowton commented Jun 30, 2017

  1. Suggest making this pattern into a utility function (typecast-if-required, probably using type_eq)
e = some_expr
if(e.type()!=t)
  e.make_typecast(t);
  1. I don't see that we've gained anything by turning an integer back and forth from decimal to binary form when often the ultimate usage is in an identifier where we want the decimal form. I continue to prefer the solution where the parser produces decimal integers and covert-method converts them to binary form if the usage context demands it, which it frequently does not.

@tautschnig
Copy link
Collaborator Author

I don't see that we've gained anything by turning an integer back and forth from decimal to binary form when often the ultimate usage is in an identifier where we want the decimal form.

The one gain is that in those cases where "often" does not apply, and after all this is where the bug fix had been necessary. Looking at my changes, there are actually a number of places that had some sort of type casting going on -- sometimes conditional, sometimes not.

Really this is a design problem, because passing an integer that is first turned into a string and then back to the original integer is questionable, irrespective of whether this is done via ID_integer or ID_signedbv.

@smowton smowton removed their request for review July 12, 2017 12:50
@tautschnig tautschnig force-pushed the no_integer_typet branch 3 times, most recently from fb2bf24 to 88d1df7 Compare July 19, 2017 09:16
@kroening
Copy link
Member

kroening commented Aug 3, 2017

This fails to build because of the change to the scope of integer_constant, but otherwise seems ready to go.

@tautschnig
Copy link
Collaborator Author

This fails to build because of the change to the scope of integer_constant, but otherwise seems ready to go.

Unless I've broken some other aspect this should now be addressed.

@tautschnig
Avoid using integer_typet where unsuitable
e2ed0df 
The solver back end cannot necessarily handle unbounded integers. Do not use
them unless explicitly requested/supported.
@kroening kroening merged commit bb9cef3 into diffblue:master Aug 4, 2017
@tautschnig tautschnig deleted the no_integer_typet branch August 4, 2017 06:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@peterschrammel peterschrammel peterschrammel approved these changes

Assignees

@kroening kroening

Labels
bugfix Solvers
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@tautschnig @smowton @kroening @peterschrammel