From 02c25936578389f1bd8f58775f94f61313b6fd0e Mon Sep 17 00:00:00 2001 From: N1ark Date: Sat, 14 Sep 2024 23:45:00 +0100 Subject: [PATCH] Remove `FSpecVars`?? --- Gillian-C/lib/MonadicSMemory.ml | 30 +++---- Gillian-JS/lib/Semantics/JSILSMemory.ml | 83 ++++++++----------- .../symbolic_semantics/Legacy_s_memory.ml | 2 +- .../engine/symbolic_semantics/SMemory.ml | 2 +- .../engine/symbolic_semantics/SState.ml | 63 +++++--------- GillianCore/monadic/MonadicSMemory.ml | 2 +- wisl/lib/semantics/wislSMemory.ml | 5 +- 7 files changed, 72 insertions(+), 115 deletions(-) diff --git a/Gillian-C/lib/MonadicSMemory.ml b/Gillian-C/lib/MonadicSMemory.ml index 28abef50..8cbb2d1a 100644 --- a/Gillian-C/lib/MonadicSMemory.ml +++ b/Gillian-C/lib/MonadicSMemory.ml @@ -903,7 +903,6 @@ let get_fixes err = let new_var_e1 = Expr.LVar new_var1 in let new_var2 = LVar.alloc () in let new_var_e2 = Expr.LVar new_var2 in - let set = SS.add new_var2 (SS.singleton new_var1) in let value = Expr.EList [ new_var_e1; new_var_e2 ] in let null_typ = if Compcert.Archi.ptr64 then Expr.string long_type @@ -911,13 +910,12 @@ let get_fixes err = in let null_ptr = Expr.EList [ null_typ; Expr.int 0 ] in [ - ( [ - single ~loc ~ofs ~chunk ~sval:value ~perm; - Asrt.Types - [ (new_var_e1, Type.ObjectType); (new_var_e2, Type.IntType) ]; - ], - set ); - ([ single ~loc ~ofs ~chunk ~sval:null_ptr ~perm ], SS.empty); + [ + single ~loc ~ofs ~chunk ~sval:value ~perm; + Asrt.Types + [ (new_var_e1, Type.ObjectType); (new_var_e2, Type.IntType) ]; + ]; + [ single ~loc ~ofs ~chunk ~sval:null_ptr ~perm ]; ] | _ -> let type_str, type_gil = @@ -928,23 +926,19 @@ let get_fixes err = | _ -> (int_type, Type.IntType) in let new_var = LVar.alloc () in - let set = SS.singleton new_var in let new_var_e = Expr.LVar new_var in let value = Expr.EList [ Expr.string type_str; new_var_e ] in [ - ( [ - single ~loc ~ofs ~chunk ~sval:value ~perm; - Asrt.Types [ (new_var_e, type_gil) ]; - ], - set ); + [ + single ~loc ~ofs ~chunk ~sval:value ~perm; + Asrt.Types [ (new_var_e, type_gil) ]; + ]; ] in (* Additional fix for store operation to handle case of unitialized memory *) let fixes = if is_store then - ( [ hole ~loc ~low:ofs ~high:(offset_by_chunk ofs chunk) ~perm ], - SS.empty ) - :: fixes + [ hole ~loc ~low:ofs ~high:(offset_by_chunk ofs chunk) ~perm ] :: fixes else fixes in fixes @@ -961,7 +955,7 @@ let get_fixes err = | InvalidLocation loc -> let new_loc = ALoc.alloc () in let new_expr = Expr.ALoc new_loc in - [ ([ Asrt.Pure (Eq (new_expr, loc)) ], SS.empty) ] + [ [ Asrt.Pure (Eq (new_expr, loc)) ] ] | SHeapTreeErr { at_locations; diff --git a/Gillian-JS/lib/Semantics/JSILSMemory.ml b/Gillian-JS/lib/Semantics/JSILSMemory.ml index 21d92d67..9cf0a69e 100644 --- a/Gillian-JS/lib/Semantics/JSILSMemory.ml +++ b/Gillian-JS/lib/Semantics/JSILSMemory.ml @@ -597,7 +597,7 @@ module M = struct let prop_abduce_none_in_js = [ "@call" ] let prop_abduce_both_in_js = [ "hasOwnProperty" ] - type fix_result = Asrt.t list * Containers.SS.t + type fix_result = Asrt.t list let complete_fix_js (i_fix : i_fix_t) : fix_result list = match i_fix with @@ -607,11 +607,10 @@ module M = struct however it only seemed to add the binding without creating any state, so did it really "do" anything? Bi-abduction is broken for Gillian-JS anyways. *) let al = ALoc.alloc () in - [ ([ Asrt.Pure (Eq (ALoc al, v)) ], Containers.SS.empty) ] + [ [ Asrt.Pure (Eq (ALoc al, v)) ] ] | FCell (l, p) -> ( let none_fix () = - ( [ Asrt.GA (JSILNames.aCell, [ l; p ], [ Lit Nono ]) ], - Containers.SS.empty ) + [ Asrt.GA (JSILNames.aCell, [ l; p ], [ Lit Nono ]) ] in let some_fix () = @@ -632,13 +631,12 @@ module M = struct Lit (Bool true); ] in - ( [ - Asrt.GA (JSILNames.aCell, [ l; p ], [ descriptor ]); - Asrt.Pure asrt_empty; - Asrt.Pure asrt_none; - Asrt.Pure asrt_list; - ], - Containers.SS.singleton vvar ) + [ + Asrt.GA (JSILNames.aCell, [ l; p ], [ descriptor ]); + Asrt.Pure asrt_empty; + Asrt.Pure asrt_none; + Asrt.Pure asrt_list; + ] in match p with @@ -651,26 +649,25 @@ module M = struct let al = ALoc.alloc () in let mloc = Expr.ALoc al in [ - ( [ - Asrt.Pure (Eq (ALoc al, l)); - Asrt.GA (JSILNames.aMetadata, [ l ], [ mloc ]); - Asrt.GA (JSILNames.aMetadata, [ mloc ], [ Lit Null ]); - Asrt.GA - ( JSILNames.aCell, - [ mloc; Lit (String "@class") ], - [ Lit (String "Object") ] ); - Asrt.GA - ( JSILNames.aCell, - [ mloc; Lit (String "@extensible") ], - [ Lit (Bool true) ] ); - Asrt.GA - ( JSILNames.aCell, - [ mloc; Lit (String "@proto") ], - [ Lit (Loc JS2JSIL_Helpers.locObjPrototype) ] ); - ], - Containers.SS.empty ); + [ + Asrt.Pure (Eq (ALoc al, l)); + Asrt.GA (JSILNames.aMetadata, [ l ], [ mloc ]); + Asrt.GA (JSILNames.aMetadata, [ mloc ], [ Lit Null ]); + Asrt.GA + ( JSILNames.aCell, + [ mloc; Lit (String "@class") ], + [ Lit (String "Object") ] ); + Asrt.GA + ( JSILNames.aCell, + [ mloc; Lit (String "@extensible") ], + [ Lit (Bool true) ] ); + Asrt.GA + ( JSILNames.aCell, + [ mloc; Lit (String "@proto") ], + [ Lit (Loc JS2JSIL_Helpers.locObjPrototype) ] ); + ]; ] - | FPure f -> [ ([ Asrt.Pure f ], Containers.SS.empty) ] + | FPure f -> [ [ Asrt.Pure f ] ] (* Fix completion: simple *) let complete_fix_jsil (i_fix : i_fix_t) : fix_result list = @@ -678,37 +675,27 @@ module M = struct | FLoc v -> (* Get a fresh location *) let al = ALoc.alloc () in - [ ([ Asrt.Pure (Eq (ALoc al, v)) ], Containers.SS.empty) ] + [ [ Asrt.Pure (Eq (ALoc al, v)) ] ] | FCell (l, p) -> (* Fresh variable to denote the property value *) let vvar = LVar.alloc () in let v : vt = LVar vvar in (* Value is not none - we always bi-abduce presence *) let not_none : Formula.t = Not (Eq (v, Lit Nono)) in - [ - ( [ Asrt.GA (JSILNames.aCell, [ l; p ], [ v ]); Asrt.Pure not_none ], - Containers.SS.singleton vvar ); - ] + [ [ Asrt.GA (JSILNames.aCell, [ l; p ], [ v ]); Asrt.Pure not_none ] ] | FMetadata l -> (* Fresh variable to denote the property value *) let vvar = LVar.alloc () in let v : vt = LVar vvar in let not_none : Formula.t = Not (Eq (v, Lit Nono)) in - [ - ( [ Asrt.GA (JSILNames.aMetadata, [ l ], [ v ]); Asrt.Pure not_none ], - Containers.SS.singleton vvar ); - ] - | FPure f -> [ ([ Asrt.Pure f ], Containers.SS.empty) ] + [ [ Asrt.GA (JSILNames.aMetadata, [ l ], [ v ]); Asrt.Pure not_none ] ] + | FPure f -> [ [ Asrt.Pure f ] ] (* An error can have multiple fixes *) let get_fixes (err : err_t) : fix_result list = let pp_fix_result ft res = let open Fmt in - let fixes, svars = res in - pf ft "@[@[[[ %a ]]@]@\n@[spec vars: %a@]@]" - (list ~sep:comma Asrt.pp) fixes - (iter ~sep:comma Containers.SS.iter string) - svars + pf ft "@[@[[[ %a ]]@]@\n@]" (list ~sep:comma Asrt.pp) res in let _, fixes, _ = err in L.verbose (fun m -> @@ -727,11 +714,7 @@ module M = struct let completed_ifixes = List_utils.list_product completed_ifixes in let completed_ifixes : fix_result list = List.map - (fun fixes -> - List.fold_right - (fun (fix, svars) (fix', svars') -> - (fix @ fix', Containers.SS.union svars svars')) - fixes ([], Containers.SS.empty)) + (fun fixes -> List.fold_right List.append fixes []) completed_ifixes in diff --git a/GillianCore/engine/symbolic_semantics/Legacy_s_memory.ml b/GillianCore/engine/symbolic_semantics/Legacy_s_memory.ml index d7f03e6c..07fd9b00 100644 --- a/GillianCore/engine/symbolic_semantics/Legacy_s_memory.ml +++ b/GillianCore/engine/symbolic_semantics/Legacy_s_memory.ml @@ -65,7 +65,7 @@ module type S = sig val pp_err : Format.formatter -> err_t -> unit val get_failing_constraint : err_t -> Formula.t val can_fix : err_t -> bool - val get_fixes : err_t -> (Asrt.t list * Containers.SS.t) list + val get_fixes : err_t -> Asrt.t list list val sure_is_nonempty : t -> bool end diff --git a/GillianCore/engine/symbolic_semantics/SMemory.ml b/GillianCore/engine/symbolic_semantics/SMemory.ml index a081cbaa..0ca184d6 100644 --- a/GillianCore/engine/symbolic_semantics/SMemory.ml +++ b/GillianCore/engine/symbolic_semantics/SMemory.ml @@ -59,7 +59,7 @@ module type S = sig val get_recovery_tactic : t -> err_t -> vt Recovery_tactic.t val pp_err : Format.formatter -> err_t -> unit val get_failing_constraint : err_t -> Formula.t - val get_fixes : err_t -> (Asrt.t list * Containers.SS.t) list + val get_fixes : err_t -> Asrt.t list list val can_fix : err_t -> bool val sure_is_nonempty : t -> bool diff --git a/GillianCore/engine/symbolic_semantics/SState.ml b/GillianCore/engine/symbolic_semantics/SState.ml index b151c3f8..cef67ca7 100644 --- a/GillianCore/engine/symbolic_semantics/SState.ml +++ b/GillianCore/engine/symbolic_semantics/SState.ml @@ -54,7 +54,7 @@ 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 = Fix of Asrt.t | FSpecVars of SS.t + 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 @@ -677,12 +677,7 @@ module Make (SMemory : SMemory.S) : let mem_constraints ({ heap; _ } : t) : Formula.t list = SMemory.mem_constraints heap - let pp_fix fmt = function - | Fix mf -> Fmt.pf fmt "Fix(%a)" Asrt.pp mf - | FSpecVars vs -> - Fmt.pf fmt "FSVar(@[%a@])" - (Fmt.iter ~sep:Fmt.comma SS.iter Fmt.string) - vs + let pp_fix = Asrt.pp let get_recovery_tactic (state : t) (errs : err_t list) : vt Recovery_tactic.t = @@ -723,21 +718,19 @@ module Make (SMemory : SMemory.S) : let normalise_fix (pfs : PFS.t) (gamma : Type_env.t) (fix : fix_t list) : fix_t list option = - let gafixes, pfs', spec_vars, types, asrts = + let gafixes, pfs', types = List.fold_right - (fun fix (mfix, pfs, spec_vars, types, asrts) -> + (fun fix (mfix, pfs, types) -> match fix with - | Fix Emp | Fix (Pure True) -> (mfix, pfs, spec_vars, types, asrts) - | Fix (GA _ as ga) -> (ga :: mfix, pfs, spec_vars, types, asrts) - | Fix (Types ts) -> (mfix, pfs, spec_vars, ts @ types, asrts) - | Fix (Pure pf') -> (mfix, pf' :: pfs, spec_vars, types, asrts) - | Fix (Pred _) | Fix (Wand _) | Fix (Star _) -> + | 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") - | FSpecVars spec_vars' -> - (mfix, pfs, SS.union spec_vars' spec_vars, types, asrts)) - fix ([], [], SS.empty, [], []) + "Invalid fix type: Pred, Wand or Star found")) + fix ([], [], []) in (* Check SAT for some notion of checking SAT *) @@ -749,13 +742,9 @@ module Make (SMemory : SMemory.S) : None | Some gamma' when FOSolver.check_satisfiability (PFS.to_list pfs @ pfs') gamma' -> - let pfixes = List.map (fun pfix -> Fix (Pure pfix)) pfs' in - let mfixes = List.map (fun fix -> Fix fix) gafixes in - let ftys = if types = [] then [] else [ Fix (Types types) ] in - let sfixes = - if SS.is_empty spec_vars then [] else [ FSpecVars spec_vars ] - in - Some (ftys @ sfixes @ pfixes @ asrts @ mfixes) + 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 @@ -769,14 +758,9 @@ module Make (SMemory : SMemory.S) : let { pfs; gamma; _ } = state in let one_step_fixes : fix_t list list = match err with - | EMem err -> - List.map - (fun (fixes, spec_vars) -> - List.map (fun pf -> Fix pf) fixes - @ if spec_vars == SS.empty then [] else [ FSpecVars spec_vars ]) - (SMemory.get_fixes err) + | EMem err -> SMemory.get_fixes err | EPure f -> - let result = [ [ Fix (Pure f) ] ] in + let result = [ [ Asrt.Pure f ] ] in L.verbose (fun m -> m "@[Memory: Fixes found:@\n%a@]" (Fmt.list ~sep:(Fmt.any "@\n") pp_fixes) @@ -786,7 +770,7 @@ module Make (SMemory : SMemory.S) : let result = (List.map (List.map (function - | Asrt.Pure fix -> Fix (Pure fix) + | Asrt.Pure _ as fix -> fix | _ -> raise (Exceptions.Impossible @@ -837,30 +821,27 @@ module Make (SMemory : SMemory.S) : let { heap; store; pfs; gamma; spec_vars } = this_state in match fix with (* Apply fix in memory - this may change the pfs and gamma *) - | Fix Emp -> [ this_state ] - | Fix (GA (name, ins, outs)) -> + | 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 } - | Fix (Pure f) -> + | Pure f -> PFS.extend pfs f; [ this_state ] - | Fix (Types types) -> ( + | 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 ]) - | Fix (Star _) | Fix (Wand _) | Fix (Pred _) -> + | Star _ | Wand _ | Pred _ -> raise (Failure "DEATH: apply_fixes: Star, Wand, and Pred not implemented.") - | FSpecVars vars -> - let spec_vars = SS.union vars spec_vars in - [ { heap; store; pfs; gamma; spec_vars } ] in let result = List.fold_left apply_fix [ state ] fixes in diff --git a/GillianCore/monadic/MonadicSMemory.ml b/GillianCore/monadic/MonadicSMemory.ml index a794fe8b..c53d1376 100644 --- a/GillianCore/monadic/MonadicSMemory.ml +++ b/GillianCore/monadic/MonadicSMemory.ml @@ -47,7 +47,7 @@ module type S = sig val get_recovery_tactic : t -> err_t -> vt Recovery_tactic.t val pp_err : Format.formatter -> err_t -> unit val get_failing_constraint : err_t -> Formula.t - val get_fixes : err_t -> (Asrt.t list * Containers.SS.t) list + val get_fixes : err_t -> Asrt.t list list val can_fix : err_t -> bool val pp_by_need : Containers.SS.t -> Format.formatter -> t -> unit val get_print_info : Containers.SS.t -> t -> Containers.SS.t * Containers.SS.t diff --git a/wisl/lib/semantics/wislSMemory.ml b/wisl/lib/semantics/wislSMemory.ml index c698e3a5..512a198e 100644 --- a/wisl/lib/semantics/wislSMemory.ml +++ b/wisl/lib/semantics/wislSMemory.ml @@ -309,14 +309,13 @@ let get_fixes (err : err_t) = | MissingResource (Cell, loc, Some ofs) -> let new_var = LVar.alloc () in let value = Expr.LVar new_var in - let set = SS.singleton new_var in let loc = Expr.loc_from_loc_name loc in let ga = WislLActions.str_ga WislLActions.Cell in - [ ([ Asrt.GA (ga, [ loc; ofs ], [ value ]) ], set) ] + [ [ Asrt.GA (ga, [ loc; ofs ], [ value ]) ] ] | InvalidLocation loc -> let new_loc = ALoc.alloc () in let new_expr = Expr.ALoc new_loc in - [ ([ Asrt.Pure (Eq (new_expr, loc)) ], SS.empty) ] + [ [ Asrt.Pure (Eq (new_expr, loc)) ] ] | _ -> [] let can_fix = function