Skip to content

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

Merged
Dudeldu merged 4 commits intomasterfrom
c-impl
Jun 15, 2022
Merged

Implement float operators in C / Support Float and Double#10
Dudeldu merged 4 commits intomasterfrom
c-impl

Conversation

@Dudeldu
Copy link
Copy Markdown
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

FelixKrayer
FelixKrayer reviewed Jun 4, 2022
View reviewed changes
@Dudeldu Dudeldu requested a review from FelixKrayer June 7, 2022 19:51
brgr
brgr reviewed Jun 9, 2022
View reviewed changes
@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
Copy Markdown
Collaborator

FelixKrayer commented Jun 10, 2022

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
Copy Markdown
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
Copy Markdown
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

@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
Copy Markdown
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 added 4 commits June 14, 2022 17:00
@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
Copy Markdown
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