source: src/joint/SemanticUtils.ma @ 1515

Last change on this file since 1515 was 1515, checked in by campbell, 8 years ago

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File size: 2.8 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
15definition init_hw_register_env: address → hw_register_env ≝
16 λaddr.
17  let 〈dpl,dph〉 ≝ addr in
18  let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in
19   hwreg_store RegisterDPL dpl env.
20
21(****************************************************************************)
22
23definition graph_pointer_of_label0:
24 pointer → label → Σp:pointer. ptype p = Code ≝
25 λoldpc,l.
26  mk_pointer Code
27   (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (pos (word_of_identifier … l))).
28// qed.
29
30definition graph_pointer_of_label:
31 ∀params1.∀globals. genv … (graph_params params1 globals) → pointer → label → res (Σp:pointer. ptype p = Code) ≝
32 λ_.λ_.λ_.λoldpc,l.
33  OK ? (graph_pointer_of_label0 oldpc l).
34
35definition graph_label_of_pointer: pointer → res label ≝
36 λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one | pos x ⇒ x | neg x ⇒ x ])).
37
38(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
39 But I can't use it directly because this one uses a concrete definition of
40 pointer_of_label and it is used to istantiate the more_sem_params record
41 where the abstract version is declared as a field. Is there a better way
42 to organize the code? *)
43definition graph_succ_p: label → address → res address ≝
44 λl,old.
45  do ptr ← pointer_of_address old ;
46  let newptr ≝ graph_pointer_of_label0 ptr l in
47  address_of_pointer newptr.
48
49axiom BadProgramCounter: String.
50
51definition graph_fetch_function:
52 ∀params1,sem_params,globals.
53  genv … (graph_params params1 globals) →
54   state sem_params → res (joint_internal_function … (graph_params params1 globals)) ≝
55 λparams1,sem_params,globals,ge,st.
56  do p ← code_pointer_of_address (pc … st) ;
57  let b ≝ pblock p in
58  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
59  match def with
60  [ Internal def' ⇒ OK … def'
61  | External _ ⇒ Error … [MSG BadProgramCounter]].
62
63definition graph_fetch_statement:
64 ∀params1,sem_params,globals.
65  genv … (graph_params params1 globals) →
66   state sem_params → res (joint_statement (graph_params_ params1) globals) ≝
67 λparams1,sem_params,globals,ge,st.
68  do p ← code_pointer_of_address (pc … st) ;
69  do f ← graph_fetch_function … ge st ;
70  do l ← graph_label_of_pointer p;
71  opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l).
Note: See TracBrowser for help on using the repository browser.