[PATCH] D79883: Fix Z3 function calls regarding arithmetic operations

[Tibor Brunner via Phabricator via llvm-commits]

bruntib created this revision.
bruntib added reviewers: Szelethus, xazax.hun, baloghadamsoftware.
bruntib added a project: LLVM.
Herald added subscribers: llvm-commits, martong, mikhail.ramalho, rnkovacs, hiraditya.
bruntib added a reviewer: steakhal.
bruntib added reviewers: martong, mikhail.ramalho.

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.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D79883

Files:
  llvm/lib/Support/Z3Solver.cpp


Index: llvm/lib/Support/Z3Solver.cpp
===================================================================
--- llvm/lib/Support/Z3Solver.cpp
+++ llvm/lib/Support/Z3Solver.cpp
@@ -516,16 +516,16 @@
     SMTExprRef RoundingMode = getFloatRoundingMode();
     return newExprRef(
         Z3Expr(Context,
-               Z3_mk_fpa_mul(Context.Context, toZ3Expr(*LHS).AST,
-                             toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
+               Z3_mk_fpa_mul(Context.Context, toZ3Expr(*RoundingMode).AST,
+                             toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
   }
 
   SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
     SMTExprRef RoundingMode = getFloatRoundingMode();
     return newExprRef(
         Z3Expr(Context,
-               Z3_mk_fpa_div(Context.Context, toZ3Expr(*LHS).AST,
-                             toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
+               Z3_mk_fpa_div(Context.Context, toZ3Expr(*RoundingMode).AST,
+                             toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
   }
 
   SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
@@ -538,16 +538,16 @@
     SMTExprRef RoundingMode = getFloatRoundingMode();
     return newExprRef(
         Z3Expr(Context,
-               Z3_mk_fpa_add(Context.Context, toZ3Expr(*LHS).AST,
-                             toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
+               Z3_mk_fpa_add(Context.Context, toZ3Expr(*RoundingMode).AST,
+                             toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
   }
 
   SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
     SMTExprRef RoundingMode = getFloatRoundingMode();
     return newExprRef(
         Z3Expr(Context,
-               Z3_mk_fpa_sub(Context.Context, toZ3Expr(*LHS).AST,
-                             toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
+               Z3_mk_fpa_sub(Context.Context, toZ3Expr(*RoundingMode).AST,
+                             toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
   }
 
   SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D79883.263750.patch
Type: text/x-patch
Size: 2168 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20200513/c67a853f/attachment.bin>