000001| (** Abstract value datatype and operations *)
000002|
000003| module Num = Numberlattice
000004| module Str = Stringlattice
000005|
000006| (** {3 Lattice type and primitives } *)
000007|
000008| type tag =
000009| | Nil
000010| | Bool
000011| | Userdata
000012|
000013| type proc =
000014| | Funtag of int
000015| | Builtin of builtin
000016| and builtin =
000017| | Error
000018| | Exit
000019| | Next
000020| | INext (* internal to IPairs *)
000021| | Pairs
000022| | IPairs
000023| | Print
000024| | Write
000025| | Tonumber
000026| | Tostring
000027| | Abs
000028| | Ceil
000029| | Floor
000030| | Mod
000031| | Random
000032| | Strlen
000033| | Strupper
000034| | Strlower
000035| | Strchar
000036| | Strbyte
000037| | Strsub
000038| | Sqrt
000039| | Type
000040| | Format
000041| | Tblconcat
000042| | Getmetatable
000043| | Setmetatable
000044| | Rawget
000045| | Rawset
000046|
000047| (* TODO: experiment with Patricia trees *)
000048| module TagSet = Set.Make(struct type t = tag
000049| let compare = (*[1]*)Pervasives.compare end)
000050| module ProcSet = Set.Make(struct type t = proc
000051| let compare = (*[1]*)Pervasives.compare end)
000052| module LabelSet = Set.Make(struct type t = int
000053| let compare = (*[1]*)Pervasives.compare end)
000054|
000055| type elem = { tags : TagSet.t;
000056| number : Num.elem;
000057| strings : Str.elem;
000058| funs : ProcSet.t;
000059| tables : LabelSet.t; }
000060|
000061| (* let top = *)
000062|
000063| let mttagset = (*[1]*)TagSet.empty
000064| let mtprocset = (*[1]*)ProcSet.empty
000065| let mtlabelset = (*[1]*)LabelSet.empty
000066|
000067| (* bot : VL *)
000068| let bot = (*[1]*){ tags = mttagset;
000069| number = Num.bot;
000070| strings = Str.bot;
000071| funs = mtprocset;
000072| tables = mtlabelset; }
000073|
000074| let mktagelem t = (*[3]*){ bot with tags = TagSet.singleton t }
000075|
000076| (* nil : VL *)
000077| let nil = (*[1]*)mktagelem Nil
000078|
000079| (* bool : VL *)
000080| let bool = (*[1]*)mktagelem Bool
000081|
000082| (* number : VL *)
000083| let number = (*[1]*){ bot with number = Num.top }
000084|
000085| (* userdata : VL *)
000086| let userdata = (*[1]*)mktagelem Userdata
000087|
000088| (* string : string -> VL *)
000089| let string s = (*[208633]*){ bot with strings = Str.const s }
000090|
000091| (* anystring : VL *)
000092| let anystring = (*[1]*){ bot with strings = Str.top }
000093|
000094| (* table : label -> VL *)
000095| let table t = (*[3636]*){ bot with tables = LabelSet.singleton t }
000096|
000097| (* proc : label -> VL *)
000099|
000100| (* builtin : builtin -> VL *)
000101| let builtin b = (*[13489]*){ bot with funs = ProcSet.singleton (Builtin b) }
000102|
000103| (* eq : VL -> VL -> bool *)
000104| let eq v1 v2 =
000105| (*[707613]*)TagSet.equal v1.tags v2.tags
000106| && (*[707613]*)Num.eq v1.number v2.number
000107| && (*[707613]*)Str.eq v1.strings v2.strings
000108| && (*[707613]*)ProcSet.equal v1.funs v2.funs
000109| && (*[707613]*)LabelSet.equal v1.tables v2.tables
000110|
000111| (* leq : VL -> VL -> bool *)
000112| let leq v1 v2 =
000113| (*[63008002]*)TagSet.subset v1.tags v2.tags
000114| && (*[59570913]*)Num.leq v1.number v2.number
000115| && (*[58642715]*)Str.leq v1.strings v2.strings
000116| && (*[57943094]*)ProcSet.subset v1.funs v2.funs
000117| && (*[57328764]*)LabelSet.subset v1.tables v2.tables
000118|
000119| (* join : VL -> VL -> VL *)
000120| let join v1 v2 =
000121| (*[25409118]*){ tags = TagSet.union v1.tags v2.tags;
000122| number = Num.join v1.number v2.number;
000123| strings = Str.join v1.strings v2.strings;
000124| funs = ProcSet.union v1.funs v2.funs;
000125| tables = LabelSet.union v1.tables v2.tables; }
000126|
000127| (* meet : VL -> VL -> VL *)
000128| let meet v1 v2 =
000129| (*[3824609]*){ tags = TagSet.inter v1.tags v2.tags;
000130| number = Num.meet v1.number v2.number;
000131| strings = Str.meet v1.strings v2.strings;
000132| funs = ProcSet.inter v1.funs v2.funs;
000133| tables = LabelSet.inter v1.tables v2.tables; }
000134|
000135| (* number_or_nil : VL *)
000136| let number_or_nil = (*[1]*)join nil number
000137|
000138|
000139| (** {3 Lattice queries } *)
000140|
000141| (** Is argument bot in lattice order? *)
000142| (* is_bot : VL -> bool *)
000143| let is_bot vlat = (*[5310877]*)leq vlat bot
000144|
000145| (** Is argument at most nil in lattice order? *)
000146| (* is_nil : VL -> bool *)
000147| let is_nil vlat = (*[20752]*)leq vlat nil
000148|
000149| (** Is argument at least nil in lattice order? *)
000150| (* may_be_nil : VL -> bool *)
000151| let may_be_nil vlat = (*[210593]*)leq nil vlat
000152|
000153| (** Can argument be different from nil in lattice order? *)
000154| (* may_be_non_nil : VL -> bool *)
000155| let may_be_non_nil vlat =
000156| (*[17047]*)vlat.tags <> (TagSet.singleton Nil)
000157| || (*[4680]*)vlat.number <> Num.bot
000158| || (*[3857]*)vlat.strings <> Str.bot
000159| || (*[3225]*)vlat.funs <> mtprocset
000160| || (*[2870]*)vlat.tables <> mtlabelset
000161|
000162| (** Is argument at least bool in lattice order? *)
000163| (* may_be_bool : VL -> bool *)
000164| let may_be_bool vlat = (*[11939]*)leq bool vlat
000165|
000166| (** Is argument at least userdata in lattice order? *)
000167| (* may_be_userdata : VL -> bool *)
000168| let may_be_userdata vlat = (*[11939]*)leq userdata vlat
000169|
000170| (** Is argument at most number in lattice order? *)
000171| (* is_number : VL -> bool *)
000172| let is_number vlat = (*[11928]*)leq vlat number
000173|
000174| (** Is argument at least number in lattice order? *)
000175| (* may_be_number : VL -> bool *)
000176| let may_be_number vlat = (*[488318]*)leq number vlat
000177|
000178| (** Is argument at most String.top in lattice order? *)
000179| (* is_strings : VL -> bool *)
000180| let is_strings vlat = (*[11925]*)leq vlat anystring
000181|
000182| (** Is argument strictly greater than String.bot in lattice order? *)
000183| (* may_be_strings : VL -> bool *)
000184| let may_be_strings vlat = (*[69556]*)vlat.strings <> Str.bot
000185|
000186| (** Is argument strictly greater then bot for some non-string component in lattice order? *)
000187| (* may_be_non_strings : VL -> bool *)
000188| let may_be_non_strings vlat =
000189| (*[71024]*)vlat.number <> Num.bot
000190| || (*[44234]*)vlat.tags <> mttagset
000191| || (*[20843]*)vlat.funs <> mtprocset
000192| || (*[16190]*)vlat.tables <> mtlabelset
000193|
000194| (** Is argument strictly greater than ProcSet.empty in lattice order? *)
000195| (* may_be_proc : VL -> bool *)
000196| let may_be_proc vlat = (*[19939]*)vlat.funs <> mtprocset
000197|
000198| (** Is argument strictly greater than LabelSet.empty in lattice order? *)
000199| (* may_be_table : VL -> bool *)
000200| let may_be_table vlat = (*[32838]*)vlat.tables <> mtlabelset
000201|
000202|
000203| (** {3 Lattice operations } *)
000204|
000205| (* exclude_nil : VL -> VL *)
000206| let exclude_nil lat =
000207| (*[77824552]*)let tags = TagSet.remove Nil lat.tags in
000208| (*[77824552]*){ lat with tags = tags }
000209|
000210| (* exclude_strings : VL -> VL *)
000211| let exclude_strings lat =
000212| (*[5963733]*){ lat with strings = Str.bot }
000213|
000214| (* exclude_proc : VL -> VL *)
000215| let exclude_proc lat =
000216| (*[5000]*){ lat with funs = mtprocset }
000217|
000218| (* exclude_tables : VL -> VL *)
000219| let exclude_tables lat =
000220| (*[46718]*){ lat with tables = mtlabelset }
000221|
000222| (* only_tables : VL -> VL *)
000223| let only_tables lat =
000224| (*[24244]*){ bot with tables = lat.tables }
000225|
000226| (* coerce_tonum : VL -> VL *)
000227| let coerce_tonum lat =
000228| (*[164332]*)if may_be_number lat
000229| then (*[77243]*)number
000230| else match lat.strings with
000231| | Str.Top -> (*[25541]*)number
000233| with (Failure _) -> (*[27604]*)bot)
000234| | Str.Bot -> (*[33944]*)bot
000235|
000236| (* coerce_tostring : VL -> VL *)
000237| let coerce_tostring lat =
000238| (*[72943]*)if may_be_number lat
000239| then (*[30116]*)anystring
000240| else (*[42827]*){ bot with strings = lat.strings }
000241|
000242| (* or_join : VL -> VL -> VL *)
000243| let or_join vlat0 vlat1 =
000244| (*[32259]*)if (*[32259]*)is_bot vlat0 || (*[18724]*)is_bot vlat1 then (*[19212]*)bot else (*FIXED*)
000245| (*[13047]*)join (if may_be_non_nil vlat0 then ((*[10210]*)exclude_nil vlat0) else (*[2837]*)bot)
000246| (if may_be_nil vlat0 then (*[8508]*)vlat1 else (*[4539]*)bot)
000247|
000248| (* upper : VL -> VL *)
000249| let upper lat =
000250| (*[11940]*)let lat' = coerce_tostring lat in
000251| (*[11940]*){ lat' with strings = Str.upper lat'.strings }
000252|
000253| (* lower : VL -> VL *)
000254| let lower lat =
000255| (*[12014]*)let lat' = coerce_tostring lat in
000256| (*[12014]*){ lat' with strings = Str.lower lat'.strings }
000257|
000258| (* char : VL -> VL *)
000259| let char lat =
000260| (*[17285]*)let lat' = coerce_tonum lat in
000261| (*[17285]*)if may_be_number lat' (* char of number (or better) is any string *)
000262| then (*[10542]*)anystring
000263| else (*[6743]*)bot
000264|
000265| (* typep : VL -> VL *)
000266| let typep lat =
000267| (*[11939]*)join (if may_be_nil lat then (*[4953]*)string "nil" else (*[6986]*)bot)
000268| (join (if may_be_bool lat then (*[4804]*)string "boolean" else (*[7135]*)bot)
000269| (join (if may_be_number lat then (*[5000]*)string "number" else (*[6939]*)bot)
000270| (join (if may_be_userdata lat then (*[4837]*)string "userdata" else (*[7102]*)bot)
000271| (join (if may_be_table lat then (*[10273]*)string "table" else (*[1666]*)bot)
000272| (join (if may_be_strings lat then (*[6770]*)string "string" else (*[5169]*)bot)
000273| (if may_be_proc lat then (*[10315]*)string "function" else (*[1624]*)bot))))))
000274|
000275| (* unop : unop -> VL -> VL *)
000276| let unop op lat =
000277| (*[15000]*)if leq lat bot
000278| then (*[3062]*)bot (* unary operation over bot is bot *)
000279| else
000280| match op with
000281| | Ast.Uminus ->
000282| (*[3980]*)let lat' = coerce_tonum lat in
000283| (*[3980]*)if may_be_number lat' (* unary minus of number (or better) is number *)
000284| then (*[2370]*)number
000285| else (*[1610]*)bot
000286| | Ast.Length ->
000287| (*[3977]*)if (*[3977]*)may_be_strings lat || (*[1590]*)may_be_table lat
000288| then (*[3774]*)number
000289| else (*[203]*)bot (* length of everything but strings and tables is number *)
000290| | Ast.Not ->
000291| (*[3981]*)bool (* negation of anything is bool *)
000292|
000293| (* binop : binop -> VL -> VL -> VL *)
000294| let binop op lat0 lat1 =
000295| (*[139275]*)if (*[139275]*)leq lat0 bot || (*[125973]*)leq lat1 bot
000296| then (*[26617]*)bot (* binary operation over a bot is bot *)
000297| else
000298| match op with
000299| | Ast.Eq
000300| | Ast.Ne -> (*[15927]*)bool (* anything can be compared *)
000301| | Ast.Lt
000302| | Ast.Gt
000303| | Ast.Le
000304| | Ast.Ge -> (*[31816]*)if ((*[31816]*)may_be_number lat0 && (*[14838]*)may_be_number lat1)
000305| || ((*[24784]*)Str.nonempty lat0.strings && (*[15596]*)Str.nonempty lat1.strings)
000306| then (*[16708]*)bool
000307| else (*[15108]*)bot
000308| | Ast.Plus
000309| | Ast.Minus
000310| | Ast.Times
000311| | Ast.Div
000312| | Ast.Mod
000313| | Ast.Pow ->
000314| (*[53788]*)if (*[53788]*)may_be_number (coerce_tonum lat0) && (*[33838]*)may_be_number (coerce_tonum lat1)
000315| then (*[21128]*)number
000316| else (*[32660]*)bot
000317| | Ast.Concat ->
000318| (*[11127]*)let lat0' = coerce_tostring lat0 in
000319| (*[11127]*)let lat1' = coerce_tostring lat1 in
000320| (*[11127]*){ bot with strings = Str.concat lat0'.strings lat1'.strings }
000321|
000322|
000323| (** {3 Pretty printing routines } *)
000324|
000325| (* pprint_tags : tagset -> unit *)
000326| let pprint_tags ts =
000327| (* pprint_tag : tag -> unit *)
000328| let pprint_tag t = match t with
000329| | Nil -> Format.printf "Nil"
000330| | Bool -> Format.printf "Bool"
000331| | Userdata -> Format.printf "Userdata" in
000332| begin
000333| Format.printf "{ @[<h 1>";
000334| ignore (TagSet.fold (fun t first ->
000335| if first
000336| then (pprint_tag t; false)
000337| else
000338| begin
000339| Format.printf ",";
000340| Format.print_space ();
000341| pprint_tag t;
000342| false
000343| end) ts true);
000344| Format.printf "@] }";
000345| end
000346|
000347| (* pprint_procs : procset -> unit *)
000348| let pprint_procs ts =
000349| (* builtin_name : builtin -> string *)
000350| let builtin_name b = match b with
000351| | Error -> "error"
000352| | Exit -> "exit"
000353| | Next -> "next"
000354| | INext -> "inext"
000355| | Pairs -> "pairs"
000356| | IPairs -> "ipairs"
000357| | Print -> "print"
000358| | Write -> "write"
000359| | Tonumber -> "tonumber"
000360| | Tostring -> "tostring"
000361| | Abs -> "abs"
000362| | Ceil -> "ceil"
000363| | Floor -> "floor"
000364| | Mod -> "mod"
000365| | Random -> "random"
000366| | Strlen -> "strlen"
000367| | Strupper -> "strupper"
000368| | Strlower -> "strlower"
000369| | Strchar -> "strchar"
000370| | Strbyte -> "strbyte"
000371| | Strsub -> "strsub"
000372| | Sqrt -> "sqrt"
000373| | Type -> "type"
000374| | Format -> "format"
000375| | Tblconcat -> "tblconcat"
000376| | Getmetatable -> "getmetatable"
000377| | Setmetatable -> "setmetatable"
000378| | Rawget -> "rawget"
000379| | Rawset -> "rawset" in
000380|
000381| (* pprint_proc : proc -> unit *)
000382| let pprint_proc p = match p with
000383| | Funtag t -> Format.printf "%i" t
000384| | Builtin b -> Format.printf "[builtin:%s]" (builtin_name b) in
000385|
000386| begin
000387| Format.printf "{ @[<h 1>";
000388| ignore (ProcSet.fold (fun t first ->
000389| if first
000390| then (pprint_proc t; false)
000391| else
000392| begin
000393| Format.printf ",";
000394| Format.print_space ();
000395| pprint_proc t;
000396| false
000397| end) ts true);
000398| Format.printf "@] }";
000399| end
000400|
000401| (* pprint_labels : labelset -> unit *)
000402| let pprint_labels ts =
000403| begin
000404| Format.printf "{ @[<h 1>";
000405| ignore (LabelSet.fold (fun t first ->
000406| if first
000407| then (Format.printf "%i" t; false)
000408| else
000409| begin
000410| Format.printf ",";
000411| Format.print_space ();
000412| Format.printf "%i" t;
000413| false
000414| end) ts true);
000415| Format.printf "@] }";
000416| end
000417|
000418| (* pprint : VL -> unit *)
000419| let pprint v =
000420| let () = Format.printf "{ @[<v 0>" in
000421| let funs =
000422| [(fun first -> if v.tags = mttagset then first else
000423| begin
000424| Format.printf "tags: ";
000425| pprint_tags v.tags;
000426| false
000427| end);
000428| (fun first -> if v.number = Num.bot then first else
000429| begin
000430| (if first then () else Format.print_space ());
000431| Format.printf "number: ";
000432| Num.pprint v.number;
000433| false
000434| end);
000435| (fun first -> if v.strings = Str.bot then first else
000436| begin
000437| (if first then () else Format.print_space ());
000438| Format.printf "strings: ";
000439| Str.pprint v.strings;
000440| false
000441| end);
000442| (fun first -> if v.funs = mtprocset then first else
000443| begin
000444| (if first then () else Format.print_space ());
000445| Format.printf "funs: ";
000446| pprint_procs v.funs;
000447| false
000448| end);
000449| (fun first -> if v.tables = mtlabelset then first else
000450| begin
000451| (if first then () else Format.print_space ());
000452| Format.printf "tables: ";
000453| pprint_labels v.tables;
000454| false
000455| end) ] in
000456| let _ = List.fold_left (fun firstacc f -> f firstacc) true funs in
000457| Format.printf "@] }"
000458|
000459| (* to_string : elem -> string *)
000460| let to_string v =
000461| let buf = Buffer.create 64 in
000462| let out,flush = Format.get_formatter_output_functions () in (* save previous outputters *)
000463| begin
000464| Format.set_formatter_output_functions (Buffer.add_substring buf) (fun () -> ());
000465| pprint v;
000466| Format.print_flush ();
000467| Format.set_formatter_output_functions out flush; (* restore previous outputters *)
000468| Buffer.contents buf
000469| end
000098| let proc p = (*[0]*){ bot with funs = ProcSet.singleton (Funtag p) }