Changeset 1515 for src/joint


Ignore:
Timestamp:
Nov 18, 2011, 1:03:14 PM (8 years ago)
Author:
campbell
Message:

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
Location:
src/joint
Files:
3 edited

Legend:

Unmodified
Added
Removed

  • src/joint/Erasure.ma

    r1472 r1515  
    55  (globals: list ident) (the_program: list (lin_statement globals))
    66    (labels: list label)
    7       on the_program: ((BitVectorTrie Word 16) × (list (lin_statement globals))) ≝
     7      on the_program: ((identifier_map ? label) × (list (lin_statement globals))) ≝
    88  match the_program with
    99  [ nil        ⇒
    1010    match labels with
    11     [ nil ⇒ 〈Stub Word 16, [ ]〉 (* XXX: labels should be empty *)
     11    [ nil ⇒ 〈empty_map …, [ ]〉 (* XXX: labels should be empty *)
    1212    | _   ⇒ ⊥
    1313    ]
    … …  
    2626          ]
    2727      | Some lbl ⇒
    28         let lbl' ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in
    2928        match instr with
    3029        [ sequential seq l ⇒
    … …  
    3332          | _ ⇒
    3433            let 〈maps, instructions〉 ≝ pre_erase_lin_internal_function' globals tl labels in
    35             let maps ≝ foldr ? ? (λl. λmap.
    36               match l with
    37               [ an_identifier l ⇒ insert … l lbl' map
    38               ]) maps (lbl :: labels)
     34            let maps ≝ foldr ? ? (λl. λmap. add … map l lbl) maps (lbl :: labels)
    3935            in
    4036              〈maps, instructions〉
    … …  
    4238        | _ ⇒
    4339          let 〈maps, instructions〉 ≝ pre_erase_lin_internal_function' globals tl labels in
    44           let maps ≝ foldr ? ? (λl. λmap.
    45             match l with
    46             [ an_identifier l ⇒ insert … l lbl' map
    47             ]) maps (lbl :: labels)
     40          let maps ≝ foldr ? ? (λl. λmap. add … map l lbl) maps (lbl :: labels)
    4841          in
    4942            〈maps, instructions〉
    … …  
    6255    ∀globals: list ident.
    6356    ∀params: params_.
    64       BitVectorTrie Word 16 → joint_instruction params globals → joint_instruction params globals ≝
     57      identifier_map LabelTag label → joint_instruction params globals → joint_instruction params globals ≝
    6558  λglobals: list ident.
    6659  λparams.
    … …  
    6962  match instr with
    7063  [ COND acc_a lbl ⇒
    71     let lbl ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in
    72     let located ≝ an_identifier LabelTag (lookup … lbl map lbl) in
     64    let located ≝ lookup_def ?? map lbl lbl in
    7365      COND params globals acc_a located
    7466  | _ ⇒ instr
    … …  
    7870  ∀globals: list ident.
    7971  ∀params: params_.
    80     BitVectorTrie Word 16 → joint_statement params globals → joint_statement params globals ≝
     72    identifier_map LabelTag label → joint_statement params globals → joint_statement params globals ≝
    8173  λglobals: list ident.
    8274  λparams: params_.
    83   λmap: BitVectorTrie Word 16.
     75  λmap: identifier_map LabelTag label.
    8476  λstmt: joint_statement params globals.
    8577  match stmt with
    … …  
    8981  | RETURN ⇒ RETURN params globals
    9082  | GOTO l ⇒
    91     let l ≝ match l with [ an_identifier l ⇒ l ] in
    92     let located ≝ an_identifier LabelTag (lookup … l map l) in
     83    let located ≝ lookup_def ?? map l l in
    9384      GOTO params globals located
    9485  ].
    9586
    9687let rec relabel_lin_internal_function'
    97   (globals: list ident) (map: BitVectorTrie Word 16)
     88  (globals: list ident) (map: identifier_map LabelTag label)
    9889    (program: list (lin_statement globals))
    9990      on program: list (lin_statement globals) ≝
    … …  
    10798      [ None ⇒ None …
    10899      | Some label ⇒
    109         let label ≝ match label with [ an_identifier l ⇒ l ] in
    110           Some … (an_identifier LabelTag (lookup … label map label))
     100          Some … (lookup_def ?? map label label)
    111101      ]
    112102    in
    … …  
    122112definition empty_graph ≝
    123113  λa: Type[0].
    124     an_id_map LabelTag a (Stub a 16).
     114    empty_map LabelTag a.
    125115
    126116let rec pre_erase_graph_internal_function'
    127117  (params1: params1) (globals: list ident)
    128118    (the_graph: codeT globals (graph_params params1 globals)) (labels: list label)
    129       (entry_point: label) (size_counter: nat) (map: BitVectorTrie Word 16)
    130         (visited: BitVectorTrie bool 16)
    131           on size_counter: ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) ≝
    132   match size_counter return λ_.  ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
     119      (entry_point: label) (size_counter: nat) (map: identifier_map LabelTag label)
     120        (visited: identifier_map LabelTag bool)
     121          on size_counter: ((identifier_map LabelTag label) × (identifier_map LabelTag bool) × (codeT globals (graph_params params1 globals))) ≝
     122  match size_counter return λ_.  ((identifier_map LabelTag label) × (identifier_map LabelTag bool) × (codeT globals (graph_params params1 globals))) with
    133123  [ O ⇒
    134124    match labels with
    … …  
    137127    ]
    138128  | S size_counter ⇒
    139     let entry_point' ≝ match entry_point with [ an_identifier e ⇒ e ] in
    140129    let statement ≝ lookup LabelTag ? the_graph entry_point in
    141     match statement return λs: option (joint_statement (graph_params params1 globals) globals). ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
     130    match statement return λs: option (joint_statement (graph_params params1 globals) globals). ((identifier_map LabelTag label) × (identifier_map LabelTag bool) × (codeT globals (graph_params params1 globals))) with
    142131    [ None ⇒ ⊥ (* XXX: should not happen *)
    143132    | Some statement ⇒
    144       let entered_previously ≝ bvt_lookup … entry_point' visited false in
    145       match entered_previously return λe: bool. ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
     133      let entered_previously ≝ lookup_def … visited entry_point false in
     134      match entered_previously return λe: bool. ((identifier_map LabelTag label) × (identifier_map LabelTag bool) × (codeT globals (graph_params params1 globals))) with
    146135      [ true ⇒ 〈map, visited, the_graph〉
    147136      | false ⇒ (* XXX: never visited here before *)
    148         let visited ≝ insert … entry_point' true visited in
    149         match statement return λs: joint_statement (graph_params params1 globals) globals. ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
     137        let visited ≝ add … visited entry_point true in
     138        match statement return λs: joint_statement (graph_params params1 globals) globals. ((identifier_map LabelTag label) × (identifier_map LabelTag bool) × (codeT globals (graph_params params1 globals))) with
    150139        [ sequential seq l ⇒
    151140          match seq with
    … …  
    155144            let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] l size_counter map visited in
    156145            let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] cond_label size_counter map visited in
    157             let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
     146            let map ≝ foldr … (λl. λmap. add … map l entry_point) map (entry_point :: labels) in
    158147              〈map, visited, the_graph〉
    159148          | _ ⇒
    160149            let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] l size_counter map visited in
    161             let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
     150            let map ≝ foldr … (λl. λmap. add … map l entry_point) map (entry_point :: labels) in
    162151              〈map, visited, the_graph〉
    163152          ]
    164153        | RETURN ⇒
    165           let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
     154          let map ≝ foldr … (λl. λmap. add … map l entry_point) map (entry_point :: labels) in
    166155            〈map, visited, the_graph〉
    167156        | GOTO l ⇒
    168157          let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] l size_counter map visited in
    169           let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
     158          let map ≝ foldr … (λl. λmap. add … map l entry_point) map (entry_point :: labels) in
    170159            〈map, visited, the_graph〉
    171160        ]
    … …  
    183172  [ dp entry entry_proof ⇒
    184173    let code ≝ joint_if_code … int_fun in
    185     let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals code [ ] entry (graph_num_nodes … code) (Stub …) (Stub …) in
     174    let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals code [ ] entry (graph_num_nodes … code) (empty_map …) (empty_map …) in
    186175      〈map, the_graph〉
    187176  ].
    … …  
    189178let rec relabel_graph'
    190179  (params1: params1) (globals: list ident)
    191     (the_graph: codeT globals (graph_params params1 globals)) (map: BitVectorTrie Word 16)
    192       (visited: BitVectorTrie bool 16) (entry_point: label) (size_counter: nat)
     180    (the_graph: codeT globals (graph_params params1 globals)) (map: identifier_map LabelTag label)
     181      (visited: identifier_map LabelTag bool) (entry_point: label) (size_counter: nat)
    193182        on size_counter: codeT globals (graph_params params1 globals) ≝
    194183  match size_counter return λs: nat. codeT globals (graph_params params1 globals) with
    195184  [ O ⇒ empty_graph …
    196185  | S size_counter ⇒
    197     let entry_point' ≝ match entry_point with [ an_identifier e ⇒ e ] in
    198     let relabelled_entry_point ≝ an_identifier LabelTag (bvt_lookup … entry_point' map entry_point') in
     186    let relabelled_entry_point ≝ lookup_def … map entry_point entry_point in
    199187    let statement ≝ lookup LabelTag ? the_graph entry_point in
    200188    match statement return λs: option (joint_statement (graph_params params1 globals) globals). codeT globals (graph_params params1 globals) with
    201189    [ None ⇒ ⊥ (* XXX: should not happen *)
    202190    | Some statement ⇒
    203       let entered_previously ≝ (bvt_lookup … entry_point' visited false) in
     191      let entered_previously ≝ lookup_def … visited entry_point false in
    204192      match entered_previously return λe: bool. codeT globals (graph_params params1 globals) with
    205193      [ true ⇒ the_graph
    206194      | false ⇒ (* XXX: never visited here before *)
    207         let visited ≝ insert … entry_point' true visited in
     195        let visited ≝ add … visited entry_point true in
    208196        match statement return λs: joint_statement (graph_params params1 globals) globals. codeT globals (graph_params params1 globals) with
    209197        [ sequential seq l ⇒
    210           let l' ≝ match l with [ an_identifier l ⇒ l ] in
    211198          let 〈the_graph, new_seq〉 ≝
    212199            match seq return λs. (codeT globals (graph_params params1 globals)) × ? with
    213200            [ COND acc_a cond_label ⇒
    214               let cond_label' ≝ match cond_label with [ an_identifier l ⇒ l ] in
    215               let relabelled ≝ an_identifier LabelTag (bvt_lookup … cond_label' map cond_label') in
     201              let relabelled ≝ lookup_def … map cond_label cond_label in
    216202              let tail_graph ≝ relabel_graph' params1 globals the_graph map visited cond_label size_counter in
    217203                〈tail_graph, COND … acc_a relabelled〉
    … …  
    220206          in
    221207            let tail_graph ≝ relabel_graph' params1 globals the_graph map visited l size_counter in
    222             let relabelled ≝ an_identifier LabelTag (bvt_lookup … l' map l') in
     208            let relabelled ≝ lookup_def … map l l in
    223209              add LabelTag … tail_graph relabelled_entry_point (sequential … new_seq relabelled)
    224210        | RETURN ⇒ the_graph
    225211        | GOTO l ⇒
    226           let l' ≝ match l with [ an_identifier l ⇒ l ] in
    227           let relabelled ≝ an_identifier LabelTag (bvt_lookup … l' map l') in
     212          let relabelled ≝ lookup_def … map l l in
    228213            add LabelTag … the_graph relabelled_entry_point (GOTO … relabelled)         
    229214        ]
    … …  
    237222  λglobals: list ident.
    238223  λparams1: params1.
    239   λmap: BitVectorTrie Word 16.
     224  λmap: identifier_map LabelTag label.
    240225  λint_fun: joint_internal_function globals (graph_params params1 globals).
    241226    match joint_if_entry … int_fun with
    242227    [ dp entry entry_prf ⇒
    243228      let code ≝ joint_if_code … int_fun in
    244         relabel_graph' … code map (Stub …) entry (graph_num_nodes … code)
     229        relabel_graph' … code map (empty_map …) entry (graph_num_nodes … code)
    245230    ].
    246231   
    … …  
    248233  λglobals: list ident.
    249234  λpars: params globals.
    250   λerasure_function: joint_internal_function globals pars → (BitVectorTrie Word 16) × (codeT … pars).
    251   λrelabelling_function: BitVectorTrie Word 16 → joint_internal_function globals pars → codeT … pars.
     235  λerasure_function: joint_internal_function globals pars → (identifier_map LabelTag label) × (codeT … pars).
     236  λrelabelling_function: identifier_map LabelTag label → joint_internal_function globals pars → codeT … pars.
    252237  λint_fun: joint_internal_function globals pars.
    253238  match joint_if_entry … int_fun with
    … …  
    255240    match joint_if_exit … int_fun with
    256241    [ dp exit exit_prf ⇒
    257       let exit' ≝ word_of_identifier … exit in
    258       let entry' ≝ word_of_identifier … entry in
    259242      let 〈maps, code〉 ≝ erasure_function int_fun in
    260243      let int_fun ≝ set_joint_code globals pars int_fun code entry exit in
    261244      let code ≝ relabelling_function maps int_fun in
    262         set_joint_code globals pars int_fun code (an_identifier … (bvt_lookup … entry' maps entry'))
    263         (an_identifier … (bvt_lookup … exit' maps exit'))
     245        set_joint_code globals pars int_fun code (lookup_def … maps entry entry)
     246        (lookup_def … maps exit exit)
    264247    ]
    265248  ].

  • src/joint/SemanticUtils.ma

    r1452 r1515  
    2525 λoldpc,l.
    2626  mk_pointer Code
    27    (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (nat_of_bitvector ? (word_of_identifier … l))).
     27   (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (pos (word_of_identifier … l))).
    2828// qed.
    2929
    … …  
    3434
    3535definition graph_label_of_pointer: pointer → res label ≝
    36  λp. OK … (an_identifier ? (bitvector_of_nat … (abs (offv (poff p))))).
     36 λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one | pos x ⇒ x | neg x ⇒ x ])).
    3737
    3838(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.

  • src/joint/TranslateUtils.ma

    r1352 r1515  
    2424    cases (fresh_regs pars0 globals def m) normalize nodelta
    2525    #def' #regs #EQ change in EQ with (|regs| = m) <EQ
    26     change with
    27     (|let 〈a,b〉 ≝ let 〈x,y〉 ≝ let 〈r,runiverse〉 ≝ ? in ? in ? in ?| = ?)
    28     cases (fresh … (joint_if_runiverse … def')) normalize // ]
     26    @refl
     27 ]
    2928qed.
    3029
Note: See TracChangeset for help on using the changeset viewer.