Changeset 723 for src/LIN


Ignore:
Timestamp:
Mar 30, 2011, 12:34:25 PM (9 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/LIN
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LIN.ma

    r722 r723  
    1 include "arithmetics/nat.ma".
    2 include "ASM/String.ma".
     1include "LIN/JointLTLLIN.ma".
     2 
     3definition PreLINStatement ≝ JointStatement unit.
    34
    4 include "ASM/I8051.ma".
    5 include "common/AST.ma".
    6 
    7 alias id "ASMOp1" = "cic:/matita/cerco/ASM/I8051/Op1.ind(1,0,0)".
    8 alias id "ASMOp2" = "cic:/matita/cerco/ASM/I8051/Op2.ind(1,0,0)".
    9 
    10 inductive JointInstruction (globals: list Identifier): Type[0] ≝
    11   | Joint_Instr_Goto: Identifier → JointInstruction globals
    12   | Joint_Instr_Comment: String → JointInstruction globals
    13   | Joint_Instr_CostLabel: Identifier → JointInstruction globals
    14   | Joint_Instr_Int: Register → Byte → JointInstruction globals
    15   | Joint_Instr_Pop: JointInstruction globals
    16   | Joint_Instr_Push: JointInstruction globals
    17   | Joint_Instr_Address: ∀i: Identifier. (member i (eq_bv ?) globals) → JointInstruction globals
    18   | Joint_Instr_FromAcc: Register → JointInstruction globals
    19   | Joint_Instr_ToAcc: Register → JointInstruction globals
    20   | Joint_Instr_OpAccs: OpAccs → JointInstruction globals
    21   | Joint_Instr_Op1: Op1 → JointInstruction globals
    22   | Joint_Instr_Op2: Op2 → Register → JointInstruction globals
    23   | Joint_Instr_ClearCarry: JointInstruction globals
    24   | Joint_Instr_Load: JointInstruction globals
    25   | Joint_Instr_Store: JointInstruction globals
    26   | Joint_Instr_CallId: Identifier → JointInstruction globals
    27   | Joint_Instr_CondAcc: Identifier → JointInstruction globals.
    28 
    29 inductive JointStatement (A: Type[0]) (globals: list Identifier): Type[0] ≝
    30   | LIN_St_Sequential: JointInstruction globals → A → JointStatement A globals
    31   | LIN_St_Return: JointStatement A globals.
    32  
    335definition LINStatement ≝
    346  λglobals.
    35     option Identifier × (JointStatement unit globals).
    36  
    37 definition LINInternalFunction ≝ λglobals. list (LINStatement globals).
     7    option Identifier × (PreLINStatement globals).
    388
     9definition WellFormedP ≝
     10  λA, B: Type[0].
     11  λcode: list (option A × B).
     12    match code with
     13    [ nil ⇒ False
     14    | cons hd tl ⇒
     15      match \fst hd with
     16      [ Some lbl ⇒ False
     17      | None ⇒ True
     18      ]
     19    ].
     20   
    3921inductive LINFunctionDefinition (globals: list Identifier): Type[0] ≝
    40   LIN_Fu_Internal: LINInternalFunction globals → LINFunctionDefinition globals
     22  LIN_Fu_Internal: ∀code: list (LINStatement globals). WellFormedP ? ? code → LINFunctionDefinition globals
    4123| LIN_Fu_External: ExternalFunction → LINFunctionDefinition globals.
    4224
  • src/LIN/LINToASM.ma

    r722 r723  
    3232  let generated ≝
    3333    match instr with
    34     [ LIN_St_Sequential instr' _ ⇒
     34    [ Joint_St_Sequential instr' _ ⇒
    3535        match instr' with
    3636        [ Joint_Instr_Goto lbl ⇒ set_insert ? lbl (set_empty ?)
     
    3939        | _ ⇒ set_empty ?
    4040        ]
    41     | LIN_St_Return ⇒ set_empty ?
     41    | Joint_St_Return ⇒ set_empty ?
    4242    ] in
    4343  match label with
     
    5959  let 〈ignore, fun_def〉 ≝ f in
    6060  match fun_def return λ_. BitVectorTrieSet ? with
    61   [ LIN_Fu_Internal stmts
     61  [ LIN_Fu_Internal stmts proof
    6262      foldl ? ? (function_labels_internal globals) (set_empty ?) stmts
    6363  | LIN_Fu_External _ ⇒ set_empty ?
     
    8686  λglobals_old: list Identifier.
    8787  λprf: ∀i: Identifier. member i (eq_bv ?) globals_old → member i (eq_bv ?) (map ? ? (fst ? ?) globals).
    88   λstatement: LINStatement globals_old.
    89   〈\fst statement, match \snd statement with
    90   [ LIN_St_Return ⇒ [ Instruction (RET ?) ]
    91   | LIN_St_Sequential instr _⇒
     88  λstatement: PreLINStatement globals_old.
     89  match statement with
     90  [ Joint_St_Return ⇒ Instruction (RET ?)
     91  | Joint_St_Sequential instr _⇒
    9292    match instr with
    93     [ Joint_Instr_Goto lbl ⇒ [ Jmp lbl ]
    94     | Joint_Instr_Comment _ ⇒ [ ]
    95     | Joint_Instr_CostLabel lbl ⇒ [ Cost lbl ]
    96     | Joint_Instr_Pop ⇒ [ Instruction (POP ? accumulator_address) ]
    97     | Joint_Instr_Push ⇒ [ Instruction (PUSH ? accumulator_address) ]
    98     | Joint_Instr_ClearCarry ⇒ [ Instruction (CLR ? CARRY) ]
    99     | Joint_Instr_CallId f ⇒ [ Call f ]
     93    [ Joint_Instr_Goto lbl ⇒ Jmp lbl
     94    | Joint_Instr_Comment comment ⇒ Comment comment
     95    | Joint_Instr_CostLabel lbl ⇒ Cost lbl
     96    | Joint_Instr_Pop ⇒ Instruction (POP ? accumulator_address)
     97    | Joint_Instr_Push ⇒ Instruction (PUSH ? accumulator_address)
     98    | Joint_Instr_ClearCarry ⇒ Instruction (CLR ? CARRY)
     99    | Joint_Instr_CallId f ⇒ Call f
    100100    | Joint_Instr_OpAccs accs ⇒
    101101      match accs with
    102       [ Mul ⇒ [ Instruction (MUL ? ACC_A ACC_B) ]
    103       | Divu ⇒ [ Instruction (DIV ? ACC_A ACC_B) ]
     102      [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
     103      | Divu ⇒ Instruction (DIV ? ACC_A ACC_B)
    104104      | Modu ⇒ ?
    105105      ]
    106106    | Joint_Instr_Op1 op1 ⇒
    107107      match op1 with
    108       [ Cmpl ⇒ [ Instruction (CPL ? ACC_A) ]
    109       | Inc ⇒ [ Instruction (INC ? ACC_A) ]
     108      [ Cmpl ⇒ Instruction (CPL ? ACC_A)
     109      | Inc ⇒ Instruction (INC ? ACC_A)
    110110      ]
    111111    | Joint_Instr_Op2 op2 reg ⇒
     
    117117                                                       register ]] x) → ? with
    118118        [ ACC_A ⇒ λacc_a: True.
    119           [ Instruction (ADD ? ACC_A accumulator_address) ]
     119          Instruction (ADD ? ACC_A accumulator_address)
    120120        | DIRECT d ⇒ λdirect1: True.
    121           [ Instruction (ADD ? ACC_A (DIRECT d)) ]
     121          Instruction (ADD ? ACC_A (DIRECT d))
    122122        | REGISTER r ⇒ λregister1: True.
    123           [ Instruction (ADD ? ACC_A (REGISTER r)) ]
     123          Instruction (ADD ? ACC_A (REGISTER r))
    124124        | _ ⇒ λother: False. ⊥
    125125        ] (subaddressing_modein … reg')
     
    130130                                                       register ]] x) → ? with
    131131        [ ACC_A ⇒ λacc_a: True.
    132           [ Instruction (ADDC ? ACC_A accumulator_address) ]
     132          Instruction (ADDC ? ACC_A accumulator_address)
    133133        | DIRECT d ⇒ λdirect2: True.
    134           [ Instruction (ADDC ? ACC_A (DIRECT d)) ]
     134          Instruction (ADDC ? ACC_A (DIRECT d))
    135135        | REGISTER r ⇒ λregister2: True.
    136           [ Instruction (ADDC ? ACC_A (REGISTER r)) ]
     136          Instruction (ADDC ? ACC_A (REGISTER r))
    137137        | _ ⇒ λother: False. ⊥
    138138        ] (subaddressing_modein … reg')
     
    143143                                                       register ]] x) → ? with
    144144        [ ACC_A ⇒ λacc_a: True.
    145           [ Instruction (SUBB ? ACC_A accumulator_address) ]
     145          Instruction (SUBB ? ACC_A accumulator_address)
    146146        | DIRECT d ⇒ λdirect3: True.
    147           [ Instruction (SUBB ? ACC_A (DIRECT d)) ]
     147          Instruction (SUBB ? ACC_A (DIRECT d))
    148148        | REGISTER r ⇒ λregister3: True.
    149           [ Instruction (SUBB ? ACC_A (REGISTER r)) ]
     149          Instruction (SUBB ? ACC_A (REGISTER r))
    150150        | _ ⇒ λother: False. ⊥
    151151        ] (subaddressing_modein … reg')
     
    156156                                                       register ]] x) → ? with
    157157        [ ACC_A ⇒ λacc_a: True.
    158           [ Instruction (NOP ?) ]
     158          Instruction (NOP ?)
    159159        | DIRECT d ⇒ λdirect4: True.
    160           [ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) ]
     160          Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
    161161        | REGISTER r ⇒ λregister4: True.
    162           [ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) ]
     162          Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
    163163        | _ ⇒ λother: False. ⊥
    164164        ] (subaddressing_modein … reg')
     
    169169                                                       register ]] x) → ? with
    170170        [ ACC_A ⇒ λacc_a: True.
    171           [ Instruction (NOP ?) ]
     171          Instruction (NOP ?)
    172172        | DIRECT d ⇒ λdirect5: True.
    173           [ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) ]
     173          Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
    174174        | REGISTER r ⇒ λregister5: True.
    175           [ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) ]
     175          Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
    176176        | _ ⇒ λother: False. ⊥
    177177        ] (subaddressing_modein … reg')
     
    182182                                                       register ]] x) → ? with
    183183        [ ACC_A ⇒ λacc_a: True.
    184           [ Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉)) ]
     184          Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉))
    185185        | DIRECT d ⇒ λdirect6: True.
    186           [ Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉)) ]
     186          Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
    187187        | REGISTER r ⇒ λregister6: True.
    188           [ Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉)) ]
     188          Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
    189189        | _ ⇒ λother: False. ⊥
    190190        ] (subaddressing_modein … reg')
     
    196196                                                       register ]] x) → ? with
    197197        [ REGISTER r ⇒ λregister7: True.
    198           [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉)))))) ]
     198          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉))))))
    199199        | ACC_A ⇒ λacc: True.
    200           [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉)))))) ]
     200          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉))))))
    201201        | DIRECT d ⇒ λdirect7: True.
    202           [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉))))) ]
     202          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉)))))
    203203        | _ ⇒ λother: False. ⊥
    204204        ] (subaddressing_modein … reg')
     
    209209                                                       register ]] x) → ? with
    210210        [ REGISTER r ⇒ λregister8: True.
    211           [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉)))))) ]
     211          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
    212212        | ACC_A ⇒ λacc: True.
    213           [ Instruction (NOP ?) ]
     213          Instruction (NOP ?)
    214214        | DIRECT d ⇒ λdirect8: True.
    215           [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉))))) ]
     215          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
    216216        | _ ⇒ λother: False. ⊥
    217217        ] (subaddressing_modein … reg')
     
    222222                                                       register ]] x) → ? with
    223223        [ REGISTER r ⇒ λregister9: True.
    224           [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))))) ]
     224          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
    225225        | DIRECT d ⇒ λdirect9: True.
    226           [ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))))) ]
     226          Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
    227227        | ACC_A ⇒ λacc_a: True.
    228           [ Instruction (NOP ?) ]
    229         | _ ⇒ λother: False. ⊥
    230         ] (subaddressing_modein … reg')
    231     | Joint_Instr_Load ⇒ [ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) ]
    232     | Joint_Instr_Store ⇒ [ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) ]
     228          Instruction (NOP ?)
     229        | _ ⇒ λother: False. ⊥
     230        ] (subaddressing_modein … reg')
     231    | Joint_Instr_Load ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
     232    | Joint_Instr_Store ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
    233233    | Joint_Instr_Address addr proof ⇒
    234234      let look ≝ association addr globals (prf ? proof) in
    235         [ Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉))))) ]
     235        Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
    236236    | Joint_Instr_CondAcc lbl ⇒
    237237      (* dpm: this should be handled in translate_code! *)
    238       [ WithLabel (JNZ ? lbl) ]
     238      WithLabel (JNZ ? lbl)
    239239    ]
    240   ].
     240  ].
    241241  try assumption
    242242  try @ I
    243243  cases ImplementedInRuntime
    244244qed.
     245
     246definition build_translated_statement ≝
     247  λglobals.
     248  λglobals_old.
     249  λprf.
     250  λstatement: LINStatement globals_old.
     251    〈\fst statement, translate_statements globals globals_old prf (\snd statement)〉.
    245252
    246253definition translate_code ≝
     
    249256  λprf.
    250257  λcode: list (LINStatement globals_old).
    251     flatten ? (map ? ? (translate_statements globals globals_old prf) code).
     258    map ? ? (build_translated_statement globals globals_old prf) code.
    252259   
     260lemma translate_code_preserves_WellFormedP:
     261  ∀globals, globals_old, prf, code.
     262    WellFormedP ? ? code → WellFormedP ? ? (translate_code globals globals_old prf code).
     263  #G #GO #P #C
     264  elim C
     265  [ normalize
     266    //
     267  | #G2 #G02 #IH (* CSC: understand here *)
     268    whd in ⊢ (% → %)
     269    normalize in ⊢ (% → %)
     270    //
     271  ]
     272qed.
     273
    253274definition translate_fun_def ≝
    254   λglobals.λglobals_old.λprf.
     275  λglobals.
     276  λglobals_old.
     277  λprf.
    255278  λid_def.
    256279    let 〈id, def〉 ≝ id_def in
    257280    match def with
    258     [ LIN_Fu_Internal code ⇒ (Label id) :: (translate_code globals globals_old prf code)
     281    [ LIN_Fu_Internal code proof ⇒
     282      match translate_code globals globals_old prf code return λtranscode. WellFormedP ? ? transcode → list labelled_instruction with
     283      [ nil ⇒ λprf2. ⊥
     284      | cons hd tl ⇒ λ_. 〈Some ? id, \snd hd〉 :: tl
     285      ] (translate_code_preserves_WellFormedP globals globals_old prf code proof)
    259286    | _ ⇒ [ ]
    260287    ].
     288    @ prf2
     289qed.
    261290   
    262291definition translate_functs ≝
     
    270299    match main with
    271300    [ None ⇒ [ ]
    272     | Some main' ⇒ [ Call main' ; Label exit_label ; Jmp exit_label ]
     301    | Some main' ⇒ [ 〈None ?, Call main'〉 ; 〈Some ? exit_label, Jmp exit_label〉 ]
    273302    ] in
    274303      preamble @ (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)).
     
    287316(* dpm: plays the role of the string "_exit" in the O'caml source *)
    288317axiom identifier_prefix: Identifier.
     318
     319(* dpm: fresh prefix stuff needs unifying with brian *)
    289320
    290321(*
     
    295326  let global_addr ≝ globals_addr (LIN_Pr_vars p) in
    296327    〈global_addr, translate_functs global_addr (map ? ? (fst ? ?) (LIN_Pr_vars p)) ? exit_label (LIN_Pr_main p) (LIN_Pr_funs p)〉.
    297     *)
     328*)
Note: See TracChangeset for help on using the changeset viewer.