search

ultimate-pa / ultimate

The Ultimate program analysis framework.
https://ultimate-pa.org/
200 stars 41 forks source link

Rework BitabsTranslation #607

Closed schuessf closed 1 year ago

schuessf commented 1 year ago

This PR reworks the existing BitabsTranslation (overapproximates bitwise operations in the integer-translation) completely, s.t. we always return an ExpressionResult (that introduces aux-vars and multiple statements) and do not require a workaround to handle assignments more precicesly. Therefore we had to change multiple methods that call the BitabsTranslation, s.t. they also return an ExpressionResult.

The diff might look more complicated than it has to. The most important commits are ecce1366fa99a80b234420aaca73e4192988e416 (implements the the variant of the BitabsTranslation) and f746bc6f731c3a251e3acde65a0ff7162b900684 (integrates it propertly).

schuessf commented 1 year ago

The nightly build seems fine:

Compared the latest nightly build #2 with the build #361 of the reference branch.

The following 4 tests failed:

schuessf commented 1 year ago

Compared the latest nightly build #3 with the build #364 of the reference branch.

The following 4 tests failed:

schuessf commented 1 year ago

The latest nightly looks good. Only one test (BugLiveVariables03-Safe.bpl) failed, but that seems flaky. It also failed on dev a few builds ago.

On the other this PR fixes some tests with bitwise operations (Bitvector-Safe.c, BitwiseOperations01.c), since we now have a more precise overapproximation.

So I will now merge this.