Changeset 1542 for Deliverables/D2.2/8051/src/LTL

Timestamp:

Nov 23, 2011, 5:43:24 PM (9 years ago)

Author:

tranquil

Message:

merge of indexed labels branch

Location:

Deliverables/D2.2/8051/src/LTL

Files:

• LTL.mli (modified) (1 diff)
• LTLInterpret.ml (modified) (6 diffs)
• LTLPrinter.ml (modified) (1 diff)
• LTLToLIN.ml (modified) (1 diff)
• LTLToLINI.ml (modified) (1 diff)
• branch.ml (modified) (1 diff)

Deliverables/D2.2/8051/src/LTL/LTL.mli

@@ -18 +18 @@
   (* Emit a cost label. *)
   | St_cost of CostLabel.t * Label.t
+
+  (* Reset to 0 a loop index *) 
+  | St_ind_0 of CostLabel.index * Label.t
+
+  (* Increment a loop index *)
+  | St_ind_inc of CostLabel.index * Label.t
 
   (* Assign an integer constant to a register. Parameters are the destination

Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml

@@ -31 +31 @@
       renv   : hdw_reg_env ;
       mem    : memory ;
+      inds   : CostLabel.const_indexing list ;
       trace  : CostLabel.t list }
 
@@ -44 +45 @@
 let change_trace st trace = { st with trace = trace }
 let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
+let ev_label st = CostLabel.ev_indexing (CostLabel.curr_const_ind st.inds)
+let new_ind st = { st with inds = CostLabel.new_const_ind st.inds }
+let forget_ind st = { st with inds = CostLabel.forget_const_ind st.inds }
+let enter_loop st = CostLabel.enter_loop st.inds
+let continue_loop st = CostLabel.continue_loop st.inds
 
 let empty_state =
@@ -52 +58 @@
     renv   = I8051.RegisterMap.empty ;
     mem    = Mem.empty ;
+    inds   = [] ;
     trace  = [] }
 
@@ -95 +102 @@
 let init_fun_call lbls_offs st ptr def =
   let pc = entry_pc lbls_offs ptr def in
+  let st = new_ind st in
   change_pc st pc
 
@@ -207 +215 @@
 
 let interpret_return lbls_offs st =
+  let st = forget_ind st in
   let (st, pc) = return_pc st in
   change_pc st pc
@@ -227 +236 @@
 
     | LTL.St_cost (cost_lbl, lbl) ->
+      let cost_lbl = ev_label st cost_lbl in
       let st = add_trace st cost_lbl in
+      next_pc st lbl
+
+    | LTL.St_ind_0 (i, lbl) ->
+      enter_loop st i;
+      next_pc st lbl
+
+    | LTL.St_ind_inc (i, lbl) ->
+      continue_loop st i; 
       next_pc st lbl
 

Deliverables/D2.2/8051/src/LTL/LTLPrinter.ml

@@ -25 +25 @@
     Printf.sprintf "*** %s *** --> %s" s lbl
   | LTL.St_cost (cost_lbl, lbl) ->
+    let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
     Printf.sprintf "emit %s --> %s" cost_lbl lbl
+  | LTL.St_ind_0 (i, lbl) ->
+    Printf.sprintf "index %d --> %s" i lbl
+  | LTL.St_ind_inc (i, lbl) ->
+    Printf.sprintf "increment %d --> %s" i lbl
   | LTL.St_int (dstr, i, lbl) ->
     Printf.sprintf "imm %s, %d --> %s" (print_reg dstr) i lbl

Deliverables/D2.2/8051/src/LTL/LTLToLIN.ml

@@ -22 +22 @@
   | LTL.St_cost (lbl, _) ->
     LIN.St_cost lbl
+  | LTL.St_ind_0 (i, _) ->
+    LIN.St_ind_0 i
+  | LTL.St_ind_inc (i, _) ->
+    LIN.St_ind_inc i
   | LTL.St_int (r, i, _) ->
     LIN.St_int (r, i)

Deliverables/D2.2/8051/src/LTL/LTLToLINI.ml

@@ -117 +117 @@
         | LTL.St_comment (_, l)
         | LTL.St_cost (_, l)
+        | LTL.St_ind_0 (_, l)
+        | LTL.St_ind_inc (_, l)
         | LTL.St_int (_, _, l)
         | LTL.St_pop l

Deliverables/D2.2/8051/src/LTL/branch.ml

@@ -52 +52 @@
     | LTL.St_cost (lbl, l) ->
       LTL.St_cost (lbl, rep l)
+    | LTL.St_ind_0 (i, l) ->
+      LTL.St_ind_0 (i, rep l)
+    | LTL.St_ind_inc (i, l) ->
+      LTL.St_ind_inc (i, rep l)
     | LTL.St_int (r, i, l) ->
       LTL.St_int (r, i, rep l)