Changeset 1469 for src/joint


Ignore:
Timestamp:
Oct 27, 2011, 3:36:37 PM (8 years ago)
Author:
mulligan
Message:

finished new relabelling for graphs subject to one axiom closed

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/ProofUtils.ma

    r1467 r1469  
    141141
    142142let rec pre_erase_graph_internal_function'
    143   (params1: params1) (sem_params: sem_params) (globals: list ident)
    144     (state: state sem_params) (the_graph: codeT globals (graph_params params1 globals))
    145       (labels: list label) (num_nodes: nat)
    146         on num_nodes: ((BitVectorTrie Word 16) × (codeT globals (graph_params params1 globals))) ≝
    147   match num_nodes return λn. ((BitVectorTrie Word 16) × (codeT globals (graph_params params1 globals))) with
     143  (params1: params1) (globals: list ident)
     144    (the_graph: codeT globals (graph_params params1 globals)) (labels: list label)
     145      (entry_point: label) (size_counter: nat) (map: BitVectorTrie Word 16)
     146        (visited: BitVectorTrie bool 16)
     147          on size_counter: ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) ≝
     148  match size_counter return λ_.  ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
    148149  [ O ⇒
    149150    match labels with
    150     [ nil ⇒ 〈Stub Word 16, empty_graph …
     151    [ nil ⇒ 〈map, visited, the_graph
    151152    | _   ⇒ ⊥
    152153    ]
    153   | S num_nodes ⇒
    154     let program_counter ≝ (pc … state) in
    155       match code_pointer_of_address program_counter with
    156       [ OK code_pointer ⇒
    157         match graph_label_of_pointer code_pointer with
    158         [ OK lbl ⇒
    159           match lookup … the_graph lbl with
    160           [ Some statement ⇒
    161             let lbl' ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in
    162             let state ≝ set_pc … program_counter state in
    163             match statement with
    164             [ sequential seq l ⇒
    165               match seq with
    166               [ COST_LABEL cost_label ⇒ pre_erase_graph_internal_function' params1 sem_params globals state the_graph (lbl :: labels) num_nodes
    167               | _ ⇒
    168                 let 〈maps, instructions〉 ≝ pre_erase_graph_internal_function' params1 sem_params globals state the_graph labels num_nodes in
    169                 let maps ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l lbl' map ]) maps (lbl :: labels) in
    170                   〈maps, instructions〉
     154  | S size_counter ⇒
     155    let entry_point' ≝ match entry_point with [ an_identifier e ⇒ e ] in
     156    let statement ≝ lookup LabelTag ? the_graph entry_point in
     157    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
     158    [ None ⇒ ⊥ (* XXX: should not happen *)
     159    | Some statement ⇒
     160      let visited ≝ insert … entry_point' true visited in
     161      let entered_previously ≝ ? in
     162      match entered_previously return λe: bool. ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
     163      [ true ⇒ 〈map, visited, the_graph〉
     164      | false ⇒ (* XXX: never visited here before *)
     165        match statement return λs: joint_statement (graph_params params1 globals) globals. ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
     166        [ sequential seq l ⇒
     167          match seq with
     168          [ COST_LABEL cost_label ⇒
     169            pre_erase_graph_internal_function' params1 globals the_graph (entry_point :: labels) l size_counter map visited
     170          | COND acc_a cond_label ⇒
     171            let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph labels l size_counter map visited in
     172              match size_counter with
     173              [ O ⇒ ⊥ (* XXX: should never happen *)
     174              | S size_counter ⇒
     175                let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph labels cond_label size_counter map visited in
     176                let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
     177                  〈map, visited, the_graph〉
    171178              ]
    172             | _ ⇒
    173               let 〈maps, instructions〉 ≝ pre_erase_graph_internal_function' params1 sem_params globals state the_graph labels num_nodes in
    174               let maps ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l lbl' map ]) maps (lbl :: labels) in
    175                 〈maps, instructions〉
    176             ]
    177           | None           ⇒ ⊥ (* XXX: shouldn't happen *)
     179          | _ ⇒
     180            let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph labels l size_counter map visited in
     181            let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
     182              〈map, visited, the_graph〉
    178183          ]
    179         | Error message ⇒ ⊥ (* XXX: shouldn't happen *)
     184        | RETURN ⇒
     185          let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
     186            〈map, visited, the_graph〉
     187        | GOTO l ⇒
     188          let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph labels l size_counter map visited in
     189          let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
     190            〈map, visited, the_graph〉
    180191        ]
    181       | Error message   ⇒ ⊥ (* XXX: shouldn't happen *)
    182192      ]
    183   ].
    184   cases daemon (* XXX *)
     193    ]
     194  ].
     195  [4: @(lookup … entry_point' visited false)
     196  |*: cases daemon
     197  ]
    185198qed.
    186199
    187200definition pre_erase_graph_internal_function ≝
    188201  λparams1: params1.
    189   λsem_params: sem_params.
    190   λglobals: list ident.
    191   λstate: state sem_params.
     202  λglobals: list ident.
    192203  λthe_graph: codeT globals (graph_params params1 globals).
    193   λlabels: list label.
    194     pre_erase_graph_internal_function' params1 sem_params globals state the_graph labels (graph_num_nodes … the_graph).
    195 
    196 let rec relabel_graph'
    197   (params1: params1) (sem_params: sem_params) (globals: list ident)
    198     (state: state sem_params) (the_graph: codeT globals (graph_params params1 globals))
    199       (map: BitVectorTrie Word 16) (num_nodes: nat)
    200         on num_nodes: codeT globals (graph_params params1 globals) ≝
    201   match num_nodes with
    202   [ O ⇒ empty_graph …
    203   | S num_nodes ⇒
    204     let program_counter ≝ (pc … state) in
    205     match code_pointer_of_address program_counter with
    206     [ OK code_pointer ⇒
    207       match graph_label_of_pointer code_pointer with
    208       [ OK lbl ⇒
    209         match lookup … the_graph lbl with
    210         [ Some statement ⇒
    211           let lbl' ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in
    212           let new_statement ≝ relabel_joint_statement globals (graph_params params1 globals) map statement in
    213           let new_lbl ≝ an_identifier LabelTag ? in
    214           let state' ≝ set_pc … program_counter state in
    215           let tail_graph ≝ relabel_graph' params1 sem_params globals state' the_graph map num_nodes in
    216             add … tail_graph new_lbl new_statement
    217         | None ⇒ ⊥
    218         ]
    219       | Error message ⇒ ⊥
    220       ]
    221     | Error message ⇒ ⊥
    222     ]         
    223   ].
    224   [2: @(lookup … lbl' map lbl')
    225   |*: cases daemon (* XXX *)
    226   ]
    227 qed.
     204  λentry_point: label.
     205    let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] entry_point (graph_num_nodes … the_graph) (Stub …) (Stub …) in
     206      〈map, the_graph〉.
     207
     208axiom relabel_graph':
     209  ∀params1: params1.
     210  ∀globals: list ident.
     211  ∀the_graph: codeT globals (graph_params params1 globals).
     212  ∀map: BitVectorTrie Word 16.
     213  ∀visited: BitVectorTrie bool 16.
     214  ∀num_nodes: nat.
     215    codeT globals (graph_params params1 globals).
    228216
    229217definition relabel_graph ≝
    230   λparams1.
    231   λsem_params.
    232   λglobals.
    233   λstate: state sem_params.
     218  λparams1: params1.
     219  λglobals: list ident.
    234220  λthe_graph: codeT globals (graph_params params1 globals).
    235221  λmap: BitVectorTrie Word 16.
    236     relabel_graph' params1 sem_params globals state the_graph map (graph_num_nodes … the_graph).
     222    relabel_graph' params1 globals the_graph map (Stub …) (graph_num_nodes … the_graph).
    237223
    238224definition pre_erase_graph_joint_internal_function ≝
    239225  λparams1: params1.
    240   λsem_params: sem_params.
    241   λglobals: list ident.
    242   λstate: state sem_params.
     226  λglobals: list ident.
    243227  λint_fun: joint_internal_function globals (graph_params params1 globals).
    244228  let luniverse ≝ joint_if_luniverse globals (graph_params params1 globals) int_fun in
     
    253237    match joint_if_exit … int_fun with
    254238    [ dp exit exit_prf ⇒
    255       let 〈maps, code〉 ≝ pre_erase_graph_internal_function params1 sem_params globals state code [ ] in
    256       let code ≝ relabel_graph params1 sem_params globals state code maps in
     239      let 〈maps, code〉 ≝ pre_erase_graph_internal_function params1 globals code entry in
     240      let code ≝ relabel_graph params1 globals code maps in
    257241        mk_joint_internal_function …
    258242          luniverse runiverse result params
     
    262246  cases daemon (* XXX *)
    263247qed.
    264 
    265 (* XXX: use make_initial_state to build an initial state for a program *)
Note: See TracChangeset for help on using the changeset viewer.