000032| | v::vs,w::ws -> (*[30]*)(VL.join v w)::(join_rlat_lists vs ws)
000033|
000034| (** {2 Monad } *)
000035|
000036| (** The following 'return' and 'bind' implements a (syntactic) monad
000037| which is handy to avoid a lot of let bindings. *)
000038|
000039| let return vlat = fun (alat,slat) -> ((*[14796]*)alat,slat,vlat)
000040| let red_return vlat =
000041| fun (alat,slat) -> (*[7490]*)if (*[7490]*)VL.is_bot vlat || (*[6789]*)SL.is_bot slat ||
000042| (*[6417]*)ST.is_bot slat.SL.store || (*[6417]*)EL.is_bot slat.SL.env
000043| then ((*[1073]*)alat,SL.bot,VL.bot) else ((*[6417]*)alat,slat,vlat)
000044| let list_return vlat = fun (alat,slat) -> ((*[8891]*)alat,slat,[vlat])
000045| let red_list_return vlats =
000046| fun (alat,slat) -> (*[1078]*)if (*[1078]*)vlats = [] || (*[1057]*)vlats = [VL.bot] ||
000047| (*[940]*)SL.is_bot slat || (*[940]*)ST.is_bot slat.SL.store || (*[938]*)EL.is_bot slat.SL.env
000048| then ((*[140]*)alat,SL.bot,[VL.bot]) else ((*[938]*)alat,slat,vlats)
000049|
000050| let bind v f = fun (alat,slat) -> match v (alat,slat) with
000051| | (alat',slat',vlat) -> (*[60110]*)f vlat (alat',slat')
000052| let ( >>= ) = (*[1]*)bind
000053|
000054|
000055| (** {3 Monadic operations } *)
000056|
000057| let adjust_to_single vlats = match vlats with
000075|
000076| let enter_scope label = fun (alat,slat) -> ((*[778]*)alat, SL.enter_scope slat label, ())
000077| let add_locals xs vlats = fun (alat,slat) -> ((*[778]*)alat, SL.add_local_list slat vlats xs, ())
000078|
000079|
000080| (** {4 lvalue read/write operations } *)
000081|
000082| let read_name x = (*[4183]*)get_curr_state >>= fun slat -> (*[4240]*)red_return (SL.read_name slat x)
000083| let lookup_event tabv strev = (*[975]*)get_curr_state >>= fun slat -> (*[975]*)return (ST.lookup_event slat.SL.store tabv strev)
000084| let raw_get tabv idxv = (*[975]*)get_curr_state >>= fun slat -> (*[975]*)return (ST.raw_get slat.SL.store tabv idxv)
000085|
000086| let write_name n vlat = (*[822]*)get_curr_state >>= fun slat ->
000087| (*[822]*)let slat' = SL.write_name slat n vlat in
000088| (*[822]*)restore_state slat'
000089|
000090| let write_dyn_prop vlat0 vlat1 vlat = (*[349]*)get_curr_state >>= fun slat ->
000091| (*[349]*)let slat' = SL.write_dyn_prop slat vlat0 vlat1 vlat in
000092| (*[349]*)restore_state slat'
000093|
000094| let alloc_closure l prop_chain =
000095| fun (alat,slat) -> ((*[394]*)alat,{slat with SL.store = ST.add_label slat.SL.store l prop_chain},())
000096|
000097| let alloc_resstore ret_label vlats = (* Hack: write 'ret_label.ret_label.res1' in heap *)
000098| fun (alat,slat) ->
000099| (*[461]*)if SL.is_bot slat then ((*[226]*)alat,SL.bot,ST.bot)
000100| else
000101| (*[235]*)let vlats = match vlats with
000102| | [] -> [(*[2]*)VL.nil] (* if return is empty, return nil value *)
000103| | _ -> (*[233]*)vlats in
000104| (*[235]*)let _,res_table = List.fold_left
000105| (fun (i,tbl) vlat -> (*[263]*)let entry = "res" ^ (string_of_int i) in
000106| ((*[263]*)i+1,PL.add entry vlat tbl)) (1,PL.mt) vlats in
000107| ((*[235]*)alat,slat,ST.add_label slat.SL.store ret_label res_table)
000108|
000109| let getbinhandler op1 op2 event =
000110| fun (alat,slat) -> ((*[299]*)alat,slat,SL.getbinhandler slat op1 op2 event)
000111|
000112| (** {4 control flow operations } *)
000113|
000114| let and_join slat0 vlat0 slat1 vlat1 =
000115| (fun (alat,slat) -> (* potentially false if overapprox. has nil *)
000116| (*[40]*)let slat,vlat = if VL.may_be_nil vlat0 then ((*[2]*)slat0,vlat0) else ((*[38]*)SL.bot,VL.bot) in
000117| (*[40]*)let slat',vlat' = if VL.may_be_non_nil vlat0 then ((*[38]*)slat1,vlat1) else ((*[2]*)SL.bot,VL.bot) in
000118| ((*[40]*)alat, SL.join slat slat', VL.join vlat vlat')) (* potentially true if overapprox. has non nil *)
000119| (* potentially reduce *)
000120|
000121| let or_join slat0 vlat0 slat1 vlat1 =
000122| (fun (alat,slat) -> (* potentially true if overapprox. has non nil *)
000123| (*[14]*)let slat,vlat = if VL.may_be_non_nil vlat0 then ((*[12]*)slat0,VL.exclude_nil vlat0) else ((*[2]*)SL.bot,VL.bot) in
000124| (*[14]*)let slat',vlat' = if VL.may_be_nil vlat0 then ((*[2]*)slat1,vlat1) else ((*[12]*)SL.bot,VL.bot) in
000125| ((*[14]*)alat, SL.join slat slat', VL.join vlat vlat')) (* potentially false if overapprox. has nil *)
000126| (* potentially reduce *)
000127|
000128| let mvl_join branch1 branch2 = (fun (alat,slat) ->
000129| (*[2249]*)let (alat1,slat1,vlat1) = branch1 (alat,slat) in
000130| (*[2249]*)let (alat2,slat2,vlat2) = branch2 (alat,slat) in
000131| ((*[2249]*)AL.join alat1 alat2, SL.join slat1 slat2, VL.join vlat1 vlat2))
000132|
000133| let branch_and_join env thenbr elsebr =
000134| (fun lat -> (*[145]*)let (alat1,slat1,()),(alat2,slat2,()) = thenbr lat, elsebr lat in
000135| (*[145]*)let joined_store = ST.join slat1.SL.store slat2.SL.store in
000136| ((*[145]*)AL.join alat1 alat2, (if ST.leq joined_store ST.bot then (*[47]*)SL.bot
000137| else (*[98]*){SL.env = env; SL.store = joined_store}), ()))
000138|
000139| let rec loop test body =
000140| (fun (alat_prev,slat_prev) ->
000141| (*[207]*)let (alat',slat',_vlat') = test (alat_prev,slat_prev) in
000142| (*[207]*)let (alat'',slat'',()) = body (alat',slat') in
000143| (*[207]*)if (*[207]*)AL.leq alat'' alat' && (*[129]*)ST.leq slat''.SL.store slat'.SL.store (* Fixpoint upto scoping of local variables *)
000144| then ((*[104]*)alat',slat',())
000145| else (*[103]*)loop (* Otherwise:iterate *)
000146| test body ((*AL.join alat'*) alat'', {slat'' with SL.store = ST.join slat'.SL.store slat''.SL.store}))
000147|
000148|
000149| (** {3 Transfer functions } *)
000150|
000151| (* transfer_call : label -> label -> VL list -> info -> (AL * SL) -> (AL * SL * VL list) *)
000152| let transfer_call clab tgtlabel vlats info (alat,slat) =
000153| (*[470]*)let f = info.fun_map tgtlabel in
000154| match f with
000155| | L.Fun (label',xs,bl,ret_label) ->
000156| (*[470]*)if (tgtlabel != label')
000161| | Some bl ->
000162| (*[470]*)let body_label = bl.L.label in
000163| (*[470]*)let entry_state = AL.lookup alat body_label in
000164| (*
000165| Caller invariant: - pass arguments and clabel
000166| - receive results through ret_label entry
000167|
000168| Receiver invariant: - pair formals and actuals and store in clabel,
000169| - add an extended scope chain,
000170| - store result(s) in AL[ret_label][ret_label][res1]
000171|
000172| Needs two allocation sites
000173| - caller-entry - for scope-chain allocation
000174| - caller-exit - for ?
000175|
000176| propagate call: - vlats into localenv of function label
000177| - slat.store into store of function label
000178| propagate return: - vlat results from return label to caller
000179| - slat.store from return label into store of caller
000180| *)
000181| (* caller: clab callee: tgtlabel body_label ret_label *)
000182|
000183| (* extend stored env with new level *)
000184| (*[470]*)let ext_env = ST.fold_labels_scopechain
000185| (fun is accpairset -> (*[468]*)EL.PairSet.add (clab,is) accpairset)
000186| slat.SL.store tgtlabel EL.PairSet.empty in
000187| (*[470]*)if EL.is_bot ext_env (* scopechain potentially deleted because of domain reduction *)
000188| then ((*[2]*)alat,slat,[VL.bot])
000189| else
000190| (* add bindings from formals to actuals *)
000191| (* join store and environment into receiver's state *)
000192| (*[468]*)let entry_state' = SL.join entry_state
000193| { SL.store =
000194| ST.add_label slat.SL.store clab (PL.add_all_params xs vlats PL.mt);
000195| SL.env = ext_env } in
000196| (*[468]*)let alat' = AL.add alat body_label entry_state' in
000197|
000198| (* lookup exit state and results *)
000199| (*[468]*)let exit_state = AL.lookup alat' ret_label in
000200| (* if body reachable but exit is bot,
000201| either func completes abnormally
000202| or: flow has not propagated through function yet *)
000203| (*[468]*)if (*[468]*)not (SL.is_bot entry_state) && (*[383]*)SL.is_bot exit_state
000204| then ((*[34]*)alat',SL.bot,[VL.bot]) (* unreachable: no return state injected *)
000205| else
000206| (*[434]*)let exit_prop = ST.find_label exit_state.SL.store ret_label in
000207|
000208| (*[434]*)let rec build_res_lat i =
000209| ((*[817]*)try
000210| (*[817]*)let entry = "res" ^ (string_of_int i) in
000211| (*[817]*)let vlat,abs = PL.find_exn entry exit_prop in
000212| (*[383]*)let vlats = build_res_lat (i+1) in
000213| (*[383]*)if abs = Abs.is_present (* result arity may vary: if so, include nil *)
000214| then (*[275]*)vlat::vlats
000215| else (*[108]*)(VL.join vlat VL.nil)::vlats
000216| with Not_found ->
000217| (*[434]*)if i=1
000218| then [(*[85]*)VL.bot] (* no result yet: head is bot *)
000219| else (*[349]*)[]) in (* Hack: read 'result' local *)
000220|
000221| (*[434]*)let res_lats = build_res_lat 1 in
000222| (* Note: L.Return is responsible for propagating to ret_label
000223| Here we only read off the propagated input *)
000224|
000225| (* return store/heap effects to caller's state (joined by transfer_calls) *)
000226| (* and restore environment*)
000227| (*[434]*)let slat' = (*SL.join slat*)
000228| { SL.store = exit_state.SL.store;
000229| SL.env = slat.SL.env (* EL.bot;*) } in
000230| ((*[434]*)alat',slat',res_lats)
000231| )
000232| | _ ->
000234|
000235| (* transfer_calls : label -> VL -> VL list -> info -> (AL * SL) -> (AL * SL * VL list) *)
000236| let transfer_calls clab vlat vlats info =
000237| (*[1281]*)if not (VL.may_be_proc vlat) (* type error: receiver is definitely not a function *)
000238| then (*[203]*)restore_state SL.bot >>= fun () -> (*[203]*)list_return VL.bot
000239| else
000240| (*[1078]*)(fun (alat,slat) ->
000241| (*[1078]*)let funs = vlat.VL.funs in
000242| (*[1078]*)VL.ProcSet.fold
000243| (fun proc (alatacc,slatacc,rlatacc) -> match proc with
000244| | VL.Funtag f ->
000245| (*[470]*)let (alatacc',slat',rlats) = transfer_call clab f vlats info (alatacc,slat) in
000246| ((*[470]*)alatacc',SL.join slatacc slat',join_rlat_lists rlatacc rlats)
000247| | VL.Builtin bi ->
000248| (*[638]*)let slat',rlats = SL.apply_builtin bi slat vlats in
000249| ((*[638]*)alatacc,SL.join slatacc slat',join_rlat_lists rlatacc rlats))
000250| funs (alat, { SL.store = ST.bot;
000251| SL.env = EL.bot } ,[]))
000252| >>= red_list_return (* slight hack to reduce to bot on callee error *)
000253|
000254| (* transfer_str : str -> info -> (AL * SL) -> (AL * SL * VL) *)
000255| let rec transfer_str s info =
000256| match s with
000257| | Ast.Normal ns -> (*[856]*)red_return (VL.string ns)
000258| | Ast.Char cs -> (*[161]*)red_return (VL.string cs)
000259| | Ast.Long ls -> (*[10]*)red_return (VL.string ls)
000260|
000261| (* transfer_lit : lit -> info -> (AL * SL) -> (AL * SL * VL) *)
000262| let rec transfer_lit l info =
000263| match l with
000264| | L.Nil -> (*[303]*)red_return VL.nil
000265| | L.Bool _ -> (*[127]*)red_return VL.bool
000266| | L.String s -> (*[1027]*)transfer_str s info
000267| | L.Number _ -> (*[870]*)red_return VL.number
000268| | L.Table (l,uns,ns) ->
000269| (* add unamed entries *)
000270| (*[337]*)transfer_exp_list uns info >>= fun unvlats ->
000271| (*[337]*)let joined_unsvlats = List.fold_left (fun acc vlat -> (*[60]*)VL.join acc vlat) VL.bot unvlats in
000272| (*[337]*)let plat =
000273| (match unvlats with
000274| | [] -> (*[319]*)PL.mt
000275| | _ -> (*[18]*)PL.add_nonstr_default VL.number joined_unsvlats PL.mt) in(*unnamed/numeric all go in default*)
000276| (* add named entries *)
000277| (*[337]*)let (props, exps) = List.split ns in
000278| (*[337]*)transfer_exp_list exps info >>= fun vlats ->
000279| (*[337]*)let plat' = List.fold_left2 (fun plat prop vlat -> (*[313]*)PL.add prop vlat plat) plat props vlats in
000280| (*[337]*)get_curr_state >>= fun slat' ->
000281| (*[337]*)restore_state { slat' with SL.store = ST.add_label slat'.SL.store l plat' } >>= fun () ->
000282| (*[337]*)return (VL.table l)
000283| | L.Fun (l,_,body,ret_label) ->
000284| (match body with
000286| | Some body ->
000287| (*[394]*)get_curr_state >>= fun slat ->
000288| (*[394]*)curr_scope_chain >>= fun scopechain ->
000289| (*[394]*)let prop_chain = SL.build_prop_chain scopechain in
000290| (*[394]*)set_state body.L.label >>= fun () ->
000291| (*[394]*)let fun_info = { info with ret_label = ret_label } in
000292| (*[394]*)transfer_stmts body.L.stmts fun_info >>= fun () ->
000293| (*[394]*)restore_state slat >>= fun () ->
000294| (* allocate abstract closure for l: record scope chain *)
000295| (*[394]*)alloc_closure l prop_chain >>= fun () ->
000296| (*[394]*)return (VL.proc l))
000297| (* invariant: any proc l, has had its scopechain allocated in store *)
000298|
000299| (* transfer_gettable_event : label -> info -> VL -> VL -> (AL * SL) -> AL * SL * VL *)
000300| and transfer_gettable_event clab info tabvlat idxvlat =
000301| (* inner_gettable_event : VL -> VL -> (AL * SL) -> AL * SL * VL *)
000302| (*[647]*)let rec inner_gettable_event tabvlat acc =
000303| (*[1116]*)if VL.is_bot tabvlat (* strict *)
000304| then (*[141]*)return VL.bot
000305| else
000306| (*[975]*)get_curr_state >>= fun slat ->
000307| (*[975]*)raw_get tabvlat idxvlat >>= fun v ->
000308| (*[975]*)lookup_event tabvlat "__index" >>= fun h ->
000309| (*[975]*)mvl_join
000310| (if VL.may_be_table tabvlat
000311| then (*[518]*)return
000312| (VL.join
000313| (VL.exclude_nil v)
000314| (if (*[518]*)VL.may_be_nil v && (*[205]*)VL.may_be_nil h then (*[172]*)VL.nil else (*[346]*)VL.bot))
000315| else (*[457]*)merror)
000316| (mvl_join
000317| (if VL.may_be_proc h
000318| then ((*[45]*)transfer_calls clab h [tabvlat;idxvlat] info >>= (*-- call the handler *)
000319| adjust_to_single)
000320| else (*[930]*)merror)
000321| (let h' = VL.exclude_proc h in
000322| (*[975]*)if VL.leq h' acc
000323| then (*[506]*)merror (* already explored base values *)
000324| else (*[469]*)inner_gettable_event h' (VL.join h' acc))) (*-- or repeat operation on it *)
000325| in
000326| (*[647]*)inner_gettable_event tabvlat VL.bot (* empty accumulator of explored 'base' values *)
000327|
000328| (* transfer_lvalue_read : lvalue -> info -> (AL * SL) -> (AL * SL * VL) *)
000329| and transfer_lvalue_read lv info =
000330| match lv with
000331| | L.Name x ->
000332| (*[4183]*)read_name x
000333| | L.DynIndex (clab,e0,e1) ->
000334| (*[591]*)transfer_exp e0 info >>= adjust_to_single >>= fun vlat0 ->
000335| (*[591]*)transfer_exp e1 info >>= adjust_to_single >>= fun vlat1 ->
000336| (*[591]*)transfer_gettable_event clab info vlat0 vlat1
000337|
000338| (* transfer_lvalue_write_list : lvalue list -> exp list -> info -> (AL * SL) -> (AL * SL * unit) *)
000339| and transfer_lvalue_write_list lvals exps info =
000340| (* Three passes: 1. evaluate lvalues down through recursion
000341| 2. at end, evaluate rhs, left-to-right
000342| 3. perform assignment back through the recursion *)
000343|
000344| (* adjust_length : int -> VL list -> VL list *)
000345| (*[1119]*)let rec adjust_length lvallen vlats = match (lvallen,vlats) with
000346| | (0,[]) -> (*[1098]*)[]
000347| | (0, _) -> (*[21]*)[] (* too many values: drop the rest *)
000348| | (n,[]) -> (*[11]*)VL.nil::(adjust_length (n-1) []) (* too few values: add nils *)
000349| | (n,vlat::vlats) -> (*[1160]*)vlat::(adjust_length (n-1) vlats)
000350| in
000351| (* inner_write_list : lvalue list -> exp list -> info -> (AL * SL) -> (AL * SL * VL list) *)
000352| (*[1119]*)let rec inner_write_list lvs exps info = match lvs with
000353| | [] ->
000354| (*[1119]*)transfer_exp_list exps info >>= fun vlats -> (* step 2: evaluate rhs *)
000355| (*[1119]*)let lvallen = List.length lvals in
000356| (* too few values: add nils, too many values: drop some *)
000357| (*[1119]*)return (List.rev (adjust_length lvallen vlats))
000358| | lv::lvs ->
000359| (match lv with
000360| | Last.Name n ->
000361| (*[822]*)inner_write_list lvs exps info >>= fun vlats ->
000362| (match vlats with
000378|
000379| (* transfer_arith_event : label -> info -> Ast.binop -> string -> VL -> VL -> (AL * SL) -> AL * SL * VL *)
000380| and transfer_arith_event clab info op event op1 op2 =
000381| (*[299]*)let o1,o2 = VL.coerce_tonum op1, VL.coerce_tonum op2 in
000382| (*[299]*)mvl_join
000383| (if VL.may_be_number (VL.meet o1 o2) (* -- both operands are numeric? *)
000384| then (*[197]*)red_return (VL.binop op o1 o2) (* -- '+' here is the primitive 'add' *)
000385| else (*[102]*)merror)
000386| (getbinhandler op1 op2 event >>= fun h ->
000387| (*[299]*)if VL.may_be_proc h
000388| then (* -- call the handler with both operands *)
000389| (*[21]*)transfer_calls clab h [op1;op2] info >>= adjust_to_single
000390| else (* -- no handler available: default behavior *)
000391| (*[278]*)merror)
000392|
000393| (* transfer_binop : op -> label -> info -> VL -> VL -> (AL * SL) -> (AL * SL * VL) *)
000394| and transfer_binop op clab info vlat0 vlat1 = match op with
000395| | Ast.Plus -> (*[125]*)transfer_arith_event clab info op "__add" vlat0 vlat1
000396| | Ast.Minus -> (*[105]*)transfer_arith_event clab info op "__sub" vlat0 vlat1
000397| | Ast.Times -> (*[17]*)transfer_arith_event clab info op "__mul" vlat0 vlat1
000398| | Ast.Div -> (*[9]*)transfer_arith_event clab info op "__div" vlat0 vlat1
000399| | Ast.Mod -> (*[15]*)transfer_arith_event clab info op "__mod" vlat0 vlat1
000400| | Ast.Pow -> (*[28]*)transfer_arith_event clab info op "__pow" vlat0 vlat1
000401| | _ -> (*[312]*)red_return (VL.binop op vlat0 vlat1) (* potentially reduce statelattice to bot *)
000402|
000403| (* transfer_exp : exp -> info -> (AL * SL) -> (AL * SL * VL list) *)
000404| and transfer_exp e info = match e with
000405| | L.Lit l ->
000406| (*[3058]*)transfer_lit l info >>=
000407| list_return
000408| | L.Lvalue lv ->
000409| (*[4774]*)transfer_lvalue_read lv info >>=
000410| list_return
000411| | L.Unop (op,e) ->
000412| (*[19]*)transfer_exp e info >>= adjust_to_single >>= fun vlat ->
000413| (*[19]*)red_return (VL.unop op vlat) >>= (* potentially reduce statelattice to bot *)
000414| list_return
000415| | L.Binop (clab,e0,op,e1) ->
000416| (*[569]*)transfer_exp e0 info >>= adjust_to_single >>= fun vlat0 -> (* left-to-right eval *)
000417| (*[611]*)transfer_exp e1 info >>= adjust_to_single >>= fun vlat1 ->
000418| (*[611]*)transfer_binop op clab info vlat0 vlat1 >>=
000419| list_return (* potentially reduce statelattice to bot *)
000420| | L.And (e0,e1) ->
000421| (*[34]*)transfer_exp e0 info >>= adjust_to_single >>= fun vlat0 -> (* left-to-right eval *)
000422| (*[40]*)get_curr_state >>= fun slat0 ->
000423| (*[40]*)transfer_exp e1 info >>= adjust_to_single >>= fun vlat1 ->
000424| (*[40]*)get_curr_state >>= fun slat1 ->
000425| (*[40]*)and_join slat0 vlat0 slat1 vlat1 >>=
000426| list_return
000427| | L.Or (e0,e1) ->
000428| (*[8]*)transfer_exp e0 info >>= adjust_to_single >>= fun vlat0 -> (* left-to-right eval *)
000429| (*[14]*)get_curr_state >>= fun slat0 ->
000430| (*[14]*)transfer_exp e1 info >>= adjust_to_single >>= fun vlat1 ->
000431| (*[14]*)get_curr_state >>= fun slat1 ->
000432| (*[14]*)or_join slat0 vlat0 slat1 vlat1 >>=
000433| list_return
000434| | L.Call (clab,e,es) ->
000435| (*[538]*)transfer_exp e info >>= adjust_to_single >>= fun vlat -> (* left-to-right eval *)
000436| (*[538]*)transfer_exp_list es info >>= fun vlats ->
000437| (*[538]*)transfer_calls clab vlat vlats info
000438| | L.Methcall (clab,ilab,e,mname,es) ->
000439| (*[46]*)transfer_exp e info >>= adjust_to_single >>= fun vlat -> (* left-to-right eval *)
000440| (*[46]*)transfer_gettable_event ilab info vlat (VL.string mname) >>= fun recv ->
000441| (*[46]*)transfer_exp_list es info >>= fun vlats ->
000442| (*[46]*)transfer_calls clab recv (vlat::vlats) info (* pass self (vlat) as first arg *)
000443| | L.Paren e ->
000444| (*[69]*)transfer_exp e info >>= adjust_to_single >>= list_return
000445|
000446| (* transfer_exp_list : exp list -> info -> (AL * SL) -> (AL * SL * VL list) *)
000447| and transfer_exp_list es info =
000448| match es with
000449| | [] -> (*[628]*)return []
000450| | [e] -> (*[3619]*)transfer_exp e info
000451| | e::es ->
000452| (*[788]*)transfer_exp e info >>= adjust_to_single >>= fun vlat ->
000453| (*[788]*)transfer_exp_list es info >>= fun vlats ->
000454| (*[788]*)return (vlat::vlats)
000455|
000456| (* transfer_stmts : stmts -> info -> (AL * SL) -> (AL * SL * unit) *)
000457| and transfer_stmts ss info =
000458| match ss with
000459| | [] ->
000460| (*[767]*)return () (* empty sequence does not necessarily mean 'Return'
000461| -- only when falling through a procedure
000462| patch: add an explicit 'Return nil' to all procedures in parser (when absent) *)
000463| | s::ss ->
000464| (*[3226]*)let lab = s.L.stmt_pos.L.line_label in
000465| (*[3226]*)record_state lab >>= fun () -> (* join into prev.elm. *)
000466| (*[3329]*)set_state lab >>= fun () -> (* and read off joined result *)
000467| (match s.L.stmt with
000468| | L.Break ->
000469| (*[53]*)lookup_state (fst info.break_labels) >>= fun slat_entry -> (* lookup old env and restore it *)
000470| (*[53]*)restore_scope_chain (slat_entry.SL.env) >>= fun () ->
000471| (*[53]*)record_state (snd info.break_labels) >>= fun () -> (*join state into outer break label *)
000472| (*[53]*)restore_state SL.bot >>= fun () -> (* i.e., unreachable *)
000473| (*[53]*)return ()
000474| | L.If (e,bl1,bl2) ->
000475| (*[145]*)curr_scope_chain >>= fun env ->
000476| (*[145]*)transfer_exp e info >>= adjust_to_single >>= fun _vlat ->
000477| (*[145]*)let thenbranch = transfer_block bl1 info in
000478| (*[145]*)let elsebranch = transfer_block bl2 info in
000479| (*[145]*)branch_and_join env thenbranch elsebranch >>= fun () ->
000480| (*[145]*)transfer_stmts ss info
000481| | L.WhileDo (e,bl,endlab) ->
000482| (*[104]*)let loop_info = { info with break_labels = (lab,endlab) } in
000483| (*[104]*)curr_scope_chain >>= fun env ->
000484| (*[104]*)let test = transfer_exp e info >>= adjust_to_single in
000485| (*[104]*)let body = transfer_block bl loop_info >>= fun () -> (*[207]*)restore_scope_chain env in
000486| (*[104]*)loop test body >>= fun () ->
000487| (* joined "breaked state" with post condition *)
000488| (*[104]*)record_state endlab >>= fun () ->
000489| (*[104]*)set_state endlab >>= fun () ->
000490| (*[104]*)transfer_stmts ss info
000491| | L.Doend bl ->
000492| (*[38]*)curr_scope_chain >>= fun env ->
000493| (*[38]*)transfer_block bl info >>= fun () ->
000494| (*[38]*)restore_scope_chain env >>= fun () ->
000495| (*[38]*)transfer_stmts ss info
000496| | L.Assign (lvs,es) ->
000497| (*[1119]*)transfer_lvalue_write_list lvs es info >>= fun () ->
000498| (*[1119]*)transfer_stmts ss info
000499| | L.Local (xs,es) ->
000500| (*[778]*)transfer_exp_list es info >>= fun vlats -> (* left-to-right eval *)
000501| (*[778]*)enter_scope lab >>= fun () ->
000502| (*[778]*)add_locals xs vlats >>= fun () ->
000503| (*[778]*)transfer_stmts ss info
000504| | L.Callstmt (e,es) ->
000505| (*[621]*)transfer_exp e info >>= adjust_to_single >>= fun vlat -> (* left-to-right eval *)
000506| (*[621]*)transfer_exp_list es info >>= fun vlats ->
000507| (*[621]*)transfer_calls lab vlat vlats info >>= fun _vlats -> (* stmt call, so ignore results *)
000508| (*[621]*)transfer_stmts ss info
000509| | L.Methcallstmt (ilab,e,mname,es) ->
000510| (*[10]*)transfer_exp e info >>= adjust_to_single >>= fun vlat -> (* left-to-right eval *)
000511| (*[10]*)transfer_gettable_event ilab info vlat (VL.string mname) >>= fun recv ->
000512| (*[10]*)transfer_exp_list es info >>= fun vlats ->
000513| (*[10]*)transfer_calls lab recv (vlat::vlats) info >>= fun _vlats -> (* pass self (vlat) as first arg *)
000514| (*[10]*)transfer_stmts ss info
000515| | L.Return es ->
000516| (*[461]*)let ret_label = info.ret_label in
000517| (*[461]*)transfer_exp_list es info >>= fun vlats ->
000518| (*[461]*)alloc_resstore ret_label vlats >>= fun ret_store ->
000519| (*[461]*)restore_state { SL.bot with SL.store = ret_store } >>= fun () ->
000520| (*[461]*)record_state ret_label >>= fun () ->
000521| (*[461]*)restore_state SL.bot (* i.e., unreachable *)
000522| )
000523| (* Since return is a control-delimiter,
000524| neither a semantics nor an analysis of a statement list
000525| should be a simple fold *)
000526|
000527| (* transfer_block : block -> info -> (AL * SL) -> (AL * SL * unit) *)
000528| and transfer_block bl info = match bl with
000529| | None -> (*[92]*)return ()
000530| | Some bl -> (*[340]*)transfer_stmts bl.L.stmts info
000531|
000532| (* transfer_prog : Last.prog -> AL *)
000533| let transfer_prog p =
000534| (*[172]*)let init = (AL.init, SL.init) in
000535| (*[172]*)let info = { fun_map = p.L.fun_map;
000536| break_labels = (p.L.ret_label,p.L.ret_label);
000537| ret_label = p.L.ret_label } in
000538| (*[172]*)let stmts = match p.L.last with
000031| | vs, [] -> (*[0]*)vs