[all-commits] [llvm/llvm-project] 5fc05c: Fix Z3 function calls regarding arithmetic operations

[Gabor Marton via All-commits]

  Branch: refs/heads/master
  Home:   https://github.com/llvm/llvm-project
  Commit: 5fc05c376a3cc0fb9a532e41d12e51f3d9916692
      https://github.com/llvm/llvm-project/commit/5fc05c376a3cc0fb9a532e41d12e51f3d9916692
  Author: Gabor Marton <gabor.marton at ericsson.com>
  Date:   2020-05-14 (Thu, 14 May 2020)

  Changed paths:
    M llvm/lib/Support/Z3Solver.cpp

  Log Message:
  -----------
  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!