Skip to content

Commit cfab02b

Browse files
michael-schwarzmichael-schwarz
authored
Merge pull request #761 from Dudeldu/master
Interval Analysis for Floating-point values
2 parents 6a4ea80 + 08a624d commit cfab02b

32 files changed

+2997
-178
lines changed

‎src/analyses/base.ml‎

Lines changed: 398 additions & 146 deletions
Large diffs are not rendered by default.

‎src/analyses/libraryDesc.ml‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,23 @@ struct
1111
}
1212
end
1313

14+
type math =
15+
| Nan of (Cil.fkind * Cil.exp)
16+
| Inf of Cil.fkind
17+
| Isfinite of Cil.exp
18+
| Isinf of Cil.exp
19+
| Isnan of Cil.exp
20+
| Isnormal of Cil.exp
21+
| Signbit of Cil.exp
22+
| Fabs of (Cil.fkind * Cil.exp)
23+
| Acos of (Cil.fkind * Cil.exp)
24+
| Asin of (Cil.fkind * Cil.exp)
25+
| Atan of (Cil.fkind * Cil.exp)
26+
| Atan2 of (Cil.fkind * Cil.exp * Cil.exp)
27+
| Cos of (Cil.fkind * Cil.exp)
28+
| Sin of (Cil.fkind * Cil.exp)
29+
| Tan of (Cil.fkind * Cil.exp)
30+
1431
(** Type of special function, or {!Unknown}. *)
1532
(* Use inline record if not single {!Cil.exp} argument. *)
1633
type special =
@@ -23,6 +40,7 @@ type special =
2340
| ThreadCreate of { thread: Cil.exp; start_routine: Cil.exp; arg: Cil.exp; }
2441
| ThreadJoin of { thread: Cil.exp; ret_var: Cil.exp; }
2542
| ThreadExit of { ret_val: Cil.exp; }
43+
| Math of { fun_args: math; }
2644
| Memset of { dest: Cil.exp; ch: Cil.exp; count: Cil.exp; }
2745
| Bzero of { dest: Cil.exp; count: Cil.exp; }
2846
| Abort

‎src/analyses/libraryFunctions.ml‎

Lines changed: 227 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,55 @@ let zstd_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
5959
("ZSTD_customFree", unknown [drop "ptr" [f]; drop "customMem" [r]]);
6060
]
6161

