Fix Z3 function calls regarding arithmetic operations

[bruntib]

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.

[martong]

LGTM!

[steakhal]

It's a huge copy-paste bug. Great job tracking this down.

I've checked several other Z3 API calls with more than 2 arguments.
They all seem to match the API specification.

[steakhal]

llvm/lib/Support/Z3Solver.cpp

257–270

Should we replace the std::set to a more performant data structure?
https://llvm.org/docs/ProgrammersManual.html#set

[martong]

llvm/lib/Support/Z3Solver.cpp

257–270

Do you have any measurements that indicate std::set functions as hotspots? If not, then it is probably not worth the effort...

llvm/lib/Support/Z3Solver.cpp

return (llvm::APFloat::semanticsPrecision(LHS) ==
          (llvm::APFloat::semanticsMinExponent(LHS) ==
           llvm::APFloat::semanticsMinExponent(RHS)) &&
          (llvm::APFloat::semanticsMaxExponent(LHS) ==
           llvm::APFloat::semanticsMaxExponent(RHS)) &&
          (llvm::APFloat::semanticsSizeInBits(LHS) ==
           llvm::APFloat::semanticsSizeInBits(RHS));
 }
 
 class Z3Solver : public SMTSolver {
   friend class Z3ConstraintManager;
 
   Z3Context Context;
 
   Z3_solver Solver;
 
   // Cache Sorts
   std::set<Z3Sort> CachedSorts;
 
   // Cache Exprs
   std::set<Z3Expr> CachedExprs;
 
 public:
   Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) {
     Z3_solver_inc_ref(Context.Context, Solver);
   }
 
   Z3Solver(const Z3Solver &Other) = delete;
   Z3Solver(Z3Solver &&Other) = delete;
   Z3Solver &operator=(Z3Solver &Other) = delete;
   Z3Solver &operator=(Z3Solver &&Other) = delete;
SMTExprRef mkFPIsZero(const SMTExprRef &Exp) override {
     return newExprRef(Z3Expr(
         Context, Z3_mk_fpa_is_zero(Context.Context, toZ3Expr(*Exp).AST)));
   }
 
   SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
     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 {
     return newExprRef(
         Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST,
                                       toZ3Expr(*RHS).AST)));
   }
 
   SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
     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 {
     return newExprRef(
         Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST,
                                      toZ3Expr(*RHS).AST)));
   }