Skip to content

Interval Analysis for Floating-point values #761

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 62 commits into from
Jul 27, 2022
Merged

Interval Analysis for Floating-point values #761

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
62 commits
Select commit Hold shift + click to select a range
39af0cc
Inject dummy float domain into analysis framework
Dudeldu May 6, 2022
87a9398
Implement basic functionality for covering const-propagated asserts
Dudeldu May 7, 2022
ffd1538
Introduce new ana.float.interval option
Dudeldu May 12, 2022
8808ced
Add wrapper domain for Floating point in general
Dudeldu May 12, 2022
e11c846
Apply different renamings and undo formatting inside FloatInterval
Dudeldu May 15, 2022
47fd747
Fix rename and unused import
Dudeldu May 17, 2022
fad2037
Add node-level configurability of float analysis
Dudeldu May 18, 2022
e8c496d
most functionality implemented - no unittests yet, only framework!
FelixKrayer May 15, 2022
bd1ef2a
fix leq and add unittests
FelixKrayer May 21, 2022
994e511
some fixes and suggested changes
FelixKrayer May 23, 2022
8c7c7f4
Add basic warnings for float domain
brgr May 30, 2022
b0c6bb1
Provide cast support between int types and double
Dudeldu May 13, 2022
c6b8592
include Printable.Std for default implementation and fix sub
FelixKrayer Jun 2, 2022
02d81db
Implementation of invariant for capturing information from branching …
Dudeldu Jun 9, 2022
e026bfa
Add unittests for our domain (#9)
Dudeldu Jun 14, 2022
1b96fe4
Add all math.h functions in libraryFunctions.ml with readsAll (#12)
brgr Jun 14, 2022
eadd02f
Implement float operators in C / Support Float and Double (#10)
Dudeldu Jun 15, 2022
82c0bf4
implemented float classification functions from math.h (#14)
FelixKrayer Jun 16, 2022
7d5b149
Add further warnings (#11)
brgr Jun 16, 2022
6fa973a
Fix and remove todos for our first "real" PR (#16)
brgr Jun 16, 2022
449ce45
reorder test ids in float regression tests (#17)
brgr Jun 16, 2022
e956617
Merge remote-tracking branch 'base-repo/master'
Dudeldu Jun 16, 2022
1231d4d
Merge pull request #18 from Dudeldu/tmp-master
Dudeldu Jun 23, 2022
9374f93
Merge remote-tracking branch 'base-repo/master'
Dudeldu Jun 23, 2022
c9e3c9f
Merge pull request #22 from Dudeldu/tmp-master2
Dudeldu Jun 23, 2022
54693dd
rename float test folder
FelixKrayer Jun 23, 2022
788c208
Implement invariant and projection for float domain (#25)
Dudeldu Jun 29, 2022
a010ad6
Address the comments in the PR (#24)
Dudeldu Jun 29, 2022
8f16da6
Remove reinterpret_cast/bit_cast between floats and ints to be sound …
Dudeldu Jun 30, 2022
dc0f084
implemented trigonometric float functions from math.h
FelixKrayer Jun 10, 2022
4935261
implement suggestions
FelixKrayer Jun 28, 2022
fcf85c1
Reset to old rounding mode in all c functions now (#27)
Dudeldu Jul 4, 2022
fde2640
Fix invariant computation according to IEEE754 (#21)
Dudeldu Jul 4, 2022
b0fa916
Check long doubles support and add tests for them (#26)
Dudeldu Jul 5, 2022
de7aa3d
float bot at 'intervalImpl'-level
FelixKrayer Jul 2, 2022
577c353
implement try with, arbitrary, suggestions
FelixKrayer Jul 4, 2022
14cf19d
add svcomp test and unittest for exception
FelixKrayer Jul 5, 2022
0b23f7c
Implement suggestion for LibraryFunctions (math type) (#30)
FelixKrayer Jul 6, 2022
4085534
Ensure that usage of complex numbers results in top (#31)
Dudeldu Jul 8, 2022
9b01b75
Different cleanups (#32)
Dudeldu Jul 8, 2022
7df73ed
Merge remote-tracking branch 'base-repo/master' into tmp-master3
Dudeldu Jul 8, 2022
5eb5c40
fix wording of Warning for Domain Error and add -f, -l trig. function…
FelixKrayer Jul 8, 2022
bc50e58
Merge pull request #35 from Dudeldu/tmp-master3
Dudeldu Jul 9, 2022
c44aee4
Change warnings (#36)
Dudeldu Jul 11, 2022
9ef18e9
fix 'Cilfacade.get_ikind: non-integer type double' (#37)
FelixKrayer Jul 13, 2022
19b7638
Wrap get_ikind in try except to avoid crashing on invalid branching t…
Dudeldu Jul 14, 2022
8c9769c
include missing asserts in regressiontests (#39)
FelixKrayer Jul 14, 2022
d660e4e
add fabs and builtin inf/nan (#40)
FelixKrayer Jul 15, 2022
d31be72
Find another location where get_ikind results in an error (#41)
Dudeldu Jul 19, 2022
380ec34
Improve narrowing by introducing additional step (#42)
Dudeldu Jul 20, 2022
2f116a6
Merge remote-tracking branch 'base-repo/master'
Dudeldu Jul 25, 2022
47c0070
Merge pull request #44 from Dudeldu/merge-remote
Dudeldu Jul 25, 2022
437ec6e
Fix typo
michael-schwarz Jul 26, 2022
c6a31b6
Modify test 57/12 to actually trigger the issue
michael-schwarz Jul 26, 2022
c21875d
Whitespace
michael-schwarz Jul 26, 2022
84d5ca5
Add unsoundness example
michael-schwarz Jul 26, 2022
93d6f91
Typo
michael-schwarz Jul 26, 2022
1600513
Fix unsoundness with floats in branches by going to top for those cases
Dudeldu Jul 26, 2022
5830912
Refine branching on floats for negative case
Dudeldu Jul 26, 2022
9dcb3b5
Typos & rename first `invariant` in `base.ml` to `invariant_fallback`
michael-schwarz Jul 27, 2022
e9589fb
Typos in `floatDomain.ml`
michael-schwarz Jul 27, 2022
08a624d
Remove CWEs from operations where they don't really apply
michael-schwarz Jul 27, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
544 changes: 398 additions & 146 deletions src/analyses/base.ml
View file
Open in desktop

Large diffs are not rendered by default.

18 changes: 18 additions & 0 deletions src/analyses/libraryDesc.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,23 @@ struct
}
end

type math =
| Nan of (Cil.fkind * Cil.exp)
| Inf of Cil.fkind
| Isfinite of Cil.exp
| Isinf of Cil.exp
| Isnan of Cil.exp
| Isnormal of Cil.exp
| Signbit of Cil.exp
| Fabs of (Cil.fkind * Cil.exp)
| Acos of (Cil.fkind * Cil.exp)
| Asin of (Cil.fkind * Cil.exp)
| Atan of (Cil.fkind * Cil.exp)
| Atan2 of (Cil.fkind * Cil.exp * Cil.exp)
| Cos of (Cil.fkind * Cil.exp)
| Sin of (Cil.fkind * Cil.exp)
| Tan of (Cil.fkind * Cil.exp)

(** Type of special function, or {!Unknown}. *)
(* Use inline record if not single {!Cil.exp} argument. *)
type special =
Expand All @@ -23,6 +40,7 @@ type special =
| ThreadCreate of { thread: Cil.exp; start_routine: Cil.exp; arg: Cil.exp; }
| ThreadJoin of { thread: Cil.exp; ret_var: Cil.exp; }
| ThreadExit of { ret_val: Cil.exp; }
| Math of { fun_args: math; }
| Memset of { dest: Cil.exp; ch: Cil.exp; count: Cil.exp; }
| Bzero of { dest: Cil.exp; count: Cil.exp; }
| Abort
Expand Down
227 changes: 227 additions & 0 deletions src/analyses/libraryFunctions.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,55 @@ let zstd_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("ZSTD_customFree", unknown [drop "ptr" [f]; drop "customMem" [r]]);
]

(** math functions.
Functions and builtin versions of function and macros defined in math.h. *)
let math_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("__builtin_nan", special [__ "str" []] @@ fun str -> Math { fun_args = (Nan (FDouble, str)) });
("__builtin_nanf", special [__ "str" []] @@ fun str -> Math { fun_args = (Nan (FFloat, str)) });
("__builtin_nanl", special [__ "str" []] @@ fun str -> Math { fun_args = (Nan (FLongDouble, str)) });
("__builtin_inf", special [] @@ Math { fun_args = Inf FDouble});
("__builtin_inff", special [] @@ Math { fun_args = Inf FFloat});
("__builtin_infl", special [] @@ Math { fun_args = Inf FLongDouble});
("__builtin_isfinite", special [__ "x" []] @@ fun x -> Math { fun_args = (Isfinite x) });
("__builtin_isinf", special [__ "x" []] @@ fun x -> Math { fun_args = (Isinf x) });
("__builtin_isinf_sign", special [__ "x" []] @@ fun x -> Math { fun_args = (Isinf x) });
("__builtin_isnan", special [__ "x" []] @@ fun x -> Math { fun_args = (Isnan x) });
("__builtin_isnormal", special [__ "x" []] @@ fun x -> Math { fun_args = (Isnormal x) });
("__builtin_signbit", special [__ "x" []] @@ fun x -> Math { fun_args = (Signbit x) });
("__builtin_fabs", special [__ "x" []] @@ fun x -> Math { fun_args = (Fabs (FDouble, x)) });
("fabs", special [__ "x" []] @@ fun x -> Math { fun_args = (Fabs (FDouble, x)) });
("fabsf", special [__ "x" []] @@ fun x -> Math { fun_args = (Fabs (FFloat, x)) });
("fabsl", special [__ "x" []] @@ fun x -> Math { fun_args = (Fabs (FLongDouble, x)) });
("__builtin_acos", special [__ "x" []] @@ fun x -> Math { fun_args = (Acos (FDouble, x)) });
("acos", special [__ "x" []] @@ fun x -> Math { fun_args = (Acos (FDouble, x)) });
("acosf", special [__ "x" []] @@ fun x -> Math { fun_args = (Acos (FFloat, x)) });
("acosl", special [__ "x" []] @@ fun x -> Math { fun_args = (Acos (FLongDouble, x)) });
("__builtin_asin", special [__ "x" []] @@ fun x -> Math { fun_args = (Asin (FDouble, x)) });
("asin", special [__ "x" []] @@ fun x -> Math { fun_args = (Asin (FDouble, x)) });
("asinf", special [__ "x" []] @@ fun x -> Math { fun_args = (Asin (FFloat, x)) });
("asinl", special [__ "x" []] @@ fun x -> Math { fun_args = (Asin (FLongDouble, x)) });
("__builtin_atan", special [__ "x" []] @@ fun x -> Math { fun_args = (Atan (FDouble, x)) });
("atan", special [__ "x" []] @@ fun x -> Math { fun_args = (Atan (FDouble, x)) });
("atanf", special [__ "x" []] @@ fun x -> Math { fun_args = (Atan (FFloat, x)) });
("atanl", special [__ "x" []] @@ fun x -> Math { fun_args = (Atan (FLongDouble, x)) });
("__builtin_atan2", special [__ "y" []; __ "x" []] @@ fun y x -> Math { fun_args = (Atan2 (FDouble, y, x)) });
("atan2", special [__ "y" []; __ "x" []] @@ fun y x -> Math { fun_args = (Atan2 (FDouble, y, x)) });
("atan2f", special [__ "y" []; __ "x" []] @@ fun y x -> Math { fun_args = (Atan2 (FFloat, y, x)) });
("atan2l", special [__ "y" []; __ "x" []] @@ fun y x -> Math { fun_args = (Atan2 (FLongDouble, y, x)) });
("__builtin_cos", special [__ "x" []] @@ fun x -> Math { fun_args = (Cos (FDouble, x)) });
("cos", special [__ "x" []] @@ fun x -> Math { fun_args = (Cos (FDouble, x)) });
("cosf", special [__ "x" []] @@ fun x -> Math { fun_args = (Cos (FFloat, x)) });
("cosl", special [__ "x" []] @@ fun x -> Math { fun_args = (Cos (FLongDouble, x)) });
("__builtin_sin", special [__ "x" []] @@ fun x -> Math { fun_args = (Sin (FDouble, x)) });
("sin", special [__ "x" []] @@ fun x -> Math { fun_args = (Sin (FDouble, x)) });
("sinf", special [__ "x" []] @@ fun x -> Math { fun_args = (Sin (FFloat, x)) });
("sinl", special [__ "x" []] @@ fun x -> Math { fun_args = (Sin (FLongDouble, x)) });
("__builtin_tan", special [__ "x" []] @@ fun x -> Math { fun_args = (Tan (FDouble, x)) });
("tan", special [__ "x" []] @@ fun x -> Math { fun_args = (Tan (FDouble, x)) });
("tanf", special [__ "x" []] @@ fun x -> Math { fun_args = (Tan (FFloat, x)) });
("tanl", special [__ "x" []] @@ fun x -> Math { fun_args = (Tan (FLongDouble, x)) });
]

(* TODO: allow selecting which lists to use *)
let library_descs = Hashtbl.of_list (List.concat [
c_descs_list;
Expand All @@ -69,6 +118,7 @@ let library_descs = Hashtbl.of_list (List.concat [
linux_descs_list;
goblint_descs_list;
zstd_descs_list;
math_descs_list;
])


Expand Down Expand Up @@ -544,6 +594,183 @@ let invalidate_actions = [
"sema_init", readsAll;
"down_trylock", readsAll;
"up", readsAll;
"acos", readsAll;
"acosf", readsAll;
"acosh", readsAll;
"acoshf", readsAll;
"acoshl", readsAll;
"acosl", readsAll;
"asin", readsAll;
"asinf", readsAll;
"asinh", readsAll;
"asinhf", readsAll;
"asinhl", readsAll;
"asinl", readsAll;
"atan", readsAll;
"atan2", readsAll;
"atan2f", readsAll;
"atan2l", readsAll;
"atanf", readsAll;
"atanh", readsAll;
"atanhf", readsAll;
"atanhl", readsAll;
"atanl", readsAll;
"cbrt", readsAll;
"cbrtf", readsAll;
"cbrtl", readsAll;
"ceil", readsAll;
"ceilf", readsAll;
"ceill", readsAll;
"copysign", readsAll;
"copysignf", readsAll;
"copysignl", readsAll;
"cos", readsAll;
"cosf", readsAll;
"cosh", readsAll;
"coshf", readsAll;
"coshl", readsAll;
"cosl", readsAll;
"erf", readsAll;
"erfc", readsAll;
"erfcf", readsAll;
"erfcl", readsAll;
"erff", readsAll;
"erfl", readsAll;
"exp", readsAll;
"exp2", readsAll;
"exp2f", readsAll;
"exp2l", readsAll;
"expf", readsAll;
"expl", readsAll;
"expm1", readsAll;
"expm1f", readsAll;
"expm1l", readsAll;
"fabs", readsAll;
"fabsf", readsAll;
"fabsl", readsAll;
"fdim", readsAll;
"fdimf", readsAll;
"fdiml", readsAll;
"floor", readsAll;
"floorf", readsAll;
"floorl", readsAll;
"fma", readsAll;
"fmaf", readsAll;
"fmal", readsAll;
"fmax", readsAll;
"fmaxf", readsAll;
"fmaxl", readsAll;
"fmin", readsAll;
"fminf", readsAll;
"fminl", readsAll;
"fmod", readsAll;
"fmodf", readsAll;
"fmodl", readsAll;
"frexp", readsAll;
"frexpf", readsAll;
"frexpl", readsAll;
"hypot", readsAll;
"hypotf", readsAll;
"hypotl", readsAll;
"ilogb", readsAll;
"ilogbf", readsAll;
"ilogbl", readsAll;
"j0", readsAll;
"j1", readsAll;
"jn", readsAll;
"ldexp", readsAll;
"ldexpf", readsAll;
"ldexpl", readsAll;
"lgamma", readsAll;
"lgammaf", readsAll;
"lgammal", readsAll;
"llrint", readsAll;
"llrintf", readsAll;
"llrintl", readsAll;
"llround", readsAll;
"llroundf", readsAll;
"llroundl", readsAll;
"log", readsAll;
"log10", readsAll;
"log10f", readsAll;
"log10l", readsAll;
"log1p", readsAll;
"log1pf", readsAll;
"log1pl", readsAll;
"log2", readsAll;
"log2f", readsAll;
"log2l", readsAll;
"logb", readsAll;
"logbf", readsAll;
"logbl", readsAll;
"logf", readsAll;
"logl", readsAll;
"lrint", readsAll;
"lrintf", readsAll;
"lrintl", readsAll;
"lround", readsAll;
"lroundf", readsAll;
"lroundl", readsAll;
"modf", readsAll;
"modff", readsAll;
"modfl", readsAll;
"nan", readsAll;
"nanf", readsAll;
"nanl", readsAll;
"nearbyint", readsAll;
"nearbyintf", readsAll;
"nearbyintl", readsAll;
"nextafter", readsAll;
"nextafterf", readsAll;
"nextafterl", readsAll;
"nexttoward", readsAll;
"nexttowardf", readsAll;
"nexttowardl", readsAll;
"pow", readsAll;
"powf", readsAll;
"powl", readsAll;
"remainder", readsAll;
"remainderf", readsAll;
"remainderl", readsAll;
"remquo", readsAll;
"remquof", readsAll;
"remquol", readsAll;
"rint", readsAll;
"rintf", readsAll;
"rintl", readsAll;
"round", readsAll;
"roundf", readsAll;
"roundl", readsAll;
"scalbln", readsAll;
"scalblnf", readsAll;
"scalblnl", readsAll;
"scalbn", readsAll;
"scalbnf", readsAll;
"scalbnl", readsAll;
"sin", readsAll;
"sinf", readsAll;
"sinh", readsAll;
"sinhf", readsAll;
"sinhl", readsAll;
"sinl", readsAll;
"sqrt", readsAll;
"sqrtf", readsAll;
"sqrtl", readsAll;
"tan", readsAll;
"tanf", readsAll;
"tanh", readsAll;
"tanhf", readsAll;
"tanhl", readsAll;
"tanl", readsAll;
"tgamma", readsAll;
"tgammaf", readsAll;
"tgammal", readsAll;
"trunc", readsAll;
"truncf", readsAll;
"truncl", readsAll;
"y0", readsAll;
"y1", readsAll;
"yn", readsAll;
]


Expand Down
Loading