From de0bd589823d189e78bdcbc8f114dcf3d3df115b Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Sat, 8 Feb 2025 19:38:28 +0000 Subject: [PATCH] Add floating-point operator `Copysign` (Closes #185) --- src/eval.ml | 2 ++ src/mappings.ml | 23 ++++++++++++++--------- src/ty.ml | 5 ++++- src/ty.mli | 1 + test/solver/test_fp.ml | 17 +++++++++++++++++ test/unit/test_binop.ml | 20 ++++++++++++++++++++ 6 files changed, 58 insertions(+), 10 deletions(-) diff --git a/src/eval.ml b/src/eval.ml index 01c2cfda..4a0a9408 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -681,6 +681,7 @@ module F32 = struct | Rem -> Float.rem | Min -> Float.min | Max -> Float.max + | Copysign -> Float.copy_sign | _ -> Fmt.failwith {|binop: Unsupported f32 operator "%a"|} Ty.Binop.pp op in @@ -743,6 +744,7 @@ module F64 = struct | Rem -> Float.rem | Min -> Float.min | Max -> Float.max + | Copysign -> Float.copy_sign | _ -> Fmt.failwith {|binop: Unsupported f32 operator "%a"|} Ty.Binop.pp op in diff --git a/src/mappings.ml b/src/mappings.ml index 3e5e3802..a52b012b 100644 --- a/src/mappings.ml +++ b/src/mappings.ml @@ -431,6 +431,8 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct val sb : int + val zero : unit -> M.term + val v : elt -> M.term (* TODO: *) (* val to_string : Z3.FuncDecl.func_decl *) @@ -451,8 +453,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct | Floor -> Float.round_to_integral ~rm:Float.Rounding_mode.rtn e | Trunc -> Float.round_to_integral ~rm:Float.Rounding_mode.rtz e | Nearest -> Float.round_to_integral ~rm:Float.Rounding_mode.rne e - | _ -> - Fmt.failwith {|Fp: Unsupported Z3 unary operator "%a"|} Unop.pp op + | _ -> Fmt.failwith {|Fp: Unsupported unary operator "%a"|} Unop.pp op let binop op e1 e2 = match op with @@ -463,11 +464,13 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct | Min -> Float.min e1 e2 | Max -> Float.max e1 e2 | Rem -> Float.rem e1 e2 - | _ -> - Fmt.failwith {|Fp: Unsupported Z3 binop operator "%a"|} Binop.pp op + | Copysign -> + let abs_float = Float.abs e1 in + M.ite (Float.ge e2 (F.zero ())) abs_float (Float.neg abs_float) + | _ -> Fmt.failwith {|Fp: Unsupported binop operator "%a"|} Binop.pp op let triop op _ = - Fmt.failwith {|Fp: Unsupported Z3 triop operator "%a"|} Triop.pp op + Fmt.failwith {|Fp: Unsupported triop operator "%a"|} Triop.pp op let relop op e1 e2 = match op with @@ -477,8 +480,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct | Le -> Float.le e1 e2 | Gt -> Float.gt e1 e2 | Ge -> Float.ge e1 e2 - | _ -> - Fmt.failwith {|Fp: Unsupported Z3 relop operator "%a"|} Relop.pp op + | _ -> Fmt.failwith {|Fp: Unsupported relop operator "%a"|} Relop.pp op let cvtop op e = match op with @@ -495,8 +497,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct | OfString -> (* TODO: FuncDecl.apply of_string [ e ] *) assert false - | _ -> - Fmt.failwith {|Fp: Unsupported Z3 cvtop operator "%a"|} Cvtop.pp op + | _ -> Fmt.failwith {|Fp: Unsupported cvtop operator "%a"|} Cvtop.pp op end module Float32_impl = Float_impl (struct @@ -508,6 +509,8 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct let v f = M.Float.v (Int32.float_of_bits f) eb sb + let zero () = v (Int32.bits_of_float 0.0) + (* TODO: *) (* let to_string = *) (* Z3.FuncDecl.mk_func_decl_s ctx "F32ToString" [ fp32_sort ] str_sort *) @@ -524,6 +527,8 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct let v f = M.Float.v (Int64.float_of_bits f) eb sb + let zero () = v (Int64.bits_of_float 0.0) + (* TODO: *) (* let to_string = *) (* Z3.FuncDecl.mk_func_decl_s ctx "F64ToString" [ fp64_sort ] str_sort *) diff --git a/src/ty.ml b/src/ty.ml index 11041339..b5a5e518 100644 --- a/src/ty.ml +++ b/src/ty.ml @@ -187,6 +187,7 @@ module Binop = struct | Pow | Min | Max + | Copysign | Rotl | Rotr | At @@ -219,6 +220,7 @@ module Binop = struct | Pow, Pow | Min, Min | Max, Max + | Copysign, Copysign | Rotl, Rotl | Rotr, Rotr | At, At @@ -232,7 +234,7 @@ module Binop = struct | Regexp_range, Regexp_range -> true | ( ( Add | Sub | Mul | Div | DivU | Rem | RemU | Shl | ShrA | ShrL | And - | Or | Xor | Pow | Min | Max | Rotl | Rotr | At | List_cons + | Or | Xor | Pow | Min | Max | Copysign | Rotl | Rotr | At | List_cons | List_append | String_prefix | String_suffix | String_contains | String_last_index | String_in_re | Regexp_range ) , _ ) -> @@ -255,6 +257,7 @@ module Binop = struct | Pow -> Fmt.string fmt "pow" | Min -> Fmt.string fmt "min" | Max -> Fmt.string fmt "max" + | Copysign -> Fmt.string fmt "copysign" | Rotl -> Fmt.string fmt "rotl" | Rotr -> Fmt.string fmt "rotr" | At -> Fmt.string fmt "at" diff --git a/src/ty.mli b/src/ty.mli index c03660d1..6e9ffed9 100644 --- a/src/ty.mli +++ b/src/ty.mli @@ -82,6 +82,7 @@ module Binop : sig | Pow | Min | Max + | Copysign | Rotl | Rotr | At diff --git a/test/solver/test_fp.ml b/test/solver/test_fp.ml index 38aed3bd..ab9ff72c 100644 --- a/test/solver/test_fp.ml +++ b/test/solver/test_fp.ml @@ -31,4 +31,21 @@ module Make (M : Mappings_intf.S) = struct Solver.add solver F32.[ Expr.unop (Ty_fp 32) Sqrt x = F32.v 2.0 ]; assert_sat (Solver.check solver []); assert (Expr.equal (Solver.get_value solver x) (F32.v 4.0)) + + (* Copysign *) + let () = + let solver = Solver.create ~logic:QF_BVFP () in + let x = F32.sym "x" in + let y = F32.sym "y" in + Solver.add solver F32.[ x > v 0.0; y < v 0.0 ]; + Solver.add solver F32.[ Expr.binop (Ty_fp 32) Copysign x y < v 0.0 ]; + assert_sat (Solver.check solver []) + + let () = + let solver = Solver.create ~logic:QF_BVFP () in + let x = F64.sym "x" in + let y = F64.sym "y" in + Solver.add solver F64.[ x > v 0.0; y < v 0.0 ]; + Solver.add solver F64.[ Expr.binop (Ty_fp 64) Copysign x y < v 0.0 ]; + assert_sat (Solver.check solver []) end diff --git a/test/unit/test_binop.ml b/test/unit/test_binop.ml index 8f8b3b83..e6a759c2 100644 --- a/test/unit/test_binop.ml +++ b/test/unit/test_binop.ml @@ -19,6 +19,10 @@ let int32 x = value (Num (I32 x)) let int64 x = value (Num (I64 x)) +let float32 x = value (Num (F32 (Int32.bits_of_float x))) + +let float64 x = value (Num (F64 (Int64.bits_of_float x))) + let list x = value (List x) (* int *) @@ -105,6 +109,22 @@ let () = assert (binop (Ty_bitv 64) Rotl (int64 Int64.min_int) (int64 2L) = int64 2L); assert (binop (Ty_bitv 64) Rotr (int64 2L) (int64 2L) = int64 Int64.min_int) +(* f32 *) +let () = + let ty = Ty_fp 32 in + assert (binop ty Copysign (float32 (-4.2)) (float32 2.0) = float32 4.2); + assert (binop ty Copysign (float32 4.2) (float32 (-2.0)) = float32 (-4.2)); + assert (binop ty Copysign (float32 4.2) (float32 2.0) = float32 4.2); + assert (binop ty Copysign (float32 (-4.2)) (float32 (-2.0)) = float32 (-4.2)) + +(* f64 *) +let () = + let ty = Ty_fp 64 in + assert (binop ty Copysign (float64 (-4.2)) (float64 2.0) = float64 4.2); + assert (binop ty Copysign (float64 4.2) (float64 (-2.0)) = float64 (-4.2)); + assert (binop ty Copysign (float64 4.2) (float64 2.0) = float64 4.2); + assert (binop ty Copysign (float64 (-4.2)) (float64 (-2.0)) = float64 (-4.2)) + (* ptr *) let () = let p0 = ptr 0l (int32 0l) in