Changeset 489


Ignore:
Timestamp:
Feb 9, 2011, 6:22:34 PM (6 years ago)
Author:
campbell
Message:

Pointer fixes for the temporary version of the compiler that can output matita
terms.

Location:
Deliverables/D2.3/8051-memoryspaces-branch
Files:
9 edited

Legend:

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

    r461 r489  
    662662
    663663let nullconst =
    664   { edesc = EConst(CInt(0L, ptr_t_ikind, "0")); etyp = TPtr(Any, TVoid [], []); espace = Code } (* XXX *)
     664  { edesc = ECast(TPtr(Any, TVoid [], []), { edesc = EConst(CInt(0L, ptr_t_ikind, "0")); etyp = TInt(ptr_t_ikind, []); espace = Code}); etyp = TPtr(Any, TVoid [], []); espace = Code } (* XXX *)
    665665
    666666(* Construct a sequence *)
  • Deliverables/D2.3/8051-memoryspaces-branch/myocamlbuild_config.ml

    r460 r489  
    1 let parser_lib = "/home/bacam/workspace/uni/cerco/prototype/lib"
     1let parser_lib = "/home/bcampbe2/afs/cerco/cerco-git/Deliverables/D2.3/8051-memoryspaces-branch/lib"
  • Deliverables/D2.3/8051-memoryspaces-branch/src/acc.ml

    r460 r489  
    3232      src_language tgt_language input_ast
    3333  in
    34   let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in
     34  let final_ast, intermediate_asts =
     35    match target_asts with
     36    | [] -> input_ast, []
     37    | _ -> Misc.ListExt.cut_last target_asts
     38  in
    3539    Languages.save filename final_ast;
    3640    if Options.is_matita_output_enabled () then
  • Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clight.mli

    r461 r489  
    7171  | Tunion of ident*(ident*ctype) list
    7272  (**r union types *)
    73   | Tcomp_ptr of ident          (**r pointer to named struct or union *)
     73  | Tcomp_ptr of memory_space * ident           (**r pointer to named struct or union *)
    7474
    7575(** ** Expressions *)
     
    194194  | Init_int8 of int
    195195  | Init_int16 of int
    196   | Init_int24 of int
     196  | Init_null of memory_space
    197197  | Init_int32 of int
    198198  | Init_float32 of float
    199199  | Init_float64 of float
    200200  | Init_space of int
    201   | Init_addrof of ident*int  (**r address of symbol + offset *)
     201  | Init_addrof of memory_space*ident*int  (**r address of symbol + offset *)
    202202
    203203type program = {
  • Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightFromC.ml

    r461 r489  
    211211    | C.TFloat(fk, a) ->
    212212        Tfloat(convertFkind fk)
    213     | C.TPtr(_,C.TStruct(id, _), _) when List.mem id seen ->
    214         Tcomp_ptr("struct " ^ id.name)
    215     | C.TPtr(_,C.TUnion(id, _), _) when List.mem id seen ->
    216         Tcomp_ptr("union " ^ id.name)
     213    | C.TPtr(r,C.TStruct(id, _), _) when List.mem id seen ->
     214        Tcomp_ptr(convertSpace r,"struct " ^ id.name)
     215    | C.TPtr(r,C.TUnion(id, _), _) when List.mem id seen ->
     216        Tcomp_ptr(convertSpace r,"union " ^ id.name)
    217217    | C.TPtr(sp,ty, a) ->
    218218        Tpointer(convertSpace sp, convertTyp seen ty)
     
    283283  | C.EConst(C.CInt(i, _, _)) ->
    284284      Expr(Econst_int( convertInt i), ty)
    285   | C.EConst(C.CNull _) ->
    286       Expr(Econst_int( convertInt 0L), ty)
     285  | C.EConst(C.CNull r) ->
     286      Expr(Ecast (Tpointer (convertSpace r, Tvoid), ezero), ty)
    287287  | C.EConst(C.CFloat(f, _, _)) ->
    288288      Expr(Econst_float f, ty)
     
    625625    | { edesc = C.EVar id; etyp = ty } ->
    626626        begin match Cutil.unroll env ty with
    627         | C.TArray _ | C.TFun _ -> Some id
     627        | C.TArray (r,_,_,_) -> Some (id,r) | C.TFun _ -> Some (id, C.Code)
    628628        | _ -> None
    629629        end
    630     | {edesc = C.EUnop(C.Oaddrof, {edesc = C.EVar id})} -> Some id
    631     | {edesc = C.ECast(ty, e)} -> reduceInitExpr e
     630    | {edesc = C.EUnop(C.Oaddrof, {edesc = C.EVar id}); etyp = ty} ->
     631         begin match Cutil.unroll env ty with
     632         | C.TPtr (r,_,_) -> Some (id,r)
     633         | _ -> assert false
     634         end
     635    | {edesc = C.ECast(ty, e)} ->
     636         begin match reduceInitExpr e with
     637         | Some (id,_) ->
     638           begin match Cutil.unroll env ty with
     639                 | C.TPtr (r,_,_) | C.TArray(r,_,_,_) -> Some (id,r)
     640                 | _ -> assert false
     641                 end
     642         | None -> None
     643         end
    632644    | _ -> None in
    633645
     
    635647  | Init_single e ->
    636648      begin match reduceInitExpr e with
    637       | Some id ->
     649      | Some (id,r) ->
    638650          check_align 4;
    639           emit 4 (Init_addrof( id.name, 0))
     651          emit 4 (Init_addrof(convertSpace r, id.name, 0))
    640652      | None ->
    641653      match Ceval.constant_expr env ty e with
     
    652664          end
    653665      | Some(C.CNull sp) ->
    654           let z = convertInt 0L in
    655           begin match sp with
    656           | C.Any   -> emit 3 (Init_int24 z)
     666          let s =
     667            (match sp with
     668          | C.Any   -> 3
    657669          | C.Data
    658670          | C.IData
    659           | C.PData -> emit 1 (Init_int8 z)
     671          | C.PData -> 1
    660672          | C.XData
    661           | C.Code  -> emit 2 (Init_int16 z)
    662           end
     673          | C.Code  -> 2
     674          ) in
     675          emit s (Init_null (convertSpace sp))
    663676      | Some(C.CFloat(v, fk, _)) ->
    664677          begin match convertFkind fk with
     
    673686          check_align 4;
    674687          let id = name_for_string_literal env s in
    675           emit 4 (Init_addrof(id, 0))
     688          let r = match  Cutil.unroll env ty with
     689                  | TPtr (r,_,_) | TArray (r,_,_,_) -> r
     690                  | _ -> assert false
     691          in
     692          emit 4 (Init_addrof(convertSpace r,id, 0))
    676693      | Some(C.CWStr _) ->
    677694          unsupported "wide character strings"
  • Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightInterpret.ml

    r461 r489  
    635635  | Init_int8 i         -> Data_int8 i
    636636  | Init_int16 i        -> Data_int16 i
    637   | Init_int24 i        -> Data_int24 i
     637  | Init_null _         -> assert false
    638638  | Init_int32 i        -> Data_int32 i
    639639  | Init_float32 f      -> assert false (* Not supported *)
    640640  | Init_float64 f      -> assert false (* Not supported *)
    641641  | Init_space i        -> Data_reserve i
    642   | Init_addrof (_,_)   -> assert false (*FIXME what is this ?*)
     642  | Init_addrof _       -> assert false (*FIXME what is this ?*)
    643643
    644644(* FIXME: ignores memory space *)
     
    649649    | Init_int16 i -> (Mem.store m Memory.MQ_int16signed ptr (Value.of_int i)
    650650                       ,Value.add ptr (Value.of_int 2))
    651     | Init_int24 i -> (Mem.store m Memory.MQ_int24 ptr (Value.of_int i)
    652                        ,Value.add ptr (Value.of_int 3))
     651    | Init_null _ -> assert false
    653652    | Init_int32 i -> (Mem.store m Memory.MQ_int32 ptr (Value.of_int i)
    654653                       ,Value.add ptr (Value.of_int 4))
     
    656655    | Init_float64 _ -> assert false (*Not supported*)
    657656    | Init_space n -> (m,Value.add ptr (Value.of_int n))
    658     | Init_addrof (_,_) -> assert false (*FIXME what is this ?*)
     657    | Init_addrof _ -> assert false (*FIXME what is this ?*)
    659658  in let (m2,ptr) = (Mem.alloc m (sizeof ty))
    660659  in (fst (List.fold_left store_data (m2,ptr) lst),ptr)
  • Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightPrintMatita.ml

    r461 r489  
    136136  | Tunion(name, fld) ->
    137137      name ^ name_optid id
    138   | Tcomp_ptr name ->
     138  | Tcomp_ptr (_,name) ->
    139139      name ^ " *" ^ id
    140140
     
    161161  | Tunion(name, fld) ->
    162162      fieldlist "(Tunion (succ_pos_of_nat " name fld
    163   | Tcomp_ptr name ->
    164       "(Tcomp_ptr (succ_pos_of_nat " ^ id_s name ^ "))"
     163  | Tcomp_ptr (sp, name) ->
     164      "(Tcomp_ptr "^ sspace sp ^" (succ_pos_of_nat " ^ id_s name ^ "))"
    165165 and typelist l =
    166166    let b = Buffer.create 20 in
     
    258258      fprintf p "@[<hv 2>(Sassign %a@ %a)@]" print_expr e1 print_expr e2
    259259  | Scall(None, e1, el) ->
    260       fprintf p "@[<hv 2>(Scall (None ?) %a @[<hov 0>%a@])@]"
     260      fprintf p "@[<hv 2>(Scall (None expr) %a @[<hov 0>%a@])@]"
    261261                print_expr e1
    262262                (print_list print_expr) el
    263263  | Scall(Some lhs, e1, el) ->
    264       fprintf p "@[<hv 2>(Scall (Some ? %a)@ %a@ @[<hov 0>%a@])@]"
     264      fprintf p "@[<hv 2>(Scall (Some expr %a)@ %a@ @[<hov 0>%a@])@]"
    265265                print_expr lhs
    266266                print_expr e1
     
    296296              print_cases cases
    297297  | Sreturn None ->
    298       fprintf p "(Sreturn (None ?))"
     298      fprintf p "(Sreturn (None expr))"
    299299  | Sreturn (Some e) ->
    300       fprintf p "(Sreturn (Some ? %a))" print_expr e
     300      fprintf p "(Sreturn (Some expr %a))" print_expr e
    301301  | Slabel(lbl, s1) ->
    302302      fprintf p "(Slabel (succ_pos_of_nat %i)@ %a)" (id_i lbl) print_stmt s1
     
    321321      | (id, ty) :: rem ->
    322322          if not first then Buffer.add_string b "; ";
    323           Buffer.add_string b "mk_pair ?? (succ_pos_of_nat ";
     323          Buffer.add_string b "mk_pair ident type (succ_pos_of_nat ";
    324324          Buffer.add_string b (id_s id);
    325325          Buffer.add_string b ") ";
     
    338338
    339339let print_fundef p (id, fd) =
    340   fprintf p "@[<v 2>mk_pair ?? (succ_pos_of_nat %i (* %s *)) " (id_i id) id;
     340  fprintf p "@[<v 2>mk_pair ident fundef (succ_pos_of_nat %i (* %s *)) " (id_i id) id;
    341341  match fd with
    342342  | External(id', args, res) ->
     
    364364  | Init_int8 n -> fprintf p "(Init_int8 (repr %d))@ " n
    365365  | Init_int16 n -> fprintf p "(Init_int16 (repr %d))@ " n
    366   | Init_int24 n -> fprintf p "(Init_int24 (repr %d))@ " n
     366  | Init_null r -> fprintf p "(Init_null %s)@ " (sspace r)
    367367  | Init_int32 n -> fprintf p "(Init_int32 (repr %d))@ " n
    368368  | Init_float32 n -> fprintf p "(Init_float32 %F)@ " n
    369369  | Init_float64 n -> fprintf p "(Iinit_float64 %F)@ " n
    370370  | Init_space n -> fprintf p "(Init_space %d)@ " n
    371   | Init_addrof(symb, ofs) -> fprintf p "(Init_addrof %d (repr %d))" (id_i symb) ofs
     371  | Init_addrof(r, symb, ofs) -> fprintf p "(Init_addrof %s (succ_pos_of_nat %i) (repr %d))" (sspace r) (id_i symb) ofs
    372372
    373373let re_string_literal = Str.regexp "__stringlit_[0-9]+"
  • Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightPrinter.ml

    r461 r489  
    131131  | Tunion(name, fld) ->
    132132      ssp ^ name ^ name_optid id
    133   | Tcomp_ptr name ->
     133  | Tcomp_ptr (_, name) ->
    134134      ssp ^ name ^ " *" ^ id
    135135
     
    384384  | Init_int8 n -> fprintf p "%ld,@ " (Int32.of_int n)
    385385  | Init_int16 n -> fprintf p "%ld,@ " (Int32.of_int n)
    386   | Init_int24 n -> fprintf p "%ld,@ " (Int32.of_int n)
     386  | Init_null _ -> fprintf p "0,@ "
    387387  | Init_int32 n -> fprintf p "%ld,@ " (Int32.of_int n)
    388388  | Init_float32 n -> fprintf p "%F,@ " n
    389389  | Init_float64 n -> fprintf p "%F,@ " n
    390390  | Init_space n -> fprintf p "/* skip %ld, */@ " (Int32.of_int n)
    391   | Init_addrof(symb, ofs) ->
     391  | Init_addrof(r, symb, ofs) ->
    392392      let ofs = Int32.of_int ofs in
    393393      if ofs = Int32.zero
     
    398398  | Init_int8 n -> fprintf p "%ld" (Int32.of_int n)
    399399  | Init_int16 n -> fprintf p "%ld" (Int32.of_int n)
    400   | Init_int24 n -> fprintf p "%ld" (Int32.of_int n)
     400  | Init_null _ -> fprintf p "0"
    401401  | Init_int32 n -> fprintf p "%ld" (Int32.of_int n)
    402402  | Init_float32 n -> fprintf p "%F" n
    403403  | Init_float64 n -> fprintf p "%F" n
    404404  | Init_space n -> fprintf p "/* skip %ld */" (Int32.of_int n)
    405   | Init_addrof(symb, ofs) ->
     405  | Init_addrof(_,symb, ofs) ->
    406406      let ofs = Int32.of_int ofs in
    407407      if ofs = Int32.zero
  • Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightToCminor.ml

    r461 r489  
    5353    | Init_int8 i       -> Data_int8 i
    5454    | Init_int16 i      -> Data_int16 i
    55     | Init_int24 i      -> Data_int24 i
     55    | Init_null _       -> Data_int32 0
    5656    | Init_int32 i      -> Data_int32 i
    5757    | Init_float32 _
    5858    | Init_float64 _    -> assert false (*Not supported*)
    5959    | Init_space n      -> Data_reserve n
    60     | Init_addrof (_,_) -> assert false (* FIXME What is this ?*)
     60    | Init_addrof _ -> assert false (* FIXME What is this ?*)
    6161) l
    6262
Note: See TracChangeset for help on using the changeset viewer.