source: src/Clight/acc-0.1.spaces.patch @ 3178

Last change on this file since 3178 was 416, checked in by campbell, 9 years ago

Fix printing of switch statements as matita terms.

File size: 130.1 KB
  • cparser/AddCasts.ml

    diff --git a/cparser/AddCasts.ml b/cparser/AddCasts.ml
    index 9ec128d..5f5184c 100644
    a b let widening_cast env tfrom tto = 
    3939      r1 < r2 || (r1 = r2 && is_signed_ikind k1 = is_signed_ikind k2)
    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
    4545
    let cast_not_needed env tfrom tto = 
    5252let cast env e tto =
    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
    5858   because casts cannot be materialized in op= expressions... *)
    let rec add_expr env e = 
    7373            EUnop(op, e1')
    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
    7979      let e2' = add_expr env e2 in
    let rec add_expr env e = 
    9797        | Oadd_assign|Osub_assign|Omul_assign|Odiv_assign|Omod_assign
    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 *)
    109110
    let add_arguments env ty_fun args = 
    132133  let ty_args =
    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
    138139        | _ -> assert false
    let add_arguments env ty_fun args = 
    146147
    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
    155156      else begin
    let add_topexpr env loc e = 
    162163  | ECall(e1, el) ->
    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  | _ ->
    168169      assert false
    let rec add_init env tto = function 
    175176  | Init_array il ->
    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) ->
    181182      Init_struct (id, List.map
  • cparser/Bitfields.ml

    diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
    index dea1862..c7dc25f 100644
    a b let insertion_mask bf = 
    118118      (Int64.pred (Int64.shift_left 1L bf.bf_size))
    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 *)
    124124
    signed int bitfield_signed_extract(unsigned int x, int ofs, int sz) 
    140140let bitfield_extract bf carrier =
    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 *)
    151151
    unsigned int bitfield_insert(unsigned int x, int ofs, int sz, unsigned int y) 
    161161
    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 *)
    179181
    let transf_expr env e = 
    188190
    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
    194196  let rec texp e =
    let transf_expr env e = 
    201203        let e1' = texp e1 in
    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
    211214    | EUnop(Oarrow fieldname, e1) ->
    212215        let e1' = texp e1 in
    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) ->
    227230        begin match e1.edesc with
    let transf_expr env e = 
    231234            | None ->
    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) ->
    247253            let lhs = texp e11 in let rhs = texp e2 in
    let transf_expr env e = 
    249255            | None ->
    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
    279289
    let bitfield_initializer bf i = 
    325335      let m = Int64.pred (Int64.shift_left 1L bf.bf_size) in
    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
    337350let rec pack_bitfield_init id carrier fld_init_list =
    let rec or_expr_list = function 
    354367  | [e] -> e
    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 =
    360374  match fld_init_list with
    let rec transf_struct_init id fld_init_list = 
    367381        ({fld_name = bf.bf_carrier; fld_typ = bf.bf_carrier_typ;
    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 ->
    373388        (fld, i) :: transf_struct_init id rem
  • cparser/Builtins.ml

    diff --git a/cparser/Builtins.ml b/cparser/Builtins.ml
    index 8eb1abf..aa243fd 100644
    a b let add_function (s, (res, args, va)) = 
    3737    TFun(res,
    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 = {
    4646  typedefs: (string * C.typ) list;
  • cparser/C.mli

    diff --git a/cparser/C.mli b/cparser/C.mli
    index d477acd..90df378 100644
    a b type binary_operator = 
    124124
    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
    135143  | TStruct of ident * attributes
    type typ = 
    137145
    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 =
    143151  | EConst of constant
    type globdecl = 
    220228  { gdesc: globdecl_desc; gloc: location }
    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 *)
    226234  | Gcompositedef of struct_or_union * ident * field list
  • cparser/Ceval.ml

    diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml
    index 0e22852..acf84aa 100644
    a b let cast env ty_to ty_from v = 
    9999      if is_signed env ty_from
    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  | _, _ ->
    109109      raise Notconst
    let constant_expr env ty e = 
    270270    match unroll env ty, cast env e.etyp ty (expr env e) with
    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
  • cparser/Cleanup.ml

    diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml
    index be28989..9644654 100644
    a b let needed id = 
    4040(* Iterate [addref] on all syntactic categories. *)
    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
    4747  | TNamed(id, _) -> addref id
    let rec add_init_globdecls accu = function 
    120120  | [] -> accu
    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) ->
    126126          add_fundef f; add_init_globdecls accu rem
    let rec add_needed_globdecls accu = function 
    135135  | [] -> accu
    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)
    141141          else add_needed_globdecls (g :: accu) rem
    let rec simpl_globdecls accu = function 
    174174  | g :: 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
    180180        | Gcompositedef(_, id, flds) -> needed id
  • cparser/Cprint.ml

    diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml
    index 7d8f2b3..70aba81 100644
    a b let rec dcl pp ty n = 
    6767      fprintf pp "%s%a%t" (name_of_ikind k) attributes a n
    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
    7373        | TFun _ | TArray _ -> fprintf pp " (*%a%t)" attributes a n
    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
    7979        | [] -> n pp
    let rec exp_of_stmt s = 
    353353  | Sdo e -> e
    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
    362364
    let rec stmt pp s = 
    373375      fprintf pp "@[<v 2>if (%a) {@ %a@;<0 -2>}@]"
    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
    379381  | Sif(e, s1, s2) ->
    let field pp f = 
    455457let globdecl pp g =
    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 ->
    461463      fundef pp f
  • cparser/Cutil.ml

    diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
    index 49b25a2..4a43d09 100644
    a b let rec add_attributes_type attr t = 
    7171  | TVoid a -> TVoid (add_attributes attr a)
    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)
    7878  | TNamed(s, a) -> TNamed(s, add_attributes attr a)
    let rec attributes_of_type env t = 
    9595  | TVoid a -> a
    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)
    102102  | TStruct(s, a) -> a
    let rec change_attributes_type env (f: attributes -> attributes) t = 
    110110  | TVoid a -> TVoid (f a)
    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) ->
    118118      let t1 = unroll env t in
    let combine_types ?(noattrs = false) env t1 t2 = 
    166166        TInt(comp_base ik1 ik2, comp_attr a1 a2)
    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) =
    175175          match params1, params2 with
    let rec alignof env t = 
    244244  | TVoid _ -> !config.alignof_void
    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)
    251251  | TStruct(name, _) ->
    let rec sizeof env t = 
    302302  | TVoid _ -> !config.sizeof_void
    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
    310310      | Some s ->
    let sizeof_union env members = 
    343343
    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
    349349      | None -> None                    (* should not happen? *)
    let float_rank = function 
    472472
    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
    479479(* The usual unary conversions (H&S 6.3.3) *)
    let unary_conversion env t = 
    489489          TInt(kind, attr)
    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
    496496
    let argument_conversion env t = 
    540540  (* Arrays and functions degrade automatically to pointers *)
    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
    547547(* Conversion on function arguments (old-style unprototyped, or vararg *)
    let enum_ikind = IInt 
    584584let type_of_constant = function
    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
    591591(* Check that a C expression is a lvalue *)
    let is_literal_0 e = 
    612612
    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
    623630               (erase_attributes_type env ty)
    let valid_cast env tfrom tto = 
    643650(* Construct an integer constant *)
    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 *)
    659666
    let sseq loc s1 s2 = 
    667674(* Construct an assignment statement *)
    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
    673680(* Empty location *)
  • cparser/Elab.ml

    diff --git a/cparser/Elab.ml b/cparser/Elab.ml
    index 7204508..1978b6b 100644
    a b let rec elab_attributes loc = function 
    270270      | None -> elab_attributes loc al
    271271      | Some a -> add_attributes [a] (elab_attributes loc al)
    272272
     273let elab_attribute_space = function
     274  | ("data", []) -> Some Data
     275  | ("idata", []) -> Some IData
     276  | ("pdata", []) -> Some PData
     277  | ("xdata", []) -> Some XData
     278  | ("code", []) -> Some Code
     279  | _ -> None
     280
     281let rec elab_attributes_space loc attrs =
     282  let rec aux = function
     283    | [] -> None
     284    | h::t -> (match elab_attribute_space h with
     285                | None -> aux t
     286                | Some v -> Some (v,t))
     287  in match aux attrs with
     288    | None -> Any
     289    | Some (space, rest) ->
     290       (match aux rest with
     291         | None -> ()
     292         | Some _ -> warning loc "Multiple memory spaces given");
     293       space
     294
    273295(* Auxiliary for typespec elaboration *)
    274296
    275297let typespec_rank = function (* Don't change this *)
    let typespec_rank = function (* Don't change this *) 
    288310
    289311let typespec_order t1 t2 = compare (typespec_rank t1) (typespec_rank t2)
    290312
     313
    291314(* Elaboration of a type specifier.  Returns 4-tuple:
    292315     (storage class, "inline" flag, elaborated type, new env)
    293316   Optional argument "only" is true if this is a standalone
    let rec elab_specifier ?(only = false) loc env specifier = 
    302325  let sto = ref Storage_default
    303326  and inline = ref false
    304327  and attr = ref []
    305   and tyspecs = ref [] in
     328  and tyspecs = ref []
     329  and space = ref Any in
    306330
    307331  let do_specifier = function
    308332  | SpecTypedef -> ()
    let rec elab_specifier ?(only = false) loc env specifier = 
    314338        | CV_RESTRICT -> ARestrict in
    315339      attr := add_attributes [a] !attr
    316340  | SpecAttr a ->
    317       attr := add_attributes (elab_attributes loc [a]) !attr
     341      attr := add_attributes (elab_attributes loc [a]) !attr;
     342      (match elab_attribute_space a with
     343        | None -> ()
     344        | Some sp ->
     345           if !space <> Any then
     346             error loc "multiple memory space specifiers";
     347           space := sp)
    318348  | SpecStorage st ->
    319349      if !sto <> Storage_default then
    320350        error loc "multiple storage specifiers";
    let rec elab_specifier ?(only = false) loc env specifier = 
    330360
    331361  List.iter do_specifier specifier;
    332362
    333   let simple ty = (!sto, !inline, add_attributes_type !attr ty, env) in
     363  let simple ty = (!space, !sto, !inline, add_attributes_type !attr ty, env) in
    334364
    335365  (* Now interpret the list of type specifiers.  Much of this code
    336366     is stolen from CIL. *)
    let rec elab_specifier ?(only = false) loc env specifier = 
    394424        let (id', env') =
    395425          elab_struct_or_union only Struct loc id optmembers env in
    396426        let attr' = add_attributes !attr (elab_attributes loc a) in
    397         (!sto, !inline, TStruct(id', attr'), env')
     427        (!space, !sto, !inline, TStruct(id', attr'), env')
    398428
    399429    | [Cabs.Tunion(id, optmembers, a)] ->
    400430        let (id', env') =
    401431          elab_struct_or_union only Union loc id optmembers env in
    402432        let attr' = add_attributes !attr (elab_attributes loc a) in
    403         (!sto, !inline, TUnion(id', attr'), env')
     433        (!space, !sto, !inline, TUnion(id', attr'), env')
    404434
    405435    | [Cabs.Tenum(id, optmembers, a)] ->
    406436        let env' =
    407437          elab_enum loc id optmembers env in
    408438        let attr' = add_attributes !attr (elab_attributes loc a) in
    409         (!sto, !inline, TInt(enum_ikind, attr'), env')
     439        (!space, !sto, !inline, TInt(enum_ikind, attr'), env')
    410440
    411441    | [Cabs.TtypeofE _] ->
    412442        fatal_error loc "GCC __typeof__ not supported"
    let rec elab_specifier ?(only = false) loc env specifier = 
    419449
    420450(* Elaboration of a type declarator.  *)
    421451
    422 and elab_type_declarator loc env ty = function
     452and elab_type_declarator loc env space ty = function
    423453  | Cabs.JUSTBASE ->
    424       (ty, env)
     454      (space, ty, env)
    425455  | Cabs.PARENTYPE(attr1, d, attr2) ->
    426456      (* XXX ignoring the distinction between attrs after and before *)
    427457      let a = elab_attributes loc (attr1 @ attr2) in
    428       elab_type_declarator loc env (add_attributes_type a ty) d
     458      (* XXX ought to use space from attrs? *)
     459      elab_type_declarator loc env space (add_attributes_type a ty) d
    429460  | Cabs.ARRAY(d, attr, sz) ->
    430461      let a = elab_attributes loc attr in
    431462      let sz' =
    and elab_type_declarator loc env ty = function 
    440471            | None ->
    441472                error loc "array size is not a compile-time constant";
    442473                Some 1L in (* produces better error messages later *)
    443        elab_type_declarator loc env (TArray(ty, sz', a)) d
     474       elab_type_declarator loc env space (TArray(space, ty, sz', a)) d
    444475  | Cabs.PTR(attr, d) ->
    445476      let a = elab_attributes loc attr in
    446        elab_type_declarator loc env (TPtr(ty, a)) d
     477      let space' = elab_attributes_space loc attr in
     478       elab_type_declarator loc env space' (TPtr(space, ty, a)) d
    447479  | Cabs.PROTO(d, params, vararg) ->
    448480       begin match unroll env ty with
    449481       | TArray _ | TFun _ ->
    and elab_type_declarator loc env ty = function 
    451483       | _ -> ()
    452484       end;
    453485       let params' = elab_parameters env params in
    454        elab_type_declarator loc env (TFun(ty, params', vararg, [])) d
     486       elab_type_declarator loc env space (TFun(ty, params', vararg, [])) d
    455487
    456488(* Elaboration of parameters in a prototype *)
    457489
    and elab_parameter env (spec, name) = 
    476508      "'extern' or 'static' storage not supported for function parameter";
    477509  (* replace array and function types by pointer types *)
    478510  let ty1 = argument_conversion env1 ty in
    479   let (id', env2) = Env.enter_ident env1 id sto ty1 in
     511  let (id', env2) = Env.enter_ident env1 id sto ty1 Any (* stack *) in
    480512  ( (id', ty1) , env2 )
    481513
    482514(* Elaboration of a (specifier, Cabs "name") pair *)
    483515
    484516and elab_name env spec (id, decl, attr, loc) =
    485   let (sto, inl, bty, env') = elab_specifier loc env spec in
    486   let (ty, env'') = elab_type_declarator loc env' bty decl in
     517  let (space, sto, inl, bty, env') = elab_specifier loc env spec in
     518  let (_, ty, env'') = elab_type_declarator loc env' space bty decl in
    487519  let a = elab_attributes loc attr in
    488520  (id, sto, inl, add_attributes_type a ty, env'')
    489521
    490522(* Elaboration of a name group *)
    491523
    492524and elab_name_group env (spec, namelist) =
    493   let (sto, inl, bty, env') =
     525  let (space, sto, inl, bty, env') =
    494526    elab_specifier (loc_of_namelist namelist) env spec in
    495527  let elab_one_name env (id, decl, attr, loc) =
    496     let (ty, env1) =
    497       elab_type_declarator loc env bty decl in
     528    let (_, ty, env1) =
     529      elab_type_declarator loc env space bty decl in
    498530    let a = elab_attributes loc attr in
    499531    ((id, sto, add_attributes_type a ty), env1) in
    500532  mmap elab_one_name env' namelist
    and elab_name_group env (spec, namelist) = 
    502534(* Elaboration of an init-name group *)
    503535
    504536and elab_init_name_group env (spec, namelist) =
    505   let (sto, inl, bty, env') =
     537  let (space, sto, inl, bty, env') =
    506538    elab_specifier (loc_of_init_name_list namelist) env spec in
    507539  let elab_one_name env ((id, decl, attr, loc), init) =
    508     let (ty, env1) =
    509       elab_type_declarator loc env bty decl in
     540    let (space', ty, env1) =
     541      elab_type_declarator loc env space bty decl in
    510542    let a = elab_attributes loc attr in
    511     ((id, sto, add_attributes_type a ty, init), env1) in
     543    ((space', id, sto, add_attributes_type a ty, init), env1) in
    512544  mmap elab_one_name env' namelist
    513545
    514546(* Elaboration of a field group *)
    and elab_struct_or_union_info kind loc env members = 
    558590  (* Check for incomplete types *)
    559591  let rec check_incomplete = function
    560592  | [] -> ()
    561   | [ { fld_typ = TArray(ty_elt, None, _) } ] when kind = Struct -> ()
     593  | [ { fld_typ = TArray(_, ty_elt, None, _) } ] when kind = Struct -> ()
    562594        (* C99: ty[] allowed as last field of a struct *)
    563595  | fld :: rem ->
    564596      if incomplete_type env' fld.fld_typ then
    and elab_enum loc tag optmembers env = 
    663695(* Elaboration of a naked type, e.g. in a cast *)
    664696
    665697let elab_type loc env spec decl =
    666   let (sto, inl, bty, env') = elab_specifier loc env spec in
    667   let (ty, env'') = elab_type_declarator loc env' bty decl in
     698  let (space, sto, inl, bty, env') = elab_specifier loc env spec in
     699  let (_, ty, env'') = elab_type_declarator loc env' space bty decl in
    668700  if sto <> Storage_default || inl then
    669701    error loc "'extern', 'static', 'register' and 'inline' are meaningless in cast";
    670702  ty
    671703
     704
     705let join_spaces s1 s2 =
     706if s1 = s2 then s1 else Any
     707
    672708
    673709
    674710(* Elaboration of expressions *)
  • cparser/Env.ml

     
    @@ -687,15 +723,15 @@ let elab_expr loc env a =
     
       | VARIABLE s ->
           begin match wrap Env.lookup_ident loc env s with
    -      | (id, II_ident(sto, ty)) ->
    -          { edesc = EVar id; etyp = ty }
    +      | (id, II_ident(sto, ty, spc)) ->
    +          { edesc = EVar id; etyp = ty; espace=spc }
           | (id, II_enum v) ->
    -          { edesc = EConst(CEnum(id, v)); etyp = TInt(enum_ikind, []) }
    +          { edesc = EConst(CEnum(id, v)); etyp = TInt(enum_ikind, []); espace = Code }
           end
     
       | CONSTANT cst ->
           let cst' = elab_constant loc cst in
    -      { edesc = EConst cst'; etyp = type_of_constant cst' }
    +      { edesc = EConst cst'; etyp = type_of_constant cst'; espace = Code }
     
       | PAREN e ->
           elab e
    @@ -704,12 +740,12 @@ let elab_expr loc env a =
     
       | INDEX(a1, a2) ->            (* e1[e2] *)
           let b1 = elab a1 in let b2 = elab a2 in
    -      let tres =
    +      let space, tres =
             match (unroll env b1.etyp, unroll env b2.etyp) with
    -        | (TPtr(t, _) | TArray(t, _, _)), TInt _ -> t
    -        | TInt _, (TPtr(t, _) | TArray(t, _, _)) -> t
    +        | (TPtr(space, t, _) | TArray(space, t, _, _)), TInt _ -> space, t
    +        | TInt _, (TPtr(space, t, _) | TArray(space, t, _, _)) -> space, t
             | t1, t2 -> error "incorrect types for array subscripting" in
    -      { edesc = EBinop(Oindex, b1, b2, TPtr(tres, [])); etyp = tres }
    +      { edesc = EBinop(Oindex, b1, b2, TPtr(space, tres, [])); etyp = tres; espace = space }
     
       | MEMBEROF(a1, fieldname) ->
           let b1 = elab a1 in
    @@ -723,25 +759,27 @@ let elab_expr loc env a =
                 error "left-hand side of '.' is not a struct or union" in
           (* A field of a const/volatile struct or union is itself const/volatile *)
           { edesc = EUnop(Odot fieldname, b1);
    -        etyp = add_attributes_type attrs fld.fld_typ }
    +        etyp = add_attributes_type attrs fld.fld_typ;
    +        espace = b1.espace }
     
       | MEMBEROFPTR(a1, fieldname) ->
           let b1 = elab a1 in
    -      let (fld, attrs) =
    +      let (space, fld, attrs) =
             match unroll env b1.etyp with
    -        | TPtr(t, _) ->
    +        | TPtr(space, t, _) ->
                 begin match unroll env t with
                 | TStruct(id, attrs) ->
    -                (wrap Env.find_struct_member loc env (id, fieldname), attrs)
    +                (space, wrap Env.find_struct_member loc env (id, fieldname), attrs)
                 | TUnion(id, attrs) ->
    -                (wrap Env.find_union_member loc env (id, fieldname), attrs)
    +                (space, wrap Env.find_union_member loc env (id, fieldname), attrs)
                 | _ ->
                     error "left-hand side of '->' is not a pointer to a struct or union"
                 end
             | _ ->
                 error "left-hand side of '->' is not a pointer " in
           { edesc = EUnop(Oarrow fieldname, b1);
    -        etyp = add_attributes_type attrs fld.fld_typ }
    +        etyp = add_attributes_type attrs fld.fld_typ;
    +        espace = space }
     
     (* Hack to treat vararg.h functions the GCC way.  Helps with testing.
         va_start(ap,n)
    @@ -754,13 +792,15 @@ let elab_expr loc env a =
       | CALL((VARIABLE "__builtin_va_start" as a1), [a2; a3]) ->
           let b1 = elab a1 and b2 = elab a2 and b3 = elab a3 in
           { edesc = ECall(b1, [b2; {edesc = EUnop(Oaddrof, b3);
    -                                etyp = TPtr(b3.etyp, [])}]);
    -        etyp = TVoid [] }
    +                                etyp = TPtr(b3.espace, b3.etyp, []);
    +                                espace = Any }]);
    +        etyp = TVoid [];
    +        espace = Any (* XXX ? *) }
       | CALL((VARIABLE "__builtin_va_arg" as a1),
              [a2; (TYPE_SIZEOF _) as a3]) ->
           let b1 = elab a1 and b2 = elab a2 and b3 = elab a3 in
           let ty = match b3.edesc with ESizeof ty -> ty | _ -> assert false in
    -      { edesc = ECall(b1, [b2; b3]); etyp = ty }
    +      { edesc = ECall(b1, [b2; b3]); etyp = ty; espace = Any (* XXX ? *) }
     
       | CALL(a1, al) ->
           let b1 =
    @@ -771,15 +811,15 @@ let elab_expr loc env a =
                 let ty = TFun(TInt(IInt, []), None, false, []) in
                 (* Emit an extern declaration for it *)
                 let id = Env.fresh_ident n in
    -            emit_elab (elab_loc loc) (Gdecl(Storage_extern, id, ty, None));
    -            { edesc = EVar id; etyp = ty }
    +            emit_elab (elab_loc loc) (Gdecl(Code, (Storage_extern, id, ty, None)));
    +            { edesc = EVar id; etyp = ty; espace = Any }
             | _ -> elab a1 in
           let bl = List.map elab al in
           (* Extract type information *)
           let (res, args, vararg) =
             match unroll env b1.etyp with
             | TFun(res, args, vararg, a) -> (res, args, vararg)
    -        | TPtr(ty, a) ->
    +        | TPtr(_, ty, a) ->
                 begin match unroll env ty with
                 | TFun(res, args, vararg, a) -> (res, args, vararg)
                 | _ -> error "the function part of a call does not have a function type"
    @@ -791,7 +831,7 @@ let elab_expr loc env a =
             match args with
             | None -> bl
             | Some proto -> elab_arguments 1 bl proto vararg in
    -      { edesc = ECall(b1, bl'); etyp = res }
    +      { edesc = ECall(b1, bl'); etyp = res; espace = Any (* Stack *) }
     
       | UNARY(POSINCR, a1) ->
           elab_pre_post_incr_decr Opostincr "postfix '++'" a1
    @@ -805,50 +845,50 @@ let elab_expr loc env a =
           let b1 = elab a1 in
           if not (valid_cast env b1.etyp ty) then
             err "illegal cast from %a@ to %a" Cprint.typ b1.etyp Cprint.typ ty;
    -      { edesc = ECast(ty, b1); etyp = ty }
    +      { edesc = ECast(ty, b1); etyp = ty; espace = b1.espace }
     
       | CAST ((spec, dcl), _) ->
           error "cast of initializer expression is not supported"
     
       | EXPR_SIZEOF(CONSTANT(CONST_STRING s)) ->
           let cst = CInt(Int64.of_int (String.length s), size_t_ikind, "") in
    -      { edesc = EConst cst; etyp = type_of_constant cst }
    +      { edesc = EConst cst; etyp = type_of_constant cst; espace = Code }
     
       | EXPR_SIZEOF a1 ->
           let b1 = elab a1 in
           if sizeof env b1.etyp = None then
             err "incomplete type %a" Cprint.typ b1.etyp;
    -      { edesc = ESizeof b1.etyp; etyp = TInt(size_t_ikind, []) }
    +      { edesc = ESizeof b1.etyp; etyp = TInt(size_t_ikind, []); espace = Code }
     
       | TYPE_SIZEOF (spec, dcl) ->
           let ty = elab_type loc env spec dcl in
           if sizeof env ty = None then
             err "incomplete type %a" Cprint.typ ty;
    -      { edesc = ESizeof ty; etyp = TInt(size_t_ikind, []) }
    +      { edesc = ESizeof ty; etyp = TInt(size_t_ikind, []); espace = Code }
     
       | UNARY(PLUS, a1) ->
           let b1 = elab a1 in
           if not (is_arith_type env b1.etyp) then
             error "argument of unary '+' is not an arithmetic type";
    -      { edesc = EUnop(Oplus, b1); etyp = unary_conversion env b1.etyp }
    +      { edesc = EUnop(Oplus, b1); etyp = unary_conversion env b1.etyp; espace = Any }
     
       | UNARY(MINUS, a1) ->
           let b1 = elab a1 in
           if not (is_arith_type env b1.etyp) then
             error "argument of unary '-' is not an arithmetic type";
    -      { edesc = EUnop(Ominus, b1); etyp = unary_conversion env b1.etyp }
    +      { edesc = EUnop(Ominus, b1); etyp = unary_conversion env b1.etyp; espace = Any }
     
       | UNARY(BNOT, a1) ->
           let b1 = elab a1 in
           if not (is_integer_type env b1.etyp) then
             error "argument of '~' is not an integer type";
    -      { edesc = EUnop(Onot, b1); etyp = unary_conversion env b1.etyp }
    +      { edesc = EUnop(Onot, b1); etyp = unary_conversion env b1.etyp; espace = Any }
     
       | UNARY(NOT, a1) ->
           let b1 = elab a1 in
           if not (is_scalar_type env b1.etyp) then
             error "argument of '!' is not a scalar type";
    -      { edesc = EUnop(Olognot, b1); etyp = TInt(IInt, []) }
    +      { edesc = EUnop(Olognot, b1); etyp = TInt(IInt, []); espace = Any }
     
       | UNARY(ADDROF, a1) ->
           let b1 = elab a1 in
    @@ -857,15 +897,15 @@ let elab_expr loc env a =
           | _ -> 
             if not (is_lvalue env b1) then err "argument of '&' is not a l-value"
           end;
    -      { edesc = EUnop(Oaddrof, b1); etyp = TPtr(b1.etyp, []) }
    +      { edesc = EUnop(Oaddrof, b1); etyp = TPtr(b1.espace, b1.etyp, []); espace = Any }
     
       | UNARY(MEMOF, a1) ->
           let b1 = elab a1 in
           begin match unroll env b1.etyp with
           (* '*' applied to a function type has no effect *)
           | TFun _ -> b1
    -      | TPtr(ty, _) | TArray(ty, _, _) ->
    -          { edesc = EUnop(Oderef, b1); etyp = ty }
    +      | TPtr(space, ty, _) | TArray(space, ty, _, _) ->
    +          { edesc = EUnop(Oderef, b1); etyp = ty; espace = space }
           | _ ->
               error "argument of unary '*' is not a pointer"
           end
    @@ -893,16 +933,16 @@ let elab_expr loc env a =
             if is_arith_type env b1.etyp && is_arith_type env b2.etyp then
               binary_conversion env b1.etyp b2.etyp
             else begin
    -          let (ty, attr) =
    +          let (space, ty, attr) =
                 match unroll env b1.etyp, unroll env b2.etyp with
    -            | (TPtr(ty, a) | TArray(ty, _, a)), TInt _ -> (ty, a)
    -            | TInt _, (TPtr(ty, a) | TArray(ty, _, a)) -> (ty, a)
    +            | (TPtr(space, ty, a) | TArray(space, ty, _, a)), TInt _ -> (space, ty, a)
    +            | TInt _, (TPtr(space, ty, a) | TArray(space, ty, _, a)) -> (space, ty, a)
                 | _, _ -> error "type error in binary '+'" in
               if not (pointer_arithmetic_ok env ty) then
                 err "illegal pointer arithmetic in binary '+'";
    -          TPtr(ty, attr)
    +          TPtr(space, ty, attr)
             end in
    -      { edesc = EBinop(Oadd, b1, b2, tyres); etyp = tyres }
    +      { edesc = EBinop(Oadd, b1, b2, tyres); etyp = tyres; espace = Any }
     
       | BINARY(SUB, a1, a2) ->
           let b1 = elab a1 in
    @@ -913,24 +953,25 @@ let elab_expr loc env a =
               (tyres, tyres)
             end else begin
               match unroll env b1.etyp, unroll env b2.etyp with
    -          | (TPtr(ty, a) | TArray(ty, _, a)), TInt _ ->
    +          | (TPtr(space, ty, a) | TArray(space, ty, _, a)), TInt _ ->
                   if not (pointer_arithmetic_ok env ty) then
                     err "illegal pointer arithmetic in binary '-'";
    -              (TPtr(ty, a), TPtr(ty, a))
    -          | TInt _, (TPtr(ty, a) | TArray(ty, _, a)) ->
    +              (TPtr(space, ty, a), TPtr(space, ty, a))
    +          | TInt _, (TPtr(space, ty, a) | TArray(space, ty, _, a)) ->
                   if not (pointer_arithmetic_ok env ty) then
                     err "illegal pointer arithmetic in binary '-'";
    -              (TPtr(ty, a), TPtr(ty, a))
    -          | (TPtr(ty1, a1) | TArray(ty1, _, a1)),
    -            (TPtr(ty2, a2) | TArray(ty2, _, a2)) ->
    -              if not (compatible_types ~noattrs:true env ty1 ty2) then
    +              (TPtr(space, ty, a), TPtr(space, ty, a))
    +          | (TPtr(space1, ty1, a1) | TArray(space1, ty1, _, a1)),
    +            (TPtr(space2, ty2, a2) | TArray(space2, ty2, _, a2)) ->
    +(* TODO: automatic cast on space mismatch? *)
    +              if not (compatible_types ~noattrs:true env ty1 ty2) || space1 != space2 then
                     err "mismatch between pointer types in binary '-'";
                   if not (pointer_arithmetic_ok env ty1) then
                     err "illegal pointer arithmetic in binary '-'";
    -              (TPtr(ty1, []), TInt(ptrdiff_t_ikind, []))
    +              (TPtr(space1, ty1, []), TInt(ptrdiff_t_ikind, []))
               | _, _ -> error "type error in binary '-'"
             end in
    -      { edesc = EBinop(Osub, b1, b2, tyop); etyp = tyres }
    +      { edesc = EBinop(Osub, b1, b2, tyop); etyp = tyres; espace = Any }
     
       | BINARY(SHL, a1, a2) ->
           elab_shift "<<" Oshl a1 a2
    @@ -970,35 +1011,38 @@ let elab_expr loc env a =
           let b1 = elab a1 in
           let b2 = elab a2 in
           let b3 = elab a3 in
    +      let space = join_spaces b2.espace b3.espace in
           if not (is_scalar_type env b1.etyp) then
             err ("the first argument of '? :' is not a scalar type");
           begin match pointer_decay env b2.etyp, pointer_decay env b3.etyp with
           | (TInt _ | TFloat _), (TInt _ | TFloat _) ->
               { edesc = EConditional(b1, b2, b3);
    -            etyp = binary_conversion env b2.etyp b3.etyp }
    -      | TPtr(ty1, a1), TPtr(ty2, a2) ->
    +            etyp = binary_conversion env b2.etyp b3.etyp;
    +            espace = space }
    +      (* TODO: maybe we should automatically cast to a generic pointer when the spaces don't match? *)
    +      | TPtr(sp1, ty1, a1), TPtr(sp2, ty2, a2) ->
               let tyres =
    -            if is_void_type env ty1 || is_void_type env ty2 then
    -              TPtr(TVoid [], add_attributes a1 a2)
    +            if (is_void_type env ty1 || is_void_type env ty2) && sp1 = sp2 then
    +              TPtr(sp1, TVoid [], add_attributes a1 a2)
                 else
                   match combine_types ~noattrs:true env
    -                                  (TPtr(ty1, a1)) (TPtr(ty2, a2)) with
    +                                  (TPtr(sp1, ty1, a1)) (TPtr(sp2, ty2, a2)) with
                   | None ->
                       error "the second and third arguments of '? :' \
                              have incompatible pointer types"
                   | Some ty -> ty
                 in
    -          { edesc = EConditional(b1, b2, b3); etyp = tyres }
    -      | TPtr(ty1, a1), TInt _ when is_literal_0 b3 ->
    -          { edesc = EConditional(b1, b2, nullconst); etyp = TPtr(ty1, a1) }
    -      | TInt _, TPtr(ty2, a2) when is_literal_0 b2 ->
    -          { edesc = EConditional(b1, nullconst, b3); etyp = TPtr(ty2, a2) }
    +          { edesc = EConditional(b1, b2, b3); etyp = tyres; espace = space }
    +      | TPtr(sp1, ty1, a1), TInt _ when is_literal_0 b3 ->
    +          { edesc = EConditional(b1, b2, nullconst); etyp = TPtr(sp1, ty1, a1); espace = space }
    +      | TInt _, TPtr(sp2, ty2, a2) when is_literal_0 b2 ->
    +          { edesc = EConditional(b1, nullconst, b3); etyp = TPtr(sp2, ty2, a2); espace = space }
           | ty1, ty2 ->
               match combine_types env ty1 ty2 with
               | None ->
                   error ("the second and third arguments of '? :' have incompatible types")
               | Some tyres ->
    -              { edesc = EConditional(b1, b2, b3); etyp = tyres }
    +              { edesc = EConditional(b1, b2, b3); etyp = tyres; espace = space }
           end
     
     (* 7.9 Assignment expressions *)
    @@ -1018,7 +1062,7 @@ let elab_expr loc env a =
               err "assigning a value of type@ %a@ to a lvalue of type@ %a"
                       Cprint.typ b2.etyp Cprint.typ b1.etyp;
           end;
    -      { edesc = EBinop(Oassign, b1, b2, b1.etyp); etyp = b1.etyp }
    +      { edesc = EBinop(Oassign, b1, b2, b1.etyp); etyp = b1.etyp; espace = b1.espace }
     
       | BINARY((ADD_ASSIGN | SUB_ASSIGN | MUL_ASSIGN | DIV_ASSIGN | MOD_ASSIGN
                 | BAND_ASSIGN | BOR_ASSIGN | XOR_ASSIGN | SHL_ASSIGN | SHR_ASSIGN
    @@ -1050,7 +1094,7 @@ let elab_expr loc env a =
                   err "assigning a value of type@ %a@ to a lvalue of type@ %a"
                           Cprint.typ ty Cprint.typ b1.etyp;
               end;
    -          { edesc = EBinop(top, b1, b2, ty); etyp = b1.etyp }
    +          { edesc = EBinop(top, b1, b2, ty); etyp = b1.etyp; espace = b1.espace }
           | _ -> assert false
           end
     
    @@ -1063,7 +1107,7 @@ let elab_expr loc env a =
           | [] -> accu
           | a :: l ->
               let b = elab a in
    -          elab_comma { edesc = EBinop(Ocomma, accu, b, b.etyp); etyp = b.etyp } l
    +          elab_comma { edesc = EBinop(Ocomma, accu, b, b.etyp); etyp = b.etyp; espace = b.espace } l
           in elab_comma (elab a1) al
     
     (* Extensions that we do not handle *)
    @@ -1099,7 +1143,7 @@ let elab_expr loc env a =
             err "the argument of %s is not a l-value" msg;
           if not (is_scalar_type env b1.etyp) then
             err "the argument of %s must be an arithmetic or pointer type" msg;
    -      { edesc = EUnop(op, b1); etyp = b1.etyp }
    +      { edesc = EUnop(op, b1); etyp = b1.etyp; espace = b1.espace }
     
     (* Elaboration of binary operators over integers *)
       and elab_binary_integer msg op a1 a2 =
    @@ -1110,7 +1154,7 @@ let elab_expr loc env a =
           if not (is_integer_type env b2.etyp) then
             error "the second argument of '%s' is not an integer type" msg;
           let tyres = binary_conversion env b1.etyp b2.etyp in
    -      { edesc = EBinop(op, b1, b2, tyres); etyp = tyres }
    +      { edesc = EBinop(op, b1, b2, tyres); etyp = tyres; espace = Any }
     
     (* Elaboration of binary operators over arithmetic types *)
       and elab_binary_arithmetic msg op a1 a2 =
    @@ -1121,7 +1165,7 @@ let elab_expr loc env a =
           if not (is_arith_type env b2.etyp) then
             error "the second argument of '%s' is not an arithmetic type" msg;
           let tyres = binary_conversion env b1.etyp b2.etyp in
    -      { edesc = EBinop(op, b1, b2, tyres); etyp = tyres }
    +      { edesc = EBinop(op, b1, b2, tyres); etyp = tyres; espace = Any }
     
     (* Elaboration of shift operators *)
       and elab_shift msg op a1 a2 =
    @@ -1132,7 +1176,7 @@ let elab_expr loc env a =
           if not (is_integer_type env b2.etyp) then
             error "the second argument of '%s' is not an integer type" msg;
           let tyres = unary_conversion env b1.etyp in
    -      { edesc = EBinop(op, b1, b2, tyres); etyp = tyres }
    +      { edesc = EBinop(op, b1, b2, tyres); etyp = tyres; espace = Any }
     
     (* Elaboration of comparisons *)
       and elab_comparison op a1 a2 =
    @@ -1142,28 +1186,28 @@ let elab_expr loc env a =
             match pointer_decay env b1.etyp, pointer_decay env b2.etyp with
             | (TInt _ | TFloat _), (TInt _ | TFloat _) ->
                 EBinop(op, b1, b2, binary_conversion env b1.etyp b2.etyp)
    -        | TInt _, TPtr(ty, _) when is_literal_0 b1 ->
    -            EBinop(op, nullconst, b2, TPtr(ty, []))
    -        | TPtr(ty, _), TInt _ when is_literal_0 b2 ->
    -            EBinop(op, b1, nullconst, TPtr(ty, []))
    -        | TPtr(ty1, _), TPtr(ty2, _)
    +        | TInt _, TPtr(sp, ty, _) when is_literal_0 b1 ->
    +            EBinop(op, nullconst, b2, TPtr(sp, ty, []))
    +        | TPtr(sp, ty, _), TInt _ when is_literal_0 b2 ->
    +            EBinop(op, b1, nullconst, TPtr(sp, ty, []))
    +        | TPtr(sp1, ty1, _), TPtr(sp2, ty2, _)
               when is_void_type env ty1 ->
    -            EBinop(op, b1, b2, TPtr(ty2, []))
    -        | TPtr(ty1, _), TPtr(ty2, _)
    +            EBinop(op, b1, b2, TPtr(sp2, ty2, []))  (* XXX sp1? *)
    +        | TPtr(sp1, ty1, _), TPtr(sp2, ty2, _)
               when is_void_type env ty2 ->
    -            EBinop(op, b1, b2, TPtr(ty1, []))
    -        | TPtr(ty1, _), TPtr(ty2, _) ->
    +            EBinop(op, b1, b2, TPtr(sp1, ty1, []))  (* XXX sp2? *)
    +        | TPtr(sp1, ty1, _), TPtr(sp2, ty2, _) ->
                 if not (compatible_types ~noattrs:true env ty1 ty2) then
                   warning "comparison between incompatible pointer types";
    -            EBinop(op, b1, b2, TPtr(ty1, []))
    -        | TPtr _, TInt _
    -        | TInt _, TPtr _ ->
    +            EBinop(op, b1, b2, TPtr(sp1, ty1, []))  (* XXX sp1? *)
    +        | TPtr (sp,_,_), TInt _
    +        | TInt _, TPtr (sp,_,_) ->
                 warning "comparison between integer and pointer";
    -            EBinop(op, b1, b2, TPtr(TVoid [], []))
    +            EBinop(op, b1, b2, TPtr(sp,TVoid [], []))
             | ty1, ty2 ->
                 error "illegal comparison between types@ %a@ and %a"
                       Cprint.typ b1.etyp Cprint.typ b2.etyp in
    -      { edesc = resdesc; etyp = TInt(IInt, []) }
    +      { edesc = resdesc; etyp = TInt(IInt, []); espace = Any }
     
     (* Elaboration of && and || *)
       and elab_logical_operator msg op a1 a2 =
    @@ -1173,7 +1217,7 @@ let elab_expr loc env a =
           let b2 = elab a2 in
           if not (is_scalar_type env b2.etyp) then
             err "the second argument of '%s' is not a scalar type" msg;
    -      { edesc = EBinop(op, b1, b2, TInt(IInt, [])); etyp = TInt(IInt, []) }
    +      { edesc = EBinop(op, b1, b2, TInt(IInt, [])); etyp = TInt(IInt, []); espace = Any }
     
     (* Type-checking of function arguments *)
       and elab_arguments argno args params vararg =
    @@ -1271,7 +1315,7 @@ let check_init_type loc env a ty =
     
     let rec elab_init loc env ty ile =
       match unroll env ty with
    -  | TArray(ty_elt, opt_sz, _) ->
    +  | TArray(space, ty_elt, opt_sz, _) ->
           let rec elab_init_array n accu rem =
             match opt_sz, rem with
             | Some sz, _ when n >= sz ->
    @@ -1390,8 +1434,8 @@ let elab_initial loc env ty ie =
     
     let fixup_typ env ty init =
       match unroll env ty, init with
    -  | TArray(ty_elt, None, attr), Init_array il ->
    -      TArray(ty_elt, Some(Int64.of_int(List.length il)), attr)
    +  | TArray(space, ty_elt, None, attr), Init_array il ->
    +      TArray(space, ty_elt, Some(Int64.of_int(List.length il)), attr)
       | _ -> ty
     
     (* Entry point *)
    @@ -1416,9 +1460,9 @@ let enter_typedef loc env (s, sto, ty) =
       emit_elab (elab_loc loc) (Gtypedef(id, ty));
       env'
     
    -let enter_or_refine_ident local loc env s sto ty =
    +let enter_or_refine_ident local loc env s sto ty space =
       match redef Env.lookup_ident env s with
    -  | Some(id, II_ident(old_sto, old_ty)) ->
    +  | Some(id, II_ident(old_sto, old_ty, old_space)) ->
           let new_ty =
             if local then begin
               error loc "redefinition of local variable '%s'" s;
    @@ -1437,17 +1481,18 @@ let enter_or_refine_ident local loc env s sto ty =
               warning loc "redefinition of '%s' with incompatible storage class" s;
               sto
             end in
    -      (id, Env.add_ident env id new_sto new_ty)
    +      let new_space = join_spaces old_space space (* XXX: incompatible? *) in
    +      (id, Env.add_ident env id new_sto new_ty new_space)
       | Some(id, II_enum v) ->
           error loc "illegal redefinition of enumerator '%s'" s;
    -      (id, Env.add_ident env id sto ty)
    +      (id, Env.add_ident env id sto ty space)
       | _ ->
    -      Env.enter_ident env s sto ty
    +      Env.enter_ident env s sto ty space
     
     let rec enter_decdefs local loc env = function
       | [] ->
           ([], env)
    -  | (s, sto, ty, init) :: rem ->
    +  | (space, s, sto, ty, init) :: rem ->
           (* Sanity checks on storage class *)
           begin match sto with
           | Storage_extern ->
    @@ -1462,11 +1507,11 @@ let rec enter_decdefs local loc env = function
             match unroll env ty with TFun _ -> Storage_extern | _ -> sto in
           (* enter ident in environment with declared type, because
              initializer can refer to the ident *)
    -      let (id, env1) = enter_or_refine_ident local loc env s sto' ty in
    +      let (id, env1) = enter_or_refine_ident local loc env s sto' ty space in
           (* process the initializer *)
           let (ty', init') = elab_initializer loc env1 ty init in
           (* update environment with refined type *)
    -      let env2 = Env.add_ident env1 id sto' ty' in
    +      let env2 = Env.add_ident env1 id sto' ty' space in
           (* check for incomplete type *)
           if sto' <> Storage_extern && incomplete_type env ty' then
             warning loc "'%s' has incomplete type" s;
    @@ -1476,7 +1521,7 @@ let rec enter_decdefs local loc env = function
             ((sto', id, ty', init') :: decls, env3)
           end else begin
             (* Global definition *)
    -        emit_elab (elab_loc loc) (Gdecl(sto, id, ty', init'));
    +        emit_elab (elab_loc loc) (Gdecl(space, (sto, id, ty', init')));
             enter_decdefs local loc env2 rem
           end
     
    @@ -1496,10 +1541,10 @@ let elab_fundef env (spec, name) body loc1 loc2 =
         | TFun(ty_ret, Some params, vararg, attr) -> (ty_ret, params, vararg)
         | _ -> fatal_error loc1 "wrong type for function definition" in
       (* Enter function in the environment, for recursive references *)
    -  let (fun_id, env1) = enter_or_refine_ident false loc1 env s sto ty in
    +  let (fun_id, env1) = enter_or_refine_ident false loc1 env s sto ty Code in
       (* Enter parameters in the environment *)
       let env2 =
    -    List.fold_left (fun e (id, ty) -> Env.add_ident e id Storage_default ty)
    +    List.fold_left (fun e (id, ty) -> Env.add_ident e id Storage_default ty Any)
                        (Env.new_scope env1) params in
       (* Elaborate function body *)
       let body' = !elab_block_f loc2 ty_ret env2 body in
    @@ -1538,7 +1583,7 @@ let rec elab_definition (local: bool) (env: Env.t) (def: Cabs.definition)
     
       (* "struct s { ...};" or "union u;" *)
       | ONLYTYPEDEF(spec, loc) ->
    -      let (sto, inl, ty, env') = elab_specifier ~only:true loc env spec in
    +      let (space, sto, inl, ty, env') = elab_specifier ~only:true loc env spec in
           if sto <> Storage_default || inl then
             error loc "Non-default storage or 'inline' on 'struct' or 'union' declaration";
           ([], env')
    diff --git a/cparser/Env.ml b/cparser/Env.ml
    index 777b3e1..1f41c0c 100644
    a b type composite_info = { 
    7070(* Infos associated with an ordinary identifier *)
    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
    7676(* Infos associated with a typedef *)
    let find_typedef env id = 
    201201
    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 =
    210210  let id = fresh_ident s in
    let enter_typedef env s info = 
    220220
    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 =
    227227  { env with env_tag = IdentMap.add id ci env.env_tag }
  • cparser/Env.mli

    diff --git a/cparser/Env.mli b/cparser/Env.mli
    index e7a74af..a9daa21 100644
    a b type composite_info = { 
    3131  ci_sizeof: int option;                (* size; None if incomplete *)
    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
    3737
    val find_struct_member : t -> C.ident * string -> C.field 
    6060val find_union_member : t -> C.ident * string -> C.field
    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
  • cparser/GCC.ml

    diff --git a/cparser/GCC.ml b/cparser/GCC.ml
    index 9f864dc..17f3cfa 100644
    a b let ulongLongType = TInt(IULongLong, []) 
    3030let floatType = TFloat(FFloat, [])
    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
    4040let builtins = {
    let builtins = { 
    150150  "__builtin_log10l",  (longDoubleType, [ longDoubleType ], false);
    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
    158158  "__builtin_nan",  (doubleType, [ charConstPtrType ], false);
  • cparser/Lexer.mll

    diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll
    index d4947ad..d3f3958 100644
    a b let init_lexicon _ = 
    181181      ("__builtin_types_compatible_p", fun loc -> BUILTIN_TYPES_COMPAT loc);
    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
    187193(* Mark an identifier as a type name. The old mapping is preserved and will
  • cparser/Parser.mly

    diff --git a/cparser/Parser.mly b/cparser/Parser.mly
    index 0eebb84..abec574 100644
    a b let transformOffsetOf (speclist, dtype) member = 
    221221%token<Cabs.cabsloc> VOLATILE EXTERN STATIC CONST RESTRICT AUTO REGISTER
    222222%token<Cabs.cabsloc> THREAD
    223223
     224%token<Cabs.cabsloc> DATA IDATA PDATA XDATA CODE
     225
    224226%token<Cabs.cabsloc> SIZEOF ALIGNOF
    225227
    226228%token EQ PLUS_EQ MINUS_EQ STAR_EQ SLASH_EQ PERCENT_EQ
    attribute_nocv: 
    12491251|   MSATTR                              { (fst $1, []), snd $1 }
    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
    12541262attribute_nocv_list:
  • cparser/Rename.ml

    diff --git a/cparser/Rename.ml b/cparser/Rename.ml
    index 4b2f350..b6de8cd 100644
    a b let ident env id = 
    7575                       id.name id.stamp
    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) ->
    8282      let (p', _) = mmap param env p in
    let constant env = function 
    9797  | cst -> cst
    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
    103103  | EConst cst -> EConst(constant env cst)
    let rec globdecl env g = 
    191191  ( { gdesc = desc'; gloc = g.gloc }, env' )
    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
    199199      (Gfundef fd', env')
    let rec reserve_public env = function 
    230230  | dcl :: rem ->
    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
    236236            | Storage_static -> env
  • cparser/SimplExpr.ml

    diff --git a/cparser/SimplExpr.ml b/cparser/SimplExpr.ml
    index 330b184..8202cb2 100644
    a b let simpl_expr loc env e act = 
    9292
    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
    103104  let sif e s1 s2 =
    let simpl_expr loc env e act = 
    149150
    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 ->
    163164            let (s1, e1') = simpl e1 LHS in
    let simpl_expr loc env e act = 
    165166            let op' = match op with Opreincr -> Oadd | _ -> Osub in
    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 ->
    171172                (sseq s1 (sseq s2 (sassign e1' e3)), voidconst)
    let simpl_expr loc env e act = 
    184185            | 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
    195196            end
    let simpl_expr loc env e act = 
    205206            let (s1, e1') = simpl e1 RHS in
    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 ->
    211212            if act = Drop && is_simpl_expr e1 then
    let simpl_expr loc env e act = 
    239240              | Oshl_assign -> Oshl    | Oshr_assign -> Oshr
    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 ->
    245246                (sseq s1 (sseq s11 (sseq s2 (sassign e1' e3))), voidconst)
    let simpl_expr loc env e act = 
    259260            let (s1, e1') = simpl e1 RHS in
    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
    265266              | Drop ->
    let simpl_expr loc env e act = 
    284285            let (s1, e1') = simpl e1 RHS in
    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
    290291              | Drop ->
    let simpl_expr loc env e act = 
    310311    | EConditional(e1, e2, e3) ->
    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
    316317          | Drop ->
    let simpl_expr loc env e act = 
    336337            simpl e1 act
    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
    342343    | ECall(e1, el) ->
    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 ->
    348349            (sseq s1 (sseq s2 {sdesc = Sdo e2; sloc=loc}), voidconst)
    let simpl_statement env s = 
    481482        let (s', _) = simpl_expr s.sloc env e (Set tmp) in
    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}
    487488      end
  • cparser/StructAssign.ml

    diff --git a/cparser/StructAssign.ml b/cparser/StructAssign.ml
    index f5cecfc..5af7bed 100644
    a b let maxsize = ref 8 
    2828let need_memcpy = ref (None: ident option)
    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, [])
    3636
    let memcpy_ident () = 
    4343  | Some id ->
    4444      id
    4545
     46let space_of_ty = function
     47| TArray(space, _, _, _)
     48| TPtr(space, _, _) -> space
     49| _ -> Any
     50
    4651let transf_assign env loc lhs rhs =
    4752
    4853  let num_assign = ref 0 in
    let transf_assign env loc lhs rhs = 
    6267        transf_struct l r ci.ci_members
    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 *)
    7075    | _ ->
    let transf_assign env loc lhs rhs = 
    7378  and transf_struct l r = function
    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
    8893
    8994  try
    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
    100106let rec transf_stmt env s =
    let program p = 
    136142  match !need_memcpy with
    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
    142148(* Horrible hack *)
  • cparser/StructByValue.ml

    diff --git a/cparser/StructByValue.ml b/cparser/StructByValue.ml
    index de79737..60e088b 100644
    a b let rec transf_type env t = 
    3838      let tres' = transf_type env tres in
    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
    5252and transf_funarg env (id, t) =
    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
    5858(* Simple exprs: no change in structure, since calls cannot occur within,
    and transf_funarg env (id, t) = 
    6060
    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
    6566      | ESizeof ty -> ESizeof (transf_type env ty)
    and transf_expr e = transf_expr env e in 
    104105let transf_arg e =
    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
    110111
    in 
    118119let rec transf_stmt s =
    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
    133134      let args = List.map transf_arg args 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)}
    142143  | Sseq(s1, s2) ->
    let transf_params loc env params = 
    184185      let ty = transf_type env ty in
    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
    197199        let (params', decls, init) = transf_prm params in
    let transf_fundef env f = 
    206208  let (ret1, params1, body1) =
    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,
    214216       transf_funbody env f.fd_body (Some eeres))
  • cparser/Transform.ml

    diff --git a/cparser/Transform.ml b/cparser/Transform.ml
    index b7f57f3..1a9dd20 100644
    a b let new_temp_var ?(name = "t") ty = 
    3333
    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 () =
    3939  let temps = !temporaries in
    let program 
    5858  | g :: gl ->
    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),
    6868             Env.add_composite env id (composite_info_decl env su))
  • cparser/Unblock.ml

    diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
    index fa304b7..d19940a 100644
    a b let rec local_initializer loc env path init k = 
    3232  match init with
    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
    4343      let rec array_init pos = function
    4444        | [] -> k
    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
    5152      array_init 0L il
    5253  | Init_struct(id, fil) ->
    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
    6364(* Record new variables to be locally defined *)
    let process_decl loc env (sto, id, ty, optinit) k = 
    8283  match optinit with
    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 *)
    8889
  • src/acc.ml

    diff --git a/src/acc.ml b/src/acc.ml
    index c8f6592..e2f782c 100644
    a b let process filename = 
    3333      src_language tgt_language input_ast
    3434  in
    3535  let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in
    36   let annotated_input_ast =  Languages.annotate input_ast final_ast in
    37   Languages.save filename annotated_input_ast;
     36  if Options.annotation_requested () then begin
     37    let annotated_input_ast =  Languages.annotate input_ast final_ast in
     38    Languages.save filename annotated_input_ast
     39  end;
    3840  Languages.save filename final_ast;
    3941  if Options.is_debug_enabled () then
    4042    List.iter (Languages.save filename) intermediate_asts;
     43  if Options.is_matita_output_enabled () then
     44    Languages.save_matita filename (input_ast :: target_asts);
    4145  if Options.interpretation_requested () || Options.is_debug_enabled () then begin
    4246    let asts = input_ast :: target_asts in
    4347    let label_traces = List.map Languages.interpret asts in
  • src/clight/clight.mli

    diff --git a/src/clight/clight.mli b/src/clight/clight.mli
    index 4c9d638..b831ef0 100644
    a b open AST 
    77
    88(** ** Types *)
    99
     10type memory_space = Any | Data | IData | PData | XData | Code
     11
    1012(** Clight types are similar to those of C.  They include numeric types,
    1113  pointers, arrays, function types, and composite types (struct and
    1214  union).  Numeric types (integers and floats) fully specify the
    type ctype = 
    6163  | Tvoid                                       (**r the [void] type *)
    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
    6870  (**r struct types *)
    type init_data = 
    199201type program = {
    200202  prog_funct: (ident * fundef) list ;
    201203  prog_main: ident;
    202   prog_vars: ((ident * init_data list) * ctype) list
     204  prog_vars: (((ident * init_data list) * memory_space) * ctype) list
    203205}
  • src/clight/clightFromC.ml

    diff --git a/src/clight/clightFromC.ml b/src/clight/clightFromC.ml
    index 0aacbce..0a4b947 100644
    a b let rec alignof = function 
    1919  | Tfloat F32 -> 4
    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
    2525  | Tunion (_,fld) -> alignof_fields fld
    let rec sizeof t = 
    4242    | Tfloat F32 -> 4
    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)
    4848    | Tunion (_,fld) -> align (max 1 (sizeof_union fld)) (alignof t)
    let name_for_string_literal env s = 
    102102    Hashtbl.add decl_atom id
    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;
    108108    Hashtbl.add stringTable s id;
    109109    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 =
    115115  let init = ref [] in
    let global_for_string s id = 
    119119       :: !init in
    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 =
    125125  Hashtbl.fold
    let register_stub_function name tres targs = 
    143143    let rec types_of_types = function
    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;
    149149    (stub_name, stub_type)
    let convertFkind = function 
    193193      if not !ClightFlags.option_flonglong then unsupported "'long double' 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
    198206  let rec convertTyp seen t =
    let convertTyp env t = 
    202210        let (sg, sz) = convertIkind ik in Tint(sz, sg)
    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";
    220228        if Cutil.is_composite_type env tres then
    let rec convertExpr env e = 
    298306      let e1' = convertExpr env e1 in
    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),
    304312                   id), ty)
    let rec convertExpr env e = 
    315323
    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)
    321329  | C.EBinop(C.Ologor, e1, e2, _) ->
    let rec convertExpr env e = 
    354362let rec projFunType env 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
    360368let convertFuncall env lhs fn args =
    let volatile_fun_suffix_type ty = 
    400408  | Tfloat F32 -> ("float32", ty)
    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)
    406414
    407415let volatile_read_fun ty =
    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 *)
    418426
    let convertTopExpr env e = 
    432440      | false, true ->                  (* volatile read *)
    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)
    442450      end
    let convertInit env ty init = 
    663671  | Init_array il ->
    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
    669677  | Init_struct(_, flds) ->
    let convertInit env ty init = 
    690698
    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
    696704  let init' =
    let convertGlobvar env (sto, id, ty, optinit as decl) = 
    701709        convertInit env ty i 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.
    707715  Result is a pair [(funs, vars)] where [funs] are
    let rec convertGlobdecls env funs vars gl = 
    714722  | g :: gl' ->
    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.
    720728             Other types become variable declarations. *)
    let rec convertGlobdecls env funs vars gl = 
    727735          | TFun(_, _, true, _) ->
    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 ->
    733741          convertGlobdecls env (convertFundef env fd :: funs) vars gl'
    let cleanupGlobals p = 
    769777    | g :: gl ->
    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);
    779787            clean (IdentSet.add id defs) (g :: accu) gl
    let rec type_is_readonly env t = 
    815823  if List.mem C.AVolatile a then false else
    816824  if List.mem C.AConst a then true else
    817825  match Cutil.unroll env t with
    818   | C.TArray(t', _, _) -> type_is_readonly env t'
     826  | C.TArray(_, t', _, _) -> type_is_readonly env t'
    819827  | _ -> false
    820828
    821829let atom_is_static a =
    open Builtins 
    853861let builtins_generic = {
    854862  typedefs = [
    855863    (* keeps GCC-specific headers happy, harmless for others *)
    856     "__builtin_va_list", C.TPtr(C.TVoid [], [])
     864    "__builtin_va_list", C.TPtr(C.Any, C.TVoid [], [])
    857865  ];
    858866  functions = [
    859867    (* The volatile read/volatile write functions *)
    860868    "__builtin_volatile_read_int8unsigned",
    861         (TInt(IUChar, []), [TPtr(TVoid [], [])], false);
     869        (TInt(IUChar, []), [TPtr(C.Any, TVoid [], [])], false);
    862870    "__builtin_volatile_read_int8signed",
    863         (TInt(ISChar, []), [TPtr(TVoid [], [])], false);
     871        (TInt(ISChar, []), [TPtr(C.Any, TVoid [], [])], false);
    864872    "__builtin_volatile_read_int16unsigned",
    865         (TInt(IUShort, []), [TPtr(TVoid [], [])], false);
     873        (TInt(IUShort, []), [TPtr(C.Any, TVoid [], [])], false);
    866874    "__builtin_volatile_read_int16signed",
    867         (TInt(IShort, []), [TPtr(TVoid [], [])], false);
     875        (TInt(IShort, []), [TPtr(C.Any, TVoid [], [])], false);
    868876    "__builtin_volatile_read_int32",
    869         (TInt(IInt, []), [TPtr(TVoid [], [])], false);
     877        (TInt(IInt, []), [TPtr(C.Any, TVoid [], [])], false);
    870878    "__builtin_volatile_read_float32",
    871         (TFloat(FFloat, []), [TPtr(TVoid [], [])], false);
     879        (TFloat(FFloat, []), [TPtr(C.Any, TVoid [], [])], false);
    872880    "__builtin_volatile_read_float64",
    873          (TFloat(FDouble, []), [TPtr(TVoid [], [])], false);
     881         (TFloat(FDouble, []), [TPtr(C.Any, TVoid [], [])], false);
    874882    "__builtin_volatile_read_pointer",
    875          (TPtr(TVoid [], []), [TPtr(TVoid [], [])], false);
     883         (TPtr(C.Any, TVoid [], []), [TPtr(C.Any, TVoid [], [])], false);
    876884    "__builtin_volatile_write_int8unsigned",
    877         (TVoid [], [TPtr(TVoid [], []); TInt(IUChar, [])], false);
     885        (TVoid [], [TPtr(C.Any, TVoid [], []); TInt(IUChar, [])], false);
    878886    "__builtin_volatile_write_int8signed",
    879         (TVoid [], [TPtr(TVoid [], []); TInt(ISChar, [])], false);
     887        (TVoid [], [TPtr(C.Any, TVoid [], []); TInt(ISChar, [])], false);
    880888    "__builtin_volatile_write_int16unsigned",
    881         (TVoid [], [TPtr(TVoid [], []); TInt(IUShort, [])], false);
     889        (TVoid [], [TPtr(C.Any, TVoid [], []); TInt(IUShort, [])], false);
    882890    "__builtin_volatile_write_int16signed",
    883         (TVoid [], [TPtr(TVoid [], []); TInt(IShort, [])], false);
     891        (TVoid [], [TPtr(C.Any, TVoid [], []); TInt(IShort, [])], false);
    884892    "__builtin_volatile_write_int32",
    885         (TVoid [], [TPtr(TVoid [], []); TInt(IInt, [])], false);
     893        (TVoid [], [TPtr(C.Any, TVoid [], []); TInt(IInt, [])], false);
    886894    "__builtin_volatile_write_float32",
    887         (TVoid [], [TPtr(TVoid [], []); TFloat(FFloat, [])], false);
     895        (TVoid [], [TPtr(C.Any, TVoid [], []); TFloat(FFloat, [])], false);
    888896    "__builtin_volatile_write_float64",
    889          (TVoid [], [TPtr(TVoid [], []); TFloat(FDouble, [])], false);
     897         (TVoid [], [TPtr(C.Any, TVoid [], []); TFloat(FDouble, [])], false);
    890898    "__builtin_volatile_write_pointer",
    891          (TVoid [], [TPtr(TVoid [], []); TPtr(TVoid [], [])], false)
     899         (TVoid [], [TPtr(C.Any, TVoid [], []); TPtr(C.Any, TVoid [], [])], false)
    892900  ]
    893901}
    894902
  • src/clight/clightInterpret.ml

    diff --git a/src/clight/clightInterpret.ml b/src/clight/clightInterpret.ml
    index 32b9884..b744932 100644
    a b let rec sizeof = function 
    2929  | Tfloat F32 -> 4
    3030  | Tfloat F64 -> 8
    3131  | Tpointer _ -> 4                     
    32   | Tarray (_,_) -> 4                     
     32  | Tarray _ -> 4                         
    3333  | Tfunction (_,_) -> assert false
    3434  | Tstruct (_,_) -> assert false
    3535  | Tunion (_,_) -> assert false
    let rec mq_of_ty = function 
    4646  | Tfloat F32 -> assert false
    4747  | Tfloat F64 -> Memory.MQ_float64
    4848  | Tpointer _ -> Memory.MQ_int32                       
    49   | Tarray (c,s) -> Memory.MQ_int32
     49  | Tarray (_,c,s) -> Memory.MQ_int32
    5050  | Tfunction (_,_) -> assert false
    5151  | Tstruct (_,_) -> assert false
    5252  | Tunion (_,_) -> assert false
    let eval_cast = function 
    207207  | (Value.Val_float f,_,Tfloat F64) -> Value.Val_float f
    208208  (* Cast pointeur *)
    209209  | (Value.Val_ptr (b,o),_,Tpointer _) -> Value.Val_ptr (b,o)
    210   | (Value.Val_ptr (b,o),_,Tarray(_,_)) -> Value.Val_ptr (b,o)
     210  | (Value.Val_ptr (b,o),_,Tarray _) -> Value.Val_ptr (b,o)
    211211  (* no cast *)
    212212  | (e,a,b) when a=b -> e
    213213  (* error *)
    let eval_add = function 
    232232      Value.Val_int (cast_int (i1+i2) t1)     
    233233  | ((Value.Val_float i1,Tfloat F64) , (Value.Val_float i2,Tfloat F64)) ->
    234234      Value.Val_float (i1+.i2)
    235   | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tarray(t,_))) ->
     235  | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tarray(_,t,_))) ->
    236236      Value.Val_ptr (b,o+(i*(sizeof t)))
    237   | ((Value.Val_ptr (b,o),Tarray(t,_)) , (Value.Val_int i,_)) ->
     237  | ((Value.Val_ptr (b,o),Tarray(_,t,_)) , (Value.Val_int i,_)) ->
    238238      Value.Val_ptr (b,o+(i*(sizeof t)))
    239   | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tpointer t)) ->
     239  | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tpointer (_,t))) ->
    240240      Value.Val_ptr (b,o+(i*(sizeof t)))
    241   | ((Value.Val_ptr (b,o),Tpointer t) , (Value.Val_int i,_)) ->
     241  | ((Value.Val_ptr (b,o),Tpointer (_,t)) , (Value.Val_int i,_)) ->
    242242      Value.Val_ptr (b,o+(i*(sizeof t)))
    243243  | ((v1,_),(v2,_)) ->
    244244      print_string ("Debug: add "^(Value.string_of_value v1)^" with "
    let eval_sub = function 
    250250      Value.Val_int (cast_int (i1-i2) t1)   
    251251  | ((Value.Val_float i1,Tfloat F64) , (Value.Val_float i2,Tfloat F64)) ->
    252252      Value.Val_float (i1-.i2)
    253   | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tarray(t,_))) ->
     253  | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tarray(_,t,_))) ->
    254254      Value.Val_ptr (b,o-(i*(sizeof t)))
    255   | ((Value.Val_ptr (b,o),Tarray(t,_)) , (Value.Val_int i,_)) ->
     255  | ((Value.Val_ptr (b,o),Tarray(_,t,_)) , (Value.Val_int i,_)) ->
    256256      Value.Val_ptr (b,o-(i*(sizeof t)))
    257   | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tpointer t)) ->
     257  | ((Value.Val_int i,_) , (Value.Val_ptr (b,o),Tpointer (_,t))) ->
    258258      Value.Val_ptr (b,o-(i*(sizeof t)))
    259   | ((Value.Val_ptr (b,o),Tpointer t) , (Value.Val_int i,_)) ->
     259  | ((Value.Val_ptr (b,o),Tpointer (_,t)) , (Value.Val_int i,_)) ->
    260260      Value.Val_ptr (b,o-(i*(sizeof t)))
    261261  | _ -> assert false
    262262
    let bind_parameters m (param_l:(ident*ctype) list) (arg_l:Value.t list) (var_l:( 
    475475    | _ -> assert false
    476476  and treat_v (m,e) = function
    477477    | [] -> (m,e)
    478     | (id,Tarray(c,n))::l ->
     478    | (id,Tarray(s,c,n))::l ->
    479479        (match alloc m 0 (n*(sizeof c)) with
    480            | Some(b,m') -> treat_v (bind m' e (id,Tarray(c,n)) (Value.Val_ptr(b,0)) ) l
     480           | Some(b,m') -> treat_v (bind m' e (id,Tarray(s,c,n)) (Value.Val_ptr(b,0)) ) l
    481481           | None -> assert false)
    482482    | var::l -> treat_v (bind m e var Value.Val_undef) l
    483483  in treat_v (treat_p (m,(Hashtbl.create 11)) (param_l,arg_l)) var_l
  • new file src/clight/clightPrintMatita.ml

    diff --git a/src/clight/clightPrintMatita.ml b/src/clight/clightPrintMatita.ml
    new file mode 100644
    index 0000000..948ef87
    - +  
     1(* *********************************************************************)
     2(*                                                                     *)
     3(*              The Compcert verified compiler                         *)
     4(*                                                                     *)
     5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
     6(*                                                                     *)
     7(*  Copyright Institut National de Recherche en Informatique et en     *)
     8(*  Automatique.  All rights reserved.  This file is distributed       *)
     9(*  under the terms of the GNU General Public License as published by  *)
     10(*  the Free Software Foundation, either version 2 of the License, or  *)
     11(*  (at your option) any later version.  This file is also distributed *)
     12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
     13(*                                                                     *)
     14(* *********************************************************************)
     15
     16(** Pretty-printer for Csyntax *)
     17
     18open Format
     19open AST
     20open Clight
     21
     22(* If there's name hiding this might get us into trouble. *)
     23let ident_map = Hashtbl.create 13;;
     24let ident_next = ref 0;;
     25let id_i n =
     26  try Hashtbl.find ident_map n
     27  with Not_found ->
     28    let i = !ident_next in
     29    Hashtbl.add ident_map n i;
     30    ident_next := i+1;
     31    i
     32let id_s n = string_of_int (id_i n)
     33
     34let print_list f fmt l =
     35  let rec aux fmt = function
     36      | [] -> ()
     37      | [x] -> f fmt x
     38      | h::t -> f fmt h; fprintf fmt ";@ "; aux fmt t
     39  in
     40  fprintf fmt "@[[%a]@]" aux l
     41
     42let name_unop = function
     43  | Onotbool -> "Onotbool"
     44  | Onotint  -> "Onotint"
     45  | Oneg     -> "Oneg"
     46
     47
     48let name_binop = function
     49  | Oadd -> "Oadd"
     50  | Osub -> "Osub"
     51  | Omul -> "Omul"
     52  | Odiv -> "Odiv"
     53  | Omod -> "Omod"
     54  | Oand -> "Oand"
     55  | Oor  -> "Oor"
     56  | Oxor -> "Oxor"
     57  | Oshl -> "Oshl"
     58  | Oshr -> "Oshr"
     59  | Oeq  -> "Oeq"
     60  | One  -> "One"
     61  | Olt  -> "Olt"
     62  | Ogt  -> "Ogt"
     63  | Ole  -> "Ole"
     64  | Oge  -> "Oge"
     65
     66let name_inttype sz sg =
     67  match sz, sg with
     68  | I8, Signed    -> "I8 Signed   "
     69  | I8, Unsigned  -> "I8 Unsigned "
     70  | I16, Signed   -> "I16 Signed  "
     71  | I16, Unsigned -> "I16 Unsigned"
     72  | I32, Signed   -> "I32 Signed  "
     73  | I32, Unsigned -> "I32 Unsigned"
     74
     75let name_floattype sz =
     76  match sz with
     77  | F32 -> "F32"
     78  | F64 -> "F64"
     79
     80(* Collecting the names and fields of structs and unions *)
     81
     82module StructUnionSet = Set.Make(struct
     83  type t = string * (ident*ctype) list
     84  let compare (n1, _ : t) (n2, _ : t) = compare n1 n2
     85end)
     86
     87let struct_unions = ref StructUnionSet.empty
     88
     89let register_struct_union id fld =
     90  struct_unions := StructUnionSet.add (id, fld) !struct_unions
     91
     92(* Declarator (identifier + type) *)
     93
     94let name_optid id =
     95  if id = "" then "" else " " ^ id
     96
     97let parenthesize_if_pointer id =
     98  if String.length id > 0 && id.[0] = '*' then "(" ^ id ^ ")" else id
     99
     100let rec name_cdecl id ty =
     101  match ty with
     102  | Tvoid ->
     103      "void" ^ name_optid id
     104  | Tint(sz, sg) ->
     105      name_inttype sz sg ^ name_optid id
     106  | Tfloat sz ->
     107      name_floattype sz ^ name_optid id
     108  | Tpointer (s,t) -> (* XXX *)
     109      name_cdecl ("*" ^ id) t
     110  | Tarray(s, t, n) -> (* XXX *)
     111      name_cdecl
     112        (sprintf "%s[%d]" (parenthesize_if_pointer id) n)
     113        t
     114  | Tfunction(args, res) ->
     115      let b = Buffer.create 20 in
     116      if id = ""
     117      then Buffer.add_string b "(*)"
     118      else Buffer.add_string b (parenthesize_if_pointer id);
     119      Buffer.add_char b '(';
     120      begin match args with
     121      | [] ->
     122          Buffer.add_string b "void"
     123      | _ ->
     124          let rec add_args first = function
     125          | [] -> ()
     126          | t1::tl ->
     127              if not first then Buffer.add_string b ", ";
     128              Buffer.add_string b (name_cdecl "" t1);
     129              add_args false tl in
     130          add_args true args
     131      end;
     132      Buffer.add_char b ')';
     133      name_cdecl (Buffer.contents b) res
     134  | Tstruct(name, fld) ->
     135      name ^ name_optid id
     136  | Tunion(name, fld) ->
     137      name ^ name_optid id
     138  | Tcomp_ptr name ->
     139      name ^ " *" ^ id
     140
     141(* Type *)
     142
     143let sspace = function
     144| Any -> "Any"
     145| Data -> "Data"
     146| IData -> "IData"
     147| PData -> "PData"
     148| XData -> "XData"
     149| Code -> "Code"
     150
     151let rec stype ty =
     152  match ty with
     153  | Tvoid -> "Tvoid"
     154  | Tint(sz, sg) -> "(Tint " ^ name_inttype sz sg ^ ")"
     155  | Tfloat sz -> "(Tfloat " ^ name_floattype sz ^ ")"
     156  | Tpointer (sp, t) -> "(Tpointer " ^ sspace sp ^ " " ^ stype t ^ ")"
     157  | Tarray(sp, t, n) -> "(Tarray " ^ sspace sp ^ " " ^ stype t ^ " " ^ (string_of_int n) ^ ")"
     158  | Tfunction(args, res) -> "(Tfunction " ^ typelist args ^ " " ^ stype res ^ ")"
     159  | Tstruct(name, fld) ->
     160      fieldlist "(Tstruct (succ_pos_of_nat " name fld
     161  | Tunion(name, fld) ->
     162      fieldlist "(Tunion (succ_pos_of_nat " name fld
     163  | Tcomp_ptr name ->
     164      "(Tcomp_ptr (succ_pos_of_nat " ^ id_s name ^ "))"
     165 and typelist l =
     166    let b = Buffer.create 20 in
     167      let rec add_types = function
     168        | [] -> Buffer.add_string b "Tnil"
     169        | t1::tl ->
     170            Buffer.add_string b "(Tcons ";
     171            Buffer.add_string b (stype t1);
     172            Buffer.add_char b ' ';
     173            add_types tl;
     174            Buffer.add_char b ')'
     175      in add_types l;
     176        Buffer.contents b
     177 and fieldlist s name l =
     178    let b = Buffer.create 20 in
     179      Buffer.add_string b s;
     180      Buffer.add_string b (id_s name);
     181      Buffer.add_string b ") ";
     182      let rec add_fields = function
     183        | [] -> Buffer.add_string b "Fnil"
     184        | (id, ty)::tl ->
     185            Buffer.add_string b "(Fcons (succ_pos_of_nat ";
     186            Buffer.add_string b (id_s id);
     187            Buffer.add_string b ") ";
     188            Buffer.add_string b (stype ty);
     189            Buffer.add_char b ' ';
     190            add_fields tl;
     191            Buffer.add_char b ')'
     192      in add_fields l;
     193        Buffer.add_char b ')';
     194        Buffer.contents b
     195
     196let name_type ty = name_cdecl "" ty
     197
     198(* Expressions *)
     199
     200let rec print_expr p (Expr (eb, ty)) =
     201  fprintf p "@[<hov 2>(Expr %a@ %s)@]" print_expr_descr eb (stype ty)
     202and print_expr_descr p eb =
     203  match eb with
     204  | Ecost (_, Expr (e, _)) -> print_expr_descr p e
     205  | Econst_int n ->
     206      fprintf p "(Econst_int (repr %d))" n
     207  | Econst_float f ->
     208      fprintf p "(Econst_float %F)" f
     209  | Evar id ->
     210      fprintf p "(Evar (succ_pos_of_nat %d))" (id_i id)
     211  | Eunop(op, e1) ->
     212      fprintf p "(Eunop %s %a)" (name_unop op) print_expr e1
     213  | Ederef e ->
     214      fprintf p "(Ederef@ %a)" print_expr e
     215  | Eaddrof e ->
     216      fprintf p "(Eaddrof@ %a)" print_expr e
     217  | Ebinop(op, e1, e2) ->
     218      fprintf p "(Ebinop@ %s@ %a@ %a)"
     219                (name_binop op)
     220                print_expr e1
     221                print_expr e2
     222  | Ecast(ty, e1) ->
     223      fprintf p "(Ecast %s@ %a)"
     224                (stype ty)
     225                print_expr e1
     226  | Econdition(e1, e2, e3) ->
     227      fprintf p "(Econdition %a@ %a@ %a)"
     228                print_expr e1
     229                print_expr e2
     230                print_expr e3
     231  | Eandbool(e1, e2) ->
     232      fprintf p "(Eandbool %a@ %a)"
     233                print_expr e1
     234                print_expr e2
     235  | Eorbool(e1, e2) ->
     236      fprintf p "(Eorbool %a@ %a)"
     237                print_expr e1
     238                print_expr e2
     239  | Esizeof ty ->
     240      fprintf p "(Esizeof %s)" (stype ty)
     241  | Efield(e1, id) ->
     242      fprintf p "(Efield %a (succ_pos_of_nat %i))" print_expr e1 (id_i id)
     243
     244let rec print_expr_list p (first, el) =
     245  match el with
     246  | [] -> ()
     247  | e1 :: et ->
     248      if not first then fprintf p ",@ ";
     249      print_expr p e1;
     250      print_expr_list p (false, et)
     251
     252let rec print_stmt p s =
     253  match s with
     254  | Scost (_, s') -> print_stmt p s'
     255  | Sskip ->
     256      fprintf p "Sskip"
     257  | Sassign(e1, e2) ->
     258      fprintf p "@[<hv 2>(Sassign %a@ %a)@]" print_expr e1 print_expr e2
     259  | Scall(None, e1, el) ->
     260      fprintf p "@[<hv 2>(Scall (None ?) %a @[<hov 0>%a@])@]"
     261                print_expr e1
     262                (print_list print_expr) el
     263  | Scall(Some lhs, e1, el) ->
     264      fprintf p "@[<hv 2>(Scall (Some ? %a)@ %a@ @[<hov 0>%a@])@]"
     265                print_expr lhs
     266                print_expr e1
     267                (print_list print_expr) el
     268  | Ssequence(s1, s2) ->
     269      fprintf p "(Ssequence@ %a@ %a)" print_stmt s1 print_stmt s2
     270  | Sifthenelse(e, s1, s2) ->
     271      fprintf p "@[<v 2>(Sifthenelse %a@ %a@ %a)@]"
     272              print_expr e
     273              print_stmt s1
     274              print_stmt s2
     275  | Swhile(e, s) ->
     276      fprintf p "@[<v 2>(Swhile %a@ %a)@]"
     277              print_expr e
     278              print_stmt s
     279  | Sdowhile(e, s) ->
     280      fprintf p "@[<v 2>S(dowhile %a@ %a)@]"
     281              print_expr e
     282              print_stmt s
     283  | Sfor(s_init, e, s_iter, s_body) ->
     284      fprintf p "@[<v 2>(Sfor %a@ %a@ %a@\n%a@;<0 -2>)@]"
     285              print_stmt s_init
     286              print_expr e
     287              print_stmt s_iter
     288              print_stmt s_body
     289  | Sbreak ->
     290      fprintf p "Sbreak"
     291  | Scontinue ->
     292      fprintf p "Scontinue"
     293  | Sswitch(e, cases) ->
     294      fprintf p "@[<v 2>(Sswitch %a (@ %a@;<0 -2>))@]"
     295              print_expr e
     296              print_cases cases
     297  | Sreturn None ->
     298      fprintf p "(Sreturn (None ?))"
     299  | Sreturn (Some e) ->
     300      fprintf p "(Sreturn (Some ? %a))" print_expr e
     301  | Slabel(lbl, s1) ->
     302      fprintf p "(Slabel (succ_pos_of_nat %i)@ %a)" (id_i lbl) print_stmt s1
     303  | Sgoto lbl ->
     304      fprintf p "(Sgoto (succ_pos_of_nat %i))" (id_i lbl)
     305
     306and print_cases p cases =
     307  match cases with
     308  | LSdefault s ->
     309      fprintf p "@[<v 2>(LSdefault@ %a)@]" print_stmt s
     310  | LScase(lbl, s, rem) ->
     311      fprintf p "@[<v 2>(LScase (repr %d)@ %a@ %a)@]"
     312              lbl
     313              print_stmt s
     314              print_cases rem
     315
     316let name_function_parameters params =
     317  let b = Buffer.create 20 in
     318  Buffer.add_char b '[';
     319    let rec add_params first = function
     320      | [] -> ()
     321      | (id, ty) :: rem ->
     322          if not first then Buffer.add_string b "; ";
     323          Buffer.add_string b "mk_pair ?? (succ_pos_of_nat ";
     324          Buffer.add_string b (id_s id);
     325          Buffer.add_string b ") ";
     326          Buffer.add_string b (stype ty);
     327          add_params false rem in
     328      add_params true params;
     329      Buffer.add_char b ']';
     330      Buffer.contents b
     331
     332let print_function p f =
     333  fprintf p "@[<v 2>mk_function %s %s %s@ " (stype f.fn_return)
     334    (name_function_parameters f.fn_params)
     335    (name_function_parameters f.fn_vars);
     336  print_stmt p f.fn_body;
     337  fprintf p "@;<0 -2>@]@ @ "
     338
     339let print_fundef p (id, fd) =
     340  fprintf p "@[<v 2>mk_pair ?? (succ_pos_of_nat %i (* %s *)) " (id_i id) id;
     341  match fd with
     342  | External(id', args, res) ->
     343      fprintf p "(External (succ_pos_of_nat %i) %s %s)@]" (id_i id) (typelist args) (stype res)
     344  | Internal f ->
     345      fprintf p "(Internal (@ %a@;<0 -2>))@]" print_function f
     346
     347let string_of_init id =
     348  let b = Buffer.create (List.length id) in
     349  let add_init = function
     350  | Init_int8 c ->
     351      if c >= 32 && c <= 126 && c <> Char.code '\"' && c <> Char.code '\\'
     352      then Buffer.add_char b (Char.chr c)
     353      else Buffer.add_string b (Printf.sprintf "\\%03o" c)
     354  | _ ->
     355      assert false
     356  in List.iter add_init id; Buffer.contents b
     357
     358let chop_last_nul id =
     359  match List.rev id with
     360  | Init_int8 0 :: tl -> List.rev tl
     361  | _ -> id
     362
     363let print_init p = function
     364  | Init_int8 n -> fprintf p "(Init_int8 (repr %d))@ " n
     365  | Init_int16 n -> fprintf p "(Init_int16 (repr %d))@ " n
     366  | Init_int32 n -> fprintf p "(Init_int32 (repr %d))@ " n
     367  | Init_float32 n -> fprintf p "(Init_float32 %F)@ " n
     368  | Init_float64 n -> fprintf p "(Iinit_float64 %F)@ " n
     369  | Init_space n -> fprintf p "(Init_space %d)@ " n
     370  | Init_addrof(symb, ofs) -> fprintf p "(Init_addrof %d (repr %d))" (id_i symb) ofs
     371
     372let re_string_literal = Str.regexp "__stringlit_[0-9]+"
     373
     374let print_globvar p ((((id, init), sp), ty)) =
     375  fprintf p "@[<hov 2>(mk_pair ?? (mk_pair ?? (mk_pair ?? (succ_pos_of_nat %i (* %s *))@ %a)@ %s)@ %s)@]"
     376    (id_i id)
     377    id
     378    (print_list print_init) init
     379    (sspace sp)
     380    (stype ty)
     381
     382(* Collect struct and union types *)
     383
     384let rec collect_type = function
     385  | Tvoid -> ()
     386  | Tint(sz, sg) -> ()
     387  | Tfloat sz -> ()
     388  | Tpointer (_,t) -> collect_type t
     389  | Tarray(_, t, n) -> collect_type t
     390  | Tfunction(args, res) -> List.iter collect_type args; collect_type res
     391  | Tstruct(id, fld) -> register_struct_union id fld; List.iter collect_field fld
     392  | Tunion(id, fld) -> register_struct_union id fld; List.iter collect_field fld
     393  | Tcomp_ptr _ -> ()
     394
     395and collect_field f = collect_type (snd f)
     396
     397let rec collect_expr (Expr(ed, ty)) =
     398  match ed with
     399  | Ecost (_, e) -> collect_expr e
     400  | Econst_int n -> ()
     401  | Econst_float f -> ()
     402  | Evar id -> ()
     403  | Eunop(op, e1) -> collect_expr e1
     404  | Ederef e -> collect_expr e
     405  | Eaddrof e -> collect_expr e
     406  | Ebinop(op, e1, e2) -> collect_expr e1; collect_expr e2
     407  | Ecast(ty, e1) -> collect_type ty; collect_expr e1
     408  | Econdition(e1, e2, e3) -> collect_expr e1; collect_expr e2; collect_expr e3
     409  | Eandbool(e1, e2) -> collect_expr e1; collect_expr e2
     410  | Eorbool(e1, e2) -> collect_expr e1; collect_expr e2
     411  | Esizeof ty -> collect_type ty
     412  | Efield(e1, id) -> collect_expr e1
     413
     414let rec collect_expr_list = function
     415  | [] -> ()
     416  | hd :: tl -> collect_expr hd; collect_expr_list tl
     417
     418let rec collect_stmt = function
     419  | Scost (_, s) -> collect_stmt s
     420  | Sskip -> ()
     421  | Sassign(e1, e2) -> collect_expr e1; collect_expr e2
     422  | Scall(None, e1, el) -> collect_expr e1; collect_expr_list el
     423  | Scall(Some lhs, e1, el) -> collect_expr lhs; collect_expr e1; collect_expr_list el
     424  | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2
     425  | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2
     426  | Swhile(e, s) -> collect_expr e; collect_stmt s
     427  | Sdowhile(e, s) -> collect_stmt s; collect_expr e
     428  | Sfor(s_init, e, s_iter, s_body) ->
     429      collect_stmt s_init; collect_expr e;
     430      collect_stmt s_iter; collect_stmt s_body
     431  | Sbreak -> ()
     432  | Scontinue -> ()
     433  | Sswitch(e, cases) -> collect_expr e; collect_cases cases
     434  | Sreturn None -> ()
     435  | Sreturn (Some e) -> collect_expr e
     436  | Slabel(lbl, s) -> collect_stmt s
     437  | Sgoto lbl -> ()
     438
     439and collect_cases = function
     440  | LSdefault s -> collect_stmt s
     441  | LScase(lbl, s, rem) -> collect_stmt s; collect_cases rem
     442
     443let collect_function f =
     444  collect_type f.fn_return;
     445  List.iter (fun (id, ty) -> collect_type ty) f.fn_params;
     446  List.iter (fun (id, ty) -> collect_type ty) f.fn_vars;
     447  collect_stmt f.fn_body
     448
     449let collect_fundef (id, fd) =
     450  match fd with
     451  | External(_, args, res) -> List.iter collect_type args; collect_type res
     452  | Internal f -> collect_function f
     453
     454let collect_globvar ((id, init), ty) =
     455  collect_type ty
     456
     457let collect_program p =
     458  List.iter collect_globvar p.prog_vars;
     459  List.iter collect_fundef p.prog_funct
     460
     461let declare_struct_or_union p (name, fld) =
     462  fprintf p "%s;@ @ " name
     463
     464let print_struct_or_union p (name, fld) =
     465  fprintf p "@[<v 2>%s {" name;
     466  let rec print_field (id, ty) =
     467    fprintf p "@ %s;" (name_cdecl id ty) in
     468  List.iter print_field fld;
     469  fprintf p "@;<0 -2>};@]@ "
     470
     471let print_program p prog =
     472  struct_unions := StructUnionSet.empty;
     473  collect_program prog;
     474  fprintf p "include \"Csyntax.ma\".@\n@\n";
     475  fprintf p "@[<v 2>ndefinition myprog := mk_program fundef type@ ";
     476(*  StructUnionSet.iter (declare_struct_or_union p) !struct_unions;
     477  StructUnionSet.iter (print_struct_or_union p) !struct_unions;*)
     478  print_list print_fundef p prog.prog_funct;
     479  fprintf p "@\n(succ_pos_of_nat %i)@\n" (id_i "main");
     480  print_list print_globvar p prog.prog_vars;
     481  fprintf p "@;<0 -2>.@]@."
     482
     483
  • src/clight/clightPrinter.ml

    diff --git a/src/clight/clightPrinter.ml b/src/clight/clightPrinter.ml
    index c458e36..b1efd87 100644
    a b open Format 
    1919open AST
    2020open Clight
    2121
     22let name_space = function
     23  | Any -> ""
     24  | Data -> "__data "
     25  | IData -> "__idata "
     26  | PData -> "__pdata "
     27  | XData -> "__xdata "
     28  | Code -> "__code "
     29
     30
    2231let name_unop = function
    2332  | Onotbool -> "!"
    2433  | Onotint  -> "~"
    let name_optid id = 
    7786let parenthesize_if_pointer id =
    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 "(*)"
    98113      else Buffer.add_string b (parenthesize_if_pointer id);
    let rec name_cdecl id ty = 
    105120          | [] -> ()
    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 *)
    126141
    let name_function_parameters fun_name params = 
    318333      | [] -> ()
    319334      | (id, ty) :: rem ->
    320335          if not first then Buffer.add_string b ", ";
    321           Buffer.add_string b (name_cdecl id ty);
     336          Buffer.add_string b (name_cdecl Any id ty);
    322337          add_params false rem in
    323338      add_params true params
    324339  end;
    let name_function_parameters fun_name params = 
    327342
    328343let print_function p id f =
    329344  fprintf p "%s@ "
    330             (name_cdecl (name_function_parameters id f.fn_params)
     345            (name_cdecl Any
     346                        (name_function_parameters id f.fn_params)
    331347                        f.fn_return);
    332348  fprintf p "@[<v 2>{@ ";
    333349  List.iter
    334350    (fun ((id, ty)) ->
    335       fprintf p "%s;@ " (name_cdecl id ty))
     351      fprintf p "%s;@ " (name_cdecl Any id ty))
    336352    f.fn_vars;
    337353  print_stmt p f.fn_body;
    338354  fprintf p "@;<0 -2>}@]@ @ "
    let print_fundef p (id, fd) = 
    341357  match fd with
    342358  | External(_, args, res) ->
    343359      fprintf p "extern %s;@ @ "
    344                 (name_cdecl id (Tfunction(args, res)))
     360                (name_cdecl Any id (Tfunction(args, res)))
    345361  | Internal f ->
    346362      print_function p id f
    347363
    let print_init p = function 
    376392
    377393let re_string_literal = Str.regexp "__stringlit_[0-9]+"
    378394
    379 let print_globvar p (((id, init), ty)) =
     395let print_globvar p ((((id, init), sp), ty)) =
    380396  match init with
    381397  | [] ->
    382398      fprintf p "extern %s;@ @ "
    383               (name_cdecl id ty)
     399              (name_cdecl sp id ty)
    384400  | [Init_space _] ->
    385401      fprintf p "%s;@ @ "
    386               (name_cdecl id ty)
     402              (name_cdecl sp id ty)
    387403  | _ ->
    388404      fprintf p "@[<hov 2>%s = "
    389               (name_cdecl id ty);
     405              (name_cdecl sp id ty);
    390406      if Str.string_match re_string_literal id 0
    391407      && List.for_all (function Init_int8 _ -> true | _ -> false) init
    392408      then
    let rec collect_type = function 
    404420  | Tvoid -> ()
    405421  | Tint(sz, sg) -> ()
    406422  | Tfloat sz -> ()
    407   | Tpointer t -> collect_type t
    408   | Tarray(t, n) -> collect_type t
     423  | Tpointer (_,t) -> collect_type t
     424  | Tarray(_, t, n) -> collect_type t
    409425  | Tfunction(args, res) -> collect_type_list args; collect_type res
    410426  | Tstruct(id, fld) -> register_struct_union id fld; collect_fields fld
    411427  | Tunion(id, fld) -> register_struct_union id fld; collect_fields fld
    let print_struct_or_union p (name, fld) = 
    491507  let rec print_fields = function
    492508  | [] -> ()
    493509  | (id, ty)::rem ->
    494       fprintf p "@ %s;" (name_cdecl id ty);
     510      fprintf p "@ %s;" (name_cdecl Any id ty);
    495511      print_fields rem in
    496512  print_fields fld;
    497513  fprintf p "@;<0 -2>};@]@ "
  • src/clight/clightToCminor.ml

    diff --git a/src/clight/clightToCminor.ml b/src/clight/clightToCminor.ml
    index 956239e..8b76ff8 100644
    a b let rec ctype_to_type_return t = match t with 
    77  | Tint (_,_) -> Type_ret Sig_int
    88  | Tfloat _ -> Type_ret Sig_float
    99  | Tpointer _ -> Type_ret Sig_int
    10   | Tarray (_,_) -> Type_ret Sig_int
     10  | Tarray _ -> Type_ret Sig_int
    1111  | Tfunction (_,_) | Tstruct (_,_)
    1212  | Tunion (_,_) | Tcomp_ptr _ -> assert false
    1313
    let rec ctype_to_sig_type t = match t with 
    1515  | Tint (_,_) -> Sig_int
    1616  | Tfloat _ -> Sig_float
    1717  | Tpointer _ -> Sig_int
    18   | Tarray (_,_) -> Sig_int
     18  | Tarray _ -> Sig_int
    1919  | Tvoid -> assert false
    2020  | Tfunction (_,_) | Tstruct (_,_)| Tunion (_,_) | Tcomp_ptr _ ->
    2121      assert false
    let rec mq_of_ty = function 
    3131  | Tfloat F32 -> assert false
    3232  | Tfloat F64 -> Memory.MQ_float64
    3333  | Tpointer _ -> Memory.MQ_int32                       
    34   | Tarray (c,s) -> Memory.MQ_int32
     34  | Tarray _ -> Memory.MQ_int32
    3535  | Tfunction (_,_) -> assert false
    3636  | Tstruct (_,_) -> assert false
    3737  | Tunion (_,_) -> assert false
    let rec size_of_ctype t = match t with 
    5959  | Tfloat F32 -> 8
    6060  | Tfloat F64 -> 8
    6161  | Tpointer _ -> 4                     
    62   | Tarray (c,s) -> s*(size_of_ctype c)                   
     62  | Tarray (_,c,s) -> s*(size_of_ctype c)                         
    6363  | Tfunction (_,_) | Tstruct (_,_) | Tunion (_,_)  | Tcomp_ptr _ ->
    6464      assert false
    6565
    6666let rec translate_vars v =
    67   let ((id,lst),cty) = v in
     67  let (((id,lst),space),cty) = v in
    6868    match cty with
    6969      | Tint (_,_) | Tfloat _ | Tpointer _ -> (id,init_data_to_data_rec lst)
    70       | Tarray(c,_) -> translate_vars ((id,lst),c)
     70      | Tarray(_,c,_) -> translate_vars (((id,lst),space),c)
    7171      | Tvoid | Tfunction (_,_) | Tstruct (_,_) | Tunion (_,_) | Tcomp_ptr _ ->
    7272          assert false
    7373
    let translate_binop t1 e1 t2 e2 = function 
    9595      (match (t1,t2) with
    9696         | (Tint(_,_),Tint(_,_)) -> Op2 (Op_add,e1,e2)
    9797         | (Tfloat _,Tfloat _) -> Op2 (Op_addf,e1,e2)
    98          | (Tpointer t,Tint(_,_)) ->
     98         | (Tpointer (_,t),Tint(_,_)) ->
    9999             Op2 (Op_add,e1, Op2 (Op_mul,e2,Cst (Cst_int (size_of_ctype t))))
    100          | (Tint(_,_),Tpointer t) ->
     100         | (Tint(_,_),Tpointer (_,t)) ->
    101101             Op2 (Op_add,Op2 (Op_mul,e1,Cst (Cst_int (size_of_ctype t))),e2)
    102          | (Tarray (t,_),Tint(_,_)) ->
     102         | (Tarray (_,t,_),Tint(_,_)) ->
    103103             Op2 (Op_add,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
    104          | (Tint(_,_),Tarray(t,_)) ->
     104         | (Tint(_,_),Tarray(_,t,_)) ->
    105105             Op2 (Op_add,e2,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t)))))
    106106         | _ -> assert false
    107107      )
    let translate_binop t1 e1 t2 e2 = function 
    109109      (match (t1,t2) with
    110110         | (Tint(_,_),Tint(_,_)) -> Op2 (Op_sub,e1,e2)
    111111         | (Tfloat _,Tfloat _) -> Op2 (Op_subf,e1,e2)
    112          | (Tpointer t,Tint(_,_)) ->
     112         | (Tpointer (_,t),Tint(_,_)) ->
    113113             Op2 (Op_sub,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
    114          | (Tint(_,_),Tpointer t) ->
     114         | (Tint(_,_),Tpointer (_,t)) ->
    115115             Op2 (Op_sub,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t)))),e2)
    116          | (Tarray (t,_),Tint(_,_)) ->
     116         | (Tarray (_,t,_),Tint(_,_)) ->
    117117             Op2 (Op_sub,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
    118          | (Tint(_,_),Tarray(t,_)) ->
     118         | (Tint(_,_),Tarray(_,t,_)) ->
    119119             Op2 (Op_sub,e2,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t)))))
    120120         | _ -> assert false
    121121      )
    let compute_stack f = 
    310310  and stck = ref 0 in
    311311  let treat_var v = match snd v with 
    312312    | Tvoid | Tint (_,_) | Tfloat _ | Tpointer _ -> ()
    313     | Tarray (_,_)  ->
     313    | Tarray _  ->
    314314        let size = size_of_ctype (snd v) in
    315315          if size > 0 then (
    316316            (Hashtbl.add addr_of_id (fst v) !stck);
    let translate_funct globals = function 
    400400  | (id,External (i,p,r)) -> (id, F_ext (translate_external i p r))
    401401
    402402let translate p =
    403   let globals = List.map (fun p -> fst (fst p)) p.prog_vars in
     403  let globals = List.map (fun p -> fst (fst (fst p))) p.prog_vars in
    404404    {Cminor.vars   = List.map translate_vars p.prog_vars;
    405405     Cminor.functs = List.map (translate_funct globals) p.prog_funct;
    406406     Cminor.main = p.prog_main }
  • src/common/cminorMemory.ml

    diff --git a/src/common/cminorMemory.ml b/src/common/cminorMemory.ml
    index 1b3e509..813be71 100644
    a b let rec sizeof = function 
    204204  | Tfloat F32 -> 4
    205205  | Tfloat F64 -> 8
    206206  | Tpointer _ -> 4                     
    207   | Tarray (_,_) -> 4                     
     207  | Tarray _ -> 4                         
    208208  | Tfunction (_,_) -> assert false
    209209  | Tstruct (_,_) -> assert false
    210210  | Tunion (_,_) -> assert false
    let vk_of_init_list = function (*FIXME*) 
    227227let cast t v = v (*TODO*)
    228228
    229229let init m b lst = function
    230   | Tarray (c,n) ->
     230  | Tarray (_,c,n) ->
    231231      (match alloc m 0 (n*(sizeof c)) with
    232232         | Some(b',m') ->
    233233             (match store m' Memory.MQ_int32 b 0 (Val_ptr(b',0)) with
    let initmem_clight p = 
    253253  let b_of_id = Hashtbl.create 11
    254254  and fd_of_b = Hashtbl.create 11
    255255  and i = ref (-1) in
    256   let update_mem m ((id,lst),cty) =
     256  let update_mem m (((id,lst),_),cty) =
    257257    (match alloc m 0 (sizeof cty) with
    258258       | Some(b,m') ->
    259259           Hashtbl.add b_of_id id b;
  • src/languages.ml

    diff --git a/src/languages.ml b/src/languages.ml
    index 4317d19..12ffdd2 100644
    a b let save filename ast = 
    230230  flush cout;
    231231  close_out cout
    232232
     233let rec find_clight = function
     234| [] -> None
     235| AstClight p :: t -> Some p
     236| _::t -> find_clight t
     237
     238let save_matita filename asts =
     239  match find_clight asts with
     240  | None -> Error.warning "during matita output" "No Clight AST."
     241  | Some prog -> begin
     242    let output_filename =
     243      Misc.SysExt.alternative
     244        (Filename.chop_extension filename
     245         ^ ".ma")
     246    in
     247    let cout = open_out output_filename in
     248    let fout = Format.formatter_of_out_channel cout in
     249    ClightPrintMatita.print_program fout prog;
     250    flush cout;
     251    close_out cout
     252  end
     253
    233254let interpret = function
    234255  | AstClight p ->
    235256    ClightInterpret.interpret true p
  • src/languages.mli

    diff --git a/src/languages.mli b/src/languages.mli
    index 3dfc31a..f5d8e45 100644
    a b val interpret : ast -> AST.label list 
    7575    is deduced from the language of the AST. *)
    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
    8085
  • src/options.ml

    diff --git a/src/options.ml b/src/options.ml
    index 061f7d0..d47e558 100644
    a b let debug_flag = ref false 
    3939let set_debug                   = (:=) debug_flag
    4040let is_debug_enabled ()         = !debug_flag
    4141
     42let matita_output_flag          = ref false
     43let is_matita_output_enabled () = !matita_output_flag
     44
    4245let options = OptionsParsing.register [
    4346  "-s", Arg.String set_source_language,
    4447  " Choose the source language between:";
    let options = OptionsParsing.register [ 
    5861
    5962  "-d", Arg.Set debug_flag,
    6063  " Debugging mode.";
     64
     65  "-ma", Arg.Set matita_output_flag,
     66  " Output matita formatted Clight program.";
    6167]
  • src/options.mli

    diff --git a/src/options.mli b/src/options.mli
    index 4517400..ec6b020 100644
    a b val input_files : unit -> string list 
    2222
    2323(** {2 Verbose mode} *)
    2424val is_debug_enabled : unit -> bool
     25
     26(** {2 Matita output of Clight programs} *)
     27val is_matita_output_enabled : unit -> bool
Note: See TracBrowser for help on using the repository browser.