Interval Analysis for Floating-point values #761

Dudeldu · 2022-06-16T10:58:48Z

Adds basic interval analysis for float and double values (Related to Issue: #734)

We implemented an interval analysis for floating-point values. In order to capture operations leading to unrepresentable values and their rounding mode dependent representations in the concrete execution, all abstract operations overestimate the worst case interval by using the rounding mode that creates the largest possible interval on both bounds.

Introduces following settings:

ana.float.interval : Enables the float interval domain (default: disabled)
- arithmetic operations on floats (+, -, *, /)
- casts between ints and floats (and vice versa)
- builtins for is_nan, is_normal, is_finite, sign, is_inf (although we can not use the captured information for more precise information inside branching)
- abstractions for different math functions like cos, tan, sin ,...
__attribute__((goblint_precision("no-float-interval"))): to disable/enable the float domain on a node/function level
warn.float: Adds warnings related to the analysis results (default: enabled)
- warn on equality/inequality check on floats
- warn on operations done on values that could be +/- Infinity or NaN
- warn in places where where loos track of the exact information (the point where the interval no longer only contains one value)

* add some implementation for the "norm" method in FloatDomain, however at the moment incorrect Now, the norm method is called at eval_binop and successfully fails, which currently is wanted like this, just to test that it works. We need to change it now s.t. it prints a warning instead of an error. * Rework norm slightly s.t. it uses set_overflow_flag now, which however is still incorrect * Add FloatMessage message category in messageCategory.ml Also add it in options.schema.json * Add a todo note for later in sarifRules.ml * Add a regression test for float that expects a warning for division by zeron / infinity * Clean up floatDomain.ml slightly: Remove TODOs/FIXMEs and inline message warning * Fix regression test naming and merge them together * Remove FloatMessage module in messageCategory.ml, as it's not needed anymore * Remove todo message * Remove todo message * Remove todo comments and/or clean up some stuff * Clean up float domain etc. with fixes from PR - Better warning message - use is_top function instead of checking for None in the domain - revert unrelated change - make 'warn.float' option not a default option - make regression test as minimal as possible * In floatDomain.ml, rearrange of_const function s.t. it finds the norm function * Add float warning parameter to 03-infinity_or_nan.c regression test

)

- lattice related functions (leq, widen, narrow, join, meet) - arithmetic operations (add, sub, mul, div) - casts (f2i, i2f)

* Support FFloat and FDouble - Implement float operators in C - Support FFloat and FDouble * Allow using DBL_MIN, DBL_MAX Some compilers specifiy DBL_MIN, DBL_MAX as long double. As we do not support long double in neither cil nor goblint itself, but want to use DBL_MIN, DBL_MAX, we have no other option than to explicitly check for this two cases

michael-schwarz · 2022-06-17T09:35:23Z

Nice, thanks for the PR! 🚀 I hope to find some time to review it this weekend!

I resolved the merge conflicts on the benchmarking machine, and started a run of all of sv-comp on that machine (2min timeout). I'll send you the results on slack.
I guess in the meanwhile, it would make sense to keep merging the upstream master into yours from time-to-time so they don't diverge too much. (nothing fancy like rebasing needed, we do this with our branches all the time as well).

jerhard · 2022-07-14T11:53:50Z

The missing content is due to the float domain being disabled at that point. Therefore we have nothing to show. This should be the exact same behaviour as if you disable all integer domains with --disable ana.int.def_exc

Ah, indeed I did not notice that.

* Find another location where get_ikind results in an error * Further refine determining safe casts with floats

Merge remote

michael-schwarz

Looks good to be merged from my perspective! Any more comments @sim642 @stilscher @jerhard?

src/analyses/base.ml

src/cdomains/floatDomain.ml

jerhard · 2022-07-26T11:15:39Z

src/cdomains/floatDomain.ml

+       | Interval (r1, r2) when not (is_exact result) && is_exact_before ->
+         Messages.warn
+           ~category:Messages.Category.Float
+           ~tags:[CWE 197; CWE 681; CWE 1339]


Are CWE 197 and CWE 681 really applicable for binary operations on floats?

Yes, I don't think those two really apply here either.

jerhard · 2022-07-26T11:15:56Z

src/cdomains/floatDomain.ml

+       | Top ->
+         Messages.warn
+           ~category:Messages.Category.Float
+           ~tags:[CWE 197; CWE 681; CWE 1339]


Same question as above.

Co-authored-by: Julian Erhard <[email protected]>

