source: src/RTLabs/import.ma @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 7 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 10.2 KB
Line 
1
2include "RTLabs/RTLabs_semantics.ma".
3
4let rec n_idents (n:nat) (tag:String) (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
45axiom MissingRegister : String.
46axiom MissingLabel : String.
47
48(* Doesn't check for identifier overflow, but don't really need to care here. *)
49definition make_internal_function : pre_internal_function → res (fundef internal_function) ≝
50λpre_f.
51  let rgen0 ≝ new_universe RegisterTag in
52  let 〈rmapgen1, result〉 ≝ match pf_result pre_f with
53                           [ None ⇒ 〈〈λ_.None ?, rgen0〉, None ?〉
54                           | Some rt ⇒ let 〈x,y〉 ≝ make_register (λ_.None ?) (\fst rt) (\snd rt) rgen0 in 〈x,Some ? 〈y,\snd rt〉〉
55                           ] in
56  let 〈rmap1, rgen1〉 ≝ rmapgen1 in
57  let 〈rmapgen2, params〉 ≝ make_registers_list rmap1 (pf_params pre_f) rgen1 in
58  let 〈rmap2, rgen2〉 ≝ rmapgen2 in
59  let 〈rmapgen3, locals〉 ≝ make_registers_list rmap2 (pf_locals pre_f) rgen2 in
60  let 〈rmap3, rgen3〉 ≝ rmapgen3 in
61  let rmap ≝ λn. opt_to_res … (msg MissingRegister) (rmap3 n) in
62  let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in
63  let 〈labels, gen〉 ≝ n_idents (S max_stmt) ? (new_universe LabelTag) in
64  let get_label ≝ λn. opt_to_res … (msg MissingLabel) (get_index_weak_v ?? labels n) in
65  do graph ← foldr ?? (λp:nat × ((pre_register → res (register×typ)) → (nat → res label) → res statement).λg0.
66                         do g ← g0;
67                         let 〈l,s〉 ≝ p in
68                         do l' ← get_label l;
69                         do s' ← s rmap get_label;
70                         OK ? (add ?? g l' s')) (OK ? (empty_map ??)) (pf_graph pre_f);
71  do entry ← get_label (pf_entry pre_f);
72  do exit ← get_label (pf_exit pre_f);
73  (* We could figure out that entry and exit are in the graph, but why bother
74     for some testing code? *)
75  match lookup … graph entry return λx. (x ≠ None ? → ?) → ? with
76  [ None ⇒ λ_. Error ? (msg MissingLabel)
77  | Some _ ⇒
78      match lookup … graph exit return λx. (? → x ≠ None ? → ?) → ? with
79      [ None ⇒ λ_. Error ? (msg MissingLabel)
80      | Some _ ⇒ λx. x ??
81      ]
82  ] (λp,q. OK ? (Internal ? (mk_internal_function
83         gen
84         rgen3
85         result
86         params
87         locals
88         (pf_stacksize pre_f)
89         graph
90         ?
91         ?
92         (mk_Sig ?? entry p)
93         (mk_Sig ?? exit q)
94         )))
95   .
96[ 1,2: % #E destruct (E)
97| 3,4: cases daemon
98]
99qed.
100
101definition make_reg_list : (nat → res (register×typ)) → list pre_register → res (list register) ≝
102λm,ps. foldr ?? (λp,rs0. do rs ← rs0; do 〈r,t〉 ← m p; OK ? (r::rs)) (OK ? [ ]) ps.
103
104(* XXX move somewhere sensible *)
105let 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) ≝
106match v with
107[ VEmpty ⇒ OK ? (VEmpty …)
108| VCons m hd tl ⇒ do hd' ← f hd;
109                  do tl' ← mmap_vec A B f m tl;
110                  OK ? (hd':::tl')
111].
112
113definition make_opt_reg : (pre_register → res (register×typ)) → option pre_register → res (option register) ≝
114λm,o. match o with [ None ⇒ OK ? (None ?) | Some r ⇒ do 〈r',t'〉 ← m r; OK ? (Some ? r') ].
115
116inductive pre_op1 : Type[0] ≝
117  | POcastint: intsize → signedness → intsize → pre_op1
118  | POnegint:  pre_op1
119  | POnotbool: pre_op1
120  | POnotint:  pre_op1
121  | POid: pre_op1
122  | POptrofint: pre_op1
123  | POintofptr: pre_op1
124.
125
126axiom TypeMismatch : String.
127
128(* duplicated from Clight/toCminor.ma. *)
129definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2).
130* * #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
131qed.
132
133definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2).
134* [ #sz1 #sg1 | #r1 | #sz1 ]
135* [ 1,5,9: | *: #a #b #c try #d @(Error ? (msg TypeMismatch)) ]
136[ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ]
137  *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
138| *; #P #p @(region_should_eq r1 ?? p)
139| *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
140] qed.
141
142definition is_bool_src : ∀ty. res (boolsrc ty) ≝
143λty. match ty return λt.res (boolsrc t) with [ ASTint _ _ ⇒ OK ? I | ASTptr _ ⇒ OK ? I | _ ⇒ Error ? (msg TypeMismatch) ].
144
145definition make_op1 : ∀t,t'. pre_op1 → res (unary_operation t' t) ≝
146λt,t',op.
147  match op with
148  [ POcastint sz sg sz' ⇒
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) (Ocastint sz sg sz' sg2);
151               typ_should_eq ? (ASTint sz2 sg2) (λt'. unary_operation t' ?) o
152      | _ ⇒ Error ? (msg TypeMismatch) ]
153  | POnegint ⇒
154      match t' return λt'. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
155        do o ← typ_should_eq ? t (λt. unary_operation ? t) (Onegint sz2 sg2);
156               typ_should_eq ? (ASTint sz2 sg2) (λt'. unary_operation t' ?) o
157      | _ ⇒ Error ? (msg TypeMismatch) ]
158  | POnotbool ⇒
159      match t return λt. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
160        do p ← is_bool_src t';
161               OK ? (Onotbool t' sz2 sg2 p)
162      | _ ⇒ Error ? (msg TypeMismatch) ]
163  | POnotint ⇒
164      match t' return λt'. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
165        do o ← typ_should_eq ? t (λt. unary_operation ? t) (Onotint sz2 sg2);
166               typ_should_eq ? (ASTint sz2 sg2) (λt'. unary_operation t' ?) o
167      | _ ⇒ Error ? (msg TypeMismatch) ]
168  | POid ⇒ typ_should_eq t t' (λt'. unary_operation t' t) (Oid t)
169  | POptrofint ⇒
170      match t' return λt'. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
171      match t return λt. res (unary_operation ? t) with [ ASTptr r1 ⇒
172        OK ? (Optrofint …)
173      | _ ⇒ Error ? (msg TypeMismatch) ]
174      | _ ⇒ Error ? (msg TypeMismatch) ]
175  | POintofptr ⇒
176      match t return λt. res (unary_operation t' t) with [ ASTint sz2 sg2 ⇒
177      match t' return λt'. res (unary_operation t' ?) with [ ASTptr r1 ⇒
178        OK ? (Ointofptr …)
179      | _ ⇒ Error ? (msg TypeMismatch) ]
180      | _ ⇒ Error ? (msg TypeMismatch) ]
181  ].
182
183let rec make_St_skip l ≝ λr:nat → res (register×typ).λf:nat → res label. do l' ← f l; OK ? (St_skip l').
184let rec make_St_cost cl l ≝ λr:nat → res (register×typ).λf:nat → res label. do l' ← f l; OK ? (St_cost cl l').
185let 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').
186let 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').
187let 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').
188let 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').
189let 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').
190let 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').
191let 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').
192let 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').
193let 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').
194let 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').
195let 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').
196definition make_St_return ≝ λr:nat → res (register×typ).λf:nat → res label. OK statement St_return.
197
Note: See TracBrowser for help on using the repository browser.