Skip to content
This repository has been archived by the owner on Aug 22, 2024. It is now read-only.

Fix issues around Z3 sorts and floating-point flags. #1253

Merged
merged 2 commits into from
Nov 19, 2023
Merged

Fix issues around Z3 sorts and floating-point flags. #1253

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
51eb521
Treat numeric transmute specially
Zeta611 Nov 17, 2023
e49cedd
Fix the return type of `bv_overflows` to be of sort BitVector
Zeta611 Nov 18, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 11 additions & 4 deletions checker/src/z3_solver.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1139,8 +1139,12 @@
Expression::TaggedExpression { operand, .. } => {
self.get_as_numeric_z3_ast(&operand.expression)
}
Expression::Transmute { operand, .. } => {
self.get_as_numeric_z3_ast(&operand.expression)
Expression::Transmute { operand, target_type } => {
if target_type.is_integer() || target_type.is_floating_point_number() {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

@Zeta611 Zeta611 Nov 19, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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!

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

self.numeric_cast(&operand.expression, *target_type)
} else {
self.get_as_numeric_z3_ast(&operand.expression)

Check warning on line 1146 in checker/src/z3_solver.rs

View check run for this annotation

Codecov / codecov/patch

checker/src/z3_solver.rs#L1146 

Added line #L1146 was not covered by tests
}
}
Expression::Top | Expression::Bottom => unsafe {
(
Expand Down Expand Up @@ -1948,14 +1952,17 @@
let right_bv = self.get_as_bv_z3_ast(&right.expression, num_bits);
unsafe {
let does_not_overflow = no_overflow(self.z3_context, left_bv, right_bv, is_signed);
if is_signed {
let overflows = if is_signed {

Check warning on line 1955 in checker/src/z3_solver.rs

View check run for this annotation

Codecov / codecov/patch

checker/src/z3_solver.rs#L1955 

Added line #L1955 was not covered by tests
let does_not_underflow = no_underflow(self.z3_context, left_bv, right_bv);
let tmp = vec![does_not_overflow, does_not_underflow];
let stays_in_range = z3_sys::Z3_mk_and(self.z3_context, 2, tmp.as_ptr());
z3_sys::Z3_mk_not(self.z3_context, stays_in_range)
} else {
z3_sys::Z3_mk_not(self.z3_context, does_not_overflow)
}
};
let bv_true = self.bv_constant(num_bits, &ConstantDomain::True);
let bv_false = self.bv_constant(num_bits, &ConstantDomain::False);
z3_sys::Z3_mk_ite(self.z3_context, overflows, bv_true, bv_false)

Check warning on line 1965 in checker/src/z3_solver.rs

View check run for this annotation

Codecov / codecov/patch

checker/src/z3_solver.rs#L1963-L1965 

Added lines #L1963 - L1965 were not covered by tests
}
}

Expand Down