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 = (*[2]*)Pervasives.compare end)
000050| module ProcSet = Set.Make(struct type t = proc
000051| let compare = (*[2]*)Pervasives.compare end)
000052| module LabelSet = Set.Make(struct type t = int
000053| let compare = (*[2]*)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 = (*[2]*)TagSet.empty
000064| let mtprocset = (*[2]*)ProcSet.empty
000065| let mtlabelset = (*[2]*)LabelSet.empty
000066|
000067| (* bot : VL *)
000068| let bot = (*[2]*){ tags = mttagset;
000069| number = Num.bot;
000070| strings = Str.bot;
000071| funs = mtprocset;
000072| tables = mtlabelset; }
000073|
000074| let mktagelem t = (*[6]*){ bot with tags = TagSet.singleton t }
000075|
000076| (* nil : VL *)
000077| let nil = (*[2]*)mktagelem Nil
000078|
000079| (* bool : VL *)
000080| let bool = (*[2]*)mktagelem Bool
000081|
000082| (* number : VL *)
000083| let number = (*[2]*){ bot with number = Num.top }
000084|
000085| (* userdata : VL *)
000086| let userdata = (*[2]*)mktagelem Userdata
000087|
000088| (* string : string -> VL *)
000089| let string s = (*[211515]*){ bot with strings = Str.const s }
000090|
000091| (* anystring : VL *)
000092| let anystring = (*[2]*){ bot with strings = Str.top }
000093|
000094| (* table : label -> VL *)
000095| let table t = (*[3990]*){ bot with tables = LabelSet.singleton t }
000096|
000097| (* proc : label -> VL *)
000098| let proc p = (*[394]*){ bot with funs = ProcSet.singleton (Funtag p) }
000099|
000100| (* builtin : builtin -> VL *)
000101| let builtin b = (*[13538]*){ bot with funs = ProcSet.singleton (Builtin b) }
000102|
000103| (* eq : VL -> VL -> bool *)
000104| let eq v1 v2 =
000105| (*[707615]*)TagSet.equal v1.tags v2.tags
000106| && (*[707615]*)Num.eq v1.number v2.number
000107| && (*[707615]*)Str.eq v1.strings v2.strings
000108| && (*[707615]*)ProcSet.equal v1.funs v2.funs
000109| && (*[707615]*)LabelSet.equal v1.tables v2.tables
000110|
000111| (* leq : VL -> VL -> bool *)
000112| let leq v1 v2 =
000113| (*[63449521]*)TagSet.subset v1.tags v2.tags
000114| && (*[60003105]*)Num.leq v1.number v2.number
000115| && (*[59068225]*)Str.leq v1.strings v2.strings
000116| && (*[58364801]*)ProcSet.subset v1.funs v2.funs
000117| && (*[57748281]*)LabelSet.subset v1.tables v2.tables
000118|
000119| (* join : VL -> VL -> VL *)
000120| let join v1 v2 =
000121| (*[31959948]*){ 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| (*[3825084]*){ 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 = (*[2]*)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 = (*[5333080]*)leq vlat bot
000144|
000145| (** Is argument at most nil in lattice order? *)
000146| (* is_nil : VL -> bool *)
000147| let is_nil vlat = (*[20794]*)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 = (*[214850]*)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| (*[17132]*)vlat.tags <> (TagSet.singleton Nil)
000157| || (*[4694]*)vlat.number <> Num.bot
000158| || (*[3871]*)vlat.strings <> Str.bot
000159| || (*[3239]*)vlat.funs <> mtprocset
000160| || (*[2884]*)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 = (*[11969]*)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 = (*[11955]*)leq userdata vlat
000169|
000170| (** Is argument at most number in lattice order? *)
000171| (* is_number : VL -> bool *)
000172| let is_number vlat = (*[11962]*)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 = (*[490603]*)leq number vlat
000177|
000178| (** Is argument at most String.top in lattice order? *)
000179| (* is_strings : VL -> bool *)
000180| let is_strings vlat = (*[11931]*)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 = (*[69661]*)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| (*[72443]*)vlat.number <> Num.bot
000190| || (*[45351]*)vlat.tags <> mttagset
000191| || (*[21870]*)vlat.funs <> mtprocset
000192| || (*[17201]*)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 = (*[22532]*)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 = (*[33951]*)vlat.tables <> mtlabelset
000201|
000202|
000203| (** {3 Lattice operations } *)
000204|
000205| (* exclude_nil : VL -> VL *)
000206| let exclude_nil lat =
000207| (*[77828956]*)let tags = TagSet.remove Nil lat.tags in
000208| (*[77828956]*){ lat with tags = tags }
000209|
000210| (* exclude_strings : VL -> VL *)
000211| let exclude_strings lat =
000212| (*[5963904]*){ lat with strings = Str.bot }
000213|
000214| (* exclude_proc : VL -> VL *)
000215| let exclude_proc lat =
000216| (*[5975]*){ lat with funs = mtprocset }
000217|
000218| (* exclude_tables : VL -> VL *)
000219| let exclude_tables lat =
000220| (*[46726]*){ lat with tables = mtlabelset }
000221|
000222| (* only_tables : VL -> VL *)
000223| let only_tables lat =
000224| (*[24607]*){ bot with tables = lat.tables }
000225|
000226| (* coerce_tonum : VL -> VL *)
000227| let coerce_tonum lat =
000228| (*[165368]*)if may_be_number lat
000229| then (*[78035]*)number
000230| else match lat.strings with
000231| | Str.Top -> (*[25553]*)number
000232| | Str.Const s -> ((*[27640]*)try (*[27640]*)let _ = float_of_string (String.trim s) in (*[36]*)number
000233| with (Failure _) -> (*[27604]*)bot)
000234| | Str.Bot -> (*[34140]*)bot
000235|
000236| (* coerce_tostring : VL -> VL *)
000237| let coerce_tostring lat =
000238| (*[73110]*)if may_be_number lat
000239| then (*[30140]*)anystring
000240| else (*[42970]*){ bot with strings = lat.strings }
000241|
000242| (* or_join : VL -> VL -> VL *)
000243| let or_join vlat0 vlat1 =
000244| (*[32487]*)if (*[32487]*)is_bot vlat0 || (*[18755]*)is_bot vlat1 then (*[19409]*)bot else (*FIXED*)
000245| (*[13078]*)join (if may_be_non_nil vlat0 then ((*[10231]*)exclude_nil vlat0) else (*[2847]*)bot)
000246| (if may_be_nil vlat0 then (*[8518]*)vlat1 else (*[4560]*)bot)
000247|
000248| (* upper : VL -> VL *)
000249| let upper lat =
000250| (*[11942]*)let lat' = coerce_tostring lat in
000251| (*[11942]*){ lat' with strings = Str.upper lat'.strings }
000252|
000253| (* lower : VL -> VL *)
000254| let lower lat =
000255| (*[12016]*)let lat' = coerce_tostring lat in
000256| (*[12016]*){ lat' with strings = Str.lower lat'.strings }
000257|
000258| (* char : VL -> VL *)
000259| let char lat =
000260| (*[17291]*)let lat' = coerce_tonum lat in
000261| (*[17291]*)if may_be_number lat' (* char of number (or better) is any string *)
000262| then (*[10548]*)anystring
000263| else (*[6743]*)bot
000264|
000265| (* typep : VL -> VL *)
000266| let typep lat =
000267| (*[11955]*)join (if may_be_nil lat then (*[4957]*)string "nil" else (*[6998]*)bot)
000268| (join (if may_be_bool lat then (*[4806]*)string "boolean" else (*[7149]*)bot)
000269| (join (if may_be_number lat then (*[5006]*)string "number" else (*[6949]*)bot)
000270| (join (if may_be_userdata lat then (*[4837]*)string "userdata" else (*[7118]*)bot)
000271| (join (if may_be_table lat then (*[10275]*)string "table" else (*[1680]*)bot)
000272| (join (if may_be_strings lat then (*[6772]*)string "string" else (*[5183]*)bot)
000273| (if may_be_proc lat then (*[10319]*)string "function" else (*[1636]*)bot))))))
000274|
000275| (* unop : unop -> VL -> VL *)
000276| let unop op lat =
000277| (*[15019]*)if leq lat bot
000278| then (*[3063]*)bot (* unary operation over bot is bot *)
000279| else
000280| match op with
000281| | Ast.Uminus ->
000282| (*[3982]*)let lat' = coerce_tonum lat in
000283| (*[3982]*)if may_be_number lat' (* unary minus of number (or better) is number *)
000284| then (*[2372]*)number
000285| else (*[1610]*)bot
000286| | Ast.Length ->
000287| (*[3981]*)if (*[3981]*)may_be_strings lat || (*[1592]*)may_be_table lat
000288| then (*[3778]*)number
000289| else (*[203]*)bot (* length of everything but strings and tables is number *)
000290| | Ast.Not ->
000291| (*[3993]*)bool (* negation of anything is bool *)
000292|
000293| (* binop : binop -> VL -> VL -> VL *)
000294| let binop op lat0 lat1 =
000295| (*[139790]*)if (*[139790]*)leq lat0 bot || (*[126440]*)leq lat1 bot
000296| then (*[26667]*)bot (* binary operation over a bot is bot *)
000297| else
000298| match op with
000299| | Ast.Eq
000300| | Ast.Ne -> (*[16009]*)bool (* anything can be compared *)
000301| | Ast.Lt
000302| | Ast.Gt
000303| | Ast.Le
000304| | Ast.Ge -> (*[31947]*)if ((*[31947]*)may_be_number lat0 && (*[14967]*)may_be_number lat1)
000305| || ((*[24788]*)Str.nonempty lat0.strings && (*[15598]*)Str.nonempty lat1.strings)
000306| then (*[16835]*)bool
000307| else (*[15112]*)bot
000308| | Ast.Plus
000309| | Ast.Minus
000310| | Ast.Times
000311| | Ast.Div
000312| | Ast.Mod
000313| | Ast.Pow ->
000314| (*[53985]*)if (*[53985]*)may_be_number (coerce_tonum lat0) && (*[34035]*)may_be_number (coerce_tonum lat1)
000315| then (*[21325]*)number
000316| else (*[32660]*)bot
000317| | Ast.Concat ->
000318| (*[11182]*)let lat0' = coerce_tostring lat0 in
000319| (*[11182]*)let lat1' = coerce_tostring lat1 in
000320| (*[11182]*){ 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