Changeset 723 for src

Timestamp:

Mar 30, 2011, 12:34:25 PM (10 years ago)

Author:

mulligan

Message:

Added dependent type internalising the invariant that LIN function bodies are non-empty and do not start with a label.

Location:

src

Files:

• CHANGES (modified) (1 diff)
• LIN/LIN.ma (modified) (1 diff)
• LIN/LINToASM.ma (modified) (17 diffs)
• LTL/LTL.ma (modified) (1 diff)
• LTL/LTLToLIN.ma (modified) (1 diff)

src/CHANGES

@@ -10 +10 @@
 
   Formalised missing Assembly.ma file.
+
+30/03/2011:
+  Split translate_statements into two functions.
+
+  Added a dependent type for the invariant that a LIN function body does not
+  start with a label, and is not empty.

src/LIN/LIN.ma

@@ -1 @@
-include "arithmetics/nat.ma".
-include "ASM/String.ma".
+include "LIN/JointLTLLIN.ma".
+  
+definition PreLINStatement ≝ JointStatement unit.
 
-include "ASM/I8051.ma".
-include "common/AST.ma".
-
-alias id "ASMOp1" = "cic:/matita/cerco/ASM/I8051/Op1.ind(1,0,0)".
-alias id "ASMOp2" = "cic:/matita/cerco/ASM/I8051/Op2.ind(1,0,0)".
-
-inductive JointInstruction (globals: list Identifier): Type[0] ≝
-  | Joint_Instr_Goto: Identifier → JointInstruction globals
-  | Joint_Instr_Comment: String → JointInstruction globals
-  | Joint_Instr_CostLabel: Identifier → JointInstruction globals
-  | Joint_Instr_Int: Register → Byte → JointInstruction globals
-  | Joint_Instr_Pop: JointInstruction globals
-  | Joint_Instr_Push: JointInstruction globals
-  | Joint_Instr_Address: ∀i: Identifier. (member i (eq_bv ?) globals) → JointInstruction globals
-  | Joint_Instr_FromAcc: Register → JointInstruction globals
-  | Joint_Instr_ToAcc: Register → JointInstruction globals
-  | Joint_Instr_OpAccs: OpAccs → JointInstruction globals
-  | Joint_Instr_Op1: Op1 → JointInstruction globals
-  | Joint_Instr_Op2: Op2 → Register → JointInstruction globals
-  | Joint_Instr_ClearCarry: JointInstruction globals
-  | Joint_Instr_Load: JointInstruction globals
-  | Joint_Instr_Store: JointInstruction globals
-  | Joint_Instr_CallId: Identifier → JointInstruction globals
-  | Joint_Instr_CondAcc: Identifier → JointInstruction globals.
-
-inductive JointStatement (A: Type[0]) (globals: list Identifier): Type[0] ≝
-  | LIN_St_Sequential: JointInstruction globals → A → JointStatement A globals
-  | LIN_St_Return: JointStatement A globals.
-  
 definition LINStatement ≝
   λglobals.
-    option Identifier × (JointStatement unit globals).
-  
-definition LINInternalFunction ≝ λglobals. list (LINStatement globals).
+    option Identifier × (PreLINStatement globals).
 
+definition WellFormedP ≝
+  λA, B: Type[0].
+  λcode: list (option A × B).
+    match code with
+    [ nil ⇒ False
+    | cons hd tl ⇒
+      match \fst hd with
+      [ Some lbl ⇒ False
+      | None ⇒ True
+      ]
+    ].
+    
 inductive LINFunctionDefinition (globals: list Identifier): Type[0] ≝
-  LIN_Fu_Internal: LINInternalFunction globals → LINFunctionDefinition globals
+  LIN_Fu_Internal: ∀code: list (LINStatement globals). WellFormedP ? ? code → LINFunctionDefinition globals
 | LIN_Fu_External: ExternalFunction → LINFunctionDefinition globals.
 

src/LIN/LINToASM.ma

@@ -32 +32 @@
   let generated ≝
     match instr with
