|
| 1 | +// PARAM: --set "ana.activated[+]" ocaml --set "mainfun[+]" "UNARY_OP" --set "mainfun[+]" "BINARY_OP" --set "mainfun[+]" "atof_double" --set "mainfun[+]" "atof_float" --set "mainfun[+]" "max_float" --set "mainfun[+]" "smallest_float" --set "mainfun[+]" "pi_float" --disable warn.imprecise --set "exp.extraspecials[+]" printInt |
| 2 | + |
| 3 | +// Code from stubs.c in src/common/cdomains/floatOps that should be correct despite missing CAMLparam, as discussed in https://github.com/goblint/analyzer/issues/1371. |
| 4 | + |
| 5 | +/* A small definition of the LXM state so sizeof works - from AI */ |
| 6 | +//struct LXM_state { uint64_t a; uint64_t x[2]; uint64_t s; }; |
| 7 | + |
| 8 | +/* Minimal macros to mimic expected behaviour */ |
| 9 | +#define Wsizeof(ty) ((sizeof(ty) + sizeof(value) - 1) / sizeof(value)) |
| 10 | +#define LXM_val(v) ((struct LXM_state *) Data_abstract_val(v)) |
| 11 | + |
| 12 | +#define CAMLparam1(x) __goblint_caml_param1(&x) |
| 13 | +#define CAMLreturn(x) return (x) // From AI - CAMLreturn needs some variable named caml__frame, which is not available in our mock CAMLparam1, so we mock the return as well. |
| 14 | + |
| 15 | + |
| 16 | +#define _GNU_SOURCE // necessary for M_PI to be defined |
| 17 | +#include <stdio.h> |
| 18 | +#include <math.h> |
| 19 | +#include <float.h> |
| 20 | +#include <fenv.h> |
| 21 | +#include <assert.h> |
| 22 | +#include <caml/mlvalues.h> |
| 23 | +#include <caml/alloc.h> |
| 24 | + |
| 25 | +// Order must match with round_mode in floatOps.ml |
| 26 | +enum round_mode |
| 27 | +{ |
| 28 | + Nearest, |
| 29 | + ToZero, |
| 30 | + Up, |
| 31 | + Down |
| 32 | +}; |
| 33 | + |
| 34 | +static void change_round_mode(int mode) |
| 35 | +{ |
| 36 | + switch (mode) |
| 37 | + { |
| 38 | + case Nearest: |
| 39 | + fesetround(FE_TONEAREST); |
| 40 | + break; |
| 41 | + case ToZero: |
| 42 | + fesetround(FE_TOWARDZERO); |
| 43 | + break; |
| 44 | + case Up: |
| 45 | + fesetround(FE_UPWARD); |
| 46 | + break; |
| 47 | + case Down: |
| 48 | + fesetround(FE_DOWNWARD); |
| 49 | + break; |
| 50 | + default: |
| 51 | + // Assert ignored to focus on the OCaml stubs. |
| 52 | + assert(0); // FAIL |
| 53 | + break; |
| 54 | + } |
| 55 | +} |
| 56 | + |
| 57 | +#define UNARY_OP(name, type, op) \ |
| 58 | + CAMLprim value name##_##type(value mode, value x) \ |
| 59 | + { \ |
| 60 | + /* No need to use CAMLparam to keep mode and x as GC roots, |
| 61 | + because next GC poll point is at allocation in caml_copy_double. |
| 62 | + We have already read their values by then. */ \ |
| 63 | + int old_roundingmode = fegetround(); \ |
| 64 | + change_round_mode(Int_val(mode)); \ |
| 65 | + volatile type r, x1 = Double_val(x); \ |
| 66 | + r = op(x1); \ |
| 67 | + fesetround(old_roundingmode); \ |
| 68 | + return caml_copy_double(r); /* NOWARN */ \ |
| 69 | + /* No need to use CAMLreturn because we don't use CAMLparam. */ \ |
| 70 | + } |
| 71 | + |
| 72 | +UNARY_OP(sqrt, double, sqrt); |
| 73 | +UNARY_OP(sqrt, float, sqrtf); |
| 74 | +UNARY_OP(acos, double, acos); |
| 75 | +UNARY_OP(acos, float, acosf); |
| 76 | +UNARY_OP(asin, double, asin); |
| 77 | +UNARY_OP(asin, float, asinf); |
| 78 | +UNARY_OP(atan, double, atan); |
| 79 | +UNARY_OP(atan, float, atanf); |
| 80 | +UNARY_OP(cos, double, cos); |
| 81 | +UNARY_OP(cos, float, cosf); |
| 82 | +UNARY_OP(sin, double, sin); |
| 83 | +UNARY_OP(sin, float, sinf); |
| 84 | +UNARY_OP(tan, double, tan); |
| 85 | +UNARY_OP(tan, float, tanf); |
| 86 | + |
| 87 | +#define BINARY_OP(name, type, op) \ |
| 88 | + CAMLprim value name##_##type(value mode, value x, value y) \ |
| 89 | + { \ |
| 90 | + /* No need to use CAMLparam to keep mode, x and y as GC roots, |
| 91 | + because next GC poll point is at allocation in caml_copy_double. |
| 92 | + We have already read their values by then. */ \ |
| 93 | + int old_roundingmode = fegetround(); \ |
| 94 | + change_round_mode(Int_val(mode)); \ |
| 95 | + volatile type r, x1 = Double_val(x), y1 = Double_val(y); \ |
| 96 | + r = x1 op y1; \ |
| 97 | + fesetround(old_roundingmode); \ |
| 98 | + return caml_copy_double(r); /* NOWARN */ \ |
| 99 | + /* No need to use CAMLreturn because we don't use CAMLparam. */ \ |
| 100 | + } |
| 101 | + |
| 102 | +BINARY_OP(add, double, +); |
| 103 | +BINARY_OP(add, float, +); |
| 104 | +BINARY_OP(sub, double, -); |
| 105 | +BINARY_OP(sub, float, -); |
| 106 | +BINARY_OP(mul, double, *); |
| 107 | +BINARY_OP(mul, float, *); |
| 108 | +BINARY_OP(div, double, /); |
| 109 | +BINARY_OP(div, float, /); |
| 110 | + |
| 111 | +CAMLprim value atof_double(value mode, value str) |
| 112 | +{ |
| 113 | + // No need to use CAMLparam to keep mode and str as GC roots, |
| 114 | + // because next GC poll point is at allocation in caml_copy_double. |
| 115 | + // We have already read their values by then. |
| 116 | + const char *s = String_val(str); |
| 117 | + volatile double r; |
| 118 | + int old_roundingmode = fegetround(); |
| 119 | + change_round_mode(Int_val(mode)); |
| 120 | + r = atof(s); |
| 121 | + fesetround(old_roundingmode); |
| 122 | + return caml_copy_double(r); // NOWARN |
| 123 | + // No need to use CAMLreturn because we don't use CAMLparam. |
| 124 | +} |
| 125 | + |
| 126 | +CAMLprim value atof_float(value mode, value str) |
| 127 | +{ |
| 128 | + // No need to use CAMLparam to keep mode and str as GC roots, |
| 129 | + // because next GC poll point is at allocation in caml_copy_double. |
| 130 | + // We have already read their values by then. |
| 131 | + const char *s = String_val(str); // Despite not being a value, this is a pointer into the OCaml heap and needs to be checked against GC. Doubles are also pointers. |
| 132 | + volatile float r; |
| 133 | + int old_roundingmode = fegetround(); // NOWARN |
| 134 | + change_round_mode(Int_val(mode)); // This makes a copy of the mode and no problems will arise. |
| 135 | + r = (float)atof(s); |
| 136 | + fesetround(old_roundingmode); |
| 137 | + return caml_copy_double(r); // NOWARN |
| 138 | + // No need to use CAMLreturn because we don't use CAMLparam. |
| 139 | +} |
| 140 | + |
| 141 | +// These are only given for floats as these operations involve no rounding and their OCaml implementation (Float module) can be used |
| 142 | + |
| 143 | +CAMLprim value max_float(value unit) |
| 144 | +{ |
| 145 | + // No need to use CAMLparam to keep unit as GC root, |
| 146 | + // because we don't use it. |
| 147 | + return caml_copy_double(FLT_MAX); // NOWARN |
| 148 | + // No need to use CAMLreturn because we don't use CAMLparam. |
| 149 | +} |
| 150 | + |
| 151 | +CAMLprim value smallest_float(value unit) |
| 152 | +{ |
| 153 | + // No need to use CAMLparam to keep unit as GC root, |
| 154 | + // because we don't use it. |
| 155 | + return caml_copy_double(FLT_MIN); // NOWARN |
| 156 | + // No need to use CAMLreturn because we don't use CAMLparam. |
| 157 | +} |
| 158 | + |
| 159 | +CAMLprim value pi_float(value unit) |
| 160 | +{ |
| 161 | + return caml_copy_double(M_PI); // NOWARN |
| 162 | +} |
0 commit comments