Ensure fixes are not lost when they lead to errors (GillianPlatform#302)

* Ensure fixes are not lost when they lead to errors

* Derive `yojson` in for error types

In particular in `PState.m_err_t`, `CMemory.err_t`, `CState.m_err_t`, `State.m_err_t`

---------

Co-authored-by: Sacha Ayoun <sachaayoun@gmail.com>

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 _ () = ()
 

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
 

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

GillianCore/engine/BiAbduction/Abductor.ml

@@ -229,7 +229,21 @@ module Make
           (Format.asprintf "When trying to build an MP for %s, I died!" name)
     in
     match result with
-    | RFail { error_state; _ } ->
+    | RFail { error_state; errors; _ } ->
+        (* Because of fixes, the state may have changed since between the start of execution
+           and the failure: the anti-frame might have been modified before immediately erroring.
+           BiState thus returns, with every error, the state immeditaly before the error happens
+           with any applied fixes - this is the state that should be used to ensure fixes
+           don't get lost. *)
+        let rec find_error_state (aux : SBAInterpreter.err_t list) =
+          match aux with
+          | [] -> error_state
+          | e :: errs -> (
+              match e with
+              | EState (EMem (s, _)) -> s
+              | _ -> find_error_state errs)
+        in
+        let error_state = find_error_state errors in
         let+ spec = process_spec name params state_i error_state Flag.Bug in
         add_spec spec;
         (spec, Flag.Bug)

GillianCore/engine/BiAbduction/BiState.ml

@@ -2,16 +2,18 @@ open Containers
 open Literal
 module L = Logging
 
+type 'a _t = { procs : SS.t; state : 'a; af_state : 'a } [@@deriving yojson]
+
 module Make (State : SState.S) = struct
   type heap_t = State.heap_t
-  type state_t = State.t
+  type state_t = State.t [@@deriving yojson]
   type st = SVal.SESubst.t
   type vt = Expr.t [@@deriving show, yojson]
-  type t = { procs : SS.t; state : state_t; af_state : state_t }
+  type t = state_t _t [@@deriving yojson]
   type store_t = SStore.t
-  type err_t = State.err_t [@@deriving yojson, show]
+  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 m_err_t = State.m_err_t
   type variants_t = (string, Expr.t option) Hashtbl.t [@@deriving yojson]
   type init_data = State.init_data
 
@@ -23,11 +25,29 @@ module Make (State : SState.S) = struct
       =
     { procs; state; af_state = State.init init_data }
 
+  let lift_error st : State.err_t -> err_t = function
+    | StateErr.EMem e -> StateErr.EMem (st, e)
+    | StateErr.EType (v, t, t') -> StateErr.EType (v, t, t')
+    | StateErr.EPure f -> StateErr.EPure f
+    | StateErr.EVar v -> StateErr.EVar v
+    | StateErr.EAsrt (v, f, a) -> StateErr.EAsrt (v, f, a)
+    | StateErr.EOther s -> StateErr.EOther s
+
+  let unlift_error : err_t -> State.err_t = function
+    | StateErr.EMem (_, e) -> StateErr.EMem e
+    | StateErr.EType (v, t, t') -> StateErr.EType (v, t, t')
+    | StateErr.EPure f -> StateErr.EPure f
+    | StateErr.EVar v -> StateErr.EVar v
+    | StateErr.EAsrt (v, f, a) -> StateErr.EAsrt (v, f, a)
+    | StateErr.EOther s -> StateErr.EOther s
+
+  let lift_errors st = List.map (lift_error st)
+
   let eval_expr (bi_state : t) (e : Expr.t) =
     let { state; _ } = bi_state in
     try State.eval_expr state e
     with State.Internal_State_Error (errs, _) ->
-      raise (Internal_State_Error (errs, bi_state))
+      raise (Internal_State_Error (lift_errors bi_state errs, bi_state))
 
   let get_store (bi_state : t) : SStore.t =
     let { state; _ } = bi_state in
@@ -137,10 +157,12 @@ module Make (State : SState.S) = struct
 
   let evaluate_slcmd (prog : 'a MP.prog) (lcmd : SLCmd.t) (bi_state : t) :
       (t, err_t) Res_list.t =
-    let open Res_list.Syntax in
+    let open Syntaxes.List in
     let { state; _ } = bi_state in
-    let++ state' = State.evaluate_slcmd prog lcmd state in
-    { bi_state with state = state' }
+    let+ res = State.evaluate_slcmd prog lcmd state in
+    match res with
+    | Ok state' -> Ok { bi_state with state = state' }
+    | Error err -> Error (lift_error bi_state err)
 
   let match_invariant _ _ _ _ _ =
     raise (Failure "ERROR: match_invariant called for bi-abductive execution")
@@ -422,10 +444,10 @@ module Make (State : SState.S) = struct
     State.mem_constraints state
 
   let is_overlapping_asrt (a : string) : bool = State.is_overlapping_asrt a
-  let pp_err = State.pp_err
+  let pp_err f e = State.pp_err f (unlift_error e)
   let pp_fix = State.pp_fix
-  let get_failing_constraint = State.get_failing_constraint
-  let can_fix = State.can_fix
+  let get_failing_constraint e = State.get_failing_constraint (unlift_error e)
+  let can_fix e = State.can_fix (unlift_error e)
 
   let rec execute_action
       (action : string)
@@ -435,7 +457,8 @@ module Make (State : SState.S) = struct
     let* ret = State.execute_action action state args in
     match ret with
     | Ok (state', outs) -> [ Ok ({ procs; state = state'; af_state }, outs) ]
-    | Error err when not (State.can_fix err) -> [ Error err ]
+    | Error err when not (State.can_fix err) ->
+        [ Error (lift_error { procs; state; af_state } err) ]
     | Error err -> (
         match State.get_fixes state err with
         | [] -> [] (* No fix, we stop *)
@@ -451,12 +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
-
-  let of_yojson _ =
-    failwith
-      "Please implement of_yojson to enable logging this type to a database"
-
-  let to_yojson _ =
-    failwith
-      "Please implement to_yojson to enable logging this type to a database"
+  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

GillianCore/engine/BiAbduction/BiState.mli

@@ -1,10 +1,14 @@
+type 'a _t
+
 module Make (BaseState : PState.S) : sig
   include
     State.S
-      with type vt = Expr.t
+      with type t = BaseState.t _t
+       and type vt = Expr.t
        and type st = SVal.SESubst.t
        and type store_t = SStore.t
        and type init_data = BaseState.init_data
+       and type m_err_t = BaseState.t _t * BaseState.m_err_t
 
   val make : procs:SS.t -> state:BaseState.t -> init_data:init_data -> t
   val get_components : t -> BaseState.t * BaseState.t

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

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]

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

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
 

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