Changeset 1174 for src/joint

Timestamp:

Sep 2, 2011, 4:09:02 PM (10 years ago)

Author:

sacerdot

Message:

Semantics of most instructions completed.

File:

• src/joint/semantics.ma (modified) (13 diffs)

src/joint/semantics.ma

@@ -33 +33 @@
 axiom val_of_nat: nat → val.
 (* Map from the front-end memory model to the back-end memory model *)
+*)
 axiom represent_block: block → val × val.
-*)
 (* CSC: fixed size chunk *)
 axiom chunk: memory_chunk.
@@ -47 +47 @@
 (* CSC: ??? *)
 axiom address_of_label: mem → label → address.
-(*
 axiom address_chunks_of_label: mem → label → Byte × Byte.
+(*
 axiom label_of_address_chunks: Byte → Byte → label.
 *)
@@ -70 +70 @@
  ; regsT: Type[0] (* regs = pseudo-registers + hw registers *)
  ; pop_frame_: framesT → res framesT
+ ; save_frame_: framesT → regsT → framesT
  ; greg_store_: generic_reg p → val → regsT → res regsT
  ; greg_retrieve_: regsT → generic_reg p → res val
@@ -80 +81 @@
  ; dph_store_: dph_reg p → val → regsT → res regsT
  ; dph_retrieve_: regsT → dph_reg p → res val
+ ; pair_reg_move_: regsT → pair_reg p → regsT
  }.
 
@@ -100 +102 @@
  λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (carry … st) (regs … st) (m … st).
 
-(*
-definition set_carry: val → state → state ≝
- λcarry,st. mk_state (st_frms st) (pc st) (sp st) (locals st) carry (regs st) (m st).
-*)
+definition set_carry: ∀p. val → state p → state p ≝
+ λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) carry (regs … st) (m … st).
 
 definition set_pc: ∀p. address → state p → state p ≝
  λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (carry … st) (regs … st) (m … st).
+
+definition set_frms: ∀p. framesT p → state p → state p ≝
+ λp,frms,st. mk_state … frms (pc … st) (sp … st) (carry … st) (regs … st) (m … st).
 
 (* CSC: was build_state in RTL *)
@@ -157 +160 @@
  λp,st,dst.dph_retrieve_ … (regs … st) dst.
 
-(*
-definition save_frame: state → state ≝ λst.st. (* CSC *)
-
-axiom FailedPopFrame: String.
-*)
+definition pair_reg_move: ∀p:sem_params. state p → pair_reg p → state p ≝
+ λp,st,rs.set_regs … (pair_reg_move_ … (regs … st) rs) st.
+
+definition save_frame: ∀p:sem_params. state p → state p ≝
+ λp,st. set_frms … (save_frame_ ? (st_frms ? st) (regs … st)) st.
 
 (* removes the top frame from the frames list *)
@@ -191 +194 @@
    (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)).
 
