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:
5 edited

Legend:

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

  • Deliverables/D3.3/id-lookup-branch/Cminor/initialisation.ma

    r1102 r1153  
    5454] qed.
    5555
    56 definition init_vars : list (ident × (list init_data) × region × unit) → Σs:stmt. stmt_inv s ≝
     56definition init_vars : list (ident × region × (list init_data)) → Σs:stmt. stmt_inv s ≝
    5757λvars. foldr ? (Σs:stmt. stmt_inv s)
    58   (λvar,s. dp ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) ?) (dp ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars.
     58  (λvar,s. dp ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (dp ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars.
    5959% [ % [ % // | @(use_sig ? stmt_inv) ] | @(use_sig ? stmt_inv) ]
    6060qed.
     
    102102] qed.
    103103
    104 definition empty_vars : list (ident × (list init_data) × region × unit) →
    105                         list (ident × (list init_data) × region × unit) ≝
    106 map ?? (λv. 〈〈〈\fst (\fst (\fst v)),
    107                [Init_space (size_init_data_list (\snd (\fst (\fst v))))]〉,
    108               \snd (\fst v)〉,
    109               \snd v〉).
     104definition empty_vars : list (ident × region × (list init_data)) →
     105                        list (ident × region × nat) ≝
     106map ?? (λv. 〈〈\fst (\fst v), \snd (\fst v)〉,
     107              size_init_data_list (\snd v)〉).
    110108
    111 definition replace_init : Cminor_program → Cminor_program ≝
     109definition replace_init : Cminor_program → Cminor_noinit_program ≝
    112110λp.
    113111  mk_program ??
  • Deliverables/D3.3/id-lookup-branch/Cminor/semantics.ma

    r1135 r1153  
    466466definition make_initial_state : Cminor_program → res (genv × state) ≝
    467467λp.
    468   do ge ← globalenv Genv ?? p;
    469   do m ← init_mem Genv ?? p;
     468  do ge ← globalenv Genv ?? (λx.x) p;
     469  do m ← init_mem Genv ?? (λx.x) p;
    470470  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    471471  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
     
    474474definition Cminor_fullexec : fullexec io_out io_in ≝
    475475  mk_fullexec … Cminor_exec ? make_initial_state.
     476
     477definition make_initial_noinit_state : Cminor_noinit_program → res (genv × state) ≝
     478λp.
     479  do ge ← globalenv Genv ?? (λx.[Init_space x]) p;
     480  do m ← init_mem Genv ?? (λx.[Init_space x]) p;
     481  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
     482  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
     483  OK ? 〈ge, Callstate f (nil ?) m SStop〉.
     484
     485definition Cminor_noinit_fullexec : fullexec io_out io_in ≝
     486  mk_fullexec … Cminor_exec ? make_initial_noinit_state.
  • Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma

    r1104 r1153  
    151151}.
    152152
    153 definition Cminor_program ≝ program (fundef internal_function) unit.
     153(* We define two closely related versions of Cminor, the first with the original
     154   initialisation data for global variables, and the second where the code is
     155   responsible for initialisation and we only give the size of each variable. *)
     156
     157definition Cminor_program ≝ program (fundef internal_function) (list init_data).
     158
     159definition Cminor_noinit_program ≝ program (fundef internal_function) nat.
  • Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma

    r1105 r1153  
    718718qed.
    719719
    720 definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
     720definition cminor_noinit_to_rtlabs : Cminor_noinit_program → res RTLabs_program ≝
    721721transform_partial_program ???
    722722  (transf_partial_fundef ?? c2ra_function).
     
    724724include "Cminor/initialisation.ma".
    725725
    726 definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝
    727 λp. let p' ≝ replace_init p in cminor_to_rtlabs p.
     726definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
     727λp. let p' ≝ replace_init p in cminor_noinit_to_rtlabs p'.
Note: See TracChangeset for help on using the changeset viewer.