Changeset 1067


Ignore:
Timestamp:
Jul 13, 2011, 5:37:42 PM (8 years ago)
Author:
mulligan
Message:

more smaller changes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1066 r1067  
    11571157definition translate_stmt ≝
    11581158  λlenv.
     1159  λret: register. (* change from o'caml code, this is taken from func. record *)
    11591160  λlbl: label.
    11601161  λstmt.
     
    11961197    translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
    11971198  | St_jumptable r l ⇒ ? (* assert false: not implemented yet *)
    1198   | St_return r ⇒
    1199     match r with
    1200     [ None ⇒ add_graph lbl (rtl_st_return [ ]) def
    1201     | Some r ⇒ add_graph lbl (rtl_st_return (find_local_env r lenv)) def
    1202     ]
    1203   | _ ⇒ ?
    1204   ].
    1205 
    1206 let translate_stmt lenv lbl stmt def = match stmt with
    1207 
    1208   | RTLabs.St_skip lbl' ->
    1209     add_graph lbl (RTL.St_skip lbl') def
    1210 
    1211   | RTLabs.St_cost (cost_lbl, lbl') ->
    1212     add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def
    1213 
    1214   | RTLabs.St_cst (destr, cst, lbl') ->
    1215     translate_cst cst (find_local_env destr lenv) lbl lbl' def
    1216 
    1217   | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
    1218     translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv)
    1219       lbl lbl' def
    1220 
    1221   | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
    1222     translate_op2 op2 (find_local_env destr lenv)
    1223       (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def
    1224 
    1225   | RTLabs.St_load (_, addr, destr, lbl') ->
    1226     translate_load (find_local_env addr lenv) (find_local_env destr lenv)
    1227       lbl lbl' def
    1228 
    1229   | RTLabs.St_store (_, addr, srcr, lbl') ->
    1230     translate_store (find_local_env addr lenv) (find_local_env srcr lenv)
    1231       lbl lbl' def
    1232 
    1233   | RTLabs.St_call_id (f, args, None, _, lbl') ->
    1234     add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, [], lbl')) def
    1235 
    1236   | RTLabs.St_call_id (f, args, Some retr, _, lbl') ->
    1237     add_graph lbl (RTL.St_call_id (f, rtl_args args lenv,
    1238                                    find_local_env retr lenv, lbl')) def
    1239 
    1240   | RTLabs.St_call_ptr (f, args, None, _, lbl') ->
    1241     let (f1, f2) = find_and_addr f lenv in
    1242     add_graph lbl (RTL.St_call_ptr (f1, f2, rtl_args args lenv, [], lbl')) def
    1243 
    1244   | RTLabs.St_call_ptr (f, args, Some retr, _, lbl') ->
    1245     let (f1, f2) = find_and_addr f lenv in
    1246     add_graph lbl
    1247       (RTL.St_call_ptr
    1248          (f1, f2, rtl_args args lenv, find_local_env retr lenv, lbl')) def
    1249 
    1250   | RTLabs.St_tailcall_id (f, args, _) ->
    1251     add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def
    1252 
    1253   | RTLabs.St_tailcall_ptr (f, args, _) ->
    1254     let (f1, f2) = find_and_addr f lenv in
    1255     add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def
    1256 
    1257   | RTLabs.St_cond (r, lbl_true, lbl_false) ->
    1258     translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
    1259 
    1260   | RTLabs.St_jumptable _ ->
    1261     error "Jump tables not supported yet."
    1262 
    1263   | RTLabs.St_return None ->
    1264     add_graph lbl (RTL.St_return []) def
    1265 
    1266   | RTLabs.St_return (Some r) ->
    1267     add_graph lbl (RTL.St_return (find_local_env r lenv)) def
     1199  | St_return ⇒ add_graph lbl (rtl_st_return (find_local_env ret lenv)) def
     1200  ].
     1201  [10: cases not_implemented (* jtable case *)
     1202  |*: cases daemon (* TODO: proofs regarding lengths of lists, examine! *)
     1203  ]
     1204qed.
     1205
     1206definition translate_internal ≝
     1207  λdef.
     1208  let runiverse ≝ f_reggen def in
     1209  let lenv ≝ initialize_local_env runiverse
     1210    (f_params def @ f_locals def) (f_result def) in ?.
     1211
     1212let translate_internal def =
     1213  let runiverse = def.RTLabs.f_runiverse in
     1214  let lenv =
     1215    initialize_local_env runiverse
     1216      (def.RTLabs.f_params @ def.RTLabs.f_locals) def.RTLabs.f_result in
     1217  let set_of_list l = List.fold_right Register.Set.add l Register.Set.empty in
     1218  let params = map_list_local_env lenv (List.map fst def.RTLabs.f_params) in
     1219  let locals = map_list_local_env lenv (List.map fst def.RTLabs.f_locals) in
     1220  let locals = set_of_list locals in
     1221  let result = match def.RTLabs.f_result with
     1222    | None -> []
     1223    | Some (r, _) -> find_local_env r lenv in
     1224  let res =
     1225    { RTL.f_luniverse = def.RTLabs.f_luniverse ;
     1226      RTL.f_runiverse = runiverse ;
     1227      RTL.f_result    = result ;
     1228      RTL.f_params    = params ;
     1229      RTL.f_locals    = locals ;
     1230      RTL.f_stacksize = concrete_size def.RTLabs.f_stacksize ;
     1231      RTL.f_graph     = Label.Map.empty ;
     1232      RTL.f_entry     = def.RTLabs.f_entry ;
     1233      RTL.f_exit      = def.RTLabs.f_exit } in
     1234  Label.Map.fold (translate_stmt lenv) def.RTLabs.f_graph res
    12681235
    12691236definition filter_and_to_list_local_env_internal ≝
Note: See TracChangeset for help on using the changeset viewer.