Changeset 2490 for src/RTLabs


Ignore:
Timestamp:
Nov 25, 2012, 1:33:09 PM (7 years ago)
Author:
tranquil
Message:

switched back to Byte immediate (instead of beval ones)
propagated pending changes to all passes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r2290 r2490  
    2626  [ ASTint isize sign ⇒
    2727    match isize with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    28   | ASTfloat _ ⇒ ? (* dpm: not implemented *)
    2928  | ASTptr ⇒ 2 (* rgn ⇒ nat_of_bitvector ? ptr_size *)
    3029  ].
    31   cases not_implemented
    32 qed.
    3330
    3431inductive register_type: Type[0] ≝
     
    161158  λr,lenv,prf. make_addr ? (find_local_env r lenv prf).
    162159
     160definition find_and_addr_arg ≝
     161  λr,lenv,prf. make_addr ? (find_local_env_arg r lenv prf).
     162
    163163include alias "common/Identifiers.ma".
    164164let rec rtl_args (args : list register) (env : local_env) on args :
     
    270270definition size_of_cst ≝ λtyp.λcst : constant typ.match cst with
    271271  [ Ointconst size _ _ ⇒ size_intsize size
    272   | Ofloatconst _ _ ⇒ ? (* not implemented *)
    273272  | _ ⇒ 2
    274273  ].
    275   cases not_implemented qed.
    276274
    277275definition cst_well_defd : ∀ty.list ident → constant ty → Prop ≝ λty,globals,cst.
     
    296294      map2 … (λr.λb : Byte.r ← b) destrs
    297295        (split_into_bytes size const) ?
    298   | Ofloatconst _ _ ⇒ ?
    299296  | Oaddrsymbol id offset ⇒ λcst_prf,prf.
    300297    let 〈r1, r2〉 ≝ make_addr … destrs ? in
     
    304301    [(rtl_stack_address r1 r2 : joint_seq RTL globals)]
    305302  ] (pi2 … cst_sig).
    306   [2: cases not_implemented
    307   |1: cases (split_into_bytes ??) #lst
     303  [ cases (split_into_bytes ??) #lst
    308304    #EQ >EQ >prf whd in ⊢ (??%?); cases size %
    309   |3: @cst_prf
     305  | @cst_prf
    310306  |*: >prf %
    311307  ]
     
    337333     destr ← .Inc. destr ;
    338334     destr ← .Cmpl. destr ]
    339   | Imm by ⇒
    340     match by with
    341     [ BVByte b ⇒
    342       if sign_bit … b then
    343         [ destr ← (maximum … : Byte) ]
    344       else
    345         [ destr ← zero_byte ]
    346     | _ ⇒ (* should not happend ... *) [ ]
    347     ]
     335  | Imm b ⇒
     336    if sign_bit … b then
     337      [ destr ← (maximum … : Byte) ]
     338    else
     339      [ destr ← zero_byte ]
    348340  ].
    349341
     
    531523  | _ ⇒ λeq1,eq2.? (* float operations implemented in runtime *)
    532524  ] (refl …) (refl …).
    533   [3,4,5,6,7,8,9: (* floats *)  cases not_implemented
    534   |*: destruct >prf1 >prf2 [3: >length_map ] //
    535   ]
     525  destruct >prf1 >prf2 [3: >length_map ] //
    536526qed.
    537527
    538528include alias "arithmetics/nat.ma".
    539 
    540 let rec range_strong_internal (start : ℕ) (count : ℕ)
    541   (* Paolo: no notation to avoid ambiguity *)
    542   on count : list (Σn : ℕ.lt n (plus start count)) ≝
    543 match count return λx.count = x → list (Σn : ℕ. n < start + count)
    544   with
    545 [ O ⇒ λ_.[ ]
    546 | S count' ⇒ λEQ.
    547   let f : (Σn : ℕ. lt n (S start + count')) → Σn : ℕ. lt n (start + count) ≝
    548     λsig.match sig with [mk_Sig n prf ⇒ n] in
    549   start :: map … f (range_strong_internal (S start) count')
    550 ] (refl …).
    551 destruct(EQ) // qed.
    552 
    553 definition range_strong : ∀end : ℕ. list (Σn.n<end) ≝
    554   λend.range_strong_internal 0 end.
    555529
    556530definition translate_mul_i :
     
    1009983      (find_local_env_arg srcr lenv ?), lbl'❭
    1010984  | St_call_id f args retr lbl' ⇒ λstmt_typed.
    1011     ❬(match retr with
    1012       [ Some retr ⇒
    1013         CALL_ID RTL ? f (rtl_args args lenv ?) (find_local_env retr lenv ?)
    1014       | None ⇒
    1015         CALL_ID RTL ? f (rtl_args args lenv ?) [ ]
    1016       ] : bind_seq_block ???), lbl'❭
     985    ❬(CALL RTL ? (inl … f) (rtl_args args lenv ?)
     986      (match retr with
     987      [ Some retr ⇒ find_local_env retr lenv ?
     988      | None ⇒ [ ]
     989      ]) : bind_seq_block ???), lbl'❭
    1017990  | St_call_ptr f args retr lbl' ⇒ λstmt_typed.
    1018     let fs ≝ find_and_addr f lenv ?? in
    1019     ❬(rtl_call_ptr (\fst fs) (\snd fs) (rtl_args args lenv ?)
     991    let fs ≝ find_and_addr_arg f lenv ?? in
     992    ❬(CALL RTL ? (inr ?? fs) (rtl_args args lenv ?)
    1020993      (match retr with
    1021994       [ Some retr ⇒
     
    10441017    | @(lenv_typed_reg_typed_ok2 … lenv_typed dstr_prf)
    10451018    ]
    1046   |*: whd in stmt_typed; cases daemon (* TODO need more stringent statement_typed *)
     1019  |*: cases daemon (* TODO *)
    10471020  ]
    10481021qed.
     
    10521025   the start and end nodes to ensure that they are in, and place dummy
    10531026   skip instructions at these nodes. *)
    1054 definition translate_internal ≝
     1027definition translate_internal :
     1028  ∀globals.internal_function → (* insert here more properties *)
     1029  joint_closed_internal_function RTL globals ≝
    10551030  λglobals: list ident.
    10561031  λdef.
Note: See TracChangeset for help on using the changeset viewer.