Commit 0fe2dd8
authored
Rollup merge of rust-lang#143906 - LorrensP-2158466:miri-float-nondet-foreign-items, r=RalfJung
Miri: non-deterministic floating point operations in `foreign_items`
Part of [rust-lang/miri/rust-lang#3555](rust-lang/miri#3555 (comment)), this pr does the `foreign_items` work.
Some things have changed since rust-lang#138062 and rust-lang#142514. I moved the "helpers" used for creating fixed outputs and clamping operations to their defined ranges to `math.rs`. These are now also extended to handle the floating-point operations in `foreign_items`. Tests in `miri/tests/float.rs` were changed/added.
Failing tests in `std` were extracted, run under miri with `-Zmiri-many-seeds=0..1000` and changed accordingly. Double checked with `-Zmiri-many-seeds`.
I noticed that the C standard doesn't specify the output ranges for all of its mathematical operations; it just specifies them as:
```
Returns
The sinh functions return sinh x.
```
So I used [Wolfram|Alpha](https://www.wolframalpha.com/).4 files changed
+35
-35
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1936 | 1936 | | |
1937 | 1937 | | |
1938 | 1938 | | |
1939 | | - | |
1940 | | - | |
| 1939 | + | |
| 1940 | + | |
1941 | 1941 | | |
1942 | 1942 | | |
1943 | 1943 | | |
| |||
1982 | 1982 | | |
1983 | 1983 | | |
1984 | 1984 | | |
1985 | | - | |
| 1985 | + | |
1986 | 1986 | | |
1987 | 1987 | | |
1988 | 1988 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
582 | 582 | | |
583 | 583 | | |
584 | 584 | | |
585 | | - | |
586 | | - | |
| 585 | + | |
| 586 | + | |
587 | 587 | | |
588 | 588 | | |
589 | 589 | | |
| |||
621 | 621 | | |
622 | 622 | | |
623 | 623 | | |
624 | | - | |
| 624 | + | |
625 | 625 | | |
626 | 626 | | |
627 | 627 | | |
| |||
652 | 652 | | |
653 | 653 | | |
654 | 654 | | |
655 | | - | |
| 655 | + | |
656 | 656 | | |
657 | 657 | | |
658 | 658 | | |
| |||
725 | 725 | | |
726 | 726 | | |
727 | 727 | | |
728 | | - | |
| 728 | + | |
729 | 729 | | |
730 | 730 | | |
731 | 731 | | |
| |||
749 | 749 | | |
750 | 750 | | |
751 | 751 | | |
752 | | - | |
| 752 | + | |
753 | 753 | | |
754 | 754 | | |
755 | | - | |
| 755 | + | |
756 | 756 | | |
757 | | - | |
| 757 | + | |
758 | 758 | | |
759 | 759 | | |
760 | 760 | | |
| |||
813 | 813 | | |
814 | 814 | | |
815 | 815 | | |
816 | | - | |
| 816 | + | |
817 | 817 | | |
818 | 818 | | |
819 | 819 | | |
| |||
854 | 854 | | |
855 | 855 | | |
856 | 856 | | |
857 | | - | |
858 | | - | |
| 857 | + | |
| 858 | + | |
859 | 859 | | |
860 | 860 | | |
861 | 861 | | |
| |||
884 | 884 | | |
885 | 885 | | |
886 | 886 | | |
887 | | - | |
888 | | - | |
| 887 | + | |
| 888 | + | |
889 | 889 | | |
890 | 890 | | |
891 | 891 | | |
| |||
982 | 982 | | |
983 | 983 | | |
984 | 984 | | |
985 | | - | |
| 985 | + | |
986 | 986 | | |
987 | 987 | | |
988 | 988 | | |
| |||
1012 | 1012 | | |
1013 | 1013 | | |
1014 | 1014 | | |
1015 | | - | |
| 1015 | + | |
1016 | 1016 | | |
1017 | 1017 | | |
1018 | 1018 | | |
| |||
1042 | 1042 | | |
1043 | 1043 | | |
1044 | 1044 | | |
1045 | | - | |
| 1045 | + | |
1046 | 1046 | | |
1047 | 1047 | | |
1048 | 1048 | | |
| |||
1067 | 1067 | | |
1068 | 1068 | | |
1069 | 1069 | | |
1070 | | - | |
| 1070 | + | |
1071 | 1071 | | |
1072 | 1072 | | |
1073 | 1073 | | |
| |||
1125 | 1125 | | |
1126 | 1126 | | |
1127 | 1127 | | |
1128 | | - | |
| 1128 | + | |
1129 | 1129 | | |
1130 | 1130 | | |
1131 | 1131 | | |
| |||
1153 | 1153 | | |
1154 | 1154 | | |
1155 | 1155 | | |
1156 | | - | |
| 1156 | + | |
1157 | 1157 | | |
1158 | 1158 | | |
1159 | 1159 | | |
| |||
1248 | 1248 | | |
1249 | 1249 | | |
1250 | 1250 | | |
1251 | | - | |
| 1251 | + | |
1252 | 1252 | | |
1253 | 1253 | | |
1254 | 1254 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
749 | 749 | | |
750 | 750 | | |
751 | 751 | | |
752 | | - | |
| 752 | + | |
753 | 753 | | |
754 | 754 | | |
755 | | - | |
| 755 | + | |
756 | 756 | | |
757 | | - | |
| 757 | + | |
758 | 758 | | |
759 | 759 | | |
760 | 760 | | |
| |||
1153 | 1153 | | |
1154 | 1154 | | |
1155 | 1155 | | |
1156 | | - | |
| 1156 | + | |
1157 | 1157 | | |
1158 | 1158 | | |
1159 | 1159 | | |
| |||
1248 | 1248 | | |
1249 | 1249 | | |
1250 | 1250 | | |
1251 | | - | |
| 1251 | + | |
1252 | 1252 | | |
1253 | 1253 | | |
1254 | 1254 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
79 | 79 | | |
80 | 80 | | |
81 | 81 | | |
82 | | - | |
| 82 | + | |
83 | 83 | | |
84 | 84 | | |
85 | 85 | | |
| |||
140 | 140 | | |
141 | 141 | | |
142 | 142 | | |
143 | | - | |
| 143 | + | |
144 | 144 | | |
145 | 145 | | |
146 | | - | |
| 146 | + | |
147 | 147 | | |
148 | 148 | | |
149 | 149 | | |
| |||
196 | 196 | | |
197 | 197 | | |
198 | 198 | | |
199 | | - | |
200 | | - | |
| 199 | + | |
| 200 | + | |
201 | 201 | | |
202 | | - | |
| 202 | + | |
203 | 203 | | |
204 | 204 | | |
205 | 205 | | |
| |||
218 | 218 | | |
219 | 219 | | |
220 | 220 | | |
221 | | - | |
| 221 | + | |
222 | 222 | | |
223 | 223 | | |
224 | 224 | | |
| |||
0 commit comments