Skip to content

Commit 5fc05c3

Browse files
author
Gabor Marton
committed
Fix Z3 function calls regarding arithmetic operations
Summary: The order of Z3_mk_fpa_mul, Z3_mk_fpa_div, Z3_mk_fpa_add and Z3_mk_fpa_sub functions' arguments is: context, rounding_mode, ast1, ast2. See for example: https://github.com/Z3Prover/z3/blob/a14c2a30516003cd1a60f8b7deca029033d11c78/src/api/api_fpa.cpp#L433 At function calls from LLVM the argument order was different: rounding_mode was passed as last argument. Unfortunately these Z3_ast and other function parameter types are technically like void* which are reinterpret_cast-ed to a specific class type. So there was no type error, but the assertions fail in runtime if something goes wrong. Such a crash happened during Z3 refutation while using StaticAnalyzer. Reviewers: Szelethus, xazax.hun, baloghadamsoftware, steakhal, martong, mikhail.ramalho Reviewed By: martong Subscribers: hiraditya, rnkovacs, mikhail.ramalho, martong, llvm-commits Tags: #llvm Differential Revision: https://reviews.llvm.org/D79883 Patch by Tibor Brunner!
1 parent ff4492c commit 5fc05c3

File tree

1 file changed

+8
-8
lines changed

1 file changed

+8
-8
lines changed

llvm/lib/Support/Z3Solver.cpp

+8-8
Original file line numberDiff line numberDiff line change
@@ -516,16 +516,16 @@ class Z3Solver : public SMTSolver {
516516
SMTExprRef RoundingMode = getFloatRoundingMode();
517517
return newExprRef(
518518
Z3Expr(Context,
519-
Z3_mk_fpa_mul(Context.Context, toZ3Expr(*LHS).AST,
520-
toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
519+
Z3_mk_fpa_mul(Context.Context, toZ3Expr(*RoundingMode).AST,
520+
toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
521521
}
522522

523523
SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
524524
SMTExprRef RoundingMode = getFloatRoundingMode();
525525
return newExprRef(
526526
Z3Expr(Context,
527-
Z3_mk_fpa_div(Context.Context, toZ3Expr(*LHS).AST,
528-
toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
527+
Z3_mk_fpa_div(Context.Context, toZ3Expr(*RoundingMode).AST,
528+
toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
529529
}
530530

531531
SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
@@ -538,16 +538,16 @@ class Z3Solver : public SMTSolver {
538538
SMTExprRef RoundingMode = getFloatRoundingMode();
539539
return newExprRef(
540540
Z3Expr(Context,
541-
Z3_mk_fpa_add(Context.Context, toZ3Expr(*LHS).AST,
542-
toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
541+
Z3_mk_fpa_add(Context.Context, toZ3Expr(*RoundingMode).AST,
542+
toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
543543
}
544544

545545
SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
546546
SMTExprRef RoundingMode = getFloatRoundingMode();
547547
return newExprRef(
548548
Z3Expr(Context,
549-
Z3_mk_fpa_sub(Context.Context, toZ3Expr(*LHS).AST,
550-
toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
549+
Z3_mk_fpa_sub(Context.Context, toZ3Expr(*RoundingMode).AST,
550+
toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
551551
}
552552

553553
SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {

0 commit comments

Comments
 (0)