Changeset 1395


Ignore:
Timestamp:
Oct 17, 2011, 5:41:44 PM (8 years ago)
Author:
sacerdot
Message:

1) New versions of pointer_of_beval/beval_of_pointer with a stricter dependent

type. They allow to close several proof obligations.

2) Globalenvs no longer uses -1 as a valid function block. It starts with -2
3) joint/semantics.ma uses a -2 block for the fake address used to signal the

end of program execution. Differently from what happens in OCaml, the block
is not allocated.

Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/common/GenMem.ma

    r1213 r1395  
    126126qed.
    127127
    128 definition alloc : ∀content. mem content → Z → Z → region → mem content × block
     128definition alloc : ∀content. mem content → Z → Z → ∀r:region. mem content × Σb:block. block_region b = r
    129129  λcontent,m,lo,hi,r.
    130130  let b ≝ mk_block r (nextblock … m) in
     
    136136    (succ_nextblock_pos … m),
    137137    b〉.
     138% qed.
    138139
    139140(* Freeing a block.  Return the updated memory state where the given
  • src/common/Globalenvs.ma

    r1231 r1395  
    390390definition empty_mem ≝ empty. (* XXX*)
    391391definition empty : ∀F. genv F ≝
    392   λF. mk_genv F (λ_. None ?) (-1) (λ_. None ?).
    393 (*  mkgenv (ZMap.init None) (-1) (PTree.empty block).*)
     392  λF. mk_genv F (λ_. None ?) (-2) (λ_. None ?).
     393(*  mkgenv (ZMap.init None) (-2) (PTree.empty block).*)
    394394
    395395definition add_functs : ∀F:Type[0]. genv F → list (ident × F) → genv F ≝
  • src/joint/BEMem.ma

    r1329 r1395  
    2929definition pointer_of_address: address → res pointer ≝
    3030 λp. let 〈v1,v2〉 ≝ p in pointer_of_bevals [v1;v2].
     31definition address_of_pointer: pointer → res address ≝ beval_pair_of_pointer.
    3132
    32 (*CSC: for pointers of type Code and XData, the next function type can be
    33  strengthtened to never fail *)
    34 definition address_of_pointer: pointer → res address ≝ beval_pair_of_pointer.
     33definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝ code_pointer_of_beval_pair.
     34definition address_of_code_pointer: (Σp:pointer. ptype p = Code) → address ≝ beval_pair_of_code_pointer.
    3535
    3636definition addr_add: address → nat → res address ≝
    3737 λaddr,n.
    38   do ptr ← pointer_of_address addr ;
    39   address_of_pointer (shift_pointer 16 ptr (bitvector_of_nat … n)).
     38  do ptr ← code_pointer_of_address addr ;
     39  OK … (address_of_code_pointer (shift_pointer 16 ptr (bitvector_of_nat … n))).
     40normalize cases ptr #p #E @E
     41qed.
    4042
    4143definition addr_sub: address → nat → res address ≝
    4244 λaddr,n.
    43   do ptr ← pointer_of_address addr ;
    44   address_of_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n)).
     45  do ptr ← code_pointer_of_address addr ;
     46  OK … (address_of_code_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n))).
     47normalize cases ptr #p #E @E
     48qed.
  • src/joint/BEValues.ma

    r1359 r1395  
    33
    44include "common/Pointers.ma".
     5include "utilities/sigma.ma".
    56
    67record part (r: region): Type[0] ≝
     
    105106% qed.
    106107
     108definition beval_pair_of_code_pointer: (Σp:pointer. ptype p = Code) → beval × beval ≝
     109 λp. match p return λp. ptype p = Code → ? with [ mk_pointer pty pbl pok poff ⇒
     110  match pty return λpty. ? → pty = Code → ? with
     111   [ Code ⇒ λpok.λE. list_to_pair ? (bevals_of_pointer (mk_pointer Code pbl ? poff)) ?
     112   | _ ⇒ λpok'.λabs. ⊥] pok] ?.
     113[@(pi2 … p) |7: // |8: %] destruct (abs)
     114qed.
     115
     116
     117axiom NotACodePointer: String.
     118definition code_pointer_of_beval_pair: beval × beval → res (Σp:pointer. ptype p = Code) ≝
     119 λp.
     120  let 〈v1,v2〉 ≝ p in
     121  do p ← pointer_of_bevals [v1;v2] ;
     122  match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = Code) with
     123  [ Code ⇒ λE.OK ? (inject … p ?)
     124  | _ ⇒ λ_.Error … [MSG NotACodePointer]] ?.
     125// qed.
     126
    107127axiom ValueNotABoolean: String.
    108128
  • src/joint/SemanticUtils.ma

    r1385 r1395  
    4545
    4646(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
    47   Maybe there is a better way to organize the code!!! *)
    48 definition graph_succ_p: label → address → res address.
    49  #l #_ generalize in match (refl … (address_of_pointer (pointer_of_label l)))
    50  cases (address_of_pointer (pointer_of_label l)) in ⊢ (???% → ?)
    51   [ #res #_ @(OK … res)
    52   | #msg cases (pointer_of_label l) * * #q #com #off #E1 destruct #E2 normalize in E2; destruct ]
    53 qed.
     47 But I can't use it directly because this one uses a concrete definition of
     48 pointer_of_label and it is used to istantiate the more_sem_params record
     49 where the abstract version is declared as a field. Is there a better way
     50 to organize the code? *)
     51definition graph_succ_p: label → address → res address ≝
     52 λl.λ_.address_of_pointer (pointer_of_label l).
    5453
    5554axiom BadProgramCounter: String.
     
    6059   state sem_params → res (joint_internal_function … (graph_params params1 globals)) ≝
    6160 λparams1,sem_params,globals,ge,st.
    62   do p ← pointer_of_address (pc … st) ;
     61  do p ← code_pointer_of_address (pc … st) ;
    6362  let b ≝ pblock p in
    6463  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
     
    7271   state sem_params → res (joint_statement (graph_params_ params1) globals) ≝
    7372 λparams1,sem_params,globals,ge,st.
    74   do p ← pointer_of_address (pc … st) ;
     73  do p ← code_pointer_of_address (pc … st) ;
    7574  do f ← graph_fetch_function … ge st ;
    7675  do l ← label_of_pointer p;
  • src/joint/semantics.ma

    r1390 r1395  
    7979 ≝ sem_params_of_sem_params2 on _x: sem_params2 ? to sem_params.
    8080
    81 definition address_of_label: sem_params → label → address.
    82  #p #l generalize in match (refl … (address_of_pointer (pointer_of_label … p l)))
    83  cases (address_of_pointer (pointer_of_label … p l)) in ⊢ (???% → ?)
    84   [ #res #_ @res
    85   | #msg cases (pointer_of_label … p l) * * #q #com #off #E1 #E2 try destruct
    86     normalize in E2; destruct ]
    87 qed.
     81definition address_of_label: sem_params → label → address ≝
     82 λp,l.address_of_code_pointer (pointer_of_label … p l).
    8883
    8984definition set_m: ∀p. bemem → state p → state p ≝
     
    352347
    353348 λpars,sparams.
    354   (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) ? (globalenv Genv … (λx.[Init_space x]) p)).
    355 cases daemon (*CSC: XXXXXXXXXXXXX*)
    356 qed.
     349 (* Invariant: a -1 block is unused in common/Globalenvs *)
     350 let b ≝ mk_block Code (-1) in
     351 let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
     352 let addr ≝ address_of_code_pointer ptr in
     353  (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) addr (globalenv Genv … (λx.[Init_space x]) p)).
     354% qed.
    357355
    358356definition make_initial_state :
Note: See TracChangeset for help on using the changeset viewer.