Changeset 816 for src/Cminor


Ignore:
Timestamp:
May 19, 2011, 3:06:42 PM (9 years ago)
Author:
campbell
Message:

Clight to Cminor compilation, modulo switch statements, temporary
generation, 32 to 8 bit translation and miscellaneous bugs.

Also, remove (unused) signatures from function call statements in Cminor
and RTLabs; and separate comparison of integers and pointers in Clight
semantics.

Location:
src/Cminor
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/cminorMatitaPrinter.ml

    r776 r816  
    178178        (print_expression p_id e2)
    179179  | Cminor.St_call (None, f, args, sg) ->
    180       Printf.sprintf "%sSt_call (None ?) (%s) [%s] (%s)\n"
     180      Printf.sprintf "%sSt_call (None ?) (%s) [%s]\n"
    181181        (n_spaces n)
    182182        (print_expression p_id f)
    183183        (print_args p_id args)
    184         (print_sig sg)
    185184  | Cminor.St_call (Some id, f, args, sg) ->
    186       Printf.sprintf "%sSt_call (Some ? %s) (%s) [%s] (%s)\n"
     185      Printf.sprintf "%sSt_call (Some ? %s) (%s) [%s]\n"
    187186        (n_spaces n)
    188187        (p_id id)
    189188        (print_expression p_id f)
    190189        (print_args p_id args)
    191         (print_sig sg)
    192190  | Cminor.St_tailcall (f, args, sg) ->
    193       Printf.sprintf "%sSt_tailcall (%s) [%s] (%s)\n"
     191      Printf.sprintf "%sSt_tailcall (%s) [%s]\n"
    194192        (n_spaces n)
    195193        (print_expression p_id f)
    196194        (print_args p_id args)
    197         (print_sig sg)
    198195  | Cminor.St_seq (s1, s2) ->
    199196      Printf.sprintf "%sSt_seq (\n%s%s) (\n%s%s)\n"
  • src/Cminor/semantics.ma

    r797 r816  
    175175        ret ? 〈tr ⧺ tr', State f St_skip en m' sp k〉
    176176
    177     | St_call dst ef args sig ⇒ (* XXX sig unused? *)
     177    | St_call dst ef args
    178178        ! 〈tr,vf〉 ← eval_expr ge ef en sp m;
    179179        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
    180180        ! 〈tr',vargs〉 ← trace_map … (λe. eval_expr ge e en sp m) args;
    181181        ret ? 〈tr ⧺ tr', Callstate fd vargs m (Kcall dst f sp en k)〉
    182     | St_tailcall ef args sig
     182    | St_tailcall ef args
    183183        ! 〈tr,vf〉 ← eval_expr ge ef en sp m;
    184184        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
  • src/Cminor/syntax.ma

    r751 r816  
    1616| St_assign : ident → expr → stmt
    1717| St_store : memory_chunk → expr → expr → stmt
    18 (* ident for returned value, expression to identify fn, args, signature. *)
    19 | St_call : option ident → expr → list expr → signature → stmt
    20 | St_tailcall : expr → list expr → signature → stmt
     18(* ident for returned value, expression to identify fn, args. *)
     19| St_call : option ident → expr → list expr → stmt
     20| St_tailcall : expr → list expr → stmt
    2121| St_seq : stmt → stmt → stmt
    2222| St_ifthenelse : expr → stmt → stmt → stmt
  • src/Cminor/test/factorial.ma

    r768 r816  
    2020  St_cost C_cost2 (
    2121  St_seq (
    22     St_call (Some ? id_main_i) (Cst (Oaddrsymbol id_get_input (repr 0))) [] (mk_signature [] (Some ? ASTint))
     22    St_call (Some ? id_main_i) (Cst (Oaddrsymbol id_get_input (repr 0))) []
    2323  ) (
    2424  St_seq (
  • src/Cminor/test/search.ma

    r768 r816  
    123123  ) (
    124124  St_seq (
    125     St_call (Some ? id_main_res) (Cst (Oaddrsymbol id_search (repr 0))) [Cst (Oaddrstack (repr 0)); Cst (Ointconst (repr 5)); Cst (Ointconst (repr 57))] (mk_signature [ASTptr Any; ASTint; ASTint] (Some ? ASTint))
     125    St_call (Some ? id_main_res) (Cst (Oaddrsymbol id_search (repr 0))) [Cst (Oaddrstack (repr 0)); Cst (Ointconst (repr 5)); Cst (Ointconst (repr 57))]
    126126  ) (
    127127  St_return (Some ? (Op1 Ocast8unsigned (Id id_main_res)))
  • src/Cminor/test/switcher.ma

    r771 r816  
    2323  ) (
    2424  St_seq (
    25     St_call (Some ? id_main_x1) (Cst (Oaddrsymbol id_get zero)) [] (mk_signature [] (Some ? ASTint))
     25    St_call (Some ? id_main_x1) (Cst (Oaddrsymbol id_get zero)) []
    2626  ) (
    2727  St_seq (
  • src/Cminor/toRTLabs.ma

    r797 r816  
    251251    do f ← add_with_addressing env e1 (λm,rs. St_store q m rs val_reg) ptrs f;
    252252    add_expr env e2 val_reg ptrs f
    253 | St_call return_opt_id e args sig
     253| St_call return_opt_id e args
    254254    do return_opt_reg ←
    255255      match return_opt_id with
     
    260260    do f ←
    261261      match e with
    262       [ Id id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg sig) f
     262      [ Id id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f
    263263      | _ ⇒
    264264        do 〈fnr, f〉 ← choose_reg env e ptrs f;
    265         do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg sig) f;
     265        do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f;
    266266        add_expr env e fnr ptrs f
    267267      ];
    268268    add_exprs env args args_regs ptrs f
    269 | St_tailcall e args sig
     269| St_tailcall e args
    270270    do 〈args_regs, f〉 ← choose_regs env args ptrs f;
    271271    do f ←
    272272      match e with
    273       [ Id id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs sig) f
     273      [ Id id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f
    274274      | _ ⇒
    275275        do 〈fnr, f〉 ← choose_reg env e ptrs f;
    276         do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs sig) f;
     276        do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f;
    277277        add_expr env e fnr ptrs f
    278278      ];
Note: See TracChangeset for help on using the changeset viewer.