source: src/RTLabs/RTLabs_syntax.ma @ 3096

Last change on this file since 3096 was 2992, checked in by campbell, 7 years ago

Add "only one return" invariant to RTLabs functions.

File size: 3.7 KB
RevLine 
[639]1include "basics/logic.ma".
2
[747]3include "common/AST.ma".
[720]4include "common/CostLabel.ma".
[702]5include "common/FrontEndOps.ma".
6include "common/Registers.ma".
[639]7
[702]8include "ASM/Vector.ma".
9include "common/Graphs.ma".
[639]10
11inductive statement : Type[0] ≝
12| St_skip : label → statement
13| St_cost : costlabel → label → statement
[1878]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 *)
[1872]17| St_load : typ → register → register → label → statement
18| St_store : typ → register → register → label → statement
[816]19| St_call_id : ident → list register → option register → label → statement
20| St_call_ptr : register → list register → option register → label → statement
[1680]21(* We're not using these just now, and they'd make the Traces.ma proofs more difficult.
[816]22| St_tailcall_id : ident → list register → statement
23| St_tailcall_ptr : register → list register → statement
[1680]24*)
[888]25| St_cond : register → label → label → statement
[765]26| St_return : statement
[639]27.
28
[1626]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
[1878]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'
[2287]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
[2292]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
[1626]42| _ ⇒ True
43].
44
[1316]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
[1878]49| St_const _ _ _ l ⇒ P l
[1369]50| St_op1 _ _ _ _ _ l ⇒ P l
[1872]51| St_op2 _ _ _ _ _ _ _ l ⇒ P l
[1316]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
[1680]56(*
[1316]57| St_tailcall_id _ _ ⇒ True
58| St_tailcall_ptr _ _ ⇒ True
[1680]59*)
[1316]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
[1626]72definition forall_nodes : ∀A.∀P:A → Prop. graph A → Prop ≝
73λA,P,g. ∀l,n. lookup ?? g l = Some ? n → P n.
74
[1316]75definition graph_closed : graph statement → Prop ≝
[1626]76  λg. forall_nodes ? (labels_present g) g.
77definition graph_typed : list (register × typ) → graph statement → Prop ≝
78  λe. forall_nodes ? (statement_typed e).
[1316]79
[639]80record internal_function : Type[0] ≝
[738]81{ f_labgen    : universe LabelTag
82; f_reggen    : universe RegisterTag
[887]83; f_result    : option (register × typ)
84; f_params    : list (register × typ)
85; f_locals    : list (register × typ)
[639]86; f_stacksize : nat
87; f_graph     : graph statement
[1316]88; f_closed    : graph_closed f_graph
[1626]89; f_typed     : graph_typed (f_locals @ f_params) f_graph
[1316]90; f_entry     : Σl:label. present ?? f_graph l
91; f_exit      : Σl:label. present ?? f_graph l
[2992]92; f_only_exit : ∀l. lookup … f_graph l = Some ? St_return → l = f_exit
[639]93}.
94
[2936]95definition RTLabs_program ≝ program (λ_.fundef internal_function) (list init_data).
[639]96
[1675]97
98
99
Note: See TracBrowser for help on using the repository browser.