Fix issues around Z3 sorts and floating-point flags.

[Zeta611]

Description

1. Properly set the floating-point flag when get_as_numeric_z3_ast meets the Expression::Transmute case, by checking the target_type and dispatching to get_as_numeric_z3_ast.
2. Fix the Z3 sort of the return type to be BitVector, not Boolean, in bv_overflows.

Fixes #1252.

Type of change

• Bug fix (non-breaking change which fixes an issue)
• New feature (non-breaking change which adds functionality)
• Breaking change (fix or feature that would cause existing functionality to not work as expected)
• API change with a documentation update
• Additional test coverage
• Code cleanup or just keeping up with the latest Rustc nightly

How Has This Been Tested?

Analyzing libm failed previously. Now it works.

Checklist:

I have run validate.sh.

• Fork the repo and create your branch from main.
• If you've added code that should be tested, add tests.
• If you've changed APIs, update the documentation.
• Ensure the test suite passes.
• Make sure your code lints.
• If you haven't already, complete your CLA here: https://code.facebook.com/cla

[codecov]

Codecov Report

Attention: 5 lines in your changes are missing coverage. Please review.

Comparison is base (a23ff7e) 74% compared to head (e49cedd) 74%.

Files	Patch %	Lines
checker/src/z3_solver.rs	37%	5 Missing ⚠️

Additional details and impacted files

@@          Coverage Diff          @@
##            main   #1253   +/-   ##
=====================================
- Coverage     74%     74%   -1%     
=====================================
  Files         23      23           
  Lines      16795   16800    +5     
=====================================
- Hits       12592   12587    -5     
- Misses      4203    4213   +10     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[hermanventer]

numeric_cast has logic for target_type == ExpressionType::Char, so it probably makes sense to use it for that case as well. I can imagine that transmuting a bit vector to a char might just happen somewhere, someday.

[Zeta611]

Are you implying that simply dispatching to numeric_cast would be enough in the case of Transmute, without the conditional to fall back to get_as_numeric_z3_ast? I can see that it will fall back to get_as_numeric_z3_ast anyways. If you confirm, I will make a new commit.

[hermanventer]

You'll still need the fall back. The idea would be to also use numeric_cast only in the case where target_type == ExpressionType::Char. I imagine that it might be interesting to write a test case for this.

[Zeta611]

But if I add Char type test like:

Expression::Transmute { operand, target_type } => {
    if target_type.is_integer() || target_type.is_floating_point_number() || target_type == ExpressionType::Char {
        self.numeric_cast(&operand.expression, *target_type)
    } else {
        self.get_as_numeric_z3_ast(&operand.expression)
    }
}

it would be the same as

Expression::Transmute { operand, target_type } => self.numeric_cast(&operand.expression, *target_type),

because numeric_cast basically falls back to calling get_as_numeric_z3_ast internally.

Or perhaps I misunderstood your intent!

[hermanventer]

Never mind then. I'll look into this separately when I get a chance.

[hermanventer]

Thanks for doing this!