Ignore:
Timestamp:
Oct 6, 2011, 6:45:54 PM (9 years ago)
Author:
campbell
Message:

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
1 deleted
9 edited
2 copied

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/common/AST.ma

    r1153 r1311  
    3838definition ident_of_nat : nat → ident ≝ identifier_of_nat ?.
    3939
    40 (* XXX backend is currently using untagged words as identifiers. *)
    41 definition Identifier ≝ Word.
    42 
    4340definition Immediate ≝ nat. (* XXX is this the best place to put this? *)
    4441
     
    8683qed.
    8784
     85lemma reflexive_eq_region: ∀r. eq_region r r = true.
     86 * //
     87qed.
     88
    8889definition eq_region_dec : ∀r1,r2:region. (r1=r2)+(r1≠r2).
    8990#r1 #r2 @(eq_region_elim ? r1 r2) /2/; qed.
     
    279280programs are common to all languages. *)
    280281
    281 record program (F,V: Type[0]) : Type[0] := {
    282   prog_funct: list (ident × F);
    283   prog_main: ident;
    284   prog_vars: list (ident × region × V)
     282record program (F: list ident → Type[0]) (V: Type[0]) : Type[0] := {
     283  prog_vars: list (ident × region × V);
     284  prog_funct: list (ident × (F (map … (λx. \fst (\fst x)) prog_vars)));
     285  prog_main: ident
    285286}.
    286287
    287288
    288 definition prog_funct_names ≝ λF,V: Type[0]. λp: program F V.
    289   map ? ? (fst ident F) (prog_funct ?? p).
    290 
    291 definition prog_var_names ≝ λF,V: Type[0]. λp: program F V.
    292   map ?? (λx: ident × region × V. (\fst (\fst x))) (prog_vars ?? p).
     289definition prog_funct_names ≝ λF,V. λp: program F V.
     290  map … \fst (prog_funct … p).
     291
     292definition prog_var_names ≝ λF,V. λp: program F V.
     293  map … (λx. \fst (\fst x)) (prog_vars … p).
    293294
    294295(* * * Generic transformations over programs *)
     
    308309  map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l.
    309310
    310 definition transform_program : ∀A,B,V. (A → B) → program A V → program B V ≝
    311 λA,B,V,transf,p.
     311definition transform_program : ∀A,B,V. ∀p:program A V. (A (prog_var_names … p) → B (prog_var_names … p)) → program B V ≝
     312λA,B,V,p,transf.
    312313  mk_program B V
     314    (prog_vars A V p)
    313315    (transf_program ?? transf (prog_funct A V p))
    314     (prog_main A V p)
    315     (prog_vars A V p).
     316    (prog_main A V p).
    316317(*
    317318lemma transform_program_function:
     
    342343                         list (A × B) → res (list (A × C)) ≝
    343344λA,B,C,f. mmap ?? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).
     345
     346lemma map_partial_preserves_first:
     347 ∀A,B,C:Type[0]. ∀f: B → res C. ∀l: list (A × B). ∀l': list (A × C).
     348  map_partial … f l = OK ? l' →
     349   map … \fst l = map … \fst l'.
     350 #A #B #C #f #l elim l
     351  [ #l' #E normalize in E; destruct %
     352  | * #a #b #tl #IH #l' normalize in ⊢ (??%? → ?) cases (f b) normalize in ⊢ (? → ??%? → ?)
     353    [2: #err #E destruct
     354    | #c change with (match map_partial … f tl with [ OK x ⇒ ? | Error y ⇒ ?] = ? → ?)
     355      cases (map_partial … f tl) in IH ⊢ %
     356      #x #IH normalize in ⊢ (??%? → ?) #ABS destruct
     357      >(IH x) // ]]
     358qed.
     359
    344360(*
    345361Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
     
    414430  MSG "In function " :: CTX id :: MSG ": " :: nil.
    415431*)
    416 definition transform_partial_program : ∀A,B,V. (A → res B) → program A V → res (program B V) ≝
    417 λA,B,V,transf_partial,p.
    418   do fl ← map_partial … (*prefix_funct_name*) transf_partial (prog_funct ?? p);
    419   OK ? (mk_program … fl (prog_main ?? p) (prog_vars ?? p)).
     432definition transform_partial_program : ∀A,B,V. ∀p:program A V. (A (prog_var_names … p) → res (B (prog_var_names … p))) →  res (program B V) ≝
     433λA,B,V,p,transf_partial.
     434  do fl ← map_partial … transf_partial (prog_funct … p);
     435  OK (program B V) (mk_program … (prog_vars … p) fl (prog_main ?? p)).
     436
    420437(*
    421438Lemma transform_partial_program_function:
     
    460477  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
    461478*)
    462 definition transform_partial_program2 : ∀A,B,V,W. (A → res B) → (V → res W) →
    463                                         program A V → res (program B W) ≝
    464 λA,B,V,W, transf_partial_function, transf_partial_variable, p.
    465   do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p);
    466   do vl ← map_partial … (*prefix_var_name*) transf_partial_variable (prog_vars ?? p);
    467   OK ? (mk_program … fl (prog_main ?? p) vl).
     479
     480(* CSC: ad hoc lemma, move away? *)
     481lemma map_fst:
     482 ∀A,B,C,C':Type[0].∀l:list (A × B × C).∀l':list (A × B × C').
     483  map … \fst l = map … \fst l' →
     484  map … (λx. \fst (\fst x)) l = map … (λx. \fst (\fst x)) l'.
     485#A #B #C #C' #l elim l
     486 [ #l' elim l' // #he #tl #IH #ABS normalize in ABS; destruct
     487 | #he1 #tl1 #IH #l' cases l' [ #ABS normalize in ABS; destruct ]
     488   #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%) >(IH tl2) destruct >e0 //
     489   >e0 in e1; normalize #H @H ]
     490qed.
     491
     492definition transform_partial_program2 :
     493 ∀A,B,V,W. ∀p: program A V.
     494  (A (prog_var_names … p) → res (B (prog_var_names ?? p)))
     495  →  (V → res W) → res (program B W) ≝
     496λA,B,V,W,p, transf_partial_function, transf_partial_variable.
     497  do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p); ?.
     498  (*CSC: interactive mode because of dependent types *)
     499  generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p))
     500  cases (map_partial … transf_partial_variable (prog_vars … p))
     501  [ #vl #EQ
     502    @(OK (program B W) (mk_program … vl … (prog_main … p)))
     503    <(map_fst … (EQ vl (refl …))) @fl
     504  | #err #_ @(Error … err)]
     505qed.
     506
    468507(*
    469508Lemma transform_partial_program2_function:
     
    633672| Compare_LessEqual: Compare
    634673| Compare_GreaterEqual: Compare.
    635 
    636 (* XXX unused definitions
    637 inductive Cast: Type[0] ≝
    638   Cast_Int: Byte → Cast
    639 | Cast_AddrSymbol: Identifier → Cast
    640 | Cast_StackOffset: Immediate → Cast.
    641 
    642 inductive Data: Type[0] ≝
    643   Data_Reserve: nat → Data
    644 | Data_Int8: Byte → Data
    645 | Data_Int16: Word → Data.
    646 
    647 inductive DataSize: Type[0] ≝
    648   DataSize_Byte: DataSize
    649 | DataSize_HalfWord: DataSize
    650 | DataSize_Word: DataSize.
    651 *)
    652 
    653 definition Trace ≝ list Identifier.
    654674
    655675inductive op1: Type[0] ≝
  • Deliverables/D3.3/id-lookup-branch/common/Animation.ma

    r963 r1311  
    1818inductive snapshot (state:Type[0]) : Type[0] ≝
    1919| running : trace → state → snapshot state
    20 | finished : trace → int → mem → snapshot state
     20| finished : trace → int → state → snapshot state
    2121| input_exhausted : trace → snapshot state.
    2222
    2323axiom StoppedMidIO : String.
    2424
    25 let rec up_to_nth_step (n:nat) (ex:execstep io_out io_in) (input:list eventval) (e:execution (state ?? ex) io_out io_in) (t:trace) : res (snapshot (state ?? ex)) ≝
     25let rec up_to_nth_step (n:nat) (state:Type[0]) (input:list eventval) (e:execution state io_out io_in) (t:trace) : res (snapshot state) ≝
    2626match n with
    2727[ O ⇒ match e with [ e_step tr s _ ⇒ OK ? (running ? (t⧺tr) s)
     
    2929                   | e_interact o k ⇒ Error ? (msg StoppedMidIO)
    3030                   | e_wrong m ⇒ Error ? m ]
    31 | S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step m ex input e' (t⧺tr)
     31| S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step m state input e' (t⧺tr)
    3232                     | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m)
    3333                     | e_interact o k ⇒
     
    3535                         [ nil ⇒ OK ? (input_exhausted ? t)
    3636                         | cons h tl ⇒ do i ← get_input o h;
    37                                        up_to_nth_step m ex tl (k i) t
     37                                       up_to_nth_step m state tl (k i) t
    3838                         ]
    3939                     | e_wrong m ⇒ Error ? m
     
    4141].
    4242
    43 definition exec_up_to : ∀fx:fullexec io_out io_in. program ?? fx → nat → list eventval → res (snapshot (state ?? fx)) ≝
    44 λfx,p,n,i. up_to_nth_step n fx i (exec_inf ?? fx p) E0.
     43definition exec_up_to : ∀fx:fullexec io_out io_in. ∀p:program ?? fx. nat → list eventval → res (snapshot (state ?? fx (make_global … p))) ≝
     44λfx,p,n,i. up_to_nth_step n ? i (exec_inf ?? fx p) E0.
    4545
    4646(* A version of exec_up_to that reports the state prior to failure. *)
     
    4848inductive snapshot' (state:Type[0]) : Type[0] ≝
    4949| running' : trace → state → snapshot' state
    50 | finished' : nat → trace → int → mem → snapshot' state
     50| finished' : nat → trace → int → state → snapshot' state
    5151| input_exhausted' : trace → snapshot' state
    5252| failed' : errmsg → nat → state → snapshot' state
    5353| init_state_fail' : errmsg → snapshot' state.
    54 
     54(*
    5555let rec up_to_nth_step' (n:nat) (total:nat) (ex:execstep io_out io_in) (input:list eventval) (e:execution (state ?? ex) io_out io_in) (prev:state ?? ex) (t:trace) : snapshot' (state ?? ex) ≝
    5656match n with
     
    7979| Error m ⇒ init_state_fail' ? m
    8080].
    81 
     81*)
    8282(* Provide an easy way to get a term in proof mode for reduction.
    8383   For example,
     
    9595λr,S,s. match s with [ OK s' ⇒ match s' with [ finished t r' _ ⇒ r = r' | _ ⇒ False ] | _ ⇒ False ].
    9696
     97include "common/Mem.ma".
     98
    9799(* Hide the representation of memory to make displaying the results easier. *)
    98100
  • Deliverables/D3.3/id-lookup-branch/common/CostLabel.ma

    r757 r1311  
    77(* For use in importing programs in intermediate languages. *)
    88definition costlabel_of_nat : nat → costlabel ≝ identifier_of_nat ?.
    9 
    10 (* dpm: fix identifier/costlabel mismatch *)
    11 axiom Identifier_of_costlabel: costlabel → Identifier.
  • Deliverables/D3.3/id-lookup-branch/common/Errors.ma

    r1153 r1311  
    271271notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
    272272
     273definition res_to_opt : ∀A:Type[0]. res A → option A ≝
     274 λA.λv. match v with [ Error _ ⇒ None ? | OK v ⇒ Some … v].
     275
  • Deliverables/D3.3/id-lookup-branch/common/Globalenvs.ma

    r1153 r1311  
    5252       of function descriptions. *)
    5353
    54   globalenv: ∀F,V: Type[0]. (V → list init_data) → program F V → res (genv_t F);
     54  globalenv: ∀F,V. (V → list init_data) → ∀p:program F V. genv_t (F (prog_var_names … p));
    5555   (* * Return the global environment for the given program. *)
    5656
    57   init_mem: ∀F,V: Type[0]. (V → list init_data) → program F V → res mem;
     57  init_mem: ∀F,V. (V → list init_data) → program F V → res mem;
    5858   (* * Return the initial memory state for the given program. *)
    5959
     
    488488       (V → (list init_data)) →
    489489       genv F × mem → list (ident × region × V) →
    490        res (genv F × mem) ≝
     490       (genv F × mem) ≝
    491491λF,V,extract_init,init_env,vars.
    492492  foldl ??
    493     (λg_st: res (genv F × mem). λid_init: ident × region × V.
     493    (λg_st: genv F × mem. λid_init: ident × region × V.
    494494      let 〈id, r, init_info〉 ≝ id_init in
    495495      let init ≝ extract_init init_info in
    496         do 〈g,st〉 ← g_st;
     496      let 〈g,st〉 ≝ g_st in
    497497        match alloc_init_data st init r with [ pair st' b ⇒
    498498          let g' ≝ add_symbol ? id b g in
    499           do st'' ← opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g' st' b OZ init);
    500             OK ? 〈g', st''〉
     499            〈g', st'〉
    501500        ] )
    502     (OK ? init_env) vars.
    503 
    504 definition globalenv_initmem : ∀F,V:Type[0]. (V → (list init_data)) → program F V → res (genv F × mem) ≝
     501    init_env vars.
     502
     503definition init_globals : ∀F,V:Type[0].
     504       (V → (list init_data)) →
     505       genv F → mem → list (ident × region × V) →
     506       res mem ≝
     507λF,V,extract_init,g,m,vars.
     508  foldl ??
     509    (λst: res mem. λid_init: ident × region × V.
     510      let 〈id, r, init_info〉 ≝ id_init in
     511      let init ≝ extract_init init_info in
     512        do st ← st;
     513        match symbols ? g id with
     514        [ Some b ⇒ opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g st b OZ init)
     515        | None ⇒ Error ? (msg InitDataStoreFailed) (* ought to be impossible *)
     516        ] )
     517    (OK ? m) vars.
     518
     519definition globalenv_allocmem : ∀F,V. (V → (list init_data)) → ∀p:program F V. (genv (F (prog_var_names … p)) × mem) ≝
    505520λF,V,init_info,p.
    506   add_globals F V init_info
     521  add_globals init_info
    507522   〈add_functs ? (empty …) (prog_funct F ? p), empty_mem〉
    508523   (prog_vars ?? p).
    509524
    510 definition globalenv_ : ∀F,V:Type[0]. (V → list init_data) → program F V → res (genv F) ≝
     525definition globalenv_ : ∀F,V. (V → list init_data) → ∀p:program F V. genv (F (prog_var_names … p)) ≝
    511526λF,V,i,p.
    512   do 〈g,m〉 ← globalenv_initmem F V i p;
    513     OK ? g.
    514 definition init_mem_ : ∀F,V:Type[0]. (V → list init_data) → program F V → res (mem) ≝
     527  \fst (globalenv_allocmem F V i p).
     528
     529definition init_mem_ : ∀F,V. (V → list init_data) → program F V → res (mem) ≝
    515530λF,V,i,p.
    516   do 〈g,m〉 ← globalenv_initmem F V i p;
    517     OK ? m.
     531  let 〈g,m〉 ≝ globalenv_allocmem F V i p in
     532  init_globals ? V i g m (prog_vars ?? p).
    518533
    519534
  • Deliverables/D3.3/id-lookup-branch/common/Graphs.ma

    r1082 r1311  
    2020definition graph : Type[0] → Type[0] ≝ identifier_map LabelTag.
    2121
     22definition graph_fold ≝
     23  λA, B: Type[0].
     24  λf.
     25  λgraph: graph A.
     26  λseed: B.
     27  match graph with
     28  [ an_id_map map ⇒ fold A B 16 f map seed
     29  ].
     30
    2231axiom graph_add:
    2332  ∀A: Type[0].
  • Deliverables/D3.3/id-lookup-branch/common/SmallstepExec.ma

    r1197 r1311  
    1 
    21include "utilities/extralib.ma".
    32include "common/IOMonad.ma".
    43include "common/Integers.ma".
    54include "common/Events.ma".
    6 include "common/Mem.ma".
    75
    8 record execstep (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
    9 { genv  : Type[0]
    10 ; state : Type[0]
    11 ; is_final : state → option int
    12 ; mem_of_state : state → mem
    13 ; step : genv → state → IO outty inty (trace×state)
     6record trans_system (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
     7{ global : Type[1]
     8; state  : global → Type[0]
     9; is_final : ∀g. state g → option int
     10; step : ∀g. state g → IO outty inty (trace×(state g))
    1411}.
    1512
    16 let rec repeat (n:nat) (outty:Type[0]) (inty:outty → Type[0]) (exec:execstep outty inty)
    17                (g:genv ?? exec) (s:state ?? exec)
    18  : IO outty inty (trace × (state ?? exec)) ≝
     13let rec repeat (n:nat) (outty:Type[0]) (inty:outty → Type[0]) (exec:trans_system outty inty)
     14               (g:global ?? exec) (s:state ?? exec g)
     15 : IO outty inty (trace × (state ?? exec g)) ≝
    1916match n with
    2017[ O ⇒ Value ??? 〈E0, s〉
     
    3532(* A (possibly non-terminating) execution.   *)
    3633coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝
    37 | e_stop : trace → int → mem → execution state output input
     34| e_stop : trace → int → state → execution state output input
    3835| e_step : trace → state → execution state output input → execution state output input
    3936| e_wrong : errmsg → execution state output input
     
    4542
    4643let corec exec_inf_aux (output:Type[0]) (input:output → Type[0])
    47                        (exec:execstep output input) (ge:genv ?? exec)
    48                        (s:IO output input (trace×(state ?? exec)))
     44                       (exec:trans_system output input) (g:global ?? exec)
     45                       (s:IO output input (trace×(state ?? exec g)))
    4946                       : execution ??? ≝
    5047match s with
    5148[ Wrong m ⇒ e_wrong ??? m
    5249| Value v ⇒ match v with [ pair t s' ⇒
    53     match is_final ?? exec s' with
    54     [ Some r ⇒ e_stop ??? t r (mem_of_state ?? exec s')
    55     | None ⇒ e_step ??? t s' (exec_inf_aux ??? ge (step ?? exec ge s')) ] ]
    56 | Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? ge (k' v))
     50    match is_final ?? exec g s' with
     51    [ Some r ⇒ e_stop ??? t r s'
     52    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ] ]
     53| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
    5754].
    5855
     
    6562  here, used reflexivity instead *)
    6663
    67 axiom exec_inf_aux_unfold: ∀o,i,exec,ge,s. exec_inf_aux o i exec ge s =
     64axiom exec_inf_aux_unfold: ∀o,i,exec,g,s. exec_inf_aux o i exec g s =
    6865match s with
    6966[ Wrong m ⇒ e_wrong ??? m
    7067| Value v ⇒ match v with [ pair t s' ⇒
    71     match is_final ?? exec s' with
    72     [ Some r ⇒ e_stop ??? t r (mem_of_state ?? exec s')
    73     | None ⇒ e_step ??? t s' (exec_inf_aux ??? ge (step ?? exec ge s')) ] ]
    74 | Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? ge (k' v))
     68    match is_final ?? exec g s' with
     69    [ Some r ⇒ e_stop ??? t r s'
     70    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ] ]
     71| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
    7572].
    7673(*
     
    8380*)
    8481
    85 record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
    86 { es1 :> execstep outty inty
    87 ; program : Type[0]
    88 ; make_initial_state : program → res (genv ?? es1 × (state ?? es1))
     82record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
     83{ program : Type[0]
     84; es1 :> trans_system outty inty
     85; make_global : program → global ?? es1
     86; make_initial_state : ∀p:program. res (state ?? es1 (make_global p))
    8987}.
    9088
    91 definition exec_inf : ∀o,i.∀fx:fullexec o i. ∀p:program ?? fx. execution (state ?? fx) o i ≝
     89definition exec_inf : ∀o,i.∀fx:fullexec o i. ∀p:program ?? fx. execution (state ?? fx (make_global … fx p)) o i ≝
    9290λo,i,fx,p.
    9391  match make_initial_state ?? fx p with
    94   [ OK gs ⇒ exec_inf_aux ?? fx (\fst gs) (Value … 〈E0,\snd gs〉)
     92  [ OK s ⇒ exec_inf_aux ?? fx (make_global … fx p) (Value … 〈E0,s〉)
    9593  | Error m ⇒ e_wrong ??? m
    9694  ].
    9795
    98 
     96(* Some preliminary simulation stuff that's not been used yet.
    9997record execstep' (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
    10098{ es0 :> execstep outty inty
     
    126124          match_states sems st1' st2'
    127125}.
     126*)
  • Deliverables/D3.3/id-lookup-branch/common/Values.ma

    r961 r1311  
    1818
    1919include "utilities/Coqlib.ma".
    20 include "common/AST.ma".
    2120include "common/Floats.ma".
    2221include "common/Errors.ma".
    23 
    24 include "ASM/BitVectorZ.ma".
    25 
     22include "common/Pointers.ma".
    2623include "basics/logic.ma".
    27 
    28 include "utilities/extralib.ma".
    29 
    30 (* To define pointers we need a few details about the memory model.
    31 
    32    There are several kinds of pointers, which differ in which regions of
    33    memory they address and the pointer's representation.
    34    
    35    Pointers are given as kind, block, offset triples, where a block identifies
    36    some memory in a given region with an arbitrary concrete address.  A proof
    37    is also required that the representation is suitable for the region the
    38    memory resides in.  Note that blocks cannot extend out of a region (in
    39    particular, a pdata pointer can address any byte in a pdata block - we never
    40    need to switch to a larger xdata pointer).
    41  *)
    42 
    43 (* blocks - represented by the region the memory resides in and a unique id *)
    44 
    45 record block : Type[0] ≝
    46 { block_region : region
    47 ; block_id : Z
    48 }.
    49 
    50 definition eq_block ≝
    51 λb1,b2.
    52   eq_region (block_region b1) (block_region b2) ∧
    53   eqZb (block_id b1) (block_id b2)
    54 .
    55 
    56 lemma eq_block_elim : ∀P:bool → Prop. ∀b1,b2.
    57   (b1 = b2 → P true) → (b1 ≠ b2 → P false) →
    58   P (eq_block b1 b2).
    59 #P * #r1 #i1 * #r2 #i2 #H1 #H2
    60 whd in ⊢ (?%) @eq_region_elim #H3
    61 [ whd in ⊢ (?%) @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ]
    62 | @H2 % #E destruct elim H3 /2/
    63 ] qed.
    64 
    65 lemma eq_block_b_b : ∀b. eq_block b b = true.
    66 * * #z whd in ⊢ (??%?) >eqZb_z_z @refl
    67 qed.
    68 
    69 (* Characterise the memory regions which the pointer representations can
    70    address.
    71 
    72    pointer_compat <block> <pointer representation> *)
    73 
    74 inductive pointer_compat : block → region → Prop ≝
    75 |        same_compat : ∀s,id. pointer_compat (mk_block s id) s
    76 |      pxdata_compat : ∀id. pointer_compat (mk_block PData id) XData
    77 |   universal_compat : ∀r,id. pointer_compat (mk_block r id) Any.
    78 
    79 lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p.
    80 * * #id *;
    81 try ( %1 // )
    82 %2 % #H inversion H #e1 #e2 try #e3 try #e4 destruct
    83 qed.
    84 
    85 definition is_pointer_compat : block → region → bool ≝
    86 λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].
    87 
    88 (* Offsets into the block.  We allow integers like CompCert so that we have
    89    the option of extending blocks backwards. *)
    90 
    91 record offset : Type[0] ≝ { offv : Z }.
    92 
    93 definition eq_offset ≝ λx,y. eqZb (offv x) (offv y).
    94 definition shift_offset : ∀n. offset → BitVector n → offset ≝
    95   λn,o,i. mk_offset (offv o + Z_of_signed_bitvector ? i).
    96 (* A version of shift_offset_n for multiplied addresses which avoids overflow. *)
    97 definition shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
    98   λn,o,i,j. mk_offset (offv o + (Z_of_nat i)*(Z_of_signed_bitvector ? j)).
    99 definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝
    100   λn,o,i. mk_offset (offv o - Z_of_signed_bitvector ? i).
    101 definition neg_shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
    102   λn,o,i,j. mk_offset (offv o - (Z_of_nat i) * (Z_of_signed_bitvector ? j)).
    103 definition sub_offset : ∀n. offset → offset → BitVector n ≝
    104   λn,x,y. bitvector_of_Z ? (offv x - offv y).
    105 definition zero_offset ≝ mk_offset OZ.
    106 definition lt_offset : offset → offset → bool ≝
    107   λx,y. Zltb (offv x) (offv y).
    10824
    10925(* * A value is either:
Note: See TracChangeset for help on using the changeset viewer.