000001| (** Abstract state datatype and operations *)
000002|
000003| module Abs = Absencelattice
000004| module VL = Valuelattice
000005| module EL = Envlattice
000006| module PL = Proplattice
000007| module ST = Storelattice
000008|
000009| type elem = { store : ST.elem;
000010| env : EL.elem; }
000011|
000012| (* leq : elem -> elem -> bool *)
000013| let leq st0 st1 =
000014| (*[643533]*)ST.leq st0.store st1.store && (*[260632]*)EL.leq st0.env st1.env
000015|
000016| (* eq : elem -> elem -> bool *)
000017| let eq st0 st1 =
000018| (*[389312]*)ST.eq st0.store st1.store && (*[389312]*)EL.eq st0.env st1.env
000019|
000020| (* join : elem -> elem -> bool *)
000021| let join st0 st1 =
000022| (*[103460]*){ store = ST.join st0.store st1.store;
000023| env = EL.join st0.env st1.env; }
000024|
000025| (* meet : elem -> elem -> bool *)
000026| let meet st0 st1 =
000027| (*[67332]*){ store = ST.meet st0.store st1.store;
000028| env = EL.meet st0.env st1.env; }
000029|
000030| (* bot : elem *)
000031| let bot = (*[1]*){ store = ST.bot;
000032| env = EL.bot; }
000033|
000034|
000035| (** {3 Lattice operations } *)
000036|
000037| (* is_bot : SL -> bool *)
000038| let is_bot slat = (*[447303]*)leq slat bot
000039|
000040| (* build_record : (string * VL) list -> PL *)
000041| let build_record bs =
000042| (*[6]*)let props, vls = List.split bs in
000043| (*[6]*)PL.add_all_params props vls PL.mt
000044|
000045| (* init : elem *)
000046| let init =
000047| (*[1]*)let localenvlab = Label.make_res_label() in
000048| (*[1]*)let globallabel = Label.make_res_label() in
000049| (*[1]*)let arglabel = Label.make_res_label() in
000050| (*[1]*)let iolabel = Label.make_res_label() in
000051| (*[1]*)let mathlabel = Label.make_res_label() in
000052| (*[1]*)let oslabel = Label.make_res_label() in
000053| (*[1]*)let stringlabel = Label.make_res_label() in
000054| (*[1]*)let tablelabel = Label.make_res_label() in
000055| (*[1]*)let store = List.fold_left
000056| (fun store (lab,table) -> (*[8]*)ST.add_label store lab table) ST.bot
000057| [ (localenvlab, PL.mt);
000058| (globallabel, build_record
000059| [ ("error", VL.builtin VL.Error);
000060| ("next", VL.builtin VL.Next);
000061| ("pairs", VL.builtin VL.Pairs);
000062| ("ipairs", VL.builtin VL.IPairs);
000063| ("print", VL.builtin VL.Print);
000064| ("tonumber", VL.builtin VL.Tonumber);
000065| ("tostring", VL.builtin VL.Tostring);
000066| (* ("abs", VL.builtin VL.Abs); *) (* from Lua 2.5 *)
000067| (* ("write", VL.builtin VL.Write); *) (* from Lua 2.5 *)
000068| (* ("floor", VL.builtin VL.Floor); *) (* from Lua 2.5 *)
000069| (* ("mod", VL.builtin VL.Mod); *) (* from Lua 2.5 *)
000070| (* ("strlen", VL.builtin VL.Strlen);*) (* from Lua 2.5 *)
000071| (* ("sqrt", VL.builtin VL.Sqrt); *) (* from Lua 2.5 *)
000072| (* ("format", VL.builtin VL.Format);*) (* from Lua 2.5 *)
000073| ("_VERSION", VL.anystring);
000074| ("_G", VL.table globallabel);
000075| ("arg", VL.table arglabel);
000076| ("io", VL.table iolabel);
000077| ("math", VL.table mathlabel);
000078| ("os", VL.table oslabel);
000079| ("string", VL.table stringlabel);
000080| ("table", VL.table tablelabel);
000081| ("type", VL.builtin VL.Type);
000082| ("setmetatable", VL.builtin VL.Setmetatable);
000083| ("getmetatable", VL.builtin VL.Getmetatable);
000084| ("rawget", VL.builtin VL.Rawget);
000085| ("rawset", VL.builtin VL.Rawset);
000086| ]);
000087| (arglabel, PL.add_nonstr_default VL.number VL.anystring PL.mt);
000088| (iolabel, build_record
000089| [ ("write", VL.builtin VL.Write); ]);
000090| (mathlabel, build_record
000091| [ ("abs", VL.builtin VL.Abs);
000092| ("ceil", VL.builtin VL.Ceil);
000093| ("floor", VL.builtin VL.Floor);
000094| ("huge", VL.number);
000095| ("random", VL.builtin VL.Random);
000096| ("sqrt", VL.builtin VL.Sqrt);
000097| ]);
000098| (oslabel, build_record
000099| [ ("exit", VL.builtin VL.Exit); ]);
000100| (stringlabel, build_record
000101| [ ("len", VL.builtin VL.Strlen);
000102| ("upper", VL.builtin VL.Strupper);
000103| ("lower", VL.builtin VL.Strlower);
000104| ("char", VL.builtin VL.Strchar);
000105| ("byte", VL.builtin VL.Strbyte);
000106| ("sub", VL.builtin VL.Strsub);
000107| ("format", VL.builtin VL.Format);
000108| ]);
000109| (tablelabel, build_record
000110| [ ("concat", VL.builtin VL.Tblconcat);
000111| ]);
000112| ] in
000113| (*[1]*)let env = EL.init localenvlab globallabel in
000114| (*[1]*){ store = store;
000115| env = env; }
000116|
000117|
000118| (* apply_builtin : builtin -> SL -> VL list -> SL * VL list *)
000119| let rec apply_builtin bi slat vlats =
000120| (*[297722]*)if is_bot slat then ((*[30425]*)bot,[]) else
000121| match bi with
000122| | VL.Error -> ((*[8946]*)bot,[]) (* unreachable *)
000123| | VL.Exit -> ((*[8953]*)bot,[]) (* unreachable *)
000124| | VL.Next ->
000125| (match vlats with
000126| | [] -> ((*[1974]*)bot,[]) (*error*)
000127| | vlat::_ ->
000128| (*[6975]*)if VL.may_be_table vlat then
000129| (*[6729]*)let keys = VL.join VL.nil (* potentially: end of table *)
000130| (ST.lookup_all_keys slat.store vlat) in
000131| (*[6729]*)let values = VL.join VL.nil (* potentially: end of table *)
000132| (ST.lookup_all_props slat.store vlat) in
000133| (* possible strengthening: if 2nd arg is nil and table is definitely non-empty (has definite entries), *)
000134| ((*[6729]*)slat,[keys;values]) (* then result cannot be nil *)
000135| else ((*[246]*)bot,[])) (*error*)
000136| | VL.INext ->
000137| (match vlats with
000138| | [] -> ((*[1955]*)bot,[]) (*error*)
000139| | vlat::_ ->
000140| (*[6998]*)if VL.may_be_table vlat
000141| then
000142| (*[6781]*)let keys = ST.lookup_all_keys slat.store vlat in
000143| ((*[6781]*)if VL.may_be_number keys
000144| then
000145| (*[1477]*)let keys = VL.join VL.nil VL.number in (* potentially: end of table *)
000146| (*[1477]*)let values = VL.join VL.nil (* potentially: end of table *)
000147| (ST.lookup_all_nonstr_props slat.store vlat) in (* array entries are nonstr *)
000148| ((*[1477]*)slat,[keys;values])
000149| else
000150| (*[5304]*)let keys,values = VL.nil,VL.nil in (* end of table *)
000151| ((*[5304]*)slat,[keys;values]))
000152| else ((*[217]*)bot,[])) (*error*)
000153| | VL.Pairs ->
000154| (match vlats with
000155| | [] -> ((*[1968]*)bot,[]) (*error*)
000156| | vlat::_ ->
000157| (*[6977]*)let vlat' = VL.only_tables vlat in
000158| (*[6977]*)if VL.is_bot vlat'
000159| then ((*[220]*)bot,[]) (*error*)
000160| else ((*[6757]*)slat,[VL.builtin VL.Next; vlat'; VL.nil]))
000161| | VL.IPairs ->
000162| (match vlats with
000163| | [] -> ((*[2005]*)bot,[]) (*error*)
000164| | vlat::_ ->
000165| (*[6940]*)let vlat' = VL.only_tables vlat in
000166| (*[6940]*)if VL.is_bot vlat'
000167| then ((*[235]*)bot,[]) (*error*)
000168| else ((*[6705]*)slat,[VL.builtin VL.INext; vlat'; VL.number])) (* return iterator, table, 0 *)
000169| | VL.Print -> ((*[7961]*)slat,[VL.nil]) (* no return value specified - Lua2.5 impl returns nil *)
000170| | VL.Write ->
000171| (match vlats with
000172| | [] -> ((*[2949]*)slat, [VL.userdata])
000173| | vlat::vlats ->
000174| (*[17985]*)if (*[17985]*)VL.may_be_number vlat || (*[9044]*)VL.may_be_strings vlat (* may succeed *)
000175| then (*[14971]*)apply_builtin bi slat vlats
000176| else ((*[3014]*)bot, []))
000177| | VL.Tonumber ->
000178| (match vlats with
000179| | [] -> ((*[1999]*)bot,[]) (*error*)
000180| | vlat::_ ->
000181| (*[6946]*)if VL.is_nil vlat then ((*[18]*)bot,[]) (* unreachable *)
000182| else
000183| (*[6928]*)let retval =
000184| if VL.is_number vlat then (*[3]*)VL.number (* number arg (at most) *)
000185| else (*[6925]*)if VL.is_strings vlat then (*[8]*)VL.number_or_nil (* string arg (at most) *)
000186| else (*[6917]*)if VL.may_be_number vlat then (*[3232]*)VL.number_or_nil (* number or other arg *)
000187| else (*[3685]*)if VL.may_be_strings vlat then (*[2297]*)VL.number_or_nil (* string or other arg *)
000188| else (*[1388]*)VL.nil (* no string or number arguments *)
000189| in ((*[6928]*)slat,[retval]))
000190| | VL.Tostring ->
000191| (match vlats with
000192| | [] -> ((*[2013]*)bot,[]) (*error*)
000193| | vlat::_ ->
000194| (*[6940]*)if VL.is_bot vlat then ((*[17]*)bot,[]) (* unreachable *)
000195| else ((*[6923]*)slat,[VL.anystring]))
000196| | VL.Abs
000197| | VL.Ceil
000198| | VL.Floor ->
000199| (match vlats with
000200| | vlat::_ ->
000201| (*[21028]*)if VL.is_bot vlat then ((*[42]*)bot, []) (* unreachable *)
000202| else (*[20986]*)if VL.may_be_number (VL.coerce_tonum vlat) then ((*[13059]*)slat, [VL.number])
000203| else ((*[7927]*)bot, [])
000204| | _ -> ((*[5844]*)bot, []))
000205| | VL.Mod ->
000206| (match vlats with
000207| | vl0::vl1::_ -> (*[6103]*)let res = VL.binop Ast.Mod vl0 vl1 in
000208| (*[6103]*)if res = VL.bot then ((*[3546]*)bot, [VL.bot])
000209| else ((*[2557]*)slat, [res])
000210| | _ -> ((*[2854]*)bot, []))
000211| | VL.Random ->
000212| (match vlats with
000213| | [] -> ((*[588]*)slat,[VL.number])
000214| | vl0::[] -> (*[587]*)if VL.may_be_number (VL.coerce_tonum vl0)
000215| then ((*[408]*)slat,[VL.number])
000216| else ((*[179]*)bot, [])
000217| | vl0::vl1::[] -> (*[587]*)if (*[587]*)VL.may_be_number (VL.coerce_tonum vl0)
000218| && (*[399]*)VL.may_be_number (VL.coerce_tonum vl1)
000219| then ((*[274]*)slat,[VL.number])
000220| else ((*[313]*)bot, [])
000221| | _ -> ((*[4203]*)bot, []))
000222| | VL.Strlen ->
000223| (match vlats with
000224| | [] -> ((*[1959]*)bot,[]) (*error*)
000225| | vlat::_ ->
000226| (*[6985]*)if VL.may_be_strings (VL.coerce_tostring vlat)
000227| then ((*[5563]*)slat,[VL.number])
000228| else ((*[1422]*)bot,[]))
000229| | VL.Strupper ->
000230| (match vlats with
000231| | [] -> ((*[2017]*)bot,[]) (*error*)
000232| | vlat::_ -> ((*[6940]*)slat,[VL.upper vlat]))
000233| | VL.Strlower ->
000234| (match vlats with
000235| | [] -> ((*[1930]*)bot,[]) (*error*)
000236| | vlat::_ -> ((*[7014]*)slat,[VL.lower vlat]))
000237| | VL.Strchar ->
000238| (match vlats with
000239| | [] -> ((*[1814]*)slat, [VL.string ""])
000240| | vlat::vlats ->
000241| (*[12285]*)let vlat' = VL.char vlat in
000242| (*[12285]*)if VL.may_be_strings vlat' (* may succeed *)
000243| then
000244| (*[8160]*)let slat',vlats' = apply_builtin bi slat vlats in (* recurse *)
000245| (match vlats' with
000246| | [] -> ((*[4988]*)bot, []) (* propagate error *)
000247| | vlat''::_ -> ((*[3172]*)slat',[VL.binop Ast.Concat vlat' vlat'']))
000248| else ((*[4125]*)bot, []))
000249| | VL.Strbyte ->
000250| (match vlats with
000251| | [] -> ((*[1624]*)bot, [])
000252| | arg::[] -> (*[557]*)if VL.may_be_strings (VL.coerce_tostring arg)
000253| then ((*[463]*)slat,[VL.number_or_nil])
000254| else ((*[94]*)bot, [])
000255| | arg1::arg2::[] -> (*[598]*)if (*[598]*)VL.may_be_strings (VL.coerce_tostring arg1)
000256| && (*[498]*)VL.may_be_number (VL.coerce_tonum arg2)
000257| then ((*[345]*)slat,[VL.number_or_nil])
000258| else ((*[253]*)bot, [])
000259| | arg1::arg2::arg3::_ -> (*[4170]*)if (*[4170]*)VL.may_be_strings (VL.coerce_tostring arg1)
000260| && (*[3474]*)VL.may_be_number (VL.coerce_tonum arg2)
000261| && (*[2268]*)VL.may_be_number (VL.coerce_tonum arg3)
000262| then (* almost conservative :-) for static strings, length gives a bound *)
000263| ((*[1465]*)slat,[VL.number_or_nil;VL.number_or_nil;VL.number_or_nil;VL.number_or_nil;VL.number_or_nil;
000264| VL.number_or_nil;VL.number_or_nil;VL.number_or_nil;VL.number_or_nil;VL.number_or_nil ])
000265| else ((*[2705]*)bot, []))
000266| | VL.Strsub ->
000267| (match vlats with
000268| | [] | [ _ ] -> ((*[2252]*)bot, [])
000269| | arg1::arg2::[] -> (*[591]*)apply_builtin bi slat ([arg1;VL.number;arg2])
000270| | arg1::arg2::arg3::_ ->
000271| (*[4695]*)let arg1' = VL.coerce_tostring arg1 in
000272| (*[4695]*)let arg2' = VL.coerce_tonum arg2 in
000273| (*[4695]*)let arg3' = VL.coerce_tonum arg3 in
000274| (*[4695]*)if (*[4695]*)VL.may_be_strings arg1' && (*[3955]*)VL.may_be_number arg2' && (*[2870]*)VL.may_be_number arg3'
000275| then ((*[1907]*)slat,[VL.anystring])
000276| else ((*[2788]*)bot,[]))
000277| | VL.Sqrt ->
000278| (match vlats with
000279| | [] -> ((*[2018]*)bot,[]) (*error*)
000280| | vlat::_ ->
000281| (*[6935]*)if VL.may_be_number (VL.coerce_tonum vlat)
000282| then ((*[4425]*)slat,[VL.number])
000283| else ((*[2510]*)bot,[]))
000284| | VL.Type ->
000285| (match vlats with
000286| | [] -> ((*[2014]*)bot,[]) (*error*)
000287| | vlat::_ -> ((*[6939]*)slat,[VL.typep vlat]))
000288| | VL.Format ->
000289| (match vlats with
000290| | [] -> ((*[2046]*)bot,[]) (*error*)
000291| | vlat::_ ->
000292| (*[6903]*)if VL.is_nil vlat then ((*[12]*)bot,[]) (*unreachable*)
000293| else (*[6891]*)if VL.may_be_strings vlat then ((*[4365]*)slat,[VL.anystring])
000294| else ((*[2526]*)bot,[]))
000295| | VL.Tblconcat ->
000296| (match vlats with
000297| | [] -> ((*[1609]*)bot,[]) (*error*)
000298| | vlat1::vlats1 ->
000299| (*[5336]*)if VL.may_be_table vlat1
000300| then (match vlats1 with
000301| | [] -> ((*[606]*)slat,[VL.anystring]) (* one arg *)
000302| | vlat2::vlats2 ->
000303| (*[4730]*)if VL.may_be_strings (VL.coerce_tostring vlat2)
000304| then (match vlats2 with
000305| | [] -> ((*[503]*)slat,[VL.anystring]) (* two args *)
000306| | vlat3::vlats3 ->
000307| (*[3458]*)if VL.may_be_number (VL.coerce_tonum vlat3)
000308| then (match vlats3 with
000309| | [] -> ((*[349]*)slat,[VL.anystring]) (* three args *)
000310| | vlat4::_ ->
000311| (*[1859]*)if VL.may_be_number (VL.coerce_tonum vlat4)
000312| then ((*[1221]*)slat,[VL.anystring]) (* four args *)
000313| else ((*[638]*)bot,[]))
000314| else ((*[1250]*)bot,[]))
000315| else ((*[769]*)bot,[]))
000317| | VL.Getmetatable ->
000318| (match vlats with
000319| | [] -> ((*[1960]*)bot,[]) (*error*)
000320| | vlat::_ -> ((*[6993]*)slat,[ST.get_metatable slat.store vlat]))
000321| | VL.Setmetatable ->
000322| (match vlats with
000323| | [] -> ((*[2029]*)bot,[]) (*error*)
000324| | [_] -> ((*[905]*)bot,[]) (*error*)
000325| | vlat::vlat'::_ ->
000326| (*[6018]*)let store' = ST.set_metatable slat.store vlat vlat' in
000327| ((*[6018]*){slat with store = store'},[vlat]))
000328| | VL.Rawget ->
000329| (match vlats with
000330| | [] -> ((*[1992]*)bot,[]) (*error*)
000331| | [_] -> ((*[885]*)bot,[]) (*error*)
000332| | vlat::vlat'::_ -> ((*[6068]*)slat,[ST.raw_get slat.store vlat vlat']))
000333| | VL.Rawset ->
000334| (match vlats with
000335| | [] -> ((*[1988]*)bot,[]) (*error*)
000336| | _::[] -> ((*[825]*)bot,[]) (*error*)
000337| | _::_::[] -> ((*[798]*)bot,[]) (*error*)
000338| | vlat0::vlat1::vlat2::_ ->
000339| (*[5327]*)let store' = ST.raw_set slat.store vlat0 vlat1 vlat2 in
000340| ((*[5327]*){slat with store = store'},[VL.only_tables vlat0]))
000341|
000342|
000343| (* add_local : SL -> VL -> str -> SL *)
000344| let add_local slat vlat x =
000345| (*[64887]*)if (*[64887]*)is_bot slat || (*[63836]*)VL.is_bot vlat
000346| then (*[2072]*)bot
000347| else
000348| (*[62815]*)let store' =
000349| EL.fold (fun (localslab,_) storeacc ->
000350| (*[300425]*)let env = ST.find_label slat.store localslab in
000351| (*[300425]*)let env' = PL.add_local x vlat env in (* strong update *)
000352| (*[300425]*)ST.join (ST.add_label slat.store localslab env') storeacc)
000353| slat.env ST.bot in
000354| (*[62815]*){ slat with store = store' }
000355|
000356| (* add_local_list : SL -> VL list -> str list -> SL *)
000357| let rec add_local_list slat vlats xs =
000358| (*[66694]*)if is_bot slat
000359| then (*[1198]*)bot
000360| else match (xs,vlats) with
000361| | [], [] -> (*[5802]*)slat
000362| | x::xs,vlat::vlats ->
000363| (*[21338]*)let slat' = add_local slat vlat x in
000364| (*[21338]*)add_local_list slat' vlats xs
000365| | x::xs,[] ->
000366| (*[33549]*)let slat' = add_local slat VL.nil x in (* missing value: assign nil *)
000367| (*[33549]*)add_local_list slat' [] xs
000368| | [], vlat::vlats ->
000369| (*[4807]*)add_local_list slat vlats [] (* missing local: drop excess value *)
000370|
000371| (* enter_scope : SL -> label -> SL *)
000372| let enter_scope slat label =
000373| (*[5000]*)if is_bot slat
000374| then (*[1041]*)bot
000375| else
000376| (*[3959]*){ store = ST.add_label slat.store label PL.mt;
000377| env = EL.enter_scope slat.env label }
000378|
000379| (* build_prop_chain : EL -> PL *)
000380| let build_prop_chain scopechain =
000381| (*[5000]*)if EL.is_bot scopechain
000382| then (*[1217]*)PL.bot
000383| else
000384| (*[3783]*)EL.fold (fun (i,is) scset -> (*[17349]*)PL.add_scopechain scset (i::is)) scopechain PL.mt
000385|
000386| (* read_name : SL -> string -> VL *)
000387| let read_name slat name =
000388| (* scope_read : lab -> lab list -> VL *)
000389| (*[5000]*)let rec scope_read envlab scopechain =
000390| (*[21802]*)if ST.is_bot slat.store
000391| then (*[1364]*)VL.bot
000392| else
000393| (*[20438]*)let env = ST.find_label slat.store envlab in
000394| (*[20438]*)if PL.is_bot env
000395| then (*[15101]*)VL.bot
000396| else
000397| (*[5337]*)try
000398| (*[5337]*)let vl,abs = PL.find_exn name env in (* slight hack: direct lookup *)
000399| (*[1373]*)if Abs.eq abs Abs.maybe_absent
000400| then (*[670]*)VL.join vl (continue_read scopechain)
000401| else (*[703]*)vl (* certain entry, don't continue *)
000402| with Not_found -> (*[3964]*)continue_read scopechain
000403| (* continue_read : lab list -> VL *)
000404| and continue_read scopechain = match scopechain with
000405| | [] -> (*[151]*)VL.nil (* not found: return nil *)
000406| | outerenvlab::scopechain' -> (*[4483]*)scope_read outerenvlab scopechain'
000407| in
000408| (*[5000]*)EL.fold (fun (envlab,chain) a -> (*[17319]*)VL.join (scope_read envlab chain) a) slat.env VL.bot
000409|
000410| (* write_name : SL -> string -> VL -> SL *)
000411| let write_name slat name vlat =
000412| (*[8000]*)if (*[8000]*)is_bot slat || (*[7950]*)VL.is_bot vlat
000413| then (*[80]*)bot
000414| else
000415| (* scope_write : lab -> lab list -> SL *)
000416| (*[7920]*)let rec scope_write envlab scopechain =
000417| (*[45261]*)try
000418| (*[45261]*)let env = ST.find_label_exn slat.store envlab in
000419| (*[12240]*)if PL.is_bot env
000420| then (*[981]*)bot
000421| else
000422| (*[11259]*)if PL.mem name env (* slight hack: direct lookup *)
000423| then
000424| (*[3089]*)let _,abs = PL.find_exn name env in (* slight hack: direct lookup *)
000425| (*[3089]*)let env' = PL.add_local name vlat env in (* strong update the local variable *)
000426| (*[3089]*)let store' = ST.add_label slat.store envlab env' in
000427| (*[3089]*)let slat' = { slat with store = store' } in
000428| ((*[3089]*)if Abs.eq abs Abs.maybe_absent
000429| then (*[1672]*)join slat' (continue_write scopechain)
000430| else (*[1417]*)slat')
000431| else (*[8170]*)continue_write scopechain
000432| with Not_found -> (*[33021]*)bot
000433| (* continue_write : list -> SL *)
000434| and continue_write scopechain = match scopechain with
000316| else ((*[0]*)bot,[])) (*unreachable*)