Changeset 1120


Ignore:
Timestamp:
Aug 26, 2011, 7:41:46 PM (8 years ago)
Author:
sacerdot
Message:

All operations implemented.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1118 r1120  
    1818(* CSC: I have a byte, I need a value, but it is complex to do so *)
    1919axiom val_of_Byte: Byte → val.
     20axiom Byte_of_val: val → res Byte.
    2021(* Map from the front-end memory model to the back-end memory model *)
    2122axiom represent_block: block → val × val.
     
    155156      ! b ← eval_bool_of_val v;
    156157      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
    157 
    158   (*
    159   | St_const r cst l ⇒
    160       ! v ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) (sp f) cst);
    161       ! locals ← reg_store r v (locals f);
    162       ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
    163   | St_op1 op dst src l ⇒
    164       ! v ← reg_retrieve (locals f) src;
    165       ! v' ← opt_to_res … (msg FailedOp) (eval_unop op v);
    166       ! locals ← reg_store dst v' (locals f);
    167       ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
    168   | St_op2 op dst src1 src2 l ⇒
    169       ! v1 ← reg_retrieve (locals f) src1;
    170       ! v2 ← reg_retrieve (locals f) src2;
    171       ! v' ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
    172       ! locals ← reg_store dst v' (locals f);
    173       ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉 *)
     158  (* CSC: mismatch between the memory models and failures for the next two opx *)
     159  | rtl_st_op1 op dst src l ⇒
     160     ! v ← reg_retrieve (locals f) src;
     161     ! v ← Byte_of_val v;
     162     let v' ≝ val_of_Byte (op1 eval op v) in
     163     ! locals ← reg_store dst v' (locals f);
     164     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
     165  | rtl_st_op2 op dst src1 src2 l ⇒
     166     ! v1 ← reg_retrieve (locals f) src1;
     167     ! v1 ← Byte_of_val v1;
     168     ! v2 ← reg_retrieve (locals f) src2;
     169     ! v2 ← Byte_of_val v2;
     170     ! carry ← eval_bool_of_val (carry f);
     171     let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
     172     let v' ≝ val_of_Byte v' in
     173     let carry ≝ of_bool carry in
     174     ! locals ← reg_store dst v' (locals f);
     175     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) carry) fs m〉
    174176
    175177  (* CSC: Removed: St_jumptable *)
     
    191193     ! locals ← reg_store dest (val_of_Byte v) (locals f);
    192194     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
    193      
    194   | rtl_st_move dreg sreg l ⇒ ?
    195   | rtl_st_opaccs op dacc dbacc sacc sbacc l ⇒ ?
    196   | rtl_st_op1 op dreg sreg l ⇒ ?
    197   | rtl_st_op2 op dreg sreg1 sreg2 l ⇒ ?
     195
     196  (* CSC: St_op1 splitted into rtl_st_op1 and rtl_st_move *)
     197  | rtl_st_move dst src l ⇒
     198     ! v ← reg_retrieve (locals f) src;
     199     ! locals ← reg_store dst v (locals f);
     200     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
     201  (* CSC: St_op2 splitted into rtl_st_op2 and rtl_st_opaccs *) 
     202  | rtl_st_opaccs op dacc dbacc sacc sbacc l ⇒
     203     ! v1 ← reg_retrieve (locals f) sacc;
     204     ! v1 ← Byte_of_val v1;
     205     ! v2 ← reg_retrieve (locals f) sbacc;
     206     ! v2 ← Byte_of_val v2;
     207     let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
     208     let v1' ≝ val_of_Byte v1' in
     209     let v2' ≝ val_of_Byte v2' in
     210     ! locals ← reg_store dacc v1' (locals f);
     211     ! locals ← reg_store dbacc v2' locals;
     212     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
    198213 
    199214  | rtl_st_clear_carry l ⇒
Note: See TracChangeset for help on using the changeset viewer.