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

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

Location:
Deliverables/D2.2/8051/src/clight
Files:
2 added
17 edited

Legend:

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

    r486 r818  
    88(** ** Types *)
    99
    10 (** Clight types are similar to those of C.  They include numeric types,
    11   pointers, arrays, function types, and composite types (struct and
    12   union).  Numeric types (integers and floats) fully specify the
    13   bit size of the type.  An integer type is a pair of a signed/unsigned
    14   flag and a bit size: 8, 16 or 32 bits. *)
    15 
    16 type signedness = Signed | Unsigned
    17 
    1810type intsize = I8 | I16 | I32
    19 
    20 (** Float types come in two sizes: 32 bits (single precision)
    21   and 64-bit (double precision). *)
    2211
    2312type floatsize = F32 | F64
     
    114103  | Econst_int of int                           (**r integer literal *)
    115104  | Econst_float of float                       (**r float literal *)
    116   | Evar of ident                       (**r variable *)
     105  | Evar of ident                               (**r variable *)
    117106  | Ederef of expr                              (**r pointer dereference (unary [*]) *)
    118107  | Eaddrof of expr                             (**r address-of operator ([&]) *)
     
    124113  | Eorbool of expr*expr                        (**r sequential or ([||]) *)
    125114  | Esizeof of ctype                            (**r size of a type *)
    126   | Efield of expr*ident                (**r access to a member of a struct or union *)
     115  | Efield of expr*ident                        (**r access to a member of a struct or union *)
    127116
    128117  (** The following constructors are used by the annotation process only. *)
     
    147136  | Ssequence of statement*statement            (**r sequence *)
    148137  | Sifthenelse of expr*statement*statement     (**r conditional *)
    149   | Swhile of expr*statement            (**r [while] loop *)
    150   | Sdowhile of expr*statement          (**r [do] loop *)
     138  | Swhile of expr*statement                    (**r [while] loop *)
     139  | Sdowhile of expr*statement                  (**r [do] loop *)
    151140  | Sfor of statement*expr*statement*statement  (**r [for] loop *)
    152141  | Sbreak                                      (**r [break] statement *)
     
    158147  | Scost of CostLabel.t * statement
    159148
    160                and labeled_statements =            (**r cases of a [switch] *)
     149and labeled_statements =                        (**r cases of a [switch] *)
    161150  | LSdefault of statement
    162151  | LScase of int*statement*labeled_statements
  • Deliverables/D2.2/8051/src/clight/clight32ToClight8.ml

    r740 r818  
    1212
    1313
    14 let rec seq = function
    15   | [] -> Clight.Sskip
    16   | [stmt] -> stmt
    17   | stmt :: l -> Clight.Ssequence (stmt, seq l)
    18 
    19 
    20 let call tmp f_id args_and_type res_type =
     14let error_prefix = "Clight32 to Clight8"
     15let error s = Error.global_error error_prefix s
     16
     17
     18let cint32s = Clight.Tint (Clight.I32, AST.Signed)
     19let cint32u = Clight.Tint (Clight.I32, AST.Unsigned)
     20let cint8s = Clight.Tint (Clight.I8, AST.Signed)
     21let cint8u = Clight.Tint (Clight.I8, AST.Unsigned)
     22
     23
     24(* Change the main so that it returns a 8 bits integer. Indeed, 32 bits integers
     25   will be replaced by structures, and returning a structure from the main is
     26   not Clight compliant. *)
     27
     28let main_ret_type = function
     29  | Clight.Tint (_, AST.Signed) -> cint8s
     30  | Clight.Tint (_, AST.Unsigned) -> cint8u
     31  | _ -> error "The main should return an integer which is not the case."
     32
     33let f_ctype ctype _ = ctype
     34let f_expr e _ _ = e
     35let f_expr_descr ed _ _ = ed
     36
     37let f_stmt ret_type stmt sub_exprs_res sub_stmts_res =
     38  match stmt, sub_exprs_res with
     39    | Clight.Sreturn (Some _), e :: _ ->
     40      let e' = Clight.Expr (Clight.Ecast (ret_type, e), ret_type) in
     41      Clight.Sreturn (Some e')
     42    | _ -> ClightFold.statement_fill_subs stmt sub_exprs_res sub_stmts_res
     43
     44let body_returns ret_type =
     45  ClightFold.statement f_ctype f_expr f_expr_descr (f_stmt ret_type)
     46
     47let fundef_returns_char = function
     48  | Clight.Internal cfun ->
     49    let ret_type = main_ret_type cfun.Clight.fn_return in
     50    let body = body_returns ret_type cfun.Clight.fn_body in
     51    Clight.Internal {cfun with Clight.fn_return = ret_type ;
     52                               Clight.fn_body = body }
     53  | Clight.External _ as fundef -> fundef
     54
     55let main_returns_char p = match p.Clight.prog_main with
     56  | None -> p
     57  | Some main ->
     58    let main_def = List.assoc main p.Clight.prog_funct in
     59    let main_def = fundef_returns_char main_def in
     60    let prog_funct =
     61      MiscPottier.update_list_assoc main main_def p.Clight.prog_funct in
     62    { p with Clight.prog_funct = prog_funct }
     63
     64
     65(* Replacement *)
     66
     67let seq =
     68  List.fold_left
     69    (fun stmt1 stmt2 -> Clight.Ssequence (stmt1, stmt2))
     70    Clight.Sskip
     71
     72let is_complex = function
     73  | Clight.Tstruct _ | Clight.Tunion _ -> true
     74  | _ -> false
     75
     76let is_subst_complex type_substitutions res_type =
     77  if List.mem_assoc res_type type_substitutions then
     78    is_complex (List.assoc res_type type_substitutions)
     79  else false
     80
     81let addrof_with_type e ctype =
     82  let ctype = Clight.Tpointer ctype in
     83  (Clight.Expr (Clight.Eaddrof e, ctype), ctype)
     84
     85let address_if_subst_complex type_substitutions =
     86  let f l (e, ctype) =
     87    let arg_and_type =
     88      if is_subst_complex type_substitutions ctype then addrof_with_type e ctype
     89      else (e, ctype) in
     90    l @ [arg_and_type] in
     91  List.fold_left f []
     92
     93let make_call_struct tmpe res_type f_var args args_types =
     94  let (res_e, res_type) = addrof_with_type tmpe res_type in
     95  let f_type = Clight.Tfunction (res_type :: args_types, Clight.Tvoid) in
     96  let f = Clight.Expr (f_var, f_type) in
     97  Clight.Scall (None, f, res_e :: args)
     98
     99let make_call_wo_struct tmpe res_type f_var args args_types =
     100  let f_type = Clight.Tfunction (args_types, res_type) in
     101  let f = Clight.Expr (f_var, f_type) in
     102  Clight.Scall (Some tmpe, f, args)
     103
     104let make_call type_substitutions tmp f_id args_with_types res_type =
    21105  let tmpe = Clight.Expr (Clight.Evar tmp, res_type) in
    22   let (args, args_type) = List.split args_and_type in
     106  let args_with_types =
     107    address_if_subst_complex type_substitutions args_with_types in
     108  let (args, args_types) = List.split args_with_types in
    23109  let f_var = Clight.Evar f_id in
    24   let f_type = Clight.Tfunction (args_type, res_type) in
    25   let f = Clight.Expr (f_var, f_type) in
    26   (tmpe, Clight.Scall (Some tmpe, f, args))
    27 
    28 let replace_primitives_expression fresh unop_assoc binop_assoc =
    29 
    30   let rec aux e =
    31     let Clight.Expr (ed, t) = e in
     110  let call =
     111    if is_subst_complex type_substitutions res_type then make_call_struct
     112    else make_call_wo_struct in
     113  (tmpe, call tmpe res_type f_var args args_types)
     114
     115let call fresh replaced type_substitutions replacement_assoc
     116    args added_stmt added_tmps ret_type =
     117  let tmp = fresh () in
     118  let replacement_fun_name = List.assoc replaced replacement_assoc in
     119  let (tmpe, call) =
     120    make_call type_substitutions tmp replacement_fun_name args ret_type in
     121  let stmt = seq (added_stmt @ [call]) in
     122  (tmpe, stmt, added_tmps @ [(tmp, ret_type)])
     123
     124let replace_ident replacement_assoc x t =
     125  let new_name = match t with
     126    | Clight.Tfunction _
     127        when List.mem_assoc (Runtime.Fun x) replacement_assoc ->
     128      let replacement_fun_name = List.assoc (Runtime.Fun x) replacement_assoc in
     129      replacement_fun_name
     130    | _ -> x in
     131  (Clight.Expr (Clight.Evar new_name, t), Clight.Sskip, [])
     132
     133let replace_expression fresh type_substitutions replacement_assoc e =
     134
     135  let rec aux (Clight.Expr (ed, t) as e) =
    32136    let expr ed = Clight.Expr (ed, t) in
    33137    match ed with
    34138
    35       | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Evar _
    36       | Clight.Esizeof _ ->
     139      | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Esizeof _ ->
    37140        (e, Clight.Sskip, [])
    38141
    39       | Clight.Ederef e ->
    40         let (e', stmt, tmps) = aux e in
     142      | Clight.Evar x -> replace_ident replacement_assoc x t
     143
     144      | Clight.Ederef e' ->
     145        let (e', stmt, tmps) = aux e' in
    41146        (expr (Clight.Ederef e'), stmt, tmps)
    42147
    43       | Clight.Eaddrof e ->
    44         let (e', stmt, tmps) = aux e in
     148      | Clight.Eaddrof e' ->
     149        let (e', stmt, tmps) = aux e' in
    45150        (expr (Clight.Eaddrof e'), stmt, tmps)
    46151
    47       | Clight.Eunop (unop, Clight.Expr (ed', t'))
    48           when List.mem_assoc (unop, t') unop_assoc ->
    49         let (e', stmt, tmps) = aux (Clight.Expr (ed', t')) in
    50         let tmp = fresh () in
    51         let (tmpe, call) =
    52           call tmp (List.assoc (unop, t') unop_assoc) [(e', t')] t in
    53         let stmt = seq [stmt ; call] in
    54         (tmpe, stmt, tmps @ [(tmp, t)])
    55 
    56       | Clight.Ebinop (binop, Clight.Expr (ed1, t1), Clight.Expr (ed2, t2))
    57           when List.mem_assoc (binop, t1, t2) binop_assoc ->
    58         let (e1, stmt1, tmps1) = aux (Clight.Expr (ed1, t1)) in
    59         let (e2, stmt2, tmps2) = aux (Clight.Expr (ed2, t2)) in
    60         let tmp = fresh () in
    61         let (tmpe, call) =
    62           call tmp (List.assoc (binop, t1, t2) binop_assoc)
    63             [(e1, t1) ; (e2, t2)] t in
    64         let stmt = seq [stmt1 ; stmt2 ; call] in
    65         (tmpe, stmt, tmps1 @ tmps2 @ [(tmp, t)])
    66 
    67       | _ -> (e, Clight.Sskip, []) (* TODO *)
     152      | Clight.Eunop (unop, (Clight.Expr (ed', t') as e'))
     153          when List.mem_assoc (Runtime.Unary (unop, t')) replacement_assoc ->
     154        let (e', stmt, tmps) = aux e' in
     155        call fresh (Runtime.Unary (unop, t'))
     156          type_substitutions replacement_assoc [(e', t')]
     157          [stmt] tmps t
     158
     159      | Clight.Eunop (unop, e') ->
     160        let (e', stmt, tmps) = aux e' in
     161        (expr (Clight.Eunop (unop, e')), stmt, tmps)
     162
     163      | Clight.Ebinop (binop,
     164                       (Clight.Expr (ed1, t1) as e1),
     165                       (Clight.Expr (ed2, t2) as e2))
     166          when
     167            List.mem_assoc (Runtime.Binary (binop, t1, t2)) replacement_assoc ->
     168        let (e1, stmt1, tmps1) = aux e1 in
     169        let (e2, stmt2, tmps2) = aux e2 in
     170        call fresh (Runtime.Binary (binop, t1, t2))
     171          type_substitutions replacement_assoc
     172          [(e1, t1) ; (e2, t2)] [stmt1 ; stmt2] (tmps1 @ tmps2) t
     173
     174      | Clight.Ebinop (binop, e1, e2) ->
     175        let (e1, stmt1, tmps1) = aux e1 in
     176        let (e2, stmt2, tmps2) = aux e2 in
     177        let stmt = seq [stmt1 ; stmt2] in
     178        (expr (Clight.Ebinop (binop, e1, e2)), stmt, tmps1 @ tmps2)
     179
     180      | Clight.Ecast (t, (Clight.Expr (_, t') as e'))
     181          when List.mem_assoc (Runtime.Cast (t, t')) replacement_assoc ->
     182        let (e', stmt, tmps) = aux e' in
     183        call fresh (Runtime.Cast (t, t'))
     184          type_substitutions replacement_assoc [(e', t')] [stmt]
     185          tmps t
     186
     187      | Clight.Ecast (t', e') ->
     188        let (e', stmt, tmps) = aux e' in
     189        (expr (Clight.Ecast (t', e')), stmt, tmps)
     190
     191      | Clight.Econdition (e1, e2, e3) ->
     192        let (e1, stmt1, tmps1) = aux e1 in
     193        let (e2, stmt2, tmps2) = aux e2 in
     194        let (e3, stmt3, tmps3) = aux e3 in
     195        let stmt = seq [stmt1 ; stmt2 ; stmt3] in
     196        (expr (Clight.Econdition (e1, e2, e3)), stmt, tmps1 @ tmps2 @ tmps3)
     197
     198      | Clight.Eandbool (e1, e2) ->
     199        let (e1, stmt1, tmps1) = aux e1 in
     200        let (e2, stmt2, tmps2) = aux e2 in
     201        let stmt = seq [stmt1 ; stmt2] in
     202        (expr (Clight.Eandbool (e1, e2)), stmt, tmps1 @ tmps2)
     203
     204      | Clight.Eorbool (e1, e2) ->
     205        let (e1, stmt1, tmps1) = aux e1 in
     206        let (e2, stmt2, tmps2) = aux e2 in
     207        let stmt = seq [stmt1 ; stmt2] in
     208        (expr (Clight.Eorbool (e1, e2)), stmt, tmps1 @ tmps2)
     209
     210      | Clight.Efield (e', field) ->
     211        let (e', stmt, tmps) = aux e' in
     212        (expr (Clight.Efield (e', field)), stmt, tmps)
     213
     214      | Clight.Ecost (lbl, e') ->
     215        let (e', stmt, tmps) = aux e' in
     216        (expr (Clight.Ecost (lbl, e')), stmt, tmps)
     217
     218      | Clight.Ecall (id, e1, e2) ->
     219        let (e1, stmt1, tmps1) = aux e1 in
     220        let (e2, stmt2, tmps2) = aux e2 in
     221        let stmt = seq [stmt1 ; stmt2] in
     222        (expr (Clight.Ecall (id, e1, e2)), stmt, tmps1 @ tmps2)
    68223
    69224  in
    70   aux
    71 
    72 
    73 let replace_primitives_expression_list fresh unop_assoc binop_assoc =
     225  aux e
     226
     227
     228let replace_expression_list fresh type_substitutions  replacement_assoc =
    74229  let f (l, stmt, tmps) e =
    75230    let (e', stmt', tmps') =
    76       replace_primitives_expression fresh unop_assoc binop_assoc e in
    77     (l @ [e], seq [stmt ; stmt'], tmps @ tmps') in
     231      replace_expression fresh type_substitutions replacement_assoc e in
     232    (l @ [e'], seq [stmt ; stmt'], tmps @ tmps') in
    78233  List.fold_left f ([], Clight.Sskip, [])
    79234
    80235
    81 let replace_primitives_statement fresh unop_assoc binop_assoc =
     236let replace_statement fresh type_substitutions replacement_assoc =
    82237  let aux_exp =
    83     replace_primitives_expression fresh unop_assoc binop_assoc in
     238    replace_expression fresh type_substitutions replacement_assoc in
    84239  let aux_exp_list =
    85     replace_primitives_expression_list fresh unop_assoc binop_assoc in
     240    replace_expression_list fresh type_substitutions replacement_assoc in
    86241
    87242  let rec aux = function
     
    89244    | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sgoto _
    90245    | Clight.Sreturn None
    91       as stmt -> (stmt, [])
     246        as stmt -> (stmt, [])
    92247
    93248    | Clight.Slabel (lbl, stmt) ->
     
    116271      let (args', stmt3, tmps3) = aux_exp_list args in
    117272      let stmt = seq [stmt1 ; stmt2 ; stmt3 ;
    118                            Clight.Scall (Some e', f', args')] in
     273                      Clight.Scall (Some e', f', args')] in
    119274      (stmt, tmps1 @ tmps2 @ tmps3)
    120275
     
    144299      let (stmt3', tmps3) = aux stmt3 in
    145300      let stmt = seq [stmt1' ; stmte ;
    146                       Clight.Swhile (e', seq [stmt2' ; stmt3' ; stmte])] in
     301                      Clight.Swhile (e', seq [stmt3' ; stmt2' ; stmte])] in
    147302      (stmt, tmpse @ tmps1 @ tmps2 @ tmps3)
    148303
     
    180335
    181336
    182 let replace_primitives_internal fresh unop_assoc binop_assoc def =
     337let f_ctype type_substitutions ctype sub_ctypes_res = match ctype with
     338  | _ when List.mem_assoc ctype type_substitutions ->
     339    List.assoc ctype type_substitutions
     340  | _ -> ClightFold.ctype_fill_subs ctype sub_ctypes_res
     341
     342let replace_ctype type_substitutions =
     343  ClightFold.ctype (f_ctype type_substitutions)
     344
     345let f_expr = ClightFold.expr_fill_subs
     346
     347let f_expr_descr = ClightFold.expr_descr_fill_subs
     348
     349let f_stmt = ClightFold.statement_fill_subs
     350
     351let statement_replace_ctype type_substitutions =
     352  ClightFold.statement (f_ctype type_substitutions) f_expr f_expr_descr f_stmt
     353
     354
     355let replace_internal fresh type_substitutions replacement_assoc def =
    183356  let (new_body, tmps) =
    184     replace_primitives_statement fresh unop_assoc binop_assoc
     357    replace_statement fresh type_substitutions replacement_assoc
    185358      def.Clight.fn_body in
    186   { def with Clight.fn_vars = def.Clight.fn_vars @ tmps ;
    187              Clight.fn_body = new_body }
    188 
    189 let replace_primitives_funct fresh unop_assoc binop_assoc (id, fundef) =
     359  let new_body = statement_replace_ctype type_substitutions new_body in
     360  let f (x, t) = (x, replace_ctype type_substitutions t) in
     361  let params = List.map f def.Clight.fn_params in
     362  let vars = List.map f (def.Clight.fn_vars @ tmps) in
     363  { Clight.fn_return = replace_ctype type_substitutions def.Clight.fn_return ;
     364    Clight.fn_params = params ;
     365    Clight.fn_vars = vars ;
     366    Clight.fn_body = new_body }
     367
     368let replace_funct fresh type_substitutions replacement_assoc (id, fundef) =
    190369  let fundef' = match fundef with
    191370    | Clight.Internal def ->
    192371      Clight.Internal
    193         (replace_primitives_internal fresh unop_assoc binop_assoc def)
     372        (replace_internal fresh type_substitutions replacement_assoc def)
    194373    | _ -> fundef in
    195374  (id, fundef')
    196375
    197 let replace_primitives fresh unop_assoc binop_assoc p =
     376let replace fresh type_substitutions replacement_assoc p =
    198377  let prog_funct =
    199     List.map (replace_primitives_funct fresh unop_assoc binop_assoc)
     378    List.map (replace_funct fresh type_substitutions replacement_assoc)
    200379      p.Clight.prog_funct in
    201380  { p with Clight.prog_funct = prog_funct }
    202381
    203382
     383(* The constant replacement replaces each 32 bits and 16 bits integer constant
     384   by a global variable of the same value. They will be replaced by the
     385   appropriate structural value by the global replacement that comes
     386   afterwards. *)
     387
     388module CstMap =
     389  Map.Make
     390    (struct
     391      type t = (int * Clight.intsize * Clight.ctype)
     392      let compare = Pervasives.compare
     393     end)
     394
     395let f_subs fresh replace subs map =
     396  let f (l, map) x =
     397    let (x, map) = replace fresh map x in
     398    (l @ [x], map) in
     399  List.fold_left f ([], map) subs
     400
     401let rec replace_constant_expr fresh map (Clight.Expr (ed, t) as e) =
     402  match ed, t with
     403    | Clight.Econst_int i, Clight.Tint (Clight.I8, _) ->
     404      (e, map)
     405    | Clight.Econst_int i, Clight.Tint (size, _)
     406      when CstMap.mem (i, size, t) map ->
     407      let id = CstMap.find (i, size, t) map in
     408      (Clight.Expr (Clight.Evar id, t), map)
     409    | Clight.Econst_int i, Clight.Tint (size, _) ->
     410      let id = fresh () in
     411      let map = CstMap.add (i, size, t) id map in
     412      let id = CstMap.find (i, size, t) map in
     413      (Clight.Expr (Clight.Evar id, t), map)
     414    | _ ->
     415      let (sub_ctypes, sub_exprs) = ClightFold.expr_descr_subs ed in
     416      let (sub_exprs, map) = f_subs fresh replace_constant_expr sub_exprs map in
     417      let ed = ClightFold.expr_descr_fill_subs ed sub_ctypes sub_exprs in
     418      (Clight.Expr (ed, t), map)
     419
     420let rec replace_constant_stmt fresh map stmt =
     421  let (sub_exprs, sub_stmts) = ClightFold.statement_subs stmt in
     422  let (sub_exprs, map) =
     423    f_subs fresh replace_constant_expr sub_exprs map in
     424  let (sub_stmts, map) =
     425    f_subs fresh replace_constant_stmt sub_stmts map in
     426  (ClightFold.statement_fill_subs stmt sub_exprs sub_stmts, map)
     427
     428let replace_constant_fundef fresh (functs, map) (id, fundef) =
     429  match fundef with
     430    | Clight.Internal cfun ->
     431      let (body, map) = replace_constant_stmt fresh map cfun.Clight.fn_body in
     432      let fundef = Clight.Internal { cfun with Clight.fn_body = body } in
     433      (functs @ [(id, fundef)], map)
     434    | Clight.External _ -> (functs @ [(id, fundef)], map)
     435
     436let init_datas i size =
     437  [match size with
     438    | Clight.I8 -> Clight.Init_int8 i
     439    | Clight.I16 -> Clight.Init_int16 i
     440    | Clight.I32 -> Clight.Init_int32 i]
     441
     442let globals_of_map map =
     443  let f (i, size, t) id l = l @ [((id, init_datas i size), t)] in
     444  CstMap.fold f map []
     445
     446let replace_constant p =
     447  let tmp_universe = ClightAnnotator.fresh_universe "_cst" p in
     448  let fresh () = StringTools.Gen.fresh tmp_universe in
     449  let (functs, map) =
     450    List.fold_left (replace_constant_fundef fresh)
     451      ([], CstMap.empty) p.Clight.prog_funct in
     452  let csts = globals_of_map map in
     453  { p with
     454    Clight.prog_funct = functs ; Clight.prog_vars = p.Clight.prog_vars @ csts }
     455
     456
     457(* Globals replacement *)
     458
     459let expand_int size i =
     460  let i = Big_int.big_int_of_int i in
     461  let i =
     462    if Big_int.ge_big_int i Big_int.zero_big_int then i
     463    else Big_int.add_big_int i (Big_int.power_int_positive_int 2 size) in
     464  let bound = Big_int.power_int_positive_int 2 8 in
     465  let rec aux n i =
     466    if n >= size then []
     467    else
     468      let (next, chunk) = Big_int.quomod_big_int i bound in
     469      chunk :: (aux (n+1) next) in
     470  List.map (fun i -> Clight.Init_int8 (Big_int.int_of_big_int i)) (aux 0 i)
     471
     472let expand_init_data = function
     473  | Clight.Init_int16 i -> expand_int 2 i
     474  | Clight.Init_int32 i -> expand_int 4 i
     475  | init_data -> [init_data]
     476
     477let expand_init_datas init_datas =
     478  List.flatten (List.map expand_init_data init_datas)
     479
     480let replace_global type_substitutions ((id, init_datas), t) =
     481  let init_datas = expand_init_datas init_datas in
     482  ((id, init_datas), replace_ctype type_substitutions t)
     483
     484let replace_globals type_substitutions p =
     485  let vars = List.map (replace_global type_substitutions) p.Clight.prog_vars in
     486  { p with Clight.prog_vars = vars }
     487
     488
     489(* Unsupported operations by the 8051. *)
     490
     491(* 8 bits signed division *)
     492
     493let divs_fun s _ =
     494  "signed char " ^ s ^ " (signed char x, signed char y) {\n" ^
     495  "  unsigned char x1 = (unsigned char) x;\n" ^
     496  "  unsigned char y1 = (unsigned char) y;\n" ^
     497  "  signed char sign = 1;\n" ^
     498  "  if (x < 0) { x1 = (unsigned char) (-x); sign = -sign; }\n" ^
     499  "  if (y < 0) { y1 = (unsigned char) (-y); sign = -sign; }\n" ^
     500  "  return (sign * ((signed char) (x1/y1)));\n" ^
     501  "}\n\n"
     502
     503let divs =
     504  (Runtime.Binary (Clight.Odiv, cint8s, cint8s), "_divs", [], divs_fun, [])
     505
     506
     507(* 8 bits signed modulo *)
     508
     509let mods_fun s _ =
     510  "signed char " ^ s ^ " (signed char x, signed char y) {\n" ^
     511  "  return (x - (x/y) * y);\n" ^
     512  "}\n\n"
     513
     514let mods =
     515  (Runtime.Binary (Clight.Omod, cint8s, cint8s), "_mods", [], mods_fun,
     516   [Runtime.Binary (Clight.Odiv, cint8s, cint8s)])
     517
     518
     519(* Shifts *)
     520
     521let sh_fun signedness op s _ =
     522  signedness ^ " char " ^ s ^ " (" ^ signedness ^ " char x, " ^
     523  signedness ^ " char y) {\n" ^
     524  "  " ^ signedness ^ " char res = x, i;\n" ^
     525  "  for (i = 0 ; i < y ; i++) res = res " ^ op ^ " 2;\n" ^
     526  "  return res;\n" ^
     527  "}\n\n"
     528
     529(* 8 bits shifts left *)
     530
     531let shls_fun = sh_fun "signed" "*"
     532
     533let shls =
     534  (Runtime.Binary (Clight.Oshl, cint8s, cint8s), "_shls", [], shls_fun, [])
     535
     536let shlu_fun s _ =
     537  "unsigned char " ^ s ^ " (unsigned char x, unsigned char y) {\n" ^
     538  "  return ((unsigned char) ((signed char) x << (signed char) y));\n" ^
     539  "}\n\n"
     540
     541let shlu =
     542  (Runtime.Binary (Clight.Oshl, cint8u, cint8u), "_shlu", [], shlu_fun,
     543   [Runtime.Binary (Clight.Oshl, cint8s, cint8s)])
     544
     545(* 8 bits shifts right *)
     546
     547let shrs_fun s _ =
     548  "signed char " ^ s ^ " (signed char x, signed char y) {\n" ^
     549  "  signed char res = x, i;\n" ^
     550  "  for (i = 0 ; i < y ; i++) {\n" ^
     551  "    res = ((unsigned char) res) / 2;\n" ^
     552  "    res = res + ((signed char) 128);\n" ^
     553  "  }\n" ^
     554  "  return res;\n" ^
     555  "}\n\n"
     556
     557let shrs =
     558  (Runtime.Binary (Clight.Oshr, cint8s, cint8s), "_shrs", [], shrs_fun, [])
     559
     560let shru_fun = sh_fun "unsigned" "/"
     561
     562let shru =
     563  (Runtime.Binary (Clight.Oshr, cint8u, cint8u), "_shru", [], shru_fun, [])
     564
     565
     566(* int32 *)
     567
     568let struct_int32 name fields = match fields with
     569  | lolo :: lohi :: hilo :: hihi :: _ ->
     570    Clight.Tstruct
     571      (name,
     572       [(lolo, cint8u) ; (lohi, cint8u) ; (hilo, cint8u) ; (hihi, cint8u)])
     573  | _ -> error ("bad field names when defining type " ^ name ^ ".")
     574
     575let struct_int32_name = "struct _int32_"
     576
     577let new_int32 int32 =
     578  let lolo = "lolo" in
     579  let lohi = "lohi" in
     580  let hilo = "hilo" in
     581  let hihi = "hihi" in
     582  (int32, struct_int32_name, [lolo ; lohi ; hilo ; hihi], struct_int32)
     583
     584let int32s = new_int32 (Clight.Tint (Clight.I32, AST.Signed))
     585let int32u = new_int32 (Clight.Tint (Clight.I32, AST.Unsigned))
     586
     587(* 32 bits operations *)
     588
     589(* 32 bits equality *)
     590
     591let eq_int32s_fun s l =
     592  let (int32, lolo, lohi, hilo, hihi) = match l with
     593    | (int32, lolo :: lohi :: hilo :: hihi :: _) :: _ ->
     594      (int32, lolo, lohi, hilo, hihi)
     595    | _ -> error ("new type definition not coherent in function " ^ s ^ ".") in
     596  int32 ^ " " ^ s ^ " (" ^ int32 ^ " x, " ^ int32 ^ " y) {\n" ^
     597  "  " ^ int32 ^ " res;\n" ^
     598  "  res." ^ lolo ^ " = 1;\n" ^
     599  "  if (x." ^ lolo ^ " != y." ^ lolo ^ ") res." ^ lolo ^ " = 0;\n" ^
     600  "  if (x." ^ lohi ^ " != y." ^ lohi ^ ") res." ^ lolo ^ " = 0;\n" ^
     601  "  if (x." ^ hilo ^ " != y." ^ hilo ^ ") res." ^ lolo ^ " = 0;\n" ^
     602  "  if (x." ^ hihi ^ " != y." ^ hihi ^ ") res." ^ lolo ^ " = 0;\n" ^
     603  "  res." ^ lohi ^ " = 0;\n" ^
     604  "  res." ^ hilo ^ " = 0;\n" ^
     605  "  res." ^ hihi ^ " = 0;\n" ^
     606  "  return (res);\n" ^
     607  "}\n\n"
     608
     609let eq32s =
     610  (Runtime.Binary (Clight.Oeq, cint32s, cint32s), "eq_int32s",
     611   [struct_int32_name], eq_int32s_fun, [])
     612
     613(* 32 bits casts *)
     614
     615let int32s_to_int8s_fun s l =
     616  let (int32, lolo, lohi, hilo, hihi) = match l with
     617    | (int32, lolo :: lohi :: hilo :: hihi :: _) :: _ ->
     618      (int32, lolo, lohi, hilo, hihi)
     619    | _ -> error ("new type definition not coherent in function " ^ s ^ ".") in
     620  "signed char " ^ s ^ " (" ^ int32 ^ " x) {\n" ^
     621  "  return ((signed char) x." ^ lolo ^ ");\n" ^
     622  "}\n\n"
     623
     624let int32s_to_int8s =
     625  (Runtime.Cast (cint8s, cint32s), "int32s_to_int8s", [struct_int32_name],
     626   int32s_to_int8s_fun, [])
     627
     628
     629(* int16 *)
     630
     631let struct_int16 name fields = match fields with
     632  | lo :: hi :: _ ->
     633    Clight.Tstruct (name, [(lo, cint8u) ; (hi, cint8u)])
     634  | _ -> error ("bad field names when defining type " ^ name ^ ".")
     635
     636let struct_int16_name = "struct _int16_"
     637
     638let new_int16 int16 =
     639  let lo = "lo" in
     640  let hi = "hi" in
     641  (int16, struct_int16_name, [lo ; hi], struct_int16)
     642
     643let int16s = new_int16 (Clight.Tint (Clight.I16, AST.Signed))
     644let int16u = new_int16 (Clight.Tint (Clight.I16, AST.Unsigned))
     645
     646
     647(* int32 and int16 *)
     648
     649let int32_and_int16_types = [int32s ; int32u ; int16s ; int16u]
     650let int32_and_int16_replacements = [eq32s ; int32s_to_int8s]
     651
     652
     653let unsupported = [divs ; mods ; shls ; shlu ; shrs ; shru]
     654
     655
     656let save_and_parse p =
     657  let tmp_file = Filename.temp_file "clight32toclight8" ".c" in
     658  try
     659    let oc = open_out tmp_file in
     660    output_string oc (ClightPrinter.print_program p) ;
     661    close_out oc ;
     662    let res = ClightParser.process tmp_file in
     663    Misc.SysExt.safe_remove tmp_file ;
     664    res
     665  with Sys_error _ -> failwith "Error reparsing Clight8 transformation."
     666
     667let add_replacements p new_types replacements =
     668  let p = ClightCasts.simplify p in
     669  let (p, type_substitutions, replacement_assoc) =
     670    Runtime.add p new_types replacements in
     671  let p = ClightCasts.simplify p in
     672  let tmp_universe = ClightAnnotator.fresh_universe "_tmp" p in
     673  let fresh () = StringTools.Gen.fresh tmp_universe in
     674  let p = replace fresh type_substitutions replacement_assoc p in
     675  let p = replace_globals type_substitutions p in
     676  (* Printf.printf "%s\n%!" (ClightPrinter.print_program p) ; *)
     677  let p = save_and_parse p in
     678  ClightCasts.simplify p
     679
    204680let translate p =
    205   (* TODO: restore below *)
    206 (*
    207   let (p, unop_assoc, binop_assoc) = Runtime.add p in
    208   let p = ClightCasts.simplify p in
    209   let labs = ClightAnnotator.all_labels p in
    210   let tmp_prefix = StringTools.Gen.fresh_prefix labs "_tmp" in
    211   let tmp_universe = StringTools.Gen.new_universe tmp_prefix in
    212   let fresh () = StringTools.Gen.fresh tmp_universe in
    213   let p = replace_primitives fresh unop_assoc binop_assoc p in
    214   (* TODO: do the translation *)
    215   p
    216 *)
    217   ClightCasts.simplify p
     681  let p = main_returns_char p in
     682  let p = replace_constant p in
     683  let p =
     684    add_replacements p int32_and_int16_types int32_and_int16_replacements in
     685  add_replacements p [] unsupported
  • Deliverables/D2.2/8051/src/clight/clightAnnotator.ml

    r645 r818  
    1919
    2020let triple_union
    21     (var_names1, cost_labels1, user_labels1)
    22     (var_names2, cost_labels2, user_labels2) =
    23   (StringTools.Set.union var_names1 var_names2,
     21    (names1, cost_labels1, user_labels1)
     22    (names2, cost_labels2, user_labels2) =
     23  (StringTools.Set.union names1 names2,
    2424   CostLabel.Set.union cost_labels1 cost_labels2,
    2525   Label.Set.union user_labels1 user_labels2)
     
    2727let empty_triple = (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.empty)
    2828
     29let name_singleton id =
     30  (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty)
     31
     32let cost_label_singleton cost_lbl =
     33  (StringTools.Set.empty, CostLabel.Set.singleton cost_lbl, Label.Set.empty)
     34
     35let label_singleton lbl =
     36  (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.singleton lbl)
     37
    2938let list_union l = List.fold_left triple_union empty_triple l
    3039
    31 let rec exp_idents e =
    32   let Clight.Expr (e, _) = e in
    33   match e with
    34     | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Esizeof _ ->
    35         empty_triple
    36     | Clight.Evar x ->
    37         (StringTools.Set.singleton x, CostLabel.Set.empty, Label.Set.empty)
    38     | Clight.Ederef e | Clight.Eaddrof e | Clight.Eunop (_, e)
    39     | Clight.Ecast (_, e) -> exp_idents e
    40     | Clight.Efield (e, x) ->
    41         let (var_names, cost_labels, user_labels) = exp_idents e in
    42         (StringTools.Set.add x var_names, cost_labels, user_labels)
    43     | Clight.Ebinop (_, e1, e2) | Clight.Eandbool (e1, e2)
    44     | Clight.Eorbool (e1, e2) -> list_union [exp_idents e1 ; exp_idents e2]
    45     | Clight.Econdition (e1, e2, e3) ->
    46         list_union [exp_idents e1 ; exp_idents e2 ; exp_idents e3]
    47     | Clight.Ecost (lbl, e) ->
    48         let (var_names, cost_labels, user_labels) = exp_idents e in
    49         (var_names, CostLabel.Set.add lbl cost_labels, user_labels)
    50     | Clight.Ecall (x, e1, e2) -> assert false (* Should not happen *)
    51 
    52 let exp_idents_opt = function
    53   | None -> empty_triple
    54   | Some e -> exp_idents e
    55 
    56 let exp_idents_list l = list_union (List.map exp_idents l)
    57 
    58 let rec body_idents = function
    59   | Clight.Sskip | Clight.Sbreak | Clight.Scontinue -> empty_triple
    60   | Clight.Sassign (e1, e2) -> list_union [exp_idents e1 ; exp_idents e2]
    61   | Clight.Scall (eopt, f, args) ->
    62       list_union [exp_idents_opt eopt ; exp_idents f ; exp_idents_list args]
    63   | Clight.Ssequence (s1, s2) -> list_union [body_idents s1 ; body_idents s2]
    64   | Clight.Sifthenelse (e, s1, s2) ->
    65       list_union [exp_idents e ; body_idents s1 ; body_idents s2]
    66   | Clight.Swhile (e, s) | Clight.Sdowhile (e, s) ->
    67       list_union [exp_idents e ; body_idents s]
    68   | Clight.Sfor (s1, e, s2, s3) ->
    69       list_union [body_idents s1 ; exp_idents e ;
    70                   body_idents s2 ; body_idents s3]
    71   | Clight.Sreturn eopt -> exp_idents_opt eopt
    72   | Clight.Sswitch (e, ls) -> list_union [exp_idents e ; ls_idents ls]
    73   | Clight.Slabel (lbl, stmt) ->
    74       let (var_names, cost_labels, user_labels) = body_idents stmt in
    75       (var_names, cost_labels, Label.Set.add lbl user_labels)
    76   | Clight.Sgoto lbl ->
    77       (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.singleton lbl)
    78   | Clight.Scost (lbl, stmt) ->
    79       let (var_names, cost_labels, user_labels) = body_idents stmt in
    80       (var_names, CostLabel.Set.add lbl cost_labels, user_labels)
    81 and ls_idents = function
    82   | Clight.LSdefault stmt -> body_idents stmt
    83   | Clight.LScase (_, stmt, ls) -> list_union [body_idents stmt ; ls_idents ls]
     40let f_ctype ctype sub_ctypes_res =
     41  let res = match ctype with
     42    | Clight.Tstruct (id, fields) | Clight.Tunion (id, fields) ->
     43      (string_set_of_list (id :: (List.map fst fields)),
     44       CostLabel.Set.empty, Label.Set.empty)
     45    | Clight.Tcomp_ptr id -> name_singleton id
     46    | _ -> empty_triple in
     47  list_union (res :: sub_ctypes_res)
     48
     49let f_expr _ sub_ctypes_res sub_expr_descrs_res =
     50  list_union (sub_ctypes_res @ sub_expr_descrs_res)
     51
     52let f_expr_descr ed sub_ctypes_res sub_exprs_res =
     53  let res = match ed with
     54    | Clight.Evar id | Clight.Efield (_, id) | Clight.Ecall (id, _, _) ->
     55      name_singleton id
     56    | Clight.Ecost (cost_lbl, _) -> cost_label_singleton cost_lbl
     57    | _ -> empty_triple in
     58  list_union (res :: (sub_ctypes_res @ sub_exprs_res))
     59
     60let f_stmt stmt sub_exprs_res sub_stmts_res =
     61  let stmt_res = match stmt with
     62    | Clight.Slabel (lbl, _) | Clight.Sgoto lbl -> label_singleton lbl
     63    | Clight.Scost (cost_lbl, _) -> cost_label_singleton cost_lbl
     64    | _ -> empty_triple in
     65  list_union (stmt_res :: (sub_exprs_res @ sub_stmts_res))
     66
     67let body_idents = ClightFold.statement f_ctype f_expr f_expr_descr f_stmt
    8468
    8569let prog_idents p =
     
    8973          string_set_of_list
    9074            (List.map fst (def.Clight.fn_params @ def.Clight.fn_vars)) in
    91         let (var_names, cost_labels, user_labels) =
     75        let (names, cost_labels, user_labels) =
    9276          body_idents def.Clight.fn_body in
    93         (StringTools.Set.union vars var_names, cost_labels, user_labels)
     77        (StringTools.Set.union vars names, cost_labels, user_labels)
    9478    | Clight.External (id, _, _) ->
    9579        (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty) in
    9680  let fun_idents (id, f_def) =
    97     let (var_names, cost_labels, user_labels) = def_idents f_def in
    98     (StringTools.Set.add id var_names, cost_labels, user_labels) in
     81    let (names, cost_labels, user_labels) = def_idents f_def in
     82    (StringTools.Set.add id names, cost_labels, user_labels) in
    9983  let f idents def = triple_union idents (fun_idents def) in
    10084  List.fold_left f empty_triple p.Clight.prog_funct
    10185
    102 let var_names p =
    103   let (var_names, _, _) = prog_idents p in var_names
     86let names p =
     87  let (names, _, _) = prog_idents p in names
    10488let cost_labels p =
    10589  let (_, cost_labels, _) = prog_idents p in cost_labels
     
    11498  Label.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) user_labels all
    11599
     100let all_idents p =
     101  let (names, cost_labels, user_labels) = prog_idents p in
     102  let to_string_set fold set =
     103    fold (fun lbl idents -> StringTools.Set.add lbl idents) set
     104      StringTools.Set.empty in
     105  let cost_labels = to_string_set CostLabel.Set.fold cost_labels in
     106  let user_labels = to_string_set Label.Set.fold user_labels in
     107  StringTools.Set.union names (StringTools.Set.union cost_labels user_labels)
     108
     109let fresh_ident base p =
     110  StringTools.Gen.fresh_prefix (all_idents p) base
     111
     112let fresh_universe base p =
     113  let universe = fresh_ident base p in
     114  StringTools.Gen.new_universe universe
     115
     116let make_fresh base p =
     117  let universe = fresh_universe base p in
     118  (fun () -> StringTools.Gen.fresh universe)
     119
    116120
    117121(* Instrumentation *)
    118122
    119 let int_typ = Clight.Tint (Clight.I32, Clight.Signed)
     123let int_typ = Clight.Tint (Clight.I32, AST.Signed)
    120124
    121125let const_int i = Clight.Expr (Clight.Econst_int i, int_typ)
     
    311315
    312316  (* Create a fresh 'cost' variable. *)
    313   let var_names = var_names p in
    314   let cost_id = StringTools.Gen.fresh_prefix var_names cost_id_prefix in
     317  let names = names p in
     318  let cost_id = StringTools.Gen.fresh_prefix names cost_id_prefix in
    315319  let cost_decl = cost_decl cost_id in
    316320
    317321  (* Define an increment function for the cost variable. *)
    318322  let cost_incr =
    319     StringTools.Gen.fresh_prefix (StringTools.Set.add cost_id var_names)
     323    StringTools.Gen.fresh_prefix (StringTools.Set.add cost_id names)
    320324      cost_incr_prefix in
    321325  let cost_incr_def = cost_incr_def cost_id cost_incr in
  • Deliverables/D2.2/8051/src/clight/clightAnnotator.mli

    r640 r818  
    1414val user_labels : Clight.program -> Label.Set.t
    1515val all_labels  : Clight.program -> StringTools.Set.t
     16val all_idents  : Clight.program -> StringTools.Set.t
     17
     18val fresh_ident : string (* base *) -> Clight.program -> string
     19
     20val fresh_universe :
     21  string (* prefix *) -> Clight.program -> StringTools.Gen.universe
     22
     23val make_fresh :
     24  string (* prefix *) -> Clight.program -> (unit -> string)
  • Deliverables/D2.2/8051/src/clight/clightCasts.ml

    r740 r818  
    66    be polymorphic, but working only on homogene types. *)
    77
     8
     9let error_prefix = "Clight casts simplification"
     10let error = Error.global_error error_prefix
     11let error_float () = error "float not supported."
     12
     13
     14(* Int sizes *)
     15
     16let int_of_intsize = function
     17  | Clight.I8 -> 8
     18  | Clight.I16 -> 16
     19  | Clight.I32 -> 32
     20
     21let intsize_of_int = function
     22  | i when i <= 8 -> Clight.I8
     23  | i when i <= 16 -> Clight.I16
     24  | _ -> Clight.I32
     25
     26let cmp_intsize cmp size1 size2 =
     27  cmp (int_of_intsize size1) (int_of_intsize size2)
     28
     29let max_intsize size1 size2 =
     30  if (int_of_intsize size1) < (int_of_intsize size2) then size2 else size1
     31
     32let intsize_union size1 size2 =
     33  intsize_of_int ((int_of_intsize size1) + (int_of_intsize size2))
     34
     35let pow2 = MiscPottier.pow 2
     36
     37let belongs_to_int_type size sign i = match size, sign with
     38  | Clight.I8, AST.Unsigned -> 0 <= i && i <= (pow2 8) - 1
     39  | Clight.I8, AST.Signed -> -(pow2 7) <= i && i <= (pow2 7) - 1
     40  | Clight.I16, AST.Unsigned -> 0 <= i && i <= (pow2 16) - 1
     41  | Clight.I16, AST.Signed -> -(pow2 15) <= i && i <= (pow2 15) - 1
     42  | Clight.I32, AST.Unsigned -> 0 <= i
     43  | Clight.I32, AST.Signed ->
     44    let pow2_30 = pow2 30 in
     45    (-(pow2_30 + pow2_30)) <= i &&
     46    i <= ((pow2_30 - 1) + pow2_30) (* = 2^31 - 1 *)
     47
     48let smallest_int_type i =
     49  let (size, sign) = match i with
     50  | _ when belongs_to_int_type Clight.I8 AST.Signed i ->
     51    (Clight.I8, AST.Signed)
     52  | _ when belongs_to_int_type Clight.I8 AST.Unsigned i ->
     53    (Clight.I8, AST.Unsigned)
     54  | _ when belongs_to_int_type Clight.I16 AST.Signed i ->
     55    (Clight.I16, AST.Signed)
     56  | _ when belongs_to_int_type Clight.I16 AST.Unsigned i ->
     57    (Clight.I16, AST.Unsigned)
     58  | _ when belongs_to_int_type Clight.I32 AST.Unsigned i ->
     59    (Clight.I32, AST.Unsigned)
     60  | _ ->
     61    (Clight.I32, AST.Signed) in
     62  Clight.Tint (size, sign)
     63
     64
     65let type_of_expr (Clight.Expr (_, t)) = t
     66
     67let int_type_union t1 t2 =
     68  let (size, sign) = match t1, t2 with
     69    | Clight.Tint (size1, sign1), Clight.Tint (size2, sign2)
     70      when sign1 = sign2 -> (max_intsize size1 size2, sign1)
     71    | Clight.Tint (size1, sign1), Clight.Tint (size2, sign2) ->
     72      (intsize_union size1 size2, AST.Signed)
     73    | _ -> assert false (* only use on int types *)
     74  in
     75  Clight.Tint (size, sign)
     76
     77let cast_if_needed t (Clight.Expr (ed, t') as e) = match t, ed with
     78  | _ when t = t' -> e
     79  | Clight.Tint (size, sign), Clight.Econst_int i
     80    when belongs_to_int_type size sign i ->
     81    Clight.Expr (Clight.Econst_int i, t)
     82  | _ -> Clight.Expr (Clight.Ecast (t, e), t)
     83
     84let rec simplify_binop t binop
     85    (Clight.Expr (ed1, t1) as e1)
     86    (Clight.Expr (ed2, t2) as e2) =
     87  let e1' = simplify_expr e1 in
     88  let e2' = simplify_expr e2 in
     89  let make_int i t = Clight.Expr (Clight.Econst_int i, t) in
     90
     91  let (e1', e2', t') = match t1, t2, ed1, ed2 with
     92
     93    | Clight.Tint _, Clight.Tint _,
     94      Clight.Econst_int i1, Clight.Econst_int i2 ->
     95      let t1' = smallest_int_type i1 in
     96      let t2' = smallest_int_type i2 in
     97      let t' = int_type_union t1' t2' in
     98      (make_int i1 t', make_int i2 t', t')
     99
     100    | Clight.Tint _, Clight.Tint _, _, Clight.Econst_int i2 ->
     101      let t' = type_of_expr e1' in
     102      let e2' = make_int i2 t' in
     103      (e1', e2', t')
     104
     105    | Clight.Tint _, Clight.Tint _, Clight.Econst_int i1, _ ->
     106      let t' = type_of_expr e2' in
     107      let e1' = make_int i1 t' in
     108      (e1', e2', t')
     109
     110    | Clight.Tint _, Clight.Tint _, _, _ ->
     111      let t' = int_type_union (type_of_expr e1') (type_of_expr e2') in
     112      (cast_if_needed t' e1', cast_if_needed t' e2', t')
     113
     114    | _ -> (e1', e2', t)
     115
     116  in
     117
     118  Clight.Expr (Clight.Ebinop (binop, e1', e2'), t')
     119
     120and simplify_bool_op f_bool t e1 e2 =
     121  let (e1', e2', t') = simplify_and_same_type t e1 e2 in
     122  Clight.Expr (f_bool e1' e2', t')
     123
     124and simplify_and_same_type t e1 e2 =
     125  let e1' = simplify_expr e1 in
     126  let e2' = simplify_expr e2 in
     127  if type_of_expr e1' = type_of_expr e2' then (e1', e2', type_of_expr e1')
     128  else (cast_if_needed t e1', cast_if_needed t e2', t)
     129
     130and simplify_expr (Clight.Expr (ed, t) as e) = match ed with
     131
     132  | Clight.Econst_int i ->
     133    let t' = smallest_int_type i in
     134    Clight.Expr (ed, t')
     135
     136  | Clight.Evar _ -> e
     137
     138  | Clight.Esizeof _ -> Clight.Expr (ed, Clight.Tint (Clight.I8, AST.Unsigned))
     139
     140  | Clight.Econst_float _ -> error_float ()
     141
     142  | Clight.Ederef e ->
     143    let e' = simplify_expr e in
     144    Clight.Expr (Clight.Ederef e', t)
     145
     146  | Clight.Eaddrof e ->
     147    let e' = simplify_expr e in
     148    Clight.Expr (Clight.Eaddrof e', t)
     149
     150  | Clight.Eunop (unop, e) ->
     151    let e' = simplify_expr e in
     152    Clight.Expr (Clight.Eunop (unop, e'), type_of_expr e')
     153
     154  | Clight.Ebinop (binop, e1, e2) ->
     155    simplify_binop t binop e1 e2
     156
     157  | Clight.Ecast (Clight.Tint (Clight.I32, AST.Signed), e) -> simplify_expr e
     158
     159  | Clight.Ecast (t', e) ->
     160    Clight.Expr (Clight.Ecast (t', simplify_expr e), t')
     161
     162  | Clight.Econdition (e1, e2, e3) ->
     163    let e1' = simplify_expr e1 in
     164    let (e2', e3', t') = simplify_and_same_type t e2 e3 in
     165    Clight.Expr (Clight.Econdition (e1', e2', e3'), t')
     166
     167  | Clight.Eandbool (e1, e2) ->
     168    simplify_bool_op (fun e1' e2' -> Clight.Eandbool (e1', e2')) t e1 e2
     169
     170  | Clight.Eorbool (e1, e2) ->
     171    simplify_bool_op (fun e1' e2' -> Clight.Eorbool (e1', e2')) t e1 e2
     172
     173  | Clight.Efield (e, field) ->
     174    Clight.Expr (Clight.Efield (simplify_expr e, field), t)
     175
     176  | Clight.Ecost (lbl, e) ->
     177    Clight.Expr (Clight.Ecost (lbl, simplify_expr e), t)
     178
     179  | Clight.Ecall (id, e1, e2) ->
     180    assert false (* should be impossible *)
     181
     182
    8183let f_ctype ctype _ = ctype
    9184
    10 (*
    11 let f_expr = ClightFold.expr_fill_subs
    12 
    13 let f_expr_descr e sub_ctypes_res sub_exprs_res =
    14   match e, sub_exprs_res with
    15     | Clight.Ecast (Clight.Tint (Clight.I8, signedness1), _),
    16       Clight.Expr
    17         (Clight.Eunop
    18            (unop,
    19             Clight.Expr
    20               (Clight.Ecast
    21                  (Clight.Tint (Clight.I32, _),
    22                   (Clight.Expr (_, Clight.Tint (Clight.I8, signedness2)) as e)),
    23                _)),
    24          _) :: _ when signedness1 = signedness2 ->
    25       Clight.Eunop (unop, e)
    26     | Clight.Ecast (Clight.Tint (Clight.I8, signedness1), _),
    27       Clight.Expr
    28         (Clight.Ebinop
    29            (binop,
    30             Clight.Expr
    31               (Clight.Ecast
    32                  (Clight.Tint (Clight.I32, _),
    33                   (Clight.Expr (_,
    34                                 Clight.Tint (Clight.I8, signedness2)) as e1)),
    35                _),
    36             Clight.Expr
    37               (Clight.Ecast
    38                  (Clight.Tint (Clight.I32, _),
    39                   (Clight.Expr (_,
    40                                 Clight.Tint (Clight.I8, signedness3)) as e2)),
    41                _)),
    42          _) :: _ when signedness1 = signedness2 && signedness2 = signedness3 ->
    43       Clight.Ebinop (binop, e1, e2)
    44     | Clight.Ecast (Clight.Tint (Clight.I8, signedness1), _),
    45       Clight.Expr
    46         (Clight.Ebinop
    47            (binop,
    48             Clight.Expr
    49               (Clight.Ecast
    50                  (Clight.Tint (Clight.I32, _),
    51                   (Clight.Expr (_,
    52                                 Clight.Tint (Clight.I8, signedness2)) as e1)),
    53                _),
    54             Clight.Expr (Clight.Econst_int i, _)),
    55          _) :: _ when signedness1 = signedness2 ->
    56       Clight.Ebinop (binop, e1,
    57                      Clight.Expr (Clight.Econst_int i,
    58                                   Clight.Tint (Clight.I8, signedness1)))
    59     | Clight.Ecast (Clight.Tint (Clight.I8, signedness1), _),
    60       Clight.Expr
    61         (Clight.Ebinop
    62            (binop,
    63             Clight.Expr (Clight.Econst_int i, _),
    64             Clight.Expr
    65               (Clight.Ecast
    66                  (Clight.Tint (Clight.I32, _),
    67                   (Clight.Expr (_,
    68                                 Clight.Tint (Clight.I8, signedness2)) as e1)),
    69                _)),sub_ctypes_res sub_exprs_res
    70          _) :: _ when signedness1 = signedness2 ->
    71       Clight.Ebinop (binop,
    72                      Clight.Expr (Clight.Econst_int i,
    73                                   Clight.Tint (Clight.I8, signedness1)),
    74                      e1)
    75     | _ -> ClightFold.expr_descr_fill_subs e sub_ctypes_res sub_exprs_res
    76 *)
    77 
    78 let simplify_exp ctype_opt e = e (* TODO *)
    79 
    80185let f_expr e _ _ = e
    81186
     
    83188
    84189let f_statement stmt _ sub_stmts_res =
    85   let sub_exprs = match stmt with
    86     | _ -> assert false in
     190  let f_expr b e =
     191    let e' = simplify_expr e in
     192    if b then cast_if_needed (type_of_expr e) e'
     193    else e' in
     194  let f_exprs b = List.map (f_expr b) in
     195  let f_sub_exprs = match stmt with
     196    | Clight.Sassign _ | Clight.Scall _ | Clight.Sreturn _ -> f_exprs true
     197    | _ -> f_exprs false in
     198  let sub_exprs = f_sub_exprs (ClightFold.statement_sub_exprs stmt) in
    87199  ClightFold.statement_fill_subs stmt sub_exprs sub_stmts_res
    88200
     
    97209  (id, fundef')
    98210
    99 let simplify p = p
    100 (* (* TODO: below *)
     211let simplify p =
    101212  { p with Clight.prog_funct = List.map simplify_funct p.Clight.prog_funct }
    102 *)
  • Deliverables/D2.2/8051/src/clight/clightFold.ml

    r624 r818  
    7575  | _ -> assert false (* wrong arguments, do not use on these values *)
    7676
     77let expr_fill_exprs (Clight.Expr (ed, t)) exprs =
     78  let (sub_ctypes, _) = expr_descr_subs ed in
     79  let ed = expr_descr_fill_subs ed sub_ctypes exprs in
     80  Clight.Expr (ed, t)
     81
    7782let rec expr f_ctype f_expr f_expr_descr e =
    7883  let (sub_ctypes, sub_expr_descrs) = expr_subs e in
     
    8893  let sub_ctypes_res = List.map (ctype f_ctype) sub_ctypes in
    8994  f_expr_descr e sub_ctypes_res sub_exprs_res
     95
     96
     97let expr_subs2 e =
     98  let (_, expr_descrs) = expr_subs e in
     99  let l = List.map expr_descr_subs expr_descrs in
     100  List.flatten (List.map snd l)
     101
     102let rec expr2 f e = f e (List.map (expr2 f) (expr_subs2 e))
    90103
    91104
     
    108121  | Clight.Sswitch (e, lbl_stmts) -> ([e], labeled_statements_subs lbl_stmts)
    109122  | Clight.Slabel (_, stmt) | Clight.Scost (_, stmt) -> ([], [stmt])
     123
     124let statement_sub_exprs stmt = fst (statement_subs stmt)
    110125
    111126let rec labeled_statements_fill_subs lbl_stmts sub_statements =
     
    149164    List.map (statement f_ctype f_expr f_expr_descr f_statement) sub_stmts in
    150165  f_statement stmt sub_exprs_res sub_stmts_res
     166
     167let rec statement2 f_expr f_statement stmt =
     168  let (sub_exprs, sub_stmts) = statement_subs stmt in
     169  let sub_exprs_res = List.map (expr2 f_expr) sub_exprs in
     170  let sub_stmts_res = List.map (statement2 f_expr f_statement) sub_stmts in
     171  f_statement stmt sub_exprs_res sub_stmts_res
  • Deliverables/D2.2/8051/src/clight/clightFold.mli

    r740 r818  
    1111  Clight.expr
    1212
     13val expr_fill_exprs :
     14  Clight.expr -> Clight.expr list -> Clight.expr
     15
    1316val expr :
    1417  (Clight.ctype -> 'a list -> 'a) ->
     
    1720  Clight.expr ->
    1821  'c
     22
     23val expr2 :
     24  (Clight.expr -> 'a list -> 'a) -> Clight.expr -> 'a
     25
     26val expr_descr_subs :
     27  Clight.expr_descr -> Clight.ctype list * Clight.expr list
    1928
    2029val expr_descr_fill_subs :
     
    2938  'b
    3039
     40val statement_subs :
     41  Clight.statement ->
     42  (Clight.expr list * Clight.statement list)
     43
     44val statement_sub_exprs : Clight.statement -> Clight.expr list
     45
    3146val statement_fill_subs :
    3247  Clight.statement -> Clight.expr list -> Clight.statement list ->
     
    4055  Clight.statement ->
    4156  'd
     57
     58val statement2 :
     59  (Clight.expr -> 'a list -> 'a) ->
     60  (Clight.statement -> 'a list -> 'b list -> 'b) ->
     61  Clight.statement ->
     62  'b
  • Deliverables/D2.2/8051/src/clight/clightFromC.ml

    r486 r818  
    110110
    111111let typeStringLiteral s =
    112   Tarray(Tint(I8, Unsigned), String.length s + 1)
     112  Tarray(Tint(I8, AST.Unsigned), String.length s + 1)
    113113
    114114let global_for_string s id =
     
    170170
    171171let convertIkind = function
    172   | C.IBool -> unsupported "'_Bool' type"; (Unsigned, I8)
    173   | C.IChar -> (Unsigned, I8)
    174   | C.ISChar -> (Signed, I8)
    175   | C.IUChar -> (Unsigned, I8)
    176   | C.IInt -> (Signed, I32)
    177   | C.IUInt -> (Unsigned, I32)
    178   | C.IShort -> (Signed, I16)
    179   | C.IUShort -> (Unsigned, I16)
    180   | C.ILong -> (Signed, I32)
    181   | C.IULong -> (Unsigned, I32)
     172  | C.IBool -> unsupported "'_Bool' type"; (AST.Unsigned, I8)
     173  | C.IChar -> (AST.Unsigned, I8)
     174  | C.ISChar -> (AST.Signed, I8)
     175  | C.IUChar -> (AST.Unsigned, I8)
     176  | C.IInt -> (AST.Signed, I32)
     177  | C.IUInt -> (AST.Unsigned, I32)
     178  | C.IShort -> (AST.Signed, I16)
     179  | C.IUShort -> (AST.Unsigned, I16)
     180  | C.ILong -> (AST.Signed, I32)
     181  | C.IULong -> (AST.Unsigned, I32)
    182182  | C.ILongLong ->
    183183      if not !ClightFlags.option_flonglong then unsupported "'long long' type";
    184       (Signed, I32)
     184      (AST.Signed, I32)
    185185  | C.IULongLong ->
    186186      if not !ClightFlags.option_flonglong then unsupported "'unsigned long long' type";
    187       (Unsigned, I32)
     187      (AST.Unsigned, I32)
    188188
    189189let convertFkind = function
     
    268268(** Expressions *)
    269269
    270 let ezero = Expr(Econst_int(0), Tint(I32, Signed))
     270let ezero = Expr(Econst_int(0), Tint(I32, AST.Signed))
    271271
    272272let rec convertExpr env e =
     
    393393let volatile_fun_suffix_type ty =
    394394  match ty with
    395   | Tint(I8, Unsigned) -> ("int8unsigned", ty)
    396   | Tint(I8, Signed) -> ("int8signed", ty)
    397   | Tint(I16, Unsigned) -> ("int16unsigned", ty)
    398   | Tint(I16, Signed) -> ("int16signed", ty)
    399   | Tint(I32, _) -> ("int32", Tint(I32, Signed))
     395  | Tint(I8, AST.Unsigned) -> ("int8unsigned", ty)
     396  | Tint(I8, AST.Signed) -> ("int8signed", ty)
     397  | Tint(I16, AST.Unsigned) -> ("int16unsigned", ty)
     398  | Tint(I16, AST.Signed) -> ("int16signed", ty)
     399  | Tint(I32, _) -> ("int32", Tint(I32, AST.Signed))
    400400  | Tfloat F32 -> ("float32", ty)
    401401  | Tfloat F64 -> ("float64", ty)
  • Deliverables/D2.2/8051/src/clight/clightInterpret.ml

    r740 r818  
    210210(* ctype functions *)
    211211
    212 let rec sizeof = function
    213   | Tint (I8, _)  -> 1
    214   | Tint (I16, _) -> 2
    215   | Tint (I32, _) -> 4
    216   | Tfloat _ -> error_float ()
    217   | Tcomp_ptr _ -> Mem.ptr_size
    218   | Tpointer _ -> Mem.ptr_size
    219   | Tarray (ty, n) -> n * (sizeof ty)
    220   | Tstruct (_, fields) ->
    221     let sizes = List.map sizeof (List.map snd fields) in
    222     snd (Mem.align 0 sizes)
    223   | Tunion (_, fields) ->
    224     MiscPottier.max_list (List.map sizeof (List.map snd fields))
    225   | _ -> assert false (* do not use on these arguments *)
     212let sizeof ctype = Mem.concrete_size (ClightToCminor.sizeof_ctype ctype)
    226213
    227214let size_of_ctype = function
     
    279266(* Interpret *)
    280267
    281 let int_of_intsize = function
    282   | I8 -> 8
    283   | I16 -> 16
    284   | I32 -> 32
    285 
    286 let choose_cast signedness n m v =
    287   let f = match signedness with
     268let byte_of_intsize = function
     269  | I8 -> 1
     270  | I16 -> 2
     271  | I32 -> 4
     272
     273let choose_cast sign n m v =
     274  let f = match sign with
    288275    | Signed -> Value.sign_ext
    289276    | Unsigned -> Value.zero_ext in
     
    292279let eval_cast = function
    293280  (* Cast Integer *)
    294   | (v,Tint(isize,signedness),Tint(isize',_)) ->
    295     choose_cast signedness (int_of_intsize isize) (int_of_intsize isize') v
     281  | (v,Tint(isize,sign),Tint(isize',_)) ->
     282    choose_cast sign (byte_of_intsize isize) (byte_of_intsize isize') v
    296283  | (v,_,_) -> v
    297284
    298 let eval_unop = function 
    299   | Onotbool -> Value.notbool
    300   | Onotint -> Value.notint
    301   | Oneg -> Value.negint
     285let to_int32 (v, t) = eval_cast (v, t, Tint (I32, Signed))
     286
     287let eval_unop ret_ctype ((_, t) as e) op =
     288  let v = to_int32 e in
     289  let v = match op with
     290    | Onotbool -> Value.notbool v
     291    | Onotint -> Value.notint v
     292    | Oneg -> Value.negint v in
     293  eval_cast (v, t, ret_ctype)
    302294
    303295let eval_add (v1,t1) (v2,t2) = match t1, t2 with
     
    316308  | _ -> Value.sub v1 v2
    317309
    318 let choose_signedness op_signed op_unsigned v1 v2 t =
     310let choose_sign op_signed op_unsigned v1 v2 t =
    319311  let op = match t with
    320312    | Tint (_, Signed) -> op_signed
     
    323315  op v1 v2
    324316
    325 let eval_binop ret_ctype ((v1,t1) as e1) ((v2,t2) as e2) op =
     317let eval_binop ret_ctype ((_, t1) as e1) ((_, t2) as e2) op =
     318  let v1 = to_int32 e1 in
     319  let v2 = to_int32 e2 in
     320  let e1 = (v1, t1) in
     321  let e2 = (v2, t2) in
    326322  let v = match op with
    327323    | Oadd -> eval_add e1 e2
    328324    | Osub -> eval_sub e1 e2
    329325    | Omul -> Value.mul v1 v2
    330     | Odiv -> choose_signedness Value.div Value.divu v1 v2 t1
    331     | Omod -> choose_signedness Value.modulo Value.modulou v1 v2 t1
     326    | Odiv -> choose_sign Value.div Value.divu v1 v2 t1
     327    | Omod -> choose_sign Value.modulo Value.modulou v1 v2 t1
    332328    | Oand -> Value.and_op v1 v2
    333329    | Oor -> Value.or_op v1 v2
     
    335331    | Oshl-> Value.shl v1 v2
    336332    | Oshr-> Value.shr v1 v2
    337     | Oeq -> choose_signedness Value.cmp_eq Value.cmp_eq_u v1 v2 t1
    338     | One -> choose_signedness Value.cmp_ne Value.cmp_ne_u v1 v2 t1
    339     | Olt -> choose_signedness Value.cmp_lt Value.cmp_lt_u v1 v2 t1
    340     | Ole -> choose_signedness Value.cmp_le Value.cmp_le_u v1 v2 t1
    341     | Ogt -> choose_signedness Value.cmp_gt Value.cmp_gt_u v1 v2 t1
    342     | Oge -> choose_signedness Value.cmp_ge Value.cmp_ge_u v1 v2 t1 in
     333    | Oeq -> choose_sign Value.cmp_eq Value.cmp_eq_u v1 v2 t1
     334    | One -> choose_sign Value.cmp_ne Value.cmp_ne_u v1 v2 t1
     335    | Olt -> choose_sign Value.cmp_lt Value.cmp_lt_u v1 v2 t1
     336    | Ole -> choose_sign Value.cmp_le Value.cmp_le_u v1 v2 t1
     337    | Ogt -> choose_sign Value.cmp_gt Value.cmp_gt_u v1 v2 t1
     338    | Oge -> choose_sign Value.cmp_ge Value.cmp_ge_u v1 v2 t1 in
    343339  eval_cast (v, t1, ret_ctype)
    344340
    345 let rec get_offset_struct v id fields =
    346   let sizes = List.map (fun (_, ty) -> sizeof ty) fields in
    347   let (offsets, _) = Mem.align 0 sizes in
    348   let rec select = function
    349     | (x, _) :: _, off :: _ when x = id -> off
    350     | _ :: fields, _ :: offsets -> select (fields, offsets)
    351     | _ -> assert false (* should be impossible *) in
    352   let off = Value.of_int (select (fields, offsets)) in
     341let rec get_offset_struct v size id fields =
     342  let offsets = fst (Mem.concrete_offsets_size size) in
     343  let fields = List.combine (List.map fst fields) offsets in
     344  let off = Value.of_int (List.assoc id fields) in
    353345  Value.add v off
    354346
    355347let get_offset v id = function
    356   | Tstruct (_, fields) -> get_offset_struct v id fields
     348  | Tstruct (_, fields) as t ->
     349    let size = ClightToCminor.sizeof_ctype t in
     350    get_offset_struct v size id fields
    357351  | Tunion _ -> v
    358352  | _ -> assert false (* do not use on these arguments *)
     
    390384      ((eval_binop tt v1 v2 op,tt),l1@l2)
    391385    | Eunop (op,exp) ->
    392       let ((v1,_),l1) = eval_expr localenv m exp in
    393       ((eval_unop op v1,tt),l1)
     386      let (e1,l1) = eval_expr localenv m exp in
     387      ((eval_unop tt e1 op,tt),l1)
    394388    | Econdition (e1,e2,e3) ->
    395389      let (v1,l1) = eval_expr localenv m e1 in
     
    554548let interpret_external k mem f args =
    555549  let (mem', v) = match InterpretExternal.t mem f args with
    556     | (mem', InterpretExternal.V v) -> (mem', v)
     550    | (mem', InterpretExternal.V vs) ->
     551      let v = if List.length vs = 0 then Value.undef else List.hd vs in
     552      (mem', v)
    557553    | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in
    558554  Returnstate (v, k, mem')
     
    583579  | Init_float32 f      -> error_float ()
    584580  | Init_float64 f      -> error_float ()
    585   | Init_space i        -> Data_reserve i
     581  | Init_space i        -> error "bad global initialization style."
    586582  | Init_addrof (x,off) -> assert false (* TODO: need the size of [x]'s cells *)
     583
     584let datas_of_init_datas = function
     585  | [Init_space _] -> None
     586  | l -> Some (List.map data_of_init_data l)
    587587
    588588let init_mem prog =
    589589  let f_var mem ((x, init_datas), ty) =
    590     Mem.add_var mem x (List.map data_of_init_data init_datas) in
     590    Mem.add_var mem x (ClightToCminor.sizeof_ctype ty)
     591      (datas_of_init_datas init_datas) in
    591592  let mem = List.fold_left f_var Mem.empty prog.prog_vars in
    592593  let f_fun_def mem (f, def) = Mem.add_fun_def mem f def in
     
    594595
    595596let compute_result v =
    596   if Value.is_int v then IntValue.Int8.cast (Value.to_int_repr v)
    597   else IntValue.Int8.zero
     597  if Value.is_int v then IntValue.Int32.cast (Value.to_int_repr v)
     598  else IntValue.Int32.zero
    598599
    599600let rec exec debug trace (state, l) =
     
    601602  let print_and_return_result res =
    602603    if debug then Printf.printf "Result = %s\n%!"
    603       (IntValue.Int8.to_string res) ;
     604      (IntValue.Int32.to_string res) ;
    604605    (res, cost_labels) in
    605606  if debug then print_state state ;
     
    608609      print_and_return_result (compute_result v)
    609610    | State(_,Sskip,Kstop,_,_) -> (* Implicit return in main *)
    610       print_and_return_result IntValue.Int8.zero
     611      print_and_return_result IntValue.Int32.zero
    611612    | state -> exec debug cost_labels (step state)
    612613
    613614let interpret debug prog =
    614   if debug then Printf.printf "*** Clight ***\n\n%!" ;
     615  Printf.printf "*** Clight interpret ***\n%!" ;
    615616  match prog.prog_main with
    616     | None -> (IntValue.Int8.zero, [])
     617    | None -> (IntValue.Int32.zero, [])
    617618    | Some main ->
    618619      let mem = init_mem prog in
  • Deliverables/D2.2/8051/src/clight/clightLabelling.ml

    r796 r818  
    1717
    1818
    19 let int_type = Tint (I32, Signed)
     19let int_type = Tint (I32, AST.Signed)
    2020let const_int i = Expr (Econst_int i, int_type)
    2121
     
    105105        (Swhile (add_cost_labels_e cost_universe e, s'))
    106106  | Sdowhile (e,s) ->
    107       let s' = add_cost_labels_st cost_universe s in
    108       let s' = add_starting_cost_label cost_universe s' in
     107      let s1 = add_cost_labels_st cost_universe s in
     108      let s2 = add_cost_labels_st cost_universe s in
     109      let s2' = add_starting_cost_label cost_universe s2 in
    109110      add_ending_cost_label cost_universe
    110         (Sdowhile (add_cost_labels_e cost_universe e, s'))
     111        (Ssequence (s1, Swhile (add_cost_labels_e cost_universe e, s2')))
    111112  | Sfor (s1,e,s2,s3) ->
    112113      let s1' = add_cost_labels_st cost_universe s1 in
  • Deliverables/D2.2/8051/src/clight/clightParser.ml

    r740 r818  
    4242        | None -> failwith "Error during C to Clight pass."
    4343        | Some(pp) -> pp
    44       ) 
     44      )
  • Deliverables/D2.2/8051/src/clight/clightPrinter.ml

    r486 r818  
    541541  flush_str_formatter ()
    542542
     543let print_ctype_prot = name_type
     544
     545let print_ctype_def = function
     546  | Tstruct (name, fld) | Tunion (name, fld) ->
     547    let f_fld s (id, t) = s ^ "  " ^ (print_ctype_prot t) ^ " " ^ id ^ ";\n" in
     548    let s_fld = List.fold_left f_fld "" in
     549    name ^ " {\n" ^ (s_fld fld) ^ "};\n"
     550  | _ -> "" (* no definition associated to the other types *)
  • Deliverables/D2.2/8051/src/clight/clightPrinter.mli

    r486 r818  
    44val print_program: Clight.program -> string
    55
    6 val print_expression : Clight.expr -> string
     6val print_expression: Clight.expr -> string
    77
    88val string_of_ctype: Clight.ctype -> string
    99
    1010val print_statement: Clight.statement -> string
     11
     12val print_ctype_prot: Clight.ctype -> string
     13
     14val print_ctype_def: Clight.ctype -> string
  • Deliverables/D2.2/8051/src/clight/clightToCminor.ml

    r740 r818  
    1 open AST
    2 open Cminor
    3 open Clight
    4 
    5 
    6 let error_prefix = "Cminor to RTLabs"
     1
     2
     3let error_prefix = "Clight to Cminor"
    74let error = Error.global_error error_prefix
    85let error_float () = error "float not supported."
    96
    107
    11 (*For internal use*)
    12 type var_type =
     8(* General helpers *)
     9
     10let clight_type_of (Clight.Expr (_, t)) = t
     11
     12let cminor_type_of (Cminor.Expr (_, t)) = t
     13
     14
     15(* Translate types *)
     16
     17let byte_size_of_intsize = function
     18  | Clight.I8 -> 1
     19  | Clight.I16 -> 2
     20  | Clight.I32 -> 4
     21
     22let sig_type_of_ctype = function
     23  | Clight.Tvoid -> assert false (* do not use on this argument *)
     24  | Clight.Tint (intsize, sign) ->
     25    AST.Sig_int (byte_size_of_intsize intsize, sign)
     26  | Clight.Tfloat _ -> error_float ()
     27  | Clight.Tfunction _ | Clight.Tstruct _ | Clight.Tunion _
     28  | Clight.Tpointer _ | Clight.Tarray _ | Clight.Tcomp_ptr _ -> AST.Sig_ptr
     29
     30let translate_args_types = List.map sig_type_of_ctype
     31
     32let type_return_of_ctype = function
     33  | Clight.Tvoid -> AST.Type_void
     34  | t -> AST.Type_ret (sig_type_of_ctype t)
     35
     36let quantity_of_sig_type = function
     37  | AST.Sig_int (size, _) -> AST.QInt size
     38  | AST.Sig_float _ -> error_float ()
     39  | AST.Sig_offset -> AST.QOffset
     40  | AST.Sig_ptr -> AST.QPtr
     41
     42let quantity_of_ctype t = quantity_of_sig_type (sig_type_of_ctype t)
     43
     44let rec sizeof_ctype = function
     45  | Clight.Tvoid | Clight.Tfunction _ -> AST.SQ (AST.QInt 1)
     46  | Clight.Tfloat _ -> error_float ()
     47  | Clight.Tint (size, _) -> AST.SQ (AST.QInt (byte_size_of_intsize size))
     48  | Clight.Tpointer _
     49  | Clight.Tcomp_ptr _ -> AST.SQ AST.QPtr
     50  | Clight.Tarray (t, n) -> AST.SArray (n, sizeof_ctype t)
     51  | Clight.Tstruct (_, fields) ->
     52    AST.SProd (List.map sizeof_ctype (List.map snd fields))
     53  | Clight.Tunion (_, fields) ->
     54    AST.SSum (List.map sizeof_ctype (List.map snd fields))
     55
     56let global_size_of_ctype = sizeof_ctype
     57
     58
     59(** Helpers on abstract sizes and offsets *)
     60
     61let max_stacksize size1 size2 = match size1, size2 with
     62  | AST.SProd l1, AST.SProd l2 when List.length l1 > List.length l2 -> size1
     63  | AST.SProd l1, AST.SProd l2 -> size2
     64  | _ -> raise (Failure "ClightToCminor.max_stacksize")
     65
     66(** Hypothesis: [offset1] is a prefix of [offset2] or vice-versa. *)
     67let max_offset offset1 offset2 =
     68  if List.length offset1 > List.length offset2 then offset1
     69  else offset2
     70
     71let next_depth = function
     72  | AST.SProd l -> List.length l
     73  | _ -> raise (Failure "ClightToCminor.next_offset")
     74
     75let add_stack offset =
     76  let e1 = Cminor.Expr (Cminor.Cst AST.Cst_stack, AST.Sig_ptr) in
     77  let e2 = Cminor.Expr (Cminor.Cst (AST.Cst_offset offset), AST.Sig_offset) in
     78  Cminor.Op2 (AST.Op_addp, e1, e2)
     79
     80let add_stacksize t = function
     81  | AST.SProd l -> AST.SProd (l @ [sizeof_ctype t])
     82  | _ -> raise (Failure "ClightToCminor.add_stacksize")
     83
     84let struct_depth field fields =
     85  let rec aux i = function
     86    | [] -> error ("unknown field " ^ field ^ ".")
     87    | (field', t) :: _ when field' = field -> i
     88    | (_, t) :: fields -> aux (i+1) fields in
     89  aux 0 fields
     90
     91let struct_offset t field fields =
     92  let size = sizeof_ctype t in
     93  let depth = struct_depth field fields in
     94  let offset = (size, depth) in
     95  let t = AST.Sig_offset in
     96  Cminor.Expr (Cminor.Cst (AST.Cst_offset offset), t)
     97
     98
     99(** Sort variables: locals, parameters, globals, in stack. *)
     100
     101type location =
     102  | Local
     103  | LocalStack of AST.abstract_offset
     104  | Param
     105  | ParamStack of AST.abstract_offset
    13106  | Global
    14   | Stack of int (*Note: this is a constraint on the size of the stack.*)
    15   | Param
    16   | Local
    17 
    18 (*Parametrisation by int and pointer size *)
    19 let int_size = Driver.CminorMemory.int_size
    20 let ptr_size = Driver.CminorMemory.ptr_size
    21 let alignment = Driver.CminorMemory.alignment
    22 
    23 let fresh_tmp variables =
    24   let rec ft i =
    25     let tmp = "tmp"^(string_of_int i) in
    26       try (match Hashtbl.find variables tmp with _ -> ft (i+1))
    27       with Not_found -> tmp
    28   in ft 0
    29 
    30 let rec ctype_to_type_return t = match t with
    31   | Tvoid       -> Type_void
    32   | Tfloat _    -> Type_ret Sig_float (*Not supported*)
    33   | Tpointer _ | Tarray (_,_) | Tstruct (_,_) | Tunion (_,_) -> Type_ret Sig_ptr
    34   | _           -> Type_ret Sig_int
    35 
    36 let rec ctype_to_sig_type t = match t with
    37   | Tfloat _    ->
    38       Sig_float (*Not supported but needed for external function from library*)
    39   | Tvoid       -> assert false
    40   | Tpointer _ | Tstruct (_,_) | Tunion (_,_) | Tarray(_,_) -> Sig_ptr
    41   | _           -> Sig_int
    42 
    43 let rec size_of_ty = function
    44   | Tvoid               -> assert false
    45   | Tfloat _            -> assert false (*Not supported*)
    46   | Tfunction (_,_)     -> assert false (*Not supported*)
    47   | Tint (I8,Signed)    -> 1
    48   | Tint (I8,Unsigned)  -> 1
    49   | Tint (I16,Signed)   -> 2
    50   | Tint (I16,Unsigned) -> 2
    51   (*FIXME MQ_int32 : signed or unsigned ? *)
    52   | Tint (I32,Signed)   -> 4
    53   | Tint (I32,Unsigned) -> 4
    54   | Tpointer _ | Tarray (_,_) | Tstruct (_,_) | Tunion (_,_)
    55   | Tcomp_ptr _         -> ptr_size
    56 
    57 let size_of_intsize = function
    58   | I8 -> 1
    59   | I16 -> 2
    60   | I32 -> 4
    61 
    62 let quantity_of_ty = function
    63   | Tvoid               -> assert false (* do not use on this argument *)
    64   | Tint (size,_)       -> Memory.QInt (size_of_intsize size)
    65   | Tpointer _ | Tarray (_,_) | Tstruct (_,_) | Tunion (_,_)
    66   | Tfunction (_,_)
    67   | Tcomp_ptr _         -> Memory.QPtr
    68   | Tfloat _            -> error_float ()
    69 
    70 let init_to_data l = List.map (
     107
     108(** Below are some helper definitions to ease the manipulation of a translation
     109    environment for variables. *)
     110
     111type var_locations = (location * Clight.ctype) StringTools.Map.t
     112
     113let empty_var_locs : var_locations = StringTools.Map.empty
     114
     115let add_var_locs : AST.ident -> (location * Clight.ctype) -> var_locations ->
     116  var_locations =
     117  StringTools.Map.add
     118
     119let mem_var_locs : AST.ident -> var_locations -> bool = StringTools.Map.mem
     120
     121let find_var_locs : AST.ident -> var_locations -> (location * Clight.ctype) =
     122  StringTools.Map.find
     123
     124let fold_var_locs : (AST.ident -> (location * Clight.ctype) -> 'a -> 'a) ->
     125  var_locations -> 'a -> 'a =
     126  StringTools.Map.fold
     127
     128
     129let is_local_or_param id var_locs = match find_var_locs id var_locs with
     130  | (Local, _) | (Param, _) -> true
     131  | _ -> false
     132
     133let get_locals var_locs =
     134  let f id (location, ctype) locals =
     135    let added = match location with
     136      | Local -> [(id, sig_type_of_ctype ctype)]
     137      | _ -> [] in
     138    locals @ added in
     139  fold_var_locs f var_locs []
     140
     141let get_stacksize var_locs =
     142  let f _ (location, _) res = match location with
     143    | LocalStack (stacksize, _) | ParamStack (stacksize, _) ->
     144      max_stacksize res stacksize
     145    | _ -> res in
     146  fold_var_locs f var_locs (AST.SProd [])
     147
     148
     149(* Variables of a function that will go in stack: variables of a complex type
     150   (array, structure or union) and variables whose address is evaluated. *)
     151
     152let is_function_ctype = function
     153  | Clight.Tfunction _ -> true
     154  | _ -> false
     155
     156let is_scalar_ctype : Clight.ctype -> bool = function
     157  | Clight.Tint _ | Clight.Tfloat _ | Clight.Tpointer _ -> true
     158  | _ -> false
     159
     160let is_complex_ctype : Clight.ctype -> bool = function
     161  | Clight.Tarray _ | Clight.Tstruct _ | Clight.Tunion _ | Clight.Tfunction _ ->
     162    true
     163  | _ -> false
     164
     165let complex_ctype_vars cfun =
     166  let f set (x, t) =
     167    if is_complex_ctype t then StringTools.Set.add x set else set in
     168  (* Because of CIL, parameters should not have a complex type, but let's add
     169     them just in case. *)
     170  List.fold_left f StringTools.Set.empty
     171    (cfun.Clight.fn_params @ cfun.Clight.fn_vars)
     172
     173let union_list = List.fold_left StringTools.Set.union StringTools.Set.empty
     174
     175let f_expr (Clight.Expr (ed, _)) sub_exprs_res =
     176  let res_ed = match ed with
     177    | Clight.Eaddrof (Clight.Expr (Clight.Evar id, _)) ->
     178      StringTools.Set.singleton id
     179    | _ -> StringTools.Set.empty in
     180  union_list (res_ed :: sub_exprs_res)
     181
     182let f_stmt _ sub_exprs_res sub_stmts_res =
     183  union_list (sub_exprs_res @ sub_stmts_res)
     184
     185let addr_vars_fun cfun = ClightFold.statement2 f_expr f_stmt cfun.Clight.fn_body
     186
     187let stack_vars cfun =
     188  StringTools.Set.union (complex_ctype_vars cfun) (addr_vars_fun cfun)
     189
     190
     191let sort_stacks stack_location vars var_locs =
     192  let stacksize = get_stacksize var_locs in
     193  let f (current_stacksize, var_locs) (id, t) =
     194    let depth = next_depth current_stacksize in
     195    let current_stacksize = add_stacksize t current_stacksize in
     196    let offset = (current_stacksize, depth) in
     197    let var_locs = add_var_locs id (stack_location offset, t) var_locs in
     198    (current_stacksize, var_locs) in
     199  snd (List.fold_left f (stacksize, var_locs) vars)
     200
     201let sort_normals normal_location vars var_locs =
     202  let f var_locs (id, ctype) =
     203    add_var_locs id (normal_location, ctype) var_locs in
     204  List.fold_left f var_locs vars
     205
     206let sort_vars normal_location stack_location_opt stack_vars vars var_locs =
     207  let f_stack (x, _) = StringTools.Set.mem x stack_vars in
     208  let (f_normal, var_locs) = match stack_location_opt with
     209    | None -> ((fun _ -> true), var_locs)
     210    | Some stack_location ->
     211      ((fun var -> not (f_stack var)),
     212       sort_stacks stack_location (List.filter f_stack vars) var_locs) in
     213  sort_normals normal_location (List.filter f_normal vars) var_locs
     214
     215let sort_locals = sort_vars Local (Some (fun offset -> LocalStack offset))
     216
     217let sort_params = sort_vars Param (Some (fun offset -> ParamStack offset))
     218
     219let sort_globals stack_vars globals var_locs =
     220  let globals = List.map (fun ((id, _), ctype) -> (id, ctype)) globals in
     221  sort_vars Global None stack_vars globals var_locs
     222
     223(* The order of insertion in the sorting environment is important: it follows
     224   the scope conventions of C. Local variables hide parameters that hide
     225   globals. *)
     226
     227let sort_variables globals cfun =
     228  let stack_vars = stack_vars cfun in
     229  let var_locs = empty_var_locs in
     230  let var_locs = sort_globals stack_vars globals var_locs in
     231  let var_locs = sort_params stack_vars cfun.Clight.fn_params var_locs in
     232  let var_locs = sort_locals stack_vars cfun.Clight.fn_vars var_locs in
     233  var_locs
     234
     235
     236(* Translate globals *)
     237
     238let init_to_data = function
     239  | [Clight.Init_space _] -> None
     240  | l -> Some (List.map (
    71241  function
    72     | Init_int8 i       -> Data_int8 i
    73     | Init_int16 i      -> Data_int16 i
    74     | Init_int32 i      -> Data_int32 i
    75     | Init_float32 _
    76     | Init_float64 _    -> assert false (*Not supported*)
    77     | Init_space n      -> Data_reserve n
    78     | Init_addrof (_,_) -> assert false (*TODO*)
    79 ) l
    80 
    81 let rec size_of_ctype t = match t with
    82   | Tvoid                       -> 0
    83   | Tint (I8,_)                 -> 1
    84   | Tint (I16,_)                -> 2
    85   | Tint (I32,_)                -> 4
    86   | Tpointer _                  -> ptr_size     
    87   | Tarray (c,s)                -> s*(size_of_ctype c)
    88   | Tstruct (_,lst)             ->
    89       List.fold_left
    90         (fun n (_,ty) -> n+(size_of_ctype ty)) 0 lst
    91   | Tunion (_,lst)              ->
    92       List.fold_left
    93         (fun n (_,ty) ->
    94            let sz = (size_of_ctype ty) in (if n>sz then n else sz)
    95         ) 0 lst
    96   | Tfloat _ | Tfunction (_,_)  -> assert false (*Not supported*)
    97   | Tcomp_ptr _                 -> ptr_size     
    98 
    99 let translate_global_vars ((id,lst),_) = (id,init_to_data lst)
    100 
    101 let translate_unop t = function
    102   | Onotbool                    -> Op_notbool
    103   | Onotint                     -> Op_notint
    104   | Oneg -> (match t with
    105                | Tint (_,_)     -> Op_negint
    106                | Tfloat _       -> assert false  (*Not supported*)
    107                | _              -> assert false  (*Type error*)
    108     )
    109 
    110 let translate_cmp t1 t2 cmp =
    111   match (t1,t2) with
    112     | (Tint(_,Signed),Tint(_,Signed))           -> Op_cmp cmp
    113     | (Tint(_,Unsigned),Tint(_,Unsigned))       -> Op_cmpu cmp
    114     | (Tpointer _,Tpointer _)                   -> Op_cmpp cmp
    115     | _                                         -> Op_cmp cmp 
    116 
    117 let translate_add e1 e2 = function
    118   | (Tint(_,_),Tint(_,_))       -> Op2 (Op_add,e1,e2)
    119   | (Tfloat _,Tfloat _)         -> assert false (*Not supported*)
    120   | (Tpointer t,Tint(_,_))      ->
    121       Op2 (Op_addp,e1, Op2 (Op_mul,e2,Cst (Cst_int (size_of_ctype t))))
    122   | (Tint(_,_),Tpointer t)      ->
    123       Op2 (Op_addp,e2,Op2 (Op_mul,e1,Cst (Cst_int (size_of_ctype t))))
    124   | (Tarray (t,_),Tint(_,_))    ->
    125       Op2 (Op_addp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
    126   | (Tint(_,_),Tarray(t,_))     ->
    127       Op2 (Op_addp,e2,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t)))))
    128   | _                           -> assert false (*Type error*)
    129 
    130 let translate_sub e1 e2 = function
    131   | (Tint(_,_),Tint(_,_))       -> Op2 (Op_sub,e1,e2)
    132   | (Tfloat _,Tfloat _)         -> assert false (*Not supported*)
    133   | (Tpointer t,Tint(_,_))      ->
    134       Op2 (Op_subp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
    135   | (Tarray (t,_),Tint(_,_))    ->
    136       Op2 (Op_subp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
    137   | _                           -> assert false (*Type error*)
    138 
    139 let translate_mul e1 e2 = function
    140   | (Tint(_,_),Tint(_,_))       -> Op2 (Op_mul,e1,e2)
    141   | (Tfloat _,Tfloat _)         -> assert false (*Not supported*)
    142   | _                           -> assert false (*Type error*)
    143 
    144 let translate_div e1 e2 = function
    145   | (Tint(_,Signed),Tint(_,Signed))     -> Op2 (Op_div,e1,e2)
    146   | (Tint(_,Unsigned),Tint(_,Unsigned)) -> Op2 (Op_divu,e1,e2)
    147   | (Tfloat _,Tfloat _)                 -> assert false (*Not supported*)
    148   | _                                   -> assert false (*Type error*)
    149 
    150 let translate_binop t1 e1 t2 e2 = function
    151   | Oadd -> translate_add e1 e2 (t1,t2)
    152   | Osub -> translate_sub e1 e2 (t1,t2)
    153   | Omul -> translate_mul e1 e2 (t1,t2)
    154   | Odiv -> translate_div e1 e2 (t1,t2)
    155   | Omod -> Op2 (Op_mod,e1,e2)
    156   | Oand -> Op2 (Op_and,e1,e2)
    157   | Oor  -> Op2 (Op_or,e1,e2)
    158   | Oxor -> Op2 (Op_xor,e1,e2)
    159   | Oshl -> Op2 (Op_shl,e1,e2)
    160   | Oshr -> Op2 (Op_shr,e1,e2)
    161   | Oeq  -> Op2 (translate_cmp t1 t2 Cmp_eq,e1,e2)
    162   | One  -> Op2 (translate_cmp t1 t2 Cmp_ne,e1,e2)
    163   | Olt  -> Op2 (translate_cmp t1 t2 Cmp_lt,e1,e2)
    164   | Ogt  -> Op2 (translate_cmp t1 t2 Cmp_gt,e1,e2)
    165   | Ole  -> Op2 (translate_cmp t1 t2 Cmp_le,e1,e2)
    166   | Oge  -> Op2 (translate_cmp t1 t2 Cmp_ge,e1,e2)
    167 
    168 let make_cast e = function
    169   | (Tint(I8,Signed),Tint(_,_))    -> Op1 (Op_cast8signed,e)
    170   | (Tint(I8,Unsigned),Tint(_,_))  -> Op1 (Op_cast8unsigned,e)
    171   | (Tint(I16,Signed),Tint(_,_))   -> Op1 (Op_cast16signed,e)
    172   | (Tint(I16,Unsigned),Tint(_,_)) -> Op1 (Op_cast16unsigned,e)
    173   | _ -> e
    174 
    175 let get_type (Expr (_,t)) = t
    176 
    177 let rec get_offset_struct e id = function
    178   | [] -> assert false (*Wrong id*)
    179   | (fi,_)::_ when fi=id -> e
    180   | (_,ty)::ll -> get_offset_struct (e+(size_of_ctype ty)) id ll
    181 
    182 let is_struct = function
    183   | Tarray(_,_) | Tstruct (_,_) | Tunion(_,_) -> true
     242    | Clight.Init_int8 i       -> AST.Data_int8 i
     243    | Clight.Init_int16 i      -> AST.Data_int16 i
     244    | Clight.Init_int32 i      -> AST.Data_int32 i
     245    | Clight.Init_float32 _
     246    | Clight.Init_float64 _    -> error_float ()
     247    | Clight.Init_space n      -> error "bad global initialization style."
     248    | Clight.Init_addrof (_,_) -> assert false (*TODO*)
     249) l)
     250
     251let translate_global ((id,lst),t) = (id,global_size_of_ctype t,init_to_data lst)
     252
     253
     254(* Translate expression *)
     255
     256let translate_unop = function
     257  | Clight.Onotbool -> AST.Op_notbool
     258  | Clight.Onotint -> AST.Op_notint
     259  | Clight.Oneg -> AST.Op_negint
     260
     261let esizeof_ctype res_type t =
     262  Cminor.Expr (Cminor.Cst (AST.Cst_sizeof (sizeof_ctype t)), res_type)
     263
     264let translate_add res_type ctype1 ctype2 e1 e2 = match ctype1, ctype2 with
     265  | Clight.Tint _, Clight.Tint _ ->
     266    Cminor.Expr (Cminor.Op2 (AST.Op_add, e1, e2), res_type)
     267  | Clight.Tfloat _, Clight.Tfloat _ -> error_float ()
     268  | Clight.Tpointer t, Clight.Tint _
     269  | Clight.Tarray (t, _), Clight.Tint _ ->
     270    let t2 = cminor_type_of e2 in
     271    let size = esizeof_ctype t2 t in
     272    let index = Cminor.Expr (Cminor.Op2 (AST.Op_mul, e2, size), t2) in
     273    Cminor.Expr (Cminor.Op2 (AST.Op_addp, e1, index), res_type)
     274  | Clight.Tint _, Clight.Tpointer t
     275  | Clight.Tint _, Clight.Tarray (t, _) ->
     276    let t1 = cminor_type_of e1 in
     277    let size = esizeof_ctype t1 t in
     278    let index = Cminor.Expr (Cminor.Op2 (AST.Op_mul, e1, size), t1) in
     279    Cminor.Expr (Cminor.Op2 (AST.Op_addp, e2, index), res_type)
     280  | _ -> error "type error."
     281
     282let translate_sub res_type ctype1 ctype2 e1 e2 = match ctype1, ctype2 with
     283  | Clight.Tint _, Clight.Tint _ ->
     284    Cminor.Expr (Cminor.Op2 (AST.Op_sub, e1, e2), res_type)
     285  | Clight.Tfloat _, Clight.Tfloat _ -> error_float ()
     286  | Clight.Tpointer t, Clight.Tint _
     287  | Clight.Tarray (t, _), Clight.Tint _ ->
     288    let t2 = cminor_type_of e2 in
     289    let size = esizeof_ctype t2 t in
     290    let index = Cminor.Expr (Cminor.Op2 (AST.Op_mul, e2, size), t2) in
     291    Cminor.Expr (Cminor.Op2 (AST.Op_subp, e1, index), res_type)
     292  | Clight.Tpointer _, Clight.Tpointer _
     293  | Clight.Tarray _, Clight.Tpointer _
     294  | Clight.Tpointer _, Clight.Tarray _
     295  | Clight.Tarray _, Clight.Tarray _ ->
     296    Cminor.Expr (Cminor.Op2 (AST.Op_subpp, e1, e2), res_type)
     297  | _ -> error "type error."
     298
     299let is_signed = function
     300  | Clight.Tint (_, AST.Signed) -> true
    184301  | _ -> false
    185302
    186 let is_ptr_to_struct = function
    187   | Tpointer t when is_struct t -> true
    188   | _ -> false 
    189 
    190 let is_function = function
    191   | Tfunction _ -> true
     303let is_pointer = function
     304  | Clight.Tpointer _ | Clight.Tarray _ -> true
    192305  | _ -> false
    193306
    194 let rec translate_expr variables expr =
    195   let Expr(d,c) = expr in match d with
    196     | Econst_int i      -> Cst (Cst_int i)
    197     | Econst_float f    -> assert false (*Not supported*)
    198     | Evar id when is_function c -> Cst (Cst_addrsymbol id)
    199     | Evar id           -> 
    200         (try (match Hashtbl.find variables id with
    201            | (Local,_)          -> Id id
    202            | (Stack o,ty) when is_struct ty     -> Cst (Cst_stackoffset o)
    203            | (Stack o,_)        ->
    204              Mem (quantity_of_ty c,Cst (Cst_stackoffset o))
    205            | (Param,_)          -> Id id
    206            | (Global,ty) when is_struct ty -> Cst (Cst_addrsymbol id)
    207            | (Global,_)         ->
    208              Mem (quantity_of_ty c,Cst (Cst_addrsymbol id))
    209         ) with Not_found -> assert false)
    210     | Ederef e when is_ptr_to_struct (get_type e) ->
    211         translate_expr variables e
    212     | Ederef e          -> Mem (quantity_of_ty c,translate_expr variables e)
    213     | Eaddrof se        ->  (
    214         match se with
    215           | Expr(Evar id,_) ->
    216              (try  (match Hashtbl.find variables id with
    217                  | (Local,_) -> assert false (*Impossible: see sort_variables*)
    218                  | (Stack o,_) -> Cst (Cst_stackoffset o)
    219                  | (Param,_) ->  Cst (Cst_addrsymbol id)
    220                  | (Global,_) -> Cst (Cst_addrsymbol id)
    221               ) with Not_found -> assert false)
    222           | Expr(Ederef ee,_)                              ->
    223               translate_expr variables ee
    224           | Expr(Efield (str,fi),_)  ->
    225               (match str with
    226                  | Expr(_,Tstruct(_,b)) ->
    227                      Op2 (Op_add
    228                           ,translate_expr variables str
    229                           ,Cst (Cst_int (get_offset_struct 0 fi b)))
    230                  | Expr(_,Tunion(_,_)) ->
    231                      translate_expr variables str
    232                  | _ -> assert false (*Type Error*)
    233               )
    234           | _ ->  assert false (*Must be a lvalue*)
    235       )
    236     | Eunop (op,e)      ->
    237         Op1 (translate_unop (get_type e) op ,translate_expr variables e)
    238     | Ebinop (op,e1,e2) ->
    239         translate_binop
    240           (get_type e1) (translate_expr variables e1)
    241           (get_type e2) (translate_expr variables e2) op
    242     | Ecast (ty,e)     -> make_cast (translate_expr variables e) (get_type e,ty)
    243     | Econdition (e1,e2,e3) ->
    244         Cond (translate_expr variables e1,
    245               translate_expr variables e2,
    246               translate_expr variables e3)
    247     | Eandbool (e1,e2) ->
    248         Cond (
    249           translate_expr variables e1,
    250           Cond(translate_expr variables e2,Cst (Cst_int 1),Cst (Cst_int 0)),
    251           Cst (Cst_int 0))
    252     | Eorbool (e1,e2) ->
    253         Cond (
    254           translate_expr variables e1,
    255           Cst (Cst_int 1),
    256           Cond(translate_expr variables e2, Cst (Cst_int 1),Cst (Cst_int 0)) )
    257     | Esizeof cc        -> Cst (Cst_int (size_of_ctype cc))
    258     | Efield (e,id)     ->
    259         (match get_type e with
    260            | Tstruct(_,lst) ->
    261                (try
    262                   Mem (quantity_of_ty (List.assoc id lst)
    263                        ,Op2(Op_add
    264                             ,translate_expr variables e
    265                             , Cst (Cst_int (get_offset_struct 0 id lst))
    266                        )
    267                   )
    268                 with Not_found -> assert false (*field does not exists*)
    269                )
    270            | Tunion(_,lst) ->
    271                (try
    272                   Mem (quantity_of_ty (List.assoc id lst), translate_expr variables e)
    273                 with Not_found -> assert false (*field does not exists*)
    274                )
    275            | _ -> assert false (*Type error*)
    276         )
    277     | Ecost (lbl,e)     -> Exp_cost (lbl,translate_expr variables e)
    278     | Ecall _           -> assert false (* Only for annotations *)
    279 
    280 let translate_assign variables e = function
    281   | Expr (Evar v,t) ->
    282       (try (match Hashtbl.find variables v with
    283          | (Local,_)            -> St_assign (v,translate_expr variables e)
    284          | (Stack o,_)          -> St_store (quantity_of_ty t
    285                                              ,Cst (Cst_stackoffset o)
    286                                              ,translate_expr variables e)
    287          | (Param,_)            -> St_assign (v,translate_expr variables e)
    288          | (Global,_)           -> St_store (quantity_of_ty t
    289                                              ,Cst (Cst_addrsymbol v)
    290                                              ,translate_expr variables e)
    291       ) with Not_found -> assert false)
    292   | Expr (Ederef ee,t)          -> St_store (quantity_of_ty t
    293                                              ,translate_expr variables ee
    294                                              ,translate_expr variables e)
    295   | Expr (Efield (ee,id),t) ->
    296       (match ee with
    297          | Expr (_,Tstruct(_,lst)) ->
    298              St_store (quantity_of_ty t
    299                        ,Op2(Op_add,translate_expr variables ee
    300                             ,Cst(Cst_int (get_offset_struct 0 id lst )))
    301                        ,translate_expr variables e)
    302          | Expr (_,Tunion(_,_)) -> St_store (quantity_of_ty t
    303                                              ,translate_expr variables ee
    304                                              ,translate_expr variables e)
    305          | _ -> assert false (*Type error*)
    306       )
    307   | _                           -> assert false (*lvalue error*)
    308 
    309 let translate_call_name variables = function
    310   | Expr (Evar id,_)    -> Cst (Cst_addrsymbol id)
    311   | _                   -> assert false (*Not supported*)
    312 
    313 let translate_call variables e1 e2 lst =
    314   let st_call f_assign f_res =
    315     St_call (f_assign
    316              ,translate_expr variables e2
    317              ,List.map (translate_expr variables) lst
    318              ,{args=List.map (fun exp ->
    319                                 let Expr(_,t) = exp in ctype_to_sig_type t
    320              )lst;res=f_res}
    321         ) in
    322     match e1 with
    323       | Some (Expr (se,tt)) -> (
    324           match se with
    325             | Evar v ->
    326                 (try (match Hashtbl.find variables v with
    327                    | (Local,_) | (Param,_) ->
    328                        st_call (Some v) (Type_ret (ctype_to_sig_type tt))
    329                    | (Stack o,_) ->
    330                        let tmp = fresh_tmp variables in
    331                          St_seq (
    332                            st_call (Some tmp) (Type_ret (ctype_to_sig_type tt))
    333                            ,St_store (quantity_of_ty tt,Cst (Cst_stackoffset o),Id tmp)
    334                          )
    335                    | (Global,_) ->
    336                        let tmp = fresh_tmp variables in
    337                          St_seq (
    338                            st_call (Some tmp) (Type_ret (ctype_to_sig_type tt))
    339                            ,St_store (quantity_of_ty tt,Cst (Cst_addrsymbol v),Id tmp)
    340                          )
    341                 ) with Not_found -> assert false )
    342             | Ederef ee         -> assert false (*Not supported*)
    343             | Efield (ee,id)    -> assert false (*Not supported*)
    344             | _ -> assert false (*Should be a lvalue*)
    345         )
    346       | None -> st_call None Type_void
    347 
    348 (*TODO rewrite this buggy function*)                 
    349 let translate_switch expr (cases,default) =
    350   let sz = List.length cases in
    351   let sw = St_block (St_switch (
    352     expr, MiscPottier.mapi (fun i (n,_) -> (n,i)) cases, sz)) in
    353   let rec add_block n e = function
    354     | [] -> St_block (St_seq(e,default))
    355     | (_,st)::l ->
    356         add_block (n-1) (St_block (St_seq(e,St_seq(st,St_exit n)))) l
    357   in add_block sz sw cases
    358 
    359 let rec translate_stmt variables = function
    360   | Sskip               -> St_skip
    361   | Sassign (e1,e2)     -> translate_assign variables e2 e1
    362   | Scall (e1,e2,lst)   -> translate_call variables e1 e2 lst
    363   | Ssequence (s1,s2)   ->
    364       St_seq (translate_stmt variables s1,
    365               translate_stmt variables s2)
    366   | Sifthenelse (e,s1,s2) ->
    367       St_ifthenelse (translate_expr variables e,
    368                      translate_stmt variables s1,
    369                      translate_stmt variables s2)
    370   | Swhile (e,s)        ->
    371       St_block(St_loop(St_seq (
    372         St_ifthenelse (
    373           Op1 (Op_notbool,translate_expr variables e),
    374           St_exit 0,St_skip),
    375         St_block (translate_stmt variables s)
    376       )))
    377   | Sdowhile (e,s)      ->
    378       St_block(St_loop(St_seq (
    379         St_block (translate_stmt variables s),
    380         St_ifthenelse (
    381           Op1(Op_notbool, translate_expr variables e),
    382           St_exit 0,St_skip)
    383       )))
    384   | Sfor (s1,e,s2,s3)   ->
    385       let b = St_block (St_loop (St_seq (
    386         St_ifthenelse (
    387           Op1(Op_notbool,translate_expr variables e),
    388           St_exit 0,St_skip),
    389         St_seq (St_block (translate_stmt variables s3),
    390                 translate_stmt variables s2
    391         )))) in
    392         (match (translate_stmt variables s1) with
    393            | St_skip -> b | ss -> St_seq (ss,b))
    394   | Sbreak              -> St_exit(1)           
    395   | Scontinue           -> St_exit(0)
    396   | Sreturn (Some e)    -> St_return (Some(translate_expr variables e))
    397   | Sreturn None        -> St_return None
    398   | Sswitch (e,lbl)     ->
    399       translate_switch (translate_expr variables e) (compute_lbl variables lbl)
    400   | Slabel (lbl,st)     ->
    401       St_label(lbl,translate_stmt variables st)
    402   | Sgoto lbl           -> St_goto lbl
    403   | Scost (lbl,s)       -> St_cost(lbl,translate_stmt variables s)
    404 
    405 and compute_lbl variables = function
    406   | LSdefault s -> ([],translate_stmt variables s)
    407   | LScase (i,s,l) ->
    408       let (ll,def) = (compute_lbl variables l) in
    409         ((i,translate_stmt variables s)::ll,def)
    410 
    411 let rec get_stack_vars_expr (Expr (exp,_)) = match exp with
    412   | Econst_int _  | Evar _ | Esizeof _ -> []
    413   | Ederef e -> (get_stack_vars_expr e)
    414   | Eaddrof Expr(e,_) -> (
    415       match e with
    416         | Evar id                       -> [id]
    417         | Ederef ee | Efield (ee,_)     -> (get_stack_vars_expr ee)
    418         | _                             -> assert false (*Should be a lvalue*)
    419     )
    420   | Eunop (_,e) -> (get_stack_vars_expr e)
    421   | Ebinop (_,e1,e2) -> (get_stack_vars_expr e1)@(get_stack_vars_expr e2)
    422   | Ecast (_,e) -> (get_stack_vars_expr e)
    423   | Econdition (e1,e2,e3) ->
    424       (get_stack_vars_expr e1)@(get_stack_vars_expr e2)
    425       @(get_stack_vars_expr e3)
    426   | Eandbool (e1,e2) -> (get_stack_vars_expr e1)@(get_stack_vars_expr e2)
    427   | Eorbool (e1,e2) -> (get_stack_vars_expr e1)@(get_stack_vars_expr e2)
    428   | Ecost (_,e) -> (get_stack_vars_expr e)
    429   | Efield (e,_) -> (get_stack_vars_expr e)
    430   | Econst_float _ -> assert false (*Not supported*)
    431   | Ecall _ -> assert false (* Should not happen *)
    432 
    433 let rec get_stack_vars_stmt = function
    434   | Sskip | Sbreak | Scontinue | Sreturn None | Sgoto _ -> []
    435   | Sassign (e1,e2) ->
    436       (get_stack_vars_expr e1)@(get_stack_vars_expr e2)
    437   | Scall (None,e,lst) ->
    438       (get_stack_vars_expr e)
    439       @(List.fold_left (fun l e -> l@(get_stack_vars_expr e)) [] lst)
    440   | Scall (Some e1,e2,lst) ->
    441       (get_stack_vars_expr e1)@(get_stack_vars_expr e2)
    442       @(List.fold_left (fun l e -> l@(get_stack_vars_expr e)) [] lst)
    443   | Ssequence (s1,s2) ->
    444       (get_stack_vars_stmt s1)@(get_stack_vars_stmt s2)
    445   | Sifthenelse (e,s1,s2) ->
    446       (get_stack_vars_expr e)@(get_stack_vars_stmt s1)@(get_stack_vars_stmt s2)
    447   | Swhile (e,s) ->
    448       (get_stack_vars_expr e)@(get_stack_vars_stmt s)
    449   | Sdowhile (e,s) ->
    450       (get_stack_vars_expr e)@(get_stack_vars_stmt s)
    451   | Sfor (s1,e,s2,s3) ->
    452       (get_stack_vars_expr e)@(get_stack_vars_stmt s1)@(get_stack_vars_stmt s2)
    453       @(get_stack_vars_stmt s3)
    454   | Sreturn (Some e) ->
    455       (get_stack_vars_expr e)
    456   | Sswitch (e,ls) ->
    457       (get_stack_vars_expr e)@(get_stack_vars_ls ls)
    458   | Slabel (_,s) -> (get_stack_vars_stmt s)
    459   | Scost (_,s) -> (get_stack_vars_stmt s)
    460 and get_stack_vars_ls = function
    461   | LSdefault s -> get_stack_vars_stmt s
    462   | LScase (_,s,ls) -> (get_stack_vars_stmt s)@(get_stack_vars_ls ls)
    463 
    464 let is_struct = function
    465   | Tarray (_,_) | Tstruct (_,_) | Tunion (_,_) -> true
    466   | _ -> false
    467 
    468 let sort_variables globals f =
    469   let variables = Hashtbl.create 47 and next_offset = ref 0 in
    470     List.iter (fun (id,ty) -> Hashtbl.add variables id (Global,ty)) globals;
    471     List.iter (fun (id,ty) -> Hashtbl.add variables id (Param,ty)) f.fn_params;
    472     List.iter
    473       (fun (id,ty) ->
    474          if is_struct ty then (
    475            Hashtbl.add variables id (Stack !next_offset,ty);
    476            next_offset := !next_offset + (size_of_ctype ty)
    477          ) else Hashtbl.add variables id (Local,ty)
    478       ) f.fn_vars;
    479     List.iter
    480       (fun id -> match
    481          (try
    482             Hashtbl.find variables id
    483           with
    484               Not_found -> (
    485                  Printf.eprintf "Error: Cannot find variable %s\n" id;
    486                  assert false)
    487          ) with
    488          | (Local,ty) ->
    489              Hashtbl.add variables id (Stack !next_offset,ty);
    490              next_offset:=!next_offset + (size_of_ctype ty)
    491          | (Global,_)           -> ()
    492          | (Param,_)            -> ()
    493          | (Stack _,_)          -> ()
    494       ) (get_stack_vars_stmt f.fn_body);
    495     variables
    496 
    497 let get_locals variables =
    498   Hashtbl.fold
    499     (fun id (v,_) l -> match v with
    500        | Local -> id::l
    501        | _ -> l
    502     ) variables []
    503 
    504 let get_stacksize variables =
    505   Hashtbl.fold
    506     (fun _ (v,t) c1 -> let c2 = match v with
    507        | Stack o -> o+(size_of_ctype t)
    508        | _ -> c1 in if c1 > c2 then c1 else c2
    509     ) variables 0
    510 
    511 let translate_internal globals f =
    512   let variables = sort_variables globals f in
    513     { f_sig =
    514         {
    515           args = List.map (fun p -> ctype_to_sig_type (snd p)) f.fn_params ;
    516           res = ctype_to_type_return f.fn_return
    517         };
    518       f_params = List.map fst f.fn_params ;
    519       f_vars = (fresh_tmp variables)::(get_locals variables);
    520       f_ptrs = [] (* will be filled in translate,
    521                      when calling CminorPointers.fill *);
    522       f_stacksize = get_stacksize variables ;
    523       f_body = translate_stmt variables f.fn_body
    524     }
     307let cmp_of_clight_binop = function
     308  | Clight.Oeq -> AST.Cmp_eq
     309  | Clight.One -> AST.Cmp_ne
     310  | Clight.Olt -> AST.Cmp_lt
     311  | Clight.Ole -> AST.Cmp_le
     312  | Clight.Ogt -> AST.Cmp_gt
     313  | Clight.Oge -> AST.Cmp_ge
     314  | _ -> assert false (* do not use on these arguments *)
     315
     316let translate_simple_binop t = function
     317  | Clight.Omul -> AST.Op_mul
     318  | Clight.Odiv when is_signed t -> AST.Op_div
     319  | Clight.Odiv -> AST.Op_divu
     320  | Clight.Omod when is_signed t -> AST.Op_mod
     321  | Clight.Omod -> AST.Op_modu
     322  | Clight.Oand -> AST.Op_and
     323  | Clight.Oor -> AST.Op_or
     324  | Clight.Oxor -> AST.Op_xor
     325  | Clight.Oshl -> AST.Op_shl
     326  | Clight.Oshr when is_signed t -> AST.Op_shr
     327  | Clight.Oshr -> AST.Op_shru
     328  | binop when is_pointer t -> AST.Op_cmpp (cmp_of_clight_binop binop)
     329  | binop when is_signed t -> AST.Op_cmp (cmp_of_clight_binop binop)
     330  | binop -> AST.Op_cmpu (cmp_of_clight_binop binop)
     331
     332let translate_binop res_type ctype1 ctype2 e1 e2 binop =
     333  match binop with
     334    | Clight.Oadd -> translate_add res_type ctype1 ctype2 e1 e2
     335    | Clight.Osub -> translate_sub res_type ctype1 ctype2 e1 e2
     336    | _ ->
     337      let cminor_binop = translate_simple_binop ctype1 binop in
     338      Cminor.Expr (Cminor.Op2 (cminor_binop, e1, e2), res_type)
     339
     340let translate_ident var_locs res_type x =
     341  let ed = match find_var_locs x var_locs with
     342    | (Local, _) | (Param, _) -> Cminor.Id x
     343    | (LocalStack off, t) | (ParamStack off, t) when is_scalar_ctype t ->
     344      let addr = Cminor.Expr (add_stack off, AST.Sig_ptr) in
     345      Cminor.Mem (quantity_of_ctype t, addr)
     346    | (LocalStack off, _) | (ParamStack off, _) ->
     347      add_stack off
     348    | (Global, t) when is_scalar_ctype t ->
     349      let addr = Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol x), AST.Sig_ptr) in
     350      Cminor.Mem (quantity_of_ctype t, addr)
     351    | (Global, _) -> Cminor.Cst (AST.Cst_addrsymbol x) in
     352  Cminor.Expr (ed, res_type)
     353
     354let translate_field res_type t e field =
     355  let (fields, offset) = match t with
     356    | Clight.Tstruct (_, fields) -> (fields, struct_offset t field fields)
     357    | Clight.Tunion (_, fields) ->
     358      (fields, Cminor.Expr (Cminor.Cst (AST.Cst_int 0), AST.Sig_offset))
     359    | _ -> assert false (* type error *) in
     360  let addr = Cminor.Expr (Cminor.Op2 (AST.Op_addp, e, offset), AST.Sig_ptr) in
     361  let quantity = quantity_of_ctype (List.assoc field fields) in
     362  Cminor.Expr (Cminor.Mem (quantity, addr), res_type)
     363
     364let translate_cast e src_type dest_type =
     365  let res_type = sig_type_of_ctype dest_type in
     366  match src_type, dest_type with
     367    | Clight.Tint (size1, sign1), Clight.Tint (size2, _) ->
     368      let t1 = (byte_size_of_intsize size1, sign1) in
     369      let t2 = byte_size_of_intsize size2 in
     370      Cminor.Expr (Cminor.Op1 (AST.Op_cast (t1, t2), e), res_type)
     371    | Clight.Tint _, Clight.Tpointer _
     372    | Clight.Tint _, Clight.Tarray _ ->
     373      Cminor.Expr (Cminor.Op1 (AST.Op_ptrofint, e), res_type)
     374    | Clight.Tpointer _, Clight.Tint _
     375    | Clight.Tarray _, Clight.Tint _ ->
     376      Cminor.Expr (Cminor.Op1 (AST.Op_intofptr, e), res_type)
     377    | _ -> e
     378
     379let rec f_expr var_locs (Clight.Expr (ed, t)) sub_exprs_res =
     380  let t_cminor = sig_type_of_ctype t in
     381  let cst_int i t = Cminor.Expr (Cminor.Cst (AST.Cst_int i), t) in
     382  match ed, sub_exprs_res with
     383
     384  | Clight.Econst_int i, _ ->
     385    Cminor.Expr (Cminor.Cst (AST.Cst_int i), t_cminor)
     386
     387  | Clight.Econst_float _, _ -> error_float ()
     388
     389  | Clight.Evar x, _ when is_function_ctype t ->
     390    Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol x), t_cminor)
     391
     392  | Clight.Evar x, _ -> translate_ident var_locs t_cminor x
     393
     394  | Clight.Ederef _, e :: _ when is_scalar_ctype t ->
     395    Cminor.Expr (Cminor.Mem (quantity_of_ctype t, e), t_cminor)
     396
     397  | Clight.Ederef _, e :: _ ->
     398    (* When dereferencing something pointing to a struct for instance, the
     399       result is the address of the struct. *)
     400    e
     401
     402  | Clight.Eaddrof e, _ -> translate_addrof var_locs e
     403
     404  | Clight.Eunop (unop, _), e :: _ ->
     405    Cminor.Expr (Cminor.Op1 (translate_unop unop, e), t_cminor)
     406
     407  | Clight.Ebinop (binop, e1, e2), e1' :: e2' :: _ ->
     408    translate_binop t_cminor (clight_type_of e1) (clight_type_of e2) e1' e2'
     409      binop
     410
     411  | Clight.Ecast (t, Clight.Expr (_, t')), e :: _ -> translate_cast e t' t
     412
     413  | Clight.Econdition _, e1 :: e2 :: e3 :: _ ->
     414    Cminor.Expr (Cminor.Cond (e1, e2, e3), t_cminor)
     415
     416  | Clight.Eandbool _, e1 :: e2 :: _ ->
     417    let zero = cst_int 0 t_cminor in
     418    let one = cst_int 1 t_cminor in
     419    let e2_cond = Cminor.Expr (Cminor.Cond (e2, one, zero), t_cminor) in
     420    Cminor.Expr (Cminor.Cond (e1, e2_cond, zero), t_cminor)
     421
     422  | Clight.Eorbool _, e1 :: e2 :: _ ->
     423    let zero = cst_int 0 t_cminor in
     424    let one = cst_int 1 t_cminor in
     425    let e2_cond = Cminor.Expr (Cminor.Cond (e2, one, zero), t_cminor) in
     426    Cminor.Expr (Cminor.Cond (e1, one, e2_cond), t_cminor)
     427
     428  | Clight.Esizeof t, _ -> esizeof_ctype t_cminor t
     429
     430  | Clight.Ecost (lbl, _), e :: _ ->
     431    Cminor.Expr (Cminor.Exp_cost (lbl, e), t_cminor)
     432
     433  | Clight.Ecall _, _ -> assert false (* only for annotations *)
     434
     435  | Clight.Efield (Clight.Expr (_, t), field), e :: _ ->
     436    translate_field t_cminor t e field
     437
     438  | _ -> assert false (* wrong number of arguments *)
     439
     440and translate_addrof_ident res_type var_locs id =
     441  match find_var_locs id var_locs with
     442    | (Local, _) | (Param, _) -> assert false (* type error *)
     443    | (LocalStack off, _) | (ParamStack off, _) ->
     444      Cminor.Expr (add_stack off, res_type)
     445    | (Global, _) ->
     446      Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol id), res_type)
     447
     448and translate_addrof_field res_type t field e =
     449  let (fields, offset) = match t with
     450    | Clight.Tstruct (_, fields) -> (fields, struct_offset t field fields)
     451    | Clight.Tunion (_, fields) ->
     452      (fields, Cminor.Expr (Cminor.Cst (AST.Cst_int 0), AST.Sig_offset))
     453    | _ -> assert false (* type error *) in
     454  Cminor.Expr (Cminor.Op2 (AST.Op_addp, e, offset), res_type)
     455
     456and translate_addrof var_locs (Clight.Expr (ed, _)) =
     457  let res_type = AST.Sig_ptr in
     458  match ed with
     459
     460    | Clight.Evar id -> translate_addrof_ident res_type var_locs id
     461
     462    | Clight.Ederef e -> translate_expr var_locs e
     463
     464    | Clight.Efield ((Clight.Expr (_, t) as e), field) ->
     465      let e = translate_expr var_locs e in
     466      translate_addrof_field res_type t field e
     467
     468    | _ -> assert false (* not a lvalue *)
     469
     470and translate_expr var_locs e = ClightFold.expr2 (f_expr var_locs) e
     471
     472
     473(* Translate statement *)
     474
     475let assign var_locs (Clight.Expr (ed, t) as e_res_clight) e_arg_cminor =
     476  match ed with
     477    | Clight.Evar id when is_local_or_param id var_locs ->
     478      Cminor.St_assign (id, e_arg_cminor)
     479    | _ ->
     480      let quantity = quantity_of_ctype t in
     481      let addr = translate_addrof var_locs e_res_clight in
     482      Cminor.St_store (quantity, addr, e_arg_cminor)
     483
     484let call_sig ret_type args =
     485  { AST.args = List.map cminor_type_of args ;
     486    AST.res = ret_type }
     487
     488let f_stmt fresh var_locs stmt sub_exprs_res sub_stmts_res =
     489  let (tmps, sub_stmts_res) = List.split sub_stmts_res in
     490  let tmps = List.flatten tmps in
     491
     492  let (added_tmps, stmt) = match stmt, sub_exprs_res, sub_stmts_res with
     493
     494    | Clight.Sskip, _, _ -> ([], Cminor.St_skip)
     495
     496    | Clight.Sassign (e1, _), _ :: e2 :: _, _ ->
     497      ([], assign var_locs e1 e2)
     498
     499    | Clight.Scall (None, _, _), f :: args, _ ->
     500      ([], Cminor.St_call (None, f, args, call_sig AST.Type_void args))
     501
     502    | Clight.Scall (Some e, _, _), _ :: f :: args, _ ->
     503      let t = sig_type_of_ctype (clight_type_of e) in
     504      let tmp = fresh () in
     505      let tmpe = Cminor.Expr (Cminor.Id tmp, t) in
     506      let stmt_call =
     507        Cminor.St_call (Some tmp, f, args, call_sig (AST.Type_ret t) args) in
     508      let stmt_assign = assign var_locs e tmpe in
     509      ([(tmp, t)], Cminor.St_seq (stmt_call, stmt_assign))
     510
     511    | Clight.Swhile _, e :: _, stmt :: _ ->
     512      let econd =
     513        Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in
     514      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      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      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)))))
     539
     540    | Clight.Sifthenelse _, e :: _, stmt1 :: stmt2 :: _ ->
     541      ([], Cminor.St_ifthenelse (e, stmt1, stmt2))
     542
     543    | Clight.Ssequence _, _, stmt1 :: stmt2 :: _ ->
     544      ([], Cminor.St_seq (stmt1, stmt2))
     545
     546    | Clight.Sbreak, _, _ -> ([], Cminor.St_exit 1)
     547
     548    | Clight.Scontinue, _, _ -> ([], Cminor.St_exit 0)
     549
     550    | Clight.Sswitch _, _, _ ->
     551      (* Should not appear because of switch transformation performed
     552         beforehand. *)
     553      assert false
     554
     555    | Clight.Sreturn None, _, _ -> ([], Cminor.St_return None)
     556
     557    | Clight.Sreturn (Some _), e :: _, _ -> ([], Cminor.St_return (Some e))
     558
     559    | Clight.Slabel (lbl, _), _, stmt :: _ -> ([], Cminor.St_label (lbl, stmt))
     560
     561    | Clight.Sgoto lbl, _, _ -> ([], Cminor.St_goto lbl)
     562
     563    | Clight.Scost (lbl, _), _, stmt :: _ -> ([], Cminor.St_cost (lbl, stmt))
     564
     565    | _ -> assert false (* type error *) in
     566
     567  (tmps @ added_tmps, stmt)
     568
     569let translate_statement fresh var_locs =
     570  ClightFold.statement2 (f_expr var_locs) (f_stmt fresh var_locs)
     571
     572
     573(* Translate functions and programs *)
     574
     575let add_stack_parameter_initialization x t off body =
     576  let addr = Cminor.Expr (add_stack off, AST.Sig_ptr) in
     577  let e = Cminor.Expr (Cminor.Id x, sig_type_of_ctype t) in
     578  let stmt = Cminor.St_store (quantity_of_ctype t, addr, e) in
     579  Cminor.St_seq (stmt, body)
     580
     581let add_stack_parameters_initialization var_locs body =
     582  let f x (location, t) body = match location with
     583    | ParamStack offset -> add_stack_parameter_initialization x t offset body
     584    | _ -> body in
     585  fold_var_locs f var_locs body
     586
     587let translate_internal fresh globals cfun =
     588  let var_locs = sort_variables globals cfun in
     589  let params =
     590    List.map (fun (x, t) -> (x, sig_type_of_ctype t)) cfun.Clight.fn_params in
     591  let (tmps, body) = translate_statement fresh var_locs cfun.Clight.fn_body in
     592  let body = add_stack_parameters_initialization var_locs body in
     593  { Cminor.f_return = type_return_of_ctype cfun.Clight.fn_return ;
     594    Cminor.f_params = params ;
     595    Cminor.f_vars = (get_locals var_locs) @ tmps ;
     596    Cminor.f_stacksize = get_stacksize var_locs ;
     597    Cminor.f_body = body }
    525598
    526599let translate_external id params return =
    527   {
    528     ef_tag = id ;
    529     ef_sig = {
    530       args = List.map ctype_to_sig_type params ;
    531       res = ctype_to_type_return return
    532     }
    533   }
    534 
    535 let translate_funct globals = function
    536   | (id,Internal ff) -> (id,F_int (translate_internal globals ff))
    537   | (id,External (i,p,r)) -> (id, F_ext (translate_external i p r))
     600  { AST.ef_tag = id ;
     601    AST.ef_sig = { AST.args = translate_args_types params ;
     602                   AST.res = type_return_of_ctype return } }
     603
     604let translate_funct fresh globals (id, def) =
     605  let def = match def with
     606    | Clight.Internal ff -> Cminor.F_int (translate_internal fresh globals ff)
     607    | Clight.External (i,p,r) -> Cminor.F_ext (translate_external i p r) in
     608  (id, def)
    538609
    539610let translate p =
    540   let p = Clight32ToClight8.translate p in
    541   let globals = List.map (fun p -> (fst (fst p),snd p) ) p.prog_vars in
    542   let p =
    543     {Cminor.vars   = List.map translate_global_vars p.prog_vars;
    544      Cminor.functs = List.map (translate_funct globals ) p.prog_funct;
    545      Cminor.main = p.prog_main } in
    546   (* TODO: find a better solution to get the pointers in the result. *)
    547   CminorPointers.fill p
     611  let fresh = ClightAnnotator.make_fresh "_tmp" p in
     612  { Cminor.vars = List.map translate_global p.Clight.prog_vars ;
     613    Cminor.functs =
     614      List.map (translate_funct fresh p.Clight.prog_vars) p.Clight.prog_funct ;
     615    Cminor.main = p.Clight.prog_main }
  • Deliverables/D2.2/8051/src/clight/clightToCminor.mli

    r486 r818  
    22    program. *)
    33
     4val sizeof_ctype : Clight.ctype -> AST.abstract_size
     5
    46(** [translate cp] compiles a Clight program into a Cminor program. *)
    5 (* Translation simplify control structures and explain memory operations *)
     7(* Translation simplifies control structures and explicits memory operations *)
    68
    79val translate : Clight.program -> Cminor.program
  • Deliverables/D2.2/8051/src/clight/runtime.ml

    r619 r818  
    11
    2 (** This module adds runtime functions in a [Clight] program. Some of these
    3     newly defined functions will be used in the Clight32ToClight8 transformation
    4     to replace primitive unary or binary operations. They are returned as
    5     association lists. The other functions implement unsupported functions by
    6     the target architecture that introduce a branch. We need to define them at
    7     the [Clight] level in order to have a correct labelling. *)
    8 
    9 
    10 let cint8 = Clight.Tint (Clight.I8, Clight.Signed)
    11 let cint32 = Clight.Tint (Clight.I32, Clight.Signed)
    12 
    13 
    14 let div_fun s =
    15   "signed char " ^ s ^ " (signed char x, signed char y) {\n" ^
    16   "  signed char x1 = x, y1 = y, sign = 1;\n" ^
    17   "  if (x1 < 0) { x1 = -x1; sign = -sign; }\n" ^
    18   "  if (y1 < 0) { y1 = -y1; sign = -sign; }\n" ^
    19   "  return (sign * (x1/y1));\n" ^
    20   "}\n\n"
    21 
    22 let div = ("_div", div_fun, (Clight.Odiv, cint8, cint8))
    23 
    24 
    25 let make_new_ops_assoc labs l =
    26   let f_op (base_name, op_fun, primitive_op) =
    27     let fresh_name = StringTools.Gen.fresh_prefix labs base_name in
    28     (op_fun fresh_name, (primitive_op, fresh_name)) in
    29   List.split (List.map f_op l)
    30 
    31 
    32 let add_new_ops new_ops p =
    33   let added_string =
    34     List.fold_left (fun s new_op -> s ^ "\n" ^ new_op) "" new_ops in
    35   let output = added_string ^ (ClightPrinter.print_program p) in
     2(** This module adds runtime functions in a [Clight] program. These functions
     3    implement unsupported functions by the target architecture that introduce a
     4    branch. We need to define them at the [Clight] level in order to have a
     5    correct labelling. *)
     6
     7
     8let error_prefix = "Adding runtime functions"
     9let error = Error.global_error error_prefix
     10
     11
     12let add_program p s =
    3613  let tmp_file = Filename.temp_file "add_runtime" ".c" in
    3714  let cout = open_out tmp_file in
     15  let output = s ^ (ClightPrinter.print_program p) in
    3816  output_string cout output ;
    3917  flush cout ;
     
    4422
    4523
    46 let add p =
    47   let labs = ClightAnnotator.all_labels p in
    48   let make_new_ops_assoc l = make_new_ops_assoc labs l in
    49   let (new_unops, unop_assoc) = make_new_ops_assoc [] in
    50   let (new_binops, binop_assoc) = make_new_ops_assoc [div] in
    51   let p = add_new_ops (new_unops @ new_binops) p in
    52   (p, unop_assoc, binop_assoc)
     24type operation =
     25  | Unary of Clight.unary_operation * Clight.ctype
     26  | Binary of Clight.binary_operation * Clight.ctype * Clight.ctype
     27  | Cast of Clight.ctype (* destination type *) * Clight.ctype (* source type *)
     28  | Fun of string (* name of the function *)
     29
     30type op_replacement =
     31    (* operation to be replaced *)
     32    operation *
     33    (* base name of the replacement function *)
     34    string *
     35    (* C definition of the replacement function, provided a name for the
     36       function *)
     37    (string -> string) *
     38    (* dependences *)
     39    operation list
     40
     41module CtypeSet =
     42  Set.Make (struct type t = Clight.ctype let compare = Pervasives.compare end)
     43
     44
     45let deps op replacements =
     46  let f res (op', _, _, deps) = if op' = op then deps else res in
     47  List.fold_left f [] replacements
     48
     49
     50(* Filter used operations only *)
     51
     52module OperationSet =
     53  Set.Make (struct type t = operation let compare = Pervasives.compare end)
     54
     55let union_list l = List.fold_left OperationSet.union OperationSet.empty l
     56
     57let f_ctype ctype _ = ctype
     58
     59let f_expr e _ sub_expr_descrs_res =
     60  let res_e = match e with
     61    | Clight.Expr (Clight.Evar x, Clight.Tfunction _) ->
     62      OperationSet.singleton (Fun x)
     63    | _ -> OperationSet.empty in
     64  union_list (res_e :: sub_expr_descrs_res)
     65
     66let f_expr_descr ed _ sub_exprs_res =
     67  let res_ed = match ed with
     68    | Clight.Eunop (unop, Clight.Expr (_, t)) ->
     69      OperationSet.singleton (Unary (unop, t))
     70    | Clight.Ebinop (binop, Clight.Expr (_, t1), Clight.Expr (_, t2)) ->
     71      OperationSet.singleton (Binary (binop, t1, t2))
     72    | Clight.Ecast (t, Clight.Expr (_, t')) ->
     73      OperationSet.singleton (Cast (t, t'))
     74    | _ -> OperationSet.empty in
     75  union_list (res_ed :: sub_exprs_res)
     76
     77let f_stmt _ sub_exprs_res sub_stmts_res =
     78  OperationSet.union (union_list sub_exprs_res) (union_list sub_stmts_res)
     79
     80let used_ops_stmt = ClightFold.statement f_ctype f_expr f_expr_descr f_stmt
     81
     82let used_ops_fundef = function
     83  | Clight.Internal cfun -> used_ops_stmt cfun.Clight.fn_body
     84  | Clight.External _ -> OperationSet.empty
     85
     86let used_ops p =
     87  let f ops (_, fundef) = OperationSet.union ops (used_ops_fundef fundef) in
     88  List.fold_left f OperationSet.empty p.Clight.prog_funct
     89
     90
     91let mem_replacements op =
     92  let f res (op', _, _, _) = res || (op' = op) in
     93  List.fold_left f false
     94
     95let rec fix equal next x =
     96  let y = next x in
     97  if equal x y then x
     98  else fix equal next y
     99
     100let needed_replacements used_ops replacements =
     101  let f op = mem_replacements op replacements in
     102  let reduced_used_ops = OperationSet.filter f used_ops in
     103  let next_ops ops =
     104    let add ops op = OperationSet.add op ops in
     105    let f op next_ops = List.fold_left add next_ops (deps op replacements) in
     106    OperationSet.fold f ops ops in
     107  let needed_ops = fix OperationSet.equal next_ops reduced_used_ops in
     108  let f (op, _, _, _) = OperationSet.mem op needed_ops in
     109  List.filter f replacements
     110
     111
     112let map_fresh_name unique map base_name =
     113  if StringTools.Map.mem base_name map then
     114    (map, StringTools.Map.find base_name map)
     115  else
     116    let fresh_name = unique base_name in
     117    (StringTools.Map.add base_name fresh_name map, fresh_name)
     118
     119let fresh_replacements unique replacements =
     120  let f (map, l) (op, base_name, new_fun, deps) =
     121    let (map, fresh_name) = map_fresh_name unique map base_name in
     122    (map, l @ [(op, fresh_name, new_fun fresh_name, deps)]) in
     123  snd (List.fold_left f (StringTools.Map.empty, []) replacements)
     124
     125
     126let add_replacements replacements p =
     127  let f_replacements s (_, _, new_fun, _) = s ^ "\n" ^ new_fun in
     128  let added_string = List.fold_left f_replacements "" replacements in
     129  add_program p added_string
     130
     131
     132let make_replacement_assoc = List.map (fun (op, name, _, _) -> (op, name))
     133
     134
     135let add p replacements =
     136  let used_ops = used_ops p in
     137  let needed_replacements = needed_replacements used_ops replacements in
     138  let unique = StringTools.make_unique (ClightAnnotator.all_idents p) in
     139  let replacements = fresh_replacements unique needed_replacements in
     140  let p = add_replacements replacements p in
     141  (p, make_replacement_assoc replacements)
     142
     143
     144(* Replacement *)
     145
     146let seq =
     147  List.fold_left
     148    (fun stmt1 stmt2 ->
     149      if stmt1 = Clight.Sskip then stmt2
     150      else
     151        if stmt2 = Clight.Sskip then stmt1
     152        else Clight.Ssequence (stmt1, stmt2))
     153    Clight.Sskip
     154
     155let f_ctype ctype _ = ctype
     156
     157let call fresh replaced replacement_assoc args ret_type =
     158  let tmp = fresh () in
     159  let replacement_fun_name = List.assoc replaced replacement_assoc in
     160  let tmpe = Clight.Expr (Clight.Evar tmp, ret_type) in
     161  let (args, args_types) = List.split args in
     162  let f_type = Clight.Tfunction (args_types, ret_type) in
     163  let f = Clight.Expr (Clight.Evar replacement_fun_name, f_type) in
     164  let call = Clight.Scall (Some tmpe, f, args) in
     165  (tmpe, call, [(tmp, ret_type)])
     166
     167let replace_ident replacement_assoc x t =
     168  let new_name = match t with
     169    | Clight.Tfunction _
     170        when List.mem_assoc (Fun x) replacement_assoc ->
     171      let replacement_fun_name = List.assoc (Fun x) replacement_assoc in
     172      replacement_fun_name
     173    | _ -> x in
     174  (Clight.Expr (Clight.Evar new_name, t), Clight.Sskip, [])
     175
     176let f_expr fresh replacement_assoc e _ _ =
     177
     178  let f (Clight.Expr (ed, t) as e) sub_exprs_res =
     179    let f_sub_exprs (es, stmt, tmps) (e, stmt', tmps') =
     180      (es @ [e], seq [stmt ; stmt'], tmps @ tmps') in
     181    let (sub_exprs, stmt1, tmps1) =
     182      List.fold_left f_sub_exprs ([], Clight.Sskip, []) sub_exprs_res in
     183    let (e, stmt2, tmps2) = match ed, sub_exprs with
     184      | Clight.Evar x, _ -> replace_ident replacement_assoc x t
     185      | Clight.Eunop (unop, Clight.Expr (_, t')), e' :: _
     186          when List.mem_assoc (Unary (unop, t')) replacement_assoc ->
     187        call fresh (Unary (unop, t')) replacement_assoc [(e', t')] t
     188      | Clight.Ebinop (binop, Clight.Expr (_, t1), Clight.Expr (_, t2)),
     189        e1 :: e2 :: _
     190          when List.mem_assoc (Binary (binop, t1, t2)) replacement_assoc ->
     191        call fresh (Binary (binop, t1, t2)) replacement_assoc
     192          [(e1, t1) ; (e2, t2)] t
     193      | Clight.Ecast (t, Clight.Expr (_, t')), e' :: _
     194          when List.mem_assoc (Cast (t, t')) replacement_assoc ->
     195        call fresh (Cast (t, t')) replacement_assoc [(e', t')] t
     196      | _ -> (e, Clight.Sskip, []) in
     197    (ClightFold.expr_fill_exprs e sub_exprs,
     198     seq [stmt1 ; stmt2],
     199     tmps1 @ tmps2) in
     200
     201  ClightFold.expr2 f e
     202
     203let f_expr_descr ed _ _ _ = ed
     204
     205let f_stmt stmt sub_exprs_res sub_stmts_res =
     206  let f_sub_exprs (es, stmt, tmps) (e, stmt', tmps') =
     207    (es @ [e], seq [stmt ; stmt'], tmps @ tmps') in
     208  let (sub_exprs, added_stmt, tmps1) =
     209    List.fold_left f_sub_exprs ([], Clight.Sskip, []) sub_exprs_res in
     210  let f_sub_stmts (stmts, tmps) (stmt, tmps') =
     211    (stmts @ [stmt], tmps @ tmps') in
     212  let (sub_stmts, tmps2) = List.fold_left f_sub_stmts ([], []) sub_stmts_res in
     213  let stmt' = ClightFold.statement_fill_subs stmt sub_exprs sub_stmts in
     214  (seq [added_stmt ; stmt'], tmps1 @ tmps2)
     215
     216let replace_statement fresh replacement_assoc =
     217  ClightFold.statement f_ctype (f_expr fresh replacement_assoc)
     218    f_expr_descr f_stmt
     219
     220let replace_internal fresh replacement_assoc def =
     221  let (new_body, tmps) =
     222    replace_statement fresh replacement_assoc def.Clight.fn_body in
     223  { def with
     224    Clight.fn_vars = def.Clight.fn_vars @ tmps ; Clight.fn_body = new_body }
     225
     226let replace_funct fresh replacement_assoc (id, fundef) =
     227  let fundef' = match fundef with
     228    | Clight.Internal def ->
     229      Clight.Internal (replace_internal fresh replacement_assoc def)
     230    | _ -> fundef in
     231  (id, fundef')
     232
     233let replace fresh replacement_assoc p =
     234  let prog_funct =
     235    List.map (replace_funct fresh replacement_assoc) p.Clight.prog_funct in
     236  { p with Clight.prog_funct = prog_funct }
     237
     238
     239let save_and_parse p =
     240  let tmp_file = Filename.temp_file "clight32toclight8" ".c" in
     241  try
     242    let oc = open_out tmp_file in
     243    output_string oc (ClightPrinter.print_program p) ;
     244    close_out oc ;
     245    let res = ClightParser.process tmp_file in
     246    Misc.SysExt.safe_remove tmp_file ;
     247    res
     248  with Sys_error _ -> failwith "Error reparsing Clight8 transformation."
     249
     250let add_replacements p replacements =
     251  let p = ClightCasts.simplify p in
     252  let (p, replacement_assoc) = add p replacements in
     253  let p = ClightCasts.simplify p in
     254  let tmp_universe = ClightAnnotator.fresh_universe "_tmp" p in
     255  let fresh () = StringTools.Gen.fresh tmp_universe in
     256  let p = replace fresh replacement_assoc p in
     257  let p = save_and_parse p in
     258  ClightCasts.simplify p
     259
     260
     261(* Unsupported operations by the 8051. *)
     262
     263let cint size sign = Clight.Tint (size, sign)
     264
     265let cints size = cint size AST.Signed
     266let cintu size = cint size AST.Unsigned
     267
     268let cint8s = cints Clight.I8
     269let cint8u = cintu Clight.I8
     270let cint16s = cints Clight.I16
     271let cint16u = cintu Clight.I16
     272let cint32s = cints Clight.I32
     273let cint32u = cintu Clight.I32
     274
     275let byte_size_of_intsize = function
     276  | Clight.I8 -> 1
     277  | Clight.I16 -> 2
     278  | Clight.I32 -> 4
     279
     280let bit_size_of_intsize size = (byte_size_of_intsize size) * 8
     281
     282let string_of_intsize size = string_of_int (bit_size_of_intsize size)
     283
     284let ctype_of_intsize = function
     285  | Clight.I8 -> "char"
     286  | Clight.I16 -> "short"
     287  | Clight.I32 -> "int"
     288
     289
     290(* Unsigned divisions and modulos *)
     291
     292let divumodu_fun res t s =
     293  "unsigned " ^ t ^ " " ^ s ^ " (unsigned " ^ t ^ " x, unsigned " ^ t ^ " y)" ^
     294    "{\n" ^
     295  "  unsigned " ^ t ^ " quo = 0;\n" ^
     296  "  unsigned " ^ t ^ " rem = x;\n" ^
     297  "  while (rem >= y) {\n" ^
     298  "    rem = rem - y;\n" ^
     299  "    quo = quo + 1;\n" ^
     300  "  }\n" ^
     301  "  return (" ^ res ^ ");\n" ^
     302  "}\n\n"
     303
     304let divumodu op sizes sizec t =
     305  let (prefix, res) = match op with
     306    | Clight.Odiv -> ("div", "quo")
     307    | Clight.Omod -> ("mod", "rem")
     308    | _ -> assert false (* do not use on these arguments *) in
     309  let cu = cintu sizec in
     310  (Binary (op, cu, cu), "_" ^ prefix ^ sizes ^ "u", divumodu_fun res t, [])
     311
     312let divu = divumodu Clight.Odiv
     313let modu = divumodu Clight.Omod
     314
     315
     316(* Unsigned divisions *)
     317
     318(* 16 bits unsigned division *)
     319
     320let div16u = divu "16" Clight.I16 "short"
     321
     322(* 32 bits unsigned division *)
     323
     324let div32u = divu "32" Clight.I32 "int"
     325
     326(* Signed divisions *)
     327
     328let divs_fun t s =
     329  "signed " ^ t ^ " " ^ s ^ " (signed " ^ t ^ " x, signed " ^ t ^ " y) {\n" ^
     330  "  unsigned " ^ t ^ " x1 = (unsigned " ^ t ^ ") x;\n" ^
     331  "  unsigned " ^ t ^ " y1 = (unsigned " ^ t ^ ") y;\n" ^
     332  "  signed " ^ t ^ " sign = 1;\n" ^
     333  "  if (x < 0) { x1 = (unsigned " ^ t ^ ") (-x); sign = -sign; }\n" ^
     334  "  if (y < 0) { y1 = (unsigned " ^ t ^ ") (-y); sign = -sign; }\n" ^
     335  "  return (sign * ((signed " ^ t ^ ") (x1/y1)));\n" ^
     336  "}\n\n"
     337
     338let divs sizes sizec t =
     339  let cs = cints sizec in
     340  let cu = cintu sizec in
     341  (Binary (Clight.Odiv, cs, cs), "_div" ^ sizes ^ "s", divs_fun t,
     342   [Binary (Clight.Odiv, cu, cu)])
     343
     344(* 8 bits signed division *)
     345
     346let div8s = divs "8" Clight.I8 "char"
     347
     348(* 16 bits signed division *)
     349
     350let div16s = divs "16" Clight.I16 "short"
     351
     352(* 32 bits signed division *)
     353
     354let div32s = divs "32" Clight.I32 "int"
     355
     356
     357(* Unsigned modulos *)
     358
     359(* 16 bits unsigned modulo *)
     360
     361let mod16u = modu "16" Clight.I16 "short"
     362
     363(* 32 bits unsigned modulo *)
     364
     365let mod32u = modu "32" Clight.I32 "int"
     366
     367(* Signed modulos *)
     368
     369let mods_fun t s =
     370  "signed " ^ t ^ " " ^ s ^ " (signed " ^ t ^ " x, signed " ^ t ^ " y) {\n" ^
     371  "  return (x - (x/y) * y);\n" ^
     372  "}\n\n"
     373
     374let mods size ct t =
     375  (Binary (Clight.Omod, ct, ct), "_mod" ^ size ^ "s", mods_fun t,
     376   [Binary (Clight.Odiv, ct, ct)])
     377
     378(* 8 bits signed modulo *)
     379
     380let mod8s = mods "8" cint8s "char"
     381
     382(* 16 bits signed modulo *)
     383
     384let mod16s = mods "16" cint16s "short"
     385
     386(* 32 bits signed modulo *)
     387
     388let mod32s = mods "32" cint32s "int"
     389
     390
     391(* Shifts *)
     392
     393let sh_fun op t s =
     394  t ^ " " ^ s ^ " (" ^ t ^ " x, " ^ t ^ " y) {\n" ^
     395  "  " ^ t ^ " res = x, i;\n" ^
     396  "  for (i = 0 ; i < y ; i++) res = res " ^ op ^ " 2;\n" ^
     397  "  return res;\n" ^
     398  "}\n\n"
     399
     400let sh cop sop direction deps size sign =
     401  let sizes = string_of_intsize size in
     402  let ct = Clight.Tint (size, sign) in
     403  let (short_sign, long_sign) = match sign with
     404    | AST.Signed -> ("s", "signed ")
     405    | AST.Unsigned -> ("u", "unsigned ") in
     406  let t = long_sign ^ (ctype_of_intsize size) in
     407  (Binary (cop, ct, ct), "_sh" ^ direction ^ sizes ^ short_sign,
     408   sh_fun sop t, deps)
     409
     410
     411(* Shift lefts *)
     412
     413let shl = sh Clight.Oshl "*" "l" []
     414
     415(* Signed shift lefts *)
     416
     417(* 8 bits signed shift left *)
     418
     419let shl8s = shl Clight.I8 AST.Signed
     420
     421(* 16 bits signed shift left *)
     422
     423let shl16s = shl Clight.I16 AST.Signed
     424
     425(* 32 bits signed shift left *)
     426
     427let shl32s = shl Clight.I32 AST.Signed
     428
     429(* Unsigned shift lefts *)
     430
     431(* 8 bits unsigned shift left *)
     432
     433let shl8u = shl Clight.I8 AST.Unsigned
     434
     435(* 16 bits unsigned shift left *)
     436
     437let shl16u = shl Clight.I16 AST.Unsigned
     438
     439(* 32 bits unsigned shift left *)
     440
     441let shl32u = shl Clight.I32 AST.Unsigned
     442
     443
     444(* Shift rights *)
     445
     446(* Signed shift rights *)
     447
     448let shrs_fun size t s =
     449  "signed " ^ t ^ " " ^ s ^ " (signed " ^ t ^ " x, signed " ^ t ^ " y) {\n" ^
     450  "  unsigned " ^ t ^ " x1, y1, to_add, res, i;\n" ^
     451  "  if (y < 0) return 0;\n" ^
     452  "  x1 = x; y1 = y; to_add = 1; res = x1;" ^
     453  "  for (i = 0 ; i < " ^ size ^ " ; i++) to_add = to_add * 2;\n" ^
     454  "  to_add = to_add & x1;\n" ^
     455  "  for (i = 0 ; i < y1 ; i++) res = (res / 2) + to_add;\n" ^
     456  "  return ((signed " ^ t ^ ") res);\n" ^
     457  "}\n\n"
     458
     459let shrs size =
     460  let sizes = string_of_int (bit_size_of_intsize size) in
     461  let op_sizes = string_of_int ((bit_size_of_intsize size) - 1) in
     462  let t = ctype_of_intsize size in
     463  let ct = Clight.Tint (size, AST.Signed) in
     464  let ctdep = Clight.Tint (size, AST.Unsigned) in
     465  (Binary (Clight.Oshr, ct, ct), "_shr" ^ sizes ^ "s", shrs_fun op_sizes t,
     466   [Binary (Clight.Odiv, ctdep, ctdep)])
     467
     468(* 8 bits signed shift right *)
     469
     470let shr8s = shrs Clight.I8
     471
     472(* 16 bits signed shift right *)
     473
     474let shr16s = shrs Clight.I16
     475
     476(* 32 bits signed shift right *)
     477
     478let shr32s = shrs Clight.I32
     479
     480(* Unsigned shift rights *)
     481
     482let shru size =
     483  let t_dep = Clight.Tint (size, AST.Unsigned) in
     484  sh Clight.Oshr "/" "r" [Binary (Clight.Odiv, t_dep, t_dep)] size AST.Unsigned
     485
     486(* 8 bits unsigned shift right *)
     487
     488let shr8u = shru Clight.I8
     489
     490(* 16 bits unsigned shift right *)
     491
     492let shr16u = shru Clight.I16
     493
     494(* 32 bits unsigned shift right *)
     495
     496let shr32u = shru Clight.I32
     497
     498
     499let unsupported =
     500  [div16u ; div32u ; div8s ; div16s ; div32s ;
     501   mod16u ; mod32u ; mod8s ; mod16s ; mod32s ;
     502   shl8s ; shl16s ; shl32s ; shl8u ; shl16u ; shl32u ;
     503   shr8s ; shr16s ; shr32s ; shr8u ; shr16u ; shr32u]
     504
     505
     506let replace_unsupported p = add_replacements p unsupported
  • Deliverables/D2.2/8051/src/clight/runtime.mli

    r619 r818  
    11
    2 (** This module adds runtime functions in a [Clight] program. Some of these
    3     newly defined functions will be used in the Clight32ToClight8 transformation
    4     to replace primitive unary or binary operations. They are returned as
    5     association lists. The other functions implement unsupported functions by
    6     the target architecture that introduce a branch. We need to define them at
    7     the [Clight] level in order to have a correct labelling. *)
     2(** This module adds runtime functions in a [Clight] program. These functions
     3    implement unsupported functions by the target architecture that introduce a
     4    branch. We need to define them at the [Clight] level in order to have a
     5    correct labelling. *)
    86
    9 val add : Clight.program ->
    10   (Clight.program *
    11      ((Clight.unary_operation * Clight.ctype) * string) list *
    12      ((Clight.binary_operation * Clight.ctype * Clight.ctype) *
    13          string) list)
     7type operation =
     8  | Unary of Clight.unary_operation * Clight.ctype
     9  | Binary of Clight.binary_operation * Clight.ctype * Clight.ctype
     10  | Cast of Clight.ctype (* destination type *) * Clight.ctype (* source type *)
     11  | Fun of string (* name of the function *)
     12
     13type op_replacement =
     14    (* operation to be replaced *)
     15    operation *
     16    (* base name of the replacement function *)
     17    string *
     18    (* C definition of the replacement function, provided a name for the
     19       function *)
     20    (string -> string) *
     21    (* dependences *)
     22    operation list
     23
     24val add :
     25  Clight.program -> op_replacement list ->
     26  (Clight.program * (operation * string) list (* operation association *))
     27
     28val replace_unsupported : Clight.program -> Clight.program
Note: See TracChangeset for help on using the changeset viewer.