Changeset 1057


Ignore:
Timestamp:
Jul 5, 2011, 5:53:11 PM (8 years ago)
Author:
mulligan
Message:

changes from today

Location:
src
Files:
1 added
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r998 r1057  
    88example daemon: False. generalize in match IMPOSSIBLE; #IMPOSSIBLE destruct(IMPOSSIBLE) qed.
    99example not_implemented: False. cases daemon qed.
     10 
     11let rec map2_opt
     12  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C)
     13  (left: list A) (right: list B) on left ≝
     14  match left with
     15  [ nil ⇒
     16    match right with
     17    [ nil ⇒ Some ? (nil C)
     18    | _ ⇒ None ?
     19    ]
     20  | cons hd tl ⇒
     21    match right with
     22    [ nil ⇒ None ?
     23    | cons hd' tl' ⇒
     24      match map2_opt A B C f tl tl' with
     25      [ None ⇒ None ?
     26      | Some tail ⇒ Some ? (f hd hd' :: tail)
     27      ]
     28    ]
     29  ].
     30
     31let rec map2
     32  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C)
     33  (left: list A) (right: list B) (proof: | left | = | right |) on left ≝
     34  match left return λx. | x | = | right | → list C with
     35  [ nil ⇒
     36    match right return λy. | [] | = | y | → list C with
     37    [ nil ⇒ λnil_prf. nil C
     38    | _ ⇒ λcons_absrd. ?
     39    ]
     40  | cons hd tl ⇒
     41    match right return λy. | hd::tl | = | y | → list C with
     42    [ nil ⇒ λnil_absrd. ?
     43    | cons hd' tl' ⇒ λcons_prf. (f hd hd') :: map2 A B C f tl tl' ?
     44    ]
     45  ] proof.
     46  [1: normalize in cons_absrd;
     47      destruct(cons_absrd)
     48  |2: normalize in nil_absrd;
     49      destruct(nil_absrd)
     50  |3: normalize in cons_prf;
     51      destruct(cons_prf)
     52      assumption
     53  ]
     54qed.
    1055 
    1156lemma eq_rect_Type0_r :
  • src/RTLabs/RTLAbstoRTL.ma

    r1053 r1057  
    44include "common/Graphs.ma".
    55include "common/Maps.ma".
    6 include "utilities/HMap.ma".
     6include "common/IntValue.ma".
    77
    88definition add_graph ≝
     
    2525                             rtl_if_exit'.
    2626     
    27 definition fresh_label
     27definition fresh_label: rtl_internal_function → rtl_internal_function × label
    2828  λdef.
    29     match fresh LabelTag (rtl_if_luniverse def) with
    30     [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ)
    31     | Error _ ⇒ None ?
    32     ].
     29    let 〈lbl, new_univ〉 ≝ fresh LabelTag (rtl_if_luniverse def) in
     30    let locals ≝ rtl_if_locals def in
     31    let rtl_if_luniverse' ≝ new_univ in
     32    let rtl_if_runiverse' ≝ rtl_if_runiverse def in
     33    let rtl_if_sig' ≝ rtl_if_sig def in
     34    let rtl_if_result' ≝ rtl_if_result def in
     35    let rtl_if_params' ≝ rtl_if_params def in
     36    let rtl_if_locals' ≝ rtl_if_locals def in
     37    let rtl_if_stacksize' ≝ rtl_if_stacksize def in
     38    let rtl_if_graph' ≝ rtl_if_graph def in
     39    let rtl_if_entry' ≝ rtl_if_entry def in
     40    let rtl_if_exit' ≝ rtl_if_exit def in
     41      〈mk_rtl_internal_function
     42        rtl_if_luniverse' rtl_if_runiverse' rtl_if_sig' rtl_if_result'
     43        rtl_if_params' rtl_if_locals' rtl_if_stacksize' rtl_if_graph'
     44        rtl_if_entry' rtl_if_exit', lbl〉.
    3345
    3446axiom register_fresh: universe RegisterTag → register.
     
    232244   labels as unbounded nats then this function will never fail.
    233245*)
     246(* Fixed with changes to label generation.
     247*)
    234248let rec adds_graph (stmt_list: ?) (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function) ≝
    235249  match stmt_list with
    236   [ nil ⇒ Some ? def
     250  [ nil ⇒ def
    237251  | cons hd tl ⇒
    238252    match tl with
    239     [ nil ⇒ Some ? (add_graph start_lbl (change_label dest_lbl hd) def)
     253    [ nil ⇒ add_graph start_lbl (change_label dest_lbl hd) def
    240254    | cons hd' tl' ⇒
    241       let tmp_lbl ≝ fresh_label def in
    242       match tmp_lbl with
    243       [ None ⇒ None ?
    244       | Some tmp_lbl ⇒
    245         let stmt ≝ change_label tmp_lbl hd in
    246         let def ≝ add_graph start_lbl stmt def in
    247           adds_graph tl tmp_lbl dest_lbl def
    248       ]
    249     ]
    250   ].
    251 
    252 (* dpm: had to lift this into option *)
     255      let 〈new_def, tmp_lbl〉 ≝ fresh_label def in
     256      let stmt ≝ change_label tmp_lbl hd in
     257      let def ≝ add_graph start_lbl stmt new_def in
     258        adds_graph tl tmp_lbl dest_lbl new_def
     259    ]
     260  ].
     261
    253262let rec add_translates (translate_list: ?) (start_lbl: label) (dest_lbl: label)
    254263                       (def: ?) on translate_list ≝
    255264  match translate_list with
    256   [ nil ⇒ Some ? def
     265  [ nil ⇒ def
    257266  | cons hd tl ⇒
    258267    match tl with
    259268    [ nil ⇒ hd start_lbl dest_lbl def
    260269    | cons hd' tl' ⇒
    261       let tmp_lbl ≝ fresh_label def in
    262       match tmp_lbl with
    263       [ None ⇒ None ?
    264       | Some tmp_lbl ⇒
    265         match hd start_lbl tmp_lbl def with
    266         [ None ⇒ None ?
    267         | Some def ⇒ add_translates tl tmp_lbl dest_lbl def
    268         ]
    269       ]
    270     ]
    271   ].
     270      let 〈new_def, tmp_lbl〉 ≝ fresh_label def in
     271      let applied ≝ hd start_lbl tmp_lbl new_def in
     272        add_translates tl tmp_lbl dest_lbl applied
     273    ]
     274  ].
     275
     276definition translate_cst_int_internal ≝
     277  λdest_lbl.
     278  λr.
     279  λi.
     280    rtl_st_int r i dest_lbl.
    272281
    273282definition translate_cst ≝
     
    281290    match destrs with
    282291    [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
    283     | cons hd tl ⇒
    284       match tl with
    285       [ nil ⇒ Some ? (add_graph start_lbl (rtl_st_int hd i dest_lbl) def)
    286       | cons hd' tl' ⇒ None ?
    287       ]
    288     ]
     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  ].
    289306  | cast_addrsymbol id ⇒
    290307    match destrs with
     
    318335  (* | cast_float f ⇒ None ? *) (* what are we doing with floats? *)
    319336  ].
     337
     338let 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
    320351
    321352definition filter_and_to_list_local_env_internal ≝
  • src/common/AST.ma

    r1052 r1057  
    5959  | cast_int: Byte → cast                     (* integer constant *)
    6060(*  | cast_float: float → cast                (* float constant *) *)
    61   | cast_addrsymbol: Identifier → cast      (* address of a global symbol *)
     61  | cast_addrsymbol: ident → cast      (* address of a global symbol *)
    6262  | cast_stack: cast                          (* address of the stack *)
    6363  | cast_offset: abstract_offset → cast       (* offset *)
  • src/common/Identifiers.ma

    r1056 r1057  
    1 
    21include "basics/types.ma".
    32include "ASM/String.ma".
Note: See TracChangeset for help on using the changeset viewer.