Changeset 2074 for src/Clight/SimplifyCasts.ma
- Timestamp:
- Jun 14, 2012, 10:23:08 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/SimplifyCasts.ma
r2032 r2074 211 211 212 212 (* Simulation relation used for expression evaluation. *) 213 inductive simulate(A : Type[0]) (r1 : res A) (r2 : res A) : Prop ≝214 | SimOk : (∀a:A. r1 = OK ? a → r2 = OK ? a) → simulateA r1 r2215 | SimFail : (∃err. r1 = Error ? err) → simulateA r1 r2.213 inductive res_sim (A : Type[0]) (r1 : res A) (r2 : res A) : Prop ≝ 214 | SimOk : (∀a:A. r1 = OK ? a → r2 = OK ? a) → res_sim A r1 r2 215 | SimFail : (∃err. r1 = Error ? err) → res_sim A r1 r2. 216 216 217 217 (* Invariant of simplify_expr *) … … 221 221 result_flag = false → 222 222 typeof e1 = typeof e2 → 223 simulate? (exec_expr ge en m e1) (exec_expr ge en m e2) →224 simulate? (exec_lvalue ge en m e1) (exec_lvalue ge en m e2) →223 res_sim ? (exec_expr ge en m e1) (exec_expr ge en m e2) → 224 res_sim ? (exec_lvalue ge en m e1) (exec_lvalue ge en m e2) → 225 225 simplify_inv ge en m e1 e2 target_sz target_sg result_flag 226 226 (* Inv_coerce_ok states that we successfuly squeezed the source expression to [target_sz]. The details are hidden in [smaller_integer_val]. *) … … 233 233 (* Invariant of simplify_inside *) 234 234 definition conservation ≝ λe,result:expr. 235 ∀ge,en,m. simulate? (exec_expr ge en m e) (exec_expr ge en m result)236 ∧ simulate? (exec_lvalue ge en m e) (exec_lvalue ge en m result)235 ∀ge,en,m. res_sim ? (exec_expr ge en m e) (exec_expr ge en m result) 236 ∧ res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge en m result) 237 237 ∧ typeof e = typeof result. 238 238 … … 2077 2077 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx). 2078 2078 2079 lemma simulation_transitive : ∀A,r0,r1,r2. simulate A r0 r1 → simulate A r1 r2 → simulateA r0 r2.2079 lemma simulation_transitive : ∀A,r0,r1,r2. res_sim A r0 r1 → res_sim A r1 r2 → res_sim A r0 r2. 2080 2080 #A #r0 #r1 #r2 * 2081 2081 [ 2: * #error #H >H #_ @SimFail /2 by ex_intro/ … … 2086 2086 2087 2087 lemma sim_related_globals : ∀ge,ge',en,m. related_globals ? simplify_fundef ge ge' → 2088 (∀e. simulate? (exec_expr ge en m e) (exec_expr ge' en m e)) ∧2089 (∀ed, ty. simulate? (exec_lvalue' ge en m ed ty) (exec_lvalue' ge' en m ed ty)).2088 (∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m e)) ∧ 2089 (∀ed, ty. res_sim ? (exec_lvalue' ge en m ed ty) (exec_lvalue' ge' en m ed ty)). 2090 2090 #ge #ge' #en #m #Hrelated @expr_lvalue_ind_combined 2091 2091 [ 1: #sz #ty #i @SimOk #a normalize // … … 2237 2237 lemma related_globals_expr_simulation : ∀ge,ge',en,m. 2238 2238 related_globals ? simplify_fundef ge ge' → 2239 ∀e. simulate? (exec_expr ge en m e) (exec_expr ge' en m (simplify_e e)) ∧2239 ∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m (simplify_e e)) ∧ 2240 2240 typeof e = typeof (simplify_e e). 2241 2241 #ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?); … … 2253 2253 lemma related_globals_lvalue_simulation : ∀ge,ge',en,m. 2254 2254 related_globals ? simplify_fundef ge ge' → 2255 ∀e. simulate? (exec_lvalue ge en m e) (exec_lvalue ge' en m (simplify_e e)) ∧2255 ∀e. res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge' en m (simplify_e e)) ∧ 2256 2256 typeof e = typeof (simplify_e e). 2257 2257 #ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?); … … 2272 2272 lemma related_globals_exprlist_simulation : ∀ge,ge',en,m. 2273 2273 related_globals ? simplify_fundef ge ge' → 2274 ∀args. simulate? (exec_exprlist ge en m args ) (exec_exprlist ge' en m (map expr expr simplify_e args)).2274 ∀args. res_sim ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m (map expr expr simplify_e args)). 2275 2275 #ge #ge' #en #m #Hrelated #args 2276 2276 elim args
Note: See TracChangeset
for help on using the changeset viewer.