Changeset 1114


Ignore:
Timestamp:
Aug 26, 2011, 1:01:04 PM (8 years ago)
Author:
sacerdot
Message:

some more operations implemented

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1113 r1114  
    1212include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)
    1313
     14(* CSC: carries are values and booleans are not values; so we use integers.
     15   But why using values at all? To have undef? *)
    1416(* CSC: ???????????? *)
    1517axiom smerge: val → val → res val.
     
    102104  [ rtl_st_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
    103105  | rtl_st_cost cl l ⇒ ret ? 〈Echarge cl, build_state f fs m l〉
    104   (*
    105   | St_const r cst l ⇒
    106       ! v ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) (sp f) cst);
    107       ! locals ← reg_store r v (locals f);
    108       ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
    109   | St_op1 op dst src l ⇒
    110       ! v ← reg_retrieve (locals f) src;
    111       ! v' ← opt_to_res … (msg FailedOp) (eval_unop op v);
    112       ! locals ← reg_store dst v' (locals f);
    113       ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
    114   | St_op2 op dst src1 src2 l ⇒
    115       ! v1 ← reg_retrieve (locals f) src1;
    116       ! v2 ← reg_retrieve (locals f) src2;
    117       ! v' ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
    118       ! locals ← reg_store dst v' (locals f);
    119       ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉 *)
    120106  | rtl_st_load addrh addrl dst l ⇒  (* CSC: pairs of regs vs reg *)
    121107      ! vaddrh ← reg_retrieve (locals f) addrh;
     
    156142      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    157143      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    158 
    159 (*  | St_cond src ltrue lfalse ⇒
    160       ! v ← reg_retrieve (locals f) src;
    161       ! b ← eval_bool_of_val v;
    162       ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
    163 
    164   | St_jumptable r ls ⇒
    165       ! v ← reg_retrieve (locals f) r;
    166       match v with
    167       [ Vint _ i ⇒
    168           ! l ← opt_to_io … (msg BadJumpTable) (nth_opt ? (nat_of_bitvector ? i) ls);
    169           ret ? 〈E0, build_state f fs m l〉
    170       | _ ⇒ Wrong ??? (msg BadJumpValue)
    171       ] *)
    172 
    173144  | rtl_st_return ⇒
    174145      (* CSC: rtl_if_result/f_result; list vs option *)
     
    176147      ! v ←  mmap … (reg_retrieve (locals f)) dest;
    177148      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
     149  | rtl_st_cond src ltrue lfalse ⇒
     150      ! v ← reg_retrieve (locals f) src;
     151      ! b ← eval_bool_of_val v;
     152      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
     153
     154  (*
     155  | St_const r cst l ⇒
     156      ! v ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) (sp f) cst);
     157      ! locals ← reg_store r v (locals f);
     158      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
     159  | St_op1 op dst src l ⇒
     160      ! v ← reg_retrieve (locals f) src;
     161      ! v' ← opt_to_res … (msg FailedOp) (eval_unop op v);
     162      ! locals ← reg_store dst v' (locals f);
     163      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
     164  | St_op2 op dst src1 src2 l ⇒
     165      ! v1 ← reg_retrieve (locals f) src1;
     166      ! v2 ← reg_retrieve (locals f) src2;
     167      ! v' ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
     168      ! locals ← reg_store dst v' (locals f);
     169      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉 *)
     170  (* CSC: Removed: St_jumptable *)
     171  (* CSC: Added: *)
     172  | rtl_st_clear_carry l ⇒
     173    ret ? 〈E0, State (mk_frame (func f) (locals f) l (sp f) (retdst f) Vfalse) fs m〉
     174  | rtl_st_set_carry l ⇒
     175    ret ? 〈E0, State (mk_frame (func f) (locals f) l (sp f) (retdst f) Vtrue) fs m〉
    178176  | _ ⇒ ? ] (*
    179177  ] *)
Note: See TracChangeset for help on using the changeset viewer.