Ignore:
Timestamp:
May 19, 2011, 4:03:04 PM (10 years ago)
Author:
ayache
Message:

32 and 16 bits operations support in D2.2/8051

Location:
Deliverables/D2.2/8051/src/cminor
Files:
12 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/cminor/cminor.mli

    r740 r818  
    33
    44(* This file describes the abstract syntax of the Cminor language.
    5    Only types are: int8, int16, int32, float32, float64 and void. *)
     5   Only types are: int8, int16, int32 and void. *)
    66
    7 type expression =
     7type etype = AST.sig_type
     8
     9type expression = Expr of expr_descr * etype
     10and expr_descr =
    811  | Id of AST.ident
    912  | Cst of AST.cst
    1013  | Op1 of AST.op1 * expression
    1114  | Op2 of AST.op2 * expression * expression
    12   | Mem of Memory.quantity * expression          (* Memory read *)
     15  | Mem of AST.quantity * expression          (* Memory read *)
    1316  | Cond of expression * expression * expression (* Ternary expression *)
    1417  | Exp_cost of CostLabel.t * expression         (* Labelled expression *)
     
    1720  | St_skip
    1821  | St_assign of AST.ident * expression
    19   | St_store of Memory.quantity * expression * expression
     22  | St_store of AST.quantity * expression * expression
    2023
    2124  (* Function call. Parameters are an optional variable to store the
     
    4750
    4851type internal_function =
    49     { f_sig       : AST.signature ;
    50       f_params    : AST.ident list ;
    51       f_vars      : AST.ident list ;
    52       f_ptrs      : AST.ident list ;
    53       f_stacksize : int ;
     52    { f_return    : AST.type_return ;
     53      f_params    : (AST.ident * etype) list ;
     54      f_vars      : (AST.ident * etype) list ;
     55      f_stacksize : AST.abstract_size ;
    5456      f_body      : statement }
    5557
     
    6365
    6466type program =
    65     { vars   : (AST.ident * (AST.data list)) list ;
     67    { vars   : (AST.ident * AST.abstract_size * AST.data list option) list ;
    6668      functs : (AST.ident * function_def) list ;
    6769      main   : AST.ident option }
  • Deliverables/D2.2/8051/src/cminor/cminorAnnotator.ml

    r740 r818  
    33
    44let funct_vars (id, fun_def) = match fun_def with
    5   | Cminor.F_int def -> id :: (def.Cminor.f_params @ def.Cminor.f_vars)
     5  | Cminor.F_int def ->
     6    id :: (List.map fst (def.Cminor.f_params @ def.Cminor.f_vars))
    67  | _ -> [id]
    78
    89let prog_idents p =
    9   let vars = List.map fst p.Cminor.vars in
     10  let vars = List.map (fun (x, _, _) -> x) p.Cminor.vars in
    1011  let f vars funct = vars @ (funct_vars funct) in
    1112  let vars = List.fold_left f vars p.Cminor.functs in
     
    1819
    1920
     21(*
    2022let increment cost_id incr =
    21   let cost = Cminor.Cst (AST.Cst_addrsymbol cost_id) in
    22   let load = Cminor.Mem (Memory.QInt 4, cost) in
    23   let incr = Cminor.Op2 (AST.Op_add, load, Cminor.Cst (AST.Cst_int incr)) in
     23  let cost =
     24    Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol cost_id), AST.Sig_ptr) in
     25  let load = Cminor.Expr (Cminor.Mem (Memory.QInt 4, cost), AST.Sig_int 4) in
     26  let incr = Cminor.Expr (Cminor.Cst (AST.Cst_int incr), AST.Sig_int 4) in
     27  let incr = Cminor.Expr (Cminor.Op2 (AST.Op_add, load, incr), AST.Sig_int 4) in
    2428  Cminor.St_store (Memory.QInt 4, cost, incr)
    2529
     
    3539
    3640let remove_cost_labels_exp e =
    37   CminorFold.expression_left f_remove_cost_labels_exp e
     41  CminorFold.expression f_remove_cost_labels_exp e
    3842
    3943let remove_cost_labels_exps exps =
     
    5963
    6064let update_cost_exp costs_mapping cost_id e =
    61   CminorFold.expression_left (f_update_cost_exp costs_mapping cost_id) e
     65  CminorFold.expression (f_update_cost_exp costs_mapping cost_id) e
    6266
    6367let update_cost_exps costs_mapping cost_id exps =
     
    148152   "" (* TODO *),
    149153   "" (* TODO *))
     154*)
    150155
    151156
     
    168173  List.fold_left f labels_empty l
    169174
    170 let f_exp_labels e subexp_res =
     175let f_exp_labels (Cminor.Expr (ed, _)) subexp_res =
    171176  let labels1 = labels_union_list subexp_res in
    172   let labels2 = match e with
     177  let labels2 = match ed with
    173178    | Cminor.Exp_cost (lbl, _) -> add_cost_label lbl labels_empty
    174179    | _ -> labels_empty in
     
    185190  labels_union labels labels3
    186191
    187 let body_labels stmt = CminorFold.statement_left f_exp_labels f_body_labels stmt
     192let body_labels stmt = CminorFold.statement f_exp_labels f_body_labels stmt
    188193
    189194let prog_labels p =
  • Deliverables/D2.2/8051/src/cminor/cminorAnnotator.mli

    r640 r818  
    22(** This module defines the instrumentation of a [Cminor] program. *)
    33
     4(*
    45(** [instrument prog cost_map] instruments the program [prog]. First a fresh
    56    global variable --- the so-called cost variable --- is added to the program.
     
    1011val instrument : Cminor.program -> int CostLabel.Map.t ->
    1112                 Cminor.program * string * string
     13*)
    1214
    1315val cost_labels : Cminor.program -> CostLabel.Set.t
  • Deliverables/D2.2/8051/src/cminor/cminorFold.ml

    r486 r818  
    44
    55
    6 (* Left operators *)
     6let expression_subs (Cminor.Expr (ed, _)) = match ed with
     7  | Cminor.Id _ | Cminor.Cst _ -> []
     8  | Cminor.Op1 (_, e) | Cminor.Mem (_, e) | Cminor.Exp_cost (_, e) -> [e]
     9  | Cminor.Op2 (_, e1, e2) -> [e1 ; e2]
     10  | Cminor.Cond (e1, e2, e3) -> [e1 ; e2 ; e3]
    711
    8 (* In [expression_left f e], [f]'s second argument is the list of
    9    [expression_left]'s results on [e]'s sub-expressions. The results are
    10    computed from left to right following their appearance order in the
    11    [Cminor.expression] type. *)
    12 
    13 let rec expression_left f_expr e =
    14   let subexpr_res = match e with
    15     | Cminor.Id _ | Cminor.Cst _ -> []
    16     | Cminor.Op1 (_, e) | Cminor.Mem (_, e) | Cminor.Exp_cost (_, e) ->
    17         [expression_left f_expr e]
    18     | Cminor.Op2 (_, e1, e2) ->
    19         let res1 = expression_left f_expr e1 in
    20         let res2 = expression_left f_expr e2 in
    21         [res1 ; res2]
    22     | Cminor.Cond (e1, e2, e3) ->
    23         let res1 = expression_left f_expr e1 in
    24         let res2 = expression_left f_expr e2 in
    25         let res3 = expression_left f_expr e3 in
    26         [res1 ; res2 ; res3]
    27   in
    28   f_expr e subexpr_res
    29 
    30 let map_left f =
    31   let rec aux = function
    32     | [] -> []
    33     | e :: l -> let x = f e in x :: (aux l)
    34   in
    35   aux
    36 
    37 (* In [statement_left f_expr f_stmt stmt], [f_stmt]'s second argument is the
    38    list of [expression_left f_expr]'s results on [stmt]'s sub-expressions, and
    39    [f_stmt]'s third argument is the list of [statement_left]'s results
    40    on [stmt]'s sub-statements. The results are computed from left to right
    41    following their appearance order in the [Cminor.statement] type. *)
    42 
    43 let rec statement_left f_expr f_stmt stmt =
    44   let expr_res e = expression_left f_expr e in
    45   let (subexpr_res, substmt_res) = match stmt with
    46     | Cminor.St_skip | Cminor.St_exit _ | Cminor.St_switch _
    47     | Cminor.St_return None | Cminor.St_goto _ -> ([], [])
    48     | Cminor.St_assign (_, e) | Cminor.St_return (Some e) -> ([expr_res e], [])
    49     | Cminor.St_store (_, e1, e2) ->
    50         let res1 = expr_res e1 in
    51         let res2 = expr_res e2 in
    52         ([res1 ; res2], [])
    53     | Cminor.St_call (_, f, args, _) | Cminor.St_tailcall (f, args, _) ->
    54         let resf = expr_res f in
    55         let resargs = map_left expr_res args in
    56         (resf :: resargs, [])
    57     | Cminor.St_seq (stmt1, stmt2) ->
    58         let res1 = statement_left f_expr f_stmt stmt1 in
    59         let res2 = statement_left f_expr f_stmt stmt2 in
    60         ([], [res1 ; res2])
    61     | Cminor.St_ifthenelse (e, stmt1, stmt2) ->
    62         let rese = expr_res e in
    63         let res1 = statement_left f_expr f_stmt stmt1 in
    64         let res2 = statement_left f_expr f_stmt stmt2 in
    65         ([rese], [res1 ; res2])
    66     | Cminor.St_loop stmt | Cminor.St_block stmt
    67     | Cminor.St_label (_, stmt) | Cminor.St_cost (_, stmt) ->
    68         ([], [statement_left f_expr f_stmt stmt])
    69   in
    70   f_stmt stmt subexpr_res substmt_res
     12let expression_fill_subs (Cminor.Expr (ed, t)) subs =
     13  let ed = match ed, subs with
     14    | Cminor.Id _, _ | Cminor.Cst _, _ -> ed
     15    | Cminor.Op1 (op1, _), e :: _ -> Cminor.Op1 (op1, e)
     16    | Cminor.Op2 (op2, _, _), e1 :: e2 :: _ -> Cminor.Op2 (op2, e1, e2)
     17    | Cminor.Mem (size, _), e :: _ -> Cminor.Mem (size, e)
     18    | Cminor.Cond _, e1 :: e2 :: e3 :: _ -> Cminor.Cond (e1, e2, e3)
     19    | Cminor.Exp_cost (lbl, _), e :: _ -> Cminor.Exp_cost (lbl, e)
     20    | _ -> assert false (* wrong parameter size *) in
     21  Cminor.Expr (ed, t)
    7122
    7223
    73 (* Right operators *)
     24(* In [expression f e], [f]'s second argument is the list of
     25   [expression]'s results on [e]'s sub-expressions. *)
    7426
    75 (* In [expression_right f e], [f]'s second argument is the list of
    76    [expression_right]'s results on [e]'s sub-expressions. The results are
    77    computed from right to left following their appearance order in the
    78    [Cminor.expression] type. *)
     27let rec expression f_expr e =
     28  let sub_es_res = List.map (expression f_expr) (expression_subs e) in
     29  f_expr e sub_es_res
    7930
    80 let rec expression_right f_expr e =
    81   let subexpr_res = match e with
    82     | Cminor.Id _ | Cminor.Cst _ -> []
    83     | Cminor.Op1 (_, e) | Cminor.Mem (_, e) | Cminor.Exp_cost (_, e) ->
    84         [expression_right f_expr e]
    85     | Cminor.Op2 (_, e1, e2) ->
    86         let res2 = expression_right f_expr e2 in
    87         let res1 = expression_right f_expr e1 in
    88         [res2 ; res1]
    89     | Cminor.Cond (e1, e2, e3) ->
    90         let res3 = expression_right f_expr e3 in
    91         let res2 = expression_right f_expr e2 in
    92         let res1 = expression_right f_expr e1 in
    93         [res3 ; res2 ; res1]
    94   in
    95   f_expr subexpr_res e
    9631
    97 let map_right f =
    98   let rec aux = function
    99     | [] -> []
    100     | e :: l -> let res = (aux l) in (f e) :: res
    101   in
    102   aux
     32let statement_subs = function
     33  | Cminor.St_skip | Cminor.St_exit _ | Cminor.St_return None
     34  | Cminor.St_goto _ -> ([], [])
     35  | Cminor.St_assign (_, e) | Cminor.St_switch (e, _, _)
     36  | Cminor.St_return (Some e) -> ([e], [])
     37  | Cminor.St_store (_, e1, e2) ->
     38    ([e1 ; e2], [])
     39  | Cminor.St_call (_, f, args, _) | Cminor.St_tailcall (f, args, _) ->
     40    (f :: args, [])
     41  | Cminor.St_seq (stmt1, stmt2) ->
     42    ([], [stmt1 ; stmt2])
     43  | Cminor.St_ifthenelse (e, stmt1, stmt2) ->
     44    ([e], [stmt1 ; stmt2])
     45  | Cminor.St_loop stmt | Cminor.St_block stmt
     46  | Cminor.St_label (_, stmt) | Cminor.St_cost (_, stmt) ->
     47    ([], [stmt])
    10348
    104 (* In [statement_right f_expr f_stmt stmt], [f_stmt]'s second argument is the
    105    list of [expression_left f_expr]'s results on [stmt]'s sub-expressions, and
    106    [f_stmt]'s third argument is the list of [statement_left]'s results
    107    on [stmt]'s sub-statements. The results are computed from right to left
    108    following their appearance order in the [Cminor.statement] type. *)
     49let statement_fill_subs stmt sub_es sub_stmts =
     50  match stmt, sub_es, sub_stmts with
     51    | (  Cminor.St_skip | Cminor.St_exit _ | Cminor.St_return None
     52       | Cminor.St_goto _), _, _ -> stmt
     53    | Cminor.St_assign (x, _), e :: _, _ ->
     54      Cminor.St_assign (x, e)
     55    | Cminor.St_switch (_, cases, dflt), e :: _, _ ->
     56      Cminor.St_switch (e, cases, dflt)
     57    | Cminor.St_return _, e :: _, _ ->
     58      Cminor.St_return (Some e)
     59    | Cminor.St_store (size, _, _), e1 :: e2 :: _, _ ->
     60      Cminor.St_store (size, e1, e2)
     61    | Cminor.St_call (x_opt, _, _, sg), f :: args, _ ->
     62      Cminor.St_call (x_opt, f, args, sg)
     63    | Cminor.St_tailcall (_, _, sg), f :: args, _ ->
     64      Cminor.St_tailcall (f, args, sg)
     65    | Cminor.St_seq _, _, stmt1 :: stmt2 :: _ ->
     66      Cminor.St_seq (stmt1, stmt2)
     67    | Cminor.St_ifthenelse _, e :: _, stmt1 :: stmt2 :: _ ->
     68      Cminor.St_ifthenelse (e, stmt1, stmt2)
     69    | Cminor.St_loop _, _, stmt :: _ ->
     70      Cminor.St_loop stmt
     71    | Cminor.St_block _, _, stmt :: _ ->
     72      Cminor.St_block stmt
     73    | Cminor.St_label (lbl, _), _, stmt :: _ ->
     74      Cminor.St_label (lbl, stmt)
     75    | Cminor.St_cost (lbl, _), _, stmt :: _ ->
     76      Cminor.St_cost (lbl, stmt)
     77    | _ -> assert false (* do not use on these arguments *)
    10978
    110 let rec statement_right f_expr f_stmt stmt =
    111   let expr_res e = expression_right f_expr e in
    112   let (subexpr_res, substmt_res) = match stmt with
    113     | Cminor.St_skip | Cminor.St_exit _ | Cminor.St_switch _
    114     | Cminor.St_return None | Cminor.St_goto _ -> ([], [])
    115     | Cminor.St_assign (_, e) | Cminor.St_return (Some e) -> ([expr_res e], [])
    116     | Cminor.St_store (_, e1, e2) ->
    117         let res2 = expr_res e2 in
    118         let res1 = expr_res e1 in
    119         ([res2 ; res1], [])
    120     | Cminor.St_call (_, f, args, _) | Cminor.St_tailcall (f, args, _) ->
    121         let resargs = map_right expr_res args in
    122         let resf = expr_res f in
    123         (resargs @ [resf], [])
    124     | Cminor.St_seq (stmt1, stmt2) ->
    125         let res2 = statement_right f_expr f_stmt stmt2 in
    126         let res1 = statement_right f_expr f_stmt stmt1 in
    127         ([], [res2 ; res1])
    128     | Cminor.St_ifthenelse (e, stmt1, stmt2) ->
    129         let res2 = statement_right f_expr f_stmt stmt2 in
    130         let res1 = statement_right f_expr f_stmt stmt1 in
    131         let rese = expr_res e in
    132         ([rese], [res2 ; res1])
    133     | Cminor.St_loop stmt | Cminor.St_block stmt
    134     | Cminor.St_label (_, stmt) | Cminor.St_cost (_, stmt) ->
    135         ([], [statement_right f_expr f_stmt stmt])
    136   in
    137   f_stmt subexpr_res substmt_res stmt
     79(* In [statement f_expr f_stmt stmt], [f_stmt]'s second argument is the
     80   list of [expression f_expr]'s results on [stmt]'s sub-expressions, and
     81   [f_stmt]'s third argument is the list of [statement]'s results
     82   on [stmt]'s sub-statements. *)
     83
     84let rec statement f_expr f_stmt stmt =
     85  let (sub_es, sub_stmts) = statement_subs stmt in
     86  let sub_es_res = List.map (expression f_expr) sub_es in
     87  let sub_stmts_res = List.map (statement f_expr f_stmt) sub_stmts in
     88  f_stmt stmt sub_es_res sub_stmts_res
  • Deliverables/D2.2/8051/src/cminor/cminorFold.mli

    r486 r818  
    33    [Cminor]'s AST. *)
    44
    5 (* In [expression_left f e], [f]'s second argument is the list of
    6    [expression_left]'s results on [e]'s sub-expressions. The results are
    7    computed from left to right following their appearance order in the
    8    [Cminor.expression] type. *)
     5val expression_subs : Cminor.expression -> Cminor.expression list
    96
    10 val expression_left : (Cminor.expression -> 'a list -> 'a) ->
    11                       Cminor.expression ->
    12                       'a
     7val expression_fill_subs : Cminor.expression -> Cminor.expression list ->
     8                           Cminor.expression
    139
    14 (* In [statement_left f_expr f_stmt stmt], [f_stmt]'s second argument is the
    15    list of [expression_left f_expr]'s results on [stmt]'s sub-expressions, and
    16    [f_stmt]'s third argument is the list of [statement_left]'s results
    17    on [stmt]'s sub-statements. The results are computed from left to right
    18    following their appearance order in the [Cminor.statement] type. *)
     10(* In [expression f e], [f]'s second argument is the list of
     11   [expression]'s results on [e]'s sub-expressions. *)
    1912
    20 val statement_left : (Cminor.expression -> 'a list -> 'a) ->
    21                      (Cminor.statement -> 'a list -> 'b list -> 'b) ->
    22                      Cminor.statement ->
    23                      'b
     13val expression : (Cminor.expression -> 'a list -> 'a) ->
     14                 Cminor.expression ->
     15                 'a
    2416
     17val statement_subs : Cminor.statement ->
     18                     (Cminor.expression list * Cminor.statement list)
    2519
    26 (* In [expression_right f e], [f]'s second argument is the list of
    27    [expression_right]'s results on [e]'s sub-expressions. The results are
    28    computed from right to left following their appearance order in the
    29    [Cminor.expression] type. *)
     20val statement_fill_subs : Cminor.statement ->
     21                          Cminor.expression list ->
     22                          Cminor.statement list ->
     23                          Cminor.statement
    3024
    31 val expression_right : ('a list -> Cminor.expression -> 'a) ->
    32                        Cminor.expression ->
    33                        'a
     25(* In [statement f_expr f_stmt stmt], [f_stmt]'s second argument is the
     26   list of [expression f_expr]'s results on [stmt]'s sub-expressions, and
     27   [f_stmt]'s third argument is the list of [statement]'s results
     28   on [stmt]'s sub-statements. *)
    3429
    35 (* In [statement_right f_expr f_stmt stmt], [f_stmt]'s second argument is the
    36    list of [expression_left f_expr]'s results on [stmt]'s sub-expressions, and
    37    [f_stmt]'s third argument is the list of [statement_left]'s results
    38    on [stmt]'s sub-statements. The results are computed from right to left
    39    following their appearance order in the [Cminor.statement] type. *)
    40 
    41 val statement_right : ('a list -> Cminor.expression -> 'a) ->
    42                       ('a list -> 'b list -> Cminor.statement -> 'b) ->
    43                       Cminor.statement ->
    44                       'b
     30val statement : (Cminor.expression -> 'a list -> 'a) ->
     31                (Cminor.statement -> 'a list -> 'b list -> 'b) ->
     32                Cminor.statement ->
     33                'b
  • Deliverables/D2.2/8051/src/cminor/cminorInterpret.ml

    r740 r818  
    33
    44module Mem = Driver.CminorMemory
    5 module Value = Mem.Value
     5module Val = Mem.Value
    66module LocalEnv = Map.Make(String)
    7 type local_env = Value.t LocalEnv.t
     7type local_env = Val.t LocalEnv.t
    88type memory = Cminor.function_def Mem.memory
    99
     
    2828  | Ct_endblock of continuation
    2929  | Ct_returnto of
    30       ident option*internal_function*Value.address*local_env*continuation
     30      ident option*internal_function*Val.address*local_env*continuation
    3131
    3232type state =
    3333    State_regular of
    34       internal_function*statement*continuation*Value.address*local_env*(function_def Mem.memory)
    35   | State_call of function_def*Value.t list*continuation*(function_def Mem.memory)
    36   | State_return of Value.t*continuation*(function_def Mem.memory)
     34      internal_function*statement*continuation*Val.address*local_env*(function_def Mem.memory)
     35  | State_call of function_def*Val.t list*continuation*(function_def Mem.memory)
     36  | State_return of Val.t*continuation*(function_def Mem.memory)
    3737
    3838let string_of_local_env lenv =
    39   let f x v s = s ^ x ^ " = " ^ (Value.to_string v) ^ "  " in
     39  let f x v s = s ^ x ^ " = " ^ (Val.to_string v) ^ "  " in
    4040  LocalEnv.fold f lenv ""
    4141
     
    7272      (string_of_local_env lenv)
    7373      (Mem.to_string mem)
    74       (Value.to_string (value_of_address sp))
     74      (Val.to_string (value_of_address sp))
    7575      (string_of_statement stmt)
    7676  | State_call (_, args, _, mem) ->
    7777    Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!"
    7878      (Mem.to_string mem)
    79       (MiscPottier.string_of_list " " Value.to_string args)
     79      (MiscPottier.string_of_list " " Val.to_string args)
    8080  | State_return (v, _, mem) ->
    8181    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
    8282      (Mem.to_string mem)
    83       (Value.to_string v)
     83      (Val.to_string v)
    8484
    8585
     
    8787
    8888let init_local_env args params vars =
    89   let f_param lenv x v = LocalEnv.add x v lenv in
    90   let f_var lenv x = LocalEnv.add x Value.undef lenv in
     89  let f_param lenv (x, _) v = LocalEnv.add x v lenv in
     90  let f_var lenv (x, _) = LocalEnv.add x Val.undef lenv in
    9191  let lenv = List.fold_left2 f_param LocalEnv.empty params args in
    9292  List.fold_left f_var lenv vars
     
    9999(* Expression evaluation *)
    100100
    101 let eval_constant stack m = function
    102   | Cst_int i -> Value.of_int i
    103   | Cst_float _ -> error_float ()
    104   | Cst_addrsymbol id when Mem.mem_global m id ->
    105     value_of_address (Mem.find_global m id)
    106   | Cst_addrsymbol id -> error ("unknown global variable " ^ id ^ ".")
    107   | Cst_stackoffset o -> Value.add (value_of_address stack) (Value.of_int o)
    108 
    109 let eval_unop = function
    110   | Op_negf
    111   | Op_absf
    112   | Op_singleoffloat
    113   | Op_intoffloat
    114   | Op_intuoffloat
    115   | Op_floatofint
    116   | Op_floatofintu -> error_float ()
    117   | Op_cast8unsigned    -> Value.cast8unsigned
    118   | Op_cast8signed      -> Value.cast8signed
    119   | Op_cast16unsigned   -> Value.cast16unsigned
    120   | Op_cast16signed     -> Value.cast16signed
    121   | Op_negint           -> Value.negint
    122   | Op_notbool          -> Value.notbool
    123   | Op_notint           -> Value.notint
    124   | Op_id               -> (fun v -> v)
    125   | Op_ptrofint         -> assert false (*Not supported yet*)
    126   | Op_intofptr         -> assert false (*Not supported yet*)
    127 
    128 let eval_binop = function
    129   | Op_add
    130   | Op_addp             -> Value.add
    131   | Op_sub
    132   | Op_subp             -> Value.sub
    133   | Op_mul              -> Value.mul
    134   | Op_div              -> Value.div
    135   | Op_divu             -> Value.divu
    136   | Op_mod              -> Value.modulo
    137   | Op_modu             -> Value.modulou
    138   | Op_and              -> Value.and_op
    139   | Op_or               -> Value.or_op
    140   | Op_xor              -> Value.xor
    141   | Op_shl              -> Value.shl
    142   | Op_shr              -> Value.shr
    143   | Op_shru             -> Value.shru
    144   | Op_addf
    145   | Op_subf
    146   | Op_mulf
    147   | Op_divf
    148   | Op_cmpf _           -> error_float ()
    149   | Op_cmp(Cmp_eq)
    150   | Op_cmpp(Cmp_eq)     -> Value.cmp_eq
    151   | Op_cmp(Cmp_ne)
    152   | Op_cmpp(Cmp_ne)     -> Value.cmp_ne
    153   | Op_cmp(Cmp_gt)
    154   | Op_cmpp(Cmp_gt)     -> Value.cmp_gt
    155   | Op_cmp(Cmp_ge)
    156   | Op_cmpp(Cmp_ge)     -> Value.cmp_ge
    157   | Op_cmp(Cmp_lt)
    158   | Op_cmpp(Cmp_lt)     -> Value.cmp_lt
    159   | Op_cmp(Cmp_le)
    160   | Op_cmpp(Cmp_le)     -> Value.cmp_le
    161   | Op_cmpu(Cmp_eq)     -> Value.cmp_eq_u
    162   | Op_cmpu(Cmp_ne)     -> Value.cmp_ne_u
    163   | Op_cmpu(Cmp_gt)     -> Value.cmp_gt_u
    164   | Op_cmpu(Cmp_ge)     -> Value.cmp_ge_u
    165   | Op_cmpu(Cmp_lt)     -> Value.cmp_lt_u
    166   | Op_cmpu(Cmp_le)     -> Value.cmp_le_u
    167 
    168 let rec eval_expression stack local_env memory = function
    169   | Id x when LocalEnv.mem x local_env -> (LocalEnv.find x local_env,[])
    170   | Id x -> error ("unknown local variable " ^ x ^ ".")
    171   | Cst(c) -> (eval_constant stack memory c,[])
    172   | Op1(op,arg) ->
    173     let (v,l) = eval_expression stack local_env memory arg in
    174     (eval_unop op v,l)
    175   | Op2(op,arg1,arg2) ->
    176     let (v1,l1) = eval_expression stack local_env memory arg1 in
    177     let (v2,l2) = eval_expression stack local_env memory arg2 in
    178     (eval_binop op v1 v2,l1@l2)
    179   | Mem(q,a) ->
    180     let (v,l) = eval_expression stack local_env memory a in
    181     (Mem.loadq memory q (address_of_value v),l)
    182   | Cond(a1,a2,a3) ->
    183     let (v1,l1) = eval_expression stack local_env memory a1 in
    184     if Value.is_true v1 then
    185       let (v2,l2) = eval_expression stack local_env memory a2 in
    186       (v2,l1@l2)
    187     else
    188       if Value.is_false v1 then
    189         let (v3,l3) = eval_expression stack local_env memory a3 in
    190         (v3,l1@l3)
    191       else error "undefined conditional value."
    192   | Exp_cost(lbl,e) ->
    193     let (v,l) = eval_expression stack local_env memory e in
    194     (v,l@[lbl])
     101module Eval_op (M : Memory.S) = struct
     102
     103  let concrete_stacksize = M.concrete_size
     104
     105  let ext_fun_of_sign = function
     106    | AST.Signed -> M.Value.sign_ext
     107    | AST.Unsigned -> M.Value.zero_ext
     108
     109  let cast_to_std t v = match t with
     110    | AST.Sig_int (size, sign) -> (ext_fun_of_sign sign) v size M.int_size
     111    | AST.Sig_float _ -> error_float ()
     112    | AST.Sig_offset | AST.Sig_ptr -> v
     113
     114  let cast_from_std t v = match t with
     115    | AST.Sig_int (size, _) -> (ext_fun_of_sign AST.Unsigned) v M.int_size size
     116    | AST.Sig_float _ -> error_float ()
     117    | AST.Sig_offset | AST.Sig_ptr -> v
     118
     119  let cst mem sp t = function
     120    | Cst_int i -> cast_to_std t (M.Value.of_int i)
     121    | Cst_float _ -> error_float ()
     122    | Cst_addrsymbol id when M.mem_global mem id ->
     123      value_of_address (M.find_global mem id)
     124    | Cst_addrsymbol id -> error ("unknown global variable " ^ id ^ ".")
     125    | Cst_stack -> value_of_address sp
     126    | Cst_offset off -> M.Value.of_int (M.concrete_offset off)
     127    | Cst_sizeof t' -> cast_to_std t (M.Value.of_int (M.concrete_size t'))
     128
     129  let fun_of_op1 = function
     130    | Op_cast ((from_size, from_sign), to_size) ->
     131      (fun v -> (ext_fun_of_sign from_sign) v from_size to_size)
     132    | Op_negint -> M.Value.negint
     133    | Op_notbool -> M.Value.notbool
     134    | Op_notint -> M.Value.negint
     135    | Op_id -> (fun v -> v)
     136    | Op_ptrofint
     137    | Op_intofptr ->
     138      error "conversion between integers and pointers not supported yet."
     139
     140  let op1 ret_type t op v =
     141    cast_from_std ret_type ((fun_of_op1 op) (cast_to_std t v))
     142
     143  let fun_of_op2 = function
     144    | Op_add | Op_addp -> M.Value.add
     145    | Op_sub | Op_subp | Op_subpp -> M.Value.sub
     146    | Op_mul -> M.Value.mul
     147    | Op_div -> M.Value.div
     148    | Op_divu -> M.Value.divu
     149    | Op_mod -> M.Value.modulo
     150    | Op_modu -> M.Value.modulou
     151    | Op_and -> M.Value.and_op
     152    | Op_or -> M.Value.or_op
     153    | Op_xor -> M.Value.xor
     154    | Op_shl -> M.Value.shl
     155    | Op_shr -> M.Value.shr
     156    | Op_shru -> M.Value.shru
     157    | Op_cmp Cmp_eq | Op_cmpp Cmp_eq -> M.Value.cmp_eq
     158    | Op_cmp Cmp_ne | Op_cmpp Cmp_ne -> M.Value.cmp_ne
     159    | Op_cmp Cmp_gt | Op_cmpp Cmp_gt -> M.Value.cmp_gt
     160    | Op_cmp Cmp_ge | Op_cmpp Cmp_ge -> M.Value.cmp_ge
     161    | Op_cmp Cmp_lt | Op_cmpp Cmp_lt -> M.Value.cmp_lt
     162    | Op_cmp Cmp_le | Op_cmpp Cmp_le -> M.Value.cmp_le
     163    | Op_cmpu Cmp_eq -> M.Value.cmp_eq_u
     164    | Op_cmpu Cmp_ne -> M.Value.cmp_ne_u
     165    | Op_cmpu Cmp_gt -> M.Value.cmp_gt_u
     166    | Op_cmpu Cmp_ge -> M.Value.cmp_ge_u
     167    | Op_cmpu Cmp_lt -> M.Value.cmp_lt_u
     168    | Op_cmpu Cmp_le -> M.Value.cmp_le_u
     169
     170  let op2 ret_type t1 t2 op2 v1 v2 =
     171    let v1 = cast_to_std t1 v1 in
     172    let v2 = cast_to_std t2 v2 in
     173    cast_from_std ret_type ((fun_of_op2 op2) v1 v2)
     174end
     175
     176module Eval = Eval_op (Mem)
     177
     178let concrete_stacksize = Eval.concrete_stacksize
     179let eval_constant = Eval.cst
     180let eval_unop = Eval.op1
     181let eval_binop = Eval.op2
     182
     183let type_of_expr (Cminor.Expr (_, t)) = t
     184
     185let rec eval_expression stack local_env memory (Cminor.Expr (ed, t)) =
     186  match ed with
     187    | Id x when LocalEnv.mem x local_env -> (LocalEnv.find x local_env,[])
     188    | Id x -> error ("unknown local variable " ^ x ^ ".")
     189    | Cst(c) -> (eval_constant memory stack t c,[])
     190    | Op1(op,arg) ->
     191      let (v,l) = eval_expression stack local_env memory arg in
     192      (eval_unop t (type_of_expr arg) op v,l)
     193    | Op2(op, arg1, arg2) ->
     194      let (v1,l1) = eval_expression stack local_env memory arg1 in
     195      let (v2,l2) = eval_expression stack local_env memory arg2 in
     196      (eval_binop t (type_of_expr arg1) (type_of_expr arg2) op v1 v2,l1@l2)
     197    | Mem(q,a) ->
     198      let (v,l) = eval_expression stack local_env memory a in
     199      (Mem.loadq memory q (address_of_value v),l)
     200    | Cond(a1,a2,a3) ->
     201      let (v1,l1) = eval_expression stack local_env memory a1 in
     202      if Val.is_true v1 then
     203        let (v2,l2) = eval_expression stack local_env memory a2 in
     204        (v2,l1@l2)
     205      else
     206        if Val.is_false v1 then
     207          let (v3,l3) = eval_expression stack local_env memory a3 in
     208          (v3,l1@l3)
     209        else error "undefined conditional value."
     210    | Exp_cost(lbl,e) ->
     211      let (v,l) = eval_expression stack local_env memory e in
     212      (v,l@[lbl])
    195213
    196214let eval_exprlist sp lenv mem es =
     
    248266  | St_skip,Ct_endblock(k) -> (State_regular(f, St_skip, k, sigma, e, m),[])
    249267  | St_skip, (Ct_returnto _ as k) ->
    250     (State_return (Value.undef,k,Mem.free m sigma),[])
     268    (State_return (Val.undef,k,Mem.free m sigma),[])
    251269  | St_skip,Ct_stop ->
    252     (State_return (Value.undef,Ct_stop,Mem.free m sigma),[])
     270    (State_return (Val.undef,Ct_stop,Mem.free m sigma),[])
    253271  | St_assign(x,exp),_ ->
    254272    let (v,l) = eval_expression sigma e m exp in
     
    268286    let (v,l) = eval_expression sigma e m exp in
    269287    let next_stmt =
    270       if Value.is_true v then s1
     288      if Val.is_true v then s1
    271289      else
    272         if Value.is_false v then s2
     290        if Val.is_false v then s2
    273291        else error "undefined conditional value." in
    274292      (State_regular(f,next_stmt,k,sigma,e,m),l)
     
    285303  | St_switch(exp,lst,def),_ ->
    286304    let (v,l) = eval_expression sigma e m exp in
    287     if Value.is_int v then
     305    if Val.is_int v then
    288306      try
    289         let i = Value.to_int v in
     307        let i = Val.to_int v in
    290308        let nb_exit =
    291309          if List.mem_assoc i lst then List.assoc i lst
     
    295313    else error "undefined switch value."
    296314  | St_return(None),_ ->
    297     (State_return (Value.undef,callcont k,Mem.free m sigma),[])
     315    (State_return (Val.undef,callcont k,Mem.free m sigma),[])
    298316  | St_return(Some(a)),_ ->
    299317      let (v,l) = eval_expression sigma e m a in
     
    307325let interpret_external k mem f args =
    308326  let (mem', v) = match InterpretExternal.t mem f args with
    309     | (mem', InterpretExternal.V v) -> (mem', v)
     327    | (mem', InterpretExternal.V vs) ->
     328      let v = if List.length vs = 0 then Val.undef else List.hd vs in
     329      (mem', v)
    310330    | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in
    311331  State_return (v, k, mem')
     
    313333let step_call vargs k m = function
    314334  | F_int f ->
    315     let (m, sp) = Mem.alloc m f.f_stacksize in
     335    let (m, sp) = Mem.alloc m (concrete_stacksize f.f_stacksize) in
    316336    let lenv = init_local_env vargs f.f_params f.f_vars in
    317337    State_regular(f,f.f_body,k,sp,lenv,m)
     
    330350
    331351let init_mem prog =
    332   let f_var mem (x, init_datas) = Mem.add_var mem x init_datas in
     352  let f_var mem (x, size, init_datas) = Mem.add_var mem x size init_datas in
    333353  let mem = List.fold_left f_var Mem.empty prog.vars in
    334354  let f_fun_def mem (f, def) = Mem.add_fun_def mem f def in
     
    336356
    337357let compute_result v =
    338   if Value.is_int v then IntValue.Int8.cast (Value.to_int_repr v)
    339   else IntValue.Int8.zero
     358  if Val.is_int v then IntValue.Int32.cast (Val.to_int_repr v)
     359  else IntValue.Int32.zero
    340360
    341361let rec exec debug trace (state, l) =
     
    343363  let print_and_return_result res =
    344364    if debug then Printf.printf "Result = %s\n%!"
    345       (IntValue.Int8.to_string res) ;
     365      (IntValue.Int32.to_string res) ;
    346366    (res, cost_labels) in
    347367  if debug then print_state state ;
     
    350370      print_and_return_result (compute_result v)
    351371    | State_regular(_,St_skip,Ct_stop,_,_,_) -> (* Implicit return in main *)
    352       print_and_return_result IntValue.Int8.zero
     372      print_and_return_result IntValue.Int32.zero
    353373    | state -> exec debug cost_labels (step state)
    354374
    355375let interpret debug prog =
    356   if debug then Printf.printf "*** Cminor ***\n\n%!" ;
     376  Printf.printf "*** Cminor interpret ***\n%!" ;
    357377  match prog.main with
    358     | None -> (IntValue.Int8.zero, [])
     378    | None -> (IntValue.Int32.zero, [])
    359379    | Some main ->
    360380      let mem = init_mem prog in
  • Deliverables/D2.2/8051/src/cminor/cminorInterpret.mli

    r486 r818  
    33    also print debug informations.  *)
    44
     5module Eval_op (M : Memory.S) : sig
     6  val concrete_stacksize : AST.abstract_size -> int
     7  val cst :
     8    'a M.memory -> M.Value.address -> AST.sig_type -> AST.cst -> M.Value.t
     9  val op1 :
     10    AST.sig_type (* returned type *) -> AST.sig_type -> AST.op1 -> M.Value.t ->
     11    M.Value.t
     12  val op2 :
     13    AST.sig_type (* returned type *) -> AST.sig_type -> AST.sig_type ->
     14    AST.op2 -> M.Value.t -> M.Value.t -> M.Value.t
     15end
     16
    517val interpret : bool -> Cminor.program -> AST.trace
  • Deliverables/D2.2/8051/src/cminor/cminorLabelling.ml

    r486 r818  
    7373
    7474let add_cost_labels_body cost_universe stmt =
    75   CminorFold.statement_left
     75  CminorFold.statement
    7676    (f_add_cost_labels_exp cost_universe)
    7777    (f_add_cost_labels_body cost_universe)
  • Deliverables/D2.2/8051/src/cminor/cminorLexer.mll

    r740 r818  
    7272(*  | "in"    { IN } *)
    7373  | "int"    { INT }
     74  | "int8"    { INT8 }
    7475  | "int16"    { INT16 }
    75   | "int16s"    { INT16S }
    76   | "int16u"    { INT16U }
    7776  | "int32"    { INT32 }
    78   | "int8"    { INT8 }
    79   | "int8s"    { INT8S }
    80   | "int8u"    { INT8U }
     77  | "int8sto8"    { INT8STO8 }
     78  | "int8sto16"    { INT8STO16 }
     79  | "int8sto32"    { INT8STO32 }
     80  | "int8uto8"    { INT8UTO8 }
     81  | "int8uto16"    { INT8UTO16 }
     82  | "int8uto32"    { INT8UTO32 }
     83  | "int16sto8"    { INT16STO8 }
     84  | "int16sto16"    { INT16STO16 }
     85  | "int16sto32"    { INT16STO32 }
     86  | "int16uto8"    { INT16UTO8 }
     87  | "int16uto16"    { INT16UTO16 }
     88  | "int16uto32"    { INT16UTO32 }
     89  | "int32sto8"    { INT32STO8 }
     90  | "int32sto16"    { INT32STO16 }
     91  | "int32sto32"    { INT32STO32 }
     92  | "int32uto8"    { INT32UTO8 }
     93  | "int32uto16"    { INT32UTO16 }
     94  | "int32uto32"    { INT32UTO32 }
    8195  | "intoffloat"    { INTOFFLOAT }
    8296  | "intuoffloat"    { INTUOFFLOAT }
  • Deliverables/D2.2/8051/src/cminor/cminorParser.mly

    r740 r818  
    2525  open Cminor
    2626  open Memory
     27
     28  let error_prefix = "Cminor parser"
     29  let error s = Error.global_error error_prefix s
     30  let warning s = Error.warning error_prefix s
     31  let error_float () = error "float not supported."
     32
     33  let uint32 = (4, Unsigned)
     34  let int32 = (4, Signed)
    2735
    2836  (* Function calls are not allowed in the AST of expressions, but function
     
    269277%token IF
    270278%token INT
     279%token INT8
    271280%token INT16
    272 %token INT16S
    273 %token INT16U
    274281%token INT32
    275 %token INT8
    276 %token INT8S
    277 %token INT8U
     282%token INT8STO8
     283%token INT8STO16
     284%token INT8STO32
     285%token INT8UTO8
     286%token INT8UTO16
     287%token INT8UTO32
     288%token INT16STO8
     289%token INT16STO16
     290%token INT16STO32
     291%token INT16UTO8
     292%token INT16UTO16
     293%token INT16UTO32
     294%token INT32STO8
     295%token INT32STO16
     296%token INT32STO32
     297%token INT32UTO8
     298%token INT32UTO16
     299%token INT32UTO32
    278300%token <int> INTLIT
    279301%token INTOFFLOAT
     
    339361%left PLUS PLUSF MINUS MINUSF
    340362%left STAR SLASH PERCENT STARF SLASHF SLASHU PERCENTU
    341 %nonassoc BANG TILDE p_uminus ABSF INTOFFLOAT INTUOFFLOAT FLOATOFINT FLOATOFINTU INT8S INT8U INT16S INT16U FLOAT32 /* ALLOC */
     363%nonassoc BANG TILDE p_uminus ABSF INTOFFLOAT INTUOFFLOAT FLOATOFINT FLOATOFINTU FLOAT32 /* ALLOC */
    342364%left LPAREN
    343365
     
    522544  | STRINGLIT                           { RCst (Cst_addrsymbol $1) }
    523545  | AMPERSAND INTLIT                    { RCst (Cst_stackoffset $2) }
    524   | MINUS expr    %prec p_uminus        { ROp1 (Op_negint, $2) }
    525   | MINUSF expr   %prec p_uminus        { ROp1 (Op_negf, $2) }
    526   | ABSF expr                           { ROp1 (Op_absf, $2) }
    527   | INTOFFLOAT expr                     { ROp1 (Op_intoffloat, $2) }
    528   | INTUOFFLOAT expr                    { ROp1 (Op_intuoffloat, $2) }
    529   | FLOATOFINT expr                     { ROp1 (Op_floatofint, $2) }
    530   | FLOATOFINTU expr                    { ROp1 (Op_floatofintu, $2) }
    531   | TILDE expr                          { ROp1 (Op_notint, $2) }
     546  | MINUS expr    %prec p_uminus        { ROp1 (Op_negint int32, $2) }
     547  | MINUSF expr   %prec p_uminus        { error_float () }
     548  | ABSF expr                           { error_float () }
     549  | INTOFFLOAT expr                     { error_float () }
     550  | INTUOFFLOAT expr                    { error_float () }
     551  | FLOATOFINT expr                     { error_float () }
     552  | FLOATOFINTU expr                    { error_float () }
     553  | TILDE expr                          { ROp1 (Op_notint int32, $2) }
    532554  | BANG expr                           { ROp1 (Op_notbool, $2) }
    533   | INT8S expr                          { ROp1 (Op_cast8signed, $2) }
    534   | INT8U expr                          { ROp1 (Op_cast8unsigned, $2) }
    535   | INT16S expr                         { ROp1 (Op_cast16signed, $2) }
    536   | INT16U expr                         { ROp1 (Op_cast16unsigned, $2) }
    537   | FLOAT32 expr                        { ROp1 (Op_singleoffloat, $2) }
    538   | expr PLUS expr                      { ROp2 (Op_add, $1, $3) }
    539   | expr MINUS expr                     { ROp2 (Op_sub, $1, $3) }
    540   | expr STAR expr                      { ROp2 (Op_mul, $1, $3) }
    541   | expr SLASH expr                     { ROp2 (Op_div, $1, $3) }
    542   | expr PERCENT expr                   { ROp2 (Op_mod, $1, $3) }
    543   | expr SLASHU expr                    { ROp2 (Op_divu, $1, $3) }
    544   | expr PERCENTU expr                  { ROp2 (Op_modu, $1, $3) }
     555  | INT8STO8 expr                       { ROp1 (Op_cast ((8, Signed), 8), $2) }
     556  | INT8STO16 expr                      { ROp1 (Op_cast ((8, Signed), 16), $2) }
     557  | INT8STO32 expr                      { ROp1 (Op_cast ((8, Signed), 32), $2) }
     558  | INT8UTO8 expr                      { ROp1 (Op_cast ((8, Unsigned), 8), $2) }
     559  | INT8UTO16 expr                    { ROp1 (Op_cast ((8, Unsigned), 16), $2) }
     560  | INT8UTO32 expr                    { ROp1 (Op_cast ((8, Unsigned), 32), $2) }
     561  | INT16STO8 expr                     { ROp1 (Op_cast ((16, Signed), 16), $2) }
     562  | INT16STO16 expr                    { ROp1 (Op_cast ((16, Signed), 16), $2) }
     563  | INT16STO32 expr                    { ROp1 (Op_cast ((16, Signed), 32), $2) }
     564  | INT16UTO8 expr                    { ROp1 (Op_cast ((16, Unsigned), 8), $2) }
     565  | INT16UTO16 expr                  { ROp1 (Op_cast ((16, Unsigned), 16), $2) }
     566  | INT16UTO32 expr                  { ROp1 (Op_cast ((16, Unsigned), 32), $2) }
     567  | INT32STO8 expr                      { ROp1 (Op_cast ((32, Signed), 8), $2) }
     568  | INT32STO16 expr                    { ROp1 (Op_cast ((32, Signed), 16), $2) }
     569  | INT32STO32 expr                    { ROp1 (Op_cast ((32, Signed), 32), $2) }
     570  | INT32UTO8 expr                    { ROp1 (Op_cast ((32, Unsigned), 8), $2) }
     571  | INT32UTO16 expr                  { ROp1 (Op_cast ((32, Unsigned), 16), $2) }
     572  | INT32UTO32 expr                  { ROp1 (Op_cast ((32, Unsigned), 32), $2) }
     573  | FLOAT32 expr                        { error_float () }
     574  | expr PLUS expr                      { ROp2 (Op_add int32, $1, $3) }
     575  | expr MINUS expr                     { ROp2 (Op_sub int32, $1, $3) }
     576  | expr STAR expr                      { ROp2 (Op_mul int32, $1, $3) }
     577  | expr SLASH expr                     { ROp2 (Op_div int32, $1, $3) }
     578  | expr PERCENT expr                   { ROp2 (Op_mod int32, $1, $3) }
     579  | expr SLASHU expr                    { ROp2 (Op_div uint32, $1, $3) }
     580  | expr PERCENTU expr                  { ROp2 (Op_mod uint32, $1, $3) }
    545581  | expr AMPERSAND expr                 { ROp2 (Op_and, $1, $3) }
    546582  | expr BAR expr                       { ROp2 (Op_or, $1, $3) }
    547583  | expr CARET expr                     { ROp2 (Op_xor, $1, $3) }
    548   | expr LESSLESS expr                  { ROp2 (Op_shl, $1, $3) }
    549   | expr GREATERGREATER expr            { ROp2 (Op_shr, $1, $3) }
    550   | expr GREATERGREATERU expr           { ROp2 (Op_shru, $1, $3) }
    551   | expr PLUSF expr                     { ROp2 (Op_addf, $1, $3) }
    552   | expr MINUSF expr                    { ROp2 (Op_subf, $1, $3) }
    553   | expr STARF expr                     { ROp2 (Op_mulf, $1, $3) }
    554   | expr SLASHF expr                    { ROp2 (Op_divf, $1, $3) }
    555   | expr EQUALEQUAL expr                { ROp2 (Op_cmp Cmp_eq, $1, $3) }
    556   | expr BANGEQUAL expr                 { ROp2 (Op_cmp Cmp_ne, $1, $3) }
    557   | expr LESS expr                      { ROp2 (Op_cmp Cmp_lt, $1, $3) }
    558   | expr LESSEQUAL expr                 { ROp2 (Op_cmp Cmp_le, $1, $3) }
    559   | expr GREATER expr                   { ROp2 (Op_cmp Cmp_gt, $1, $3) }
    560   | expr GREATEREQUAL expr              { ROp2 (Op_cmp Cmp_ge, $1, $3) }
    561   | expr EQUALEQUALU expr               { ROp2 (Op_cmpu Cmp_eq, $1, $3) }
    562   | expr BANGEQUALU expr                { ROp2 (Op_cmpu Cmp_ne, $1, $3) }
    563   | expr LESSU expr                     { ROp2 (Op_cmpu Cmp_lt, $1, $3) }
    564   | expr LESSEQUALU expr                { ROp2 (Op_cmpu Cmp_le, $1, $3) }
    565   | expr GREATERU expr                  { ROp2 (Op_cmpu Cmp_gt, $1, $3) }
    566   | expr GREATEREQUALU expr             { ROp2 (Op_cmpu Cmp_ge, $1, $3) }
    567   | expr EQUALEQUALF expr               { ROp2 (Op_cmpf Cmp_eq, $1, $3) }
    568   | expr BANGEQUALF expr                { ROp2 (Op_cmpf Cmp_ne, $1, $3) }
    569   | expr LESSF expr                     { ROp2 (Op_cmpf Cmp_lt, $1, $3) }
    570   | expr LESSEQUALF expr                { ROp2 (Op_cmpf Cmp_le, $1, $3) }
    571   | expr GREATERF expr                  { ROp2 (Op_cmpf Cmp_gt, $1, $3) }
    572   | expr GREATEREQUALF expr             { ROp2 (Op_cmpf Cmp_ge, $1, $3) }
     584  | expr LESSLESS expr                  { ROp2 (Op_shl int32, $1, $3) }
     585  | expr GREATERGREATER expr            { ROp2 (Op_shr int32, $1, $3) }
     586  | expr GREATERGREATERU expr           { ROp2 (Op_shr uint32, $1, $3) }
     587  | expr PLUSF expr                     { error_float () }
     588  | expr MINUSF expr                    { error_float () }
     589  | expr STARF expr                     { error_float () }
     590  | expr SLASHF expr                    { error_float () }
     591  | expr EQUALEQUAL expr               { ROp2 (Op_cmp (Cmp_eq, int32), $1, $3) }
     592  | expr BANGEQUAL expr                { ROp2 (Op_cmp (Cmp_ne, int32), $1, $3) }
     593  | expr LESS expr                     { ROp2 (Op_cmp (Cmp_lt, int32), $1, $3) }
     594  | expr LESSEQUAL expr                { ROp2 (Op_cmp (Cmp_le, int32), $1, $3) }
     595  | expr GREATER expr                  { ROp2 (Op_cmp (Cmp_gt, int32), $1, $3) }
     596  | expr GREATEREQUAL expr             { ROp2 (Op_cmp (Cmp_ge, int32), $1, $3) }
     597  | expr EQUALEQUALU expr             { ROp2 (Op_cmp (Cmp_eq, uint32), $1, $3) }
     598  | expr BANGEQUALU expr              { ROp2 (Op_cmp (Cmp_ne, uint32), $1, $3) }
     599  | expr LESSU expr                   { ROp2 (Op_cmp (Cmp_lt, uint32), $1, $3) }
     600  | expr LESSEQUALU expr              { ROp2 (Op_cmp (Cmp_le, uint32), $1, $3) }
     601  | expr GREATERU expr                { ROp2 (Op_cmp (Cmp_gt, uint32), $1, $3) }
     602  | expr GREATEREQUALU expr           { ROp2 (Op_cmp (Cmp_ge, uint32), $1, $3) }
     603  | expr EQUALEQUALF expr               { error_float () }
     604  | expr BANGEQUALF expr                { error_float () }
     605  | expr LESSF expr                     { error_float () }
     606  | expr LESSEQUALF expr                { error_float () }
     607  | expr GREATERF expr                  { error_float () }
     608  | expr GREATEREQUALF expr             { error_float () }
    573609  | quantity LBRACKET expr RBRACKET       { RMem ($1, $3) }
    574610  | expr AMPERSANDAMPERSAND expr        { RCond ($1, $3, RCst (Cst_int 0)) }
  • Deliverables/D2.2/8051/src/cminor/cminorPrinter.ml

    r740 r818  
    11open AST
    22
    3 let print_type = function
    4   | Sig_int -> "int"
    5   | Sig_float -> "float"
    6   | Sig_ptr -> "ptr"
    7 
    8 let print_ret_type = function
    9   | Type_ret t -> print_type t
    10   | Type_void -> "void"
    11 
    12 let print_sig sg =
    13   let rec aux = function
    14     | [] -> ""
    15     | [t] -> (print_type t) ^ " -> "
    16     | t :: sg -> (print_type t) ^ " -> " ^ (aux sg)
    17   in
    18   (aux sg.args) ^ (print_ret_type sg.res)
    19 
     3
     4let rec print_size = function
     5  | AST.SQ q -> Memory.string_of_quantity q
     6  | AST.SProd l -> "struct {" ^ (print_size_list l) ^ "}"
     7  | AST.SSum l -> "union {" ^ (print_size_list l) ^ "}"
     8  | AST.SArray (i, se) ->
     9    (print_size se) ^ "[" ^ (string_of_int i) ^ "]"
     10and print_size_list l =
     11  MiscPottier.string_of_list ", " print_size l
     12
     13let print_stacksize = print_size
     14
     15let print_offset (size, depth) =
     16  "offset[" ^ (print_size size) ^ ", " ^ (string_of_int depth) ^ "]"
     17
     18let print_sizeof = print_size
     19
     20let print_global_size = print_size
    2021
    2122let print_data = function
     23(*
    2224  | Data_reserve n -> Printf.sprintf "[%d]" n
     25*)
    2326  | Data_int8 i -> Printf.sprintf "(int8) %d" i
    2427  | Data_int16 i -> Printf.sprintf "(int16) %d" i
     
    3538  Printf.sprintf "{%s}" (aux init)
    3639
    37 let print_var (id, init) =
    38   Printf.sprintf "var \"%s\" %s\n" id (print_datas init)
     40let print_datas_opt = function
     41  | None -> ""
     42  | Some init -> " = " ^ (print_datas init)
     43
     44let print_var (id, size, init_opt) =
     45  Printf.sprintf "var \"%s\" : %s%s;\n"
     46    id (print_global_size size) (print_datas_opt init_opt)
    3947
    4048let print_vars = List.fold_left (fun s v -> s ^ (print_var v)) ""
     
    4452  | Cst_float f -> string_of_float f
    4553  | Cst_addrsymbol id -> "\"" ^ id ^ "\""
    46   | Cst_stackoffset off -> "&" ^ (string_of_int off)
     54  | Cst_stack -> "&0"
     55  | Cst_offset off -> "{" ^ (print_offset off) ^ "}"
     56  | Cst_sizeof t -> "sizeof (" ^ (print_sizeof t) ^ ")"
    4757
    4858let print_cmp = function
     
    5565
    5666let print_op1 = function
    57   | Op_cast8unsigned -> "int8u"
    58   | Op_cast8signed -> "int8s"
    59   | Op_cast16unsigned -> "int16u"
    60   | Op_cast16signed -> "int16s"
     67  | Op_cast ((src_size, sign), dest_size) ->
     68    Printf.sprintf "int%s%sto%s"
     69      (Primitive.print_size src_size)
     70      (Primitive.print_signedness sign)
     71      (Primitive.print_size dest_size)
    6172  | Op_negint -> "-"
    6273  | Op_notbool -> "!"
    6374  | Op_notint -> "~"
    64   | Op_negf -> "-f"
    65   | Op_absf -> "absf"
    66   | Op_singleoffloat -> "float32"
    67   | Op_intoffloat -> "intoffloat"
    68   | Op_intuoffloat -> "intuoffloat"
    69   | Op_floatofint -> "floatofint"
    70   | Op_floatofintu -> "floatofintu"
    7175  | Op_id -> ""
    7276  | Op_intofptr -> "intofptr"
     
    8791  | Op_shr -> ">>"
    8892  | Op_shru -> ">>u"
    89   | Op_addf -> "+f"
    90   | Op_subf -> "-f"
    91   | Op_mulf -> "*f"
    92   | Op_divf -> "/f"
    9393  | Op_cmp cmp -> print_cmp cmp
    9494  | Op_cmpu cmp -> (print_cmp cmp) ^ "u"
    95   | Op_cmpf cmp -> (print_cmp cmp) ^ "f"
    9695  | Op_addp -> "+p"
    9796  | Op_subp -> "-p"
     97  | Op_subpp -> "-pp"
    9898  | Op_cmpp cmp -> (print_cmp cmp) ^ "p"
    9999
    100 let rec print_expression = function
     100let rec print_expression (Cminor.Expr (ed, _)) = match ed with
    101101  | Cminor.Id id -> id
    102102  | Cminor.Cst cst -> print_constant cst
    103103  | Cminor.Op1 (op1, e) ->
    104       Printf.sprintf "%s%s" (print_op1 op1) (add_parenthesis e)
     104      Printf.sprintf "%s %s" (print_op1 op1) (add_parenthesis e)
    105105  | Cminor.Op2 (op2, e1, e2) ->
    106106      Printf.sprintf "%s %s %s"
     
    117117  | Cminor.Exp_cost (lab, e) ->
    118118      Printf.sprintf "/* %s */ %s" lab (print_expression e)
    119 and add_parenthesis e = match e with
     119and add_parenthesis (Cminor.Expr (ed, _) as e) = match ed with
    120120  | Cminor.Id _ | Cminor.Cst _ | Cminor.Mem _ -> print_expression e
    121121  | _ -> Printf.sprintf "(%s)" (print_expression e)
    122122
    123123
    124 let rec print_args = function
    125   | [] -> ""
    126   | [e] -> print_expression e
    127   | e :: args -> (print_expression e) ^ ", " ^ (print_args args)
     124let print_args  =
     125  MiscPottier.string_of_list ", " print_expression
     126
     127let print_decl (x, t) = (Primitive.print_type t) ^ " " ^ x
     128
     129let print_decls vars =
     130  MiscPottier.string_of_list ", " print_decl vars
    128131
    129132
    130133let n_spaces n = String.make n ' '
    131 
    132 
    133 let print_locals vars =
    134   (MiscPottier.string_of_list ", " (fun x -> x) vars ^
    135    (if vars = [] then "" else ";"))
    136134
    137135
     
    158156        (print_expression f)
    159157        (print_args args)
    160         (print_sig sg)
     158        (Primitive.print_sig sg)
    161159  | Cminor.St_call (Some id, f, args, sg) ->
    162160      Printf.sprintf "%s%s = %s(%s) : %s;\n"
     
    165163        (print_expression f)
    166164        (print_args args)
    167         (print_sig sg)
     165        (Primitive.print_sig sg)
    168166  | Cminor.St_tailcall (f, args, sg) ->
    169167      Printf.sprintf "%stailcall %s(%s) : %s;\n"
     
    171169        (print_expression f)
    172170        (print_args args)
    173         (print_sig sg)
     171        (Primitive.print_sig sg)
    174172  | Cminor.St_seq (s1, s2) -> (print_body n s1) ^ (print_body n s2)
    175173  | Cminor.St_ifthenelse (e, s1, s2) ->
     
    214212
    215213let print_internal f_name f_def =
    216   Printf.sprintf "\"%s\" (%s) : %s {\n\n  stack %d;\n\n  vars: %s\n  pointers: %s\n\n%s}\n\n\n"
     214  Printf.sprintf "\"%s\" (%s) : %s {\n\n  stack: %s\n\n  vars: %s;\n\n%s}\n\n\n"
    217215    f_name
    218     (print_args (List.map (fun id -> Cminor.Id id) f_def.Cminor.f_params))
    219     (print_sig f_def.Cminor.f_sig)
    220     f_def.Cminor.f_stacksize
    221     (print_locals f_def.Cminor.f_vars)
    222     (print_locals f_def.Cminor.f_ptrs)
     216    (print_decls f_def.Cminor.f_params)
     217    (Primitive.print_type_return f_def.Cminor.f_return)
     218    (print_stacksize f_def.Cminor.f_stacksize)
     219    (print_decls f_def.Cminor.f_vars)
    223220    (print_body 2 f_def.Cminor.f_body)
    224221
     
    227224  Printf.sprintf "extern \"%s\" : %s\n\n\n"
    228225    f_name
    229     (print_sig f_def.ef_sig)
     226    (Primitive.print_sig f_def.ef_sig)
    230227
    231228
  • Deliverables/D2.2/8051/src/cminor/cminorToRTLabs.ml

    r740 r818  
    1212(* Helper functions *)
    1313
    14 let is_pointer_op1 = function
    15   | AST.Op_cast8unsigned | AST.Op_cast8signed | AST.Op_cast16unsigned
    16   | AST.Op_cast16signed | AST.Op_negint | AST.Op_notbool | AST.Op_notint
    17   | AST.Op_intoffloat | AST.Op_intuoffloat | AST.Op_intofptr
    18   | AST.Op_negf | AST.Op_absf | AST.Op_singleoffloat | AST.Op_floatofint
    19   | AST.Op_floatofintu ->
    20       false
    21   | AST.Op_ptrofint ->
    22       true
    23   | AST.Op_id ->
    24       assert false (* Dependent on argument. Treated in type_of_expr. *)
    25 
    26 let is_pointer_op2 = function
    27   | AST.Op_add | AST.Op_sub | AST.Op_mul | AST.Op_div | AST.Op_divu | AST.Op_mod
    28   | AST.Op_modu | AST.Op_and | AST.Op_or | AST.Op_xor | AST.Op_shl | AST.Op_shr
    29   | AST.Op_shru
    30   | AST.Op_addf | AST.Op_subf | AST.Op_mulf | AST.Op_divf
    31   | AST.Op_cmp _ | AST.Op_cmpu _ | AST.Op_cmpf _ | AST.Op_cmpp _ ->
    32       false
    33   | AST.Op_addp | AST.Op_subp ->
    34       true
    35 
    36 let rec is_pointer ptrs = function
    37   | Cminor.Id x -> List.mem x ptrs
    38   | Cminor.Cst (AST.Cst_int _)
    39   | Cminor.Cst (AST.Cst_float _) -> false
    40   | Cminor.Cst (AST.Cst_addrsymbol _)
    41   | Cminor.Cst (AST.Cst_stackoffset _) -> true
    42   | Cminor.Op1 (AST.Op_id, e) -> is_pointer ptrs e
    43   | Cminor.Op1 (op1, _) -> is_pointer_op1 op1
    44   | Cminor.Op2 (op2, _, _) -> is_pointer_op2 op2
    45   | Cminor.Mem (q, _) -> q = Memory.QPtr
    46   | Cminor.Cond _ -> false
    47   | Cminor.Exp_cost (_, e) -> is_pointer ptrs e
    48 
    49 let allocate (rtlabs_fun : RTLabs.internal_function) (is_pointer : bool)
     14let allocate (rtlabs_fun : RTLabs.internal_function) (sig_type : AST.sig_type)
    5015    : RTLabs.internal_function * Register.t =
    5116  let r = Register.fresh rtlabs_fun.RTLabs.f_runiverse in
     17  let locals = rtlabs_fun.RTLabs.f_locals @ [(r, sig_type)] in
    5218  let rtlabs_fun =
    53     { rtlabs_fun with RTLabs.f_locals = rtlabs_fun.RTLabs.f_locals @ [r] } in
    54   let rtlabs_fun =
    55     if is_pointer then
    56       { rtlabs_fun with RTLabs.f_ptrs = rtlabs_fun.RTLabs.f_ptrs @ [r] }
    57     else rtlabs_fun in
     19    { rtlabs_fun with RTLabs.f_locals = locals } in
    5820  (rtlabs_fun, r)
    5921
     22let type_of (Cminor.Expr (_, t)) = t
     23
    6024let allocate_expr
    61     (ptrs       : AST.ident list)
    6225    (rtlabs_fun : RTLabs.internal_function)
    6326    (e          : Cminor.expression)
    6427    : (RTLabs.internal_function * Register.t) =
    65   allocate rtlabs_fun (is_pointer ptrs e)
     28  allocate rtlabs_fun (type_of e)
    6629
    6730type local_env = Register.t StringTools.Map.t
     
    7134  else error ("Unknown local \"" ^ x ^ "\".")
    7235
    73 let find_olocal
    74     (rtlabs_fun : RTLabs.internal_function)
    75     (lenv       : local_env)
    76     (ox         : AST.ident option)
    77     : RTLabs.internal_function * Register.t =
     36let find_olocal (lenv : local_env) (ox : AST.ident option) : Register.t option =
    7837  match ox with
    79     | None -> allocate rtlabs_fun false
    80     | Some x -> (rtlabs_fun, find_local lenv x)
     38    | None -> None
     39    | Some x -> Some (find_local lenv x)
    8140
    8241let choose_destination
    83     (ptrs       : AST.ident list)
    8442    (rtlabs_fun : RTLabs.internal_function)
    8543    (lenv       : local_env)
     
    8745    : RTLabs.internal_function * Register.t =
    8846  match e with
    89     | Cminor.Id x -> (rtlabs_fun, find_local lenv x)
    90     | _ -> allocate_expr ptrs rtlabs_fun e
     47    | Cminor.Expr (Cminor.Id x, _) -> (rtlabs_fun, find_local lenv x)
     48    | _ -> allocate_expr rtlabs_fun e
    9149
    9250let choose_destinations
    93     (ptrs       : AST.ident list)
    9451    (rtlabs_fun : RTLabs.internal_function)
    9552    (lenv       : local_env)
     
    9754    : RTLabs.internal_function * Register.t list =
    9855  let f (rtlabs_fun, regs) e =
    99     let (rtlabs_fun, r) = choose_destination ptrs rtlabs_fun lenv e in
     56    let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in
    10057    (rtlabs_fun, regs @ [r]) in
    10158  List.fold_left f (rtlabs_fun, []) args
     
    13188
    13289
     90(*
    13391(* [addressing e] returns the type of address represented by [e],
    13492   along with its arguments *)
    13593
    136 let addressing (e : Cminor.expression)
     94let addressing (Cminor.Expr (ed, t) : Cminor.expression)
    13795    : (RTLabs.addressing * Cminor.expression list)  =
    138   match e with
     96  match ed with
    13997    | Cminor.Cst (AST.Cst_addrsymbol id) -> (RTLabs.Aglobal (id, 0), [])
    14098    | Cminor.Cst (AST.Cst_stackoffset n) -> (RTLabs.Ainstack n, [])
    141     | Cminor.Op2 (AST.Op_add,
     99    | Cminor.Op2 (AST.Op_addp _,
    142100                  Cminor.Cst (AST.Cst_addrsymbol id),
    143101                  Cminor.Cst (AST.Cst_int n)) ->
    144         (RTLabs.Aglobal (id, n), [])
    145     | Cminor.Op2 (AST.Op_add, e1, Cminor.Cst (AST.Cst_int n)) ->
    146         (RTLabs.Aindexed n, [e1])
    147     | Cminor.Op2 (AST.Op_add,
     102      (RTLabs.Aglobal (id, n), [])
     103    | Cminor.Op2 (AST.Op_addp _, e1, Cminor.Cst (AST.Cst_int n)) ->
     104      (RTLabs.Aindexed n, [e1])
     105    | Cminor.Op2 (AST.Op_addp _,
    148106                  Cminor.Cst (AST.Cst_addrsymbol id),
    149107                  e2) ->
    150         (RTLabs.Abased (id, 0), [e2])
    151     | Cminor.Op2 (AST.Op_add, e1, e2) -> (RTLabs.Aindexed2, [e1 ; e2])
     108      (RTLabs.Abased (id, 0), [e2])
     109    | Cminor.Op2 (AST.Op_addp _, e1, e2) -> (RTLabs.Aindexed2, [e1 ; e2])
    152110    | _ -> (RTLabs.Aindexed 0, [e])
    153 
    154 
    155 (* Translating conditions
    156 
    157    [ptrs] is used for typing purposes (differencing from integers and
    158    pointers). [rtlabs_fun] is the function being constructed. [lenv] is the
    159    environment associating a pseudo-register to the variables of the program
    160    being translated. *)
     111*)
     112
     113
     114(* Translating conditions *)
    161115
    162116let rec translate_branch
    163     (ptrs       : AST.ident list)
    164117    (rtlabs_fun : RTLabs.internal_function)
    165118    (lenv       : local_env)
     
    168121    (lbl_false  : Label.t)
    169122    : RTLabs.internal_function =
    170   match e with
     123  let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in
     124  let stmt = RTLabs.St_cond (r, lbl_true, lbl_false) in
     125  let rtlabs_fun = generate rtlabs_fun stmt in
     126  translate_expr rtlabs_fun lenv r e
     127
     128(*
     129  let Cminor.Expr (ed, t) = e in
     130  match ed with
    171131
    172132    | Cminor.Id x ->
     
    176136
    177137    | Cminor.Cst cst ->
    178       generate rtlabs_fun (RTLabs.St_condcst (cst, lbl_true, lbl_false))
     138      generate rtlabs_fun (RTLabs.St_condcst (cst, t, lbl_true, lbl_false))
    179139
    180140    | Cminor.Op1 (op1, e) ->
    181       let (rtlabs_fun, r) = choose_destination ptrs rtlabs_fun lenv e in
     141      let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in
    182142      let stmt = RTLabs.St_cond1 (op1, r, lbl_true, lbl_false) in
    183143      let rtlabs_fun = generate rtlabs_fun stmt in
    184       translate_expr ptrs rtlabs_fun lenv r e
     144      translate_expr rtlabs_fun lenv r e
    185145
    186146    | Cminor.Op2 (op2, e1, e2) ->
    187       let (rtlabs_fun, r1) = choose_destination ptrs rtlabs_fun lenv e1 in
    188       let (rtlabs_fun, r2) = choose_destination ptrs rtlabs_fun lenv e2 in
     147      let (rtlabs_fun, r1) = choose_destination rtlabs_fun lenv e1 in
     148      let (rtlabs_fun, r2) = choose_destination rtlabs_fun lenv e2 in
    189149      let stmt = RTLabs.St_cond2 (op2, r1, r2, lbl_true, lbl_false) in
    190150      let rtlabs_fun = generate rtlabs_fun stmt in
    191       translate_exprs ptrs rtlabs_fun lenv [r1 ; r2] [e1 ; e2]
     151      translate_exprs rtlabs_fun lenv [r1 ; r2] [e1 ; e2]
    192152
    193153    | _ ->
    194       let (rtlabs_fun, r) = choose_destination ptrs rtlabs_fun lenv e in
     154      let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in
    195155      let stmt = RTLabs.St_cond1 (AST.Op_id, r, lbl_true, lbl_false) in
    196156      let rtlabs_fun = generate rtlabs_fun stmt in
    197       translate_expr ptrs rtlabs_fun lenv r e
    198 
    199 (* Translating expressions
    200 
    201    [ptrs] is used for typing purposes (differencing from integers and
    202    pointers). [rtlabs_fun] is the function being constructed. [lenv] is the
    203    environment associating a pseudo-register to the variables of the program
    204    being translated. [destr] is the destination register. *)
     157      translate_expr rtlabs_fun lenv r e
     158*)
     159
     160(* Translating expressions *)
    205161
    206162and translate_expr
    207     (ptrs       : AST.ident list)
    208163    (rtlabs_fun : RTLabs.internal_function)
    209164    (lenv       : local_env)
     
    211166    (e          : Cminor.expression)
    212167    : RTLabs.internal_function =
    213   match e with
     168  let Cminor.Expr (ed, t) = e in
     169  match ed with
    214170
    215171    | Cminor.Id x ->
     
    228184
    229185    | Cminor.Op1 (op1, e) ->
    230       let (rtlabs_fun, r) = choose_destination ptrs rtlabs_fun lenv e in
     186      let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in
    231187      let old_entry = rtlabs_fun.RTLabs.f_entry in
    232188      let stmt = RTLabs.St_op1 (op1, destr, r, old_entry) in
    233189      let rtlabs_fun = generate rtlabs_fun stmt in
    234       translate_expr ptrs rtlabs_fun lenv r e
     190      translate_expr rtlabs_fun lenv r e
    235191
    236192    | Cminor.Op2 (op2, e1, e2) ->
    237       let (rtlabs_fun, r1) = choose_destination ptrs rtlabs_fun lenv e1 in
    238       let (rtlabs_fun, r2) = choose_destination ptrs rtlabs_fun lenv e2 in
     193      let (rtlabs_fun, r1) = choose_destination rtlabs_fun lenv e1 in
     194      let (rtlabs_fun, r2) = choose_destination rtlabs_fun lenv e2 in
    239195      let old_entry = rtlabs_fun.RTLabs.f_entry in
    240196      let stmt = RTLabs.St_op2 (op2, destr, r1, r2, old_entry) in
    241197      let rtlabs_fun = generate rtlabs_fun stmt in
    242       translate_exprs ptrs rtlabs_fun lenv [r1 ; r2] [e1 ; e2]
     198      translate_exprs rtlabs_fun lenv [r1 ; r2] [e1 ; e2]
    243199
    244200    | Cminor.Mem (chunk, e) ->
    245       let (mode, args) = addressing e in
    246       let (rtlabs_fun, regs) = choose_destinations ptrs rtlabs_fun lenv args in
    247       let old_entry = rtlabs_fun.RTLabs.f_entry in
    248       let stmt = RTLabs.St_load (chunk, mode, regs, destr, old_entry) in
    249       let rtlabs_fun = generate rtlabs_fun stmt in
    250       translate_exprs ptrs rtlabs_fun lenv regs args
     201      let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in
     202      let old_entry = rtlabs_fun.RTLabs.f_entry in
     203      let stmt = RTLabs.St_load (chunk, r, destr, old_entry) in
     204      let rtlabs_fun = generate rtlabs_fun stmt in
     205      translate_expr rtlabs_fun lenv r e
    251206
    252207    | Cminor.Cond (e1, e2, e3) ->
    253208      let old_entry = rtlabs_fun.RTLabs.f_entry in
    254       let rtlabs_fun = translate_expr ptrs rtlabs_fun lenv destr e3 in
     209      let rtlabs_fun = translate_expr rtlabs_fun lenv destr e3 in
    255210      let lbl_false = rtlabs_fun.RTLabs.f_entry in
    256211      let rtlabs_fun = change_entry rtlabs_fun old_entry in
    257       let rtlabs_fun = translate_expr ptrs rtlabs_fun lenv destr e2 in
     212      let rtlabs_fun = translate_expr rtlabs_fun lenv destr e2 in
    258213      let lbl_true = rtlabs_fun.RTLabs.f_entry in
    259       translate_branch ptrs rtlabs_fun lenv e1 lbl_true lbl_false
     214      translate_branch rtlabs_fun lenv e1 lbl_true lbl_false
    260215
    261216    | Cminor.Exp_cost (lbl, e) ->
    262       let rtlabs_fun = translate_expr ptrs rtlabs_fun lenv destr e in
     217      let rtlabs_fun = translate_expr rtlabs_fun lenv destr e in
    263218      let old_entry = rtlabs_fun.RTLabs.f_entry in
    264219      generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry))
    265220
    266221and translate_exprs
    267     (ptrs       : AST.ident list)
    268222    (rtlabs_fun : RTLabs.internal_function)
    269223    (lenv       : local_env)
     
    271225    (args       : Cminor.expression list)
    272226    : RTLabs.internal_function =
    273   let f destr e rtlabs_fun = translate_expr ptrs rtlabs_fun lenv destr e in
     227  let f destr e rtlabs_fun = translate_expr rtlabs_fun lenv destr e in
    274228  List.fold_right2 f regs args rtlabs_fun
    275229
    276230
     231(*
    277232(* Switch transformation
    278233
     
    298253    | [] -> Cminor.St_skip
    299254    | (case, exit) :: cases ->
    300         let c =
    301           Cminor.Op2 (AST.Op_cmp AST.Cmp_eq,
    302                       e, Cminor.Cst (AST.Cst_int case)) in
    303         let stmt =
    304           Cminor.St_ifthenelse (c, Cminor.St_exit exit, Cminor.St_skip) in
    305         Cminor.St_seq (stmt, aux cases)
     255      let c =
     256        Cminor.Op2 (AST.Op_cmp (AST.Cmp_eq, uint),
     257                    e, Cminor.Cst (AST.Cst_int case)) in
     258      let stmt =
     259        Cminor.St_ifthenelse (c, Cminor.St_exit exit, Cminor.St_skip) in
     260      Cminor.St_seq (stmt, aux cases)
    306261  in
    307262  Cminor.St_seq (aux cases, Cminor.St_exit dfl)
    308 
    309 
    310 (* Translating statements
    311 
    312    [ptrs] is used for typing purposes (differencing from integers and
    313    pointers). [rtlabs_fun] is the function being constructed. [lenv] is the
    314    environment associating a pseudo-register to each variable of the function
    315    being translated. [exists] is the list of label to exit to. The leftmost
    316    label in the list is used to exit the closest block. *)
     263*)
     264
     265
     266(* Translating statements *)
    317267
    318268let rec translate_stmt
    319     (ptrs       : AST.ident list)
    320269    (rtlabs_fun : RTLabs.internal_function)
    321270    (lenv       : local_env)
     
    328277
    329278    | Cminor.St_assign (x, e) ->
    330       translate_expr ptrs rtlabs_fun lenv (find_local lenv x) e
     279      translate_expr rtlabs_fun lenv (find_local lenv x) e
    331280
    332281    | Cminor.St_store (chunk, e1, e2) ->
    333       let (mode, args) = addressing e1 in
    334       let (rtlabs_fun, regs) = choose_destinations ptrs rtlabs_fun lenv args in
    335       let (rtlabs_fun, r) = choose_destination ptrs rtlabs_fun lenv e2 in
    336       let old_entry = rtlabs_fun.RTLabs.f_entry in
    337       let stmt = RTLabs.St_store (chunk, mode, regs, r, old_entry) in
    338       let rtlabs_fun = generate rtlabs_fun stmt in
    339       let rtlabs_fun = translate_expr ptrs rtlabs_fun lenv r e2 in
    340       translate_exprs ptrs rtlabs_fun lenv regs args
    341 
    342     | Cminor.St_call (oret, Cminor.Cst (AST.Cst_addrsymbol f), args, sg) ->
    343       let (rtlabs_fun, regs) = choose_destinations ptrs rtlabs_fun lenv args in
    344       let (rtlabs_fun, retr) = find_olocal rtlabs_fun lenv oret in
    345       let old_entry = rtlabs_fun.RTLabs.f_entry in
    346       let stmt = RTLabs.St_call_id (f, regs, retr, sg, old_entry) in
    347       let rtlabs_fun = generate rtlabs_fun stmt in
    348       translate_exprs ptrs rtlabs_fun lenv regs args
     282      let (rtlabs_fun, addr) = choose_destination rtlabs_fun lenv e1 in
     283      let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e2 in
     284      let old_entry = rtlabs_fun.RTLabs.f_entry in
     285      let stmt = RTLabs.St_store (chunk, addr, r, old_entry) in
     286      let rtlabs_fun = generate rtlabs_fun stmt in
     287      translate_exprs rtlabs_fun lenv [addr ; r] [e1 ; e2]
     288
     289    | Cminor.St_call (oret,
     290                      Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol f), _),
     291                      args, sg) ->
     292      let (rtlabs_fun, regs) = choose_destinations rtlabs_fun lenv args in
     293      let oretr = find_olocal lenv oret in
     294      let old_entry = rtlabs_fun.RTLabs.f_entry in
     295      let stmt = RTLabs.St_call_id (f, regs, oretr, sg, old_entry) in
     296      let rtlabs_fun = generate rtlabs_fun stmt in
     297      translate_exprs rtlabs_fun lenv regs args
    349298
    350299    | Cminor.St_call (oret, f, args, sg) ->
    351       let (rtlabs_fun, fr) = choose_destination ptrs rtlabs_fun lenv f in
    352       let (rtlabs_fun, regs) = choose_destinations ptrs rtlabs_fun lenv args in
    353       let (rtlabs_fun, retr) = find_olocal rtlabs_fun lenv oret in
    354       let old_entry = rtlabs_fun.RTLabs.f_entry in
    355       let stmt = RTLabs.St_call_ptr (fr, regs, retr, sg, old_entry) in
    356       let rtlabs_fun = generate rtlabs_fun stmt in
    357       let rtlabs_fun = translate_exprs ptrs rtlabs_fun lenv regs args in
    358       translate_expr ptrs rtlabs_fun lenv fr f
    359 
    360     | Cminor.St_tailcall (Cminor.Cst (AST.Cst_addrsymbol f), args, sg) ->
    361       let (rtlabs_fun, regs) = choose_destinations ptrs rtlabs_fun lenv args in
     300      let (rtlabs_fun, fr) = choose_destination rtlabs_fun lenv f in
     301      let (rtlabs_fun, regs) = choose_destinations rtlabs_fun lenv args in
     302      let oretr = find_olocal lenv oret in
     303      let old_entry = rtlabs_fun.RTLabs.f_entry in
     304      let stmt = RTLabs.St_call_ptr (fr, regs, oretr, sg, old_entry) in
     305      let rtlabs_fun = generate rtlabs_fun stmt in
     306      translate_exprs rtlabs_fun lenv (fr :: regs) (f :: args)
     307
     308    | Cminor.St_tailcall (Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol f), _),
     309                          args, sg) ->
     310      let (rtlabs_fun, regs) = choose_destinations rtlabs_fun lenv args in
    362311      let stmt = RTLabs.St_tailcall_id (f, regs, sg) in
    363312      let rtlabs_fun = generate rtlabs_fun stmt in
    364       translate_exprs ptrs rtlabs_fun lenv regs args
     313      translate_exprs rtlabs_fun lenv regs args
    365314
    366315    | Cminor.St_tailcall (f, args, sg) ->
    367       let (rtlabs_fun, fr) = choose_destination ptrs rtlabs_fun lenv f in
    368       let (rtlabs_fun, regs) = choose_destinations ptrs rtlabs_fun lenv args in
     316      let (rtlabs_fun, fr) = choose_destination rtlabs_fun lenv f in
     317      let (rtlabs_fun, regs) = choose_destinations rtlabs_fun lenv args in
    369318      let stmt = RTLabs.St_tailcall_ptr (fr, regs, sg) in
    370319      let rtlabs_fun = generate rtlabs_fun stmt in
    371       let rtlabs_fun = translate_exprs ptrs rtlabs_fun lenv regs args in
    372       translate_expr ptrs rtlabs_fun lenv fr f
     320      translate_exprs rtlabs_fun lenv (fr :: regs) (f :: args)
    373321
    374322    | Cminor.St_seq (s1, s2) ->
    375       let rtlabs_fun = translate_stmt ptrs rtlabs_fun lenv exits s2 in
    376       translate_stmt ptrs rtlabs_fun lenv exits s1
     323      let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s2 in
     324      translate_stmt rtlabs_fun lenv exits s1
    377325
    378326    | Cminor.St_ifthenelse (e, s1, s2) ->
    379327      let old_entry = rtlabs_fun.RTLabs.f_entry in
    380       let rtlabs_fun = translate_stmt ptrs rtlabs_fun lenv exits s2 in
     328      let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s2 in
    381329      let lbl_false = rtlabs_fun.RTLabs.f_entry in
    382330      let rtlabs_fun = change_entry rtlabs_fun old_entry in
    383       let rtlabs_fun = translate_stmt ptrs rtlabs_fun lenv exits s1 in
     331      let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s1 in
    384332      let lbl_true = rtlabs_fun.RTLabs.f_entry in
    385       translate_branch ptrs rtlabs_fun lenv e lbl_true lbl_false
     333      translate_branch rtlabs_fun lenv e lbl_true lbl_false
    386334
    387335    | Cminor.St_loop s ->
    388336      let loop_start = fresh_label rtlabs_fun in
    389337      let rtlabs_fun = change_entry rtlabs_fun loop_start in
    390       let rtlabs_fun = translate_stmt ptrs rtlabs_fun lenv exits s in
     338      let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s in
    391339      let old_entry = rtlabs_fun.RTLabs.f_entry in
    392340      add_graph rtlabs_fun loop_start (RTLabs.St_skip old_entry)
     
    394342    | Cminor.St_block s ->
    395343      let old_entry = rtlabs_fun.RTLabs.f_entry in
    396       translate_stmt ptrs rtlabs_fun lenv (old_entry :: exits) s
     344      translate_stmt rtlabs_fun lenv (old_entry :: exits) s
    397345
    398346    | Cminor.St_exit n ->
     
    402350      let rtlabs_fun = change_entry rtlabs_fun rtlabs_fun.RTLabs.f_exit in
    403351      (match eopt, rtlabs_fun.RTLabs.f_result with
    404         | None, _ -> rtlabs_fun
    405         | Some e, retr -> translate_expr ptrs rtlabs_fun lenv retr e)
     352        | None, None -> rtlabs_fun
     353        | Some e, Some (retr, _) -> translate_expr rtlabs_fun lenv retr e
     354        | _ -> assert false (* should be impossible *))
    406355
    407356    | Cminor.St_switch (e, cases, dfl) ->
     357      assert false (* should have been simplified before *)
     358(*
    408359      let stmt = transform_switch e cases dfl in
    409       translate_stmt ptrs rtlabs_fun lenv exits stmt
     360      translate_stmt rtlabs_fun lenv exits stmt
     361*)
    410362
    411363    | Cminor.St_label (lbl, s) ->
    412       let rtlabs_fun = translate_stmt ptrs rtlabs_fun lenv exits s in
     364      let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s in
    413365      let old_entry = rtlabs_fun.RTLabs.f_entry in
    414366      add_graph rtlabs_fun lbl (RTLabs.St_skip old_entry)
    415367
    416368    | Cminor.St_cost (lbl, s) ->
    417       let rtlabs_fun = translate_stmt ptrs rtlabs_fun lenv exits s in
     369      let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s in
    418370      let old_entry = rtlabs_fun.RTLabs.f_entry in
    419371      generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry))
     
    432384   - Extract the registers representing the formal variables
    433385   - Extract the registers representing the local variables
     386   - Allocate a fresh register to hold the result of the function
    434387   - Allocate a fresh label representing the exit point
    435    - Allocate fresh registers holding the result of the function
    436388   - Initialize the graph with a return instruction at the end
    437389   - Complete the graph according to the function's body.
     
    448400
    449401  (* Local environment *)
    450   let add_local lenv x =
     402  let add_local lenv (x, _) =
    451403    StringTools.Map.add x (Register.fresh runiverse) lenv in
    452404  let lenv = StringTools.Map.empty in
    453405  let lenv = List.fold_left add_local lenv f_def.Cminor.f_params in
    454406  let lenv = List.fold_left add_local lenv f_def.Cminor.f_vars in
    455   let lenv = List.fold_left add_local lenv f_def.Cminor.f_ptrs in
    456407
    457408  let extract vars =
    458     List.fold_left (fun l x -> l @ [StringTools.Map.find x lenv]) [] vars in
     409    let f l (x, t) = l @ [(find_local lenv x, t)] in
     410    List.fold_left f [] vars in
    459411
    460412  (* Parameter registers *)
    461413  let params = extract f_def.Cminor.f_params in
    462  
    463  (* Local registers *)
    464   let locals = extract (f_def.Cminor.f_vars @ f_def.Cminor.f_ptrs) in
    465 
    466  (* Pointer registers *)
    467   let ptrs = extract f_def.Cminor.f_ptrs in
     414 
     415  (* Local registers *)
     416  let locals =  extract f_def.Cminor.f_vars in
     417
     418  (* [result] is the result of the body, if any. *)
     419  let result = match f_def.Cminor.f_return with
     420    | AST.Type_void -> None
     421    | AST.Type_ret t -> Some (Register.fresh runiverse, t) in
     422
     423  let locals =
     424    locals @ (match result with None -> [] | Some (r, t) -> [(r, t)]) in
    468425
    469426  (* Exit label of the graph *)
    470427  let exit = Label.Gen.fresh luniverse in
    471428
    472   (* [retr] is the register that holds the return value of the body, if any. *)
    473   let retr = Register.fresh runiverse in
    474 
    475   let locals = locals @ [retr] in
    476 
    477429  (* The control flow graph: for now, it is only a return instruction at the
    478430     end. *)
    479   let graph = Label.Map.add exit (RTLabs.St_return retr) Label.Map.empty in
     431  let return = match result with
     432    | None -> None
     433    | Some (retr, _) -> Some retr in
     434  let graph = Label.Map.add exit (RTLabs.St_return return) Label.Map.empty in
    480435
    481436  let rtlabs_fun =
    482437    { RTLabs.f_luniverse = luniverse ;
    483438      RTLabs.f_runiverse = runiverse ;
    484       RTLabs.f_sig       = f_def.Cminor.f_sig ;
    485       RTLabs.f_result    = retr ;
     439      RTLabs.f_result    = result ;
    486440      RTLabs.f_params    = params ;
    487441      RTLabs.f_locals    = locals ;
    488       RTLabs.f_ptrs      = ptrs ;
    489442      RTLabs.f_stacksize = f_def.Cminor.f_stacksize ;
    490443      RTLabs.f_graph     = graph ;
     
    493446
    494447  (* Complete the graph *)
    495   translate_stmt f_def.Cminor.f_ptrs rtlabs_fun lenv [] f_def.Cminor.f_body
     448  translate_stmt rtlabs_fun lenv [] f_def.Cminor.f_body
    496449
    497450
    498451let translate_functions lbls (f_id, f_def) = match f_def with
    499452  | Cminor.F_int int_def ->
    500       let lbl_prefix = StringTools.Gen.fresh_prefix lbls f_id in
    501       let def = translate_internal lbl_prefix int_def in
    502       (f_id, RTLabs.F_int def)
     453    let lbl_prefix = StringTools.Gen.fresh_prefix lbls f_id in
     454    let def = translate_internal lbl_prefix int_def in
     455    (f_id, RTLabs.F_int def)
    503456  | Cminor.F_ext def -> (f_id, RTLabs.F_ext def)
    504457
     
    506459(* Initialization of globals *)
    507460
    508 let quantity_of_data data =
     461let sum_offsets =
     462  let f res off =
     463    let cst_off =
     464      Cminor.Expr (Cminor.Cst (AST.Cst_offset off), AST.Sig_offset) in
     465    Cminor.Expr (Cminor.Op2 (AST.Op_add, res, cst_off), AST.Sig_offset) in
     466  List.fold_left f (Cminor.Expr (Cminor.Cst (AST.Cst_int 0), AST.Sig_offset))
     467
     468let quantity_sig_of_data data =
    509469  let i = match data with
    510470    | AST.Data_int8 _ -> 1
     
    512472    | AST.Data_int32 _ -> 4
    513473    | _ -> assert false (* do not use on these arguments *) in
    514   Memory.QInt i
    515 
    516 let assign_data x stmt (data, off) =
    517   let e = Cminor.Op2 (AST.Op_add,
    518                       Cminor.Cst (AST.Cst_addrsymbol x),
    519                       Cminor.Cst (AST.Cst_int off)) in
     474  (AST.QInt i, AST.Sig_int (i, AST.Unsigned))
     475
     476let assign_data x stmt (offsets, data) =
     477  let off = sum_offsets offsets in
     478  let addr = Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol x), AST.Sig_ptr) in
     479  let e = Cminor.Expr (Cminor.Op2 (AST.Op_addp, addr, off), AST.Sig_ptr) in
    520480  let stmt' = match data with
     481(*
    521482    | AST.Data_reserve _ -> Cminor.St_skip
     483*)
    522484    | AST.Data_int8 i | AST.Data_int16 i | AST.Data_int32 i ->
    523         Cminor.St_store (quantity_of_data data, e, Cminor.Cst (AST.Cst_int i))
     485      let (quantity, etype) = quantity_sig_of_data data in
     486      let cst = Cminor.Expr (Cminor.Cst (AST.Cst_int i), etype) in
     487      Cminor.St_store (quantity, e, cst)
    524488    | AST.Data_float32 f | AST.Data_float64 f -> error_float () in
    525489  Cminor.St_seq (stmt, stmt')
    526490
    527491let add_global_initializations_body vars body =
    528   let f stmt (x, datas) =
    529     let offs_of_datas = RTLabsMemory.offsets_of_datas datas in
    530     List.fold_left (assign_data x) stmt offs_of_datas in
     492  let f stmt (x, size, datas_opt) = match datas_opt with
     493    | None -> Cminor.St_skip
     494    | Some datas ->
     495      let offsets = Memory.all_offsets size in
     496      if List.length offsets <> List.length datas then
     497        error "bad global initialization style."
     498      else
     499        let offs_datas = List.combine offsets datas in
     500        List.fold_left (assign_data x) stmt offs_datas in
    531501  Cminor.St_seq (List.fold_left f Cminor.St_skip vars, body)
    532502
    533503let add_global_initializations_funct vars = function
    534504  | Cminor.F_int def ->
    535       let f_body = add_global_initializations_body vars def.Cminor.f_body in
    536       Cminor.F_int { def with Cminor.f_body = f_body }
     505    let f_body = add_global_initializations_body vars def.Cminor.f_body in
     506    Cminor.F_int { def with Cminor.f_body = f_body }
    537507  | def -> def
    538508
     
    547517    MiscPottier.update_list_assoc main main_def p.Cminor.functs
    548518
    549 
    550519(* Translation of a Cminor program to a RTLabs program. *)
    551520
    552521let translate p =
    553 
    554   (* Fetch the variables in the program that are pointers (whose value is an
    555      address). Some architectures have different sizes for pointers and
    556      integers. *)
    557   let p = CminorPointers.fill p in
    558522
    559523  (* Fetch the labels already used in the program to create new ones. *)
     
    564528
    565529  (* The globals are associated their size. *)
    566   let f (id, datas) = (id, RTLabsMemory.size_of_datas datas) in
     530  let f (id, size, _) = (id, size) in
    567531
    568532  (* Put all this together and translate each function. *)
Note: See TracChangeset for help on using the changeset viewer.