Changeset 1542 for Deliverables/D2.2

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

Files:

• ASM/ASM.mli (modified) (2 diffs)
• ASM/ASMCosts.ml (modified) (1 diff)
• ASM/ASMInterpret.ml (modified) (9 diffs)
• ASM/ASMInterpret.mli (modified) (1 diff)
• ASM/Pretty.ml (modified) (2 diffs)
• ERTL/ERTL.mli (modified) (1 diff)
• ERTL/ERTLInterpret.ml (modified) (7 diffs)
• ERTL/ERTLPrinter.ml (modified) (1 diff)
• ERTL/ERTLToLTLI.ml (modified) (1 diff)
• ERTL/liveness.ml (modified) (5 diffs)
• ERTL/uses.ml (modified) (1 diff)
• LIN/LIN.mli (modified) (1 diff)
• LIN/LINInterpret.ml (modified) (7 diffs)
• LIN/LINPrinter.ml (modified) (1 diff)
• LIN/LINToASM.ml (modified) (2 diffs)
• LTL/LTL.mli (modified) (1 diff)
• LTL/LTLInterpret.ml (modified) (6 diffs)
• LTL/LTLPrinter.ml (modified) (1 diff)
• LTL/LTLToLIN.ml (modified) (1 diff)
• LTL/LTLToLINI.ml (modified) (1 diff)
• LTL/branch.ml (modified) (1 diff)
• RTL/RTL.mli (modified) (1 diff)
• RTL/RTLInterpret.ml (modified) (17 diffs)
• RTL/RTLPrinter.ml (modified) (1 diff)
• RTL/RTLToERTL.ml (modified) (3 diffs)
• RTLabs/RTLabs.mli (modified) (3 diffs)
• RTLabs/RTLabsInterpret.ml (modified) (18 diffs)
• RTLabs/RTLabsPrinter.ml (modified) (7 diffs)
• RTLabs/RTLabsPrinter.mli (modified) (1 diff)
• RTLabs/RTLabsToRTL.ml (modified) (4 diffs)
• acc.ml (modified) (3 diffs)
• checker.ml (modified) (1 diff)
• clight/clight.mli (modified) (3 diffs)
• clight/clightAnnotator.ml (modified) (7 diffs)
• clight/clightAnnotator.mli (modified) (1 diff)
• clight/clightFold.ml (modified) (2 diffs)
• clight/clightFromC.ml (modified) (1 diff)
• clight/clightInterpret.ml (modified) (17 diffs)
• clight/clightLabelling.ml (modified) (4 diffs)
• clight/clightParser.mli (modified) (1 diff)
• clight/clightPrinter.ml (modified) (4 diffs)
• clight/clightToCminor.ml (modified) (3 diffs)
• cminor/cminor.mli (modified) (1 diff)
• cminor/cminorAnnotator.ml (modified) (1 diff)
• cminor/cminorFold.ml (modified) (3 diffs)
• cminor/cminorInterpret.ml (modified) (11 diffs)
• cminor/cminorPrinter.ml (modified) (8 diffs)
• cminor/cminorToRTLabs.ml (modified) (8 diffs)
• common/costLabel.ml (modified) (1 diff)
• common/costLabel.mli (modified) (1 diff)
• common/label.ml (modified) (1 diff)
• common/label.mli (modified) (1 diff)
• languages.ml (modified) (6 diffs)
• languages.mli (modified) (3 diffs)
• options.ml (modified) (4 diffs)
• options.mli (modified) (2 diffs)

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

@@ -102 +102 @@
 type labelled_instruction =
  [ instruction
- | `Cost of string
+ | `Cost of CostLabel.t
+ | `Index of int
+ | `Inc of int
  | `Label of string
  | `Jmp of string
@@ -122 +124 @@
 type program =
     { code        : BitVectors.byte list ;
-      cost_labels : string BitVectors.WordMap.t ;
+      inds        : int BitVectors.WordMap.t ; (* loop index resets *)
+      incs        : int BitVectors.WordMap.t ; (* loop index increments *)
+      cost_labels : CostLabel.t BitVectors.WordMap.t ;
       labels      : BitVectors.word StringTools.Map.t ;
+
       exit_addr   : BitVectors.word ;
       has_main    : bool }

Deliverables/D2.2/8051/src/ASM/ASMCosts.ml

@@ -50 +50 @@
     warning
       (Printf.sprintf
-         "Warning: branching to %s has cost %d, branching to %s has cost %d"
-         (string_of_int (BitVectors.int_of_vect pc1)) cost1
-         (string_of_int (BitVectors.int_of_vect pc2)) cost2) ;
+         "Warning: branching to %X has cost %d, branching to %X has cost %d"
+         (BitVectors.int_of_vect pc1) cost1
+         (BitVectors.int_of_vect pc2) cost2) ;
     max cost1 (compare ((pc2, cost2) :: l))
   | _ :: l -> compare l

Deliverables/D2.2/8051/src/ASM/ASMInterpret.ml

@@ -131 +131 @@
 
   exit_addr   : BitVectors.word;
-  cost_labels : string BitVectors.WordMap.t
+        
+(*
+  ind_0s      : int BitVectors.WordMap.t;
+  ind_incs    : int BitVectors.WordMap.t;
+  cost_labels : CostLabel.t BitVectors.WordMap.t
+*)      
 }
 
@@ -284 +289 @@
 
   exit_addr = BitVectors.zero `Sixteen;
+(*
+  ind_0s = BitVectors.WordMap.empty;
+  ind_incs = BitVectors.WordMap.empty;
   cost_labels = BitVectors.WordMap.empty
+*)
 }
 
@@ -950 +959 @@
    ) (StringTools.Map.empty,0) p.ASM.ppreamble
  in
- let pc,exit_addr,labels,costs =
+ let pc,exit_addr,labels,inds,incs,costs =
   List.fold_left
-   (fun (pc,exit_addr,labels,costs) i ->
+   (fun (pc,exit_addr,labels,inds,incs,costs) i ->
      match i with
-        `Label s when s = p.ASM.pexit_label -> pc, pc, StringTools.Map.add s pc labels, costs
-      | `Label s -> pc, exit_addr, StringTools.Map.add s pc labels, costs
-      | `Cost s -> pc, exit_addr, labels, BitVectors.WordMap.add pc s costs
-      | `Mov (_,_) -> (snd (half_add pc (vect_of_int 3 `Sixteen))), exit_addr, labels, costs
+        `Label s when s = p.ASM.pexit_label -> pc, pc, StringTools.Map.add s pc labels, inds, incs, costs
+      | `Label s -> pc, exit_addr, StringTools.Map.add s pc labels, inds, incs, costs
+      | `Cost s -> pc, exit_addr, labels, inds, incs, BitVectors.WordMap.add pc s costs
+      | `Index i -> pc, exit_addr, labels, BitVectors.WordMap.add pc i inds, incs, costs
+      | `Inc i -> pc, exit_addr, labels, inds, BitVectors.WordMap.add pc i incs, costs
+      | `Mov (_,_) -> (snd (half_add pc (vect_of_int 3 `Sixteen))), exit_addr, labels, inds, incs, costs
+
       | `Jmp _ 
-      | `Call _ -> (snd (half_add pc (BitVectors.vect_of_int 3 `Sixteen))), exit_addr, labels, costs
+      | `Call _ -> (snd (half_add pc (BitVectors.vect_of_int 3 `Sixteen))), exit_addr, labels, inds, incs, costs
       (*CSC: very stupid: always expand to worst opcode *)
       | `WithLabel i ->
@@ -967 +979 @@
         assert (fake_jump = i');
         let pc' = snd (half_add pc' (vect_of_int 5 `Sixteen)) in
-          (snd (half_add pc pc'), exit_addr, labels, costs)
+          (snd (half_add pc pc'), exit_addr, labels, inds, incs, costs)
       | #instruction as i ->
         let i',pc',_ = fetch (load_code_memory (assembly1 i)) (vect_of_int 0 `Sixteen) in
          assert (i = i');
-         (snd (half_add pc pc'),exit_addr,labels, costs)
+         (snd (half_add pc pc'),exit_addr,labels, inds, incs, costs)
    )
     (BitVectors.zero `Sixteen,BitVectors.zero `Sixteen,
-     StringTools.Map.empty, BitVectors.WordMap.empty) p.ASM.pcode
+     StringTools.Map.empty, BitVectors.WordMap.empty, BitVectors.WordMap.empty,
+     BitVectors.WordMap.empty) p.ASM.pcode
  in
  let code =
@@ -980 +993 @@
      (function
         `Label _
-      | `Cost _ -> []
+      | `Cost _
+      | `Index _
+      | `Inc _ -> []
       | `WithLabel i ->
          (* We need to expand a conditional jump to a label to a machine language
@@ -1032 +1047 @@
                  address, reconstructed
          in
-           let sjmp, jmp = `SJMP (`REL (vect_of_int 3 `Eight)), `LJMP (`ADDR16 jmp_address) in
+           let sjmp = `SJMP (`REL (vect_of_int 3 `Eight)) in
+           let jmp = `LJMP (`ADDR16 jmp_address) in
            let translation = [ translated_jump; sjmp; jmp ] in
              List.flatten (List.map assembly1 translation)
@@ -1048 +1064 @@
             assembly1 (`LCALL (`ADDR16 pc_offset ))
       | #instruction as i -> assembly1 i) p.ASM.pcode) in
- { ASM.code = code ; ASM.cost_labels = costs ;
+ { ASM.code = code ;
+   ASM.inds = inds; ASM.incs = incs; ASM.cost_labels = costs ;
    ASM.labels = StringTools.Map.empty ;
    ASM.exit_addr = exit_addr ; ASM.has_main = p.ASM.phas_main }
@@ -1975 +1992 @@
 let load_program p =
   let st = load p.ASM.code initialize in
-  { st with exit_addr = p.ASM.exit_addr ; cost_labels = p.ASM.cost_labels }
-
-let observe_trace trace_ref st =
-  let cost_label =
-    if BitVectors.WordMap.mem st.pc st.cost_labels then
-      [BitVectors.WordMap.find st.pc st.cost_labels]
-    else [] in
-  trace_ref := cost_label @ !trace_ref ;
+  { st with exit_addr = p.ASM.exit_addr (* ; cost_labels = p.ASM.cost_labels *)}
+
+type cost_trace = {
+  mutable ct_labels : CostLabel.t list;
+  mutable ct_inds   : CostLabel.const_indexing list;
+}
+
+(* FIXME: supposing only one index reset or increment per instruction *)
+let update_indexes trace p st =
+  try
+    let i = BitVectors.WordMap.find st.pc p.ASM.inds in
+    CostLabel.enter_loop trace.ct_inds i
+  with Not_found -> ();
+    try
+      let i = BitVectors.WordMap.find st.pc p.ASM.incs in
+      CostLabel.continue_loop trace.ct_inds i
+    with Not_found -> ();
+      let instr,_,_ = fetch st.code_memory st.pc in
+      match instr with
+        | `ACALL _ | `LCALL _ ->
+          trace.ct_inds <- CostLabel.new_const_ind trace.ct_inds
+        | `RET ->
+          trace.ct_inds <- CostLabel.forget_const_ind trace.ct_inds
+        | _ -> ()
+
+let update_labels trace p st =
+  try
+    let cost_label = BitVectors.WordMap.find st.pc p.cost_labels in
+    let ind = CostLabel.curr_const_ind trace.ct_inds in
+    let cost_label = CostLabel.ev_indexing ind cost_label in
+    trace.ct_labels <- cost_label :: trace.ct_labels
+  with Not_found -> ()
+
+
+
+let update_trace trace p st =
+  update_labels trace p st;
+  update_indexes trace p st;
   if st.pc = st.exit_addr (* <=> end of program *) then raise Halt else st
 
@@ -2000 +2047 @@
   if p.ASM.has_main then
     let st = load_program p in
-    let trace = ref [] in
-    let callback = observe_trace trace in
+    let trace = {ct_labels = []; ct_inds = []} in
+    let callback = update_trace trace p in
     let st = execute callback st in
     let res = result st in
     if debug then
       Printf.printf "Result = %s\n%!" (IntValue.Int32.to_string res) ;
-    (res, List.rev !trace)
+    (res, List.rev trace.ct_labels)
   else (IntValue.Int32.zero, [])
 

Deliverables/D2.2/8051/src/ASM/ASMInterpret.mli

@@ -98 +98 @@
 
       exit_addr   : BitVectors.word;
-      cost_labels : string BitVectors.WordMap.t
+(*
+      ind_0s      : int BitVectors.WordMap.t;
+      ind_incs    : int BitVectors.WordMap.t;
+      cost_labels : CostLabel.t BitVectors.WordMap.t
+*)
     }
       

Deliverables/D2.2/8051/src/ASM/Pretty.ml

@@ -43 +43 @@
  function
     `Label l -> l ^ ":"
-  | `Cost l -> l ^ ":"
+  | `Cost l -> CostLabel.string_of_cost_label ~pretty:true l ^ ":"
+  | `Index i -> "index " ^ string_of_int i ^ ":"
+  | `Inc i -> "increment " ^ string_of_int i ^ ":"
   | `Jmp j -> "ljmp  " ^ j
   | `Call j -> "lcall " ^ j
@@ -96 +98 @@
   | `XRL(`U2(a1,a2)) -> "xrl   " ^ pp_arg a1 ^ ", " ^ pp_arg a2
 
+let find_comment p pc =
+  let s1 =
+    try
+      let lbl = BitVectors.WordMap.find pc p.ASM.cost_labels in
+      ", " ^ CostLabel.string_of_cost_label ~pretty:true lbl 
+    with Not_found -> "" in
+  let s2 =
+    try
+      let i = BitVectors.WordMap.find pc p.ASM.inds in
+      ", index " ^ string_of_int i 
+    with Not_found -> "" in
+  let s3 =
+    try
+      let i = BitVectors.WordMap.find pc p.ASM.incs in
+      ", inc " ^ string_of_int i 
+    with Not_found -> "" in
+  s1 ^ s2 ^ s3
+                        
+
 let print_program p =
   let mem = ASMInterpret.load_code_memory p.ASM.code in
   let f (s, pc) _ =
     let (inst, new_pc, cost) = ASMInterpret.fetch mem pc in
-    (Printf.sprintf "%s% 6X:  %- 18s ;; %d  %s\n"
+    (Printf.sprintf "%s% 6X:  %- 18s ;; %d%s\n"
        s
        (BitVectors.int_of_vect pc)
        (pp_instruction inst)
        cost
-       (if BitVectors.WordMap.mem pc p.ASM.cost_labels then
-           (BitVectors.WordMap.find pc p.ASM.cost_labels)
-        else ""),
+       (find_comment p pc),
      new_pc) in
   fst (List.fold_left f ("", BitVectors.zero `Sixteen) p.ASM.code)

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

@@ -48 +48 @@
   (* 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 the content of a hardware register to a pseudo register. Parameters

Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.ml

@@ -32 +32 @@
 
 type stack_frame = local_env
+
+type indexing = CostLabel.const_indexing
 
 (* Execution states. *)
@@ -44 +46 @@
       renv   : hdw_reg_env ;
       mem    : memory ;
+      inds   : indexing list;
       trace  : CostLabel.t list }
 
@@ -62 +65 @@
 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 =
@@ -72 +80 @@
     renv   = I8051.RegisterMap.empty ;
     mem    = Mem.empty ;
+    inds   = [] ;
     trace  = [] }
 
@@ -118 +127 @@
   let lenv = Register.Set.fold f def.ERTL.f_locals Register.Map.empty in
   let pc = entry_pc lbls_offs ptr def in
+  let st = new_ind st in
   change_lenv (change_pc st pc) lenv
 
@@ -231 +241 @@
 
 let interpret_return lbls_offs st =
+  let st = forget_ind st in
   let st = pop_st_frs st in
   let (st, pch) = pop st in
@@ -254 +265 @@
 
     | ERTL.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
+
+    | ERTL.St_ind_0 (i, lbl) ->
+      enter_loop st i;
+      next_pc st lbl
+
+    | ERTL.St_ind_inc (i, lbl) ->
+      continue_loop st i; 
       next_pc st lbl
 

Deliverables/D2.2/8051/src/ERTL/ERTLPrinter.ml

@@ -43 +43 @@
     Printf.sprintf "*** %s *** --> %s" s lbl
   | ERTL.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
+  | ERTL.St_ind_0 (i, lbl) ->
+    Printf.sprintf "index %d --> %s" i lbl
+  | ERTL.St_ind_inc (i, lbl) ->
+    Printf.sprintf "increment %d --> %s" i lbl
   | ERTL.St_get_hdw (r1, r2, lbl) ->
     Printf.sprintf "move %s, %s --> %s"

Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml

@@ -163 +163 @@
 
       | ERTL.St_cost (cost_lbl, l) ->
-        LTL.St_cost (cost_lbl, l)
+        LTL.St_cost (cost_lbl, l)
+
+      | ERTL.St_ind_0 (i, l) ->
+        LTL.St_ind_0 (i, l)
+
+      | ERTL.St_ind_inc (i, l) ->
+        LTL.St_ind_inc (i, l)
 
       | ERTL.St_get_hdw (destr, sourcehwr, l) ->

Deliverables/D2.2/8051/src/ERTL/liveness.ml

@@ -18 +18 @@
   | St_comment (_, l)
   | St_cost (_, l)
+  | St_ind_0 (_, l)
+  | St_ind_inc (_, l)
   | St_set_hdw (_, _, l)
   | St_get_hdw (_, _, l)
@@ -83 +85 @@
 end
 
-module Label_ImperativeMap = struct
-
-  type key =
-      Label.Map.key
-  
-  type 'data t =
-      'data Label.Map.t ref
-      
-  let create () =
-    ref Label.Map.empty
-
-  let clear t =
-    t := Label.Map.empty
-    
-  let add k d t =
-    t := Label.Map.add k d !t
-
-  let find k t =
-    Label.Map.find k !t
-
-  let iter f t =
-    Label.Map.iter f !t
-
-end
-
-module F = Fix.Make (Label_ImperativeMap) (L)
+module F = Fix.Make (Label.ImpMap) (L)
 
 (* These are the sets of variables defined at (written by) a statement. *)
@@ -117 +94 @@
   | St_comment _
   | St_cost _
+  | St_ind_0 _
+  | St_ind_inc _
   | St_push _
   | St_store _
@@ -169 +148 @@
   | St_comment _
   | St_cost _
+  | St_ind_0 _
+  | St_ind_inc _
   | St_framesize _
   | St_pop _
@@ -227 +208 @@
   | St_comment _
   | St_cost _
+  | St_ind_0 _
+  | St_ind_inc _
   | St_newframe _
   | St_delframe _

Deliverables/D2.2/8051/src/ERTL/uses.ml

@@ -20 +20 @@
   | St_comment _
   | St_cost _
+  | St_ind_0 _
+  | St_ind_inc _
   | St_hdw_to_hdw _
   | St_newframe _

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

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

Deliverables/D2.2/8051/src/LIN/LINInterpret.ml

@@ -21 +21 @@
 
 type hdw_reg_env = Val.t I8051.RegisterMap.t
+
+
+type indexing = CostLabel.const_indexing
 
 (* Execution states. *)
@@ -31 +34 @@
       renv   : hdw_reg_env ;
       mem    : memory ;
+      inds   : indexing list ;
       trace  : CostLabel.t list }
 
@@ -44 +48 @@
 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 +61 @@
     renv   = I8051.RegisterMap.empty ;
     mem    = Mem.empty ;
+    inds   = [] ;
     trace  = [] }
 
@@ -72 +82 @@
 
 let init_fun_call st ptr =
+  let st = new_ind st in
   change_pc st (Val.change_address_offset ptr Val.Offset.zero)
 
@@ -176 +187 @@
 
 let interpret_return st =
+  let st = forget_ind st in
   let (st, pc) = return_pc st in
   change_pc st pc
@@ -195 +207 @@
 
     | LIN.St_cost cost_lbl ->
+      let cost_lbl = ev_label st cost_lbl in
       let st = add_trace st cost_lbl in
+      next_pc st
+
+    | LIN.St_ind_0 i ->
+      enter_loop st i;
+      next_pc st
+
+    | LIN.St_ind_inc i ->
+      continue_loop st i;
       next_pc st
 

Deliverables/D2.2/8051/src/LIN/LINPrinter.ml

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

Deliverables/D2.2/8051/src/LIN/LINToASM.ml

@@ -25 +25 @@
   | LIN.St_goto lbl
   | LIN.St_label lbl
-  | LIN.St_cost lbl
   | LIN.St_condacc lbl -> Label.Set.singleton lbl
+    (* taking the atom as a fresh prefix will be generated *)
+  | LIN.St_cost lbl -> Label.Set.singleton (lbl.CostLabel.name)
   | _ -> Label.Set.empty
 
@@ -69 +70 @@
     (* TODO: hack! Need to make the difference between cost labels and regular
        labels. *)
-    [`Cost lbl ; `NOP]
+    [`Cost lbl ; `NOP ]
+  | LIN.St_ind_0 i -> [`Index i ; `NOP (* TODO: hack! *)]
+  | LIN.St_ind_inc i -> [`Inc i ; `NOP (* TODO: hack! *)]
   | LIN.St_int (r, i) ->
     [`MOV (`U3 (I8051.reg_addr r, data_of_int i))]

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)

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

@@ -16 +16 @@
   (* 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 the address of a symbol to registers. Parameters are the destination

Deliverables/D2.2/8051/src/RTL/RTLInterpret.ml

@@ -34 +34 @@
       carry    : Val.t }
 
+type indexing = CostLabel.const_indexing
+
 (* Execution states. There are three possible states :
    - The constructor [State] represents a state when executing a function
@@ -41 +43 @@
 type state =
   | State of stack_frame list * RTL.graph * Label.t * Val.address (* sp *) *
-             local_env * Val.t (* carry *) * memory * CostLabel.t list
+             local_env * Val.t (* carry *) * memory * indexing list *
+                                                 CostLabel.t list
   | CallState of stack_frame list * RTL.function_def *
-                 Val.t list (* args *) * memory * CostLabel.t list
+              Val.t list (* args *) * memory * indexing list * CostLabel.t list
   | ReturnState of stack_frame list * Val.t list (* return values *) *
-                   memory * CostLabel.t list
+                   memory * indexing list * CostLabel.t list
 
 let string_of_local_env lenv =
@@ -59 +62 @@
 
 let print_state = function
-  | State (_, _, lbl, sp, lenv, carry, mem, _) ->
-    Printf.printf "Stack pointer: %s\n\nCarry: %s\n\nLocal environment:\n%s\n\nMemory:%s\nRegular state: %s\n\n%!"
+  | State (_, _, lbl, sp, lenv, carry, mem, ind, _) ->
+    Printf.printf "Stack pointer: %s\n\nCarry: %s\n\nLocal environment:\n%s\n\nMemory:%s\nIndexing:"
       (Val.string_of_address sp)
       (Val.to_string carry)
       (string_of_local_env lenv)
-      (Mem.to_string mem)
+      (Mem.to_string mem);
+    let i = CostLabel.curr_const_ind ind in
+    CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) i;
+    Printf.printf "Regular state: %s\n\n%!"
       lbl
-  | CallState (_, _, args, mem, _) ->
+  | CallState (_, _, args, mem, _, _) ->
     Printf.printf "Memory:%s\nCall state: %s\n\n%!"
       (Mem.to_string mem)
       (string_of_args args)
-  | ReturnState (_, vs, mem, _) ->
+  | ReturnState (_, vs, mem, _, _) ->
     Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
       (Mem.to_string mem)
@@ -96 +102 @@
 (* Assign a value to some destinations registers. *)
 
-let assign_state sfrs graph lbl sp lenv carry mem trace destrs vs =
+let assign_state sfrs graph lbl sp lenv carry mem inds trace destrs vs =
   let lenv = adds destrs vs lenv in
-  State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
+  State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
 
 (* Branch on a value. *)
 
-let branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v =
+let branch_state sfrs graph lbl_true lbl_false sp lenv carry mem inds trace v =
   let next_lbl =
     if Val.is_true v then lbl_true
@@ -108 +114 @@
       if Val.is_false v then lbl_false
       else error "Undefined conditional value." in
