File: src/statelattice.ml (return to index)


Statistics:  
kind coverage
binding 46 / 47 (97%)
sequence 0 / 0 (-%)
for 0 / 0 (-%)
if/then 48 / 79 (60%)
try 3 / 3 (100%)
while 0 / 0 (-%)
match/function 64 / 100 (64%)
kind coverage
class expression 0 / 0 (-%)
class initializer 0 / 0 (-%)
class method 0 / 0 (-%)
class value 0 / 0 (-%)
toplevel expression 0 / 0 (-%)
lazy operator 16 / 20 (80%)


Source:

fold all unfold all
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|   (*[18513]*)ST.leq st0.store st1.store && (*[5467]*)EL.leq st0.env st1.env
000015|  
000016| (*  eq : elem -> elem -> bool  *)
000017| let eq st0 st1 =
000018|   (*[0]*)ST.eq st0.store st1.store && (*[0]*)EL.eq st0.env st1.env
000019|  
000020| (*  join : elem -> elem -> bool  *)
000021| let join st0 st1 =
000022|   (*[61142]*){ 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|   (*[0]*){ 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 = (*[13711]*)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|   (*[658]*)if is_bot slat then ((*[5]*)bot,[]) else
000121|   match bi with
000122|   | VL.Error    -> ((*[12]*)bot,[]) (* unreachable *)
000123|   | VL.Exit     -> ((*[2]*)bot,[]) (* unreachable *)
000124|   | VL.Next     ->
000125|     (match vlats with
000126|       | []      -> ((*[0]*)bot,[]) (*error*)
000127|       | vlat::_ ->
000128|         (*[72]*)if VL.may_be_table vlat        then
000129|           (*[72]*)let keys = VL.join VL.nil (* potentially: end of table *)
000130|                        (ST.lookup_all_keys slat.store vlat) in
000131|           (*[72]*)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|           ((*[72]*)slat,[keys;values])    (* then result cannot be nil *)
000135|         else ((*[0]*)bot,[])) (*error*)
000136|   | VL.INext     ->
000137|     (match vlats with
000138|       | []      -> ((*[0]*)bot,[]) (*error*)
000139|       | vlat::_ ->
000140|         (*[15]*)if VL.may_be_table vlat
000141|         then
000142|           (*[15]*)let keys = ST.lookup_all_keys slat.store vlat in
000143|           ((*[15]*)if VL.may_be_number keys
000144|            then
000145|               (*[10]*)let keys   = VL.join VL.nil VL.number in (* potentially: end of table *)
000146|               (*[10]*)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|               ((*[10]*)slat,[keys;values])
000149|            else
000150|               (*[5]*)let keys,values = VL.nil,VL.nil in       (* end of table *)
000151|               ((*[5]*)slat,[keys;values]))
000152|         else ((*[0]*)bot,[])) (*error*)
000153|   | VL.Pairs    ->
000154|     (match vlats with
000155|       | []      -> ((*[0]*)bot,[]) (*error*)
000156|       | vlat::_ ->
000157|         (*[4]*)let vlat' = VL.only_tables vlat in
000158|         (*[4]*)if VL.is_bot vlat'
000159|         then ((*[0]*)bot,[]) (*error*)
000160|         else ((*[4]*)slat,[VL.builtin VL.Next; vlat'; VL.nil]))
000161|   | VL.IPairs    ->
000162|     (match vlats with
000163|       | []      -> ((*[0]*)bot,[]) (*error*)
000164|       | vlat::_ ->
000165|         (*[6]*)let vlat' = VL.only_tables vlat in
000166|         (*[6]*)if VL.is_bot vlat'
000167|         then ((*[0]*)bot,[]) (*error*)
000168|         else ((*[6]*)slat,[VL.builtin VL.INext; vlat'; VL.number])) (* return iterator, table, 0 *)
000169|   | VL.Print    -> ((*[306]*)slat,[VL.nil]) (* no return value specified - Lua2.5 impl returns nil *)
000170|   | VL.Write    ->
000171|     (match vlats with
000172|       | [] -> ((*[7]*)slat, [VL.userdata])
000173|       | vlat::vlats ->
000174|         (*[14]*)if (*[14]*)VL.may_be_number vlat || (*[7]*)VL.may_be_strings vlat (* may succeed *)
000175|         then (*[14]*)apply_builtin bi slat vlats
000176|         else ((*[0]*)bot, []))
000177|   | VL.Tonumber ->
000178|     (match vlats with
000179|       | []      -> ((*[0]*)bot,[]) (*error*)
000180|       | vlat::_ -> 
000181|         (*[34]*)if VL.is_nil vlat then ((*[0]*)bot,[]) (* unreachable *)
000182|         else
000183|           (*[34]*)let retval =
000184|                  if VL.is_number vlat      then (*[28]*)VL.number        (* number arg (at most) *)
000185|             else (*[6]*)if VL.is_strings vlat     then (*[4]*)VL.number_or_nil (* string arg (at most) *)
000186|             else (*[2]*)if VL.may_be_number vlat  then (*[0]*)VL.number_or_nil (* number or other arg   *)
000187|             else (*[2]*)if VL.may_be_strings vlat then (*[2]*)VL.number_or_nil (* string or other arg  *)
000188|             else (*[0]*)VL.nil                                 (* no string or number arguments *)
000189|           in ((*[34]*)slat,[retval]))
000190|   | VL.Tostring ->
000191|     (match vlats with
000192|       | []      -> ((*[0]*)bot,[]) (*error*)
000193|       | vlat::_ -> 
000194|         (*[2]*)if VL.is_bot vlat then ((*[0]*)bot,[]) (* unreachable *)
000195|         else ((*[2]*)slat,[VL.anystring]))
000196|   | VL.Abs
000197|   | VL.Ceil
000198|   | VL.Floor    ->
000199|     (match vlats with
000200|       | vlat::_ ->
000201|         (*[2]*)if VL.is_bot vlat then ((*[0]*)bot, []) (* unreachable *)
000202|         else (*[2]*)if VL.may_be_number (VL.coerce_tonum vlat) then ((*[2]*)slat, [VL.number])
000203|         else ((*[0]*)bot, [])
000204|       | _      -> ((*[0]*)bot, []))
000205|   | VL.Mod      ->
000206|     (match vlats with
000207|       | vl0::vl1::_ -> (*[0]*)let res = VL.binop Ast.Mod vl0 vl1 in
000208|                        (*[0]*)if res = VL.bot then ((*[0]*)bot, [VL.bot])
000209|                        else ((*[0]*)slat, [res])
000210|       | _           -> ((*[0]*)bot, []))
000211|   | VL.Random   ->
000212|     (match vlats with
000213|       | []           -> ((*[0]*)slat,[VL.number])
000214|       | vl0::[]      -> (*[2]*)if VL.may_be_number (VL.coerce_tonum vl0)
000215|                         then ((*[2]*)slat,[VL.number])
000216|                         else ((*[0]*)bot, [])
000217|       | vl0::vl1::[] -> (*[2]*)if (*[2]*)VL.may_be_number (VL.coerce_tonum vl0)
000218|                            && (*[2]*)VL.may_be_number (VL.coerce_tonum vl1)
000219|                         then ((*[2]*)slat,[VL.number])
000220|                         else ((*[0]*)bot, [])
000221|       | _            -> ((*[0]*)bot, []))
000222|   | VL.Strlen   ->
000223|     (match vlats with
000224|       | []      -> ((*[0]*)bot,[]) (*error*)
000225|       | vlat::_ -> 
000226|           (*[35]*)if VL.may_be_strings (VL.coerce_tostring vlat)
000227|           then ((*[33]*)slat,[VL.number])
000228|           else ((*[2]*)bot,[]))
000229|   | VL.Strupper ->
000230|     (match vlats with
000231|       | []      -> ((*[0]*)bot,[]) (*error*)
000232|       | vlat::_ -> ((*[2]*)slat,[VL.upper vlat]))
000233|   | VL.Strlower ->
000234|     (match vlats with
000235|       | []      -> ((*[0]*)bot,[]) (*error*)
000236|       | vlat::_ -> ((*[2]*)slat,[VL.lower vlat]))
000237|   | VL.Strchar  ->
000238|     (match vlats with
000239|       | []          -> ((*[2]*)slat, [VL.string ""])
000240|       | vlat::vlats ->
000241|         (*[6]*)let vlat' = VL.char vlat in
000242|         (*[6]*)if VL.may_be_strings vlat' (* may succeed *)
000243|         then 
000244|           (*[6]*)let slat',vlats' = apply_builtin bi slat vlats in (* recurse *)
000245|           (match vlats' with
000246|             | []        -> ((*[0]*)bot, []) (* propagate error *)
000247|             | vlat''::_ -> ((*[6]*)slat',[VL.binop Ast.Concat vlat' vlat'']))
000248|         else ((*[0]*)bot, []))
000249|   | VL.Strbyte  ->
000250|     (match vlats with
000251|       | []                  -> ((*[0]*)bot, [])
000252|       | arg::[]             -> (*[2]*)if VL.may_be_strings (VL.coerce_tostring arg)
000253|                                then ((*[2]*)slat,[VL.number_or_nil])
000254|                                else ((*[0]*)bot, [])
000255|       | arg1::arg2::[]      -> (*[0]*)if (*[0]*)VL.may_be_strings (VL.coerce_tostring arg1)
000256|                                   && (*[0]*)VL.may_be_number (VL.coerce_tonum arg2)
000257|                                then ((*[0]*)slat,[VL.number_or_nil])
000258|                                else ((*[0]*)bot, [])
000259|       | arg1::arg2::arg3::_ -> (*[2]*)if (*[2]*)VL.may_be_strings (VL.coerce_tostring arg1)
000260|                                   && (*[2]*)VL.may_be_number (VL.coerce_tonum arg2)
000261|                                   && (*[2]*)VL.may_be_number (VL.coerce_tonum arg3)
000262|                                  then (* almost conservative :-) for static strings, length gives a bound *)
000263|                                     ((*[2]*)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 ((*[0]*)bot, []))
000266|   | VL.Strsub   ->
000267|     (match vlats with
000268|       | [] | [ _ ]          -> ((*[0]*)bot, [])
000269|       | arg1::arg2::[]      -> (*[0]*)apply_builtin bi slat ([arg1;VL.number;arg2])
000270|       | arg1::arg2::arg3::_ ->
000271|         (*[8]*)let arg1' = VL.coerce_tostring arg1 in
000272|         (*[8]*)let arg2' = VL.coerce_tonum arg2 in
000273|         (*[8]*)let arg3' = VL.coerce_tonum arg3 in
000274|         (*[8]*)if (*[8]*)VL.may_be_strings arg1' && (*[8]*)VL.may_be_number arg2' && (*[8]*)VL.may_be_number arg3'
000275|         then ((*[8]*)slat,[VL.anystring])
000276|         else ((*[0]*)bot,[]))
000277|   | VL.Sqrt     ->
000278|     (match vlats with
000279|       | []      -> ((*[0]*)bot,[]) (*error*)
000280|       | vlat::_ -> 
000281|           (*[2]*)if VL.may_be_number (VL.coerce_tonum vlat)
000282|           then ((*[2]*)slat,[VL.number])
000283|           else ((*[0]*)bot,[]))
000284|   | VL.Type     ->
000285|     (match vlats with
000286|       | []      -> ((*[0]*)bot,[]) (*error*)
000287|       | vlat::_ -> ((*[16]*)slat,[VL.typep vlat]))
000288|   | VL.Format ->
000289|     (match vlats with
000290|       | []      -> ((*[0]*)bot,[]) (*error*)
000291|       | vlat::_ -> 
000292|              (*[4]*)if VL.is_nil vlat         then ((*[0]*)bot,[]) (*unreachable*)
000293|         else (*[4]*)if VL.may_be_strings vlat then ((*[4]*)slat,[VL.anystring])
000294|         else ((*[0]*)bot,[]))
000295|   | VL.Tblconcat ->
000296|     (match vlats with
000297|       | []          -> ((*[0]*)bot,[]) (*error*)
000298|       | vlat1::vlats1 -> 
000299|         (*[6]*)if VL.may_be_table vlat1
000300|         then (match vlats1 with
000301|           | []            -> ((*[0]*)slat,[VL.anystring]) (* one arg *)
000302|           | vlat2::vlats2 ->
000303|             (*[6]*)if VL.may_be_strings (VL.coerce_tostring vlat2)
000304|             then (match vlats2 with
000305|               | []            -> ((*[2]*)slat,[VL.anystring]) (* two args *)
000306|               | vlat3::vlats3 ->
000307|                 (*[4]*)if VL.may_be_number (VL.coerce_tonum vlat3)
000308|                 then (match vlats3 with
000309|                   | []       -> ((*[2]*)slat,[VL.anystring]) (* three args *)
000310|                   | vlat4::_ ->
000311|                     (*[2]*)if VL.may_be_number (VL.coerce_tonum vlat4)
000312|                     then ((*[2]*)slat,[VL.anystring]) (* four args *)
000313|                     else ((*[0]*)bot,[]))
000314|                 else ((*[0]*)bot,[]))
000315|             else ((*[0]*)bot,[]))
000316|         else ((*[0]*)bot,[])) (*unreachable*)
000317|   | VL.Getmetatable ->
000318|     (match vlats with
000319|       | []      -> ((*[0]*)bot,[]) (*error*)
000320|       | vlat::_ -> ((*[8]*)slat,[ST.get_metatable slat.store vlat]))
000321|   | VL.Setmetatable ->
000322|     (match vlats with
000323|       | []             -> ((*[0]*)bot,[]) (*error*)
000324|       | [_]            -> ((*[0]*)bot,[]) (*error*)
000325|       | vlat::vlat'::_ ->
000326|         (*[70]*)let store' = ST.set_metatable slat.store vlat vlat' in
000327|         ((*[70]*){slat with store = store'},[vlat]))
000328|   | VL.Rawget ->
000329|     (match vlats with
000330|       | []             -> ((*[0]*)bot,[]) (*error*)
000331|       | [_]            -> ((*[0]*)bot,[]) (*error*)
000332|       | vlat::vlat'::_ -> ((*[4]*)slat,[ST.raw_get slat.store vlat vlat']))
000333|   | VL.Rawset ->
000334|     (match vlats with
000335|       | []                     -> ((*[0]*)bot,[]) (*error*)
000336|       | _::[]                  -> ((*[0]*)bot,[]) (*error*)
000337|       | _::_::[]               -> ((*[0]*)bot,[]) (*error*)
000338|       | vlat0::vlat1::vlat2::_ ->
000339|         (*[4]*)let store' = ST.raw_set slat.store vlat0 vlat1 vlat2 in
000340|         ((*[4]*){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|   (*[813]*)if (*[813]*)is_bot slat || (*[813]*)VL.is_bot vlat
000346|   then (*[8]*)bot
000347|   else
000348|     (*[805]*)let store' =
000349|       EL.fold (fun (localslab,_) storeacc ->
000350|                             (*[883]*)let env  = ST.find_label slat.store localslab in
000351|                             (*[883]*)let env' = PL.add_local x vlat env in (* strong update *)
000352|                             (*[883]*)ST.join (ST.add_label slat.store localslab env') storeacc)
000353|         slat.env ST.bot in
000354|     (*[805]*){ 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|   (*[1599]*)if is_bot slat
000359|   then (*[118]*)bot
000360|   else match (xs,vlats) with
000361|     | [],   []          -> (*[660]*)slat
000362|     | x::xs,vlat::vlats ->
000363|       (*[783]*)let slat' = add_local slat vlat x in
000364|       (*[783]*)add_local_list slat' vlats xs
000365|     | x::xs,[]          ->
000366|       (*[30]*)let slat' = add_local slat VL.nil x in (* missing value: assign nil *)
000367|       (*[30]*)add_local_list slat' [] xs
000368|     | [],   vlat::vlats ->
000369|       (*[8]*)add_local_list slat vlats []           (* missing local: drop excess value *)
000370|  
000371| (*  enter_scope : SL -> label -> SL  *)
000372| let enter_scope slat label =
000373|   (*[778]*)if is_bot slat
000374|   then (*[107]*)bot
000375|   else
000376|     (*[671]*){ 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|   (*[394]*)if EL.is_bot scopechain
000382|   then (*[14]*)PL.bot
000383|   else
000384|     (*[380]*)EL.fold (fun (i,is) scset -> (*[380]*)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|   (*[4440]*)let rec scope_read envlab scopechain =
000390|     (*[9234]*)if ST.is_bot slat.store
000391|     then (*[0]*)VL.bot
000392|     else
000393|       (*[9234]*)let env = ST.find_label slat.store envlab in
000394|       (*[9234]*)if PL.is_bot env
000395|       then (*[24]*)VL.bot
000396|       else
000397|         (*[9210]*)try
000398|           (*[9210]*)let vl,abs = PL.find_exn name env in (* slight hack: direct lookup *)
000399|           (*[4525]*)if Abs.eq abs Abs.maybe_absent
000400|           then (*[83]*)VL.join vl (continue_read scopechain)
000401|           else (*[4442]*)vl (* certain entry, don't continue *)
000402|         with Not_found -> (*[4685]*)continue_read scopechain
000403|   (*  continue_read : lab list -> VL  *)
000404|   and continue_read scopechain = match scopechain with
000405|       | [] -> (*[156]*)VL.nil (* not found: return nil *)
000406|       | outerenvlab::scopechain' -> (*[4612]*)scope_read outerenvlab scopechain'
000407|   in
000408|   (*[4440]*)EL.fold (fun (envlab,chain) a -> (*[4622]*)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|   (*[822]*)if (*[822]*)is_bot slat || (*[755]*)VL.is_bot vlat
000413|   then (*[67]*)bot
000414|   else
000415|     (*      scope_write : lab -> lab list -> SL  *)
000416|     (*[755]*)let rec scope_write envlab scopechain =
000417|       (*[1120]*)try
000418|         (*[1120]*)let env = ST.find_label_exn slat.store envlab in
000419|         (*[1120]*)if PL.is_bot env
000420|         then (*[0]*)bot
000421|         else
000422|           (*[1120]*)if PL.mem name env (* slight hack: direct lookup *)
000423|           then
000424|             (*[308]*)let _,abs  = PL.find_exn name env in (* slight hack: direct lookup *)
000425|             (*[308]*)let env'   = PL.add_local name vlat env in (* strong update the local variable *)
000426|             (*[308]*)let store' = ST.add_label slat.store envlab env' in
000427|             (*[308]*)let slat'  = { slat with store = store' } in
000428|             ((*[308]*)if Abs.eq abs Abs.maybe_absent
000429|              then (*[0]*)join slat' (continue_write scopechain)
000430|              else (*[308]*)slat')
000431|           else (*[812]*)continue_write scopechain
000432|       with Not_found -> (*[0]*)bot
000433|     (*  continue_write : list -> SL  *)
000434|     and continue_write scopechain = match scopechain with
000435|       | []          -> (*[0]*)failwith "Outside any environment\n";
000436|       | [globallab] ->
000437|         ((*[522]*)try
000438|           (*[522]*)let globalenv  = ST.find_label_exn slat.store globallab in
000439|           (*[522]*)let globalenv' = PL.add name vlat globalenv in  (* strong update: only *one* global env *)
000440|           (*[522]*)let store'     = ST.add_label slat.store globallab globalenv' in
000441|           (*[522]*){ slat with store = store' }
000442|          with Not_found -> (*[0]*)bot)
000443|       | outerenvlab::scopechain' -> (*[290]*)scope_write outerenvlab scopechain'
000444|     in
000445|     (*[755]*)EL.fold
000446|       (fun (envlab,chain) slatacc -> 
000447|         (*try *)(*[830]*)join (scope_write envlab chain) slatacc
000448|         (*with Not_found -> (*Printf.printf "Unknown environment label\n";*)
000449|                           slatacc*)) slat.env bot
000450|  
000451| (*  write_dyn_prop : SL -> VL -> VL -> VL -> SL *)
000452| let write_dyn_prop slat vlat0 vlat1 vlat =
000453|   (*[349]*)let store' = ST.write_dyn_prop slat.store vlat0 vlat1 vlat in
000454|   (*[349]*){ slat with store = store' }
000455|  
000456| (*  getbinhandler : SL -> VL -> VL -> string -> VL *)
000457| let getbinhandler slat vlat0 vlat1 strevent =
000458|   (*[299]*)ST.getbinhandler slat.store vlat0 vlat1 strevent
000459|  
000460|  
000461| (** {3 Pretty printing} *)
000462|  
000463| (*  pprint : SL -> unit *)
000464| let pprint slat =
000465|     begin
000466|       Format.printf "{ @[<v 0>store:   ";
000467|       ST.pprint slat.store;
000468|       Format.print_space ();
000469|       Format.printf "env:     ";
000470|       EL.pprint slat.env;
000471|       Format.printf "@] }";
000472|     end
000473|  
000474| (*  to_string : elem -> string  *)
000475| let to_string s =
000476|   let buf = Buffer.create 128 in
000477|   let out,flush = Format.get_formatter_output_functions () in (* save previous outputters *)
000478|   begin
000479|     Format.set_formatter_output_functions (Buffer.add_substring buf) (fun () -> ());
000480|     pprint s;
000481|     Format.print_flush ();
000482|     Format.set_formatter_output_functions out flush;       (* restore previous outputters *)
000483|     Buffer.contents buf
000484|   end
Legend:
   some code - line containing no point
   some code - line containing only visited points
   some code - line containing only unvisited points
   some code - line containing both visited and unvisited points

Generated by Bisect 1.3 on 2016-07-04 16:56:57