This is an archive of the discontinued LLVM Phabricator instance.

[analyzer] Fixed method to get APSInt model
ClosedPublic

Authored by mikhail.ramalho on Jul 25 2018, 1:06 PM.

Details

Summary

This patch replaces the current method of getting an APSInt from Z3's model by calling generic API method getBitvector instead of Z3_get_numeral_uint64.

By calling getBitvector, there's no need to handle bitvectors with bit width == 128 separately.

And, as a bonus, clang now compiles correctly with Z3 4.7.1.

Diff Detail

Event Timeline

george.karpenkov requested changes to this revision.Jul 25 2018, 2:05 PM

requesting clarification

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
737–741

should const be dropped from signature?

818–827

what is this branch doing? What's special about bitvector sort size <= 64 or exactly 128?

This revision now requires changes to proceed.Jul 25 2018, 2:05 PM
lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
737–741

On the function where getBitvector is called (get interpretation), the value is assigned to a llvm::APSInt. I removed it so we don't an error that const was dropped.

818–827

This function is also used to retrieve floating-point values, which can be 16, 32, 64 or 128 bits long. Bitvectors can be anything between 1 and 64 bits long.

In the future, we need proper calls in the backend to retrieve floating-points and its special values (NaN, +/-infinity, +/-zero), then we can drop this weird condition. I didn't implement them because the floating-point part of the backend is not being used.

george.karpenkov accepted this revision.Jul 25 2018, 2:39 PM

LGTM, but could you also add the response you have written regarding 128/<=64 bits objects as a comment.

This revision is now accepted and ready to land.Jul 25 2018, 2:39 PM

Added a comment explaining why we have a weird if condition in toAPSInt.

This revision was automatically updated to reflect the committed changes.