-  State (sfrs, graph, next_lbl, sp, lenv, carry, mem, trace)
+  State (sfrs, graph, next_lbl, sp, lenv, carry, mem, inds, trace)
+
+let curr_ind = CostLabel.curr_const_ind
+
+let forget_ind = CostLabel.forget_const_ind
+
+let new_ind = CostLabel.new_const_ind
 
 
@@ -120 +132 @@
     (carry : Val.t)
     (mem   : memory)
+    (inds  : indexing list)
     (stmt  : RTL.statement)
     (trace : CostLabel.t list) :
@@ -125 +138 @@
 
       | RTL.St_skip lbl ->
-        State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
+        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
 
       | RTL.St_cost (cost_lbl, lbl) ->
-        State (sfrs, graph, lbl, sp, lenv, carry, mem, cost_lbl :: trace)
+        let cost_lbl = CostLabel.ev_indexing (curr_ind inds) cost_lbl in
+        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, cost_lbl :: trace)
+
+      | RTL.St_ind_0 (i, lbl) ->
+        CostLabel.enter_loop inds i; 
+        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
+
+      | RTL.St_ind_inc (i, lbl) ->
+        CostLabel.continue_loop inds i; 
+        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
 
       | RTL.St_addr (r1, r2, x, lbl) ->
-        assign_state sfrs graph lbl sp lenv carry mem trace [r1 ; r2]
+        assign_state sfrs graph lbl sp lenv carry mem inds trace [r1 ; r2]
           (Mem.find_global mem x)
 
       | RTL.St_stackaddr (r1, r2, lbl) ->
-        assign_state sfrs graph lbl sp lenv carry mem trace [r1 ; r2] sp
+        assign_state sfrs graph lbl sp lenv carry mem inds trace [r1 ; r2] sp
 
       | RTL.St_int (r, i, lbl) ->
-        assign_state sfrs graph lbl sp lenv carry mem trace [r] [Val.of_int i]
+        assign_state sfrs graph lbl sp lenv carry mem inds trace [r] [Val.of_int i]
 
       | RTL.St_move (destr, srcr, lbl) ->
-        assign_state sfrs graph lbl sp lenv carry mem trace [destr]
+        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr]
           [get_local_value lenv srcr]
 
@@ -149 +171 @@
             (get_local_value lenv srcr1)
             (get_local_value lenv srcr2) in
-        assign_state sfrs graph lbl sp lenv carry mem trace
+        assign_state sfrs graph lbl sp lenv carry mem inds trace
           [destr1 ; destr2] [v1 ; v2]
 
       | RTL.St_op1 (op1, destr, srcr, lbl) ->
         let v = Eval.op1 op1 (get_local_value lenv srcr) in
-        assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
+        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v]
 
       | RTL.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
@@ -161 +183 @@
             (get_local_value lenv srcr1)
             (get_local_value lenv srcr2) in
-        assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
+        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v]
 
       | RTL.St_clear_carry lbl ->
-        State (sfrs, graph, lbl, sp, lenv, Val.zero, mem, trace)
+        State (sfrs, graph, lbl, sp, lenv, Val.zero, mem, inds, trace)
 
       | RTL.St_set_carry lbl ->
-        State (sfrs, graph, lbl, sp, lenv, Val.of_int 1, mem, trace)
+        State (sfrs, graph, lbl, sp, lenv, Val.of_int 1, mem, inds, trace)
 
       | RTL.St_load (destr, addr1, addr2, lbl) ->
         let addr = get_local_addr lenv addr1 addr2 in
         let v = Mem.load mem chunk addr in
-        assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
+        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v]
 
       | RTL.St_store (addr1, addr2, srcr, lbl) ->
         let addr = get_local_addr lenv addr1 addr2 in
         let mem = Mem.store mem chunk addr (get_local_value lenv srcr) in
-        State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
+        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
 
       | RTL.St_call_id (f, args, ret_regs, lbl) ->
@@ -186 +208 @@
             sp = sp ; lenv = lenv ; carry = carry }
         in
-        CallState (sf :: sfrs, f_def, args, mem, trace)
+        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
 
       | RTL.St_call_ptr (f1, f2, args, ret_regs, lbl) ->
@@ -194 +216 @@
         let sf = { ret_regs = ret_regs ; graph = graph ; pc = lbl ;
                    sp = sp ; lenv = lenv ; carry = carry } in
-        CallState (sf :: sfrs, f_def, args, mem, trace)
+        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
 
       | RTL.St_tailcall_id (f, args) ->
@@ -200 +222 @@
         let args = get_arg_values lenv args in
         let mem = Mem.free mem sp in
-        CallState (sfrs, f_def, args, mem, trace)
+        CallState (sfrs, f_def, args, mem, inds, trace)
 
       | RTL.St_tailcall_ptr (f1, f2, args) ->
@@ -207 +229 @@
         let args = get_arg_values lenv args in
         let mem = Mem.free mem sp in
-        CallState (sfrs, f_def, args, mem, trace)
+        CallState (sfrs, f_def, args, mem, inds, trace)
 
       | RTL.St_cond (srcr, lbl_true, lbl_false) ->
         let v = get_local_value lenv srcr in
-        branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v
+        branch_state sfrs graph lbl_true lbl_false sp lenv carry mem inds trace v
 
       | RTL.St_return rl ->
         let vl = List.map (get_local_value lenv) rl in
         let mem = Mem.free mem sp in
-        ReturnState (sfrs, vl, mem, trace)
+        ReturnState (sfrs, vl, mem, inds, trace)
 
 
@@ -240 +262 @@
     (args  : Val.t list)
     (mem   : memory)
+    (inds  : indexing list)
     (trace : CostLabel.t list) :
     state =
   match f_def with
     | RTL.F_int def ->
