Changeset 1285
 Timestamp:
 Oct 3, 2011, 3:08:21 PM (9 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1283 r1285 216 216 ] start_lbl dest_lbl def. 217 217 218 (* 219 definition translate_cast_signed≝220 λglobals .218 definition translate_cast_signed: 219 ∀globals: list ident. list register → ? → label → label → rtl_internal_function globals → rtl_internal_function globals ≝ 220 λglobals: list ident. 221 221 λdestrs. 222 222 λsrcr. … … 229 229 let 〈def, dummy〉 ≝ fresh_reg … def in 230 230 let insts ≝ [ 231 rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl; 232 rtl_st_op2 And tmpr tmp_128 srcr start_lbl; 233 rtl_st_opaccs DivuModu tmpr dummy tmpr tmp_128 start_lbl; 234 rtl_st_int tmp_255 (bitvector_of_nat ? 255) start_lbl; 235 rtl_st_opaccs Mul tmpr dummy tmpr tmp_255 start_lbl 236 ] in 231 sequential … (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128)); 232 sequential … (OP2 rtl_params_ globals And tmpr tmp_128 srcr); 233 sequential … (OPACCS rtl_params_ globals DivuModu tmpr dummy tmpr tmp_128); 234 sequential … (INT rtl_params_ globals tmp_255 (bitvector_of_nat ? 255)); 235 sequential … (OPACCS rtl_params_ globals Mul tmpr dummy tmpr tmp_255) 236 ] 237 in 237 238 let srcrs ≝ make … tmpr (length … destrs) in 238 add_translates …[239 adds_graph …insts;240 translate_move destrs srcrs239 add_translates rtl_params1 globals [ 240 adds_graph rtl_params1 globals insts; 241 translate_move globals destrs srcrs 241 242 ] start_lbl dest_lbl def. 242 243 243 244 definition translate_cast ≝ 244 λsrc_size. 245 λsrc_sign. 246 λdest_size. 247 λdestrs. 248 λsrcrs. 245 λglobals: list ident. 246 λsrc_size: nat. 247 λsrc_sign: signedness. 248 λdest_size: nat. 249 λdestrs: list register. 250 λsrcrs: list register. 249 251 match srcrs return λx. srcrs = x → ? with 250 [ O ⇒ λzero_prf. adds_graph [ ]252 [ O ⇒ λzero_prf. adds_graph rtl_params1 globals [ ] 251 253  S n' ⇒ λsucc_prf. 252 254 if ltb dest_size src_size then 253 translate_move destrs srcrs255 translate_move globals destrs srcrs 254 256 else 255 257 match reduce_strong register register destrs srcrs with … … 259 261 let restl ≝ \snd (\fst crl) in 260 262 let restr ≝ \snd (\snd crl) in 261 let insts_common ≝ translate_move commonl commonr in263 let insts_common ≝ translate_move globals commonl commonr in 262 264 let sign_reg ≝ last_safe ? srcrs ? in 263 265 let insts_sign ≝ 264 266 match src_sign with 265 [ Unsigned ⇒ translate_cast_unsigned restl266  Signed ⇒ translate_cast_signed restl sign_reg267 [ Unsigned ⇒ translate_cast_unsigned globals restl 268  Signed ⇒ translate_cast_signed globals restl sign_reg 267 269 ] 268 270 in 269 add_translates [ insts_common; insts_sign ]271 add_translates rtl_params1 globals [ insts_common; insts_sign ] 270 272 ] 271 273 ] (refl ? (srcrs)). … … 274 276 275 277 definition translate_negint ≝ 276 λdestrs. 277 λsrcrs. 278 λstart_lbl. 279 λdest_lbl. 280 λdef. 281 λprf:  destrs  =  srcrs . (* assert in caml code *) 282 let 〈def, tmpr〉 ≝ fresh_reg def in 283 let f_cmpl ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in 284 let insts_cmpl ≝ map2 ? ? ? f_cmpl destrs srcrs prf in 278 λglobals: list ident. 279 λdestrs: list register. 280 λsrcrs: list register. 281 λstart_lbl: label. 282 λdest_lbl: label. 283 λdef: rtl_internal_function globals. 284 λprf: destrs = srcrs. (* assert in caml code *) 285 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in 286 let f_cmpl ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 rtl_params1 globals Cmpl destr srcr) in 287 let insts_cmpl ≝ map2 … f_cmpl destrs srcrs prf in 285 288 let insts_init ≝ [ 286 rtl_st_set_carry start_lbl;287 rtl_st_int tmpr (zero ?) start_lbl289 sequential … (SET_CARRY …); 290 sequential … (INT rtl_params_ globals tmpr (zero ?)) 288 291 ] in 289 let f_add ≝ λdestr. rtl_st_op2 Addc destr destr tmpr start_lblin292 let f_add ≝ λdestr. sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) in 290 293 let insts_add ≝ map … f_add destrs in 291 adds_graph (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def. 292 293 definition translate_notbool ≝ 294 λdestrs. 295 λsrcrs. 296 λstart_lbl. 297 λdest_lbl. 298 λdef. 294 adds_graph rtl_params1 globals (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def. 295 296 definition translate_notbool: ∀globals. list register → list register → label → label → rtl_internal_function globals → rtl_internal_function globals ≝ 297 λglobals: list ident. 298 λdestrs: list register. 299 λsrcrs: list register. 300 λstart_lbl: label. 301 λdest_lbl: label. 302 λdef: rtl_internal_function globals. 299 303 match destrs with 300 [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def304 [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … start_lbl) def 301 305  cons destr destrs ⇒ 302 let 〈def, tmpr〉 ≝ fresh_reg def in303 let 〈def, tmp_srcrs〉 ≝ fresh_regs def (length ? srcrs) in304 let save_srcrs ≝ translate_move tmp_srcrs srcrs in305 let init_destr ≝ rtl_st_int destr (bitvector_of_nat ? 1) start_lblin306 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in 307 let 〈def, tmp_srcrs〉 ≝ fresh_regs rtl_params0 globals def (length ? srcrs) in 308 let save_srcrs ≝ translate_move globals tmp_srcrs srcrs in 309 let init_destr ≝ sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1)) in 306 310 let f ≝ λtmp_srcr. [ 307 rtl_st_clear_carry start_lbl;308 rtl_st_int tmpr (zero ?) start_lbl;309 rtl_st_op2 Sub tmpr tmpr tmp_srcr start_lbl;310 rtl_st_int tmpr (zero ?) start_lbl;311 rtl_st_op2 Addc tmpr tmpr tmpr start_lbl;312 rtl_st_op2 Xor destr destr tmpr start_lbl311 sequential … (CLEAR_CARRY rtl_params_ globals); 312 sequential … (INT rtl_params_ globals tmpr (zero ?)); 313 sequential … (OP2 rtl_params_ globals Sub tmpr tmpr tmp_srcr); 314 sequential … (INT rtl_params_ globals tmpr (zero ?)); 315 sequential … (OP2 rtl_params_ globals Addc tmpr tmpr tmpr); 316 sequential … (OP2 rtl_params_ globals Xor destr destr tmpr) 313 317 ] in 314 let insts ≝ init_destr :: (flatten ?(map … f tmp_srcrs)) in315 let epilogue ≝ translate_cst (Ointconst I8 (bitvector_of_nat ? 0)) destrs in316 add_translates [317 save_srcrs; adds_graph insts; epilogue318 let insts ≝ init_destr :: (flatten … (map … f tmp_srcrs)) in 319 let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in 320 add_translates rtl_params1 globals [ 321 save_srcrs; adds_graph rtl_params1 globals insts; epilogue 318 322 ] start_lbl dest_lbl def 319 323 ]. 324 325 (* 320 326 321 327 (* TODO: examine this properly. This is a change from the O'caml code due 
src/utilities/adt/table_adt.ma
r1274 r1285 13 13  empty: table dom_type rng_type 14 14  node : nat → dom_type → rng_type → table dom_type rng_type → table dom_type rng_type → table dom_type rng_type. 15 16 definition tbl_empty ≝ empty. 17 18 definition tbl_size ≝ 15 16 definition tbl_height ≝ 19 17 λdom_type : Type[0]. 20 18 λrng_type : Type[0]. … … 25 23 ]. 26 24 25 let rec tbl_size 26 (dom_type : Type[0]) (rng_type : Type[0]) (the_table: table dom_type rng_type) 27 on the_table: nat ≝ 28 match the_table with 29 [ empty ⇒ 0 30  node sz key val l r ⇒ S (tbl_size … l) + (tbl_size … r) 31 ]. 32 33 definition tbl_empty ≝ 34 λdom_type: Type[0]. 35 λrng_type: Type[0]. 36 empty dom_type rng_type. 37 38 definition tbl_is_empty ≝ 39 λdom_type: Type[0]. 40 λrng_type: Type[0]. 41 λthe_table: table dom_type rng_type. 42 match the_table with 43 [ empty ⇒ true 44  _ ⇒ false 45 ]. 46 47 definition tbl_is_empty_p ≝ 48 λdom_type: Type[0]. 49 λrng_type: Type[0]. 50 λthe_table: table dom_type rng_type. 51 match the_table with 52 [ empty ⇒ True 53  _ ⇒ False 54 ]. 55 27 56 let rec tbl_to_list 28 57 (dom_type: Type[0]) (rng_type: Type[0]) (the_table: table dom_type rng_type) … … 32 61  node sz key val l r ⇒ 〈key, val〉 :: tbl_to_list … l @ tbl_to_list … r 33 62 ]. 34 35 axiom tbl_insert : ∀key_type, rng_type. key_type → rng_type → table key_type rng_type → table key_type rng_type. 36 37 axiom tbl_merge: 38 ∀key_type, rng_type. 39 (key_type → key_type → order) → table key_type rng_type → table key_type rng_type → table key_type rng_type. 40 41 axiom tbl_remove : ∀key_type, rng_type. key_type → table key_type rng_type → table key_type rng_type. 63 64 let rec tbl_min_binding 65 (key_type: Type[0]) (rng_type: Type[0]) (the_table: table key_type rng_type) 66 (proof: ¬ (tbl_is_empty_p … the_table)) 67 on the_table: key_type × rng_type ≝ 68 match the_table return λx. ¬ (tbl_is_empty_p … x) → key_type × rng_type with 69 [ empty ⇒ λabsurd. ? 70  node sz key val l r ⇒ λproof. 71 match l return λx. x = l → key_type × rng_type with 72 [ empty ⇒ λproof. 〈key, val〉 73  _ ⇒ λproof. tbl_min_binding key_type rng_type l ? 74 ] (refl … l) 75 ] proof. 76 [1: normalize in absurd; 77 elim absurd; 78 #ABSURD 79 @⊥ @ABSURD @I 80 2: <proof 81 normalize 82 /2/ 83 ] 84 qed. 85 86 definition tbl_create ≝ 87 λkey_type: Type[0]. 88 λrng_type: Type[0]. 89 λleft : table key_type rng_type. 90 λkey : key_type. 91 λval : rng_type. 92 λright : table key_type rng_type. 93 let hl ≝ tbl_height … left in 94 let hr ≝ tbl_height … right in 95 let height ≝ if gtb hl hr then hl + 1 else hr + 1 in 96 node key_type rng_type height key val left right. 97 98 let rec tbl_balance 99 (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order) 100 (left: table key_type rng_type) (key: key_type) (val: rng_type) 101 (right: table key_type rng_type) (left_proof: ¬ (tbl_is_empty_p … left)) 102 (right_proof: ¬ (tbl_is_empty_p … right)) 103 on left: table key_type rng_type ≝ 104 match gtb (tbl_height … left) ((tbl_height … right) + 2) with 105 [ true ⇒ 106 match left return λx. ¬ (tbl_is_empty_p … x) → table key_type rng_type with 107 [ empty ⇒ λabsurd. ? 108  node _ lv ld ll lr ⇒ λnon_empty_proof. 109 if gtb (tbl_height … ll) (tbl_height … lr) then 110 tbl_create … ll lv ld (tbl_create … lr key val right) 111 else 112 match lr return λx. ¬ (tbl_is_empty_p … x) → table key_type rng_type with 113 [ empty ⇒ λabsurd. ? 114  node _ lrv lrd lrl lrr ⇒ λ 115 tbl_create … (tbl_create … ll lv ld lrl) lrv lrd (tbl_create … lrr key val right) 116 ] 117 ] left_proof 118  false ⇒ ? 119 ]. 120 [1: normalize in absurd; 121 elim absurd 122 #ABSURD 123 @⊥ @ABSURD @I 124 *: cases daemon 125 ] 126 qed. 127 128 let rec tbl_remove_min_binding 129 (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order) 130 (the_table: table key_type rng_type) (proof: ¬ (tbl_is_empty_p … the_table)) 131 on the_table: table key_type rng_type ≝ 132 match the_table return λx. ¬ (tbl_is_empty_p … x) → table key_type rng_type with 133 [ empty ⇒ λabsurd. ? 134  node sz key val l r ⇒ λproof. 135 match l return λx. x = l → table key_type rng_type with 136 [ empty ⇒ λproof. r 137  _ ⇒ λproof. tbl_balance … ord (tbl_remove_min_binding … ord l ?) key val r 138 ] (refl … l) 139 ] proof. 140 [1: normalize in absurd; 141 elim absurd; 142 #ABSURD 143 @⊥ @ABSURD @I 144 2: <proof 145 normalize 146 @nmk // 147 ] 148 qed. 149 150 let rec tbl_insert 151 (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order) 152 (key: key_type) (val: rng_type) (the_table: table key_type rng_type) 153 on the_table: table key_type rng_type ≝ 154 match the_table with 155 [ empty ⇒ node … 1 key val (empty …) (empty …) 156  node sz key' val' l r ⇒ 157 match ord key key' with 158 [ order_lt ⇒ tbl_balance … ord (tbl_insert … ord key val l) key' val' r 159  order_eq ⇒ node … sz key val l r 160  order_gt ⇒ tbl_balance … ord l key' val' (tbl_insert … ord key val r) 161 ] 162 ]. 163 164 let rec tbl_merge 165 (dom_type: Type[0]) (rng_type: Type[0]) (ord: dom_type → dom_type → order) 166 (left: table dom_type rng_type) (right: table dom_type rng_type) 167 on left: table dom_type rng_type ≝ 168 match left with 169 [ empty ⇒ right 170  _ ⇒ 171 match right return λx. x = right → table dom_type rng_type with 172 [ empty ⇒ λid_proof. left 173  node sz key val l r ⇒ λid_proof. 174 let 〈x, d〉 ≝ tbl_min_binding dom_type rng_type right ? in 175 tbl_balance … ord left x d (tbl_remove_min_binding … ord right ?) 176 ] (refl … right) 177 ]. 178 <id_proof 179 normalize /2/ 180 qed. 181 182 let rec tbl_remove 183 (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order) 184 (key: key_type) (the_table: table key_type rng_type) 185 on the_table: table key_type rng_type ≝ 186 match the_table with 187 [ empty ⇒ empty … 188  node sz key' val' l r ⇒ 189 match ord key key' with 190 [ order_lt ⇒ tbl_balance … ord (tbl_remove … ord key l) key' val' r 191  order_eq ⇒ tbl_merge … ord l r 192  order_gt ⇒ tbl_balance … ord l key' val' (tbl_remove … ord key r) 193 ] 194 ]. 42 195 43 196 let rec tbl_find … … 87 240  node sz key val l r ⇒ f val ∨ tbl_exists … f l ∨ tbl_exists … f r 88 241 ]. 89 90 axiom tbl_equal : ∀key_type, rng_type. table key_type rng_type 91 → table key_type rng_type → bool. 242 243 axiom tbl_equal: 244 ∀key_type, rng_type. 245 (key_type → key_type → order) → (rng_type → rng_type → order) → 246 table key_type rng_type → table key_type rng_type → bool. 92 247 93 248 let rec tbl_mapi … … 117 272  node sz key val l r ⇒ tbl_fold … f r (f key val (tbl_fold … f l seed)) 118 273 ]. 119 120 definition tbl_is_empty ≝121 λkey_type : Type[0].122 λrng_type : Type[0].123 λtable : table key_type rng_type.124 tbl_size … table = 0.125 274 126 275 definition tbl_singleton ≝ … … 129 278 λkey : key_type. 130 279 λrng : rng_type. 131 tbl_insert … key rng (tbl_empty …).280 node key_type rng_type 1 key rng (empty …) (empty …). 132 281 133 282 definition tbl_from_list ≝ 134 283 λkey_type : Type[0]. 135 284 λrng_type : Type[0]. 285 λord : key_type → key_type → order. 136 286 λthe_list : list (key_type × rng_type). 137 287 foldr … (λkey_rng. 138 288 let 〈key, rng〉 ≝ key_rng in 139 tbl_insert … key rng) (tbl_empty …) the_list.289 tbl_insert … ord key rng) (tbl_empty …) the_list. 140 290 141 291 definition tbl_filter ≝ 142 292 λdom_type : Type[0]. 143 293 λrng_type : Type[0]. 294 λord : dom_type → dom_type → order. 144 295 λf : rng_type → bool. 145 296 λthe_table: table dom_type rng_type. 146 297 let as_list ≝ tbl_to_list … the_table in 147 298 let filtered ≝ filter … (λx. f (\snd x)) as_list in 148 tbl_from_list … filtered.149 299 tbl_from_list … ord filtered. 300
Note: See TracChangeset
for help on using the changeset viewer.