Changeset 1059


Ignore:
Timestamp:
Jul 6, 2011, 6:09:39 PM (8 years ago)
Author:
mulligan
Message:

work from today, bit of a mess at the moment

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1057 r1059  
    88example daemon: False. generalize in match IMPOSSIBLE; #IMPOSSIBLE destruct(IMPOSSIBLE) qed.
    99example not_implemented: False. cases daemon qed.
    10  
     10
     11notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
     12 with precedence 10
     13for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
     14
     15let 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(*
     31let 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
     47axiom 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   
    1153let rec map2_opt
    1254  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C)
     
    255297    | S o ⇒ f (iterate A f a o)
    256298    ].
    257    
    258 notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
    259  with precedence 10
    260 for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
    261299
    262300(* Yeah, I probably ought to do something more general... *)
  • src/RTLabs/RTLAbstoRTL.ma

    r1057 r1059  
    44include "common/Graphs.ma".
    55include "common/Maps.ma".
    6 include "common/IntValue.ma".
     6(* include "common/IntValue.ma". *)
     7include "common/FrontEndOps.ma".
    78
    89definition add_graph ≝
     
    280281    rtl_st_int r i dest_lbl.
    281282
    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
     283axiom 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
     291definition translate_move_internal ≝
     292  λstart_lbl: label.
     293  λdestr: register.
     294  λsrcr: register.
     295    rtl_st_move destr srcr start_lbl.
     296
     297definition 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   
     310let 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
    351316
    352317definition filter_and_to_list_local_env_internal ≝
  • src/common/AST.ma

    r1057 r1059  
    4343definition Immediate ≝ nat. (* XXX is this the best place to put this? *)
    4444
     45(* dpm: not needed
    4546inductive quantity: Type[0] ≝
    4647  | q_int: Byte → quantity
     
    5354  | size_sum: list abstract_size → abstract_size
    5455  | 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*)
    6557
    6658(* Memory spaces *)
     
    191183definition repr : ∀sz:intsize. nat → bvint sz ≝
    192184λsz,x. bitvector_of_nat (bitsize_of_intsize sz) x.
    193 
    194185
    195186definition size_floatsize : floatsize → nat ≝
  • src/common/IntValue.ma

    r1057 r1059  
    22include "arithmetics/exp.ma".
    33include "basics/list.ma".
     4include "common/AST.ma".
    45include "common/Order.ma".
    56
    6 definition big_int_size ≝ nat.
    7 axiom big_int: big_int_size → Type[0].
    8 axiom big_int_int_repr: Type[0].
     7definition bvint ≝ λsize. BitVector (bitsize_of_intsize size).
    98
    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.
     9definition bitsize_of_intsize: intsize → nat ≝
     10  λsize.
     11    S (match size with [ I8 ⇒ 7 | I16 ⇒ 15 | I32 ⇒ 31]).
     12
     13definition of_int ≝
     14  λsize.
     15  λn.
     16    bitvector_of_nat (bitsize_of_intsize size) n.
     17
     18axiom compare: ∀size: intsize. bvint size → bvint size → order.
     19axiom zero: ∀size: intsize. bvint size.
     20axiom one: ∀size: intsize. bvint size.
     21axiom to_signed_int_repr: ∀size: intsize. bvint size → bvint_int_repr.
     22axiom to_unsigned_int_repr: ∀size: intsize. bvint size → bvint_int_repr.
     23axiom succ: ∀size: intsize. bvint size → bvint size.
     24axiom pred: ∀size: intsize. bvint size → bvint size.
     25axiom add: ∀size: intsize. bvint size → bvint size → bvint size.
     26axiom add_of: ∀size: intsize. bvint size → bvint size → bool.
     27axiom sub: ∀size: intsize. bvint size → bvint size → bvint size.
     28axiom sub_uf: ∀size: intsize. bvint size → bvint size → bool.
     29axiom mul: ∀size: intsize. bvint size → bvint size → bvint size.
     30axiom div: ∀size: intsize. bvint size → bvint size → bvint size.
     31axiom divu: ∀size: intsize. bvint size → bvint size → bvint size.
     32axiom modulo: ∀size: intsize. bvint size → bvint size → bvint size.
     33axiom modulou: ∀size: intsize. bvint size → bvint size → bvint size.
     34axiom eq: ∀size: intsize. bvint size → bvint size → bool.
     35axiom neq: ∀size: intsize. bvint size → bvint size → bool.
     36axiom lt: ∀size: intsize. bvint size → bvint size → bool.
     37axiom ltu: ∀size: intsize. bvint size → bvint size → bool.
     38axiom le: ∀size: intsize. bvint size → bvint size → bool.
     39axiom leu: ∀size: intsize. bvint size → bvint size → bool.
     40axiom gt: ∀size: intsize. bvint size → bvint size → bool.
     41axiom gtu: ∀size: intsize. bvint size → bvint size → bool.
     42axiom ge: ∀size: intsize. bvint size → bvint size → bool.
     43axiom geu: ∀size: intsize. bvint size → bvint size → bool.
     44axiom neg: ∀size: intsize. bvint size → bvint size.
     45axiom lognot: ∀size: intsize. bvint size → bvint size.
     46axiom logand: ∀size: intsize. bvint size → bvint size → bvint size.
     47axiom logor: ∀size: intsize. bvint size → bvint size → bvint size.
     48axiom logxor: ∀size: intsize. bvint size → bvint size → bvint size.
     49axiom shl: ∀size: intsize. bvint size → bvint size → bvint size.
     50axiom shr: ∀size: intsize. bvint size → bvint size → bvint size.
     51axiom shrl: ∀size: intsize. bvint size → bvint size → bvint size.
     52axiom max: ∀size: intsize. bvint size → bvint size → bvint size.
     53axiom maxu: ∀size: intsize. bvint size → bvint size → bvint size.
     54axiom min: ∀size: intsize. bvint size → bvint size → bvint size.
     55axiom minu: ∀size: intsize. bvint size → bvint size → bvint size.
     56axiom cast: ∀size: intsize. bvint_int_repr → bvint size.
     57axiom to_int: ∀size: intsize. bvint size → nat. (*dpm: """" *)
     58axiom zero_ext: ∀size: intsize. nat → bvint size → bvint size. (* nat here correct *)
     59axiom sign_ext: ∀size: intsize. nat → bvint size → bvint size. (* nat here correct *)
     60axiom break: ∀size: intsize. bvint size → nat → list (bvint size).
     61axiom merge: ∀size: intsize. list (bvint size) → bvint size.
Note: See TracChangeset for help on using the changeset viewer.