CHANGES: Goblint "lean" release after a lot of cleanup. * Remove unmaintained analyses: OSEK, ARINC, shapes, containment, deadlocksByRaces (goblint/analyzer#460, goblint/analyzer#736, goblint/analyzer#812, goblint/analyzer#474). * Add interactive analysis (goblint/analyzer#391). * Add server mode (goblint/analyzer#522). * Add Compilation Database support (goblint/analyzer#406, goblint/analyzer#448). * Add floating point domain, unrolled array domain and improved struct domains (goblint/analyzer#734, goblint/analyzer#761, goblint/analyzer#577, goblint/analyzer#419). * Add static loop unrolling and heap variable unrolling (goblint/analyzer#563, goblint/analyzer#722). * Improve race detection with may-happen-in-parallel analysis (goblint/analyzer#529, goblint/analyzer#518, goblint/analyzer#595). * Reimplement lockset and deadlock analyses (goblint/analyzer#659, goblint/analyzer#662, goblint/analyzer#650, goblint/analyzer#655). * Add pthread extraction to Promela (goblint/analyzer#220). * Add location spans to output (goblint/analyzer#428, goblint/analyzer#449). * Improve race reporting (goblint/analyzer#550, goblint/analyzer#551). * Improve dead code reporting (goblint/analyzer#94, goblint/analyzer#353, goblint/analyzer#785). * Refactor warnings (goblint/analyzer#55, goblint/analyzer#783). * Add JSON schema for configuration (goblint/analyzer#476, goblint/analyzer#499). * Refactor option names (goblint/analyzer#28, goblint/analyzer#192, goblint/analyzer#516, goblint/analyzer#675). * Add bash completion (goblint/analyzer#669). * Add OCaml 4.13 and 4.14 support, remove OCaml 4.09 support (goblint/analyzer#503, goblint/analyzer#672).

Dudeldu and others added 21 commits May 6, 2022 17:14

Inject dummy float domain into analysis framework

39af0cc

Implement basic functionality for covering const-propagated asserts

87a9398

Introduce new ana.float.interval option

ffd1538

Add wrapper domain for Floating point in general

8808ced

Apply different renamings and undo formatting inside FloatInterval

e11c846

Fix rename and unused import

47fd747

Add node-level configurability of float analysis

fad2037

most functionality implemented - no unittests yet, only framework!

e8c496d

fix leq and add unittests

bd1ef2a

some fixes and suggested changes

994e511

Provide cast support between int types and double

b0c6bb1

include Printable.Std for default implementation and fix sub

c6b8592

Implementation of invariant for capturing information from branching (#6

02d81db

)

Add unittests for our domain (#9)

e026bfa

- lattice related functions (leq, widen, narrow, join, meet) - arithmetic operations (add, sub, mul, div) - casts (f2i, i2f)

Add all math.h functions in libraryFunctions.ml with readsAll (#12)

1b96fe4

implemented float classification functions from math.h (#14)

82c0bf4

Add further warnings (#11)

7d5b149

Fix and remove todos for our first "real" PR (#16)

6fa973a

reorder test ids in float regression tests (#17)

449ce45

sim642 self-requested a review June 16, 2022 11:18

sim642 added feature precision labels Jun 16, 2022

Merge remote-tracking branch 'base-repo/master'

e956617

michael-schwarz self-requested a review June 16, 2022 11:48

michael-schwarz added student-job practical-course Practical Course at TUM sv-comp SV-COMP (analyses, results), witnesses labels Jun 16, 2022

include missing asserts in regressiontests (#39)

8c9769c

add fabs and builtin inf/nan (#40)

d660e4e

FelixKrayer removed their assignment Jul 18, 2022

Dudeldu added 4 commits July 19, 2022 12:47

Find another location where get_ikind results in an error (#41)

d31be72

* Find another location where get_ikind results in an error * Further refine determining safe casts with floats

Improve narrowing by introducing additional step (#42)

380ec34

Merge remote-tracking branch 'base-repo/master'

2f116a6

Merge pull request #44 from Dudeldu/merge-remote

47c0070

Merge remote

michael-schwarz approved these changes Jul 25, 2022

View reviewed changes

sim642 self-requested a review July 25, 2022 17:55

sim642 approved these changes Jul 26, 2022

View reviewed changes

jerhard self-requested a review July 26, 2022 09:25

jerhard reviewed Jul 26, 2022

View reviewed changes

src/analyses/base.ml Outdated Show resolved Hide resolved

jerhard reviewed Jul 26, 2022

View reviewed changes

michael-schwarz and others added 10 commits July 26, 2022 13:35

Fix typo

437ec6e

Co-authored-by: Julian Erhard <[email protected]>

Modify test 57/12 to actually trigger the issue

c6a31b6

Whitespace

c21875d

Add unsoundness example

84d5ca5

Typo

93d6f91

Fix unsoundness with floats in branches by going to top for those cases

1600513

Refine branching on floats for negative case

5830912

Typos & rename first invariant in base.ml to invariant_fallback

9dcb3b5

Typos in floatDomain.ml

e9589fb

Remove CWEs from operations where they don't really apply

08a624d

michael-schwarz merged commit cfab02b into goblint:master Jul 27, 2022

michael-schwarz mentioned this pull request Jul 27, 2022

Interval Analysis for Floating-point values #734

Closed

sim642 mentioned this pull request Aug 18, 2022

[new release] goblint (2.0.0) ocaml/opam-repository#21998

Merged

sim642 mentioned this pull request Aug 19, 2022

Float domain tests fail on arm64 #824

Closed

5 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Interval Analysis for Floating-point values #761

Interval Analysis for Floating-point values #761

Dudeldu commented Jun 16, 2022 •

edited

Loading

michael-schwarz commented Jun 17, 2022

jerhard commented Jul 14, 2022 •

edited

Loading

michael-schwarz left a comment

jerhard Jul 26, 2022

michael-schwarz Jul 26, 2022

jerhard Jul 26, 2022

Interval Analysis for Floating-point values #761

Interval Analysis for Floating-point values #761

Conversation

Dudeldu commented Jun 16, 2022 • edited Loading

michael-schwarz commented Jun 17, 2022

jerhard commented Jul 14, 2022 • edited Loading

michael-schwarz left a comment

Choose a reason for hiding this comment

jerhard Jul 26, 2022

Choose a reason for hiding this comment

michael-schwarz Jul 26, 2022

Choose a reason for hiding this comment

jerhard Jul 26, 2022

Choose a reason for hiding this comment

Dudeldu commented Jun 16, 2022 •

edited

Loading

jerhard commented Jul 14, 2022 •

edited

Loading