Ignore:
Timestamp:
Aug 30, 2011, 6:55:12 PM (9 years ago)
Author:
campbell
Message:

Merge trunk into branch.

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

Legend:

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

  • Deliverables/D3.3/id-lookup-branch/RTLabs/semantics.ma

    r961 r1153  
    168168    [ Internal fn ⇒
    169169        ! locals ← params_store (f_params fn) params (init_locals (f_locals fn));
     170        (* CSC: XXX alignment call (concrete_stacksize in OCaml) is missing
     171           here *)
    170172        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
    171173        ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) fs m'〉
     
    207209definition make_initial_state : RTLabs_program → res (genv × state) ≝
    208210λp.
    209   do ge ← globalenv Genv ?? p;
    210   do m ← init_mem Genv ?? p;
     211  do ge ← globalenv Genv ?? (λx.[Init_space x]) p;
     212  do m ← init_mem Genv ?? (λx.[Init_space x]) p;
    211213  let main ≝ prog_main ?? p in
    212214  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
  • Deliverables/D3.3/id-lookup-branch/RTLabs/syntax.ma

    r1105 r1153  
    1414| St_cost : costlabel → label → statement
    1515| St_const : register → constant → label → statement
    16 | St_op1 : unary_operation → register → register → label → statement
    17 | St_op2 : binary_operation → register → register → register → label → statement
     16| St_op1 : unary_operation → register → register → label → statement (* destination source *)
     17| St_op2 : binary_operation → register → register → register → label → statement (* destination source1 source2 *)
    1818| St_load : memory_chunk → register → register → label → statement
    1919| St_store : memory_chunk → register → register → label → statement
     
    7070
    7171(* Note that the global variables will be initialised by the code in main
    72    by this stage.  All initialisation data should only reserve space. *)
     72   by this stage, so the only initialisation data is the amount of space to
     73   allocate. *)
    7374
    74 definition RTLabs_program ≝ program (fundef internal_function) unit.
     75definition RTLabs_program ≝ program (fundef internal_function) nat.
    7576
    76 (* TO CONSIDER:
    77 
    78    - removing most successor labels from the statements (bit icky, what about
    79      return and jump tables?)
    80    - seems like load and store ought to have types that control the size of the
    81      register list based on the addressing mode; similarly, memory_chunk and
    82      register are probably related.
    83    - label and register generation really tell us something about the sets of
    84      labels and register that may appear, perhaps it should be renamed, or the
    85      graph made dependent on them to make it obvious, etc.
    86  *)
Note: See TracChangeset for help on using the changeset viewer.