000001| (** Abstract datatype and operations for property maps (environments) *)
000002|
000003| module Abs = Absencelattice
000004| module VL = Valuelattice
000005|
000006| module TableKey = struct
000007| type t =
000008| | String of string
000009| | Metatable
000010| let compare k k' = match (k,k') with
000011| | Metatable, Metatable -> (*[2309]*)0
000012| | String _, Metatable -> (*[484]*)-1 (* ordering: forall s. s < metatable = metatable *)
000013| | Metatable, String _ -> (*[1532]*)1
000014| | String s, String s' -> (*[4132418]*)String.compare s s'
000015| end
000016| module TableMap = Map.Make(TableKey)
000017|
000018| module ScopeChainSet =
000019| Set.Make(struct type t = int list
000020| let rec compare is1 is2 = match is1,is2 with
000021| | [],[] -> (*[194104]*)0
000022| | [],_ -> (*[0]*)1
000023| | _,[] -> (*[0]*)-1
000024| | i1::is1',i2::is2' ->
000025| (*[397635]*)let r = compare is1' is2' in
000026| (match r with
000027| | 0 -> (*[397635]*)i1 - i2
000028| | _ -> (*[0]*)r) end)
000029|
000030| (* TODO: add default (integer) index for more precise "array approximation" *)
000031| type elem =
000032| | Bot
000033| | Table of table
000034| and table = { table : (VL.elem * Abs.elem) TableMap.t;
000035| default_str : VL.elem; (* fallback for string entries *)
000036| default_key : VL.elem; (* collective approx. of non-string keys *)
000037| default : VL.elem; (* collective approx. of non-string entries *)
000038| scopechain : ScopeChainSet.t; }
000039|
000040| (* table : table -> elem *)
000041| let table { table; default_str; default_key; default; scopechain } =
000042| (*[1250592]*)Table { table; default_str; default_key; default; scopechain }
000043|
000044| (* bot : elem *)
000045| let bot = (*[1]*)Bot
000046|
000047| (* mt : elem *)
000048| let mt = (*[1]*)Table { table = TableMap.empty;
000049| default_str = VL.bot;
000050| default_key = VL.bot;
000051| default = VL.bot;
000052| scopechain = ScopeChainSet.empty; }
000053|
000054| (* leq : elem -> elem -> bool *)
000055| let leq m0 m1 = match m0,m1 with
000056| | Bot,_ -> (*[53]*)true
000057| | _,Bot -> (*[48033]*)false
000058| | Table m0,Table m1 ->
000059| (*[70850]*)VL.leq m0.default_str m1.default_str
000060| && (*[70839]*)VL.leq m0.default_key m1.default_key
000061| && (*[70826]*)VL.leq m0.default m1.default
000062| && (*[70824]*)((*[70824]*)TableMap.fold
000063| (fun p (v,a) acc ->
000064| (*[194349]*)acc
000065| && ((*[194267]*)try (*[194267]*)let v',a' = TableMap.find p m0.table in
000066| ((*[194267]*)VL.leq v' v && (*[194231]*)Abs.leq a' a)
000067| with Not_found -> (* not necessarily in first map *)
000068| (*[0]*)Abs.eq a Abs.maybe_absent)) (* if definite entry in second: not ordered *)
000069| m1.table true)
000070| && (*[70787]*)((*[70787]*)TableMap.fold
000071| (fun p (v,a) acc ->
000072| (*[194098]*)acc
000073| &&
000074| ((*[194098]*)try (*[194098]*)let _ = TableMap.find p m1.table in
000075| (*[194094]*)true (* elements in both have already been checked above *)
000076| with Not_found -> (* not necessarily in second map *)
000077| (match p with
000078| | TableKey.String s -> ((*[4]*)VL.leq v m1.default_str)
000079| | TableKey.Metatable -> (*[0]*)false))) (* metatable in first, but not in second *)
000080| m0.table true)
000081| && (*[70785]*)ScopeChainSet.subset m0.scopechain m1.scopechain
000082|
000083| (* eq : elem -> elem -> bool *)
000084| let eq m0 m1 = (*[0]*)leq m0 m1 && (*[0]*)leq m1 m0 (* a pragmatic implementation choice *)
000085|
000086| (* join : elem -> elem -> elem *)
000087| let join m0 m1 = match m0,m1 with
000088| | Bot,_ -> (*[0]*)m1
000089| | _,Bot -> (*[0]*)m0
000090| | Table m0,Table m1 ->
000091| (*[1246867]*)let def_str = VL.join m0.default_str m1.default_str in
000092| (*[1246867]*)let def_key = VL.join m0.default_key m1.default_key in
000093| (*[1246867]*)let def = VL.join m0.default m1.default in
000094| (*[1246867]*)let tab = TableMap.merge (fun s l0 l1 -> match l0,l1 with
000095| | None, None -> (*[0]*)None
000096| | None, Some (v1,a1) ->
000097| (match s with
000098| | TableKey.String s ->
000099| (*[47]*)Some (VL.join m0.default_str v1, Abs.maybe_absent)
000100| | TableKey.Metatable ->
000101| (*[0]*)Some (v1, Abs.maybe_absent)) (* default does not include metatables *)
000102| | Some (v0,a0), None ->
000103| (match s with
000104| | TableKey.String s ->
000105| (*[100]*)Some (VL.join v0 m1.default_str, Abs.maybe_absent) (*fixed was: m1.default *)
000106| | TableKey.Metatable ->
000107| (*[0]*)Some (v0, Abs.maybe_absent))
000108| | Some (v0,a0), Some (v1,a1) -> (*[2796711]*)Some (VL.join v0 v1, Abs.join a0 a1)) m0.table m1.table in
000109| (*[1246867]*)let sch = ScopeChainSet.union m0.scopechain m1.scopechain in
000110| (*[1246867]*)table { table = tab; default_str = def_str; default_key = def_key; default = def; scopechain = sch }
000111|
000112| exception Returnbot
000113|
000114| (* meet : elem -> elem -> elem *)
000115| let meet m0 m1 = match m0,m1 with
000116| | Bot,_ -> (*[0]*)bot
000117| | _,Bot -> (*[0]*)bot
000118| | Table m0,Table m1 ->
000119| (*[0]*)try
000120| (*[0]*)let def_str = VL.meet m0.default_str m1.default_str in
000121| (*[0]*)let def_key = VL.meet m0.default_key m1.default_key in
000122| (*[0]*)let def = VL.meet m0.default m1.default in
000123| (*[0]*)let tab = TableMap.merge (fun s l0 l1 -> match l0,l1 with
000124| | None, None -> (*[0]*)None
000125| | None, Some (v1,a1) ->
000126| (match s with
000127| | TableKey.String s ->
000128| (*[0]*)let entrycand = VL.meet m0.default_str v1 in
000129| (*[0]*)if VL.is_bot entrycand
000130| then
000131| ((*[0]*)if Abs.eq a1 Abs.is_present
000132| then (*[0]*)raise Returnbot (* certainly in second, but not in meet --> return bot *)
000133| else (*[0]*)Some (entrycand, a1) (* maybe in second and not in result *)
000134| ) (* -> absent from meet, represented as uncertain bot entry *)
000135| else
000136| (*[0]*)Some (entrycand, a1)
000137| | TableKey.Metatable ->
000138| ((*[0]*)if Abs.eq a1 Abs.is_present
000139| then (*[0]*)raise Returnbot
000140| else (*[0]*)None))
000141| | Some (v0,a0), None ->
000142| (match s with
000143| | TableKey.String s ->
000144| (*[0]*)let entrycand = VL.meet v0 m1.default_str in
000145| (*[0]*)if VL.is_bot entrycand
000146| then
000147| ((*[0]*)if Abs.eq a0 Abs.is_present
000148| then (*[0]*)raise Returnbot (* certainly in first, but not in meet --> return bot *)
000149| else (*[0]*)Some (entrycand, a0) (* maybe in first and not in result *)
000150| ) (* -> absent from meet, represented as uncertain bot entry *)
000151| else (*[0]*)Some (entrycand, a0)
000152| | TableKey.Metatable ->
000153| ((*[0]*)if Abs.eq a0 Abs.is_present
000154| then (*[0]*)raise Returnbot
000155| else (*[0]*)None))
000156| | Some (v0,a0), Some (v1,a1) ->
000157| (*[0]*)let abscand = Abs.meet a0 a1 in
000158| (*[0]*)let entrycand = VL.meet v0 v1 in
000159| (*[0]*)if VL.is_bot entrycand
000160| then
000161| ((*[0]*)if Abs.eq abscand Abs.is_present
000162| then (*[0]*)raise Returnbot (* definite, empty entry -> result is bottom *)
000163| else ((*[0]*)Some (entrycand, abscand)))
000164| else
000165| (*[0]*)Some (entrycand, abscand)) m0.table m1.table in
000166| (*[0]*)let sch = ScopeChainSet.inter m0.scopechain m1.scopechain in
000167| (*[0]*)table { table = tab; default_str = def_str; default_key = def_key; default = def; scopechain = sch }
000168| with Returnbot -> (*[0]*)Bot
000169|
000170| (* is_bot : map -> bool *)
000171| let is_bot pl = (*[10354]*)leq pl bot
000172|
000173| (* mem : str -> map -> bool *)
000174| let mem s map = match map with
000175| | Bot -> (*[0]*)false
000176| | Table map -> (*[1120]*)TableMap.mem (TableKey.String s) map.table
000177|
000178| (* find_exn : str -> map -> VL * Abs *)
000179| let find_exn str map = match map with
000180| | Bot -> (*[85]*)raise Not_found
000181| | Table map -> (*[10250]*)TableMap.find (TableKey.String str) map.table (* used for variable lookup *)
000182|
000183| (* find : str -> map -> VL *)
000184| let find str map = match map with
000185| | Bot -> (*[0]*)VL.bot
000186| | Table map ->
000187| (*[670]*)try
000188| (*[670]*)let (vlat,abs) = TableMap.find (TableKey.String str) map.table in
000189| (*[489]*)if abs = Abs.is_present
000190| then (*[448]*)vlat
000191| else (*[41]*)VL.join vlat VL.nil (* not definite read --> include nil *)
000192| with Not_found ->
000193| (*[181]*)VL.join map.default_str VL.nil (* maybe not covered by default *)
000194|
000195| (* find_nonstr_defaults : map -> VL * VL *)
000196| let find_nonstr_defaults map = match map with
000197| | Bot -> ((*[0]*)VL.bot,VL.bot)
000198| | Table map -> ((*[463]*)map.default_key, map.default)
000199|
000200| (* find_all_keys : map -> VL *)
000201| let find_all_keys map = match map with
000202| | Bot -> (*[0]*)VL.bot
000203| | Table map ->
000204| (*[118]*)TableMap.fold (fun name (_vlat,_abs) acc -> match name with
000205| | TableKey.Metatable -> (*[0]*)acc (* excluding metatable *)
000206| | TableKey.String kname -> (*[256]*)VL.join (VL.string kname) acc)
000207| map.table (VL.join map.default_key
000208| (if VL.is_bot map.default_str then (*[100]*)VL.bot else (*[18]*)VL.anystring))
000209|
000210| (* find_all : map -> VL *)
000211| let find_all map = match map with
000212| | Bot -> (*[0]*)VL.bot
000213| | Table map ->
000214| (*[142]*)TableMap.fold (fun name (vlat,_abs) acc -> match name with
000215| | TableKey.Metatable -> (*[0]*)acc (* excluding metatable *)
000216| | TableKey.String name -> (*[319]*)VL.join vlat acc) map.table map.default_str
000217|
000218| (* get_metatable : map -> VL *)
000219| let get_metatable map = match map with
000220| | Bot -> (*[0]*)VL.bot
000221| | Table map ->
000222| (*[672]*)try
000223| (*[672]*)let (vlat,abs) = TableMap.find TableKey.Metatable map.table in
000224| (*[144]*)if abs = Abs.is_present
000225| then (*[140]*)vlat
000226| else (*[4]*)VL.join vlat VL.nil (* not definite read --> include nil *)
000227| with Not_found -> (*[528]*)VL.nil (* failure: return nil *)
000228|
000229| (* set_metatable : VL -> map -> map *)
000230| let set_metatable v map = match map with
000231| | Bot -> (*[0]*)bot
000232| | Table map ->
000233| (*[66]*)if v = VL.bot
000234| then (*[0]*)bot
000235| else (*[66]*)table { map with table = TableMap.add TableKey.Metatable (v,Abs.is_present) map.table }
000236|
000237| (* set_metatable_absent : map -> map *)
000238| let set_metatable_absent map' = match map' with
000239| | Bot -> (*[0]*)bot
000240| | Table map ->
000241| (*[4]*)try
000242| (*[4]*)let (vlat,abs) = TableMap.find TableKey.Metatable map.table in
000243| (*[4]*)if abs = Abs.is_present (* already marked absent? *)
000244| then (*[4]*)table { map with table = TableMap.add TableKey.Metatable (vlat,Abs.maybe_absent) map.table }
000245| else (*[0]*)map'
000246| with Not_found -> (*[0]*)map' (* failure: return nil *)
000247|
000248| (* add : str -> val -> map -> map *)
000249| let add s v map = match map with
000250| | Bot -> (*[2]*)bot
000251| | Table map ->
000252| (*[1870]*)if VL.leq v VL.bot
000253| then (*[15]*)bot
000254| else
000255| (*[1855]*)table { map with table =
000256| let v' = VL.exclude_nil v in
000257| (*[1855]*)if (*[1855]*)VL.may_be_nil v || (*[1667]*)VL.is_bot v'
000258| then (*[188]*)TableMap.add (TableKey.String s) (v',Abs.maybe_absent) map.table
000259| else (*[1667]*)TableMap.add (TableKey.String s) (v',Abs.is_present) map.table }
000260|
000261| (* add_local : str -> val -> map -> map *)
000262| let add_local s v map = match map with
000263| | Bot -> (*[0]*)bot
000264| | Table map ->
000265| (*[1191]*)if VL.leq v VL.bot
000266| then (*[0]*)bot
000267| else (* adding a local variable with value nil, makes it visible in scope, e.g. for recursion *)
000268| (*[1191]*)table { map with table = TableMap.add (TableKey.String s) (v,Abs.is_present) map.table }
000269|
000270| (* add_nonstr_default : val -> val -> map -> map *)
000271| let add_nonstr_default k v map = match map with
000272| | Bot -> (*[0]*)bot
000273| | Table map ->
000274| (*[190]*)if (*[190]*)VL.leq k VL.bot || (*[190]*)VL.leq v VL.bot
000275| then (*[0]*)bot
000276| else
000277| (*[190]*)let k = VL.exclude_nil k in
000278| (*[190]*)if VL.leq k VL.bot
000279| then (*[44]*)table { map with default_key = VL.bot; default = VL.bot } (* reduce domain *)
000280| else (*[146]*)table { map with default_key = k; default = (VL.exclude_nil v) }
000281|
000282| (* add_scopechain : map -> label list -> map *)
000283| let add_scopechain map sc = match map with
000284| | Bot -> (*[0]*)bot
000285| | Table map -> (*[380]*)table { map with scopechain = ScopeChainSet.add sc map.scopechain }
000286|
000287| (* add_all_str : val -> map -> map *)
000288| let add_all_str v map = match map with
000289| | Bot -> (*[0]*)bot
000290| | Table map ->
000291| (*[39]*)if VL.leq v VL.bot
000292| then (*[0]*)bot
000293| else
000294| (*[39]*)let delete = VL.may_be_nil v in
000295| (*[39]*)table { table = TableMap.mapi
000296| (fun key (old_vlat,old_abs) -> match key with
000297| | TableKey.Metatable -> ((*[0]*)old_vlat,old_abs) (* excluding metatable *)
000298| | TableKey.String _ ->
000299| (*[0]*)if delete
000300| then ((*[0]*)VL.join (VL.exclude_nil v) old_vlat,Abs.maybe_absent)
000301| else ((*[0]*)VL.join (VL.exclude_nil v) old_vlat,old_abs)) map.table;
000302| default_str = VL.join v map.default_str;
000303| default_key = map.default_key;
000304| default = map.default;
000305| scopechain = map.scopechain; }
000306|
000307| (* add_all_params : str list -> val list -> map -> map *)
000308| let rec add_all_params xs vs map' = match map' with
000309| | Bot -> (*[0]*)bot
000310| | Table map -> match (xs,vs) with
000311| | [] , [] -> (*[458]*)map'
000312| | [] , v::vs -> (*[16]*)map' (* drop superflous arguments *)
000313| | x::xs, [] -> (*[10]*)add_all_params xs vs (add x VL.nil (Table map)) (* unsupplied args are nil *)
000314| | x::xs, v::vs -> (*[609]*)add_all_params xs vs (add x v (Table map))
000315|
000316|
000317| (** {2 Pretty printing} *)
000318|
000319| (* pprint : PL -> unit *)
000320| let pprint plat =
000321| (* string_of_tablekey : tablekey -> string *)
000322| let string_of_tablekey k = match k with
000323| | TableKey.Metatable -> "metatable"
000324| | TableKey.String s -> "\"" ^ s ^ "\""
000325| in
000326| (* pprint_list : int list -> unit *)
000327| let pprint_list is =
000328| begin
000329| Format.printf "[ @[<h 1>";
000330| ignore (List.fold_left (fun first i ->
000331| if first
000332| then (Format.print_int i; false)
000333| else
000334| begin
000335| Format.printf ",";
000336| Format.print_space ();
000337| Format.print_int i;
000338| false
000339| end) true is);
000340| Format.printf "@] ]";
000341| end in
000342| match plat with
000343| | Bot -> Format.printf "bot"
000344| | Table plat ->
000345| begin
000346| Format.printf "{ @[<v 0>";
000347| (* print table *)
000348| let first =
000349| TableMap.fold (fun prop (vlat,abs) first ->
000350| if first
000351| then
000352| begin
000353| Format.printf "%-12s -> " (string_of_tablekey prop);
000354| Abs.pprint abs;
000355| Format.printf " ";
000356| VL.pprint vlat;
000357| false
000358| end
000359| else
000360| begin
000361| Format.print_space ();
000362| Format.printf "%-12s -> " (string_of_tablekey prop);
000363| Abs.pprint abs; Format.printf " "; VL.pprint vlat;
000364| false
000365| end) plat.table true in
000366| (* prettyprint default str *)
000367| let first =
000368| (if VL.is_bot plat.default_str
000369| then first
000370| else
000371| begin
000372| (if first then () else Format.print_space ());
000373| Format.printf "%-12s -> " "default str";
000374| VL.pprint plat.default_str;
000375| false
000376| end) in
000377| (* prettyprint default key and default *)
000378| (if VL.is_bot plat.default_key
000379| then ()
000380| else
000381| begin
000382| (if first then () else Format.print_space ());
000383| Format.printf "%-12s -> " "default key";
000384| VL.pprint plat.default_key;
000385| Format.print_space ();
000386| Format.printf "%-12s -> " "default";
000387| VL.pprint plat.default
000388| end);
000389| (* prettyprint scopechain *)
000390| (if plat.scopechain = ScopeChainSet.empty
000391| then ()
000392| else
000393| begin
000394| (if first then () else Format.print_space ());
000395| Format.printf "%-12s -> " "scopechain";
000396| Format.printf "{ @[<h 1>";
000397| ignore (ScopeChainSet.fold (fun sc first ->
000398| if first
000399| then (pprint_list sc; false)
000400| else
000401| begin
000402| Format.printf ",";
000403| Format.print_space ();
000404| pprint_list sc;
000405| false
000406| end) plat.scopechain true);
000407| Format.printf "@] }";
000408| end);
000409| Format.printf "@] }";
000410| end
000411|
000412| (* to_string : elem -> string *)
000413| let to_string pl =
000414| let buf = Buffer.create 128 in
000415| let out,flush = Format.get_formatter_output_functions () in (* save previous outputters *)
000416| begin
000417| Format.set_formatter_output_functions (Buffer.add_substring buf) (fun () -> ());
000418| pprint pl;
000419| Format.print_flush ();
000420| Format.set_formatter_output_functions out flush; (* restore previous outputters *)
000421| Buffer.contents buf
000422| end