Remove fixes entirely?

GillianCore/engine/Abstraction/PState.ml

@@ -66,7 +66,6 @@ module Make (State : SState.S) :
   type abs_t = Preds.abs_t
   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 [@@deriving yojson]
 
   exception Internal_State_Error of err_t list * t
@@ -1186,7 +1185,6 @@ module Make (State : SState.S) :
 
   let is_overlapping_asrt (a : string) : bool = State.is_overlapping_asrt a
   let pp_err = State.pp_err
-  let pp_fix = State.pp_fix
   let get_recovery_tactic astate vs = State.get_recovery_tactic astate.state vs
 
   let try_recovering (astate : t) (tactic : vt Recovery_tactic.t) :
@@ -1196,15 +1194,9 @@ module Make (State : SState.S) :
   let get_failing_constraint = State.get_failing_constraint
   let can_fix = State.can_fix
 
-  let get_fixes (astate : t) (errs : err_t) : fix_t list list =
+  let get_fixes (errs : err_t) =
     L.verbose (fun m -> m "AState: get_fixes");
-    State.get_fixes astate.state errs
-
-  let apply_fixes (astate : t) (fixes : fix_t list) : t list =
-    L.verbose (fun m -> m "AState: apply_fixes");
-    match State.apply_fixes astate.state fixes with
-    | [ state ] -> [ { astate with state } ]
-    | states -> List.map (copy_with_state astate) states
+    State.get_fixes errs
 
   let get_equal_values astate = State.get_equal_values astate.state
   let get_heap astate = State.get_heap astate.state

GillianCore/engine/BiAbduction/BiState.ml

@@ -13,7 +13,6 @@ module Make (State : SState.S) = struct
   type store_t = SStore.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
 
@@ -194,6 +193,31 @@ module Make (State : SState.S) = struct
     in
     SVal.SESubst.init bindings
 
+  let fix_list_apply s =
+    let open Syntaxes.List in
+    List.fold_left
+      (fun acc a ->
+        let* this_state = acc in
+        match a with
+        | Asrt.Emp -> [ this_state ]
+        | Pure f ->
+            State.assume_a ~matching:true this_state [ f ] |> Option.to_list
+        | Types types ->
+            types
+            |> List.fold_left
+                 (fun ac (e, t) ->
+                   match ac with
+                   | None -> None
+                   | Some s -> State.assume_t s e t)
+                 (Some this_state)
+            |> Option.to_list
+        | GA (corepred, ins, outs) ->
+            State.produce_core_pred corepred this_state (ins @ outs)
+        | Star _ -> raise (Failure "DEATH. fix_list_apply star")
+        | Wand _ -> raise (Failure "DEATH. fix_list_apply wand")
+        | Pred _ -> raise (Failure "DEATH. fix_list_apply pred"))
+      [ s ]
+
   type post_res = (Flag.t * Asrt.t list) option
 
   let match_
@@ -238,12 +262,12 @@ module Make (State : SState.S) = struct
                 [])
               else (
                 L.verbose (fun m -> m "May be able to fix!!!");
-                let* fixes = State.get_fixes state err in
+                let* fixes = State.get_fixes err in
                 (* TODO: a better implementation here might be to say that apply_fix returns a list of fixed states, possibly empty *)
                 let state' = State.copy state in
                 let af_state' = State.copy af_state in
-                let* state' = State.apply_fixes state' fixes in
-                let* af_state' = State.apply_fixes af_state' fixes in
+                let* state' = fix_list_apply state' fixes in
+                let* af_state' = fix_list_apply af_state' fixes in
                 L.verbose (fun m -> m "BEFORE THE SIMPLIFICATION!!!");
                 let new_subst, states = State.simplify state' in
                 let state' =
@@ -422,12 +446,9 @@ module Make (State : SState.S) = struct
 
   (* to throw errors: *)
 
-  let get_fixes (_ : t) (_ : err_t) : fix_t list list =
+  let get_fixes (_ : err_t) : Asrt.t list list =
     raise (Failure "get_fixes not implemented in MakeBiState")
 
-  let apply_fixes (_ : t) (_ : fix_t list) : t list =
-    raise (Failure "apply_fixes not implemented in MakeBiState")
-
   let get_recovery_tactic (_ : t) (_ : err_t list) =
     raise (Failure "get_recovery_tactic not implemented in MakeBiState")
 
@@ -443,7 +464,6 @@ module Make (State : SState.S) = struct
 
   let is_overlapping_asrt (a : string) : bool = State.is_overlapping_asrt a
   let pp_err f e = State.pp_err f (unlift_error e)
-  let pp_fix = State.pp_fix
   let get_failing_constraint e = State.get_failing_constraint (unlift_error e)
   let can_fix e = State.can_fix (unlift_error e)
 
@@ -458,14 +478,14 @@ module Make (State : SState.S) = struct
     | 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
+        match State.get_fixes err with
         | [] -> [] (* No fix, we stop *)
         | fixes ->
             let* fix = fixes in
             let state' = State.copy state in
             let af_state' = State.copy af_state in
-            let* state' = State.apply_fixes state' fix in
-            let* af_state' = State.apply_fixes af_state' fix in
+            let* state' = fix_list_apply state' fix in
+            let* af_state' = fix_list_apply af_state' fix in
             execute_action action
               { procs; state = state'; af_state = af_state' }
               args)

