Ignore:
Timestamp:
Oct 6, 2011, 6:45:54 PM (9 years ago)
Author:
campbell
Message:

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

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

Legend:

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

  • Deliverables/D3.3/id-lookup-branch/Cminor/cminorMatitaPrinter.ml

    r1197 r1311  
    352352
    353353let print_program p =
    354   Printf.sprintf "include \"Cminor/semantics.ma\".\ninclude \"common/Animation.ma\".\n\n%s\n\n%s\n\ndefinition myprog : Cminor_program :=\nmk_program ?? [\n%s\n]%s\n[%s]\n.\n"
     354  Printf.sprintf "include \"Cminor/semantics.ma\".\ninclude \"common/Animation.ma\".\n\n%s\n\n%s\n\ndefinition myprog : Cminor_program :=\nmk_program ?? [%s] [\n%s\n]%s\n.\n"
    355355    (define_var_ids p.Cminor.vars)
    356356    (print_functs p.Cminor.functs)
     357    (print_vars 2 p.Cminor.vars)
    357358    (print_fun' 2 p.Cminor.functs)
    358359    (print_main 2 p.Cminor.main)
    359     (print_vars 2 p.Cminor.vars)
    360 
     360
  • Deliverables/D3.3/id-lookup-branch/Cminor/initialisation.ma

    r1153 r1311  
    110110λp.
    111111  mk_program ??
     112    (empty_vars (prog_vars ?? p))
    112113    (add_statement (prog_main ?? p) (init_vars (prog_vars ?? p)) (prog_funct ?? p))
    113     (prog_main ?? p)
    114     (empty_vars (prog_vars ?? p)).
    115    
     114    (prog_main ?? p).
  • Deliverables/D3.3/id-lookup-branch/Cminor/semantics.ma

    r1153 r1311  
    459459].
    460460
    461 definition Cminor_exec : execstep io_out io_in ≝
    462   mk_execstep … ? is_final mem_of_state eval_step.
     461definition Cminor_exec : trans_system io_out io_in ≝
     462  mk_trans_system … ? (λ_.is_final) eval_step.
    463463
    464464axiom MainMissing : String.
    465465
    466 definition make_initial_state : Cminor_program → res (genv × state) ≝
     466definition make_global : Cminor_program → genv ≝
     467λp. globalenv Genv ?? (λx.x) p.
     468
     469definition make_initial_state : Cminor_program → res state ≝
    467470λp.
    468   do ge ← globalenv Genv ?? (λx.x) p;
     471  let ge ≝ make_global p in
    469472  do m ← init_mem Genv ?? (λx.x) p;
    470473  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    471474  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
    472   OK ? 〈ge, Callstate f (nil ?) m SStop〉.
     475  OK ? (Callstate f (nil ?) m SStop).
    473476
    474477definition Cminor_fullexec : fullexec io_out io_in ≝
    475   mk_fullexec … Cminor_exec ? make_initial_state.
    476 
    477 definition make_initial_noinit_state : Cminor_noinit_program → res (genv × state) ≝
     478  mk_fullexec … Cminor_exec make_global make_initial_state.
     479
     480definition make_noinit_global : Cminor_noinit_program → genv ≝
     481λp. globalenv Genv ?? (λx.[Init_space x]) p.
     482
     483definition make_initial_noinit_state : Cminor_noinit_program → res state ≝
    478484λp.
    479   do ge ← globalenv Genv ?? (λx.[Init_space x]) p;
     485  let ge ≝ make_noinit_global p in
    480486  do m ← init_mem Genv ?? (λx.[Init_space x]) p;
    481487  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    482488  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
    483   OK ? 〈ge, Callstate f (nil ?) m SStop〉.
     489  OK ? (Callstate f (nil ?) m SStop).
    484490
    485491definition Cminor_noinit_fullexec : fullexec io_out io_in ≝
    486   mk_fullexec … Cminor_exec ? make_initial_noinit_state.
     492  mk_fullexec … Cminor_exec make_noinit_global make_initial_noinit_state.
  • Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma

    r1153 r1311  
    155155   responsible for initialisation and we only give the size of each variable. *)
    156156
    157 definition Cminor_program ≝ program (fundef internal_function) (list init_data).
     157definition Cminor_program ≝ program (λ_.fundef internal_function) (list init_data).
    158158
    159 definition Cminor_noinit_program ≝ program (fundef internal_function) nat.
     159definition Cminor_noinit_program ≝ program (λ_.fundef internal_function) nat.
  • Deliverables/D3.3/id-lookup-branch/Cminor/test/search.Cminor.ma

    r1197 r1311  
    281281
    282282definition myprog : Cminor_program :=
    283 mk_program ?? [
     283mk_program ?? [] [
    284284  (pair ?? id__div32u f__div32u);
    285285  (pair ?? id__div32s f__div32s);
     
    287287  (pair ?? id_main f_main)
    288288]  id_main
    289 []
    290289.
    291 
    292    example exec: finishes_with (repr 3) ? (exec_up_to Cminor_fullexec myprog 1000 [ ]).
    293    normalize  (* you can examine the result here *)
    294    @refl qed.
    295 
    296 
    297 include "Cminor/toRTLabs.ma".
    298 include "RTLabs/semantics.ma".
    299 
    300 example execRTL: finishes_with (repr 3) ? (do myprog' ← cminor_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [ ]).
    301 normalize  (* you can examine the result here *)
    302 @refl
    303 qed.
    304 
    305 
  • Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma

    r1153 r1311  
    719719
    720720definition cminor_noinit_to_rtlabs : Cminor_noinit_program → res RTLabs_program ≝
    721 transform_partial_program ???
    722   (transf_partial_fundef ?? c2ra_function).
     721λp.transform_partial_program … p (transf_partial_fundef … c2ra_function).
    723722
    724723include "Cminor/initialisation.ma".
Note: See TracChangeset for help on using the changeset viewer.