Ignore:
Timestamp:
Aug 24, 2011, 5:12:10 PM (9 years ago)
Author:
campbell
Message:

Update branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/ERTL/ERTL.ma

    r1084 r1109  
    3232  | ertl_st_load: register → register → register → label → ertl_statement
    3333  | ertl_st_store: register → register → register → label → ertl_statement
    34   | ertl_st_call_id: label → Byte → label → ertl_statement
     34  | ertl_st_call_id: ident → Byte → label → ertl_statement
    3535  | ertl_st_cond: register → label → label → ertl_statement
    36   | ertl_st_return: label → ertl_statement.
     36  | ertl_st_return: ertl_statement.
    3737
    3838definition ertl_statement_graph ≝ graph ertl_statement.
  • Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTLI.ma

    r1084 r1109  
    231231    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    232232      joint_st_sequential ? globals (joint_instr_skip globals) l
    233   | ertl_st_return l ⇒ joint_st_return ? globals
     233  | ertl_st_return ⇒ joint_st_return ? globals
    234234  ].
    235235  cases daemon (* XXX: todo -- proofs regarding gvars *)
  • Deliverables/D3.3/id-lookup-branch/ERTL/liveness.ma

    r1098 r1109  
    1 
     1include "utilities/Fix.ma".
    22include "ASM/Util.ma".
    33include "ERTL/ERTL.ma".
     
    3131    foldr ? ? andb true (map ? ? (λx. member A eq_a x r) l).
    3232
    33 definition list_set_member ≝
    34   λA: Type[0].
    35   λeq_a: A → A → bool.
    36   λa: A.
    37   λl: list A.
    38     member A eq_a a l.
     33definition list_set_member ≝ member.
     34
     35definition list_set_fold ≝ foldr.
    3936
    4037definition statement_successors ≝
     
    303300    | Some stmt ⇒ statement_semantics stmt (liveafter label)
    304301    ]
     302  in
     303  let liveafter ≝ λlabel. λliveafter: valuation.
     304    match lookup ? ? (ertl_if_graph int_fun) label with
     305    [ None      ⇒ ?
     306    | Some stmt ⇒ list_set_fold ? ? (λsuccessor. λaccu.
     307        lattice_join (livebefore successor liveafter) accu)
     308        lattice_bottom (statement_successors stmt)
     309    ]
    305310  in ?.
Note: See TracChangeset for help on using the changeset viewer.