Changeset 1059
- Timestamp:
- Jul 6, 2011, 6:09:39 PM (10 years ago)
- Location:
- src
- Files:
-
- 4 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Util.ma
r1057 r1059 8 8 example daemon: False. generalize in match IMPOSSIBLE; #IMPOSSIBLE destruct(IMPOSSIBLE) qed. 9 9 example not_implemented: False. cases daemon qed. 10 10 11 notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)" 12 with precedence 10 13 for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }. 14 15 let rec reduce 16 (A: Type[0]) (left: list A) (right: list A) on left ≝ 17 match left with 18 [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉 19 | cons hd tl ⇒ 20 match right with 21 [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉 22 | cons hd' tl' ⇒ 23 let 〈cleft, cright〉 ≝ reduce A tl tl' in 24 let 〈commonl, restl〉 ≝ cleft in 25 let 〈commonr, restr〉 ≝ cright in 26 〈〈hd :: commonl, restl〉, 〈hd' :: commonr, restr〉〉 27 ] 28 ]. 29 30 (* 31 let rec reduce_strong 32 (A: Type[0]) (left: list A) (right: list A) (prf: | left | = | right |) on left ≝ 33 match left return λx. |x| = |right| → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with 34 [ nil ⇒ 35 match right return λy. | [ ] | = | y | → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with 36 [ nil ⇒ λnil_nil_prf. dp ? 〈〈[ ], [ ]〉, 〈[ ], [ ]〉〉 ? 37 | cons hd tl ⇒ λnil_cons_asrd_prf. ? 38 ] 39 | cons hd tl ⇒ 40 match right return λy. | hd::tl | = | y | → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with 41 [ nil ⇒ λcons_nil_absrd_prf. ? 42 | cons hd' tl' ⇒ λcons_cons_prf. ? 43 ] 44 ] prf. 45 *) 46 47 axiom reduce_length: 48 ∀A: Type[0]. 49 ∀left, right: list A. 50 ∀prf: | left | = | right |. 51 \fst (\fst (reduce A left right)) = \fst (\snd (reduce A left right)). 52 11 53 let rec map2_opt 12 54 (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C) … … 255 297 | S o ⇒ f (iterate A f a o) 256 298 ]. 257 258 notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"259 with precedence 10260 for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.261 299 262 300 (* Yeah, I probably ought to do something more general... *) -
src/RTLabs/RTLAbstoRTL.ma
r1057 r1059 4 4 include "common/Graphs.ma". 5 5 include "common/Maps.ma". 6 include "common/IntValue.ma". 6 (* include "common/IntValue.ma". *) 7 include "common/FrontEndOps.ma". 7 8 8 9 definition add_graph ≝ … … 280 281 rtl_st_int r i dest_lbl. 281 282 282 definition translate_cst ≝ 283 λcst. 284 λdestrs. 285 λstart_lbl. 286 λdest_lbl. 287 λdef. 288 match cst with 289 [ cast_int i ⇒ 290 match destrs with 291 [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def 292 | _ ⇒ 293 (* this case needs changing when Z is added to stdlib as we are using 294 nats instead of ints here! *) 295 let size ≝ length ? destrs in 296 let is ≝ map … (to_int size) (break size (of_int size (nat_of_bitvector ? i)) size) in 297 let is' ≝ map … (bitvector_of_nat ?) is in 298 let l ≝ map2 … (translate_cst_int_internal dest_lbl) destrs is' ? in 299 adds_graph l start_lbl dest_lbl def 300 ] 301 | cast_addrsymbol id ⇒ 302 let 〈r1, r2〉 ≝ make_addr ? destrs ? in 303 add_graph start_lbl (rtl_st_addr r1 r2 id dest_lbl) def 304 | _ ⇒ ? 305 ]. 306 | cast_addrsymbol id ⇒ 307 match destrs with 308 [ nil ⇒ None ? 309 | cons hd tl ⇒ 310 match tl with 311 [ nil ⇒ None ? 312 | cons hd' tl' ⇒ 313 Some ? (add_graph start_lbl (rtl_st_addr hd hd' id dest_lbl) def) 314 ] 315 ] 316 | cast_offset off ⇒ 317 match destrs with 318 [ nil ⇒ None ? 319 | cons hd tl ⇒ 320 match tl with 321 [ nil ⇒ None ? 322 | cons hd' tl' ⇒ 323 let 〈def, tmpr〉 ≝ fresh_reg def in 324 adds_graph [ 325 rtl_st_stack_addr hd hd' start_lbl; 326 rtl_st_int tmpr off start_lbl; 327 rtl_st_op2 Add hd hd tmpr start_lbl; 328 rtl_st_int tmpr (bitvector_of_nat ? 0) start_lbl; 329 rtl_st_op2 Addc hd' hd' tmpr start_lbl 330 ] start_lbl dest_lbl def 331 ] 332 ] 333 | cast_stack ⇒ ? 334 | cast_sizeof size ⇒ ? 335 (* | cast_float f ⇒ None ? *) (* what are we doing with floats? *) 336 ]. 337 338 let rec translate_cst cst destrs start_lbl dest_lbl def = match cst with 339 340 | AST.Cst_stack -> 341 let (r1, r2) = make_addr destrs in 342 add_graph start_lbl (RTL.St_stackaddr (r1, r2, dest_lbl)) def 343 344 | AST.Cst_offset off -> 345 let i = concrete_offset off in 346 translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def 347 348 | AST.Cst_sizeof size -> 349 let i = concrete_size size in 350 translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def 283 axiom translate_cst: 284 ∀cst: constant. 285 ∀destrs: list register. 286 ∀start_lbl: label. 287 ∀dest_lbl: label. 288 ∀def: rtl_internal_function. 289 rtl_internal_function. 290 291 definition translate_move_internal ≝ 292 λstart_lbl: label. 293 λdestr: register. 294 λsrcr: register. 295 rtl_st_move destr srcr start_lbl. 296 297 definition translate_move ≝ 298 λdestrs: list register. 299 λsrcrs: list register. 300 λstart_lbl: label. 301 λprf: | destrs | = | srcrs |. 302 let 〈crl, crr〉 ≝ reduce register destrs srcrs in 303 let 〈commonl, restl〉 ≝ crl in 304 let 〈commonr, restr〉 ≝ crr in 305 let f_common ≝ translate_move_internal start_lbl in 306 let translate1 ≝ adds_graph (map2 … f_common commonl commonr ?) in 307 let translate2 ≝ translate_cst (Ointconst ? (repr I8 0)) restl in (* should this be 8? *) 308 add_translates [ translate1 ; translate2 ] start_lbl. 309 310 let rec translate_move destrs srcrs start_lbl = 311 let ((common1, rest1), (common2, rest2)) = MiscPottier.reduce destrs srcrs in 312 let f_common destr srcr = RTL.St_move (destr, srcr, start_lbl) in 313 let translates1 = adds_graph (List.map2 f_common common1 common2) in 314 let translates2 = translate_cst (AST.Cst_int 0) rest1 in 315 add_translates [translates1 ; translates2] start_lbl 351 316 352 317 definition filter_and_to_list_local_env_internal ≝ -
src/common/AST.ma
r1057 r1059 43 43 definition Immediate ≝ nat. (* XXX is this the best place to put this? *) 44 44 45 (* dpm: not needed 45 46 inductive quantity: Type[0] ≝ 46 47 | q_int: Byte → quantity … … 53 54 | size_sum: list abstract_size → abstract_size 54 55 | size_array: nat → abstract_size → abstract_size. 55 56 definition abstract_offset ≝ abstract_size × nat. (* nth in size *) 57 58 inductive cast: Type[0] ≝ 59 | cast_int: Byte → cast (* integer constant *) 60 (* | cast_float: float → cast (* float constant *) *) 61 | cast_addrsymbol: ident → cast (* address of a global symbol *) 62 | cast_stack: cast (* address of the stack *) 63 | cast_offset: abstract_offset → cast (* offset *) 64 | cast_sizeof: abstract_size → cast. (* size of a type *) 56 *) 65 57 66 58 (* Memory spaces *) … … 191 183 definition repr : ∀sz:intsize. nat → bvint sz ≝ 192 184 λsz,x. bitvector_of_nat (bitsize_of_intsize sz) x. 193 194 185 195 186 definition size_floatsize : floatsize → nat ≝ -
src/common/IntValue.ma
r1057 r1059 2 2 include "arithmetics/exp.ma". 3 3 include "basics/list.ma". 4 include "common/AST.ma". 4 5 include "common/Order.ma". 5 6 6 definition big_int_size ≝ nat. 7 axiom big_int: big_int_size → Type[0]. 8 axiom big_int_int_repr: Type[0]. 7 definition bvint ≝ λsize. BitVector (bitsize_of_intsize size). 9 8 10 axiom compare: ∀size: big_int_size. big_int size → big_int size → order. 11 axiom zero: ∀size: big_int_size. big_int size. 12 axiom one: ∀size: big_int_size. big_int size. 13 axiom to_signed_int_repr: ∀size: big_int_size. big_int size → big_int_int_repr. 14 axiom to_unsigned_int_repr: ∀size: big_int_size. big_int size → big_int_int_repr. 15 axiom succ: ∀size: big_int_size. big_int size → big_int size. 16 axiom pred: ∀size: big_int_size. big_int size → big_int size. 17 axiom add: ∀size: big_int_size. big_int size → big_int size → big_int size. 18 axiom add_of: ∀size: big_int_size. big_int size → big_int size → bool. 19 axiom sub: ∀size: big_int_size. big_int size → big_int size → big_int size. 20 axiom sub_uf: ∀size: big_int_size. big_int size → big_int size → bool. 21 axiom mul: ∀size: big_int_size. big_int size → big_int size → big_int size. 22 axiom div: ∀size: big_int_size. big_int size → big_int size → big_int size. 23 axiom divu: ∀size: big_int_size. big_int size → big_int size → big_int size. 24 axiom modulo: ∀size: big_int_size. big_int size → big_int size → big_int size. 25 axiom modulou: ∀size: big_int_size. big_int size → big_int size → big_int size. 26 axiom eq: ∀size: big_int_size. big_int size → big_int size → bool. 27 axiom neq: ∀size: big_int_size. big_int size → big_int size → bool. 28 axiom lt: ∀size: big_int_size. big_int size → big_int size → bool. 29 axiom ltu: ∀size: big_int_size. big_int size → big_int size → bool. 30 axiom le: ∀size: big_int_size. big_int size → big_int size → bool. 31 axiom leu: ∀size: big_int_size. big_int size → big_int size → bool. 32 axiom gt: ∀size: big_int_size. big_int size → big_int size → bool. 33 axiom gtu: ∀size: big_int_size. big_int size → big_int size → bool. 34 axiom ge: ∀size: big_int_size. big_int size → big_int size → bool. 35 axiom geu: ∀size: big_int_size. big_int size → big_int size → bool. 36 axiom neg: ∀size: big_int_size. big_int size → big_int size. 37 axiom lognot: ∀size: big_int_size. big_int size → big_int size. 38 axiom logand: ∀size: big_int_size. big_int size → big_int size → big_int size. 39 axiom logor: ∀size: big_int_size. big_int size → big_int size → big_int size. 40 axiom logxor: ∀size: big_int_size. big_int size → big_int size → big_int size. 41 axiom shl: ∀size: big_int_size. big_int size → big_int size → big_int size. 42 axiom shr: ∀size: big_int_size. big_int size → big_int size → big_int size. 43 axiom shrl: ∀size: big_int_size. big_int size → big_int size → big_int size. 44 axiom max: ∀size: big_int_size. big_int size → big_int size → big_int size. 45 axiom maxu: ∀size: big_int_size. big_int size → big_int size → big_int size. 46 axiom min: ∀size: big_int_size. big_int size → big_int size → big_int size. 47 axiom minu: ∀size: big_int_size. big_int size → big_int size → big_int size. 48 axiom cast: ∀size: big_int_size. big_int_int_repr → big_int size. 49 axiom of_int: ∀size: big_int_size. nat → big_int size. (*dpm: replace when Z is added to stdlib *) 50 axiom to_int: ∀size: big_int_size. big_int size → nat. (*dpm: """" *) 51 axiom zero_ext: ∀size: big_int_size. nat → big_int size → big_int size. (* nat here correct *) 52 axiom sign_ext: ∀size: big_int_size. nat → big_int size → big_int size. (* nat here correct *) 53 axiom break: ∀size: big_int_size. big_int size → nat → list (big_int size). 54 axiom merge: ∀size: big_int_size. list (big_int size) → big_int size. 9 definition bitsize_of_intsize: intsize → nat ≝ 10 λsize. 11 S (match size with [ I8 ⇒ 7 | I16 ⇒ 15 | I32 ⇒ 31]). 12 13 definition of_int ≝ 14 λsize. 15 λn. 16 bitvector_of_nat (bitsize_of_intsize size) n. 17 18 axiom compare: ∀size: intsize. bvint size → bvint size → order. 19 axiom zero: ∀size: intsize. bvint size. 20 axiom one: ∀size: intsize. bvint size. 21 axiom to_signed_int_repr: ∀size: intsize. bvint size → bvint_int_repr. 22 axiom to_unsigned_int_repr: ∀size: intsize. bvint size → bvint_int_repr. 23 axiom succ: ∀size: intsize. bvint size → bvint size. 24 axiom pred: ∀size: intsize. bvint size → bvint size. 25 axiom add: ∀size: intsize. bvint size → bvint size → bvint size. 26 axiom add_of: ∀size: intsize. bvint size → bvint size → bool. 27 axiom sub: ∀size: intsize. bvint size → bvint size → bvint size. 28 axiom sub_uf: ∀size: intsize. bvint size → bvint size → bool. 29 axiom mul: ∀size: intsize. bvint size → bvint size → bvint size. 30 axiom div: ∀size: intsize. bvint size → bvint size → bvint size. 31 axiom divu: ∀size: intsize. bvint size → bvint size → bvint size. 32 axiom modulo: ∀size: intsize. bvint size → bvint size → bvint size. 33 axiom modulou: ∀size: intsize. bvint size → bvint size → bvint size. 34 axiom eq: ∀size: intsize. bvint size → bvint size → bool. 35 axiom neq: ∀size: intsize. bvint size → bvint size → bool. 36 axiom lt: ∀size: intsize. bvint size → bvint size → bool. 37 axiom ltu: ∀size: intsize. bvint size → bvint size → bool. 38 axiom le: ∀size: intsize. bvint size → bvint size → bool. 39 axiom leu: ∀size: intsize. bvint size → bvint size → bool. 40 axiom gt: ∀size: intsize. bvint size → bvint size → bool. 41 axiom gtu: ∀size: intsize. bvint size → bvint size → bool. 42 axiom ge: ∀size: intsize. bvint size → bvint size → bool. 43 axiom geu: ∀size: intsize. bvint size → bvint size → bool. 44 axiom neg: ∀size: intsize. bvint size → bvint size. 45 axiom lognot: ∀size: intsize. bvint size → bvint size. 46 axiom logand: ∀size: intsize. bvint size → bvint size → bvint size. 47 axiom logor: ∀size: intsize. bvint size → bvint size → bvint size. 48 axiom logxor: ∀size: intsize. bvint size → bvint size → bvint size. 49 axiom shl: ∀size: intsize. bvint size → bvint size → bvint size. 50 axiom shr: ∀size: intsize. bvint size → bvint size → bvint size. 51 axiom shrl: ∀size: intsize. bvint size → bvint size → bvint size. 52 axiom max: ∀size: intsize. bvint size → bvint size → bvint size. 53 axiom maxu: ∀size: intsize. bvint size → bvint size → bvint size. 54 axiom min: ∀size: intsize. bvint size → bvint size → bvint size. 55 axiom minu: ∀size: intsize. bvint size → bvint size → bvint size. 56 axiom cast: ∀size: intsize. bvint_int_repr → bvint size. 57 axiom to_int: ∀size: intsize. bvint size → nat. (*dpm: """" *) 58 axiom zero_ext: ∀size: intsize. nat → bvint size → bvint size. (* nat here correct *) 59 axiom sign_ext: ∀size: intsize. nat → bvint size → bvint size. (* nat here correct *) 60 axiom break: ∀size: intsize. bvint size → nat → list (bvint size). 61 axiom merge: ∀size: intsize. list (bvint size) → bvint size.
Note: See TracChangeset
for help on using the changeset viewer.