source: src/joint/SemanticUtils.ma @ 1408

Last change on this file since 1408 was 1408, checked in by sacerdot, 8 years ago
  1. Added joint/BEGlobalenvs that is a modification of common/Globalenvs where
    • the memory used is the back-end one
    • no lookup via values is implemented
    • global variables are never initialized in the back-end
  2. Added to all semantics some default value to initialize the initial state
  3. Initial state initialization (in joint/semantics.ma) almost completed.
File size: 3.4 KB
Line 
1include "joint/semantics.ma".
2include alias "common/Identifiers.ma".
3
4(*** Store/retrieve on pseudo-registers ***)
5
6axiom BadRegister : String.
7
8definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v.
9
10definition reg_retrieve : register_env beval → register → res beval ≝
11 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
12
13(*** Store/retrieve on hardware registers ***)
14
15axiom hw_register_env: Type[0]. (* CSC: use the one in I8051? *)
16axiom empty_hw_register_env: hw_register_env.
17axiom hwreg_retrieve : hw_register_env → Register → res beval.
18axiom hwreg_store : Register → beval → hw_register_env → res hw_register_env.
19
20(****************************************************************************)
21
22(*CSC: XXXXXXXXXXXXXXXXX bug here; we need to change the encoding so that
23  the block is the one of the function and the offset corresponds to the
24  label. Code pointer arithmetics must be prevented in another way, i.e.
25  by not allowing any increment/decrement on Code regions (with the
26  exception of LIN's succ_pc function). If we don't do that, then the
27  find_funct_ptr (e.g. in graph_fetch_statement) are not correct! *)
28(*CSC: XXXX; do we need to create a brand new chunk per label, so that
29  pointer operations on labels are not semantically valid?
30  ATM, the pointers are not valid (they do not point to allocated regions)
31  and, moreover, they conflict with function blocks and with other pointers
32  in other functions. However, there could be simpler ways to invalidate
33  pointer arithmetics on Code pointers.
34*)
35definition pointer_of_label: label → Σp:pointer. ptype p = Code ≝
36 λl.
37  mk_pointer Code
38   (mk_block Code (Zopp (nat_of_bitvector ? (word_of_identifier … l))))
39   ? (mk_offset OZ).
40// qed.
41
42(*CSC: XXXX; inverse of the previous function, but it does not check that
43  the offset is zero and thus it never fails. *)
44definition label_of_pointer: pointer → res label ≝
45 λp. OK … (an_identifier ? (bitvector_of_nat … (abs (block_id (pblock p))))).
46
47(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
48 But I can't use it directly because this one uses a concrete definition of
49 pointer_of_label and it is used to istantiate the more_sem_params record
50 where the abstract version is declared as a field. Is there a better way
51 to organize the code? *)
52definition graph_succ_p: label → address → res address ≝
53 λl.λ_.address_of_pointer (pointer_of_label l).
54
55axiom BadProgramCounter: String.
56
57definition graph_fetch_function:
58 ∀params1,sem_params,globals.
59  genv … (graph_params params1 globals) →
60   state sem_params → res (joint_internal_function … (graph_params params1 globals)) ≝
61 λparams1,sem_params,globals,ge,st.
62  do p ← code_pointer_of_address (pc … st) ;
63  let b ≝ pblock p in
64  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
65  match def with
66  [ Internal def' ⇒ OK … def'
67  | External _ ⇒ Error … [MSG BadProgramCounter]].
68
69definition graph_fetch_statement:
70 ∀params1,sem_params,globals.
71  genv … (graph_params params1 globals) →
72   state sem_params → res (joint_statement (graph_params_ params1) globals) ≝
73 λparams1,sem_params,globals,ge,st.
74  do p ← code_pointer_of_address (pc … st) ;
75  do f ← graph_fetch_function … ge st ;
76  do l ← label_of_pointer p;
77  opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l).
Note: See TracBrowser for help on using the repository browser.