Changeset 467


Ignore:
Timestamp:
Jan 21, 2011, 10:02:20 AM (7 years ago)
Author:
campbell
Message:

Update some of the commented-out parts of Globalenvs for testing.

Location:
Deliverables/D3.1/C-semantics
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/AST.ma

    r456 r467  
    149149
    150150ndefinition prog_var_names ≝ λF,V: Type. λp: program F V.
    151   map ?? (λx: ident × (list init_data) × memory_space × V. fst ?? (fst ?? x)) (prog_vars ?? p).
     151  map ?? (λx: ident × (list init_data) × memory_space × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p).
    152152(*
    153153(** * Generic transformations over programs *)
  • Deliverables/D3.1/C-semantics/Globalenvs.ma

    r125 r467  
    7272
    7373  find_funct_inv:
    74     ∀F: Type. ∀ge: t F. ∀v: val. ∀f: F.
    75     find_funct ? ge v = Some ? f → ∃b. v = Vptr b zero;
     74    ∀F: Type. ∀ge: genv_t F. ∀v: val. ∀f: F.
     75    find_funct ? ge v = Some ? f → ∃b. v = Vptr Code b zero;
    7676  find_funct_find_funct_ptr:
    77     ∀F: Type. ∀ge: t F. ∀b: block.
    78     find_funct ? ge (Vptr b zero) = find_funct_ptr ? ge b;
     77    ∀F: Type. ∀ge: genv_t F. ∀sp. ∀b: block.
     78    find_funct ? ge (Vptr sp b zero) = find_funct_ptr ? ge b;
    7979
    8080  find_symbol_exists:
    8181    ∀F,V: Type. ∀p: program F V.
    82            ∀id: ident. ∀init: list init_data. ∀v: V.
    83     in_list ? 〈〈id, init〉, v〉 (prog_vars ?? p) →
     82           ∀id: ident. ∀sp. ∀init: list init_data. ∀v: V.
     83    in_list ? 〈〈〈id, init〉,sp〉, v〉 (prog_vars ?? p) →
    8484    ∃b. find_symbol ? (globalenv ?? p) id = Some ? b;
    8585  find_funct_ptr_exists:
     
    8888    list_disjoint ? (prog_funct_names ?? p) (prog_var_names ?? p) →
    8989    in_list ? 〈id, f〉 (prog_funct ?? p) →
    90     ∃b. find_symbol ? (globalenv ?? p) id = Some ? b
     90    ∃sp,b. find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉
    9191           ∧ find_funct_ptr ? (globalenv ?? p) b = Some ? f;
    9292
     
    100100    ∃id. in_list ? 〈id, f〉 (prog_funct ?? p);
    101101  find_funct_ptr_symbol_inversion:
    102     ∀F,V: Type. ∀p: program F V. ∀id: ident. ∀b: block. ∀f: F.
    103     find_symbol ? (globalenv ?? p) id = Some ? b
     102    ∀F,V: Type. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block. ∀f: F.
     103    find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉
    104104    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
    105105    in_list ? 〈id, f〉 (prog_funct ?? p);
     
    120120    let m ≝ init_mem ?? p in
    121121    valid_block m nullptr ∧
    122     (blocks m) nullptr = empty_block 0 0;
    123   initmem_inject_neutral:
     122    (blocks m) nullptr = empty_block 0 0 Any;
     123(*  initmem_inject_neutral:
    124124    ∀F,V: Type. ∀p: program F V.
    125     mem_inject_neutral (init_mem ?? p);
     125    mem_inject_neutral (init_mem ?? p);*)
    126126  find_funct_ptr_negative:
    127127    ∀F,V: Type. ∀p: program F V. ∀b: block. ∀f: F.
    128128    find_funct_ptr ? (globalenv ?? p) b = Some ? f → b < 0;
    129129  find_symbol_not_fresh:
    130     ∀F,V: Type. ∀p: program F V. ∀id: ident. ∀b: block.
    131     find_symbol ? (globalenv ?? p) id = Some ? b → b < nextblock (init_mem ?? p);
     130    ∀F,V: Type. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block.
     131    find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → b < nextblock (init_mem ?? p);
    132132  find_symbol_not_nullptr:
    133     ∀F,V: Type. ∀p: program F V. ∀id: ident. ∀b: block.
    134     find_symbol ? (globalenv ?? p) id = Some ? b → b ≠ nullptr;
     133    ∀F,V: Type. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block.
     134    find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → b ≠ nullptr;
    135135  global_addresses_distinct:
    136136    ∀F,V: Type. ∀p: program F V. ∀id1,id2,b1,b2.
     
    138138    find_symbol ? (globalenv ?? p) id1 = Some ? b1 →
    139139    find_symbol ? (globalenv ?? p) id2 = Some ? b2 →
    140     b1≠b2(*;
     140    b1≠b2;
    141141
    142142(* * Commutation properties between program transformations
    143143  and operations over global environments. *)
    144 *)
     144
    145145  find_funct_ptr_transf:
    146146    ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V.
     
    170170    ∀v : val. ∀tf : B.
    171171    find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? tf →
    172     ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = tf
     172    ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = tf;
    173173
    174174(* * Commutation properties between partial program transformations
     
    211211    find_funct ? (globalenv ?? p') v = Some ? tf →
    212212    ∃f : A.
    213       find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = OK ? tf;
     213      find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = OK ? tf(*;
    214214
    215215  find_funct_ptr_transf_partial2:
     
    300300           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
    301301    match_program … match_fun match_var p p' →
    302     init_mem ?? p' = init_mem ?? p*)
     302    init_mem ?? p' = init_mem ?? p*)*)
    303303}.
    304304
Note: See TracChangeset for help on using the changeset viewer.