Changeset 2208 for src/joint


Ignore:
Timestamp:
Jul 18, 2012, 1:26:43 PM (8 years ago)
Author:
tranquil
Message:
  • moving some code around
  • changed immediates to hold beval in general, not only bytes
  • fixed RTLabsToRTL after redefinitions in front end
Location:
src/joint
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint_paolo.ma

    r2186 r2208  
    3939| Labels : list label → possible_flows
    4040| Call : possible_flows.
     41
     42inductive argument (T : Type[0]) : Type[0] ≝
     43| Reg : T → argument T
     44| Imm : beval → argument T.
     45
     46definition psd_argument ≝ argument register.
     47 
     48definition psd_argument_from_reg : register → psd_argument ≝ Reg register.
     49coercion reg_to_psd_argument : ∀r : register.psd_argument ≝ psd_argument_from_reg
     50  on _r : register to psd_argument.
     51
     52definition psd_argument_from_beval : beval → psd_argument ≝ Imm register.
     53coercion beval_to_psd_argument : ∀b : beval.psd_argument ≝ psd_argument_from_beval
     54  on _b : beval to psd_argument.
     55
     56definition psd_argument_from_byte : Byte → psd_argument ≝ λb.Imm ? (BVByte b).
     57coercion byte_to_psd_argument : ∀b : Byte.psd_argument ≝ psd_argument_from_byte
     58  on _b : Byte to psd_argument.
     59
     60definition hdw_argument ≝ argument Register.
     61 
     62definition hdw_argument_from_reg : Register → hdw_argument ≝ Reg Register.
     63coercion reg_to_hdw_argument : ∀r : Register.hdw_argument ≝ hdw_argument_from_reg
     64  on _r : Register to hdw_argument.
     65
     66definition hdw_argument_from_beval : beval → hdw_argument ≝ Imm Register.
     67coercion beval_to_hdw_argument : ∀b : beval.hdw_argument ≝ hdw_argument_from_beval
     68  on _b : beval to hdw_argument.
     69
     70definition hdw_argument_from_byte : Byte → hdw_argument ≝ λb.Imm ? (BVByte b).
     71coercion byte_to_hdw_argument : ∀b : Byte.psd_argument ≝ psd_argument_from_byte
     72  on _b : Byte to hdw_argument.
     73
     74definition byte_of_nat : nat → Byte ≝ bitvector_of_nat 8.
     75definition zero_byte : Byte ≝ bv_zero 8.
    4176
    4277record step_params : Type[1] ≝
  • src/joint/semanticsUtils_paolo.ma

    r2200 r2208  
    1414(*** Store/retrieve on hardware registers ***)
    1515
    16 definition init_hw_register_env: address → hw_register_env ≝
    17  λaddr.
    18   let 〈dpl,dph〉 ≝ addr in
     16definition init_hw_register_env: xpointer → hw_register_env ≝
     17 λsp.
     18  let 〈dpl,dph〉 ≝
     19    match beval_pair_of_pointer sp return λx.beval_pair_of_pointer sp = x → ? with
     20    [ OK p ⇒ λ_.p
     21    | _ ⇒ λprf.⊥
     22    ] (refl …) in
    1923  let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in
    2024   hwreg_store RegisterDPL dpl env.
     25@hide_prf
     26normalize in prf; destruct(prf)
     27qed.
    2128
    2229(******************************** GRAPHS **************************************)
Note: See TracChangeset for help on using the changeset viewer.