Changeset 1245 for src/LIN

Timestamp:

Sep 21, 2011, 10:22:13 PM (9 years ago)

Author:

sacerdot

Message:

RTLtoERTL and LINToASM: porting to new Joint data type in progress.
However, it seems better to go back to a Joint representation where
the "mapping" from label to internal functions is more concrete.
To be done.

File:

• src/LIN/LINToASM.ma (modified) (10 diffs)

src/LIN/LINToASM.ma

@@ -28 +28 @@
 definition statement_labels ≝
   λg: list ident.
-  λs: lin_statement g.
+  λs: (option label) × (lin_statement g).
   let 〈label, instr〉 ≝ s in
   let generated ≝
@@ -51 +51 @@
   λglobals: list ident.
   λlabels: BitVectorTrieSet ?.
-  λstatement: lin_statement globals.
+  λstatement: (option label) × (lin_statement globals).
     set_union ? labels (statement_labels globals statement).
 
+(*
 (* dpm: A = Identifier *)
 definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet ? ≝
@@ -61 +62 @@
   let 〈ignore, fun_def〉 ≝ f in
   match fun_def return λ_. BitVectorTrieSet ? with
-  [ lin_fu_internal stmts proof ⇒
+  [ Internal stmts ⇒
       foldl ? ? (function_labels_internal globals) (set_empty ?) stmts
-  | lin_fu_external _ ⇒ set_empty ?
+  | External _ ⇒ set_empty ?
   ].
   
@@ -77 +78 @@
     foldl ? ? (program_labels_internal ? (map ? ? (fst ? ?) (lin_pr_vars program)))
               (set_empty ?) (lin_pr_funcs program).
-    
+*)  
 definition data_of_int ≝ λbv. DATA bv.
 definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
 definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
-
-axiom ImplementedInRuntime: False.
 
 definition translate_statements ≝
@@ -88 +87 @@
   λglobals_old: list ident.
   λprf: ∀i: ident. member i (eq_identifier ?) globals_old → member i (eq_identifier ?) (map ? ? (fst ? ?) globals).
-  λstatement: pre_lin_statement globals_old.
+  λstatement: lin_statement globals_old.
   match statement with
   [ joint_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
-  | joint_st_extension ext ⇒ Instruction (NOP ?) (* XXX: NOP or something else? *)
+  | joint_st_extension ext ⇒ ⊥
   | joint_st_return ⇒ Instruction (RET ?)
   | joint_st_sequential instr _ ⇒
@@ -97 +96 @@
       [ joint_instr_comment comment ⇒ Comment comment
       | joint_instr_cost_label lbl ⇒ Cost (Identifier_of_costlabel lbl)
-      | joint_instr_pop ⇒ Instruction (POP ? accumulator_address)
-      | joint_instr_push ⇒ Instruction (PUSH ? accumulator_address)
+      | joint_instr_pop _ ⇒ Instruction (POP ? accumulator_address)
+      | joint_instr_push _ ⇒ Instruction (PUSH ? accumulator_address)
       | joint_instr_clear_carry ⇒ Instruction (CLR ? CARRY)
-      | joint_instr_call_id f ⇒ Call (word_of_identifier ? f)
-      | joint_instr_opaccs accs ⇒
+      | joint_instr_call_id f _ ⇒ Call (word_of_identifier ? f)
+      | joint_instr_opaccs accs _ _ ⇒
         match accs with
         [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
         | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
         ]
-      | joint_instr_op1 op1 ⇒
+      | joint_instr_op1 op1 _ ⇒
         match op1 with
         [ Cmpl ⇒ Instruction (CPL ? ACC_A)
         | Inc ⇒ Instruction (INC ? ACC_A)
         ]
-      | joint_instr_op2 op2 reg ⇒
+      | joint_instr_op2 op2 _ reg ⇒
         match op2 with
         [ Add ⇒
@@ -205 +204 @@
           | _ ⇒ λother: False. ⊥
           ] (subaddressing_modein … reg')
-      | joint_instr_from_acc reg ⇒
-        let reg' ≝ register_address reg in
-          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
-                                                         direct;
-                                                         registr ]] x) → ? with
-          [ REGISTER r ⇒ λregister8: True.
-            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
-          | ACC_A ⇒ λacc: True.
-            Instruction (NOP ?)
-          | DIRECT d ⇒ λdirect8: True.
-            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
-          | _ ⇒ λother: False. ⊥
-          ] (subaddressing_modein … reg')
-      | joint_instr_to_acc reg ⇒
-        let reg' ≝ register_address reg in
-          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
-                                                         direct;
-                                                         registr ]] x) → ? with
-          [ REGISTER r ⇒ λregister9: True.
-            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
-          | DIRECT d ⇒ λdirect9: True.
-            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
-          | ACC_A ⇒ λacc_a: True.
-            Instruction (NOP ?)
-          | _ ⇒ λother: False. ⊥
-          ] (subaddressing_modein … reg')
-      | joint_instr_load ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
-      | joint_instr_store ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
-      | joint_instr_address addr proof ⇒
+      | joint_instr_move regs ⇒
+         match regs with
+          [ from_acc reg ⇒
+             let reg' ≝ register_address reg in
+               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
+                                                              direct;
+                                                              registr ]] x) → ? with
+               [ REGISTER r ⇒ λregister8: True.
+                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
+               | ACC_A ⇒ λacc: True.
+                 Instruction (NOP ?)
+               | DIRECT d ⇒ λdirect8: True.
+                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
+               | _ ⇒ λother: False. ⊥
+               ] (subaddressing_modein … reg')
+          | to_acc reg ⇒
+             let reg' ≝ register_address reg in
+               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
+                                                              direct;
+                                                              registr ]] x) → ? with
+               [ REGISTER r ⇒ λregister9: True.
+                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
+               | DIRECT d ⇒ λdirect9: True.
+                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
+               | ACC_A ⇒ λacc_a: True.
+                 Instruction (NOP ?)
+               | _ ⇒ λother: False. ⊥
+               ] (subaddressing_modein … reg')]
+      | joint_instr_load _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
+      | joint_instr_store _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
+      | joint_instr_address addr proof _ _ ⇒
         let look ≝ association addr globals (prf ? proof) in
           Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
-      | joint_instr_cond_acc lbl ⇒
+      | joint_instr_cond _ lbl ⇒
         (* dpm: this should be handled in translate_code! *)
         Instruction (JNZ ? (word_of_identifier ? lbl))
@@ -245 +246 @@
   try assumption
   try @ I
-  cases ImplementedInRuntime
 qed.
 
@@ -252 +252 @@
   λglobals_old.
   λprf.
-  λstatement: lin_statement globals_old.
+  λstatement: (option label) × (lin_statement globals_old).
     〈\fst statement, translate_statements globals globals_old prf (\snd statement)〉.
 
@@ -259 +259 @@
   λglobals_old: list ident.
   λprf.
-  λcode: list (lin_statement globals_old).
+  λcode: list ((option label) × (lin_statement globals_old)).
     map ? ? (build_translated_statement globals globals_old prf) code.