source: src/RTLabs/import.ma @ 726

Last change on this file since 726 was 726, checked in by campbell, 9 years ago

Change identifiers to Words in Clight and RTLabs semantics.

File size: 8.1 KB
Line 
1
2include "RTLabs/RTLabs-sem.ma".
3
4definition new_reg : internal_function → res (register × internal_function) ≝
5λf. do 〈r, g〉 ← register_new (f_reggen f);
6    OK ? 〈r, mk_internal_function (f_labgen f) g (f_sig f) (f_result f) (f_params f)
7            (f_locals f) (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
8
9definition new_label : internal_function → res (label × internal_function) ≝
10λf. do 〈l, g〉 ← label_new (f_labgen f);
11    OK ? 〈l, mk_internal_function g (f_reggen f) (f_sig f) (f_result f) (f_params f)
12            (f_locals f) (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
13
14definition new_statement : internal_function → label → statement → internal_function ≝
15λf,l,s. mk_internal_function (f_labgen f) (f_reggen f) (f_sig f) (f_result f) (f_params f)
16            (f_locals f) (f_stacksize f)
17            (graph_add ? (f_graph f) l s) (f_entry f) (f_exit f).
18
19let rec n_labels (n:nat) (g:label_generation) : res (Vector label n × label_generation) ≝
20match n with
21[ O ⇒ OK ? 〈[[ ]], g〉
22| S m ⇒ do 〈ls, g'〉 ← n_labels m g;
23        do 〈l, g''〉 ← label_new g;
24        OK ? 〈l:::ls, g''〉
25].
26
27let rec n_regs (n:nat) (g:register_generation) : res (Vector label n × register_generation) ≝
28match n with
29[ O ⇒ OK ? 〈[[ ]], g〉
30| S m ⇒ do 〈ls, g'〉 ← n_regs m g;
31        do 〈l, g''〉 ← register_new g;
32        OK ? 〈l:::ls, g''〉
33].
34
35definition pre_registers ≝ Sig nat (Vector nat).
36
37record pre_internal_function : Type[0] ≝
38{ pf_sig       : signature
39; pf_result    : pre_registers
40; pf_params    : list pre_registers
41; pf_locals    : list pre_registers
42; pf_stacksize : nat
43; pf_graph     : list (nat × ((nat → res label) → (nat → res register) → res statement))
44; pf_entry     : nat
45; pf_exit      : nat
46}.
47(* XXX projection generation with nat broken *)
48definition pf_stacksize ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ s _ _ _ ⇒ s ].
49definition pf_graph ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ g _ _ ⇒ g ].
50definition pf_entry ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ e _ ⇒ e ].
51definition pf_exit ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ _ e ⇒ e ].
52
53definition make_registers :
54  (nat → option register) → pre_registers → register_generation →
55  res ((nat → option register) × register_generation × registers) ≝
56λm,rs0,g.
57match rs0 with [ dp n rs ⇒
58  do 〈m,grs〉 ← fold_right_i ??? (λn,r,mr.
59                  do 〈m,grs〉 ← mr;
60                  let 〈g,rs〉 ≝ grs in
61                  match m r with
62                  [ Some r' ⇒ OK ? 〈m,〈g,r':::rs〉〉
63                  | None ⇒ do 〈r',g'〉 ← register_new g;
64                           OK ? 〈λn. if eqb r n then Some ? r' else m n,〈g',r':::rs〉〉
65                  ]) (OK ? 〈m,〈g,[[ ]]〉〉) rs;
66  let 〈g',rs'〉 ≝ grs in
67    OK ? 〈〈m,g'〉,dp ?? n rs'〉
68].
69
70definition make_registers_list :
71  (nat → option register) → list pre_registers → register_generation →
72  res ((nat → option register) × register_generation × (list registers)) ≝
73λm,lrs,g.
74foldr ?? (λrs,acc. do 〈acc',l〉 ← acc;
75                   let 〈m,g〉 ≝ acc' in
76                   do 〈mg,rs'〉 ← make_registers m rs g;
77                   OK ? 〈mg,rs'::l〉) (OK ? 〈〈m,g〉,[ ]〉) lrs.
78
79definition make_internal_function : pre_internal_function → res internal_function ≝
80λpre_f.
81  let rgen0 ≝ register_gen_new in
82  do 〈rmapgen1, result〉 ← make_registers (λ_.None ?) (pf_result pre_f) rgen0;
83  let 〈rmap1, rgen1〉 ≝ rmapgen1 in
84  do 〈rmapgen2, params〉 ← make_registers_list rmap1 (pf_params pre_f) rgen1;
85  let 〈rmap2, rgen2〉 ≝ rmapgen2 in
86  do 〈rmapgen3, locals〉 ← make_registers_list rmap2 (pf_locals pre_f) rgen2;
87  let 〈rmap3, rgen3〉 ≝ rmapgen3 in
88  let rmap ≝ λn. opt_to_res … (rmap3 n) in
89  let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in
90  do 〈labels, gen〉 ← n_labels max_stmt label_gen_new;
91  let get_label ≝ λn. opt_to_res … (get_index_weak_v ?? labels n) in
92  do graph ← foldr ?? (λp,g0. do g ← g0;
93                              let 〈l,s〉 ≝ p in
94                              do l' ← get_label l;
95                              do s' ← s rmap get_label;
96                              OK ? (graph_add ? g l' s')) (OK ? (empty_graph ?)) (pf_graph pre_f);
97  do entry ← get_label (pf_entry pre_f);
98  do exit ← get_label (pf_exit pre_f);
99  OK ? (mk_internal_function
100         gen
101         rgen3
102         (pf_sig pre_f)
103         result
104         params
105         locals
106         (pf_stacksize pre_f)
107         graph
108         entry
109         exit
110         ).
111
112definition make_regs : (nat → res register) → pre_registers → res registers ≝
113λm,p.
114match p with
115[ dp n ps ⇒
116    do rs ← fold_right_i ??? (λn,r,rs0.
117                  do rs ← rs0;
118                  do r' ← m r;
119                  OK ? (r':::rs)) (OK ? [[ ]]) ps;
120    OK ? (dp ?? n rs)
121].
122
123definition make_regs_list : (nat → res register) → list pre_registers → res (list registers) ≝
124λm,ps. foldr ?? (λp,rs0. do rs ← rs0; do r ← make_regs m p; OK ? (r::rs)) (OK ? [ ]) ps.
125
126let rec make_St_skip l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_skip l').
127let rec make_St_cost cl l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_cost cl l').
128let rec make_St_const rs cst l ≝ λr:nat → res register.λf:nat → res label. do rs' ← make_regs r rs; do l' ← f l; OK ? (St_const rs' cst l').
129let rec make_St_op1 op dst src l ≝ λr:nat → res register.λf:nat → res label. do dst' ← make_regs r dst; do src' ← make_regs r src; do l' ← f l; OK ? (St_op1 op dst' src' l').
130let rec make_St_op2 op dst src1 src2 l ≝ λr:nat → res register.λf:nat → res label. do dst' ← make_regs r dst; do src1' ← make_regs r src1; do src2' ← make_regs r src2; do l' ← f l; OK ? (St_op2 op dst' src1' src2' l').
131let rec make_St_load chunk mode args dst l ≝ λr:nat → res register.λf:nat → res label. do dst' ← make_regs r dst; do l' ← f l; OK ? (St_load chunk mode args dst' l').
132let rec make_St_store chunk mode args src l ≝ λr:nat → res register.λf:nat → res label. do src' ← make_regs r src; do l' ← f l; OK ? (St_store chunk mode args src' l').
133let rec make_St_call_id id args dst sig l ≝ λr:nat → res register.λf:nat → res label. do args' ← make_regs_list r args; do dst' ← make_regs r dst; do l' ← f l; OK ? (St_call_id id args' dst' sig l').
134let rec make_St_call_ptr frs args dst sig l ≝ λr:nat → res register.λf:nat → res label. do frs' ← make_regs r frs; do args' ← make_regs_list r args; do dst' ← make_regs r dst; do l' ← f l; OK ? (St_call_ptr frs' args' dst' sig l').
135let rec make_St_tailcall_id id args sig ≝ λr:nat → res register.λf:nat → res label.  do args' ← make_regs_list r args; OK statement (St_tailcall_id id args' sig).
136let rec make_St_tailcall_ptr frs args sig ≝ λr:nat → res register.λf:nat → res label. do frs' ← make_regs r frs; do args' ← make_regs_list r args; OK statement (St_tailcall_ptr frs' args' sig).
137let rec make_St_condcst cst ltrue lfalse ≝ λr:nat → res register.λf:nat → res label. do ltrue' ← f ltrue; do lfalse' ← f lfalse; OK ? (St_condcst cst ltrue' lfalse').
138let rec make_St_cond1 op src ltrue lfalse ≝ λr:nat → res register.λf:nat → res label. do src' ← make_regs r src; do ltrue' ← f ltrue; do lfalse' ← f lfalse;  OK ? (St_cond1 op src' ltrue' lfalse').
139let rec make_St_cond2 op src1 src2 ltrue lfalse ≝ λr:nat → res register.λf:nat → res label. do src1' ← make_regs r src1; do src2' ← make_regs r src2; do ltrue' ← f ltrue; do lfalse' ← f lfalse; OK ? (St_cond2 op src1' src2' ltrue' lfalse').
140let rec make_St_jumptable rs ls ≝ λr:nat → res register.λf:nat → res label. do rs' ← make_regs r rs; do ls' ← foldr ?? (λl,ls0. do ls ← ls0; do l' ← f l; OK ? (l'::ls)) (OK ? [ ]) ls; OK ? (St_jumptable rs' ls').
141let rec make_St_return src ≝ λr:nat → res register.λf:nat → res label. do src' ← make_regs r src; OK statement (St_return src').
142
Note: See TracBrowser for help on using the repository browser.