-    [ LIN_St_Sequential instr' _ ⇒
+    [ Joint_St_Sequential instr' _ ⇒
         match instr' with
         [ Joint_Instr_Goto lbl ⇒ set_insert ? lbl (set_empty ?)
@@ -39 +39 @@
         | _ ⇒ set_empty ?
         ]
-    | LIN_St_Return ⇒ set_empty ?
+    | Joint_St_Return ⇒ set_empty ?
     ] in
   match label with
@@ -59 +59 @@
   let 〈ignore, fun_def〉 ≝ f in
   match fun_def return λ_. BitVectorTrieSet ? with
-  [ LIN_Fu_Internal stmts ⇒
+  [ LIN_Fu_Internal stmts proof ⇒
       foldl ? ? (function_labels_internal globals) (set_empty ?) stmts
   | LIN_Fu_External _ ⇒ set_empty ?
@@ -86 +86 @@
   λglobals_old: list Identifier.
   λprf: ∀i: Identifier. member i (eq_bv ?) globals_old → member i (eq_bv ?) (map ? ? (fst ? ?) globals).
-  λstatement: LINStatement globals_old.
-  〈\fst statement, match \snd statement with
-  [ LIN_St_Return ⇒ [ Instruction (RET ?) ]
-  | LIN_St_Sequential instr _⇒
+  λstatement: PreLINStatement globals_old.
+  match statement with
+  [ Joint_St_Return ⇒ Instruction (RET ?)
+  | Joint_St_Sequential instr _⇒
     match instr with
-    [ Joint_Instr_Goto lbl ⇒ [ Jmp lbl ] 
-    | Joint_Instr_Comment _ ⇒ [ ]
-    | Joint_Instr_CostLabel lbl ⇒ [ Cost lbl ]
-    | Joint_Instr_Pop ⇒ [ Instruction (POP ? accumulator_address) ]
-    | Joint_Instr_Push ⇒ [ Instruction (PUSH ? accumulator_address) ]
-    | Joint_Instr_ClearCarry ⇒ [ Instruction (CLR ? CARRY) ]
-    | Joint_Instr_CallId f ⇒ [ Call f ]
+    [ Joint_Instr_Goto lbl ⇒ Jmp lbl
+    | Joint_Instr_Comment comment ⇒ Comment comment
+    | Joint_Instr_CostLabel lbl ⇒ Cost lbl
+    | Joint_Instr_Pop ⇒ Instruction (POP ? accumulator_address)
+    | Joint_Instr_Push ⇒ Instruction (PUSH ? accumulator_address)
+    | Joint_Instr_ClearCarry ⇒ Instruction (CLR ? CARRY)
+    | Joint_Instr_CallId f ⇒ Call f
     | Joint_Instr_OpAccs accs ⇒
       match accs with
-      [ Mul ⇒ [ Instruction (MUL ? ACC_A ACC_B) ]
-      | Divu ⇒ [ Instruction (DIV ? ACC_A ACC_B) ]
+      [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
+      | Divu ⇒ Instruction (DIV ? ACC_A ACC_B)
       | Modu ⇒ ?
       ]
     | Joint_Instr_Op1 op1 ⇒
       match op1 with
-      [ Cmpl ⇒ [ Instruction (CPL ? ACC_A) ]
-      | Inc ⇒ [ Instruction (INC ? ACC_A) ]
+      [ Cmpl ⇒ Instruction (CPL ? ACC_A)
+      | Inc ⇒ Instruction (INC ? ACC_A)
       ]
     | Joint_Instr_Op2 op2 reg ⇒
@@ -117 +117 @@
                                                        register ]] x) → ? with
         [ ACC_A ⇒ λacc_a: True.
-          [ Instruction (ADD ? ACC_A accumulator_address) ]
+          Instruction (ADD ? ACC_A accumulator_address)
         | DIRECT d ⇒ λdirect1: True.
-          [ Instruction (ADD ? ACC_A (DIRECT d)) ]
+          Instruction (ADD ? ACC_A (DIRECT d))
         | REGISTER r ⇒ λregister1: True.
-          [ Instruction (ADD ? ACC_A (REGISTER r)) ]
+          Instruction (ADD ? ACC_A (REGISTER r))
         | _ ⇒ λother: False. ⊥
         ] (subaddressing_modein … reg')
@@ -130 +130 @@
                                                        register ]] x) → ? with
         [ ACC_A ⇒ λacc_a: True.
-          [ Instruction (ADDC ? ACC_A accumulator_address) ]
+          Instruction (ADDC ? ACC_A accumulator_address)
         | DIRECT d ⇒ λdirect2: True.
-          [ Instruction (ADDC ? ACC_A (DIRECT d)) ]
+          Instruction (ADDC ? ACC_A (DIRECT d))
         | REGISTER r ⇒ λregister2: True.
-          [ Instruction (ADDC ? ACC_A (REGISTER r)) ]
+          Instruction (ADDC ? ACC_A (REGISTER r))
         | _ ⇒ λother: False. ⊥
         ] (subaddressing_modein … reg')
@@ -143 +143 @@
                                                        register ]] x) → ? with
         [ ACC_A ⇒ λacc_a: True.
-          [ Instruction (SUBB ? ACC_A accumulator_address) ]
+          Instruction (SUBB ? ACC_A accumulator_address)
         | DIRECT d ⇒ λdirect3: True.
-          [ Instruction (SUBB ? ACC_A (DIRECT d)) ]
+          Instruction (SUBB ? ACC_A (DIRECT d))
         | REGISTER r ⇒ λregister3: True.
-          [ Instruction (SUBB ? ACC_A (REGISTER r)) ]
+          Instruction (SUBB ? ACC_A (REGISTER r))
         | _ ⇒ λother: False. ⊥
         ] (subaddressing_modein … reg')
@@ -156 +156 @@
                                                        register ]] x) → ? with
         [ ACC_A ⇒ λacc_a: True.
-          [ Instruction (NOP ?) ]
+          Instruction (NOP ?)
         | DIRECT d ⇒ λdirect4: True.
-          [ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) ]
+          Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
         | REGISTER r ⇒ λregister4: True.
