source: src/RTLabs/RTLabs_syntax.ma @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 5 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: 3.8 KB
Line 
1include "basics/logic.ma".
2
3include "common/AST.ma".
4include "common/CostLabel.ma".
5include "common/FrontEndOps.ma".
6include "common/Registers.ma".
7
8include "ASM/Vector.ma".
9include "common/Graphs.ma".
10
11inductive statement : Type[0] ≝
12| St_skip : label → statement
13| St_cost : costlabel → label → statement
14| St_const : ∀t. register → constant t → label → statement
15| St_op1 : ∀t',t. unary_operation t t' → register → register → label → statement (* destination source *)
16| St_op2 : ∀t',t1,t2. binary_operation t1 t2 t' → register → register → register → label → statement (* destination source1 source2 *)
17| St_load : typ → register → register → label → statement
18| St_store : typ → register → register → label → statement
19| St_call_id : ident → list register → option register → label → statement
20| St_call_ptr : register → list register → option register → label → statement
21(* We're not using these just now, and they'd make the Traces.ma proofs more difficult.
22| St_tailcall_id : ident → list register → statement
23| St_tailcall_ptr : register → list register → statement
24*)
25| St_cond : register → label → label → statement
26| St_return : statement
27.
28
29definition env_has : list (register × typ) → register → typ → Prop ≝
30λl,r,t. Exists ? (λx. 〈r,t〉 = x) l.
31
32definition statement_typed : list (register × typ) → statement → Prop ≝
33λe,s. match s with
34[ St_const t r _ _ ⇒ env_has e r t
35| St_op1 t' t _ r' r _ ⇒ env_has e r' t' ∧ env_has e r t
36| St_op2 t' t1 t2 _ r' r1 r2 _ ⇒ env_has e r1 t1 ∧ env_has e r2 t2 ∧ env_has e r' t'
37| St_load t' addr dst _ ⇒ env_has e dst t' ∧ env_has e addr ASTptr
38| St_store t' addr src _ ⇒ env_has e src t' ∧ env_has e addr ASTptr
39| St_call_id id args dst _ ⇒ All ? (λr. ∃t'.env_has e r t') args ∧ (match dst with [ Some r ⇒ ∃t'.env_has e r t' | _ ⇒ True])
40| St_call_ptr fnptr args dst _ ⇒ env_has e fnptr ASTptr ∧ All ? (λr. ∃t'.env_has e r t') args ∧ (match dst with [ Some r ⇒ ∃t'.env_has e r t' | _ ⇒ True])
41| St_cond r _ _ ⇒ ∃t. env_has e r t
42| _ ⇒ True
43].
44
45definition labels_P : (label → Prop) → statement → Prop ≝
46λP,s. match s with
47[ St_skip l ⇒ P l
48| St_cost _ l ⇒ P l
49| St_const _ _ _ l ⇒ P l
50| St_op1 _ _ _ _ _ l ⇒ P l
51| St_op2 _ _ _ _ _ _ _ l ⇒ P l
52| St_load _ _ _ l ⇒ P l
53| St_store _ _ _ l ⇒ P l
54| St_call_id _ _ _ l ⇒ P l
55| St_call_ptr _ _ _ l ⇒ P l
56(*
57| St_tailcall_id _ _ ⇒ True
58| St_tailcall_ptr _ _ ⇒ True
59*)
60| St_cond _ l1 l2 ⇒ P l1 ∧ P l2
61| St_return ⇒ True
62].
63
64lemma labels_P_mp : ∀P,Q. (∀l. P l → Q l) → ∀s.labels_P P s → labels_P Q s.
65#P #Q #H * /3/
66#r #l #l' * /3/
67qed.
68
69definition labels_present : graph statement → statement → Prop ≝
70λg,s. labels_P (present ?? g) s.
71
72definition forall_nodes : ∀A.∀P:A → Prop. graph A → Prop ≝
73λA,P,g. ∀l,n. lookup ?? g l = Some ? n → P n.
74
75definition graph_closed : graph statement → Prop ≝
76  λg. forall_nodes ? (labels_present g) g.
77definition graph_typed : list (register × typ) → graph statement → Prop ≝
78  λe. forall_nodes ? (statement_typed e).
79
80record internal_function : Type[0] ≝
81{ f_labgen    : universe LabelTag
82; f_reggen    : universe RegisterTag
83; f_result    : option (register × typ)
84; f_params    : list (register × typ)
85; f_locals    : list (register × typ)
86; f_stacksize : nat
87; f_graph     : graph statement
88; f_closed    : graph_closed f_graph
89; f_typed     : graph_typed (f_locals @ f_params) f_graph
90; f_entry     : Σl:label. present ?? f_graph l
91; f_exit      : Σl:label. present ?? f_graph l
92}.
93
94(* Note that the global variables will be initialised by the code in main
95   by this stage, so the only initialisation data is the amount of space to
96   allocate. *)
97
98definition RTLabs_program ≝ program (λ_.fundef internal_function) nat.
99
100
101
102
Note: See TracBrowser for help on using the repository browser.