Changeset 2437


Ignore:
Timestamp:
Nov 6, 2012, 5:00:01 PM (7 years ago)
Author:
tranquil
Message:

generalised calls to calls with pointers

Location:
src/joint
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/joint/BEMem.ma

    r2286 r2437  
    2020  [ XData ⇒ true | Code ⇒ true | _ ⇒ false ].
    2121
    22 definition is_address : (beval × beval) → Prop ≝ λa.
    23   ∃b : Σb.bool_to_Prop (is_addressable (block_region b)).
    24   ∃p0,p1,o0,o1.
    25     \fst a = BVptr b p0 o0 ∧ part_no … p0 = 0 ∧
    26     \snd a = BVptr b p1 o1 ∧ part_no … p1 = 1 ∧
    27     bool_to_Prop (vsuffix … (eq_bv 8) o0 o1).
    28 
    29 (*
    30 definition is_addressb : (beval × beval) → bool ≝ λa.
    31   let 〈a0,a1〉 ≝ a in
    32   match a0 with
    33   [ BVptr b0 part0 o0 ⇒
    34       is_addressable (block_region b0) ∧ eqb part0 0 ∧
    35         match a1 with
    36         [ BVptr b1 part1 o1 ⇒
    37           eq_block b0 b1 ∧ eqb part1 1 ∧ subvector_with … (eq_bv 8) o0 o1
    38         | _ ⇒ false
    39         ]
    40   | _ ⇒ false
    41   ].
    42 
    43 lemma is_addressb_elim : ∀P : bool → Prop.∀a : beval × beval.
    44   (is_address a → P true) → (¬is_address a → P false) → P (is_addressb a).
    45 #P * * [||#b0|(*#r0*)#part0|#b0#part0#o0] #a1
    46 [5: whd in match is_addressb; normalize nodelta
    47   elim (true_or_false_Prop (is_addressable (block_region b0)))
    48   #H >H
    49   [ @(eqb_elim part0 0) #Heq
    50     [ cases a1 [||#b1|(*#r1*)#part1|#b1#part1#o1] whd in match (?∧?);
    51       [5: @eq_block_elim #Heq'
    52         [ @(eqb_elim part1 1) #Heq''
    53           [ elim (true_or_false_Prop (subvector_with … (eq_bv 8) o0 o1)) #Heq''' >Heq'''
    54             [ #Ptrue #_ @Ptrue destruct
    55               %{b1} [assumption] %{part0} %{part1} %{o0} %{o1}
    56               % [ % [ % [ % ]]] try assumption %
    57             ]
    58           ]
    59         ]
    60       ]
    61     ]
    62   ]
    63 ]
    64 #_ #Pfalse @Pfalse % ** #b0' #H' * #part0' * #part1' * #o0' * #o1' ****
    65 #H0 #H1 #H2 #H3 #H4 destruct /2 by absurd/
    66 qed.
    67 *)
    68 
    6922(* CSC: only pointers to XRAM or code memory ATM *)
    7023definition address ≝ beval × beval.
    71 
    72 (* definition safe_address ≝ Sig address is_address.
    73 unification hint 0 ≔ ;
    74 P ≟ Prod beval beval
    75 (*------------------*)⊢
    76 safe_address ≡ Sig P is_address. *)
    77 
    78 definition eq_address: address → address → bool ≝
    79  λaddr1,addr2.
    80   eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).
    8124
    8225definition pointer_of_address: address → res pointer ≝
    8326 λp. let 〈v1,v2〉 ≝ p in pointer_of_bevals [v1;v2].
    8427
     28definition is_address : (beval × beval) → Prop ≝ λa.
     29  ∃ptr.pointer_of_address a = OK … ptr.
     30
    8531lemma bevals_of_pointer_is_address :
    8632  ∀p.is_address (list_to_pair … (bevals_of_pointer p) (refl …)).
    87 * #b * #o whd in ⊢ (?%); whd
    88 %{b} [ elim (block_region b) % ] %{(mk_part 0 ?)} [ %2 %1 ] %{(mk_part 1 ?)} [ %1 ]
    89 @(vsplit_elim … 8 8 o) #o1 #o0 #EQ >EQ -o
    90 %{[[o0]]} %{[[o1;o0]]}
    91 % [2: change with (bool_to_Prop (if eq_bv ??? then ? else ?))
    92       >eq_bv_refl % ]
    93 %%[2: normalize nodelta @vsplit_elim #pre >(Vector_O … pre) #post #EQ
    94       normalize in EQ; <EQ -pre -post
    95       whd in match (rvsplit ????);
    96       <(vsplit_prod … (refl …)) normalize nodelta
    97   | % [2: % ]
    98   ]
    99 whd in match (rvsplit ????);
    100 try <(vector_append_empty … o0) in ⊢ (??%?);
    101 <(vsplit_prod … (refl …)) normalize nodelta %
    102 qed.
    103 
    104 lemma is_address_to_pointer : ∀a.is_address a → ∃p.pointer_of_address a = return p.
    105 * #a0 #a1 ** #bl #bl_prf ** #p0 #p0_prf ** #p1 #p1_prf * #o0' * #o1o0 ****
    106 #EQ1 #EQ2 #EQ3 #EQ4 destruct
    107 @(Vector_pair_elim … o1o0) #o1 #o0 #EQ >EQ -o1o0
    108 @(Vector_singl_elim … o0') #o0'' #EQ >EQ -o0'
    109 whd in ⊢ (?%→?);
    110 @eq_bv_elim #EQ * >EQ -o0''
    111 whd in match (pointer_of_address ?);
    112 >eq_block_b_b >(eqb_n_n 1)
    113 >vsuffix_vflatten
    114 [2: change with (bool_to_Prop (vsuffix ????? ([[?]]@@[[?]])))
    115   @vsuffix_true change with (bool_to_Prop (if eq_bv ? o0 o0 then ? else ?))
    116   >eq_bv_refl % ]
    117 normalize nodelta
    118 whd in ⊢ (??(λ_.??%?));
    119 % [2: % |]
     33* #bl #o
     34whd in ⊢ (?%); whd %
     35[2: whd in ⊢ (??%?);
     36  >eq_block_b_b
     37  change with (eq_bv ???) in match (eq_bv_suffix ?????);
     38  >eq_bv_refl normalize %]
    12039qed.
    12140
     
    16382qed.*)
    16483   
    165 definition address_of_pointer : pointer → res address ≝ beval_pair_of_pointer.
    166 
    167 example address_of_pointer_OK_to_safe :
    168   ∀p,a.address_of_pointer p = OK … a → is_address a.
    169 #p #a whd in match address_of_pointer; normalize nodelta
    170 #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
    171 //
    172 qed.
    173 
    17484(*definition safe_address_of_pointer: pointer → res safe_address ≝ λp.
    17585  do a as EQ ← address_of_pointer p ; return «a ,address_of_pointer_OK_to_safe ?? EQ».
  • src/joint/Joint.ma

    r2422 r2437  
    107107  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_seq p globals
    108108  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals
    109   | CALL_ID: ident → call_args p → call_dest p → joint_seq p globals
    110   | extension_seq : ext_seq p → joint_seq p globals
    111   | extension_call : ext_call p → joint_seq p globals.
     109  | CALL: (ident + dpl_arg p×(dph_arg p)) → call_args p → call_dest p → joint_seq p globals
     110  | extension_seq : ext_seq p → joint_seq p globals.
    112111
    113112axiom EmptyString : String.
     
    129128coercion extension_seq_to_seq : ∀p,globals.∀s : ext_seq p.joint_seq p globals ≝
    130129  extension_seq on _s : ext_seq ? to joint_seq ??.
    131 coercion extension_call_to_seq : ∀p,globals.∀s : ext_call p.joint_seq p globals ≝
    132   extension_call on _s : ext_call ? to joint_seq ??.
    133  
     130
    134131(* inductive joint_branch (p : step_params) : Type[0] ≝
    135132  | COND: acc_a_reg p → label → joint_branch p
     
    150147  [ step_seq s ⇒
    151148    match s with
    152     [ CALL_ID _ _ _ ⇒ Call
    153     | extension_call _ ⇒ Call
     149    [ CALL _ _ _ ⇒ Call
    154150    | _ ⇒ Labels … [ ]
    155151    ]
  • src/joint/semantics.ma

    r2422 r2437  
    152152      F globals → state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars))
    153153  ; ext_tailcall_id : ∀globals.genv_gen F globals → ext_tailcall uns_pars →
    154       state st_pars → IO io_out io_in ident
    155   ; eval_ext_call: ∀globals.genv_gen F globals →
    156       ext_call uns_pars → state st_pars →
    157       IO io_out io_in ((step_flow uns_pars (F globals) Call)×(state st_pars))
    158   ; ext_call_id : ∀globals.genv_gen F globals → ext_call uns_pars →
    159154      state st_pars → IO io_out io_in ident
    160155  ; pop_frame: ∀globals.genv_gen F globals → F globals → state st_pars → res (state st_pars)
     
    256251definition save_ra : ∀p. state p → cpointer → res (state p) ≝
    257252 λp,st,l.
    258   ! 〈addrl,addrh〉 ← address_of_pointer l ; (* always succeeds *)
     253  ! 〈addrl,addrh〉 ← beval_pair_of_pointer l ; (* always succeeds *)
    259254  ! st' ← push … st addrl;
    260255  push … st' addrh.
     
    431426axiom BadFunction : String.
    432427axiom SuccessorNotProvided : String.
     428
     429definition block_of_call ≝ λp:sem_params.λglobals.
     430  λge: genv p globals.λst : state p.λf.
     431  match f with
     432  [ inl id ⇒
     433    opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id)
     434  | inr addr ⇒
     435    ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
     436    ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
     437    ! ptr ← pointer_of_bevals [addr_l ; addr_h] ;
     438    if eq_bv … (bv_zero …) (offv (poff … ptr)) then
     439      return pblock ptr
     440    else Error … [MSG BadFunction]
     441  ].
    433442
    434443definition eval_seq_no_pc :
     
    455464  | ADDRESS id prf ldest hdest ⇒
    456465    let addr ≝ opt_safe ? (find_symbol … ge id) ? in
    457     ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer addr zero_offset) ;
     466    ! 〈laddr,haddr〉 ← beval_pair_of_pointer (mk_pointer addr zero_offset) ;
    458467    ! st' ← dpl_store … ldest laddr st;
    459468    dph_store … hdest haddr st'
     
    486495  | MOVE dst_src ⇒
    487496    pair_reg_move … st dst_src
    488   | CALL_ID id args dest ⇒
    489     ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
     497  | CALL f args dest ⇒
     498    ! b ← block_of_call … ge st f : IO ???;
    490499    ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ;
    491     return st'
    492   | extension_call s ⇒
    493     !〈flow, st'〉 ← eval_ext_call … ge s st ;
    494500    return st'
    495501  | _ ⇒ return st
     
    507513  IO io_out io_in (step_flow p ? (step_flows … s)) ≝
    508514  λp,g,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with
    509   [ CALL_ID id args dest ⇒
    510     ! b ← opt_to_res \ldots  [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
     515  [ CALL f args dest ⇒
     516    ! b ← block_of_call … ge st f : IO ???;
    511517    ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ;
    512     return flow
    513   | extension_call s ⇒
    514     !〈flow, st'〉 ← eval_ext_call … ge s st ;
    515518    return flow
    516519  | _ ⇒ return Proceed ???
Note: See TracChangeset for help on using the changeset viewer.