From e3521ae317d2e33f8bf2c835461627d3f13275fe Mon Sep 17 00:00:00 2001 From: Kevin Phoenix Date: Wed, 18 Sep 2024 14:31:13 -0700 Subject: [PATCH 1/9] Make RM the final argument in FP ops --- claripy/ast/fp.py | 34 +++++++++++----------------------- claripy/backends/backend_z3.py | 14 +++++++------- claripy/fp.py | 2 +- claripy/operations.py | 4 ++-- tests/test_fp.py | 3 ++- 5 files changed, 23 insertions(+), 34 deletions(-) diff --git a/claripy/ast/fp.py b/claripy/ast/fp.py index a32540ad1..7031847ac 100644 --- a/claripy/ast/fp.py +++ b/claripy/ast/fp.py @@ -126,19 +126,15 @@ def FPV(value, sort): def _fp_length_calc(a1, a2, a3=None): - if isinstance(a1, fp.RM) and a3 is None: - raise Exception - if a3 is None: - return a2.length - return a3.length + return a2.length fpToFP = operations.op("fpToFP", object, FP, calc_length=_fp_length_calc) -fpToFPUnsigned = operations.op("fpToFPUnsigned", (fp.RM, BV, fp.FSort), FP, calc_length=_fp_length_calc) +fpToFPUnsigned = operations.op("fpToFPUnsigned", (BV, fp.FSort, fp.RM), FP, calc_length=_fp_length_calc) fpFP = operations.op("fpFP", (BV, BV, BV), FP, calc_length=lambda a, b, c: a.length + b.length + c.length) fpToIEEEBV = operations.op("fpToIEEEBV", (FP,), BV, calc_length=lambda fp: fp.length) -fpToSBV = operations.op("fpToSBV", (fp.RM, FP, int), BV, calc_length=lambda _rm, _fp, len: len) -fpToUBV = operations.op("fpToUBV", (fp.RM, FP, int), BV, calc_length=lambda _rm, _fp, len: len) +fpToSBV = operations.op("fpToSBV", (FP, int, fp.RM), BV, calc_length=lambda _fp, len, _rm: len) +fpToUBV = operations.op("fpToUBV", (FP, int, fp.RM), BV, calc_length=lambda _fp, len, _rm: len) # # unbound float point comparisons @@ -162,29 +158,21 @@ def _fp_cmp_check(a, b): # -def _fp_binop_check(rm, a, b): # pylint:disable=unused-argument +def _fp_binop_check(a, b, _): return a.length == b.length, "Lengths must be equal" -def _fp_binop_length(rm, a, b): # pylint:disable=unused-argument +def _fp_binop_length(a, _b, _rm): return a.length fpAbs = operations.op("fpAbs", (FP,), FP, calc_length=lambda x: x.length) fpNeg = operations.op("fpNeg", (FP,), FP, calc_length=lambda x: x.length) -fpSub = operations.op("fpSub", (fp.RM, FP, FP), FP, extra_check=_fp_binop_check, calc_length=_fp_binop_length) -fpAdd = operations.op("fpAdd", (fp.RM, FP, FP), FP, extra_check=_fp_binop_check, calc_length=_fp_binop_length) -fpMul = operations.op("fpMul", (fp.RM, FP, FP), FP, extra_check=_fp_binop_check, calc_length=_fp_binop_length) -fpDiv = operations.op("fpDiv", (fp.RM, FP, FP), FP, extra_check=_fp_binop_check, calc_length=_fp_binop_length) -fpSqrt = operations.op( - "fpSqrt", - ( - fp.RM, - FP, - ), - FP, - calc_length=lambda _, x: x.length, -) +fpSub = operations.op("fpSub", (FP, FP, fp.RM), FP, extra_check=_fp_binop_check, calc_length=_fp_binop_length) +fpAdd = operations.op("fpAdd", (FP, FP, fp.RM), FP, extra_check=_fp_binop_check, calc_length=_fp_binop_length) +fpMul = operations.op("fpMul", (FP, FP, fp.RM), FP, extra_check=_fp_binop_check, calc_length=_fp_binop_length) +fpDiv = operations.op("fpDiv", (FP, FP, fp.RM), FP, extra_check=_fp_binop_check, calc_length=_fp_binop_length) +fpSqrt = operations.op("fpSqrt", (FP, fp.RM), FP, calc_length=lambda x, _: x.length) # # bound fp operations diff --git a/claripy/backends/backend_z3.py b/claripy/backends/backend_z3.py index 8ff8f2d87..5fb24f58d 100644 --- a/claripy/backends/backend_z3.py +++ b/claripy/backends/backend_z3.py @@ -1021,23 +1021,23 @@ def _op_raw_fpNeg(self, a): return z3.FPRef(z3.Z3_mk_fpa_neg(self._context.ref(), a.as_ast()), self._context) @condom - def _op_raw_fpAdd(self, rm, a, b): + def _op_raw_fpAdd(self, a, b, rm): return z3.FPRef(z3.Z3_mk_fpa_add(self._context.ref(), rm.as_ast(), a.as_ast(), b.as_ast()), self._context) @condom - def _op_raw_fpSub(self, rm, a, b): + def _op_raw_fpSub(self, a, b, rm): return z3.FPRef(z3.Z3_mk_fpa_sub(self._context.ref(), rm.as_ast(), a.as_ast(), b.as_ast()), self._context) @condom - def _op_raw_fpMul(self, rm, a, b): + def _op_raw_fpMul(self, a, b, rm): return z3.FPRef(z3.Z3_mk_fpa_mul(self._context.ref(), rm.as_ast(), a.as_ast(), b.as_ast()), self._context) @condom - def _op_raw_fpDiv(self, rm, a, b): + def _op_raw_fpDiv(self, a, b, rm): return z3.FPRef(z3.Z3_mk_fpa_div(self._context.ref(), rm.as_ast(), a.as_ast(), b.as_ast()), self._context) @condom - def _op_raw_fpSqrt(self, rm, a): + def _op_raw_fpSqrt(self, a, rm): return z3.FPRef(z3.Z3_mk_fpa_sqrt(self._context.ref(), rm.as_ast(), a.as_ast()), self._context) @condom @@ -1073,11 +1073,11 @@ def _op_raw_fpFP(self, sgn, exp, sig): return z3.FPRef(z3.Z3_mk_fpa_fp(self._context.ref(), sgn.ast, exp.ast, sig.ast), self._context) @condom - def _op_raw_fpToSBV(self, rm, fp, bv_len): + def _op_raw_fpToSBV(self, fp, bv_len, rm): return z3.BitVecRef(z3.Z3_mk_fpa_to_sbv(self._context.ref(), rm.ast, fp.ast, bv_len), self._context) @condom - def _op_raw_fpToUBV(self, rm, fp, bv_len): + def _op_raw_fpToUBV(self, fp, bv_len, rm): return z3.BitVecRef(z3.Z3_mk_fpa_to_ubv(self._context.ref(), rm.ast, fp.ast, bv_len), self._context) @condom diff --git a/claripy/fp.py b/claripy/fp.py index 4678c78db..1a397f386 100644 --- a/claripy/fp.py +++ b/claripy/fp.py @@ -355,7 +355,7 @@ def fpToSBV(rm, fp, size): raise -def fpToUBV(rm, fp, size): +def fpToUBV(fp, size, rm): # todo: actually make unsigned try: rounding_mode = rm.pydecimal_equivalent_rounding_mode() diff --git a/claripy/operations.py b/claripy/operations.py index a96050563..fc746b380 100644 --- a/claripy/operations.py +++ b/claripy/operations.py @@ -18,8 +18,8 @@ def op(name, arg_types, return_type, extra_check=None, calc_length=None, do_coer def _type_fixer(args): num_args = len(args) if expected_num_args is not None and num_args != expected_num_args: - if num_args + 1 == expected_num_args and arg_types[0] is fp.RM: - args = (fp.RM.default(), *args) + if num_args + 1 == expected_num_args and arg_types[-1] is fp.RM: + args = (*args, fp.RM.default()) else: raise ClaripyTypeError(f"Operation {name} takes exactly {len(arg_types)} arguments ({len(args)} given)") diff --git a/tests/test_fp.py b/tests/test_fp.py index 916a6bd9b..49b5311b3 100644 --- a/tests/test_fp.py +++ b/tests/test_fp.py @@ -5,6 +5,7 @@ import unittest import claripy +from claripy.fp import RM class TestFp(unittest.TestCase): @@ -54,7 +55,7 @@ def test_negative_zero(self): def test_fp_ops(self): a = claripy.FPV(1.5, claripy.FSORT_DOUBLE) - b = claripy.fpToUBV(claripy.fp.RM_NearestTiesEven, a, 32) + b = claripy.fpToUBV(a, 32, RM.RM_NearestTiesEven) s = claripy.Solver() assert s.eval(b, 1)[0] == 2 From e865706d2952c3457ce70bd7419216f46c0f947f Mon Sep 17 00:00:00 2001 From: Kevin Phoenix Date: Wed, 18 Sep 2024 15:03:09 -0700 Subject: [PATCH 2/9] Fix _op_fpSqrt in BackendConcrete --- claripy/backends/backend_concrete.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/claripy/backends/backend_concrete.py b/claripy/backends/backend_concrete.py index 1bcd15921..52eb644b2 100644 --- a/claripy/backends/backend_concrete.py +++ b/claripy/backends/backend_concrete.py @@ -102,7 +102,7 @@ def _op_boolnot(arg): return not arg @staticmethod - def _op_fpSqrt(rm, a): # pylint:disable=unused-argument + def _op_fpSqrt(a, _): return a.fpSqrt() def convert(self, expr): From ddf894f402673c47baf78fe718386113b261988a Mon Sep 17 00:00:00 2001 From: Kevin Phoenix Date: Wed, 18 Sep 2024 15:04:08 -0700 Subject: [PATCH 3/9] Improve lint --- claripy/ast/fp.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/claripy/ast/fp.py b/claripy/ast/fp.py index 7031847ac..4d31d0de7 100644 --- a/claripy/ast/fp.py +++ b/claripy/ast/fp.py @@ -125,7 +125,7 @@ def FPV(value, sort): # -def _fp_length_calc(a1, a2, a3=None): +def _fp_length_calc(_a1, a2, _a3=None): return a2.length From 9519bf02c4d5f6bd86c8d0bf31930e5101a7802f Mon Sep 17 00:00:00 2001 From: Kevin Phoenix Date: Wed, 18 Sep 2024 15:09:29 -0700 Subject: [PATCH 4/9] Fix some test cases --- claripy/ast/fp.py | 6 +++--- claripy/fp.py | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/claripy/ast/fp.py b/claripy/ast/fp.py index 4d31d0de7..35d04fb4b 100644 --- a/claripy/ast/fp.py +++ b/claripy/ast/fp.py @@ -35,7 +35,7 @@ def to_fp(self, sort, rm=None): if rm is None: rm = fp.RM.default() - return fpToFP(rm, self, sort) + return fpToFP(self, sort, rm) def raw_to_fp(self): """ @@ -68,7 +68,7 @@ def val_to_bv(self, size, signed=True, rm=None): rm = fp.RM.default() op = fpToSBV if signed else fpToUBV - return op(rm, self, size) + return op(self, size, rm) @property def sort(self): @@ -129,7 +129,7 @@ def _fp_length_calc(_a1, a2, _a3=None): return a2.length -fpToFP = operations.op("fpToFP", object, FP, calc_length=_fp_length_calc) +fpToFP = operations.op("fpToFP", (FP, fp.FSort, fp.RM), FP, calc_length=_fp_length_calc) fpToFPUnsigned = operations.op("fpToFPUnsigned", (BV, fp.FSort, fp.RM), FP, calc_length=_fp_length_calc) fpFP = operations.op("fpFP", (BV, BV, BV), FP, calc_length=lambda a, b, c: a.length + b.length + c.length) fpToIEEEBV = operations.op("fpToIEEEBV", (FP,), BV, calc_length=lambda fp: fp.length) diff --git a/claripy/fp.py b/claripy/fp.py index 1a397f386..0783d60e0 100644 --- a/claripy/fp.py +++ b/claripy/fp.py @@ -342,7 +342,7 @@ def fpFP(sgn, exp, mantissa): return FPV(unpacked, sort) -def fpToSBV(rm, fp, size): +def fpToSBV(fp, size, rm): try: rounding_mode = rm.pydecimal_equivalent_rounding_mode() val = int(Decimal(fp.value).to_integral_value(rounding_mode)) From 69e3fb22682158f420850261c82963a0c85d1a77 Mon Sep 17 00:00:00 2001 From: Kevin Phoenix Date: Wed, 18 Sep 2024 15:24:54 -0700 Subject: [PATCH 5/9] Remove default arg in test_fp.py --- tests/test_fp.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/tests/test_fp.py b/tests/test_fp.py index 49b5311b3..774af2904 100644 --- a/tests/test_fp.py +++ b/tests/test_fp.py @@ -5,7 +5,6 @@ import unittest import claripy -from claripy.fp import RM class TestFp(unittest.TestCase): @@ -55,7 +54,7 @@ def test_negative_zero(self): def test_fp_ops(self): a = claripy.FPV(1.5, claripy.FSORT_DOUBLE) - b = claripy.fpToUBV(a, 32, RM.RM_NearestTiesEven) + b = claripy.fpToUBV(a, 32) s = claripy.Solver() assert s.eval(b, 1)[0] == 2 From a4a79748db06f4a504de66714ce1928ed2d3fccc Mon Sep 17 00:00:00 2001 From: Kevin Phoenix Date: Wed, 18 Sep 2024 15:41:28 -0700 Subject: [PATCH 6/9] Fix fpToFP --- claripy/ast/fp.py | 9 +++------ claripy/fp.py | 45 ++++++--------------------------------------- 2 files changed, 9 insertions(+), 45 deletions(-) diff --git a/claripy/ast/fp.py b/claripy/ast/fp.py index 35d04fb4b..0e868260f 100644 --- a/claripy/ast/fp.py +++ b/claripy/ast/fp.py @@ -3,7 +3,7 @@ import struct from claripy import fp, operations -from claripy.ast.base import _make_name +from claripy.ast.base import Base, _make_name from claripy.fp import FSORT_FLOAT from .bits import Bits @@ -24,7 +24,7 @@ class FP(Bits): __slots__ = () - def to_fp(self, sort, rm=None): + def to_fp(self, sort, rm=fp.RM.RM_NearestTiesEven): """ Convert this float to a different sort @@ -32,9 +32,6 @@ def to_fp(self, sort, rm=None): :param rm: Optional: The rounding mode to use :return: An FP AST """ - if rm is None: - rm = fp.RM.default() - return fpToFP(self, sort, rm) def raw_to_fp(self): @@ -129,7 +126,7 @@ def _fp_length_calc(_a1, a2, _a3=None): return a2.length -fpToFP = operations.op("fpToFP", (FP, fp.FSort, fp.RM), FP, calc_length=_fp_length_calc) +fpToFP = operations.op("fpToFP", (Base, fp.FSort, fp.RM), FP, calc_length=_fp_length_calc) fpToFPUnsigned = operations.op("fpToFPUnsigned", (BV, fp.FSort, fp.RM), FP, calc_length=_fp_length_calc) fpFP = operations.op("fpFP", (BV, BV, BV), FP, calc_length=lambda a, b, c: a.length + b.length + c.length) fpToIEEEBV = operations.op("fpToIEEEBV", (FP,), BV, calc_length=lambda fp: fp.length) diff --git a/claripy/fp.py b/claripy/fp.py index 0783d60e0..84e505641 100644 --- a/claripy/fp.py +++ b/claripy/fp.py @@ -241,47 +241,14 @@ def __repr__(self): return f"FPV({self.value:f}, {self.sort})" -def fpToFP(a1, a2, a3=None): - """ - Returns a FP AST and has three signatures: - - fpToFP(ubvv, sort) - Returns a FP AST whose value is the same as the unsigned BVV `a1` - and whose sort is `a2`. - - fpToFP(rm, fpv, sort) - Returns a FP AST whose value is the same as the floating point `a2` - and whose sort is `a3`. - - fpToTP(rm, sbvv, sort) - Returns a FP AST whose value is the same as the signed BVV `a2` and - whose sort is `a3`. - """ - if isinstance(a1, BVV) and isinstance(a2, FSort): - sort = a2 - if sort == FSORT_FLOAT: - pack, unpack = "I", "f" - elif sort == FSORT_DOUBLE: - pack, unpack = "Q", "d" - else: - raise ClaripyOperationError("unrecognized float sort") - - try: - packed = struct.pack("<" + pack, a1.value) - (unpacked,) = struct.unpack("<" + unpack, packed) - except OverflowError as e: - # struct.pack sometimes overflows - raise ClaripyOperationError("OverflowError: " + str(e)) from e - - return FPV(unpacked, sort) - if isinstance(a1, RM) and isinstance(a2, FPV) and isinstance(a3, FSort): - return FPV(a2.value, a3) - if isinstance(a1, RM) and isinstance(a2, BVV) and isinstance(a3, FSort): - return FPV(float(a2.signed), a3) - raise ClaripyOperationError("unknown types passed to fpToFP") +def fpToFP(arg: BVV | FPV, sort: FSort, _rm: RM = RM.RM_NearestTiesEven): + """Returns a FP AST given a BVV or FPV.""" + if isinstance(arg, BVV): + arg = FPV(float(arg.value), sort) + return FPV(arg.value, sort) -def fpToFPUnsigned(_rm, thing, sort): +def fpToFPUnsigned(thing, sort, _rm): """ Returns a FP AST whose value is the same as the unsigned BVV `thing` and whose sort is `sort`. From 29e5800736cd5e3299db3693d92028b33cb5a0be Mon Sep 17 00:00:00 2001 From: Kevin Phoenix Date: Wed, 18 Sep 2024 15:53:57 -0700 Subject: [PATCH 7/9] Add docstrings --- claripy/fp.py | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/claripy/fp.py b/claripy/fp.py index 84e505641..4bd8a9ea4 100644 --- a/claripy/fp.py +++ b/claripy/fp.py @@ -37,7 +37,12 @@ def normalize_helper(self, o): class RM(Enum): - # see https://en.wikipedia.org/wiki/IEEE_754#Rounding_rules + """Floating point rounding mode, as defined by IEEE754. + + See this wikipedia entry for details: + https://en.wikipedia.org/wiki/IEEE_754#Rounding_rules + """ + RM_NearestTiesEven = "RM_RNE" RM_NearestTiesAwayFromZero = "RM_RNA" RM_TowardsZero = "RM_RTZ" @@ -66,6 +71,10 @@ def pydecimal_equivalent_rounding_mode(self): class FSort: + """Floating point sort, desribing the size of the exponent and mantissa for + an IEEE754 floating point number. + """ + def __init__(self, name, exp, mantissa): self.name = name self.exp = exp @@ -106,6 +115,9 @@ def from_params(exp, mantissa): class FPV(BackendObject): + """Floating point value. A concrete floating point value with a specific + sort (FSORT_FLOAT or FSORT_DOUBLE).""" + __slots__ = ["sort", "value"] def __init__(self, value, sort): From f21b9df9e5e1eb151af23d96fcfb9d32ef929fbc Mon Sep 17 00:00:00 2001 From: Kevin Phoenix Date: Thu, 19 Sep 2024 16:53:32 -0700 Subject: [PATCH 8/9] Special case RM position in z3 backend --- claripy/backends/backend_z3.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/claripy/backends/backend_z3.py b/claripy/backends/backend_z3.py index 5fb24f58d..fc6605e0b 100644 --- a/claripy/backends/backend_z3.py +++ b/claripy/backends/backend_z3.py @@ -550,6 +550,9 @@ def _abstract_internal(self, ctx, ast, split_on=None): l.error(err) raise BackendError(err) + if ty is FP and isinstance(args[0], RM): + args = [*args[1:], args[0]] + if op_name == "If": # If is polymorphic and thus must be handled specially ty = type(args[1]) From e5341fe0fbe817124d16a765ed1187c9ad79fc3e Mon Sep 17 00:00:00 2001 From: Kevin Phoenix Date: Fri, 20 Sep 2024 17:19:48 -0700 Subject: [PATCH 9/9] Remove special case in _type_fixer for fp.RM as args[0] --- claripy/operations.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/claripy/operations.py b/claripy/operations.py index fc746b380..63894d3d4 100644 --- a/claripy/operations.py +++ b/claripy/operations.py @@ -27,7 +27,7 @@ def _type_fixer(args): matches = list(itertools.starmap(isinstance, zip(args, actual_arg_types, strict=False))) # heuristically, this works! - thing = args[matches.index(True, 1 if actual_arg_types[0] is fp.RM else 0)] if True in matches else None + thing = args[matches.index(True, 0)] if True in matches else None for arg, argty, match in zip(args, actual_arg_types, matches, strict=False): if not match: