source: src/joint/SemanticUtils.ma @ 1329

Last change on this file since 1329 was 1329, checked in by sacerdot, 9 years ago
  1. Definition of addresses moved to BEMem
  2. Basic functions on addresses implemented in BEMem and used everywhere
  3. Semantics of ERTL extended statements completed
File size: 2.5 KB
Line 
1include "joint/semantics.ma".
2
3(*** Store/retrieve on pseudo-registers ***)
4
5axiom BadRegister : String.
6
7definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v.
8
9definition reg_retrieve : register_env beval → register → res beval ≝
10 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
11
12(*** Store/retrieve on hardware registers ***)
13
14axiom hw_register_env: Type[0]. (* CSC: use the one in I8051? *)
15axiom hwreg_retrieve : hw_register_env → Register → res beval.
16axiom hwreg_store : Register → beval → hw_register_env → res hw_register_env.
17
18(****************************************************************************)
19
20(*CSC: XXXX; do we need to create a brand new chunk per label, so that
21  pointer operations on labels are not semantically valid?
22  ATM, the pointers are not valid (they do not point to allocated regions)
23  and, moreover, they conflict with function blocks and with other pointers
24  in other functions. However, there could be simpler ways to invalidate
25  pointer arithmetics on Code pointers.
26*)
27definition pointer_of_label: label → Σp:pointer. ptype p = Code ≝
28 λl.
29  mk_pointer Code
30   (mk_block Code (Zopp (nat_of_bitvector ? (word_of_identifier … l))))
31   ? (mk_offset OZ).
32// qed.
33
34(*CSC: XXXX; inverse of the previous function, but it does not check that
35  the offset is zero and thus it never fails. *)
36definition label_of_pointer: pointer → res label ≝
37 λp. OK … (an_identifier ? (bitvector_of_nat … (abs (block_id (pblock p))))).
38
39(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
40  Maybe there is a better way to organize the code!!! *)
41definition graph_succ_p: label → address → address.
42 #l #_ generalize in match (refl … (address_of_pointer (pointer_of_label l)))
43 cases (address_of_pointer (pointer_of_label l)) in ⊢ (???% → ?)
44  [ #res #_ @res
45  | #msg cases (pointer_of_label l) * * #q #com #off #E1 #E2 destruct ]
46qed.
47
48axiom BadProgramCounter: String.
49definition graph_fetch_statement:
50 ∀params1,sem_params,globals.
51  genv … (graph_params params1 globals) →
52   state sem_params → res (joint_statement (graph_params_ params1) globals) ≝
53 λparams1,sem_params,globals,ge,st.
54  do p ← pointer_of_address (pc … st) ;
55  let b ≝ pblock p in
56  do l ← label_of_pointer p;
57  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
58  match def with
59  [ Internal def' ⇒
60     opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … def') l)
61  | External _ ⇒ Error … [MSG BadProgramCounter]].
Note: See TracBrowser for help on using the repository browser.