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 = (*[2882]*){ 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 = (*[354]*){ 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 = (*[49]*){ bot with funs = ProcSet.singleton (Builtin b) }
000102|
000103| (* eq : VL -> VL -> bool *)
000104| let eq v1 v2 =
000105| (*[2]*)TagSet.equal v1.tags v2.tags
000106| && (*[2]*)Num.eq v1.number v2.number
000107| && (*[2]*)Str.eq v1.strings v2.strings
000108| && (*[2]*)ProcSet.equal v1.funs v2.funs
000109| && (*[2]*)LabelSet.equal v1.tables v2.tables
000110|
000111| (* leq : VL -> VL -> bool *)
000112| let leq v1 v2 =
000113| (*[441519]*)TagSet.subset v1.tags v2.tags
000114| && (*[432192]*)Num.leq v1.number v2.number
000115| && (*[425510]*)Str.leq v1.strings v2.strings
000116| && (*[421707]*)ProcSet.subset v1.funs v2.funs
000117| && (*[419517]*)LabelSet.subset v1.tables v2.tables
000118|
000119| (* join : VL -> VL -> VL *)
000120| let join v1 v2 =
000121| (*[6550830]*){ 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| (*[475]*){ 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 = (*[22203]*)leq vlat bot
000144|
000145| (** Is argument at most nil in lattice order? *)
000146| (* is_nil : VL -> bool *)
000147| let is_nil vlat = (*[42]*)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 = (*[4257]*)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| (*[85]*)vlat.tags <> (TagSet.singleton Nil)
000157| || (*[14]*)vlat.number <> Num.bot
000158| || (*[14]*)vlat.strings <> Str.bot
000159| || (*[14]*)vlat.funs <> mtprocset
000160| || (*[14]*)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 = (*[30]*)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 = (*[16]*)leq userdata vlat
000169|
000170| (** Is argument at most number in lattice order? *)
000171| (* is_number : VL -> bool *)
000172| let is_number vlat = (*[34]*)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 = (*[2285]*)leq number vlat
000177|
000178| (** Is argument at most String.top in lattice order? *)
000179| (* is_strings : VL -> bool *)
000180| let is_strings vlat = (*[6]*)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 = (*[105]*)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| (*[1419]*)vlat.number <> Num.bot
000190| || (*[1117]*)vlat.tags <> mttagset
000191| || (*[1027]*)vlat.funs <> mtprocset
000192| || (*[1011]*)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 = (*[2593]*)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 = (*[1113]*)vlat.tables <> mtlabelset
000201|
000202|
000203| (** {3 Lattice operations } *)
000204|
000205| (* exclude_nil : VL -> VL *)
000206| let exclude_nil lat =
000207| (*[4404]*)let tags = TagSet.remove Nil lat.tags in
000208| (*[4404]*){ lat with tags = tags }
000209|
000210| (* exclude_strings : VL -> VL *)
000211| let exclude_strings lat =
000212| (*[171]*){ lat with strings = Str.bot }
000213|
000214| (* exclude_proc : VL -> VL *)
000215| let exclude_proc lat =
000216| (*[975]*){ lat with funs = mtprocset }
000217|
000218| (* exclude_tables : VL -> VL *)
000219| let exclude_tables lat =
000220| (*[8]*){ lat with tables = mtlabelset }
000221|
000222| (* only_tables : VL -> VL *)
000223| let only_tables lat =
000224| (*[363]*){ bot with tables = lat.tables }
000225|
000226| (* coerce_tonum : VL -> VL *)
000227| let coerce_tonum lat =
000228| (*[1036]*)if may_be_number lat
000229| then (*[792]*)number
000230| else match lat.strings with
000231| | Str.Top -> (*[12]*)number
000232| | Str.Const s -> ((*[36]*)try (*[36]*)let _ = float_of_string (String.trim s) in (*[36]*)number
000317| | Ast.Concat ->
000318| (*[55]*)let lat0' = coerce_tostring lat0 in
000319| (*[55]*)let lat1' = coerce_tostring lat1 in
000320| (*[55]*){ 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
000233| with (Failure _) -> (*[0]*)bot)