GillianCore/engine/concrete_semantics/CState.ml

@@ -32,7 +32,6 @@ end = struct
   type store_t = CStore.t
   type heap_t = CMemory.t
   type t = CMemory.t * CStore.t * vt list
-  type fix_t
   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
@@ -187,8 +186,6 @@ end = struct
   let mem_constraints (_ : t) : Formula.t list =
     raise (Failure "DEATH. mem_constraints")
 
-  let pp_fix _ _ = raise (Failure "str_of_fix from non-symbolic state.")
-
   let get_recovery_tactic _ =
     raise (Failure "get_recovery_tactic from non-symbolic state.")
 
@@ -212,12 +209,9 @@ end = struct
   let can_fix (_ : err_t) : bool = false
   let get_failing_constraint (_ : err_t) : Formula.t = True
 
-  let get_fixes (_ : t) (_ : err_t) : fix_t list list =
+  let get_fixes (_ : err_t) : Asrt.t list list =
     raise (Failure "Concrete: get_fixes not implemented in CState.Make")
 
-  let apply_fixes (_ : t) (_ : fix_t list) : t list =
-    raise (Failure "Concrete: apply_fixes not implemented in CState.Make")
-
   let get_equal_values _ vs = vs
 
   let get_heap state =

GillianCore/engine/general_semantics/state.ml

@@ -24,7 +24,6 @@ module type S = sig
   type m_err_t [@@deriving yojson]
 
   type err_t = (m_err_t, vt) StateErr.t [@@deriving yojson, show]
-  type fix_t
 
   exception Internal_State_Error of err_t list * t
 
@@ -93,7 +92,6 @@ module type S = sig
     unit
 
   val pp_err : Format.formatter -> err_t -> unit
-  val pp_fix : Format.formatter -> fix_t -> unit
   val get_recovery_tactic : t -> err_t list -> vt Recovery_tactic.t
 
   (** State Copy *)
@@ -146,8 +144,7 @@ module type S = sig
   val mem_constraints : t -> Formula.t list
   val can_fix : err_t -> bool
   val get_failing_constraint : err_t -> Formula.t
-  val get_fixes : t -> err_t -> fix_t list list
-  val apply_fixes : t -> fix_t list -> t list
+  val get_fixes : err_t -> Asrt.t list list
   val get_equal_values : t -> vt list -> vt list
   val get_heap : t -> heap_t
 end

GillianCore/engine/symbolic_semantics/SState.ml

@@ -54,7 +54,6 @@ module Make (SMemory : SMemory.S) :
 
   type variants_t = (string, Expr.t option) Hashtbl.t [@@deriving yojson]
   type init_data = SMemory.init_data
-  type fix_t = Asrt.t
   type err_t = (m_err_t, vt) StateErr.t [@@deriving yojson, show]
   type action_ret = (t * vt list, err_t) result list
 
@@ -330,8 +329,7 @@ module Make (SMemory : SMemory.S) :
             Expr.pp e msg (Fmt.Dump.list Formula.pp) ps);
       None
 
-  let assume_t (state : t) (v : vt) (t : Type.t) : t option =
-    let { gamma; _ } = state in
+  let assume_t ({ gamma; _ } as state : t) (v : vt) (t : Type.t) : t option =
     match Typing.reverse_type_lexpr true gamma [ (v, t) ] with
     | None -> None
     | Some gamma' ->
@@ -677,8 +675,6 @@ module Make (SMemory : SMemory.S) :
   let mem_constraints ({ heap; _ } : t) : Formula.t list =
     SMemory.mem_constraints heap
 
-  let pp_fix = Asrt.pp
-
   let get_recovery_tactic (state : t) (errs : err_t list) : vt Recovery_tactic.t
       =
     let { heap; pfs; _ } = state in
@@ -716,47 +712,13 @@ module Make (SMemory : SMemory.S) :
   let get_failing_constraint (err : err_t) : Formula.t =
     StateErr.get_failing_constraint err SMemory.get_failing_constraint
 
