-
Notifications
You must be signed in to change notification settings - Fork 273
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.
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
adding code to generate hexadecimal numbers in java tests #1061
adding code to generate hexadecimal numbers in java tests #1061
Conversation
src/goto-programs/interpreter.cpp
Outdated
@@ -960,7 +960,8 @@ bool interpretert::unbounded_size(const typet &type) | |||
size_t interpretert::get_size(const typet &type) | |||
{ | |||
if(unbounded_size(type)) | |||
return 2ULL << 32ULL; | |||
return 1ULL << 31ULL; | |||
//return 2ULL << 32ULL; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This seems unrelated to the actual change. It's also not clear why it's needed.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
this is required for 32 bit systems, as the original code is UB for those, it's not yet obvious how to fix this in general for 32 bit
Still, it should not be part of this PR
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Please remove code instead of commenting out
src/java_bytecode/expr2java.cpp
Outdated
buffer << D; | ||
return(buffer.str()); | ||
} | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Seems a bit clunky but I think that's just what C++ forces you to do. Other than that; looks good.
src/java_bytecode/expr2java.cpp
Outdated
@@ -235,6 +237,23 @@ std::string expr2javat::convert_constant( | |||
dest+='L'; | |||
return dest; | |||
} | |||
else if (src.type() == java_float_type()) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
could you please also run the scripts/cpplint.py
script on this
For example, there should be no spaces around =
or ==
or after if
src/java_bytecode/expr2java.cpp
Outdated
@@ -235,6 +237,23 @@ std::string expr2javat::convert_constant( | |||
dest+='L'; | |||
return dest; | |||
} | |||
else if (src.type() == java_float_type()) { | |||
ieee_floatt Fpn(to_constant_expr(src)); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do not use upper case in identifiers.
src/java_bytecode/expr2java.cpp
Outdated
std::stringstream buffer; | ||
buffer << std::hexfloat; | ||
buffer << F << 'f'; | ||
return(buffer.str()); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
return buffer.str();
(several occurrences)
src/java_bytecode/expr2java.cpp
Outdated
float F = Fpn.to_float(); | ||
std::stringstream buffer; | ||
buffer << std::hexfloat; | ||
buffer << F << 'f'; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You could merge this with the previous statement to make it shorter
Since this is my first CBMC patch, Matthias asked me to submit a PR with
the code I added just to start the process. (To tell the truth I thought
that 'in progress' meant the same thing as "don't disturb" on a hotel door.
Nevertheless your comments are greatly appreciated. ) This patch still
misses the code that takes care about special cases e.g. NaN, infinity and
so on reported in 'ieee_floatt'. After I add it, I will start working on
your comments.
…On Tue, Jun 27, 2017 at 4:28 AM, Peter Schrammel ***@***.***> wrote:
***@***.**** commented on this pull request.
------------------------------
In src/java_bytecode/expr2java.cpp
<#1061 (comment)>:
> @@ -235,6 +237,23 @@ std::string expr2javat::convert_constant(
dest+='L';
return dest;
}
+ else if (src.type() == java_float_type()) {
+ ieee_floatt Fpn(to_constant_expr(src));
Do not use upper case in identifiers.
------------------------------
In src/java_bytecode/expr2java.cpp
<#1061 (comment)>:
> @@ -235,6 +237,23 @@ std::string expr2javat::convert_constant(
dest+='L';
return dest;
}
+ else if (src.type() == java_float_type()) {
+ ieee_floatt Fpn(to_constant_expr(src));
+ float F = Fpn.to_float();
+ std::stringstream buffer;
+ buffer << std::hexfloat;
+ buffer << F << 'f';
+ return(buffer.str());
return buffer.str(); (several occurrences)
------------------------------
In src/java_bytecode/expr2java.cpp
<#1061 (comment)>:
> @@ -235,6 +237,23 @@ std::string expr2javat::convert_constant(
dest+='L';
return dest;
}
+ else if (src.type() == java_float_type()) {
+ ieee_floatt Fpn(to_constant_expr(src));
+ float F = Fpn.to_float();
+ std::stringstream buffer;
+ buffer << std::hexfloat;
+ buffer << F << 'f';
You could merge this with the previous statement to make it shorter
—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHub
<#1061 (review)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AS5pCp_8xvX6uyKfhNeLbsMTp3zl2BIMks5sIL0VgaJpZM4OFzFY>
.
|
@eigold no worries, for the "in progress", this means basically that you are working on it and yes, "ready to Review" will be the next step. But I have to admit that this is not always treated as it should be :-) |
src/goto-programs/interpreter.cpp
Outdated
@@ -960,7 +960,8 @@ bool interpretert::unbounded_size(const typet &type) | |||
size_t interpretert::get_size(const typet &type) | |||
{ | |||
if(unbounded_size(type)) | |||
return 2ULL << 32ULL; | |||
return 1ULL << 31ULL; | |||
//return 2ULL << 32ULL; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Please remove code instead of commenting out
Sorry, I have been distracted by work on a new ebmc release.
As for the code in question I will actually restore the commented-out line.
The problem is that I run 32-bit Ubuntu. Line
'return 2ULL << 32ULL'
causes the error message below:
interpreter.cpp:964:20: error: large integer implicitly truncated to
unsigned type [-Werror=overflow]
Matthias suggested that I should use a replacement line 'return 1ULL <<
31ULL' on my computer. Since this line does not look good for 64-bit
systems, currently it is just my "personal patch" used to build a binary on
my desktop.
…On Fri, Jun 30, 2017 at 6:26 AM, Peter Schrammel ***@***.***> wrote:
***@***.**** requested changes on this pull request.
------------------------------
In src/goto-programs/interpreter.cpp
<#1061 (comment)>:
> @@ -960,7 +960,8 @@ bool interpretert::unbounded_size(const typet &type)
size_t interpretert::get_size(const typet &type)
{
if(unbounded_size(type))
- return 2ULL << 32ULL;
+ return 1ULL << 31ULL;
+ //return 2ULL << 32ULL;
Please remove code instead of commenting out
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#1061 (review)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AS5pCox4auU6ActOuD0u2U_ZRRvdFr7qks5sJM1kgaJpZM4OFzFY>
.
|
Then this should be fixed in the interpreter to work on 32bit systems (can be done as a separate PR). |
Okay
…On Fri, Jun 30, 2017 at 9:54 AM, Peter Schrammel ***@***.***> wrote:
Then this should be fixed in the interpreter to work on 32bit systems (can
be done as a separate PR).
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#1061 (comment)>, or mute
the thread
<https://github.com/notifications/unsubscribe-auth/AS5pCs6qQXqUVg2TMdvV-CipN6N3INZ5ks5sJP4RgaJpZM4OFzFY>
.
|
Please note that such a PR exists already but is currently not worked on
as 32 bit compatibility is not high priority for test-gen.
#987
The above fix is problematic as it will not allow creation of many
objects, and even for 32 bits 64 bit adressing should be used. But this
requires a more complex rewrite.
|
@eigold could you please change the PR, so that it does not contain the change to |
acf1da9
to
e46a320
Compare
@eigold, any progress on this? |
Yes. I have made the change as a separate commit. It shows when
I run 'git log' on my computer but for some reason github shows only
the first commit for this branch.
Eugene
…On Mon, Jul 3, 2017 at 3:30 PM, Peter Schrammel ***@***.***> wrote:
@eigold <https://github.com/eigold>, any progress on this?
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#1061 (comment)>, or mute
the thread
<https://github.com/notifications/unsubscribe-auth/AS5pCjr4kgmi903HF8KA_AGDdl3qvKq1ks5sKUFMgaJpZM4OFzFY>
.
|
@eigold as one of the last commits says "starting a new branch" could it be that the newer commit are simply in a different, new branch? Only commits pushed to |
When I run 'git branch' in ~/test-gen/lib/cbmc it shows
* feature/hexadecimal_float_output_in_expr2java
master
The last two commits that I get after running 'git log'
in ~/test-gen/lib/cbmc are shown below.
Date: Mon Jul 3 05:54:01 2017 -0400
removing an accidental change
commit e46a320de0eaf8c99c4dd485448a25a764d6986d
Author: eigold <[email protected]>
Date: Mon Jun 26 16:05:48 2017 -0400
starting a new branch to use hexadecimal floating point numbers in
tests (amended)
commit 05875e1
…On Mon, Jul 3, 2017 at 4:50 PM, Matthias Güdemann ***@***.***> wrote:
@eigold <https://github.com/eigold> as one of the last commits says
"starting a new branch" could it be that the newer commit are simply in a
different, new branch? Only commits pushed to eigold:feature/hexadecimal_
float_output_in_expr2java will appear here
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#1061 (comment)>, or mute
the thread
<https://github.com/notifications/unsubscribe-auth/AS5pCisK9OE7O6sh42PJzNbLcLStPJUCks5sKVQVgaJpZM4OFzFY>
.
|
@eigold all these commits are shown on github then. You just have to scroll down, "removing and accidental change" is just right in front of Peter's last comment |
Oops. You are right. I got distracted with the work on ebmc release and
forgot that I gave the same names to the branches of test-gen and
a fork of cbmc. I was actually checking the status of the former that
indeed has not changed. Sorry.
Eugene
…On Mon, Jul 3, 2017 at 6:27 PM, Matthias Güdemann ***@***.***> wrote:
@eigold <https://github.com/eigold> all these commits are shown on github
then. You just have to scroll down, "removing and accidental change" is
just right in front of Peter's last comment
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#1061 (comment)>, or mute
the thread
<https://github.com/notifications/unsubscribe-auth/AS5pCuyhqiDtCiXY-Nt-gKNaWwOm575Oks5sKWrJgaJpZM4OFzFY>
.
|
src/java_bytecode/expr2java.cpp
Outdated
if(ieee_repr.is_NaN()) | ||
result+="NaN"; | ||
else | ||
result+="inf"; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
for Java, this is Double/Float.NEGATIVE_INFINITY
or Double/Float.POSITIVE_INFINITY
(cf. https://docs.oracle.com/javase/7/docs/api/java/lang/Float.html)
src/java_bytecode/expr2java.cpp
Outdated
else | ||
result="+"; | ||
if(ieee_repr.is_NaN()) | ||
result+="NaN"; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
for Java, this is Float/Double.NaN
src/java_bytecode/expr2java.cpp
Outdated
std::stringstream buffer; | ||
buffer << std::hexfloat; | ||
buffer << D; | ||
if(float_flag) | ||
buffer << f_num << 'f'; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
please simplify to buffer << ieee_repr.to_float() << 'f';
src/java_bytecode/expr2java.cpp
Outdated
if(float_flag) | ||
buffer << f_num << 'f'; | ||
else | ||
buffer << d_num; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
as above
src/java_bytecode/expr2java.cpp
Outdated
std::stringstream buffer; | ||
buffer << std::hexfloat; | ||
buffer << D; | ||
if(float_flag) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
nitpick, explicit bool
is not needed, if(src.type()==java_float_type())
would be enough
Matthias,
. . .
please simplify to buffer << ieee_repr.to_float() << 'f';
...
I simplified the code as you suggested.
I missed the point of references to Java functions
for checking NaN and Infinity.
…On Thu, Jul 6, 2017 at 3:31 AM, Matthias Güdemann ***@***.***> wrote:
***@***.**** requested changes on this pull request.
------------------------------
In src/java_bytecode/expr2java.cpp
<#1061 (comment)>:
> - double D = Fpn.to_double();
+ else if((src.type()==java_float_type()) ||
+ (src.type()==java_double_type()))
+ {
+ ieee_floatt ieee_repr(to_constant_expr(src));
+ if(ieee_repr.is_NaN() || ieee_repr.is_infinity())
+ {
+ std::string result;
+ if(ieee_repr.get_sign())
+ result="-";
+ else
+ result="+";
+ if(ieee_repr.is_NaN())
+ result+="NaN";
+ else
+ result+="inf";
for Java, this is Double/Float.NEGATIVE_INFINITY or
Double/Float.POSITIVE_INFINITY
(cf. https://docs.oracle.com/javase/7/docs/api/java/lang/Float.html)
------------------------------
In src/java_bytecode/expr2java.cpp
<#1061 (comment)>:
> - else if (src.type() == java_double_type()) {
- ieee_floatt Fpn(to_constant_expr(src));
- double D = Fpn.to_double();
+ else if((src.type()==java_float_type()) ||
+ (src.type()==java_double_type()))
+ {
+ ieee_floatt ieee_repr(to_constant_expr(src));
+ if(ieee_repr.is_NaN() || ieee_repr.is_infinity())
+ {
+ std::string result;
+ if(ieee_repr.get_sign())
+ result="-";
+ else
+ result="+";
+ if(ieee_repr.is_NaN())
+ result+="NaN";
for Java, this is Float/Double.NaN
------------------------------
In src/java_bytecode/expr2java.cpp
<#1061 (comment)>:
> std::stringstream buffer;
buffer << std::hexfloat;
- buffer << D;
+ if(float_flag)
+ buffer << f_num << 'f';
please simplify to buffer << ieee_repr.to_float() << 'f';
------------------------------
In src/java_bytecode/expr2java.cpp
<#1061 (comment)>:
> std::stringstream buffer;
buffer << std::hexfloat;
- buffer << D;
+ if(float_flag)
+ buffer << f_num << 'f';
+ else
+ buffer << d_num;
as above
------------------------------
In src/java_bytecode/expr2java.cpp
<#1061 (comment)>:
> std::stringstream buffer;
buffer << std::hexfloat;
- buffer << D;
+ if(float_flag)
nitpick, explicit bool is not needed, if(src.type()==java_float_type())
would be enough
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#1061 (review)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AS5pCjQqn_1Y5TI5U0fKrIIrO5EFxkEdks5sLI1jgaJpZM4OFzFY>
.
|
Hi Eugene,
I missed the point of references to Java functions
for checking NaN and Infinity.
this function emits Java code, therefore it should emit valid Java.
```
float f = Float.POSITIVE_INFINITY;
```
is valid, while
```
float f = +inf;
```
is not, but this would currently be generated.
These special numbers are all defines as static members of either
`java.lang.Float` or `java.lang.Double`.
Best,
Matthias
|
I see.
Note that this has nothing to do with outputting floating point numbers
in the hexadecimal form. I commented out the code I added and ran java
programs where one has to go beyond regular floating point numbers to
reach some lines.
The test generator produced tests where value +NAN, -NAN, -INFINITY,
+INFINITY were assigned (that is tests that would not compile).
So, this PR should count as two :-)
…On Thu, Jul 6, 2017 at 8:25 AM, Matthias Güdemann ***@***.***> wrote:
Hi Eugene,
> I missed the point of references to Java functions
> for checking NaN and Infinity.
this function emits Java code, therefore it should emit valid Java.
```
float f = Float.POSITIVE_INFINITY;
```
is valid, while
```
float f = +inf;
```
is not, but this would currently be generated.
These special numbers are all defines as static members of either
`java.lang.Float` or `java.lang.Double`.
Best,
Matthias
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#1061 (comment)>, or mute
the thread
<https://github.com/notifications/unsubscribe-auth/AS5pCt-7EmOgOyOE-JbNqE4ukyTkIf8dks5sLNIygaJpZM4OFzFY>
.
|
Hi Eugene,
Note that this has nothing to do with outputting floating point numbers
in the hexadecimal form. I commented out the code I added and ran java
programs where one has to go beyond regular floating point numbers to
reach some lines.
The test generator produced tests where value +NAN, -NAN, -INFINITY,
+INFINITY were assigned (that is tests that would not compile).
I fear I cannot follow you here.
What I did was to checkout your branch in `lib/cbmc` and run
test-generator on a test that requires NaN to reach a location. What I
got was the following test-case
```
/*
* This test covers `boolean f(float)' block 2 (line 4)
*/
@org.junit.Test
public void nan_tst_f_a5f1433ea6d903e6_001() throws Throwable {
boolean retval;
{
/* initialize test parameters */
nan_tst param_1 = (nan_tst) Reflector.getInstance("nan_tst");
float arg1f = -NaN;
/* call function under test */
retval = param_1.f(arg1f);
}
{
/* check return value */
java.lang.Object expected_return_value;
expected_return_value = true;
CompareWithFieldList.compare(expected_return_value, retval);
}
}
```
Which is not valid Java.
I think ew should have `arg1f = -Float.NaN;` here. It is possible to
give hex values for +-inf/nan too, but that would not make much sense.
I'd also prefer to have `0` if zero is exactly represented (via
`is_zero` as you mentioned earlier).
Best,
Matthias
|
Right. And if you comment out the code I have added you should get
float arg1f = -NAN;
(instead of float arg1f = -NaN; )
That is currently (i.e. even without the patch I have added) test-gen
generates incorrect values for java tests if a non-number or Infinity is
involved.
For instance, it assigns -NAN instead of Float.NaN.
That is all I am saying.
Eugene
…On Thu, Jul 6, 2017 at 10:23 AM, Matthias Güdemann ***@***.*** > wrote:
Hi Eugene,
> Note that this has nothing to do with outputting floating point numbers
> in the hexadecimal form. I commented out the code I added and ran java
> programs where one has to go beyond regular floating point numbers to
> reach some lines.
> The test generator produced tests where value +NAN, -NAN, -INFINITY,
> +INFINITY were assigned (that is tests that would not compile).
I fear I cannot follow you here.
What I did was to checkout your branch in `lib/cbmc` and run
test-generator on a test that requires NaN to reach a location. What I
got was the following test-case
```
/*
* This test covers `boolean f(float)' block 2 (line 4)
*/
@org.junit.Test
public void nan_tst_f_a5f1433ea6d903e6_001() throws Throwable {
boolean retval;
{
/* initialize test parameters */
nan_tst param_1 = (nan_tst) Reflector.getInstance("nan_tst");
float arg1f = -NaN;
/* call function under test */
retval = param_1.f(arg1f);
}
{
/* check return value */
java.lang.Object expected_return_value;
expected_return_value = true;
CompareWithFieldList.compare(expected_return_value, retval);
}
}
```
Which is not valid Java.
I think ew should have `arg1f = -Float.NaN;` here. It is possible to
give hex values for +-inf/nan too, but that would not make much sense.
I'd also prefer to have `0` if zero is exactly represented (via
`is_zero` as you mentioned earlier).
Best,
Matthias
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#1061 (comment)>, or mute
the thread
<https://github.com/notifications/unsubscribe-auth/AS5pCgY_RcM5Wc69B8qnT7B6rdgkuGG5ks5sLO3bgaJpZM4OFzFY>
.
|
Right. And if you comment out the code I have added you should get
float arg1f = -NAN;
which is because it falls back to expr2c, right? Which is using the NAN
macro as output for NaN.
(instead of float arg1f = -NaN; )
That is currently (i.e. even without the patch I have added) test-gen
generates incorrect values for java tests if a non-number or Infinity is
involved.
yes, which is why we want your PR to correct this problem :-)
I'd say now mostly the only necessary change is from "NaN" to
"Float.NaN" or "Double.NaN" and do the case distinction for
"Double/Float.NEGATIVE/POSITIVE_INFINITY", then is should all be
set. Other hexadecimal float output should be ok with using `std::hex`.
Best,
Matthias
|
Probably, it makes sense to add three more regression tests to cover
all three special cases: non-number, infinity, and clean zero?
…On Thu, Jul 6, 2017 at 10:53 AM, Matthias Güdemann ***@***.*** > wrote:
> Right. And if you comment out the code I have added you should get
>
> float arg1f = -NAN;
which is because it falls back to expr2c, right? Which is using the NAN
macro as output for NaN.
> (instead of float arg1f = -NaN; )
>
> That is currently (i.e. even without the patch I have added) test-gen
> generates incorrect values for java tests if a non-number or Infinity is
> involved.
yes, which is why we want your PR to correct this problem :-)
I'd say now mostly the only necessary change is from "NaN" to
"Float.NaN" or "Double.NaN" and do the case distinction for
"Double/Float.NEGATIVE/POSITIVE_INFINITY", then is should all be
set. Other hexadecimal float output should be ok with using `std::hex`.
Best,
Matthias
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#1061 (comment)>, or mute
the thread
<https://github.com/notifications/unsubscribe-auth/AS5pCk00voF1_Yk13fOdD2eoUN3seb7Wks5sLPUBgaJpZM4OFzFY>
.
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM, please squash commits
removed an accidental change, added code to process special cases: NaN and infiinity made required simplications, made corrections in treatment of special cases
664cda2
to
9b2e643
Compare
Done.
…On Wed, Jul 12, 2017 at 3:37 PM, Matthias Güdemann ***@***.*** > wrote:
***@***.**** commented on this pull request.
LGTM, please squash commits
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#1061 (review)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AS5pCjBAi0YorMRDfsFneYCkfECIkg_oks5sNSCFgaJpZM4OFzFY>
.
|
obsoleted by #1216 |
No description provided.