Changeset 1117


Ignore:
Timestamp:
Aug 26, 2011, 6:47:52 PM (8 years ago)
Author:
sacerdot
Message:

More operations implemented.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1114 r1117  
    1616(* CSC: ???????????? *)
    1717axiom smerge: val → val → res val.
     18(* CSC: I have a byte, I need a value, but it is complex to do so *)
     19axiom val_of_Byte: Byte → val.
    1820(* CSC: fixed size chunk *)
    1921axiom chunk: memory_chunk.
     
    104106  [ rtl_st_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
    105107  | rtl_st_cost cl l ⇒ ret ? 〈Echarge cl, build_state f fs m l〉
    106   | rtl_st_load addrh addrl dst l ⇒  (* CSC: pairs of regs vs reg *)
     108  | rtl_st_load addrl addrh dst l ⇒  (* CSC: pairs of regs vs reg *)
    107109      ! vaddrh ← reg_retrieve (locals f) addrh;
    108110      ! vaddrl ← reg_retrieve (locals f) addrl;
    109       ! vaddr ← smerge vaddrh vaddrl;
     111      ! vaddr ← smerge vaddrl vaddrh;
    110112      ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr);
    111113      ! locals ← reg_store dst v (locals f);
    112114      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
    113   | rtl_st_store addrh addrl src l ⇒  (* CSC: pairs of regs vs reg *)
     115  | rtl_st_store addrl addrh src l ⇒  (* CSC: pairs of regs vs reg *)
    114116      ! vaddrh ← reg_retrieve (locals f) addrh;
    115117      ! vaddrl ← reg_retrieve (locals f) addrl;
    116       ! vaddr ← smerge vaddrh vaddrl;
     118      ! vaddr ← smerge vaddrl vaddrh;
    117119      ! v ← reg_retrieve (locals f) src;
    118120      ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v);
     
    123125      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    124126      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
    125   | rtl_st_call_ptr hfrs lfrs args dst l ⇒ (* CSC: pairs of regs vs reg *)
     127  | rtl_st_call_ptr lfrs hfrs args dst l ⇒ (* CSC: pairs of regs vs reg *)
    126128      ! hfv ← reg_retrieve (locals f) hfrs;
    127129      ! lfv ← reg_retrieve (locals f) lfrs;
    128       ! fv  ← smerge hfv lfv;
     130      ! fv  ← smerge lfv hfv;
    129131      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
    130132      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
     
    135137      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    136138      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    137   | rtl_st_tailcall_ptr hfrs lfrs args ⇒ (* CSC: pairs of regs vs reg *)
     139  | rtl_st_tailcall_ptr lfrs hfrs args ⇒ (* CSC: pairs of regs vs reg *)
    138140      ! hfv ← reg_retrieve (locals f) hfrs;
    139141      ! lfv ← reg_retrieve (locals f) lfrs;
    140       ! fv  ← smerge hfv lfv;
     142      ! fv  ← smerge lfv hfv;
    141143      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
    142144      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
     
    170172  (* CSC: Removed: St_jumptable *)
    171173  (* CSC: Added: *)
     174  | rtl_st_addr ldest hdest id l ⇒ ?
     175  | rtl_st_stack_addr ldest hdest l ⇒ ?
     176  (* CSC: St_const splitted into rtl_st_int *)
     177  | rtl_st_int dest v l ⇒
     178     ! locals ← reg_store dest (val_of_Byte v) (locals f);
     179     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
     180  | rtl_st_move dreg sreg l ⇒ ?
     181  | rtl_st_opaccs op dacc dbacc sacc sbacc l ⇒ ?
     182  | rtl_st_op1 op dreg sreg l ⇒ ?
     183  | rtl_st_op2 op dreg sreg1 sreg2 l ⇒ ?
     184 
    172185  | rtl_st_clear_carry l ⇒
    173186    ret ? 〈E0, State (mk_frame (func f) (locals f) l (sp f) (retdst f) Vfalse) fs m〉
    174187  | rtl_st_set_carry l ⇒
    175188    ret ? 〈E0, State (mk_frame (func f) (locals f) l (sp f) (retdst f) Vtrue) fs m〉
    176   | _ ⇒ ? ] (*
    177   ] *)
     189  ]
    178190| Callstate fd params dst fs m ⇒ ? (* CSC: XXXXXXXXXXXX
    179191    match fd with
Note: See TracChangeset for help on using the changeset viewer.