AbsInt Failure Notices: aiT/StackAnalyzer/TimeWeaver/ValueAnalyzer

Failure notice #27077 and #27370 for aiT/StackAnalyzer/TimeWeaver/ValueAnalyzer.

The reported issues will be fixed with the 19.10 release.

[Failure Notice #27077]

Problem Description:

—————————

The value analysis doesn’t invalidate enough information in its memory domain for misaligned unknown accesses if either

1) For 64-bit target architectures:

The analysis computes an access of a width large enough to let it wrap around the 0xffffffffffffffff border.

2) For all target architectures:

The analysis computes an access with a wrapped interval that wraps around and the access width is larger than the gap.

Scenario:

———

Only analysis runs are affected that contain misaligned unknown memory accesses.

Example to trigger issue 1)

The analysis computes an access range of [0x0..0xffffffffffffffff] for a two byte wide access

Example to trigger issue 2)

The analysis computes an access range of [0x0..0x3, 0x5..0xffffffffffffffff] for a two byte wide access

Symptoms:

———

Some information in the memory domain is not updated correctly. This can lead to e.g. some paths are considered infeasible while they are feasible or some value ranges are too small.

Affected versions:

——————

Release 14.10 and newer

Troubleshooting:

——————

Upgrade to the 19.10 version or:

* One can annotate imprecise accesses with some access ranges that avoid the above wrapping/imprecision.

* One can exclude program parts with such accesses via the “snippet not analyzed” annotation.

========================================================================================================

[Failure Notice #27370]

Problem Description:

—————————

The value analysis may incorrectly truncate the value range of a register or memory cell if

1) The register or memory cell is linearly updated inside a loop (i.e., only by addition or subtraction), and 2) a type-cast like operation is applied to the register or memory cell (e.g., a truncation to the 8-bit unsigned range [0x0..0xff]), and 3) the loop is not fully unrolled.

Such a code pattern is typically not emitted by a compiler but can be constructed via e.g. inline assembly code.

Symptoms:

———

Some information in the register or memory domain is updated incorrectly. This can lead to some paths being incorrectly considered as infeasible or some value ranges that are too small.

Affected versions:

——————

Release 14.10 and newer

Troubleshooting:

——————

The problem has been fixed in version 19.10 or later.

The problem can also be circumvented by fully unrolling each affected loop.

www.absint.com

2019-10-09T15:39:50+00:00