Fix model parsing

CHANGES.md

@@ -4,6 +4,12 @@
 ### Changed
 ### Fixed
 
+## v0.6.1
+
+### Fixed
+
+- Fixes model parsing in the JSON format.
+
 ## v0.6.0
 
 ### Added

src/smtml/model.ml

@@ -62,7 +62,7 @@ let to_json (model : t) : Yojson.t =
     ]} *)
 let to_json_string model =
   let model = to_json model in
-  Fmt.str "%a" Yojson.pp model
+  Fmt.str "%a" (Yojson.pretty_print ~std:true) model
 
 let to_scfg ~no_value model =
   let open Scfg.Types in

src/smtml/num.ml

@@ -95,4 +95,4 @@ let of_string (cast : Ty.t) value =
     | Some n -> Ok (F64 (Int64.bits_of_float n)) )
   | _ -> Fmt.error_msg "invalid value, expected num"
 
-let to_json (n : t) : Yojson.Basic.t = `String (to_string n)
+let to_json (n : t) : Yojson.Basic.t = `String (Fmt.str "%a" pp_no_type n)

test/unit/test_model.ml

@@ -15,8 +15,6 @@ let test_to_json () =
   let model_to_json = Model.to_json model in
   Format.printf "%a@." (Yojson.pretty_print ~std:true) model_to_json
 
-let test_serialization () = test_to_json ()
-
 let test_of_json () =
   let open Result in
   let model_str =
@@ -25,14 +23,50 @@ let test_of_json () =
         "model" : {
           "x_0" : { "ty" : "int", "value" : 42 },
           "x_1" : { "ty" : "bool", "value" : true },
-          "x_2" : { "ty" : "f32", "value" : 42.42 }
+          "x_2" : { "ty" : "f32", "value" : 42.42 },
+          "x_3" : { "ty" : "i64", "value" : -13333337 }
         }
       }
     |}
   in
   let model = Model.Parse.Json.from_string model_str in
   assert (match model with Ok _ -> true | _ -> false)
 
+let test_rt_json () =
+  let x = Symbol.make (Ty_bitv 32) "x" in
+  let y = Symbol.make (Ty_bitv 64) "y" in
+  let z = Symbol.make (Ty_fp 32) "y" in
+  let orig_model : Model.t =
+    let tbl = Hashtbl.create 16 in
+    List.iter
+      (fun ((s, v) : Symbol.t * Value.t) -> Hashtbl.replace tbl s v)
+      [ (x, Num (I32 Int32.min_int))
+      ; (y, Num (I64 Int64.max_int))
+      ; (z, Num (F32 1084227584l))
+      ];
+    tbl
+  in
+  let json_model = Model.to_json_string orig_model in
+  match Model.Parse.Json.from_string json_model with
+  | Error (`Msg err) -> Fmt.failwith "%s" err
+  | Ok model -> begin
+    let x_val = Model.evaluate model x in
+    let y_val = Model.evaluate model y in
+    let z_val = Model.evaluate model z in
+    match (x_val, y_val, z_val) with
+    | Some x_val, Some y_val, Some z_val ->
+      assert (
+        Value.equal x_val (Num (I32 Int32.min_int))
+        && Value.equal y_val (Num (I64 Int64.max_int))
+        && Value.equal z_val (Num (F32 (Int32.bits_of_float 5.0))) )
+    | _ -> assert false
+  end
+
+let test_json () =
+  test_to_json ();
+  test_of_json ();
+  test_rt_json ()
+
 let test_of_scfg () =
   let open Result in
   let model_str =
@@ -41,16 +75,15 @@ let test_of_scfg () =
         symbol x_0 int 42
         symbol x_1 bool true
         symbol x_2 f32 42.42
+        symbol x_3 i64 -13333337
       }
     |}
   in
   let model = Model.Parse.Scfg.from_string model_str in
   assert (match model with Ok _ -> true | _ -> false)
 
-let test_deserialization () =
-  test_of_json ();
-  test_of_scfg ()
+let test_scfg () = test_of_scfg ()
 
 let () =
-  test_serialization ();
-  test_deserialization ()
+  test_json ();
+  test_scfg ()