-  let normalise_fix (pfs : PFS.t) (gamma : Type_env.t) (fix : fix_t list) :
-      fix_t list option =
-    let gafixes, pfs', types =
-      List.fold_right
-        (fun fix (mfix, pfs, types) ->
-          match fix with
-          | Asrt.Emp | Pure True -> (mfix, pfs, types)
-          | GA _ as ga -> (ga :: mfix, pfs, types)
-          | Types ts -> (mfix, pfs, ts @ types)
-          | Pure pf' -> (mfix, pf' :: pfs, types)
-          | Pred _ | Wand _ | Star _ ->
-              raise
-                (Exceptions.Impossible
-                   "Invalid fix type: Pred, Wand or Star found"))
-        fix ([], [], [])
-    in
-
-    (* Check SAT for some notion of checking SAT *)
-    let gamma' = Type_env.copy gamma in
-    let gamma' = Typing.reverse_type_lexpr true gamma' types in
-    match gamma' with
-    | None ->
-        L.verbose (fun m -> m "Warning: invalid fix, types are inconsistent.");
-        None
-    | Some gamma'
-      when FOSolver.check_satisfiability (PFS.to_list pfs @ pfs') gamma' ->
-        let pfixes = List.map (fun pfix -> Asrt.Pure pfix) pfs' in
-        let ftys = if types = [] then [] else [ Asrt.Types types ] in
-        Some (ftys @ pfixes @ gafixes)
-    | Some _ ->
-        L.verbose (fun m -> m "Warning: invalid fix.");
-        None
-
   (* get_fixes returns a list of possible fixes.
-     Each "fix" is actually a list of fix_t, each of which have to be applied to the same state *)
-  let get_fixes (state : t) (err : err_t) : fix_t list list =
+     Each "fix" is actually a list of assertions, each of which have to be applied to the same state *)
+  let get_fixes (err : err_t) : Asrt.t list list =
     let pp_fixes fmt fixes =
-      Fmt.pf fmt "[[ %a ]]" (Fmt.list ~sep:(Fmt.any ", ") pp_fix) fixes
+      Fmt.pf fmt "[[ %a ]]" (Fmt.list ~sep:(Fmt.any ", ") Asrt.pp) fixes
     in
-    let { pfs; gamma; _ } = state in
-    let one_step_fixes : fix_t list list =
+    let one_step_fixes : Asrt.t list list =
       match err with
       | EMem err -> SMemory.get_fixes err
       | EPure f ->
@@ -787,68 +749,13 @@ module Make (SMemory : SMemory.S) :
 
     L.tmi (fun m ->
         m "All fixes before normalisation: %a"
-          Fmt.Dump.(list @@ list @@ pp_fix)
+          Fmt.Dump.(list @@ list @@ Asrt.pp)
           one_step_fixes);
-    (* Cartesian product of the fixes *)
-    let result =
-      List.filter_map
-        (fun fix ->
-          match normalise_fix pfs gamma fix with
-          | None | Some [] -> None
-          | other -> other)
-        one_step_fixes
-    in
-    L.(verbose (fun m -> m "Normalised fixes: %i" (List.length result)));
-    L.verbose (fun m ->
-        m "%a" (Fmt.list ~sep:(Fmt.any "@\n@\n") (Fmt.Dump.list pp_fix)) result);
-    result
-
-  (**
-   @param state The state on which to apply the fixes
-   @param fixes A list of fixes to apply
-
-   @return The state resulting from applying the fixes
-
-   [apply_fixes state fixes] applies the fixes [fixes] to the state [state],
-   and returns the resulting state, if successful.
-   *)
-  let apply_fixes (state : t) (fixes : fix_t list) : t list =
-    L.verbose (fun m -> m "SState: apply_fixes");
-    let apply_fix (states : t list) (fix : fix_t) : t list =
-      L.verbose (fun m -> m "applying fix: %a" pp_fix fix);
-      let open Syntaxes.List in
-      let* this_state = states in
-      let { heap; store; pfs; gamma; spec_vars } = this_state in
-      match fix with
-      (* Apply fix in memory - this may change the pfs and gamma *)
-      | Asrt.Emp -> [ this_state ]
-      | GA (name, ins, outs) ->
-          L.verbose (fun m -> m "SState: before applying fixes %a" pp state);
-          let pc = Gpc.make ~matching:false ~pfs ~gamma () in
-          let+ Gbranch.{ value = heap; pc } =
-            SMemory.produce name heap pc (ins @ outs)
-          in
-          { heap; store; pfs = pc.pfs; gamma = pc.gamma; spec_vars }
-      | Pure f ->
-          PFS.extend pfs f;
-          [ this_state ]
-      | Types types -> (
-          let gamma' = Typing.reverse_type_lexpr true gamma types in
-          match gamma' with
-          | None -> []
-          | Some gamma' ->
-              Type_env.extend gamma gamma';
-              [ this_state ])
-      | Star _ | Wand _ | Pred _ ->
-          raise
-            (Failure "DEATH: apply_fixes: Star, Wand, and Pred not implemented.")
-    in
-
-    let result = List.fold_left apply_fix [ state ] fixes in
-
-    L.verbose (fun m ->
-        m "SState: after applying fixes %a" (Fmt.Dump.list pp) result);
-    result
+    List.map
+      (fun fixes ->
+        let pure, unpure = List.partition Asrt.is_pure_asrt fixes in
+        pure @ unpure)
+      one_step_fixes
 
   let get_equal_values state les =
     let { pfs; _ } = state in