diff --git a/Gillian-JS/lib/Debugging/JSLifter.ml b/Gillian-JS/lib/Debugging/JSLifter.ml index b8f5b887e..6f79b502f 100644 --- a/Gillian-JS/lib/Debugging/JSLifter.ml +++ b/Gillian-JS/lib/Debugging/JSLifter.ml @@ -67,7 +67,7 @@ struct node let add_memory_vars smemory get_new_scope_id (variables : Variable.ts) = - let sorted_locs_with_vals = Legacy_symbolic.sorted_locs_with_vals smemory in + let sorted_locs_with_vals = Base_symbolic.sorted_locs_with_vals smemory in let value_nodes (loc, ((properties, domain), metadata)) : Variable.t = let () = ignore properties in let properties = @@ -262,9 +262,7 @@ struct in scopes else - let sorted_locs_with_vals = - Legacy_symbolic.sorted_locs_with_vals memory - in + let sorted_locs_with_vals = Base_symbolic.sorted_locs_with_vals memory in let loc_to_scope_id = Hashtbl.create 0 in let () = List.iter diff --git a/Gillian-JS/lib/Semantics/JSILSMemory.ml b/Gillian-JS/lib/Semantics/JSILSMemory.ml index 746b33cfb..26db6d212 100644 --- a/Gillian-JS/lib/Semantics/JSILSMemory.ml +++ b/Gillian-JS/lib/Semantics/JSILSMemory.ml @@ -1,15 +1,16 @@ open Gillian open Gillian.Gil_syntax +open Gillian.Monadic +open Delayed.Syntax +open Delayed_result.Syntax open Javert_utils open Js2jsil_lib module GAsrt = Asrt module SSubst = Gillian.Symbolic.Subst module L = Logging module SVal = Gillian.Symbolic.Values -module PFS = Gillian.Symbolic.Pure_context -module Type_env = Gillian.Symbolic.Type_env module Recovery_tactic = Gillian.General.Recovery_tactic -open Gillian.Logic +module DR = Delayed_result module M = struct type init_data = unit @@ -32,11 +33,7 @@ module M = struct [@@deriving yojson, show] type err_t = vt list * i_fix_t list list * Expr.t [@@deriving yojson, show] - - type action_ret = - ( (t * vt list * Expr.t list * (string * Type.t) list) list, - err_t list ) - result + type action_ret = (t * vt list, err_t) result let pp_i_fix ft (i_fix : i_fix_t) : unit = let open Fmt in @@ -81,7 +78,7 @@ module M = struct let metadata_recovery_vals = List.fold_left (fun mrvs aloc -> - match Hashtbl.find_opt imeta aloc with + match Expr.Map.find_opt aloc imeta with | Some md -> md :: mrvs | _ -> mrvs) [] alocs @@ -94,92 +91,79 @@ module M = struct let lvars (heap : t) : Containers.SS.t = SHeap.lvars heap let alocs (heap : t) : Containers.SS.t = SHeap.alocs heap - let clean_up ?(keep = Expr.Set.empty) (heap : t) : Expr.Set.t * Expr.Set.t = - SHeap.clean_up heap; + let clean_up ?(keep = Expr.Set.empty) (_ : t) : Expr.Set.t * Expr.Set.t = (Expr.Set.empty, keep) - let substitution_in_place ~pfs:_ ~gamma:_ (subst : st) (heap : t) = - SHeap.substitution_in_place subst heap; - [ (heap, Expr.Set.empty, []) ] + let substitution_in_place (subst : st) (heap : t) : t Delayed.t = + Delayed.return (SHeap.substitution subst heap) let pp fmt (heap : t) : unit = SHeap.pp fmt heap let pp_by_need locs fmt heap = SHeap.pp_by_need locs fmt heap let get_print_info = SHeap.get_print_info - let copy (heap : t) : t = SHeap.copy heap + let copy (heap : t) : t = heap let init () : t = SHeap.init () let get_init_data _ = () let clear (_ : t) = init () (* We don't maintain any context *) - let get_loc_name pfs gamma = - Gillian.Logic.FOSolver.resolve_loc_name ~pfs ~gamma - - let fresh_loc ?(loc : vt option) (pfs : PFS.t) (gamma : Type_env.t) : - string * vt * Expr.t list = + (** Resolves the location to its name, or creates a new abstract location + equal to it if it cannot be resolved. *) + let fresh_loc ?(loc : vt option) () : (string * vt) Delayed.t = match loc with | Some loc -> ( - let loc_name = get_loc_name pfs gamma loc in + let* loc_name = Delayed.resolve_loc loc in match loc_name with | Some loc_name -> - if Names.is_aloc_name loc_name then - (loc_name, Expr.ALoc loc_name, []) - else (loc_name, Expr.Lit (Loc loc_name), []) + Delayed.return (loc_name, Expr.loc_from_loc_name loc_name) | None -> let al = ALoc.alloc () in - (al, ALoc al, [ Expr.BinOp (ALoc al, Equal, loc) ])) + Delayed.return + ~learned:[ Expr.BinOp (ALoc al, Equal, loc) ] + (al, Expr.ALoc al)) | None -> let al = ALoc.alloc () in - (al, ALoc al, []) - - let alloc - (heap : t) - (pfs : PFS.t) - (loc : vt option) - ?is_empty:(ie = false) - (mv : vt option) : action_ret = - let (loc_name : string), (loc : Expr.t) = + Delayed.return (al, Expr.ALoc al) + + let alloc (heap : t) (loc : vt option) ?is_empty:(ie = false) (mv : vt option) + : action_ret Delayed.t = + let* loc_name, loc = match (loc : Expr.t option) with | None -> let loc_name = ALoc.alloc () in - (loc_name, ALoc loc_name) - | Some (Lit (Loc loc)) -> (loc, Lit (Loc loc)) - | Some (ALoc loc) -> (loc, ALoc loc) + Delayed.return (loc_name, Expr.ALoc loc_name) + | Some (Lit (Loc loc)) -> Delayed.return (loc, Expr.Lit (Loc loc)) + | Some (ALoc loc) -> Delayed.return (loc, Expr.ALoc loc) | Some (LVar v) -> let loc_name = ALoc.alloc () in - PFS.extend pfs (BinOp (LVar v, Equal, ALoc loc_name)); - (loc_name, ALoc loc_name) + Delayed.return + ~learned:[ Expr.BinOp (LVar v, Equal, ALoc loc_name) ] + (loc_name, Expr.ALoc loc_name) | Some le -> raise (Failure (Printf.sprintf "Alloc with a non-loc loc argument: %s" ((Fmt.to_to_string Expr.pp) le))) in - SHeap.init_object heap loc_name ~is_empty:ie mv; - Ok [ (heap, [ loc ], [], []) ] - - let set_cell - (heap : t) - (pfs : PFS.t) - (gamma : Type_env.t) - (loc : vt) - (prop : vt) - (v : vt) : action_ret = - let loc_name, _, new_pfs = fresh_loc ~loc pfs gamma in - SHeap.set_fv_pair heap loc_name prop v; - Ok [ (heap, [], new_pfs, []) ] - - let get_cell - (heap : t) - (pfs : PFS.t) - (gamma : Type_env.t) - (loc : vt) - (prop : vt) : action_ret = - let loc_name = get_loc_name pfs gamma loc in - - L.tmi (fun m -> - m "@[GetCell: resolved location: %a -> %a@]" SVal.pp loc - Fmt.(option ~none:(any "None") string) - loc_name); + let heap = SHeap.init_object heap loc_name ~is_empty:ie mv in + DR.ok (heap, [ loc ]) + + let set_cell (heap : t) (loc : vt) (prop : vt) (v : vt) : action_ret Delayed.t + = + let* loc_name, _ = fresh_loc ~loc () in + DR.ok (SHeap.set_fv_pair heap loc_name prop v, []) + + (** Returns the first field of [fv_list] whose name is provably equal to + [prop], if any. *) + let get_equal_field (prop : vt) (fv_list : SFVL.t) : + (Expr.t * Expr.t) option Delayed.t = + let rec aux = function + | [] -> Delayed.return None + | (name, value) :: rest -> + let* eq = Delayed.entails [] (Expr.BinOp (name, Equal, prop)) in + if eq then Delayed.return (Some (name, value)) else aux rest + in + aux (SFVL.to_list fv_list) + let get_cell (heap : t) (loc : vt) (prop : vt) : action_ret Delayed.t = let make_gc_error (loc_name : string) (prop : vt) @@ -212,364 +196,275 @@ module M = struct | None -> ([ loc; prop ], fix_new_property :: fixes_exist_props, ff) in - let get_cell_from_loc loc_name = - Option.fold - ~some:(fun ((fv_list, dom), mtdt) -> - L.tmi (fun m -> m "fv_list: %a" SFVL.pp fv_list); - L.tmi (fun m -> - m "domain: %a" Fmt.(option ~none:(any "None") Expr.pp) dom); - L.tmi (fun m -> - m "metadata: %a" Fmt.(option ~none:(any "None") Expr.pp) mtdt); - match SFVL.get prop fv_list with - | Some ffv -> Ok [ (heap, [ loc; prop; ffv ], [], []) ] - | None -> ( - match - ( dom, - SFVL.get_first - (fun name -> FOSolver.is_equal ~pfs ~gamma name prop) - fv_list ) - with - | None, None -> - Error - [ - make_gc_error loc_name prop (SFVL.field_names fv_list) - None; - ] - | _, Some (ffn, ffv) -> Ok [ (heap, [ loc; ffn; ffv ], [], []) ] - | Some dom, None -> - let a_set_inclusion : Expr.t = - UnOp (Not, BinOp (prop, SetMem, dom)) + (* The cases in which the property might exist in the field-value list *) + let get_cell_branches loc_name fv_list dom mtdt = + match SFVL.get prop fv_list with + | Some ffv -> DR.ok (heap, [ loc; prop; ffv ]) + | None -> ( + let* equal_field = get_equal_field prop fv_list in + match (dom, equal_field) with + | None, None -> + DR.error + (make_gc_error loc_name prop (SFVL.field_names fv_list) None) + | _, Some (ffn, ffv) -> DR.ok (heap, [ loc; ffn; ffv ]) + | Some dom, None -> + let not_in_dom = Expr.UnOp (Not, BinOp (prop, SetMem, dom)) in + Delayed.if_sure not_in_dom + ~then_:(fun () -> + (* The property is certainly absent: it is added to the + object as None, and to its domain *) + let* new_domain = + Delayed.reduce (NOp (SetUnion, [ dom; ESet [ prop ] ])) + in + let fv_list' = SFVL.add prop (Lit Nono) fv_list in + let heap' = + SHeap.set heap loc_name fv_list' (Some new_domain) mtdt in - if - FOSolver.check_entailment Containers.SS.empty pfs - [ a_set_inclusion ] gamma - then ( - let new_domain : Expr.t = - NOp (SetUnion, [ dom; ESet [ prop ] ]) - in - let new_domain = - Reduction.reduce_lexpr ?gamma:(Some gamma) ?pfs:(Some pfs) - new_domain - in - let fv_list' = SFVL.add prop (Lit Nono) fv_list in - SHeap.set heap loc_name fv_list' (Some new_domain) mtdt; - Ok [ (heap, [ loc; prop; Lit Nono ], [], []) ]) - else - let f_names : Expr.t list = SFVL.field_names fv_list in - let full_knowledge : Expr.t = - BinOp (dom, Equal, ESet f_names) - in - if - FOSolver.check_entailment Containers.SS.empty pfs - [ full_knowledge ] gamma - then ( + DR.ok (heap', [ loc; prop; Lit Nono ])) + ~else_:(fun () -> + let f_names : Expr.t list = SFVL.field_names fv_list in + let full_knowledge : Expr.t = + BinOp (dom, Equal, ESet f_names) + in + Delayed.if_sure full_knowledge + ~then_:(fun () -> + (* The domain is fully known: the property is either one + of the fields it is equal to, or it is absent *) L.verbose (fun m -> m "GET CELL will branch\n"); - let rets : (t * vt list * Expr.t list * 'a) option list = + let field_branches = List.map (fun (f_name, f_value) -> - let new_f : Expr.t = BinOp (f_name, Equal, prop) in - let sat = - FOSolver.check_satisfiability - ~time:"JS getCell branch: heap" - (new_f :: PFS.to_list pfs) gamma + let this_prop : Expr.t = + BinOp (f_name, Equal, prop) in - match sat with - | false -> None - | true -> - (* Cases in which the prop exists *) - let heap' = SHeap.copy heap in - Some - ( heap', - [ loc; f_name; f_value ], - [ new_f ], - [] )) + let* sat = Delayed.check_sat this_prop in + if sat then + DR.ok ~learned:[ this_prop ] + (heap, [ loc; f_name; f_value ]) + else Delayed.vanish ()) (SFVL.to_list fv_list) in - - let rets = - List.map Option.get (List.filter Option.is_some rets) - in - - (* I need the case in which the prop does not exist *) - let new_f : Expr.t = - UnOp (Not, BinOp (prop, SetMem, dom)) - in - let sat = - FOSolver.check_satisfiability - ~time:"JS getCell branch: domain" - (new_f :: PFS.to_list pfs) gamma + let none_branch = + let not_in_dom : Expr.t = + UnOp (Not, BinOp (prop, SetMem, dom)) + in + let* sat = Delayed.check_sat not_in_dom in + if sat then + DR.ok ~learned:[ not_in_dom ] + (heap, [ loc; prop; Lit Nono ]) + else Delayed.vanish () in - let dom_ret = - match sat with - | false -> [] - | true -> - [ (heap, [ loc; prop; Lit Nono ], [ new_f ], []) ] - in - Ok (rets @ dom_ret)) - else - Error - [ - make_gc_error loc_name prop (SFVL.field_names fv_list) - (Some dom); - ])) - ~none:(Error [ ([], [ [ FLoc loc; FCell (loc, prop) ] ], Expr.false_) ]) - (SHeap.get heap loc_name) + Delayed.branches (field_branches @ [ none_branch ])) + ~else_:(fun () -> + DR.error + (make_gc_error loc_name prop (SFVL.field_names fv_list) + (Some dom))))) in - let result = - Option.fold ~some:get_cell_from_loc - ~none:(Error [ ([], [ [ FLoc loc; FCell (loc, prop) ] ], Expr.false_) ]) - loc_name + let* loc_name = Delayed.resolve_loc loc in + L.tmi (fun m -> + m "@[GetCell: resolved location: %a -> %a@]" SVal.pp loc + Fmt.(option ~none:(any "None") string) + loc_name); + match Option.map (fun ln -> (ln, SHeap.get heap ln)) loc_name with + | None | Some (_, None) -> + DR.error ([], [ [ FLoc loc; FCell (loc, prop) ] ], Expr.false_) + | Some (loc_name, Some ((fv_list, dom), mtdt)) -> + L.tmi (fun m -> m "fv_list: %a" SFVL.pp fv_list); + L.tmi (fun m -> + m "domain: %a" Fmt.(option ~none:(any "None") Expr.pp) dom); + L.tmi (fun m -> + m "metadata: %a" Fmt.(option ~none:(any "None") Expr.pp) mtdt); + get_cell_branches loc_name fv_list dom mtdt + + let remove_cell (heap : t) (loc : vt) (prop : vt) : action_ret Delayed.t = + let+ loc_name = Delayed.resolve_loc loc in + let heap = + match Option.map (fun ln -> (ln, SHeap.get heap ln)) loc_name with + | None | Some (_, None) -> heap + | Some (loc_name, Some ((fv_list, dom), mtdt)) -> + SHeap.set heap loc_name (SFVL.remove prop fv_list) dom mtdt in - result - - let remove_cell - (heap : t) - (pfs : PFS.t) - (gamma : Type_env.t) - (loc : vt) - (prop : vt) : action_ret = - let heap = SHeap.copy heap in - let f (loc_name : string) : unit = - Option.fold - ~some:(fun ((fv_list, dom), mtdt) -> - SHeap.set heap loc_name (SFVL.remove prop fv_list) dom mtdt; - ()) - ~none:() (SHeap.get heap loc_name) + Ok (heap, []) + + let set_domain (heap : t) (loc : vt) (dom : vt) : action_ret Delayed.t = + let+ loc_name, _ = fresh_loc ~loc () in + let heap = + match SHeap.get heap loc_name with + | None -> SHeap.set heap loc_name SFVL.empty (Some dom) None + | Some ((fv_list, _), mtdt) -> + (* TODO: This probably needs to be a bit more sophisticated *) + SHeap.set heap loc_name fv_list (Some dom) mtdt in - Option.fold ~some:f ~none:() (get_loc_name pfs gamma loc); - Ok [ (heap, [], [], []) ] - - let set_domain - (heap : t) - (pfs : PFS.t) - (gamma : Type_env.t) - (loc : vt) - (dom : vt) : action_ret = - let loc_name, _, new_pfs = fresh_loc ~loc pfs gamma in - - (match SHeap.get heap loc_name with - | None -> SHeap.set heap loc_name SFVL.empty (Some dom) None - | Some ((fv_list, _), mtdt) -> - (* TODO: This probably needs to be a bit more sophisticated *) - SHeap.set heap loc_name fv_list (Some dom) mtdt); - Ok [ (heap, [], new_pfs, []) ] - - let get_metadata (heap : t) (pfs : PFS.t) (gamma : Type_env.t) (loc : vt) : - action_ret = - let loc_name = get_loc_name pfs gamma loc in + Ok (heap, []) + let get_metadata (heap : t) (loc : vt) : action_ret Delayed.t = let make_gm_error (loc_name : string) : err_t = let loc = Expr.loc_from_loc_name loc_name in ([ loc ], [ [ FMetadata loc ] ], Expr.false_) in - - let f loc_name = - let loc = - if Names.is_aloc_name loc_name then Expr.ALoc loc_name - else Expr.Lit (Loc loc_name) - in - match SHeap.get heap loc_name with - | None -> Error [ make_gm_error loc_name ] - | Some ((_, _), mtdt) -> - Option.fold - ~some:(fun mtdt -> Ok [ (heap, [ loc; mtdt ], [], []) ]) - ~none:(Error [ make_gm_error loc_name ]) - mtdt - in - - Option.fold ~some:f - ~none:(Error [ ([ loc ], [ [ FLoc loc; FMetadata loc ] ], Expr.false_) ]) - loc_name - - let set_metadata - (heap : t) - (pfs : PFS.t) - (gamma : Type_env.t) - (loc : vt) - (mtdt : vt) : action_ret = - L.tmi (fun m -> m "Trying to set metadata."); - let loc_name, _, new_pfs = fresh_loc ~loc pfs gamma in - - (match SHeap.get heap loc_name with - | None -> SHeap.set heap loc_name SFVL.empty None (Some mtdt) + let* loc_name = Delayed.resolve_loc loc in + match loc_name with + | None -> DR.error ([ loc ], [ [ FLoc loc; FMetadata loc ] ], Expr.false_) + | Some loc_name -> ( + let loc = Expr.loc_from_loc_name loc_name in + match SHeap.get heap loc_name with + | None | Some (_, None) -> DR.error (make_gm_error loc_name) + | Some (_, Some mtdt) -> DR.ok (heap, [ loc; mtdt ])) + + let set_metadata (heap : t) (loc : vt) (mtdt : vt) : action_ret Delayed.t = + let* loc_name, _ = fresh_loc ~loc () in + match SHeap.get heap loc_name with + | None -> DR.ok (SHeap.set heap loc_name SFVL.empty None (Some mtdt), []) | Some ((fv_list, dom), None) -> - SHeap.set heap loc_name fv_list dom (Some mtdt) + DR.ok (SHeap.set heap loc_name fv_list dom (Some mtdt), []) | Some ((fv_list, dom), Some omet) -> - if omet <> Option.get (SVal.from_expr (Lit Null)) then - PFS.extend pfs (BinOp (mtdt, Equal, omet)) - else SHeap.set heap loc_name fv_list dom (Some mtdt)); - L.tmi (fun m -> m "Done setting metadata."); - Ok [ (heap, [], new_pfs, []) ] - - let delete_object (heap : t) (pfs : PFS.t) (gamma : Type_env.t) (loc : vt) : - action_ret = - let loc_name = get_loc_name pfs gamma loc in + if omet <> Expr.Lit Null then + DR.ok ~learned:[ Expr.BinOp (mtdt, Equal, omet) ] (heap, []) + else DR.ok (SHeap.set heap loc_name fv_list dom (Some mtdt), []) + let delete_object (heap : t) (loc : vt) : action_ret Delayed.t = + let* loc_name = Delayed.resolve_loc loc in match loc_name with | Some loc_name -> - if SHeap.has_loc heap loc_name then ( - SHeap.remove heap loc_name; - Ok [ (heap, [], [], []) ]) + if SHeap.has_loc heap loc_name then + DR.ok (SHeap.remove heap loc_name, []) else raise (Failure "delete_obj. Unknown Location") | None -> raise (Failure "delete_obj. Unknown Location") - let get_partial_domain - (heap : t) - (pfs : PFS.t) - (gamma : Type_env.t) - (loc : vt) - (e_dom : vt) : action_ret = - let loc_name = get_loc_name pfs gamma loc in - + let get_partial_domain (heap : t) (loc : vt) (e_dom : vt) : + action_ret Delayed.t = L.verbose (fun fmt -> fmt "Get partial domain"); L.verbose (fun fmt -> fmt "Expected domain: %a" SVal.pp e_dom); - - let f loc_name = - let loc = Expr.loc_from_loc_name loc_name in - match SHeap.get heap loc_name with - | None -> raise (Failure "DEATH. get_partial_domain. illegal loc_name") - | Some ((_, None), _) -> - raise (Failure "DEATH. get_partial_domain. missing domain") - | Some ((fv_list, Some dom), mtdt) -> ( - L.verbose (fun fmt -> fmt "Domain: %a" Expr.pp dom); - let none_fv_list, pos_fv_list = - SFVL.partition (fun _ fv -> fv = Lit Nono) fv_list - in - (* Called from the entailment - compute all negative resource associated with - the location whose name is loc_name *) - let none_props = SFVL.field_names none_fv_list in - L.verbose (fun fmt -> - fmt "None-props in heap: %a" - Fmt.(brackets (list ~sep:comma Expr.pp)) - none_props); - let dom' = Expr.BinOp (dom, SetDiff, ESet none_props) in - let dom'' = - Reduction.reduce_lexpr ?gamma:(Some gamma) ?pfs:(Some pfs) dom' - in - - (* Expected dom - dom *) - let dom_diff = Expr.BinOp (e_dom, SetDiff, dom'') in - let dom_diff' = - Reduction.reduce_lexpr ?gamma:(Some gamma) ?pfs:(Some pfs) dom_diff - in - - (* if dom_diff' != {} then we have to put the excess properties in the heap as nones *) - match dom_diff' with - | ESet props -> - let new_fv_list = - List.fold_left - (fun fv_list prop -> SFVL.add prop (Lit Nono) fv_list) - pos_fv_list props - in - SHeap.set heap loc_name new_fv_list (Some e_dom) mtdt; - Ok [ (heap, [ loc; e_dom ], [], []) ] - | _ -> raise (Failure "DEATH. get_partial_domain. dom_diff")) - in - let result = - Option.fold ~some:f ~none:(Error [ ([ loc ], [], Expr.false_) ]) loc_name - in - result - - let get_full_domain (heap : t) (pfs : PFS.t) (gamma : Type_env.t) (loc : vt) : - action_ret = - let loc_name = get_loc_name pfs gamma loc in - let f loc_name = - let loc = Expr.loc_from_loc_name loc_name in - match SHeap.get heap loc_name with - | None -> - (* This should never happen *) - raise (Failure "DEATH. get_full_domain. illegal loc_name") - | Some ((_, None), _) -> - (* This is not correct *) - raise (Failure "DEATH. TODO. get_full_domain. missing domain") - | Some ((fv_list, Some dom), _) -> - let props = SFVL.field_names fv_list in - let a_set_equality : Expr.t = BinOp (dom, Equal, ESet props) in - let solver_ret = - FOSolver.check_entailment Containers.SS.empty pfs [ a_set_equality ] - gamma - in - if solver_ret then - let _, pos_fv_list = + let* loc_name = Delayed.resolve_loc loc in + match loc_name with + | None -> DR.error ([ loc ], [], Expr.false_) + | Some loc_name -> ( + let loc = Expr.loc_from_loc_name loc_name in + match SHeap.get heap loc_name with + | None -> raise (Failure "DEATH. get_partial_domain. illegal loc_name") + | Some ((_, None), _) -> + raise (Failure "DEATH. get_partial_domain. missing domain") + | Some ((fv_list, Some dom), mtdt) -> ( + L.verbose (fun fmt -> fmt "Domain: %a" Expr.pp dom); + let none_fv_list, pos_fv_list = SFVL.partition (fun _ fv -> fv = Lit Nono) fv_list in - Ok [ (heap, [ loc; EList (SFVL.field_names pos_fv_list) ], [], []) ] - else raise (Failure "DEATH. TODO. get_full_domain. incomplete domain") + (* Called from the entailment - compute all negative resource + associated with the location whose name is loc_name *) + let none_props = SFVL.field_names none_fv_list in + L.verbose (fun fmt -> + fmt "None-props in heap: %a" + Fmt.(brackets (list ~sep:comma Expr.pp)) + none_props); + let* dom' = + Delayed.reduce (Expr.BinOp (dom, SetDiff, ESet none_props)) + in + (* Expected dom - dom *) + let* dom_diff = + Delayed.reduce (Expr.BinOp (e_dom, SetDiff, dom')) + in + (* if dom_diff != {} then we have to put the excess properties in + the heap as nones *) + match dom_diff with + | ESet props -> + let new_fv_list = + List.fold_left + (fun fv_list prop -> SFVL.add prop (Lit Nono) fv_list) + pos_fv_list props + in + let heap' = + SHeap.set heap loc_name new_fv_list (Some e_dom) mtdt + in + DR.ok (heap', [ loc; e_dom ]) + | _ -> raise (Failure "DEATH. get_partial_domain. dom_diff"))) + + let get_full_domain (heap : t) (loc : vt) : action_ret Delayed.t = + let* loc_name = Delayed.resolve_loc loc in + match loc_name with + | None -> DR.error ([ loc ], [], Expr.false_) + | Some loc_name -> ( + let loc = Expr.loc_from_loc_name loc_name in + match SHeap.get heap loc_name with + | None -> + (* This should never happen *) + raise (Failure "DEATH. get_full_domain. illegal loc_name") + | Some ((_, None), _) -> + (* This is not correct *) + raise (Failure "DEATH. TODO. get_full_domain. missing domain") + | Some ((fv_list, Some dom), _) -> + let props = SFVL.field_names fv_list in + let a_set_equality : Expr.t = BinOp (dom, Equal, ESet props) in + Delayed.if_sure a_set_equality + ~then_:(fun () -> + let _, pos_fv_list = + SFVL.partition (fun _ fv -> fv = Lit Nono) fv_list + in + DR.ok (heap, [ loc; EList (SFVL.field_names pos_fv_list) ])) + ~else_:(fun () -> + raise + (Failure "DEATH. TODO. get_full_domain. incomplete domain"))) + + let remove_domain (heap : t) (loc : vt) : action_ret Delayed.t = + let+ loc_name = Delayed.resolve_loc loc in + let heap = + match Option.map (fun ln -> (ln, SHeap.get heap ln)) loc_name with + | None | Some (_, None) -> heap + | Some (loc_name, Some ((fv_list, _), mtdt)) -> + SHeap.set heap loc_name fv_list None mtdt in + Ok (heap, []) - let result = - Option.fold ~some:f ~none:(Error [ ([ loc ], [], Expr.false_) ]) loc_name - in - result - - let remove_domain (heap : t) (pfs : PFS.t) (gamma : Type_env.t) (loc : vt) : - action_ret = - let f (loc_name : string) : unit = - Option.fold - ~some:(fun ((fv_list, _), mtdt) -> - SHeap.set heap loc_name fv_list None mtdt; - ()) - ~none:() (SHeap.get heap loc_name) - in - Option.fold ~some:f ~none:() (get_loc_name pfs gamma loc); - Ok [ (heap, [], [], []) ] - - let execute_action - ?matching:_ - (action : string) - (heap : t) - (pfs : PFS.t) - (gamma : Type_env.t) - (args : vt list) : action_ret = + let execute_action ~action_name:(action : string) (heap : t) (args : vt list) + : action_ret Delayed.t = if action = JSILNames.getCell then match args with - | [ loc; prop ] -> get_cell heap pfs gamma loc prop + | [ loc; prop ] -> get_cell heap loc prop | _ -> raise (Failure "Internal Error. execute_action") else if action = JSILNames.setCell then match args with - | [ loc; prop; v ] -> set_cell heap pfs gamma loc prop v + | [ loc; prop; v ] -> set_cell heap loc prop v | _ -> raise (Failure "Internal Error. execute_action. setCell") else if action = JSILNames.delCell then match args with - | [ loc; prop ] -> remove_cell heap pfs gamma loc prop + | [ loc; prop ] -> remove_cell heap loc prop | _ -> raise (Failure "Internal Error. execute_action. delCell") else if action = JSILNames.alloc then match args with - | [ Lit Empty; m_loc ] -> alloc heap pfs None (Some m_loc) - | [ loc; m_loc ] -> alloc heap pfs (Some loc) (Some m_loc) + | [ Lit Empty; m_loc ] -> alloc heap None (Some m_loc) + | [ loc; m_loc ] -> alloc heap (Some loc) (Some m_loc) | _ -> raise (Failure "Internal Error. execute_action. alloc") else if action = JSILNames.delObj then match args with - | [ loc ] -> delete_object heap pfs gamma loc + | [ loc ] -> delete_object heap loc | _ -> raise (Failure "Internal Error. execute_action. delObj") else if action = JSILNames.getAllProps then match args with - | [ loc ] -> get_full_domain heap pfs gamma loc + | [ loc ] -> get_full_domain heap loc | _ -> raise (Failure "Internal Error. execute_action. getAllProps") else if action = JSILNames.getMetadata then match args with - | [ loc ] -> get_metadata heap pfs gamma loc + | [ loc ] -> get_metadata heap loc | _ -> raise (Failure "Internal Error. execute_action. getMetadata") else if action = JSILNames.setMetadata then match args with - | [ loc; loc_m ] -> set_metadata heap pfs gamma loc loc_m + | [ loc; loc_m ] -> set_metadata heap loc loc_m | _ -> raise (Failure "Internal Error. execute_action. setMetadata") else if action = JSILNames.delMetadata then match args with - | [ _ ] -> Ok [ (heap, [], [], []) ] + | [ _ ] -> DR.ok (heap, []) | _ -> raise (Failure "Internal Error. execute_action. delMetadata") else if action = JSILNames.getProps then match args with - | [ loc; props ] -> get_partial_domain heap pfs gamma loc props + | [ loc; props ] -> get_partial_domain heap loc props | _ -> raise (Failure "Internal Error. execute_action. getProps") else if action = JSILNames.setProps then match args with - | [ loc; props ] -> set_domain heap pfs gamma loc props + | [ loc; props ] -> set_domain heap loc props | _ -> raise (Failure "Internal Error. execute_action") else if action = JSILNames.delProps then match args with - | [ loc; _ ] -> remove_domain heap pfs gamma loc + | [ loc; _ ] -> remove_domain heap loc | _ -> raise (Failure "Internal Error. execute_action. remove_domain") else raise (Failure "Internal Error. execute_action") @@ -591,7 +486,28 @@ module M = struct else if a_id = JSILNames.aProps then JSILNames.delProps else raise (Failure "DEATH. ga_to_setter") - let mem_constraints (state : t) : Expr.t list = SHeap.wf_assertions state + (* Consuming a core predicate is achieved by getting it and then deleting + it. *) + let consume ~(core_pred : string) (heap : t) (args : vt list) : + action_ret Delayed.t = + let getter = ga_to_getter core_pred in + let deleter = ga_to_deleter core_pred in + let** heap', vs = execute_action ~action_name:getter heap args in + let vs_ins, vs_outs = List_utils.split_at vs (List.length args) in + let++ heap'', _ = execute_action ~action_name:deleter heap' vs_ins in + (heap'', vs_outs) + + (* Producing a core predicate is achieved by setting it; failing producers + are allowed to vanish, there is no unsoundness *) + let produce ~(core_pred : string) (heap : t) (args : vt list) : t Delayed.t = + let setter = ga_to_setter core_pred in + let* set_res = execute_action ~action_name:setter heap args in + match set_res with + | Error _ -> Delayed.vanish () + | Ok (heap', _) -> Delayed.return heap' + + let split_further _ _ _ _ = None + let mem_constraints (heap : t) : Expr.t list = SHeap.wf_assertions heap let is_overlapping_asrt (a : string) : bool = if a = JSILNames.aMetadata then true else false @@ -741,7 +657,7 @@ module M = struct let can_fix _ = true - let sorted_locs_with_vals (smemory : t) = - let sorted_locs = Containers.SS.elements (SHeap.domain smemory) in - List.map (fun loc -> (loc, Option.get (SHeap.get smemory loc))) sorted_locs + let sorted_locs_with_vals (heap : t) = + let sorted_locs = Containers.SS.elements (SHeap.domain heap) in + List.map (fun loc -> (loc, Option.get (SHeap.get heap loc))) sorted_locs end diff --git a/Gillian-JS/lib/Semantics/SHeap.ml b/Gillian-JS/lib/Semantics/SHeap.ml index b7c816873..0f6044185 100644 --- a/Gillian-JS/lib/Semantics/SHeap.ml +++ b/Gillian-JS/lib/Semantics/SHeap.ml @@ -3,102 +3,23 @@ open Gillian.Gil_syntax open Javert_utils module SSubst = Gillian.Symbolic.Subst -module L = Logging -type s_object = (SFVL.t * Expr.t option) * Expr.t option +module SMap = Gillian.Utils.Prelude.Map.Make (struct + include String -type t = { - cfvl : (string, SFVL.t) Hashtbl.t; - cdom : (string, Expr.t option) Hashtbl.t; - cmet : (string, Expr.t option) Hashtbl.t; - sfvl : (string, SFVL.t) Hashtbl.t; - sdom : (string, Expr.t option) Hashtbl.t; - smet : (string, Expr.t option) Hashtbl.t; - cdmn : SS.t ref; - sdmn : SS.t ref; -} -[@@deriving yojson] + let of_yojson = function + | `String s -> Ok s + | _ -> Error "string_of_yojson: expected string" -(* ************* * - * AUXILIARIES * - * ************* *) + let to_yojson s = `String s +end) -let is_c = Expr.is_concrete +type s_object = (SFVL.t * Expr.t option) * Expr.t option [@@deriving yojson] -let merge (a : 't option) (b : 't option) (f : 't -> 't -> 't) : 't option = - match (a, b) with - | a, None -> a - | None, b -> b - | Some a, Some b -> Some (f a b) - -let get_fvl (heap : t) (loc : string) : SFVL.t option = - let cfvl = Hashtbl.find_opt heap.cfvl loc in - let sfvl = Hashtbl.find_opt heap.sfvl loc in - merge cfvl sfvl SFVL.union - -let get_dom (heap : t) (loc : string) : Expr.t option = - let cdom = Option.value ~default:None (Hashtbl.find_opt heap.cdom loc) in - let sdom = Option.value ~default:None (Hashtbl.find_opt heap.sdom loc) in - merge cdom sdom (fun _ _ -> - raise - (Failure "Domain in both the concrete and symbolic part of the heap.")) - -let get_met (heap : t) (loc : string) : Expr.t option = - let cmet = Option.value ~default:None (Hashtbl.find_opt heap.cmet loc) in - let smet = Option.value ~default:None (Hashtbl.find_opt heap.smet loc) in - merge cmet smet (fun _ _ -> - raise - (Failure "MetaData in both the concrete and symbolic part of the heap.")) - -let set_fvl (heap : t) (loc : string) (fvl : SFVL.t) : unit = - Hashtbl.remove heap.cfvl loc; - Hashtbl.remove heap.sfvl loc; - heap.cdmn := Var.Set.remove loc !(heap.cdmn); - heap.sdmn := Var.Set.remove loc !(heap.sdmn); - - let cfvl, sfvl = - SFVL.partition (fun prop value -> is_c value && is_c prop) fvl - in - match (cfvl = SFVL.empty, sfvl = SFVL.empty) with - | true, true -> - Hashtbl.replace heap.cfvl loc SFVL.empty; - Hashtbl.remove heap.sfvl loc; - heap.cdmn := Var.Set.add loc !(heap.cdmn) - | true, false -> - Hashtbl.remove heap.cfvl loc; - Hashtbl.replace heap.sfvl loc sfvl; - heap.cdmn := Var.Set.add loc !(heap.cdmn) - | false, true -> - Hashtbl.replace heap.cfvl loc cfvl; - Hashtbl.remove heap.sfvl loc; - heap.sdmn := Var.Set.add loc !(heap.sdmn) - | false, false -> - Hashtbl.replace heap.cfvl loc cfvl; - Hashtbl.replace heap.sfvl loc sfvl; - heap.cdmn := Var.Set.add loc !(heap.cdmn); - heap.sdmn := Var.Set.add loc !(heap.sdmn) - -let set_dom (heap : t) (loc : string) (dom : Expr.t option) : unit = - Hashtbl.remove heap.cdom loc; - Hashtbl.remove heap.sdom loc; - let add, rem = - match dom with - | Some x when not (is_c x) -> (heap.sdom, heap.cdom) - | _ -> (heap.cdom, heap.sdom) - in - Hashtbl.replace add loc dom; - Hashtbl.remove rem loc - -let set_met (heap : t) (loc : string) (met : Expr.t option) : unit = - Hashtbl.remove heap.cmet loc; - Hashtbl.remove heap.smet loc; - let add, rem = - match met with - | Some x when not (is_c x) -> (heap.smet, heap.cmet) - | _ -> (heap.cmet, heap.smet) - in - Hashtbl.replace add loc met; - Hashtbl.remove rem loc +(** A symbolic heap is an immutable map from location names to objects. An + object is a field-value list, an optional domain (an over-approximation of + the set of fields the object may have) and an optional metadata location. *) +type t = s_object SMap.t [@@deriving yojson] (*************************************) (** Symbolic heap functions **) @@ -106,24 +27,10 @@ let set_met (heap : t) (loc : string) (met : Expr.t option) : unit = (*************************************) (** Returns an empty symbolic heap *) -let init () : t = - let open Config in - { - cfvl = Hashtbl.create big_tbl_size; - sfvl = Hashtbl.create big_tbl_size; - cdom = Hashtbl.create big_tbl_size; - sdom = Hashtbl.create big_tbl_size; - cmet = Hashtbl.create big_tbl_size; - smet = Hashtbl.create big_tbl_size; - cdmn = ref SS.empty; - sdmn = ref SS.empty; - } +let init () : t = SMap.empty (** Symbolic heap read heap(loc) *) -let get (heap : t) (loc : string) : s_object option = - Option.map - (fun sfvl -> ((sfvl, get_dom heap loc), get_met heap loc)) - (get_fvl heap loc) +let get (heap : t) (loc : string) : s_object option = SMap.find_opt loc heap (** Symbolic heap read heap(loc) with the normal new obj default *) let get_with_default (heap : t) (loc : string) : s_object = @@ -135,178 +42,71 @@ let set (loc : string) (fv_list : SFVL.t) (dom : Expr.t option) - (metadata : Expr.t option) : unit = - set_fvl heap loc fv_list; - set_dom heap loc dom; - set_met heap loc metadata + (metadata : Expr.t option) : t = + SMap.add loc ((fv_list, dom), metadata) heap -(** Symbolic heap put heap (loc, (perm, field)) is assigned to value *) -let set_fv_pair (heap : t) (loc : string) (field : Expr.t) (value : Expr.t) : - unit = - heap.cdmn := Var.Set.remove loc !(heap.cdmn); - heap.sdmn := Var.Set.remove loc !(heap.sdmn); - let add, sadd, rem = - if is_c field && is_c value then (heap.cfvl, heap.cdmn, heap.sfvl) - else (heap.sfvl, heap.sdmn, heap.cfvl) - in - let fvadd = - SFVL.add field value - (Option.value ~default:SFVL.empty (Hashtbl.find_opt add loc)) - in - let fvrem = - SFVL.remove field - (Option.value ~default:SFVL.empty (Hashtbl.find_opt rem loc)) - in - sadd := Var.Set.add loc !sadd; - Hashtbl.replace add loc fvadd; - if fvrem = SFVL.empty then Hashtbl.remove rem loc - else Hashtbl.replace rem loc fvrem +(** Symbolic heap put heap(loc, field) is assigned to value *) +let set_fv_pair (heap : t) (loc : string) (field : Expr.t) (value : Expr.t) : t + = + let (fv_list, dom), metadata = get_with_default heap loc in + set heap loc (SFVL.add field value fv_list) dom metadata let init_object (heap : t) (loc : string) ?is_empty:(ie = false) - (mtdt : Expr.t option) : unit = - if Hashtbl.mem heap.cfvl loc || Hashtbl.mem heap.sfvl loc then - raise (Failure "Illegal init_object") + (mtdt : Expr.t option) : t = + if SMap.mem loc heap then raise (Failure "Illegal init_object") else let dom : Expr.t option = if ie then None else Some (ESet []) in set heap loc SFVL.empty dom mtdt -let has_loc (heap : t) (loc : string) : bool = - Hashtbl.mem heap.cfvl loc || Hashtbl.mem heap.sfvl loc +let has_loc (heap : t) (loc : string) : bool = SMap.mem loc heap -(** Removes the fv-list associated with --loc-- in --heap-- *) -let remove (heap : t) (loc : string) : unit = - Hashtbl.remove heap.cfvl loc; - Hashtbl.remove heap.sfvl loc; - Hashtbl.remove heap.cdom loc; - Hashtbl.remove heap.sdom loc; - Hashtbl.remove heap.cmet loc; - Hashtbl.remove heap.smet loc; - heap.cdmn := Var.Set.remove loc !(heap.cdmn); - heap.sdmn := Var.Set.remove loc !(heap.sdmn) +(** Removes the object associated with --loc-- in --heap-- *) +let remove (heap : t) (loc : string) : t = SMap.remove loc heap (** Retrieves the domain of --heap-- *) -let domain (heap : t) : SS.t = SS.union !(heap.cdmn) !(heap.sdmn) - -let cdomain (heap : t) : SS.t = !(heap.cdmn) - -(** Returns a copy of --heap-- *) -let copy (heap : t) : t = - { - cfvl = Hashtbl.copy heap.cfvl; - sfvl = Hashtbl.copy heap.sfvl; - cdom = Hashtbl.copy heap.cdom; - sdom = Hashtbl.copy heap.sdom; - cmet = Hashtbl.copy heap.cmet; - smet = Hashtbl.copy heap.smet; - cdmn = ref !(heap.cdmn); - sdmn = ref !(heap.sdmn); - } - -let merge_loc (heap : t) (new_loc : string) (old_loc : string) : unit = - let domain = domain heap in - let cfvl, sfvl, dom, met = - match SS.mem new_loc domain with - | true -> - (* Merge field-value lists *) - let ocvfl, osfvl = - ( Option.value ~default:SFVL.empty (Hashtbl.find_opt heap.cfvl old_loc), - Option.value ~default:SFVL.empty - (Hashtbl.find_opt heap.sfvl old_loc) ) - in - let ncvfl, nsfvl = - ( Option.value ~default:SFVL.empty (Hashtbl.find_opt heap.cfvl new_loc), - Option.value ~default:SFVL.empty - (Hashtbl.find_opt heap.sfvl new_loc) ) - in - let cfvl = SFVL.union ncvfl ocvfl in - let sfvl = SFVL.union nsfvl osfvl in - - (* Merge metadata *) - let odom = get_dom heap old_loc in - let ndom = get_dom heap new_loc in +let domain (heap : t) : SS.t = + SMap.fold (fun loc _ acc -> SS.add loc acc) heap SS.empty + +let merge_loc (heap : t) (new_loc : string) (old_loc : string) : t = + let (old_fvl, old_dom), old_met = get_with_default heap old_loc in + let merged = + match get heap new_loc with + | None -> ((old_fvl, old_dom), old_met) + | Some ((new_fvl, new_dom), new_met) -> + (* Merge field-value lists, with the new location taking precedence *) + let fvl = SFVL.union new_fvl old_fvl in let dom = - match (odom, ndom) with + match (old_dom, new_dom) with | None, None -> None | None, Some dom | Some dom, None -> Some dom - | Some dom1, Some dom2 -> Some (NOp (SetUnion, [ dom1; dom2 ])) + | Some dom1, Some dom2 -> Some (Expr.NOp (SetUnion, [ dom1; dom2 ])) in - - let omet = get_met heap old_loc in - let nmet = get_met heap new_loc in let met = - match (omet, nmet) with + match (old_met, new_met) with | None, None -> None | None, Some met | Some met, None -> Some met | Some met1, Some _ -> Some met1 in - - (cfvl, sfvl, dom, met) - | false -> - ( Option.value ~default:SFVL.empty (Hashtbl.find_opt heap.cfvl old_loc), - Option.value ~default:SFVL.empty (Hashtbl.find_opt heap.sfvl old_loc), - get_dom heap old_loc, - get_met heap old_loc ) + ((fvl, dom), met) in - set_fvl heap new_loc (SFVL.union cfvl sfvl); - set_dom heap new_loc dom; - set_met heap new_loc met; - remove heap old_loc + SMap.add new_loc merged (SMap.remove old_loc heap) -(** Modifies --heap-- in place updating it to subst(heap) *) -let substitution_in_place (subst : SSubst.t) (heap : t) : unit = +(** Returns subst(heap) *) +let substitution (subst : SSubst.t) (heap : t) : t = (* If the substitution is empty, there is nothing to be done *) - if not (SSubst.domain subst None = Expr.Set.empty) then ( - (* The substitution is not empty *) + if SSubst.domain subst None = Expr.Set.empty then heap + else let le_subst = SSubst.subst_in_expr subst ~partial:true in - - (* - L.(verbose (fun m -> m "CFVL: %d" (Hashtbl.length heap.cfvl))); - L.(verbose (fun m -> m "SFVL: %d" (Hashtbl.length heap.sfvl))); - L.(verbose (fun m -> m "CDOM: %d" (Hashtbl.length heap.cdom))); - L.(verbose (fun m -> m "SDOM: %d" (Hashtbl.length heap.sdom))); - L.(verbose (fun m -> m "CMET: %d" (Hashtbl.length heap.cmet))); - L.(verbose (fun m -> m "SMET: %d" (Hashtbl.length heap.smet))); - *) - - (* Field-value lists *) - Hashtbl.iter - (fun loc fvl -> - (* Substitute *) - let fvl = SFVL.substitution subst true fvl in - (* Partition into concrete and symbolic *) - let cfvl, sfvl = - SFVL.partition (fun prop value -> is_c value && is_c prop) fvl - in - (* Set symbolic *) - Hashtbl.replace heap.sfvl loc sfvl; - (* Merge concrete with new value taking precedence *) - let prev_cfvl = - Option.value ~default:SFVL.empty (Hashtbl.find_opt heap.cfvl loc) - in - Hashtbl.replace heap.cfvl loc (SFVL.union cfvl prev_cfvl)) - heap.sfvl; - - (* Domain table *) - Hashtbl.iter - (fun loc dom -> - (* Substitute *) - let dom = Option.map le_subst dom in - (* Set domain *) - set_dom heap loc dom) - heap.sdom; - - (* Metadata table *) - Hashtbl.iter - (fun loc met -> - (* Substitute *) - let met = Option.map le_subst met in - (* Set domain *) - set_met heap loc met) - heap.smet; - + let heap = + SMap.map + (fun ((fv_list, dom), met) -> + ( (SFVL.substitution subst true fv_list, Option.map le_subst dom), + Option.map le_subst met )) + heap + in (* Now we need to deal with any substitutions in the locations themselves *) let aloc_subst = SSubst.filter subst (fun var _ -> @@ -314,10 +114,11 @@ let substitution_in_place (subst : SSubst.t) (heap : t) : unit = | ALoc _ -> true | _ -> false) in - SSubst.iter aloc_subst (fun aloc new_loc -> + SSubst.fold aloc_subst + (fun aloc new_loc heap -> let aloc = match aloc with - | ALoc loc -> loc + | Expr.ALoc loc -> loc | _ -> raise (Failure "Impossible by construction") in let new_loc = @@ -330,12 +131,12 @@ let substitution_in_place (subst : SSubst.t) (heap : t) : unit = (Printf.sprintf "Heap substitution fail for loc: %s" ((Fmt.to_to_string Expr.pp) new_loc))) in - merge_loc heap new_loc aloc)) + merge_loc heap new_loc aloc) + heap (** Returns the serialization of --heap-- as a list *) let to_list (heap : t) : (string * s_object) list = - let domain = domain heap in - SS.fold (fun loc ac -> (loc, Option.get (get heap loc)) :: ac) domain [] + SMap.fold (fun loc obj ac -> (loc, obj) :: ac) heap [] (** converts a symbolic heap to a list of assertions *) let assertions (heap : t) : Asrt.t = @@ -362,11 +163,11 @@ let assertions (heap : t) : Asrt.t = to_list heap |> List.concat_map assertions_of_object |> List.sort Asrt.compare let wf_assertions_of_obj (heap : t) (loc : string) : Expr.t list = - let cfvl = - Option.value ~default:SFVL.empty (Hashtbl.find_opt heap.cfvl loc) - in - let sfvl = - Option.value ~default:SFVL.empty (Hashtbl.find_opt heap.sfvl loc) + let (fv_list, _), _ = get_with_default heap loc in + let cfvl, sfvl = + SFVL.partition + (fun prop value -> Expr.is_concrete value && Expr.is_concrete prop) + fv_list in let cpps = SFVL.field_names cfvl in let spps = SFVL.field_names sfvl in @@ -375,73 +176,25 @@ let wf_assertions_of_obj (heap : t) (loc : string) : Expr.t list = List.map (fun (x, y) : Expr.t -> UnOp (Not, BinOp (x, Equal, y))) props let wf_assertions (heap : t) : Expr.t list = - let domain = domain heap in - SS.fold (fun loc ac -> wf_assertions_of_obj heap loc @ ac) domain [] - -let is_well_formed (heap : t) : unit = - let cfvl = - Hashtbl.fold - (fun _ fvl ac -> - SFVL.fold (fun prop value ac -> ac && is_c prop && is_c value) fvl ac) - heap.cfvl true - in - if not cfvl then raise (Failure "Symbolicness in concrete part of the heap"); - let sfvl = - Hashtbl.fold - (fun _ fvl ac -> - SFVL.fold - (fun prop value ac -> ac && ((not (is_c prop)) || not (is_c value))) - fvl ac) - heap.sfvl true - in - if not sfvl then - raise (Failure "Concreteness in the symbolic part of the heap"); - let dom_kept = domain heap in - let dom_calc_1 = - SS.union - (Hashtbl.fold (fun v _ ac -> SS.add v ac) heap.cfvl SS.empty) - (Hashtbl.fold (fun v _ ac -> SS.add v ac) heap.sfvl SS.empty) - in - let dom_calc_2 = - SS.union - (Hashtbl.fold (fun v _ ac -> SS.add v ac) heap.cdom SS.empty) - (Hashtbl.fold (fun v _ ac -> SS.add v ac) heap.sdom SS.empty) - in - let dom_calc_3 = - SS.union - (Hashtbl.fold (fun v _ ac -> SS.add v ac) heap.cmet SS.empty) - (Hashtbl.fold (fun v _ ac -> SS.add v ac) heap.smet SS.empty) - in - let dom_calc = SS.union dom_calc_1 (SS.union dom_calc_2 dom_calc_3) in - if SS.elements dom_kept <> SS.elements dom_calc then - let msg = - Printf.sprintf "Domain mismatch:\n%s\n%s" - (String.concat ", " (SS.elements dom_kept)) - (String.concat ", " (SS.elements dom_calc)) - in - L.fail msg + SMap.fold (fun loc _ ac -> wf_assertions_of_obj heap loc @ ac) heap [] let pp ft heap = let open Fmt in - let sorted_locs = SS.elements (domain heap) in - let sorted_locs_with_vals = - List.map (fun loc -> (loc, Option.get (get heap loc))) sorted_locs - in let pp_one ft (loc, ((fv_pairs, domain), metadata)) = pf ft "@[%s |-> [ @[%a@] | @[%a@] ] with metadata %a@]" loc SFVL.pp fv_pairs (option Expr.pp) domain (option ~none:(any "unknown") Expr.pp) metadata in - (list ~sep:(any "@\n") pp_one) ft sorted_locs_with_vals + (list ~sep:(any "@\n") pp_one) ft (List.rev (to_list heap)) let get_print_info locs heap = let domain = domain heap in let metadata_locs = SS.fold (fun loc locs -> - match get_met heap loc with - | (Some (Lit (Loc x)) | Some (ALoc x)) when SS.mem x domain -> + match get heap loc with + | Some (_, (Some (Lit (Loc x)) | Some (ALoc x))) when SS.mem x domain -> SS.add x locs | _ -> locs) locs SS.empty @@ -450,8 +203,7 @@ let get_print_info locs heap = (SS.empty, metadata_locs) let pp_by_need locs ft heap = - let domain = domain heap in - let existent_locs = SS.inter locs domain in + let existent_locs = SS.inter locs (domain heap) in let sorted_locs_with_vals = List.map (fun loc -> (loc, Option.get (get heap loc))) @@ -466,71 +218,33 @@ let pp_by_need locs ft heap = in (list ~sep:(any "@\n") pp_one) ft sorted_locs_with_vals -let get_inv_metadata (heap : t) : (Expr.t, Expr.t) Hashtbl.t = - let inv_metadata = Hashtbl.create Config.medium_tbl_size in - let traverse_metadata_table mt : unit = - Hashtbl.iter - (fun loc e_metadata -> - match e_metadata with - | None -> () - | Some e_metadata -> - let loc_e = - if Names.is_lloc_name loc then Expr.Lit (Loc loc) else ALoc loc - in - Hashtbl.add inv_metadata e_metadata loc_e) - mt - in - traverse_metadata_table heap.smet; - traverse_metadata_table heap.cmet; - inv_metadata - -let clean_up (heap : t) : unit = - SS.iter - (fun loc -> - match has_loc heap loc with - | false -> () - | true -> ( - let (fvl, dom), met = get_with_default heap loc in - match (fvl = SFVL.empty, dom) with - | true, None -> ( - remove heap loc; - match met with - | Some (ALoc loc) | Some (Lit (Loc loc)) -> remove heap loc - | _ -> ()) - | _, _ -> ())) - (domain heap) +(** Maps metadata expressions back to the locations they are the metadata of *) +let get_inv_metadata (heap : t) : Expr.t Expr.Map.t = + SMap.fold + (fun loc (_, met) inv_metadata -> + match met with + | None -> inv_metadata + | Some e_metadata -> + let loc_e = + if Names.is_lloc_name loc then Expr.Lit (Loc loc) else ALoc loc + in + Expr.Map.add e_metadata loc_e inv_metadata) + heap Expr.Map.empty let lvars (heap : t) : Var.Set.t = - let lvars_fvl = - Hashtbl.fold - (fun _ fvl ac -> Var.Set.union (SFVL.lvars fvl) ac) - heap.sfvl Var.Set.empty - in - let lvars_dom = - Hashtbl.fold - (fun _ oe ac -> - let voe = Option.fold ~some:Expr.lvars ~none:Var.Set.empty oe in - Var.Set.union voe ac) - heap.sdom Var.Set.empty - in - let lvars_met = - Hashtbl.fold - (fun _ oe ac -> - let voe = Option.fold ~some:Expr.lvars ~none:Var.Set.empty oe in - Var.Set.union voe ac) - heap.smet Var.Set.empty - in - List.fold_left SS.union Var.Set.empty [ lvars_fvl; lvars_met; lvars_dom ] + let of_opt oe = Option.fold ~some:Expr.lvars ~none:Var.Set.empty oe in + SMap.fold + (fun _ ((fv_list, dom), met) acc -> + Var.Set.union acc + (Var.Set.union (SFVL.lvars fv_list) + (Var.Set.union (of_opt dom) (of_opt met)))) + heap Var.Set.empty let alocs (heap : t) : Var.Set.t = - let union = Var.Set.union in - Var.Set.empty - |> Hashtbl.fold (fun _ fvl ac -> Var.Set.union (SFVL.alocs fvl) ac) heap.sfvl - |> Hashtbl.fold - (fun _ oe ac -> - Option.fold ~some:(fun oe -> union (Expr.alocs oe) ac) ~none:ac oe) - heap.sdom - |> Hashtbl.fold - (fun _ oe ac -> - Option.fold ~some:(fun oe -> union (Expr.alocs oe) ac) ~none:ac oe) - heap.smet + let of_opt oe = Option.fold ~some:Expr.alocs ~none:Var.Set.empty oe in + SMap.fold + (fun _ ((fv_list, dom), met) acc -> + Var.Set.union acc + (Var.Set.union (SFVL.alocs fv_list) + (Var.Set.union (of_opt dom) (of_opt met)))) + heap Var.Set.empty diff --git a/Gillian-JS/lib/Semantics/semantics.ml b/Gillian-JS/lib/Semantics/semantics.ml index b80b8dca1..93c16c573 100644 --- a/Gillian-JS/lib/Semantics/semantics.ml +++ b/Gillian-JS/lib/Semantics/semantics.ml @@ -1,5 +1,5 @@ -module Legacy_symbolic = JSILSMemory.M -module Symbolic = Gillian.Symbolic.Legacy_s_memory.Modernize (Legacy_symbolic) +module Base_symbolic = JSILSMemory.M +module Symbolic = Gillian.Monadic.MonadicSMemory.Lift (Base_symbolic) module Concrete = JSILCMemory.M module External = External.M module SHeap = SHeap diff --git a/GillianCore/engine/symbolic_semantics/Legacy_s_memory.ml b/GillianCore/engine/symbolic_semantics/Legacy_s_memory.ml deleted file mode 100644 index 46170383a..000000000 --- a/GillianCore/engine/symbolic_semantics/Legacy_s_memory.ml +++ /dev/null @@ -1,150 +0,0 @@ -module type S = sig - (** Type of data that is given the first time memory is created. Useful when - there's global context to know about like a type-system *) - type init_data - - (** Type of GIL values *) - type vt := SVal.M.t - - (** Type of GIL substitutions *) - type st := SVal.SESubst.t - - type err_t [@@deriving yojson, show] - - (** Type of GIL general states *) - type t [@@deriving yojson] - - type action_ret := - ( (t * vt list * Expr.t list * (string * Type.t) list) list, - err_t list ) - result - - (** Initialisation *) - val init : init_data -> t - - val get_init_data : t -> init_data - val clear : t -> t - - (** Execute action *) - val execute_action : - ?matching:bool -> - string -> - t -> - PFS.t -> - Type_env.t -> - vt list -> - action_ret - - val ga_to_setter : string -> string - val ga_to_getter : string -> string - val ga_to_deleter : string -> string - val is_overlapping_asrt : string -> bool - - (** State Copy *) - val copy : t -> t - - (** Printer *) - val pp : Format.formatter -> t -> unit - - 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 - - val substitution_in_place : - pfs:PFS.t -> - gamma:Type_env.t -> - st -> - t -> - (t * Expr.Set.t * (string * Type.t) list) list - - val clean_up : ?keep:Expr.Set.t -> t -> Expr.Set.t * Expr.Set.t - val lvars : t -> Containers.SS.t - val alocs : t -> Containers.SS.t - val assertions : ?to_keep:Containers.SS.t -> t -> Asrt.t - val mem_constraints : t -> Expr.t list - 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 -> Expr.t - val can_fix : err_t -> bool - val get_fixes : err_t -> Asrt.t list - val sure_is_nonempty : t -> bool -end - -module Dummy : S with type init_data = unit = struct - type init_data = unit - type err_t = unit [@@deriving yojson, show] - type t = unit [@@deriving yojson] - - let init () = () - let get_init_data () = () - let clear () = () - let execute_action ?matching:_ _ _ _ _ _ = failwith "Please implement SMemory" - let ga_to_setter _ = failwith "Please implement SMemory" - let ga_to_getter _ = failwith "Please implement SMemory" - let ga_to_deleter _ = failwith "Please implement SMemory" - let is_overlapping_asrt _ = failwith "Please implement SMemory" - let copy () = () - let pp _ _ = () - let pp_by_need _ _ _ = () - let get_print_info _ _ = failwith "Please implement SMemory" - let substitution_in_place ~pfs:_ ~gamma:_ _ _ = [] - let clean_up ?keep:_ _ = failwith "Please implement SMemory" - let lvars _ = failwith "Please implement SMemory" - let alocs _ = failwith "Please implement SMemory" - let assertions ?to_keep:_ _ = failwith "Please implement SMemory" - let mem_constraints _ = failwith "Please implement SMemory" - let get_recovery_tactic _ _ = failwith "Please implement SMemory" - let pp_err _ _ = () - let get_failing_constraint _ = failwith "Please implement SMemory" - let get_fixes _ = failwith "Please implement SMemory" - let can_fix _ = failwith "Please implement SMemory" - let sure_is_nonempty _ = failwith "Please implement SMemory" -end - -module Modernize (Old_memory : S) = struct - include Old_memory - - let execute_action action_name heap (pc : Gpc.t) args = - let open Syntaxes.List in - match - execute_action ~matching:pc.matching action_name heap pc.pfs pc.gamma args - with - | Ok oks -> - let+ new_heap, v, new_fofs, new_types = oks in - let new_pfs = PFS.copy pc.pfs in - let new_gamma = Type_env.copy pc.gamma in - List.iter (fun (x, t) -> Type_env.update new_gamma x t) new_types; - List.iter (fun fof -> PFS.extend new_pfs fof) new_fofs; - let new_pc = - Gpc.make ~matching:pc.matching ~pfs:new_pfs ~gamma:new_gamma () - in - Gbranch.{ pc = new_pc; value = Ok (new_heap, v) } - | Error errs -> - let+ err = errs in - let pc = Gpc.copy pc in - Gbranch.{ pc; value = Error err } - - let consume core_pred heap (pc : Gpc.t) args = - let open Syntaxes.List in - let getter = ga_to_getter core_pred in - let deleter = ga_to_deleter core_pred in - let* get_res = execute_action getter heap pc args in - match get_res.value with - | Error _ -> [ get_res ] - | Ok (heap', vs) -> ( - let vs_ins, vs_outs = List_utils.split_at vs (List.length args) in - let+ rem_res = execute_action deleter heap' get_res.pc vs_ins in - match rem_res.value with - | Error _ -> rem_res - | Ok (heap'', _) -> { rem_res with value = Ok (heap'', vs_outs) }) - - let produce core_pred heap (pc : Gpc.t) args = - let open Syntaxes.List in - let setter = ga_to_setter core_pred in - let* set_res = execute_action setter heap pc args in - match set_res.value with - | Error _ -> - [] (* It's ok for failing producers to vanish, no unsoundness *) - | Ok (heap', _) -> [ { set_res with value = heap' } ] - - let split_further _ _ _ _ = None -end diff --git a/GillianCore/engine/symbolic_semantics/Symbolic.ml b/GillianCore/engine/symbolic_semantics/Symbolic.ml index 0492488f1..cb9804eff 100644 --- a/GillianCore/engine/symbolic_semantics/Symbolic.ml +++ b/GillianCore/engine/symbolic_semantics/Symbolic.ml @@ -56,9 +56,6 @@ module type Memory_S = SMemory.S (** @canonical Gillian.Symbolic.Dummy_memory *) module Dummy_memory = SMemory.Dummy -(** @canonical Gillian.Symbolic.Legacy_s_memory *) -module Legacy_s_memory = Legacy_s_memory - (** @canonical Gillian.Symbolic.Store *) module Store = SStore