diff --git a/ECMA-SL/dune b/ECMA-SL/dune index 6eef299470..ed3043f0fd 100644 --- a/ECMA-SL/dune +++ b/ECMA-SL/dune @@ -107,9 +107,9 @@ symbolic symbolic_interpreter symbolic_object + symbolic_object2 symbolic_memory symbolic_memory2 - s_object_branch_get symbolic_value value_intf value_reducer diff --git a/ECMA-SL/functorial/domains/heap_impl/symbolic_memory2.ml b/ECMA-SL/functorial/domains/heap_impl/symbolic_memory2.ml index 5b43ff67c0..1d296e1578 100644 --- a/ECMA-SL/functorial/domains/heap_impl/symbolic_memory2.ml +++ b/ECMA-SL/functorial/domains/heap_impl/symbolic_memory2.ml @@ -1,10 +1,12 @@ module V = Symbolic_value.M -module Object = S_object_branch_get open Syntax.Option -module Make () : Memory_intf.S2 = struct - type value = V.value - type value2 = Encoding.Expr.t +module Make + (Object : Object_intf.S2 + with type value = V.value + and type value2 = Encoding.Expr.t) : Memory_intf.S2 = struct + type value = Object.value + type value2 = Object.value2 type object_ = Object.t type t = @@ -71,7 +73,7 @@ module Make () : Memory_intf.S2 = struct let set_field heap loc ~field ~data solver pc = let obj = get heap loc in let res = - Option.bind obj (fun o -> Some (Object.set o field data solver pc)) + Option.bind obj (fun o -> Some (Object.set o ~key:field ~data solver pc)) in match res with | None -> Log.err "set Return is never none. loc: %s" loc diff --git a/ECMA-SL/functorial/domains/obj_impl/s_object_branch_get.ml b/ECMA-SL/functorial/domains/obj_impl/s_object_branch_get.ml deleted file mode 100644 index 3b5af75cd6..0000000000 --- a/ECMA-SL/functorial/domains/obj_impl/s_object_branch_get.ml +++ /dev/null @@ -1,339 +0,0 @@ -module V = Symbolic_value.M -module Reducer = Value_reducer -module Translator = Value_translator - -type value = V.value -type pct = V.value -type encoded_pct = Encoding.Expr.t - -type t = - { concrete_fields : (string, value) Hashtbl.t - ; symbolic_fields : (value, value) Hashtbl.t - } - -let create () : t = - { concrete_fields = Hashtbl.create 16; symbolic_fields = Hashtbl.create 16 } - -let clone (o : t) : t = - { concrete_fields = Hashtbl.copy o.concrete_fields - ; symbolic_fields = Hashtbl.copy o.symbolic_fields - } - -(* let to_string (o : t) (printer : Expr.t -> string) : string = *) -(* let str_obj = *) -(* Hashtbl.fold o.concrete_fields ~init:"{ " ~f:(fun ~key:n ~data:v ac -> *) -(* (if String.(ac <> "{ ") then ac ^ ", " else ac) *) -(* ^ Printf.sprintf "\"%s\": %s" n (printer v) ) *) -(* ^ "|||" *) -(* in *) -(* let str_obj = *) -(* List.fold_left (Expr_Hashtbl.to_alist o.symbolic_fields) *) -(* ~init:(str_obj ^ ", ") ~f:(fun acc (key, data) -> *) -(* acc ^ Printf.sprintf "\"$symb_%s\": %s, " (Expr.str key) (printer data) ) *) -(* in *) -(* str_obj ^ " }" *) - -let set_symbolic_field (o : t) (key : value) (data : value) : unit = - Hashtbl.replace o.symbolic_fields key data - -let set_concrete_field (o : t) (key : value) (data : value) : unit = - match key with - | V.Val (Val.Str field) -> Hashtbl.replace o.concrete_fields field data - | _ -> Format.kasprintf failwith "bad field: %a" V.Pp.pp key - -let has_concrete_key (o : t) (key : string) : bool = - Hashtbl.mem o.concrete_fields key - -let concrete_to_list (o : t) : (pct * value) list = - Hashtbl.fold - (fun k v acc -> (V.Val (Val.Str k), v) :: acc) - o.concrete_fields [] - -let get_symbolic_field (o : t) (key : value) : value option = - Hashtbl.find_opt o.symbolic_fields key - -let get_concrete_field (o : t) (key : string) : value option = - Hashtbl.find_opt o.concrete_fields key - -let mk_eq e1 e2 = V.BinOpt (Operator.Eq, e1, e2) - -let create_not_pct (l : (pct * value) list) (key : pct) : encoded_pct list = - List.fold_left - (fun acc (pc, _) -> - let ne = V.UnOpt (Operator.LogicalNot, mk_eq key pc) in - let expr = Reducer.reduce ne |> Translator.translate in - expr :: acc ) - [] l - -let create_object (o : t) (k1 : pct) (k2 : pct) : t * encoded_pct list = - let o' = clone o in - let eq = Reducer.reduce (mk_eq k1 k2) |> Translator.translate in - (o', [ eq ]) - -let is_key_possible (k1 : value) (k2 : value) (solver : Solver.t) - (pc : encoded_pct list) : bool = - let eq0 = mk_eq k1 k2 in - let eq = Reducer.reduce eq0 |> Translator.translate in - Solver.check solver (eq :: pc) - -let get_possible_fields_concrete (o : t) (key : value) (solver : Solver.t) - (pc : encoded_pct list) : (pct * pct) list = - Hashtbl.fold - (fun k d acc -> - let k' = V.Val (Val.Str k) in - if is_key_possible key k' solver pc then (k', d) :: acc else acc ) - o.concrete_fields [] - -let get_possible_fields_symbolic (o : t) (key : value) (solver : Solver.t) - (pc : encoded_pct list) : (pct * pct) list = - Hashtbl.fold - (fun k d acc -> - if is_key_possible key k solver pc then (k, d) :: acc else acc ) - o.symbolic_fields [] - -let get_possible_fields (o : t) (key : value) (solver : Solver.t) - (pc : encoded_pct list) : (pct * pct) list = - let conc = get_possible_fields_concrete o key solver pc in - let symb = get_possible_fields_symbolic o key solver pc in - conc @ symb - -let mk_ite e1 e2 e3 = V.TriOpt (Operator.ITE, e1, e2, e3) -let is_val = function V.Val _ -> true | _ -> false - -let has_field (o : t) (k : value) : value = - let open Val in - if - Hashtbl.length o.concrete_fields = 0 && Hashtbl.length o.symbolic_fields = 0 - then Val (Bool false) - else if is_val k then - match k with - | Val (Str s) -> - if Hashtbl.mem o.concrete_fields s then Val (Bool true) - else - Hashtbl.fold - (fun key _ acc -> mk_ite (mk_eq k key) (Val (Bool true)) acc) - o.symbolic_fields (Val (Bool false)) - | _ -> failwith "impossible" - else - let v0 = - Hashtbl.fold - (fun key _ acc -> mk_ite (mk_eq k key) (Val (Bool true)) acc) - o.symbolic_fields (Val (Bool false)) - in - Hashtbl.fold - (fun key _ acc -> mk_ite (mk_eq k (Val (Str key))) (Val (Bool true)) acc) - o.concrete_fields v0 - -let set (o : t) (key : value) (data : value) (solver : Solver.t) - (pc : encoded_pct list) : (t * encoded_pct list) list = - match key with - | V.Val (Val.Str s) -> - if has_concrete_key o s || Hashtbl.length o.symbolic_fields = 0 then - let _ = set_concrete_field o key data in - [ (o, []) ] - else - let lst = get_possible_fields_symbolic o key solver pc in - (* create an object for each possible equality *) - let rets = - List.map - (fun (k, _) -> - let (o', pc') = create_object o key k in - set_concrete_field o' key data; - Hashtbl.remove o'.symbolic_fields k; - (o', pc') ) - lst - in - (* update current object with the condition of not - being equal to any of the existing fields *) - let new_pc = create_not_pct lst key in - if Solver.check solver (new_pc @ pc) then ( - let o' = clone o in - Hashtbl.replace o'.concrete_fields s data; - (o', new_pc) :: rets ) - else rets - | _ -> - let temp = - Hashtbl.length o.concrete_fields + Hashtbl.length o.symbolic_fields - in - if temp = 0 then ( - set_symbolic_field o key data; - [ (o, []) ] ) - else - let symbolic_conds = get_possible_fields_symbolic o key solver pc in - let concrete_conds = get_possible_fields_concrete o key solver pc in - (* Two maps because set functions differ *) - let rets = - List.map - (fun (concrete_key, _) -> - let (o', pc') = create_object o key concrete_key in - set_concrete_field o' concrete_key data; - (o', pc') ) - concrete_conds - in - let rets = - rets - @ List.map - (fun (symbolic_key, _) -> - let (o', pc') = create_object o key symbolic_key in - set_symbolic_field o' symbolic_key data; - (o', pc') ) - symbolic_conds - in - let new_pc = create_not_pct (concrete_conds @ symbolic_conds) key in - let check = Solver.check solver (new_pc @ pc) in - if check then - let o' = clone o in - let _ = Hashtbl.replace o'.symbolic_fields key data in - (o', new_pc) :: rets - else rets - -let get (o : t) (key : value) (solver : Solver.t) (pc : encoded_pct list) : - (t * encoded_pct list * value option) list = - match key with - | V.Val (Val.Str key_s) -> ( - let res = Hashtbl.find_opt o.concrete_fields key_s in - match res with - | Some v -> [ (o, [], Some v) ] - | None -> - if Hashtbl.length o.symbolic_fields = 0 then [ (o, [], None) ] - else - let l = - Hashtbl.fold - (fun k d acc -> - if is_key_possible key k solver pc then (k, d) :: acc else acc ) - o.symbolic_fields [] - in - let obj_list = - List.map - (fun (k, v) -> - let (o', pc') = create_object o key k in - Hashtbl.remove o'.symbolic_fields k; - Hashtbl.replace o'.concrete_fields key_s v; - (o', pc', Some v) ) - l - in - (* Does not match any symbolic value, create new pct *) - let new_pc = create_not_pct l key in - if Solver.check solver (new_pc @ pc) then - let o' = clone o in - (o', new_pc, None) :: obj_list - else obj_list ) - | _ -> ( - let res = get_symbolic_field o key in - match res with - | Some v -> [ (o, [], Some v) ] - | None -> - let cond_list = - Hashtbl.fold - (fun k d acc -> - let k' = V.Val (Val.Str k) in - if is_key_possible key k' solver pc then (k', d) :: acc else acc ) - o.concrete_fields [] - in - let cond_list = - Hashtbl.fold - (fun k d acc -> - if is_key_possible key k solver pc then (k, d) :: acc else acc ) - o.symbolic_fields cond_list - in - (* Get objects for all possible symb and concrete equalities *) - let rets = - List.map - (fun (k, v) -> - let (o', pc') = create_object o key k in - (o', pc', Some v) ) - cond_list - in - (* Does not match any symbolic value, create new pct *) - let new_pc = create_not_pct cond_list key in - let rets = - if Solver.check solver (new_pc @ pc) then - let o' = clone o in - (o', new_pc, None) :: rets - else rets - in - rets ) - -let delete (o : t) (key : value) (solver : Solver.t) (pc : encoded_pct list) : - (t * encoded_pct list) list = - match key with - | V.Val (Val.Str s) -> - if has_concrete_key o s then - let _ = Hashtbl.remove o.concrete_fields s in - [ (o, []) ] - else if Hashtbl.length o.symbolic_fields = 0 then [ (o, []) ] - else - let lst = get_possible_fields_symbolic o key solver pc in - (* create an object for each possible equality *) - let rets = - List.map - (fun (k, _) -> - let (o', pc') = create_object o key k in - Hashtbl.remove o'.symbolic_fields k; - (o', pc') ) - lst - in - (* update current object with the condition of not - being equal to any of the existing fields *) - let new_pc = create_not_pct lst key in - if Solver.check solver (new_pc @ pc) then - let o' = clone o in - (o', new_pc) :: rets - else rets - | _ -> ( - let res = get_symbolic_field o key in - match res with - | Some _v -> - Hashtbl.remove o.symbolic_fields key; - [ (o, []) ] - | None -> - let symbolic_list = get_possible_fields_symbolic o key solver pc in - let concrete_list = get_possible_fields_concrete o key solver pc in - (* Get objects for all possible symb equalities *) - let rets = - List.map - (fun (k, _) -> - let (o', pc') = create_object o key k in - Hashtbl.remove o'.symbolic_fields k; - (o', pc') ) - symbolic_list - in - (* Get objects for all possible concrete equalities *) - let rets = - List.map - (fun (k, _) -> - let (o', pc') = create_object o key k in - let s = - match k with - | V.Val (Val.Str s) -> s - | _ -> failwith "Invalid key value." - in - Hashtbl.remove o'.concrete_fields s; - (o', pc') ) - concrete_list - @ rets - in - (* Does not match any symbolic value, create new pct *) - let new_pc = create_not_pct (symbolic_list @ concrete_list) key in - if Solver.check solver (new_pc @ pc) then - let o' = clone o in - (o', new_pc) :: rets - else rets ) - -(* let to_json (o : 'a t) (printer : 'a -> string) : string = - let str_obj = - Hashtbl.fold o ~init:"{ " ~f:(fun ~key:n ~data:v ac -> - (if String.(ac <> "{ ") then ac ^ ", " else ac) - ^ Printf.sprintf "\"%s\": %s" n (printer v)) - in - str_obj ^ " }" *) - -let to_list (o : t) : (value * 'a) list = - (*TODO add symb values*) - concrete_to_list o @ (Hashtbl.to_seq o.symbolic_fields |> List.of_seq) - -let get_fields (o : t) : value list = - let ret = - Seq.map (fun f -> V.Val (Val.Str f)) (Hashtbl.to_seq_keys o.concrete_fields) - in - List.of_seq ret @ List.of_seq @@ Hashtbl.to_seq_keys o.symbolic_fields diff --git a/ECMA-SL/functorial/domains/obj_impl/symbolic_object2.ml b/ECMA-SL/functorial/domains/obj_impl/symbolic_object2.ml new file mode 100644 index 0000000000..10f0aacdb6 --- /dev/null +++ b/ECMA-SL/functorial/domains/obj_impl/symbolic_object2.ml @@ -0,0 +1,341 @@ +module V = Symbolic_value.M +module Reducer = Value_reducer +module Translator = Value_translator + +module M : + Object_intf.S2 with type value = V.value and type value2 = Encoding.Expr.t = +struct + type value = V.value + type value2 = Encoding.Expr.t + + type t = + { concrete_fields : (string, value) Hashtbl.t + ; symbolic_fields : (value, value) Hashtbl.t + } + + let create () : t = + { concrete_fields = Hashtbl.create 16; symbolic_fields = Hashtbl.create 16 } + + let clone (o : t) : t = + { concrete_fields = Hashtbl.copy o.concrete_fields + ; symbolic_fields = Hashtbl.copy o.symbolic_fields + } + + (* let to_string (o : t) (printer : Expr.t -> string) : string = *) + (* let str_obj = *) + (* Hashtbl.fold o.concrete_fields ~init:"{ " ~f:(fun ~key:n ~data:v ac -> *) + (* (if String.(ac <> "{ ") then ac ^ ", " else ac) *) + (* ^ Printf.sprintf "\"%s\": %s" n (printer v) ) *) + (* ^ "|||" *) + (* in *) + (* let str_obj = *) + (* List.fold_left (Expr_Hashtbl.to_alist o.symbolic_fields) *) + (* ~init:(str_obj ^ ", ") ~f:(fun acc (key, data) -> *) + (* acc ^ Printf.sprintf "\"$symb_%s\": %s, " (Expr.str key) (printer data) ) *) + (* in *) + (* str_obj ^ " }" *) + + let is_empty o = + Hashtbl.(length o.concrete_fields = 0 && length o.symbolic_fields = 0) + + let set_symbolic_field (o : t) (key : value) (data : value) : unit = + Hashtbl.replace o.symbolic_fields key data + + let set_concrete_field (o : t) (key : value) (data : value) : unit = + match key with + | V.Val (Val.Str field) -> Hashtbl.replace o.concrete_fields field data + | _ -> Format.kasprintf failwith "bad field: %a" V.Pp.pp key + + let has_concrete_key (o : t) (key : string) : bool = + Hashtbl.mem o.concrete_fields key + + let concrete_to_list (o : t) : (value * value) list = + Hashtbl.fold + (fun k v acc -> (V.Val (Val.Str k), v) :: acc) + o.concrete_fields [] + + let get_symbolic_field (o : t) (key : value) : value option = + Hashtbl.find_opt o.symbolic_fields key + + let mk_eq e1 e2 = V.BinOpt (Operator.Eq, e1, e2) + + let create_not_pct (l : (value * value) list) (key : value) : value2 list = + List.fold_left + (fun acc (pc, _) -> + let ne = V.UnOpt (Operator.LogicalNot, mk_eq key pc) in + let expr = Reducer.reduce ne |> Translator.translate in + expr :: acc ) + [] l + + let create_object (o : t) (k1 : value) (k2 : value) : t * value2 list = + let o' = clone o in + let eq = Reducer.reduce (mk_eq k1 k2) |> Translator.translate in + (o', [ eq ]) + + let is_key_possible (k1 : value) (k2 : value) (solver : Solver.t) + (pc : value2 list) : bool = + let eq0 = mk_eq k1 k2 in + let eq = Reducer.reduce eq0 |> Translator.translate in + Solver.check solver (eq :: pc) + + let get_possible_fields_concrete (o : t) (key : value) (solver : Solver.t) + (pc : value2 list) : (value * value) list = + Hashtbl.fold + (fun k d acc -> + let k' = V.Val (Val.Str k) in + if is_key_possible key k' solver pc then (k', d) :: acc else acc ) + o.concrete_fields [] + + let get_possible_fields_symbolic (o : t) (key : value) (solver : Solver.t) + (pc : value2 list) : (value * value) list = + Hashtbl.fold + (fun k d acc -> + if is_key_possible key k solver pc then (k, d) :: acc else acc ) + o.symbolic_fields [] + + let mk_ite e1 e2 e3 = V.TriOpt (Operator.ITE, e1, e2, e3) + let is_val = function V.Val _ -> true | _ -> false + + let has_field (o : t) (k : value) : value = + let open Val in + if + Hashtbl.length o.concrete_fields = 0 + && Hashtbl.length o.symbolic_fields = 0 + then Val (Bool false) + else if is_val k then + match k with + | Val (Str s) -> + if Hashtbl.mem o.concrete_fields s then Val (Bool true) + else + Hashtbl.fold + (fun key _ acc -> mk_ite (mk_eq k key) (Val (Bool true)) acc) + o.symbolic_fields (Val (Bool false)) + | _ -> failwith "impossible" + else + let v0 = + Hashtbl.fold + (fun key _ acc -> mk_ite (mk_eq k key) (Val (Bool true)) acc) + o.symbolic_fields (Val (Bool false)) + in + Hashtbl.fold + (fun key _ acc -> mk_ite (mk_eq k (Val (Str key))) (Val (Bool true)) acc) + o.concrete_fields v0 + + let set (o : t) ~(key : value) ~(data : value) (solver : Solver.t) + (pc : value2 list) : (t * value2 list) list = + match key with + | V.Val (Val.Str s) -> + if has_concrete_key o s || Hashtbl.length o.symbolic_fields = 0 then + let _ = set_concrete_field o key data in + [ (o, []) ] + else + let lst = get_possible_fields_symbolic o key solver pc in + (* create an object for each possible equality *) + let rets = + List.map + (fun (k, _) -> + let (o', pc') = create_object o key k in + set_concrete_field o' key data; + Hashtbl.remove o'.symbolic_fields k; + (o', pc') ) + lst + in + (* update current object with the condition of not + being equal to any of the existing fields *) + let new_pc = create_not_pct lst key in + if Solver.check solver (new_pc @ pc) then ( + let o' = clone o in + Hashtbl.replace o'.concrete_fields s data; + (o', new_pc) :: rets ) + else rets + | _ -> + let temp = + Hashtbl.length o.concrete_fields + Hashtbl.length o.symbolic_fields + in + if temp = 0 then ( + set_symbolic_field o key data; + [ (o, []) ] ) + else + let symbolic_conds = get_possible_fields_symbolic o key solver pc in + let concrete_conds = get_possible_fields_concrete o key solver pc in + (* Two maps because set functions differ *) + let rets = + List.map + (fun (concrete_key, _) -> + let (o', pc') = create_object o key concrete_key in + set_concrete_field o' concrete_key data; + (o', pc') ) + concrete_conds + in + let rets = + rets + @ List.map + (fun (symbolic_key, _) -> + let (o', pc') = create_object o key symbolic_key in + set_symbolic_field o' symbolic_key data; + (o', pc') ) + symbolic_conds + in + let new_pc = create_not_pct (concrete_conds @ symbolic_conds) key in + let check = Solver.check solver (new_pc @ pc) in + if check then + let o' = clone o in + let _ = Hashtbl.replace o'.symbolic_fields key data in + (o', new_pc) :: rets + else rets + + let get (o : t) (key : value) (solver : Solver.t) (pc : value2 list) : + (t * value2 list * value option) list = + match key with + | V.Val (Val.Str key_s) -> ( + let res = Hashtbl.find_opt o.concrete_fields key_s in + match res with + | Some v -> [ (o, [], Some v) ] + | None -> + if Hashtbl.length o.symbolic_fields = 0 then [ (o, [], None) ] + else + let l = + Hashtbl.fold + (fun k d acc -> + if is_key_possible key k solver pc then (k, d) :: acc else acc + ) + o.symbolic_fields [] + in + let obj_list = + List.map + (fun (k, v) -> + let (o', pc') = create_object o key k in + Hashtbl.remove o'.symbolic_fields k; + Hashtbl.replace o'.concrete_fields key_s v; + (o', pc', Some v) ) + l + in + (* Does not match any symbolic value, create new pct *) + let new_pc = create_not_pct l key in + if Solver.check solver (new_pc @ pc) then + let o' = clone o in + (o', new_pc, None) :: obj_list + else obj_list ) + | _ -> ( + let res = get_symbolic_field o key in + match res with + | Some v -> [ (o, [], Some v) ] + | None -> + let cond_list = + Hashtbl.fold + (fun k d acc -> + let k' = V.Val (Val.Str k) in + if is_key_possible key k' solver pc then (k', d) :: acc else acc + ) + o.concrete_fields [] + in + let cond_list = + Hashtbl.fold + (fun k d acc -> + if is_key_possible key k solver pc then (k, d) :: acc else acc ) + o.symbolic_fields cond_list + in + (* Get objects for all possible symb and concrete equalities *) + let rets = + List.map + (fun (k, v) -> + let (o', pc') = create_object o key k in + (o', pc', Some v) ) + cond_list + in + (* Does not match any symbolic value, create new pct *) + let new_pc = create_not_pct cond_list key in + let rets = + if Solver.check solver (new_pc @ pc) then + let o' = clone o in + (o', new_pc, None) :: rets + else rets + in + rets ) + + let delete (o : t) (key : value) (solver : Solver.t) (pc : value2 list) : + (t * value2 list) list = + match key with + | V.Val (Val.Str s) -> + if has_concrete_key o s then + let _ = Hashtbl.remove o.concrete_fields s in + [ (o, []) ] + else if Hashtbl.length o.symbolic_fields = 0 then [ (o, []) ] + else + let lst = get_possible_fields_symbolic o key solver pc in + (* create an object for each possible equality *) + let rets = + List.map + (fun (k, _) -> + let (o', pc') = create_object o key k in + Hashtbl.remove o'.symbolic_fields k; + (o', pc') ) + lst + in + (* update current object with the condition of not + being equal to any of the existing fields *) + let new_pc = create_not_pct lst key in + if Solver.check solver (new_pc @ pc) then + let o' = clone o in + (o', new_pc) :: rets + else rets + | _ -> ( + let res = get_symbolic_field o key in + match res with + | Some _v -> + Hashtbl.remove o.symbolic_fields key; + [ (o, []) ] + | None -> + let symbolic_list = get_possible_fields_symbolic o key solver pc in + let concrete_list = get_possible_fields_concrete o key solver pc in + (* Get objects for all possible symb equalities *) + let rets = + List.map + (fun (k, _) -> + let (o', pc') = create_object o key k in + Hashtbl.remove o'.symbolic_fields k; + (o', pc') ) + symbolic_list + in + (* Get objects for all possible concrete equalities *) + let rets = + List.map + (fun (k, _) -> + let (o', pc') = create_object o key k in + let s = + match k with + | V.Val (Val.Str s) -> s + | _ -> failwith "Invalid key value." + in + Hashtbl.remove o'.concrete_fields s; + (o', pc') ) + concrete_list + @ rets + in + (* Does not match any symbolic value, create new pct *) + let new_pc = create_not_pct (symbolic_list @ concrete_list) key in + if Solver.check solver (new_pc @ pc) then + let o' = clone o in + (o', new_pc) :: rets + else rets ) + + (* let to_json (o : 'a t) (printer : 'a -> string) : string = + let str_obj = + Hashtbl.fold o ~init:"{ " ~f:(fun ~key:n ~data:v ac -> + (if String.(ac <> "{ ") then ac ^ ", " else ac) + ^ Printf.sprintf "\"%s\": %s" n (printer v)) + in + str_obj ^ " }" *) + + let to_list (o : t) : (value * 'a) list = + (*TODO add symb values*) + concrete_to_list o @ (Hashtbl.to_seq o.symbolic_fields |> List.of_seq) + + let get_fields (o : t) : value list = + let ret = + Seq.map + (fun f -> V.Val (Val.Str f)) + (Hashtbl.to_seq_keys o.concrete_fields) + in + List.of_seq ret @ List.of_seq @@ Hashtbl.to_seq_keys o.symbolic_fields +end diff --git a/ECMA-SL/functorial/interpreter_functor_intf.ml b/ECMA-SL/functorial/interpreter_functor_intf.ml index dec377d395..06aab5d9e7 100644 --- a/ECMA-SL/functorial/interpreter_functor_intf.ml +++ b/ECMA-SL/functorial/interpreter_functor_intf.ml @@ -50,6 +50,7 @@ module type P = sig val set_field : t -> Loc.t -> field:value -> data:value -> unit val get_field : t -> Loc.t -> value -> value option Choice.t val delete_field : t -> Loc.t -> value -> unit + val pp : Fmt.formatter -> t -> unit val to_string : t -> string val loc : value -> Loc.t Choice.t val pp_val : t -> value -> string diff --git a/ECMA-SL/functorial/memory_intf.ml b/ECMA-SL/functorial/memory_intf.ml index 03d259f6a9..df3de7a3f5 100644 --- a/ECMA-SL/functorial/memory_intf.ml +++ b/ECMA-SL/functorial/memory_intf.ml @@ -1,3 +1,4 @@ +(* TODO: merge these type signatures *) module type S = sig type t type value diff --git a/ECMA-SL/functorial/object_intf.ml b/ECMA-SL/functorial/object_intf.ml index 92d758d343..2ee1c52a93 100644 --- a/ECMA-SL/functorial/object_intf.ml +++ b/ECMA-SL/functorial/object_intf.ml @@ -1,3 +1,4 @@ +(* TODO: merge these type signatures *) module type S = sig type t type value @@ -15,3 +16,33 @@ module type S = sig val to_string : t -> string val to_json : t -> string end + +module type S2 = sig + type t + type value + type value2 + + val create : unit -> t + val clone : t -> t + val is_empty : t -> bool + val to_list : t -> (value * value) list + val has_field : t -> value -> value + val get_fields : t -> value list + + val set : + t + -> key:value + -> data:value + -> Solver.t + -> value2 list + -> (t * value2 list) list + + val get : + t + -> value + -> Solver.t + -> value2 list + -> (t * value2 list * value option) list + + val delete : t -> value -> Solver.t -> value2 list -> (t * value2 list) list +end diff --git a/ECMA-SL/functorial/symbolic.ml b/ECMA-SL/functorial/symbolic.ml index 1ecf0609fb..a5854d5dce 100644 --- a/ECMA-SL/functorial/symbolic.ml +++ b/ECMA-SL/functorial/symbolic.ml @@ -131,6 +131,7 @@ module P = struct let thread = Thread.clone_mem thread in List.filter_map (return thread) locs + let pp = Memory.pp let pp_val = Memory.pp_val end diff --git a/ECMA-SL/functorial/symbolic_memory.ml b/ECMA-SL/functorial/symbolic_memory.ml index c34f77c055..8fb8de9d7b 100644 --- a/ECMA-SL/functorial/symbolic_memory.ml +++ b/ECMA-SL/functorial/symbolic_memory.ml @@ -59,17 +59,13 @@ module Make (O : Object_intf.S with type value = V.value) = struct set h loc o' ) obj - let pp_hashtbl ~pp_sep pp_v fmt v = - Format.pp_print_seq ~pp_sep pp_v fmt (Hashtbl.to_seq v) - let rec pp fmt ({ data; parent } : t) = - let open Format in - let pp_sep fmt () = fprintf fmt ",@ " in + let open Fmt in let pp_v fmt (key, data) = fprintf fmt "%a: %a" Loc.pp key O.pp data in - let pp_parent fmt p = - pp_print_option (fun fmt h -> fprintf fmt "%a@ <-@ " pp h) fmt p + let pp_parent fmt v = + pp_opt (fun fmt h -> fprintf fmt "%a@ <-@ " pp h) fmt v in - fprintf fmt "%a{ %a }" pp_parent parent (pp_hashtbl ~pp_sep pp_v) data + fprintf fmt "%a{ %a }" pp_parent parent (pp_hashtbl ", " pp_v) data let rec unfold_ite ~(accum : value) (e : value) : (value option * string) list = @@ -90,15 +86,15 @@ module Make (O : Object_intf.S with type value = V.value) = struct | TriOpt (Operator.ITE, c, Val (Val.Loc l), v) -> Ok ((Some c, l) :: unfold_ite ~accum:(UnOpt (Operator.LogicalNot, c)) v) | _ -> - Error (Format.asprintf "Value '%a' is not a loc expression" V.Pp.pp e) + Error (Fmt.asprintf "Value '%a' is not a loc expression" V.Pp.pp e) let pp_val (h : t) (e : value) : string = match e with | V.Val (Val.Loc l) -> ( match get h l with | None -> l - | Some o -> Format.asprintf "%s -> %a" l O.pp o ) - | _ -> Format.asprintf "%a" V.Pp.pp e + | Some o -> Fmt.asprintf "%s -> %a" l O.pp o ) + | _ -> Fmt.asprintf "%a" V.Pp.pp e end module M : diff --git a/ECMA-SL/functorial/symbolic_object.ml b/ECMA-SL/functorial/symbolic_object.ml index 2cd5e90e28..acbeae709d 100644 --- a/ECMA-SL/functorial/symbolic_object.ml +++ b/ECMA-SL/functorial/symbolic_object.ml @@ -32,7 +32,7 @@ module M : Object_intf.S with type value = V.value = struct o let is_empty o = VMap.(is_empty o.fields && is_empty o.symbols) - let to_list o = VMap.to_list o.symbols @ VMap.to_list o.fields + let to_list o = VMap.bindings o.symbols @ VMap.bindings o.fields let get_fields o = let symbols = VMap.fold (fun key _ acc -> key :: acc) o.symbols [] in @@ -115,15 +115,15 @@ module M : Object_intf.S with type value = V.value = struct | _ -> assert false let pp_map fmt v = - Format.pp_print_seq - ~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ") + let map_iter f m = VMap.iter (fun k d -> f (k, d)) m in + Fmt.pp_iter "," map_iter (fun fmt (key, data) -> - Format.fprintf fmt {|"%a": %a|} V.Pp.pp key V.Pp.pp data ) - fmt (VMap.to_seq v) + Fmt.fprintf fmt {|"%a": %a|} V.Pp.pp key V.Pp.pp data ) + fmt v let pp fmt { fields; symbols } = - Format.fprintf fmt "{ %a, %a }" pp_map fields pp_map symbols + Fmt.fprintf fmt "{ %a, %a }" pp_map fields pp_map symbols - let to_string o = Format.asprintf "%a" pp o + let to_string o = Fmt.asprintf "%a" pp o let to_json = to_string end