Changeset 1310 for Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightAnnotator.ml

Timestamp:

Oct 6, 2011, 6:31:27 PM (9 years ago)

Author:

tranquil

Message:

• finished changes on annotator
• implementing indexes in interpreter

File:

• Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightAnnotator.ml (modified) (4 diffs)

Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightAnnotator.ml

@@ -10 +10 @@
 let cost_id_prefix = "_cost"
 let cost_incr_prefix = "_cost_incr"
+let loop_id_prefix = "_i"
 
 
@@ -313 +314 @@
     | Clight.Internal def ->
         let max_depth = max_loop_index def.Clight.fn_body in
-        let indexes_defs = loop_indexes_defs l_ind max_depth in
+        let vars = loop_indexes_defs l_ind max_depth in
+        let vars = List.rev_append vars def.Clight.fn_vars in
         let body = instrument_body l_ind cost_mapping cost_incr def.Clight.fn_body in
-        Clight.Internal { def with Clight.fn_body = body }
+        Clight.Internal { def with Clight.fn_body = body; Clight.fn_vars = vars}
     | Clight.External _ -> def
   in
@@ -361 +363 @@
   let cost_id = StringTools.Gen.fresh_prefix names cost_id_prefix in
   let cost_decl = cost_decl cost_id in
+        
+        (* Create a fresh loop index prefix *)
+        let names = StringTools.Set.add cost_id names in
+  let l_ind = StringTools.Gen.fresh_prefix names loop_id_prefix in
 
   (* Define an increment function for the cost variable. *)
@@ -369 +375 @@
 
   (* Instrument each function *)
-  let prog_funct =
-    List.map (instrument_funct cost_mapping cost_incr) p.Clight.prog_funct in
+  let prog_funct = p.Clight.prog_funct in
+        let prog_funct = 
+    List.map (instrument_funct l_ind cost_mapping cost_incr) prog_funct in
 
   (* Glue all this together. *)