+      let inds = new_ind inds in
       let (mem', sp) = Mem.alloc mem def.RTL.f_stacksize in
       State (sfrs, def.RTL.f_graph, def.RTL.f_entry, sp,
              init_locals def.RTL.f_locals def.RTL.f_params args,
-             Val.undef, mem', trace)
+             Val.undef, mem', inds, trace)
     | RTL.F_ext def ->
       let (mem', vs) = interpret_external mem def.AST.ef_tag args in
-      ReturnState (sfrs, vs, mem', trace)
+      ReturnState (sfrs, vs, mem', inds, trace)
 
 let state_after_return
@@ -257 +281 @@
     (ret_vals : Val.t list)
     (mem      : memory)
+    (inds     : indexing list)
     (trace    : CostLabel.t list) :
     state =
   let f i lenv r = Register.Map.add r (List.nth ret_vals i) lenv in
   let lenv = MiscPottier.foldi f sf.lenv sf.ret_regs in
-  State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, trace)
+  let inds = forget_ind inds in
+  State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, inds, trace)
 
 
 let small_step (st : state) : state = match st with
-  | State (sfrs, graph, pc, sp, lenv, carry, mem, trace) ->
+  | State (sfrs, graph, pc, sp, lenv, carry, mem, inds, trace) ->
     let stmt = Label.Map.find pc graph in
-    interpret_statement sfrs graph sp lenv carry mem stmt trace
-  | CallState (sfrs, f_def, args, mem, trace) ->
-    state_after_call sfrs f_def args mem trace
-  | ReturnState ([], ret_vals, mem, trace) ->
+    interpret_statement sfrs graph sp lenv carry mem inds stmt trace
+  | CallState (sfrs, f_def, args, mem, inds, trace) ->
+    state_after_call sfrs f_def args mem inds trace
+  | ReturnState ([], ret_vals, mem, inds, trace) ->
     assert false (* End of execution; handled in iter_small_step. *)
-  | ReturnState (sf :: sfrs, ret_vals, mem, trace) ->
-    state_after_return sf sfrs ret_vals mem trace
+  | ReturnState (sf :: sfrs, ret_vals, mem, inds, trace) ->
+    state_after_return sf sfrs ret_vals mem inds trace
 
 
@@ -292 +318 @@
   if debug then print_state st ;
   match small_step st with
-    | ReturnState ([], vs, mem, trace) ->
+    | ReturnState ([], vs, mem, _, trace) ->
       print_and_return_result (compute_result vs, List.rev trace)
     | st' -> iter_small_step debug st'
@@ -321 +347 @@
       let mem = init_mem p in
       let main_def = find_function mem main in
-      let st = CallState ([], main_def, [], mem, []) in
+      let st = CallState ([], main_def, [], mem, [], []) in
       iter_small_step debug st

Deliverables/D2.2/8051/src/RTL/RTLPrinter.ml

@@ -43 +43 @@
   | RTL.St_skip lbl -> "--> " ^ lbl
   | RTL.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
+  | RTL.St_ind_0 (i, lbl) ->
+    Printf.sprintf "index %d --> %s" i lbl
+  | RTL.St_ind_inc (i, lbl) ->
+    Printf.sprintf "increment %d --> %s" i lbl
   | RTL.St_addr (dstr1, dstr2, id, lbl) ->
     Printf.sprintf "imm (%s, %s), %s --> %s"

Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml

@@ -22 +22 @@
   | ERTL.St_comment (s, _) -> ERTL.St_comment (s, lbl)
   | ERTL.St_cost (cost_lbl, _) -> ERTL.St_cost (cost_lbl, lbl)
+  | ERTL.St_ind_0 (i, _) -> ERTL.St_ind_0 (i, lbl)
+  | ERTL.St_ind_inc (i, _) -> ERTL.St_ind_inc (i, lbl)
   | ERTL.St_get_hdw (r1, r2, _) -> ERTL.St_get_hdw (r1, r2, lbl)
   | ERTL.St_set_hdw (r1, r2, _) -> ERTL.St_set_hdw (r1, r2, lbl)
@@ -319 +321 @@
     add_graph lbl (ERTL.St_cost (cost_lbl, lbl')) def
 
+  | RTL.St_ind_0 (i, lbl') ->
+    add_graph lbl (ERTL.St_ind_0 (i, lbl')) def
+
+  | RTL.St_ind_inc (i, lbl') ->
+    add_graph lbl (ERTL.St_ind_inc (i, lbl')) def
+
   | RTL.St_addr (r1, r2, x, lbl') ->
     adds_graph
@@ -432 +440 @@
       let graph = Label.Map.add lbl (ERTL.St_skip next_lbl) def.ERTL.f_graph in
       (Some cost_label, { def with ERTL.f_graph = graph })
+    | ERTL.St_ind_0 (_, lbl) | ERTL.St_ind_inc (_, lbl)
     | ERTL.St_skip lbl | ERTL.St_comment (_, lbl) | ERTL.St_get_hdw (_, _, lbl)
     | ERTL.St_set_hdw (_, _, lbl) | ERTL.St_hdw_to_hdw (_, _, lbl)

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

@@ -11 +11 @@
 
 
+type argument =
+  | Reg of Register.t
+  | Imm of AST.cst*AST.sig_type
+
 (* A function in RTLabs is a mapping from labels to
    statements. Statements explicitely mention their successors. *)
@@ -22 +26 @@
   | 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 a constant to registers. Parameters are the destination register,
      the constant and the label of the next statement. *)
@@ -32 +42 @@
 
   (* Application of a binary operation. Parameters are the operation, the
-     destination register, the two argument registers and the label of the next
+     destination register, the two arguments and the label of the next
      statement. *)
-  | St_op2 of AST.op2 * Register.t * Register.t * Register.t * Label.t
+  | St_op2 of AST.op2 * Register.t * argument * argument * Label.t
 
   (* Memory load. Parameters are the size in bytes of what to load, the
      register containing the address, the destination register and the label
      of the next statement. *)
-  | St_load of AST.quantity * Register.t * Register.t * Label.t
+  | St_load of AST.quantity * argument * Register.t * Label.t
 
   (* Memory store. Parameters are the size in bytes of what to store, the
      register containing the address, the source register and the label of the
      next statement. *)
-  | St_store of AST.quantity * Register.t * Register.t * Label.t
+  | St_store of AST.quantity * argument * argument * Label.t
 
   (* Call to a function given its name. Parameters are the name of the

Deliverables/D2.2/8051/src/RTLabs/RTLabsInterpret.ml

@@ -33 +33 @@
       lenv     : local_env }
 
+type indexing = CostLabel.const_indexing
+
 (* Execution states. There are three possible states :
    - The constructor [State] represents a state when executing a function
@@ -40 +42 @@
 type state =
   | State of stack_frame list * RTLabs.graph * Val.address (* stack pointer *) *
-             Label.t * local_env * memory * CostLabel.t list
+       Label.t * local_env * memory * indexing list * CostLabel.t list
   | CallState of stack_frame list * RTLabs.function_def *
-                 Val.t list (* args *) * memory * CostLabel.t list
+              Val.t list (* args *) * memory * indexing list * CostLabel.t list
   | ReturnState of stack_frame list * Val.t (* return value *) *
-                   memory * CostLabel.t list
+        memory * indexing list * CostLabel.t list
 
 let string_of_local_env lenv =
@@ -57 +59 @@
   List.fold_left f "" args
 
-let print_state = function
-  | State (_, _, sp, lbl, lenv, mem, _) ->
-    Printf.printf "Stack pointer: %s\n\nLocal environment:\n%s\n\nMemory:%s\nRegular state: %s\n\n%!"
+let print_state state = match state with
+  | State (_, _, sp, lbl, lenv, mem, inds, _) ->
+    Printf.printf "Stack pointer: %s\n\nLocal environment:\n%s\n\nMemory:%s\nIndexing:"
       (Val.string_of_address sp)
       (string_of_local_env lenv)
-      (Mem.to_string mem)
+      (Mem.to_string mem);
+    let i = CostLabel.curr_const_ind inds in
+    CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) i;
+    Printf.printf "Regular state: %s\n\n%!"
       lbl
-  | CallState (_, _, args, mem, _) ->
+  | CallState (_, _, args, mem, _, _) ->
     Printf.printf "Memory:%s\nCall state: %s\n\n%!"
       (Mem.to_string mem)
       (string_of_args args)
-  | ReturnState (_, v, mem, _) ->
+  | ReturnState (_, v, mem, _, _) ->
     Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
       (Mem.to_string mem)
@@ -106 +111 @@
 (* Assign a value to some destinations registers. *)
 
-let assign_state sfrs graph sp lbl lenv mem trace destr v =
+let assign_state sfrs graph sp lbl lenv mem inds trace destr v =
   let lenv = update_local destr v lenv in
-  State (sfrs, graph, sp, lbl, lenv, mem, trace)
+  State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
 
 (* Branch on a value. *)
 
-let branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v =
+let branch_state sfrs graph sp lbl_true lbl_false lenv mem inds trace v =
   let next_lbl =
     if Val.is_true v then lbl_true
@@ -118 +123 @@
       if Val.is_false v then lbl_false
       else error "Undefined conditional value." in
-  State (sfrs, graph, sp, next_lbl, lenv, mem, trace)
-
+  State (sfrs, graph, sp, next_lbl, lenv, mem, inds, trace)
+
+let curr_ind = CostLabel.curr_const_ind
+
+let forget_ind = CostLabel.forget_const_ind
+
+let new_ind = CostLabel.new_const_ind
+
+let eval_arg lenv mem sp = function
+  | RTLabs.Reg r -> get_value lenv r
+  | RTLabs.Imm (c, t) -> Eval.cst mem sp t c
+
+let get_type_arg lenv = function
+  | RTLabs.Reg r -> get_type lenv r
+  | RTLabs.Imm (_, typ) -> typ
 
 (* Interpret statements. *)
@@ -130 +148 @@
     (mem   : memory)
     (stmt  : RTLabs.statement)
+    (inds  : indexing list)
     (trace : CostLabel.t list) :
     state = match stmt with
 
       | RTLabs.St_skip lbl ->
-        State (sfrs, graph, sp, lbl, lenv, mem, trace)
+        State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
 
       | RTLabs.St_cost (cost_lbl, lbl) ->
-        State (sfrs, graph, sp, lbl, lenv, mem, cost_lbl :: trace)
+        let cost_lbl =
+          CostLabel.ev_indexing (curr_ind inds) cost_lbl in
+        State (sfrs, graph, sp, lbl, lenv,
+               mem, inds, cost_lbl :: trace)
+
+      | RTLabs.St_ind_0 (i, lbl) ->
+        CostLabel.enter_loop inds i; 
+        State (sfrs, graph, sp, lbl, lenv,
+               mem, inds, trace)
+
+      | RTLabs.St_ind_inc (i, lbl) ->
+        CostLabel.continue_loop inds i; 
+        State (sfrs, graph, sp, lbl, lenv,
+               mem, inds, trace)
 
       | RTLabs.St_cst (destr, cst, lbl) ->
         let v = Eval.cst mem sp (get_type lenv destr) cst in
-        assign_state sfrs graph sp lbl lenv mem trace destr v
+        assign_state sfrs graph sp lbl lenv mem inds trace destr v
 
       | RTLabs.St_op1 (op1, destr, srcr, lbl) ->
@@ -147 +179 @@
           Eval.op1 (get_type lenv destr) (get_type lenv srcr) op1
             (get_value lenv srcr) in
-        assign_state sfrs graph sp lbl lenv mem trace destr v
+        assign_state sfrs graph sp lbl lenv mem inds trace destr v
 
       | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
         let v =
           Eval.op2
-            (get_type lenv destr) (get_type lenv srcr1) (get_type lenv srcr2)
+            (get_type lenv destr)
+            (get_type_arg lenv srcr1)
+            (get_type_arg lenv srcr2)
             op2
-            (get_value lenv srcr1)
-            (get_value lenv srcr2) in
-        assign_state sfrs graph sp lbl lenv mem trace destr v
+            (eval_arg lenv mem sp srcr1)
+            (eval_arg lenv mem sp srcr2) in
+        assign_state sfrs graph sp lbl lenv mem inds trace destr v
 
       | RTLabs.St_load (q, addr, destr, lbl) ->
-        let addr = address_of_value (get_value lenv addr) in
+        let addr = address_of_value (eval_arg lenv mem sp addr) in
         let v = Mem.loadq mem q addr in
-        assign_state sfrs graph sp lbl lenv mem trace destr v
+        assign_state sfrs graph sp lbl lenv mem inds trace destr v
 
       | RTLabs.St_store (q, addr, srcr, lbl) ->
-        let addr = address_of_value (get_value lenv addr) in
-        let v = get_value lenv srcr in
+        let addr = address_of_value (eval_arg lenv mem sp addr) in
+        let v = eval_arg lenv mem sp srcr in
         let mem = Mem.storeq mem q addr v in
-        State (sfrs, graph, sp, lbl, lenv, mem, trace)
+        State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
 
       | RTLabs.St_call_id (f, args, destr, sg, lbl) ->
@@ -176 +210 @@
           { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
         in
-        CallState (sf :: sfrs, f_def, args, mem, trace)
+        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
 
       | RTLabs.St_call_ptr (r, args, destr, sg, lbl) ->
@@ -186 +220 @@
           { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
         in
-        CallState (sf :: sfrs, f_def, args, mem, trace)
+        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
 
       | RTLabs.St_tailcall_id (f, args, sg) ->
@@ -193 +227 @@
         (* No need to save the stack frame. But free the stack. *)
         let mem = Mem.free mem sp in
-        CallState (sfrs, f_def, args, mem, trace)
+        CallState (sfrs, f_def, args, mem, inds, trace)
 
       | RTLabs.St_tailcall_ptr (r, args, sg) ->
@@ -201 +235 @@
         (* No need to save the stack frame. But free the stack. *)
         let mem = Mem.free mem sp in
-        CallState (sfrs, f_def, args, mem, trace)
+        CallState (sfrs, f_def, args, mem, inds, trace)
 
       | RTLabs.St_cond (srcr, lbl_true, lbl_false) ->
         let v = get_value lenv srcr in
-        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
+        branch_state sfrs graph sp lbl_true lbl_false lenv mem inds trace v
 
 (*
@@ -242 +276 @@
       | RTLabs.St_return None ->
         let mem = Mem.free mem sp in
-        ReturnState (sfrs, Val.undef, mem, trace)
+        ReturnState (sfrs, Val.undef, mem, inds, trace)
 
       | RTLabs.St_return (Some r) ->
         let v = get_value lenv r in
         let mem = Mem.free mem sp in
-        ReturnState (sfrs, v, mem, trace)
+        ReturnState (sfrs, v, mem, inds, trace)
 
 
@@ -274 +308 @@
     (args  : Val.t list)
     (mem   : memory)
+    (inds  : indexing list)
     (trace : CostLabel.t list) :
     state =
@@ -281 +316 @@
         Mem.alloc mem (concrete_stacksize def.RTLabs.f_stacksize) in
       let lenv = init_locals def.RTLabs.f_locals def.RTLabs.f_params args in
-      State (sfrs, def.RTLabs.f_graph, sp, def.RTLabs.f_entry, lenv, mem',
-             trace)
+      (* allocate new constant indexing *)
+      let graph = def.RTLabs.f_graph in
+      let inds = new_ind inds in
+      State (sfrs, graph, sp, def.RTLabs.f_entry, lenv, mem', inds, trace)
     | RTLabs.F_ext def ->
       let (mem', v) = interpret_external mem def.AST.ef_tag args in
-      ReturnState (sfrs, v, mem', trace)
+      ReturnState (sfrs, v, mem', inds, trace)
 
 
@@ -293 +330 @@
     (ret_val : Val.t)
     (mem     : memory)
+    (inds    : indexing list)
     (trace   : CostLabel.t list) :
     state =
@@ -298 +336 @@
     | None -> sf.lenv
     | Some ret_reg -> update_local ret_reg ret_val sf.lenv in
-  State (sfrs, sf.graph, sf.sp, sf.pc, lenv, mem, trace)
+      (* erase current indexing and revert to previous one *)
+      let inds = forget_ind inds in
+      State (sfrs, sf.graph, sf.sp, sf.pc, lenv,
+             mem, inds, trace)
 
 
 let small_step (st : state) : state = match st with
-  | State (sfrs, graph, sp, pc, lenv, mem, trace) ->
+  | State (sfrs, graph, sp, pc, lenv, mem, inds, trace) ->
     let stmt = Label.Map.find pc graph in
-    interpret_statement sfrs graph sp lenv mem stmt trace
-  | CallState (sfrs, f_def, args, mem, trace) ->
-    state_after_call sfrs f_def args mem trace
-  | ReturnState ([], ret_val, mem, trace) ->
+    interpret_statement sfrs graph sp lenv mem stmt inds trace
+  | CallState (sfrs, f_def, args, mem, inds, trace) ->
+    state_after_call sfrs f_def args mem inds trace
+  | ReturnState ([], ret_val, mem, inds, trace) ->
     assert false (* End of execution; handled in iter_small_step. *)
-  | ReturnState (sf :: sfrs, ret_val, mem, trace) ->
-    state_after_return sf sfrs ret_val mem trace
+  | ReturnState (sf :: sfrs, ret_val, mem, inds, trace) ->
+    state_after_return sf sfrs ret_val mem inds trace
 
 
@@ -324 +365 @@
   if debug then print_state st ;
   match small_step st with
-    | ReturnState ([], v, mem, trace) ->
+    | ReturnState ([], v, mem, inds, trace) ->
       print_and_return_result (compute_result v, List.rev trace)
     | st' -> iter_small_step debug st'
@@ -352 +393 @@
       let mem = init_mem p in
       let main_def = find_function mem main in
-      let st = CallState ([], main_def, [], mem, []) in
+      let st = CallState ([], main_def, [], mem, [], []) in
       iter_small_step debug st

Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.ml

@@ -45 +45 @@
 
 let print_cmp = function
-  | AST.Cmp_eq -> "eq"
-  | AST.Cmp_ne -> "ne"
-  | AST.Cmp_gt -> "gt"
-  | AST.Cmp_ge -> "ge"
-  | AST.Cmp_lt -> "lt"
-  | AST.Cmp_le -> "le"
+  | AST.Cmp_eq -> "="
+  | AST.Cmp_ne -> "!="
+  | AST.Cmp_gt -> ">"
+  | AST.Cmp_ge -> ">="
+  | AST.Cmp_lt -> "<"
+  | AST.Cmp_le -> "<="
 
 let rec print_size = function
@@ -83 +83 @@
   Printf.sprintf "%d%s" size (string_of_signedness sign)
 
-let print_op1 = function
+let print_op1 op r = Printf.sprintf "%s %s"
+  (match op with
   | AST.Op_cast (int_type, dest_size) ->
     Printf.sprintf "int%sto%d" (string_of_int_type int_type) dest_size
-  | AST.Op_negint -> "negint"
-  | AST.Op_notbool -> "notbool"
-  | AST.Op_notint -> "notint"
-  | AST.Op_id -> "id"
+  | AST.Op_negint -> "-"
+  | AST.Op_notbool -> "!"
+  | AST.Op_notint -> "!i"
+  | AST.Op_id -> ""
   | AST.Op_ptrofint -> "ptrofint"
-  | AST.Op_intofptr -> "intofptr"
-
-let print_op2 = function
-  | AST.Op_add -> "add"
-  | AST.Op_sub -> "sub"
-  | AST.Op_mul -> "mul"
-  | AST.Op_div -> "div"
+  | AST.Op_intofptr -> "intofptr")
+        (print_reg r)
+
+let print_arg = function
+  | RTLabs.Reg r -> print_reg r
+  | RTLabs.Imm (c, t) ->
+    Printf.sprintf "(%s)%s" (Primitive.print_type t) (print_cst c)
+
+let print_op2 op r s = Printf.sprintf "%s %s %s"
+  (print_arg r)
+  (match op with
+  | AST.Op_add -> "+"
+  | AST.Op_sub -> "-"
+  | AST.Op_mul -> "*"
+  | AST.Op_div -> "/"
   | AST.Op_divu -> "/u"
   | AST.Op_mod -> "mod"
@@ -104 +113 @@
   | AST.Op_or -> "or"
   | AST.Op_xor -> "xor"
-  | AST.Op_shl -> "shl"
-  | AST.Op_shr -> "shr"
-  | AST.Op_shru -> "shru"
+  | AST.Op_shl -> "<<"
+  | AST.Op_shr -> ">>"
+  | AST.Op_shru -> ">>u"
   | AST.Op_cmp cmp -> print_cmp cmp
-  | AST.Op_addp -> "addp"
-  | AST.Op_subp -> "subp"
-  | AST.Op_subpp -> "subpp"
+  | AST.Op_addp -> "+p"
+  | AST.Op_subp -> "-p"
+  | AST.Op_subpp -> "-pp"
   | AST.Op_cmpp cmp -> (print_cmp cmp) ^ "p"
-  | AST.Op_cmpu cmp -> (print_cmp cmp) ^ "u"
+  | AST.Op_cmpu cmp -> (print_cmp cmp) ^ "u")
+  (print_arg s)
 
 
@@ -136 +146 @@
   | RTLabs.St_skip lbl -> "--> " ^ lbl
   | RTLabs.St_cost (cost_lbl, lbl) ->
-      Printf.sprintf "emit %s --> %s" cost_lbl lbl
+    let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
+    Printf.sprintf "emit %s --> %s" cost_lbl lbl
+  | RTLabs.St_ind_0 (i, lbl) ->
+    Printf.sprintf "index %d --> %s" i lbl
+  | RTLabs.St_ind_inc (i, lbl) ->
+    Printf.sprintf "increment %d --> %s" i lbl
   | RTLabs.St_cst (destr, cst, lbl) ->
-      Printf.sprintf "imm %s, %s --> %s"
+      Printf.sprintf "%s := %s --> %s"
         (print_reg destr)
         (print_cst cst)
         lbl
   | RTLabs.St_op1 (op1, destr, srcr, lbl) ->
-      Printf.sprintf "%s %s, %s --> %s"
-        (print_op1 op1)
+      Printf.sprintf "%s := %s --> %s"
         (print_reg destr)
-        (print_reg srcr)
+  (print_op1 op1 srcr)
         lbl
   | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
-      Printf.sprintf "%s %s, %s, %s --> %s"
-        (print_op2 op2)
+      Printf.sprintf "%s := %s --> %s"
         (print_reg destr)
-        (print_reg srcr1)
-        (print_reg srcr2)
+  (print_op2 op2 srcr1 srcr2)
         lbl
   | RTLabs.St_load (q, addr, destr, lbl) ->
-      Printf.sprintf "load %s, %s, %s --> %s"
+      Printf.sprintf "%s := *(%s) %s --> %s"
+        (print_reg destr)
         (Memory.string_of_quantity q)
-        (print_reg addr)
-        (print_reg destr)
+        (print_arg addr)
         lbl
   | RTLabs.St_store (q, addr, srcr, lbl) ->
-      Printf.sprintf "store %s, %s, %s --> %s"
-        (Memory.string_of_quantity q)
-        (print_reg addr)
-        (print_reg srcr)
-        lbl
-  | RTLabs.St_call_id (f, args, res, sg, lbl) ->
-      Printf.sprintf "call \"%s\", %s, %s: %s --> %s"
+      Printf.sprintf "*(%s)%s := %s --> %s"
+        (Memory.string_of_quantity q)
+        (print_arg addr)
+        (print_arg srcr)
+        lbl
+  | RTLabs.St_call_id (f, args, Some r, sg, lbl) ->
+      Printf.sprintf "%s := \"%s\"(%s) : %s --> %s"
+        (print_reg r)
         f
         (print_args args)
-        (print_oreg res)
-        (Primitive.print_sig sg)
-        lbl
-  | RTLabs.St_call_ptr (f, args, res, sg, lbl) ->
-      Printf.sprintf "call_ptr %s, %s, %s: %s --> %s"
+        (Primitive.print_sig sg)
+        lbl
+  | RTLabs.St_call_id (f, args, None, sg, lbl) ->
+      Printf.sprintf "\"%s\"(%s) : %s --> %s"
+        f
+        (print_args args)
+        (Primitive.print_sig sg)
+        lbl
+  | RTLabs.St_call_ptr (f, args, Some r, sg, lbl) ->
+      Printf.sprintf "%s := *%s (%s) : %s --> %s"
+        (print_reg r)
         (print_reg f)
         (print_args args)
-        (print_oreg res)
+        (Primitive.print_sig sg)
+        lbl
+  | RTLabs.St_call_ptr (f, args, None, sg, lbl) ->
+      Printf.sprintf "*%s (%s) : %s --> %s"
+        (print_reg f)
+        (print_args args)
         (Primitive.print_sig sg)
         lbl
   | RTLabs.St_tailcall_id (f, args, sg) ->
-      Printf.sprintf "tailcall \"%s\", %s: %s"
+      Printf.sprintf "tailcall \"%s\" (%s) : %s"
         f
         (print_args args)
         (Primitive.print_sig sg)
   | RTLabs.St_tailcall_ptr (f, args, sg) ->
-      Printf.sprintf "tailcall_ptr \"%s\", %s: %s"
+      Printf.sprintf "tailcall *%s (%s) : %s"
         (print_reg f)
         (print_args args)
@@ -225 +249 @@
 
 
-let print_graph n c =
+let print_graph n c entry =
   let f lbl stmt s =
     Printf.sprintf "%s%s: %s\n%s"
@@ -232 +256 @@
       (print_statement stmt)
       s in
-  Label.Map.fold f c ""
-
-
+  let f' lbl stmt (reach, s) =
+    (Label.Set.add lbl reach, f lbl stmt s) in
+  let (reachable, str) =
+    RTLabsUtilities.dfs_fold f' c entry (Label.Set.empty, "") in
+  let filter lbl _ = not (Label.Set.mem lbl reachable) in
+  let c_rest = Label.Map.filter filter c in
+  if Label.Map.is_empty c_rest then str else
+    let str' = Label.Map.fold f c_rest "" in
+    str ^ "DEAD NODES:\n" ^ str'
+        
 let print_internal_decl n f def =
 
@@ -252 +283 @@
     (n_spaces (n+2))
     def.RTLabs.f_exit
-    (print_graph (n+2) def.RTLabs.f_graph)
+    (print_graph (n+2) def.RTLabs.f_graph def.RTLabs.f_entry)
 
 

Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.mli

@@ -4 +4 @@
 val print_statement : RTLabs.statement -> string
 
+val print_cst : AST.cst -> string
+
+val print_op1 : AST.op1 -> Register.t -> string
+
+val print_op2 : AST.op2 -> RTLabs.argument -> RTLabs.argument -> string
+
 val print_program : RTLabs.program -> string

Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml

@@ -93 +93 @@
   | RTL.St_skip _ -> RTL.St_skip lbl
   | RTL.St_cost (cost_lbl, _) -> RTL.St_cost (cost_lbl, lbl)
+  | RTL.St_ind_0 (i, _) -> RTL.St_ind_0 (i, lbl)
+  | RTL.St_ind_inc (i, _) -> RTL.St_ind_inc (i, lbl)
   | RTL.St_addr (r1, r2, id, _) -> RTL.St_addr (r1, r2, id, lbl)
   | RTL.St_stackaddr (r1, r2, _) -> RTL.St_stackaddr (r1, r2, lbl)
@@ -685 +687 @@
     add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def
 
+  | RTLabs.St_ind_0 (i, lbl') ->
+    add_graph lbl (RTL.St_ind_0 (i, lbl')) def
+
+  | RTLabs.St_ind_inc (i, lbl') ->
+    add_graph lbl (RTL.St_ind_inc (i, lbl')) def
+
   | RTLabs.St_cst (destr, cst, lbl') ->
     translate_cst cst (find_local_env destr lenv) lbl lbl' def
@@ -692 +700 @@
       lbl lbl' def
 
-  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
+  | RTLabs.St_op2 (op2, destr, RTLabs.Reg srcr1, RTLabs.Reg srcr2, lbl') ->
     translate_op2 op2 (find_local_env destr lenv)
       (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def
 
-  | RTLabs.St_load (_, addr, destr, lbl') ->
+  | RTLabs.St_load (_, RTLabs.Reg addr, destr, lbl') ->
     translate_load (find_local_env addr lenv) (find_local_env destr lenv)
       lbl lbl' def
 
-  | RTLabs.St_store (_, addr, srcr, lbl') ->
+  | RTLabs.St_store (_, RTLabs.Reg addr, RTLabs.Reg srcr, lbl') ->
     translate_store (find_local_env addr lenv) (find_local_env srcr lenv)
       lbl lbl' def
@@ -739 +747 @@
   | RTLabs.St_return (Some r) ->
     add_graph lbl (RTL.St_return (find_local_env r lenv)) def
-
-
+                
+  | _ -> assert false (*not possible because of previous removal of immediates*)
+
+let remove_immediates def =
+  let load_arg a lbl g rs = match a with
+    | RTLabs.Reg r -> (lbl, g, rs, r)
+    | RTLabs.Imm (c, t) ->
+      let new_l = Label.Gen.fresh def.RTLabs.f_luniverse in
+      let new_r = Register.fresh def.RTLabs.f_runiverse in
+      let g = Label.Map.add lbl (RTLabs.St_cst (new_r, c, new_l)) g in
+      (new_l, g, (new_r, t) :: rs, new_r) in 
+  let f lbl stmt (g, rs) =
+    match stmt with
+      | RTLabs.St_op2(op, r, a1, a2, l) ->
+        let (lbl', g, rs, r1) = load_arg a1 lbl g rs in
+        let (lbl', g, rs, r2) = load_arg a2 lbl' g rs in
+        let s = RTLabs.St_op2 (op, r, RTLabs.Reg r1, RTLabs.Reg r2, l) in
+        let g = Label.Map.add lbl' s g in
+        (g, rs)
+      | RTLabs.St_store(q, a1, a2, l) ->
+        let (lbl', g, rs, r1) = load_arg a1 lbl g rs in
+        let (lbl', g, rs, r2) = load_arg a2 lbl' g rs in
+        let s = RTLabs.St_store (q, RTLabs.Reg r1, RTLabs.Reg r2, l) in
+        let g = Label.Map.add lbl' s g in
+        (g, rs)
+      | RTLabs.St_load (q, a, r, l) ->
+        let (lbl', g, rs, r1) = load_arg a lbl g rs in
+        let s = RTLabs.St_load (q, RTLabs.Reg r1, r, l) in
+        let g = Label.Map.add lbl' s g in
+        (g, rs)
+      | _ -> (g, rs) in
+  let g = def.RTLabs.f_graph in
+  let (g, rs) = Label.Map.fold f g (g, []) in
+  let locals = List.rev_append rs def.RTLabs.f_locals in
+  { def with RTLabs.f_graph = g; RTLabs.f_locals = locals }
+ 
 let translate_internal def =
+  let def = remove_immediates def in
   let runiverse = def.RTLabs.f_runiverse in
   let lenv =

Deliverables/D2.2/8051/src/acc.ml

@@ -44 +44 @@
         the intermediate programs. *)
     Languages.compile (Options.is_debug_enabled ()) 
-      src_language tgt_language input_ast
+      (Options.get_transformations ()) src_language tgt_language input_ast
   in
   let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in
@@ -51 +51 @@
     begin
       let (annotated_input_ast, cost_id, cost_incr, extern_cost_variables) =
-        Languages.annotate input_ast final_ast in (
+        let cost_tern = Options.is_cost_ternary_enabled () in
+        Languages.annotate cost_tern input_ast final_ast in (
           save ~suffix:"-annotated" annotated_input_ast;
           Languages.save_cost exact_output output_filename cost_id cost_incr
             extern_cost_variables);
     end;
-                                             
-  if Options.is_debug_enabled () then 
+
+  if Options.is_debug_enabled () then
     List.iter save intermediate_asts;
 
@@ -93 +94 @@
     Languages.save
       (Options.is_asm_pretty ()) exact_output output_filename "" ast in
-  let target_asts = Languages.compile false src_language tgt_language input_ast
+  let target_asts =
+    Languages.compile false (Options.get_transformations ())
+      src_language tgt_language input_ast
   in
   let final_ast, _ = Misc.ListExt.cut_last target_asts in

Deliverables/D2.2/8051/src/checker.ml

@@ -14 +14 @@
     in 
     let sentence (k, (v1, v2)) =
+      let k = CostLabel.string_of_cost_label ~pretty:true k in
       Printf.sprintf "  Label %s %s in language `%s' \
                         whereas it %s in language `%s'."

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

@@ -117 +117 @@
   (** The following constructors are used by the annotation process only. *)
 
-  | Ecost of CostLabel.t*expr                   (**r cost label. *)
+  | Ecost of CostLabel.t * expr                 (**r cost label. *)
   | Ecall of ident * expr * expr
 
@@ -130 +130 @@
 type label = Label.t
 
+type loop_index = CostLabel.index option
+
 type statement =
   | Sskip                                       (**r do nothing *)
@@ -136 +138 @@
   | Ssequence of statement*statement            (**r sequence *)
   | Sifthenelse of expr*statement*statement     (**r conditional *)
-  | Swhile of expr*statement                    (**r [while] loop *)
-  | Sdowhile of expr*statement                  (**r [do] loop *)
-  | Sfor of statement*expr*statement*statement  (**r [for] loop *)
+  | Swhile of loop_index*expr*statement         (**r [while] loop *)
+  | Sdowhile of loop_index*expr*statement       (**r [do] loop *)
+  | Sfor of loop_index*statement*expr*statement*statement (**r [for] loop *)
   | Sbreak                                      (**r [break] statement *)
   | Scontinue                                   (**r [continue] statement *)

Deliverables/D2.2/8051/src/clight/clightAnnotator.ml

@@ -10 +10 @@
 let cost_id_prefix = "_cost"
 let cost_incr_prefix = "_cost_incr"
+let loop_id_prefix = "_i"
 
 
@@ -70 +71 @@
   let def_idents = function
     | Clight.Internal def ->
-        let vars =
-          string_set_of_list
-            (List.map fst (def.Clight.fn_params @ def.Clight.fn_vars)) in
-        let (names, cost_labels, user_labels) =
-          body_idents def.Clight.fn_body in
-        (StringTools.Set.union vars names, cost_labels, user_labels)
+      let vars =
+        string_set_of_list
+          (List.map fst (def.Clight.fn_params @ def.Clight.fn_vars)) in
+      let (names, cost_labels, user_labels) =
+        body_idents def.Clight.fn_body in
+      (StringTools.Set.union vars names, cost_labels, user_labels)
     | Clight.External (id, _, _) ->
-        (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty) in
+      (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty) in
   let fun_idents (id, f_def) =
     let (names, cost_labels, user_labels) = def_idents f_def in
@@ -93 +94 @@
 let all_labels p =
   let (_, cost_labels, user_labels) = prog_idents p in
-  let all =
-    CostLabel.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls)
-      cost_labels StringTools.Set.empty in
-  Label.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) user_labels all
+  let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in 
+  let all = CostLabel.Set.fold f cost_labels StringTools.Set.empty in
+  Label.Set.fold StringTools.Set.add user_labels all
 
 let all_idents p =
   let (names, cost_labels, user_labels) = prog_idents p in
+  let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in
+  let cost_labels = CostLabel.Set.fold f cost_labels StringTools.Set.empty in
   let to_string_set fold set =
     fold (fun lbl idents -> StringTools.Set.add lbl idents) set
       StringTools.Set.empty in
-  let cost_labels = to_string_set CostLabel.Set.fold cost_labels in
   let user_labels = to_string_set Label.Set.fold user_labels in
   StringTools.Set.union names (StringTools.Set.union cost_labels user_labels)
@@ -125 +126 @@
 let const_int i = Clight.Expr (Clight.Econst_int i, int_typ)
 
+let expr_of_cost_cond var = function
+  | CostExpr.Ceq k ->
+    Clight.Expr(Clight.Ebinop(Clight.Oeq, var, const_int k),int_typ) 
+  | CostExpr.Cgeq k ->
+    Clight.Expr(Clight.Ebinop(Clight.Oge, var, const_int k),int_typ) 
+  | CostExpr.Cmod (a, b) ->
+    let modulus =
+      Clight.Expr(Clight.Ebinop(Clight.Omod, var, const_int a), int_typ) in
+    Clight.Expr(Clight.Ebinop(Clight.Oeq, modulus, const_int b),int_typ)
+  | CostExpr.Cgeqmod (k, a, b) ->
+    let modulus =
+      Clight.Expr(Clight.Ebinop(Clight.Omod, var, const_int a), int_typ) in
+    let modulus_eq =
+      Clight.Expr(Clight.Ebinop(Clight.Oeq, modulus, const_int b),int_typ) in
+    let greater =
+      Clight.Expr(Clight.Ebinop(Clight.Oge, var, const_int k),int_typ) in
+    Clight.Expr(Clight.Eandbool(modulus_eq, greater),int_typ)
+
+let rec expr_of_cost_gen_cond var gc =
+  assert (not (CostExpr.CondSet.is_empty gc));
+  let c = CostExpr.CondSet.min_elt gc in
+  let c_expr = expr_of_cost_cond var c in
+  let rest = CostExpr.CondSet.remove c gc in
+  if CostExpr.CondSet.is_empty rest then c_expr else
+    let rest_expr = expr_of_cost_gen_cond var rest in
+    Clight.Expr(Clight.Eandbool(c_expr, rest_expr), int_typ)
+
+let rec expr_of_cost_expr prefix = function
+  | CostExpr.Exact k -> const_int k
+  | CostExpr.Ternary(index, cond, if_true, if_false) ->
+    let id = CostLabel.make_id prefix index in
+    let var = Clight.Expr(Clight.Evar id, int_typ) in 
+    let cond_e = expr_of_cost_gen_cond var cond in
+    let if_true_e = expr_of_cost_expr prefix if_true in
+    let if_false_e = expr_of_cost_expr prefix if_false in
+    Clight.Expr(Clight.Econdition(cond_e, if_true_e, if_false_e), int_typ)
+
+(* as long as Clight parser will be called at the end, this hack works *)
+(* this will be called in case -no-cost-tern is active. *)
+let rec side_effect_expr_of_cost_expr prefix cost_incr cont e_type = function
+  | CostExpr.Exact k ->
+    Clight.Expr(Clight.Ecall (cost_incr, const_int k, cont), e_type)
+  | CostExpr.Ternary(index, cond, if_true, if_false) ->
+    let id = CostLabel.make_id prefix index in
+    let var = Clight.Expr(Clight.Evar id, int_typ) in
+    let cond_e = expr_of_cost_gen_cond var cond in
+    let rec_call = side_effect_expr_of_cost_expr prefix cost_incr cont e_type in
+    let if_true_e = rec_call if_true in
+    let if_false_e = rec_call if_false in
+    Clight.Expr(Clight.Econdition(cond_e, if_true_e, if_false_e), int_typ)
+
+let rec stmt_of_cost_expr prefix cost_incr = function
+  | CostExpr.Exact k -> Clight.Scall (None, cost_incr, [const_int k])
+  | CostExpr.Ternary(index, cond, if_true, if_false) ->
+    let id = CostLabel.make_id prefix index in
+    let var = Clight.Expr(Clight.Evar id, int_typ) in 
+    let cond_e = expr_of_cost_gen_cond var cond in
+    let if_true_s = stmt_of_cost_expr prefix cost_incr if_true in
+    let if_false_s = stmt_of_cost_expr prefix cost_incr if_false in
+    Clight.Sifthenelse (cond_e, if_true_s, if_false_s)
+
 (* Instrument an expression. *)
 
-let rec instrument_expr cost_mapping cost_incr e =
-  let Clight.Expr (e, t) = e in
-  match e with
-    | Clight.Ecost (lbl, e)
-        when CostLabel.Map.mem lbl cost_mapping &&
-             CostLabel.Map.find lbl cost_mapping = 0 ->
-        e
-    | _ ->
-        let e' = instrument_expr_descr cost_mapping cost_incr e in
-        Clight.Expr (e', t)
-and instrument_expr_descr cost_mapping cost_incr e = match e with
-  | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Evar _
-  | Clight.Esizeof _ -> e
-  | Clight.Ederef e ->
-      let e' = instrument_expr cost_mapping cost_incr e in
-      Clight.Ederef e'
-  | Clight.Eaddrof e ->
-      let e' = instrument_expr cost_mapping cost_incr e in
-      Clight.Eaddrof e'
-  | Clight.Eunop (op, e) ->
-      let e' = instrument_expr cost_mapping cost_incr e in
-      Clight.Eunop (op, e')
-  | Clight.Ebinop (op, e1, e2) ->
-      let e1' = instrument_expr cost_mapping cost_incr e1 in
-      let e2' = instrument_expr cost_mapping cost_incr e2 in
-      Clight.Ebinop (op, e1', e2')
-  | Clight.Ecast (t, e) ->
-      let e' = instrument_expr cost_mapping cost_incr e in
-      Clight.Ecast (t, e')
-  | Clight.Econdition (e1, e2, e3) ->
-      let e1' = instrument_expr cost_mapping cost_incr e1 in
-      let e2' = instrument_expr cost_mapping cost_incr e2 in
-      let e3' = instrument_expr cost_mapping cost_incr e3 in
-      Clight.Econdition (e1', e2', e3')
-  | Clight.Eandbool (e1, e2) ->
-      let e1' = instrument_expr cost_mapping cost_incr e1 in
-      let e2' = instrument_expr cost_mapping cost_incr e2 in
-      Clight.Eandbool (e1', e2')
-  | Clight.Eorbool (e1, e2) ->
-      let e1' = instrument_expr cost_mapping cost_incr e1 in
-      let e2' = instrument_expr cost_mapping cost_incr e2 in
-      Clight.Eorbool (e1', e2')
-  | Clight.Efield (e, x) ->
-      let e' = instrument_expr cost_mapping cost_incr e in
-      Clight.Efield (e', x)
-  | Clight.Ecost (lbl, e) when CostLabel.Map.mem lbl cost_mapping ->
-      let e' = instrument_expr cost_mapping cost_incr e in
-      let incr = CostLabel.Map.find lbl cost_mapping in
-      if incr = 0 then let Clight.Expr (e'', _) = e' in e''
-      else Clight.Ecall (cost_incr, const_int incr, e')
-  | Clight.Ecost (_, e) ->
-    let Clight.Expr (e', _) = instrument_expr cost_mapping cost_incr e in
-    e'
-  | Clight.Ecall (x, e1, e2) -> assert false (* Should not happen. *)
+(* FIXME: currently using a hack (reparsing) *)
+let instrument_expr cost_tern l_ind cost_mapping cost_incr =
+  let f_expr (Clight.Expr(ed, et) as e) sub_res = match ed, sub_res with
+  | Clight.Ecost (lbl, _), e' :: _ ->
+    let atom = lbl.CostLabel.name in
+    let cost =
+      try
+        CostLabel.Atom.Map.find atom cost_mapping
+      with (* if atom is not present, then map to 0 *)
+        | Not_found -> CostExpr.Exact 0 in
+    if cost = CostExpr.Exact 0 then e' else
+      if cost_tern then
+        let cost = expr_of_cost_expr l_ind cost in
+        Clight.Expr(Clight.Ecall (cost_incr, cost, e'), et)
+      else
+        side_effect_expr_of_cost_expr l_ind cost_incr e' et cost
+  | Clight.Ecall (_, _, _), _ -> assert false (* Should not happen. *)
+  | _ -> ClightFold.expr_fill_exprs e sub_res in
+  ClightFold.expr2 f_expr
+
+let loop_increment prefix depth body = match depth  with
+  | None -> body
+  | Some d ->
+    let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), int_typ) in
+    let add a b = Clight.Expr(Clight.Ebinop(Clight.Oadd, a, b), int_typ) in
+    Clight.Ssequence(body, Clight.Sassign(id, add id (const_int 1)))
+      
+let loop_reset_index prefix depth loop = match depth with
+  | None -> loop
+  | Some d ->
+    let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), int_typ) in
+    Clight.Ssequence(Clight.Sassign(id, const_int 0), loop)
+
 
 (* Instrument a statement. *)
 
-let rec instrument_body cost_mapping cost_incr stmt = match stmt with
-  | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sreturn None
-  | Clight.Sgoto _ ->
-    stmt
-  | Clight.Sassign (e1, e2) ->
-    let e1' = instrument_expr cost_mapping cost_incr e1 in
-    let e2' = instrument_expr cost_mapping cost_incr e2 in
-    Clight.Sassign (e1', e2')
-  | Clight.Scall (eopt, f, args) ->
-    let eopt' = match eopt with
-      | None -> None
-      | Some e -> Some (instrument_expr cost_mapping cost_incr e) in
-    let f' = instrument_expr cost_mapping cost_incr f in
-    let args' = List.map (instrument_expr cost_mapping cost_incr) args in
-    Clight.Scall (eopt', f', args')
-  | Clight.Ssequence (s1, s2) ->
-    Clight.Ssequence (instrument_body cost_mapping cost_incr s1,
-                      instrument_body cost_mapping cost_incr s2)
-  | Clight.Sifthenelse (e, s1, s2) ->
-    let e' = instrument_expr cost_mapping cost_incr e in
-    let s1' = instrument_body cost_mapping cost_incr s1 in
-    let s2' = instrument_body cost_mapping cost_incr s2 in
-    Clight.Sifthenelse (e', s1', s2')
-  | Clight.Swhile (e, s) ->
-    let e' = instrument_expr cost_mapping cost_incr e in
-    let s' = instrument_body cost_mapping cost_incr s in
-    Clight.Swhile (e', s')
-  | Clight.Sdowhile (e, s) ->
-    let e' = instrument_expr cost_mapping cost_incr e in
-    let s' = instrument_body cost_mapping cost_incr s in
-    Clight.Sdowhile (e', s')
-  | Clight.Sfor (s1, e, s2, s3) ->
-    let s1' = instrument_body cost_mapping cost_incr s1 in
-    let e' = instrument_expr cost_mapping cost_incr e in
-    let s2' = instrument_body cost_mapping cost_incr s2 in
-    let s3' = instrument_body cost_mapping cost_incr s3 in
-    Clight.Sfor (s1', e', s2', s3')
-  | Clight.Sreturn (Some e) ->
-    let e' = instrument_expr cost_mapping cost_incr e in
-    Clight.Sreturn (Some e')
-  | Clight.Sswitch (e, ls) ->
-    let e' = instrument_expr cost_mapping cost_incr e in
-    let ls' = instrument_ls cost_mapping cost_incr ls in
-    Clight.Sswitch (e', ls')
-  | Clight.Slabel (lbl, s) ->
-    let s' = instrument_body cost_mapping cost_incr s in
-    Clight.Slabel (lbl, s')
-  | Clight.Scost (lbl, s) when CostLabel.Map.mem lbl cost_mapping ->
+(* FIXME: use ClightFold, a much better option *)
+let rec instrument_body cost_tern l_ind cost_mapping cost_incr stmt =
+  let instr_expr = instrument_expr cost_tern l_ind cost_mapping cost_incr in
+  let instr_body = instrument_body cost_tern l_ind cost_mapping cost_incr in
+  match stmt with
+    | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sreturn None
+    | Clight.Sgoto _ ->
+      stmt
+    | Clight.Sassign (e1, e2) ->
+      let e1' = instr_expr e1 in
+      let e2' = instr_expr e2 in
+      Clight.Sassign (e1', e2')
+    | Clight.Scall (eopt, f, args) ->
+      let eopt' = Option.map instr_expr eopt in
+      let f' = instr_expr f in
+      let args = List.map (instr_expr) args in
+      Clight.Scall (eopt', f', args)
+    | Clight.Ssequence (s1, s2) ->
+      Clight.Ssequence (
+        instr_body s1,
+        instr_body s2)
+    | Clight.Sifthenelse (e, s1, s2) ->
+      let e' = instr_expr e in
+      let s1' = instr_body s1 in
+      let s2' = instr_body s2 in
+      Clight.Sifthenelse (e', s1', s2')
+    | Clight.Swhile (i, e, s) ->
+      let e' = instr_expr e in
+      let s' = instr_body s in
+      let s' = loop_increment l_ind i s' in
+      loop_reset_index l_ind i (Clight.Swhile (None, e', s'))
+    | Clight.Sdowhile (i, e, s) ->
+      let e' = instr_expr e in
+      let s' = instr_body s in
+      let s' = loop_increment l_ind i s' in
+      loop_reset_index l_ind i (Clight.Sdowhile (None, e', s'))
+    | Clight.Sfor (i, s1, e, s2, s3) ->
+      let s1' = instr_body s1 in
+      let e' = instr_expr e in
+      let s2' = instr_body s2 in
+      let s3' = instr_body s3 in
+      let s3' = loop_increment l_ind i s3' in
+      loop_reset_index l_ind i (Clight.Sfor (None, s1', e', s2', s3'))
+    | Clight.Sreturn (Some e) ->
+      let e' = instr_expr e in
+      Clight.Sreturn (Some e')
+    | Clight.Sswitch (e, ls) ->
+      let e' = instr_expr e in
+      let ls' = instrument_ls cost_tern l_ind cost_mapping cost_incr ls in
+      Clight.Sswitch (e', ls')
+    | Clight.Slabel (lbl, s) ->
+      let s' = instr_body s in
+      Clight.Slabel (lbl, s')
+    | Clight.Scost (lbl, s) ->
     (* Keep the cost label in the code. *)
-    let s' = instrument_body cost_mapping cost_incr s in
-    let incr = CostLabel.Map.find lbl cost_mapping in
-    let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
-    let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
-    let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
-    Clight.Scost (lbl, Clight.Ssequence (Clight.Scall (None, f, args), s'))
-  (*
-    let s' = instrument_body cost_mapping cost_incr s in
-    let incr = CostLabel.Map.find lbl cost_mapping in
-    if incr = 0 then s'
-    else
-    let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
-    let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
-    let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
-    Clight.Ssequence (Clight.Scall (None, f, args), s')
-  *)
-  | Clight.Scost (lbl, s) ->
-    (* Keep the cost label in the code and show the increment of 0. *)
-    let s' = instrument_body cost_mapping cost_incr s in
-    let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
-    let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
-    let args = [Clight.Expr (Clight.Econst_int 0, int_typ)] in
-    Clight.Scost (lbl, Clight.Ssequence (Clight.Scall (None, f, args), s'))
-  (*
-    instrument_body cost_mapping cost_incr s
-  *)
-and instrument_ls cost_mapping cost_incr = function
+      let s' = instr_body s in
+      let atom = lbl.CostLabel.name in
+      let cost =
+        try
+          CostLabel.Atom.Map.find atom cost_mapping
+        with (* if atom is not present, then map to 0 *)
+          | Not_found -> CostExpr.Exact 0 in
+      let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
+      let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
+      let cost_stmt =
+        if not cost_tern then stmt_of_cost_expr l_ind f cost else
+        let cost = expr_of_cost_expr l_ind cost in
+        Clight.Scall(None, f, [cost]) in
+      Clight.Scost (lbl, Clight.Ssequence (cost_stmt, s'))
+(*
+  let s' = instrument_body l_ind cost_mapping cost_incr s in
+  let incr = CostLabel.Map.find lbl cost_mapping in
+  if incr = 0 then s'
+  else
+  let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
+  let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
+  let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
+  Clight.Ssequence (Clight.Scall (None, f, args), s')
+*)
+(*
+  instrument_body l_ind cost_mapping cost_incr s
+*)
+and instrument_ls cost_tern l_ind cost_mapping cost_incr = function
   | Clight.LSdefault s ->
-    let s' = instrument_body cost_mapping cost_incr s in
+    let s' = instrument_body cost_tern l_ind cost_mapping cost_incr s in
     Clight.LSdefault s'
   | Clight.LScase (i, s, ls) ->
-    let s' = instrument_body cost_mapping cost_incr s in
-    let ls' = instrument_ls cost_mapping cost_incr ls in
+    let s' = instrument_body cost_tern l_ind cost_mapping cost_incr s in
+    let ls' = instrument_ls cost_tern l_ind cost_mapping cost_incr ls in
     Clight.LScase (i, s', ls')
+      
+let rec loop_indexes_defs prefix max_depth =
+  if max_depth = 0 then [] else
+    let max_depth = max_depth - 1 in
+    let id = CostLabel.make_id prefix max_depth in
+    (id, int_typ) :: loop_indexes_defs prefix max_depth
+
+let max_depth =
+  let f_expr _ _ = () in
+  let f_stmt stmt _ res_stmts =
+    let curr_max = List.fold_left max 0 res_stmts in
+    if curr_max > 0 then curr_max else  
+      match stmt with
+        | Clight.Swhile(Some x,_,_) | Clight.Sdowhile(Some x,_,_)
+        | Clight.Sfor(Some x,_,_,_,_) -> x + 1
+        | _ -> 0 in
+  ClightFold.statement2 f_expr f_stmt
 
 (* Instrument a function. *)
 
-let instrument_funct cost_mapping cost_incr (id, def) =
+let instrument_funct cost_tern  l_ind cost_mapping cost_incr (id, def) =
   let def = match def with
     | Clight.Internal def ->
-        let body = instrument_body cost_mapping cost_incr def.Clight.fn_body in
-        Clight.Internal { def with Clight.fn_body = body }
+      let max_depth = max_depth def.Clight.fn_body in
+      let vars = loop_indexes_defs l_ind max_depth in
+      let vars = List.rev_append vars def.Clight.fn_vars in
+      let body = def.Clight.fn_body in
+      let body =
+        instrument_body cost_tern l_ind cost_mapping cost_incr body in
+      Clight.Internal { def with Clight.fn_body = body; Clight.fn_vars = vars}
     | Clight.External _ -> def
   in
@@ -326 +396 @@
     name of the cost variable and the name of the cost increment function. *)
 
-let instrument p cost_mapping =
+let instrument cost_tern p cost_mapping =
 
   (* Create a fresh 'cost' variable. *)
@@ -334 +404 @@
   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
+
   (* Create a fresh uninitialized global variable for each extern function. *)
   let (extern_cost_decls, extern_cost_variables) =
@@ -344 +418 @@
   let cost_incr_def = cost_incr_def cost_id cost_incr in
 
+  (* Turn the mapping from indexed cost labels to integers into one from *)
+  (* cost atoms to cost expresisons *)
+  let cost_mapping = CostExpr.cost_expr_mapping_of_cost_mapping cost_mapping in
+
   (* Instrument each function *)
+  let prog_funct = p.Clight.prog_funct in
   let prog_funct =
-    List.map (instrument_funct cost_mapping cost_incr) p.Clight.prog_funct in
+    let f = instrument_funct cost_tern l_ind cost_mapping cost_incr in
+    List.map f prog_funct in
 
   (* Glue all this together. *)

Deliverables/D2.2/8051/src/clight/clightAnnotator.mli

@@ -2 +2 @@
 (** This module defines the instrumentation of a [Clight] program. *)
 
-(** [instrument prog cost_map] instruments the program [prog]. First a fresh
-    global variable --- the so-called cost variable --- is added to the program.
-    Then, each cost label in the program is replaced by an increment of the cost
-    variable, following the mapping [cost_map]. The function also returns the
-    name of the cost variable, the name of the cost increment function, and a
-    fresh uninitialized global (cost) variable associated to each extern
-    function. *)
-
-val instrument : Clight.program -> int CostLabel.Map.t ->
+(** [instrument cost_tern prog cost_map] instruments the program [prog]. First a
+    fresh global variable --- the so-called cost variable --- is added to the
+    program. Then, each cost label in the program is replaced by an increment of
+    the cost variable, following the mapping [cost_map]. The function also
+    returns the name of the cost variable, the name of the cost increment
+    function, and a fresh uninitialized global (cost) variable associated to each
+    extern function. [cost_tern] rules whether cost increments are given by
+    ternary expressions (more readable) or by branch statements (for frama-c
+    itegration). *)
+val instrument : bool -> Clight.program -> int CostLabel.Map.t ->
                  Clight.program * string * string * string StringTools.Map.t
 

Deliverables/D2.2/8051/src/clight/clightFold.ml

@@ -116 +116 @@
   | Clight.Ssequence (stmt1, stmt2) -> ([], [stmt1 ; stmt2])
   | Clight.Sifthenelse (e, stmt1, stmt2) -> ([e], [stmt1 ; stmt2])
-  | Clight.Swhile (e, stmt) | Clight.Sdowhile (e, stmt) -> ([e], [stmt])
-  | Clight.Sfor (stmt1, e, stmt2, stmt3) -> ([e], [stmt1 ; stmt2 ; stmt3])
+  | Clight.Swhile (_, e, stmt) | Clight.Sdowhile (_, e, stmt) -> ([e], [stmt])
+  | Clight.Sfor (_, stmt1, e, stmt2, stmt3) -> ([e], [stmt1 ; stmt2 ; stmt3])
   | Clight.Sreturn (Some e) -> ([e], [])
   | Clight.Sswitch (e, lbl_stmts) -> ([e], labeled_statements_subs lbl_stmts)
@@ -145 +145 @@
     | Clight.Sifthenelse _, e :: _, stmt1 :: stmt2 :: _ ->
       Clight.Sifthenelse (e, stmt1, stmt2)
-    | Clight.Swhile _, e :: _, stmt :: _ ->
-      Clight.Swhile (e, stmt)
-    | Clight.Sdowhile _, e :: _, stmt :: _ ->
-      Clight.Sdowhile (e, stmt)
-    | Clight.Sfor _, e :: _, stmt1 :: stmt2 :: stmt3 :: _ ->
-      Clight.Sfor (stmt1, e, stmt2, stmt3)
+    | Clight.Swhile (i, _, _), e :: _, stmt :: _ ->
+      Clight.Swhile (i, e, stmt)
+    | Clight.Sdowhile (i, _, _), e :: _, stmt :: _ ->
+      Clight.Sdowhile (i, e, stmt)
+    | Clight.Sfor (i, _, _, _, _), e :: _, stmt1 :: stmt2 :: stmt3 :: _ ->
+      Clight.Sfor (i, stmt1, e, stmt2, stmt3)
     | Clight.Sreturn (Some _), e :: _, _ -> Clight.Sreturn (Some e)
     | Clight.Sswitch (_, lbl_stmts), e :: _, _ ->

Deliverables/D2.2/8051/src/clight/clightFromC.ml

@@ -490 +490 @@
       Sifthenelse(convertExpr env e, convertStmt env s1, convertStmt env s2)
   | C.Swhile(e, s1) ->
-      Swhile(convertExpr env e, convertStmt env s1)
+      Swhile(None, convertExpr env e, convertStmt env s1)
   | C.Sdowhile(s1, e) ->
-      Sdowhile(convertExpr env e, convertStmt env s1)
+      Sdowhile(None, convertExpr env e, convertStmt env s1)
   | C.Sfor(s1, e, s2, s3) ->
-      Sfor(convertStmt env s1, convertExpr env e, convertStmt env s2,
+      Sfor(None, convertStmt env s1, convertExpr env e, convertStmt env s2,
            convertStmt env s3)
   | C.Sbreak ->

Deliverables/D2.2/8051/src/clight/clightInterpret.ml

@@ -4 +4 @@
 type localEnv = Value.address LocalEnv.t
 type memory = Clight.fundef Mem.memory
+type indexing = CostLabel.const_indexing
 
 open Clight
@@ -26 +27 @@
   | Kstop
   | Kseq of statement*continuation
-  | Kwhile of expr*statement*continuation
-  | Kdowhile of expr*statement*continuation
-  | Kfor2 of expr*statement*statement*continuation
-  | Kfor3 of expr*statement*statement*continuation 
+  | Kwhile of int option*expr*statement*continuation
+  | Kdowhile of int option*expr*statement*continuation
+  | Kfor2 of int option*expr*statement*statement*continuation
+  | Kfor3 of int option*expr*statement*statement*continuation 
   | Kswitch of continuation
   | Kcall of (Value.address*ctype) option*cfunction*localEnv*continuation
 
 type state =
-  | State of cfunction*statement*continuation*localEnv*memory
-  | Callstate of fundef*Value.t list*continuation*memory
-  | Returnstate of Value.t*continuation*memory
+  | State of cfunction*statement*continuation*localEnv*memory*indexing list
+  | Callstate of fundef*Value.t list*continuation*memory*indexing list
+  | Returnstate of Value.t*continuation*memory*indexing list
 
 let string_of_unop = function
@@ -104 +105 @@
   | Esizeof ty -> "sizeof(" ^ (string_of_ctype ty) ^ ")"
   | Efield (e, field) -> "(" ^ (string_of_expr e) ^ ")." ^ field
-  | Ecost (cost_lbl, e) -> "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e)
+  | Ecost (cost_lbl, e) -> 
+    let cost_lbl = CostLabel.string_of_cost_label cost_lbl in
+    "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e)
   | Ecall (f, arg, e) ->
     "(" ^ f ^ "(" ^ (string_of_expr arg) ^ "), " ^ (string_of_expr e) ^ ")"
@@ -110 +113 @@
 let string_of_args args =
   "(" ^ (MiscPottier.string_of_list ", " string_of_expr args) ^ ")"
+
+let string_of_loop_depth = function
+        | None -> ""
+        | Some d -> " at " ^ string_of_int d
 
 let rec string_of_statement = function
@@ -119 +126 @@
   | Ssequence _ -> "sequence"
   | Sifthenelse (e, _, _) -> "if (" ^ (string_of_expr e) ^ ")"
-  | Swhile (e, _) -> "while (" ^ (string_of_expr e) ^ ")"
-  | Sdowhile _ -> "dowhile"
-  | Sfor (s, _, _, _) -> "for (" ^ (string_of_statement s) ^ "; ...)"
+  | Swhile (i, e, _) ->
+                let d = string_of_loop_depth i in
+                "while" ^ d ^ " (" ^ (string_of_expr e) ^ ")"
+  | Sdowhile (i, _, _) ->
+    let d = string_of_loop_depth i in
+    "dowhile" ^ d
+  | Sfor (i, s, _, _, _) ->
+                let d = string_of_loop_depth i in
+                "for" ^ d ^ " (" ^ (string_of_statement s) ^ "; ...)"
   | Sbreak -> "break"
   | Scontinue -> "continue"
@@ -129 +142 @@
   | Slabel (lbl, _) -> "label " ^ lbl
   | Sgoto lbl -> "goto " ^ lbl
-  | Scost (lbl, _) -> "cost " ^ lbl
+  | Scost (lbl, _) ->
+    let lbl = CostLabel.string_of_cost_label lbl in
+                "cost " ^ lbl
 
 let string_of_local_env lenv =
@@ -136 +151 @@
   LocalEnv.fold f lenv ""
 
-let print_state = function
-  | State (_, stmt, _, lenv, mem) ->
-    Printf.printf "Local environment:\n%s\n\nMemory:%s\nRegular state: %s\n\n%!"
+let print_state state = match state with
+  | State (_, stmt, _, lenv, mem, c) ->
+    Printf.printf "Local environment:\n%s\n\nMemory:%s\nLoop indexing: "
       (string_of_local_env lenv)
-      (Mem.to_string mem)
+      (Mem.to_string mem);
+    let i = CostLabel.curr_const_ind c in
+    CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) i;
+    Printf.printf "\nRegular state: %s\n\n%!"
       (string_of_statement stmt)
-  | Callstate (_, args, _, mem) ->
+  | Callstate (_, args, _, mem, _) ->
     Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!"
       (Mem.to_string mem)
       (MiscPottier.string_of_list " " Value.to_string args)
-  | Returnstate (v, _, mem) ->
+  | Returnstate (v, _, mem, _) ->
     Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
       (Mem.to_string mem)
@@ -155 +173 @@
 
 let rec call_cont = function
-  | Kseq (_,k) | Kwhile (_,_,k) | Kdowhile (_,_,k)
-  | Kfor2 (_,_,_,k) | Kfor3 (_,_,_,k) | Kswitch k -> call_cont k
+  | Kseq (_,k) | Kwhile (_, _,_,k) | Kdowhile (_, _,_,k)
+  | Kfor2 (_, _,_,_,k) | Kfor3 (_, _,_,_,k) | Kswitch k -> call_cont k
   | k -> k
 
@@ -174 +192 @@
       | None -> find_label1 lbl s2 k
       )
-  | Swhile (a,s1) -> find_label1 lbl s1 (Kwhile(a,s1,k))
-  | Sdowhile (a,s1) -> find_label1 lbl s1 (Kdowhile(a,s1,k))
-  | Sfor (a1,a2,a3,s1) ->
-      (match find_label1 lbl a1 (Kseq ((Sfor(Sskip,a2,a3,s1)),k)) with
+  | Swhile (i,a,s1) -> find_label1 lbl s1 (Kwhile(i,a,s1,k))
+  | Sdowhile (i,a,s1) -> find_label1 lbl s1 (Kdowhile(i,a,s1,k))
+  | Sfor (i,a1,a2,a3,s1) ->
+                (* doubt: should we search for labels in a1? *)
+      (match find_label1 lbl a1 (Kseq ((Sfor(i,Sskip,a2,a3,s1)),k)) with
       | Some sk -> Some sk
       | None ->
-          (match find_label1 lbl s1 (Kfor2(a2,a3,s1,k)) with
+          (match find_label1 lbl s1 (Kfor2(i,a2,a3,s1,k)) with
           | Some sk -> Some sk
-          | None -> find_label1 lbl a3 (Kfor3(a2,a3,s1,k))
+          | None -> find_label1 lbl a3 (Kfor3(i,a2,a3,s1,k))
           ))
   | Sswitch (e,sl) -> find_label_ls lbl sl (Kswitch k)
@@ -355 +374 @@
 let is_false (v, _) = Value.is_false v
 
-let rec eval_expr localenv m (Expr (ee, tt)) =
+let rec eval_expr localenv m c (Expr (ee, tt)) =
   match ee with
     | Econst_int i ->
@@ -369 +388 @@
       ((v, tt), [])
     | Ederef e when is_function_type tt || is_big_type tt ->
-      let ((v1,_),l1) = eval_expr localenv m e in
+      let ((v1,_),l1) = eval_expr localenv m c e in
       ((v1,tt),l1) 
     | Ederef e ->
-      let ((v1,_),l1) = eval_expr localenv m e in
+      let ((v1,_),l1) = eval_expr localenv m c e in
       let addr = address_of_value v1 in
       let v = Mem.load m (size_of_ctype tt) addr in
       ((v,tt),l1) 
     | Eaddrof exp ->
-      let ((addr,_),l) = eval_lvalue localenv m exp in
+      let ((addr,_),l) = eval_lvalue localenv m c exp in
       ((value_of_address addr,tt),l)
     | Ebinop (op,exp1,exp2) ->  
-      let (v1,l1) = eval_expr localenv m exp1 in
-      let (v2,l2) = eval_expr localenv m exp2 in
+      let (v1,l1) = eval_expr localenv m c exp1 in
+      let (v2,l2) = eval_expr localenv m c exp2 in
       ((eval_binop tt v1 v2 op,tt),l1@l2)
     | Eunop (op,exp) -> 
-      let (e1,l1) = eval_expr localenv m exp in
+      let (e1,l1) = eval_expr localenv m c exp in
       ((eval_unop tt e1 op,tt),l1)
     | Econdition (e1,e2,e3) ->
-      let (v1,l1) = eval_expr localenv m e1 in
-      if is_true v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)
+      let (v1,l1) = eval_expr localenv m c e1 in
+      if is_true v1 then let (v2,l2) = eval_expr localenv m c e2 in (v2,l1@l2)
       else
-        if is_false v1 then let (v3,l3) = eval_expr localenv m e3 in (v3,l1@l3)
+        if is_false v1 then let (v3,l3) = eval_expr localenv m c e3 in (v3,l1@l3)
       else (v1,l1)
     | Eandbool (e1,e2) -> 
-      let (v1,l1) = eval_expr localenv m e1 in
-      if is_true v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)
+      let (v1,l1) = eval_expr localenv m c e1 in
+      if is_true v1 then let (v2,l2) = eval_expr localenv m c e2 in (v2,l1@l2)
       else (v1,l1)
     | Eorbool (e1,e2) ->
-      let (v1,l1) = eval_expr localenv m e1 in
-      if is_false v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)
+      let (v1,l1) = eval_expr localenv m c e1 in
+      if is_false v1 then let (v2,l2) = eval_expr localenv m c e2 in (v2,l1@l2)
       else (v1,l1)
     | Esizeof cty -> ((Value.of_int (sizeof cty),tt),[])
     | Efield (e1,id) -> 
-      let ((v1,t1),l1) = eval_expr localenv m e1 in
+      let ((v1,t1),l1) = eval_expr localenv m c e1 in
       let addr = address_of_value (get_offset v1 id t1) in
       ((Mem.load m (size_of_ctype tt) addr, tt), l1)
     | Ecost (lbl,e1) ->
-      let (v1,l1) = eval_expr localenv m e1 in
+      (* applying current indexing on label *)
+      let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in
+      let (v1,l1) = eval_expr localenv m c e1 in
       (v1,lbl::l1)
     | Ecall _ -> assert false (* only used by the annotation process *)
     | Ecast (cty,exp) -> 
-      let ((v,ty),l1) = eval_expr localenv m exp in
+      let ((v,ty),l1) = eval_expr localenv m c exp in
       ((eval_cast (v,ty,cty),tt),l1)
 
-and eval_lvalue localenv m (Expr (e,t)) = match e with
+and eval_lvalue localenv m c (Expr (e,t)) = match e with
   | Econst_int _ | Econst_float _ | Eaddrof _ | Eunop (_,_) | Ebinop (_,_,_) 
   | Ecast (_,_) | Econdition (_,_,_) | Eandbool (_,_)  | Eorbool (_,_) 
@@ -419 +440 @@
   | Evar id -> ((find_symbol localenv m id,t),[])
   | Ederef ee ->
-    let ((v,_),l1) = eval_expr localenv m ee in 
+    let ((v,_),l1) = eval_expr localenv m c ee in 
     ((address_of_value v,t),l1)
   | Efield (ee,id) ->
-    let ((v,tt),l1) = eval_expr localenv m ee in 
+    let ((v,tt),l1) = eval_expr localenv m c ee in 
     let v' = get_offset v id tt in
     ((address_of_value v', t), l1)
   | Ecost (lbl,ee) ->
-    let (v,l) = eval_lvalue localenv m ee in
+    let (v,l) = eval_lvalue localenv m c ee in
     (v,lbl::l)
   | Ecall _ -> assert false (* only used in the annotation process *)
 
-let eval_exprlist lenv mem es =
+let eval_exprlist lenv mem c es =
   let f (vs, cost_lbls) e =
-    let ((v, _), cost_lbls') = eval_expr lenv mem e in
+    let ((v, _), cost_lbls') = eval_expr lenv mem c e in
     (vs @ [v], cost_lbls @ cost_lbls') in
   List.fold_left f ([], []) es
@@ -464 +485 @@
   else error "undefined condition guard value."
 
-let eval_stmt f k e m s = match s, k with
-  | Sskip, Kseq(s,k) -> (State(f,s,k,e,m),[])
-  | Sskip, Kwhile(a,s,k) -> (State(f,Swhile(a,s),k,e,m),[])
-  | Sskip, Kdowhile(a,s,k) ->
-    let ((v1, _),l1) = eval_expr e m a in 
-    let a_false = (State(f,Sskip,k,e,m),l1) in
-    let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in
+let eval_stmt f k e m s c = match s, k with
+  | Sskip, Kseq(s,k) -> (State(f,s,k,e,m,c),[])
+  | Sskip, Kwhile(i,a,s,k') | Scontinue, Kwhile(i,a,s,k')
+  | Sskip, Kdowhile(i,a,s,k') | Scontinue, Kdowhile (i,a,s,k') ->
+    (* possibly continuing a loop *)
+    CostLabel.continue_loop_opt c i; (* if loop is not continued, this change 
+                                        will have no effect in the following. *) 
+    let ((v1,_),l1) = eval_expr e m c a in 
+    let a_false = (State(f,Sskip,k',e,m,c),l1) in
+    let a_true = (State(f,s,k,e,m,c),l1) in
     condition v1 a_true a_false
-  | Sskip, Kfor3(a2,a3,s,k) -> (State(f,Sfor(Sskip,a2,a3,s),k,e,m),[])
-  | Sskip, Kfor2(a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
-  | Sskip, Kswitch k -> (State(f,Sskip,k,e,m),[])
+  | Sskip, Kfor3(i,a2,a3,s,k) | Scontinue, Kfor3(i,a2,a3,s,k) ->
+    CostLabel.continue_loop_opt c i;
+    let ((v1,_),l1) = eval_expr e m c a2 in 
+    let a_false = (State(f,Sskip,k,e,m,c),l1) in
+    let a_true = (State(f,s,Kfor2(i,a2,a3,s,k),e,m,c),l1) in
+    condition v1 a_true a_false
+  | Sskip, Kfor2(i,a2,a3,s,k) ->
+    (State(f,a3,Kfor3(i,a2,a3,s,k),e,m,c),[])
+  | Sskip, Kswitch k -> (State(f,Sskip,k,e,m,c),[])
   | Sskip, Kcall _ -> 
     let m' = free_local_env m e in
-    (Returnstate(Value.undef,k,m'),[])
+    (Returnstate(Value.undef,k,m',c),[])
   | Sassign(a1, a2), _ -> 
-    let ((v1,t1),l1) = (eval_lvalue e m a1) in
-    let ((v2,t2),l2) = eval_expr e m a2 in
-    (State(f,Sskip,k,e,assign m v2 t1 v1),l1@l2)
+    let ((v1,t1),l1) = (eval_lvalue e m c a1) in
+    let ((v2,t2),l2) = eval_expr e m c a2 in
+    (State(f,Sskip,k,e,assign m v2 t1 v1,c),l1@l2)
   | Scall(None,a,al), _ ->
-    let ((v1,_),l1) = eval_expr e m a in 
+    let ((v1,_),l1) = eval_expr e m c a in 
     let fd = Mem.find_fun_def m (address_of_value v1) in
-    let (vargs,l2) = eval_exprlist e m al in
-    (Callstate(fd,vargs,Kcall(None,f,e,k),m),l1@l2)
+    let (vargs,l2) = eval_exprlist e m c al in
+    (Callstate(fd,vargs,Kcall(None,f,e,k),m,c),l1@l2)
   | Scall(Some lhs,a,al), _ ->
-    let ((v1,_),l1) = eval_expr e m a in 
+    let ((v1,_),l1) = eval_expr e m c a in 
     let fd = Mem.find_fun_def m (address_of_value v1) in
-    let (vargs,l2) = eval_exprlist e m al in
-    let (vt3,l3) = eval_lvalue e m lhs in
-    (Callstate(fd,vargs,Kcall(Some vt3,f,e,k),m),l1@l2@l3)
-  | Ssequence(s1,s2), _ -> (State(f,s1,Kseq(s2,k),e,m),[])
+    let (vargs,l2) = eval_exprlist e m c al in
+    let (vt3,l3) = eval_lvalue e m c lhs in
+    (Callstate(fd,vargs,Kcall(Some vt3,f,e,k),m,c),l1@l2@l3)
+  | Ssequence(s1,s2), _ -> (State(f,s1,Kseq(s2,k),e,m,c),[])
   | Sifthenelse(a,s1,s2), _ -> 
-    let ((v1,_),l1) = eval_expr e m a in 
-    let a_true = (State(f,s1,k,e,m),l1) in
-    let a_false = (State(f,s2,k,e,m),l1) in
+    let ((v1,_),l1) = eval_expr e m c a in 
+    let a_true = (State(f,s1,k,e,m,c),l1) in
+    let a_false = (State(f,s2,k,e,m,c),l1) in
     condition v1 a_true a_false
-  | Swhile(a,s), _ ->
-    let ((v1,_),l1) = eval_expr e m a in 
-    let a_false = (State(f,Sskip,k,e,m),l1) in
-    let a_true = (State(f,s,Kwhile(a,s,k),e,m),l1) in
+  | Swhile(i,a,s), _ ->
+    CostLabel.enter_loop_opt c i;
+    let ((v1,_),l1) = eval_expr e m c a in 
+    let a_false = (State(f,Sskip,k,e,m,c),l1) in
+    let a_true = (State(f,s,Kwhile(i,a,s,k),e,m,c),l1) in
     condition v1 a_true a_false
-  | Sdowhile(a,s), _ -> (State(f,s,Kdowhile(a,s,k),e,m),[])
-  | Sfor(Sskip,a2,a3,s), _ ->
-    let ((v1,_),l1) = eval_expr e m a2 in 
-    let a_false = (State(f,Sskip,k,e,m),l1) in
-    let a_true = (State(f,s,Kfor2(a2,a3,s,k),e,m),l1) in
+  | Sdowhile(i,a,s), _ ->
+    CostLabel.enter_loop_opt c i;
+    (State(f,s,Kdowhile(i,a,s,k),e,m,c),[])
+  | Sfor(i,Sskip,a2,a3,s), _ ->
+    CostLabel.enter_loop_opt c i;
+    let ((v1,_),l1) = eval_expr e m c a2 in 
+    let a_false = (State(f,Sskip,k,e,m,c),l1) in
+    let a_true = (State(f,s,Kfor2(i,a2,a3,s,k),e,m,c),l1) in
     condition v1 a_true a_false
-  | Sfor(a1,a2,a3,s), _ -> (State(f,a1,Kseq(Sfor(Sskip,a2,a3,s),k),e,m),[])
-  | Sbreak, Kseq(s,k) -> (State(f,Sbreak,k,e,m),[])
-  | Sbreak, Kwhile(_,_,k) -> (State(f,Sskip,k,e,m),[])
-  | Sbreak, Kdowhile(_,_,k) -> (State(f,Sskip,k,e,m),[])
-  | Sbreak, Kfor2(_,_,_,k) -> (State(f,Sskip,k,e,m),[])
-  | Sbreak, Kswitch k -> (State(f,Sskip,k,e,m),[])
-  | Scontinue, Kseq(_,k) -> (State(f,Scontinue,k,e,m),[])
-  | Scontinue, Kwhile(a,s,k) -> (State(f,Swhile(a,s),k,e,m),[])
-  | Scontinue, Kdowhile(a,s,k) ->
-    let ((v1,_),l1) = eval_expr e m a in 
-    let a_false = (State(f,Sskip,k,e,m),l1) in
-    let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in
-    condition v1 a_true a_false
-  | Scontinue, Kfor2(a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
-  | Scontinue, Kswitch k -> (State(f,Scontinue,k,e,m),[])
+  | Sfor(i,a1,a2,a3,s), _ -> (State(f,a1,Kseq(Sfor(i,Sskip,a2,a3,s),k),e,m,c),[])
+  | Sbreak, Kseq(s,k) -> (State(f,Sbreak,k,e,m,c),[])
+  | Sbreak, Kwhile(_,_,_,k) | Sbreak, Kdowhile(_,_,_,k)
+  | Sbreak, Kfor2(_,_,_,_,k) | Sbreak, Kswitch k -> (State(f,Sskip,k,e,m,c),[])
+  | Scontinue, Kseq(_,k)
+  | Scontinue, Kswitch k -> (State(f,Scontinue,k,e,m,c),[])
   | Sreturn None, _ -> 
     let m' = free_local_env m e in
-    (Returnstate(Value.undef,(call_cont k),m'),[])
+    (Returnstate(Value.undef,(call_cont k),m',c),[])
   | Sreturn (Some a), _ -> 
-    let ((v1,_),l1) = eval_expr e m a  in
+    let ((v1,_),l1) = eval_expr e m c a  in
     let m' = free_local_env m e in
-    (Returnstate(v1,call_cont k,m'),l1)
+    (Returnstate(v1,call_cont k,m',c),l1)
   | Sswitch(a,sl), _ -> 
-    let ((v,_),l) = eval_expr e m a in
+    let ((v,_),l) = eval_expr e m c a in
     let n = Value.to_int v in
-    (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m),l)
-  | Slabel(lbl,s), _ -> (State(f,s,k,e,m),[])
-  | Scost(lbl,s), _ -> (State(f,s,k,e,m),[lbl])
+  (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m,c),l)
+  | Slabel(lbl,s), _ -> (State(f,s,k,e,m,c),[])
+  | Scost(lbl,s), _ ->
+    (* applying current indexing on label *)
+    let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in
+    (State(f,s,k,e,m,c),[lbl])
   | Sgoto lbl, _ ->
+    (* if we exit an indexed loop, we don't care. It should not be possible to *)
+    (* enter an indexed loop that is not the current one, so we do nothing *)
+    (* to loop indexes *)
     let (s', k') = find_label lbl f.fn_body (call_cont k) in
-    (State(f,s',k',e,m),[])
+    (State(f,s',k',e,m,c),[])
   | _ -> assert false (* should be impossible *)
 
@@ -546 +577 @@
 module InterpretExternal = Primitive.Interpret (Mem)
 
-let interpret_external k mem f args =
+let interpret_external k mem c f args =
   let (mem', v) = match InterpretExternal.t mem f args with
     | (mem', InterpretExternal.V vs) ->
@@ -552 +583 @@
       (mem', v)
     | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in
-  Returnstate (v, k, mem')
-
-let step_call args cont mem = function
+  Returnstate (v, k, mem',c)
+
+let step_call args cont mem c = function
   | Internal f -> 
     let (mem', e) = init_fun_env mem f.fn_params args f.fn_vars in
-    State (f, f.fn_body, cont, e, mem')
+    (* initializing loop indices *)
+    let c = CostLabel.new_const_ind c in
+    State (f, f.fn_body, cont, e, mem', c)
   | External(id,targs,tres) when List.length targs = List.length args -> 
-    interpret_external cont mem id args
+    interpret_external cont mem c id args
   | External(id,_,_) -> 
     error ("wrong size of arguments when calling external " ^ id ^ ".")
 
 let step = function
-  | State(f,stmt,k,e,m) -> eval_stmt f k e m stmt
-  | Callstate(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[])
-  | Returnstate(v,Kcall(None,f,e,k),m) -> (State(f,Sskip,k,e,m),[])
-  | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m) -> 
+  | State(f,stmt,k,e,m,c) -> eval_stmt f k e m stmt c
+  | Callstate(fun_def,vargs,k,m,c) -> (step_call vargs k m c fun_def,[])
+  | Returnstate(v,Kcall(None,f,e,k),m,c) ->
+    let c = CostLabel.forget_const_ind c in
+    (State(f,Sskip,k,e,m,c),[])
+  | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m,c) -> 
+    let c = CostLabel.forget_const_ind c in
     let m' = assign m v ty vv in
-    (State(f,Sskip,k,e,m'),[])
+    (State(f,Sskip,k,e,m',c),[])
   | _ -> error "state malformation."
 
@@ -603 +639 @@
     if debug then Printf.printf "Result = %s\n%!"
       (IntValue.Int32.to_string res) ;
-    (res, cost_labels) in
+    (res, List.rev cost_labels) in
   if debug then print_state state ;
   match state with
-    | Returnstate(v,Kstop,_) -> (* Explicit return in main *)
+    | Returnstate(v,Kstop,_,_) -> (* Explicit return in main *)
       print_and_return_result (compute_result v)
-    | State(_,Sskip,Kstop,_,_) -> (* Implicit return in main *)
+    | State(_,Sskip,Kstop,_,_,_) -> (* Implicit return in main *)
       print_and_return_result IntValue.Int32.zero
     | state -> exec debug cost_labels (step state)
@@ -618 +654 @@
     | Some main ->
       let mem = init_mem prog in
-      let first_state = (Callstate (find_fundef main mem,[],Kstop,mem),[]) in
+      let first_state = (Callstate (find_fundef main mem,[],Kstop,mem,[]),[]) in
       exec debug [] first_state

Deliverables/D2.2/8051/src/clight/clightLabelling.ml

@@ -1 +1 @@
 
 (** This module defines the labelling of a [Clight] program. *)
+
+module IntListSet = Set.Make(struct type t = int list let compare = compare end)
 
 open Clight
@@ -6 +8 @@
 
 
-(* Add a cost label in front of a statement. *)
-
-let add_starting_cost_label cost_universe stmt =
-  Clight.Scost (CostLabel.Gen.fresh cost_universe, stmt)
+(* Add a cost label in front of a statement with the current indexing. *)
+
+let add_starting_cost_label indexing cost_universe stmt =
+  Clight.Scost (CostLabel.fresh indexing cost_universe, stmt)
 
 (* Add a cost label at the end of a statement. *)
 
-let add_ending_cost_label cost_universe stmt =
-  Clight.Ssequence (stmt, add_starting_cost_label cost_universe Clight.Sskip)
+let add_ending_cost_label indexing cost_universe stmt =
+  let lbld_skip = add_starting_cost_label indexing cost_universe Clight.Sskip in
+  Clight.Ssequence (stmt, lbld_skip)
 
 
@@ -24 +27 @@
 
 
-let add_cost_label_e cost_universe e =
-  Expr (Ecost (CostLabel.Gen.fresh cost_universe, e), typeof e)
+let add_cost_label_e indexing cost_universe e =
+  Expr (Ecost (CostLabel.fresh indexing cost_universe, e), typeof e)
 
 
 (* Add cost labels to an expression. *)
 
-let rec add_cost_labels_e cost_universe = function  
-  | Expr (exp,cty) -> Expr (add_cost_labels_expr cost_universe exp,cty)
-
-and add_cost_labels_expr cost_universe exp = match exp with
+let rec add_cost_labels_e ind cost_universe = function  
+  | Expr (exp,cty) -> Expr (add_cost_labels_expr ind cost_universe exp,cty)
+
+and add_cost_labels_expr ind cost_universe exp = match exp with
   | Econst_int _ | Econst_float _ | Evar _ | Esizeof _ -> exp
-  | Ederef e -> Ederef (add_cost_labels_e cost_universe e)
-  | Eaddrof e -> Eaddrof (add_cost_labels_e cost_universe e)
-  | Eunop (op,e) -> Eunop (op,(add_cost_labels_e cost_universe e))
+  | Ederef e -> Ederef (add_cost_labels_e ind cost_universe e)
+  | Eaddrof e -> Eaddrof (add_cost_labels_e ind cost_universe e)
+  | Eunop (op,e) -> Eunop (op,(add_cost_labels_e ind cost_universe e))
   | Ebinop (op,e1,e2) ->
       Ebinop (op,
-              add_cost_labels_e cost_universe e1,
-              add_cost_labels_e cost_universe e2)
-  | Ecast (t,e) -> Ecast (t, add_cost_labels_e cost_universe e)
+              add_cost_labels_e ind cost_universe e1,
+              add_cost_labels_e ind cost_universe e2)
+  | Ecast (t,e) -> Ecast (t, add_cost_labels_e ind cost_universe e)
   | Eandbool (e1,e2) ->
-      let e1' = add_cost_labels_e cost_universe e1 in
-      let e2' = add_cost_labels_e cost_universe e2 in
-      let b1 = add_cost_label_e cost_universe (const_int 1) in
-      let b2 = add_cost_label_e cost_universe (const_int 0) in
+      let e1' = add_cost_labels_e ind cost_universe e1 in
+      let e2' = add_cost_labels_e ind cost_universe e2 in
+      let b1 = add_cost_label_e ind cost_universe (const_int 1) in
+      let b2 = add_cost_label_e ind cost_universe (const_int 0) in
       let e2' = Expr (Econdition (e2', b1, b2), int_type) in
-      let e2' = add_cost_label_e cost_universe e2' in
-      let e3' = add_cost_label_e cost_universe (const_int 0) in
+      let e2' = add_cost_label_e ind cost_universe e2' in
+      let e3' = add_cost_label_e ind cost_universe (const_int 0) in
       Econdition (e1', e2', e3')
   | Eorbool (e1,e2) ->
-      let e1' = add_cost_labels_e cost_universe e1 in
-      let e2' = add_cost_label_e cost_universe (const_int 1) in
-      let e3' = add_cost_labels_e cost_universe e2 in
-      let b1 = add_cost_label_e cost_universe (const_int 1) in
-      let b2 = add_cost_label_e cost_universe (const_int 0) in
+      let e1' = add_cost_labels_e ind cost_universe e1 in
+      let e2' = add_cost_label_e ind cost_universe (const_int 1) in
+      let e3' = add_cost_labels_e ind cost_universe e2 in
+      let b1 = add_cost_label_e ind cost_universe (const_int 1) in
+      let b2 = add_cost_label_e ind cost_universe (const_int 0) in
       let e3' = Expr (Econdition (e3', b1, b2), int_type) in
-      let e3' = add_cost_label_e cost_universe e3' in
+      let e3' = add_cost_label_e ind cost_universe e3' in
       Econdition (e1', e2', e3')
-  | Efield (e,id) -> Efield (add_cost_labels_e cost_universe e,id)
+  | Efield (e,id) -> Efield (add_cost_labels_e ind cost_universe e,id)
   | Econdition (e1,e2,e3) ->
-      let e1' = add_cost_labels_e cost_universe e1 in
-      let e2' = add_cost_labels_e cost_universe e2 in
-      let e2' = add_cost_label_e cost_universe e2' in
-      let e3' = add_cost_labels_e cost_universe e3 in
-      let e3' = add_cost_label_e cost_universe e3' in
+      let e1' = add_cost_labels_e ind cost_universe e1 in
+      let e2' = add_cost_labels_e ind cost_universe e2 in
+      let e2' = add_cost_label_e ind cost_universe e2' in
+      let e3' = add_cost_labels_e ind cost_universe e3 in
+      let e3' = add_cost_label_e ind cost_universe e3' in
       Econdition (e1', e2', e3')
   | Ecost (_,_) | Ecall _ -> assert false (* Should not happen *)
 
-let add_cost_labels_opt cost_universe = function
-  | None -> None
-  | Some e -> Some (add_cost_labels_e cost_universe e)
-
-let add_cost_labels_lst cost_universe l =
-  List.map (add_cost_labels_e cost_universe) l
+let add_cost_labels_opt ind cost_universe =
+  Option.map (add_cost_labels_e ind cost_universe) 
+
+let add_cost_labels_lst ind cost_universe l =
+  List.map (add_cost_labels_e ind cost_universe) l
 
 
 (* Add cost labels to a statement. *)
 
-let rec add_cost_labels_st cost_universe = function
+let update_ind i ind =
+  match i with
+    | None -> ind
+    | Some _ -> CostLabel.add_id_indexing ind
+
+let rec add_cost_labels_st ind cost_universe = function
   | Sskip -> Sskip
   | Sassign (e1,e2) ->
-      Sassign (add_cost_labels_e cost_universe e1,
-               add_cost_labels_e cost_universe e2)
+    Sassign (add_cost_labels_e ind cost_universe e1,
+             add_cost_labels_e ind cost_universe e2)
   | Scall (e1,e2,lst) ->
-      Scall (add_cost_labels_opt cost_universe e1,
-             add_cost_labels_e cost_universe e2,
-             add_cost_labels_lst cost_universe lst)
+    Scall (add_cost_labels_opt ind cost_universe e1,
+           add_cost_labels_e ind cost_universe e2,
+           add_cost_labels_lst ind cost_universe lst)
   | Ssequence (s1,s2) ->
-      Ssequence (add_cost_labels_st cost_universe s1,
-                 add_cost_labels_st cost_universe s2) 
+    Ssequence (add_cost_labels_st ind cost_universe s1,
+               add_cost_labels_st ind cost_universe s2)
   | Sifthenelse (e,s1,s2) ->
-      let s1' = add_cost_labels_st cost_universe s1 in
-      let s1' = add_starting_cost_label cost_universe s1' in
-      let s2' = add_cost_labels_st cost_universe s2 in
-      let s2' = add_starting_cost_label cost_universe s2' in
-      Sifthenelse (add_cost_labels_e cost_universe e, s1', s2')
-  | Swhile (e,s) ->
-      let s' = add_cost_labels_st cost_universe s in
-      let s' = add_starting_cost_label cost_universe s' in
-      add_ending_cost_label cost_universe
-        (Swhile (add_cost_labels_e cost_universe e, s'))
-  | Sdowhile (e,s) ->
-      let s = add_cost_labels_st cost_universe s in
-      let s' = add_starting_cost_label cost_universe s in
-      add_ending_cost_label cost_universe
-        (Sdowhile (add_cost_labels_e cost_universe e, s'))
-  | Sfor (s1,e,s2,s3) ->
-      let s1' = add_cost_labels_st cost_universe s1 in
-      let s2' = add_cost_labels_st cost_universe s2 in
-      let s3' = add_cost_labels_st cost_universe s3 in
-      let s3' = add_starting_cost_label cost_universe s3' in
-      add_ending_cost_label cost_universe
-        (Sfor (s1', add_cost_labels_e cost_universe e, s2', s3'))
-  | Sreturn e -> Sreturn (add_cost_labels_opt cost_universe e)
+    let s1' = add_cost_labels_st ind cost_universe s1 in
+    let s1' = add_starting_cost_label ind cost_universe s1' in
+    let s2' = add_cost_labels_st ind cost_universe s2 in
+    let s2' = add_starting_cost_label ind cost_universe s2' in
+    Sifthenelse (add_cost_labels_e ind cost_universe e, s1', s2')
+  | Swhile (i,e,s) ->
+    let ind' = update_ind i ind in
+    let s' = add_cost_labels_st ind' cost_universe s in
+    let s' = add_starting_cost_label ind' cost_universe s' in
+      (* exit label indexed with outside indexing *) 
+    add_ending_cost_label ind cost_universe
+      (Swhile (i,add_cost_labels_e ind cost_universe e, s'))
+  | Sdowhile (i,e,s) ->
+    let ind' = update_ind i ind in
+    let s' = add_cost_labels_st ind' cost_universe s in
+    let s' = add_starting_cost_label ind' cost_universe s' in
+    add_ending_cost_label ind cost_universe
+      (Sdowhile (i,add_cost_labels_e ind cost_universe e, s'))
+  | Sfor (i,s1,e,s2,s3) ->
+    let s1' = add_cost_labels_st ind cost_universe s1 in
+    let ind' = update_ind i ind in
+    let s2' = add_cost_labels_st ind' cost_universe s2 in
+    let s3' = add_cost_labels_st ind' cost_universe s3 in
+    let s3' = add_starting_cost_label ind' cost_universe s3' in
+    add_ending_cost_label ind cost_universe
+      (Sfor (i, s1', add_cost_labels_e ind cost_universe e, s2', s3'))
+  | Sreturn e -> Sreturn (add_cost_labels_opt ind cost_universe e)
   | Sswitch (e,ls) ->
-      Sswitch (add_cost_labels_e cost_universe e,
-               add_cost_labels_ls cost_universe ls)
+    Sswitch (add_cost_labels_e ind cost_universe e,
+             add_cost_labels_ls ind cost_universe ls)
   | Slabel (lbl,s) ->
-      let s' = add_cost_labels_st cost_universe s in
-      let s' = add_starting_cost_label cost_universe s' in
-      Slabel (lbl,s')
+    let s' = add_cost_labels_st ind cost_universe s in
+    let s' = add_starting_cost_label ind cost_universe s' in
+    Slabel (lbl,s')
   | Scost (_,_) -> assert false
   | _ as stmt -> stmt
 
-and add_cost_labels_ls cost_universe = function
+and add_cost_labels_ls ind cost_universe = function
   | LSdefault s ->
-      let s' = add_cost_labels_st cost_universe s in
-      let s' = add_starting_cost_label cost_universe s' in
+      let s' = add_cost_labels_st ind cost_universe s in
+      let s' = add_starting_cost_label ind cost_universe s' in
       LSdefault s'
   | LScase (i,s,ls) ->
-      let s' = add_cost_labels_st cost_universe s in
-      let s' = add_starting_cost_label cost_universe s' in
-      LScase (i, s', add_cost_labels_ls cost_universe ls)
-
-
-(* Add cost labels to a function. *)
-
-let add_cost_labels_f cost_universe = function
-  | (id,Internal fd) -> (id,Internal {
-      fn_return = fd.fn_return ;
-      fn_params = fd.fn_params ;
-      fn_vars = fd.fn_vars ;
-      fn_body = add_starting_cost_label cost_universe
-                             (add_cost_labels_st cost_universe fd.fn_body)
-    })
-  | (id,External (a,b,c)) -> (id,External (a,b,c))
-
+      let s' = add_cost_labels_st ind cost_universe s in
+      let s' = add_starting_cost_label ind cost_universe s' in
+      LScase (i, s', add_cost_labels_ls ind cost_universe ls)
+
+
+(* traversal of code assigning to every label the "loop address" of it. *)
+(* A loop address like [2, 0, 1] means the corresponding label is in the *)
+(* third loop inside the first loop inside the second loop of the body. *)
+let rec assign_loop_addrs_s
+    (current : int list)
+    (offset  : int)
+    (m       : int list Label.Map.t)
+    : Clight.statement -> int*int list Label.Map.t =
+  function
+      (* I am supposing you cannot jump to the update statement of for loops... *)
+    | Swhile(_,_,s) | Sdowhile(_,_,s) | Sfor(_,_,_,_,s) ->
+      let (_, m) = assign_loop_addrs_s (offset :: current) 0 m s in
+      (offset + 1, m)
+    | Ssequence(s1,s2) | Sifthenelse(_,s1,s2) ->
+      let (offset, m) = assign_loop_addrs_s current offset m s1 in
+      assign_loop_addrs_s current offset m s2
+    | Slabel(l,s) ->
+      let (offset, m) = assign_loop_addrs_s current offset m s in
+      (offset, Label.Map.add l current m)
+    | Sswitch(_,ls) -> assign_loop_addrs_ls current offset m ls
+    | _ -> (offset, m)
+
+and assign_loop_addrs_ls current offset m = function
+  | LSdefault s -> assign_loop_addrs_s current offset m s
+  | LScase(_,s,ls) ->
+    let (offset, m) = assign_loop_addrs_s current offset m s in
+    assign_loop_addrs_ls current offset m ls
+
+let rec is_prefix l1 l2 = match l1, l2 with
+  | [], _ -> true
+  | hd1 :: tl1, hd2 :: tl2 when hd1 = hd2 -> is_prefix tl1 tl2
+  | _ -> false
+
+(* traversal of code which for every statement [s] returns the set of loop*)
+(* addresses which are multi-entry due to a goto in [s]. *)
+let rec find_multi_entry_loops_s
+    (m       : int list Label.Map.t)
+    (current : int list)
+    (offset  : int)
+    : Clight.statement -> int*IntListSet.t =
+  function
+      (* I am supposing you cannot jump to the update statement of for loops... *)
+    | Swhile(_,_,s) | Sdowhile(_,_,s) | Sfor(_,_,_,_,s) ->
+      let current' = offset :: current in
+      let (_, set) = find_multi_entry_loops_s m current' 0 s in
+      (offset + 1, set)
+    | Ssequence(s1,s2) | Sifthenelse(_,s1,s2) ->
+      let (offset, set1) = find_multi_entry_loops_s m current offset s1 in
+      let (offset, set2) = find_multi_entry_loops_s m current offset s2 in
+      (offset, IntListSet.union set1 set2)
+    | Slabel(_,s) -> find_multi_entry_loops_s m current offset s
+    | Sgoto l ->
+        (* all labels should have a binding in m *)
+      let addr = Label.Map.find l m in
+      let cond = is_prefix addr current in
+      let set = if cond then IntListSet.empty else IntListSet.singleton addr in
+      (offset, set)   
+    | Sswitch(_,ls) -> find_multi_entry_loops_ls m current offset ls
+    | _ -> (offset, IntListSet.empty)
+
+and find_multi_entry_loops_ls m current offset = function
+  | LSdefault s -> find_multi_entry_loops_s m current offset s
+  | LScase(_,s,ls) ->
+    let (offset, set1) = find_multi_entry_loops_s m current offset s in
+    let (offset, set2) = find_multi_entry_loops_ls m current offset ls in
+    (offset, IntListSet.union set1 set2)
+      
+(* final pass where loops are indexed *)
+let rec index_loops_s multi_entry current offset depth = function
+  (* I am supposing you cannot jump to the update statement of for loops... *)
+  | Swhile(_,b,s) ->
+    let current' = offset :: current in
+    let is_bad = IntListSet.mem current' multi_entry in 
+    let i, depth = if is_bad then None, depth else Some depth, depth + 1 in 
+    let (_, s) = index_loops_s multi_entry current' 0 depth s in 
+    (offset + 1, Swhile(i,b,s))
+  | Sdowhile(_,b,s) ->
+    let current' = offset :: current in
+    let is_bad = IntListSet.mem current' multi_entry in 
+    let i, depth = if is_bad then None, depth else Some depth, depth + 1 in 
+    let (_, s) = index_loops_s multi_entry current' 0 depth s in 
+    (offset + 1, Sdowhile(i,b,s))
+  | Sfor(_,a1,a2,a3,s) ->
+    let current' = offset :: current in
+    let is_bad = IntListSet.mem current' multi_entry in 
+    let i, depth = if is_bad then None, depth else Some depth, depth + 1 in 
+    let (_, s) = index_loops_s multi_entry current' 0 depth s in 
+    (offset + 1, Sfor(i,a1,a2,a3,s))
+  | Ssequence(s1,s2) ->
+    let (offset, s1) = index_loops_s multi_entry current offset depth s1 in
+    let (offset, s2) = index_loops_s multi_entry current offset depth s2 in
+    (offset, Ssequence(s1,s2))
+  | Sifthenelse(b,s1,s2) ->
+    let (offset, s1) = index_loops_s multi_entry current offset depth s1 in
+    let (offset, s2) = index_loops_s multi_entry current offset depth s2 in
+    (offset, Sifthenelse(b,s1,s2))
+  | Slabel(l,s) ->
+    let (offset, s) = index_loops_s multi_entry current offset depth s in
+    (offset, Slabel(l, s))
+  | Sswitch(v,ls) ->
+    let (offset, s) = index_loops_ls multi_entry current offset depth ls in
+    (offset, Sswitch(v, ls))
+  | _ as s -> (offset, s)
+
+and index_loops_ls multi_entry current offset depth = function
+  | LSdefault s ->
+    let (offset, s) =
+      index_loops_s multi_entry current offset depth s in
+    (offset, LSdefault s)
+  | LScase(v,s,ls) ->
+    let (offset, s) = index_loops_s multi_entry current offset depth s in
+    let (offset, ls) = index_loops_ls multi_entry current offset depth ls in
+    (offset, LScase(v,s,ls))
+
+(* Index loops and introduce cost labels in functions *)
+let process_f cost_universe = function
+  | (id,Internal fd) ->
+    let body = fd.fn_body in
+    (* assign loop addresses to labels *)
+    let (_, m) = assign_loop_addrs_s [] 0 Label.Map.empty body in
+    (* find which loops are potentially multi-entry *)
+    let (_, multi_entry) = find_multi_entry_loops_s m [] 0 body in
+    (* index loops accordingly *)
+    let (_, body) = index_loops_s multi_entry [] 0 0 body in
+    (* initialize indexing *)
+    let ind = CostLabel.empty_indexing in
+    (* add cost labels inside *)
+    let body = add_cost_labels_st ind cost_universe body in
+    (* add cost label in front *)
+    let body = add_starting_cost_label ind cost_universe body in 
+    (id,Internal {fd with fn_body = body})
+  | _ as x -> x
+        
+          
 
 (** [add_cost_labels prog] inserts some labels to enable
@@ -156 +289 @@
 let add_cost_labels p =
   let labs = ClightAnnotator.all_labels p in
-  let labs = StringTools.Set.fold CostLabel.Set.add labs CostLabel.Set.empty in
-  let cost_prefix = CostLabel.Gen.fresh_prefix labs "_cost" in
-  let cost_universe = CostLabel.Gen.new_universe cost_prefix in
-  {
-    prog_funct = List.map (add_cost_labels_f cost_universe) p.prog_funct;
-    prog_main = p.prog_main;
-    prog_vars = p.prog_vars
-  }
+  let add = CostLabel.Atom.Set.add in
+  let empty = CostLabel.Atom.Set.empty in
+  let labs = StringTools.Set.fold add labs empty in
+  let cost_prefix = CostLabel.Atom.Gen.fresh_prefix labs "_cost" in
+  let cost_universe = CostLabel.Atom.Gen.new_universe cost_prefix in
+  {p with prog_funct = List.map (process_f cost_universe) p.prog_funct}

Deliverables/D2.2/8051/src/clight/clightParser.mli

@@ -1 @@
-
 (** This module implements a parser for [C] based on [gcc] and
     [CIL]. *)

Deliverables/D2.2/8051/src/clight/clightPrinter.ml

@@ -196 +196 @@
   | Efield(e1, id) ->
       fprintf p "%a.%s" print_expr_prec (level, e1) id
-  | Ecost (lbl,e1) ->
-      fprintf p "(/* %s */ %a)" lbl print_expr e1
-  | Ecall (f, arg, e) ->
+  | Ecost(lbl, e1) ->
+    (* printing label uglily even if in comment for consistence *)
+    let lbl = CostLabel.string_of_cost_label lbl in
+    fprintf p "(/* %s */ %a)" lbl print_expr e1
+  | Ecall(f, arg, e) ->
       fprintf p "(%s(%a), %a)" f print_expr arg print_expr e
 
@@ -214 +216 @@
       print_expr p e1;
       print_expr_list p (false, et)
+
+let print_loop_depth p = function
+  | None -> fprintf p ""
+  | Some x -> fprintf p "/* single entry loop depth: %d */@," x 
 
 let rec print_stmt p s =
@@ -241 +247 @@
               print_stmt s1
               print_stmt s2
-  | Swhile(e, s) ->
-      fprintf p "@[<v 2>while (%a) {@ %a@;<0 -2>}@]"
-              print_expr e
-              print_stmt s
-  | Sdowhile(e, s) ->
-      fprintf p "@[<v 2>do {@ %a@;<0 -2>} while(%a);@]"
-              print_stmt s
-              print_expr e
-  | Sfor(s_init, e, s_iter, s_body) ->
-      fprintf p "@[<v 2>for (@[<hv 0>%a;@ %a;@ %a) {@]@ %a@;<0 -2>}@]"
-              print_stmt_for s_init
-              print_expr e
-              print_stmt_for s_iter
-              print_stmt s_body
+  | Swhile(i, e, s) ->
+    fprintf p "@[<v 0>%a@[<v 2>while (%a) {@ %a@;<0 -2>}@]@]"
+      print_loop_depth i
+      print_expr e
+      print_stmt s
+  | Sdowhile(i, e, s) ->
+    fprintf p "@[<v 0>%a@[<v 2>do {@ %a@;<0 -2>} while(%a);@]@]"
+      print_loop_depth i
+      print_stmt s
+      print_expr e
+  | Sfor(i, s_init, e, s_iter, s_body) ->
+    fprintf p "@[<v 0>%a@[<v 2>for (@[<hv 0>%a;@ %a;@ %a) {@]@ %a@;<0 -2>}@]@]"
+      print_loop_depth i
+      print_stmt_for s_init
+      print_expr e
+      print_stmt_for s_iter
+      print_stmt s_body
   | Sbreak ->
-      fprintf p "break;"
+    fprintf p "break;"
   | Scontinue ->
-      fprintf p "continue;"
+    fprintf p "continue;"
   | Sswitch(e, cases) ->
-      fprintf p "@[<v 2>switch (%a) {@ %a@;<0 -2>}@]"
-              print_expr e
-              print_cases cases
+    fprintf p "@[<v 2>switch (%a) {@ %a@;<0 -2>}@]"
+      print_expr e
+      print_cases cases
   | Sreturn None ->
-      fprintf p "return;"
+    fprintf p "return;"
   | Sreturn (Some e) ->
-      fprintf p "return %a;" print_expr e
+    fprintf p "return %a;" print_expr e
   | Slabel(lbl, s1) ->
-      fprintf p "%s:@ %a" lbl print_stmt s1
+    fprintf p "%s:@ %a" lbl print_stmt s1
   | Sgoto lbl ->
-      fprintf p "goto %s;" lbl
- | Scost (lbl,s1) ->
+    fprintf p "goto %s;" lbl
+  | Scost (lbl,s1) ->
+    let lbl = CostLabel.string_of_cost_label lbl in
      fprintf p "%s:@ %a" lbl print_stmt s1
 
@@ -468 +478 @@
   | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2
   | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2
-  | Swhile(e, s) -> collect_expr e; collect_stmt s
-  | Sdowhile(e, s) -> collect_stmt s; collect_expr e
-  | Sfor(s_init, e, s_iter, s_body) ->
-      collect_stmt s_init; collect_expr e;
-      collect_stmt s_iter; collect_stmt s_body
+  | Swhile(_, e, s) -> collect_expr e; collect_stmt s
+  | Sdowhile(_, e, s) -> collect_stmt s; collect_expr e
+  | Sfor(_, s_init, e, s_iter, s_body) ->
+    collect_stmt s_init; collect_expr e;
+    collect_stmt s_iter; collect_stmt s_body
   | Sbreak -> ()
   | Scontinue -> ()

Deliverables/D2.2/8051/src/clight/clightToCminor.ml

@@ -495 +495 @@
     AST.res = ret_type }
 
-let f_stmt fresh var_locs stmt sub_exprs_res sub_stmts_res =
-  let (tmps, sub_stmts_res) = List.split sub_stmts_res in
-  let tmps = List.flatten tmps in
-
-  let (added_tmps, stmt) = match stmt, sub_exprs_res, sub_stmts_res with
-
-    | Clight.Sskip, _, _ -> ([], Cminor.St_skip)
-
-    | Clight.Sassign (e1, _), _ :: e2 :: _, _ ->
+let ind_0 i stmt = match i with
+  | None -> stmt
+  | Some x -> Cminor.St_ind_0(x, stmt)
+
+let ind_inc i stmt = match i with
+  | None -> stmt
+  | Some x -> Cminor.St_ind_inc(x, stmt)
+
+let trans_for =
+  let f_expr e _ = e in
+  let f_stmt stmt expr_res stmt_res = match expr_res, stmt_res, stmt with
+    | e::_, s1::s2::s3::_, Clight.Sfor(i,_,_,_,_) ->
+      Clight.Ssequence(s1,Clight.Swhile(i,e,
+                                        Clight.Ssequence(s3, s2)))
+    | exprs, sub_sts, stm ->
+      ClightFold.statement_fill_subs stm exprs sub_sts in
+  ClightFold.statement2 f_expr f_stmt
+
+let cmp_complement = function
+  | AST.Cmp_eq -> AST.Cmp_ne
+  | AST.Cmp_ne -> AST.Cmp_eq
+  | AST.Cmp_gt -> AST.Cmp_le
+  | AST.Cmp_ge -> AST.Cmp_lt
+  | AST.Cmp_lt -> AST.Cmp_ge
+  | AST.Cmp_le -> AST.Cmp_gt
+
+let negate_expr (Cminor.Expr (_, et) as e) =
+  let ed' = Cminor.Op1 (AST.Op_notbool, e) in
+  Cminor.Expr(ed', et)
+
+let rec translate_stmt fresh var_locs cnt_lbl br_lbl = function
+
+    | Clight.Sskip -> ([], Cminor.St_skip)
+
+    | Clight.Sassign (e1, e2) ->
+      let e2 = translate_expr var_locs e2 in
       ([], assign var_locs e1 e2)
 
-    | Clight.Scall (None, _, _), f :: args, _ ->
+    | Clight.Scall (None, f, args) ->
+      let f = translate_expr var_locs f in
+      let args = List.map (translate_expr var_locs) args in
       ([], Cminor.St_call (None, f, args, call_sig AST.Type_void args))
 
-    | Clight.Scall (Some e, _, _), _ :: f :: args, _ ->
+    | Clight.Scall (Some e, f, args) ->
+      let f = translate_expr var_locs f in
+      let args = List.map (translate_expr var_locs) args in
       let t = sig_type_of_ctype (clight_type_of e) in
       let tmp = fresh () in
@@ -518 +549 @@
       ([(tmp, t)], Cminor.St_seq (stmt_call, stmt_assign))
 
-    | Clight.Swhile _, e :: _, stmt :: _ ->
-      let econd =
-        Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in
+    | Clight.Swhile (i,e,stmt) ->
+      let loop_lbl = fresh () in
+      let llbl_opt = Some loop_lbl in
+      let exit_lbl = fresh () in
+      let elbl_opt = Some exit_lbl in
+      let (tmps, stmt) = translate_stmt fresh var_locs llbl_opt elbl_opt stmt in
+      let e = translate_expr var_locs e in
+      let jmp lbl = Cminor.St_goto lbl in
+      (* let econd = negate_expr e in *)
       let scond =
-        Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in
-      ([],
-       Cminor.St_block (Cminor.St_loop (Cminor.St_seq (scond,
-                                                       Cminor.St_block stmt))))
-
-    | Clight.Sdowhile _, e :: _, stmt :: _ ->
-      let econd =
-        Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in
+        Cminor.St_ifthenelse (e, Cminor.St_skip, jmp exit_lbl) in
+      let loop =
+        Cminor.St_seq(scond,Cminor.St_seq (stmt, ind_inc i (jmp loop_lbl))) in
+      let loop = ind_0 i (Cminor.St_label(loop_lbl,loop)) in
+      (tmps, Cminor.St_seq (loop, Cminor.St_label(exit_lbl,Cminor.St_skip)))
+        
+    | Clight.Sdowhile (i,e,stmt) ->
+      let loop_lbl = fresh () in
+      let llbl_opt = Some loop_lbl in
+      let exit_lbl = fresh () in
+      let elbl_opt = Some exit_lbl in
+      let (tmps, stmt) = translate_stmt fresh var_locs llbl_opt elbl_opt stmt in
+      let e = translate_expr var_locs e in
+      let jmp lbl = Cminor.St_goto lbl in
       let scond =
-        Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in
-      ([],
-       Cminor.St_block (Cminor.St_loop (Cminor.St_seq (Cminor.St_block stmt,
-                                                       scond))))
-
-    | Clight.Sfor _, e :: _, stmt1 :: stmt2 :: stmt3 :: _ ->
-      let econd = 
-        Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in
-      let scond =
-        Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in
-      let body = Cminor.St_seq (Cminor.St_block stmt3, stmt2) in
-      ([],
-       Cminor.St_seq (stmt1,
-                      Cminor.St_block
-                        (Cminor.St_loop (Cminor.St_seq (scond, body)))))
-
-    | Clight.Sifthenelse _, e :: _, stmt1 :: stmt2 :: _ ->
-      ([], Cminor.St_ifthenelse (e, stmt1, stmt2))
-
-    | Clight.Ssequence _, _, stmt1 :: stmt2 :: _ ->
-      ([], Cminor.St_seq (stmt1, stmt2))
-
-    | Clight.Sbreak, _, _ -> ([], Cminor.St_exit 1)
-
-    | Clight.Scontinue, _, _ -> ([], Cminor.St_exit 0)
-
-    | Clight.Sswitch _, _, _ ->
+        Cminor.St_ifthenelse (e, ind_inc i (jmp loop_lbl), Cminor.St_skip) in
+      let loop =
+        Cminor.St_seq (stmt, scond) in
+      let loop = ind_0 i (Cminor.St_label(loop_lbl,loop)) in
+      (tmps, Cminor.St_seq (loop, Cminor.St_label(exit_lbl,Cminor.St_skip)))
+        
+    | Clight.Sfor _ -> assert false (* transformed *)
+
+    | Clight.Sifthenelse (e, stmt1, stmt2) ->
+      let (tmps1, stmt1) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt1 in
+      let (tmps2, stmt2) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt2 in
+      let e = translate_expr var_locs e in
+      (tmps1 @ tmps2, Cminor.St_ifthenelse (e, stmt1, stmt2))
+
+    | Clight.Ssequence(stmt1,stmt2) ->
+      let (tmps1, stmt1) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt1 in
+      let (tmps2, stmt2) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt2 in
+      (tmps1 @ tmps2, Cminor.St_seq (stmt1, stmt2))
+
+    | Clight.Sbreak -> 
+      let br_lbl = match br_lbl with
+        | Some x -> x
+        | None -> invalid_arg("break without enclosing scope") in
+      ([], Cminor.St_goto br_lbl)
+
+    | Clight.Scontinue ->
+      let cnt_lbl = match cnt_lbl with
+        | Some x -> x
+        | None -> invalid_arg("continue without enclosing scope") in
+      ([], Cminor.St_goto cnt_lbl)
+    | Clight.Sswitch _ ->
       (* Should not appear because of switch transformation performed
          beforehand. *)
       assert false
 
-    | Clight.Sreturn None, _, _ -> ([], Cminor.St_return None)
-
-    | Clight.Sreturn (Some _), e :: _, _ -> ([], Cminor.St_return (Some e))
-
-    | Clight.Slabel (lbl, _), _, stmt :: _ -> ([], Cminor.St_label (lbl, stmt))
-
-    | Clight.Sgoto lbl, _, _ -> ([], Cminor.St_goto lbl)
-
-    | Clight.Scost (lbl, _), _, stmt :: _ -> ([], Cminor.St_cost (lbl, stmt))
-
-    | _ -> assert false (* type error *) in
-
-  (tmps @ added_tmps, stmt)
-
-let translate_statement fresh var_locs =
-  ClightFold.statement2 (f_expr var_locs) (f_stmt fresh var_locs)
+    | Clight.Sreturn None -> ([], Cminor.St_return None)
+
+    | Clight.Sreturn (Some e) ->
+      let e = translate_expr var_locs e in
+      ([], Cminor.St_return (Some e))
+
+    | Clight.Slabel (lbl, stmt) ->
+      let (tmps, stmt) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt in
+      (tmps, Cminor.St_label (lbl, stmt))
+
+    | Clight.Sgoto lbl -> ([], Cminor.St_goto lbl)
+
+    | Clight.Scost (lbl, stmt) ->
+      let (tmps, stmt) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt in
+      (tmps, Cminor.St_cost (lbl, stmt))
+
+(*    | _ -> assert false (* type error *) *)
 
 
@@ -598 +646 @@
   let params =
     List.map (fun (x, t) -> (x, sig_type_of_ctype t)) cfun.Clight.fn_params in
-  let (tmps, body) = translate_statement fresh var_locs cfun.Clight.fn_body in
+  let body = cfun.Clight.fn_body in
+  let body = trans_for body in
+  let (tmps, body) = translate_stmt fresh var_locs None None body in
   let body = add_stack_parameters_initialization var_locs body in
   { Cminor.f_return = type_return_of_ctype cfun.Clight.fn_return ;

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

@@ -34 +34 @@
   | St_seq of statement * statement
   | St_ifthenelse of expression * statement * statement
-  | St_loop of statement
+(*  | St_loop of statement
   | St_block of statement
-  | St_exit of int
+  | St_exit of int *)
 
   (* Switch. Parameters are the expression whose value is switch, a
-     table of cases and their corresponding number of blocks to exit,
-     and the number of block to exit in the default case. *)
-  | St_switch of expression * (int*int) list * int
+     table of cases and their corresponding labels to go to,
+     and the label to go to in the default case. *)
+  | St_switch of expression * (int*Label.t) list * Label.t
 
   | St_return of expression option
   | St_label of AST.ident * statement
-  | St_goto of string
+  | St_goto of Label.t
   | St_cost of CostLabel.t * statement
+  | St_ind_0 of CostLabel.index * statement
+  | St_ind_inc of CostLabel.index * statement
 
 

Deliverables/D2.2/8051/src/cminor/cminorAnnotator.ml

@@ -204 +204 @@
 let all_labels p =
   let (cost_labels, user_labels) = prog_labels p in
-  let all =
-    CostLabel.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls)
-      cost_labels StringTools.Set.empty in
+  let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in
+  let all = CostLabel.Set.fold f cost_labels StringTools.Set.empty in
   Label.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) user_labels all

Deliverables/D2.2/8051/src/cminor/cminorFold.ml

@@ -31 +31 @@
 
 let statement_subs = function
-  | Cminor.St_skip | Cminor.St_exit _ | Cminor.St_return None
+  | Cminor.St_skip | (*Cminor.St_exit _ |*) Cminor.St_return None
   | Cminor.St_goto _ -> ([], [])
   | Cminor.St_assign (_, e) | Cminor.St_switch (e, _, _)
@@ -43 +43 @@
   | Cminor.St_ifthenelse (e, stmt1, stmt2) ->
     ([e], [stmt1 ; stmt2])
-  | Cminor.St_loop stmt | Cminor.St_block stmt
-  | Cminor.St_label (_, stmt) | Cminor.St_cost (_, stmt) ->
+  (*| Cminor.St_loop stmt | Cminor.St_block stmt *)
+  | Cminor.St_label (_, stmt) | Cminor.St_cost (_, stmt)
+  | Cminor.St_ind_0 (_, stmt) | Cminor.St_ind_inc (_, stmt) ->
     ([], [stmt])
 
 let statement_fill_subs stmt sub_es sub_stmts =
   match stmt, sub_es, sub_stmts with
-    | (  Cminor.St_skip | Cminor.St_exit _ | Cminor.St_return None
+    | (  Cminor.St_skip | (*Cminor.St_exit _ |*) Cminor.St_return None
        | Cminor.St_goto _), _, _ -> stmt
     | Cminor.St_assign (x, _), e :: _, _ ->
@@ -67 +68 @@
     | Cminor.St_ifthenelse _, e :: _, stmt1 :: stmt2 :: _ ->
       Cminor.St_ifthenelse (e, stmt1, stmt2)
-    | Cminor.St_loop _, _, stmt :: _ ->
+ (*   | Cminor.St_loop _, _, stmt :: _ ->
       Cminor.St_loop stmt
     | Cminor.St_block _, _, stmt :: _ ->
-      Cminor.St_block stmt
+      Cminor.St_block stmt *)
     | Cminor.St_label (lbl, _), _, stmt :: _ ->
       Cminor.St_label (lbl, stmt)
     | Cminor.St_cost (lbl, _), _, stmt :: _ ->
       Cminor.St_cost (lbl, stmt)
+    | Cminor.St_ind_0 (i, _), _, stmt :: _ ->
+      Cminor.St_ind_0 (i, stmt)
+    | Cminor.St_ind_inc (i, _), _, stmt :: _ ->
+      Cminor.St_ind_inc (i, stmt)
     | _ -> assert false (* do not use on these arguments *)
 

Deliverables/D2.2/8051/src/cminor/cminorInterpret.ml

@@ -23 +23 @@
 (* State of execution *)
 
+type indexing = CostLabel.const_indexing
+
 type continuation = 
     Ct_stop
   | Ct_cont of statement*continuation
-  | Ct_endblock of continuation
+(*  | Ct_endblock of continuation *)
   | Ct_returnto of
       ident option*internal_function*Val.address*local_env*continuation
@@ -32 +34 @@
 type state = 
     State_regular of
-      internal_function*statement*continuation*Val.address*local_env*(function_def Mem.memory)
-  | State_call of function_def*Val.t list*continuation*(function_def Mem.memory)
-  | State_return of Val.t*continuation*(function_def Mem.memory)
+      internal_function*statement*continuation*Val.address*local_env*
+                         (function_def Mem.memory)*indexing list
+  | State_call of function_def*Val.t list*continuation*
+             (function_def Mem.memory)*indexing list
+  | State_return of Val.t*continuation*(function_def Mem.memory)*indexing list
 
 let string_of_local_env lenv =
@@ -57 +61 @@
   | St_seq _ -> "sequence"
   | St_ifthenelse (e, _, _) -> "if (" ^ (string_of_expr e) ^ ")"
-  | St_loop _ -> "loop"
+(*  | St_loop _ -> "loop"
   | St_block _ -> "block"
-  | St_exit n -> "exit " ^ (string_of_int n)
+  | St_exit n -> "exit " ^ (string_of_int n) *)
   | St_switch (e, _, _) -> "switch (" ^ (string_of_expr e) ^ ")"
   | St_return None -> "return"
@@ -65 +69 @@
   | St_label (lbl, _) -> "label " ^ lbl
   | St_goto lbl -> "goto " ^ lbl
-  | St_cost (lbl, _) -> "cost " ^ lbl
+  | St_cost (lbl, _) ->
+    let lbl = CostLabel.string_of_cost_label lbl in
+    "cost " ^ lbl
+  | St_ind_0 (i, _) -> "reset " ^ string_of_int i ^ " to 0"
+  | St_ind_inc (i, _) -> "post-increment " ^ string_of_int i
 
 let print_state = function
-  | State_regular (_, stmt, _, sp, lenv, mem) ->
-    Printf.printf "Local environment:\n%s\n\nMemory:%s\nStack pointer: %s\n\nRegular state: %s\n\n%!"
+  | State_regular (_, stmt, _, sp, lenv, mem, i) ->
+    Printf.printf "Local environment:\n%s\n\nMemory:%s\nStack pointer: %s\nIndexing:"
       (string_of_local_env lenv)
       (Mem.to_string mem)
-      (Val.to_string (value_of_address sp))
+      (Val.to_string (value_of_address sp));
+    let ind = CostLabel.curr_const_ind i in
+    CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) ind;
+    Printf.printf "\nRegular state: %s\n\n%!"
       (string_of_statement stmt)
-  | State_call (_, args, _, mem) ->
+  | State_call (_, args, _, mem,_) ->
     Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!"
       (Mem.to_string mem)
       (MiscPottier.string_of_list " " Val.to_string args)
-  | State_return (v, _, mem) ->
+  | State_return (v, _, mem,_) ->
     Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
       (Mem.to_string mem)
@@ -221 +232 @@
 
 let rec callcont = function
-    Ct_stop                     -> Ct_stop
-  | Ct_cont(_,k)                -> callcont k
-  | Ct_endblock(k)              -> callcont k
-  | Ct_returnto(a,b,c,d,e)      -> Ct_returnto(a,b,c,d,e)
+  | Ct_cont(_,k) (*| Ct_endblock k *) -> callcont k
+  | (Ct_stop | Ct_returnto _) as k -> k
 
 let findlabel lbl st k = 
@@ -243 +252 @@
          | Some(v) -> Some(v)
       )
-  | St_loop(s)                     -> fdlbl (Ct_cont(St_loop(s),k)) s
-  | St_block(s)                    -> fdlbl (Ct_endblock(k)) s
-  | St_exit(_)                     -> None
-  | St_switch(_,_,_)               -> None
-  | St_return(_)                   -> None
-  | St_label(l,s) when l = lbl     -> Some((s,k))
-  | St_goto(_)                     -> None
-  | St_cost (_,s) | St_label (_,s) -> fdlbl k s
+(*  | St_loop(s)                  -> fdlbl (Ct_cont(St_loop(s),k)) s
+  | St_block(s)                 -> fdlbl (Ct_endblock(k)) s
+  | St_exit(_)                  -> None *)
+  | St_switch(_,_,_)            -> None
+  | St_return(_)                -> None
+  | St_label(l,s) when l = lbl  -> Some((s,k))
+  | St_goto(_)                  -> None
+  | St_cost(_,s)  | St_label(_,s)
+  | St_ind_0(_,s) | St_ind_inc(_,s) -> fdlbl k s
   in match fdlbl k st with
       None -> assert false (*Wrong label*)
@@ -256 +266 @@
 
 
-let call_state sigma e m f params cont =
+let call_state sigma e m i f params cont =
   let (addr,l1) = eval_expression sigma e m f in
   let fun_def = Mem.find_fun_def m (address_of_value addr) in
   let (args,l2) = eval_exprlist sigma e m params in
-  (State_call(fun_def,args,cont,m),l1@l2)
-
-let eval_stmt f k sigma e m s = match s, k with
-  | St_skip,Ct_cont(s,k) -> (State_regular(f, s, k, sigma, e, m),[])
-  | St_skip,Ct_endblock(k) -> (State_regular(f, St_skip, k, sigma, e, m),[])
+  (State_call(fun_def,args,cont,m,i),l1@l2)
+
+let eval_stmt f k sigma e m i s = match s, k with
+  | St_skip,Ct_cont(s,k) -> (State_regular(f, s, k, sigma, e, m, i),[])
+(*  | St_skip,Ct_endblock(k) -> (State_regular(f, St_skip, k, sigma, e, m, i),[]) *)
   | St_skip, (Ct_returnto _ as k) ->
-    (State_return (Val.undef,k,Mem.free m sigma),[])
+    (State_return (Val.undef,k,Mem.free m sigma,i),[])
   | St_skip,Ct_stop -> 
-    (State_return (Val.undef,Ct_stop,Mem.free m sigma),[])
+    (State_return (Val.undef,Ct_stop,Mem.free m sigma,i),[])
   | St_assign(x,exp),_ -> 
     let (v,l) = eval_expression sigma e m exp in
     let e = LocalEnv.add x v e in
-    (State_regular(f, St_skip, k, sigma, e, m),l)
+    (State_regular(f, St_skip, k, sigma, e, m, i),l)
   | St_store(q,a1,a2),_ ->
     let (v1,l1) = eval_expression sigma e m a1 in
     let (v2,l2) = eval_expression sigma e m a2 in
     let m = Mem.storeq m q (address_of_value v1) v2 in
-    (State_regular(f, St_skip, k, sigma, e, m),l1@l2)
+    (State_regular(f, St_skip, k, sigma, e, m, i),l1@l2)
   | St_call(xopt,f',params,_),_ ->
-    call_state sigma e m f' params (Ct_returnto(xopt,f,sigma,e,k))
+    call_state sigma e m i f' params (Ct_returnto(xopt,f,sigma,e,k))
   | St_tailcall(f',params,_),_ -> 
-    call_state sigma e m f' params (callcont k)
-  | St_seq(s1,s2),_ -> (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m),[])
+    call_state sigma e m i f' params (callcont k)
+  | St_seq(s1,s2),_ -> (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m, i),[])
   | St_ifthenelse(exp,s1,s2),_ ->
     let (v,l) = eval_expression sigma e m exp in
@@ -290 +300 @@
         if Val.is_false v then s2
         else error "undefined conditional value." in
-      (State_regular(f,next_stmt,k,sigma,e,m),l)
-  | St_loop(s),_ -> (State_regular(f,s,Ct_cont((St_loop s),k),sigma,e,m),[])
-  | St_block(s),_ -> (State_regular(f,s,(Ct_endblock k),sigma,e,m),[])
-  | St_exit(n),Ct_cont(s,k) -> (State_regular(f,(St_exit n),k,sigma,e,m),[])
-  | St_exit(0),Ct_endblock(k) -> (State_regular(f,St_skip,k,sigma,e,m),[])
+      (State_regular(f,next_stmt,k,sigma,e,m,i),l)
+(*  | St_loop(s),_ -> (State_regular(f,s,Ct_cont((St_loop s),k),sigma,e,m,i),[])
+  | St_block(s),_ -> (State_regular(f,s,(Ct_endblock k),sigma,e,m,i),[])
+  | St_exit(n),Ct_cont(s,k) -> (State_regular(f,(St_exit n),k,sigma,e,m,i),[])
+  | St_exit(0),Ct_endblock(k) -> (State_regular(f,St_skip,k,sigma,e,m,i),[])
   | St_exit(n),Ct_endblock(k) ->
-    (State_regular(f,(St_exit (n-1)),k,sigma,e,m),[])
-  | St_label(_,s),_ -> (State_regular(f,s,k,sigma,e,m),[])
-  | St_goto(lbl),_ -> 
+    (State_regular(f,(St_exit (n-1)),k,sigma,e,m,i),[]) *)
+  | St_label(_,s),_ -> (State_regular(f,s,k,sigma,e,m,i),[])
+  | St_goto(lbl),_ ->
     let (s2,k2) = findlabel lbl f.f_body (callcont k) in
-    (State_regular(f,s2,k2,sigma,e,m),[])
+    (State_regular(f,s2,k2,sigma,e,m,i),[])
   | St_switch(exp,lst,def),_ ->
     let (v,l) = eval_expression sigma e m exp in
     if Val.is_int v then
       try
-        let i = Val.to_int v in
-        let nb_exit =
-          if List.mem_assoc i lst then List.assoc i lst
-          else def in
-        (State_regular(f, St_exit nb_exit,k, sigma, e, m),l)
+        let v = Val.to_int v in
+        let lbl =
+          try
+            List.assoc v lst
+          with
+            | Not_found -> def in
+        let (s',k') = findlabel lbl f.f_body (callcont k) in
+        (State_regular(f, s', k', sigma, e, m, i),l)
       with _ -> error "int value too big."
     else error "undefined switch value."
   | St_return(None),_ ->
-    (State_return (Val.undef,callcont k,Mem.free m sigma),[])
+    (State_return (Val.undef,callcont k,Mem.free m sigma,i),[])
   | St_return(Some(a)),_ ->
       let (v,l) = eval_expression sigma e m a in
-      (State_return (v,callcont k,Mem.free m sigma),l)
-  | St_cost(lbl,s),_ -> (State_regular(f,s,k,sigma,e,m),[lbl])
-  | _ -> error "state malformation."
+      (State_return (v,callcont k,Mem.free m sigma,i),l)
+  | St_cost(lbl,s),_ ->
+    (* applying current indexing on label *)
+    let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind i) lbl in
+    (State_regular(f,s,k,sigma,e,m,i),[lbl])
+  | St_ind_0(ind,s),_ ->
+    CostLabel.enter_loop i ind;
+    (State_regular(f,s,k,sigma,e,m,i), [])
+  | St_ind_inc(ind,s),_ ->
+    CostLabel.continue_loop i ind;
+    (State_regular(f,s,k,sigma,e,m,i), [])
+(*  | _ -> error "state malformation." *)
 
 
 module InterpretExternal = Primitive.Interpret (Mem)
 
-let interpret_external k mem f args =
+let interpret_external k mem i f args =
   let (mem', v) = match InterpretExternal.t mem f args with
     | (mem', InterpretExternal.V vs) ->
@@ -329 +351 @@
       (mem', v)
     | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in
-  State_return (v, k, mem')
-
-let step_call vargs k m = function
+  State_return (v, k, mem', i)
+
+let step_call vargs k m i = function
   | F_int f ->
     let (m, sp) = Mem.alloc m (concrete_stacksize f.f_stacksize) in
     let lenv = init_local_env vargs f.f_params f.f_vars in
-    State_regular(f,f.f_body,k,sp,lenv,m)
-  | F_ext f -> interpret_external k m f.ef_tag vargs
+    let i = CostLabel.new_const_ind i in 
+    State_regular(f,f.f_body,k,sp,lenv,m,i)
+  | F_ext f -> interpret_external k m i f.ef_tag vargs
 
 let step = function
-  | State_regular(f,stmt,k,sp,e,m) -> eval_stmt f k sp e m stmt
-  | State_call(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[])
-  | State_return(v,Ct_returnto(None,f,sigma,e,k),m) ->
-    (State_regular(f,St_skip,k,sigma,e,m),[])
-  | State_return(v,Ct_returnto(Some x,f,sigma,e,k),m) ->
+  | State_regular(f,stmt,k,sp,e,m,i) -> eval_stmt f k sp e m i stmt
+  | State_call(fun_def,vargs,k,m,i) -> (step_call vargs k m i fun_def,[])
+  | State_return(v,Ct_returnto(None,f,sigma,e,k),m,i) ->
+    let i = CostLabel.forget_const_ind i in
+    (State_regular(f,St_skip,k,sigma,e,m,i),[])
+  | State_return(v,Ct_returnto(Some x,f,sigma,e,k),m,i) ->
     let e = LocalEnv.add x v e in
-    (State_regular(f,St_skip,k,sigma,e,m),[])
+    let i = CostLabel.forget_const_ind i in
+    (State_regular(f,St_skip,k,sigma,e,m,i),[])
   | _ -> error "state malformation."
 
@@ -364 +389 @@
     if debug then Printf.printf "Result = %s\n%!"
       (IntValue.Int32.to_string res) ;
-    (res, cost_labels) in
+    (res, List.rev cost_labels) in
   if debug then print_state state ;
   match state with
-    | State_return(v,Ct_stop,_) -> (* Explicit return in main *)
+    | State_return(v,Ct_stop,_,_) -> (* Explicit return in main *)
       print_and_return_result (compute_result v)
-    | State_regular(_,St_skip,Ct_stop,_,_,_) -> (* Implicit return in main *)
+    | State_regular(_,St_skip,Ct_stop,_,_,_,_) -> (* Implicit return in main *)
       print_and_return_result IntValue.Int32.zero
     | state -> exec debug cost_labels (step state)
@@ -379 +404 @@
     | Some main ->
       let mem = init_mem prog in
-      let first_state = (State_call (find_fundef main mem,[],Ct_stop,mem),[]) in
+      let main = find_fundef main mem in
+      let first_state = (State_call (main,[],Ct_stop,mem,[]),[]) in
       exec debug [] first_state

Deliverables/D2.2/8051/src/cminor/cminorPrinter.ml

@@ -116 +116 @@
         (add_parenthesis e3)
   | Cminor.Exp_cost (lab, e) ->
+      let lab = CostLabel.string_of_cost_label lab in
       Printf.sprintf "/* %s */ %s" lab (print_expression e)
 and add_parenthesis (Cminor.Expr (ed, _) as e) = match ed with
@@ -136 +137 @@
 let print_table n =
   let f s (case, exit) =
-    Printf.sprintf "%s%scase %d: exit %d;\n" s (n_spaces n) case exit
+    Printf.sprintf "%s%scase %d: goto %s;\n" s (n_spaces n) case exit
   in
   List.fold_left f ""
@@ -171 +172 @@
         (Primitive.print_sig sg)
   | Cminor.St_seq (s1, s2) -> (print_body n s1) ^ (print_body n s2)
+  | Cminor.St_ifthenelse (e, s1, Cminor.St_skip) ->
+    Printf.sprintf "%sif (%s) {\n%s%s}\n"
+    (n_spaces n)
+    (print_expression e)
+    (print_body (n+2) s1)
+    (n_spaces n)
   | Cminor.St_ifthenelse (e, s1, s2) ->
       Printf.sprintf "%sif (%s) {\n%s%s}\n%selse {\n%s%s}\n"
@@ -180 +187 @@
         (print_body (n+2) s2)
         (n_spaces n)
-  | Cminor.St_loop s ->
+(*  | Cminor.St_loop s ->
       Printf.sprintf "%sloop {\n%s%s}\n"
         (n_spaces n)
@@ -191 +198 @@
         (n_spaces n)
   | Cminor.St_exit i ->
-      Printf.sprintf "%sexit %d;\n" (n_spaces n) i
+      Printf.sprintf "%sexit %d;\n" (n_spaces n) i *)
   | Cminor.St_switch (e, tbl, dflt) ->
-      Printf.sprintf "%sswitch (%s) {\n%s%sdefault: exit %d;\n%s}\n"
+      Printf.sprintf "%sswitch (%s) {\n%s%sdefault: goto %s;\n%s}\n"
         (n_spaces n)
         (print_expression e)
@@ -208 +215 @@
       Printf.sprintf "%sgoto %s;\n" (n_spaces n) lbl
   | Cminor.St_cost (lbl, s) ->
-      Printf.sprintf "%s%s:\n%s"
-        (n_spaces n) lbl (print_body n s)
+      let lbl = CostLabel.string_of_cost_label lbl in
+      Printf.sprintf "%s%s:\n%s" (n_spaces n) lbl (print_body n s)
+  | Cminor.St_ind_0 (i, s) ->
+      Printf.sprintf "%sindex %d:\n%s" (n_spaces n) i (print_body n s)
+  | Cminor.St_ind_inc (i,s) ->
+      Printf.sprintf "%sincrement %d:\n%s\n" (n_spaces n) i (print_body n s)
 
 let print_internal f_name f_def =
@@ -246 +257 @@
   | Cminor.St_seq(_,_) -> "seq"
   | Cminor.St_ifthenelse(_,_,_) -> "ifthenelse"
-  | Cminor.St_loop(_) -> "loop"
+(*  | Cminor.St_loop(_) -> "loop"
   | Cminor.St_block(_) -> "block"
-  | Cminor.St_exit(_) -> "exit"
+  | Cminor.St_exit(_) -> "exit" *)
   | Cminor.St_switch(_,_,_) -> "switch"
   | Cminor.St_return(_) -> "return"
@@ -254 +265 @@
   | Cminor.St_goto(_) -> "goto"
   | Cminor.St_cost(_,_) -> "cost"
+  | Cminor.St_ind_0 _ -> "index"
+  | Cminor.St_ind_inc _ -> "increment"

Deliverables/D2.2/8051/src/cminor/cminorToRTLabs.ml

@@ -194 +194 @@
       let (rtlabs_fun, r2) = choose_destination rtlabs_fun lenv e2 in
       let old_entry = rtlabs_fun.RTLabs.f_entry in
-      let stmt = RTLabs.St_op2 (op2, destr, r1, r2, old_entry) in
+      let r1_arg = RTLabs.Reg r1 in
+      let r2_arg = RTLabs.Reg r2 in
+      let stmt = RTLabs.St_op2 (op2, destr, r1_arg, r2_arg, old_entry) in
       let rtlabs_fun = generate rtlabs_fun stmt in
       translate_exprs rtlabs_fun lenv [r1 ; r2] [e1 ; e2]
@@ -201 +203 @@
       let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in
       let old_entry = rtlabs_fun.RTLabs.f_entry in
-      let stmt = RTLabs.St_load (chunk, r, destr, old_entry) in
+      let stmt =
+        RTLabs.St_load (chunk, RTLabs.Reg r, destr, old_entry) in
       let rtlabs_fun = generate rtlabs_fun stmt in
       translate_expr rtlabs_fun lenv r e
@@ -269 +272 @@
     (rtlabs_fun : RTLabs.internal_function)
     (lenv       : local_env)
-    (exits      : Label.t list)
+(*    (exits      : Label.t list) *)
     (stmt       : Cminor.statement)
     : RTLabs.internal_function =
@@ -283 +286 @@
       let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e2 in
       let old_entry = rtlabs_fun.RTLabs.f_entry in
-      let stmt = RTLabs.St_store (chunk, addr, r, old_entry) in
+      let stmt =
+        RTLabs.St_store (chunk, RTLabs.Reg addr, RTLabs.Reg r, old_entry) in
       let rtlabs_fun = generate rtlabs_fun stmt in
       translate_exprs rtlabs_fun lenv [addr ; r] [e1 ; e2]
@@ -321 +325 @@
 
     | Cminor.St_seq (s1, s2) ->
-      let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s2 in
-      translate_stmt rtlabs_fun lenv exits s1
+      let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s2 in
+      translate_stmt rtlabs_fun lenv (*exits*) s1
 
     | Cminor.St_ifthenelse (e, s1, s2) ->
       let old_entry = rtlabs_fun.RTLabs.f_entry in
-      let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s2 in
+      let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s2 in
       let lbl_false = rtlabs_fun.RTLabs.f_entry in
       let rtlabs_fun = change_entry rtlabs_fun old_entry in
-      let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s1 in
+      let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s1 in
       let lbl_true = rtlabs_fun.RTLabs.f_entry in
       translate_branch rtlabs_fun lenv e lbl_true lbl_false
 
-    | Cminor.St_loop s ->
+(*    | Cminor.St_loop s ->
       let loop_start = fresh_label rtlabs_fun in
       let rtlabs_fun = change_entry rtlabs_fun loop_start in
@@ -345 +349 @@
 
     | Cminor.St_exit n ->
-      change_entry rtlabs_fun (List.nth exits n)
+      change_entry rtlabs_fun (List.nth exits n) *)
 
     | Cminor.St_return eopt ->
@@ -362 +366 @@
 
     | Cminor.St_label (lbl, s) ->
-      let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s in
+      let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s in
       let old_entry = rtlabs_fun.RTLabs.f_entry in
       add_graph rtlabs_fun lbl (RTLabs.St_skip old_entry)
 
     | Cminor.St_cost (lbl, s) ->
-      let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s in
+      let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s in
       let old_entry = rtlabs_fun.RTLabs.f_entry in
       generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry))
+
+    | Cminor.St_ind_0 (i, s) ->
+      let rtlabs_fun = translate_stmt rtlabs_fun lenv s in
+      let old_entry = rtlabs_fun.RTLabs.f_entry in
+      generate rtlabs_fun (RTLabs.St_ind_0 (i, old_entry))
+
+    | Cminor.St_ind_inc (i, s) ->
+      let rtlabs_fun = translate_stmt rtlabs_fun lenv s in
+      let old_entry = rtlabs_fun.RTLabs.f_entry in
+      generate rtlabs_fun (RTLabs.St_ind_inc (i, old_entry))
 
     | Cminor.St_goto lbl ->
@@ -446 +460 @@
 
   (* Complete the graph *)
-  translate_stmt rtlabs_fun lenv [] f_def.Cminor.f_body
+  translate_stmt rtlabs_fun lenv (*[]*) f_def.Cminor.f_body
 
 

Deliverables/D2.2/8051/src/common/costLabel.ml

@@ +1 @@
+module Atom =
+  struct
+    include StringTools
+  end
 
-include StringTools
+module StringMap = Map.Make(String)
+
+(** Simple expressions are for now affine maps of the form a*_+b *)
+type sexpr =
+    | Sexpr of int*int
+
+let is_const_sexpr (Sexpr(a, _)) = (a = 0)
+
+let sexpr_id = Sexpr(1, 0)
+
+let const_sexpr n = Sexpr(0, n)
+
+type index = int
+
+let make_id prefix depth = prefix ^ string_of_int depth
+
+type indexing = sexpr list
+
+type const_indexing = int ExtArray.t
+
+let const_ind_iter = ExtArray.iter
+
+let curr_const_ind = function
+    | hd :: _ -> hd
+    | _ -> invalid_arg "curr_const_ind applied to non-empty list"
+
+let init_const_indexing () = ExtArray.make ~buff:1 0 0 
+
+let enter_loop_single indexing n = ExtArray.set indexing n 0
+
+let continue_loop_single indexing n =
+  try
+    ExtArray.set indexing n (ExtArray.get indexing n + 1)
+  with | _ ->
+    invalid_arg "uninitialized loop index" 
+
+let curr_ind = function
+    | hd :: _ -> hd
+    | _ -> invalid_arg "non-empty indexing stack"
+
+let enter_loop inds = enter_loop_single (curr_ind inds)
+
+let continue_loop inds = continue_loop_single (curr_ind inds)
+
+let enter_loop_opt indexing = Option.iter (enter_loop indexing) 
+
+let continue_loop_opt indexing = Option.iter (continue_loop indexing)
+
+let new_const_ind inds = init_const_indexing () :: inds
+
+let forget_const_ind = function
+        | _ :: inds -> inds
+        | _ -> invalid_arg "non-empty indexing stack"
+
+let sexpr_of i l = 
+    try
+        List.nth l i
+    with
+                        | Failure _
+      | Invalid_argument _ -> invalid_arg "costLabel.sexpr_of"
+
+let empty_indexing = []
+
+let add_id_indexing ind = sexpr_id :: ind
+
+(* a*_+b is composed with c*_+d by substitution: *)
+(* namely a*_+b ° c*_+d = c*(a*_+b)+d              *)
+let compose_sexpr (Sexpr(a, b)) (Sexpr(c, d)) =
+    Sexpr (a * c, b * c + d)
+                
+let ev_sexpr i (Sexpr(a, b)) = a*i+b
+
+(* i|-->e ° I *)
+let rec compose_index_indexing i s l = match i, l with
+        | 0, s' :: l' -> compose_sexpr s s' :: l'
+        | x, s' :: l' -> s' :: compose_index_indexing (i-1) s l'
+        | _ -> l 
+
+
+(* I°J applies every mapping in I to every mapping in J *)
+let rec compose_indexing m n = match m, n with
+        | s1 :: l1, s2 :: l2 -> compose_sexpr s1 s2 :: compose_indexing l1 l2
+        | _ -> n  
+
+let rec compose_const_indexing_i i c = function
+        | [] -> []
+        | s :: l ->
+                let head =
+                        (* if s is constant leave it be. In particular, avoid raising the error *)
+                        if is_const_sexpr s then s else
+                        try
+                          const_sexpr (ev_sexpr (ExtArray.get c i) s) 
+                        with
+                                | Invalid_argument _ ->
+                                        invalid_arg "constant indexing not enough to be applied" in
+          head :: compose_const_indexing_i (i+1) c l 
+
+module IndexingSet = Set.Make(struct
+    type t = indexing
+                let compare = compare
+        end)
+
+type t = {
+    name : Atom.t;
+    i : indexing
+}
+
+let comp_index i s lbl =
+        {lbl with i = compose_index_indexing i s lbl.i}
+
+let ev_indexing c lbl =
+    {lbl with i = compose_const_indexing_i 0 c lbl.i}
+
+
+(* if [pretty] is false then a name suitable for labels is given*)
+(* ('P' replaces '+') *)
+let string_of_sexpr pretty prefix i (Sexpr(a, b)) =
+        let plus = if pretty then "+" else "P" in
+        let id = prefix ^ string_of_int i in
+  let a_id_s = if a = 1 then id else string_of_int a ^ id in
+        let b_s = string_of_int b in
+        if a = 0 then b_s else
+        if b = 0 then a_id_s else a_id_s ^ plus ^ b_s
+        
+(* examples:*)
+(* [pretty] true:  (0,i1+1,2i2+2)*)
+(* [pretty] false: _0_i1P1_2i2P2 *)
+let rec string_of_indexing_tl pretty prefix i = function
+        | [] -> if pretty then ")" else ""
+        | hd :: tl ->
+                let sep = if pretty then "," else "_" in
+                let str = string_of_sexpr pretty prefix i hd in
+                sep ^ str ^ string_of_indexing_tl pretty prefix (i+1) tl
+
+let string_of_indexing pretty prefix = function
+        | [] -> ""
+        | hd :: tl ->
+                let start = if pretty then "(" else "_" in
+    let str = string_of_sexpr pretty prefix 0 hd in
+                start ^ str ^ string_of_indexing_tl pretty prefix 1 tl
+                
+let string_of_cost_label ?(pretty = false) lab =
+        lab.name ^ string_of_indexing pretty "i" lab.i
+
+let fresh l universe =
+        {name = Atom.Gen.fresh universe; i = l}  
+
+(* TODO: urgh. Necessary? *)
+type aux_t = t
+                                                        
+(** labels are endowed with a lexicographical ordering *)
+module T : Map.OrderedType with type t = aux_t =
+    struct
+        type t = aux_t
+        let compare = compare (* uses the built-in lexicographical comparison *) 
+    end
+
+module Map = Map.Make(T)   
+module Set = Set.Make(T) 
+(** [constant_map d x] produces a finite map which associates 
+    [x] to every element of the set [d]. *)
+
+let indexings_of atom s =
+        let f k accu = if k.name = atom then IndexingSet.add k.i accu else accu in
+        Set.fold f s IndexingSet.empty
 
 let constant_map d x = 

Deliverables/D2.2/8051/src/common/costLabel.mli

@@ -1 +1 @@
 
-(** This module provides functions to manipulate and create fresh cost
+(** This module provides functions to manipulate and create indexed cost
     labels. *)
 
-include StringSig.S
+(** [Atom] provides functions for cost atoms, the root of indexed costs *)
+module Atom : sig
+  include StringSig.S
+end
+
+(** Simple expressions corresponding to loop tranformations. 
+    TODO: abstract or not? *)
+type sexpr = Sexpr of int*int
+
+(** The identity simple expression, used in initialization. *)
+val sexpr_id : sexpr
+
+(** Indexes are identified with (single-entry) loop depths. *)
+type index = int
+
+(** [make_id prefix index] produces an identifier out of a
+    prefix and a loop depth. *)
+val make_id : string -> index -> string
+
+type indexing = sexpr list
+
+(** The type of constant indexings, to be used by interpreations *)
+type const_indexing
+
+(** [const_ind_iter f c] iterates [f] over the values of indexes in c *)
+val const_ind_iter : (int -> unit) -> const_indexing -> unit
+
+(** This is equivalent to [List.hd], but raises
+    [Invalid_argument "non-empty indexing stack"] if argument is empty *)
+val curr_const_ind : const_indexing list -> const_indexing
+
+(** [enter_loop inds n] is used to update the indexing stack [ind] when one
+    is entering a loop indexed by [n]. Raises [Invalid_argument
+    "non-empty indexing stack"] if [inds] is empty. *)
+val enter_loop : const_indexing list -> index -> unit
+
+(** [enter_loop_opt inds (Some n)] behaves like [enter_loop inds n], and does
+    nothing in case of [None].
+    @see enter_loop *)
+val enter_loop_opt : const_indexing list -> index option -> unit 
+
+(** [continue_loop inds n] is used to update the indexing stack [inds] when
+    one is continuing a loop indexed by [n].
+    @raise [Invalid_argument "non-empty indexing stack"] if [inds] is empty.
+    @raise [Invalid_argument "uninitialized loop index"] if the head of
+    [inds] has no value for [index]. *)
+val continue_loop : const_indexing list -> index -> unit
+
+(** [continue_loop_opt inds (Some n)] behaves like [continue_loop inds n], and
+    does nothing in case of [None].
+    @see continue_loop *)
+val continue_loop_opt : const_indexing list -> index option -> unit
+
+(** [new_const_ind inds] pushes a new empty constant indexing on top of the
+    stack [inds]. *) 
+val new_const_ind : const_indexing list -> const_indexing list
+
+(** [forget_const_ind inds] pops and discards the top constant indexing from the
+    stack [inds].  Raises [Invalid_argument "non-empty indexing stack"] if
+    [inds] is empty. *) 
+val forget_const_ind : const_indexing list -> const_indexing list
+
+(** [empty_indexing] is the empty indexing *) 
+val empty_indexing : indexing
+
+(** [add_id_indexing ind] adds an identity mapping in front of ind **)
+val add_id_indexing : indexing -> indexing
+
+module IndexingSet : Set.S with type elt = indexing
+
+type t = {
+  name : Atom.t;
+  i : indexing
+}
+
+(** [comp_index i s lbl] gives back the label [lbl] where index [i] is remapped
+    to the simple expression [s]. *)
+val comp_index : index -> sexpr -> t -> t
+
+(** [ev_indexing ind lbl] returns [lbl] where its indexing has been
+    evaluated in the constant indexing [ind].
+    @raise  Invalid_argument "constant indexing not enough to be applied" if
+    [ind] does not contain enough mappings to evaluate [lbl]'s indexing. *)
+val ev_indexing : const_indexing -> t -> t
+
+(** [string_of_cost_label pref t] converts an indexed label to a
+    string suitable for a label name in C source. 
+    [string_of_cost_label ~pretty:true t] prints a more readable form *)
+val string_of_cost_label : ?pretty : bool -> t -> string
+
+(** [fresh i u] creates a fresh label using [u] as name universe, inside
+    the indexing [i] (which represents the nested loops containing the label) *)
+val fresh : indexing -> Atom.Gen.universe -> t
+
+module Set : Set.S with type elt = t
+module Map : Map.S with type key = t
+
+(** [indexings_of a s] produces the set of indexings of an atom [a] occurring
+    in the set of indexed labels [s]. *)
+val indexings_of : Atom.t -> Set.t -> IndexingSet.t
 
 (** [constant_map d x] produces a finite map which associates 

Deliverables/D2.2/8051/src/common/label.ml

@@ -1 +1 @@
 
 include StringTools
+
+module ImpMap = struct
+
+  type key =
+      Map.key
+  
+  type 'data t =
+      'data Map.t ref
+      
+  let create () =
+    ref Map.empty
+
+  let clear t =
+    t := Map.empty
+    
+  let add k d t =
+    t := Map.add k d !t
+
+  let find k t =
+    Map.find k !t
+
+  let iter f t =
+    Map.iter f !t
+
+end

Deliverables/D2.2/8051/src/common/label.mli

@@ -4 +4 @@
 
 include StringSig.S
+
+(** Imperative label maps for use with Fix *)
+module ImpMap : (Fix.IMPERATIVE_MAPS with type key = t)

Deliverables/D2.2/8051/src/languages.ml

@@ -35 +35 @@
   | AstLIN    of LIN.program
   | AstASM    of ASM.program
+
+type transformation = name * (ast -> ast) 
 
 let language_of_ast = function
@@ -136 +138 @@
 ]
 
-let compile debug src tgt = 
-  (* Find the maximal suffix of the chain that starts with the
-     language [src]. *)
-  let rec subchain = function
-    | [] -> 
-      (* The chain is assumed to be well-formed: such a suffix 
-         exists. *)
-      assert false 
-    | ((l, _, _) :: _) as chain when l = src -> chain
-    | _ :: chain -> subchain chain
-  in
+let insert_transformations ts chain =
+  (* turn transformation into elements of the compilation chain *)
+  let trans_to_comp (n, t) = (n, n, t) in
+  let ts = List.map trans_to_comp ts in
+  (* ts and chain are merged, and then sorted so that the resulting list is *)
+  (* still a well formed compilation chain. Stable sort preserves order *)
+  (* between transformations on the same language as appearing in ts *)
+  let compare (n1, n2, s) (m1, m2, t) = compare (n1, n2) (m1, m2) in
+  List.stable_sort compare (ts @ chain)
+
+let compile debug ts src tgt =
+  (* insert intermediate transformations *) 
+  let chain = insert_transformations ts compilation_chain in
+  (* erase transformations whose source is strictly before src *)
+  let chain = List.filter (function (l1, _, _) -> l1 >= src) chain in
+  (* erase transformations whose target is strictly after tgt *)
+  let chain = List.filter (function (_, l2, _) -> l2 <= tgt) chain in
   (* Compose the atomic translations to build a compilation function
      from [src] to [tgt]. Again, we assume that the compilation chain
@@ -153 +161 @@
      translation from [src] to [tgt]. *)
   let rec compose iprogs src tgt chains ast = 
-    if src = tgt then List.rev (ast :: iprogs)
-    else 
-      match chains with
-        | [] -> 
+    match chains with
+        | [] when src = tgt -> List.rev (ast :: iprogs)
+        | [] ->  
           Error.global_error "During compilation configuration"
             (Printf.sprintf "It is not possible to compile from `%s' to `%s'."
@@ -168 +175 @@
           ast :: l2_to_tgt iprog
   in
-  compose [] src tgt (subchain compilation_chain)
+  compose [] src tgt chain
 
 
@@ -210 +217 @@
 
 (* FIXME *)
-let instrument costs_mapping = function
+let instrument cost_tern costs_mapping = function
   | AstClight p ->
     let (p', cost_id, cost_incr, extern_cost_variables) =
-      ClightAnnotator.instrument p costs_mapping in
+      ClightAnnotator.instrument cost_tern p costs_mapping in
     (AstClight p', cost_id, cost_incr, extern_cost_variables)
 (*
@@ -227 +234 @@
     (p, "", "", StringTools.Map.empty)
 
-let annotate input_ast final =
+let annotate cost_tern input_ast final = 
   let costs_mapping = compute_costs final in 
-  instrument costs_mapping input_ast
+  instrument cost_tern costs_mapping input_ast
 
 let string_output asm_pretty = function

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

@@ -30 +30 @@
   | AstASM     of ASM.program
 
+
+(** The type of additional transfromations, with the language they take place 
+    in and the actual transformation *)
+type transformation = name * (ast -> ast)
+
 (** [language_of_ast ast] returns the programming language of the 
     abstract syntax tree [ast]. *)
@@ -41 +46 @@
 (** {2 Compilation} *)
 
-(** [compile debug l1 l2] returns the compilation function that
-    translates the language [l1] to the language [l2]. This may be the
+(** [compile debug ts l1 l2] returns the compilation function that
+    translates the language [l1] to the language [l2], employing the
+    transformations in [ts] along the way . This may be the
     composition of several compilation functions. If [debug] is
     [true], all the intermediate programs are inserted in the
     output. *)
-val compile : bool -> name -> name -> (ast -> ast list)
+val compile : bool -> transformation list -> name -> name -> (ast -> ast list)
 
 (** [add_runtime ast] adds runtime functions for the operations not supported by
@@ -66 +72 @@
 val labelize : ast -> ast
 
-(** [annotate input_ast target_ast] inserts cost annotations into the input AST
-    from the (final) target AST. It also returns the name of the cost variable,
-    the name of the cost increment function, and a the name of a fresh
-    uninitialized global variable for each external function. *)
-val annotate : ast -> ast -> (ast * string * string * string StringTools.Map.t)
+(** [annotate cost_tern input_ast target_ast] inserts cost annotations into the
+    input AST from the (final) target AST. It also returns the name of the cost
+    variable and the name of the cost increment function, and a the name of a fresh
+    uninitialized global variable for each external function. The [cost_tern] flag
+    rules whether cost increments are given by ternary expressions or branch
+    statements. *)
+val annotate : bool -> ast -> ast -> (ast * string * string * string StringTools.Map.t)
 
 (** [interpret debug ast] runs the program [ast] from the default initial

Deliverables/D2.2/8051/src/options.ml

@@ -48 +48 @@
 let is_debug_enabled ()         = !debug_flag
 
+let transformations = ref []
+let add_transformation t () = transformations := !transformations @ [t]
+let add_transformations ts () = transformations := !transformations @ ts
+let get_transformations () = !transformations
+
+let cost_ternary_flag           = ref true
+let set_cost_ternary            = (:=) cost_ternary_flag
+let is_cost_ternary_enabled ()  = !cost_ternary_flag
+
 let asm_pretty_flag             = ref false
 let set_asm_pretty              = (:=) asm_pretty_flag
@@ -79 +88 @@
 let set_lustre_test_max_int     = (:=) lustre_test_max_int
 let get_lustre_test_max_int ()  = !lustre_test_max_int
+
 
 (*
@@ -89 +99 @@
 let set_dev_test                = (:=) dev_test
 let is_dev_test_enabled ()      = !dev_test
+
+let help_specify_opt_stage (trans : Languages.transformation) =
+        Printf.sprintf "(done at the %s stage)." (Languages.to_string (fst trans)) 
+
+let basic_optimizations =
+  [
+    LoopPeeling.trans;
+    ConstPropagation.trans;
+    CopyPropagation.trans;
+    RedundancyElimination.trans;
+    CopyPropagation.trans;
+    RedundancyElimination.trans
+  ]
+ 
 
 let options = OptionsParsing.register [
@@ -148 +172 @@
   extra_doc " [default is 1000]";
 
+  "-peel", Arg.Unit (add_transformation LoopPeeling.trans),
+  " Apply loop peeling " ^
+    help_specify_opt_stage LoopPeeling.trans;
+
+  "-cst-prop", Arg.Unit (add_transformation ConstPropagation.trans),
+  " Apply constant propagation " ^
+    help_specify_opt_stage ConstPropagation.trans;
+
+  "-cpy-prop", Arg.Unit (add_transformation CopyPropagation.trans),
+  " Apply copy propagation " ^
+    help_specify_opt_stage CopyPropagation.trans;
+
+  "-pre", Arg.Unit (add_transformation RedundancyElimination.trans),
+  " Apply partial redundancy elimination " ^
+    help_specify_opt_stage RedundancyElimination.trans;
+
+  "-unroll-for",
+  Arg.Int (fun i -> add_transformation (LoopUnrolling.trans ~factor:i ()) ()),
+  " Apply loop unrolling, specifying factor " ^
+  help_specify_opt_stage (LoopUnrolling.trans ());
+
+  "-unroll", Arg.Unit (add_transformation (LoopUnrolling.trans ())),
+  " Apply loop unrolling " ^
+  help_specify_opt_stage (LoopUnrolling.trans ());
+
+  "-O", Arg.Unit (add_transformations basic_optimizations),
+  " Apply some optimizations.";
+
+  "-no-cost-tern",  Arg.Clear cost_ternary_flag,
+  " Replace cost ternary expressions with equivalent branch statements.";
+  
 (*
   "-res", Arg.Set print_result_flag,

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

@@ -32 +32 @@
 val is_debug_enabled : unit -> bool
 
+(** {2 Cost ternary expressions} *)
+val is_cost_ternary_enabled : unit -> bool
+
 (** {2 Assembly pretty print} *)
 val set_asm_pretty : bool -> unit
@@ -64 +67 @@
 val get_lustre_test_max_int : unit -> int
 
+
+(** {2 Intermediate transformations } *)
+val get_transformations : unit -> Languages.transformation list
 (*
 (** {2 Print results requests} *)