000001| (** Abstract store datatype and operations *)
000002|
000003| module VL = Valuelattice
000004| module PL = Proplattice
000005| module StoreMap = Map.Make(struct type t = int
000006| let compare i i' = (*[1719787]*)i - i' end)
000007| module Str = Stringlattice
000008|
000009| type elem = Proplattice.elem StoreMap.t
000010|
000011| (* leq : elem -> elem -> bool *)
000012| let leq st0 st1 =
000013| (*[43643]*)StoreMap.fold (fun lab obj acc ->
000014| (*[702173]*)let obj' = try (*[702173]*)StoreMap.find lab st1
000015| with Not_found -> (*[630846]*)PL.bot
000016| in (*[702173]*)acc && (*[108582]*)PL.leq obj obj') st0 true
000017|
000018| (* eq : elem -> elem -> bool *)
000019| let eq = (*[1]*)StoreMap.equal Proplattice.eq
000020|
000021| (* join : elem -> elem -> elem *)
000022| let join st0 st1 = (*[62745]*)StoreMap.merge (fun lab obj0 obj1 -> match obj0,obj1 with
000023| | None,_ -> (*[19013]*)obj1
000024| | _,None -> (*[52026]*)obj0
000025| | Some obj0,Some obj1 -> (*[1246867]*)Some (PL.join obj0 obj1)) st0 st1
000026|
000027| (* meet : elem -> elem -> elem *)
000032|
000033| (* bot : elem *)
000034| let bot = (*[1]*)StoreMap.empty
000035|
000036|
000037| (** {3 Lattice operations } *)
000038|
000039| (* is_bot : store -> bool *)
000040| let is_bot st = (*[24856]*)leq st bot
000041|
000042| (* add_label : store -> label -> PL -> store *)
000043| let add_label st lab prop =
000044| (*[4259]*)StoreMap.add lab prop st
000045|
000046| (* find_label_exn : store -> label -> PL *)
000047| let find_label_exn st lab =
000048| (*[14765]*)StoreMap.find lab st
000049|
000050| (* find_label : store -> label -> PL *)
000051| let find_label st lab =
000052| (*[12859]*)try (*[12859]*)find_label_exn st lab
000053| with Not_found -> (*[109]*)PL.bot
000054|
000055| (* fold_labels_scopechain : (label list -> 'a -> 'a) -> store -> label -> 'a -> 'a *)
000056| let fold_labels_scopechain f st lab acc =
000057| (*[470]*)if is_bot st
000058| then (*[2]*)acc
000059| else
000060| (*[468]*)try
000061| (*[468]*)let pl = find_label st lab in
000062| (match pl with
000073| else
000074| (*[828]*)let tables = vlat.VL.tables in
000075| (*[828]*)VL.LabelSet.fold (fun lab acc ->
000076| (*[497]*)let plat = find_label st lab in
000077| (*[497]*)VL.join acc (PL.find prop plat) ) tables VL.bot
000078|
000079| (* lookup_all_keys : store -> VL -> VL *)
000080| let lookup_all_keys st vlat =
000081| (*[97]*)let tables = vlat.VL.tables in
000082| (*[97]*)VL.LabelSet.fold (fun lab acc ->
000083| (*[118]*)let plat = find_label st lab in
000084| (*[118]*)VL.join acc (PL.find_all_keys plat) ) tables VL.bot
000085|
000086| (* lookup_all_str_props : store -> VL -> VL *)
000087| let lookup_all_str_props st vlat =
000088| (*[126]*)let tables = vlat.VL.tables in
000089| (*[126]*)VL.LabelSet.fold (fun lab acc ->
000090| (*[142]*)let plat = find_label st lab in
000091| (*[142]*)VL.join acc (PL.find_all plat) ) tables VL.bot
000092|
000093| (* lookup_all_nonstr_props : store -> VL -> VL *)
000094| let lookup_all_nonstr_props st vlat =
000095| (*[95]*)let tables = vlat.VL.tables in
000096| (*[95]*)VL.LabelSet.fold (fun lab acc ->
000097| (*[116]*)let plat = find_label st lab in
000098| (*[116]*)VL.join acc (snd (PL.find_nonstr_defaults plat))) tables VL.bot
000099|
000100| (* lookup_all_props : store -> VL -> VL *)
000101| let lookup_all_props st vlat =
000102| (*[79]*)VL.join (lookup_all_str_props st vlat) (lookup_all_nonstr_props st vlat)
000103|
000104| (* lookup_nonstr_default_prop : store -> VL -> VL -> VL *)
000105| let lookup_nonstr_default_prop st vlat vlat' =
000106| (*[288]*)if (*[288]*)is_bot st (*|| VL.is_bot vlat*) || (*[288]*)VL.is_bot vlat'
000108| else
000109| (*[288]*)let tables = vlat.VL.tables in
000110| (*[288]*)VL.LabelSet.fold (fun lab acc ->
000111| (*[176]*)let plat = find_label st lab in
000112| (*[176]*)let def_key,def = PL.find_nonstr_defaults plat in (* Note: for non-str entries *)
000113| (*[176]*)let acc' = VL.join VL.nil acc in
000114| (*[176]*)if VL.is_bot (VL.meet vlat' def_key)
000115| then (*[70]*)acc'
000116| else (*[106]*)VL.join acc' def) tables VL.bot
000117|
000118| (* lookup_dyn_prop : store -> VL -> VL -> VL *)
000119| let lookup_dyn_prop st vlat vlat' =
000120| (*[2411]*)if (*[2411]*)is_bot st || (*[2411]*)VL.is_bot vlat (* No indexed expr values *)
000121| || (*[1108]*)VL.is_bot vlat' (* No indexing expr values *)
000122| then (*[1303]*)VL.bot
000123| else
000124| (*[1108]*)let res = if VL.may_be_non_strings vlat'
000125| then (*[288]*)lookup_nonstr_default_prop st vlat vlat' (* all relevant default entries *)
000126| else (*[820]*)VL.bot in
000127| (*[1108]*)let strres = match vlat'.VL.strings with
000128| | Str.Top -> (*[38]*)lookup_all_str_props st vlat
000129| | Str.Const s -> (*[820]*)lookup_str_prop st vlat s
000130| | Str.Bot -> (*[250]*)VL.bot in
000131| (*[1108]*)VL.join res strres
000132|
000133| (* raw_get : store -> VL -> VL -> VL *)
000134| let raw_get = (*[1]*)lookup_dyn_prop
000135|
000136| (* write_str_prop : store -> VL -> str -> VL -> store *)
000137| let write_str_prop st vlat prop vlat' =
000139| (*[155]*)let tables = vlat.VL.tables in
000140| (*[155]*)VL.LabelSet.fold
000141| (fun lab stacc ->
000142| (*[155]*)try
000143| (*[155]*)let plat = find_label_exn st lab in
000144| (*[155]*)let old_vlat = PL.find prop plat in (* can be improved if not (str <= def_key) *)
000145| (*[155]*)let new_plat = PL.add prop (VL.join vlat' (* join in default + weak update *)
000146| (VL.exclude_nil old_vlat)) plat in
000147| (* if prev. entry was nil (not present) filter it and add strongly *)
000148| (*[155]*)join (add_label st lab new_plat) stacc (* improvements: exclude nil from vlat', model removal *)
000149| with Not_found -> ((*Printf.printf "Unknown allocation site label %i\n" lab;*)
000156| else
000157| (*[39]*)let tables = vlat0.VL.tables in
000158| (*[39]*)VL.LabelSet.fold (fun lab stacc ->
000159| (*[39]*)try
000160| (*[39]*)let plat = find_label_exn st lab in
000161| (*[39]*)let new_plat = PL.add_all_str vlat plat in (* weak updates all str entries -- incl.default_str *)
000162| (*[39]*)add_label stacc lab new_plat
000163| with Not_found -> ((*Printf.printf "Unknown allocation site label %i\n" lab;*)
000170| else
000171| (*[171]*)let tables = vlat0.VL.tables in
000172| (*[171]*)VL.LabelSet.fold (fun lab stacc ->
000173| (*[171]*)let plat = find_label st lab in
000174| (*[171]*)let old_def_key, old_def = PL.find_nonstr_defaults plat in
000175| (*[171]*)let new_plat = PL.add_nonstr_default (VL.join vlat1 old_def_key) (VL.join vlat old_def) plat in (* weak update in default *)
000176| (*[171]*)add_label stacc lab new_plat) tables st
000177|
000178| (* write_dyn_prop : store -> VL -> VL -> VL -> store *)
000179| let write_dyn_prop st vlat0 vlat1 vlat =
000180| (*[353]*)if (*[353]*)is_bot st || (*[311]*)VL.is_bot vlat0 (* No indexed expr values *)
000181| || (*[311]*)VL.is_bot vlat1 (* No indexing expr values *)
000182| || (*[311]*)VL.is_bot vlat (* No value to write *)
000183| then (*[42]*)bot
000184| else
000185| (*[311]*)let res = if VL.may_be_non_strings vlat1
000186| then (*[171]*)write_default_nonstr_prop st vlat0 (VL.exclude_strings vlat1) vlat (* write to all relevant default entries *)
000187| else (*[140]*)bot in (* don't *)
000188| (*[311]*)let strres = match vlat1.VL.strings with
000189| | Str.Top -> (*[39]*)write_all_str_props st vlat0 vlat
000190| | Str.Const s -> (*[155]*)write_str_prop st vlat0 s vlat
000191| | Str.Bot -> (*[117]*)bot in
000192| (*[311]*)if is_bot res
000193| then (*[140]*)strres
000194| else (*[171]*)join res strres
000195|
000196| (* raw_set : store -> VL -> VL -> VL -> store *)
000197| let raw_set = (*[1]*)write_dyn_prop
000198|
000199| (* get_metatable : store -> VL -> VL *)
000200| let get_metatable st vlat = (* fixme: strings have a metatable with a __index metamethod? *)
000201| (*[8]*)if (*[8]*)is_bot st || (*[8]*)VL.is_bot vlat
000203| else (* semantics: http://www.lua.org/manual/5.1/manual.html#pdf-getmetatable *)
000204| (*[8]*)let tables = vlat.VL.tables in
000205| (*[8]*)VL.LabelSet.fold (fun lab acc ->
000206| (*[8]*)let plat = find_label st lab in (* for each table: *)
000207| (*[8]*)let metatabs = PL.get_metatable plat in (* lookup metatable *)
000208| (*[8]*)let metametatabs =
000209| VL.LabelSet.fold (fun metalab acc ->
000210| (*[10]*)let metatab = find_label st metalab in (* and __metatable in metatable *)
000211| (*[10]*)let metametatab = PL.find "__metatable" metatab in
000212| (*[10]*)if VL.may_be_nil metametatab (* second lookup may fail: include metatab *)
000213| then (*[10]*)VL.join (VL.table metalab) (VL.join (VL.exclude_nil metametatab) acc)
000215| (*[8]*)VL.join acc
000216| (VL.join (VL.exclude_tables metatabs) metametatabs)) tables VL.bot
000217|
000218| (* set_metatable : store -> VL -> VL -> store *)
000219| let set_metatable st vlat metavlat =
000220| (*[70]*)if is_bot st
000222| else (* semantics: http://www.lua.org/manual/5.1/manual.html#pdf-setmetatable *)
000223| (*[70]*)let tables = vlat.VL.tables in
000224| (*[70]*)VL.LabelSet.fold (fun lab stacc ->
000225| (*[70]*)try
000226| (*[70]*)let plat = find_label_exn st lab in
000227| (*[70]*)let old_metavlat = PL.get_metatable plat in
000228| (*[70]*)join stacc
000229| (join
000230| (* no metatable present -> set it *)
000231| (if VL.may_be_nil old_metavlat
000232| then (* normal operation *)
000233| (*[62]*)let plat' = PL.set_metatable (VL.exclude_nil metavlat) plat in
000234| (*[62]*)add_label st lab plat'
000235| else (*[8]*)bot)
000236|
000237| (* metatable labels present, potentially with __metatable fields *)
000238| (VL.LabelSet.fold (fun metalab acc ->
000239| (*[8]*)let metatab = find_label st metalab in
000240| (*[8]*)let metametatab = PL.find "__metatable" metatab in
000241| (*[8]*)if VL.may_be_nil metametatab
000242| then (* may fail to have __metatable field, i.e., may succeed -> update *)
000243| (*[6]*)if (*[6]*)VL.may_be_nil metavlat && (*[4]*)VL.is_nil metavlat (* "rhs" definitely nil *)
000244| then
000245| (*[2]*)let plat' = PL.set_metatable_absent plat in (* weak update: delete+keep = maybe absent *)
000246| (*[2]*)join acc (add_label st lab plat')
000247| else (* weak update *)
000248| (*[4]*)if VL.may_be_nil metavlat (* maybe delete, maybe write = maybe absent *)
000249| then
000250| (*[2]*)let plat' = PL.set_metatable (VL.join old_metavlat (VL.exclude_nil metavlat)) plat in
000251| (*[2]*)let plat' = PL.set_metatable_absent plat' in
000252| (*[2]*)join acc (add_label st lab plat')
000253| else (* just write *)
000254| (*[2]*)let plat' = PL.set_metatable (VL.join old_metavlat (VL.exclude_nil metavlat)) plat in
000255| (*[2]*)join acc (add_label st lab plat')
000256| else
000257| (*[2]*)acc (* error, so return bot, i.e., no effect on acc *) ) old_metavlat.VL.tables bot))
000258| with Not_found -> ((*Printf.printf "Unknown allocation site label %i\n" lab;*)
000260|
000261| (* The following function helps to implement the metatable(obj)[event] notation *)
000262| (* modelling an internal metatable lookup *)
000263| (* This operation differs from the semantics of the API getmetatable (it is unprotected) *)
000264| (* despite the explanation in http://www.lua.org/manual/5.1/manual.html#2.8 *)
000265| (* myget_metatable : store -> VL -> VL *)
000266| let myget_metatable st vlat = (* fixme: strings have a metatable with a __index metamethod? *)
000267| (*[1431]*)if (*[1431]*)is_bot st || (*[1431]*)VL.is_bot vlat
000269| else
000270| (*[1431]*)let tables = vlat.VL.tables in
000271| (*[1431]*)VL.LabelSet.fold (fun lab acc ->
000272| (*[594]*)let plat = find_label st lab in (* for each table: *)
000273| (*[594]*)let metatabs = PL.get_metatable plat in (* lookup metatable *)
000274| (*[594]*)VL.join acc metatabs) tables VL.bot
000275|
000276| (* lookup_event : ST -> VL -> string -> VL *)
000277| let lookup_event st vlat strevent = (* corresponds to metatable(obj)[event] notation in manual *)
000278| (*[1431]*)if (*[1431]*)is_bot st || (*[1431]*)VL.is_bot vlat
000280| else
000281| (*[1431]*)let base = myget_metatable st vlat in (* http://www.lua.org/manual/5.1/manual.html#2.8 *)
000282| (*[1431]*)let res = raw_get st (VL.exclude_nil base) (VL.string strevent) in
000283| (*[1431]*)if VL.may_be_nil base
000284| then (*[452]*)VL.join VL.nil res
000285| else (*[979]*)res
000286|
000287| (* getbinhandler : ST -> VL -> VL -> string -> VL *)
000288| let getbinhandler st vlat0 vlat1 strevent =
000289| (*[299]*)if (*[299]*)is_bot st || (*[228]*)VL.is_bot vlat0 || (*[228]*)VL.is_bot vlat1 (* FIXED *)
000290| then (*[71]*)VL.bot
000291| else (*[228]*)VL.or_join (lookup_event st vlat0 strevent)
000292| (lookup_event st vlat1 strevent)
000293|
000294|
000295| (** {3 Pretty printing} *)
000296|
000297| (* pprint : store -> unit *)
000298| let pprint st =
000299| begin
000300| Format.printf "{ @[<v 0>";
000301| ignore (StoreMap.fold (fun lab plat first ->
000302| if first
000303| then (Format.printf "%-8i -> " lab; PL.pprint plat; false)
000304| else
000305| begin
000306| Format.print_space ();
000307| Format.printf "%-8i -> " lab;
000308| PL.pprint plat;
000309| false
000310| end) st true);
000311| Format.printf "@]}";
000312| end
000313|
000314| (* to_string : elem -> string *)
000315| let to_string st =
000316| let buf = Buffer.create 128 in
000317| let out,flush = Format.get_formatter_output_functions () in (* save previous outputters *)
000318| begin
000319| Format.set_formatter_output_functions (Buffer.add_substring buf) (fun () -> ());
000320| pprint st;
000321| Format.print_flush ();
000322| Format.set_formatter_output_functions out flush; (* restore previous outputters *)
000323| Buffer.contents buf
000324| end
000028| let meet st0 st1 = (*[0]*)StoreMap.merge (fun lab obj0 obj1 -> match obj0,obj1 with