Ignore:
Timestamp:
Oct 6, 2011, 5:27:32 PM (8 years ago)
Author:
mulligan
Message:

changes to translate_cst

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1307 r1308  
    127127  λglobals,dest_lbl,r,i. sequential rtl_params_ globals (INT … r i) dest_lbl.
    128128
     129axiom split_into_bytes:
     130  ∀size.
     131  ∀int: bvint size.
     132    Σbytes: list Byte. |bytes| = size_intsize size.
     133
     134lemma eqb_implies_eq:
     135  ∀m, n: nat.
     136    eqb m n = true → m = n.
     137  #M
     138  elim M
     139  [1: #N normalize
     140      cases N
     141      [1: normalize //
     142      |2: #M' normalize #HYP destruct(HYP)
     143      ]
     144  |2: #M' #IND_HYP #N
     145      normalize
     146      cases N
     147      [1: normalize #HYP destruct(HYP)
     148      |2: #M'' normalize #HYP
     149          @eq_f @(IND_HYP M'')
     150          assumption
     151      ]
     152   ]
     153qed.
     154
    129155let rec translate_cst
    130156  (globals: list ident) (cst: constant) (destrs: list register)
     
    134160  [ Ointconst size const ⇒
    135161    match destrs with
    136     [ nil        ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
    137     | cons hd tl ⇒ ?
     162    [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
     163    | _   ⇒
     164      let size' ≝ size_intsize size in
     165        match eqb size' (|destrs|) return λx. (eqb size' (|destrs|)) = x → rtl_internal_function globals with
     166        [ true  ⇒ λgood_case.
     167          match split_into_bytes size const with
     168          [ dp bytes bytes_length_proof ⇒
     169            let mapped ≝ map2 … (λd. λb. (sequential … (INT rtl_params_ globals d b))) destrs bytes ? in
     170              adds_graph rtl_params1 globals mapped start_lbl dest_lbl def
     171          ]
     172        | false ⇒ λbad_case. ?
     173        ] (refl … (eqb size' (|destrs|)))
    138174    ]
    139175  | Ofloatconst float ⇒ ⊥
    140   | Oaddrsymbol id offset ⇒ ?
    141   | Oaddrstack offset ⇒ ?
    142   ].
    143   [5: cases not_implemented (* XXX: float, error_float in o'caml *)
     176  | Oaddrsymbol id offset ⇒
     177    let 〈r1, r2〉 ≝ make_addr … destrs ? in
     178      add_graph rtl_params1 globals start_lbl (sequential … (ADDRESS rtl_params_ globals id ? r1 r2) dest_lbl) def
     179  | Oaddrstack offset ⇒
     180    let 〈r1, r2〉 ≝ make_addr … destrs ? in
     181      add_graph rtl_params1 globals start_lbl (sequential … (STACK_ADDRESS rtl_params_ globals r1 r2) dest_lbl) def
     182  ].
     183  [1: >bytes_length_proof
     184      cut(size' = |destrs|)
     185      [1: @eqb_implies_eq
     186          assumption
     187      |2: #EQ_HYP
     188          <EQ_HYP %
     189      ]
     190  |5: cases not_implemented (* XXX: float, error_float in o'caml *)
    144191  ].
    145192 
Note: See TracChangeset for help on using the changeset viewer.