dev/sw/annotatedIR.sml

21    type annt = {fspec : thm, ins : exp, outs : exp, context : exp list};
94     else if (List.find (fn m => #2 m = n0) (#1(G.context(n1,gr)))) <> NONE then gr              (* raise Edge *)
108                                    one_node (b, G.embed (([(a,nodeNo)],b,#3 (G.context(b,gr)),[]), gr''))
110                             gr' (#4 (G.context(nodeNo,gr)))
112            one_node (start_node, G.embed(([],start_node, #3 (G.context(start_node,gr)),[]),G.empty))
126                             (SOME start_node,false) (#4 (G.context(nodeNo,gr)))
142            val context = G.context(n,gr)
146            if is_label (#instr ((#3 context):CFG.node)) then
147                 (length (#1 context) > 1, n)
148            else is_rec gr (#2 (hd (#4 context)))
159         fun get_sucL n = #4 (G.context(n,gr));
160         fun get_preL n = #1 (G.context(n,gr));
176         val cond = to_cond (#instr ((#3 (G.context(cmp_node,gr))):CFG.node),
177                             #instr ((#3 (G.context(cj_node,gr))):CFG.node));
198         fun get_sucL n = #4 (G.context(n,gr));
199         fun get_preL n = #1 (G.context(n,gr));
202         val sucL = #4 (G.context(cj_node,gr));
211         val cond = to_cond (#instr ((#3 (G.context(cmp_node,gr))):CFG.node),
212                             #instr ((#3 (G.context(cj_node,gr))):CFG.node));
229    val init_info = {fspec = thm_t, ins = NA, outs = NA, context = []};
240            val (preL,_,{instr = inst', def = def', use = sue'},sucL) = G.context(n,cfg);
249                                         outs = list2pair (List.map to_exp dList), context = []})
284                 val bal_node = #2 (valOf (List.find (fn (flag,n) => flag = 1) (#1 (G.context(lab_node,cfg)))));
285                 val (Assem.OPER {src = rec_argL,...}) = #instr ((#3(G.context(bal_node,cfg))):CFG.node);
289                 val info = {fspec = DECIDE(Term`T`), ins = ins, outs = ins, context = []}
295                                     SC (TR (cond', r_ir_1, {fspec = thm_t, ins = ins, outs = ins, context = []}),
300                                         val ir1 = TR (cond', ir0, {fspec = thm_t, ins = ins, outs = outs, context = []})
301                                         val ir2 = SC (ir1, b_ir, {fspec = thm_t, ins = ins, outs = ins, context = []})
303                                          SC (p_ir, ir2, {fspec = thm_t, ins = ins, outs = outs, context = []})
404     |  get_annt (STM stmL) = {ins = NA, outs = NA, fspec = thm_t, context = []};
406    fun replace_ins {ins = ins', outs = outs', context = context', fspec = fspec'} ins'' =
407            {ins = ins'', outs = outs', context = context', fspec = fspec'};
409    fun replace_outs {ins = ins', outs = outs', context = context', fspec = fspec'} outs'' =
410            {ins = ins', outs = outs'', context = context', fspec = fspec'};
412    fun replace_context {ins = ins', outs = outs', context = context', fspec = fspec'} context'' =
413            {ins = ins', outs = outs', context = context'', fspec = fspec'};
415    fun replace_fspec {ins = ins', outs = outs', context = context', fspec = fspec'} fspec'' =
416            {ins = ins', outs = outs', context = context', fspec = fspec''};
457  (*      Set input, output and context information                                  *)
463    fun adjust_ins ir (outer_info as ({ins = outer_ins, outs = outer_outs, context = outer_context, ...}:annt)) =
464         let val inner_info as {ins = inner_ins, context = inner_context, outs = inner_outs, fspec = inner_spec, ...} = get_annt ir;
488    (* Given the outputs and the context of an ir, calculate its inputs *)
494 fun extract (SC(s1,s2,inner_info)) (outer_info as {outs = outer_outs, context = contextL, ...}:annt) =
503 fun extract (CJ(cond, s1, s2, inner_info)) (outer_info as {outs = outer_outs, context = contextL, ...}:annt) =
508 fun extract (CALL (fname, pre, body, post, info)) (outer_info as {outs = outer_outs, context = contextL, fspec = fout_spec, ...}:annt) =
511 val (fname, pre, body, post, info, outer_info, outer_outs, contextL, fout_spec) = extract s1 {ins = #ins outer_info, outs = #ins s2_info, context = #context s2_info, fspec = #fspec s1_info};
515    fun back_trace (BLK (stmL,inner_info)) (outer_info as {outs = outer_outs, context = contextL, ...}:annt) =
522               BLK (stmL, {outs = outer_outs, ins = set2pair read_inS, context = contextL, fspec = #fspec inner_info})
528     |  back_trace (SC(s1,s2,inner_info)) (outer_info as {outs = outer_outs, context = contextL, ...}) =
536               val s1' = back_trace s1 {ins = #ins outer_info, outs = #ins s2_info, context = #context s2_info, fspec = #fspec s1_info};
539               SC(s1',s2'', {ins = #ins s1_info, outs = #outs s2_info, fspec = thm_t, context = contextL})
542     |  back_trace (CJ(cond, s1, s2, inner_info)) (outer_info as {outs = outer_outs, context = contextL, ...}) =
560     |  back_trace (TR (cond, body, info)) (outer_info as {outs = outer_outs, context = contextL, ...}) =
570     |  back_trace (CALL (fname, pre, body, post, info)) (outer_info as {outs = outer_outs, context = contextL, fspec = fout_spec, ...}) =
591                             else SC (ir0, BLK ([], {context = #context info0, ins = #outs info0, outs = outs, fspec = thm_t}),
596                   else SC (BLK ([], {context = #context info1, ins = ins, outs = #ins info0, fspec = thm_t}),
599           val info =  {ins = ins, outs = outs, context = [], fspec = thm_t}
617                  SC (BLK ([], {ins = outs1, outs = ins2, context = #context info2, fspec = thm_t}), ir2,
628                             BLK ([], {ins = post_outs, outs = outer_outs, context = #context info, fspec = thm_t}),
633               SC (BLK([], {ins = outer_ins, outs = pre_ins, context = #context info, fspec = thm_t}),