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

Implement float operators in C / Support Float and Double #10

Merged
merged 4 commits into from
Jun 15, 2022
Merged

Implement float operators in C / Support Float and Double #10

merged 4 commits into from
Jun 15, 2022

Conversation

Dudeldu
Copy link
Owner

@Dudeldu Dudeldu commented Jun 4, 2022 •
edited
Loading

This fixes multiple issues:

  • it reimplements ocaml round -> therefore we can get ride of the external dependency
  • it exposes c's atof to ocaml to make string parsing possible
  • all the operations are possible for floats and doubles and a uniform interface is provided for both
  • it would now also be fairly simple to "out-source" other functions to c like sqrt, log, cos, sin etc.
  • we now support at least the two float kinds Float and Double
  • adjusts the casting in forward evaluation as well as backwards (invariant) and also fixes some rounding issues in invariant generally
  • introduces yet another module layer to store the ftype information
  • extends the regression and unit tests to also test for floats

Builds on #9

@Dudeldu Dudeldu requested a review from FelixKrayer June 7, 2022 19:51
brgr
brgr reviewed Jun 9, 2022
View reviewed changes
src/cdomains/floatDomain.ml Outdated Show resolved Hide resolved
@Dudeldu Dudeldu changed the title Implement float operators in C Implement float operators in C / Support Float and Double Jun 9, 2022
@Dudeldu Dudeldu changed the title Implement float operators in C / Support Float and Double WIP: Implement float operators in C / Support Float and Double Jun 9, 2022
@FelixKrayer
Copy link
Collaborator

Could you please also include a min_value function (You can of course choose a different name for it)?
min_value is actually the least Float, that is not a subnormal and I will need it for implementing the __builtin_isnormal function (to check if the interval may contain subnormals).
Alternatively classify_float should also work, but min_value (or similar) would be nicer for me

@Dudeldu Dudeldu changed the title WIP: Implement float operators in C / Support Float and Double Implement float operators in C / Support Float and Double Jun 10, 2022
@Dudeldu
Copy link
Owner Author

Dudeldu commented Jun 10, 2022 •
edited
Loading

This should now be covered by smallest, i guess. But the setup also allows extending the interface and adding new c methods easily. Most of the __builtin_*** could then also be outsourced to "real" c and do not require reassembling them inside ocaml

@Dudeldu Dudeldu requested a review from brgr June 10, 2022 15:17
FelixKrayer
FelixKrayer previously approved these changes Jun 13, 2022
View reviewed changes
Copy link
Collaborator

@FelixKrayer FelixKrayer left a comment

Choose a reason for hiding this comment

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

Looks good

src/cdomains/valueDomain.ml Outdated Show resolved Hide resolved
@FelixKrayer FelixKrayer mentioned this pull request Jun 13, 2022
Merged
@Dudeldu Dudeldu requested a review from FelixKrayer June 13, 2022 08:08
FelixKrayer
FelixKrayer previously approved these changes Jun 13, 2022
View reviewed changes
Copy link
Collaborator

@FelixKrayer FelixKrayer left a comment

Choose a reason for hiding this comment

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

⊤

@Dudeldu
Support FFloat and FDouble
96e2360 
- Implement float operators in C
- Support FFloat and FDouble
@Dudeldu
Add tests
a4dae22
@Dudeldu
Allow using DBL_MIN, DBL_MAX
f6a5b03 
Some compilers specifiy DBL_MIN, DBL_MAX as long double.
As we do not support long double in neither cil nor goblint itself,
 but want to use DBL_MIN, DBL_MAX we have no other option than to explicitly check for this one case
@Dudeldu
Improve match patterns
e45a009
brgr
brgr approved these changes Jun 14, 2022
View reviewed changes
Copy link
Collaborator

@brgr brgr left a comment

Choose a reason for hiding this comment

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

Please for the next time smaller more separated PRs would be really appreaciated ^^ But looks really good!

@Dudeldu Dudeldu requested a review from FelixKrayer June 15, 2022 05:56
@Dudeldu Dudeldu merged commit eadd02f into master Jun 15, 2022
@Dudeldu Dudeldu mentioned this pull request Jun 15, 2022
Merged
brgr pushed a commit that referenced this pull request Jun 16, 2022
@Dudeldu @brgr
Implement float operators in C / Support Float and Double (#10)
1d72a2a 
* Support FFloat and FDouble
- Implement float operators in C
- Support FFloat and FDouble

* Allow using DBL_MIN, DBL_MAX
Some compilers specifiy DBL_MIN, DBL_MAX as long double.
As we do not support long double in neither cil nor goblint itself, but want to use DBL_MIN, DBL_MAX, we have no other option than to explicitly check for this two cases
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@brgr brgr brgr approved these changes

@FelixKrayer FelixKrayer FelixKrayer approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@Dudeldu @FelixKrayer @brgr