From a79eb9aff52ca0f940f88d7ab741bd87026f0e61 Mon Sep 17 00:00:00 2001 From: FelixKrayer Date: Mon, 25 Jul 2022 17:40:30 +0200 Subject: [PATCH 01/24] Add math_funeval option and better abstractions using c-stubs --- src/cdomains/floatDomain.ml | 104 ++++++++++++++++--- src/cdomains/floatOps/floatOps.ml | 22 ++++ src/cdomains/floatOps/floatOps.mli | 6 ++ src/cdomains/floatOps/stubs.c | 12 +++ src/common/util/options.schema.json | 7 ++ tests/regression/57-floats/22-math-funeval.c | 67 ++++++++++++ 6 files changed, 205 insertions(+), 13 deletions(-) create mode 100644 tests/regression/57-floats/22-math-funeval.c diff --git a/src/cdomains/floatDomain.ml b/src/cdomains/floatDomain.ml index 39d3744401..0a61a74c9a 100644 --- a/src/cdomains/floatDomain.ml +++ b/src/cdomains/floatDomain.ml @@ -618,8 +618,74 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct | (l, _) when l > Float_t.zero -> false_zero_IInt () | _ -> unknown_IInt () (**any interval containing zero has to fall in this case, because we do not distinguish between 0. and -0. *) - (**This Constant overapproximates pi to use as bounds for the return values of trigonometric functions *) + (**These constants over-/underpproximate pi *) let overapprox_pi = 3.1416 + let underapprox_pi = 3.1415 + + let trig_helper l h k = (** computes dist = distance, l'' = (l/(k*pi) % 10) - floor(l/(k*pi)), h'' = (h/(k*pi)) - floor(h/(k*pi))*) + let ft_over_kpi = (Float_t.mul Up (Float_t.of_float Up k) (Float_t.of_float Up overapprox_pi)) in + let ft_under_kpi = (Float_t.mul Down (Float_t.of_float Down k) (Float_t.of_float Down underapprox_pi)) in + let l' = + if l >= Float_t.zero then (Float_t.div Down l ft_over_kpi) + else (Float_t.div Up l ft_under_kpi) + in + let h' = + if h >= Float_t.zero then (Float_t.div Up h ft_under_kpi) + else (Float_t.div Down h ft_over_kpi) + in + let dist = (Float_t.sub Up h' l') in + let l'' = + if l' >= Float_t.zero then + Float_t.sub Down l' (Float_t.of_float Down (Big_int_Z.float_of_big_int (Float_t.to_big_int l'))) + else + Float_t.sub Down l' (Float_t.of_float Down (Big_int_Z.float_of_big_int (IntOps.BigIntOps.sub (Float_t.to_big_int l') (Big_int_Z.big_int_of_int 1)))) + in + let h'' = + if h' >= Float_t.zero then + Float_t.sub Up h' (Float_t.of_float Up (Big_int_Z.float_of_big_int (Float_t.to_big_int h'))) + else + Float_t.sub Up h' (Float_t.of_float Up (Big_int_Z.float_of_big_int (IntOps.BigIntOps.sub (Float_t.to_big_int h') (Big_int_Z.big_int_of_int 1)))) + in + (dist, l'', h'') + + let eval_cos_cfun l h = + let (dist, l'', h'') = trig_helper l h 2. in + if Messages.tracing then Messages.trace "CstubsTrig" "sin: dist %s; l'' %s; h'' %s\n" (Float_t.to_string dist) (Float_t.to_string l'') (Float_t.to_string h''); + if dist <= (Float_t.of_float Down 0.5) && (h'' <= Float_t.of_float Up 0.5) && (h'' >= l'') then + Interval (Float_t.cos Down h, Float_t.cos Up l) + else if dist <= (Float_t.of_float Down 0.5) && (l'' >= Float_t.of_float Down 0.5) && (h'' >= l'') then + Interval (Float_t.cos Down l, Float_t.cos Up h) + else if dist <= (Float_t.of_float Down 1.) && (l'' <= h'') then + Interval (Float_t.of_float Down (-.1.), max (Float_t.cos Up l) (Float_t.cos Up h)) + else if dist <= (Float_t.of_float Down 1.) && (l'' >= Float_t.of_float Down 0.5) && (h'' <= Float_t.of_float Down 0.5) then + Interval (min (Float_t.cos Down l) (Float_t.cos Down h), Float_t.of_float Up 1.) + else + of_interval (-. 1., 1.) + + let eval_sin_cfun l h = + let (dist, l'', h'') = trig_helper l h 2. in + if Messages.tracing then Messages.trace "CstubsTrig" "cos: dist %s; l'' %s; h'' %s\n" (Float_t.to_string dist) (Float_t.to_string l'') (Float_t.to_string h''); + (* phase shift -0.25 -> same phase as cos *) + let l'' = if l'' <= Float_t.of_float Down 0.25 then Float_t.add Up l'' (Float_t.of_float Up 0.75) else Float_t.sub Down l'' (Float_t.of_float Up 0.25) in + let h'' = if h'' <= Float_t.of_float Down 0.25 then Float_t.add Up h'' (Float_t.of_float Up 0.75) else Float_t.sub Down h'' (Float_t.of_float Up 0.25) in + if dist <= (Float_t.of_float Down 0.5) && (h'' <= Float_t.of_float Up 0.5) && (h'' >= l'') then + Interval (Float_t.sin Down h, Float_t.sin Up l) + else if dist <= (Float_t.of_float Down 0.5) && (l'' >= Float_t.of_float Down 0.5) && (h'' >= l'') then + Interval (Float_t.sin Down l, Float_t.sin Up h) + else if dist <= (Float_t.of_float Down 1.) && (l'' <= h'') then + Interval (Float_t.of_float Down (-.1.), max (Float_t.sin Up l) (Float_t.sin Up h)) + else if dist <= (Float_t.of_float Down 1.) && (l'' >= Float_t.of_float Down 0.5) && (h'' <= Float_t.of_float Down 0.5) then + Interval (min (Float_t.sin Down l) (Float_t.sin Down h), Float_t.of_float Up 1.) + else + of_interval (-. 1., 1.) + + let eval_tan_cfun l h = + let (dist, l'', h'') = trig_helper l h 1. in + if Messages.tracing then Messages.trace "CstubsTrig" "tan: dist %s; l'' %s; h'' %s\n" (Float_t.to_string dist) (Float_t.to_string l'') (Float_t.to_string h''); + if dist <= (Float_t.of_float Down 1.) && Bool.not ((l'' <= Float_t.of_float Up 0.5) && (h'' >= Float_t.of_float Down 0.5)) then + Interval (Float_t.tan Down l, Float_t.tan Up h) + else + top () let eval_fabs = function | (l, h) when l > Float_t.zero -> Interval (l, h) @@ -644,33 +710,45 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct let eval_acos = function | (l, h) when l = h && l = Float_t.of_float Nearest 1. -> of_const 0. (*acos(1) = 0*) - | (l, h) -> - if l < (Float_t.of_float Down (-.1.)) || h > (Float_t.of_float Up 1.) then - Messages.warn ~category:Messages.Category.Float "Domain error might occur: acos argument might be outside of [-1., 1.]"; - of_interval (0., (overapprox_pi)) (**could be more exact *) + | (l, h) when l < (Float_t.of_float Down (-.1.)) || h > (Float_t.of_float Up 1.) -> + Messages.warn ~category:Messages.Category.Float "Domain error might occur: acos argument might be outside of [-1., 1.]"; + of_interval (0., (overapprox_pi)) + | (l, h) when GobConfig.get_bool "ana.float.math_funeval" -> + norm @@ Interval (Float_t.acos Down h, Float_t.acos Up l) (** acos is monotonic decreasing in [-1, 1]*) + | _ -> of_interval (0., (overapprox_pi)) let eval_asin = function | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*asin(0) = 0*) - | (l, h) -> - if l < (Float_t.of_float Down (-.1.)) || h > (Float_t.of_float Up 1.) then - Messages.warn ~category:Messages.Category.Float "Domain error might occur: asin argument might be outside of [-1., 1.]"; - div (of_interval ((-. overapprox_pi), overapprox_pi)) (of_const 2.) (**could be more exact *) + | (l, h) when l < (Float_t.of_float Down (-.1.)) || h > (Float_t.of_float Up 1.) -> + Messages.warn ~category:Messages.Category.Float "Domain error might occur: asin argument might be outside of [-1., 1.]"; + div (of_interval ((-. overapprox_pi), overapprox_pi)) (of_const 2.) + | (l, h) when GobConfig.get_bool "ana.float.math_funeval" -> + norm @@ Interval (Float_t.asin Down l, Float_t.asin Up h) (** asin is monotonic increasing in [-1, 1]*) + | _ -> div (of_interval ((-. overapprox_pi), overapprox_pi)) (of_const 2.) let eval_atan = function | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*atan(0) = 0*) - | _ -> div (of_interval ((-. overapprox_pi), overapprox_pi)) (of_const 2.) (**could be more exact *) + | (l, h) when GobConfig.get_bool "ana.float.math_funeval" -> + norm @@ Interval (Float_t.atan Down l, Float_t.atan Up h) (** atan is monotonic increasing*) + | _ -> div (of_interval ((-. overapprox_pi), overapprox_pi)) (of_const 2.) let eval_cos = function | (l, h) when l = h && l = Float_t.zero -> of_const 1. (*cos(0) = 1*) - | _ -> of_interval (-. 1., 1.) (**could be exact for intervals where l=h, or even for Interval intervals *) + | (l, h) when GobConfig.get_bool "ana.float.math_funeval" -> + norm @@ eval_cos_cfun l h + | _ -> of_interval (-. 1., 1.) let eval_sin = function | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*sin(0) = 0*) - | _ -> of_interval (-. 1., 1.) (**could be exact for intervals where l=h, or even for some intervals *) + | (l, h) when GobConfig.get_bool "ana.float.math_funeval" -> + norm @@ eval_sin_cfun l h + | _ -> of_interval (-. 1., 1.) let eval_tan = function | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*tan(0) = 0*) - | _ -> top () (**could be exact for intervals where l=h, or even for some intervals *) + | (l, h) when GobConfig.get_bool "ana.float.math_funeval" -> + norm @@ eval_tan_cfun l h + | _ -> top () let eval_sqrt = function | (l, h) when l = Float_t.zero && h = Float_t.zero -> of_const 0. diff --git a/src/cdomains/floatOps/floatOps.ml b/src/cdomains/floatOps/floatOps.ml index a4e39d930e..b73e7b424e 100644 --- a/src/cdomains/floatOps/floatOps.ml +++ b/src/cdomains/floatOps/floatOps.ml @@ -36,6 +36,14 @@ module type CFloatType = sig val mul: round_mode -> t -> t -> t val div: round_mode -> t -> t -> t val sqrt: round_mode -> t -> t + + val acos: round_mode -> t -> t + val asin: round_mode -> t -> t + val atan: round_mode -> t -> t + val cos: round_mode -> t -> t + val sin: round_mode -> t -> t + val tan: round_mode -> t -> t + val atof: round_mode -> string -> t end @@ -77,6 +85,13 @@ module CDouble = struct external div: round_mode -> t -> t -> t = "div_double" external sqrt: round_mode -> t -> t = "sqrt_double" + external acos: round_mode -> t -> t = "acos_double" + external asin: round_mode -> t -> t = "asin_double" + external atan: round_mode -> t -> t = "atan_double" + external cos: round_mode -> t -> t = "cos_double" + external sin: round_mode -> t -> t = "sin_double" + external tan: round_mode -> t -> t = "tan_double" + external atof: round_mode -> string -> t = "atof_double" end @@ -111,6 +126,13 @@ module CFloat = struct external div: round_mode -> t -> t -> t = "div_float" external sqrt: round_mode -> t -> t = "sqrt_float" + external acos: round_mode -> t -> t = "acos_float" + external asin: round_mode -> t -> t = "asin_float" + external atan: round_mode -> t -> t = "atan_float" + external cos: round_mode -> t -> t = "cos_float" + external sin: round_mode -> t -> t = "sin_float" + external tan: round_mode -> t -> t = "tan_float" + external atof: round_mode -> string -> t = "atof_float" let of_float mode x = add mode zero x diff --git a/src/cdomains/floatOps/floatOps.mli b/src/cdomains/floatOps/floatOps.mli index cf24f75ed5..75d0481822 100644 --- a/src/cdomains/floatOps/floatOps.mli +++ b/src/cdomains/floatOps/floatOps.mli @@ -39,6 +39,12 @@ module type CFloatType = sig val mul: round_mode -> t -> t -> t val div: round_mode -> t -> t -> t val sqrt: round_mode -> t -> t + val acos: round_mode -> t -> t + val asin: round_mode -> t -> t + val atan: round_mode -> t -> t + val cos: round_mode -> t -> t + val sin: round_mode -> t -> t + val tan: round_mode -> t -> t val atof: round_mode -> string -> t end diff --git a/src/cdomains/floatOps/stubs.c b/src/cdomains/floatOps/stubs.c index 50e4a2fb31..4489ef71e1 100644 --- a/src/cdomains/floatOps/stubs.c +++ b/src/cdomains/floatOps/stubs.c @@ -49,6 +49,18 @@ static void change_round_mode(int mode) UNARY_OP(sqrt, double, sqrt); UNARY_OP(sqrt, float, sqrtf); +UNARY_OP(acos, double, acos); +UNARY_OP(acos, float, acosf); +UNARY_OP(asin, double, asin); +UNARY_OP(asin, float, asinf); +UNARY_OP(atan, double, atan); +UNARY_OP(atan, float, atanf); +UNARY_OP(cos, double, cos); +UNARY_OP(cos, float, cosf); +UNARY_OP(sin, double, sin); +UNARY_OP(sin, float, sinf); +UNARY_OP(tan, double, tan); +UNARY_OP(tan, float, tanf); #define BINARY_OP(name, type, op) \ CAMLprim value name##_##type(value mode, value x, value y) \ diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json index 7c921c4f53..a3145d5469 100644 --- a/src/common/util/options.schema.json +++ b/src/common/util/options.schema.json @@ -463,6 +463,13 @@ "Use FloatDomain: (float * float) option.", "type": "boolean", "default": false + }, + "math_funeval": { + "title": "ana.float.math_funeval", + "description": + "Allow evaluation of functions from math.h with c-stubs. Only sound, if the same math.h implementation is used for the programm that is also used in Goblint", + "type": "boolean", + "default": false } }, "additionalProperties": false diff --git a/tests/regression/57-floats/22-math-funeval.c b/tests/regression/57-floats/22-math-funeval.c new file mode 100644 index 0000000000..51a9454fa8 --- /dev/null +++ b/tests/regression/57-floats/22-math-funeval.c @@ -0,0 +1,67 @@ +// PARAM: --enable ana.float.interval --enable ana.float.math_funeval +#include +#include +#include + +int main() +{ + int x; + double s1, s2, s3, c1, c2, sc1, sc2, t1, t2; + //s1: 0.5pi < [2.0, 7.5] < 2.5pi + //s2: 1.5pi < [5.0, 10.5] < 3.5pi + //s3: -0.5pi < [-1.0, -1.0] < 0.5pi + //c1: 0pi < [0.2, 6.1] < 2pi + //c2: pi < [3.3, 9.0] < 3pi + //sc1: 0.5pi < [2.0, 3.0] < pi + //sc2: 4.5pi < [14.5, 15.5] < 5pi + //t1: 0pi-0.1 <= [-0.1, -0.1] <= 0pi+0.1 + //t2: 6pi-0.1 < [18.8, 18.9] < 6pi+0.1 + if (x) { + s1 = 2.0; + s2 = 5.0; + s3 = -1.0; + c1 = 0.2; + c2 = 3.3; + sc1 = 2.0; + sc2 = 14.5; + t1 = -0.1; + t2 = 18.8; + } + else { + s1 = 7.5; + s2 = 10.5; + s3 = 1.0; + c1 = 6.1; + c2 = 9.0; + sc1 = 3.0; + sc2 = 15.5; + t1 = 0.1; + t2 = 18.9; + } + + //acos(x) + assert(1.4 < acos(0.1) && acos(0.1) < 1.5); // SUCCESS + + //asin(x) + assert(0.6 < asin(0.6) && asin(0.6) < 0.7); // SUCCESS + + //atan(x) + assert(0.7 < atan(1.) && atan(1.) < 0.8); // SUCCESS + + //cos(x) + assert(-1. <= cos(c1) && cos(c1) < 0.99); // SUCCESS + assert(-0.99 < cos(c2) && cos(c2) <= 1.0); // SUCCESS + assert(-0.99 < cos(sc1) && cos(sc1) < 0.); // SUCCESS + assert(-0.99 < cos(sc2) && cos(sc2) < 0.); // SUCCESS + + //sin(x) + assert(-1. <= sin(s1) && sin(s1) < 0.99); // SUCCESS + assert(-0.99 < sin(s2) && sin(s2) <= 1.); // SUCCESS + assert(-0.99 < sin(s3) && sin(s3) <= 0.99); // SUCCESS + assert(0. < sin(sc1) && sin(sc1) < 0.99); // SUCCESS + assert(0. < sin(sc2) && sin(sc2) < 0.99); // SUCCESS + + //tan(x) + assert(-0.11 < tan(t1) && tan(t1) < 0.11 ); // SUCCESS + assert(-0.1 < tan(t2) && tan(t2) < 0.1 ); // SUCCESS +} From 0a3164f8f80d9e2904d3b32ec2bd217fc363b805 Mon Sep 17 00:00:00 2001 From: FelixKrayer Date: Thu, 7 Dec 2023 22:59:40 +0100 Subject: [PATCH 02/24] remove math_funeval option --- src/cdomains/floatDomain.ml | 32 ++++++-------------- src/common/util/options.schema.json | 7 ----- tests/regression/57-floats/22-math-funeval.c | 2 +- 3 files changed, 11 insertions(+), 30 deletions(-) diff --git a/src/cdomains/floatDomain.ml b/src/cdomains/floatDomain.ml index 0a61a74c9a..93a39c14cd 100644 --- a/src/cdomains/floatDomain.ml +++ b/src/cdomains/floatDomain.ml @@ -622,7 +622,7 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct let overapprox_pi = 3.1416 let underapprox_pi = 3.1415 - let trig_helper l h k = (** computes dist = distance, l'' = (l/(k*pi) % 10) - floor(l/(k*pi)), h'' = (h/(k*pi)) - floor(h/(k*pi))*) + let trig_helper l h k = (** computes dist = distance, l'' = (l/(k*pi)) - floor(l/(k*pi)), h'' = (h/(k*pi)) - floor(h/(k*pi))*) let ft_over_kpi = (Float_t.mul Up (Float_t.of_float Up k) (Float_t.of_float Up overapprox_pi)) in let ft_under_kpi = (Float_t.mul Down (Float_t.of_float Down k) (Float_t.of_float Down underapprox_pi)) in let l' = @@ -660,7 +660,7 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct else if dist <= (Float_t.of_float Down 1.) && (l'' >= Float_t.of_float Down 0.5) && (h'' <= Float_t.of_float Down 0.5) then Interval (min (Float_t.cos Down l) (Float_t.cos Down h), Float_t.of_float Up 1.) else - of_interval (-. 1., 1.) + of_interval (-. 1., 1.) let eval_sin_cfun l h = let (dist, l'', h'') = trig_helper l h 2. in @@ -678,12 +678,12 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct Interval (min (Float_t.sin Down l) (Float_t.sin Down h), Float_t.of_float Up 1.) else of_interval (-. 1., 1.) - + let eval_tan_cfun l h = let (dist, l'', h'') = trig_helper l h 1. in if Messages.tracing then Messages.trace "CstubsTrig" "tan: dist %s; l'' %s; h'' %s\n" (Float_t.to_string dist) (Float_t.to_string l'') (Float_t.to_string h''); if dist <= (Float_t.of_float Down 1.) && Bool.not ((l'' <= Float_t.of_float Up 0.5) && (h'' >= Float_t.of_float Down 0.5)) then - Interval (Float_t.tan Down l, Float_t.tan Up h) + Interval (Float_t.tan Down l, Float_t.tan Up h) else top () @@ -713,42 +713,30 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct | (l, h) when l < (Float_t.of_float Down (-.1.)) || h > (Float_t.of_float Up 1.) -> Messages.warn ~category:Messages.Category.Float "Domain error might occur: acos argument might be outside of [-1., 1.]"; of_interval (0., (overapprox_pi)) - | (l, h) when GobConfig.get_bool "ana.float.math_funeval" -> - norm @@ Interval (Float_t.acos Down h, Float_t.acos Up l) (** acos is monotonic decreasing in [-1, 1]*) - | _ -> of_interval (0., (overapprox_pi)) + | (l, h) -> norm @@ Interval (Float_t.acos Down h, Float_t.acos Up l) (** acos is monotonic decreasing in [-1, 1]*) let eval_asin = function | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*asin(0) = 0*) | (l, h) when l < (Float_t.of_float Down (-.1.)) || h > (Float_t.of_float Up 1.) -> Messages.warn ~category:Messages.Category.Float "Domain error might occur: asin argument might be outside of [-1., 1.]"; div (of_interval ((-. overapprox_pi), overapprox_pi)) (of_const 2.) - | (l, h) when GobConfig.get_bool "ana.float.math_funeval" -> - norm @@ Interval (Float_t.asin Down l, Float_t.asin Up h) (** asin is monotonic increasing in [-1, 1]*) - | _ -> div (of_interval ((-. overapprox_pi), overapprox_pi)) (of_const 2.) + | (l, h) -> norm @@ Interval (Float_t.asin Down l, Float_t.asin Up h) (** asin is monotonic increasing in [-1, 1]*) let eval_atan = function | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*atan(0) = 0*) - | (l, h) when GobConfig.get_bool "ana.float.math_funeval" -> - norm @@ Interval (Float_t.atan Down l, Float_t.atan Up h) (** atan is monotonic increasing*) - | _ -> div (of_interval ((-. overapprox_pi), overapprox_pi)) (of_const 2.) + | (l, h) -> norm @@ Interval (Float_t.atan Down l, Float_t.atan Up h) (** atan is monotonic increasing*) let eval_cos = function | (l, h) when l = h && l = Float_t.zero -> of_const 1. (*cos(0) = 1*) - | (l, h) when GobConfig.get_bool "ana.float.math_funeval" -> - norm @@ eval_cos_cfun l h - | _ -> of_interval (-. 1., 1.) + | (l, h) -> norm @@ eval_cos_cfun l h let eval_sin = function | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*sin(0) = 0*) - | (l, h) when GobConfig.get_bool "ana.float.math_funeval" -> - norm @@ eval_sin_cfun l h - | _ -> of_interval (-. 1., 1.) + | (l, h) -> norm @@ eval_sin_cfun l h let eval_tan = function | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*tan(0) = 0*) - | (l, h) when GobConfig.get_bool "ana.float.math_funeval" -> - norm @@ eval_tan_cfun l h - | _ -> top () + | (l, h) -> norm @@ eval_tan_cfun l h let eval_sqrt = function | (l, h) when l = Float_t.zero && h = Float_t.zero -> of_const 0. diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json index a3145d5469..7c921c4f53 100644 --- a/src/common/util/options.schema.json +++ b/src/common/util/options.schema.json @@ -463,13 +463,6 @@ "Use FloatDomain: (float * float) option.", "type": "boolean", "default": false - }, - "math_funeval": { - "title": "ana.float.math_funeval", - "description": - "Allow evaluation of functions from math.h with c-stubs. Only sound, if the same math.h implementation is used for the programm that is also used in Goblint", - "type": "boolean", - "default": false } }, "additionalProperties": false diff --git a/tests/regression/57-floats/22-math-funeval.c b/tests/regression/57-floats/22-math-funeval.c index 51a9454fa8..1096abd591 100644 --- a/tests/regression/57-floats/22-math-funeval.c +++ b/tests/regression/57-floats/22-math-funeval.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.float.interval --enable ana.float.math_funeval +// PARAM: --enable ana.float.interval #include #include #include From 6cfe061c5b94df62ca3530561d14d057d8ce50c5 Mon Sep 17 00:00:00 2001 From: FelixKrayer Date: Sat, 27 Jan 2024 16:37:04 +0100 Subject: [PATCH 03/24] add clarifying comments and rename function to project_and_compress --- src/cdomains/floatDomain.ml | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) diff --git a/src/cdomains/floatDomain.ml b/src/cdomains/floatDomain.ml index 93a39c14cd..614188a964 100644 --- a/src/cdomains/floatDomain.ml +++ b/src/cdomains/floatDomain.ml @@ -622,7 +622,11 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct let overapprox_pi = 3.1416 let underapprox_pi = 3.1415 - let trig_helper l h k = (** computes dist = distance, l'' = (l/(k*pi)) - floor(l/(k*pi)), h'' = (h/(k*pi)) - floor(h/(k*pi))*) + (** this function does two things: *) + (** 1. projects l and h onto the interval [0, k*pi] (for k = 2 this is the phase length of sin/cos, for k = 1 it is the phase length of tan)*) + (** 2. compresses/transforms the interval [0, k*pi] to the interval [0, 1] to ease further computations *) + (** i.e. the it computes dist = distance, l'' = (l/(k*pi)) - floor(l/(k*pi)), h'' = (h/(k*pi)) - floor(h/(k*pi))*) + let project_and_compress l h k = let ft_over_kpi = (Float_t.mul Up (Float_t.of_float Up k) (Float_t.of_float Up overapprox_pi)) in let ft_under_kpi = (Float_t.mul Down (Float_t.of_float Down k) (Float_t.of_float Down underapprox_pi)) in let l' = @@ -649,40 +653,49 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct (dist, l'', h'') let eval_cos_cfun l h = - let (dist, l'', h'') = trig_helper l h 2. in + let (dist, l'', h'') = project_and_compress l h 2. in if Messages.tracing then Messages.trace "CstubsTrig" "sin: dist %s; l'' %s; h'' %s\n" (Float_t.to_string dist) (Float_t.to_string l'') (Float_t.to_string h''); if dist <= (Float_t.of_float Down 0.5) && (h'' <= Float_t.of_float Up 0.5) && (h'' >= l'') then + (** case: monotonic decreasing interval*) Interval (Float_t.cos Down h, Float_t.cos Up l) else if dist <= (Float_t.of_float Down 0.5) && (l'' >= Float_t.of_float Down 0.5) && (h'' >= l'') then + (** case: monotonic increasing interval*) Interval (Float_t.cos Down l, Float_t.cos Up h) else if dist <= (Float_t.of_float Down 1.) && (l'' <= h'') then + (** case: contains at most one minimum*) Interval (Float_t.of_float Down (-.1.), max (Float_t.cos Up l) (Float_t.cos Up h)) else if dist <= (Float_t.of_float Down 1.) && (l'' >= Float_t.of_float Down 0.5) && (h'' <= Float_t.of_float Down 0.5) then + (** case: contains at most one maximum*) Interval (min (Float_t.cos Down l) (Float_t.cos Down h), Float_t.of_float Up 1.) else of_interval (-. 1., 1.) let eval_sin_cfun l h = - let (dist, l'', h'') = trig_helper l h 2. in + let (dist, l'', h'') = project_and_compress l h 2. in if Messages.tracing then Messages.trace "CstubsTrig" "cos: dist %s; l'' %s; h'' %s\n" (Float_t.to_string dist) (Float_t.to_string l'') (Float_t.to_string h''); (* phase shift -0.25 -> same phase as cos *) let l'' = if l'' <= Float_t.of_float Down 0.25 then Float_t.add Up l'' (Float_t.of_float Up 0.75) else Float_t.sub Down l'' (Float_t.of_float Up 0.25) in let h'' = if h'' <= Float_t.of_float Down 0.25 then Float_t.add Up h'' (Float_t.of_float Up 0.75) else Float_t.sub Down h'' (Float_t.of_float Up 0.25) in if dist <= (Float_t.of_float Down 0.5) && (h'' <= Float_t.of_float Up 0.5) && (h'' >= l'') then + (** case: monotonic decreasing interval*) Interval (Float_t.sin Down h, Float_t.sin Up l) else if dist <= (Float_t.of_float Down 0.5) && (l'' >= Float_t.of_float Down 0.5) && (h'' >= l'') then + (** case: monotonic increasing interval*) Interval (Float_t.sin Down l, Float_t.sin Up h) else if dist <= (Float_t.of_float Down 1.) && (l'' <= h'') then + (** case: contains at most one minimum*) Interval (Float_t.of_float Down (-.1.), max (Float_t.sin Up l) (Float_t.sin Up h)) else if dist <= (Float_t.of_float Down 1.) && (l'' >= Float_t.of_float Down 0.5) && (h'' <= Float_t.of_float Down 0.5) then + (** case: contains at most one maximum*) Interval (min (Float_t.sin Down l) (Float_t.sin Down h), Float_t.of_float Up 1.) else of_interval (-. 1., 1.) let eval_tan_cfun l h = - let (dist, l'', h'') = trig_helper l h 1. in + let (dist, l'', h'') = project_and_compress l h 1. in if Messages.tracing then Messages.trace "CstubsTrig" "tan: dist %s; l'' %s; h'' %s\n" (Float_t.to_string dist) (Float_t.to_string l'') (Float_t.to_string h''); if dist <= (Float_t.of_float Down 1.) && Bool.not ((l'' <= Float_t.of_float Up 0.5) && (h'' >= Float_t.of_float Down 0.5)) then + (** case: monotonic increasing interval*) Interval (Float_t.tan Down l, Float_t.tan Up h) else top () From ec4ec25701132f49b612345be2c3c089d4a79eb2 Mon Sep 17 00:00:00 2001 From: FelixKrayer Date: Sat, 27 Jan 2024 17:33:32 +0100 Subject: [PATCH 04/24] fix some rounding modes --- src/cdomain/value/cdomains/floatDomain.ml | 34 +++++++++++------------ 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/src/cdomain/value/cdomains/floatDomain.ml b/src/cdomain/value/cdomains/floatDomain.ml index 967bcf899b..3561d70202 100644 --- a/src/cdomain/value/cdomains/floatDomain.ml +++ b/src/cdomain/value/cdomains/floatDomain.ml @@ -631,40 +631,40 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct let ft_under_kpi = (Float_t.mul Down (Float_t.of_float Down k) (Float_t.of_float Down underapprox_pi)) in let l' = if l >= Float_t.zero then (Float_t.div Down l ft_over_kpi) - else (Float_t.div Up l ft_under_kpi) + else (Float_t.div Down l ft_under_kpi) in let h' = if h >= Float_t.zero then (Float_t.div Up h ft_under_kpi) - else (Float_t.div Down h ft_over_kpi) + else (Float_t.div Up h ft_over_kpi) in let dist = (Float_t.sub Up h' l') in let l'' = if l' >= Float_t.zero then - Float_t.sub Down l' (Float_t.of_float Down (Big_int_Z.float_of_big_int (Float_t.to_big_int l'))) + Float_t.sub Down l' (Float_t.of_float Up (Big_int_Z.float_of_big_int (Float_t.to_big_int l'))) else - Float_t.sub Down l' (Float_t.of_float Down (Big_int_Z.float_of_big_int (IntOps.BigIntOps.sub (Float_t.to_big_int l') (Big_int_Z.big_int_of_int 1)))) + Float_t.sub Down l' (Float_t.of_float Up (Big_int_Z.float_of_big_int (IntOps.BigIntOps.sub (Float_t.to_big_int l') (Big_int_Z.big_int_of_int 1)))) in let h'' = if h' >= Float_t.zero then - Float_t.sub Up h' (Float_t.of_float Up (Big_int_Z.float_of_big_int (Float_t.to_big_int h'))) + Float_t.sub Up h' (Float_t.of_float Down (Big_int_Z.float_of_big_int (Float_t.to_big_int h'))) else - Float_t.sub Up h' (Float_t.of_float Up (Big_int_Z.float_of_big_int (IntOps.BigIntOps.sub (Float_t.to_big_int h') (Big_int_Z.big_int_of_int 1)))) + Float_t.sub Up h' (Float_t.of_float Down (Big_int_Z.float_of_big_int (IntOps.BigIntOps.sub (Float_t.to_big_int h') (Big_int_Z.big_int_of_int 1)))) in (dist, l'', h'') let eval_cos_cfun l h = let (dist, l'', h'') = project_and_compress l h 2. in if Messages.tracing then Messages.trace "CstubsTrig" "sin: dist %s; l'' %s; h'' %s\n" (Float_t.to_string dist) (Float_t.to_string l'') (Float_t.to_string h''); - if dist <= (Float_t.of_float Down 0.5) && (h'' <= Float_t.of_float Up 0.5) && (h'' >= l'') then + if (dist <= Float_t.of_float Down 0.5) && (h'' <= Float_t.of_float Down 0.5) && (h'' >= l'') then (** case: monotonic decreasing interval*) Interval (Float_t.cos Down h, Float_t.cos Up l) - else if dist <= (Float_t.of_float Down 0.5) && (l'' >= Float_t.of_float Down 0.5) && (h'' >= l'') then + else if (dist <= Float_t.of_float Down 0.5) && (l'' >= Float_t.of_float Up 0.5) && (h'' >= l'') then (** case: monotonic increasing interval*) Interval (Float_t.cos Down l, Float_t.cos Up h) - else if dist <= (Float_t.of_float Down 1.) && (l'' <= h'') then + else if (dist <= Float_t.of_float Down 1.) && (l'' <= h'') then (** case: contains at most one minimum*) Interval (Float_t.of_float Down (-.1.), max (Float_t.cos Up l) (Float_t.cos Up h)) - else if dist <= (Float_t.of_float Down 1.) && (l'' >= Float_t.of_float Down 0.5) && (h'' <= Float_t.of_float Down 0.5) then + else if (dist <= Float_t.of_float Down 1.) && (l'' >= Float_t.of_float Up 0.5) && (h'' <= Float_t.of_float Down 0.5) then (** case: contains at most one maximum*) Interval (min (Float_t.cos Down l) (Float_t.cos Down h), Float_t.of_float Up 1.) else @@ -674,18 +674,18 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct let (dist, l'', h'') = project_and_compress l h 2. in if Messages.tracing then Messages.trace "CstubsTrig" "cos: dist %s; l'' %s; h'' %s\n" (Float_t.to_string dist) (Float_t.to_string l'') (Float_t.to_string h''); (* phase shift -0.25 -> same phase as cos *) - let l'' = if l'' <= Float_t.of_float Down 0.25 then Float_t.add Up l'' (Float_t.of_float Up 0.75) else Float_t.sub Down l'' (Float_t.of_float Up 0.25) in - let h'' = if h'' <= Float_t.of_float Down 0.25 then Float_t.add Up h'' (Float_t.of_float Up 0.75) else Float_t.sub Down h'' (Float_t.of_float Up 0.25) in - if dist <= (Float_t.of_float Down 0.5) && (h'' <= Float_t.of_float Up 0.5) && (h'' >= l'') then + let l'' = if l'' <= Float_t.of_float Down 0.25 then Float_t.add Down l'' (Float_t.of_float Down 0.75) else Float_t.sub Down l'' (Float_t.of_float Up 0.25) in + let h'' = if h'' <= Float_t.of_float Down 0.25 then Float_t.add Up h'' (Float_t.of_float Up 0.75) else Float_t.sub Up h'' (Float_t.of_float Down 0.25) in + if (dist <= Float_t.of_float Down 0.5) && (h'' <= Float_t.of_float Down 0.5) && (h'' >= l'') then (** case: monotonic decreasing interval*) Interval (Float_t.sin Down h, Float_t.sin Up l) - else if dist <= (Float_t.of_float Down 0.5) && (l'' >= Float_t.of_float Down 0.5) && (h'' >= l'') then + else if (dist <= Float_t.of_float Down 0.5) && (l'' >= Float_t.of_float Up 0.5) && (h'' >= l'') then (** case: monotonic increasing interval*) Interval (Float_t.sin Down l, Float_t.sin Up h) - else if dist <= (Float_t.of_float Down 1.) && (l'' <= h'') then + else if (dist <= Float_t.of_float Down 1.) && (l'' <= h'') then (** case: contains at most one minimum*) Interval (Float_t.of_float Down (-.1.), max (Float_t.sin Up l) (Float_t.sin Up h)) - else if dist <= (Float_t.of_float Down 1.) && (l'' >= Float_t.of_float Down 0.5) && (h'' <= Float_t.of_float Down 0.5) then + else if (dist <= Float_t.of_float Down 1.) && (l'' >= Float_t.of_float Up 0.5) && (h'' <= Float_t.of_float Down 0.5) then (** case: contains at most one maximum*) Interval (min (Float_t.sin Down l) (Float_t.sin Down h), Float_t.of_float Up 1.) else @@ -694,7 +694,7 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct let eval_tan_cfun l h = let (dist, l'', h'') = project_and_compress l h 1. in if Messages.tracing then Messages.trace "CstubsTrig" "tan: dist %s; l'' %s; h'' %s\n" (Float_t.to_string dist) (Float_t.to_string l'') (Float_t.to_string h''); - if dist <= (Float_t.of_float Down 1.) && Bool.not ((l'' <= Float_t.of_float Up 0.5) && (h'' >= Float_t.of_float Down 0.5)) then + if (dist <= Float_t.of_float Down 1.) && (Bool.not ((l'' <= Float_t.of_float Up 0.5) && (h'' >= Float_t.of_float Up 0.5))) then (** case: monotonic increasing interval*) Interval (Float_t.tan Down l, Float_t.tan Up h) else From c5f0a6e70a14759d0cf87e49fe3398b3a38b97c2 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Tue, 30 Jan 2024 15:09:25 +0100 Subject: [PATCH 05/24] address semgrep warnings --- src/cdomain/value/cdomains/floatDomain.ml | 26 +++++++++++------------ 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/src/cdomain/value/cdomains/floatDomain.ml b/src/cdomain/value/cdomains/floatDomain.ml index 3561d70202..f1276b8d1f 100644 --- a/src/cdomain/value/cdomains/floatDomain.ml +++ b/src/cdomain/value/cdomains/floatDomain.ml @@ -626,29 +626,29 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct (** 1. projects l and h onto the interval [0, k*pi] (for k = 2 this is the phase length of sin/cos, for k = 1 it is the phase length of tan)*) (** 2. compresses/transforms the interval [0, k*pi] to the interval [0, 1] to ease further computations *) (** i.e. the it computes dist = distance, l'' = (l/(k*pi)) - floor(l/(k*pi)), h'' = (h/(k*pi)) - floor(h/(k*pi))*) - let project_and_compress l h k = + let project_and_compress l h k = let ft_over_kpi = (Float_t.mul Up (Float_t.of_float Up k) (Float_t.of_float Up overapprox_pi)) in let ft_under_kpi = (Float_t.mul Down (Float_t.of_float Down k) (Float_t.of_float Down underapprox_pi)) in let l' = if l >= Float_t.zero then (Float_t.div Down l ft_over_kpi) else (Float_t.div Down l ft_under_kpi) in - let h' = + let h' = if h >= Float_t.zero then (Float_t.div Up h ft_under_kpi) else (Float_t.div Up h ft_over_kpi) in let dist = (Float_t.sub Up h' l') in - let l'' = - if l' >= Float_t.zero then - Float_t.sub Down l' (Float_t.of_float Up (Big_int_Z.float_of_big_int (Float_t.to_big_int l'))) - else - Float_t.sub Down l' (Float_t.of_float Up (Big_int_Z.float_of_big_int (IntOps.BigIntOps.sub (Float_t.to_big_int l') (Big_int_Z.big_int_of_int 1)))) + let l'' = + if l' >= Float_t.zero then + Float_t.sub Down l' (Float_t.of_float Up (Z.to_float (Float_t.to_big_int l'))) + else + Float_t.sub Down l' (Float_t.of_float Up (Z.to_float (IntOps.BigIntOps.sub (Float_t.to_big_int l') (Z.of_int 1)))) in - let h'' = - if h' >= Float_t.zero then - Float_t.sub Up h' (Float_t.of_float Down (Big_int_Z.float_of_big_int (Float_t.to_big_int h'))) - else - Float_t.sub Up h' (Float_t.of_float Down (Big_int_Z.float_of_big_int (IntOps.BigIntOps.sub (Float_t.to_big_int h') (Big_int_Z.big_int_of_int 1)))) + let h'' = + if h' >= Float_t.zero then + Float_t.sub Up h' (Float_t.of_float Down (Z.to_float (Float_t.to_big_int h'))) + else + Float_t.sub Up h' (Float_t.of_float Down (Z.to_float (IntOps.BigIntOps.sub (Float_t.to_big_int h') (Z.of_int 1)))) in (dist, l'', h'') @@ -688,7 +688,7 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct else if (dist <= Float_t.of_float Down 1.) && (l'' >= Float_t.of_float Up 0.5) && (h'' <= Float_t.of_float Down 0.5) then (** case: contains at most one maximum*) Interval (min (Float_t.sin Down l) (Float_t.sin Down h), Float_t.of_float Up 1.) - else + else of_interval (-. 1., 1.) let eval_tan_cfun l h = From 73d65b900d67b0d167a40a42fc675f6c506f9d11 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Tue, 30 Jan 2024 15:16:41 +0100 Subject: [PATCH 06/24] use Z.pred instead of sub 1 --- src/cdomain/value/cdomains/floatDomain.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cdomain/value/cdomains/floatDomain.ml b/src/cdomain/value/cdomains/floatDomain.ml index f1276b8d1f..26308e7ab1 100644 --- a/src/cdomain/value/cdomains/floatDomain.ml +++ b/src/cdomain/value/cdomains/floatDomain.ml @@ -642,13 +642,13 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct if l' >= Float_t.zero then Float_t.sub Down l' (Float_t.of_float Up (Z.to_float (Float_t.to_big_int l'))) else - Float_t.sub Down l' (Float_t.of_float Up (Z.to_float (IntOps.BigIntOps.sub (Float_t.to_big_int l') (Z.of_int 1)))) + Float_t.sub Down l' (Float_t.of_float Up (Z.to_float (Z.pred (Float_t.to_big_int l')))) in let h'' = if h' >= Float_t.zero then Float_t.sub Up h' (Float_t.of_float Down (Z.to_float (Float_t.to_big_int h'))) else - Float_t.sub Up h' (Float_t.of_float Down (Z.to_float (IntOps.BigIntOps.sub (Float_t.to_big_int h') (Z.of_int 1)))) + Float_t.sub Up h' (Float_t.of_float Down (Z.to_float (Z.pred (Float_t.to_big_int h')))) in (dist, l'', h'') From 16f997bff6c87ed7866fe3ec03a9a7aa50a34e83 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Tue, 30 Jan 2024 16:13:54 +0100 Subject: [PATCH 07/24] use c stub for pi constant --- src/cdomain/value/cdomains/floatDomain.ml | 8 ++++---- src/common/cdomains/floatOps/floatOps.ml | 4 ++++ src/common/cdomains/floatOps/floatOps.mli | 1 + src/common/cdomains/floatOps/stubs.c | 6 ++++++ 4 files changed, 15 insertions(+), 4 deletions(-) diff --git a/src/cdomain/value/cdomains/floatDomain.ml b/src/cdomain/value/cdomains/floatDomain.ml index 26308e7ab1..cc9f62e9d8 100644 --- a/src/cdomain/value/cdomains/floatDomain.ml +++ b/src/cdomain/value/cdomains/floatDomain.ml @@ -627,8 +627,8 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct (** 2. compresses/transforms the interval [0, k*pi] to the interval [0, 1] to ease further computations *) (** i.e. the it computes dist = distance, l'' = (l/(k*pi)) - floor(l/(k*pi)), h'' = (h/(k*pi)) - floor(h/(k*pi))*) let project_and_compress l h k = - let ft_over_kpi = (Float_t.mul Up (Float_t.of_float Up k) (Float_t.of_float Up overapprox_pi)) in - let ft_under_kpi = (Float_t.mul Down (Float_t.of_float Down k) (Float_t.of_float Down underapprox_pi)) in + let ft_over_kpi = (Float_t.mul Up (Float_t.of_float Up k) Float_t.pi) in + let ft_under_kpi = (Float_t.mul Down (Float_t.of_float Down k) Float_t.pi) in let l' = if l >= Float_t.zero then (Float_t.div Down l ft_over_kpi) else (Float_t.div Down l ft_under_kpi) @@ -654,7 +654,7 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct let eval_cos_cfun l h = let (dist, l'', h'') = project_and_compress l h 2. in - if Messages.tracing then Messages.trace "CstubsTrig" "sin: dist %s; l'' %s; h'' %s\n" (Float_t.to_string dist) (Float_t.to_string l'') (Float_t.to_string h''); + if Messages.tracing then Messages.trace "CstubsTrig" "cos: dist %s; l'' %s; h'' %s\n" (Float_t.to_string dist) (Float_t.to_string l'') (Float_t.to_string h''); if (dist <= Float_t.of_float Down 0.5) && (h'' <= Float_t.of_float Down 0.5) && (h'' >= l'') then (** case: monotonic decreasing interval*) Interval (Float_t.cos Down h, Float_t.cos Up l) @@ -672,7 +672,7 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct let eval_sin_cfun l h = let (dist, l'', h'') = project_and_compress l h 2. in - if Messages.tracing then Messages.trace "CstubsTrig" "cos: dist %s; l'' %s; h'' %s\n" (Float_t.to_string dist) (Float_t.to_string l'') (Float_t.to_string h''); + if Messages.tracing then Messages.trace "CstubsTrig" "sin: dist %s; l'' %s; h'' %s\n" (Float_t.to_string dist) (Float_t.to_string l'') (Float_t.to_string h''); (* phase shift -0.25 -> same phase as cos *) let l'' = if l'' <= Float_t.of_float Down 0.25 then Float_t.add Down l'' (Float_t.of_float Down 0.75) else Float_t.sub Down l'' (Float_t.of_float Up 0.25) in let h'' = if h'' <= Float_t.of_float Down 0.25 then Float_t.add Up h'' (Float_t.of_float Up 0.75) else Float_t.sub Up h'' (Float_t.of_float Down 0.25) in diff --git a/src/common/cdomains/floatOps/floatOps.ml b/src/common/cdomains/floatOps/floatOps.ml index b73e7b424e..5bf717bfc3 100644 --- a/src/common/cdomains/floatOps/floatOps.ml +++ b/src/common/cdomains/floatOps/floatOps.ml @@ -12,6 +12,7 @@ module type CFloatType = sig val upper_bound: t val lower_bound: t val smallest : t + val pi : t val of_float: round_mode -> float -> t val to_float: t -> float option @@ -63,6 +64,7 @@ module CDouble = struct let upper_bound = Float.max_float let lower_bound = -. Float.max_float let smallest = Float.min_float + let pi = Float.pi let of_float _ x = x let to_float x = Some x @@ -103,10 +105,12 @@ module CFloat = struct external upper': unit -> float = "max_float" external smallest': unit -> float = "smallest_float" + external pi': unit -> float = "pi" let upper_bound = upper' () let lower_bound = -. upper_bound let smallest = smallest' () + let pi = pi' () let to_float x = Some x let to_big_int = big_int_of_float diff --git a/src/common/cdomains/floatOps/floatOps.mli b/src/common/cdomains/floatOps/floatOps.mli index 75d0481822..7cd74f7e7d 100644 --- a/src/common/cdomains/floatOps/floatOps.mli +++ b/src/common/cdomains/floatOps/floatOps.mli @@ -14,6 +14,7 @@ module type CFloatType = sig val upper_bound: t val lower_bound: t val smallest : t + val pi : t val of_float: round_mode -> float -> t val to_float: t -> float option diff --git a/src/common/cdomains/floatOps/stubs.c b/src/common/cdomains/floatOps/stubs.c index 4489ef71e1..7c9c1aff9d 100644 --- a/src/common/cdomains/floatOps/stubs.c +++ b/src/common/cdomains/floatOps/stubs.c @@ -1,3 +1,4 @@ +#define _GNU_SOURCE #include #include #include @@ -113,3 +114,8 @@ CAMLprim value smallest_float(value unit) { return caml_copy_double(FLT_MIN); } + +CAMLprim value pi(value unit) +{ + return caml_copy_double(M_PI); +} From cb09d05147c69dd7096efdef2ff7d12118edbb9e Mon Sep 17 00:00:00 2001 From: FelixKrayer Date: Tue, 30 Jan 2024 16:34:41 +0100 Subject: [PATCH 08/24] remove phase shift in sin and adjust case checks instead --- src/cdomain/value/cdomains/floatDomain.ml | 17 ++++++++--------- ...th-funeval.c => 22-trig_functions_c-stubs.c} | 0 2 files changed, 8 insertions(+), 9 deletions(-) rename tests/regression/57-floats/{22-math-funeval.c => 22-trig_functions_c-stubs.c} (100%) diff --git a/src/cdomain/value/cdomains/floatDomain.ml b/src/cdomain/value/cdomains/floatDomain.ml index cc9f62e9d8..88d2652fd4 100644 --- a/src/cdomain/value/cdomains/floatDomain.ml +++ b/src/cdomain/value/cdomains/floatDomain.ml @@ -655,10 +655,10 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct let eval_cos_cfun l h = let (dist, l'', h'') = project_and_compress l h 2. in if Messages.tracing then Messages.trace "CstubsTrig" "cos: dist %s; l'' %s; h'' %s\n" (Float_t.to_string dist) (Float_t.to_string l'') (Float_t.to_string h''); - if (dist <= Float_t.of_float Down 0.5) && (h'' <= Float_t.of_float Down 0.5) && (h'' >= l'') then + if (dist <= Float_t.of_float Down 0.5) && (h'' <= Float_t.of_float Down 0.5) && (l'' <= h'') then (** case: monotonic decreasing interval*) Interval (Float_t.cos Down h, Float_t.cos Up l) - else if (dist <= Float_t.of_float Down 0.5) && (l'' >= Float_t.of_float Up 0.5) && (h'' >= l'') then + else if (dist <= Float_t.of_float Down 0.5) && (l'' >= Float_t.of_float Up 0.5) && (l'' <= h'') then (** case: monotonic increasing interval*) Interval (Float_t.cos Down l, Float_t.cos Up h) else if (dist <= Float_t.of_float Down 1.) && (l'' <= h'') then @@ -673,19 +673,18 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct let eval_sin_cfun l h = let (dist, l'', h'') = project_and_compress l h 2. in if Messages.tracing then Messages.trace "CstubsTrig" "sin: dist %s; l'' %s; h'' %s\n" (Float_t.to_string dist) (Float_t.to_string l'') (Float_t.to_string h''); - (* phase shift -0.25 -> same phase as cos *) - let l'' = if l'' <= Float_t.of_float Down 0.25 then Float_t.add Down l'' (Float_t.of_float Down 0.75) else Float_t.sub Down l'' (Float_t.of_float Up 0.25) in - let h'' = if h'' <= Float_t.of_float Down 0.25 then Float_t.add Up h'' (Float_t.of_float Up 0.75) else Float_t.sub Up h'' (Float_t.of_float Down 0.25) in - if (dist <= Float_t.of_float Down 0.5) && (h'' <= Float_t.of_float Down 0.5) && (h'' >= l'') then + if (dist <= Float_t.of_float Down 0.5) && (l'' >= Float_t.of_float Up 0.25) && (h'' <= Float_t.of_float Down 0.75) && (l'' <= h'') then (** case: monotonic decreasing interval*) Interval (Float_t.sin Down h, Float_t.sin Up l) - else if (dist <= Float_t.of_float Down 0.5) && (l'' >= Float_t.of_float Up 0.5) && (h'' >= l'') then + else if (dist <= Float_t.of_float Down 0.5) && + ((((l'' >= Float_t.of_float Up 0.75) || (h'' <= Float_t.of_float Down 0.25)) && (l'' <= h'')) || (** two cases with l'' <= h''*) + ((l'' >= Float_t.of_float Up 0.75) && (h'' <= Float_t.of_float Down 0.25))) then (** projected interval is "wrapped", i.e., l'' >= h''*) (** case: monotonic increasing interval*) Interval (Float_t.sin Down l, Float_t.sin Up h) - else if (dist <= Float_t.of_float Down 1.) && (l'' <= h'') then + else if (dist <= Float_t.of_float Down 1.) && (l'' >= Float_t.of_float Up 0.25) && ((l'' <= h'') || (h'' <= Float_t.of_float Down 0.25)) then (** case: contains at most one minimum*) Interval (Float_t.of_float Down (-.1.), max (Float_t.sin Up l) (Float_t.sin Up h)) - else if (dist <= Float_t.of_float Down 1.) && (l'' >= Float_t.of_float Up 0.5) && (h'' <= Float_t.of_float Down 0.5) then + else if (dist <= Float_t.of_float Down 1.) && (h'' <= Float_t.of_float Down 0.75) && ((l'' <= h'') || (l'' >= Float_t.of_float Up 0.75))then (** case: contains at most one maximum*) Interval (min (Float_t.sin Down l) (Float_t.sin Down h), Float_t.of_float Up 1.) else diff --git a/tests/regression/57-floats/22-math-funeval.c b/tests/regression/57-floats/22-trig_functions_c-stubs.c similarity index 100% rename from tests/regression/57-floats/22-math-funeval.c rename to tests/regression/57-floats/22-trig_functions_c-stubs.c From b47fa008f6d0529302151ba72882f28b49bcf298 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Tue, 30 Jan 2024 19:00:42 +0100 Subject: [PATCH 09/24] Update GobView submodule --- gobview | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/gobview b/gobview index c8fcb09e9a..841090e5b7 160000 --- a/gobview +++ b/gobview @@ -1 +1 @@ -Subproject commit c8fcb09e9a3e27de22d4803606d5784f667a542a +Subproject commit 841090e5b76a20ca0a49ce30e99bf2a11b51f31c From ae732f1034a14b29979628fb594dc62da58c97e4 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Thu, 1 Feb 2024 18:53:17 +0100 Subject: [PATCH 10/24] implement sinus function as shift of cosinus --- src/cdomain/value/cdomains/floatDomain.ml | 21 +++------------------ 1 file changed, 3 insertions(+), 18 deletions(-) diff --git a/src/cdomain/value/cdomains/floatDomain.ml b/src/cdomain/value/cdomains/floatDomain.ml index 88d2652fd4..adda13bbcf 100644 --- a/src/cdomain/value/cdomains/floatDomain.ml +++ b/src/cdomain/value/cdomains/floatDomain.ml @@ -671,24 +671,9 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct of_interval (-. 1., 1.) let eval_sin_cfun l h = - let (dist, l'', h'') = project_and_compress l h 2. in - if Messages.tracing then Messages.trace "CstubsTrig" "sin: dist %s; l'' %s; h'' %s\n" (Float_t.to_string dist) (Float_t.to_string l'') (Float_t.to_string h''); - if (dist <= Float_t.of_float Down 0.5) && (l'' >= Float_t.of_float Up 0.25) && (h'' <= Float_t.of_float Down 0.75) && (l'' <= h'') then - (** case: monotonic decreasing interval*) - Interval (Float_t.sin Down h, Float_t.sin Up l) - else if (dist <= Float_t.of_float Down 0.5) && - ((((l'' >= Float_t.of_float Up 0.75) || (h'' <= Float_t.of_float Down 0.25)) && (l'' <= h'')) || (** two cases with l'' <= h''*) - ((l'' >= Float_t.of_float Up 0.75) && (h'' <= Float_t.of_float Down 0.25))) then (** projected interval is "wrapped", i.e., l'' >= h''*) - (** case: monotonic increasing interval*) - Interval (Float_t.sin Down l, Float_t.sin Up h) - else if (dist <= Float_t.of_float Down 1.) && (l'' >= Float_t.of_float Up 0.25) && ((l'' <= h'') || (h'' <= Float_t.of_float Down 0.25)) then - (** case: contains at most one minimum*) - Interval (Float_t.of_float Down (-.1.), max (Float_t.sin Up l) (Float_t.sin Up h)) - else if (dist <= Float_t.of_float Down 1.) && (h'' <= Float_t.of_float Down 0.75) && ((l'' <= h'') || (l'' >= Float_t.of_float Up 0.75))then - (** case: contains at most one maximum*) - Interval (min (Float_t.sin Down l) (Float_t.sin Down h), Float_t.of_float Up 1.) - else - of_interval (-. 1., 1.) + let lcos = Float_t.sub Down l (Float_t.div Up Float_t.pi (Float_t.of_float Down 2.0)) in + let hcos = Float_t.sub Up h (Float_t.div Down Float_t.pi (Float_t.of_float Up 2.0)) in + eval_cos_cfun lcos hcos let eval_tan_cfun l h = let (dist, l'', h'') = project_and_compress l h 1. in From 6ea0a1c360daaefb1a0d64da4ec74de9a5695e21 Mon Sep 17 00:00:00 2001 From: FelixKrayer Date: Fri, 2 Feb 2024 09:20:02 +0100 Subject: [PATCH 11/24] fix comments and remove underapprox_pi --- src/cdomain/value/cdomains/floatDomain.ml | 39 +++++++++++------------ 1 file changed, 19 insertions(+), 20 deletions(-) diff --git a/src/cdomain/value/cdomains/floatDomain.ml b/src/cdomain/value/cdomains/floatDomain.ml index adda13bbcf..669429f457 100644 --- a/src/cdomain/value/cdomains/floatDomain.ml +++ b/src/cdomain/value/cdomains/floatDomain.ml @@ -273,12 +273,12 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct | _ -> Bot (** [widen x y] assumes [leq x y]. Solvers guarantee this by calling [widen old (join old new)]. *) - let widen v1 v2 = (**TODO: support 'threshold_widening' option *) + let widen v1 v2 = (* TODO: support 'threshold_widening' option *) match v1, v2 with | Top, _ | _, Top -> Top | Bot, v | v, Bot -> v | Interval (l1, h1), Interval (l2, h2) -> - (**If we widen and we know that neither interval contains +-inf or nan, it is ok to widen only to +-max_float, + (* If we widen and we know that neither interval contains +-inf or nan, it is ok to widen only to +-max_float, because a widening with +-inf/nan will always result in the case above -> Top *) let low = if l1 <= l2 then l1 else Float_t.lower_bound in let high = if h1 >= h2 then h1 else Float_t.upper_bound in @@ -289,7 +289,7 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct | _ -> Top let narrow v1 v2 = - match v1, v2 with (**we cannot distinguish between the lower bound beeing -inf or the upper bound beeing inf. Also there is nan *) + match v1, v2 with (* we cannot distinguish between the lower bound beeing -inf or the upper bound beeing inf. Also there is nan *) | Bot, _ | _, Bot -> Bot | Top, _ -> v2 | Interval (l1, h1), Interval (l2, h2) -> @@ -611,21 +611,20 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct else unknown_IInt () - (**it seems strange not to return an explicit 1 for negative numbers, but in c99 signbit is defined as: *) - (**<> *) + (**it seems strange not to return an explicit 1 for negative numbers, but in c99 signbit is defined as: + **<> *) let eval_signbit = function | (_, h) when h < Float_t.zero -> true_nonZero_IInt () | (l, _) when l > Float_t.zero -> false_zero_IInt () - | _ -> unknown_IInt () (**any interval containing zero has to fall in this case, because we do not distinguish between 0. and -0. *) + | _ -> unknown_IInt () (* any interval containing zero has to fall in this case, because we do not distinguish between 0. and -0. *) - (**These constants over-/underpproximate pi *) + (**This constant overapproximates pi *) let overapprox_pi = 3.1416 - let underapprox_pi = 3.1415 - (** this function does two things: *) - (** 1. projects l and h onto the interval [0, k*pi] (for k = 2 this is the phase length of sin/cos, for k = 1 it is the phase length of tan)*) - (** 2. compresses/transforms the interval [0, k*pi] to the interval [0, 1] to ease further computations *) - (** i.e. the it computes dist = distance, l'' = (l/(k*pi)) - floor(l/(k*pi)), h'' = (h/(k*pi)) - floor(h/(k*pi))*) + (** This function does two things: + ** 1. projects l and h onto the interval [0, k*pi] (for k = 2 this is the phase length of sin/cos, for k = 1 it is the phase length of tan) + ** 2. compresses/transforms the interval [0, k*pi] to the interval [0, 1] to ease further computations + ** i.e. the function computes dist = distance, l'' = (l/(k*pi)) - floor(l/(k*pi)), h'' = (h/(k*pi)) - floor(h/(k*pi))*) let project_and_compress l h k = let ft_over_kpi = (Float_t.mul Up (Float_t.of_float Up k) Float_t.pi) in let ft_under_kpi = (Float_t.mul Down (Float_t.of_float Down k) Float_t.pi) in @@ -656,16 +655,16 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct let (dist, l'', h'') = project_and_compress l h 2. in if Messages.tracing then Messages.trace "CstubsTrig" "cos: dist %s; l'' %s; h'' %s\n" (Float_t.to_string dist) (Float_t.to_string l'') (Float_t.to_string h''); if (dist <= Float_t.of_float Down 0.5) && (h'' <= Float_t.of_float Down 0.5) && (l'' <= h'') then - (** case: monotonic decreasing interval*) + (* case: monotonic decreasing interval*) Interval (Float_t.cos Down h, Float_t.cos Up l) else if (dist <= Float_t.of_float Down 0.5) && (l'' >= Float_t.of_float Up 0.5) && (l'' <= h'') then - (** case: monotonic increasing interval*) + (* case: monotonic increasing interval*) Interval (Float_t.cos Down l, Float_t.cos Up h) else if (dist <= Float_t.of_float Down 1.) && (l'' <= h'') then - (** case: contains at most one minimum*) + (* case: contains at most one minimum*) Interval (Float_t.of_float Down (-.1.), max (Float_t.cos Up l) (Float_t.cos Up h)) else if (dist <= Float_t.of_float Down 1.) && (l'' >= Float_t.of_float Up 0.5) && (h'' <= Float_t.of_float Down 0.5) then - (** case: contains at most one maximum*) + (* case: contains at most one maximum*) Interval (min (Float_t.cos Down l) (Float_t.cos Down h), Float_t.of_float Up 1.) else of_interval (-. 1., 1.) @@ -679,7 +678,7 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct let (dist, l'', h'') = project_and_compress l h 1. in if Messages.tracing then Messages.trace "CstubsTrig" "tan: dist %s; l'' %s; h'' %s\n" (Float_t.to_string dist) (Float_t.to_string l'') (Float_t.to_string h''); if (dist <= Float_t.of_float Down 1.) && (Bool.not ((l'' <= Float_t.of_float Up 0.5) && (h'' >= Float_t.of_float Up 0.5))) then - (** case: monotonic increasing interval*) + (* case: monotonic increasing interval*) Interval (Float_t.tan Down l, Float_t.tan Up h) else top () @@ -710,18 +709,18 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct | (l, h) when l < (Float_t.of_float Down (-.1.)) || h > (Float_t.of_float Up 1.) -> Messages.warn ~category:Messages.Category.Float "Domain error might occur: acos argument might be outside of [-1., 1.]"; of_interval (0., (overapprox_pi)) - | (l, h) -> norm @@ Interval (Float_t.acos Down h, Float_t.acos Up l) (** acos is monotonic decreasing in [-1, 1]*) + | (l, h) -> norm @@ Interval (Float_t.acos Down h, Float_t.acos Up l) (* acos is monotonic decreasing in [-1, 1]*) let eval_asin = function | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*asin(0) = 0*) | (l, h) when l < (Float_t.of_float Down (-.1.)) || h > (Float_t.of_float Up 1.) -> Messages.warn ~category:Messages.Category.Float "Domain error might occur: asin argument might be outside of [-1., 1.]"; div (of_interval ((-. overapprox_pi), overapprox_pi)) (of_const 2.) - | (l, h) -> norm @@ Interval (Float_t.asin Down l, Float_t.asin Up h) (** asin is monotonic increasing in [-1, 1]*) + | (l, h) -> norm @@ Interval (Float_t.asin Down l, Float_t.asin Up h) (* asin is monotonic increasing in [-1, 1]*) let eval_atan = function | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*atan(0) = 0*) - | (l, h) -> norm @@ Interval (Float_t.atan Down l, Float_t.atan Up h) (** atan is monotonic increasing*) + | (l, h) -> norm @@ Interval (Float_t.atan Down l, Float_t.atan Up h) (* atan is monotonic increasing*) let eval_cos = function | (l, h) when l = h && l = Float_t.zero -> of_const 1. (*cos(0) = 1*) From 203b52fe5e3bcdd6656659df635f15734d597996 Mon Sep 17 00:00:00 2001 From: FelixKrayer Date: Fri, 2 Feb 2024 10:28:59 +0100 Subject: [PATCH 12/24] remove overapprox_pi and replace with Float_t.pi --- src/cdomain/value/cdomains/floatDomain.ml | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/cdomain/value/cdomains/floatDomain.ml b/src/cdomain/value/cdomains/floatDomain.ml index 669429f457..eb16c11184 100644 --- a/src/cdomain/value/cdomains/floatDomain.ml +++ b/src/cdomain/value/cdomains/floatDomain.ml @@ -618,9 +618,6 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct | (l, _) when l > Float_t.zero -> false_zero_IInt () | _ -> unknown_IInt () (* any interval containing zero has to fall in this case, because we do not distinguish between 0. and -0. *) - (**This constant overapproximates pi *) - let overapprox_pi = 3.1416 - (** This function does two things: ** 1. projects l and h onto the interval [0, k*pi] (for k = 2 this is the phase length of sin/cos, for k = 1 it is the phase length of tan) ** 2. compresses/transforms the interval [0, k*pi] to the interval [0, 1] to ease further computations @@ -708,14 +705,14 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct | (l, h) when l = h && l = Float_t.of_float Nearest 1. -> of_const 0. (*acos(1) = 0*) | (l, h) when l < (Float_t.of_float Down (-.1.)) || h > (Float_t.of_float Up 1.) -> Messages.warn ~category:Messages.Category.Float "Domain error might occur: acos argument might be outside of [-1., 1.]"; - of_interval (0., (overapprox_pi)) + Interval (Float_t.of_float Down 0., Float_t.succ Float_t.pi) | (l, h) -> norm @@ Interval (Float_t.acos Down h, Float_t.acos Up l) (* acos is monotonic decreasing in [-1, 1]*) let eval_asin = function | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*asin(0) = 0*) | (l, h) when l < (Float_t.of_float Down (-.1.)) || h > (Float_t.of_float Up 1.) -> Messages.warn ~category:Messages.Category.Float "Domain error might occur: asin argument might be outside of [-1., 1.]"; - div (of_interval ((-. overapprox_pi), overapprox_pi)) (of_const 2.) + div (Interval (Float_t.pred (Float_t.neg Float_t.pi), Float_t.succ Float_t.pi)) (of_const 2.) | (l, h) -> norm @@ Interval (Float_t.asin Down l, Float_t.asin Up h) (* asin is monotonic increasing in [-1, 1]*) let eval_atan = function From eb7b597169c34c63a0f47eca13ba48586bc430c7 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Fri, 2 Feb 2024 13:22:50 +0100 Subject: [PATCH 13/24] add comment for float C stubs --- src/common/cdomains/floatOps/stubs.c | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/common/cdomains/floatOps/stubs.c b/src/common/cdomains/floatOps/stubs.c index 7c9c1aff9d..19e0ab5cfe 100644 --- a/src/common/cdomains/floatOps/stubs.c +++ b/src/common/cdomains/floatOps/stubs.c @@ -105,6 +105,8 @@ CAMLprim value atof_float(value mode, value str) return caml_copy_double(r); } +// These are only given for floats as these operations involve no rounding and their OCaml implementation (Float module) can be used + CAMLprim value max_float(value unit) { return caml_copy_double(FLT_MAX); From 2bf5854e2066f1d9b4343932253bca2fdda1d877 Mon Sep 17 00:00:00 2001 From: Felix Krayer Date: Fri, 2 Feb 2024 14:56:42 +0100 Subject: [PATCH 14/24] remove pred/succ and change asserts to goblint_check --- .../57-floats/22-trig_functions_c-stubs.c | 30 +++++++++---------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/tests/regression/57-floats/22-trig_functions_c-stubs.c b/tests/regression/57-floats/22-trig_functions_c-stubs.c index 1096abd591..2e34cb629f 100644 --- a/tests/regression/57-floats/22-trig_functions_c-stubs.c +++ b/tests/regression/57-floats/22-trig_functions_c-stubs.c @@ -1,7 +1,7 @@ // PARAM: --enable ana.float.interval -#include #include #include +#include int main() { @@ -40,28 +40,28 @@ int main() } //acos(x) - assert(1.4 < acos(0.1) && acos(0.1) < 1.5); // SUCCESS + __goblint_check(1.4 < acos(0.1) && acos(0.1) < 1.5); // SUCCESS //asin(x) - assert(0.6 < asin(0.6) && asin(0.6) < 0.7); // SUCCESS + __goblint_check(0.6 < asin(0.6) && asin(0.6) < 0.7); // SUCCESS //atan(x) - assert(0.7 < atan(1.) && atan(1.) < 0.8); // SUCCESS + __goblint_check(0.7 < atan(1.) && atan(1.) < 0.8); // SUCCESS //cos(x) - assert(-1. <= cos(c1) && cos(c1) < 0.99); // SUCCESS - assert(-0.99 < cos(c2) && cos(c2) <= 1.0); // SUCCESS - assert(-0.99 < cos(sc1) && cos(sc1) < 0.); // SUCCESS - assert(-0.99 < cos(sc2) && cos(sc2) < 0.); // SUCCESS + __goblint_check(-1. <= cos(c1) && cos(c1) < 0.99); // SUCCESS + __goblint_check(-0.99 < cos(c2) && cos(c2) <= 1.0); // SUCCESS + __goblint_check(-0.99 < cos(sc1) && cos(sc1) < 0.); // SUCCESS + __goblint_check(-0.99 < cos(sc2) && cos(sc2) < 0.); // SUCCESS //sin(x) - assert(-1. <= sin(s1) && sin(s1) < 0.99); // SUCCESS - assert(-0.99 < sin(s2) && sin(s2) <= 1.); // SUCCESS - assert(-0.99 < sin(s3) && sin(s3) <= 0.99); // SUCCESS - assert(0. < sin(sc1) && sin(sc1) < 0.99); // SUCCESS - assert(0. < sin(sc2) && sin(sc2) < 0.99); // SUCCESS + __goblint_check(-1. <= sin(s1) && sin(s1) < 0.99); // SUCCESS + __goblint_check(-0.99 < sin(s2) && sin(s2) <= 1.); // SUCCESS + __goblint_check(-0.99 < sin(s3) && sin(s3) <= 0.99); // SUCCESS + __goblint_check(0. < sin(sc1) && sin(sc1) < 0.99); // SUCCESS + __goblint_check(0. < sin(sc2) && sin(sc2) < 0.99); // SUCCESS //tan(x) - assert(-0.11 < tan(t1) && tan(t1) < 0.11 ); // SUCCESS - assert(-0.1 < tan(t2) && tan(t2) < 0.1 ); // SUCCESS + __goblint_check(-0.11 < tan(t1) && tan(t1) < 0.11 ); // SUCCESS + __goblint_check(-0.1 < tan(t2) && tan(t2) < 0.1 ); // SUCCESS } From 1668ca556419d86ed77948754ad974bf08147a6e Mon Sep 17 00:00:00 2001 From: Felix Krayer Date: Fri, 2 Feb 2024 14:58:31 +0100 Subject: [PATCH 15/24] remove pred/succ and change asserts to goblint_check --- src/cdomain/value/cdomains/floatDomain.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cdomain/value/cdomains/floatDomain.ml b/src/cdomain/value/cdomains/floatDomain.ml index eb16c11184..283806427f 100644 --- a/src/cdomain/value/cdomains/floatDomain.ml +++ b/src/cdomain/value/cdomains/floatDomain.ml @@ -705,14 +705,14 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct | (l, h) when l = h && l = Float_t.of_float Nearest 1. -> of_const 0. (*acos(1) = 0*) | (l, h) when l < (Float_t.of_float Down (-.1.)) || h > (Float_t.of_float Up 1.) -> Messages.warn ~category:Messages.Category.Float "Domain error might occur: acos argument might be outside of [-1., 1.]"; - Interval (Float_t.of_float Down 0., Float_t.succ Float_t.pi) + Interval (Float_t.of_float Down 0., Float_t.pi) | (l, h) -> norm @@ Interval (Float_t.acos Down h, Float_t.acos Up l) (* acos is monotonic decreasing in [-1, 1]*) let eval_asin = function | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*asin(0) = 0*) | (l, h) when l < (Float_t.of_float Down (-.1.)) || h > (Float_t.of_float Up 1.) -> Messages.warn ~category:Messages.Category.Float "Domain error might occur: asin argument might be outside of [-1., 1.]"; - div (Interval (Float_t.pred (Float_t.neg Float_t.pi), Float_t.succ Float_t.pi)) (of_const 2.) + div (Interval (Float_t.neg Float_t.pi, Float_t.pi)) (of_const 2.) | (l, h) -> norm @@ Interval (Float_t.asin Down l, Float_t.asin Up h) (* asin is monotonic increasing in [-1, 1]*) let eval_atan = function From c9eb861781d4d716d465d398ea65331c8cc9e072 Mon Sep 17 00:00:00 2001 From: Felix Krayer Date: Tue, 6 Feb 2024 16:19:53 +0100 Subject: [PATCH 16/24] change Float_t.to_string so all floats are differentiable --- src/common/cdomains/floatOps/floatOps.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/common/cdomains/floatOps/floatOps.ml b/src/common/cdomains/floatOps/floatOps.ml index 5bf717bfc3..4be98e0612 100644 --- a/src/common/cdomains/floatOps/floatOps.ml +++ b/src/common/cdomains/floatOps/floatOps.ml @@ -75,7 +75,7 @@ module CDouble = struct let succ = Float.succ let hash = Hashtbl.hash - let to_string = Float.to_string + let to_string = Printf.sprintf "%.17F" let neg = Float.neg let fabs = Float.abs @@ -118,7 +118,7 @@ module CFloat = struct let is_finite x = Float.is_finite x && x >= lower_bound && x <= upper_bound let hash = Hashtbl.hash - let to_string = Float.to_string + let to_string = Printf.sprintf "%.9F" let neg = Float.neg let fabs = Float.abs From bbef3158f2ffb7d6d62366817d02c2fc0cc2a85f Mon Sep 17 00:00:00 2001 From: FelixKrayer Date: Wed, 28 Feb 2024 09:36:39 +0100 Subject: [PATCH 17/24] Reintroduce math_funeval option with a few changes --- src/cdomain/value/cdomains/floatDomain.ml | 41 +++++++++++++++---- src/config/options.schema.json | 7 ++++ .../57-floats/22-trig_functions_c-stubs.c | 2 +- 3 files changed, 42 insertions(+), 8 deletions(-) diff --git a/src/cdomain/value/cdomains/floatDomain.ml b/src/cdomain/value/cdomains/floatDomain.ml index 283806427f..3912e3207e 100644 --- a/src/cdomain/value/cdomains/floatDomain.ml +++ b/src/cdomain/value/cdomains/floatDomain.ml @@ -5,6 +5,21 @@ open FloatOps exception ArithmeticOnFloatBot of string +(** Define records that hold mutable variables representing different Configuration values. + * These values are used to keep track of whether or not the corresponding Config values are en-/disabled *) +type ana_int_config_values = { + mutable math_fun_eval_cstub : bool option; +} + +let ana_int_config: ana_int_config_values = { + math_fun_eval_cstub = None; +} + +let get_math_fun_eval_cstub () = + if ana_int_config.math_fun_eval_cstub = None then + ana_int_config.math_fun_eval_cstub <- Some (GobConfig.get_bool "ana.float.math_fun_eval_cstub"); + Option.get ana_int_config.math_fun_eval_cstub + module type FloatArith = sig type t @@ -706,34 +721,46 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct | (l, h) when l < (Float_t.of_float Down (-.1.)) || h > (Float_t.of_float Up 1.) -> Messages.warn ~category:Messages.Category.Float "Domain error might occur: acos argument might be outside of [-1., 1.]"; Interval (Float_t.of_float Down 0., Float_t.pi) - | (l, h) -> norm @@ Interval (Float_t.acos Down h, Float_t.acos Up l) (* acos is monotonic decreasing in [-1, 1]*) + | (l, h) when get_math_fun_eval_cstub () -> + norm @@ Interval (Float_t.acos Down h, Float_t.acos Up l) (* acos is monotonic decreasing in [-1, 1]*) + | _ -> Interval (Float_t.of_float Down 0., Float_t.pi) let eval_asin = function | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*asin(0) = 0*) | (l, h) when l < (Float_t.of_float Down (-.1.)) || h > (Float_t.of_float Up 1.) -> Messages.warn ~category:Messages.Category.Float "Domain error might occur: asin argument might be outside of [-1., 1.]"; div (Interval (Float_t.neg Float_t.pi, Float_t.pi)) (of_const 2.) - | (l, h) -> norm @@ Interval (Float_t.asin Down l, Float_t.asin Up h) (* asin is monotonic increasing in [-1, 1]*) + | (l, h) when get_math_fun_eval_cstub () -> + norm @@ Interval (Float_t.asin Down l, Float_t.asin Up h) (* asin is monotonic increasing in [-1, 1]*) + | _ -> div (Interval (Float_t.neg Float_t.pi, Float_t.pi)) (of_const 2.) let eval_atan = function | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*atan(0) = 0*) - | (l, h) -> norm @@ Interval (Float_t.atan Down l, Float_t.atan Up h) (* atan is monotonic increasing*) + | (l, h) when get_math_fun_eval_cstub () -> + norm @@ Interval (Float_t.atan Down l, Float_t.atan Up h) (* atan is monotonic increasing*) + | _ -> div (Interval (Float_t.neg Float_t.pi, Float_t.pi)) (of_const 2.) let eval_cos = function | (l, h) when l = h && l = Float_t.zero -> of_const 1. (*cos(0) = 1*) - | (l, h) -> norm @@ eval_cos_cfun l h + | (l, h) when get_math_fun_eval_cstub () -> + norm @@ eval_cos_cfun l h + | _ -> of_interval (-. 1., 1.) let eval_sin = function | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*sin(0) = 0*) - | (l, h) -> norm @@ eval_sin_cfun l h + | (l, h) when get_math_fun_eval_cstub () -> + norm @@ eval_sin_cfun l h + | _ -> of_interval (-. 1., 1.) let eval_tan = function | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*tan(0) = 0*) - | (l, h) -> norm @@ eval_tan_cfun l h + | (l, h) when get_math_fun_eval_cstub () -> + norm @@ eval_tan_cfun l h + | _ -> top () let eval_sqrt = function | (l, h) when l = Float_t.zero && h = Float_t.zero -> of_const 0. - | (l, h) when l >= Float_t.zero -> + | (l, h) when l >= Float_t.zero && get_math_fun_eval_cstub () -> let low = Float_t.sqrt Down l in let high = Float_t.sqrt Up h in Interval (low, high) diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 0c83e342e0..afeab6ddb3 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -463,6 +463,13 @@ "Use FloatDomain: (float * float) option.", "type": "boolean", "default": false + }, + "math_fun_eval_cstub": { + "title": "ana.float.math_fun_eval_cstub", + "description": + "Allow evaluation of functions from math.h using C-stubs. Evaluation of functions may differ depending on the implementation of math.h. Only produces sound results, if the analyzed program and Goblint are used with the same version of math.h.", + "type": "boolean", + "default": false } }, "additionalProperties": false diff --git a/tests/regression/57-floats/22-trig_functions_c-stubs.c b/tests/regression/57-floats/22-trig_functions_c-stubs.c index 2e34cb629f..8c5a7604dd 100644 --- a/tests/regression/57-floats/22-trig_functions_c-stubs.c +++ b/tests/regression/57-floats/22-trig_functions_c-stubs.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.float.interval +// PARAM: --enable ana.float.interval --enable ana.float.math_fun_eval_cstub #include #include #include From d454cb4d31bd74d5104d76244657fcc19d36b16f Mon Sep 17 00:00:00 2001 From: FelixKrayer Date: Wed, 28 Feb 2024 10:00:52 +0100 Subject: [PATCH 18/24] guard usages of math functions by max/min of both rounding modes --- src/cdomain/value/cdomains/floatDomain.ml | 25 ++++++++++++++--------- 1 file changed, 15 insertions(+), 10 deletions(-) diff --git a/src/cdomain/value/cdomains/floatDomain.ml b/src/cdomain/value/cdomains/floatDomain.ml index 3912e3207e..1e24a3bc36 100644 --- a/src/cdomain/value/cdomains/floatDomain.ml +++ b/src/cdomain/value/cdomains/floatDomain.ml @@ -633,6 +633,11 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct | (l, _) when l > Float_t.zero -> false_zero_IInt () | _ -> unknown_IInt () (* any interval containing zero has to fall in this case, because we do not distinguish between 0. and -0. *) + (** returns the max of the given mfun once computed with rounding mode Up and once with rounding mode down*) + let safe_mathfun_up mfun f = max (mfun Down f) (mfun Up f) + (** returns the min of the given mfun once computed with rounding mode Up and once with rounding mode down*) + let safe_mathfun_down mfun f = min (mfun Down f) (mfun Up f) + (** This function does two things: ** 1. projects l and h onto the interval [0, k*pi] (for k = 2 this is the phase length of sin/cos, for k = 1 it is the phase length of tan) ** 2. compresses/transforms the interval [0, k*pi] to the interval [0, 1] to ease further computations @@ -668,16 +673,16 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct if Messages.tracing then Messages.trace "CstubsTrig" "cos: dist %s; l'' %s; h'' %s\n" (Float_t.to_string dist) (Float_t.to_string l'') (Float_t.to_string h''); if (dist <= Float_t.of_float Down 0.5) && (h'' <= Float_t.of_float Down 0.5) && (l'' <= h'') then (* case: monotonic decreasing interval*) - Interval (Float_t.cos Down h, Float_t.cos Up l) + Interval (safe_mathfun_down Float_t.cos h, safe_mathfun_up Float_t.cos l) else if (dist <= Float_t.of_float Down 0.5) && (l'' >= Float_t.of_float Up 0.5) && (l'' <= h'') then (* case: monotonic increasing interval*) - Interval (Float_t.cos Down l, Float_t.cos Up h) + Interval (safe_mathfun_down Float_t.cos l, safe_mathfun_up Float_t.cos h) else if (dist <= Float_t.of_float Down 1.) && (l'' <= h'') then (* case: contains at most one minimum*) - Interval (Float_t.of_float Down (-.1.), max (Float_t.cos Up l) (Float_t.cos Up h)) + Interval (Float_t.of_float Down (-.1.), max (safe_mathfun_up Float_t.cos l) (safe_mathfun_up Float_t.cos h)) else if (dist <= Float_t.of_float Down 1.) && (l'' >= Float_t.of_float Up 0.5) && (h'' <= Float_t.of_float Down 0.5) then (* case: contains at most one maximum*) - Interval (min (Float_t.cos Down l) (Float_t.cos Down h), Float_t.of_float Up 1.) + Interval (min (safe_mathfun_down Float_t.cos l) (safe_mathfun_down Float_t.cos h), Float_t.of_float Up 1.) else of_interval (-. 1., 1.) @@ -691,7 +696,7 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct if Messages.tracing then Messages.trace "CstubsTrig" "tan: dist %s; l'' %s; h'' %s\n" (Float_t.to_string dist) (Float_t.to_string l'') (Float_t.to_string h''); if (dist <= Float_t.of_float Down 1.) && (Bool.not ((l'' <= Float_t.of_float Up 0.5) && (h'' >= Float_t.of_float Up 0.5))) then (* case: monotonic increasing interval*) - Interval (Float_t.tan Down l, Float_t.tan Up h) + Interval (safe_mathfun_down Float_t.tan l, safe_mathfun_up Float_t.tan h) else top () @@ -722,7 +727,7 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct Messages.warn ~category:Messages.Category.Float "Domain error might occur: acos argument might be outside of [-1., 1.]"; Interval (Float_t.of_float Down 0., Float_t.pi) | (l, h) when get_math_fun_eval_cstub () -> - norm @@ Interval (Float_t.acos Down h, Float_t.acos Up l) (* acos is monotonic decreasing in [-1, 1]*) + norm @@ Interval (safe_mathfun_down Float_t.acos h, safe_mathfun_up Float_t.acos l) (* acos is monotonic decreasing in [-1, 1]*) | _ -> Interval (Float_t.of_float Down 0., Float_t.pi) let eval_asin = function @@ -731,13 +736,13 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct Messages.warn ~category:Messages.Category.Float "Domain error might occur: asin argument might be outside of [-1., 1.]"; div (Interval (Float_t.neg Float_t.pi, Float_t.pi)) (of_const 2.) | (l, h) when get_math_fun_eval_cstub () -> - norm @@ Interval (Float_t.asin Down l, Float_t.asin Up h) (* asin is monotonic increasing in [-1, 1]*) + norm @@ Interval (safe_mathfun_down Float_t.asin l, safe_mathfun_up Float_t.asin h) (* asin is monotonic increasing in [-1, 1]*) | _ -> div (Interval (Float_t.neg Float_t.pi, Float_t.pi)) (of_const 2.) let eval_atan = function | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*atan(0) = 0*) | (l, h) when get_math_fun_eval_cstub () -> - norm @@ Interval (Float_t.atan Down l, Float_t.atan Up h) (* atan is monotonic increasing*) + norm @@ Interval (safe_mathfun_down Float_t.atan l, safe_mathfun_up Float_t.atan h) (* atan is monotonic increasing*) | _ -> div (Interval (Float_t.neg Float_t.pi, Float_t.pi)) (of_const 2.) let eval_cos = function @@ -761,8 +766,8 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct let eval_sqrt = function | (l, h) when l = Float_t.zero && h = Float_t.zero -> of_const 0. | (l, h) when l >= Float_t.zero && get_math_fun_eval_cstub () -> - let low = Float_t.sqrt Down l in - let high = Float_t.sqrt Up h in + let low = safe_mathfun_down Float_t.sqrt l in + let high = safe_mathfun_up Float_t.sqrt h in Interval (low, high) | _ -> top () From 407d58ece35681b41985bf65da49ac083a0ff6ce Mon Sep 17 00:00:00 2001 From: Felix Krayer Date: Thu, 29 Feb 2024 03:56:24 +0100 Subject: [PATCH 19/24] activate ana.float.math_fun_eval_cstub on regtests with sqrt --- tests/regression/39-signed-overflows/07-abs-sqrt.c | 2 +- tests/regression/39-signed-overflows/09-labs-sqrt.c | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/regression/39-signed-overflows/07-abs-sqrt.c b/tests/regression/39-signed-overflows/07-abs-sqrt.c index 13ed863e51..fa7cd2ea66 100644 --- a/tests/regression/39-signed-overflows/07-abs-sqrt.c +++ b/tests/regression/39-signed-overflows/07-abs-sqrt.c @@ -1,4 +1,4 @@ -//PARAM: --enable ana.int.interval --enable ana.float.interval --set ana.activated[+] tmpSpecial +//PARAM: --enable ana.int.interval --enable ana.float.interval --enable ana.float.math_fun_eval_cstub --set ana.activated[+] tmpSpecial #include int main() { int data; diff --git a/tests/regression/39-signed-overflows/09-labs-sqrt.c b/tests/regression/39-signed-overflows/09-labs-sqrt.c index 3a4b20a82b..7542882463 100644 --- a/tests/regression/39-signed-overflows/09-labs-sqrt.c +++ b/tests/regression/39-signed-overflows/09-labs-sqrt.c @@ -1,4 +1,4 @@ -//PARAM: --enable ana.int.interval --enable ana.float.interval --set ana.activated[+] tmpSpecial +//PARAM: --enable ana.int.interval --enable ana.float.interval --enable ana.float.math_fun_eval_cstub --set ana.activated[+] tmpSpecial #include int main() { int data; From 920b3fc591567d9561d5e85edfdfa95b70a336ba Mon Sep 17 00:00:00 2001 From: Felix Krayer Date: Sun, 10 Mar 2024 18:07:03 +0100 Subject: [PATCH 20/24] rename option, better description, add reset_lazy --- src/cdomain/value/cdomains/floatDomain.ml | 32 ++++++++++--------- src/cdomain/value/cdomains/floatDomain.mli | 2 ++ src/config/options.schema.json | 6 ++-- src/util/server.ml | 1 + .../39-signed-overflows/07-abs-sqrt.c | 2 +- .../39-signed-overflows/09-labs-sqrt.c | 2 +- .../57-floats/23-trig_functions_c-stubs.c | 2 +- 7 files changed, 26 insertions(+), 21 deletions(-) diff --git a/src/cdomain/value/cdomains/floatDomain.ml b/src/cdomain/value/cdomains/floatDomain.ml index f86e93bb1f..503feba88e 100644 --- a/src/cdomain/value/cdomains/floatDomain.ml +++ b/src/cdomain/value/cdomains/floatDomain.ml @@ -7,18 +7,20 @@ exception ArithmeticOnFloatBot of string (** Define records that hold mutable variables representing different Configuration values. * These values are used to keep track of whether or not the corresponding Config values are en-/disabled *) -type ana_int_config_values = { - mutable math_fun_eval_cstub : bool option; +type ana_float_config_values = { + mutable evaluate_math_functions : bool option; } -let ana_int_config: ana_int_config_values = { - math_fun_eval_cstub = None; +let ana_float_config: ana_float_config_values = { + evaluate_math_functions = None; } -let get_math_fun_eval_cstub () = - if ana_int_config.math_fun_eval_cstub = None then - ana_int_config.math_fun_eval_cstub <- Some (GobConfig.get_bool "ana.float.math_fun_eval_cstub"); - Option.get ana_int_config.math_fun_eval_cstub +let get_evaluate_math_functions () = + if ana_float_config.evaluate_math_functions = None then + ana_float_config.evaluate_math_functions <- Some (GobConfig.get_bool "ana.float.evaluate_math_functions"); + Option.get ana_float_config.evaluate_math_functions + +let reset_lazy () = ana_float_config.evaluate_math_functions <- None module type FloatArith = sig type t @@ -738,7 +740,7 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct | (l, h) when l < (Float_t.of_float Down (-.1.)) || h > (Float_t.of_float Up 1.) -> Messages.warn ~category:Messages.Category.Float "Domain error might occur: acos argument might be outside of [-1., 1.]"; Interval (Float_t.of_float Down 0., Float_t.pi) - | (l, h) when get_math_fun_eval_cstub () -> + | (l, h) when get_evaluate_math_functions () -> norm @@ Interval (safe_mathfun_down Float_t.acos h, safe_mathfun_up Float_t.acos l) (* acos is monotonic decreasing in [-1, 1]*) | _ -> Interval (Float_t.of_float Down 0., Float_t.pi) @@ -747,37 +749,37 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct | (l, h) when l < (Float_t.of_float Down (-.1.)) || h > (Float_t.of_float Up 1.) -> Messages.warn ~category:Messages.Category.Float "Domain error might occur: asin argument might be outside of [-1., 1.]"; div (Interval (Float_t.neg Float_t.pi, Float_t.pi)) (of_const 2.) - | (l, h) when get_math_fun_eval_cstub () -> + | (l, h) when get_evaluate_math_functions () -> norm @@ Interval (safe_mathfun_down Float_t.asin l, safe_mathfun_up Float_t.asin h) (* asin is monotonic increasing in [-1, 1]*) | _ -> div (Interval (Float_t.neg Float_t.pi, Float_t.pi)) (of_const 2.) let eval_atan = function | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*atan(0) = 0*) - | (l, h) when get_math_fun_eval_cstub () -> + | (l, h) when get_evaluate_math_functions () -> norm @@ Interval (safe_mathfun_down Float_t.atan l, safe_mathfun_up Float_t.atan h) (* atan is monotonic increasing*) | _ -> div (Interval (Float_t.neg Float_t.pi, Float_t.pi)) (of_const 2.) let eval_cos = function | (l, h) when l = h && l = Float_t.zero -> of_const 1. (*cos(0) = 1*) - | (l, h) when get_math_fun_eval_cstub () -> + | (l, h) when get_evaluate_math_functions () -> norm @@ eval_cos_cfun l h | _ -> of_interval (-. 1., 1.) let eval_sin = function | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*sin(0) = 0*) - | (l, h) when get_math_fun_eval_cstub () -> + | (l, h) when get_evaluate_math_functions () -> norm @@ eval_sin_cfun l h | _ -> of_interval (-. 1., 1.) let eval_tan = function | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*tan(0) = 0*) - | (l, h) when get_math_fun_eval_cstub () -> + | (l, h) when get_evaluate_math_functions () -> norm @@ eval_tan_cfun l h | _ -> top () let eval_sqrt = function | (l, h) when l = Float_t.zero && h = Float_t.zero -> of_const 0. - | (l, h) when l >= Float_t.zero && get_math_fun_eval_cstub () -> + | (l, h) when l >= Float_t.zero && get_evaluate_math_functions () -> let low = safe_mathfun_down Float_t.sqrt l in let high = safe_mathfun_up Float_t.sqrt h in Interval (low, high) diff --git a/src/cdomain/value/cdomains/floatDomain.mli b/src/cdomain/value/cdomains/floatDomain.mli index d958e1ee81..b672bbdf34 100644 --- a/src/cdomain/value/cdomains/floatDomain.mli +++ b/src/cdomain/value/cdomains/floatDomain.mli @@ -4,6 +4,8 @@ open GoblintCil exception ArithmeticOnFloatBot of string +val reset_lazy: unit -> unit + module type FloatArith = sig type t diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 0005b77031..8e4ca51fee 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -464,10 +464,10 @@ "type": "boolean", "default": false }, - "math_fun_eval_cstub": { - "title": "ana.float.math_fun_eval_cstub", + "evaluate_math_functions": { + "title": "ana.float.evaluate_math_functions", "description": - "Allow evaluation of functions from math.h using C-stubs. Evaluation of functions may differ depending on the implementation of math.h. Only produces sound results, if the analyzed program and Goblint are used with the same version of math.h.", + "Allow a more precise evaluation of some functions from math.h. Evaluation of functions may differ depending on the implementation of math.h. Caution: For some implementations of functions it is not guaranteed that they behave monotonic where they mathematically should, thus possibly leading to unsoundness.", "type": "boolean", "default": false } diff --git a/src/util/server.ml b/src/util/server.ml index 31e1036652..6f760e6856 100644 --- a/src/util/server.ml +++ b/src/util/server.ml @@ -284,6 +284,7 @@ let analyze ?(reset=false) (s: t) = InvariantCil.reset_lazy (); WideningThresholds.reset_lazy (); IntDomain.reset_lazy (); + FloatDomain.reset_lazy (); StringDomain.reset_lazy (); PrecisionUtil.reset_lazy (); ApronDomain.reset_lazy (); diff --git a/tests/regression/39-signed-overflows/07-abs-sqrt.c b/tests/regression/39-signed-overflows/07-abs-sqrt.c index fa7cd2ea66..e1e5462362 100644 --- a/tests/regression/39-signed-overflows/07-abs-sqrt.c +++ b/tests/regression/39-signed-overflows/07-abs-sqrt.c @@ -1,4 +1,4 @@ -//PARAM: --enable ana.int.interval --enable ana.float.interval --enable ana.float.math_fun_eval_cstub --set ana.activated[+] tmpSpecial +//PARAM: --enable ana.int.interval --enable ana.float.interval --enable ana.float.evaluate_math_functions --set ana.activated[+] tmpSpecial #include int main() { int data; diff --git a/tests/regression/39-signed-overflows/09-labs-sqrt.c b/tests/regression/39-signed-overflows/09-labs-sqrt.c index 7542882463..8ec231c879 100644 --- a/tests/regression/39-signed-overflows/09-labs-sqrt.c +++ b/tests/regression/39-signed-overflows/09-labs-sqrt.c @@ -1,4 +1,4 @@ -//PARAM: --enable ana.int.interval --enable ana.float.interval --enable ana.float.math_fun_eval_cstub --set ana.activated[+] tmpSpecial +//PARAM: --enable ana.int.interval --enable ana.float.interval --enable ana.float.evaluate_math_functions --set ana.activated[+] tmpSpecial #include int main() { int data; diff --git a/tests/regression/57-floats/23-trig_functions_c-stubs.c b/tests/regression/57-floats/23-trig_functions_c-stubs.c index 8c5a7604dd..7c764a53e4 100644 --- a/tests/regression/57-floats/23-trig_functions_c-stubs.c +++ b/tests/regression/57-floats/23-trig_functions_c-stubs.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.float.interval --enable ana.float.math_fun_eval_cstub +// PARAM: --enable ana.float.interval --enable ana.float.evaluate_math_functions #include #include #include From 0e387a202b875b31156515fdbcfb7af5feeee803 Mon Sep 17 00:00:00 2001 From: Felix Krayer Date: Sun, 10 Mar 2024 18:17:23 +0100 Subject: [PATCH 21/24] Revert "change Float_t.to_string so all floats are differentiable" This reverts commit c9eb861781d4d716d465d398ea65331c8cc9e072. --- src/common/cdomains/floatOps/floatOps.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/common/cdomains/floatOps/floatOps.ml b/src/common/cdomains/floatOps/floatOps.ml index 02e88fd13d..2a60ec515b 100644 --- a/src/common/cdomains/floatOps/floatOps.ml +++ b/src/common/cdomains/floatOps/floatOps.ml @@ -76,7 +76,7 @@ module CDouble = struct let succ = Float.succ let hash = Hashtbl.hash - let to_string = Printf.sprintf "%.17F" + let to_string = Float.to_string let neg = Float.neg let fabs = Float.abs @@ -119,7 +119,7 @@ module CFloat = struct let is_finite x = Float.is_finite x && x >= lower_bound && x <= upper_bound let hash = Hashtbl.hash - let to_string = Printf.sprintf "%.9F" + let to_string = Float.to_string let neg = Float.neg let fabs = Float.abs From 47154e4bff3fc73431cf1d9a31d818b3a049bcf4 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Mon, 11 Mar 2024 13:46:21 +0100 Subject: [PATCH 22/24] rename pi to pi_float --- src/common/cdomains/floatOps/floatOps.ml | 2 +- src/common/cdomains/floatOps/stubs.c | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/common/cdomains/floatOps/floatOps.ml b/src/common/cdomains/floatOps/floatOps.ml index 2a60ec515b..ecfc6436d4 100644 --- a/src/common/cdomains/floatOps/floatOps.ml +++ b/src/common/cdomains/floatOps/floatOps.ml @@ -106,7 +106,7 @@ module CFloat = struct external upper': unit -> float = "max_float" external smallest': unit -> float = "smallest_float" - external pi': unit -> float = "pi" + external pi': unit -> float = "pi_float" let upper_bound = upper' () let lower_bound = -. upper_bound diff --git a/src/common/cdomains/floatOps/stubs.c b/src/common/cdomains/floatOps/stubs.c index 9d93b48935..ba1520c703 100644 --- a/src/common/cdomains/floatOps/stubs.c +++ b/src/common/cdomains/floatOps/stubs.c @@ -140,7 +140,7 @@ CAMLprim value smallest_float(value unit) // No need to use CAMLreturn because we don't use CAMLparam. } -CAMLprim value pi(value unit) +CAMLprim value pi_float(value unit) { return caml_copy_double(M_PI); } From 02afa4a478b2e32cd3d20a71da8c5e6238964dcc Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Mon, 11 Mar 2024 13:46:54 +0100 Subject: [PATCH 23/24] update GobView submodule --- gobview | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/gobview b/gobview index 1d29c9f0c9..74e2958708 160000 --- a/gobview +++ b/gobview @@ -1 +1 @@ -Subproject commit 1d29c9f0c93c0f334055b1884c81729df38627e7 +Subproject commit 74e295870848c66885fa446970b0c59617a242a7 From 5c3df9395549af86f97825191e258d9761b431a6 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Mon, 11 Mar 2024 13:47:26 +0100 Subject: [PATCH 24/24] add comment for _GNU_SOURCE --- src/common/cdomains/floatOps/stubs.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/common/cdomains/floatOps/stubs.c b/src/common/cdomains/floatOps/stubs.c index ba1520c703..213eacba22 100644 --- a/src/common/cdomains/floatOps/stubs.c +++ b/src/common/cdomains/floatOps/stubs.c @@ -1,4 +1,4 @@ -#define _GNU_SOURCE +#define _GNU_SOURCE // necessary for M_PI to be defined #include #include #include