-          [ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) ]
+          Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
         | _ ⇒ λother: False. ⊥
         ] (subaddressing_modein … reg')
@@ -169 +169 @@
                                                        register ]] x) → ? with
         [ ACC_A ⇒ λacc_a: True.
-          [ Instruction (NOP ?) ]
+          Instruction (NOP ?)
         | DIRECT d ⇒ λdirect5: True.
-          [ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) ]
+          Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
         | REGISTER r ⇒ λregister5: True.
-          [ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) ]
+          Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
         | _ ⇒ λother: False. ⊥
         ] (subaddressing_modein … reg')
@@ -182 +182 @@
                                                        register ]] x) → ? with
         [ ACC_A ⇒ λacc_a: True.
-          [ Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉)) ]
+          Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉))
         | DIRECT d ⇒ λdirect6: True.
-          [ Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉)) ]
+          Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
         | REGISTER r ⇒ λregister6: True.
-          [ Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉)) ]
+          Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
         | _ ⇒ λother: False. ⊥
         ] (subaddressing_modein … reg')
@@ -196 +196 @@
                                                        register ]] x) → ? with
         [ REGISTER r ⇒ λregister7: True.
-          [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉)))))) ]
+          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉))))))
         | ACC_A ⇒ λacc: True.
-          [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉)))))) ]
+          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉))))))
         | DIRECT d ⇒ λdirect7: True.
-          [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉))))) ]
+          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉)))))
         | _ ⇒ λother: False. ⊥
         ] (subaddressing_modein … reg')
@@ -209 +209 @@
                                                        register ]] x) → ? with
         [ REGISTER r ⇒ λregister8: True.
-          [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉)))))) ]
+          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
         | ACC_A ⇒ λacc: True.
-          [ Instruction (NOP ?) ]
+          Instruction (NOP ?)
         | DIRECT d ⇒ λdirect8: True.
-          [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉))))) ]
+          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
         | _ ⇒ λother: False. ⊥
         ] (subaddressing_modein … reg')
@@ -222 +222 @@
                                                        register ]] x) → ? with
         [ REGISTER r ⇒ λregister9: True.
-          [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))))) ]
+          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〉)))))) ]
+          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〉)) ]
+          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)〉))))) ]
+        Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
     | Joint_Instr_CondAcc lbl ⇒
       (* dpm: this should be handled in translate_code! *)
