diff --git a/runtime/rust_backend/Runtime.cpp b/runtime/rust_backend/Runtime.cpp index 91adf9e9..a00ff4f9 100644 --- a/runtime/rust_backend/Runtime.cpp +++ b/runtime/rust_backend/Runtime.cpp @@ -205,6 +205,7 @@ DEF_BINARY_BV_EXPR_BUILDER(fp_rem) #undef DEF_BINARY_BV_EXPR_BUILDER DEF_UNARY_EXPR_BUILDER(fp_abs) +DEF_UNARY_EXPR_BUILDER(fp_neg) DEF_UNARY_EXPR_BUILDER(not ) DEF_BINARY_BOOL_EXPR_BUILDER(not_equal) @@ -227,6 +228,11 @@ DEF_BINARY_BOOL_EXPR_BUILDER(float_unordered_not_equal) #undef DEF_BINARY_BOOL_EXPR_BUILDER +SymExpr _sym_build_ite(SymExpr cond, SymExpr a, SymExpr b) { + return registerExpression(symexpr( + _rsym_build_ite(symexpr_id(cond), symexpr_id(a), symexpr_id(b)), 0)); +} + SymExpr _sym_build_sext(SymExpr expr, uint8_t bits) { return registerExpression(symexpr(_rsym_build_sext(symexpr_id(expr), bits), symexpr_width(expr) + bits)); diff --git a/runtime/rust_backend/RustRuntime.h b/runtime/rust_backend/RustRuntime.h index 7789a86f..766faa41 100644 --- a/runtime/rust_backend/RustRuntime.h +++ b/runtime/rust_backend/RustRuntime.h @@ -66,6 +66,7 @@ RSymExpr _rsym_build_fp_mul(RSymExpr a, RSymExpr b); RSymExpr _rsym_build_fp_div(RSymExpr a, RSymExpr b); RSymExpr _rsym_build_fp_rem(RSymExpr a, RSymExpr b); RSymExpr _rsym_build_fp_abs(RSymExpr a); +RSymExpr _rsym_build_fp_neg(RSymExpr a); /* * Boolean operations @@ -87,6 +88,7 @@ RSymExpr _rsym_build_bool_or(RSymExpr a, RSymExpr b); RSymExpr _rsym_build_or(RSymExpr a, RSymExpr b); RSymExpr _rsym_build_bool_xor(RSymExpr a, RSymExpr b); RSymExpr _rsym_build_xor(RSymExpr a, RSymExpr b); +RSymExpr _rsym_build_ite(RSymExpr cond, RSymExpr a, RSymExpr b); RSymExpr _rsym_build_float_ordered_greater_than(RSymExpr a, RSymExpr b); RSymExpr _rsym_build_float_ordered_greater_equal(RSymExpr a, RSymExpr b);