From 7b2ed97ba7539bf9b5e1c2ca56b66b61ccc25fd1 Mon Sep 17 00:00:00 2001 From: N1ark Date: Sun, 15 Sep 2024 00:26:08 +0100 Subject: [PATCH] Remove fixes entirely? --- GillianCore/engine/Abstraction/PState.ml | 12 +- GillianCore/engine/BiAbduction/BiState.ml | 44 +++++-- .../engine/concrete_semantics/CState.ml | 8 +- GillianCore/engine/general_semantics/state.ml | 5 +- .../engine/symbolic_semantics/SState.ml | 115 ++---------------- 5 files changed, 47 insertions(+), 137 deletions(-) diff --git a/GillianCore/engine/Abstraction/PState.ml b/GillianCore/engine/Abstraction/PState.ml index 6a9b42e5..200377d4 100644 --- a/GillianCore/engine/Abstraction/PState.ml +++ b/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 diff --git a/GillianCore/engine/BiAbduction/BiState.ml b/GillianCore/engine/BiAbduction/BiState.ml index b067d2ed..d096e622 100644 --- a/GillianCore/engine/BiAbduction/BiState.ml +++ b/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) diff --git a/GillianCore/engine/concrete_semantics/CState.ml b/GillianCore/engine/concrete_semantics/CState.ml index e5585514..71bb9c00 100644 --- a/GillianCore/engine/concrete_semantics/CState.ml +++ b/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 = diff --git a/GillianCore/engine/general_semantics/state.ml b/GillianCore/engine/general_semantics/state.ml index e3960dbd..c677d0e4 100644 --- a/GillianCore/engine/general_semantics/state.ml +++ b/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 diff --git a/GillianCore/engine/symbolic_semantics/SState.ml b/GillianCore/engine/symbolic_semantics/SState.ml index cef67ca7..9b6b0526 100644 --- a/GillianCore/engine/symbolic_semantics/SState.ml +++ b/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