62+
(** math functions.
63+
Functions and builtin versions of function and macros defined in math.h. *)
64+
let math_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
65+
("__builtin_nan", special [__ "str" []] @@ fun str -> Math { fun_args = (Nan (FDouble, str)) });
66+
("__builtin_nanf", special [__ "str" []] @@ fun str -> Math { fun_args = (Nan (FFloat, str)) });
67+
("__builtin_nanl", special [__ "str" []] @@ fun str -> Math { fun_args = (Nan (FLongDouble, str)) });
68+
("__builtin_inf", special [] @@ Math { fun_args = Inf FDouble});
69+
("__builtin_inff", special [] @@ Math { fun_args = Inf FFloat});
70+
("__builtin_infl", special [] @@ Math { fun_args = Inf FLongDouble});
71+
("__builtin_isfinite", special [__ "x" []] @@ fun x -> Math { fun_args = (Isfinite x) });
72+
("__builtin_isinf", special [__ "x" []] @@ fun x -> Math { fun_args = (Isinf x) });
73+
("__builtin_isinf_sign", special [__ "x" []] @@ fun x -> Math { fun_args = (Isinf x) });
74+
("__builtin_isnan", special [__ "x" []] @@ fun x -> Math { fun_args = (Isnan x) });
75+
("__builtin_isnormal", special [__ "x" []] @@ fun x -> Math { fun_args = (Isnormal x) });
76+
("__builtin_signbit", special [__ "x" []] @@ fun x -> Math { fun_args = (Signbit x) });
77+
("__builtin_fabs", special [__ "x" []] @@ fun x -> Math { fun_args = (Fabs (FDouble, x)) });
78+
("fabs", special [__ "x" []] @@ fun x -> Math { fun_args = (Fabs (FDouble, x)) });
79+
("fabsf", special [__ "x" []] @@ fun x -> Math { fun_args = (Fabs (FFloat, x)) });
80+
("fabsl", special [__ "x" []] @@ fun x -> Math { fun_args = (Fabs (FLongDouble, x)) });
81+
("__builtin_acos", special [__ "x" []] @@ fun x -> Math { fun_args = (Acos (FDouble, x)) });
82+
("acos", special [__ "x" []] @@ fun x -> Math { fun_args = (Acos (FDouble, x)) });
83+
("acosf", special [__ "x" []] @@ fun x -> Math { fun_args = (Acos (FFloat, x)) });
84+
("acosl", special [__ "x" []] @@ fun x -> Math { fun_args = (Acos (FLongDouble, x)) });
85+
("__builtin_asin", special [__ "x" []] @@ fun x -> Math { fun_args = (Asin (FDouble, x)) });
86+
("asin", special [__ "x" []] @@ fun x -> Math { fun_args = (Asin (FDouble, x)) });
87+
("asinf", special [__ "x" []] @@ fun x -> Math { fun_args = (Asin (FFloat, x)) });
88+
("asinl", special [__ "x" []] @@ fun x -> Math { fun_args = (Asin (FLongDouble, x)) });
89+
("__builtin_atan", special [__ "x" []] @@ fun x -> Math { fun_args = (Atan (FDouble, x)) });
90+
("atan", special [__ "x" []] @@ fun x -> Math { fun_args = (Atan (FDouble, x)) });
91+
("atanf", special [__ "x" []] @@ fun x -> Math { fun_args = (Atan (FFloat, x)) });
92+
("atanl", special [__ "x" []] @@ fun x -> Math { fun_args = (Atan (FLongDouble, x)) });
93+
("__builtin_atan2", special [__ "y" []; __ "x" []] @@ fun y x -> Math { fun_args = (Atan2 (FDouble, y, x)) });
94+
("atan2", special [__ "y" []; __ "x" []] @@ fun y x -> Math { fun_args = (Atan2 (FDouble, y, x)) });
95+
("atan2f", special [__ "y" []; __ "x" []] @@ fun y x -> Math { fun_args = (Atan2 (FFloat, y, x)) });
96+
("atan2l", special [__ "y" []; __ "x" []] @@ fun y x -> Math { fun_args = (Atan2 (FLongDouble, y, x)) });
97+
("__builtin_cos", special [__ "x" []] @@ fun x -> Math { fun_args = (Cos (FDouble, x)) });
98+
("cos", special [__ "x" []] @@ fun x -> Math { fun_args = (Cos (FDouble, x)) });
99+
("cosf", special [__ "x" []] @@ fun x -> Math { fun_args = (Cos (FFloat, x)) });
100+
("cosl", special [__ "x" []] @@ fun x -> Math { fun_args = (Cos (FLongDouble, x)) });
101+
("__builtin_sin", special [__ "x" []] @@ fun x -> Math { fun_args = (Sin (FDouble, x)) });
102+
("sin", special [__ "x" []] @@ fun x -> Math { fun_args = (Sin (FDouble, x)) });
103+
("sinf", special [__ "x" []] @@ fun x -> Math { fun_args = (Sin (FFloat, x)) });
104+
("sinl", special [__ "x" []] @@ fun x -> Math { fun_args = (Sin (FLongDouble, x)) });
105+
("__builtin_tan", special [__ "x" []] @@ fun x -> Math { fun_args = (Tan (FDouble, x)) });
106+
("tan", special [__ "x" []] @@ fun x -> Math { fun_args = (Tan (FDouble, x)) });
107+
("tanf", special [__ "x" []] @@ fun x -> Math { fun_args = (Tan (FFloat, x)) });
108+
("tanl", special [__ "x" []] @@ fun x -> Math { fun_args = (Tan (FLongDouble, x)) });
109+
]
110+
62111
(* TODO: allow selecting which lists to use *)
63112
let library_descs = Hashtbl.of_list (List.concat [
64113
c_descs_list;
@@ -68,6 +117,7 @@ let library_descs = Hashtbl.of_list (List.concat [
68117
linux_descs_list;
69118
goblint_descs_list;
70119
zstd_descs_list;
120+
math_descs_list;
71121
])
72122

73123

@@ -543,6 +593,183 @@ let invalidate_actions = [
543593
"sema_init", readsAll;
544594
"down_trylock", readsAll;
545595
"up", readsAll;
596+
"acos", readsAll;
597+
"acosf", readsAll;
598+
"acosh", readsAll;
599+
"acoshf", readsAll;
600+
"acoshl", readsAll;
601+
"acosl", readsAll;
602+
"asin", readsAll;
603+
"asinf", readsAll;
604+
"asinh", readsAll;
605+
"asinhf", readsAll;
606+
"asinhl", readsAll;
607+
"asinl", readsAll;
608+
"atan", readsAll;
609+
"atan2", readsAll;
610+
"atan2f", readsAll;
611+
"atan2l", readsAll;
612+
"atanf", readsAll;
613+
"atanh", readsAll;
614+
"atanhf", readsAll;
615+
"atanhl", readsAll;
616+
"atanl", readsAll;
617+
"cbrt", readsAll;
618+
"cbrtf", readsAll;
619+
"cbrtl", readsAll;
620+
"ceil", readsAll;
621+
"ceilf", readsAll;
622+
"ceill", readsAll;
623+
"copysign", readsAll;
624+
"copysignf", readsAll;
625+
"copysignl", readsAll;
626+
"cos", readsAll;
627+
"cosf", readsAll;
628+
"cosh", readsAll;
629+
"coshf", readsAll;
630+
"coshl", readsAll;
631+
"cosl", readsAll;
632+
"erf", readsAll;
633+
"erfc", readsAll;
634+
"erfcf", readsAll;
635+
"erfcl", readsAll;
636+
"erff", readsAll;
637+
"erfl", readsAll;
638+
"exp", readsAll;
639+
"exp2", readsAll;
640+
"exp2f", readsAll;
641+
"exp2l", readsAll;
642+
"expf", readsAll;
643+
"expl", readsAll;
644+
"expm1", readsAll;
645+
"expm1f", readsAll;
646+
"expm1l", readsAll;
647+
"fabs", readsAll;
648+
"fabsf", readsAll;
649+
"fabsl", readsAll;
650+
"fdim", readsAll;
651+
"fdimf", readsAll;
652+
"fdiml", readsAll;
653+
"floor", readsAll;
654+
"floorf", readsAll;
655+
"floorl", readsAll;
656+
"fma", readsAll;
657+
"fmaf", readsAll;
658+
"fmal", readsAll;
659+
"fmax", readsAll;
660+
"fmaxf", readsAll;
661+
"fmaxl", readsAll;
662+
"fmin", readsAll;
663+
"fminf", readsAll;
664+
"fminl", readsAll;
665+
"fmod", readsAll;
666+
"fmodf", readsAll;
667+
"fmodl", readsAll;
668+
"frexp", readsAll;
669+
"frexpf", readsAll;
670+
"frexpl", readsAll;
671+
"hypot", readsAll;
672+
"hypotf", readsAll;
673+
"hypotl", readsAll;
674+
"ilogb", readsAll;
675+
"ilogbf", readsAll;
676+
"ilogbl", readsAll;
677+
"j0", readsAll;
678+
"j1", readsAll;
679+
"jn", readsAll;
680+
"ldexp", readsAll;
681+
"ldexpf", readsAll;
682+
"ldexpl", readsAll;
683+
"lgamma", readsAll;
684+
"lgammaf", readsAll;
685+
"lgammal", readsAll;
686+
"llrint", readsAll;
687+
"llrintf", readsAll;
688+
"llrintl", readsAll;
689+
"llround", readsAll;
690+
"llroundf", readsAll;
691+
"llroundl", readsAll;
692+
"log", readsAll;
693+
"log10", readsAll;
694+
"log10f", readsAll;
695+
"log10l", readsAll;
696+
"log1p", readsAll;
697+
"log1pf", readsAll;
698+
"log1pl", readsAll;
699+
"log2", readsAll;
700+
"log2f", readsAll;
701+
"log2l", readsAll;
702+
"logb", readsAll;
703+
"logbf", readsAll;
704+
"logbl", readsAll;
705+
"logf", readsAll;
706+
"logl", readsAll;
707+
"lrint", readsAll;
708+
"lrintf", readsAll;
709+
"lrintl", readsAll;
710+
"lround", readsAll;
711+
"lroundf", readsAll;
712+
"lroundl", readsAll;
713+
"modf", readsAll;
714+
"modff", readsAll;
715+
"modfl", readsAll;
716+
"nan", readsAll;
717+
"nanf", readsAll;
718+
"nanl", readsAll;
719+
"nearbyint", readsAll;
720+
"nearbyintf", readsAll;
721+
"nearbyintl", readsAll;
722+
"nextafter", readsAll;
723+
"nextafterf", readsAll;
724+
"nextafterl", readsAll;
725+
"nexttoward", readsAll;
726+
"nexttowardf", readsAll;
727+
"nexttowardl", readsAll;
728+
"pow", readsAll;
729+
"powf", readsAll;
730+
"powl", readsAll;
731+
"remainder", readsAll;
732+
"remainderf", readsAll;
733+
"remainderl", readsAll;
734+
"remquo", readsAll;
735+
"remquof", readsAll;
736+
"remquol", readsAll;
737+
"rint", readsAll;
738+
"rintf", readsAll;
739+
"rintl", readsAll;
740+
"round", readsAll;
741+
"roundf", readsAll;
742+
"roundl", readsAll;
743+
"scalbln", readsAll;
744+
"scalblnf", readsAll;
745+
"scalblnl", readsAll;
746+
"scalbn", readsAll;
747+
"scalbnf", readsAll;
748+
"scalbnl", readsAll;
749+
"sin", readsAll;
750+
"sinf", readsAll;
751+
"sinh", readsAll;
752+
"sinhf", readsAll;
753+
"sinhl", readsAll;
754+
"sinl", readsAll;
755+
"sqrt", readsAll;
756+
"sqrtf", readsAll;
757+
"sqrtl", readsAll;
758+
"tan", readsAll;
759+
"tanf", readsAll;
760+
"tanh", readsAll;
761+
"tanhf", readsAll;
762+
"tanhl", readsAll;
763+
"tanl", readsAll;
764+
"tgamma", readsAll;
765+
"tgammaf", readsAll;
766+
"tgammal", readsAll;
767+
"trunc", readsAll;
768+
"truncf", readsAll;
769+
"truncl", readsAll;
770+
"y0", readsAll;
771+
"y1", readsAll;
772+
"yn", readsAll;
546773
]
547774

548775

0 commit comments

Comments
 (0)