 Timestamp:
 Oct 10, 2011, 4:34:54 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D2.2/8051indexedlabelsbranch/src/RTL/RTLInterpret.ml
r818 r1340 34 34 carry : Val.t } 35 35 36 type indexing = CostLabel.const_indexing 37 36 38 (* Execution states. There are three possible states : 37 39  The constructor [State] represents a state when executing a function … … 41 43 type state = 42 44  State of stack_frame list * RTL.graph * Label.t * Val.address (* sp *) * 43 local_env * Val.t (* carry *) * memory * CostLabel.t list 45 local_env * Val.t (* carry *) * memory * indexing list * 46 CostLabel.t list 44 47  CallState of stack_frame list * RTL.function_def * 45 Val.t list (* args *) * memory* CostLabel.t list48 Val.t list (* args *) * memory * indexing list * CostLabel.t list 46 49  ReturnState of stack_frame list * Val.t list (* return values *) * 47 memory * CostLabel.t list50 memory * indexing list * CostLabel.t list 48 51 49 52 let string_of_local_env lenv = … … 59 62 60 63 let print_state = function 61  State (_, _, lbl, sp, lenv, carry, mem, _) >62 Printf.printf "Stack pointer: %s\n\nCarry: %s\n\nLocal environment:\n%s\n\nMemory:%s\n Regular state: %s\n\n%!"64  State (_, _, lbl, sp, lenv, carry, mem, ind::_, _) > 65 Printf.printf "Stack pointer: %s\n\nCarry: %s\n\nLocal environment:\n%s\n\nMemory:%s\nIndexing:" 63 66 (Val.string_of_address sp) 64 67 (Val.to_string carry) 65 68 (string_of_local_env lenv) 66 (Mem.to_string mem) 69 (Mem.to_string mem); 70 Array.iter (fun a > Printf.printf "%d, " a) ind; 71 Printf.printf "Regular state: %s\n\n%!" 67 72 lbl 68  CallState (_, _, args, mem, _) > 73  State (_, _, _, _, _, _, _, [], _) > assert false (* indexings nonempty *) 74  CallState (_, _, args, mem, _, _) > 69 75 Printf.printf "Memory:%s\nCall state: %s\n\n%!" 70 76 (Mem.to_string mem) 71 77 (string_of_args args) 72  ReturnState (_, vs, mem, _ ) >78  ReturnState (_, vs, mem, _, _) > 73 79 Printf.printf "Memory:%s\nReturn state: %s\n\n%!" 74 80 (Mem.to_string mem) … … 96 102 (* Assign a value to some destinations registers. *) 97 103 98 let assign_state sfrs graph lbl sp lenv carry mem trace destrs vs =104 let assign_state sfrs graph lbl sp lenv carry mem inds trace destrs vs = 99 105 let lenv = adds destrs vs lenv in 100 State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)106 State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace) 101 107 102 108 (* Branch on a value. *) 103 109 104 let branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v =110 let branch_state sfrs graph lbl_true lbl_false sp lenv carry mem inds trace v = 105 111 let next_lbl = 106 112 if Val.is_true v then lbl_true … … 108 114 if Val.is_false v then lbl_false 109 115 else error "Undefined conditional value." in 110 State (sfrs, graph, next_lbl, sp, lenv, carry, mem, trace) 116 State (sfrs, graph, next_lbl, sp, lenv, carry, mem, inds, trace) 117 118 let curr_ind : indexing list > indexing = function 119  ind :: _ > ind 120  _ > assert false (* indexing list must be nonempty *) 121 122 let forget_ind : indexing list > indexing list = function 123  _ :: tail > tail 124  _ > assert false (* indexing list must be nonempty *) 125 126 let max_depth graph = 127 let f_stmt _ = function 128  RTL.St_ind_0(i,_)  RTL.St_ind_inc(i,_) > max (i + 1) 129  _ > fun x > x in 130 Label.Map.fold f_stmt graph 0 111 131 112 132 … … 120 140 (carry : Val.t) 121 141 (mem : memory) 142 (inds : indexing list) 122 143 (stmt : RTL.statement) 123 144 (trace : CostLabel.t list) : … … 125 146 126 147  RTL.St_skip lbl > 127 State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)148 State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace) 128 149 129 150  RTL.St_cost (cost_lbl, lbl) > 130 State (sfrs, graph, lbl, sp, lenv, carry, mem, cost_lbl :: trace) 151 let cost_lbl = CostLabel.apply_const_indexing (curr_ind inds) cost_lbl in 152 State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, cost_lbl :: trace) 153 154  RTL.St_ind_0 (i, lbl) > 155 CostLabel.enter_loop (Some i) (curr_ind inds); 156 State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace) 157 158  RTL.St_ind_inc (i, lbl) > 159 CostLabel.continue_loop (Some i) (curr_ind inds); 160 State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace) 131 161 132 162  RTL.St_addr (r1, r2, x, lbl) > 133 assign_state sfrs graph lbl sp lenv carry mem trace [r1 ; r2]163 assign_state sfrs graph lbl sp lenv carry mem inds trace [r1 ; r2] 134 164 (Mem.find_global mem x) 135 165 136 166  RTL.St_stackaddr (r1, r2, lbl) > 137 assign_state sfrs graph lbl sp lenv carry mem trace [r1 ; r2] sp167 assign_state sfrs graph lbl sp lenv carry mem inds trace [r1 ; r2] sp 138 168 139 169  RTL.St_int (r, i, lbl) > 140 assign_state sfrs graph lbl sp lenv carry mem trace [r] [Val.of_int i]170 assign_state sfrs graph lbl sp lenv carry mem inds trace [r] [Val.of_int i] 141 171 142 172  RTL.St_move (destr, srcr, lbl) > 143 assign_state sfrs graph lbl sp lenv carry mem trace [destr]173 assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] 144 174 [get_local_value lenv srcr] 145 175 … … 149 179 (get_local_value lenv srcr1) 150 180 (get_local_value lenv srcr2) in 151 assign_state sfrs graph lbl sp lenv carry mem trace181 assign_state sfrs graph lbl sp lenv carry mem inds trace 152 182 [destr1 ; destr2] [v1 ; v2] 153 183 154 184  RTL.St_op1 (op1, destr, srcr, lbl) > 155 185 let v = Eval.op1 op1 (get_local_value lenv srcr) in 156 assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]186 assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v] 157 187 158 188  RTL.St_op2 (op2, destr, srcr1, srcr2, lbl) > … … 161 191 (get_local_value lenv srcr1) 162 192 (get_local_value lenv srcr2) in 163 assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]193 assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v] 164 194 165 195  RTL.St_clear_carry lbl > 166 State (sfrs, graph, lbl, sp, lenv, Val.zero, mem, trace)196 State (sfrs, graph, lbl, sp, lenv, Val.zero, mem, inds, trace) 167 197 168 198  RTL.St_set_carry lbl > 169 State (sfrs, graph, lbl, sp, lenv, Val.of_int 1, mem, trace)199 State (sfrs, graph, lbl, sp, lenv, Val.of_int 1, mem, inds, trace) 170 200 171 201  RTL.St_load (destr, addr1, addr2, lbl) > 172 202 let addr = get_local_addr lenv addr1 addr2 in 173 203 let v = Mem.load mem chunk addr in 174 assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]204 assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v] 175 205 176 206  RTL.St_store (addr1, addr2, srcr, lbl) > 177 207 let addr = get_local_addr lenv addr1 addr2 in 178 208 let mem = Mem.store mem chunk addr (get_local_value lenv srcr) in 179 State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)209 State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace) 180 210 181 211  RTL.St_call_id (f, args, ret_regs, lbl) > … … 186 216 sp = sp ; lenv = lenv ; carry = carry } 187 217 in 188 CallState (sf :: sfrs, f_def, args, mem, trace)218 CallState (sf :: sfrs, f_def, args, mem, inds, trace) 189 219 190 220  RTL.St_call_ptr (f1, f2, args, ret_regs, lbl) > … … 194 224 let sf = { ret_regs = ret_regs ; graph = graph ; pc = lbl ; 195 225 sp = sp ; lenv = lenv ; carry = carry } in 196 CallState (sf :: sfrs, f_def, args, mem, trace)226 CallState (sf :: sfrs, f_def, args, mem, inds, trace) 197 227 198 228  RTL.St_tailcall_id (f, args) > … … 200 230 let args = get_arg_values lenv args in 201 231 let mem = Mem.free mem sp in 202 CallState (sfrs, f_def, args, mem, trace)232 CallState (sfrs, f_def, args, mem, inds, trace) 203 233 204 234  RTL.St_tailcall_ptr (f1, f2, args) > … … 207 237 let args = get_arg_values lenv args in 208 238 let mem = Mem.free mem sp in 209 CallState (sfrs, f_def, args, mem, trace)239 CallState (sfrs, f_def, args, mem, inds, trace) 210 240 211 241  RTL.St_cond (srcr, lbl_true, lbl_false) > 212 242 let v = get_local_value lenv srcr in 213 branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v243 branch_state sfrs graph lbl_true lbl_false sp lenv carry mem inds trace v 214 244 215 245  RTL.St_return rl > 216 246 let vl = List.map (get_local_value lenv) rl in 217 247 let mem = Mem.free mem sp in 218 ReturnState (sfrs, vl, mem, trace)248 ReturnState (sfrs, vl, mem, inds, trace) 219 249 220 250 … … 240 270 (args : Val.t list) 241 271 (mem : memory) 272 (inds : indexing list) 242 273 (trace : CostLabel.t list) : 243 274 state = 244 275 match f_def with 245 276  RTL.F_int def > 277 let ind = Array.make (max_depth def.RTL.f_graph) 0 in 246 278 let (mem', sp) = Mem.alloc mem def.RTL.f_stacksize in 247 279 State (sfrs, def.RTL.f_graph, def.RTL.f_entry, sp, 248 280 init_locals def.RTL.f_locals def.RTL.f_params args, 249 Val.undef, mem', trace)281 Val.undef, mem', ind::inds, trace) 250 282  RTL.F_ext def > 251 283 let (mem', vs) = interpret_external mem def.AST.ef_tag args in 252 ReturnState (sfrs, vs, mem', trace)284 ReturnState (sfrs, vs, mem', inds, trace) 253 285 254 286 let state_after_return … … 257 289 (ret_vals : Val.t list) 258 290 (mem : memory) 291 (inds : indexing list) 259 292 (trace : CostLabel.t list) : 260 293 state = 261 294 let f i lenv r = Register.Map.add r (List.nth ret_vals i) lenv in 262 295 let lenv = MiscPottier.foldi f sf.lenv sf.ret_regs in 263 State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, trace) 296 let inds = forget_ind inds in 297 State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, inds, trace) 264 298 265 299 266 300 let small_step (st : state) : state = match st with 267  State (sfrs, graph, pc, sp, lenv, carry, mem, trace) >301  State (sfrs, graph, pc, sp, lenv, carry, mem, inds, trace) > 268 302 let stmt = Label.Map.find pc graph in 269 interpret_statement sfrs graph sp lenv carry mem stmt trace270  CallState (sfrs, f_def, args, mem, trace) >271 state_after_call sfrs f_def args mem trace272  ReturnState ([], ret_vals, mem, trace) >303 interpret_statement sfrs graph sp lenv carry mem inds stmt trace 304  CallState (sfrs, f_def, args, mem, inds, trace) > 305 state_after_call sfrs f_def args mem inds trace 306  ReturnState ([], ret_vals, mem, inds, trace) > 273 307 assert false (* End of execution; handled in iter_small_step. *) 274  ReturnState (sf :: sfrs, ret_vals, mem, trace) >275 state_after_return sf sfrs ret_vals mem trace308  ReturnState (sf :: sfrs, ret_vals, mem, inds, trace) > 309 state_after_return sf sfrs ret_vals mem inds trace 276 310 277 311 … … 292 326 if debug then print_state st ; 293 327 match small_step st with 294  ReturnState ([], vs, mem, trace) >295 print_and_return_result (compute_result vs, List.revtrace)328  ReturnState ([], vs, mem, _, trace) > 329 print_and_return_result (compute_result vs, trace) 296 330  st' > iter_small_step debug st' 297 331 … … 321 355 let mem = init_mem p in 322 356 let main_def = find_function mem main in 323 let st = CallState ([], main_def, [], mem, [] ) in357 let st = CallState ([], main_def, [], mem, [], []) in 324 358 iter_small_step debug st
Note: See TracChangeset
for help on using the changeset viewer.