source: src/ERTLptr/ERTLptr_semantics.ma @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 8 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 2.6 KB
Line 
1include "joint/semanticsUtils.ma".
2include "ERTLptr/ERTLptr.ma". (* CSC: syntax.ma in RTLabs *)
3include "ERTL/ERTL_semantics.ma".
4include alias "common/Identifiers.ma".
5
6definition ertlptr_save_frame:
7 call_kind → unit → ident → state_pc ERTL_state → res (state … ERTL_state) ≝
8 λk.λ_.λid.λst.
9 do st ← match k with [ID ⇒ push_ra … st (pc … st) |
10 PTR ⇒ return (st_no_pc … st)] ; OK …
11   (set_frms ERTL_state (〈\fst (regs ERTL_state st),id〉 :: (st_frms … st))
12    (set_regs ERTL_state 〈empty_map …,\snd (regs … st)〉 st)).
13
14definition eval_ertlptr_seq:
15 ∀F. ∀globals. genv_gen F globals →
16  ertlptr_seq → ident → state ERTL_state →
17   res (state ERTL_state) ≝
18 λF,globals,ge,stm,id,st.
19  match stm with
20   [ ertlptr_ertl seq ⇒ eval_ertl_seq F globals ge seq id st
21   | LOW_ADDRESS r l ⇒  ! pc_lab ← get_pc_from_label … ge id l;
22                        let 〈addrl,addrh〉 ≝ beval_pair_of_pc pc_lab in
23                        ps_reg_store_status r addrl st
24   | HIGH_ADDRESS r l ⇒ ! pc_lab ← get_pc_from_label … ge id l;
25                        let 〈addrl,addrh〉 ≝  beval_pair_of_pc pc_lab in
26                        ps_reg_store_status r addrh st
27   ].
28   
29definition ERTLptr_semantics ≝
30  make_sem_graph_params ERTLptr
31  (λF. mk_sem_unserialized_params ??
32  (* st_pars            ≝ *) ERTL_state
33  (* acca_store_        ≝ *) ps_reg_store
34  (* acca_retrieve_     ≝ *) ps_reg_retrieve
35  (* acca_arg_retrieve_ ≝ *) ps_arg_retrieve
36  (* accb_store_        ≝ *) ps_reg_store
37  (* accb_retrieve_     ≝ *) ps_reg_retrieve
38  (* accb_arg_retrieve_ ≝ *) ps_arg_retrieve
39  (* dpl_store_         ≝ *) ps_reg_store
40  (* dpl_retrieve_      ≝ *) ps_reg_retrieve
41  (* dpl_arg_retrieve_  ≝ *) ps_arg_retrieve
42  (* dph_store_         ≝ *) ps_reg_store
43  (* dph_retrieve_      ≝ *) ps_reg_retrieve
44  (* dph_arg_retrieve_  ≝ *) ps_arg_retrieve
45  (* snd_arg_retrieve_  ≝ *) ps_arg_retrieve
46  (* pair_reg_move_     ≝ *) ertl_eval_move
47  (* allocate_local     ≝ *) ertl_allocate_local
48  (* save_frame         ≝ *) ertlptr_save_frame
49  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
50  (* fetch_external_args≝ *) ertl_fetch_external_args
51  (* set_result         ≝ *) ertl_set_result
52  (* call_args_for_main ≝ *) 0
53  (* call_dest_for_main ≝ *) it
54  (* read_result        ≝ *) (λ_.λ_.λ_.
55     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
56  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.λ_.eval_ertlptr_seq F gl ge stm id)
57  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.pop_ra …)).
Note: See TracBrowser for help on using the repository browser.