Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Encode floating point operations as uninterpreted functions #1095

Open
wants to merge 7 commits into
base: master
Choose a base branch
from
Open

Encode floating point operations as uninterpreted functions #1095

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
a2cdfce
Add unit tests
can-leh-emmtrix Oct 9, 2024
59cebcc
Encode floating point operations as uninterpreted functions
can-leh-emmtrix Oct 9, 2024
b407dfc
Revert changes to llvm2alive
can-leh-emmtrix Oct 9, 2024
aa96616
Return bit vectors from float constructors
can-leh-emmtrix Oct 9, 2024
a38be5a
Add argument and range types to UF name
can-leh-emmtrix Oct 9, 2024
15eef2a
Add uf-float approximation
can-leh-emmtrix Oct 9, 2024
69ada2a
Fix
can-leh-emmtrix Oct 9, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 5 additions & 1 deletion ir/state.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -255,7 +255,11 @@ 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))) {

if (get_uf_float())
doesApproximation("uf-float");
Comment on lines +260 to +261
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am not sure what the best way to handle doesApproximation is with this approach. One option would be to call it in fm_poison in instr.cpp, however we don't have direct access to the UFs anymore. From what I can tell from the source code, the second argument to doesApproximation needs to be the APP node of the UF. However we do not have access to that anymore at this point. It may be possible to obtain the UFs by traversing the AST though. Another option might be to register a callback function with expr.h which is called for each created UF.

}

void State::resetGlobals() {
Memory::resetGlobals();
Expand Down
3 changes: 2 additions & 1 deletion ir/type.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 <array>
#include <cassert>
Expand Down Expand Up @@ -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();
Expand Down
1 change: 1 addition & 0 deletions llvm_util/cmd_args_def.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
5 changes: 5 additions & 0 deletions llvm_util/cmd_args_list.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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("Encode floating point operations using uninterpreted functions"),
llvm::cl::init(false), llvm::cl::cat(alive_cmdargs));

}
Loading