From a79eb9aff52ca0f940f88d7ab741bd87026f0e61 Mon Sep 17 00:00:00 2001 From: FelixKrayer Date: Mon, 25 Jul 2022 17:40:30 +0200 Subject: [PATCH 01/55] 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/55] 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/55] 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/55] 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/55] 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/55] 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/55] 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/55] 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/55] 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/55] 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/55] 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/55] 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/55] 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/55] 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/55] 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 978b5e6c1cda8cd612f1011d4268e79718b5c931 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 6 Feb 2024 12:21:10 +0100 Subject: [PATCH 16/55] Add failing test case. --- .../regression/46-apron2/61-context-insens.c | 46 +++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 tests/regression/46-apron2/61-context-insens.c diff --git a/tests/regression/46-apron2/61-context-insens.c b/tests/regression/46-apron2/61-context-insens.c new file mode 100644 index 0000000000..43b7c412cc --- /dev/null +++ b/tests/regression/46-apron2/61-context-insens.c @@ -0,0 +1,46 @@ +// PARAM: --set ana.activated "['base', 'threadid', 'threadflag', 'threadreturn','mallocWrapper','mutexEvents','mutex','access','race','escape','expRelation','assert','var_eq','symb_locks','apron','memLeak']" --enable ana.int.interval_set --set ana.ctx_insens "['base', 'threadid', 'threadflag', 'threadreturn','mallocWrapper','mutexEvents','mutex','access','race','escape','expRelation','assert','var_eq','symb_locks','apron','memLeak']" --enable ana.autotune.enabled --set ana.autotune.activated "['octagon']" --set ana.specification "CHECK( init(main()), LTL(G valid-memcleanup) )" --set ana.path_sens "['mutex', 'malloc_null', 'uninit','expsplit','activeSetjmp','memLeak', 'threadflag']" --set ana.malloc.unique_address_count 5 + +// Adapted from https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/list-properties/list_search-1.c +#include +#include +#include + +typedef struct list { + int key; + struct list *next; +} mlist; + +mlist *head; + +mlist* search(mlist *l, int k){ + l = head; + while(l!=0 && l->key!=k) { // Used to detect dead code after loop head + l = l->next; + } + return l; +} + +int insert(mlist *l, int k){ + l = (mlist*)malloc(sizeof(mlist)); + l->key = k; + if (head==0) { + } else { + l->key = k; + l->next = head; + } + head = l; + return 0; +} + +int main(void){ + int i; + mlist *mylist, *temp; + insert(mylist,2); + insert(mylist,5); + + temp = search(head,2); + + __goblint_check(1); // Should be reachable + return 0; +} + From 554a5f03a94b09aae1d17277ebb8ba9bc3a7f0cc Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 6 Feb 2024 12:29:29 +0100 Subject: [PATCH 17/55] apronDomain.join: Check for is_bot_env instead of is_bot. is_bot returned true for some elements for which is_top_env returned true, leading to too small values being returned. --- src/cdomains/apron/apronDomain.apron.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index e78176fc41..01827d9437 100644 --- a/src/cdomains/apron/apronDomain.apron.ml +++ b/src/cdomains/apron/apronDomain.apron.ml @@ -672,9 +672,9 @@ struct let join x y = (* just to optimize joining folds, which start with bot *) - if is_bot x then (* TODO: also for non-empty env *) + if is_bot_env x then (* TODO: also for non-empty env *) y - else if is_bot y then (* TODO: also for non-empty env *) + else if is_bot_env y then (* TODO: also for non-empty env *) x else ( if M.tracing then M.traceli "apron" "join %a %a\n" pretty x pretty y; From c9eb861781d4d716d465d398ea65331c8cc9e072 Mon Sep 17 00:00:00 2001 From: Felix Krayer Date: Tue, 6 Feb 2024 16:19:53 +0100 Subject: [PATCH 18/55] 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 231179560acf80a20dade058eb3285e7d34fe07c Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 6 Feb 2024 18:09:21 +0100 Subject: [PATCH 19/55] Define bot and top in apron domain correctly. --- src/analyses/apron/relationAnalysis.apron.ml | 6 +++--- src/cdomains/apron/apronDomain.apron.ml | 10 +++++----- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index ea570b338a..3b752a7b53 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -44,10 +44,10 @@ struct if ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.relation.context" ~removeAttr:"relation.no-context" ~keepAttr:"relation.context" fd then x else - D.bot () (* just like startstate, heterogeneous RD.bot () means top over empty set of variables *) + D.top () - let exitstate _ = { rel = RD.bot (); priv = Priv.startstate () } - let startstate _ = { rel = RD.bot (); priv = Priv.startstate () } + let exitstate _ = { rel = RD.top (); priv = Priv.startstate () } + let startstate _ = { rel = RD.top (); priv = Priv.startstate () } (* Functions for manipulating globals as temporary locals. *) diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index 01827d9437..f60790845b 100644 --- a/src/cdomains/apron/apronDomain.apron.ml +++ b/src/cdomains/apron/apronDomain.apron.ml @@ -660,21 +660,21 @@ struct let empty_env = Environment.make [||] [||] let bot () = - top_env empty_env + bot_env empty_env let top () = - failwith "D2.top" + top_env empty_env let is_bot = equal (bot ()) - let is_top _ = false + let is_top = equal (top ()) let strengthening_enabled = GobConfig.get_bool "ana.apron.strengthening" let join x y = (* just to optimize joining folds, which start with bot *) - if is_bot_env x then (* TODO: also for non-empty env *) + if is_bot x then (* TODO: also for non-empty env *) y - else if is_bot_env y then (* TODO: also for non-empty env *) + else if is_bot y then (* TODO: also for non-empty env *) x else ( if M.tracing then M.traceli "apron" "join %a %a\n" pretty x pretty y; From 8848276821cf785b3106cfb29afccfb9351235b7 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 6 Feb 2024 18:31:47 +0100 Subject: [PATCH 20/55] Adapt relationPriv for bot being proper bot. --- src/analyses/apron/relationPriv.apron.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index b4e23b65cc..669bf1e9a5 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -127,7 +127,7 @@ struct {st with rel = rel_local} let threadenter ask getg (st: relation_components_t): relation_components_t = - {rel = RD.bot (); priv = startstate ()} + {rel = RD.top (); priv = startstate ()} let iter_sys_vars getg vq vf = () let invariant_vars ask getg st = [] @@ -599,7 +599,7 @@ struct List.fold_left (fun st v -> escape_one v st) st esc_vars let threadenter ask getg (st: relation_components_t): relation_components_t = - {rel = RD.bot (); priv = startstate ()} + {rel = RD.top (); priv = startstate ()} let init () = () let finalize () = () @@ -732,7 +732,7 @@ struct let lock_get_m oct local_m get_m = let joined = LRD.join local_m get_m in if M.tracing then M.traceli "relationpriv" "lock_get_m:\n get=%a\n joined=%a\n" LRD.pretty get_m LRD.pretty joined; - let r = LRD.fold (fun _ -> RD.meet) joined (RD.bot ()) in (* bot is top with empty env *) + let r = LRD.fold (fun _ -> RD.meet) joined (RD.top ()) in if M.tracing then M.trace "relationpriv" "meet=%a\n" RD.pretty r; let r = RD.meet oct r in if M.tracing then M.traceu "relationpriv" "-> %a\n" RD.pretty r; @@ -1075,7 +1075,7 @@ struct let threadenter ask getg (st: relation_components_t): relation_components_t = let _,lmust,l = st.priv in - {rel = RD.bot (); priv = (W.bot (),lmust,l)} + {rel = RD.top (); priv = (W.bot (),lmust,l)} let iter_sys_vars getg vq vf = match vq with From d2ffcf02e35c53aea55c3e79e3845d5ea1dcfd33 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 18 Feb 2024 15:35:47 +0100 Subject: [PATCH 21/55] Do not side-effect empty relationship --- src/analyses/apron/relationPriv.apron.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 669bf1e9a5..321025d2e2 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -565,7 +565,9 @@ struct ) (RD.vars rel) in let rel_side = RD.keep_vars rel g_vars in - sideg V.mutex_inits rel_side; + (* If no globals are contained here, none need to be published *) + (* https://github.com/goblint/analyzer/pull/1354 *) + if g_vars <> [] then sideg V.mutex_inits rel_side; let rel_local = RD.remove_filter rel (fun var -> match AV.find_metadata var with | Some (Global g) -> is_unprotected ask g From b57fd0ff52e3a52052c8d75885ffb344f50b46e1 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 18 Feb 2024 16:19:47 +0100 Subject: [PATCH 22/55] Fix escape handling --- src/analyses/apron/relationPriv.apron.ml | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 321025d2e2..47593a8aa3 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -480,7 +480,11 @@ struct let get_mutex_inits = getg V.mutex_inits in let g_var = AV.global g in let get_mutex_inits' = RD.keep_vars get_mutex_inits [g_var] in - RD.join get_mutex_global_g get_mutex_inits' + if not (RD.mem_var get_mutex_inits' g_var) then + (* This is an escaped variable whose value was never side-effected to get_mutex_inits' *) + get_mutex_global_g + else + RD.join get_mutex_global_g get_mutex_inits' let read_global ask getg (st: relation_components_t) g x: RD.t = let rel = st.rel in @@ -500,10 +504,11 @@ struct in rel_local' - let write_global ?(invariant=false) ask getg sideg (st: relation_components_t) g x: relation_components_t = + (* Like write global but has option to skip meet with current value, as the value will not have been side-effected to a useful location thus far *) + let write_global_internal ?(skip_meet=false) ?(invariant=false) ask getg sideg (st: relation_components_t) g x: relation_components_t = let rel = st.rel in (* lock *) - let rel = RD.meet rel (get_mutex_global_g_with_mutex_inits ask getg g) in + let rel = if not skip_meet then RD.meet rel (get_mutex_global_g_with_mutex_inits ask getg g) else rel in (* write *) let g_var = AV.global g in let x_var = AV.local x in @@ -520,6 +525,9 @@ struct in {st with rel = rel_local'} + let write_global = write_global_internal ~skip_meet:false + let write_escape = write_global_internal ~skip_meet:true + let lock ask getg (st: relation_components_t) m = (* TODO: somehow actually unneeded here? *) if Locksets.(not (Lockset.mem m (current_lockset ask))) then ( @@ -597,7 +605,7 @@ struct let escape node ask getg sideg (st:relation_components_t) escaped : relation_components_t = let esc_vars = EscapeDomain.EscapedVars.elements escaped in let esc_vars = List.filter (fun v -> not v.vglob && RD.Tracked.varinfo_tracked v && RD.mem_var st.rel (AV.local v)) esc_vars in - let escape_one (x:varinfo) st = write_global ask getg sideg st x x in + let escape_one (x:varinfo) st = write_escape ask getg sideg st x x in List.fold_left (fun st v -> escape_one v st) st esc_vars let threadenter ask getg (st: relation_components_t): relation_components_t = From 8787f5942a197bdde612388dda75f40584b70de9 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 18 Feb 2024 16:29:02 +0100 Subject: [PATCH 23/55] Add a top to `affeq`? --- src/cdomains/apron/affineEqualityDomain.apron.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index ea8a350d3c..55589c6741 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -307,7 +307,7 @@ struct let is_bot_env t = t.d = None - let top () = failwith "D.top ()" + let top () = {d = Some (Matrix.empty ()); env = Environment.make [||] [||]} let is_top _ = false From bbef3158f2ffb7d6d62366817d02c2fc0cc2a85f Mon Sep 17 00:00:00 2001 From: FelixKrayer Date: Wed, 28 Feb 2024 09:36:39 +0100 Subject: [PATCH 24/55] 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 25/55] 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 26/55] 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 5f7ce7f4fc4bbd7421aebd0e75db05163426e643 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 3 Mar 2024 11:56:06 +0100 Subject: [PATCH 27/55] Comment about top and bot over empty environment being different --- src/cdomains/apron/apronDomain.apron.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index f30030efef..fbfddbe94d 100644 --- a/src/cdomains/apron/apronDomain.apron.ml +++ b/src/cdomains/apron/apronDomain.apron.ml @@ -659,6 +659,7 @@ struct let empty_env = Environment.make [||] [||] + (* top and bottom over the empty environment are different, pending https://github.com/goblint/analyzer/issues/1380 *) let bot () = bot_env empty_env From b0465a2d97efbdaff7629c3d2245ee995221b2ba Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 3 Mar 2024 12:26:04 +0100 Subject: [PATCH 28/55] AffEq: Make `top` and `is_top` consistent --- src/cdomains/apron/affineEqualityDomain.apron.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index ed6f2c5936..944515f4ec 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -307,7 +307,7 @@ struct let top () = {d = Some (Matrix.empty ()); env = Environment.make [||] [||]} - let is_top _ = false + let is_top t = Environment.equal empty_env t.env && GobOption.exists Matrix.is_empty t.d let is_top_env t = (not @@ Environment.equal empty_env t.env) && GobOption.exists Matrix.is_empty t.d From 171443be205930cb470ca742605f4b007a732b08 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 3 Mar 2024 13:21:44 +0100 Subject: [PATCH 29/55] Minimize example --- .../regression/46-apron2/79-context-insens.c | 42 ++++++------------- 1 file changed, 12 insertions(+), 30 deletions(-) diff --git a/tests/regression/46-apron2/79-context-insens.c b/tests/regression/46-apron2/79-context-insens.c index 43b7c412cc..822caae414 100644 --- a/tests/regression/46-apron2/79-context-insens.c +++ b/tests/regression/46-apron2/79-context-insens.c @@ -1,46 +1,28 @@ -// PARAM: --set ana.activated "['base', 'threadid', 'threadflag', 'threadreturn','mallocWrapper','mutexEvents','mutex','access','race','escape','expRelation','assert','var_eq','symb_locks','apron','memLeak']" --enable ana.int.interval_set --set ana.ctx_insens "['base', 'threadid', 'threadflag', 'threadreturn','mallocWrapper','mutexEvents','mutex','access','race','escape','expRelation','assert','var_eq','symb_locks','apron','memLeak']" --enable ana.autotune.enabled --set ana.autotune.activated "['octagon']" --set ana.specification "CHECK( init(main()), LTL(G valid-memcleanup) )" --set ana.path_sens "['mutex', 'malloc_null', 'uninit','expsplit','activeSetjmp','memLeak', 'threadflag']" --set ana.malloc.unique_address_count 5 +// PARAM: --enable annotation.goblint_relation_track --set ana.activated[+] apron --set ana.activated[+] memLeak --set ana.ctx_insens "['base','mallocWrapper','mutexEvents','assert','apron','memLeak']" --set ana.malloc.unique_address_count 2 // Adapted from https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/list-properties/list_search-1.c -#include -#include #include -typedef struct list { +typedef struct thing { int key; - struct list *next; -} mlist; +} thing; -mlist *head; +thing *container; -mlist* search(mlist *l, int k){ - l = head; - while(l!=0 && l->key!=k) { // Used to detect dead code after loop head - l = l->next; - } - return l; -} - -int insert(mlist *l, int k){ - l = (mlist*)malloc(sizeof(mlist)); - l->key = k; - if (head==0) { - } else { - l->key = k; - l->next = head; - } - head = l; +int insert(int k __attribute__((__goblint_relation_track__))) { + container = (thing*) malloc(sizeof(thing)); + container->key = k; return 0; } int main(void){ - int i; - mlist *mylist, *temp; - insert(mylist,2); - insert(mylist,5); + insert(2); + insert(5); - temp = search(head,2); + if(container !=0) { // Used to detect dead code after loop head + + } __goblint_check(1); // Should be reachable return 0; } - From 6c4742cd00186c02f3d451eac2051fb60180f402 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Mon, 4 Mar 2024 13:55:08 +0100 Subject: [PATCH 30/55] make function argument explicit to fix gobview test --- src/cdomains/apron/apronDomain.apron.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index fbfddbe94d..158d3ca907 100644 --- a/src/cdomains/apron/apronDomain.apron.ml +++ b/src/cdomains/apron/apronDomain.apron.ml @@ -666,8 +666,8 @@ struct let top () = top_env empty_env - let is_bot = equal (bot ()) - let is_top = equal (top ()) + let is_bot x = equal (bot ()) x + let is_top x = equal (top ()) x let strengthening_enabled = GobConfig.get_bool "ana.apron.strengthening" From db019b50ac0a5dddb69d7ca5d82fe662accf0484 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 4 Mar 2024 17:39:21 +0200 Subject: [PATCH 31/55] Add RelationPriv TODO from PR #1354 --- src/analyses/apron/relationPriv.apron.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 206e6417df..2383cad5f9 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -489,7 +489,7 @@ struct in let get_mutex_inits = getg V.mutex_inits in let get_mutex_inits' = RD.keep_vars get_mutex_inits [g_var] in - if not (RD.mem_var get_mutex_inits' g_var) then + if not (RD.mem_var get_mutex_inits' g_var) then (* TODO: is this just a workaround for an escape bug? https://github.com/goblint/analyzer/pull/1354/files#r1498882657 *) (* This is an escaped variable whose value was never side-effected to get_mutex_inits' *) get_mutex_global_g else From cdca6b7c03a4fd5b50cb6d95019097273ff658ca Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 4 Mar 2024 17:39:35 +0200 Subject: [PATCH 32/55] Fix RelationPriv indentation (PR #1354) --- src/analyses/apron/relationPriv.apron.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 2383cad5f9..5e78a02153 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -638,10 +638,10 @@ struct let rel = st.rel in (* Replace with remove_filter once issues are fixed *) let g_vars = List.filter (fun var -> - match AV.find_metadata var with - | Some (Global _) -> true - | _ -> false - ) (RD.vars rel) + match AV.find_metadata var with + | Some (Global _) -> true + | _ -> false + ) (RD.vars rel) in let rel_side = RD.keep_vars rel g_vars in (* If no globals are contained here, none need to be published *) From 920b3fc591567d9561d5e85edfdfa95b70a336ba Mon Sep 17 00:00:00 2001 From: Felix Krayer Date: Sun, 10 Mar 2024 18:07:03 +0100 Subject: [PATCH 33/55] 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 34/55] 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 35/55] 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 36/55] 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 37/55] 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 From 7ffd335fd104e54dd2c79ecc36cb9c699ca6c9dd Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 12 Mar 2024 10:13:18 +0200 Subject: [PATCH 38/55] Add tests for __VERIFIER_assert --- .../29-svcomp/33-verifier-assert-undef.c | 9 ++++++++ .../29-svcomp/33-verifier-assert-undef.t | 15 +++++++++++++ .../29-svcomp/34-verifier-assert-def.c | 13 +++++++++++ .../29-svcomp/34-verifier-assert-def.t | 22 +++++++++++++++++++ 4 files changed, 59 insertions(+) create mode 100644 tests/regression/29-svcomp/33-verifier-assert-undef.c create mode 100644 tests/regression/29-svcomp/33-verifier-assert-undef.t create mode 100644 tests/regression/29-svcomp/34-verifier-assert-def.c create mode 100644 tests/regression/29-svcomp/34-verifier-assert-def.t diff --git a/tests/regression/29-svcomp/33-verifier-assert-undef.c b/tests/regression/29-svcomp/33-verifier-assert-undef.c new file mode 100644 index 0000000000..075eae9878 --- /dev/null +++ b/tests/regression/29-svcomp/33-verifier-assert-undef.c @@ -0,0 +1,9 @@ +// PARAM: --enable ana.sv-comp.functions + +int main() { + int r; // rand + __VERIFIER_assert(1); + __VERIFIER_assert(r); // UNKNOWN! + __VERIFIER_assert(0); // FAIL + return 0; +} diff --git a/tests/regression/29-svcomp/33-verifier-assert-undef.t b/tests/regression/29-svcomp/33-verifier-assert-undef.t new file mode 100644 index 0000000000..28be64329f --- /dev/null +++ b/tests/regression/29-svcomp/33-verifier-assert-undef.t @@ -0,0 +1,15 @@ + $ goblint --enable ana.sv-comp.functions 33-verifier-assert-undef.c + [Error][Imprecise][Unsound] Function definition missing for __VERIFIER_assert (33-verifier-assert-undef.c:5:3-5:23) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (33-verifier-assert-undef.c:5:3-5:23) + [Info][Imprecise] Invalidating expressions: 1 (33-verifier-assert-undef.c:5:3-5:23) + [Error][Imprecise][Unsound] Function definition missing for __VERIFIER_assert (33-verifier-assert-undef.c:6:3-6:23) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (33-verifier-assert-undef.c:6:3-6:23) + [Info][Imprecise] Invalidating expressions: r (33-verifier-assert-undef.c:6:3-6:23) + [Error][Imprecise][Unsound] Function definition missing for __VERIFIER_assert (33-verifier-assert-undef.c:7:3-7:23) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (33-verifier-assert-undef.c:7:3-7:23) + [Info][Imprecise] Invalidating expressions: 0 (33-verifier-assert-undef.c:7:3-7:23) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 5 + dead: 0 + total lines: 5 + [Error][Imprecise][Unsound] Function definition missing diff --git a/tests/regression/29-svcomp/34-verifier-assert-def.c b/tests/regression/29-svcomp/34-verifier-assert-def.c new file mode 100644 index 0000000000..c23c831a69 --- /dev/null +++ b/tests/regression/29-svcomp/34-verifier-assert-def.c @@ -0,0 +1,13 @@ +// PARAM: --enable ana.sv-comp.functions --enable ana.int.interval + +void __VERIFIER_assert(int cond) { + int x = 1 << 80; +} + +int main() { + int r; // rand + __VERIFIER_assert(1); // NOWARN + __VERIFIER_assert(r); // NOWARN + __VERIFIER_assert(0); // NOWARN + return 0; +} diff --git a/tests/regression/29-svcomp/34-verifier-assert-def.t b/tests/regression/29-svcomp/34-verifier-assert-def.t new file mode 100644 index 0000000000..8d15832540 --- /dev/null +++ b/tests/regression/29-svcomp/34-verifier-assert-def.t @@ -0,0 +1,22 @@ + $ goblint --enable ana.sv-comp.functions --enable ana.int.interval 34-verifier-assert-def.c + [Warning][Integer > Overflow][CWE-190] Signed integer overflow (34-verifier-assert-def.c:4:7-4:18) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 8 + dead: 0 + total lines: 8 + + $ goblint --enable ana.sv-comp.functions --set exp.extraspecials[+] __VERIFIER_assert 34-verifier-assert-def.c + [Info][Analyzer] Using special for defined function __VERIFIER_assert (34-verifier-assert-def.c:9:3-9:23) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (34-verifier-assert-def.c:9:3-9:23) + [Info][Imprecise] Invalidating expressions: 1 (34-verifier-assert-def.c:9:3-9:23) + [Info][Analyzer] Using special for defined function __VERIFIER_assert (34-verifier-assert-def.c:10:3-10:23) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (34-verifier-assert-def.c:10:3-10:23) + [Info][Imprecise] Invalidating expressions: r (34-verifier-assert-def.c:10:3-10:23) + [Info][Analyzer] Using special for defined function __VERIFIER_assert (34-verifier-assert-def.c:11:3-11:23) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (34-verifier-assert-def.c:11:3-11:23) + [Info][Imprecise] Invalidating expressions: 0 (34-verifier-assert-def.c:11:3-11:23) + [Warning][Deadcode] Function '__VERIFIER_assert' is uncalled: 2 LLoC (34-verifier-assert-def.c:3:1-5:1) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 5 + dead: 2 (2 in uncalled functions) + total lines: 7 From 98ef567d822a14edd9668c153a2678456aec0f4c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 12 Mar 2024 10:19:51 +0200 Subject: [PATCH 39/55] Add __VERIFIER_assert to library functions for evalAssert transformed output analysis --- src/util/library/libraryFunctions.ml | 1 + .../29-svcomp/33-verifier-assert-undef.t | 22 ++++++++----------- .../29-svcomp/34-verifier-assert-def.c | 2 +- .../29-svcomp/34-verifier-assert-def.t | 18 +++++++-------- 4 files changed, 20 insertions(+), 23 deletions(-) diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index 824c9dc4d9..53bf804b1d 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -1028,6 +1028,7 @@ let svcomp_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__VERIFIER_nondet_loff_t", unknown []); (* cannot give it in sv-comp.c without including stdlib or similar *) ("__VERIFIER_nondet_int", unknown []); (* declare invalidate actions to prevent invalidating globals when extern in regression tests *) ("__VERIFIER_nondet_size_t", unknown []); (* cannot give it in sv-comp.c without including stdlib or similar *) + ("__VERIFIER_assert", special [__ "exp" []] @@ fun exp -> Assert { exp; check = true; refine = get_bool "sem.assert.refine" }); (* only used if definition missing (e.g. in evalAssert transformed output) or extraspecial *) ] [@@coverage off] diff --git a/tests/regression/29-svcomp/33-verifier-assert-undef.t b/tests/regression/29-svcomp/33-verifier-assert-undef.t index 28be64329f..3acd4f7e25 100644 --- a/tests/regression/29-svcomp/33-verifier-assert-undef.t +++ b/tests/regression/29-svcomp/33-verifier-assert-undef.t @@ -1,15 +1,11 @@ $ goblint --enable ana.sv-comp.functions 33-verifier-assert-undef.c - [Error][Imprecise][Unsound] Function definition missing for __VERIFIER_assert (33-verifier-assert-undef.c:5:3-5:23) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (33-verifier-assert-undef.c:5:3-5:23) - [Info][Imprecise] Invalidating expressions: 1 (33-verifier-assert-undef.c:5:3-5:23) - [Error][Imprecise][Unsound] Function definition missing for __VERIFIER_assert (33-verifier-assert-undef.c:6:3-6:23) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (33-verifier-assert-undef.c:6:3-6:23) - [Info][Imprecise] Invalidating expressions: r (33-verifier-assert-undef.c:6:3-6:23) - [Error][Imprecise][Unsound] Function definition missing for __VERIFIER_assert (33-verifier-assert-undef.c:7:3-7:23) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (33-verifier-assert-undef.c:7:3-7:23) - [Info][Imprecise] Invalidating expressions: 0 (33-verifier-assert-undef.c:7:3-7:23) - [Info][Deadcode] Logical lines of code (LLoC) summary: - live: 5 - dead: 0 + [Success][Assert] Assertion "1" will succeed (33-verifier-assert-undef.c:5:3-5:23) + [Warning][Assert] Assertion "r" is unknown. (33-verifier-assert-undef.c:6:3-6:23) + [Error][Assert] Assertion "0" will fail. (33-verifier-assert-undef.c:7:3-7:23) + [Warning][Deadcode] Function 'main' does not return + [Warning][Deadcode] Function 'main' has dead code: + on line 8 (33-verifier-assert-undef.c:8-8) + [Warning][Deadcode] Logical lines of code (LLoC) summary: + live: 4 + dead: 1 total lines: 5 - [Error][Imprecise][Unsound] Function definition missing diff --git a/tests/regression/29-svcomp/34-verifier-assert-def.c b/tests/regression/29-svcomp/34-verifier-assert-def.c index c23c831a69..fcc389cc04 100644 --- a/tests/regression/29-svcomp/34-verifier-assert-def.c +++ b/tests/regression/29-svcomp/34-verifier-assert-def.c @@ -1,6 +1,6 @@ // PARAM: --enable ana.sv-comp.functions --enable ana.int.interval -void __VERIFIER_assert(int cond) { +void __VERIFIER_assert(int cond) { // NOWARN (update_suite assert detection spurious) int x = 1 << 80; } diff --git a/tests/regression/29-svcomp/34-verifier-assert-def.t b/tests/regression/29-svcomp/34-verifier-assert-def.t index 8d15832540..c581893e36 100644 --- a/tests/regression/29-svcomp/34-verifier-assert-def.t +++ b/tests/regression/29-svcomp/34-verifier-assert-def.t @@ -7,16 +7,16 @@ $ goblint --enable ana.sv-comp.functions --set exp.extraspecials[+] __VERIFIER_assert 34-verifier-assert-def.c [Info][Analyzer] Using special for defined function __VERIFIER_assert (34-verifier-assert-def.c:9:3-9:23) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (34-verifier-assert-def.c:9:3-9:23) - [Info][Imprecise] Invalidating expressions: 1 (34-verifier-assert-def.c:9:3-9:23) + [Success][Assert] Assertion "1" will succeed (34-verifier-assert-def.c:9:3-9:23) [Info][Analyzer] Using special for defined function __VERIFIER_assert (34-verifier-assert-def.c:10:3-10:23) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (34-verifier-assert-def.c:10:3-10:23) - [Info][Imprecise] Invalidating expressions: r (34-verifier-assert-def.c:10:3-10:23) + [Warning][Assert] Assertion "r" is unknown. (34-verifier-assert-def.c:10:3-10:23) [Info][Analyzer] Using special for defined function __VERIFIER_assert (34-verifier-assert-def.c:11:3-11:23) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (34-verifier-assert-def.c:11:3-11:23) - [Info][Imprecise] Invalidating expressions: 0 (34-verifier-assert-def.c:11:3-11:23) + [Error][Assert] Assertion "0" will fail. (34-verifier-assert-def.c:11:3-11:23) [Warning][Deadcode] Function '__VERIFIER_assert' is uncalled: 2 LLoC (34-verifier-assert-def.c:3:1-5:1) - [Info][Deadcode] Logical lines of code (LLoC) summary: - live: 5 - dead: 2 (2 in uncalled functions) + [Warning][Deadcode] Function 'main' does not return + [Warning][Deadcode] Function 'main' has dead code: + on line 12 (34-verifier-assert-def.c:12-12) + [Warning][Deadcode] Logical lines of code (LLoC) summary: + live: 4 + dead: 3 (2 in uncalled functions) total lines: 7 From 83c7cf1f7d288c20ee3f3e88107a24ab0320be32 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 12 Mar 2024 11:15:16 +0200 Subject: [PATCH 40/55] Add test from issue #1388 Co-authored-by: Michael Schwarz --- tests/regression/11-heap/16-issue-1388.c | 27 ++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 tests/regression/11-heap/16-issue-1388.c diff --git a/tests/regression/11-heap/16-issue-1388.c b/tests/regression/11-heap/16-issue-1388.c new file mode 100644 index 0000000000..ce212b3265 --- /dev/null +++ b/tests/regression/11-heap/16-issue-1388.c @@ -0,0 +1,27 @@ +// PARAM: --set ana.malloc.unique_address_count 2 --set ana.activated[-] threadid + +typedef struct list { + struct list *next; +} mlist; + +mlist *head; + +int insert_list(mlist *l){ + l = (mlist*)malloc(sizeof(mlist)); + l->next = head; + + head = l; + return 0; +} + +int main(void){ + mlist *mylist; + insert_list(mylist); + insert_list(mylist); + + while(head!=((void *)0)) { + head = head->next; + } + + __goblint_check(1); +} From 79b8d76764ddfdea86fa34e4c25687ef16a62a71 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 12 Mar 2024 11:16:33 +0200 Subject: [PATCH 41/55] Fix alloc varinfo name with no thread ID but with counter (closes #1388) --- src/analyses/wrapperFunctionAnalysis.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/wrapperFunctionAnalysis.ml b/src/analyses/wrapperFunctionAnalysis.ml index 827213d15e..9510304e56 100644 --- a/src/analyses/wrapperFunctionAnalysis.ml +++ b/src/analyses/wrapperFunctionAnalysis.ml @@ -141,9 +141,9 @@ module MallocWrapper : MCPSpec = struct if not (GobConfig.get_bool "dbg.full-output") && ThreadLifted.is_top t then Format.dprintf "" else - Format.dprintf "@tid:%s%t" (ThreadLifted.show t) uniq_count + Format.dprintf "@tid:%s" (ThreadLifted.show t) in - Format.asprintf "(alloc@sid:%s%t)" (Node.show_id node) tid + Format.asprintf "(alloc@sid:%s%t%t)" (Node.show_id node) tid uniq_count end module NodeVarinfoMap = RichVarinfo.BiVarinfoMap.Make(ThreadNode) From 11a7f31f83b7fc413fd482865cd7583c70dff95c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 12 Mar 2024 14:49:20 +0200 Subject: [PATCH 42/55] Add SKIP to apron test (PR #1354) --- tests/regression/46-apron2/79-context-insens.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/regression/46-apron2/79-context-insens.c b/tests/regression/46-apron2/79-context-insens.c index 822caae414..9f949a313a 100644 --- a/tests/regression/46-apron2/79-context-insens.c +++ b/tests/regression/46-apron2/79-context-insens.c @@ -1,4 +1,4 @@ -// PARAM: --enable annotation.goblint_relation_track --set ana.activated[+] apron --set ana.activated[+] memLeak --set ana.ctx_insens "['base','mallocWrapper','mutexEvents','assert','apron','memLeak']" --set ana.malloc.unique_address_count 2 +// SKIP PARAM: --enable annotation.goblint_relation_track --set ana.activated[+] apron --set ana.activated[+] memLeak --set ana.ctx_insens "['base','mallocWrapper','mutexEvents','assert','apron','memLeak']" --set ana.malloc.unique_address_count 2 // Adapted from https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/list-properties/list_search-1.c #include From 93b88217d5d0e7aeaa881d66ba9969ba4d0db096 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 12 Mar 2024 17:12:59 +0200 Subject: [PATCH 43/55] Fix --version always printing library versions --- src/maingoblint.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 7fdb7a4a13..a5e99b62ba 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -9,6 +9,7 @@ let writeconffile = ref None (** Print version and bail. *) let print_version ch = + Logs.Level.current := Logs.Level.of_string (get_string "dbg.level"); (* duplicated from handle_options to be affected by -v *) Logs.result "Goblint version: %s" Goblint_build_info.version; Logs.result "Cil version: %s" Cil.cilVersion; Logs.result "Dune profile: %s" Goblint_build_info.dune_profile; From 50487af47d25d557ea7c2bc13316a69f2b5a7a7c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 12 Mar 2024 17:26:30 +0200 Subject: [PATCH 44/55] Add build time to --version --- src/build-info/dune | 6 ++++++ src/build-info/goblint_build_info.ml | 3 +++ src/maingoblint.ml | 1 + 3 files changed, 10 insertions(+) diff --git a/src/build-info/dune b/src/build-info/dune index ff8d68671b..5a64b399a4 100644 --- a/src/build-info/dune +++ b/src/build-info/dune @@ -27,6 +27,12 @@ (mode (promote (until-clean) (only configOcaml.ml))) ; replace existing file in source tree, even if releasing (only overrides) (action (write-file %{target} "(* Automatically regenerated, changes do not persist! *)\nlet flambda = \"%{ocaml-config:flambda}\""))) +(rule + (target configDatetime.ml) + (mode (promote (until-clean) (only configDatetime.ml))) ; replace existing file in source tree, even if releasing (only overrides) + (deps (universe)) ; do not cache, always regenerate + (action (pipe-stdout (bash "date +\"%Y-%m-%dT%H:%M:%S\" || echo \"n/a\"") (with-stdout-to %{target} (bash "xargs printf '(* Automatically regenerated, changes do not persist! *)\nlet datetime = \"%s\"'"))))) + (env (_ (flags (:standard -w -no-cmx-file)))) ; suppress warning from flambda compiler bug: https://github.com/ocaml/dune/issues/3277 diff --git a/src/build-info/goblint_build_info.ml b/src/build-info/goblint_build_info.ml index cf5165d51c..14e30a1b36 100644 --- a/src/build-info/goblint_build_info.ml +++ b/src/build-info/goblint_build_info.ml @@ -32,3 +32,6 @@ let version = (** Statically linked libraries with versions. *) let statically_linked_libraries = Dune_build_info.statically_linked_libraries + +(** Build date and time. *) +let datetime = ConfigDatetime.datetime diff --git a/src/maingoblint.ml b/src/maingoblint.ml index a5e99b62ba..4b67804bb8 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -22,6 +22,7 @@ let print_version ch = Logs.result " %s: %s" name version ) Goblint_build_info.statically_linked_libraries ); + Logs.result "Build time: %s" Goblint_build_info.datetime; exit 0 (** Print helpful messages. *) From 1c04f03513491d898cd197141aed8456867eac6c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 12 Mar 2024 17:40:19 +0200 Subject: [PATCH 45/55] Use match in SvcompSpec --- src/witness/svcompSpec.ml | 44 +++++++++++++++++---------------------- 1 file changed, 19 insertions(+), 25 deletions(-) diff --git a/src/witness/svcompSpec.ml b/src/witness/svcompSpec.ml index c7601ef637..3a41cb250d 100644 --- a/src/witness/svcompSpec.ml +++ b/src/witness/svcompSpec.ml @@ -19,37 +19,31 @@ let of_string s = let regexp_single = Str.regexp "CHECK( init(main()), LTL(G \\(.*\\)) )" in let regexp_negated = Str.regexp "CHECK( init(main()), LTL(G ! \\(.*\\)) )" in let regexp_finally = Str.regexp "CHECK( init(main()), LTL(F \\(.*\\)) )" in - if Str.string_match regexp_negated s 0 then - let global_not = Str.matched_group 1 s in - if global_not = "data-race" then - NoDataRace - else if global_not = "overflow" then - NoOverflow - else + if Str.string_match regexp_negated s 0 then ( + match Str.matched_group 1 s with + | "data-race" -> NoDataRace + | "overflow" -> NoOverflow + | global_not -> let call_regex = Str.regexp "call(\\(.*\\)())" in if Str.string_match call_regex global_not 0 then let f = Str.matched_group 1 global_not in UnreachCall f else failwith "Svcomp.Specification.of_string: unknown global not expression" - else if Str.string_match regexp_single s 0 then - let global = Str.matched_group 1 s in - if global = "valid-free" then - ValidFree - else if global = "valid-deref" then - ValidDeref - else if global = "valid-memtrack" then - ValidMemtrack - else if global = "valid-memcleanup" then - ValidMemcleanup - else - failwith "Svcomp.Specification.of_string: unknown global expression" - else if Str.string_match regexp_finally s 0 then - let finally = Str.matched_group 1 s in - if finally = "end" then - Termination - else - failwith "Svcomp.Specification.of_string: unknown finally expression" + ) + else if Str.string_match regexp_single s 0 then ( + match Str.matched_group 1 s with + | "valid-free" -> ValidFree + | "valid-deref" -> ValidDeref + | "valid-memtrack" -> ValidMemtrack + | "valid-memcleanup" -> ValidMemcleanup + | _ -> failwith "Svcomp.Specification.of_string: unknown global expression" + ) + else if Str.string_match regexp_finally s 0 then ( + match Str.matched_group 1 s with + | "end" -> Termination + | _ -> failwith "Svcomp.Specification.of_string: unknown finally expression" + ) else failwith "Svcomp.Specification.of_string: unknown expression" From ba60e5835fd7fe075f7ffeb7ca05a12a56043218 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 13 Mar 2024 10:30:17 +0200 Subject: [PATCH 46/55] Refine goblint-cil dependencies on goblint.lib --- src/dune | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/dune b/src/dune index c8ed2f311a..e7226466ad 100644 --- a/src/dune +++ b/src/dune @@ -7,7 +7,7 @@ (name goblint_lib) (public_name goblint.lib) (modules :standard \ goblint privPrecCompare apronPrecCompare messagesCompare) - (libraries goblint.sites goblint.build-info goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common goblint_domain goblint_constraint goblint_solver goblint_library goblint_cdomain_value goblint_incremental goblint_tracing goblint_logs + (libraries goblint.sites goblint.build-info goblint-cil goblint-cil.pta goblint-cil.syntacticsearch batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common goblint_domain goblint_constraint goblint_solver goblint_library goblint_cdomain_value goblint_incremental goblint_tracing goblint_logs ; Conditionally compile based on whether apron optional dependency is installed or not. ; Alternative dependencies seem like the only way to optionally depend on optional dependencies. ; See: https://dune.readthedocs.io/en/stable/concepts.html#alternative-dependencies. From 3e2f370150a9fd8273f434088c29463b2a350a47 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 30 Nov 2023 15:01:12 +0200 Subject: [PATCH 47/55] Add lock-digest example from more-traces --- tests/regression/46-apron2/80-lock-digest.c | 36 +++++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 tests/regression/46-apron2/80-lock-digest.c diff --git a/tests/regression/46-apron2/80-lock-digest.c b/tests/regression/46-apron2/80-lock-digest.c new file mode 100644 index 0000000000..1a44d8c420 --- /dev/null +++ b/tests/regression/46-apron2/80-lock-digest.c @@ -0,0 +1,36 @@ +// SKIP PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet +// TODO: why does this work? even with earlyglobs +#include +#include + +int g, h; +pthread_mutex_t a = PTHREAD_MUTEX_INITIALIZER; + +void *t2(void *arg) { + pthread_mutex_lock(&a); + __goblint_check(h <= g); // TODO: should be h < g? + pthread_mutex_unlock(&a); + return NULL; +} + +void *t1(void *arg) { + pthread_t x; + pthread_create(&x, NULL, t2, NULL); + + pthread_mutex_lock(&a); + h = 11; g = 12; + pthread_mutex_unlock(&a); + + return NULL; +} + +int main() { + pthread_mutex_lock(&a); + h = 9; + g = 10; + pthread_mutex_unlock(&a); + + pthread_t x; + pthread_create(&x, NULL, t1, NULL); + return 0; +} From ff7262cb87987b150e8ae07be3d8d9babd92bf59 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 30 Nov 2023 15:04:11 +0200 Subject: [PATCH 48/55] Add going multithreaded to lock-digest test --- tests/regression/46-apron2/80-lock-digest.c | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/tests/regression/46-apron2/80-lock-digest.c b/tests/regression/46-apron2/80-lock-digest.c index 1a44d8c420..20e139e61c 100644 --- a/tests/regression/46-apron2/80-lock-digest.c +++ b/tests/regression/46-apron2/80-lock-digest.c @@ -20,11 +20,17 @@ void *t1(void *arg) { pthread_mutex_lock(&a); h = 11; g = 12; pthread_mutex_unlock(&a); + return NULL; +} +void *t0(void *arg) { return NULL; } int main() { + pthread_t x; + pthread_create(&x, NULL, t0, NULL); // go multithreaded + pthread_mutex_lock(&a); h = 9; g = 10; From 8f0c28441e77046808ef01edc64f036e7d98b0b4 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 30 Nov 2023 15:06:03 +0200 Subject: [PATCH 49/55] Fix lock-digest test --- tests/regression/46-apron2/80-lock-digest.c | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/tests/regression/46-apron2/80-lock-digest.c b/tests/regression/46-apron2/80-lock-digest.c index 20e139e61c..826d4f3b41 100644 --- a/tests/regression/46-apron2/80-lock-digest.c +++ b/tests/regression/46-apron2/80-lock-digest.c @@ -1,5 +1,4 @@ // SKIP PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet -// TODO: why does this work? even with earlyglobs #include #include @@ -8,7 +7,8 @@ pthread_mutex_t a = PTHREAD_MUTEX_INITIALIZER; void *t2(void *arg) { pthread_mutex_lock(&a); - __goblint_check(h <= g); // TODO: should be h < g? + // wrong in more-traces! + __goblint_check(h < g); // TODO pthread_mutex_unlock(&a); return NULL; } @@ -36,7 +36,6 @@ int main() { g = 10; pthread_mutex_unlock(&a); - pthread_t x; pthread_create(&x, NULL, t1, NULL); return 0; } From 29df7ecaa3d34a8e21f66a9b77a56d9db74a03f4 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 13 Mar 2024 10:41:33 +0200 Subject: [PATCH 50/55] Make 46-apron2/80-lock-digest pass with mutex-meet-tid --- tests/regression/46-apron2/80-lock-digest.c | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/tests/regression/46-apron2/80-lock-digest.c b/tests/regression/46-apron2/80-lock-digest.c index 826d4f3b41..02adf8116d 100644 --- a/tests/regression/46-apron2/80-lock-digest.c +++ b/tests/regression/46-apron2/80-lock-digest.c @@ -1,4 +1,5 @@ -// SKIP PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet +// SKIP PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid --set ana.path_sens[+] threadflag +// cherry-picked from https://github.com/goblint/analyzer/pull/1286: works with mutex-meet-tid, without lock digests #include #include @@ -8,7 +9,7 @@ pthread_mutex_t a = PTHREAD_MUTEX_INITIALIZER; void *t2(void *arg) { pthread_mutex_lock(&a); // wrong in more-traces! - __goblint_check(h < g); // TODO + __goblint_check(h < g); pthread_mutex_unlock(&a); return NULL; } From a7e284f3339a81ab0453606abe52883e193df154 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 15 Mar 2024 11:38:26 +0200 Subject: [PATCH 51/55] Port witness metadata fixes from goblint/bench for unassume examples --- tests/regression/56-witness/26-mine-tutorial-ex4.6.yml | 6 ++---- tests/regression/56-witness/27-mine-tutorial-ex4.7.yml | 8 ++------ tests/regression/56-witness/28-mine-tutorial-ex4.8.yml | 8 ++------ tests/regression/56-witness/29-mine-tutorial-ex4.10.yml | 9 ++------- tests/regression/56-witness/35-hh-ex1b.yml | 8 ++------ tests/regression/56-witness/36-hh-ex2b.yml | 8 ++------ tests/regression/56-witness/37-hh-ex3.yml | 8 ++------ tests/regression/56-witness/38-bh-ex3.yml | 8 ++------ tests/regression/56-witness/39-bh-ex-add.yml | 8 ++------ tests/regression/56-witness/40-bh-ex1-poly.yml | 8 ++------ tests/regression/56-witness/41-as-hybrid.yml | 8 ++------ 11 files changed, 22 insertions(+), 65 deletions(-) diff --git a/tests/regression/56-witness/26-mine-tutorial-ex4.6.yml b/tests/regression/56-witness/26-mine-tutorial-ex4.6.yml index 2e3c6758fc..1dc21aeacc 100644 --- a/tests/regression/56-witness/26-mine-tutorial-ex4.6.yml +++ b/tests/regression/56-witness/26-mine-tutorial-ex4.6.yml @@ -4,10 +4,8 @@ uuid: 0e84a9de-b9f6-44dd-ab8d-ebdeca941482 creation_time: 2022-10-07T09:14:31Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-g1e981de3d-dirty - command_line: '''../../../goblint'' ''--enable'' ''ana.int.interval'' ''26-mine-tutorial-ex4.6.c'' - ''--html'' ''--set'' ''exp.g2html_path'' ''../../..'' ''--enable'' ''witness.yaml.enabled''' + name: Simmo Saan + version: n/a task: input_files: - 26-mine-tutorial-ex4.6.c diff --git a/tests/regression/56-witness/27-mine-tutorial-ex4.7.yml b/tests/regression/56-witness/27-mine-tutorial-ex4.7.yml index ad4c287227..c0473adecb 100644 --- a/tests/regression/56-witness/27-mine-tutorial-ex4.7.yml +++ b/tests/regression/56-witness/27-mine-tutorial-ex4.7.yml @@ -4,12 +4,8 @@ uuid: e17f9860-95af-4213-a767-ab4876ead27e creation_time: 2022-10-07T10:33:01Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-g9426848d9-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''27-mine-tutorial-ex4.7.c'' - ''--enable'' ''ana.int.interval'' ''--enable'' ''ana.sv-comp.functions'' ''--enable'' - ''witness.yaml.enabled'' ''--set'' ''dbg.debug'' ''true'' ''--enable'' ''dbg.timing.enabled'' - ''--set'' ''goblint-dir'' ''.goblint-56-27''' + name: Simmo Saan + version: n/a task: input_files: - 27-mine-tutorial-ex4.7.c diff --git a/tests/regression/56-witness/28-mine-tutorial-ex4.8.yml b/tests/regression/56-witness/28-mine-tutorial-ex4.8.yml index 69479e6df0..2ccf85fdd2 100644 --- a/tests/regression/56-witness/28-mine-tutorial-ex4.8.yml +++ b/tests/regression/56-witness/28-mine-tutorial-ex4.8.yml @@ -4,12 +4,8 @@ uuid: 299c2080-fb13-4879-be2b-5d2758465577 creation_time: 2022-10-07T10:36:41Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-g9426848d9-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''28-mine-tutorial-ex4.8.c'' - ''--enable'' ''ana.int.interval'' ''--enable'' ''ana.sv-comp.functions'' ''--enable'' - ''witness.yaml.enabled'' ''--set'' ''dbg.debug'' ''true'' ''--enable'' ''dbg.timing.enabled'' - ''--set'' ''goblint-dir'' ''.goblint-56-28''' + name: Simmo Saan + version: n/a task: input_files: - 28-mine-tutorial-ex4.8.c diff --git a/tests/regression/56-witness/29-mine-tutorial-ex4.10.yml b/tests/regression/56-witness/29-mine-tutorial-ex4.10.yml index 0f9b362290..f82c321f73 100644 --- a/tests/regression/56-witness/29-mine-tutorial-ex4.10.yml +++ b/tests/regression/56-witness/29-mine-tutorial-ex4.10.yml @@ -4,13 +4,8 @@ uuid: f04fe372-3d6e-4a80-9567-80c64bd7fd03 creation_time: 2022-10-07T10:47:08Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-g9426848d9-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''29-mine-tutorial-ex4.10.c'' - ''--set'' ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra'' - ''--enable'' ''witness.yaml.enabled'' ''--enable'' ''witness.yaml.enabled'' - ''--set'' ''dbg.debug'' ''true'' ''--enable'' ''dbg.timing.enabled'' ''--set'' - ''goblint-dir'' ''.goblint-56-29''' + name: Simmo Saan + version: n/a task: input_files: - 29-mine-tutorial-ex4.10.c diff --git a/tests/regression/56-witness/35-hh-ex1b.yml b/tests/regression/56-witness/35-hh-ex1b.yml index 9763960fd7..530ae08906 100644 --- a/tests/regression/56-witness/35-hh-ex1b.yml +++ b/tests/regression/56-witness/35-hh-ex1b.yml @@ -4,12 +4,8 @@ uuid: 1a354f1e-76e8-40e9-808a-8d5efbe35496 creation_time: 2022-10-12T10:45:49Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-g8b307fe1f-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''35-hh-ex1b.c'' - ''--enable'' ''ana.int.interval'' ''--disable'' ''solvers.td3.remove-wpoint'' - ''--enable'' ''witness.yaml.enabled'' ''--set'' ''dbg.debug'' ''true'' ''--enable'' - ''dbg.timing.enabled'' ''--set'' ''goblint-dir'' ''.goblint-56-35''' + name: Simmo Saan + version: n/a task: input_files: - 35-hh-ex1b.c diff --git a/tests/regression/56-witness/36-hh-ex2b.yml b/tests/regression/56-witness/36-hh-ex2b.yml index 69e0a88841..9ec4a7845a 100644 --- a/tests/regression/56-witness/36-hh-ex2b.yml +++ b/tests/regression/56-witness/36-hh-ex2b.yml @@ -4,12 +4,8 @@ uuid: 9589b9d4-edce-4043-8413-279703946762 creation_time: 2022-10-12T10:38:16Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-g8b307fe1f - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''36-hh-ex2b.c'' - ''--enable'' ''ana.int.interval'' ''--enable'' ''ana.sv-comp.functions'' ''--enable'' - ''witness.yaml.enabled'' ''--set'' ''dbg.debug'' ''true'' ''--enable'' ''dbg.timing.enabled'' - ''--set'' ''goblint-dir'' ''.goblint-56-36''' + name: Simmo Saan + version: n/a task: input_files: - 36-hh-ex2b.c diff --git a/tests/regression/56-witness/37-hh-ex3.yml b/tests/regression/56-witness/37-hh-ex3.yml index d6cd5150a4..5d18ef644f 100644 --- a/tests/regression/56-witness/37-hh-ex3.yml +++ b/tests/regression/56-witness/37-hh-ex3.yml @@ -4,12 +4,8 @@ uuid: d834761a-d0d7-4fea-bf42-2ff2b9a19143 creation_time: 2022-10-12T10:59:25Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-g8b307fe1f-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''37-hh-ex3.c'' - ''--set'' ''ana.activated[+]'' ''apron'' ''--disable'' ''solvers.td3.remove-wpoint'' - ''--enable'' ''witness.yaml.enabled'' ''--set'' ''dbg.debug'' ''true'' ''--enable'' - ''dbg.timing.enabled'' ''--set'' ''goblint-dir'' ''.goblint-56-37''' + name: Simmo Saan + version: n/a task: input_files: - 37-hh-ex3.c diff --git a/tests/regression/56-witness/38-bh-ex3.yml b/tests/regression/56-witness/38-bh-ex3.yml index d1f6677fbb..8a55e96e3a 100644 --- a/tests/regression/56-witness/38-bh-ex3.yml +++ b/tests/regression/56-witness/38-bh-ex3.yml @@ -4,12 +4,8 @@ uuid: bd436e09-244f-45db-a5f4-9337ca997424 creation_time: 2022-10-12T11:13:15Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-g8b307fe1f-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''38-bh-ex3.c'' - ''--enable'' ''ana.int.interval'' ''--enable'' ''ana.sv-comp.functions'' ''--enable'' - ''witness.yaml.enabled'' ''--set'' ''dbg.debug'' ''true'' ''--enable'' ''dbg.timing.enabled'' - ''--set'' ''goblint-dir'' ''.goblint-56-38''' + name: Simmo Saan + version: n/a task: input_files: - 38-bh-ex3.c diff --git a/tests/regression/56-witness/39-bh-ex-add.yml b/tests/regression/56-witness/39-bh-ex-add.yml index 84aa374c1e..c20801d044 100644 --- a/tests/regression/56-witness/39-bh-ex-add.yml +++ b/tests/regression/56-witness/39-bh-ex-add.yml @@ -4,12 +4,8 @@ uuid: bd436e09-244f-45db-a5f4-9337ca997424 creation_time: 2022-10-12T11:13:15Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-g8b307fe1f-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''39-bh-ex-add.c'' - ''--enable'' ''ana.int.interval'' ''--enable'' ''ana.sv-comp.functions'' ''--enable'' - ''witness.yaml.enabled'' ''--set'' ''dbg.debug'' ''true'' ''--enable'' ''dbg.timing.enabled'' - ''--set'' ''goblint-dir'' ''.goblint-56-38''' + name: Simmo Saan + version: n/a task: input_files: - 39-bh-ex-add.c diff --git a/tests/regression/56-witness/40-bh-ex1-poly.yml b/tests/regression/56-witness/40-bh-ex1-poly.yml index cdbd8d666b..7ddf289d14 100644 --- a/tests/regression/56-witness/40-bh-ex1-poly.yml +++ b/tests/regression/56-witness/40-bh-ex1-poly.yml @@ -4,12 +4,8 @@ uuid: 6ee08942-60e6-4291-a9fc-ff6f2744ef4b creation_time: 2022-10-12T11:19:46Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-g8b307fe1f-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''40-bh-ex1-poly.c'' - ''--set'' ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra'' - ''--enable'' ''witness.yaml.enabled'' ''--set'' ''dbg.debug'' ''true'' ''--enable'' - ''dbg.timing.enabled'' ''--set'' ''goblint-dir'' ''.goblint-56-40''' + name: Simmo Saan + version: n/a task: input_files: - 40-bh-ex1-poly.c diff --git a/tests/regression/56-witness/41-as-hybrid.yml b/tests/regression/56-witness/41-as-hybrid.yml index 0e810b6aca..336657e52d 100644 --- a/tests/regression/56-witness/41-as-hybrid.yml +++ b/tests/regression/56-witness/41-as-hybrid.yml @@ -4,12 +4,8 @@ uuid: 71b761c6-4f85-405e-8ee6-9a3a8f743513 creation_time: 2022-10-12T11:50:43Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-g811f2aff3 - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''41-as-hybrid.c'' - ''--enable'' ''ana.int.interval'' ''--enable'' ''witness.yaml.enabled'' ''--set'' - ''dbg.debug'' ''true'' ''--enable'' ''dbg.timing.enabled'' ''--set'' ''goblint-dir'' - ''.goblint-56-41''' + name: Simmo Saan + version: n/a task: input_files: - 41-as-hybrid.c From cde3bacc3d49494bda089f5157352cc7c29b0914 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 15 Mar 2024 11:57:44 +0200 Subject: [PATCH 52/55] Fix witness metadata for many tests --- .../56-witness/03-int-log-short.yml | 16 ++++--------- .../56-witness/04-base-priv-sync-prune.yml | 9 ++----- .../56-witness/07-base-lor-interval.yml | 18 ++++---------- .../56-witness/15-base-unassume-query.yml | 10 ++++---- .../56-witness/16-base-unassume-dependent.yml | 21 +++++----------- .../56-witness/17-base-unassume-tauto.yml | 7 ++---- .../56-witness/18-base-unassume-contra.yml | 7 ++---- .../56-witness/19-base-unassume-mem.yml | 12 ++++------ .../56-witness/21-apron-unassume-priv.yml | 8 ++----- .../56-witness/22-base-unassume-priv.yml | 8 ++----- .../56-witness/23-base-unassume-priv2.yml | 8 ++----- .../56-witness/24-apron-unassume-priv2.yml | 8 ++----- .../25-apron-unassume-strengthening.yml | 8 ++----- .../56-witness/30-base-unassume-inc-dec.yml | 16 ++++--------- .../56-witness/31-base-unassume-mem-ex.yml | 24 +++++-------------- .../56-witness/32-base-unassume-lor-addr.yml | 7 ++---- .../56-witness/33-base-unassume-lor-enums.yml | 8 ++----- .../34-base-unassume-inc-dec-traces.yml | 16 ++++--------- .../56-witness/42-base-unassume-precheck.yml | 7 ++---- .../56-witness/43-apron-unassume-precheck.yml | 14 ++++------- 20 files changed, 62 insertions(+), 170 deletions(-) diff --git a/tests/regression/56-witness/03-int-log-short.yml b/tests/regression/56-witness/03-int-log-short.yml index dfcde23f59..ab6928c71c 100644 --- a/tests/regression/56-witness/03-int-log-short.yml +++ b/tests/regression/56-witness/03-int-log-short.yml @@ -4,12 +4,8 @@ uuid: 872fc896-7029-4d06-b733-6ecc2d3f8074 creation_time: 2022-06-29T09:18:35Z producer: - name: Goblint - version: heads/int-log-0-g5f8473450-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''03-int-log-short.c'' - ''--enable'' ''witness.yaml.enabled'' ''--set'' ''dbg.debug'' ''true'' ''--set'' - ''printstats'' ''true'' ''--set'' ''goblint-dir'' - ''.goblint-56-03''' + name: Simmo Saan + version: n/a task: input_files: - 03-int-log-short.c @@ -33,12 +29,8 @@ uuid: f42797cf-479e-469f-b378-3bf9ab3f79a9 creation_time: 2022-06-29T09:18:35Z producer: - name: Goblint - version: heads/int-log-0-g5f8473450-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''03-int-log-short.c'' - ''--enable'' ''witness.yaml.enabled'' ''--set'' ''dbg.debug'' ''true'' ''--set'' - ''printstats'' ''true'' ''--set'' ''goblint-dir'' - ''.goblint-56-03''' + name: Simmo Saan + version: n/a task: input_files: - 03-int-log-short.c diff --git a/tests/regression/56-witness/04-base-priv-sync-prune.yml b/tests/regression/56-witness/04-base-priv-sync-prune.yml index d85f152415..b71970d411 100644 --- a/tests/regression/56-witness/04-base-priv-sync-prune.yml +++ b/tests/regression/56-witness/04-base-priv-sync-prune.yml @@ -4,13 +4,8 @@ uuid: 640889a9-5b82-4fc0-9365-7d4a21f11a45 creation_time: 2022-07-01T11:30:04Z producer: - name: Goblint - version: heads/apron-ikind-11-gb9a9ada69-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''04-base-priv-sync-prune.c'' - ''--enable'' ''ana.int.interval'' ''--enable'' ''witness.yaml.enabled'' ''--set'' - ''witness.yaml.path'' ''04-base-priv-sync-prune.yml'' ''--set'' ''dbg.debug'' - ''true'' ''--set'' ''printstats'' ''true'' - ''--set'' ''goblint-dir'' ''.goblint-56-03''' + name: Simmo Saan + version: n/a task: input_files: - 04-base-priv-sync-prune.c diff --git a/tests/regression/56-witness/07-base-lor-interval.yml b/tests/regression/56-witness/07-base-lor-interval.yml index 07b1eef0fb..6f1deb1431 100644 --- a/tests/regression/56-witness/07-base-lor-interval.yml +++ b/tests/regression/56-witness/07-base-lor-interval.yml @@ -4,13 +4,8 @@ uuid: b000a41c-b7eb-4187-92ea-40530a44479c creation_time: 2023-01-24T09:33:20Z producer: - name: Goblint - version: heads/yaml-witness-unassume-bench-0-g22403e387-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''07-base-lor-interval.c'' - ''--enable'' ''ana.int.interval'' ''--enable'' ''witness.yaml.enabled'' ''--enable'' - ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed'' ''--set'' - ''dbg.debug'' ''true'' ''--enable'' ''dbg.timing.enabled'' ''--set'' ''goblint-dir'' - ''.goblint-56-07''' + name: Simmo Saan + version: n/a task: input_files: - 07-base-lor-interval.c @@ -34,13 +29,8 @@ uuid: b000a41c-b7eb-4187-92ea-40530a44479c creation_time: 2023-01-24T09:33:20Z producer: - name: Goblint - version: heads/yaml-witness-unassume-bench-0-g22403e387-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''07-base-lor-interval.c'' - ''--enable'' ''ana.int.interval'' ''--enable'' ''witness.yaml.enabled'' ''--enable'' - ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed'' ''--set'' - ''dbg.debug'' ''true'' ''--enable'' ''dbg.timing.enabled'' ''--set'' ''goblint-dir'' - ''.goblint-56-07''' + name: Simmo Saan + version: n/a task: input_files: - 07-base-lor-interval.c diff --git a/tests/regression/56-witness/15-base-unassume-query.yml b/tests/regression/56-witness/15-base-unassume-query.yml index cf037d2d62..664331fb88 100644 --- a/tests/regression/56-witness/15-base-unassume-query.yml +++ b/tests/regression/56-witness/15-base-unassume-query.yml @@ -4,9 +4,8 @@ uuid: dc8526c7-69d5-4ec2-b90c-670bd19c6f1a creation_time: 2022-08-08T11:19:10Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-g1007f57eb-dirty - command_line: '''./goblint'' ''--enable'' ''witness.yaml.enabled'' ''unassume.c''' + name: Simmo Saan + version: n/a task: input_files: - 15-base-unassume-query.c @@ -30,9 +29,8 @@ uuid: 48ab49c6-c030-446d-9b31-673979f1cbd0 creation_time: 2022-08-08T11:19:10Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-g1007f57eb-dirty - command_line: '''./goblint'' ''--enable'' ''witness.yaml.enabled'' ''unassume.c''' + name: Simmo Saan + version: n/a task: input_files: - 15-base-unassume-query.c diff --git a/tests/regression/56-witness/16-base-unassume-dependent.yml b/tests/regression/56-witness/16-base-unassume-dependent.yml index fe8dcd303b..cd84a72c9c 100644 --- a/tests/regression/56-witness/16-base-unassume-dependent.yml +++ b/tests/regression/56-witness/16-base-unassume-dependent.yml @@ -4,11 +4,8 @@ uuid: 349896cf-62cc-42e7-b9a3-f5f422ff4071 creation_time: 2022-08-30T14:46:04Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-ge4b5d9f12-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''16-base-unassume-dependent.c'' - ''--enable'' ''witness.yaml.enabled'' ''--set'' ''dbg.debug'' ''true'' ''--set'' - ''printstats'' ''true'' ''--set'' ''goblint-dir'' ''.goblint-56-16''' + name: Simmo Saan + version: n/a task: input_files: - 16-base-unassume-dependent.c @@ -32,11 +29,8 @@ uuid: 349896cf-62cc-42e7-b9a3-f5f422ff4071 creation_time: 2022-08-30T14:46:04Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-ge4b5d9f12-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''16-base-unassume-dependent.c'' - ''--enable'' ''witness.yaml.enabled'' ''--set'' ''dbg.debug'' ''true'' ''--set'' - ''printstats'' ''true'' ''--set'' ''goblint-dir'' ''.goblint-56-16''' + name: Simmo Saan + version: n/a task: input_files: - 16-base-unassume-dependent.c @@ -60,11 +54,8 @@ uuid: 349896cf-62cc-42e7-b9a3-f5f422ff4071 creation_time: 2022-08-30T14:46:04Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-ge4b5d9f12-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''16-base-unassume-dependent.c'' - ''--enable'' ''witness.yaml.enabled'' ''--set'' ''dbg.debug'' ''true'' ''--set'' - ''printstats'' ''true'' ''--set'' ''goblint-dir'' ''.goblint-56-16''' + name: Simmo Saan + version: n/a task: input_files: - 16-base-unassume-dependent.c diff --git a/tests/regression/56-witness/17-base-unassume-tauto.yml b/tests/regression/56-witness/17-base-unassume-tauto.yml index 358434238c..2ef3c6df54 100644 --- a/tests/regression/56-witness/17-base-unassume-tauto.yml +++ b/tests/regression/56-witness/17-base-unassume-tauto.yml @@ -4,11 +4,8 @@ uuid: 828f8b0f-590b-4180-bef1-d2b18cc240e6 creation_time: 2022-08-30T14:58:31Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-ge4b5d9f12-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''17-base-unassume-tauto.c'' - ''--enable'' ''witness.yaml.enabled'' ''--set'' ''dbg.debug'' ''true'' ''--set'' - ''printstats'' ''true'' ''--set'' ''goblint-dir'' ''.goblint-56-17''' + name: Simmo Saan + version: n/a task: input_files: - 17-base-unassume-tauto.c diff --git a/tests/regression/56-witness/18-base-unassume-contra.yml b/tests/regression/56-witness/18-base-unassume-contra.yml index c3306e1ffa..f793820a61 100644 --- a/tests/regression/56-witness/18-base-unassume-contra.yml +++ b/tests/regression/56-witness/18-base-unassume-contra.yml @@ -4,11 +4,8 @@ uuid: e9cde5db-0c69-4413-ad46-7a15b93f1834 creation_time: 2022-08-30T15:00:25Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-ge4b5d9f12-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''18-base-unassume-contra.c'' - ''--enable'' ''witness.yaml.enabled'' ''--set'' ''dbg.debug'' ''true'' ''--set'' - ''printstats'' ''true'' ''--set'' ''goblint-dir'' ''.goblint-56-18''' + name: Simmo Saan + version: n/a task: input_files: - 18-base-unassume-contra.c diff --git a/tests/regression/56-witness/19-base-unassume-mem.yml b/tests/regression/56-witness/19-base-unassume-mem.yml index 9d68446eba..ec45270322 100644 --- a/tests/regression/56-witness/19-base-unassume-mem.yml +++ b/tests/regression/56-witness/19-base-unassume-mem.yml @@ -4,10 +4,8 @@ uuid: ddb9942d-998c-425d-a74f-228044bc38fb creation_time: 2022-09-01T10:15:07Z producer: - name: Goblint - version: heads/yaml-witness-unassume-base-0-ged336aa6c-dirty - command_line: '''../../../goblint'' ''--enable'' ''ana.int.interval'' ''--enable'' - ''witness.yaml.enabled'' ''19-base-unassume-mem.c''' + name: Simmo Saan + version: n/a task: input_files: - 19-base-unassume-mem.c @@ -31,10 +29,8 @@ uuid: ddb9942d-998c-425d-a74f-228044bc38fb creation_time: 2022-09-01T10:15:07Z producer: - name: Goblint - version: heads/yaml-witness-unassume-base-0-ged336aa6c-dirty - command_line: '''../../../goblint'' ''--enable'' ''ana.int.interval'' ''--enable'' - ''witness.yaml.enabled'' ''19-base-unassume-mem.c''' + name: Simmo Saan + version: n/a task: input_files: - 19-base-unassume-mem.c diff --git a/tests/regression/56-witness/21-apron-unassume-priv.yml b/tests/regression/56-witness/21-apron-unassume-priv.yml index ab3eb0c6c1..93bef12853 100644 --- a/tests/regression/56-witness/21-apron-unassume-priv.yml +++ b/tests/regression/56-witness/21-apron-unassume-priv.yml @@ -4,12 +4,8 @@ uuid: 85b0932e-717e-47ea-b7a0-6ed5ca294047 creation_time: 2022-09-14T09:58:32Z producer: - name: Goblint - version: heads/yaml-witness-unassume-apron-0-gbb3e9f109-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''21-apron-unassume-priv.c'' - ''--set'' ''ana.activated[+]'' ''apron'' ''--enable'' ''witness.yaml.enabled'' - ''--set'' ''dbg.debug'' ''true'' ''--set'' ''printstats'' ''true'' ''--set'' - ''goblint-dir'' ''.goblint-56-21''' + name: Simmo Saan + version: n/a task: input_files: - 21-apron-unassume-priv.c diff --git a/tests/regression/56-witness/22-base-unassume-priv.yml b/tests/regression/56-witness/22-base-unassume-priv.yml index f063ed7e6b..1fcba2e4ac 100644 --- a/tests/regression/56-witness/22-base-unassume-priv.yml +++ b/tests/regression/56-witness/22-base-unassume-priv.yml @@ -4,12 +4,8 @@ uuid: 85b0932e-717e-47ea-b7a0-6ed5ca294047 creation_time: 2022-09-14T09:58:32Z producer: - name: Goblint - version: heads/yaml-witness-unassume-apron-0-gbb3e9f109-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''22-base-unassume-priv.c'' - ''--set'' ''ana.activated[+]'' ''apron'' ''--enable'' ''witness.yaml.enabled'' - ''--set'' ''dbg.debug'' ''true'' ''--set'' ''printstats'' ''true'' ''--set'' - ''goblint-dir'' ''.goblint-56-21''' + name: Simmo Saan + version: n/a task: input_files: - 22-base-unassume-priv.c diff --git a/tests/regression/56-witness/23-base-unassume-priv2.yml b/tests/regression/56-witness/23-base-unassume-priv2.yml index 4ca5142b0a..9265d21f77 100644 --- a/tests/regression/56-witness/23-base-unassume-priv2.yml +++ b/tests/regression/56-witness/23-base-unassume-priv2.yml @@ -4,12 +4,8 @@ uuid: 85b0932e-717e-47ea-b7a0-6ed5ca294047 creation_time: 2022-09-14T09:58:32Z producer: - name: Goblint - version: heads/yaml-witness-unassume-apron-0-gbb3e9f109-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''23-base-unassume-priv2.c'' - ''--set'' ''ana.activated[+]'' ''apron'' ''--enable'' ''witness.yaml.enabled'' - ''--set'' ''dbg.debug'' ''true'' ''--set'' ''printstats'' ''true'' ''--set'' - ''goblint-dir'' ''.goblint-56-21''' + name: Simmo Saan + version: n/a task: input_files: - 23-base-unassume-priv2.c diff --git a/tests/regression/56-witness/24-apron-unassume-priv2.yml b/tests/regression/56-witness/24-apron-unassume-priv2.yml index d775d14929..6ca529fb76 100644 --- a/tests/regression/56-witness/24-apron-unassume-priv2.yml +++ b/tests/regression/56-witness/24-apron-unassume-priv2.yml @@ -4,12 +4,8 @@ uuid: 85b0932e-717e-47ea-b7a0-6ed5ca294047 creation_time: 2022-09-14T09:58:32Z producer: - name: Goblint - version: heads/yaml-witness-unassume-apron-0-gbb3e9f109-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''24-apron-unassume-priv2.c'' - ''--set'' ''ana.activated[+]'' ''apron'' ''--enable'' ''witness.yaml.enabled'' - ''--set'' ''dbg.debug'' ''true'' ''--set'' ''printstats'' ''true'' ''--set'' - ''goblint-dir'' ''.goblint-56-21''' + name: Simmo Saan + version: n/a task: input_files: - 24-apron-unassume-priv2.c diff --git a/tests/regression/56-witness/25-apron-unassume-strengthening.yml b/tests/regression/56-witness/25-apron-unassume-strengthening.yml index 75d4df8026..1189a926fa 100644 --- a/tests/regression/56-witness/25-apron-unassume-strengthening.yml +++ b/tests/regression/56-witness/25-apron-unassume-strengthening.yml @@ -4,12 +4,8 @@ uuid: dec4db01-03ed-47dd-ae55-c84f8dcd51ed creation_time: 2022-09-13T11:38:16Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-g82e0e31ba-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''19-apron-unassume-strengthening.c'' - ''--set'' ''ana.activated[+]'' ''apron'' ''--enable'' ''witness.yaml.enabled'' - ''--set'' ''dbg.debug'' ''true'' ''--set'' ''printstats'' ''true'' ''--set'' - ''goblint-dir'' ''.goblint-56-19''' + name: Simmo Saan + version: n/a task: input_files: - 25-apron-unassume-strengthening.c diff --git a/tests/regression/56-witness/30-base-unassume-inc-dec.yml b/tests/regression/56-witness/30-base-unassume-inc-dec.yml index d328abe556..f372149f44 100644 --- a/tests/regression/56-witness/30-base-unassume-inc-dec.yml +++ b/tests/regression/56-witness/30-base-unassume-inc-dec.yml @@ -4,12 +4,8 @@ uuid: e1da1c44-5406-4bce-ab4a-3597a2b36e24 creation_time: 2022-10-07T11:52:13Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-g9426848d9-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''30-base-unassume-inc-dec.c'' - ''--enable'' ''ana.int.interval'' ''--enable'' ''witness.yaml.enabled'' ''--set'' - ''dbg.debug'' ''true'' ''--enable'' ''dbg.timing.enabled'' ''--set'' ''goblint-dir'' - ''.goblint-56-30''' + name: Simmo Saan + version: n/a task: input_files: - 30-base-unassume-inc-dec.c @@ -33,12 +29,8 @@ uuid: 16a70fb8-6f51-4a2c-a2e0-a68a4baf1575 creation_time: 2022-10-07T11:52:13Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-g9426848d9-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''30-base-unassume-inc-dec.c'' - ''--enable'' ''ana.int.interval'' ''--enable'' ''witness.yaml.enabled'' ''--set'' - ''dbg.debug'' ''true'' ''--enable'' ''dbg.timing.enabled'' ''--set'' ''goblint-dir'' - ''.goblint-56-30''' + name: Simmo Saan + version: n/a task: input_files: - 30-base-unassume-inc-dec.c diff --git a/tests/regression/56-witness/31-base-unassume-mem-ex.yml b/tests/regression/56-witness/31-base-unassume-mem-ex.yml index 75b1dba18d..1bbe991811 100644 --- a/tests/regression/56-witness/31-base-unassume-mem-ex.yml +++ b/tests/regression/56-witness/31-base-unassume-mem-ex.yml @@ -4,12 +4,8 @@ uuid: 8a156304-0058-4a15-a934-884483183ba8 creation_time: 2022-10-07T12:43:24Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-g9426848d9-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''31-base-unassume-mem-ex.c'' - ''--enable'' ''ana.int.interval'' ''--enable'' ''witness.yaml.enabled'' ''--set'' - ''dbg.debug'' ''true'' ''--enable'' ''dbg.timing.enabled'' ''--set'' ''goblint-dir'' - ''.goblint-56-31''' + name: Simmo Saan + version: n/a task: input_files: - 31-base-unassume-mem-ex.c @@ -33,12 +29,8 @@ uuid: 1d367e5b-84a7-42e3-8191-11384aeca509 creation_time: 2022-10-07T12:43:24Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-g9426848d9-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''31-base-unassume-mem-ex.c'' - ''--enable'' ''ana.int.interval'' ''--enable'' ''witness.yaml.enabled'' ''--set'' - ''dbg.debug'' ''true'' ''--enable'' ''dbg.timing.enabled'' ''--set'' ''goblint-dir'' - ''.goblint-56-31''' + name: Simmo Saan + version: n/a task: input_files: - 31-base-unassume-mem-ex.c @@ -62,12 +54,8 @@ uuid: a5dc6e03-3748-4e52-befc-8c846634e329 creation_time: 2022-10-07T12:43:24Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-g9426848d9-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''31-base-unassume-mem-ex.c'' - ''--enable'' ''ana.int.interval'' ''--enable'' ''witness.yaml.enabled'' ''--set'' - ''dbg.debug'' ''true'' ''--enable'' ''dbg.timing.enabled'' ''--set'' ''goblint-dir'' - ''.goblint-56-31''' + name: Simmo Saan + version: n/a task: input_files: - 31-base-unassume-mem-ex.c diff --git a/tests/regression/56-witness/32-base-unassume-lor-addr.yml b/tests/regression/56-witness/32-base-unassume-lor-addr.yml index a0c6476fe1..a657a452ad 100644 --- a/tests/regression/56-witness/32-base-unassume-lor-addr.yml +++ b/tests/regression/56-witness/32-base-unassume-lor-addr.yml @@ -4,11 +4,8 @@ uuid: d2a65147-2d04-49f8-8f27-fe3a7c8553b7 creation_time: 2022-10-07T12:50:05Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-g9426848d9-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''32-base-unassume-lor-addr.c'' - ''--enable'' ''witness.yaml.enabled'' ''--set'' ''dbg.debug'' ''true'' ''--enable'' - ''dbg.timing.enabled'' ''--set'' ''goblint-dir'' ''.goblint-56-32''' + name: Simmo Saan + version: n/a task: input_files: - 32-base-unassume-lor-addr.c diff --git a/tests/regression/56-witness/33-base-unassume-lor-enums.yml b/tests/regression/56-witness/33-base-unassume-lor-enums.yml index c3220fca14..1ecc84802e 100644 --- a/tests/regression/56-witness/33-base-unassume-lor-enums.yml +++ b/tests/regression/56-witness/33-base-unassume-lor-enums.yml @@ -4,12 +4,8 @@ uuid: 8c07adbd-908d-45be-af99-943634ad66b4 creation_time: 2022-10-07T13:43:40Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-gd4687e4f4-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''33-base-unassume-lor-enums.c'' - ''--enable'' ''ana.int.enums'' ''--enable'' ''witness.yaml.enabled'' ''--set'' - ''dbg.debug'' ''true'' ''--enable'' ''dbg.timing.enabled'' ''--set'' ''goblint-dir'' - ''.goblint-56-33''' + name: Simmo Saan + version: n/a task: input_files: - 33-base-unassume-lor-enums.c diff --git a/tests/regression/56-witness/34-base-unassume-inc-dec-traces.yml b/tests/regression/56-witness/34-base-unassume-inc-dec-traces.yml index 55fa88bd52..9f411870cc 100644 --- a/tests/regression/56-witness/34-base-unassume-inc-dec-traces.yml +++ b/tests/regression/56-witness/34-base-unassume-inc-dec-traces.yml @@ -4,12 +4,8 @@ uuid: e1da1c44-5406-4bce-ab4a-3597a2b36e24 creation_time: 2022-10-07T11:52:13Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-g9426848d9-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''34-base-unassume-inc-dec-traces.c'' - ''--enable'' ''ana.int.interval'' ''--enable'' ''witness.yaml.enabled'' ''--set'' - ''dbg.debug'' ''true'' ''--enable'' ''dbg.timing.enabled'' ''--set'' ''goblint-dir'' - ''.goblint-56-30''' + name: Simmo Saan + version: n/a task: input_files: - 34-base-unassume-inc-dec-traces.c @@ -33,12 +29,8 @@ uuid: 16a70fb8-6f51-4a2c-a2e0-a68a4baf1575 creation_time: 2022-10-07T11:52:13Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-g9426848d9-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''34-base-unassume-inc-dec-traces.c'' - ''--enable'' ''ana.int.interval'' ''--enable'' ''witness.yaml.enabled'' ''--set'' - ''dbg.debug'' ''true'' ''--enable'' ''dbg.timing.enabled'' ''--set'' ''goblint-dir'' - ''.goblint-56-30''' + name: Simmo Saan + version: n/a task: input_files: - 34-base-unassume-inc-dec-traces.c diff --git a/tests/regression/56-witness/42-base-unassume-precheck.yml b/tests/regression/56-witness/42-base-unassume-precheck.yml index 30f8901c3a..fa00d06528 100644 --- a/tests/regression/56-witness/42-base-unassume-precheck.yml +++ b/tests/regression/56-witness/42-base-unassume-precheck.yml @@ -4,11 +4,8 @@ uuid: e9cde5db-0c69-4413-ad46-7a15b93f1834 creation_time: 2022-08-30T15:00:25Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-ge4b5d9f12-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''42-base-unassume-precheck.c'' - ''--enable'' ''witness.yaml.enabled'' ''--set'' ''dbg.debug'' ''true'' ''--set'' - ''printstats'' ''true'' ''--set'' ''goblint-dir'' ''.goblint-56-18''' + name: Simmo Saan + version: n/a task: input_files: - 42-base-unassume-precheck.c diff --git a/tests/regression/56-witness/43-apron-unassume-precheck.yml b/tests/regression/56-witness/43-apron-unassume-precheck.yml index 355283228c..65e72e1b45 100644 --- a/tests/regression/56-witness/43-apron-unassume-precheck.yml +++ b/tests/regression/56-witness/43-apron-unassume-precheck.yml @@ -4,11 +4,8 @@ uuid: e9cde5db-0c69-4413-ad46-7a15b93f1834 creation_time: 2022-08-30T15:00:25Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-ge4b5d9f12-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''43-apron-unassume-precheck.c'' - ''--enable'' ''witness.yaml.enabled'' ''--set'' ''dbg.debug'' ''true'' ''--set'' - ''printstats'' ''true'' ''--set'' ''goblint-dir'' ''.goblint-56-18''' + name: Simmo Saan + version: n/a task: input_files: - 43-apron-unassume-precheck.c @@ -32,11 +29,8 @@ uuid: e9cde5db-0c69-4413-ad46-7a15b93f1834 creation_time: 2022-08-30T15:00:25Z producer: - name: Goblint - version: heads/yaml-witness-unassume-0-ge4b5d9f12-dirty - command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''43-apron-unassume-precheck.c'' - ''--enable'' ''witness.yaml.enabled'' ''--set'' ''dbg.debug'' ''true'' ''--set'' - ''printstats'' ''true'' ''--set'' ''goblint-dir'' ''.goblint-56-18''' + name: Simmo Saan + version: n/a task: input_files: - 43-apron-unassume-precheck.c From bb7cedb989402fcf0b7188107e1b82f83b15f192 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 15 Mar 2024 12:01:25 +0200 Subject: [PATCH 53/55] Fix witness metadata for 56-witness/01-base-lor-enums and 02-base-lor-addr --- .../56-witness/01-base-lor-enums.yml | 55 +++++++------------ .../56-witness/02-base-lor-addr.yml | 55 +++++++------------ 2 files changed, 40 insertions(+), 70 deletions(-) diff --git a/tests/regression/56-witness/01-base-lor-enums.yml b/tests/regression/56-witness/01-base-lor-enums.yml index 836255d5d4..8f1f64f66c 100644 --- a/tests/regression/56-witness/01-base-lor-enums.yml +++ b/tests/regression/56-witness/01-base-lor-enums.yml @@ -4,16 +4,13 @@ uuid: e5802c77-d0ac-4f91-a0ac-c97ba97697d5 creation_time: 2022-06-16T06:37:52Z producer: - name: Goblint - version: heads/base-eval-lor-0-g5a1ac0905-dirty - command_line: '''./goblint'' ''--enable'' ''dbg.debug'' ''--enable'' ''dbg.regression'' - ''--html'' ''--enable'' ''ana.int.enums'' ''--enable'' ''witness.yaml.enabled'' - ''tests/regression/56-witness/01-base-lor-enums.c''' + name: Simmo Saan + version: n/a task: input_files: - - tests/regression/56-witness/01-base-lor-enums.c + - 01-base-lor-enums.c input_file_hashes: - tests/regression/56-witness/01-base-lor-enums.c: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01 + 01-base-lor-enums.c: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01 data_model: LP64 language: C location: @@ -32,16 +29,13 @@ uuid: e5802c77-d0ac-4f91-a0ac-c97ba97697d5 creation_time: 2022-06-16T06:37:52Z producer: - name: Goblint - version: heads/base-eval-lor-0-g5a1ac0905-dirty - command_line: '''./goblint'' ''--enable'' ''dbg.debug'' ''--enable'' ''dbg.regression'' - ''--html'' ''--enable'' ''ana.int.enums'' ''--enable'' ''witness.yaml.enabled'' - ''tests/regression/56-witness/01-base-lor-enums.c''' + name: Simmo Saan + version: n/a task: input_files: - - tests/regression/56-witness/01-base-lor-enums.c + - 01-base-lor-enums.c input_file_hashes: - tests/regression/56-witness/01-base-lor-enums.c: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01 + 01-base-lor-enums.c: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01 data_model: LP64 language: C location: @@ -60,16 +54,13 @@ uuid: e5802c77-d0ac-4f91-a0ac-c97ba97697d5 creation_time: 2022-06-16T06:37:52Z producer: - name: Goblint - version: heads/base-eval-lor-0-g5a1ac0905-dirty - command_line: '''./goblint'' ''--enable'' ''dbg.debug'' ''--enable'' ''dbg.regression'' - ''--html'' ''--enable'' ''ana.int.enums'' ''--enable'' ''witness.yaml.enabled'' - ''tests/regression/56-witness/01-base-lor-enums.c''' + name: Simmo Saan + version: n/a task: input_files: - - tests/regression/56-witness/01-base-lor-enums.c + - 01-base-lor-enums.c input_file_hashes: - tests/regression/56-witness/01-base-lor-enums.c: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01 + 01-base-lor-enums.c: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01 data_model: LP64 language: C location: @@ -88,16 +79,13 @@ uuid: e5802c77-d0ac-4f91-a0ac-c97ba97697d5 creation_time: 2022-06-16T06:37:52Z producer: - name: Goblint - version: heads/base-eval-lor-0-g5a1ac0905-dirty - command_line: '''./goblint'' ''--enable'' ''dbg.debug'' ''--enable'' ''dbg.regression'' - ''--html'' ''--enable'' ''ana.int.enums'' ''--enable'' ''witness.yaml.enabled'' - ''tests/regression/56-witness/01-base-lor-enums.c''' + name: Simmo Saan + version: n/a task: input_files: - - tests/regression/56-witness/01-base-lor-enums.c + - 01-base-lor-enums.c input_file_hashes: - tests/regression/56-witness/01-base-lor-enums.c: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01 + 01-base-lor-enums.c: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01 data_model: LP64 language: C location: @@ -116,16 +104,13 @@ uuid: e5802c77-d0ac-4f91-a0ac-c97ba97697d5 creation_time: 2022-06-16T06:37:52Z producer: - name: Goblint - version: heads/base-eval-lor-0-g5a1ac0905-dirty - command_line: '''./goblint'' ''--enable'' ''dbg.debug'' ''--enable'' ''dbg.regression'' - ''--html'' ''--enable'' ''ana.int.enums'' ''--enable'' ''witness.yaml.enabled'' - ''tests/regression/56-witness/01-base-lor-enums.c''' + name: Simmo Saan + version: n/a task: input_files: - - tests/regression/56-witness/01-base-lor-enums.c + - 01-base-lor-enums.c input_file_hashes: - tests/regression/56-witness/01-base-lor-enums.c: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01 + 01-base-lor-enums.c: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01 data_model: LP64 language: C location: diff --git a/tests/regression/56-witness/02-base-lor-addr.yml b/tests/regression/56-witness/02-base-lor-addr.yml index b2980416a5..e8922b0894 100644 --- a/tests/regression/56-witness/02-base-lor-addr.yml +++ b/tests/regression/56-witness/02-base-lor-addr.yml @@ -4,16 +4,13 @@ uuid: e5802c77-d0ac-4f91-a0ac-c97ba97697d5 creation_time: 2022-06-16T06:37:52Z producer: - name: Goblint - version: heads/base-eval-lor-0-g5a1ac0905-dirty - command_line: '''./goblint'' ''--enable'' ''dbg.debug'' ''--enable'' ''dbg.regression'' - ''--html'' ''--enable'' ''ana.int.enums'' ''--enable'' ''witness.yaml.enabled'' - ''tests/regression/56-witness/02-base-lor-addr.c''' + name: Simmo Saan + version: n/a task: input_files: - - tests/regression/56-witness/02-base-lor-addr.c + - 02-base-lor-addr.c input_file_hashes: - tests/regression/56-witness/02-base-lor-addr.c: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01 + 02-base-lor-addr.c: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01 data_model: LP64 language: C location: @@ -32,16 +29,13 @@ uuid: e5802c77-d0ac-4f91-a0ac-c97ba97697d5 creation_time: 2022-06-16T06:37:52Z producer: - name: Goblint - version: heads/base-eval-lor-0-g5a1ac0905-dirty - command_line: '''./goblint'' ''--enable'' ''dbg.debug'' ''--enable'' ''dbg.regression'' - ''--html'' ''--enable'' ''ana.int.enums'' ''--enable'' ''witness.yaml.enabled'' - ''tests/regression/56-witness/02-base-lor-addr.c''' + name: Simmo Saan + version: n/a task: input_files: - - tests/regression/56-witness/02-base-lor-addr.c + - 02-base-lor-addr.c input_file_hashes: - tests/regression/56-witness/02-base-lor-addr.c: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01 + 02-base-lor-addr.c: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01 data_model: LP64 language: C location: @@ -60,16 +54,13 @@ uuid: e5802c77-d0ac-4f91-a0ac-c97ba97697d5 creation_time: 2022-06-16T06:37:52Z producer: - name: Goblint - version: heads/base-eval-lor-0-g5a1ac0905-dirty - command_line: '''./goblint'' ''--enable'' ''dbg.debug'' ''--enable'' ''dbg.regression'' - ''--html'' ''--enable'' ''ana.int.enums'' ''--enable'' ''witness.yaml.enabled'' - ''tests/regression/56-witness/02-base-lor-addr.c''' + name: Simmo Saan + version: n/a task: input_files: - - tests/regression/56-witness/02-base-lor-addr.c + - 02-base-lor-addr.c input_file_hashes: - tests/regression/56-witness/02-base-lor-addr.c: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01 + 02-base-lor-addr.c: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01 data_model: LP64 language: C location: @@ -88,16 +79,13 @@ uuid: e5802c77-d0ac-4f91-a0ac-c97ba97697d5 creation_time: 2022-06-16T06:37:52Z producer: - name: Goblint - version: heads/base-eval-lor-0-g5a1ac0905-dirty - command_line: '''./goblint'' ''--enable'' ''dbg.debug'' ''--enable'' ''dbg.regression'' - ''--html'' ''--enable'' ''ana.int.enums'' ''--enable'' ''witness.yaml.enabled'' - ''tests/regression/56-witness/02-base-lor-addr.c''' + name: Simmo Saan + version: n/a task: input_files: - - tests/regression/56-witness/02-base-lor-addr.c + - 02-base-lor-addr.c input_file_hashes: - tests/regression/56-witness/02-base-lor-addr.c: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01 + 02-base-lor-addr.c: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01 data_model: LP64 language: C location: @@ -116,16 +104,13 @@ uuid: e5802c77-d0ac-4f91-a0ac-c97ba97697d5 creation_time: 2022-06-16T06:37:52Z producer: - name: Goblint - version: heads/base-eval-lor-0-g5a1ac0905-dirty - command_line: '''./goblint'' ''--enable'' ''dbg.debug'' ''--enable'' ''dbg.regression'' - ''--html'' ''--enable'' ''ana.int.enums'' ''--enable'' ''witness.yaml.enabled'' - ''tests/regression/56-witness/02-base-lor-addr.c''' + name: Simmo Saan + version: n/a task: input_files: - - tests/regression/56-witness/02-base-lor-addr.c + - 02-base-lor-addr.c input_file_hashes: - tests/regression/56-witness/02-base-lor-addr.c: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01 + 02-base-lor-addr.c: 5f686f726d140fbb7f3052f778e99aa09e3807cc6972a4d4905df2f6ed0c3e01 data_model: LP64 language: C location: From 8f318b25e8c9ff61a7910866a9f7f0298684725c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 15 Mar 2024 17:53:27 +0200 Subject: [PATCH 54/55] Unskip working 04-mutex/26-ptrrace_default --- tests/regression/04-mutex/26-ptrrace_default.c | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/tests/regression/04-mutex/26-ptrrace_default.c b/tests/regression/04-mutex/26-ptrrace_default.c index fe9315b40b..38b7cc8729 100644 --- a/tests/regression/04-mutex/26-ptrrace_default.c +++ b/tests/regression/04-mutex/26-ptrrace_default.c @@ -1,6 +1,3 @@ -// SKIP: Don't see the point in such elaborate invalidations for unknown -// functions since we warn unsound on this anyway. - #include /** @@ -29,7 +26,7 @@ int main() { pthread_t id; pthread_create(&id, NULL, t_fun, NULL); /* reset_glob(); */ - foo(reset_glob); + foo(reset_glob); // TODO: make invalidate call instead of spawning pthread_join (id, NULL); return 0; } From 92de654854c45e48dc4e210dd9b208b7ea834b23 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 15 Mar 2024 18:02:04 +0200 Subject: [PATCH 55/55] Remove TODO from 04-mutex/40-rw_lock_rc Done by issue #843 and PR #1184. --- tests/regression/04-mutex/40-rw_lock_rc.c | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/tests/regression/04-mutex/40-rw_lock_rc.c b/tests/regression/04-mutex/40-rw_lock_rc.c index 36bd01a95d..27c4cf4d8b 100644 --- a/tests/regression/04-mutex/40-rw_lock_rc.c +++ b/tests/regression/04-mutex/40-rw_lock_rc.c @@ -1,5 +1,4 @@ -// PARAM: --set kernel true --set mainfun[+] "'test_init'" --set ana.thread.domain plain -// TODO: make unknown function spawns non-unique with history thread domain for data1 self-race +// PARAM: --set kernel true --set mainfun[+] "'test_init'" #include #include #include