Changeset 1334 for Deliverables/D2.2


Ignore:
Timestamp:
Oct 10, 2011, 2:17:02 PM (9 years ago)
Author:
tranquil
Message:

work on Cminor completed

Location:
Deliverables/D2.2/8051-indexed-labels-branch/src
Files:
6 edited

Legend:

Unmodified
Added
Removed

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

    r1328 r1334  
    487487
    488488let eval_stmt f k e m s c =
    489         let enter_loop = CostLabel.enter_loop in
    490         let continue_loop = CostLabel.continue_loop in
    491489        match s, k with
    492490  | Sskip, Kseq(s,k) -> (State(f,s,k,e,m,c),[])
    … …  
    494492  | Sskip, Kdowhile(i,a,s,k') | Scontinue, Kdowhile (i,a,s,k') ->
    495493                (* possibly continuing a loop *)
    496                 continue_loop i c; (* if loop is not continued, this change will have no
    497                                       effect in the following. Can be made stricter *)
     494                CostLabel.continue_loop i c; (* if loop is not continued, this change
     495                                                will have no effect in the following. *)
    498496    let ((v1,_),l1) = eval_expr e m c a in
    499497    let a_false = (State(f,Sskip,k',e,m,c),l1) in
    … …  
    501499    condition v1 a_true a_false
    502500  | Sskip, Kfor3(i,a2,a3,s,k) | Scontinue, Kfor3(i,a2,a3,s,k) ->
    503     continue_loop i c;
     501    CostLabel.continue_loop i c;
    504502    let ((v1,_),l1) = eval_expr e m c a2 in
    505503    let a_false = (State(f,Sskip,k,e,m,c),l1) in
    … …  
    533531    condition v1 a_true a_false
    534532  | Swhile(i,a,s), _ ->
    535                 enter_loop i c;
     533                CostLabel.enter_loop i c;
    536534    let ((v1,_),l1) = eval_expr e m c a in
    537535    let a_false = (State(f,Sskip,k,e,m,c),l1) in
    … …  
    539537    condition v1 a_true a_false
    540538  | Sdowhile(i,a,s), _ ->
    541                 enter_loop i c;
     539                CostLabel.enter_loop i c;
    542540                (State(f,s,Kdowhile(i,a,s,k),e,m,c),[])
    543541  | Sfor(i,Sskip,a2,a3,s), _ ->
    544                 enter_loop i c;
     542                CostLabel.enter_loop i c;
    545543    let ((v1,_),l1) = eval_expr e m c a2 in
    546544    let a_false = (State(f,Sskip,k,e,m,c),l1) in

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

    r818 r1334  
    486486    AST.res = ret_type }
    487487
     488let ind_0 i stmt = match i with
     489        | None -> stmt
     490        | Some x -> Cminor.St_ind_0(x, stmt)
     491
     492let ind_inc i stmt = match i with
     493        | None -> stmt
     494        | Some x -> Cminor.St_ind_inc(stmt, x)
     495
    488496let f_stmt fresh var_locs stmt sub_exprs_res sub_stmts_res =
    489497  let (tmps, sub_stmts_res) = List.split sub_stmts_res in
    … …  
    509517      ([(tmp, t)], Cminor.St_seq (stmt_call, stmt_assign))
    510518
    511     | Clight.Swhile _, e :: _, stmt :: _ ->
    512       let econd =
    513         Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in
     519    | Clight.Swhile (i,_,_), e :: _, stmt :: _ ->
     520      let econd =               
     521        Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in
    514522      let scond =
    515         Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in
    516       ([],
    517        Cminor.St_block (Cminor.St_loop (Cminor.St_seq (scond,
    518                                                        Cminor.St_block stmt))))
    519 
    520     | Clight.Sdowhile _, e :: _, stmt :: _ ->
    521       let econd =
    522         Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in
     523        Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in
     524            let loop_body = Cminor.St_seq (scond, ind_inc i (Cminor.St_block stmt)) in
     525                        let loop = ind_0 i (Cminor.St_loop loop_body) in
     526      ([], Cminor.St_block loop)
     527                       
     528    | Clight.Sdowhile (i,_,_), e :: _, stmt :: _ ->
     529      let econd =               
     530        Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in
    523531      let scond =
    524         Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in
    525       ([],
    526        Cminor.St_block (Cminor.St_loop (Cminor.St_seq (Cminor.St_block stmt,
    527                                                        scond))))
    528 
    529     | Clight.Sfor _, e :: _, stmt1 :: stmt2 :: stmt3 :: _ ->
    530       let econd =
    531         Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in
     532              Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in
     533                        let loop_body = ind_inc i (Cminor.St_seq (Cminor.St_block stmt, scond)) in
     534                        let loop = ind_0 i (Cminor.St_loop loop_body) in
     535      ([], Cminor.St_block loop)
     536
     537    | Clight.Sfor (i,_,_,_,_), e :: _, stmt1 :: stmt2 :: stmt3 :: _ ->
     538      let econd =                               
     539        Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in
    532540      let scond =
    533         Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in
    534       let body = Cminor.St_seq (Cminor.St_block stmt3, stmt2) in
    535       ([],
    536        Cminor.St_seq (stmt1,
    537                       Cminor.St_block
    538                         (Cminor.St_loop (Cminor.St_seq (scond, body)))))
     541              Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in
     542      let body = Cminor.St_seq (ind_inc i (Cminor.St_block stmt3), stmt2) in
     543                        let body = Cminor.St_seq (scond, body) in
     544                        let block = Cminor.St_block (ind_0 i (Cminor.St_loop body)) in 
     545      ([], Cminor.St_seq (stmt1, block))
    539546
    540547    | Clight.Sifthenelse _, e :: _, stmt1 :: stmt2 :: _ ->

  • Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminor.mli

    r818 r1334  
    4747  | St_goto of string
    4848  | St_cost of CostLabel.t * statement
     49        | St_ind_0 of CostLabel.index * statement
     50  | St_ind_inc of statement * CostLabel.index
    4951
    5052

  • Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorFold.ml

    r818 r1334  
    4444    ([e], [stmt1 ; stmt2])
    4545  | Cminor.St_loop stmt | Cminor.St_block stmt
    46   | Cminor.St_label (_, stmt) | Cminor.St_cost (_, stmt) ->
    47     ([], [stmt])
     46  | Cminor.St_label (_, stmt) | Cminor.St_cost (_, stmt)
     47        | Cminor.St_ind_0 (_, stmt) | Cminor.St_ind_inc (stmt, _) ->
     48                ([], [stmt])
    4849
    4950let statement_fill_subs stmt sub_es sub_stmts =

  • Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorInterpret.ml

    r1291 r1334  
    2323(* State of execution *)
    2424
     25type indexing = CostLabel.const_indexing
     26
    2527type continuation =
    2628    Ct_stop
    2729  | Ct_cont of statement*continuation
     30        | Ct_ind_inc of CostLabel.index*continuation
    2831  | Ct_endblock of continuation
    2932  | Ct_returnto of
    30       ident option*internal_function*Val.address*local_env*continuation
     33      ident option*internal_function*Val.address*local_env*indexing*continuation
    3134
    3235type state =
    3336    State_regular of
    34       internal_function*statement*continuation*Val.address*local_env*(function_def Mem.memory)
     37      internal_function*statement*continuation*Val.address*local_env*
     38                         (function_def Mem.memory)*indexing
    3539  | State_call of function_def*Val.t list*continuation*(function_def Mem.memory)
    3640  | State_return of Val.t*continuation*(function_def Mem.memory)
    … …  
    6872                let lbl = CostLabel.string_of_cost_label lbl in
    6973                "cost " ^ lbl
     74        | St_ind_0 (i, _) -> "reset " ^ string_of_int i ^ " to 0"
     75        | St_ind_inc (_, i) -> "post-increment " ^ string_of_int i
    7076
    7177let print_state = function
    72   | State_regular (_, stmt, _, sp, lenv, mem) ->
    73     Printf.printf "Local environment:\n%s\n\nMemory:%s\nStack pointer: %s\n\nRegular state: %s\n\n%!"
     78  | State_regular (_, stmt, _, sp, lenv, mem, i) ->
     79    Printf.printf "Local environment:\n%s\n\nMemory:%s\nStack pointer: %s\nIndexing:"
    7480      (string_of_local_env lenv)
    7581      (Mem.to_string mem)
    76       (Val.to_string (value_of_address sp))
     82      (Val.to_string (value_of_address sp));
     83                        Array.iter (fun a -> Printf.printf "%d, " a) i;
     84                        Printf.printf "\nRegular state: %s\n\n%!"
    7785      (string_of_statement stmt)
    7886  | State_call (_, args, _, mem) ->
    … …  
    223231
    224232let rec callcont = function
    225     Ct_stop                     -> Ct_stop
    226   | Ct_cont(_,k)                -> callcont k
    227   | Ct_endblock(k)              -> callcont k
    228   | Ct_returnto(a,b,c,d,e)      -> Ct_returnto(a,b,c,d,e)
     233  | Ct_cont(_,k) | Ct_endblock k | Ct_ind_inc(_,k) -> callcont k
     234        | (Ct_stop | Ct_returnto _) as k -> k
    229235
    230236let findlabel lbl st k =
    … …  
    252258  | St_label(l,s)               -> if l=lbl then Some((s,k)) else None
    253259  | St_goto(_)                  -> None
    254   | St_cost (_,s)               -> fdlbl k s
     260  | St_cost (_,s) | St_ind_0(_,s) | St_ind_inc(s,_) -> fdlbl k s
    255261  in match fdlbl k st with
    256262      None -> assert false (*Wrong label*)
    … …  
    264270  (State_call(fun_def,args,cont,m),l1@l2)
    265271
    266 let eval_stmt f k sigma e m s = match s, k with
    267   | St_skip,Ct_cont(s,k) -> (State_regular(f, s, k, sigma, e, m),[])
    268   | St_skip,Ct_endblock(k) -> (State_regular(f, St_skip, k, sigma, e, m),[])
     272let eval_stmt f k sigma e m i s = match s, k with
     273  | St_skip,Ct_cont(s,k) -> (State_regular(f, s, k, sigma, e, m, i),[])
     274  | St_skip,Ct_endblock(k) -> (State_regular(f, St_skip, k, sigma, e, m, i),[])
    269275  | St_skip, (Ct_returnto _ as k) ->
    270276    (State_return (Val.undef,k,Mem.free m sigma),[])
     277  | St_skip,Ct_ind_inc(ind,k) ->
     278                CostLabel.continue_loop (Some ind) i;
     279                (State_regular(f, s, k, sigma, e, m, i),[])
    271280  | St_skip,Ct_stop ->
    272281    (State_return (Val.undef,Ct_stop,Mem.free m sigma),[])
    … …  
    274283    let (v,l) = eval_expression sigma e m exp in
    275284    let e = LocalEnv.add x v e in
    276     (State_regular(f, St_skip, k, sigma, e, m),l)
     285    (State_regular(f, St_skip, k, sigma, e, m, i),l)
    277286  | St_store(q,a1,a2),_ ->
    278287    let (v1,l1) = eval_expression sigma e m a1 in
    279288    let (v2,l2) = eval_expression sigma e m a2 in
    280289    let m = Mem.storeq m q (address_of_value v1) v2 in
    281     (State_regular(f, St_skip, k, sigma, e, m),l1@l2)
     290    (State_regular(f, St_skip, k, sigma, e, m, i),l1@l2)
    282291  | St_call(xopt,f',params,_),_ ->
    283     call_state sigma e m f' params (Ct_returnto(xopt,f,sigma,e,k))
     292    call_state sigma e m f' params (Ct_returnto(xopt,f,sigma,e,i,k))
    284293  | St_tailcall(f',params,_),_ ->
    285294    call_state sigma e m f' params (callcont k)
    286   | St_seq(s1,s2),_ -> (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m),[])
     295  | St_seq(s1,s2),_ -> (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m, i),[])
    287296  | St_ifthenelse(exp,s1,s2),_ ->
    288297    let (v,l) = eval_expression sigma e m exp in
    … …  
    292301        if Val.is_false v then s2
    293302        else error "undefined conditional value." in
    294       (State_regular(f,next_stmt,k,sigma,e,m),l)
    295   | St_loop(s),_ -> (State_regular(f,s,Ct_cont((St_loop s),k),sigma,e,m),[])
    296   | St_block(s),_ -> (State_regular(f,s,(Ct_endblock k),sigma,e,m),[])
    297   | St_exit(n),Ct_cont(s,k) -> (State_regular(f,(St_exit n),k,sigma,e,m),[])
    298   | St_exit(0),Ct_endblock(k) -> (State_regular(f,St_skip,k,sigma,e,m),[])
     303      (State_regular(f,next_stmt,k,sigma,e,m,i),l)
     304  | St_loop(s),_ -> (State_regular(f,s,Ct_cont((St_loop s),k),sigma,e,m,i),[])
     305  | St_block(s),_ -> (State_regular(f,s,(Ct_endblock k),sigma,e,m,i),[])
     306  | St_exit(n),Ct_cont(s,k) -> (State_regular(f,(St_exit n),k,sigma,e,m,i),[])
     307  | St_exit(0),Ct_endblock(k) -> (State_regular(f,St_skip,k,sigma,e,m,i),[])
    299308  | St_exit(n),Ct_endblock(k) ->
    300     (State_regular(f,(St_exit (n-1)),k,sigma,e,m),[])
    301   | St_label(_,s),_ -> (State_regular(f,s,k,sigma,e,m),[])
     309    (State_regular(f,(St_exit (n-1)),k,sigma,e,m,i),[])
     310  | St_label(_,s),_ -> (State_regular(f,s,k,sigma,e,m,i),[])
    302311  | St_goto(lbl),_ ->
    303312    let (s2,k2) = findlabel lbl f.f_body (callcont k) in
    304     (State_regular(f,s2,k2,sigma,e,m),[])
     313    (State_regular(f,s2,k2,sigma,e,m,i),[])
    305314  | St_switch(exp,lst,def),_ ->
    306315    let (v,l) = eval_expression sigma e m exp in
    307316    if Val.is_int v then
    308317      try
    309         let i = Val.to_int v in
     318        let v = Val.to_int v in
    310319        let nb_exit =
    311           if List.mem_assoc i lst then List.assoc i lst
     320          if List.mem_assoc v lst then List.assoc v lst
    312321          else def in
    313         (State_regular(f, St_exit nb_exit,k, sigma, e, m),l)
     322        (State_regular(f, St_exit nb_exit,k, sigma, e, m, i),l)
    314323      with _ -> error "int value too big."
    315324    else error "undefined switch value."
    … …  
    319328      let (v,l) = eval_expression sigma e m a in
    320329      (State_return (v,callcont k,Mem.free m sigma),l)
    321   | St_cost(lbl,s),_ -> (State_regular(f,s,k,sigma,e,m),[lbl])
     330  | St_cost(lbl,s),_ ->
     331    (* applying current indexing on label *)
     332    let lbl = CostLabel.apply_const_indexing i lbl in
     333                (State_regular(f,s,k,sigma,e,m,i),[lbl])
     334        | St_ind_0(ind,s),_ ->
     335                CostLabel.enter_loop (Some ind) i;
     336                (State_regular(f,s,k,sigma,e,m,i), [])
     337        | St_ind_inc(s,ind),_ ->
     338    (State_regular(f,s,Ct_ind_inc(ind,k),sigma,e,m,i), [])
    322339  | _ -> error "state malformation."
    323340
    … …  
    333350  State_return (v, k, mem')
    334351
     352let max_loop_index =
     353  let f_expr _ _ = () in
     354  let f_stmt stmt _ sub_stmts_res =
     355        let curr_max = List.fold_left max 0 sub_stmts_res in
     356        match stmt with
     357          | Cminor.St_ind_0 (x, _) | Cminor.St_ind_inc (_, x) ->
     358                                                 max (x+1) curr_max
     359          | _ -> curr_max in
     360  CminorFold.statement f_expr f_stmt
     361
    335362let step_call vargs k m = function
    336363  | F_int f ->
    337364    let (m, sp) = Mem.alloc m (concrete_stacksize f.f_stacksize) in
    338365    let lenv = init_local_env vargs f.f_params f.f_vars in
    339     State_regular(f,f.f_body,k,sp,lenv,m)
     366                let i = Array.make (max_loop_index f.f_body) 0 in
     367    State_regular(f,f.f_body,k,sp,lenv,m,i)
    340368  | F_ext f -> interpret_external k m f.ef_tag vargs
    341369
    342370let step = function
    343   | State_regular(f,stmt,k,sp,e,m) -> eval_stmt f k sp e m stmt
     371  | State_regular(f,stmt,k,sp,e,m,i) -> eval_stmt f k sp e m i stmt
    344372  | State_call(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[])
    345   | State_return(v,Ct_returnto(None,f,sigma,e,k),m) ->
    346     (State_regular(f,St_skip,k,sigma,e,m),[])
    347   | State_return(v,Ct_returnto(Some x,f,sigma,e,k),m) ->
     373  | State_return(v,Ct_returnto(None,f,sigma,e,i,k),m) ->
     374    (State_regular(f,St_skip,k,sigma,e,m,i),[])
     375  | State_return(v,Ct_returnto(Some x,f,sigma,e,i,k),m) ->
    348376    let e = LocalEnv.add x v e in
    349     (State_regular(f,St_skip,k,sigma,e,m),[])
     377    (State_regular(f,St_skip,k,sigma,e,m,i),[])
    350378  | _ -> error "state malformation."
    351379
    … …  
    371399    | State_return(v,Ct_stop,_) -> (* Explicit return in main *)
    372400      print_and_return_result (compute_result v)
    373     | State_regular(_,St_skip,Ct_stop,_,_,_) -> (* Implicit return in main *)
     401    | State_regular(_,St_skip,Ct_stop,_,_,_,_) -> (* Implicit return in main *)
    374402      print_and_return_result IntValue.Int32.zero
    375403    | state -> exec debug cost_labels (step state)

  • Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorPrinter.ml

    r1291 r1334  
    172172        (Primitive.print_sig sg)
    173173  | Cminor.St_seq (s1, s2) -> (print_body n s1) ^ (print_body n s2)
     174  | Cminor.St_ifthenelse (e, s1, Cminor.St_skip) ->
     175    Printf.sprintf "%sif (%s) {\n%s%s}\n"
     176    (n_spaces n)
     177    (print_expression e)
     178    (print_body (n+2) s1)
     179    (n_spaces n)
    174180  | Cminor.St_ifthenelse (e, s1, s2) ->
    175181      Printf.sprintf "%sif (%s) {\n%s%s}\n%selse {\n%s%s}\n"
    … …  
    211217                  let lbl = CostLabel.string_of_cost_label lbl in
    212218      Printf.sprintf "%s%s:\n%s" (n_spaces n) lbl (print_body n s)
     219        | Cminor.St_ind_0 (i, s) ->
     220                  Printf.sprintf "%sindex %d:\n%s" (n_spaces n) i (print_body n s)
     221        | Cminor.St_ind_inc (s, i) ->
     222                  Printf.sprintf "%s%sincrement %d;\n" (print_body n s) (n_spaces n) i
    213223
    214224let print_internal f_name f_def =
    … …  
    255265  | Cminor.St_goto(_) -> "goto"
    256266  | Cminor.St_cost(_,_) -> "cost"
     267        | Cminor.St_ind_0 _ -> "index"
     268        | Cminor.St_ind_inc _ -> "increment"
Note: See TracChangeset for help on using the changeset viewer.