-      [ WithLabel (JNZ ? lbl) ]
+      WithLabel (JNZ ? lbl)
     ]
-  ]〉.
+  ].
   try assumption
   try @ I
   cases ImplementedInRuntime
 qed.
+
+definition build_translated_statement ≝
+  λglobals.
+  λglobals_old.
+  λprf.
+  λstatement: LINStatement globals_old.
+    〈\fst statement, translate_statements globals globals_old prf (\snd statement)〉.
 
 definition translate_code ≝
@@ -249 +256 @@
   λprf.
   λcode: list (LINStatement globals_old).
-    flatten ? (map ? ? (translate_statements globals globals_old prf) code).
+    map ? ? (build_translated_statement globals globals_old prf) code.
     
+lemma translate_code_preserves_WellFormedP:
+  ∀globals, globals_old, prf, code.
+    WellFormedP ? ? code → WellFormedP ? ? (translate_code globals globals_old prf code).
+  #G #GO #P #C
+  elim C
+  [ normalize
+    //
+  | #G2 #G02 #IH (* CSC: understand here *)
+    whd in ⊢ (% → %)
+    normalize in ⊢ (% → %)
+    //
+  ]
+qed.
+
 definition translate_fun_def ≝
-  λglobals.λglobals_old.λprf.
+  λglobals.
+  λglobals_old.
+  λprf.
   λid_def.
     let 〈id, def〉 ≝ id_def in
     match def with
-    [ LIN_Fu_Internal code ⇒ (Label id) :: (translate_code globals globals_old prf code)
+    [ LIN_Fu_Internal code proof ⇒
+      match translate_code globals globals_old prf code return λtranscode. WellFormedP ? ? transcode → list labelled_instruction with
+      [ nil ⇒ λprf2. ⊥
+      | cons hd tl ⇒ λ_. 〈Some ? id, \snd hd〉 :: tl
+      ] (translate_code_preserves_WellFormedP globals globals_old prf code proof)
     | _ ⇒ [ ]
     ].
+    @ prf2
+qed.
     
 definition translate_functs ≝
@@ -270 +299 @@
     match main with
     [ None ⇒ [ ]
-    | Some main' ⇒ [ Call main' ; Label exit_label ; Jmp exit_label ]
+    | Some main' ⇒ [ 〈None ?, Call main'〉 ; 〈Some ? exit_label, Jmp exit_label〉 ]
     ] in
       preamble @ (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)).
@@ -287 +316 @@
 (* dpm: plays the role of the string "_exit" in the O'caml source *)
 axiom identifier_prefix: Identifier.
+
+(* dpm: fresh prefix stuff needs unifying with brian *)
 
 (*
@@ -295 +326 @@
   let global_addr ≝ globals_addr (LIN_Pr_vars p) in
     〈global_addr, translate_functs global_addr (map ? ? (fst ? ?) (LIN_Pr_vars p)) ? exit_label (LIN_Pr_main p) (LIN_Pr_funs p)〉.
-    *)
+*)

src/LTL/LTL.ma

@@ -1 +1 @@
 include "common/Graphs.ma".
-include "common/AST.ma".
-
 include "utilities/IdentifierTools.ma".
-
-include "ASM/I8051.ma".
-include "ASM/String.ma".
 
 include "LIN/LIN.ma".

src/LTL/LTLToLIN.ma

@@ -2 +2 @@
 include "LIN/LIN.ma".
 
-definition translate_statement: ∀globals. LTLStatement globals → LINStatement globals ≝
+definition translate_statement: ∀globals. LTLStatement globals → PreLINStatement globals ≝
   λglobals: list Identifier.
   λs: LTLStatement globals.
     match s with
-    [ LIN_St_Return ⇒ LIN_St_Return ? globals
-    | LIN_St_Sequential instr _ ⇒ LIN_St_Sequential ? globals instr it
+    [ Joint_St_Return ⇒ Joint_St_Return ? globals
+    | Joint_St_Sequential instr _ ⇒ Joint_St_Sequential ? globals instr it
     ].