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' = (*[33450163]*)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| (*[1209488]*)StoreMap.fold (fun lab obj acc ->
000014| (*[8470200]*)let obj' = try (*[8470200]*)StoreMap.find lab st1
000015| with Not_found -> (*[7385632]*)PL.bot
000016| in (*[8470200]*)acc && (*[2144626]*)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 = (*[498075]*)StoreMap.merge (fun lab obj0 obj1 -> match obj0,obj1 with
000023| | None,_ -> (*[603274]*)obj1
000024| | _,None -> (*[1344051]*)obj0
000025| | Some obj0,Some obj1 -> (*[3200982]*)Some (PL.join obj0 obj1)) st0 st1
000026|
000027| (* meet : elem -> elem -> elem *)
000028| let meet st0 st1 = (*[80332]*)StoreMap.merge (fun lab obj0 obj1 -> match obj0,obj1 with
000029| | None,_ -> (*[310131]*)None
000030| | _,None -> (*[173270]*)None
000031| | Some obj0, Some obj1 -> (*[322438]*)Some (PL.meet obj0 obj1)) st0 st1
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 = (*[515955]*)leq st bot
000041|
000042| (* add_label : store -> label -> PL -> store *)
000043| let add_label st lab prop =
000044| (*[510808]*)StoreMap.add lab prop st
000045|
000046| (* find_label_exn : store -> label -> PL *)
000047| let find_label_exn st lab =
000048| (*[1388314]*)StoreMap.find lab st
000049|
000050| (* find_label : store -> label -> PL *)
000051| let find_label st lab =
000052| (*[1154616]*)try (*[1154616]*)find_label_exn st lab
000053| with Not_found -> (*[686962]*)PL.bot
000054|
000055| (* fold_labels_scopechain : (label list -> 'a -> 'a) -> store -> label -> 'a -> 'a *)
000056| let fold_labels_scopechain f st lab acc =
000068|
000069| (* lookup_str_prop : store -> VL -> str -> VL *)
000070| let lookup_str_prop st vlat prop =
000071| (*[31111]*)if (*[31111]*)is_bot st || (*[29497]*)VL.is_bot vlat
000072| then (*[2581]*)VL.bot
000073| else
000074| (*[28530]*)let tables = vlat.VL.tables in
000075| (*[28530]*)VL.LabelSet.fold (fun lab acc ->
000076| (*[90600]*)let plat = find_label st lab in
000077| (*[90600]*)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| (*[23510]*)let tables = vlat.VL.tables in
000082| (*[23510]*)VL.LabelSet.fold (fun lab acc ->
000083| (*[63382]*)let plat = find_label st lab in
000084| (*[63382]*)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| (*[31988]*)let tables = vlat.VL.tables in
000089| (*[31988]*)VL.LabelSet.fold (fun lab acc ->
000090| (*[94383]*)let plat = find_label st lab in
000091| (*[94383]*)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| (*[28206]*)let tables = vlat.VL.tables in
000096| (*[28206]*)VL.LabelSet.fold (fun lab acc ->
000097| (*[82412]*)let plat = find_label st lab in
000098| (*[82412]*)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| (*[16729]*)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| (*[31720]*)if (*[31720]*)is_bot st (*|| VL.is_bot vlat*) || (*[29752]*)VL.is_bot vlat'
000107| then (*[2932]*)VL.bot
000108| else
000109| (*[28788]*)let tables = vlat.VL.tables in
000110| (*[28788]*)VL.LabelSet.fold (fun lab acc ->
000111| (*[84750]*)let plat = find_label st lab in
000112| (*[84750]*)let def_key,def = PL.find_nonstr_defaults plat in (* Note: for non-str entries *)
000113| (*[84750]*)let acc' = VL.join VL.nil acc in
000114| (*[84750]*)if VL.is_bot (VL.meet vlat' def_key)
000115| then (*[71209]*)acc'
000116| else (*[13541]*)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| (*[72961]*)if (*[72961]*)is_bot st || (*[70592]*)VL.is_bot vlat (* No indexed expr values *)
000121| || (*[33427]*)VL.is_bot vlat' (* No indexing expr values *)
000122| then (*[40521]*)VL.bot
000123| else
000124| (*[32440]*)let res = if VL.may_be_non_strings vlat'
000125| then (*[16720]*)lookup_nonstr_default_prop st vlat vlat' (* all relevant default entries *)
000126| else (*[15720]*)VL.bot in
000127| (*[32440]*)let strres = match vlat'.VL.strings with
000128| | Str.Top -> (*[5259]*)lookup_all_str_props st vlat
000129| | Str.Const s -> (*[21111]*)lookup_str_prop st vlat s
000130| | Str.Bot -> (*[6070]*)VL.bot in
000131| (*[32440]*)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' =
000138| (*[24582]*)if (*[24582]*)is_bot st || (*[22788]*)VL.is_bot vlat || (*[22764]*)VL.is_bot vlat' then (*[1835]*)bot else
000139| (*[22747]*)let tables = vlat.VL.tables in
000140| (*[22747]*)VL.LabelSet.fold
000141| (fun lab stacc ->
000142| (*[69723]*)try
000143| (*[69723]*)let plat = find_label_exn st lab in
000144| (*[17687]*)let old_vlat = PL.find prop plat in (* can be improved if not (str <= def_key) *)
000145| (*[17687]*)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| (*[17687]*)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;*)
000150| (*[52036]*)stacc)) tables bot
000151|
000152| (* write_all_str_props : store -> VL -> VL -> VL -> store *)
000153| let write_all_str_props st vlat0 (*vlat1*) vlat =
000154| (*[23901]*)if (*[23901]*)is_bot st || (*[22926]*)VL.is_bot vlat0 || (*VL.is_bot vlat1 ||*) (*[21958]*)VL.is_bot vlat
000155| then (*[1967]*)bot
000156| else
000157| (*[21934]*)let tables = vlat0.VL.tables in
000158| (*[21934]*)VL.LabelSet.fold (fun lab stacc ->
000159| (*[68234]*)try
000160| (*[68234]*)let plat = find_label_exn st lab in
000161| (*[17351]*)let new_plat = PL.add_all_str vlat plat in (* weak updates all str entries -- incl.default_str *)
000162| (*[17351]*)add_label stacc lab new_plat
000163| with Not_found -> ((*Printf.printf "Unknown allocation site label %i\n" lab;*)
000164| (*[50883]*)stacc)) tables st
000165|
000166| (* write_default_nonstr_prop : store -> VL -> VL -> VL -> store *)
000167| let write_default_nonstr_prop st vlat0 vlat1 vlat =
000168| (*[50545]*)if (*[50545]*)is_bot st || (*[49456]*)VL.is_bot vlat0 || (*[49431]*)VL.is_bot vlat1 || (*[49415]*)VL.is_bot vlat
000169| then (*[1148]*)bot
000170| else
000171| (*[49397]*)let tables = vlat0.VL.tables in
000172| (*[49397]*)VL.LabelSet.fold (fun lab stacc ->
000173| (*[146366]*)let plat = find_label st lab in
000174| (*[146366]*)let old_def_key, old_def = PL.find_nonstr_defaults plat in
000175| (*[146366]*)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| (*[146366]*)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| (*[37327]*)if (*[37327]*)is_bot st || (*[34734]*)VL.is_bot vlat0 (* No indexed expr values *)
000181| || (*[34689]*)VL.is_bot vlat1 (* No indexing expr values *)
000182| || (*[34644]*)VL.is_bot vlat (* No value to write *)
000183| then (*[2743]*)bot
000184| else
000185| (*[34584]*)let res = if VL.may_be_non_strings vlat1
000186| then (*[34545]*)write_default_nonstr_prop st vlat0 (VL.exclude_strings vlat1) vlat (* write to all relevant default entries *)
000187| else (*[39]*)bot in (* don't *)
000188| (*[34584]*)let strres = match vlat1.VL.strings with
000189| | Str.Top -> (*[10901]*)write_all_str_props st vlat0 vlat
000190| | Str.Const s -> (*[11582]*)write_str_prop st vlat0 s vlat
000191| | Str.Bot -> (*[12101]*)bot in
000192| (*[34584]*)if is_bot res
000193| then (*[39]*)strres
000194| else (*[34545]*)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| (*[16993]*)if (*[16993]*)is_bot st || (*[14847]*)VL.is_bot vlat
000202| then (*[3128]*)VL.bot
000203| else (* semantics: http://www.lua.org/manual/5.1/manual.html#pdf-getmetatable *)
000204| (*[13865]*)let tables = vlat.VL.tables in
000205| (*[13865]*)VL.LabelSet.fold (fun lab acc ->
000206| (*[41718]*)let plat = find_label st lab in (* for each table: *)
000207| (*[41718]*)let metatabs = PL.get_metatable plat in (* lookup metatable *)
000208| (*[41718]*)let metametatabs =
000209| VL.LabelSet.fold (fun metalab acc ->
000210| (*[11729]*)let metatab = find_label st metalab in (* and __metatable in metatable *)
000211| (*[11729]*)let metametatab = PL.find "__metatable" metatab in
000212| (*[11729]*)if VL.may_be_nil metametatab (* second lookup may fail: include metatab *)
000213| then (*[3629]*)VL.join (VL.table metalab) (VL.join (VL.exclude_nil metametatab) acc)
000214| else (*[8100]*)VL.join (VL.exclude_nil metametatab) acc) metatabs.VL.tables VL.bot in
000215| (*[41718]*)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| (*[19018]*)if is_bot st
000221| then (*[2221]*)bot
000222| else (* semantics: http://www.lua.org/manual/5.1/manual.html#pdf-setmetatable *)
000223| (*[16797]*)let tables = vlat.VL.tables in
000224| (*[16797]*)VL.LabelSet.fold (fun lab stacc ->
000225| (*[49277]*)try
000226| (*[49277]*)let plat = find_label_exn st lab in
000227| (*[12390]*)let old_metavlat = PL.get_metatable plat in
000228| (*[12390]*)join stacc
000229| (join
000230| (* no metatable present -> set it *)
000231| (if VL.may_be_nil old_metavlat
000232| then (* normal operation *)
000233| (*[8316]*)let plat' = PL.set_metatable (VL.exclude_nil metavlat) plat in
000234| (*[8316]*)add_label st lab plat'
000235| else (*[4074]*)bot)
000236|
000237| (* metatable labels present, potentially with __metatable fields *)
000238| (VL.LabelSet.fold (fun metalab acc ->
000239| (*[13815]*)let metatab = find_label st metalab in
000240| (*[13815]*)let metametatab = PL.find "__metatable" metatab in
000241| (*[13815]*)if VL.may_be_nil metametatab
000242| then (* may fail to have __metatable field, i.e., may succeed -> update *)
000243| (*[4178]*)if (*[4178]*)VL.may_be_nil metavlat && (*[1903]*)VL.is_nil metavlat (* "rhs" definitely nil *)
000244| then
000247| else (* weak update *)
000248| (*[4178]*)if VL.may_be_nil metavlat (* maybe delete, maybe write = maybe absent *)
000249| then
000250| (*[1903]*)let plat' = PL.set_metatable (VL.join old_metavlat (VL.exclude_nil metavlat)) plat in
000251| (*[1903]*)let plat' = PL.set_metatable_absent plat' in
000252| (*[1903]*)join acc (add_label st lab plat')
000253| else (* just write *)
000254| (*[2275]*)let plat' = PL.set_metatable (VL.join old_metavlat (VL.exclude_nil metavlat)) plat in
000255| (*[2275]*)join acc (add_label st lab plat')
000256| else
000257| (*[9637]*)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;*)
000259| (*[36887]*)stacc)) tables bot
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| (*[61893]*)if (*[61893]*)is_bot st || (*[60236]*)VL.is_bot vlat
000268| then (*[2629]*)VL.bot
000269| else
000270| (*[59264]*)let tables = vlat.VL.tables in
000271| (*[59264]*)VL.LabelSet.fold (fun lab acc ->
000272| (*[198598]*)let plat = find_label st lab in (* for each table: *)
000273| (*[198598]*)let metatabs = PL.get_metatable plat in (* lookup metatable *)
000274| (*[198598]*)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| (*[54518]*)if (*[54518]*)is_bot st || (*[52850]*)VL.is_bot vlat
000279| then (*[2625]*)VL.bot
000280| else
000281| (*[51893]*)let base = myget_metatable st vlat in (* http://www.lua.org/manual/5.1/manual.html#2.8 *)
000282| (*[51893]*)let res = raw_get st (VL.exclude_nil base) (VL.string strevent) in
000283| (*[51893]*)if VL.may_be_nil base
000284| then (*[19946]*)VL.join VL.nil res
000285| else (*[31947]*)res
000286|
000287| (* getbinhandler : ST -> VL -> VL -> string -> VL *)
000288| let getbinhandler st vlat0 vlat1 strevent =
000289| (*[30000]*)if (*[30000]*)is_bot st || (*[26109]*)VL.is_bot vlat0 || (*[24183]*)VL.is_bot vlat1 (* FIXED *)
000290| then (*[7741]*)VL.bot
000291| else (*[22259]*)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
000057| (*[0]*)if is_bot st