Optionally encode floating point operations as uninterpreted functions

ir/instr.h

@@ -89,6 +89,8 @@ class FpBinOp final : public Instr {
   bool propagatesPoison() const override;
   bool hasSideEffects() const override;
   void rauw(const Value &what, Value &with) override;
+  const char* getOpName() const;
+  bool isCommutative() const;
   void print(std::ostream &os) const override;
   StateValue toSMT(State &s) const override;
   smt::expr getTypeConstraints(const Function &f) const override;
@@ -155,6 +157,7 @@ class FpUnaryOp final : public Instr {
   bool propagatesPoison() const override;
   bool hasSideEffects() const override;
   void rauw(const Value &what, Value &with) override;
+  const char* getOpName() const;
   void print(std::ostream &os) const override;
   StateValue toSMT(State &s) const override;
   smt::expr getTypeConstraints(const Function &f) const override;
@@ -244,6 +247,7 @@ class FpTernaryOp final : public Instr {
   bool propagatesPoison() const override;
   bool hasSideEffects() const override;
   void rauw(const Value &what, Value &with) override;
+  const char* getOpName() const;
   void print(std::ostream &os) const override;
   StateValue toSMT(State &s) const override;
   smt::expr getTypeConstraints(const Function &f) const override;
@@ -269,6 +273,7 @@ class TestOp final : public Instr {
   bool propagatesPoison() const override;
   bool hasSideEffects() const override;
   void rauw(const Value &what, Value &with) override;
+  const char* getOpName() const;
   void print(std::ostream &os) const override;
   StateValue toSMT(State &s) const override;
   smt::expr getTypeConstraints(const Function &f) const override;
@@ -333,6 +338,7 @@ class FpConversionOp final : public Instr {
   bool propagatesPoison() const override;
   bool hasSideEffects() const override;
   void rauw(const Value &what, Value &with) override;
+  const char* getOpName() const;
   void print(std::ostream &os) const override;
   StateValue toSMT(State &s) const override;
   smt::expr getTypeConstraints(const Function &f) const override;
@@ -474,6 +480,7 @@ class FCmp final : public Instr {
   bool propagatesPoison() const override;
   bool hasSideEffects() const override;
   void rauw(const Value &what, Value &with) override;
+  const char* getCondName() const;
   void print(std::ostream &os) const override;
   StateValue toSMT(State &s) const override;
   smt::expr getTypeConstraints(const Function &f) const override;

llvm_util/cmd_args_def.h

@@ -29,6 +29,12 @@ if ((config::disallow_ub_exploitation = opt_disallow_ub_exploitation)) {
   config::disable_poison_input = true;
 }
 
+if (opt_uf_float) {
+  config::fp_encoding_mode = config::FpEncodingMode::UninterpretedFunctions;
+} else {
+  config::fp_encoding_mode = config::FpEncodingMode::FloatingPoint;
+}
+
 func_names.insert(opt_funcs.begin(), opt_funcs.end());
 
 if (!report_dir_created && !opt_report_dir.empty()) {

llvm_util/cmd_args_list.h

@@ -185,4 +185,9 @@ llvm::cl::opt<bool> 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<bool> opt_uf_float(
+  LLVM_ARGS_PREFIX "uf-float",
+  llvm::cl::desc("Approximate floating point operations as uninterpreted functions"),
+  llvm::cl::init(false), llvm::cl::cat(alive_cmdargs));
+
 }

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
+}

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
+}

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
+}

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
+}

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
+}

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
+}

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
+}

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
+}

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
+}

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
+}

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
+}

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
+}

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
+}

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
+}

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
+}

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
+}

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
+}

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
+}

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
+}

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
+}

util/config.cpp

@@ -23,6 +23,7 @@ unsigned src_unroll_cnt = 0;
 unsigned tgt_unroll_cnt = 0;
 unsigned max_offset_bits = 64;
 unsigned max_sizet_bits = 64;
+FpEncodingMode fp_encoding_mode = FpEncodingMode::FloatingPoint;
 
 ostream &dbg() {
   return *debug_os;
@@ -32,4 +33,8 @@ void set_debug(ostream &os) {
   debug_os = &os;
 }
 
+bool is_uf_float() {
+  return fp_encoding_mode == FpEncodingMode::UninterpretedFunctions;
+}
+
 }

util/config.h

@@ -44,7 +44,15 @@ extern unsigned max_offset_bits;
 // size and size of pointers (not to be confused with program pointer size).
 extern unsigned max_sizet_bits;
 
+enum FpEncodingMode {
+  FloatingPoint,
+  UninterpretedFunctions
+};
+
+extern FpEncodingMode fp_encoding_mode;
+
 std::ostream &dbg();
 void set_debug(std::ostream &os);
+bool is_uf_float();
 
 }