Changeset 816 for src/RTLabs


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/RTLabs
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • 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));
Note: See TracChangeset for help on using the changeset viewer.