source: src/RTLabs/import.ma @ 3022

Last change on this file since 3022 was 2645, checked in by sacerdot, 7 years ago
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File size: 10.1 KB
Line 
1
2include "RTLabs/RTLabs_semantics.ma".
3
4let rec n_idents (n:nat) (tag:identifierTag) (g:universe tag) : Vector (identifier tag) n × (universe tag) ≝
5match n with
6[ O ⇒ 〈[[ ]], g〉
7| S m ⇒ let 〈ls, g'〉 ≝ n_idents m tag g in
8        let 〈l, g''〉 ≝ fresh ? g' in
9        〈l:::ls, g''〉
10].
11
12definition pre_register ≝ nat.
13
14record pre_internal_function : Type[0] ≝
15{ pf_result    : option (pre_register × typ)
16; pf_params    : list (pre_register × typ)
17; pf_locals    : list (pre_register × typ)
18; pf_stacksize : nat
19; pf_graph     : list (nat × ((pre_register → res (register×typ)) → (nat → res label) → res statement))
20; pf_entry     : nat
21; pf_exit      : nat
22}.
23
24definition make_register :
25  (pre_register → option (register×typ)) → pre_register → typ → universe RegisterTag →
26  (nat → option (register×typ)) × (universe RegisterTag) × register ≝
27λm,reg,ty,g.
28  match m reg with
29  [ Some r' ⇒ 〈〈m,g〉,\fst r'〉
30  | None ⇒ let 〈r',g'〉 ≝ fresh ? g in
31             〈〈λn. if eqb reg n then Some ? 〈r',ty〉 else m n,g'〉,r'〉
32  ]
33.
34
35definition make_registers_list :
36  (nat → option (register×typ)) → list (pre_register × typ) → universe RegisterTag →
37    (nat → option (register×typ)) × (universe RegisterTag) × (list (register×typ)) ≝
38λm,lrs,g.
39foldr ?? (λrst,acc. let 〈acc',l〉 ≝ acc in
40                    let 〈rs,ty〉 ≝ rst in
41                    let 〈m,g〉 ≝ acc' in
42                    let 〈mg,rs'〉 ≝ make_register m rs ty g in
43                      〈mg,〈rs',ty〉::l〉) 〈〈m,g〉,[ ]〉 lrs.
44
45(* Doesn't check for identifier overflow, but don't really need to care here. *)
46definition make_internal_function : pre_internal_function → res (fundef internal_function) ≝
47λpre_f.
48  let rgen0 ≝ new_universe RegisterTag in
49  let 〈rmapgen1, result〉 ≝ match pf_result pre_f with
50                           [ None ⇒ 〈〈λ_.None ?, rgen0〉, None ?〉
51                           | Some rt ⇒ let 〈x,y〉 ≝ make_register (λ_.None ?) (\fst rt) (\snd rt) rgen0 in 〈x,Some ? 〈y,\snd rt〉〉
52                           ] in
53  let 〈rmap1, rgen1〉 ≝ rmapgen1 in
54  let 〈rmapgen2, params〉 ≝ make_registers_list rmap1 (pf_params pre_f) rgen1 in
55  let 〈rmap2, rgen2〉 ≝ rmapgen2 in
56  let 〈rmapgen3, locals〉 ≝ make_registers_list rmap2 (pf_locals pre_f) rgen2 in
57  let 〈rmap3, rgen3〉 ≝ rmapgen3 in
58  let rmap ≝ λn. opt_to_res … (msg MissingRegister) (rmap3 n) in
59  let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in
60  let 〈labels, gen〉 ≝ n_idents (S max_stmt) ? (new_universe LabelTag) in
61  let get_label ≝ λn. opt_to_res … (msg MissingLabel) (get_index_weak_v ?? labels n) in
62  do graph ← foldr ?? (λp:nat × ((pre_register → res (register×typ)) → (nat → res label) → res statement).λg0.
63                         do g ← g0;
64                         let 〈l,s〉 ≝ p in
65                         do l' ← get_label l;
66                         do s' ← s rmap get_label;
67                         OK ? (add ?? g l' s')) (OK ? (empty_map ??)) (pf_graph pre_f);
68  do entry ← get_label (pf_entry pre_f);
69  do exit ← get_label (pf_exit pre_f);
70  (* We could figure out that entry and exit are in the graph, but why bother
71     for some testing code? *)
72  match lookup … graph entry return λx. (x ≠ None ? → ?) → ? with
73  [ None ⇒ λ_. Error ? (msg MissingLabel)
74  | Some _ ⇒
75      match lookup … graph exit return λx. (? → x ≠ None ? → ?) → ? with
76      [ None ⇒ λ_. Error ? (msg MissingLabel)
77      | Some _ ⇒ λx. x ??
78      ]
79  ] (λp,q. OK ? (Internal ? (mk_internal_function
80         gen
81         rgen3
82         result
83         params
84         locals
85         (pf_stacksize pre_f)
86         graph
87         ?
88         ?
89         (mk_Sig ?? entry p)
90         (mk_Sig ?? exit q)
91         )))
92   .
93[ 1,2: % #E destruct (E)
94| 3,4: cases daemon
95]
96qed.
97
98definition make_reg_list : (nat → res (register×typ)) → list pre_register → res (list register) ≝
99λm,ps. foldr ?? (λp,rs0. do rs ← rs0; do 〈r,t〉 ← m p; OK ? (r::rs)) (OK ? [ ]) ps.
100
101(* XXX move somewhere sensible *)
102let rec mmap_vec (A:Type[0]) (B:Type[0]) (f:A → res B) (n:nat) (v:Vector A n) on v : res (Vector B n) ≝
103match v with
104[ VEmpty ⇒ OK ? (VEmpty …)
105| VCons m hd tl ⇒ do hd' ← f hd;
106                  do tl' ← mmap_vec A B f m tl;
107                  OK ? (hd':::tl')
108].
109
110definition make_opt_reg : (pre_register → res (register×typ)) → option pre_register → res (option register) ≝
111λm,o. match o with [ None ⇒ OK ? (None ?) | Some r ⇒ do 〈r',t'〉 ← m r; OK ? (Some ? r') ].
112
113inductive pre_op1 : Type[0] ≝
114  | POcastint: intsize → signedness → intsize → pre_op1
115  | POnegint:  pre_op1
116  | POnotbool: pre_op1
117  | POnotint:  pre_op1
118  | POid: pre_op1
119  | POptrofint: pre_op1
120  | POintofptr: pre_op1
121.
122
123(* duplicated from Clight/toCminor.ma. *)
124definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2).
125* * #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
126qed.
127
128definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2).
129* [ #sz1 #sg1 | #r1 | #sz1 ]
130* [ 1,5,9: | *: #a #b #c try #d @(Error ? (msg TypeMismatch)) ]
131[ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ]
132  *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
133| *; #P #p @(region_should_eq r1 ?? p)
134| *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
135] qed.
136
137definition is_bool_src : ∀ty. res (boolsrc ty) ≝
138λty. match ty return λt.res (boolsrc t) with [ ASTint _ _ ⇒ OK ? I | ASTptr _ ⇒ OK ? I | _ ⇒ Error ? (msg TypeMismatch) ].
139
140definition make_op1 : ∀t,t'. pre_op1 → res (unary_operation t' t) ≝
141λt,t',op.
142  match op with
143  [ POcastint sz sg sz' ⇒
144      match t' return λt'. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
145        do o ← typ_should_eq ? t (λt. unary_operation ? t) (Ocastint sz sg sz' sg2);
146               typ_should_eq ? (ASTint sz2 sg2) (λt'. unary_operation t' ?) o
147      | _ ⇒ Error ? (msg TypeMismatch) ]
148  | POnegint ⇒
149      match t' return λt'. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
150        do o ← typ_should_eq ? t (λt. unary_operation ? t) (Onegint sz2 sg2);
151               typ_should_eq ? (ASTint sz2 sg2) (λt'. unary_operation t' ?) o
152      | _ ⇒ Error ? (msg TypeMismatch) ]
153  | POnotbool ⇒
154      match t return λt. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
155        do p ← is_bool_src t';
156               OK ? (Onotbool t' sz2 sg2 p)
157      | _ ⇒ Error ? (msg TypeMismatch) ]
158  | POnotint ⇒
159      match t' return λt'. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
160        do o ← typ_should_eq ? t (λt. unary_operation ? t) (Onotint sz2 sg2);
161               typ_should_eq ? (ASTint sz2 sg2) (λt'. unary_operation t' ?) o
162      | _ ⇒ Error ? (msg TypeMismatch) ]
163  | POid ⇒ typ_should_eq t t' (λt'. unary_operation t' t) (Oid t)
164  | POptrofint ⇒
165      match t' return λt'. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
166      match t return λt. res (unary_operation ? t) with [ ASTptr r1 ⇒
167        OK ? (Optrofint …)
168      | _ ⇒ Error ? (msg TypeMismatch) ]
169      | _ ⇒ Error ? (msg TypeMismatch) ]
170  | POintofptr ⇒
171      match t return λt. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
172      match t' return λt'. res (unary_operation t' ?) with [ ASTptr r1 ⇒
173        OK ? (Ointofptr …)
174      | _ ⇒ Error ? (msg TypeMismatch) ]
175      | _ ⇒ Error ? (msg TypeMismatch) ]
176  ].
177
178let rec make_St_skip l ≝ λr:nat → res (register×typ).λf:nat → res label. do l' ← f l; OK ? (St_skip l').
179let rec make_St_cost cl l ≝ λr:nat → res (register×typ).λf:nat → res label. do l' ← f l; OK ? (St_cost cl l').
180let rec make_St_const rs cst l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈rs',ty'〉 ← r rs; do l' ← f l; OK ? (St_const rs' cst l').
181let rec make_St_op1 op dst src l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈dst',dty〉 ← r dst; do 〈src',sty〉 ← r src; do l' ← f l; do op ← make_op1 dty sty op; OK ? (St_op1 dty sty op dst' src' l').
182let rec make_St_op2 op dst src1 src2 l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈dst',dty〉 ← r dst; do 〈src1',sty1〉 ← r src1; do 〈src2',sty2〉 ← r src2; do l' ← f l; OK ? (St_op2 op dst' src1' src2' l').
183let rec make_St_load chunk addr dst l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈addr',aty〉 ← r addr; do 〈dst',dty〉 ← r dst; do l' ← f l; OK ? (St_load chunk addr' dst' l').
184let rec make_St_store chunk addr src l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈addr',aty〉 ← r addr; do 〈src',sty〉 ← r src; do l' ← f l; OK ? (St_store chunk addr' src' l').
185let rec make_St_call_id id args dst l ≝ λr:nat → res (register×typ).λf:nat → res label. do args' ← make_reg_list r args; do dst' ← make_opt_reg r dst; do l' ← f l; OK ? (St_call_id id args' dst' l').
186let rec make_St_call_ptr frs args dst l ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈frs',fty〉 ← r frs; do args' ← make_reg_list r args; do dst' ← make_opt_reg r dst; do l' ← f l; OK ? (St_call_ptr frs' args' dst' l').
187let rec make_St_tailcall_id id args ≝ λr:nat → res (register×typ).λf:nat → res label.  do args' ← make_reg_list r args; OK statement (St_tailcall_id id args').
188let rec make_St_tailcall_ptr frs args ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈frs',fty〉 ← r frs; do args' ← make_reg_list r args; OK statement (St_tailcall_ptr frs' args').
189let rec make_St_cond src ltrue lfalse ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈src',sty〉 ← r src; do ltrue' ← f ltrue; do lfalse' ← f lfalse;  OK ? (St_cond src' ltrue' lfalse').
190let rec make_St_jumptable rs ls ≝ λr:nat → res (register×typ).λf:nat → res label. do 〈rs',rty〉 ← r rs; do ls' ← foldr ?? (λl,ls0. do ls ← ls0; do l' ← f l; OK ? (l'::ls)) (OK ? [ ]) ls; OK ? (St_jumptable rs' ls').
191definition make_St_return ≝ λr:nat → res (register×typ).λf:nat → res label. OK statement St_return.
192
Note: See TracBrowser for help on using the repository browser.