Handle floating point operators with non-default rms

Author: filipeom

src/smtml/expr.ml

@@ -109,7 +109,7 @@ let rec ty (hte : t) : Ty.t =
   | Ptr _ -> Ty_bitv 32
   | Symbol x -> Symbol.type_of x
   | List _ -> Ty_list
-  | App _ -> Ty_app
+  | App (sym, _) -> begin match sym.ty with Ty_none -> Ty_app | ty -> ty end
   | Unop (ty, _, _) -> ty
   | Binop (ty, _, _, _) -> ty
   | Triop (_, Ite, _, hte1, hte2) ->

src/smtml/mappings.ml

@@ -656,6 +656,20 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       | Ty.Ty_regexp -> Regexp_impl.naryop
       | ty -> Fmt.failwith "Naryop for type \"%a\" not implemented" Ty.pp ty
 
+    let get_rounding_mode rm =
+      match Expr.view rm with
+      | Symbol { name = Simple ("roundNearestTiesToEven" | "RNE"); _ } ->
+        M.Float.Rounding_mode.rne
+      | Symbol { name = Simple ("roundNearestTiesToAway" | "RNA"); _ } ->
+        M.Float.Rounding_mode.rna
+      | Symbol { name = Simple ("roundTowardPositive" | "RTP"); _ } ->
+        M.Float.Rounding_mode.rtp
+      | Symbol { name = Simple ("roundTowardNegative" | "RTN"); _ } ->
+        M.Float.Rounding_mode.rtn
+      | Symbol { name = Simple ("roundTowardZero" | "RTZ"); _ } ->
+        M.Float.Rounding_mode.rtz
+      | _ -> Fmt.failwith "unknown rouding mode: %a" Expr.pp rm
+
     let rec encode_expr ctx (hte : Expr.t) : symbol_ctx * M.term =
       match Expr.view hte with
       | Val value -> (ctx, v value)
@@ -664,6 +678,35 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
         let ctx, offset' = encode_expr ctx offset in
         (ctx, I32.binop Add base' offset')
       | Symbol sym -> make_symbol ctx sym
+      (* FIXME: add a way to support building these expressions without apps *)
+      | App ({ name = Simple "fp.add"; _ }, [ rm; a; b ]) ->
+        let ctx, a = encode_expr ctx a in
+        let ctx, b = encode_expr ctx b in
+        let rm = get_rounding_mode rm in
+        (ctx, M.Float.add ~rm a b)
+      | App ({ name = Simple "fp.sub"; _ }, [ rm; a; b ]) ->
+        let ctx, a = encode_expr ctx a in
+        let ctx, b = encode_expr ctx b in
+        let rm = get_rounding_mode rm in
+        (ctx, M.Float.sub ~rm a b)
+      | App ({ name = Simple "fp.mul"; _ }, [ rm; a; b ]) ->
+        let ctx, a = encode_expr ctx a in
+        let ctx, b = encode_expr ctx b in
+        let rm = get_rounding_mode rm in
+        (ctx, M.Float.mul ~rm a b)
+      | App ({ name = Simple "fp.div"; _ }, [ rm; a; b ]) ->
+        let ctx, a = encode_expr ctx a in
+        let ctx, b = encode_expr ctx b in
+        let rm = get_rounding_mode rm in
+        (ctx, M.Float.div ~rm a b)
+      | App ({ name = Simple "fp.sqrt"; _ }, [ rm; a ]) ->
+        let ctx, a = encode_expr ctx a in
+        let rm = get_rounding_mode rm in
+        (ctx, M.Float.sqrt ~rm a)
+      | App ({ name = Simple "fp.roundToIntegral"; _ }, [ rm; a ]) ->
+        let ctx, a = encode_expr ctx a in
+        let rm = get_rounding_mode rm in
+        (ctx, M.Float.round_to_integral ~rm a)
       | App (sym, args) ->
         let name =
           match Symbol.name sym with

src/smtml/rewrite.ml

@@ -38,14 +38,28 @@ let rec rewrite_expr (type_map, expr_map) hte =
   | Val _ -> hte
   | Ptr { base; offset } ->
     Expr.ptr base (rewrite_expr (type_map, expr_map) offset)
-  | Symbol sym -> (
+  | Symbol sym -> begin
     match Symb_map.find_opt sym type_map with
     | None -> (
       match Symb_map.find_opt sym expr_map with
       | None -> Fmt.failwith "Undefined symbol: %a" Symbol.pp sym
       | Some expr -> expr )
-    | Some ty -> Expr.symbol { sym with ty } )
+    | Some ty -> Expr.symbol { sym with ty }
+  end
   | List htes -> Expr.list (List.map (rewrite_expr (type_map, expr_map)) htes)
+  | App
+      ( ({ name = Simple ("fp.add" | "fp.sub" | "fp.mul" | "fp.div"); _ } as sym)
+      , [ rm; a; b ] ) ->
+    let a = rewrite_expr (type_map, expr_map) a in
+    let b = rewrite_expr (type_map, expr_map) b in
+    let ty = rewrite_ty Ty_none [ Expr.ty a; Expr.ty b ] in
+    Expr.app { sym with ty } [ rm; a; b ]
+  | App
+      ( ({ name = Simple ("fp.sqrt" | "fp.roundToIntegral"); _ } as sym)
+      , [ rm; a ] ) ->
+    let a = rewrite_expr (type_map, expr_map) a in
+    let ty = rewrite_ty Ty_none [ Expr.ty a ] in
+    Expr.app { sym with ty } [ rm; a ]
   | App (sym, htes) ->
     let sym =
       match Symb_map.find_opt sym type_map with

