From a2cdfce4aa68d8f6f5f659c78a1e204514004d6e Mon Sep 17 00:00:00 2001 From: Can Date: Wed, 9 Oct 2024 14:04:55 +0200 Subject: [PATCH 1/7] Add unit tests --- .../alive-tv/uf-float/add-assoc-fail.srctgt.ll | 14 ++++++++++++++ .../alive-tv/uf-float/add-comm-double.srctgt.ll | 11 +++++++++++ .../alive-tv/uf-float/add-comm-fp128.srctgt.ll | 11 +++++++++++ tests/alive-tv/uf-float/add-comm-half.srctgt.ll | 11 +++++++++++ tests/alive-tv/uf-float/add-comm-ninf.srctgt.ll | 11 +++++++++++ tests/alive-tv/uf-float/add-comm-nnan.srctgt.ll | 11 +++++++++++ tests/alive-tv/uf-float/add-comm.srctgt.ll | 11 +++++++++++ tests/alive-tv/uf-float/cmp-eq-comm.srctgt.ll | 11 +++++++++++ tests/alive-tv/uf-float/cmp-eq-ne.srctgt.ll | 12 ++++++++++++ tests/alive-tv/uf-float/cmp-lt-gt.srctgt.ll | 11 +++++++++++ tests/alive-tv/uf-float/cmp-lt-le.srctgt.ll | 12 ++++++++++++ .../uf-float/cmp-olt-ult-fail.srctgt.ll | 12 ++++++++++++ tests/alive-tv/uf-float/cmp-ord-uno.srctgt.ll | 12 ++++++++++++ tests/alive-tv/uf-float/load-bitcast.srctgt.ll | 13 +++++++++++++ tests/alive-tv/uf-float/load-store.srctgt.ll | 12 ++++++++++++ tests/alive-tv/uf-float/select.srctgt.ll | 17 +++++++++++++++++ tests/alive-tv/uf-float/vector-binop.srctgt.ll | 14 ++++++++++++++ tests/alive-tv/uf-float/vector-cmp.srctgt.ll | 14 ++++++++++++++ .../alive-tv/uf-float/vector-convert.srctgt.ll | 15 +++++++++++++++ tests/alive-tv/uf-float/vector-unop.srctgt.ll | 13 +++++++++++++ 20 files changed, 248 insertions(+) create mode 100644 tests/alive-tv/uf-float/add-assoc-fail.srctgt.ll create mode 100644 tests/alive-tv/uf-float/add-comm-double.srctgt.ll create mode 100644 tests/alive-tv/uf-float/add-comm-fp128.srctgt.ll create mode 100644 tests/alive-tv/uf-float/add-comm-half.srctgt.ll create mode 100644 tests/alive-tv/uf-float/add-comm-ninf.srctgt.ll create mode 100644 tests/alive-tv/uf-float/add-comm-nnan.srctgt.ll create mode 100644 tests/alive-tv/uf-float/add-comm.srctgt.ll create mode 100644 tests/alive-tv/uf-float/cmp-eq-comm.srctgt.ll create mode 100644 tests/alive-tv/uf-float/cmp-eq-ne.srctgt.ll create mode 100644 tests/alive-tv/uf-float/cmp-lt-gt.srctgt.ll create mode 100644 tests/alive-tv/uf-float/cmp-lt-le.srctgt.ll create mode 100644 tests/alive-tv/uf-float/cmp-olt-ult-fail.srctgt.ll create mode 100644 tests/alive-tv/uf-float/cmp-ord-uno.srctgt.ll create mode 100644 tests/alive-tv/uf-float/load-bitcast.srctgt.ll create mode 100644 tests/alive-tv/uf-float/load-store.srctgt.ll create mode 100644 tests/alive-tv/uf-float/select.srctgt.ll create mode 100644 tests/alive-tv/uf-float/vector-binop.srctgt.ll create mode 100644 tests/alive-tv/uf-float/vector-cmp.srctgt.ll create mode 100644 tests/alive-tv/uf-float/vector-convert.srctgt.ll create mode 100644 tests/alive-tv/uf-float/vector-unop.srctgt.ll diff --git a/tests/alive-tv/uf-float/add-assoc-fail.srctgt.ll b/tests/alive-tv/uf-float/add-assoc-fail.srctgt.ll new file mode 100644 index 000000000..33a3d5323 --- /dev/null +++ b/tests/alive-tv/uf-float/add-assoc-fail.srctgt.ll @@ -0,0 +1,14 @@ +; TEST-ARGS: --uf-float +; ERROR: Couldn't prove the correctness of the transformation + +define float @src(float noundef %x, float noundef %y, float noundef %z) { + %a = fadd float %x, %y + %b = fadd float %a, %z + ret float %b +} + +define float @tgt(float noundef %x, float noundef %y, float noundef %z) { + %a = fadd float %y, %z + %b = fadd float %x, %a + ret float %b +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/add-comm-double.srctgt.ll b/tests/alive-tv/uf-float/add-comm-double.srctgt.ll new file mode 100644 index 000000000..4981661a4 --- /dev/null +++ b/tests/alive-tv/uf-float/add-comm-double.srctgt.ll @@ -0,0 +1,11 @@ +; TEST-ARGS: --uf-float + +define double @src(double noundef %x, double noundef %y) { + %sum = fadd double %x, %y + ret double %sum +} + +define double @tgt(double noundef %x, double noundef %y) { + %sum = fadd double %y, %x + ret double %sum +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/add-comm-fp128.srctgt.ll b/tests/alive-tv/uf-float/add-comm-fp128.srctgt.ll new file mode 100644 index 000000000..deb6c3213 --- /dev/null +++ b/tests/alive-tv/uf-float/add-comm-fp128.srctgt.ll @@ -0,0 +1,11 @@ +; TEST-ARGS: --uf-float + +define fp128 @src(fp128 noundef %x, fp128 noundef %y) { + %sum = fadd fp128 %x, %y + ret fp128 %sum +} + +define fp128 @tgt(fp128 noundef %x, fp128 noundef %y) { + %sum = fadd fp128 %y, %x + ret fp128 %sum +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/add-comm-half.srctgt.ll b/tests/alive-tv/uf-float/add-comm-half.srctgt.ll new file mode 100644 index 000000000..731eae0d5 --- /dev/null +++ b/tests/alive-tv/uf-float/add-comm-half.srctgt.ll @@ -0,0 +1,11 @@ +; TEST-ARGS: --uf-float + +define half @src(half noundef %x, half noundef %y) { + %sum = fadd half %x, %y + ret half %sum +} + +define half @tgt(half noundef %x, half noundef %y) { + %sum = fadd half %y, %x + ret half %sum +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/add-comm-ninf.srctgt.ll b/tests/alive-tv/uf-float/add-comm-ninf.srctgt.ll new file mode 100644 index 000000000..c52c7779c --- /dev/null +++ b/tests/alive-tv/uf-float/add-comm-ninf.srctgt.ll @@ -0,0 +1,11 @@ +; TEST-ARGS: --uf-float + +define float @src(float noundef %x, float noundef %y) { + %sum = fadd ninf float %x, %y + ret float %sum +} + +define float @tgt(float noundef %x, float noundef %y) { + %sum = fadd ninf float %y, %x + ret float %sum +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/add-comm-nnan.srctgt.ll b/tests/alive-tv/uf-float/add-comm-nnan.srctgt.ll new file mode 100644 index 000000000..50d7a7c7e --- /dev/null +++ b/tests/alive-tv/uf-float/add-comm-nnan.srctgt.ll @@ -0,0 +1,11 @@ +; TEST-ARGS: --uf-float + +define float @src(float noundef %x, float noundef %y) { + %sum = fadd nnan float %x, %y + ret float %sum +} + +define float @tgt(float noundef %x, float noundef %y) { + %sum = fadd nnan float %y, %x + ret float %sum +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/add-comm.srctgt.ll b/tests/alive-tv/uf-float/add-comm.srctgt.ll new file mode 100644 index 000000000..7f9fa9728 --- /dev/null +++ b/tests/alive-tv/uf-float/add-comm.srctgt.ll @@ -0,0 +1,11 @@ +; TEST-ARGS: --uf-float + +define float @src(float noundef %x, float noundef %y) { + %sum = fadd float %x, %y + ret float %sum +} + +define float @tgt(float noundef %x, float noundef %y) { + %sum = fadd float %y, %x + ret float %sum +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/cmp-eq-comm.srctgt.ll b/tests/alive-tv/uf-float/cmp-eq-comm.srctgt.ll new file mode 100644 index 000000000..573ade1a4 --- /dev/null +++ b/tests/alive-tv/uf-float/cmp-eq-comm.srctgt.ll @@ -0,0 +1,11 @@ +; TEST-ARGS: --uf-float + +define i1 @src(float noundef %x, float noundef %y) { + %cmp = fcmp oeq float %x, %y + ret i1 %cmp +} + +define i1 @tgt(float noundef %x, float noundef %y) { + %cmp = fcmp oeq float %y, %x + ret i1 %cmp +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/cmp-eq-ne.srctgt.ll b/tests/alive-tv/uf-float/cmp-eq-ne.srctgt.ll new file mode 100644 index 000000000..779b655e0 --- /dev/null +++ b/tests/alive-tv/uf-float/cmp-eq-ne.srctgt.ll @@ -0,0 +1,12 @@ +; TEST-ARGS: --uf-float + +define i1 @src(float noundef %x, float noundef %y) { + %cmp = fcmp oeq float %x, %y + ret i1 %cmp +} + +define i1 @tgt(float noundef %x, float noundef %y) { + %cmp = fcmp une float %x, %y + %notcmp = xor i1 %cmp, 1 + ret i1 %notcmp +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/cmp-lt-gt.srctgt.ll b/tests/alive-tv/uf-float/cmp-lt-gt.srctgt.ll new file mode 100644 index 000000000..4b3ccdbbb --- /dev/null +++ b/tests/alive-tv/uf-float/cmp-lt-gt.srctgt.ll @@ -0,0 +1,11 @@ +; TEST-ARGS: --uf-float + +define i1 @src(float noundef %x, float noundef %y) { + %cmp = fcmp olt float %x, %y + ret i1 %cmp +} + +define i1 @tgt(float noundef %x, float noundef %y) { + %cmp = fcmp ogt float %y, %x + ret i1 %cmp +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/cmp-lt-le.srctgt.ll b/tests/alive-tv/uf-float/cmp-lt-le.srctgt.ll new file mode 100644 index 000000000..ad124452e --- /dev/null +++ b/tests/alive-tv/uf-float/cmp-lt-le.srctgt.ll @@ -0,0 +1,12 @@ +; TEST-ARGS: --uf-float + +define i1 @src(float noundef %x, float noundef %y) { + %cmp = fcmp olt float %x, %y + ret i1 %cmp +} + +define i1 @tgt(float noundef %x, float noundef %y) { + %cmp = fcmp ule float %y, %x + %notcmp = xor i1 %cmp, 1 + ret i1 %notcmp +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/cmp-olt-ult-fail.srctgt.ll b/tests/alive-tv/uf-float/cmp-olt-ult-fail.srctgt.ll new file mode 100644 index 000000000..b9f92c905 --- /dev/null +++ b/tests/alive-tv/uf-float/cmp-olt-ult-fail.srctgt.ll @@ -0,0 +1,12 @@ +; TEST-ARGS: --uf-float +; ERROR: Couldn't prove the correctness of the transformation + +define i1 @src(float noundef %x, float noundef %y) { + %cmp = fcmp olt float %x, %y + ret i1 %cmp +} + +define i1 @tgt(float noundef %x, float noundef %y) { + %cmp = fcmp ult float %x, %y + ret i1 %cmp +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/cmp-ord-uno.srctgt.ll b/tests/alive-tv/uf-float/cmp-ord-uno.srctgt.ll new file mode 100644 index 000000000..9e0d7a0fd --- /dev/null +++ b/tests/alive-tv/uf-float/cmp-ord-uno.srctgt.ll @@ -0,0 +1,12 @@ +; TEST-ARGS: --uf-float + +define i1 @src(float noundef %x, float noundef %y) { + %cmp = fcmp ord float %x, %y + %notcmp = xor i1 %cmp, 1 + ret i1 %notcmp +} + +define i1 @tgt(float noundef %x, float noundef %y) { + %cmp = fcmp uno float %y, %x + ret i1 %cmp +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/load-bitcast.srctgt.ll b/tests/alive-tv/uf-float/load-bitcast.srctgt.ll new file mode 100644 index 000000000..8ec87e261 --- /dev/null +++ b/tests/alive-tv/uf-float/load-bitcast.srctgt.ll @@ -0,0 +1,13 @@ +; TEST-ARGS: --uf-float + +define i32 @src(float noundef %x) { + %a = bitcast float %x to i32 + ret i32 %a +} + +define i32 @tgt(float noundef %x) { + %a = alloca float + store float %x, ptr %a + %b = load i32, ptr %a + ret i32 %b +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/load-store.srctgt.ll b/tests/alive-tv/uf-float/load-store.srctgt.ll new file mode 100644 index 000000000..1c397c404 --- /dev/null +++ b/tests/alive-tv/uf-float/load-store.srctgt.ll @@ -0,0 +1,12 @@ +; TEST-ARGS: --uf-float + +define float @src(float noundef %x) { + ret float %x +} + +define float @tgt(float noundef %x) { + %a = alloca float + store float %x, ptr %a + %b = load float, ptr %a + ret float %b +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/select.srctgt.ll b/tests/alive-tv/uf-float/select.srctgt.ll new file mode 100644 index 000000000..2dcc46005 --- /dev/null +++ b/tests/alive-tv/uf-float/select.srctgt.ll @@ -0,0 +1,17 @@ +; TEST-ARGS: --uf-float + +define float @src(float noundef %x, float noundef %y) { + %cmp = fcmp olt float %x, %y + %a = fsub float %y, %x + %b = fsub float %x, %y + %c = select i1 %cmp, float %a, float %b + ret float %c +} + +define float @tgt(float noundef %x, float noundef %y) { + %cmp = fcmp olt float %x, %y + %min = select i1 %cmp, float %x, float %y + %max = select i1 %cmp, float %y, float %x + %res = fsub float %max, %min + ret float %res +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/vector-binop.srctgt.ll b/tests/alive-tv/uf-float/vector-binop.srctgt.ll new file mode 100644 index 000000000..98c599077 --- /dev/null +++ b/tests/alive-tv/uf-float/vector-binop.srctgt.ll @@ -0,0 +1,14 @@ +; TEST-ARGS: --uf-float + +define float @src(float noundef %x, float noundef %y) { + %sum = fadd float %x, %y + ret float %sum +} + +define float @tgt(float noundef %x, float noundef %y) { + %vec1 = insertelement <2 x float> poison, float %x, i32 0 + %vec2 = insertelement <2 x float> poison, float %y, i32 0 + %vec3 = fadd <2 x float> %vec1, %vec2 + %sum = extractelement <2 x float> %vec3, i32 0 + ret float %sum +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/vector-cmp.srctgt.ll b/tests/alive-tv/uf-float/vector-cmp.srctgt.ll new file mode 100644 index 000000000..ddc62145b --- /dev/null +++ b/tests/alive-tv/uf-float/vector-cmp.srctgt.ll @@ -0,0 +1,14 @@ +; TEST-ARGS: --uf-float + +define i1 @src(float noundef %x, float noundef %y) { + %res = fcmp olt float %x, %y + ret i1 %res +} + +define i1 @tgt(float noundef %x, float noundef %y) { + %vec1 = insertelement <2 x float> poison, float %x, i32 0 + %vec2 = insertelement <2 x float> poison, float %y, i32 0 + %vec3 = fcmp olt <2 x float> %vec1, %vec2 + %res = extractelement <2 x i1> %vec3, i32 0 + ret i1 %res +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/vector-convert.srctgt.ll b/tests/alive-tv/uf-float/vector-convert.srctgt.ll new file mode 100644 index 000000000..05636d146 --- /dev/null +++ b/tests/alive-tv/uf-float/vector-convert.srctgt.ll @@ -0,0 +1,15 @@ +; TEST-ARGS: --uf-float + +define float @src(float noundef %x) { + %a = fptosi float %x to i32 + %res = sitofp i32 %a to float + ret float %res +} + +define float @tgt(float noundef %x) { + %vec1 = insertelement <4 x float> poison, float %x, i32 0 + %vec2 = fptosi <4 x float> %vec1 to <4 x i32> + %vec3 = sitofp <4 x i32> %vec2 to <4 x float> + %res = extractelement <4 x float> %vec3, i32 0 + ret float %res +} \ No newline at end of file diff --git a/tests/alive-tv/uf-float/vector-unop.srctgt.ll b/tests/alive-tv/uf-float/vector-unop.srctgt.ll new file mode 100644 index 000000000..09e70791d --- /dev/null +++ b/tests/alive-tv/uf-float/vector-unop.srctgt.ll @@ -0,0 +1,13 @@ +; TEST-ARGS: --uf-float + +define float @src(float noundef %x) { + %res = fneg float %x + ret float %res +} + +define float @tgt(float noundef %x) { + %vec1 = insertelement <2 x float> poison, float %x, i32 0 + %vec2 = fneg <2 x float> %vec1 + %res = extractelement <2 x float> %vec2, i32 0 + ret float %res +} \ No newline at end of file From 59cebcc6adcbee2e22bb9c4200a244bc3c209dd8 Mon Sep 17 00:00:00 2001 From: Can Date: Wed, 9 Oct 2024 14:06:44 +0200 Subject: [PATCH 2/7] Encode floating point operations as uninterpreted functions --- llvm_util/cmd_args_def.h | 1 + llvm_util/cmd_args_list.h | 5 ++ llvm_util/llvm2alive.cpp | 1 - smt/expr.cpp | 99 +++++++++++++++++++++++++++++++++++---- smt/expr.h | 3 ++ smt/smt.cpp | 9 ++++ smt/smt.h | 2 + 7 files changed, 111 insertions(+), 9 deletions(-) diff --git a/llvm_util/cmd_args_def.h b/llvm_util/cmd_args_def.h index f1c473df5..3b5fba6f0 100644 --- a/llvm_util/cmd_args_def.h +++ b/llvm_util/cmd_args_def.h @@ -23,6 +23,7 @@ smt::solver_tactic_verbose(opt_tactic_verbose); config::debug = opt_debug; config::max_offset_bits = opt_max_offset_in_bits; config::max_sizet_bits = opt_max_sizet_in_bits; +smt::set_uf_float(opt_uf_float); if ((config::disallow_ub_exploitation = opt_disallow_ub_exploitation)) { config::disable_undef_input = true; diff --git a/llvm_util/cmd_args_list.h b/llvm_util/cmd_args_list.h index b732ec92a..c70689c2a 100644 --- a/llvm_util/cmd_args_list.h +++ b/llvm_util/cmd_args_list.h @@ -185,4 +185,9 @@ llvm::cl::opt opt_disallow_ub_exploitation( llvm::cl::desc("Disallow UB exploitation by optimizations (default=allow)"), llvm::cl::init(false), llvm::cl::cat(alive_cmdargs)); +llvm::cl::opt opt_uf_float( + LLVM_ARGS_PREFIX "uf-float", + llvm::cl::desc("Encode floating point operations using uninterpreted functions"), + llvm::cl::init(false), llvm::cl::cat(alive_cmdargs)); + } diff --git a/llvm_util/llvm2alive.cpp b/llvm_util/llvm2alive.cpp index 1b6cdb985..35c9c15a7 100644 --- a/llvm_util/llvm2alive.cpp +++ b/llvm_util/llvm2alive.cpp @@ -1212,7 +1212,6 @@ class llvm2alive_ : public llvm::InstVisitor> { case llvm::Intrinsic::dbg_label: case llvm::Intrinsic::dbg_value: case llvm::Intrinsic::donothing: - case llvm::Intrinsic::fake_use: case llvm::Intrinsic::instrprof_increment: case llvm::Intrinsic::instrprof_increment_step: case llvm::Intrinsic::instrprof_value_profile: diff --git a/smt/expr.cpp b/smt/expr.cpp index 70353e8a1..0bbd43bf8 100644 --- a/smt/expr.cpp +++ b/smt/expr.cpp @@ -4,6 +4,7 @@ #include "smt/expr.h" #include "smt/exprs.h" #include "smt/ctx.h" +#include "smt/smt.h" #include "util/compiler.h" #include #include @@ -1137,6 +1138,9 @@ expr expr::round_up(const expr &power_of_two) const { } while (0) expr expr::isNaN() const { + if (get_uf_float()) + return expr::mkUF("isNaN", {*this}, true); + fold_fp_neg(isNaN); expr v; @@ -1147,6 +1151,9 @@ expr expr::isNaN() const { } expr expr::isInf() const { + if (get_uf_float()) + return expr::mkUF("isInf", {*this}, true); + fold_fp_neg(isInf); expr v; @@ -1159,10 +1166,14 @@ expr expr::isInf() const { expr expr::isFPZero() const { if (isBV()) return extract(bits()-2, 0) == 0; + if (get_uf_float()) + return expr::mkUF("isFPZero", {*this}, true); return unop_fold(Z3_mk_fpa_is_zero); } expr expr::isFPNegative() const { + if (get_uf_float()) + return expr::mkUF("isFPNegative", {*this}, true); return unop_fold(Z3_mk_fpa_is_negative); } @@ -1171,10 +1182,14 @@ expr expr::isFPNegZero() const { } expr expr::isFPNormal() const { + if (get_uf_float()) + return expr::mkUF("isFPNormal", {*this}, true); return unop_fold(Z3_mk_fpa_is_normal); } expr expr::isFPSubNormal() const { + if (get_uf_float()) + return expr::mkUF("isFPSubNormal", {*this}, true); return unop_fold(Z3_mk_fpa_is_subnormal); } @@ -1200,26 +1215,36 @@ expr expr::rtz() { expr expr::fadd(const expr &rhs, const expr &rm) const { C(rhs, rm); + if (get_uf_float()) + return expr::mkCommutativeUF("fadd", {*this, rhs, rm}, *this); return simplify_const(Z3_mk_fpa_add(ctx(), rm(), ast(), rhs()), *this, rhs); } expr expr::fsub(const expr &rhs, const expr &rm) const { C(rhs, rm); + if (get_uf_float()) + return expr::mkUF("fsub", {*this, rhs, rm}, *this); return simplify_const(Z3_mk_fpa_sub(ctx(), rm(), ast(), rhs()), *this, rhs); } expr expr::fmul(const expr &rhs, const expr &rm) const { C(rhs, rm); + if (get_uf_float()) + return expr::mkCommutativeUF("fmul", {*this, rhs, rm}, *this); return simplify_const(Z3_mk_fpa_mul(ctx(), rm(), ast(), rhs()), *this, rhs); } expr expr::fdiv(const expr &rhs, const expr &rm) const { C(rhs, rm); + if (get_uf_float()) + return expr::mkUF("fdiv", {*this, rhs, rm}, *this); return simplify_const(Z3_mk_fpa_div(ctx(), rm(), ast(), rhs()), *this, rhs); } expr expr::frem(const expr &rhs) const { C(rhs); + if (get_uf_float()) + return expr::mkUF("frem", {*this, rhs}, *this); return simplify_const(Z3_mk_fpa_rem(ctx(), ast(), rhs()), *this, rhs); } @@ -1227,6 +1252,9 @@ expr expr::fabs() const { if (isBV()) return mkUInt(0, 1).concat(extract(bits() - 2, 0)); + if (get_uf_float()) + return expr::mkUF("fabs", {*this}, *this); + fold_fp_neg(fabs); return unop_fold(Z3_mk_fpa_abs); } @@ -1237,6 +1265,10 @@ expr expr::fneg() const { return (extract(signbit, signbit) ^ mkUInt(1, 1)) .concat(extract(signbit - 1, 0)); } + + if (get_uf_float()) + return expr::mkUF("fneg", {*this}, *this); + return unop_fold(Z3_mk_fpa_neg); } @@ -1247,11 +1279,15 @@ expr expr::copysign(const expr &sign) const { expr expr::sqrt(const expr &rm) const { C(rm); + if (get_uf_float()) + return expr::mkUF("sqrt", {*this, rm}, *this); return simplify_const(Z3_mk_fpa_sqrt(ctx(), rm(), ast()), *this); } expr expr::fma(const expr &a, const expr &b, const expr &c, const expr &rm) { C2(a, b, c, rm); + if (get_uf_float()) + return expr::mkUF("fma", {a, b, c, rm}, a); return simplify_const(Z3_mk_fpa_fma(ctx(), rm(), a(), b(), c()), a, b, c); } @@ -1265,32 +1301,38 @@ expr expr::floor() const { expr expr::round(const expr &rm) const { C(rm); + if (get_uf_float()) + return expr::mkUF("round", {*this, rm}, *this); return simplify_const(Z3_mk_fpa_round_to_integral(ctx(), rm(), ast()), *this); } expr expr::foeq(const expr &rhs) const { + if (get_uf_float()) + return expr::mkCommutativeUF("foeq", {*this, rhs}, true); return binop_commutative(rhs, Z3_mk_fpa_eq); } expr expr::fogt(const expr &rhs) const { - return binop_fold(rhs, Z3_mk_fpa_gt); + return rhs.folt(*this); } expr expr::foge(const expr &rhs) const { - return binop_fold(rhs, Z3_mk_fpa_geq); + return !fult(rhs); } expr expr::folt(const expr &rhs) const { + if (get_uf_float()) + return expr::mkUF("folt", {*this, rhs}, true); return binop_fold(rhs, Z3_mk_fpa_lt); } expr expr::fole(const expr &rhs) const { - return binop_fold(rhs, Z3_mk_fpa_leq); + return rhs.foge(*this); } expr expr::fone(const expr &rhs) const { - return ford(rhs) && !binop_commutative(rhs, Z3_mk_fpa_eq); + return !fueq(rhs); } expr expr::ford(const expr &rhs) const { @@ -1298,27 +1340,31 @@ expr expr::ford(const expr &rhs) const { } expr expr::fueq(const expr &rhs) const { + if (get_uf_float()) + return expr::mkCommutativeUF("fueq", {*this, rhs}, true); return funo(rhs) || binop_commutative(rhs, Z3_mk_fpa_eq); } expr expr::fugt(const expr &rhs) const { - return funo(rhs) || binop_fold(rhs, Z3_mk_fpa_gt); + return rhs.fult(*this); } expr expr::fuge(const expr &rhs) const { - return funo(rhs) || binop_fold(rhs, Z3_mk_fpa_geq); + return !folt(rhs); } expr expr::fult(const expr &rhs) const { + if (get_uf_float()) + return expr::mkUF("fult", {*this, rhs}, true); return funo(rhs) || binop_fold(rhs, Z3_mk_fpa_lt); } expr expr::fule(const expr &rhs) const { - return funo(rhs) || binop_fold(rhs, Z3_mk_fpa_leq); + return rhs.fuge(*this); } expr expr::fune(const expr &rhs) const { - return funo(rhs) || !binop_commutative(rhs, Z3_mk_fpa_eq); + return !foeq(rhs); } expr expr::funo(const expr &rhs) const { @@ -1925,6 +1971,9 @@ expr expr::toBVBool() const { } expr expr::float2BV() const { + if (isBV()) + return *this; + if (auto app = isAppOf(Z3_OP_FPA_TO_FP)) // ((_ to_fp e s) BV) if (Z3_get_app_num_args(ctx(), app) == 1) return Z3_get_app_arg(ctx(), app, 0); @@ -1938,6 +1987,9 @@ expr expr::float2Real() const { expr expr::BV2float(const expr &type) const { C(type); + if (get_uf_float()) + return *this; + if (auto app = isAppOf(Z3_OP_FPA_TO_IEEE_BV)) { expr arg = Z3_get_app_arg(ctx(), app, 0); if (arg.sort() == type.sort()) @@ -1949,28 +2001,38 @@ expr expr::BV2float(const expr &type) const { expr expr::float2Float(const expr &type, const expr &rm) const { C(type, rm); + if (get_uf_float()) + return expr::mkUF("float2Float", {*this, rm}, type); return simplify_const(Z3_mk_fpa_to_fp_float(ctx(), rm(), ast(), type.sort()), *this); } expr expr::fp2sint(unsigned bits, const expr &rm) const { C(rm); + if (get_uf_float()) + return expr::mkUF("fp2sint", {*this, rm}, expr::mkUInt(0, bits)); return simplify_const(Z3_mk_fpa_to_sbv(ctx(), rm(), ast(), bits), *this); } expr expr::fp2uint(unsigned bits, const expr &rm) const { C(rm); + if (get_uf_float()) + return expr::mkUF("fp2uint", {*this, rm}, expr::mkUInt(0, bits)); return simplify_const(Z3_mk_fpa_to_ubv(ctx(), rm(), ast(), bits), *this); } expr expr::sint2fp(const expr &type, const expr &rm) const { C(type, rm); + if (get_uf_float()) + return expr::mkUF("sint2fp", {*this, rm}, type); return simplify_const(Z3_mk_fpa_to_fp_signed(ctx(), rm(), ast(), type.sort()), *this); } expr expr::uint2fp(const expr &type, const expr &rm) const { C(type, rm); + if (get_uf_float()) + return expr::mkUF("uint2fp", {*this, rm}, type); return simplify_const(Z3_mk_fpa_to_fp_unsigned(ctx(), rm(), ast(), type.sort()), *this); @@ -1995,6 +2057,27 @@ expr expr::mkUF(const char *name, const vector &args, const expr &range) { return Z3_mk_app(ctx(), decl, num_args, z3_args.data()); } +expr expr::mkCommutativeUF(const string &name, vector args, + const expr &range) { + + // Commutative functions are encoded as + // op(x, y) = op'(x, y) & op'(y, x) + // where & is the bitwise and operator and op' is an uninterpreted function. + // This encoding comes from "SMT-based Translation Validation for Machine + // Learning Compiler" by Seongwon Bang, Seunghyeon Nam, Inwhan Chun, + // Ho Young Jhoo, and Juneyoung Lee + + assert(args.size() >= 2); + assert(range.isBV() || range.isBool()); + assert(args[0].isSameTypeOf(args[1])); + expr uf = expr::mkUF(name, args, range); + swap(args[0], args[1]); + expr uf2 = expr::mkUF(name, args, range); + if (range.isBool()) + return uf && uf2; + return uf & uf2; +} + expr expr::mkArray(const char *name, const expr &domain, const expr &range) { C2(domain, range); return ::mkVar(name, Z3_mk_array_sort(ctx(), domain.sort(), range.sort())); diff --git a/smt/expr.h b/smt/expr.h index 038613e7c..d89c0aca8 100644 --- a/smt/expr.h +++ b/smt/expr.h @@ -338,6 +338,9 @@ class expr { return mkUF(name.data(), args, range); } + static expr mkCommutativeUF(const std::string &name, std::vector args, + const expr &range); + static expr mkArray(const char *name, const expr &domain, const expr &range); static expr mkConstArray(const expr &domain, const expr &value); diff --git a/smt/smt.cpp b/smt/smt.cpp index 1f72aeb8b..7bb396072 100644 --- a/smt/smt.cpp +++ b/smt/smt.cpp @@ -42,6 +42,7 @@ void smt_initializer::destroy() { static string query_timeout = "10000"; static string rand_seed = "0"; +static bool uf_float = false; void set_query_timeout(string ms) { query_timeout = std::move(ms); @@ -59,6 +60,14 @@ const char *get_random_seed() { return rand_seed.c_str(); } +void set_uf_float(bool enable) { + uf_float = enable; +} + +bool get_uf_float() { + return uf_float; +} + static uint64_t z3_memory_limit = 1ull << 30; // 1 GB diff --git a/smt/smt.h b/smt/smt.h index a33390539..f340e5348 100644 --- a/smt/smt.h +++ b/smt/smt.h @@ -23,6 +23,8 @@ void set_query_timeout(std::string ms); const char* get_query_timeout(); void set_random_seed(std::string seed); const char *get_random_seed(); +void set_uf_float(bool enable); +bool get_uf_float(); void set_memory_limit(uint64_t limit); bool hit_memory_limit(); From b407dfc992b373fc8ab9868bc50518a420cd43a4 Mon Sep 17 00:00:00 2001 From: Can Date: Wed, 9 Oct 2024 14:20:48 +0200 Subject: [PATCH 3/7] Revert changes to llvm2alive --- llvm_util/llvm2alive.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/llvm_util/llvm2alive.cpp b/llvm_util/llvm2alive.cpp index 35c9c15a7..1b6cdb985 100644 --- a/llvm_util/llvm2alive.cpp +++ b/llvm_util/llvm2alive.cpp @@ -1212,6 +1212,7 @@ class llvm2alive_ : public llvm::InstVisitor> { case llvm::Intrinsic::dbg_label: case llvm::Intrinsic::dbg_value: case llvm::Intrinsic::donothing: + case llvm::Intrinsic::fake_use: case llvm::Intrinsic::instrprof_increment: case llvm::Intrinsic::instrprof_increment_step: case llvm::Intrinsic::instrprof_value_profile: From aa966164144e7dc5278c8f7ef87ce3f891bf9c7a Mon Sep 17 00:00:00 2001 From: Can Date: Wed, 9 Oct 2024 15:37:40 +0200 Subject: [PATCH 4/7] Return bit vectors from float constructors --- ir/type.cpp | 3 ++- smt/expr.cpp | 26 ++++++++++++++++++-------- 2 files changed, 20 insertions(+), 9 deletions(-) diff --git a/ir/type.cpp b/ir/type.cpp index ee7c1e805..8059bd0fb 100644 --- a/ir/type.cpp +++ b/ir/type.cpp @@ -5,6 +5,7 @@ #include "ir/globals.h" #include "ir/state.h" #include "smt/solver.h" +#include "smt/smt.h" #include "util/compiler.h" #include #include @@ -450,7 +451,7 @@ expr FloatType::fromFloat(State &s, const expr &fp, const Type &from_type0, expr isnan = fp.isNaN(); expr val = fp.float2BV(); - if (isnan.isFalse()) + if (isnan.isFalse() || get_uf_float()) return val; unsigned fraction_bits = fractionBits(); diff --git a/smt/expr.cpp b/smt/expr.cpp index 0bbd43bf8..f29dce484 100644 --- a/smt/expr.cpp +++ b/smt/expr.cpp @@ -219,13 +219,20 @@ expr expr::mkInt(const char *n, unsigned bits) { return bits ? Z3_mk_numeral(ctx(), n, mkBVSort(bits)) : expr(); } +static expr to_uf_float_sort(expr&& e) { + if (get_uf_float() && e.isFloat()) + return e.float2BV(); + return e; +} + expr expr::mkFloat(double n, const expr &type) { C2(type); - return Z3_mk_fpa_numeral_double(ctx(), n, type.sort()); + return to_uf_float_sort(Z3_mk_fpa_numeral_double(ctx(), n, type.sort())); } expr expr::mkHalf(float n) { - return Z3_mk_fpa_numeral_float(ctx(), n, Z3_mk_fpa_sort_half(ctx())); + return to_uf_float_sort( + Z3_mk_fpa_numeral_float(ctx(), n, Z3_mk_fpa_sort_half(ctx()))); } static Z3_sort mk_bfloat_sort() { @@ -233,29 +240,32 @@ static Z3_sort mk_bfloat_sort() { } expr expr::mkBFloat(float n) { - return Z3_mk_fpa_numeral_float(ctx(), n, mk_bfloat_sort()); + return to_uf_float_sort(Z3_mk_fpa_numeral_float(ctx(), n, mk_bfloat_sort())); } expr expr::mkFloat(float n) { - return Z3_mk_fpa_numeral_float(ctx(), n, Z3_mk_fpa_sort_single(ctx())); + return to_uf_float_sort( + Z3_mk_fpa_numeral_float(ctx(), n, Z3_mk_fpa_sort_single(ctx()))); } expr expr::mkDouble(double n) { - return Z3_mk_fpa_numeral_double(ctx(), n, Z3_mk_fpa_sort_double(ctx())); + return to_uf_float_sort( + Z3_mk_fpa_numeral_double(ctx(), n, Z3_mk_fpa_sort_double(ctx()))); } expr expr::mkQuad(double n) { - return Z3_mk_fpa_numeral_double(ctx(), n, Z3_mk_fpa_sort_quadruple(ctx())); + return to_uf_float_sort( + Z3_mk_fpa_numeral_double(ctx(), n, Z3_mk_fpa_sort_quadruple(ctx()))); } expr expr::mkNaN(const expr &type) { C2(type); - return Z3_mk_fpa_nan(ctx(), type.sort()); + return to_uf_float_sort(Z3_mk_fpa_nan(ctx(), type.sort())); } expr expr::mkNumber(const char *n, const expr &type) { C2(type); - return Z3_mk_numeral(ctx(), n, type.sort()); + return to_uf_float_sort(Z3_mk_numeral(ctx(), n, type.sort())); } expr expr::mkConst(Z3_decl decl) { From a38be5a90f1033b2fdd42f8e0296954c9758ff3b Mon Sep 17 00:00:00 2001 From: Can Date: Wed, 9 Oct 2024 16:18:57 +0200 Subject: [PATCH 5/7] Add argument and range types to UF name --- smt/expr.cpp | 110 ++++++++++++++++++++++++++++++--------------------- smt/expr.h | 4 +- 2 files changed, 65 insertions(+), 49 deletions(-) diff --git a/smt/expr.cpp b/smt/expr.cpp index f29dce484..24c0e2572 100644 --- a/smt/expr.cpp +++ b/smt/expr.cpp @@ -13,6 +13,7 @@ #include #include #include +#include #include #define DEBUG_Z3_RC 0 @@ -1147,9 +1148,43 @@ expr expr::round_up(const expr &power_of_two) const { return v.fn(); \ } while (0) +static expr uf_float(const char *prefix, vector args, + const expr &range, bool is_commutative = false) { + ostringstream os; + os << prefix; + for (const expr& arg : args) { + os << '.'; + arg.printSort(os); + } + os << '.'; + range.printSort(os); + + string name = std::move(os).str(); + expr uf = expr::mkUF(name, args, range); + if (is_commutative) { + assert(args.size() >= 2); + assert(range.isBV() || range.isBool()); + assert(args[0].isSameTypeOf(args[1])); + + // Commutative functions are encoded as + // op(x, y) = op'(x, y) & op'(y, x) + // where & is the bitwise and operator and op' is an uninterpreted function. + // This encoding comes from "SMT-based Translation Validation for Machine + // Learning Compiler" by Seongwon Bang, Seunghyeon Nam, Inwhan Chun, + // Ho Young Jhoo, and Juneyoung Lee + + swap(args[0], args[1]); + expr uf2 = expr::mkUF(name, args, range); + if (range.isBool()) + return uf && uf2; + return uf & uf2; + } + return uf; +} + expr expr::isNaN() const { if (get_uf_float()) - return expr::mkUF("isNaN", {*this}, true); + return uf_float("isNaN", {*this}, true); fold_fp_neg(isNaN); @@ -1162,7 +1197,7 @@ expr expr::isNaN() const { expr expr::isInf() const { if (get_uf_float()) - return expr::mkUF("isInf", {*this}, true); + return uf_float("isInf", {*this}, true); fold_fp_neg(isInf); @@ -1177,13 +1212,13 @@ expr expr::isFPZero() const { if (isBV()) return extract(bits()-2, 0) == 0; if (get_uf_float()) - return expr::mkUF("isFPZero", {*this}, true); + return uf_float("isFPZero", {*this}, true); return unop_fold(Z3_mk_fpa_is_zero); } expr expr::isFPNegative() const { if (get_uf_float()) - return expr::mkUF("isFPNegative", {*this}, true); + return uf_float("isFPNegative", {*this}, true); return unop_fold(Z3_mk_fpa_is_negative); } @@ -1193,13 +1228,13 @@ expr expr::isFPNegZero() const { expr expr::isFPNormal() const { if (get_uf_float()) - return expr::mkUF("isFPNormal", {*this}, true); + return uf_float("isFPNormal", {*this}, true); return unop_fold(Z3_mk_fpa_is_normal); } expr expr::isFPSubNormal() const { if (get_uf_float()) - return expr::mkUF("isFPSubNormal", {*this}, true); + return uf_float("isFPSubNormal", {*this}, true); return unop_fold(Z3_mk_fpa_is_subnormal); } @@ -1226,35 +1261,35 @@ expr expr::rtz() { expr expr::fadd(const expr &rhs, const expr &rm) const { C(rhs, rm); if (get_uf_float()) - return expr::mkCommutativeUF("fadd", {*this, rhs, rm}, *this); + return uf_float("fadd", {*this, rhs, rm}, *this, true); return simplify_const(Z3_mk_fpa_add(ctx(), rm(), ast(), rhs()), *this, rhs); } expr expr::fsub(const expr &rhs, const expr &rm) const { C(rhs, rm); if (get_uf_float()) - return expr::mkUF("fsub", {*this, rhs, rm}, *this); + return uf_float("fsub", {*this, rhs, rm}, *this); return simplify_const(Z3_mk_fpa_sub(ctx(), rm(), ast(), rhs()), *this, rhs); } expr expr::fmul(const expr &rhs, const expr &rm) const { C(rhs, rm); if (get_uf_float()) - return expr::mkCommutativeUF("fmul", {*this, rhs, rm}, *this); + return uf_float("fmul", {*this, rhs, rm}, *this, true); return simplify_const(Z3_mk_fpa_mul(ctx(), rm(), ast(), rhs()), *this, rhs); } expr expr::fdiv(const expr &rhs, const expr &rm) const { C(rhs, rm); if (get_uf_float()) - return expr::mkUF("fdiv", {*this, rhs, rm}, *this); + return uf_float("fdiv", {*this, rhs, rm}, *this); return simplify_const(Z3_mk_fpa_div(ctx(), rm(), ast(), rhs()), *this, rhs); } expr expr::frem(const expr &rhs) const { C(rhs); if (get_uf_float()) - return expr::mkUF("frem", {*this, rhs}, *this); + return uf_float("frem", {*this, rhs}, *this); return simplify_const(Z3_mk_fpa_rem(ctx(), ast(), rhs()), *this, rhs); } @@ -1263,7 +1298,7 @@ expr expr::fabs() const { return mkUInt(0, 1).concat(extract(bits() - 2, 0)); if (get_uf_float()) - return expr::mkUF("fabs", {*this}, *this); + return uf_float("fabs", {*this}, *this); fold_fp_neg(fabs); return unop_fold(Z3_mk_fpa_abs); @@ -1277,7 +1312,7 @@ expr expr::fneg() const { } if (get_uf_float()) - return expr::mkUF("fneg", {*this}, *this); + return uf_float("fneg", {*this}, *this); return unop_fold(Z3_mk_fpa_neg); } @@ -1290,14 +1325,14 @@ expr expr::copysign(const expr &sign) const { expr expr::sqrt(const expr &rm) const { C(rm); if (get_uf_float()) - return expr::mkUF("sqrt", {*this, rm}, *this); + return uf_float("sqrt", {*this, rm}, *this); return simplify_const(Z3_mk_fpa_sqrt(ctx(), rm(), ast()), *this); } expr expr::fma(const expr &a, const expr &b, const expr &c, const expr &rm) { C2(a, b, c, rm); if (get_uf_float()) - return expr::mkUF("fma", {a, b, c, rm}, a); + return uf_float("fma", {a, b, c, rm}, a); return simplify_const(Z3_mk_fpa_fma(ctx(), rm(), a(), b(), c()), a, b, c); } @@ -1312,14 +1347,14 @@ expr expr::floor() const { expr expr::round(const expr &rm) const { C(rm); if (get_uf_float()) - return expr::mkUF("round", {*this, rm}, *this); + return uf_float("round", {*this, rm}, *this); return simplify_const(Z3_mk_fpa_round_to_integral(ctx(), rm(), ast()), *this); } expr expr::foeq(const expr &rhs) const { if (get_uf_float()) - return expr::mkCommutativeUF("foeq", {*this, rhs}, true); + return uf_float("foeq", {*this, rhs}, true, true); return binop_commutative(rhs, Z3_mk_fpa_eq); } @@ -1333,7 +1368,7 @@ expr expr::foge(const expr &rhs) const { expr expr::folt(const expr &rhs) const { if (get_uf_float()) - return expr::mkUF("folt", {*this, rhs}, true); + return uf_float("folt", {*this, rhs}, true); return binop_fold(rhs, Z3_mk_fpa_lt); } @@ -1351,7 +1386,7 @@ expr expr::ford(const expr &rhs) const { expr expr::fueq(const expr &rhs) const { if (get_uf_float()) - return expr::mkCommutativeUF("fueq", {*this, rhs}, true); + return uf_float("fueq", {*this, rhs}, true, true); return funo(rhs) || binop_commutative(rhs, Z3_mk_fpa_eq); } @@ -1365,7 +1400,7 @@ expr expr::fuge(const expr &rhs) const { expr expr::fult(const expr &rhs) const { if (get_uf_float()) - return expr::mkUF("fult", {*this, rhs}, true); + return uf_float("fult", {*this, rhs}, true); return funo(rhs) || binop_fold(rhs, Z3_mk_fpa_lt); } @@ -2012,7 +2047,7 @@ expr expr::BV2float(const expr &type) const { expr expr::float2Float(const expr &type, const expr &rm) const { C(type, rm); if (get_uf_float()) - return expr::mkUF("float2Float", {*this, rm}, type); + return uf_float("float2Float", {*this, rm}, type); return simplify_const(Z3_mk_fpa_to_fp_float(ctx(), rm(), ast(), type.sort()), *this); } @@ -2020,21 +2055,21 @@ expr expr::float2Float(const expr &type, const expr &rm) const { expr expr::fp2sint(unsigned bits, const expr &rm) const { C(rm); if (get_uf_float()) - return expr::mkUF("fp2sint", {*this, rm}, expr::mkUInt(0, bits)); + return uf_float("fp2sint", {*this, rm}, expr::mkUInt(0, bits)); return simplify_const(Z3_mk_fpa_to_sbv(ctx(), rm(), ast(), bits), *this); } expr expr::fp2uint(unsigned bits, const expr &rm) const { C(rm); if (get_uf_float()) - return expr::mkUF("fp2uint", {*this, rm}, expr::mkUInt(0, bits)); + return uf_float("fp2uint", {*this, rm}, expr::mkUInt(0, bits)); return simplify_const(Z3_mk_fpa_to_ubv(ctx(), rm(), ast(), bits), *this); } expr expr::sint2fp(const expr &type, const expr &rm) const { C(type, rm); if (get_uf_float()) - return expr::mkUF("sint2fp", {*this, rm}, type); + return uf_float("sint2fp", {*this, rm}, type); return simplify_const(Z3_mk_fpa_to_fp_signed(ctx(), rm(), ast(), type.sort()), *this); } @@ -2042,7 +2077,7 @@ expr expr::sint2fp(const expr &type, const expr &rm) const { expr expr::uint2fp(const expr &type, const expr &rm) const { C(type, rm); if (get_uf_float()) - return expr::mkUF("uint2fp", {*this, rm}, type); + return uf_float("uint2fp", {*this, rm}, type); return simplify_const(Z3_mk_fpa_to_fp_unsigned(ctx(), rm(), ast(), type.sort()), *this); @@ -2067,27 +2102,6 @@ expr expr::mkUF(const char *name, const vector &args, const expr &range) { return Z3_mk_app(ctx(), decl, num_args, z3_args.data()); } -expr expr::mkCommutativeUF(const string &name, vector args, - const expr &range) { - - // Commutative functions are encoded as - // op(x, y) = op'(x, y) & op'(y, x) - // where & is the bitwise and operator and op' is an uninterpreted function. - // This encoding comes from "SMT-based Translation Validation for Machine - // Learning Compiler" by Seongwon Bang, Seunghyeon Nam, Inwhan Chun, - // Ho Young Jhoo, and Juneyoung Lee - - assert(args.size() >= 2); - assert(range.isBV() || range.isBool()); - assert(args[0].isSameTypeOf(args[1])); - expr uf = expr::mkUF(name, args, range); - swap(args[0], args[1]); - expr uf2 = expr::mkUF(name, args, range); - if (range.isBool()) - return uf && uf2; - return uf & uf2; -} - expr expr::mkArray(const char *name, const expr &domain, const expr &range) { C2(domain, range); return ::mkVar(name, Z3_mk_array_sort(ctx(), domain.sort(), range.sort())); @@ -2421,6 +2435,10 @@ void expr::printHexadecimal(ostream &os) const { os << (rem == 0 ? *this : zext(4 - rem)); } +void expr::printSort(ostream &os) const { + os << Z3_sort_to_string(ctx(), sort()); +} + string expr::numeral_string() const { C(); return Z3_get_numeral_decimal_string(ctx(), ast(), 12); diff --git a/smt/expr.h b/smt/expr.h index d89c0aca8..ce9d0b821 100644 --- a/smt/expr.h +++ b/smt/expr.h @@ -338,9 +338,6 @@ class expr { return mkUF(name.data(), args, range); } - static expr mkCommutativeUF(const std::string &name, std::vector args, - const expr &range); - static expr mkArray(const char *name, const expr &domain, const expr &range); static expr mkConstArray(const expr &domain, const expr &value); @@ -373,6 +370,7 @@ class expr { void printUnsigned(std::ostream &os) const; void printSigned(std::ostream &os) const; void printHexadecimal(std::ostream &os) const; + void printSort(std::ostream &os) const; std::string numeral_string() const; std::string fn_name() const; // empty if not a function unsigned getFnNumArgs() const; From 15eef2aeaa0dd8e432d63971ff5b0382acb46c2d Mon Sep 17 00:00:00 2001 From: Can Date: Wed, 9 Oct 2024 17:52:05 +0200 Subject: [PATCH 6/7] Add uf-float approximation --- ir/state.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/ir/state.cpp b/ir/state.cpp index 8fd14c42f..f4159aed0 100644 --- a/ir/state.cpp +++ b/ir/state.cpp @@ -255,7 +255,10 @@ State::State(const Function &f, bool source) : f(f), source(source), memory(*this), fp_rounding_mode(expr::mkVar("fp_rounding_mode", 3)), fp_denormal_mode(expr::mkVar("fp_denormal_mode", 2)), - return_val(DisjointExpr(f.getType().getDummyValue(false))) {} + return_val(DisjointExpr(f.getType().getDummyValue(false))) { + + doesApproximation("uf-float"); +} void State::resetGlobals() { Memory::resetGlobals(); From 69ada2affa12eac1b26b246416ddd262e4f37dd8 Mon Sep 17 00:00:00 2001 From: Can Date: Wed, 9 Oct 2024 18:02:14 +0200 Subject: [PATCH 7/7] Fix --- ir/state.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/ir/state.cpp b/ir/state.cpp index f4159aed0..032ab83ad 100644 --- a/ir/state.cpp +++ b/ir/state.cpp @@ -257,7 +257,8 @@ State::State(const Function &f, bool source) fp_denormal_mode(expr::mkVar("fp_denormal_mode", 2)), return_val(DisjointExpr(f.getType().getDummyValue(false))) { - doesApproximation("uf-float"); + if (get_uf_float()) + doesApproximation("uf-float"); } void State::resetGlobals() {