Changeset 1310 for Deliverables/D2.2

Timestamp:

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

Author:

tranquil

Message:

• finished changes on annotator
• implementing indexes in interpreter

Location:

Deliverables/D2.2/8051-indexed-labels-branch/src

Files:

• clight/clightAnnotator.ml (modified) (4 diffs)
• clight/clightInterpret.ml (modified) (8 diffs)
• common/costLabel.ml (modified) (4 diffs)
• common/costLabel.mli (modified) (2 diffs)

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

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

Deliverables/D2.2/8051-indexed-labels-branch/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
+  | State of cfunction*statement*continuation*localEnv*memory*indexing
   | Callstate of fundef*Value.t list*continuation*memory
   | Returnstate of Value.t*continuation*memory
@@ -113 +114 @@
   "(" ^ (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
   | Sskip -> "skip"
@@ -121 +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"
@@ -159 +170 @@
 
 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
 
@@ -178 +189 @@
       | 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)
@@ -468 +480 @@
   else error "undefined condition guard value."
 
-let eval_stmt f k e m s = match s, k with
+(** FIXME: modifying here! *)
+let eval_stmt f k e m s c = 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) ->
+  | Sskip, Kwhile(i,a,s,k) as w ->
+                (* possibly continuing a loop *)
+                let c = continue_loop i c in
+    let ((v1,_),l1) = eval_expr e m a in 
+    let a_false = (State(f,Sskip,k,e,m,c),l1) in
+    let a_true = (State(f,s,w,e,m,c),l1) in
+    condition v1 a_true a_false
+  | Sskip, Kdowhile(i,a,s,k) as w ->
+    let c = continue_loop i c in
     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 a_false = (State(f,Sskip,k,e,m,c),l1) in
+    let a_true = (State(f,s,w,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, Kfor3(i,a2,a3,s,k) -> (State(f,Sfor(i,Sskip,a2,a3,s),k,e,m),[])
+  | Sskip, Kfor2(i,a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
   | Sskip, Kswitch k -> (State(f,Sskip,k,e,m),[])
   | Sskip, Kcall _ -> 
@@ -509 +529 @@
     condition v1 a_true a_false
   | Sdowhile(a,s), _ -> (State(f,s,Kdowhile(a,s,k),e,m),[])
-  | Sfor(Sskip,a2,a3,s), _ ->
+  | Sfor(i,Sskip,a2,a3,s), _ ->
+                let c = enter_loop i c in
     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
+    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),[])

Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.ml

@@ -16 +16 @@
 let make_id prefix depth = prefix ^ string_of_int depth
 
-type indexing = sexpr array
+type indexing = sexpr list
+
+type const_indexing = int ref list
+
+(** [enter_loop n indexing] is used to update indexing when one is entering a
+    loop indexed by [n].
+                The function recycles the same constant indexing *)
+let rec enter_loop n indexing = match n, indexing with
+        | None, _ -> indexing (* entering a multi-entry loop *)
+        | Some 0, [] -> [ref 0] (* entering a single entry loop, current depth *)
+        | Some 0, hd :: tl -> hd := 0; indexing (* as above, reusing slot *) 
+        | Some x, hd :: tl -> hd :: enter_loop (Some (x-1)) tl (* lower depth *)
+        | Some x, [] -> assert false(* means I'm entering a single entry loop *)
+                                    (* without having entered the one containing it *)       
+
+(** [enter_loop n indexing] is used to update indexing when one is continuing a
+    loop indexed by [n]. *)
+let rec continue_loop n indexing = match n, indexing with
+        | None, _ -> indexing (* continuing a multi-entry loop *)
+        | Some 0, hd :: tl -> hd := !hd + 1; indexing (* incrementing index *) 
+        | Some x, hd :: tl -> hd :: continue_loop (Some (x-1)) tl (* lower depth *)
+        | Some _, [] -> assert false (* means I'm continuing a single entry loop *)
+                                     (* without having entered it *)       
 
 let sexpr_of i l = 
     try
-        l.(i)
+        List.nth l i
     with
-        | Invalid_argument _ -> invalid_arg("costLabel.sexpr_of")
+                        | Failure _
+      | Invalid_argument _ -> invalid_arg "costLabel.sexpr_of"
 
-let id_indexing n = Array.make n sexpr_id
+let rec id_indexing = function
+        | 0 -> []
+        | n -> sexpr_id :: id_indexing (n-1)
 
 (* a*_+b is composed with c*_+d by substitution: *)
@@ -30 +55 @@
 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 compose_index i s l = 
-  try
-                l.(i) <- compose_sexpr s l.(i)
-        with
-                | Not_found -> ()
+let rec compose_index i s l = match i, l with
+        | 0, s' :: l' -> compose_sexpr s s' :: l'
+        | x, s' :: l' -> compose_index (i-1) s l'
+        | _ -> l 
 
 
 (* I°J applies every mapping in I to every mapping in J *)
-let compose_indexing m n =
-        let f i a = compose_index i a n in
-        Array.iteri f m
+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 c m = match c, m with
+        | i1 :: l1, s2 :: l2 -> ev_sexpr !i1 s2 :: compose_const_indexing l1 l2
+        | _, [] -> [] (* that's ok as current indexings will not be shrinked *)
+        | [], _ -> assert false (* means an indexed label is not in the right ctx *) 
 
 module IndexingSet = Set.Make(struct
@@ -59 +89 @@
 (* if [pretty] is false then a name suitable for labels is given*)
 (* ('P' replaces '+') *)
-let string_of_sexpr pretty id (Sexpr(a, b)) =
+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
@@ -69 +100 @@
 (* [pretty] true:  (0,i1+1,2i2+2)*)
 (* [pretty] false: _0_i1P1_2i2P2 *)
-let string_of_indexing pretty prefix m = 
-        if Array.length m = 0 then "" else
-        let buff = Buffer.create 16 in
-  Buffer.add_char buff (if pretty then '(' else '_');
-        let sep = if pretty then ',' else '_' in
-        let f i a =
-                if i > 0 then Buffer.add_char buff sep;
-                let str = string_of_sexpr pretty (prefix ^ string_of_int i) a in
-                Buffer.add_string buff str in
-        Array.iteri f m;
-        Buffer.contents buff
+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 =

Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.mli

@@ -19 +19 @@
 val make_id : string -> index -> string
 
-type indexing = sexpr array
+type indexing = sexpr list
+
+type const_indexing = int ref list
+
+(** [enter_loop n indexing] is used to update indexing when one is entering a
+    loop indexed by [n].
+        The function recycles the same constant indexing *)
+val enter_loop : index option -> const_indexing -> const_indexing
+
+(** [continue_loop n indexing] is used to update indexing when one is continuing a
+    loop indexed by [n]. *)
+val continue_loop : index option -> const_indexing -> const_indexing
 
 (** [id_indexing n] generates an identity indexing nested in [n] loops *) 
@@ -25 +36 @@
 
 (** [compose_index i s l] applies the transformation [i] |--> [s] to [l] *) 
-val compose_index : index -> sexpr -> indexing -> unit
+val compose_index : index -> sexpr -> indexing -> indexing
 
 (** [compose_index l m] applies all the transformations in  [l] to [m] *)
-val compose_indexing : indexing -> indexing -> unit
+val compose_indexing : indexing -> indexing -> indexing
+
+val compose_const_indexing : const_indexing -> indexing -> int list
 
 module IndexingSet : Set.S with type elt = indexing