Changeset 816


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
Files:
1 added
18 edited

Legend:

Unmodified
Added
Removed
  • src/CHANGES

    r774 r816  
    4949  One of the front end operations for subtraction (subpp) appears to be missing
    5050  from the prototype at present.
     51
     5219/05/2011:
     53  Dump Param var_type from the Clight to Cminor stage - we need to treat them
     54  like the other variables.
     55
     56  Generate list of pointer variables from Clight types rather than
     57  recalculation.
     58
     59  Drop signatures from function call statements in Cminor and RTLabs - they
     60  appear to be unused.
  • src/Clight/Csem.ma

    r776 r816  
    322322        | _ ⇒ None ? ]
    323323      | _ ⇒ None ? ]
    324   | cmp_case_ipip
     324  | cmp_case_ii
    325325      match v1 with
    326326      [ Vint n1 ⇒ match v2 with
     
    328328         | _ ⇒ None ?
    329329         ]
    330       | Vptr r1 b1 p1 ofs1 ⇒
     330      | _ ⇒ None ?     
     331      ]
     332  | cmp_case_pp ⇒
     333      match v1 with
     334      [ Vptr r1 b1 p1 ofs1 ⇒
    331335        match v2 with
    332336        [ Vptr r2 b2 p2 ofs2 ⇒
  • src/Clight/Csyntax.ma

    r797 r816  
    830830inductive classify_cmp_cases : Type[0] ≝
    831831  | cmp_case_I32unsi: classify_cmp_cases (**r unsigned I32 , int *)
    832   | cmp_case_ipip: classify_cmp_cases  (**r int|ptr|array , int|ptr|array*)
     832  | cmp_case_ii: classify_cmp_cases  (**r int, int*)
     833  | cmp_case_pp: classify_cmp_cases  (**r ptr|array , ptr|array*)
    833834  | cmp_case_ff: classify_cmp_cases  (**r float , float *)
    834835  | cmp_default: classify_cmp_cases . (**r other *)
     
    840841    [ Tint i2 s2 ⇒
    841842      classify_32un_aux ? i1 s1 cmp_case_I32unsi
    842         (classify_32un_aux ? i2 s2 cmp_case_I32unsi cmp_case_ipip)
     843        (classify_32un_aux ? i2 s2 cmp_case_I32unsi cmp_case_ii)
    843844    | _ ⇒ cmp_default ]
    844845  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ cmp_case_ff | _ ⇒ cmp_default ]
    845846  | Tpointer _ _ ⇒
    846847    match ty2 with
    847     [ Tint _ _ ⇒ cmp_case_ipip
    848     | Tpointer _ _ ⇒ cmp_case_ipip
    849     | Tarray _ _ _ ⇒ cmp_case_ipip
     848    [ Tpointer _ _ ⇒ cmp_case_pp
     849    | Tarray _ _ _ ⇒ cmp_case_pp
    850850    | _ ⇒ cmp_default ]
    851851  | Tarray _ _ _ ⇒
    852852    match ty2 with
    853     [ Tint _ _ ⇒ cmp_case_ipip
    854     | Tpointer _ _ ⇒ cmp_case_ipip
    855     | Tarray _ _ _ ⇒ cmp_case_ipip
     853    [ Tpointer _ _ ⇒ cmp_case_pp
     854    | Tarray _ _ _ ⇒ cmp_case_pp
    856855    | _ ⇒ cmp_default ]
    857856  | _ ⇒ cmp_default
  • src/Clight/test/search.ma

    r748 r816  
    193193@refl
    194194qed.
     195
     196include "Clight/toCminor.ma".
     197include "Cminor/semantics.ma".
     198
     199example e1: finishes_with (repr 3) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
     200normalize
     201@refl
     202qed.
     203
     204include "Cminor/toRTLabs.ma".
     205include "RTLabs/semantics.ma".
     206
     207example e2: finishes_with (repr 3) ? (
     208do p1 ← clight_to_cminor myprog;
     209do p2 ← cminor_to_rtlabs p1;
     210 exec_up_to RTLabs_fullexec p2 1000 [ ]).
     211normalize
     212@refl
     213qed.
  • 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      ];
  • src/RTLabs/RTLabsMatitaPrinter.ml

    r765 r816  
    167167        lbl
    168168  | RTLabs.St_call_id (f, args, res, sg, lbl) ->
    169       Printf.sprintf "make_St_call_id id_%s %s (Some ? %s) (%s) %s"
     169      Printf.sprintf "make_St_call_id id_%s %s (Some ? %s) %s"
    170170        f
    171171        (print_params args)
    172172        (Register.print res)
    173         (print_sig sg)
    174173        lbl
    175174  | RTLabs.St_call_ptr (f, args, res, sg, lbl) ->
    176       Printf.sprintf "make_St_call_ptr %s %s (Some ? %s) (%s) %s"
     175      Printf.sprintf "make_St_call_ptr %s %s (Some ? %s) %s"
    177176        (Register.print f)
    178177        (print_params args)
    179178        (Register.print res)
    180         (print_sig sg)
    181179        lbl
    182180  | RTLabs.St_tailcall_id (f, args, sg) ->
    183       Printf.sprintf "make_St_tailcall_id id_%s %s (%s)"
     181      Printf.sprintf "make_St_tailcall_id id_%s %s"
    184182        f
    185183        (print_params args)
    186         (print_sig sg)
    187184  | RTLabs.St_tailcall_ptr (f, args, sg) ->
    188       Printf.sprintf "make_St_tailcall_ptr %s %s (%s)"
     185      Printf.sprintf "make_St_tailcall_ptr %s %s"
    189186        (Register.print f)
    190187        (print_params args)
    191         (print_sig sg)
    192188  | RTLabs.St_condcst (cst, lbl_true, lbl_false) ->
    193189      Printf.sprintf "make_St_condcst (%s) %s %s"
  • src/RTLabs/import.ma

    r797 r816  
    116116let rec make_St_load chunk mode args dst l ≝ λr:nat → res register.λf:nat → res label. do dst' ← r dst; do l' ← f l; do args' ← make_addr r ? args; OK ? (St_load chunk mode args' dst' l').
    117117let rec make_St_store chunk mode args src l ≝ λr:nat → res register.λf:nat → res label. do src' ← r src; do l' ← f l; do args' ← make_addr r ? args; OK ? (St_store chunk mode args' src' l').
    118 let rec make_St_call_id id args dst sig l ≝ λr:nat → res register.λf:nat → res label. do args' ← make_reg_list r args; do dst' ← make_opt_reg r dst; do l' ← f l; OK ? (St_call_id id args' dst' sig l').
    119 let rec make_St_call_ptr frs args dst sig l ≝ λr:nat → res register.λf:nat → res label. do frs' ← r frs; do args' ← make_reg_list r args; do dst' ← make_opt_reg r dst; do l' ← f l; OK ? (St_call_ptr frs' args' dst' sig l').
    120 let rec make_St_tailcall_id id args sig ≝ λr:nat → res register.λf:nat → res label.  do args' ← make_reg_list r args; OK statement (St_tailcall_id id args' sig).
    121 let rec make_St_tailcall_ptr frs args sig ≝ λr:nat → res register.λf:nat → res label. do frs' ← r frs; do args' ← make_reg_list r args; OK statement (St_tailcall_ptr frs' args' sig).
     118let rec make_St_call_id id args dst l ≝ λr:nat → res register.λf:nat → res label. do args' ← make_reg_list r args; do dst' ← make_opt_reg r dst; do l' ← f l; OK ? (St_call_id id args' dst' l').
     119let rec make_St_call_ptr frs args dst l ≝ λr:nat → res register.λf:nat → res label. do frs' ← r frs; do args' ← make_reg_list r args; do dst' ← make_opt_reg r dst; do l' ← f l; OK ? (St_call_ptr frs' args' dst' l').
     120let rec make_St_tailcall_id id args ≝ λr:nat → res register.λf:nat → res label.  do args' ← make_reg_list r args; OK statement (St_tailcall_id id args').
     121let rec make_St_tailcall_ptr frs args ≝ λr:nat → res register.λf:nat → res label. do frs' ← r frs; do args' ← make_reg_list r args; OK statement (St_tailcall_ptr frs' args').
    122122let rec make_St_condcst cst ltrue lfalse ≝ λr:nat → res register.λf:nat → res label. do ltrue' ← f ltrue; do lfalse' ← f lfalse; OK ? (St_condcst cst ltrue' lfalse').
    123123let rec make_St_cond1 op src ltrue lfalse ≝ λr:nat → res register.λf:nat → res label. do src' ← r src; do ltrue' ← f ltrue; do lfalse' ← f lfalse;  OK ? (St_cond1 op src' ltrue' lfalse').
  • src/RTLabs/semantics.ma

    r797 r816  
    142142      ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v);
    143143      ret ? 〈E0, build_state f fs m' l〉
    144   | St_call_id id args dst sig l ⇒ (* XXX: haven't used sig *)
     144  | St_call_id id args dst l ⇒
    145145      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    146146      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    147147      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    148148      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
    149   | St_call_ptr frs args dst sig l ⇒  (* XXX: haven't used sig *)
     149  | St_call_ptr frs args dst l ⇒
    150150      ! fv ← reg_retrieve (locals f) frs;
    151151      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
    152152      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    153153      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
    154   | St_tailcall_id id args sig ⇒ (* XXX: haven't used sig *)
     154  | St_tailcall_id id args
    155155      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    156156      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    157157      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    158158      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    159   | St_tailcall_ptr frs args sig ⇒  (* XXX: haven't used sig *)
     159  | St_tailcall_ptr frs args
    160160      ! fv ← reg_retrieve (locals f) frs;
    161161      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
  • src/RTLabs/syntax.ma

    r765 r816  
    4545| St_load : memory_chunk → ∀m:addressing. addr m → register → label → statement
    4646| St_store : memory_chunk → ∀m:addressing. addr m → register → label → statement
    47 | St_call_id : ident → list register → option register → signature → label → statement
    48 | St_call_ptr : register → list register → option register → signature → label → statement
    49 | St_tailcall_id : ident → list register → signature → statement
    50 | St_tailcall_ptr : register → list register → signature → statement
     47| St_call_id : ident → list register → option register → label → statement
     48| St_call_ptr : register → list register → option register → label → statement
     49| St_tailcall_id : ident → list register → statement
     50| St_tailcall_ptr : register → list register → statement
    5151(* Um, what? *)
    5252| St_condcst : constant → label → label → statement
  • src/RTLabs/test/search.ma

    r765 r816  
    221221    (pair ?? main21 (make_St_const 19 (Ointconst (repr 23)) main20));
    222222    (pair ?? main20 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[18]] 19 main19));
    223     (pair ?? main2 (make_St_call_id id_search [3; 4; 5] (Some ? 1) (mk_signature [ASTptr Any; ASTint; ASTint] (Some ? ASTint)) main1));
     223    (pair ?? main2 (make_St_call_id id_search [3; 4; 5] (Some ? 1) main1));
    224224    (pair ?? main19 (make_St_const 14 (Oaddrstack (repr 0)) main18));
    225225    (pair ?? main18 (make_St_const 16 (Ointconst (repr 3)) main17));
  • src/common/Identifiers.ma

    r797 r816  
    114114λtag,s,s'. an_id_set tag (merge unit 16 (match s with [ an_id_set s0 ⇒ s0 ])
    115115                                        (match s' with [ an_id_set s1 ⇒ s1 ])).
     116
     117interpretation "identifier set union" 'union a b = (union_set ? a b).
     118notation "∅" non associative with precedence 90 for @{ 'empty }.
     119interpretation "empty identifier set" 'empty = (empty_set ?).
     120interpretation "singleton identifier set" 'singl a = (add_set ? (empty_set ?) a).
  • src/utilities/lists.ma

    r780 r816  
    77].
    88
     9let rec All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
     10match l with
     11[ nil ⇒ False
     12| cons h t ⇒ P h ∧ All A P t
     13].
     14
    915let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝
    1016match l with
Note: See TracChangeset for help on using the changeset viewer.