src/smtml/smtlib.ml

@@ -135,6 +135,12 @@ module Term = struct
     let exponent_shifted = Int32.shift_left exponent 23 in
     Int32.logor sign_shifted (Int32.logor exponent_shifted mantissa)
 
+  let make_fp_binop symbol (op : Ty.Binop.t) rm a b =
+    match Expr.view rm with
+    | Symbol { name = Simple "roundNearestTiesToEven"; _ } ->
+      Expr.raw_binop Ty_none op a b
+    | _ -> Expr.app symbol [ rm; a; b ]
+
   let apply ?loc (id : t) (args : t list) : t =
     match Expr.view id with
     | Symbol ({ namespace = Term; name = Simple name; _ } as symbol) -> (
@@ -237,63 +243,38 @@ module Term = struct
             Expr.pp eb Expr.pp i )
       | "fp.abs", [ a ] -> Expr.raw_unop Ty_none Abs a
       | "fp.neg", [ a ] -> Expr.raw_unop Ty_none Neg a
-      | ( "fp.add"
-        , [ { node = Symbol { name = Simple "roundNearestTiesToEven"; _ }; _ }
-          ; a
-          ; b
-          ] ) ->
-        Expr.raw_binop Ty_none Add a b
-      | ( "fp.sub"
-        , [ { node = Symbol { name = Simple "roundNearestTiesToEven"; _ }; _ }
-          ; a
-          ; b
-          ] ) ->
-        Expr.raw_binop Ty_none Sub a b
-      | ( "fp.mul"
-        , [ { node = Symbol { name = Simple "roundNearestTiesToEven"; _ }; _ }
-          ; a
-          ; b
-          ] ) ->
-        Expr.raw_binop Ty_none Mul a b
-      | ( "fp.div"
-        , [ { node = Symbol { name = Simple "roundNearestTiesToEven"; _ }; _ }
-          ; a
-          ; b
-          ] ) ->
-        Expr.raw_binop Ty_none Div a b
+      | "fp.add", [ rm; a; b ] -> make_fp_binop symbol Add rm a b
+      | "fp.sub", [ rm; a; b ] -> make_fp_binop symbol Sub rm a b
+      | "fp.mul", [ rm; a; b ] -> make_fp_binop symbol Mul rm a b
+      | "fp.div", [ rm; a; b ] -> make_fp_binop symbol Div rm a b
       | ( "fp.sqrt"
         , [ { node = Symbol { name = Simple "roundNearestTiesToEven"; _ }; _ }
           ; a
           ] ) ->
         Expr.raw_unop Ty_none Sqrt a
       | "fp.rem", [ a; b ] -> Expr.raw_binop Ty_none Rem a b
-      | ( "fp.roundToIntegral"
-        , [ { node = Symbol { name = Simple "roundNearestTiesToEven"; _ }; _ }
-          ; a
-          ] ) ->
-        Expr.raw_unop Ty_none Nearest a
-      | ( "fp.roundToIntegral"
-        , [ { node = Symbol { name = Simple "roundTowardPositive"; _ }; _ }; a ]
-        ) ->
-        Expr.raw_unop Ty_none Ceil a
-      | ( "fp.roundToIntegral"
-        , [ { node = Symbol { name = Simple "roundTowardNegative"; _ }; _ }; a ]
-        ) ->
-        Expr.raw_unop Ty_none Floor a
-      | ( "fp.roundToIntegral"
-        , [ { node = Symbol { name = Simple "roundTowardZero"; _ }; _ }; a ] )
-        ->
-        Expr.raw_unop Ty_none Trunc a
+      | "fp.roundToIntegral", [ rm; a ] -> begin
+        match Expr.view rm with
+        | Symbol { name = Simple "roundNearestTiesToEven"; _ } ->
+          Expr.raw_unop Ty_none Nearest a
+        | Symbol { name = Simple "roundTowardPositive"; _ } ->
+          Expr.raw_unop Ty_none Ceil a
+        | Symbol { name = Simple "roundTowardNegative"; _ } ->
+          Expr.raw_unop Ty_none Floor a
+        | Symbol { name = Simple "roundTowardZero"; _ } ->
+          Expr.raw_unop Ty_none Trunc a
+        | _ -> Expr.app symbol args
+      end
       | "fp.min", [ a; b ] -> Expr.raw_binop Ty_none Min a b
       | "fp.max", [ a; b ] -> Expr.raw_binop Ty_none Max a b
       | "fp.leq", [ a; b ] -> Expr.raw_relop Ty_none Le a b
       | "fp.lt", [ a; b ] -> Expr.raw_relop Ty_none Lt a b
       | "fp.geq", [ a; b ] -> Expr.raw_relop Ty_none Ge a b
       | "fp.gt", [ a; b ] -> Expr.raw_relop Ty_none Gt a b
       | "fp.eq", [ a; b ] -> Expr.raw_relop Ty_none Eq a b
-      | _, l ->
+      | _ ->
         Log.debug (fun k -> k "apply: unknown %a making app" Symbol.pp symbol);
-        Expr.app symbol l )
+        Expr.app symbol args )
     | Symbol ({ name = Simple _; namespace = Attr; _ } as attr) ->
       Log.debug (fun k -> k "apply: unknown %a making app" Symbol.pp attr);
       Expr.app attr args