Changeset 460


Ignore:
Timestamp:
Jan 19, 2011, 6:23:27 PM (7 years ago)
Author:
campbell
Message:

Port memory spaces changes to latest prototype compiler.

Location:
Deliverables/D2.3/8051-memoryspaces-branch
Files:
1 added
32 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.3/8051-memoryspaces-branch/cparser/AddCasts.ml

    r453 r460  
    4040  | TFloat(k1, _), TFloat(k2, _) ->
    4141      float_rank k1 <= float_rank k2
    42   | TPtr(ty1, _), TPtr(ty2, _) -> is_void_type env ty2
     42  | TPtr(sp1, ty1, _), TPtr(sp2, ty2, _) when sp1 = sp2 -> is_void_type env ty2
    4343  | _, _ -> false
    4444  end
     
    5353  if cast_not_needed env e.etyp tto
    5454  then e
    55   else {edesc = ECast(tto, e); etyp = tto}
     55  else {edesc = ECast(tto, e); etyp = tto; espace = Any}
    5656
    5757(* Note: this pass applies only to simplified expressions
     
    7474        | Opreincr | Opredecr | Opostincr | Opostdecr ->
    7575            assert false (* not simplified *)
    76       in { edesc = desc; etyp = e.etyp }
     76      in { edesc = desc; etyp = e.etyp; espace = e.espace }
    7777  | EBinop(op, e1, e2, ty) ->
    7878      let e1' = add_expr env e1 in
     
    9898        | Oand_assign|Oor_assign|Oxor_assign|Oshl_assign|Oshr_assign ->
    9999            assert false (* not simplified *)
    100       in { edesc = desc; etyp = e.etyp }
     100      in { edesc = desc; etyp = e.etyp; espace = e.espace }
    101101  | EConditional(e1, e2, e3) ->
    102102      { edesc =
    103103          EConditional(add_expr env e1, add_expr env e2, add_expr env e3);
    104         etyp = e.etyp }
     104        etyp = e.etyp;
     105        espace = e.espace }
    105106  | ECast(ty, e1) ->
    106       { edesc = ECast(ty, add_expr env e1); etyp = e.etyp }
     107      { edesc = ECast(ty, add_expr env e1); etyp = e.etyp; espace = e.espace }
    107108  | ECall(e1, el) ->
    108109      assert false (* not simplified *)
     
    133134    match unroll env ty_fun with
    134135    | TFun(res, args, vararg, a) -> args
    135     | TPtr(ty, a) ->
     136    | TPtr(_, ty, a) ->
    136137        begin match unroll env ty with
    137138        | TFun(res, args, vararg, a) -> args
     
    147148let add_topexpr env loc e =
    148149  match e.edesc with
    149   | EBinop(Oassign, lhs, {edesc = ECall(e1, el); etyp = ty}, _) ->
     150  | EBinop(Oassign, lhs, {edesc = ECall(e1, el); etyp = ty; espace = space}, _) ->
    150151      let ecall =
    151152        {edesc = ECall(add_expr env e1, add_arguments env e1.etyp el);
    152          etyp = ty} in
     153         etyp = ty; espace = space} in
    153154      if cast_not_needed env ty lhs.etyp then
    154155        sassign loc (add_expr env lhs) ecall
     
    163164      let ecall =
    164165        {edesc = ECall(add_expr env e1, add_arguments env e1.etyp el);
    165          etyp = e.etyp} in
     166         etyp = e.etyp; espace = e.espace} in
    166167      {sdesc = Sdo ecall; sloc = loc}
    167168  | _ ->
     
    176177      let ty_elt =
    177178        match unroll env tto with
    178         | TArray(ty, _, _) -> ty | _ -> assert false in
     179        | TArray(_,ty, _, _) -> ty | _ -> assert false in
    179180      Init_array (List.map (add_init env ty_elt) il)
    180181  | Init_struct(id, fil) ->
  • Deliverables/D2.3/8051-memoryspaces-branch/cparser/Bitfields.ml

    r453 r460  
    119119      bf.bf_pos in
    120120  (* Give the mask an hexadecimal string representation, nicer to read *)
    121   {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m)); etyp = TInt(IUInt, [])}
     121  {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m)); etyp = TInt(IUInt, []); espace = Code} (* XXX are consts always Code? *)
    122122
    123123(* Extract the value of a bitfield *)
     
    141141  let e1 =
    142142    {edesc = EBinop(Oshl, carrier, left_shift_count bf, TInt(IUInt, []));
    143      etyp = carrier.etyp} in
     143     etyp = carrier.etyp; espace = Any} in
    144144  let ty = TInt((if bf.bf_signed then IInt else IUInt), []) in
    145145  let e2 =
    146     {edesc = ECast(ty, e1); etyp = ty} in
     146    {edesc = ECast(ty, e1); etyp = ty; espace = Any} in
    147147  {edesc = EBinop(Oshr, e2, right_shift_count bf, e2.etyp);
    148    etyp = e2.etyp}
     148   etyp = e2.etyp; espace = Any}
    149149
    150150(* Assign a bitfield within a carrier *)
     
    162162let bitfield_assign bf carrier newval =
    163163  let msk = insertion_mask bf in
    164   let notmsk = {edesc = EUnop(Onot, msk); etyp = msk.etyp} in
     164  let notmsk = {edesc = EUnop(Onot, msk); etyp = msk.etyp; espace = Any} in
    165165  let newval_shifted =
    166166    {edesc = EBinop(Oshl, newval, intconst (Int64.of_int bf.bf_pos) IUInt,
    167167                    TInt(IUInt,[]));
    168      etyp = TInt(IUInt,[])} in
     168     etyp = TInt(IUInt,[]);
     169     espace = Any} in
    169170  let newval_masked =
    170171    {edesc = EBinop(Oand, newval_shifted, msk, TInt(IUInt,[]));
    171      etyp = TInt(IUInt,[])}
     172     etyp = TInt(IUInt,[]);
     173     espace = Any}
    172174  and oldval_masked =
    173175    {edesc = EBinop(Oand, carrier, notmsk, TInt(IUInt,[]));
    174      etyp = TInt(IUInt,[])} in
     176     etyp = TInt(IUInt,[]); espace = Any} in
    175177  {edesc = EBinop(Oor,  oldval_masked, newval_masked,  TInt(IUInt,[]));
    176    etyp =  TInt(IUInt,[])}
     178   etyp =  TInt(IUInt,[]); espace = Any}
    177179
    178180(* Expressions *)
     
    189191  let is_bitfield_access_ptr ty fieldname =
    190192    match unroll env ty with
    191     | TPtr(ty', _) -> is_bitfield_access ty' fieldname
     193    | TPtr(_, ty', _) -> is_bitfield_access ty' fieldname
    192194    | _ -> None in
    193195
     
    202204        begin match is_bitfield_access e1.etyp fieldname with
    203205        | None ->
    204             {edesc = EUnop(Odot fieldname, e1'); etyp = e.etyp}
     206            {edesc = EUnop(Odot fieldname, e1'); etyp = e.etyp; espace = e1'.espace}
    205207        | Some bf ->
    206208            bitfield_extract bf
    207209              {edesc = EUnop(Odot bf.bf_carrier, e1');
    208                etyp = bf.bf_carrier_typ}
     210               etyp = bf.bf_carrier_typ;
     211               espace = e1'.espace}
    209212        end
    210213
     
    213216        begin match is_bitfield_access_ptr e1.etyp fieldname with
    214217        | None ->
    215             {edesc = EUnop(Oarrow fieldname, e1'); etyp = e.etyp}
     218            {edesc = EUnop(Oarrow fieldname, e1'); etyp = e.etyp; espace = Any}
    216219        | Some bf ->
    217220            bitfield_extract bf
    218221              {edesc = EUnop(Oarrow bf.bf_carrier, e1');
    219                etyp = bf.bf_carrier_typ}
     222               etyp = bf.bf_carrier_typ; espace = Any}
    220223        end
    221224
    222225    | EUnop(op, e1) ->
    223226        (* Note: simplified expr, so no ++/-- *)
    224         {edesc = EUnop(op, texp e1); etyp = e.etyp}
     227        {edesc = EUnop(op, texp e1); etyp = e.etyp; espace = e.espace}
    225228
    226229    | EBinop(Oassign, e1, e2, ty) ->
     
    232235                {edesc = EBinop(Oassign,
    233236                                {edesc = EUnop(Odot fieldname, lhs);
    234                                  etyp = e1.etyp},
     237                                 etyp = e1.etyp; espace = lhs.espace},
    235238                                rhs, ty);
    236                  etyp = e.etyp}
     239                 etyp = e.etyp;
     240                 espace = e.espace}
    237241            | Some bf ->
    238242                let carrier =
    239243                  {edesc = EUnop(Odot bf.bf_carrier, lhs);
    240                    etyp = bf.bf_carrier_typ} in
     244                   etyp = bf.bf_carrier_typ;
     245                   espace = lhs.espace} in
    241246                {edesc = EBinop(Oassign, carrier,
    242247                                bitfield_assign bf carrier rhs,
    243248                                carrier.etyp);
    244                  etyp = carrier.etyp}
     249                 etyp = carrier.etyp;
     250                 espace = lhs.espace}
    245251            end
    246252        | EUnop(Oarrow fieldname, e11) ->
     
    250256                {edesc = EBinop(Oassign,
    251257                                {edesc = EUnop(Oarrow fieldname, lhs);
    252                                  etyp = e1.etyp},
     258                                 etyp = e1.etyp;
     259                                 espace = e1.espace},
    253260                                rhs, ty);
    254                  etyp = e.etyp}
     261                 etyp = e.etyp;
     262                 espace = e.espace}
    255263            | Some bf ->
    256264                let carrier =
    257265                  {edesc = EUnop(Oarrow bf.bf_carrier, lhs);
    258                    etyp = bf.bf_carrier_typ} in
     266                   etyp = bf.bf_carrier_typ;
     267                   espace = Any} in
    259268                {edesc = EBinop(Oassign, carrier,
    260269                                bitfield_assign bf carrier rhs,
    261270                                carrier.etyp);
    262                  etyp = carrier.etyp}
     271                 etyp = carrier.etyp;
     272                 espace = Any}
    263273            end
    264274        | _ ->
    265             {edesc = EBinop(Oassign, texp e1, texp e2, e1.etyp); etyp = e1.etyp}
     275            {edesc = EBinop(Oassign, texp e1, texp e2, e1.etyp); etyp = e1.etyp; espace = e1.espace}
    266276        end
    267277
    268278    | EBinop(op, e1, e2, ty) ->
    269279        (* Note: simplified expr assumed, so no assign-op *)
    270         {edesc = EBinop(op, texp e1, texp e2, ty); etyp = e.etyp}
     280        {edesc = EBinop(op, texp e1, texp e2, ty); etyp = e.etyp; espace = e.espace}
    271281    | EConditional(e1, e2, e3) ->
    272         {edesc = EConditional(texp e1, texp e2, texp e3); etyp = e.etyp}
     282        {edesc = EConditional(texp e1, texp e2, texp e3); etyp = e.etyp; espace = e.espace}
    273283    | ECast(ty, e1) ->
    274         {edesc = ECast(ty, texp e1); etyp = e.etyp}
     284        {edesc = ECast(ty, texp e1); etyp = e.etyp; espace = e.espace}
    275285    | ECall(e1, el) ->
    276         {edesc = ECall(texp e1, List.map texp el); etyp = e.etyp}
     286        {edesc = ECall(texp e1, List.map texp el); etyp = e.etyp; espace = e.espace}
    277287
    278288  in texp e
     
    326336      let e_mask =
    327337        {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m));
    328          etyp = TInt(IUInt, [])} in
     338         etyp = TInt(IUInt, []);
     339         espace = Any} in
    329340      let e_and =
    330341        {edesc = EBinop(Oand, e, e_mask, TInt(IUInt,[]));
    331          etyp = TInt(IUInt,[])} in
     342         etyp = TInt(IUInt,[]);
     343         espace = Any} in
    332344      {edesc = EBinop(Oshl, e_and, intconst (Int64.of_int bf.bf_pos) IInt,
    333345                      TInt(IUInt, []));
    334        etyp = TInt(IUInt, [])}
     346       etyp = TInt(IUInt, []);
     347       espace = Any}
    335348  | _ -> assert false
    336349
     
    355368  | e1 :: el ->
    356369      {edesc = EBinop(Oor, e1, or_expr_list el, TInt(IUInt,[]));
    357        etyp = TInt(IUInt,[])}
     370       etyp = TInt(IUInt,[]);
     371       espace = Any}
    358372
    359373let rec transf_struct_init id fld_init_list =
     
    368382          fld_bitfield = None},
    369383         Init_single {edesc = ECast(bf.bf_carrier_typ, or_expr_list el);
    370                       etyp = bf.bf_carrier_typ})
     384                      etyp = bf.bf_carrier_typ;
     385                      espace = Any})
    371386        :: transf_struct_init id rem'
    372387      with Not_found ->
  • Deliverables/D2.3/8051-memoryspaces-branch/cparser/Builtins.ml

    r453 r460  
    3838         Some (List.map (fun ty -> (Env.fresh_ident "", ty)) args),
    3939         va, []) in
    40   let (id, env') = Env.enter_ident !env s Storage_extern ty in
     40  let (id, env') = Env.enter_ident !env s Storage_extern ty Code in
    4141  env := env';
    4242  idents := id :: !idents;
    43   decls := {gdesc = Gdecl(Storage_extern, id, ty, None); gloc = no_loc} :: !decls
     43  decls := {gdesc = Gdecl(Code, (Storage_extern, id, ty, None)); gloc = no_loc} :: !decls
    4444
    4545type t = {
  • Deliverables/D2.3/8051-memoryspaces-branch/cparser/C.mli

    r453 r460  
    125125(** Types *)
    126126
     127type memory_space =
     128  | Any
     129  | Data
     130  | IData
     131  | PData
     132  | XData
     133  | Code
     134
    127135type typ =
    128136  | TVoid of attributes
    129137  | TInt of ikind * attributes
    130138  | TFloat of fkind * attributes
    131   | TPtr of typ * attributes
    132   | TArray of typ * int64 option * attributes
     139  | TPtr of memory_space * typ * attributes
     140  | TArray of memory_space * typ * int64 option * attributes
    133141  | TFun of typ * (ident * typ) list option * bool * attributes
    134142  | TNamed of ident * attributes
     
    138146(** Expressions *)
    139147
    140 type exp = { edesc: exp_desc; etyp: typ }
     148type exp = { edesc: exp_desc; etyp: typ; espace: memory_space }
    141149
    142150and exp_desc =
     
    221229
    222230and globdecl_desc =
    223   | Gdecl of decl           (* variable declaration, function prototype *)
     231  | Gdecl of memory_space * decl  (* variable declaration, function prototype *)
    224232  | Gfundef of fundef                   (* function definition *)
    225233  | Gcompositedecl of struct_or_union * ident (* struct/union declaration *)
  • Deliverables/D2.3/8051-memoryspaces-branch/cparser/Ceval.ml

    r453 r460  
    100100      then F(normalize_float (Int64.to_float n) fk)
    101101      else F(normalize_float (int64_unsigned_to_float n) fk)
    102   | TPtr(ty, _), I n ->
     102  | TPtr(_, ty, _), I n ->
    103103      I (normalize_int n ptr_t_ikind)
    104   | TPtr(ty, _), F n ->
     104  | TPtr(_, ty, _), F n ->
    105105      if n = 0.0 then I 0L else raise Notconst
    106   | TPtr(ty, _), (S _ | WS _) ->
     106  | TPtr(_, ty, _), (S _ | WS _) ->
    107107      v
    108108  | _, _ ->
     
    271271    | TInt(ik, _), I n -> Some(CInt(n, ik, ""))
    272272    | TFloat(fk, _), F n -> Some(CFloat(n, fk, ""))
    273     | TPtr(_, _), I 0L -> Some(CInt(0L, IInt, ""))
    274     | TPtr(_, _), S s -> Some(CStr s)
    275     | TPtr(_, _), WS s -> Some(CWStr s)
     273    | TPtr(_, _, _), I 0L -> Some(CInt(0L, IInt, ""))
     274    | TPtr(_, _, _), S s -> Some(CStr s)
     275    | TPtr(_, _, _), WS s -> Some(CWStr s)
    276276    | _   -> None
    277277  with Notconst -> None
  • Deliverables/D2.3/8051-memoryspaces-branch/cparser/Cleanup.ml

    r453 r460  
    4141
    4242let rec add_typ = function
    43   | TPtr(ty, _) -> add_typ ty
    44   | TArray(ty, _, _) -> add_typ ty
     43  | TPtr(_, ty, _) -> add_typ ty
     44  | TArray(_, ty, _, _) -> add_typ ty
    4545  | TFun(res, None, _, _) -> add_typ res
    4646  | TFun(res, Some params, _, _) -> add_typ res; add_vars params
     
    121121  | g :: rem ->
    122122      match g.gdesc with
    123       | Gdecl decl when visible_decl decl ->
     123      | Gdecl (_,decl) when visible_decl decl ->
    124124          add_decl decl; add_init_globdecls accu rem
    125125      | Gfundef({fd_storage = Storage_default} as f) ->
     
    136136  | g :: rem ->
    137137      match g.gdesc with
    138       | Gdecl((sto, id, ty, init) as decl) ->
     138      | Gdecl(_, ((sto, id, ty, init) as decl)) ->
    139139          if needed id
    140140          then (add_decl decl; add_needed_globdecls accu rem)
     
    175175      let need =
    176176        match g.gdesc with
    177         | Gdecl((sto, id, ty, init) as decl) -> visible_decl decl || needed id
     177        | Gdecl(_, ((sto, id, ty, init) as decl)) -> visible_decl decl || needed id
    178178        | Gfundef f -> f.fd_storage = Storage_default || needed f.fd_name
    179179        | Gcompositedecl(_, id) -> needed id
  • Deliverables/D2.3/8051-memoryspaces-branch/cparser/Cprint.ml

    r453 r460  
    6868  | TFloat(k, a) ->
    6969      fprintf pp "%s%a%t" (name_of_fkind k) attributes a n
    70   | TPtr(t, a) ->
     70  | TPtr(_, t, a) -> (* XXX *)
    7171      let n' pp =
    7272        match t with
     
    7474        | _ -> fprintf pp " *%a%t" attributes a n in
    7575      dcl pp t n'
    76   | TArray(t, sz, a) ->
     76  | TArray(_, t, sz, a) -> (* XXX *)
    7777      let n' pp =
    7878        begin match a with
     
    354354  | Sseq(s1, s2) ->
    355355      {edesc = EBinop(Ocomma, exp_of_stmt s1, exp_of_stmt s2, TVoid []);
    356        etyp = TVoid []}
     356       etyp = TVoid [];
     357       espace = Any}
    357358  | Sif(e, s1, s2) ->
    358359      {edesc = EConditional(e, exp_of_stmt s1, exp_of_stmt s2);
    359        etyp = TVoid []}
     360       etyp = TVoid [];
     361       espace = Any}
    360362  | _ ->
    361363      raise Not_expr
     
    374376              exp (0, e) stmt_block s1
    375377  | Sif(e, {sdesc = Sskip}, s2) ->
    376       let not_e = {edesc = EUnop(Olognot, e); etyp = TInt(IInt, [])} in
     378      let not_e = {edesc = EUnop(Olognot, e); etyp = TInt(IInt, []); espace = Any} in
    377379      fprintf pp "@[<v 2>if (%a) {@ %a@;<0 -2>}@]"
    378380              exp (0, not_e) stmt_block s2
     
    456458  location pp g.gloc;
    457459  match g.gdesc with
    458   | Gdecl d ->
     460  | Gdecl (_, d) -> (* XXX *)
    459461      fprintf pp "%a@ @ " full_decl d
    460462  | Gfundef f ->
  • Deliverables/D2.3/8051-memoryspaces-branch/cparser/Cutil.ml

    r453 r460  
    7272  | TInt(ik, a) -> TInt(ik, add_attributes attr a)
    7373  | TFloat(fk, a) -> TFloat(fk, add_attributes attr a)
    74   | TPtr(ty, a) -> TPtr(ty, add_attributes attr a)
    75   | TArray(ty, sz, a) -> TArray(add_attributes_type attr ty, sz, a)
     74  | TPtr(sp, ty, a) -> TPtr(sp, ty, add_attributes attr a)
     75  | TArray(sp, ty, sz, a) -> TArray(sp, add_attributes_type attr ty, sz, a)
    7676  | TFun(ty, params, vararg, a) -> TFun(ty, params, vararg, add_attributes attr
    7777a)
     
    9696  | TInt(ik, a) -> a
    9797  | TFloat(fk, a) -> a
    98   | TPtr(ty, a) -> a
    99   | TArray(ty, sz, a) -> a              (* correct? *)
     98  | TPtr(_, ty, a) -> a
     99  | TArray(_, ty, sz, a) -> a              (* correct? *)
    100100  | TFun(ty, params, vararg, a) -> a
    101101  | TNamed(s, a) -> attributes_of_type env (unroll env t)
     
    111111  | TInt(ik, a) -> TInt(ik, f a)
    112112  | TFloat(fk, a) -> TFloat(fk, f a)
    113   | TPtr(ty, a) -> TPtr(ty, f a)
    114   | TArray(ty, sz, a) ->
    115       TArray(change_attributes_type env f ty, sz, a)
     113  | TPtr(sp, ty, a) -> TPtr(sp, ty, f a)
     114  | TArray(sp, ty, sz, a) ->
     115      TArray(sp, change_attributes_type env f ty, sz, a)
    116116  | TFun(ty, params, vararg, a) -> TFun(ty, params, vararg, f a)
    117117  | TNamed(s, a) ->
     
    167167    | TFloat(fk1, a1), TFloat(fk2, a2) ->
    168168        TFloat(comp_base fk1 fk2, comp_attr a1 a2)
    169     | TPtr(ty1, a1), TPtr(ty2, a2) ->
    170         TPtr(comp ty1 ty2, comp_attr a1 a2)
    171     | TArray(ty1, sz1, a1), TArray(ty2, sz2, a2) ->
    172         TArray(comp ty1 ty2, comp_array_size sz1 sz2, comp_attr a1 a2)
     169    | TPtr(sp1, ty1, a1), TPtr(sp2, ty2, a2) when sp1 = sp2 ->
     170        TPtr(sp1, comp ty1 ty2, comp_attr a1 a2)
     171    | TArray(sp1, ty1, sz1, a1), TArray(sp2, ty2, sz2, a2) when sp1 = sp2 ->
     172        TArray(sp1, comp ty1 ty2, comp_array_size sz1 sz2, comp_attr a1 a2)
    173173    | TFun(ty1, params1, vararg1, a1), TFun(ty2, params2, vararg2, a2) ->
    174174        let (params, vararg) =
     
    245245  | TInt(ik, _) -> Some(alignof_ikind ik)
    246246  | TFloat(fk, _) -> Some(alignof_fkind fk)
    247   | TPtr(_, _) -> Some(!config.alignof_ptr)
    248   | TArray(ty, _, _) -> alignof env ty
     247  | TPtr(_, _, _) -> Some(!config.alignof_ptr)
     248  | TArray(_, ty, _, _) -> alignof env ty
    249249  | TFun(_, _, _, _) -> !config.alignof_fun
    250250  | TNamed(_, _) -> alignof env (unroll env t)
     
    303303  | TInt(ik, _) -> Some(sizeof_ikind ik)
    304304  | TFloat(fk, _) -> Some(sizeof_fkind fk)
    305   | TPtr(_, _) -> Some(!config.sizeof_ptr)
    306   | TArray(ty, None, _) -> None
    307   | TArray(ty, Some n, _) as t' ->
     305  | TPtr(_, _, _) -> Some(!config.sizeof_ptr) (* FIXME *)
     306  | TArray(_, ty, None, _) -> None
     307  | TArray(_, ty, Some n, _) as t' ->
    308308      begin match sizeof env ty with
    309309      | None -> None
     
    344344let sizeof_struct env members =
    345345  let rec sizeof_rec ofs = function
    346   | [] | [ { fld_typ = TArray(_, None, _) } ] ->
     346  | [] | [ { fld_typ = TArray(_, _, None, _) } ] ->
    347347      (* C99: ty[] allowed as last field *)
    348348      begin match alignof_struct_union env members with
     
    473473let pointer_decay env t =
    474474  match unroll env t with
    475   | TArray(ty, _, _) -> TPtr(ty, [])
    476   | TFun _ as ty -> TPtr(ty, [])
     475  | TArray(sp, ty, _, _) -> TPtr(sp, ty, [])
     476  | TFun _ as ty -> TPtr(Code, ty, [])
    477477  | t -> t
    478478
     
    490490      end
    491491  (* Arrays and functions decay automatically to pointers *)
    492   | TArray(ty, _, _) -> TPtr(ty, [])
    493   | TFun _ as ty -> TPtr(ty, [])
     492  | TArray(sp, ty, _, _) -> TPtr(sp, ty, [])
     493  | TFun _ as ty -> TPtr(Code, ty, [])
    494494  (* Other types are not changed *)
    495495  | t -> t
     
    541541  (* Other types are not changed *)
    542542  match unroll env t with
    543   | TArray(ty, _, _) -> TPtr(ty, [])
    544   | TFun _ as ty -> TPtr(ty, [])
     543  | TArray(sp, ty, _, _) -> TPtr(sp, ty, [])
     544  | TFun _ as ty -> TPtr(Code, ty, [])
    545545  | _ -> t (* preserve typedefs *)
    546546
     
    585585  | CInt(_, ik, _) -> TInt(ik, [])
    586586  | CFloat(_, fk, _) -> TFloat(fk, [])
    587   | CStr _ -> TPtr(TInt(IChar, []), [])          (* XXX or array? const? *)
    588   | CWStr _ -> TPtr(TInt(wchar_ikind, []), [])   (* XXX or array? const? *)
     587  | CStr _ -> TPtr(Code, TInt(IChar, []), [])          (* XXX or array? const? *)
     588  | CWStr _ -> TPtr(Code, TInt(wchar_ikind, []), [])   (* XXX or array? const? *)
    589589  | CEnum(_, _) -> TInt(IInt, [])
    590590
     
    613613(* Check that an assignment is allowed *)
    614614
     615let valid_pointer_conv from tto =
     616  match from, tto with
     617  | Any, _
     618  | _, Any -> true
     619  | f, t -> f = t
     620
    615621let valid_assignment env from tto =
    616622  match pointer_decay env from.etyp, pointer_decay env tto with
    617623  | (TInt _ | TFloat _), (TInt _ | TFloat _) -> true
    618624  | TInt _, TPtr _ -> is_literal_0 from
    619   | TPtr(ty, _), TPtr(ty', _) ->
    620       incl_attributes (attributes_of_type env ty) (attributes_of_type env ty')
     625  | TPtr(sp, ty, _), TPtr(sp', ty', _) ->
     626      valid_pointer_conv sp sp'
     627      && incl_attributes (attributes_of_type env ty) (attributes_of_type env ty')
    621628      && (is_void_type env ty || is_void_type env ty'
    622629          || compatible_types env
     
    644651
    645652let intconst v ik =
    646   { edesc = EConst(CInt(v, ik, "")); etyp = TInt(ik, []) }
     653  { edesc = EConst(CInt(v, ik, "")); etyp = TInt(ik, []); espace = Code }
    647654
    648655(* Construct a float constant *)
    649656
    650657let floatconst v fk =
    651   { edesc = EConst(CFloat(v, fk, "")); etyp = TFloat(fk, []) }
     658  { edesc = EConst(CFloat(v, fk, "")); etyp = TFloat(fk, []); espace = Code }
    652659
    653660(* Construct the literal "0" with void * type *)
    654661
    655662let nullconst =
    656   { edesc = EConst(CInt(0L, ptr_t_ikind, "0")); etyp = TPtr(TVoid [], []) }
     663  { edesc = EConst(CInt(0L, ptr_t_ikind, "0")); etyp = TPtr(Any, TVoid [], []); espace = Code } (* XXX *)
    657664
    658665(* Construct a sequence *)
     
    668675
    669676let sassign loc lv rv =
    670   { sdesc = Sdo {edesc = EBinop(Oassign, lv, rv, lv.etyp); etyp = lv.etyp};
     677  { sdesc = Sdo {edesc = EBinop(Oassign, lv, rv, lv.etyp); etyp = lv.etyp; espace = lv.espace};
    671678    sloc = loc }
    672679
  • Deliverables/D2.3/8051-memoryspaces-branch/cparser/Elab.ml

    r453 r460  
    273273      | Some a -> add_attributes [a] (elab_attributes loc al)
    274274
     275let elab_attribute_space = function
     276  | ("data", []) -> Some Data
     277  | ("idata", []) -> Some IData
     278  | ("pdata", []) -> Some PData
     279  | ("xdata", []) -> Some XData
     280  | ("code", []) -> Some Code
     281  | _ -> None
     282
     283let rec elab_attributes_space loc attrs =
     284  let rec aux = function
     285    | [] -> None
     286    | h::t -> (match elab_attribute_space h with
     287                | None -> aux t
     288                | Some v -> Some (v,t))
     289  in match aux attrs with
     290    | None -> Any
     291    | Some (space, rest) ->
     292       (match aux rest with
     293         | None -> ()
     294         | Some _ -> warning loc "Multiple memory spaces given");
     295       space
     296
    275297(* Auxiliary for typespec elaboration *)
    276298
     
    291313let typespec_order t1 t2 = compare (typespec_rank t1) (typespec_rank t2)
    292314
     315
    293316(* Elaboration of a type specifier.  Returns 4-tuple:
    294317     (storage class, "inline" flag, elaborated type, new env)
     
    305328  and inline = ref false
    306329  and attr = ref []
    307   and tyspecs = ref [] in
     330  and tyspecs = ref []
     331  and space = ref Any in
    308332
    309333  let do_specifier = function
     
    317341      attr := add_attributes [a] !attr
    318342  | SpecAttr a ->
    319       attr := add_attributes (elab_attributes loc [a]) !attr
     343      attr := add_attributes (elab_attributes loc [a]) !attr;
     344      (match elab_attribute_space a with
     345        | None -> ()
     346        | Some sp ->
     347           if !space <> Any then
     348             error loc "multiple memory space specifiers";
     349           space := sp)
    320350  | SpecStorage st ->
    321351      if !sto <> Storage_default then
     
    333363  List.iter do_specifier specifier;
    334364
    335   let simple ty = (!sto, !inline, add_attributes_type !attr ty, env) in
     365  let simple ty = (!space, !sto, !inline, add_attributes_type !attr ty, env) in
    336366
    337367  (* Now interpret the list of type specifiers.  Much of this code
     
    397427          elab_struct_or_union only Struct loc id optmembers env in
    398428        let attr' = add_attributes !attr (elab_attributes loc a) in
    399         (!sto, !inline, TStruct(id', attr'), env')
     429        (!space, !sto, !inline, TStruct(id', attr'), env')
    400430
    401431    | [Cabs.Tunion(id, optmembers, a)] ->
     
    403433          elab_struct_or_union only Union loc id optmembers env in
    404434        let attr' = add_attributes !attr (elab_attributes loc a) in
    405         (!sto, !inline, TUnion(id', attr'), env')
     435        (!space, !sto, !inline, TUnion(id', attr'), env')
    406436
    407437    | [Cabs.Tenum(id, optmembers, a)] ->
     
    409439          elab_enum loc id optmembers env in
    410440        let attr' = add_attributes !attr (elab_attributes loc a) in
    411         (!sto, !inline, TInt(enum_ikind, attr'), env')
     441        (!space, !sto, !inline, TInt(enum_ikind, attr'), env')
    412442
    413443    | [Cabs.TtypeofE _] ->
     
    422452(* Elaboration of a type declarator.  *)
    423453
    424 and elab_type_declarator loc env ty = function
     454and elab_type_declarator loc env space ty = function
    425455  | Cabs.JUSTBASE ->
    426       (ty, env)
     456      (space, ty, env)
    427457  | Cabs.PARENTYPE(attr1, d, attr2) ->
    428458      (* XXX ignoring the distinction between attrs after and before *)
    429459      let a = elab_attributes loc (attr1 @ attr2) in
    430       elab_type_declarator loc env (add_attributes_type a ty) d
     460      (* XXX ought to use space from attrs? *)
     461      elab_type_declarator loc env space (add_attributes_type a ty) d
    431462  | Cabs.ARRAY(d, attr, sz) ->
    432463      let a = elab_attributes loc attr in
     
    443474                error loc "array size is not a compile-time constant";
    444475                Some 1L in (* produces better error messages later *)
    445        elab_type_declarator loc env (TArray(ty, sz', a)) d
     476       elab_type_declarator loc env space (TArray(space, ty, sz', a)) d
    446477  | Cabs.PTR(attr, d) ->
    447478      let a = elab_attributes loc attr in
    448        elab_type_declarator loc env (TPtr(ty, a)) d
     479      let space' = elab_attributes_space loc attr in
     480       elab_type_declarator loc env space' (TPtr(space, ty, a)) d
    449481  | Cabs.PROTO(d, params, vararg) ->
    450482       begin match unroll env ty with
     
    454486       end;
    455487       let params' = elab_parameters env params in
    456        elab_type_declarator loc env (TFun(ty, params', vararg, [])) d
     488       elab_type_declarator loc env space (TFun(ty, params', vararg, [])) d
    457489
    458490(* Elaboration of parameters in a prototype *)
     
    479511  (* replace array and function types by pointer types *)
    480512  let ty1 = argument_conversion env1 ty in
    481   let (id', env2) = Env.enter_ident env1 id sto ty1 in
     513  let (id', env2) = Env.enter_ident env1 id sto ty1 Any (* stack *) in
    482514  ( (id', ty1) , env2 )
    483515
     
    485517
    486518and elab_name env spec (id, decl, attr, loc) =
    487   let (sto, inl, bty, env') = elab_specifier loc env spec in
    488   let (ty, env'') = elab_type_declarator loc env' bty decl in
     519  let (space, sto, inl, bty, env') = elab_specifier loc env spec in
     520  let (_, ty, env'') = elab_type_declarator loc env' space bty decl in
    489521  let a = elab_attributes loc attr in
    490522  (id, sto, inl, add_attributes_type a ty, env'')
     
    493525
    494526and elab_name_group env (spec, namelist) =
    495   let (sto, inl, bty, env') =
     527  let (space, sto, inl, bty, env') =
    496528    elab_specifier (loc_of_namelist namelist) env spec in
    497529  let elab_one_name env (id, decl, attr, loc) =
    498     let (ty, env1) =
    499       elab_type_declarator loc env bty decl in
     530    let (_, ty, env1) =
     531      elab_type_declarator loc env space bty decl in
    500532    let a = elab_attributes loc attr in
    501533    ((id, sto, add_attributes_type a ty), env1) in
     
    505537
    506538and elab_init_name_group env (spec, namelist) =
    507   let (sto, inl, bty, env') =
     539  let (space, sto, inl, bty, env') =
    508540    elab_specifier (loc_of_init_name_list namelist) env spec in
    509541  let elab_one_name env ((id, decl, attr, loc), init) =
    510     let (ty, env1) =
    511       elab_type_declarator loc env bty decl in
     542    let (space', ty, env1) =
     543      elab_type_declarator loc env space bty decl in
    512544    let a = elab_attributes loc attr in
    513     ((id, sto, add_attributes_type a ty, init), env1) in
     545    ((space', id, sto, add_attributes_type a ty, init), env1) in
    514546  mmap elab_one_name env' namelist
    515547
     
    561593  let rec check_incomplete = function
    562594  | [] -> ()
    563   | [ { fld_typ = TArray(ty_elt, None, _) } ] when kind = Struct -> ()
     595  | [ { fld_typ = TArray(_, ty_elt, None, _) } ] when kind = Struct -> ()
    564596        (* C99: ty[] allowed as last field of a struct *)
    565597  | fld :: rem ->
     
    666698
    667699let elab_type loc env spec decl =
    668   let (sto, inl, bty, env') = elab_specifier loc env spec in
    669   let (ty, env'') = elab_type_declarator loc env' bty decl in
     700  let (space, sto, inl, bty, env') = elab_specifier loc env spec in
     701  let (_, ty, env'') = elab_type_declarator loc env' space bty decl in
    670702  if sto <> Storage_default || inl then
    671703    error loc "'extern', 'static', 'register' and 'inline' are meaningless in cast";
     
    673705
    674706
     707let join_spaces s1 s2 =
     708if s1 = s2 then s1 else Any
     709
     710
    675711
    676712(* Elaboration of expressions *)
     
    691727  | VARIABLE s ->
    692728      begin match wrap Env.lookup_ident loc env s with
    693       | (id, II_ident(sto, ty)) ->
    694           { edesc = EVar id; etyp = ty }
     729      | (id, II_ident(sto, ty, spc)) ->
     730          { edesc = EVar id; etyp = ty; espace=spc }
    695731      | (id, II_enum v) ->
    696           { edesc = EConst(CEnum(id, v)); etyp = TInt(enum_ikind, []) }
     732          { edesc = EConst(CEnum(id, v)); etyp = TInt(enum_ikind, []); espace = Code }
    697733      end
    698734
    699735  | CONSTANT cst ->
    700736      let cst' = elab_constant loc cst in
    701       { edesc = EConst cst'; etyp = type_of_constant cst' }
     737      { edesc = EConst cst'; etyp = type_of_constant cst'; espace = Code }
    702738
    703739  | PAREN e ->
     
    708744  | INDEX(a1, a2) ->            (* e1[e2] *)
    709745      let b1 = elab a1 in let b2 = elab a2 in
    710       let tres =
     746      let space, tres =
    711747        match (unroll env b1.etyp, unroll env b2.etyp) with
    712         | (TPtr(t, _) | TArray(t, _, _)), TInt _ -> t
    713         | TInt _, (TPtr(t, _) | TArray(t, _, _)) -> t
     748        | (TPtr(space, t, _) | TArray(space, t, _, _)), TInt _ -> space, t
     749        | TInt _, (TPtr(space, t, _) | TArray(space, t, _, _)) -> space, t
    714750        | t1, t2 -> error "incorrect types for array subscripting" in
    715       { edesc = EBinop(Oindex, b1, b2, TPtr(tres, [])); etyp = tres }
     751      { edesc = EBinop(Oindex, b1, b2, TPtr(space, tres, [])); etyp = tres; espace = space }
    716752
    717753  | MEMBEROF(a1, fieldname) ->
     
    727763      (* A field of a const/volatile struct or union is itself const/volatile *)
    728764      { edesc = EUnop(Odot fieldname, b1);
    729         etyp = add_attributes_type attrs fld.fld_typ }
     765        etyp = add_attributes_type attrs fld.fld_typ;
     766        espace = b1.espace }
    730767
    731768  | MEMBEROFPTR(a1, fieldname) ->
    732769      let b1 = elab a1 in
    733       let (fld, attrs) =
     770      let (space, fld, attrs) =
    734771        match unroll env b1.etyp with
    735         | TPtr(t, _) ->
     772        | TPtr(space, t, _) ->
    736773            begin match unroll env t with
    737774            | TStruct(id, attrs) ->
    738                 (wrap Env.find_struct_member loc env (id, fieldname), attrs)
     775                (space, wrap Env.find_struct_member loc env (id, fieldname), attrs)
    739776            | TUnion(id, attrs) ->
    740                 (wrap Env.find_union_member loc env (id, fieldname), attrs)
     777                (space, wrap Env.find_union_member loc env (id, fieldname), attrs)
    741778            | _ ->
    742779                error "left-hand side of '->' is not a pointer to a struct or union"
     
    745782            error "left-hand side of '->' is not a pointer " in
    746783      { edesc = EUnop(Oarrow fieldname, b1);
    747         etyp = add_attributes_type attrs fld.fld_typ }
     784        etyp = add_attributes_type attrs fld.fld_typ;
     785        espace = space }
    748786
    749787(* Hack to treat vararg.h functions the GCC way.  Helps with testing.
     
    758796      let b1 = elab a1 and b2 = elab a2 and b3 = elab a3 in
    759797      { edesc = ECall(b1, [b2; {edesc = EUnop(Oaddrof, b3);
    760                                 etyp = TPtr(b3.etyp, [])}]);
    761         etyp = TVoid [] }
     798                                etyp = TPtr(b3.espace, b3.etyp, []);
     799                                espace = Any }]);
     800        etyp = TVoid [];
     801        espace = Any (* XXX ? *) }
    762802  | CALL((VARIABLE "__builtin_va_arg" as a1),
    763803         [a2; (TYPE_SIZEOF _) as a3]) ->
    764804      let b1 = elab a1 and b2 = elab a2 and b3 = elab a3 in
    765805      let ty = match b3.edesc with ESizeof ty -> ty | _ -> assert false in
    766       { edesc = ECall(b1, [b2; b3]); etyp = ty }
     806      { edesc = ECall(b1, [b2; b3]); etyp = ty; espace = Any (* XXX ? *) }
    767807
    768808  | CALL(a1, al) ->
     
    775815            (* Emit an extern declaration for it *)
    776816            let id = Env.fresh_ident n in
    777             emit_elab (elab_loc loc) (Gdecl(Storage_extern, id, ty, None));
    778             { edesc = EVar id; etyp = ty }
     817            emit_elab (elab_loc loc) (Gdecl(Code, (Storage_extern, id, ty, None)));
     818            { edesc = EVar id; etyp = ty; espace = Any }
    779819        | _ -> elab a1 in
    780820      let bl = List.map elab al in
     
    783823        match unroll env b1.etyp with
    784824        | TFun(res, args, vararg, a) -> (res, args, vararg)
    785         | TPtr(ty, a) ->
     825        | TPtr(_, ty, a) ->
    786826            begin match unroll env ty with
    787827            | TFun(res, args, vararg, a) -> (res, args, vararg)
     
    795835        | None -> bl
    796836        | Some proto -> elab_arguments 1 bl proto vararg in
    797       { edesc = ECall(b1, bl'); etyp = res }
     837      { edesc = ECall(b1, bl'); etyp = res; espace = Any (* Stack *) }
    798838
    799839  | UNARY(POSINCR, a1) ->
     
    809849      if not (valid_cast env b1.etyp ty) then
    810850        err "illegal cast from %a@ to %a" Cprint.typ b1.etyp Cprint.typ ty;
    811       { edesc = ECast(ty, b1); etyp = ty }
     851      { edesc = ECast(ty, b1); etyp = ty; espace = b1.espace }
    812852
    813853  | CAST ((spec, dcl), _) ->
     
    816856  | EXPR_SIZEOF(CONSTANT(CONST_STRING s)) ->
    817857      let cst = CInt(Int64.of_int (String.length s), size_t_ikind, "") in
    818       { edesc = EConst cst; etyp = type_of_constant cst }
     858      { edesc = EConst cst; etyp = type_of_constant cst; espace = Code }
    819859
    820860  | EXPR_SIZEOF a1 ->
     
    822862      if sizeof env b1.etyp = None then
    823863        err "incomplete type %a" Cprint.typ b1.etyp;
    824       { edesc = ESizeof b1.etyp; etyp = TInt(size_t_ikind, []) }
     864      { edesc = ESizeof b1.etyp; etyp = TInt(size_t_ikind, []); espace = Code }
    825865
    826866  | TYPE_SIZEOF (spec, dcl) ->
     
    828868      if sizeof env ty = None then
    829869        err "incomplete type %a" Cprint.typ ty;
    830       { edesc = ESizeof ty; etyp = TInt(size_t_ikind, []) }
     870      { edesc = ESizeof ty; etyp = TInt(size_t_ikind, []); espace = Code }
    831871
    832872  | UNARY(PLUS, a1) ->
     
    834874      if not (is_arith_type env b1.etyp) then
    835875        error "argument of unary '+' is not an arithmetic type";
    836       { edesc = EUnop(Oplus, b1); etyp = unary_conversion env b1.etyp }
     876      { edesc = EUnop(Oplus, b1); etyp = unary_conversion env b1.etyp; espace = Any }
    837877
    838878  | UNARY(MINUS, a1) ->
     
    840880      if not (is_arith_type env b1.etyp) then
    841881        error "argument of unary '-' is not an arithmetic type";
    842       { edesc = EUnop(Ominus, b1); etyp = unary_conversion env b1.etyp }
     882      { edesc = EUnop(Ominus, b1); etyp = unary_conversion env b1.etyp; espace = Any }
    843883
    844884  | UNARY(BNOT, a1) ->
     
    846886      if not (is_integer_type env b1.etyp) then
    847887        error "argument of '~' is not an integer type";
    848       { edesc = EUnop(Onot, b1); etyp = unary_conversion env b1.etyp }
     888      { edesc = EUnop(Onot, b1); etyp = unary_conversion env b1.etyp; espace = Any }
    849889
    850890  | UNARY(NOT, a1) ->
     
    852892      if not (is_scalar_type env b1.etyp) then
    853893        error "argument of '!' is not a scalar type";
    854       { edesc = EUnop(Olognot, b1); etyp = TInt(IInt, []) }
     894      { edesc = EUnop(Olognot, b1); etyp = TInt(IInt, []); espace = Any }
    855895
    856896  | UNARY(ADDROF, a1) ->
     
    861901        if not (is_lvalue env b1) then err "argument of '&' is not a l-value"
    862902      end;
    863       { edesc = EUnop(Oaddrof, b1); etyp = TPtr(b1.etyp, []) }
     903      { edesc = EUnop(Oaddrof, b1); etyp = TPtr(b1.espace, b1.etyp, []); espace = Any }
    864904
    865905  | UNARY(MEMOF, a1) ->
     
    868908      (* '*' applied to a function type has no effect *)
    869909      | TFun _ -> b1
    870       | TPtr(ty, _) | TArray(ty, _, _) ->
    871           { edesc = EUnop(Oderef, b1); etyp = ty }
     910      | TPtr(space, ty, _) | TArray(space, ty, _, _) ->
     911          { edesc = EUnop(Oderef, b1); etyp = ty; espace = space }
    872912      | _ ->
    873913          error "argument of unary '*' is not a pointer"
     
    897937          binary_conversion env b1.etyp b2.etyp
    898938        else begin
    899           let (ty, attr) =
     939          let (space, ty, attr) =
    900940            match unroll env b1.etyp, unroll env b2.etyp with
    901             | (TPtr(ty, a) | TArray(ty, _, a)), TInt _ -> (ty, a)
    902             | TInt _, (TPtr(ty, a) | TArray(ty, _, a)) -> (ty, a)
     941            | (TPtr(space, ty, a) | TArray(space, ty, _, a)), TInt _ -> (space, ty, a)
     942            | TInt _, (TPtr(space, ty, a) | TArray(space, ty, _, a)) -> (space, ty, a)
    903943            | _, _ -> error "type error in binary '+'" in
    904944          if not (pointer_arithmetic_ok env ty) then
    905945            err "illegal pointer arithmetic in binary '+'";
    906           TPtr(ty, attr)
     946          TPtr(space, ty, attr)
    907947        end in
    908       { edesc = EBinop(Oadd, b1, b2, tyres); etyp = tyres }
     948      { edesc = EBinop(Oadd, b1, b2, tyres); etyp = tyres; espace = Any }
    909949
    910950  | BINARY(SUB, a1, a2) ->
     
    917957        end else begin
    918958          match unroll env b1.etyp, unroll env b2.etyp with
    919           | (TPtr(ty, a) | TArray(ty, _, a)), TInt _ ->
     959          | (TPtr(space, ty, a) | TArray(space, ty, _, a)), TInt _ ->
    920960              if not (pointer_arithmetic_ok env ty) then
    921961                err "illegal pointer arithmetic in binary '-'";
    922               (TPtr(ty, a), TPtr(ty, a))
    923           | TInt _, (TPtr(ty, a) | TArray(ty, _, a)) ->
     962              (TPtr(space, ty, a), TPtr(space, ty, a))
     963          | TInt _, (TPtr(space, ty, a) | TArray(space, ty, _, a)) ->
    924964              if not (pointer_arithmetic_ok env ty) then
    925965                err "illegal pointer arithmetic in binary '-'";
    926               (TPtr(ty, a), TPtr(ty, a))
    927           | (TPtr(ty1, a1) | TArray(ty1, _, a1)),
    928             (TPtr(ty2, a2) | TArray(ty2, _, a2)) ->
    929               if not (compatible_types ~noattrs:true env ty1 ty2) then
     966              (TPtr(space, ty, a), TPtr(space, ty, a))
     967          | (TPtr(space1, ty1, a1) | TArray(space1, ty1, _, a1)),
     968            (TPtr(space2, ty2, a2) | TArray(space2, ty2, _, a2)) ->
     969(* TODO: automatic cast on space mismatch? *)
     970              if not (compatible_types ~noattrs:true env ty1 ty2) || space1 != space2 then
    930971                err "mismatch between pointer types in binary '-'";
    931972              if not (pointer_arithmetic_ok env ty1) then
    932973                err "illegal pointer arithmetic in binary '-'";
    933               (TPtr(ty1, []), TInt(ptrdiff_t_ikind, []))
     974              (TPtr(space1, ty1, []), TInt(ptrdiff_t_ikind, []))
    934975          | _, _ -> error "type error in binary '-'"
    935976        end in
    936       { edesc = EBinop(Osub, b1, b2, tyop); etyp = tyres }
     977      { edesc = EBinop(Osub, b1, b2, tyop); etyp = tyres; espace = Any }
    937978
    938979  | BINARY(SHL, a1, a2) ->
     
    9741015      let b2 = elab a2 in
    9751016      let b3 = elab a3 in
     1017      let space = join_spaces b2.espace b3.espace in
    9761018      if not (is_scalar_type env b1.etyp) then
    9771019        err ("the first argument of '? :' is not a scalar type");
     
    9791021      | (TInt _ | TFloat _), (TInt _ | TFloat _) ->
    9801022          { edesc = EConditional(b1, b2, b3);
    981             etyp = binary_conversion env b2.etyp b3.etyp }
    982       | TPtr(ty1, a1), TPtr(ty2, a2) ->
     1023            etyp = binary_conversion env b2.etyp b3.etyp;
     1024            espace = space }
     1025      (* TODO: maybe we should automatically cast to a generic pointer when the spaces don't match? *)
     1026      | TPtr(sp1, ty1, a1), TPtr(sp2, ty2, a2) ->
    9831027          let tyres =
    984             if is_void_type env ty1 || is_void_type env ty2 then
    985               TPtr(TVoid [], add_attributes a1 a2)
     1028            if (is_void_type env ty1 || is_void_type env ty2) && sp1 = sp2 then
     1029              TPtr(sp1, TVoid [], add_attributes a1 a2)
    9861030            else
    9871031              match combine_types ~noattrs:true env
    988                                   (TPtr(ty1, a1)) (TPtr(ty2, a2)) with
     1032                                  (TPtr(sp1, ty1, a1)) (TPtr(sp2, ty2, a2)) with
    9891033              | None ->
    9901034                  error "the second and third arguments of '? :' \
     
    9921036              | Some ty -> ty
    9931037            in
    994           { edesc = EConditional(b1, b2, b3); etyp = tyres }
    995       | TPtr(ty1, a1), TInt _ when is_literal_0 b3 ->
    996           { edesc = EConditional(b1, b2, nullconst); etyp = TPtr(ty1, a1) }
    997       | TInt _, TPtr(ty2, a2) when is_literal_0 b2 ->
    998           { edesc = EConditional(b1, nullconst, b3); etyp = TPtr(ty2, a2) }
     1038          { edesc = EConditional(b1, b2, b3); etyp = tyres; espace = space }
     1039      | TPtr(sp1, ty1, a1), TInt _ when is_literal_0 b3 ->
     1040          { edesc = EConditional(b1, b2, nullconst); etyp = TPtr(sp1, ty1, a1); espace = space }
     1041      | TInt _, TPtr(sp2, ty2, a2) when is_literal_0 b2 ->
     1042          { edesc = EConditional(b1, nullconst, b3); etyp = TPtr(sp2, ty2, a2); espace = space }
    9991043      | ty1, ty2 ->
    10001044          match combine_types env ty1 ty2 with
     
    10021046              error ("the second and third arguments of '? :' have incompatible types")
    10031047          | Some tyres ->
    1004               { edesc = EConditional(b1, b2, b3); etyp = tyres }
     1048              { edesc = EConditional(b1, b2, b3); etyp = tyres; espace = space }
    10051049      end
    10061050
     
    10221066                  Cprint.typ b2.etyp Cprint.typ b1.etyp;
    10231067      end;
    1024       { edesc = EBinop(Oassign, b1, b2, b1.etyp); etyp = b1.etyp }
     1068      { edesc = EBinop(Oassign, b1, b2, b1.etyp); etyp = b1.etyp; espace = b1.espace }
    10251069
    10261070  | BINARY((ADD_ASSIGN | SUB_ASSIGN | MUL_ASSIGN | DIV_ASSIGN | MOD_ASSIGN
     
    10541098                      Cprint.typ ty Cprint.typ b1.etyp;
    10551099          end;
    1056           { edesc = EBinop(top, b1, b2, ty); etyp = b1.etyp }
     1100          { edesc = EBinop(top, b1, b2, ty); etyp = b1.etyp; espace = b1.espace }
    10571101      | _ -> assert false
    10581102      end
     
    10671111      | a :: l ->
    10681112          let b = elab a in
    1069           elab_comma { edesc = EBinop(Ocomma, accu, b, b.etyp); etyp = b.etyp } l
     1113          elab_comma { edesc = EBinop(Ocomma, accu, b, b.etyp); etyp = b.etyp; espace = b.espace } l
    10701114      in elab_comma (elab a1) al
    10711115
     
    11031147      if not (is_scalar_type env b1.etyp) then
    11041148        err "the argument of %s must be an arithmetic or pointer type" msg;
    1105       { edesc = EUnop(op, b1); etyp = b1.etyp }
     1149      { edesc = EUnop(op, b1); etyp = b1.etyp; espace = b1.espace }
    11061150
    11071151(* Elaboration of binary operators over integers *)
     
    11141158        error "the second argument of '%s' is not an integer type" msg;
    11151159      let tyres = binary_conversion env b1.etyp b2.etyp in
    1116       { edesc = EBinop(op, b1, b2, tyres); etyp = tyres }
     1160      { edesc = EBinop(op, b1, b2, tyres); etyp = tyres; espace = Any }
    11171161
    11181162(* Elaboration of binary operators over arithmetic types *)
     
    11251169        error "the second argument of '%s' is not an arithmetic type" msg;
    11261170      let tyres = binary_conversion env b1.etyp b2.etyp in
    1127       { edesc = EBinop(op, b1, b2, tyres); etyp = tyres }
     1171      { edesc = EBinop(op, b1, b2, tyres); etyp = tyres; espace = Any }
    11281172
    11291173(* Elaboration of shift operators *)
     
    11361180        error "the second argument of '%s' is not an integer type" msg;
    11371181      let tyres = unary_conversion env b1.etyp in
    1138       { edesc = EBinop(op, b1, b2, tyres); etyp = tyres }
     1182      { edesc = EBinop(op, b1, b2, tyres); etyp = tyres; espace = Any }
    11391183
    11401184(* Elaboration of comparisons *)
     
    11461190        | (TInt _ | TFloat _), (TInt _ | TFloat _) ->
    11471191            EBinop(op, b1, b2, binary_conversion env b1.etyp b2.etyp)
    1148         | TInt _, TPtr(ty, _) when is_literal_0 b1 ->
    1149             EBinop(op, nullconst, b2, TPtr(ty, []))
    1150         | TPtr(ty, _), TInt _ when is_literal_0 b2 ->
    1151             EBinop(op, b1, nullconst, TPtr(ty, []))
    1152         | TPtr(ty1, _), TPtr(ty2, _)
     1192        | TInt _, TPtr(sp, ty, _) when is_literal_0 b1 ->
     1193            EBinop(op, nullconst, b2, TPtr(sp, ty, []))
     1194        | TPtr(sp, ty, _), TInt _ when is_literal_0 b2 ->
     1195            EBinop(op, b1, nullconst, TPtr(sp, ty, []))
     1196        | TPtr(sp1, ty1, _), TPtr(sp2, ty2, _)
    11531197          when is_void_type env ty1 ->
    1154             EBinop(op, b1, b2, TPtr(ty2, []))
    1155         | TPtr(ty1, _), TPtr(ty2, _)
     1198            EBinop(op, b1, b2, TPtr(sp2, ty2, []))  (* XXX sp1? *)
     1199        | TPtr(sp1, ty1, _), TPtr(sp2, ty2, _)
    11561200          when is_void_type env ty2 ->
    1157             EBinop(op, b1, b2, TPtr(ty1, []))
    1158         | TPtr(ty1, _), TPtr(ty2, _) ->
     1201            EBinop(op, b1, b2, TPtr(sp1, ty1, []))  (* XXX sp2? *)
     1202        | TPtr(sp1, ty1, _), TPtr(sp2, ty2, _) ->
    11591203            if not (compatible_types ~noattrs:true env ty1 ty2) then
    11601204              warning "comparison between incompatible pointer types";
    1161             EBinop(op, b1, b2, TPtr(ty1, []))
    1162         | TPtr _, TInt _
    1163         | TInt _, TPtr _ ->
     1205            EBinop(op, b1, b2, TPtr(sp1, ty1, []))  (* XXX sp1? *)
     1206        | TPtr (sp,_,_), TInt _
     1207        | TInt _, TPtr (sp,_,_) ->
    11641208            warning "comparison between integer and pointer";
    1165             EBinop(op, b1, b2, TPtr(TVoid [], []))
     1209            EBinop(op, b1, b2, TPtr(sp,TVoid [], []))
    11661210        | ty1, ty2 ->
    11671211            error "illegal comparison between types@ %a@ and %a"
    11681212                  Cprint.typ b1.etyp Cprint.typ b2.etyp in
    1169       { edesc = resdesc; etyp = TInt(IInt, []) }
     1213      { edesc = resdesc; etyp = TInt(IInt, []); espace = Any }
    11701214
    11711215(* Elaboration of && and || *)
     
    11771221      if not (is_scalar_type env b2.etyp) then
    11781222        err "the second argument of '%s' is not a scalar type" msg;
    1179       { edesc = EBinop(op, b1, b2, TInt(IInt, [])); etyp = TInt(IInt, []) }
     1223      { edesc = EBinop(op, b1, b2, TInt(IInt, [])); etyp = TInt(IInt, []); espace = Any }
    11801224
    11811225(* Type-checking of function arguments *)
     
    12761320let rec elab_init loc env ty ile =
    12771321  match unroll env ty with
    1278   | TArray(ty_elt, opt_sz, _) ->
     1322  | TArray(space, ty_elt, opt_sz, _) ->
    12791323      let rec elab_init_array n accu rem =
    12801324        match opt_sz, rem with
     
    13951439let fixup_typ env ty init =
    13961440  match unroll env ty, init with
    1397   | TArray(ty_elt, None, attr), Init_array il ->
    1398       TArray(ty_elt, Some(Int64.of_int(List.length il)), attr)
     1441  | TArray(space, ty_elt, None, attr), Init_array il ->
     1442      TArray(space, ty_elt, Some(Int64.of_int(List.length il)), attr)
    13991443  | _ -> ty
    14001444
     
    14221466  env'
    14231467
    1424 let enter_or_refine_ident local loc env s sto ty =
     1468let enter_or_refine_ident local loc env s sto ty space =
    14251469  match redef Env.lookup_ident env s with
    1426   | Some(id, II_ident(old_sto, old_ty)) ->
     1470  | Some(id, II_ident(old_sto, old_ty, old_space)) ->
    14271471      let new_ty =
    14281472        if local then begin
     
    14431487          sto
    14441488        end in
    1445       (id, Env.add_ident env id new_sto new_ty)
     1489      let new_space = join_spaces old_space space (* XXX: incompatible? *) in
     1490      (id, Env.add_ident env id new_sto new_ty new_space)
    14461491  | Some(id, II_enum v) ->
    14471492      error loc "illegal redefinition of enumerator '%s'" s;
    1448       (id, Env.add_ident env id sto ty)
     1493      (id, Env.add_ident env id sto ty space)
    14491494  | _ ->
    1450       Env.enter_ident env s sto ty
     1495      Env.enter_ident env s sto ty space
    14511496
    14521497let rec enter_decdefs local loc env = function
    14531498  | [] ->
    14541499      ([], env)
    1455   | (s, sto, ty, init) :: rem ->
     1500  | (space, s, sto, ty, init) :: rem ->
    14561501      (* Sanity checks on storage class *)
    14571502      begin match sto with
     
    14681513      (* enter ident in environment with declared type, because
    14691514         initializer can refer to the ident *)
    1470       let (id, env1) = enter_or_refine_ident local loc env s sto' ty in
     1515      let (id, env1) = enter_or_refine_ident local loc env s sto' ty space in
    14711516      (* process the initializer *)
    14721517      let (ty', init') = elab_initializer loc env1 ty init in
    14731518      (* update environment with refined type *)
    1474       let env2 = Env.add_ident env1 id sto' ty' in
     1519      let env2 = Env.add_ident env1 id sto' ty' space in
    14751520      (* check for incomplete type *)
    14761521      if sto' <> Storage_extern && incomplete_type env ty' then
     
    14821527      end else begin
    14831528        (* Global definition *)
    1484         emit_elab (elab_loc loc) (Gdecl(sto, id, ty', init'));
     1529        emit_elab (elab_loc loc) (Gdecl(space, (sto, id, ty', init')));
    14851530        enter_decdefs local loc env2 rem
    14861531      end
     
    15021547    | _ -> fatal_error loc1 "wrong type for function definition" in
    15031548  (* Enter function in the environment, for recursive references *)
    1504   let (fun_id, env1) = enter_or_refine_ident false loc1 env s sto ty in
     1549  let (fun_id, env1) = enter_or_refine_ident false loc1 env s sto ty Code in
    15051550  (* Enter parameters in the environment *)
    15061551  let env2 =
    1507     List.fold_left (fun e (id, ty) -> Env.add_ident e id Storage_default ty)
     1552    List.fold_left (fun e (id, ty) -> Env.add_ident e id Storage_default ty Any)
    15081553                   (Env.new_scope env1) params in
    15091554  (* Elaborate function body *)
     
    15441589  (* "struct s { ...};" or "union u;" *)
    15451590  | ONLYTYPEDEF(spec, loc) ->
    1546       let (sto, inl, ty, env') = elab_specifier ~only:true loc env spec in
     1591      let (space, sto, inl, ty, env') = elab_specifier ~only:true loc env spec in
    15471592      if sto <> Storage_default || inl then
    15481593        error loc "Non-default storage or 'inline' on 'struct' or 'union' declaration";
  • Deliverables/D2.3/8051-memoryspaces-branch/cparser/Env.ml

    r453 r460  
    7171
    7272type ident_info =
    73   | II_ident of storage * typ
     73  | II_ident of storage * typ * memory_space
    7474  | II_enum of int64                    (* value of the enum *)
    7575
     
    202202(* Inserting things by source name, with generation of a translated name *)
    203203
    204 let enter_ident env s sto ty =
     204let enter_ident env s sto ty sp =
    205205  let id = fresh_ident s in
    206206  (id,
    207    { env with env_ident = IdentMap.add id (II_ident(sto, ty)) env.env_ident })
     207   { env with env_ident = IdentMap.add id (II_ident(sto, ty, sp)) env.env_ident })
    208208
    209209let enter_composite env s ci =
     
    221221(* Inserting things by translated name *)
    222222
    223 let add_ident env id sto ty =
    224   { env with env_ident = IdentMap.add id (II_ident(sto, ty)) env.env_ident }
     223let add_ident env id sto ty sp =
     224  { env with env_ident = IdentMap.add id (II_ident(sto, ty, sp)) env.env_ident }
    225225
    226226let add_composite env id ci =
  • Deliverables/D2.3/8051-memoryspaces-branch/cparser/Env.mli

    r453 r460  
    3232}
    3333
    34 type ident_info = II_ident of C.storage * C.typ | II_enum of int64
     34type ident_info = II_ident of C.storage * C.typ * C.memory_space | II_enum of int64
    3535
    3636type typedef_info = C.typ
     
    6161val find_typedef : t -> C.ident -> typedef_info
    6262
    63 val enter_ident : t -> string -> C.storage -> C.typ -> C.ident * t
     63val enter_ident : t -> string -> C.storage -> C.typ -> C.memory_space -> C.ident * t
    6464val enter_composite : t -> string -> composite_info -> C.ident * t
    6565val enter_enum_item : t -> string -> int64 -> C.ident * t
    6666val enter_typedef : t -> string -> typedef_info -> C.ident * t
    6767
    68 val add_ident : t -> C.ident -> C.storage -> C.typ -> t
     68val add_ident : t -> C.ident -> C.storage -> C.typ -> C.memory_space -> t
    6969val add_composite : t -> C.ident -> composite_info -> t
    7070val add_typedef : t -> C.ident -> typedef_info -> t
  • Deliverables/D2.3/8051-memoryspaces-branch/cparser/GCC.ml

    r453 r460  
    3131let doubleType = TFloat(FDouble, [])
    3232let longDoubleType = TFloat (FLongDouble, [])
    33 let voidPtrType = TPtr(TVoid [], [])
    34 let voidConstPtrType = TPtr(TVoid [AConst], [])
    35 let charPtrType = TPtr(TInt(IChar, []), [])
    36 let charConstPtrType = TPtr(TInt(IChar, [AConst]), [])
    37 let intPtrType = TPtr(TInt(IInt, []), [])
     33let voidPtrType = TPtr(Any,TVoid [], [])
     34let voidConstPtrType = TPtr(Any,TVoid [AConst], [])
     35let charPtrType = TPtr(Any,TInt(IChar, []), [])
     36let charConstPtrType = TPtr(Any,TInt(IChar, [AConst]), [])
     37let intPtrType = TPtr(Any,TInt(IInt, []), [])
    3838let sizeType = TInt(size_t_ikind, [])
    3939
     
    151151
    152152  "__builtin_modff",  (floatType, [ floatType;
    153                                           TPtr(floatType,[]) ], false);
     153                                          TPtr(Any,floatType,[]) ], false);
    154154  "__builtin_modfl",  (longDoubleType, [ longDoubleType;
    155                                                TPtr(longDoubleType, []) ],
     155                                               TPtr(Any,longDoubleType, []) ],
    156156                             false);
    157157
  • Deliverables/D2.3/8051-memoryspaces-branch/cparser/Lexer.mll

    r453 r460  
    182182      ("__builtin_offsetof", fun loc -> BUILTIN_OFFSETOF loc);
    183183      (* On some versions of GCC __thread is a regular identifier *)
    184       ("__thread", fun loc -> THREAD loc)
     184      ("__thread", fun loc -> THREAD loc);
     185      (* 8051 memory space extensions *)
     186      ("__data", fun loc -> DATA loc);
     187      ("__idata", fun loc -> IDATA loc);
     188      ("__pdata", fun loc -> PDATA loc);
     189      ("__xdata", fun loc -> XDATA loc);
     190      ("__code", fun loc -> CODE loc);
    185191    ]
    186192
  • Deliverables/D2.3/8051-memoryspaces-branch/cparser/Parser.mly

    r453 r460  
    221221%token<Cabs.cabsloc> VOLATILE EXTERN STATIC CONST RESTRICT AUTO REGISTER
    222222%token<Cabs.cabsloc> THREAD
     223
     224%token<Cabs.cabsloc> DATA IDATA PDATA XDATA CODE
    223225
    224226%token<Cabs.cabsloc> SIZEOF ALIGNOF
     
    12501252                                        /* ISO 6.7.3 */
    12511253|   THREAD                              { ("__thread",[]), $1 }
     1254
     1255|   DATA                                { ("data",[]), $1 }
     1256|   IDATA                               { ("idata",[]), $1 }
     1257|   PDATA                               { ("pdata",[]), $1 }
     1258|   XDATA                               { ("xdata",[]), $1 }
     1259|   CODE                                { ("code",[]), $1 }
    12521260;
    12531261
  • Deliverables/D2.3/8051-memoryspaces-branch/cparser/Rename.ml

    r453 r460  
    7676
    7777let rec typ env = function
    78   | TPtr(ty, a) -> TPtr(typ env ty, a)
    79   | TArray(ty, sz, a) -> TArray(typ env ty, sz, a)
     78  | TPtr(sp, ty, a) -> TPtr(sp, typ env ty, a)
     79  | TArray(sp, ty, sz, a) -> TArray(sp, typ env ty, sz, a)
    8080  | TFun(res, None, va, a) -> TFun(typ env res, None, va, a)
    8181  | TFun(res, Some p, va, a) ->
     
    9898
    9999let rec exp env e =
    100   { edesc = exp_desc env e.edesc; etyp = typ env e.etyp }
     100  { edesc = exp_desc env e.edesc; etyp = typ env e.etyp; espace = e.espace }
    101101
    102102and exp_desc env = function
     
    192192
    193193and globdecl_desc env = function
    194   | Gdecl d ->
     194  | Gdecl (sp,d) ->
    195195      let (d', env') = decl env d in
    196       (Gdecl d', env')
     196      (Gdecl (sp,d'), env')
    197197  | Gfundef fd ->
    198198      let (fd', env') = fundef env fd in
     
    231231      let env' =
    232232        match dcl.gdesc with
    233         | Gdecl(sto, id, _, _) ->
     233        | Gdecl (_, (sto, id, _, _)) ->
    234234            begin match sto with
    235235            | Storage_default | Storage_extern -> enter_global env id
  • Deliverables/D2.3/8051-memoryspaces-branch/cparser/SimplExpr.ml

    r453 r460  
    9393  let eboolvalof e =
    9494    { edesc = EBinop(One, e, intconst 0L IInt, TInt(IInt, []));
    95       etyp = TInt(IInt, []) } in
     95      etyp = TInt(IInt, []);
     96      espace = Any } in
    9697
    9798  let sseq s1 s2 = Cutil.sseq loc s1 s2 in
    9899
    99100  let sassign e1 e2 =
    100     { sdesc = Sdo {edesc = EBinop(Oassign, e1, e2, e1.etyp); etyp = e1.etyp};
     101    { sdesc = Sdo {edesc = EBinop(Oassign, e1, e2, e1.etyp); etyp = e1.etyp; espace = e1.espace};
    101102      sloc = loc } in
    102103
     
    150151        | Ominus | Oplus | Olognot | Onot | Oderef | Oarrow _ ->
    151152            let (s1, e1') = simpl e1 RHS in
    152             finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp}
     153            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp; espace = e.espace}
    153154
    154155        | Oaddrof ->
    155156            let (s1, e1') = simpl e1 LHS in
    156             finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp}
     157            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp; espace = e.espace}
    157158
    158159        | Odot _ ->
    159160            let (s1, e1') = simpl e1 (if act = LHS then LHS else RHS) in
    160             finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp}
     161            finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp; espace = e.espace}
    161162
    162163        | Opreincr | Opredecr ->
     
    166167            let ty = unary_conversion env e.etyp in
    167168            let e3 =
    168               {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty} in
     169              {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty; espace = Any} in
    169170            begin match act with
    170171            | Drop ->
     
    185186                let (s2, e2') = lhs_to_rhs e1' in
    186187                let e3 =
    187                   {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty} in
     188                  {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty; espace = Any} in
    188189                (sseq s1 (sseq s2 (sassign e1' e3)), voidconst)
    189190            | _ ->
    190191                let tmp = new_temp e.etyp in
    191192                let e3 =
    192                   {edesc = EBinop(op', tmp, intconst 1L IInt, ty); etyp = ty} in
     193                  {edesc = EBinop(op', tmp, intconst 1L IInt, ty); etyp = ty; espace = Any} in
    193194                finish act (sseq s1 (sseq (sassign tmp e1') (sassign e1' e3)))
    194195                       tmp
     
    206207            let (s2, e2') = simpl e2 RHS in
    207208            finish act (sseq s1 s2)
    208                        {edesc = EBinop(op, e1', e2', ty); etyp = e.etyp}
     209                       {edesc = EBinop(op, e1', e2', ty); etyp = e.etyp; espace = Any}
    209210
    210211        | Oassign ->
     
    240241              | _ -> assert false in
    241242            let e3 =
    242               { edesc = EBinop(op', e11', e2', ty); etyp = ty } in
     243              { edesc = EBinop(op', e11', e2', ty); etyp = ty; espace = Any } in
    243244            begin match act with
    244245            | Drop ->
     
    260261            if is_simpl_expr e2 then begin
    261262              finish act s1
    262                      {edesc = EBinop(Ologand, e1', e2, ty); etyp = e.etyp}
     263                     {edesc = EBinop(Ologand, e1', e2, ty); etyp = e.etyp; espace = e.espace}
    263264            end else begin
    264265              match act with
     
    285286            if is_simpl_expr e2 then begin
    286287              finish act s1
    287                      {edesc = EBinop(Ologor, e1', e2, ty); etyp = e.etyp}
     288                     {edesc = EBinop(Ologor, e1', e2, ty); etyp = e.etyp; espace = e.espace}
    288289            end else begin
    289290              match act with
     
    311312        let (s1, e1') = simpl e1 RHS in
    312313        if is_simpl_expr e2 && is_simpl_expr e3 then begin
    313           finish act s1 {edesc = EConditional(e1', e2, e3); etyp = e.etyp}
     314          finish act s1 {edesc = EConditional(e1', e2, e3); etyp = e.etyp; espace = e.espace}
    314315        end else begin
    315316          match act with
     
    337338        end else begin
    338339          let (s1, e1') = simpl e1 RHS in
    339           finish act s1 {edesc = ECast(ty, e1'); etyp = e.etyp}
     340          finish act s1 {edesc = ECast(ty, e1'); etyp = e.etyp; espace = e.espace}
    340341        end
    341342
     
    343344        let (s1, e1') = simpl e1 RHS in
    344345        let (s2, el') = simpl_list el in
    345         let e2 = { edesc = ECall(e1', el'); etyp = e.etyp } in
     346        let e2 = { edesc = ECall(e1', el'); etyp = e.etyp; espace = e.espace } in
    346347        begin match act with
    347348        | Drop ->
     
    482483        let s_init =
    483484          {sdesc = Sdo {edesc = EBinop(Oassign, tmp, intconst 1L IInt, tmp.etyp);
    484                         etyp = tmp.etyp};
     485                        etyp = tmp.etyp; espace = tmp.espace};
    485486           sloc = s.sloc} in
    486487        {sdesc = Sfor(s_init, tmp, s', simpl_stmt s1); sloc = s.sloc}
  • Deliverables/D2.3/8051-memoryspaces-branch/cparser/StructAssign.ml

    r453 r460  
    2929
    3030let memcpy_type =
    31   TFun(TPtr(TVoid [], []),
    32        Some [(Env.fresh_ident "", TPtr(TVoid [], []));
    33              (Env.fresh_ident "", TPtr(TVoid [AConst], []));
     31  TFun(TPtr(Any,TVoid [], []),
     32       Some [(Env.fresh_ident "", TPtr(Any,TVoid [], []));
     33             (Env.fresh_ident "", TPtr(Any,TVoid [AConst], []));
    3434             (Env.fresh_ident "", TInt(size_t_ikind, []))],
    3535       false, [])
     
    4343  | Some id ->
    4444      id
     45
     46let space_of_ty = function
     47| TArray(space, _, _, _)
     48| TPtr(space, _, _) -> space
     49| _ -> Any
    4550
    4651let transf_assign env loc lhs rhs =
     
    6368    | TUnion(id, attr) ->
    6469        raise Exit
    65     | TArray(ty_elt, Some sz, attr) ->
    66         transf_array l r ty_elt 0L sz
    67     | TArray(ty_elt, None, attr) ->
     70    | TArray(space, ty_elt, Some sz, attr) ->
     71        transf_array space l (space_of_ty (unroll env r.etyp)) r ty_elt 0L sz
     72    | TArray(space, ty_elt, None, attr) ->
    6873        error "%a: Error: array of unknown size" formatloc loc;
    6974        sskip                           (* will be ignored later *)
     
    7479    | [] -> sskip
    7580    | f :: fl ->
    76         sseq loc (transf {edesc = EUnop(Odot f.fld_name, l); etyp = f.fld_typ}
    77                          {edesc = EUnop(Odot f.fld_name, r); etyp = f.fld_typ})
     81        sseq loc (transf {edesc = EUnop(Odot f.fld_name, l); etyp = f.fld_typ; espace = l.espace}
     82                         {edesc = EUnop(Odot f.fld_name, r); etyp = f.fld_typ; espace = r.espace})
    7883                 (transf_struct l r fl)
    7984
    80   and transf_array l r ty idx sz =
     85  and transf_array lsp l rsp r ty idx sz =
    8186    if idx >= sz then sskip else begin
    8287      let e = intconst idx size_t_ikind in
    83       sseq loc (transf {edesc = EBinop(Oindex, l, e, ty); etyp = ty}
    84                        {edesc = EBinop(Oindex, r, e, ty); etyp = ty})
    85                (transf_array l r ty (Int64.add idx 1L) sz)
     88      sseq loc (transf {edesc = EBinop(Oindex, l, e, ty); etyp = ty; espace = lsp}
     89                       {edesc = EBinop(Oindex, r, e, ty); etyp = ty; espace = rsp})
     90               (transf_array lsp l rsp r ty (Int64.add idx 1L) sz)
    8691    end
    8792  in
     
    9095    transf lhs rhs
    9196  with Exit ->
    92     let memcpy = {edesc = EVar(memcpy_ident()); etyp = memcpy_type} in
    93     let e_lhs = {edesc = EUnop(Oaddrof, lhs); etyp = TPtr(lhs.etyp, [])} in
    94     let e_rhs = {edesc = EUnop(Oaddrof, rhs); etyp = TPtr(rhs.etyp, [])} in
    95     let e_size = {edesc = ESizeof(lhs.etyp); etyp = TInt(size_t_ikind, [])} in
     97    let memcpy = {edesc = EVar(memcpy_ident()); etyp = memcpy_type; espace = Any} in
     98    (* XXX: casts required? *)
     99    let e_lhs = {edesc = EUnop(Oaddrof, lhs); etyp = TPtr(Any, lhs.etyp, []); espace = Any} in
     100    let e_rhs = {edesc = EUnop(Oaddrof, rhs); etyp = TPtr(Any, rhs.etyp, []); espace = Any} in
     101    let e_size = {edesc = ESizeof(lhs.etyp); etyp = TInt(size_t_ikind, []); espace = Any} in
    96102    {sdesc = Sdo {edesc = ECall(memcpy, [e_lhs; e_rhs; e_size]);
    97                   etyp = TVoid[]};
     103                  etyp = TVoid[]; espace = Any};
    98104     sloc = loc}
    99105
     
    137143  | None -> p'
    138144  | Some id ->
    139       {gdesc = Gdecl(Storage_extern, id, memcpy_type, None); gloc = no_loc}
     145      {gdesc = Gdecl(Code, (Storage_extern, id, memcpy_type, None)); gloc = no_loc}
    140146      :: p'
    141147
  • Deliverables/D2.3/8051-memoryspaces-branch/cparser/StructByValue.ml

    r453 r460  
    3939      if is_composite_type env tres then begin
    4040        let res = Env.fresh_ident "_res" in
    41         TFun(TVoid [], Some((res, TPtr(tres', [])) :: args'), vararg, attr)
     41        TFun(TVoid [], Some((res, TPtr(Any, tres', [])) :: args'), vararg, attr)
    4242      end else
    4343        TFun(tres', Some args', vararg, attr)
    44   | TPtr(t1, attr) ->
     44  | TPtr(sp, t1, attr) ->
    4545      let t1' = transf_type env t1 in
    46       if t1' = t1 then t else TPtr(transf_type env t1, attr)
    47   | TArray(t1, sz, attr) ->
     46      if t1' = t1 then t else TPtr(sp, transf_type env t1, attr)
     47  | TArray(sp, t1, sz, attr) ->
    4848      let t1' = transf_type env t1 in
    49       if t1' = t1 then t else TArray(transf_type env t1, sz, attr)
     49      if t1' = t1 then t else TArray(sp, transf_type env t1, sz, attr)
    5050  | _ -> t
    5151
     
    5353  let t = transf_type env t in
    5454  if is_composite_type env t
    55   then (id, TPtr(add_attributes_type [AConst] t, []))
     55  then (id, TPtr(Any, add_attributes_type [AConst] t, []))
    5656  else (id, t)
    5757
     
    6161let rec transf_expr env e =
    6262  { etyp = transf_type env e.etyp;
     63    espace = e.espace;
    6364    edesc = match e.edesc with
    6465      | EConst c -> EConst c
     
    105106  let e' = transf_expr e in
    106107  if is_composite_type env e'.etyp
    107   then {edesc = EUnop(Oaddrof, e'); etyp = TPtr(e'.etyp, [])}
     108  then {edesc = EUnop(Oaddrof, e'); etyp = TPtr(Any, e'.etyp, []); espace = Any} (* XXX: this might require a cast? *)
    108109  else e'
    109110in
     
    119120  match s.sdesc with
    120121  | Sskip -> s
    121   | Sdo {edesc = ECall(fn, args); etyp = ty} ->
     122  | Sdo {edesc = ECall(fn, args); etyp = ty; espace = space} ->
    122123      let fn = transf_expr fn in
    123124      let args = List.map transf_arg args in
    124125      if is_composite_type env ty then begin
    125126        let tmp = new_temp ~name:"_res" ty in
    126         let arg0 = {edesc = EUnop(Oaddrof, tmp); etyp = TPtr(ty, [])} in
    127         {s with sdesc = Sdo {edesc = ECall(fn, arg0 :: args); etyp = TVoid []}}
     127        let arg0 = {edesc = EUnop(Oaddrof, tmp); etyp = TPtr(Any, ty, []); espace = Any} in
     128        {s with sdesc = Sdo {edesc = ECall(fn, arg0 :: args); etyp = TVoid []; espace = Any}}
    128129      end else
    129         {s with sdesc = Sdo {edesc = ECall(fn, args); etyp = ty}}
    130   | Sdo {edesc = EBinop(Oassign, dst, {edesc = ECall(fn, args); etyp = ty}, _)} ->
     130        {s with sdesc = Sdo {edesc = ECall(fn, args); etyp = ty; espace = space}}
     131  | Sdo {edesc = EBinop(Oassign, dst, {edesc = ECall(fn, args); etyp = ty; espace = space}, _)} ->
    131132      let dst = transf_expr dst in
    132133      let fn = transf_expr fn in
     
    134135      let ty = transf_type ty in
    135136      if is_composite_type env ty then begin
    136         let arg0 = {edesc = EUnop(Oaddrof, dst); etyp = TPtr(dst.etyp, [])} in
    137         {s with sdesc = Sdo {edesc = ECall(fn, arg0 :: args); etyp = TVoid []}}
     137        let arg0 = {edesc = EUnop(Oaddrof, dst); etyp = TPtr(Any, dst.etyp, []); espace = Any} in
     138        {s with sdesc = Sdo {edesc = ECall(fn, arg0 :: args); etyp = TVoid []; espace = Any}}
    138139      end else
    139         sassign s.sloc dst {edesc = ECall(fn, args); etyp = ty}
     140        sassign s.sloc dst {edesc = ECall(fn, args); etyp = ty; espace = space}
    140141  | Sdo e ->
    141142      {s with sdesc = Sdo(transf_expr e)}
     
    185186      if is_composite_type env ty then begin
    186187        let id' = Env.fresh_ident id.name in
    187         let ty' = TPtr(add_attributes_type [AConst] ty, []) in
     188        let ty' = TPtr(Any, add_attributes_type [AConst] ty, []) in
    188189        let (params', decls, init) = transf_prm params in
    189190        ((id', ty') :: params',
    190191         (Storage_default, id, ty, None) :: decls,
    191192         sseq loc
    192           (sassign loc {edesc = EVar id; etyp = ty}
    193                        {edesc = EUnop(Oderef, {edesc = EVar id'; etyp = ty'});
    194                         etyp = ty})
     193          (sassign loc {edesc = EVar id; etyp = ty; espace = Any}
     194                       {edesc = EUnop(Oderef, {edesc = EVar id'; etyp = ty'; espace = Any});
     195                        etyp = ty;
     196                        espace = Any})
    195197          init)
    196198      end else begin
     
    207209    if is_composite_type env ret then begin
    208210      let vres = Env.fresh_ident "_res" in
    209       let tres = TPtr(ret, []) in
    210       let eres = {edesc = EVar vres; etyp = tres} in
    211       let eeres = {edesc = EUnop(Oderef, eres); etyp = ret} in
     211      let tres = TPtr(Any, ret, []) in
     212      let eres = {edesc = EVar vres; etyp = tres; espace = Any} in
     213      let eeres = {edesc = EUnop(Oderef, eres); etyp = ret; espace = Any} in
    212214      (TVoid [],
    213215       (vres, tres) :: params,
  • Deliverables/D2.3/8051-memoryspaces-branch/cparser/Transform.ml

    r453 r460  
    3434let new_temp ?(name = "t") ty =
    3535  let id = new_temp_var ~name ty in
    36   { edesc = EVar id; etyp = ty }
     36  { edesc = EVar id; etyp = ty; espace = Any (* Always stack allocated? *) }
    3737
    3838let get_temps () =
     
    5959      let (desc', env') =
    6060        match g.gdesc with
    61         | Gdecl((sto, id, ty, init) as d) ->
    62            (Gdecl(decl env d), Env.add_ident env id sto ty)
     61        | Gdecl (sp, ((sto, id, ty, init) as d)) ->
     62           (Gdecl(sp, decl env d), Env.add_ident env id sto ty sp)
    6363        | Gfundef f ->
    6464           (Gfundef(fundef env f),
    65             Env.add_ident env f.fd_name f.fd_storage (fundef_typ f))
     65            Env.add_ident env f.fd_name f.fd_storage (fundef_typ f) Code)
    6666        | Gcompositedecl(su, id) ->
    6767            (Gcompositedecl(su, id),
  • Deliverables/D2.3/8051-memoryspaces-branch/cparser/Unblock.ml

    r453 r460  
    3333  | Init_single e ->
    3434      sdoseq loc
    35         { edesc = EBinop(Oassign, path, e, path.etyp); etyp = path.etyp }
     35        { edesc = EBinop(Oassign, path, e, path.etyp); etyp = path.etyp; espace = path.espace }
    3636        k
    3737  | Init_array il ->
    38       let ty_elt =
     38      let space, ty_elt =
    3939        match unroll env path.etyp with
    40         | TArray(ty_elt, _, _) -> ty_elt
     40        | TArray(space, ty_elt, _, _) -> space, ty_elt
    4141        | _ -> fatal_error "%aWrong type for array initializer"
    4242                           formatloc loc in
     
    4545        | i :: il ->
    4646            local_initializer loc env
    47               { edesc = EBinop(Oindex, path, intconst pos IInt, TPtr(ty_elt, []));
    48                 etyp = ty_elt }
     47              { edesc = EBinop(Oindex, path, intconst pos IInt, TPtr(space, ty_elt, []));
     48                etyp = ty_elt;
     49                espace = Any }
    4950              i
    5051              (array_init (Int64.succ pos) il) in
     
    5354      let field_init (fld, i) k =
    5455        local_initializer loc env
    55           { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ }
     56          { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ; espace = Any }
    5657          i k in
    5758      List.fold_right field_init fil k
    5859  | Init_union(id, fld, i) ->
    5960      local_initializer loc env
    60         { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ }
     61        { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ; espace = Any }
    6162        i k
    6263
     
    8384  | None -> k
    8485  | Some init ->
    85       local_initializer loc env { edesc = EVar id; etyp = ty' } init k
     86      local_initializer loc env { edesc = EVar id; etyp = ty'; espace = Any } init k
    8687
    8788(* Simplification of blocks within a statement *)
  • Deliverables/D2.3/8051-memoryspaces-branch/myocamlbuild_config.ml

    r453 r460  
    1 let parser_lib = "/home/ayache/Work/Source/CerCo/experiments/compiler/branches/8051/lib"
     1let parser_lib = "/home/bacam/workspace/uni/cerco/prototype/lib"
  • Deliverables/D2.3/8051-memoryspaces-branch/src/acc.ml

    r453 r460  
    3434  let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in
    3535    Languages.save filename final_ast;
     36    if Options.is_matita_output_enabled () then
     37      Languages.save_matita filename (input_ast :: target_asts);
    3638    (if Options.annotation_requested () then
    3739       let annotated_input_ast = Languages.annotate input_ast final_ast in
  • Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clight.mli

    r453 r460  
    77
    88(** ** Types *)
     9
     10type memory_space = Any | Data | IData | PData | XData | Code
    911
    1012(** Clight types are similar to those of C.  They include numeric types,
     
    6264  | Tint of intsize*signedness                  (**r integer types *)
    6365  | Tfloat of floatsize                         (**r floating-point types *)
    64   | Tpointer of ctype                           (**r pointer types ([*ty]) *)
    65   | Tarray of ctype*int                         (**r array types ([ty[len]]) *)
     66  | Tpointer of memory_space * ctype            (**r pointer types ([*ty]) *)
     67  | Tarray of memory_space * ctype*int          (**r array types ([ty[len]]) *)
    6668  | Tfunction of ctype list*ctype               (**r function types *)
    6769  | Tstruct of ident*(ident*ctype) list
     
    201203  prog_funct: (ident * fundef) list ;
    202204  prog_main: ident option;
    203   prog_vars: ((ident * init_data list) * ctype) list
     205  prog_vars: (((ident * init_data list) * memory_space) * ctype) list
    204206}
  • Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightAnnotator.ml

    r453 r460  
    254254let cost_decl cost_id =
    255255  let init = [Clight.Init_int32 0] in
    256   ((cost_id, init), int_typ)
     256  (((cost_id, init), Clight.Any), int_typ)
    257257
    258258(* This is the definition of the increment cost function. *)
  • Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightFromC.ml

    r453 r460  
    2020  | Tfloat F64 -> 8
    2121  | Tpointer _ -> 4
    22   | Tarray (t',n) -> alignof t'
     22  | Tarray (_,t',n) -> alignof t'
    2323  | Tfunction (_,_) -> 1
    2424  | Tstruct (_,fld) -> alignof_fields fld
     
    4343    | Tfloat F64 -> 8
    4444    | Tpointer _ -> 4
    45     | Tarray (t',n) -> sizeof t' * max 1 n
     45    | Tarray (_,t',n) -> sizeof t' * max 1 n
    4646    | Tfunction (_,_) -> 1
    4747    | Tstruct (_,fld) -> align (max 1 (sizeof_struct fld 0)) (alignof t)
     
    103103      (env, (C.Storage_static,
    104104             Env.fresh_ident name,
    105              C.TPtr(C.TInt(C.IChar,[C.AConst]),[]),
     105             C.TPtr(C.Any,C.TInt(C.IChar,[C.AConst]),[]),
    106106             None));
    107107    !define_stringlit_hook id;
     
    110110
    111111let typeStringLiteral s =
    112   Tarray(Tint(I8, Unsigned), String.length s + 1)
     112  Tarray(Code, Tint(I8, Unsigned), String.length s + 1)
    113113
    114114let global_for_string s id =
     
    120120  add_char '\000';
    121121  for i = String.length s - 1 downto 0 do add_char s.[i] done;
    122   ((id, !init), typeStringLiteral s)
     122  (((id, !init), Code), typeStringLiteral s)
    123123
    124124let globals_for_strings globs =
     
    144144      | [] -> []
    145145      | Tfloat(_)::tl -> Tfloat(F64)::(types_of_types tl)
    146       | _::tl -> Tpointer(Tvoid)::(types_of_types tl) in
     146      | _::tl -> Tpointer(Any,Tvoid)::(types_of_types tl) in
    147147    let stub_type = Tfunction (types_of_types targs, tres) in
    148148    Hashtbl.add stub_function_table stub_name stub_type;
     
    194194      F64
    195195
     196let convertSpace = function
     197  | C.Any -> Any
     198  | C.Data -> Data
     199  | C.IData -> IData
     200  | C.PData -> PData
     201  | C.XData -> XData
     202  | C.Code -> Code
     203
    196204let convertTyp env t =
    197205
     
    203211    | C.TFloat(fk, a) ->
    204212        Tfloat(convertFkind fk)
    205     | C.TPtr(C.TStruct(id, _), _) when List.mem id seen ->
     213    | C.TPtr(_,C.TStruct(id, _), _) when List.mem id seen ->
    206214        Tcomp_ptr("struct " ^ id.name)
    207     | C.TPtr(C.TUnion(id, _), _) when List.mem id seen ->
     215    | C.TPtr(_,C.TUnion(id, _), _) when List.mem id seen ->
    208216        Tcomp_ptr("union " ^ id.name)
    209     | C.TPtr(ty, a) ->
    210         Tpointer(convertTyp seen ty)
    211     | C.TArray(ty, None, a) ->
     217    | C.TPtr(sp,ty, a) ->
     218        Tpointer(convertSpace sp, convertTyp seen ty)
     219    | C.TArray(sp, ty, None, a) ->
    212220        (* Cparser verified that the type ty[] occurs only in
    213221           contexts that are safe for Clight, so just treat as ty[0]. *)
    214222        (* warning "array type of unspecified size"; *)
    215         Tarray(convertTyp seen ty, 0)
    216     | C.TArray(ty, Some sz, a) ->
    217         Tarray(convertTyp seen ty, convertInt sz )
     223        Tarray(convertSpace sp, convertTyp seen ty, 0)
     224    | C.TArray(sp, ty, Some sz, a) ->
     225        Tarray(convertSpace sp, convertTyp seen ty, convertInt sz )
    218226    | C.TFun(tres, targs, va, a) ->
    219227        if va then unsupported "variadic function type";
     
    299307      let ty1 =
    300308        match typeof e1' with
    301         | Tpointer t -> t
     309        | Tpointer (_,t) -> t
    302310        | _ -> error ("wrong type for ->" ^ id ^ " access"); Tvoid in
    303311      Expr(Efield(Expr(Ederef(convertExpr env e1), ty1),
     
    316324  | C.EBinop(C.Oindex, e1, e2, _) ->
    317325      Expr(Ederef(Expr(Ebinop(Oadd, convertExpr env e1, convertExpr env e2),
    318                        Tpointer ty)), ty)
     326                       convertTyp env e1.etyp)), ty)
    319327  | C.EBinop(C.Ologand, e1, e2, _) ->
    320328      Expr(Eandbool(convertExpr env e1, convertExpr env e2), ty)
     
    355363  match Cutil.unroll env ty with
    356364  | TFun(res, args, vararg, attr) -> Some(res, vararg)
    357   | TPtr(ty', attr) -> projFunType env ty'
     365  | TPtr(_, ty', attr) -> projFunType env ty'
    358366  | _ -> None
    359367
     
    401409  | Tfloat F64 -> ("float64", ty)
    402410  | Tpointer _ | Tarray _ | Tfunction _ | Tcomp_ptr _ ->
    403       ("pointer", Tpointer Tvoid)
     411      ("pointer", Tpointer (Any, Tvoid)) (* XXX: what is the pointer is to a different space? *)
    404412  | _ ->
    405413      unsupported "operation on volatile struct or union"; ("", Tvoid)
     
    408416  let (suffix, ty') = volatile_fun_suffix_type ty in
    409417  Expr(Evar( ("__builtin_volatile_read_" ^ suffix)),
    410        Tfunction((Tpointer Tvoid)::[], ty'))
     418       Tfunction((Tpointer (Any,Tvoid))::[], ty'))
    411419
    412420let volatile_write_fun ty =
    413421  let (suffix, ty') = volatile_fun_suffix_type ty in
    414422  Expr(Evar( ("__builtin_volatile_write_" ^ suffix)),
    415        Tfunction((Tpointer Tvoid)::(ty'::[]), Tvoid))
     423       Tfunction((Tpointer (Any,Tvoid))::(ty'::[]), Tvoid))
    416424
    417425(* Toplevel expression, argument of an Sdo *)
     
    433441          Scall(Some lhs',
    434442                volatile_read_fun (typeof rhs'),
    435                 [ Expr (Eaddrof rhs', Tpointer (typeof rhs')) ])
     443                [ Expr (Eaddrof rhs', Tpointer (Any (* XXX ? *), typeof rhs')) ])
    436444      | true, false ->                  (* volatile write *)
    437445          Scall(None,
    438446                volatile_write_fun (typeof lhs'),
    439                 [ Expr(Eaddrof lhs', Tpointer (typeof lhs')); rhs' ])
     447                [ Expr(Eaddrof lhs', Tpointer (Any (* XXX ? *), typeof lhs')); rhs' ])
    440448      | false, false ->                 (* regular assignment *)
    441449          Sassign(convertExpr env lhs, convertExpr env rhs)
     
    664672      let ty_elt =
    665673        match Cutil.unroll env ty with
    666         | C.TArray(t, _, _) -> t
     674        | C.TArray(_, t, _, _) -> t
    667675        | _ -> error "array type expected in initializer"; C.TVoid [] in
    668676      List.iter (cvtInit ty_elt) il
     
    691699(** Global variable *)
    692700
    693 let convertGlobvar env (sto, id, ty, optinit as decl) =
     701let convertGlobvar env space (sto, id, ty, optinit as decl) =
    694702  let id' =  id.name in
    695703  let ty' = convertTyp env ty in
     
    702710  Hashtbl.add decl_atom id' (env, decl);
    703711  !define_variable_hook id' decl;
    704   ((id', init'), ty')
     712  (((id', init'), convertSpace space), ty')
    705713
    706714(** Convert a list of global declarations.
     
    715723      updateLoc g.gloc;
    716724      match g.gdesc with
    717       | C.Gdecl((sto, id, ty, optinit) as d) ->
     725      | C.Gdecl(space, ((sto, id, ty, optinit) as d)) ->
    718726          (* Prototyped functions become external declarations.
    719727             Variadic functions are skipped.
     
    728736              convertGlobdecls env funs vars gl'
    729737          | _ ->
    730               convertGlobdecls env funs (convertGlobvar env d :: vars) gl'
     738              convertGlobdecls env funs (convertGlobvar env space d :: vars) gl'
    731739          end
    732740      | C.Gfundef fd ->
     
    770778        updateLoc g.gloc;
    771779        match g.gdesc with
    772         | C.Gdecl(sto, id, ty, None) ->
     780        | C.Gdecl(_, (sto, id, ty, None)) ->
    773781            if IdentSet.mem id defs
    774782            then clean defs accu gl
    775783            else clean (IdentSet.add id defs) (g :: accu) gl
    776         | C.Gdecl(_, id, ty, _) ->
     784        | C.Gdecl(_, (_, id, ty, _)) ->
    777785            if IdentSet.mem id defs then
    778786              error ("multiple definitions of " ^ id.name);
     
    818826  if List.mem C.AConst a then true else
    819827  match Cutil.unroll env t with
    820   | C.TArray(t', _, _) -> type_is_readonly env t'
     828  | C.TArray(_, t', _, _) -> type_is_readonly env t'
    821829  | _ -> false
    822830
     
    856864  typedefs = [
    857865    (* keeps GCC-specific headers happy, harmless for others *)
    858     "__builtin_va_list", C.TPtr(C.TVoid [], [])
     866    "__builtin_va_list", C.TPtr(C.Any, C.TVoid [], [])
    859867  ];
    860868  functions = [
    861869    (* The volatile read/volatile write functions *)
    862870    "__builtin_volatile_read_int8unsigned",
    863         (TInt(IUChar, []), [TPtr(TVoid [], [])], false);
     871        (TInt(IUChar, []), [TPtr(C.Any, TVoid [], [])], false);
    864872    "__builtin_volatile_read_int8signed",
    865         (TInt(ISChar, []), [TPtr(TVoid [], [])], false);
     873        (TInt(ISChar, []), [TPtr(C.Any, TVoid [], [])], false);
    866874    "__builtin_volatile_read_int16unsigned",
    867         (TInt(IUShort, []), [TPtr(TVoid [], [])], false);
     875        (TInt(IUShort, []), [TPtr(C.Any, TVoid [], [])], false);
    868876    "__builtin_volatile_read_int16signed",
    869         (TInt(IShort, []), [TPtr(TVoid [], [])], false);
     877        (TInt(IShort, []), [TPtr(C.Any, TVoid [], [])], false);
    870878    "__builtin_volatile_read_int32",
    871         (TInt(IInt, []), [TPtr(TVoid [], [])], false);
     879        (TInt(IInt, []), [TPtr(C.Any, TVoid [], [])], false);
    872880    "__builtin_volatile_read_float32",
    873         (TFloat(FFloat, []), [TPtr(TVoid [], [])], false);
     881        (TFloat(FFloat, []), [TPtr(C.Any, TVoid [], [])], false);
    874882    "__builtin_volatile_read_float64",
    875          (TFloat(FDouble, []), [TPtr(TVoid [], [])], false);
     883         (TFloat(FDouble, []), [TPtr(C.Any, TVoid [], [])], false);
    876884    "__builtin_volatile_read_pointer",
    877          (TPtr(TVoid [], []), [TPtr(TVoid [], [])], false);
     885         (TPtr(C.Any, TVoid [], []), [TPtr(C.Any, TVoid [], [])], false);
    878886    "__builtin_volatile_write_int8unsigned",
    879         (TVoid [], [TPtr(TVoid [], []); TInt(IUChar, [])], false);
     887        (TVoid [], [TPtr(C.Any, TVoid [], []); TInt(IUChar, [])], false);
    880888    "__builtin_volatile_write_int8signed",
    881         (TVoid [], [TPtr(TVoid [], []); TInt(ISChar, [])], false);
     889        (TVoid [], [TPtr(C.Any, TVoid [], []); TInt(ISChar, [])], false);
    882890    "__builtin_volatile_write_int16unsigned",
    883         (TVoid [], [TPtr(TVoid [], []); TInt(IUShort, [])], false);
     891        (TVoid [], [TPtr(C.Any, TVoid [], []); TInt(IUShort, [])], false);
    884892    "__builtin_volatile_write_int16signed",
    885         (TVoid [], [TPtr(TVoid [], []); TInt(IShort, [])], false);
     893        (TVoid [], [TPtr(C.Any, TVoid [], []); TInt(IShort, [])], false);
    886894    "__builtin_volatile_write_int32",
    887         (TVoid [], [TPtr(TVoid [], []); TInt(IInt, [])], false);
     895        (TVoid [], [TPtr(C.Any, TVoid [], []); TInt(IInt, [])], false);
    888896    "__builtin_volatile_write_float32",
    889         (TVoid [], [TPtr(TVoid [], []); TFloat(FFloat, [])], false);
     897        (TVoid [], [TPtr(C.Any, TVoid [], []); TFloat(FFloat, [])], false);
    890898    "__builtin_volatile_write_float64",
    891          (TVoid [], [TPtr(TVoid [], []); TFloat(FDouble, [])], false);
     899         (TVoid [], [TPtr(C.Any, TVoid [], []); TFloat(FDouble, [])], false);
    892900    "__builtin_volatile_write_pointer",
    893          (TVoid [], [TPtr(TVoid [], []); TPtr(TVoid [], [])], false)
     901         (TVoid [], [TPtr(C.Any, TVoid [], []); TPtr(C.Any, TVoid [], [])], false)
    894902  ]
    895903}
  • Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightInterpret.ml

    r453 r460  
    3434  | Tfloat _            -> assert false (* Not supported *)
    3535  | Tpointer _          -> Mem.ptr_size
    36   | Tarray (t,s)        -> s*(sizeof t)                   
     36  | Tarray (_,t,s)      -> s*(sizeof t)                   
    3737  | Tfunction (_,_)     -> assert false (* Not supported *)
    3838  | Tstruct (_,lst)     ->
     
    5656  | Tfloat _            -> assert false (* Not supported *)
    5757  | Tpointer _          -> Mem.mq_of_ptr
    58   | Tarray (c,s)        -> Mem.mq_of_ptr
     58  | Tarray (_,c,s)      -> Mem.mq_of_ptr
    5959  | Tfunction (_,_)     -> assert false (* Not supported *)
    6060  | Tstruct (_,_)       -> Mem.mq_of_ptr
     
    187187  | _ -> false
    188188let is_pointer_type = function
    189   | Tpointer _ | Tarray (_,_) | Tstruct (_,_)
     189  | Tpointer _ | Tarray _ | Tstruct (_,_)
    190190  | Tunion (_,_) | Tcomp_ptr _ -> true
    191191  | _ -> false
     
    203203  (* Cast float*)
    204204  | (v,_,Tfloat _)                              -> assert false(*Not supported*)
    205   (* Cast pointeur *)
    206   | (v,Tarray(_,_),Tpointer _)                  -> v
    207   | (v,Tpointer _,Tarray(_,_))                  -> v
     205  (* Cast pointeur FIXME: ignores memory spaces *)
     206  | (v,Tarray _,Tpointer _)                     -> v
     207  | (v,Tpointer _,Tarray _)                     -> v
    208208  | (v,Tpointer _,Tpointer _)                   -> v
    209   | (v,Tarray (_,_),Tarray(_,_))                -> v
     209  | (v,Tarray _,Tarray _)                       -> v
    210210  (*Struct and pointer to struct FIXME: is it correct ?*)
    211   | (v,Tstruct(a,b),Tpointer (Tstruct(c,d))) when a=c && b=d -> v
    212   | (v,Tpointer (Tstruct(a,b)),Tstruct(c,d)) when a=c && b=d -> v
     211  | (v,Tstruct(a,b),Tpointer (_,Tstruct(c,d))) when a=c && b=d -> v
     212  | (v,Tpointer (_,Tstruct(a,b)),Tstruct(c,d)) when a=c && b=d -> v
    213213  (*Union and pointer to union FIXME: is it correct ?*)
    214   | (v,Tunion(a,b),Tpointer (Tunion(c,d))) when a=c && b=d -> v
    215   | (v,Tpointer (Tunion(a,b)),Tunion(c,d)) when a=c && b=d -> v
     214  | (v,Tunion(a,b),Tpointer (_,Tunion(c,d))) when a=c && b=d -> v
     215  | (v,Tpointer (_,Tunion(a,b)),Tunion(c,d)) when a=c && b=d -> v
    216216  (* error *)
    217217  | (e,_,_)                                     ->
     
    226226
    227227let get_subtype = function
    228   | Tarray(t,_) -> t
    229   | Tpointer t -> t
     228  | Tarray(_,t,_) -> t
     229  | Tpointer (_,t) -> t
    230230  | _ -> assert false (*Misuse of get_subtype*)
    231231
     
    481481
    482482let is_struct = function
    483   | Tarray (_,_) | Tunion (_,_) | Tstruct (_,_) -> true
     483  | Tarray _ | Tunion (_,_) | Tstruct (_,_) -> true
    484484  | _ -> false
    485485
     
    641641  | Init_addrof (_,_)   -> assert false (*FIXME what is this ?*)
    642642
    643 let alloc_datas m ((_,lst),ty) =
     643(* FIXME: ignores memory space *)
     644let alloc_datas m (((_,lst),_),ty) =
    644645  let store_data (m,ptr) = function (*FIXME signed ?*)
    645646    | Init_int8  i -> (Mem.store m Memory.MQ_int8signed ptr (Value.of_int i)
     
    661662    Valtbl.add f (Value.of_int (-i-1)) fct;
    662663    (g,f)
     664  (* FIXME: ignores memory space *)
    663665  and alloc_var (m,g) v =
    664666    let (m',ptr) = alloc_datas m v in
     
    666668        let (m2,ptr2) = Mem.alloc m' (Mem.ptr_size) in
    667669        let m3 = Mem.store m2 Mem.mq_of_ptr ptr2 ptr in
    668         Hashtbl.add g (fst (fst v)) ptr2;(m3,g)
     670        Hashtbl.add g (fst (fst (fst v))) ptr2;(m3,g)
    669671      else
    670         ( (Hashtbl.add g (fst (fst v)) ptr);(m',g) )
     672        ( (Hashtbl.add g (fst (fst (fst v))) ptr);(m',g) )
    671673  in let (m,g) =
    672674    List.fold_left alloc_var (Mem.empty,Hashtbl.create 13) prog.prog_vars
  • Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightPrinter.ml

    r453 r460  
    1919open AST
    2020open Clight
     21
     22let name_space = function
     23  | Any -> ""
     24  | Data -> "__data "
     25  | IData -> "__idata "
     26  | PData -> "__pdata "
     27  | XData -> "__xdata "
     28  | Code -> "__code "
     29
    2130
    2231let name_unop = function
     
    7887  if String.length id > 0 && id.[0] = '*' then "(" ^ id ^ ")" else id
    7988
    80 let rec name_cdecl id ty =
     89(* Use Any for the space when nothing should appear. *)
     90
     91let rec name_cdecl sp id ty =
     92  let ssp = name_space sp in
    8193  match ty with
    8294  | Tvoid ->
    83       "void" ^ name_optid id
     95      ssp ^ "void" ^ name_optid id
    8496  | Tint(sz, sg) ->
    85       name_inttype sz sg ^ name_optid id
     97      ssp ^ name_inttype sz sg ^ name_optid id
    8698  | Tfloat sz ->
    87       name_floattype sz ^ name_optid id
    88   | Tpointer t ->
    89       name_cdecl ("*" ^ id) t
    90   | Tarray(t, n) ->
     99      ssp ^ name_floattype sz ^ name_optid id
     100  | Tpointer (sp',t) ->
     101      name_cdecl sp' ("* " ^ ssp ^ id) t
     102  | Tarray(sp', t, n) ->
     103      if sp <> sp' then eprintf "Array %s has wrong memory space.\n%!" id;
    91104      name_cdecl
     105        sp'
    92106        (sprintf "%s[%ld]" (parenthesize_if_pointer id) (Int32.of_int n))
    93107        t
    94108  | Tfunction(args, res) ->
    95109      let b = Buffer.create 20 in
     110      Buffer.add_string b ssp;
    96111      if id = ""
    97112      then Buffer.add_string b "(*)"
     
    106121          | t1::tl ->
    107122              if not first then Buffer.add_string b ", ";
    108               Buffer.add_string b (name_cdecl "" t1);
     123              Buffer.add_string b (name_cdecl Any "" t1);
    109124              add_args false tl in
    110125          add_args true args
    111126      end;
    112127      Buffer.add_char b ')';
    113       name_cdecl (Buffer.contents b) res
     128      name_cdecl Any (Buffer.contents b) res
    114129  | Tstruct(name, fld) ->
    115       name ^ name_optid id
     130      ssp ^ name ^ name_optid id
    116131  | Tunion(name, fld) ->
    117       name ^ name_optid id
     132      ssp ^ name ^ name_optid id
    118133  | Tcomp_ptr name ->
    119       name ^ " *" ^ id
     134      ssp ^ name ^ " *" ^ id
    120135
    121136(* Type *)
    122137
    123 let name_type ty = name_cdecl "" ty
     138let name_type ty = name_cdecl Any "" ty
    124139
    125140(* Expressions *)
     
    322337      | (id, ty) :: rem ->
    323338          if not first then Buffer.add_string b ", ";
    324           Buffer.add_string b (name_cdecl id ty);
     339          Buffer.add_string b (name_cdecl Any id ty);
    325340          add_params false rem in
    326341      add_params true params
     
    331346let print_function p id f =
    332347  fprintf p "%s@ "
    333             (name_cdecl (name_function_parameters id f.fn_params)
     348            (name_cdecl Any
     349                        (name_function_parameters id f.fn_params)
    334350                        f.fn_return);
    335351  fprintf p "@[<v 2>{@ ";
    336352  List.iter
    337353    (fun ((id, ty)) ->
    338       fprintf p "%s;@ " (name_cdecl id ty))
     354      fprintf p "%s;@ " (name_cdecl Any id ty))
    339355    f.fn_vars;
    340356  print_stmt p f.fn_body;
     
    345361  | External(_, args, res) ->
    346362      fprintf p "extern %s;@ @ "
    347                 (name_cdecl id (Tfunction(args, res)))
     363                (name_cdecl Any id (Tfunction(args, res)))
    348364  | Internal f ->
    349365      print_function p id f
     
    393409let re_string_literal = Str.regexp "__stringlit_[0-9]+"
    394410
    395 let print_globvar p (((id, init), ty)) =
     411let print_globvar p ((((id, init), sp), ty)) =
    396412  match init with
    397413  | [] ->
    398414      fprintf p "extern %s;@ @ "
    399               (name_cdecl id ty)
     415              (name_cdecl sp id ty)
    400416  | [Init_space _] ->
    401417      fprintf p "%s;@ @ "
    402               (name_cdecl id ty)
     418              (name_cdecl sp id ty)
    403419  | [init] ->
    404420      fprintf p "@[<hov 2>%s = %a;@]@ @ "
    405               (name_cdecl id ty) print_init1 init
     421              (name_cdecl sp id ty) print_init1 init
    406422  | _ ->
    407423      fprintf p "@[<hov 2>%s = "
    408               (name_cdecl id ty);
     424              (name_cdecl sp id ty);
    409425      if Str.string_match re_string_literal id 0
    410426      && List.for_all (function Init_int8 _ -> true | _ -> false) init
     
    424440  | Tint(sz, sg) -> ()
    425441  | Tfloat sz -> ()
    426   | Tpointer t -> collect_type t
    427   | Tarray(t, n) -> collect_type t
     442  | Tpointer (_,t) -> collect_type t
     443  | Tarray(_, t, n) -> collect_type t
    428444  | Tfunction(args, res) -> collect_type_list args; collect_type res
    429445  | Tstruct(id, fld) -> register_struct_union id fld; collect_fields fld
     
    512528  | [] -> ()
    513529  | (id, ty)::rem ->
    514       fprintf p "@ %s;" (name_cdecl id ty);
     530      fprintf p "@ %s;" (name_cdecl Any id ty);
    515531      print_fields rem in
    516532  print_fields fld;
  • Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightToCminor.ml

    r453 r460  
    2626  | Tvoid       -> Type_void
    2727  | Tfloat _    -> Type_ret Sig_float (*Not supported*)
    28   | Tpointer _ | Tarray (_,_) | Tstruct (_,_) | Tunion (_,_) -> Type_ret Sig_ptr
     28  | Tpointer _ | Tarray _ | Tstruct (_,_) | Tunion (_,_) -> Type_ret Sig_ptr
    2929  | _           -> Type_ret Sig_int
    3030
     
    3333      Sig_float (*Not supported but needed for external function from library*)
    3434  | Tvoid       -> assert false
    35   | Tpointer _ | Tstruct (_,_) | Tunion (_,_) | Tarray(_,_) -> Sig_ptr
     35  | Tpointer _ | Tstruct (_,_) | Tunion (_,_) | Tarray _ -> Sig_ptr
    3636  | _           -> Sig_int
    3737
     
    4646  | Tint (I32,Signed)   -> Memory.MQ_int32
    4747  | Tint (I32,Unsigned) -> assert false (*FIXME why not int32unsigned exists ?*)
    48   | Tpointer _ | Tarray (_,_) | Tstruct (_,_) | Tunion (_,_) -> ptr_mq
     48  | Tpointer _ | Tarray _ | Tstruct (_,_) | Tunion (_,_) -> ptr_mq
    4949  | Tcomp_ptr _         -> assert false (*FIXME what is this ? *)               
    5050
     
    7676  | Tint (I32,_)                -> 4
    7777  | Tpointer _                  -> ptr_size     
    78   | Tarray (c,s)                -> s*(size_of_ctype c)
     78  | Tarray (_,c,s)                -> s*(size_of_ctype c)
    7979  | Tstruct (_,lst)             ->
    8080      List.fold_left
     
    8888  | Tcomp_ptr _                 -> assert false (*FIXME what is this ?*)
    8989
    90 let translate_global_vars ((id,lst),_) = (id,init_to_data lst)
     90let translate_global_vars (((id,lst),_),_) = (id,init_to_data lst)
    9191
    9292let translate_unop t = function
     
    110110  | (Tint(_,_),Tint(_,_))       -> Op2 (Op_add,e1,e2)
    111111  | (Tfloat _,Tfloat _)         -> assert false (*Not supported*)
    112   | (Tpointer t,Tint(_,_))      ->
     112  | (Tpointer (_,t),Tint(_,_))      ->
    113113      Op2 (Op_addp,e1, Op2 (Op_mul,e2,Cst (Cst_int (size_of_ctype t))))
    114   | (Tint(_,_),Tpointer t)      ->
     114  | (Tint(_,_),Tpointer (_,t))      ->
    115115      Op2 (Op_addp,Op2 (Op_mul,e1,Cst (Cst_int (size_of_ctype t))),e2)
    116   | (Tarray (t,_),Tint(_,_))    ->
     116  | (Tarray (_,t,_),Tint(_,_))    ->
    117117      Op2 (Op_addp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
    118   | (Tint(_,_),Tarray(t,_))     ->
     118  | (Tint(_,_),Tarray(_,t,_))     ->
    119119      Op2 (Op_addp,e2,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t)))))
    120120  | _                           -> assert false (*Type error*)
     
    123123  | (Tint(_,_),Tint(_,_))       -> Op2 (Op_sub,e1,e2)
    124124  | (Tfloat _,Tfloat _)         -> assert false (*Not supported*)
    125   | (Tpointer t,Tint(_,_))      ->
     125  | (Tpointer (_,t),Tint(_,_))      ->
    126126      Op2 (Op_subp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
    127   | (Tint(_,_),Tpointer t)      ->
     127  | (Tint(_,_),Tpointer (_,t))      ->
    128128      Op2 (Op_subp,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t)))),e2)
    129   | (Tarray (t,_),Tint(_,_))    ->
     129  | (Tarray (_,t,_),Tint(_,_))    ->
    130130      Op2 (Op_subp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
    131   | (Tint(_,_),Tarray(t,_))     ->
     131  | (Tint(_,_),Tarray(_,t,_))     ->
    132132      Op2 (Op_subp,e2,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t)))))
    133133  | _                           -> assert false (*Type error*)
     
    177177
    178178let is_struct = function
    179   | Tarray(_,_) | Tstruct (_,_) | Tunion(_,_) -> true
     179  | Tarray _ | Tstruct (_,_) | Tunion(_,_) -> true
    180180  | _ -> false
    181181
    182182let is_ptr_to_struct = function
    183   | Tpointer t when is_struct t -> true
     183  | Tpointer (_,t) when is_struct t -> true
    184184  | _ -> false 
    185185
     
    450450
    451451let is_struct = function
    452   | Tarray (_,_) | Tstruct (_,_) | Tunion (_,_) -> true
     452  | Tarray _ | Tstruct (_,_) | Tunion (_,_) -> true
    453453  | _ -> false
    454454
     
    519519
    520520let translate p =
    521   let globals = List.map (fun p -> (fst (fst p),snd p) ) p.prog_vars in
     521  let globals = List.map (fun p -> (fst (fst (fst p)),snd p) ) p.prog_vars in
    522522  let p =
    523523    {Cminor.vars   = List.map translate_global_vars p.prog_vars;
  • Deliverables/D2.3/8051-memoryspaces-branch/src/languages.ml

    r453 r460  
    241241  close_out cout
    242242
     243let rec find_clight = function
     244| [] -> None
     245| AstClight p :: t -> Some p
     246| _::t -> find_clight t
     247
     248let save_matita filename asts =
     249  match find_clight asts with
     250  | None -> Error.warning "during matita output" "No Clight AST."
     251  | Some prog -> begin
     252    let output_filename =
     253      Misc.SysExt.alternative
     254        (Filename.chop_extension filename
     255         ^ ".ma")
     256    in
     257    let cout = open_out output_filename in
     258    let fout = Format.formatter_of_out_channel cout in
     259    ClightPrintMatita.print_program fout prog;
     260    flush cout;
     261    close_out cout
     262  end
     263
    243264let interpret = function
    244265  | AstClight p ->
  • Deliverables/D2.3/8051-memoryspaces-branch/src/languages.mli

    r453 r460  
    7676val save : string -> ast -> unit
    7777
     78(** [save_matita filename asts] pretty prints the first Clight AST in
     79    [asts] in a fresh file whose name is prefixed by [filename] and whose
     80    extension is .ma. *)
     81val save_matita : string -> ast list -> unit
     82
    7883(** [from_string s] parses [s] as an intermediate language name. *)
    7984val from_string : string -> name
  • Deliverables/D2.3/8051-memoryspaces-branch/src/options.ml

    r453 r460  
    4444let is_dev_test_enabled ()      = !dev_test
    4545
     46let matita_output_flag          = ref false
     47let is_matita_output_enabled () = !matita_output_flag
     48
    4649let options = OptionsParsing.register [
    4750  "-s", Arg.String set_source_language,
     
    6669  "-dev", Arg.Set dev_test,
    6770  " Playground for developers.";
     71
     72  "-ma", Arg.Set matita_output_flag,
     73  " Output matita formatted Clight program.";
    6874]
  • Deliverables/D2.3/8051-memoryspaces-branch/src/options.mli

    r453 r460  
    2626(** {2 Developers' playground} *)
    2727val is_dev_test_enabled : unit -> bool
     28
     29(** {2 Matita output of Clight programs} *)
     30val is_matita_output_enabled : unit -> bool
     31
Note: See TracChangeset for help on using the changeset viewer.