Derive yojson in for error types

In particular in `PState.m_err_t`, `CMemory.err_t`, `CState.m_err_t`, `State.m_err_t`
GillianPlatform · Jul 17, 2024 · 846c7da · 846c7da
1 parent cddf0d3
commit 846c7da
Show file tree

Hide file tree

Showing 9 changed files with 11 additions and 38 deletions.
diff --git a/Gillian-C/lib/CMemory.ml b/Gillian-C/lib/CMemory.ml
@@ -6,7 +6,7 @@ module Expr = Gillian.Gil_syntax.Expr
 type init_data = Global_env.t
 type vt = Values.t
 type st = Subst.t
-type err_t = unit [@@deriving show]
+type err_t = unit [@@deriving yojson, show]
 
 let pp_err _ () = ()
 

diff --git a/Gillian-JS/lib/Semantics/JSILCMemory.ml b/Gillian-JS/lib/Semantics/JSILCMemory.ml
@@ -13,7 +13,7 @@ module M : Memory_S with type init_data = unit = struct
   type st = Subst.t
 
   (** Errors *)
-  type err_t = unit [@@deriving show]
+  type err_t = unit [@@deriving yojson, show]
 
   type action_ret = (t * vt list, err_t) result
 

diff --git a/GillianCore/engine/Abstraction/PState.ml b/GillianCore/engine/Abstraction/PState.ml
@@ -67,7 +67,7 @@ module Make (State : SState.S) :
   type state_t = State.t
   type err_t = State.err_t [@@deriving yojson, show]
   type fix_t = State.fix_t
-  type m_err_t = State.m_err_t
+  type m_err_t = State.m_err_t [@@deriving yojson]
 
   exception Internal_State_Error of err_t list * t
   exception Preprocessing_Error of MP.err list

diff --git a/GillianCore/engine/BiAbduction/BiState.ml b/GillianCore/engine/BiAbduction/BiState.ml
@@ -11,8 +11,8 @@ module Make (State : SState.S) = struct
   type vt = Expr.t [@@deriving show, yojson]
   type t = state_t _t [@@deriving yojson]
   type store_t = SStore.t
-  type m_err_t = t * State.m_err_t
-  type err_t = (m_err_t, vt) StateErr.t
+  type m_err_t = t * State.m_err_t [@@deriving yojson]
+  type err_t = (m_err_t, vt) StateErr.t [@@deriving yojson]
   type fix_t = State.fix_t
   type variants_t = (string, Expr.t option) Hashtbl.t [@@deriving yojson]
   type init_data = State.init_data
@@ -474,33 +474,6 @@ module Make (State : SState.S) = struct
 
   let get_equal_values { state; _ } = State.get_equal_values state
   let get_heap { state; _ } = State.get_heap state
-
-  (* Sadly need to hand-implement this, because m_err_t doesn't expose a yojson interface *)
-  let err_t_to_yojson : err_t -> Yojson.Safe.t = function
-    | StateErr.EMem (s, _) as e ->
-        let s' = to_yojson s in
-        let e' = State.err_t_to_yojson (unlift_error e) in
-        `List [ `String "BSEMem"; s'; e' ]
-    | e -> State.err_t_to_yojson (unlift_error e)
-
-  let err_t_of_yojson :
-      Yojson.Safe.t -> err_t Ppx_deriving_yojson_runtime.error_or =
-    let open Syntaxes.Result in
-    function
-    | `List [ `String "BSEMem"; s; e ] ->
-        let* s = of_yojson s in
-        let+ e = State.err_t_of_yojson e in
-        lift_error s e
-    | e -> (
-        let* err = State.err_t_of_yojson e in
-        match err with
-        | StateErr.EMem _ -> Error "Expected a list with two elements"
-        | StateErr.EType (v, t, t') -> Ok (StateErr.EType (v, t, t'))
-        | StateErr.EPure f -> Ok (StateErr.EPure f)
-        | StateErr.EVar v -> Ok (StateErr.EVar v)
-        | StateErr.EAsrt (v, f, a) -> Ok (StateErr.EAsrt (v, f, a))
-        | StateErr.EOther s -> Ok (StateErr.EOther s))
-
   let pp_err_t f err = State.pp_err_t f (unlift_error err)
   let show_err_t err = State.show_err_t (unlift_error err)
 end
diff --git a/GillianCore/engine/concrete_semantics/CMemory.ml b/GillianCore/engine/concrete_semantics/CMemory.ml
@@ -9,7 +9,7 @@ module type S = sig
   type st = CVal.CSubst.t
 
   (** Errors *)
-  type err_t [@@deriving show]
+  type err_t [@@deriving yojson, show]
 
   (** Type of GIL general states *)
   type t

diff --git a/GillianCore/engine/concrete_semantics/CState.ml b/GillianCore/engine/concrete_semantics/CState.ml
@@ -33,7 +33,7 @@ end = struct
   type heap_t = CMemory.t
   type t = CMemory.t * CStore.t * vt list
   type fix_t
-  type m_err_t = CMemory.err_t [@@deriving show]
+  type m_err_t = CMemory.err_t [@@deriving yojson, show]
   type err_t = (m_err_t, vt) StateErr.t [@@deriving show]
   type init_data = CMemory.init_data
   type variants_t = (string, Expr.t option) Hashtbl.t [@@deriving yojson]

diff --git a/GillianCore/engine/general_semantics/state.ml b/GillianCore/engine/general_semantics/state.ml
@@ -1,7 +1,7 @@
 (** @canonical Gillian.General.State
 
   Interface for GIL General States.
-  
+
   They are considered to be mutable. *)
 
 (** @canonical Gillian.General.State.S *)
@@ -21,7 +21,7 @@ module type S = sig
   type heap_t
 
   (** Errors *)
-  type m_err_t
+  type m_err_t [@@deriving yojson]
 
   type err_t = (m_err_t, vt) StateErr.t [@@deriving yojson, show]
   type fix_t

diff --git a/kanillian/lib/memory_model/CMemory.ml b/kanillian/lib/memory_model/CMemory.ml
@@ -3,7 +3,7 @@ open Gillian.Concrete
 type init_data = unit
 type vt = Values.t
 type st = Subst.t
-type err_t = unit [@@deriving show]
+type err_t = unit [@@deriving yojson, show]
 type t = unit
 type action_ret = (t * vt list, err_t) result
 

diff --git a/wisl/lib/semantics/wislCMemory.ml b/wisl/lib/semantics/wislCMemory.ml
@@ -4,7 +4,7 @@ module Literal = Gillian.Gil_syntax.Literal
 type init_data = unit
 type vt = Values.t
 type st = Subst.t
-type err_t = unit [@@deriving show]
+type err_t = unit [@@deriving yojson, show]
 type t = WislCHeap.t
 type action_ret = (t * vt list, err_t) result