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 -> (*[8846877]*)0
000012| | String _, Metatable -> (*[9143320]*)-1 (* ordering: forall s. s < metatable = metatable *)
000013| | Metatable, String _ -> (*[21045544]*)1
000014| | String s, String s' -> (*[354728590]*)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| | [],[] -> (*[46535215]*)0
000022| | [],_ -> (*[22992672]*)1
000023| | _,[] -> (*[23008930]*)-1
000024| | i1::is1',i2::is2' ->
000025| (*[400758778]*)let r = compare is1' is2' in
000026| (match r with
000027| | 0 -> (*[194412770]*)i1 - i2
000028| | _ -> (*[206346008]*)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| (*[8956748]*)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,_ -> (*[1021774]*)true
000057| | _,Bot -> (*[894970]*)false
000058| | Table m0,Table m1 ->
000059| (*[5472200]*)VL.leq m0.default_str m1.default_str
000060| && (*[5472200]*)VL.leq m0.default_key m1.default_key
000061| && (*[5472200]*)VL.leq m0.default m1.default
000062| && (*[5472200]*)((*[5472200]*)TableMap.fold
000063| (fun p (v,a) acc ->
000064| (*[40437922]*)acc
000065| && ((*[40437922]*)try (*[40437922]*)let v',a' = TableMap.find p m0.table in
000066| ((*[39342488]*)VL.leq v' v && (*[39342488]*)Abs.leq a' a)
000067| with Not_found -> (* not necessarily in first map *)
000068| (*[1095434]*)Abs.eq a Abs.maybe_absent)) (* if definite entry in second: not ordered *)
000069| m1.table true)
000070| && (*[5472200]*)((*[5472200]*)TableMap.fold
000071| (fun p (v,a) acc ->
000072| (*[39553530]*)acc
000073| &&
000074| ((*[39553530]*)try (*[39553530]*)let _ = TableMap.find p m1.table in
000075| (*[39342488]*)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 -> ((*[211042]*)VL.leq v m1.default_str)
000125| | None, Some (v1,a1) ->
000126| (match s with
000127| | TableKey.String s ->
000128| (*[295361]*)let entrycand = VL.meet m0.default_str v1 in
000129| (*[295361]*)if VL.is_bot entrycand
000130| then
000131| ((*[153236]*)if Abs.eq a1 Abs.is_present
000132| then (*[8142]*)raise Returnbot (* certainly in second, but not in meet --> return bot *)
000133| else (*[145094]*)Some (entrycand, a1) (* maybe in second and not in result *)
000134| ) (* -> absent from meet, represented as uncertain bot entry *)
000135| else
000136| (*[142125]*)Some (entrycand, a1)
000137| | TableKey.Metatable ->
000138| ((*[24714]*)if Abs.eq a1 Abs.is_present
000139| then (*[5096]*)raise Returnbot
000140| else (*[19618]*)None))
000141| | Some (v0,a0), None ->
000142| (match s with
000143| | TableKey.String s ->
000144| (*[92363]*)let entrycand = VL.meet v0 m1.default_str in
000145| (*[92363]*)if VL.is_bot entrycand
000146| then
000147| ((*[16063]*)if Abs.eq a0 Abs.is_present
000148| then (*[7965]*)raise Returnbot (* certainly in first, but not in meet --> return bot *)
000149| else (*[8098]*)Some (entrycand, a0) (* maybe in first and not in result *)
000150| ) (* -> absent from meet, represented as uncertain bot entry *)
000151| else (*[76300]*)Some (entrycand, a0)
000152| | TableKey.Metatable ->
000153| ((*[10225]*)if Abs.eq a0 Abs.is_present
000154| then (*[5136]*)raise Returnbot
000155| else (*[5089]*)None))
000156| | Some (v0,a0), Some (v1,a1) ->
000157| (*[1668152]*)let abscand = Abs.meet a0 a1 in
000158| (*[1668152]*)let entrycand = VL.meet v0 v1 in
000159| (*[1668152]*)if VL.is_bot entrycand
000160| then
000161| ((*[8109]*)if Abs.eq abscand Abs.is_present
000162| then (*[4279]*)raise Returnbot (* definite, empty entry -> result is bottom *)
000163| else ((*[3830]*)Some (entrycand, abscand)))
000164| else
000165| (*[1660043]*)Some (entrycand, abscand)) m0.table m1.table in
000166| (*[256527]*)let sch = ScopeChainSet.inter m0.scopechain m1.scopechain in
000167| (*[256527]*)table { table = tab; default_str = def_str; default_key = def_key; default = def; scopechain = sch }
000168| with Returnbot -> (*[30618]*)Bot
000169|
000170| (* is_bot : map -> bool *)
000171| let is_bot pl = (*[37678]*)leq pl bot
000172|
000173| (* mem : str -> map -> bool *)
000174| let mem s map = match map with
000176| | Table map -> (*[11259]*)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 -> (*[1677]*)raise Not_found
000181| | Table map -> (*[14669]*)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 -> (*[87443]*)VL.bot
000186| | Table map ->
000187| (*[55297]*)try
000188| (*[55297]*)let (vlat,abs) = TableMap.find (TableKey.String str) map.table in
000189| (*[15448]*)if abs = Abs.is_present
000190| then (*[8128]*)vlat
000191| else (*[7320]*)VL.join vlat VL.nil (* not definite read --> include nil *)
000192| with Not_found ->
000193| (*[39849]*)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 -> ((*[244235]*)VL.bot,VL.bot)
000198| | Table map -> ((*[74293]*)map.default_key, map.default)
000199|
000200| (* find_all_keys : map -> VL *)
000201| let find_all_keys map = match map with
000202| | Bot -> (*[52119]*)VL.bot
000203| | Table map ->
000204| (*[16263]*)TableMap.fold (fun name (_vlat,_abs) acc -> match name with
000205| | TableKey.Metatable -> (*[8432]*)acc (* excluding metatable *)
000206| | TableKey.String kname -> (*[107974]*)VL.join (VL.string kname) acc)
000207| map.table (VL.join map.default_key
000208| (if VL.is_bot map.default_str then (*[778]*)VL.bot else (*[15485]*)VL.anystring))
000209|
000210| (* find_all : map -> VL *)
000211| let find_all map = match map with
000212| | Bot -> (*[76733]*)VL.bot
000213| | Table map ->
000214| (*[22650]*)TableMap.fold (fun name (vlat,_abs) acc -> match name with
000215| | TableKey.Metatable -> (*[11345]*)acc (* excluding metatable *)
000216| | TableKey.String name -> (*[150793]*)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 -> (*[188877]*)VL.bot
000221| | Table map ->
000222| (*[69733]*)try
000223| (*[69733]*)let (vlat,abs) = TableMap.find TableKey.Metatable map.table in
000224| (*[37242]*)if abs = Abs.is_present
000225| then (*[19493]*)vlat
000226| else (*[17749]*)VL.join vlat VL.nil (* not definite read --> include nil *)
000227| with Not_found -> (*[32491]*)VL.nil (* failure: return nil *)
000228|
000229| (* set_metatable : VL -> map -> map *)
000230| let set_metatable v map = match map with
000231| | Bot -> (*[1930]*)bot
000232| | Table map ->
000233| (*[21468]*)if v = VL.bot
000234| then (*[956]*)bot
000235| else (*[20512]*)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 -> (*[1469]*)bot
000240| | Table map ->
000241| (*[5434]*)try
000242| (*[5434]*)let (vlat,abs) = TableMap.find TableKey.Metatable map.table in
000243| (*[3637]*)if abs = Abs.is_present (* already marked absent? *)
000244| then (*[2853]*)table { map with table = TableMap.add TableKey.Metatable (vlat,Abs.maybe_absent) map.table }
000245| else (*[784]*)map'
000246| with Not_found -> (*[1797]*)map' (* failure: return nil *)
000247|
000248| (* add : str -> val -> map -> map *)
000249| let add s v map = match map with
000250| | Bot -> (*[3768]*)bot
000251| | Table map ->
000252| (*[61481]*)if VL.leq v VL.bot
000253| then (*[950]*)bot
000254| else
000255| (*[60531]*)table { map with table =
000256| let v' = VL.exclude_nil v in
000257| (*[60531]*)if (*[60531]*)VL.may_be_nil v || (*[20649]*)VL.is_bot v'
000258| then (*[39882]*)TableMap.add (TableKey.String s) (v',Abs.maybe_absent) map.table
000259| else (*[20649]*)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 -> (*[233126]*)bot
000264| | Table map ->
000265| (*[83308]*)if VL.leq v VL.bot
000266| then (*[955]*)bot
000267| else (* adding a local variable with value nil, makes it visible in scope, e.g. for recursion *)
000268| (*[82353]*)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 -> (*[114664]*)bot
000273| | Table map ->
000274| (*[46703]*)if (*[46703]*)VL.leq k VL.bot || (*[45760]*)VL.leq v VL.bot
000275| then (*[1859]*)bot
000276| else
000277| (*[44844]*)let k = VL.exclude_nil k in
000278| (*[44844]*)if VL.leq k VL.bot
000279| then (*[3]*)table { map with default_key = VL.bot; default = VL.bot } (* reduce domain *)
000280| else (*[44841]*)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 -> (*[1464]*)bot
000285| | Table map -> (*[20885]*)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 -> (*[3507]*)bot
000290| | Table map ->
000291| (*[23844]*)if VL.leq v VL.bot
000292| then (*[951]*)bot
000293| else
000294| (*[22893]*)let delete = VL.may_be_nil v in
000295| (*[22893]*)table { table = TableMap.mapi
000296| (fun key (old_vlat,old_abs) -> match key with
000297| | TableKey.Metatable -> ((*[11670]*)old_vlat,old_abs) (* excluding metatable *)
000298| | TableKey.String _ ->
000299| (*[152541]*)if delete
000300| then ((*[70501]*)VL.join (VL.exclude_nil v) old_vlat,Abs.maybe_absent)
000301| else ((*[82040]*)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 -> (*[1445]*)bot
000310| | Table map -> match (xs,vs) with
000311| | [] , [] -> (*[2763]*)map'
000312| | [] , v::vs -> (*[798]*)map' (* drop superflous arguments *)
000313| | x::xs, [] -> (*[21098]*)add_all_params xs vs (add x VL.nil (Table map)) (* unsupplied args are nil *)
000314| | x::xs, v::vs -> (*[13126]*)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
000079| | TableKey.Metatable -> (*[0]*)false))) (* metatable in first, but not in second *)