Changeset 467 for Deliverables
 Timestamp:
 Jan 21, 2011, 10:02:20 AM (9 years ago)
 Location:
 Deliverables/D3.1/Csemantics
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/AST.ma
r456 r467 149 149 150 150 ndefinition 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). 152 152 (* 153 153 (** * Generic transformations over programs *) 
Deliverables/D3.1/Csemantics/Globalenvs.ma
r125 r467 72 72 73 73 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; 76 76 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; 79 79 80 80 find_symbol_exists: 81 81 ∀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) → 84 84 ∃b. find_symbol ? (globalenv ?? p) id = Some ? b; 85 85 find_funct_ptr_exists: … … 88 88 list_disjoint ? (prog_funct_names ?? p) (prog_var_names ?? p) → 89 89 in_list ? 〈id, f〉 (prog_funct ?? p) → 90 ∃ b. find_symbol ? (globalenv ?? p) id = Some ? b90 ∃sp,b. find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 91 91 ∧ find_funct_ptr ? (globalenv ?? p) b = Some ? f; 92 92 … … 100 100 ∃id. in_list ? 〈id, f〉 (prog_funct ?? p); 101 101 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〉 → 104 104 find_funct_ptr ? (globalenv ?? p) b = Some ? f → 105 105 in_list ? 〈id, f〉 (prog_funct ?? p); … … 120 120 let m ≝ init_mem ?? p in 121 121 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: 124 124 ∀F,V: Type. ∀p: program F V. 125 mem_inject_neutral (init_mem ?? p); 125 mem_inject_neutral (init_mem ?? p);*) 126 126 find_funct_ptr_negative: 127 127 ∀F,V: Type. ∀p: program F V. ∀b: block. ∀f: F. 128 128 find_funct_ptr ? (globalenv ?? p) b = Some ? f → b < 0; 129 129 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); 132 132 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; 135 135 global_addresses_distinct: 136 136 ∀F,V: Type. ∀p: program F V. ∀id1,id2,b1,b2. … … 138 138 find_symbol ? (globalenv ?? p) id1 = Some ? b1 → 139 139 find_symbol ? (globalenv ?? p) id2 = Some ? b2 → 140 b1≠b2 (*;140 b1≠b2; 141 141 142 142 (* * Commutation properties between program transformations 143 143 and operations over global environments. *) 144 *) 144 145 145 find_funct_ptr_transf: 146 146 ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V. … … 170 170 ∀v : val. ∀tf : B. 171 171 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; 173 173 174 174 (* * Commutation properties between partial program transformations … … 211 211 find_funct ? (globalenv ?? p') v = Some ? tf → 212 212 ∃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(*; 214 214 215 215 find_funct_ptr_transf_partial2: … … 300 300 ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. 301 301 match_program … match_fun match_var p p' → 302 init_mem ?? p' = init_mem ?? p*) 302 init_mem ?? p' = init_mem ?? p*)*) 303 303 }. 304 304
Note: See TracChangeset
for help on using the changeset viewer.