-(*
-definition save_ra : state → label → res state ≝
- λst,l.
-  let 〈addrl,addrh〉 ≝ address_chunks_of_label (m st) l in
+definition save_ra : ∀p. state p → label → res (state p) ≝
+ λp,st,l.
+  let 〈addrl,addrh〉 ≝ address_chunks_of_label (m … st) l in
   (* No monadic notation here *)
-  bind ?? (push st addrl) (λst.push st addrh).
-
+  bind ?? (push … st addrl) (λst.push … st addrh).
+
+(*
 (*CSC: unused now
 definition fetch_ra : state → res (state × label) ≝
@@ -211 +214 @@
 axiom fetch_statement: ∀globals: list ident. state → res (ltl_statement globals). (* CSC *)
 axiom fetch_function: ∀globals: list ident. state → res (ltl_internal_function globals). (* CSC *)
-
-definition init_locals : list register → register_env val ≝
+*)
+
+definition init_locals : ∀p.list register → regsT p ≝
 foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
 
+(*
 definition reg_store ≝
 λreg,v,locals. update RegisterTag val locals reg v.
@@ -222 +227 @@
 definition reg_retrieve : register_env val → register → res val ≝
 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
+*)
 
 axiom MissingSymbol : String.
-*)
+
 axiom FailedLoad : String.
-(*
+
 axiom BadFunction : String.
 
+(*
 (*CSC: to be implemented *)
 axiom fetch_external_args: external_function → state → res (list val).(* ≝
@@ -286 +293 @@
   bind ?? (hwreg_store RegisterSPL (val_of_Byte sph) regs) (λregs.
   OK ? (set_regs regs st))).
-
-(*
-(* CSC: completely different because different type for registers_move *)
-definition retrieve: state → registers_move → res val ≝
-  λst.
-  λr.
-  match r with
-  [ pseudo   src ⇒ reg_retrieve (locals st) src 
-  | from_acc src ⇒ hwreg_retrieve (regs st) src
-  ].
-
-definition store ≝
-  λst.
-  λv.
-  λr.
-  match r with
-  [ pseudo   dst ⇒
-    ! locals ← reg_store dst v (locals st);
-      ret ? (set_locals locals st)
-  | hardware dst ⇒
-    ! regs ← hwreg_store dst v (regs st);
-      ret ? (set_regs regs st)
-  ].
-*)
 *)
 
@@ -333 +316 @@
         ! st ← acca_store … dst v st;
           ret ? 〈E0, goto … l st〉
-(*      | joint_instr_store addrl addrh src ⇒
-        ! vaddrh ← hwreg_retrieve (regs st) addrh; (*CSC*)
-        ! vaddrl ← hwreg_retrieve (regs st) addrl; (*CSC*)
+      | joint_instr_store addrl addrh src ⇒
+        ! vaddrh ← dph_retrieve … st addrh;
+        ! vaddrl ← dpl_retrieve … st addrl;
         ! vaddr ← smerge vaddrl vaddrh;
-        ! v ← hwreg_retrieve (regs st) src; (*CSC*)
-        ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);
-          ret ? 〈E0, goto l (set_m m' st)〉
+        ! v ← acca_retrieve … st src;
+        ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m … st) vaddr v);
+          ret ? 〈E0, goto … l (set_m … m' st)〉
       | joint_instr_cond src ltrue ⇒
-        ! v ← hwreg_retrieve (regs st) src; (*CSC*)
+        ! v ← acca_retrieve … st src;
         ! b ← eval_bool_of_val v;
-          ret ? 〈E0, goto (if b then ltrue else l) st〉
+          ret ? 〈E0, goto … (if b then ltrue else l) st〉
       | joint_instr_address ident prf ldest hdest ⇒
         ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
           let 〈laddr,haddr〉 ≝ represent_block addr in
-        ! locals ← reg_store ldest laddr (locals st);
-        ! locals ← reg_store hdest haddr locals;
-          ret ? 〈E0, goto l (set_locals locals st)〉
+        ! st ← dpl_store … ldest laddr st;
+        ! st ← dph_store … hdest haddr st;
+          ret ? 〈E0, goto … l st〉
       | joint_instr_op1 op acc_a ⇒
-        ! v ← reg_retrieve (locals st) acc_a;
+        ! v ← acca_retrieve … st acc_a;
         ! v ← Byte_of_val v;
           let v' ≝ val_of_Byte (op1 eval op v) in
-        ! locals ← reg_store acc_a v' (locals st);
-          ret ? 〈E0, goto l (set_locals locals st)〉
-      | joint_instr_op2 op acc_a_reg dest ⇒
-        ! v1 ← reg_retrieve (locals st) acc_a_reg;
+        ! st ← acca_store … acc_a v' st;
+          ret ? 〈E0, goto … l st〉
+      | joint_instr_op2 op acc_a src ⇒
+        ! v1 ← acca_retrieve … st acc_a;
         ! v1 ← Byte_of_val v1;
-        ! v2 ← reg_retrieve (locals st) acc_a_reg;
+        ! v2 ← greg_retrieve … src;
         ! v2 ← Byte_of_val v2;
-        ! carry ← eval_bool_of_val (carry st);
+        ! carry ← eval_bool_of_val (carry … st);
           let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
           let v' ≝ val_of_Byte v' in
           let carry ≝ of_bool carry in
-        ! locals ← reg_store dest v' (locals st);
-          ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉
-      | joint_instr_clear_carry ⇒ ret ? 〈E0, goto l (set_carry Vfalse st)〉
-      | joint_instr_set_carry ⇒ ret ? 〈E0, goto l (set_carry Vtrue st)〉
+        ! st ← acca_store … acc_a v' st;
+          ret ? 〈E0, goto … l (set_carry … carry st)〉
+      | joint_instr_clear_carry ⇒ ret ? 〈E0, goto … l (set_carry … Vfalse st)〉
+      | joint_instr_set_carry ⇒ ret ? 〈E0, goto … l (set_carry … Vtrue st)〉
       | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
-        ! v1 ← reg_retrieve (locals st) acc_a_reg;
+        ! v1 ← acca_retrieve … st acc_a_reg;
         ! v1 ← Byte_of_val v1;
-        ! v2 ← reg_retrieve (locals st) acc_b_reg;
+        ! v2 ← accb_retrieve … st acc_b_reg;
         ! v2 ← Byte_of_val v2;
           let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
           let v1' ≝ val_of_Byte v1' in
           let v2' ≝ val_of_Byte v2' in
-        ! locals ← reg_store acc_a_reg v1' (locals st);
-        ! locals ← reg_store acc_b_reg v2' locals;
-          ret ? 〈E0, goto l (set_locals locals st)〉
+        ! st ← acca_store … acc_a_reg v1' st;
+        ! st ← accb_store … acc_b_reg v2' st;
+          ret ? 〈E0, goto … l st〉
       | joint_instr_pop dst ⇒
-        ! 〈st,v〉 ← pop st;
-        ! locals ← reg_store dst (val_of_Byte v) (locals st);
-          ret ? 〈E0, goto l (set_locals locals st)〉
+        ! 〈st,v〉 ← pop … st;
+        ! st ← acca_store … dst (val_of_Byte v) st;
+          ret ? 〈E0, goto … l st〉
       | joint_instr_push src ⇒
-        ! v ← reg_retrieve (locals st) src;
+        ! v ← acca_retrieve … st src;
         ! v ← Byte_of_val v; 
-        ! st ← push st v;
-          ret ? 〈E0, goto l st〉
+        ! st ← push … st v;
+          ret ? 〈E0, goto … l st〉
       | joint_instr_move dst_src ⇒
-        let 〈dst, src〉 ≝ dst_src in
-        ! v ← retrieve st src;
-        ! st ← store st v dst;
-          ret ? 〈E0, goto l st〉
+          ret ? 〈E0, goto … l (pair_reg_move … st dst_src)〉
       | joint_instr_call_id id argsno ⇒ (* CSC: only the number of args kept, no return reg *)
         ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
@@ -400 +380 @@
           [ Internal fn ⇒
             ! st ← save_ra st l;
-              let st ≝ save_frame st in
-              let locals ≝ init_locals (ertl_if_locals globals fn) in
+              let st ≝ save_frame … st in
+              let regs ≝ init_locals … (ertl_if_locals globals fn) in
               let l' ≝ ertl_if_entry globals fn in
-              ret ? 〈 E0, goto l' (set_locals locals st)〉
+              ret ? 〈 E0, goto … l' (set_regs … regs st)〉
           | External fn ⇒
             ! params ← fetch_external_args fn st;
@@ -413 +393 @@
             ! st ← set_result vs st; 
               ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
-*)
-          | _ ⇒ ?
           ]
+      ]
     | joint_st_return ⇒
       ! st ← pop_frame … st;