source: src/RTLabs/CostSpec.ma @ 2774

Last change on this file since 2774 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: 3.2 KB
Line 
1
2include "RTLabs/RTLabs_syntax.ma".
3
4(* We define a boolean cost label function on statements as well as a cost
5   label extraction function because we can use it in hypotheses without naming
6   the label. *)
7   
8definition is_cost_label : statement → bool ≝
9λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ].
10
11definition cost_label_of : statement → option costlabel ≝
12λs. match s with [ St_cost s _ ⇒ Some ? s | _ ⇒ None ? ].
13
14(* We require that labels appear after branch instructions and at the start of
15   functions.  The first is required for preciseness, the latter for soundness.
16   We will make a separate requirement for there to be a finite number of steps
17   between labels to catch loops for soundness (is this sufficient?). *)
18
19definition well_cost_labelled_statement : ∀g:graph statement. ∀s. labels_present g s → bool ≝
20λg,s. match s return λs. labels_present g s → bool with
21[ St_cond _ l1 l2 ⇒ λH.
22    is_cost_label (lookup_present … g l1 ?) ∧
23    is_cost_label (lookup_present … g l2 ?)
24(*| St_jumptable _ ls ⇒ λH.
25    (* I did have a dependent version of All here, but it's a pain. *)
26    All … (λl. ∃H. is_cost_label (lookup_present … g l H) = true) ls*)
27| _ ⇒ λ_. true
28]. whd in H;
29[ @(proj1 … H)
30| @(proj2 … H)
31] qed.
32
33definition well_cost_labelled_fn : internal_function → Prop ≝
34λf. (∀l,PR. well_cost_labelled_statement (f_graph f) (lookup_present … (f_graph f) l PR) (f_closed f l …)) ∧
35    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true.
36[ @lookup_lookup_present | cases (f_entry f) // ] qed.
37
38(* Define a notion of sound labellings of RTLabs programs. *)
39
40let rec successors (s : statement) : list label ≝
41match s with
42[ St_skip l ⇒ [l]
43| St_cost _ l ⇒ [l]
44| St_const _ _ _ l ⇒ [l]
45| St_op1 _ _ _ _ _ l ⇒ [l]
46| St_op2 _ _ _ _ _ _ _ l ⇒ [l]
47| St_load _ _ _ l ⇒ [l]
48| St_store _ _ _ l ⇒ [l]
49| St_call_id _ _ _ l ⇒ [l]
50| St_call_ptr _ _ _ l ⇒ [l]
51(*
52| St_tailcall_id _ _ ⇒ [ ]
53| St_tailcall_ptr _ _ ⇒ [ ]
54*)
55| St_cond _ l1 l2 ⇒ [l1; l2]
56(*| St_jumptable _ ls ⇒ ls*)
57| St_return ⇒ [ ]
58].
59
60(* To show that the labelling is sound we need a bound on the number of
61   instructions in the current function until the next cost label. *)
62
63inductive bound_on_instrs_to_cost (g:graph statement) : label → nat → Prop ≝
64| boitc_step : ∀l,n,H.
65    let stmt ≝ lookup_present … g l H in
66    (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
67          bound_on_instrs_to_cost' g l' n) →
68    bound_on_instrs_to_cost g l (S n)
69with bound_on_instrs_to_cost' : label → nat → Prop ≝
70| boitc_here : ∀l,n,H.
71    is_cost_label (lookup_present … g l H) →
72    bound_on_instrs_to_cost' g l n
73| boitc_later : ∀l,n,H.
74    ¬ is_cost_label (lookup_present … g l H) →
75    bound_on_instrs_to_cost g l n →
76    bound_on_instrs_to_cost' g l n.
77
78definition soundly_labelled_fn : internal_function → Prop ≝
79λf. ∀l. present … (f_graph f) l → ∃n. bound_on_instrs_to_cost (f_graph f) l n.
80
81definition well_cost_labelled_program : RTLabs_program → Prop ≝
82  λp. All ? (λx. match \snd x with [ Internal fn ⇒
83    well_cost_labelled_fn fn ∧ soundly_labelled_fn fn
84  | _ ⇒ True]) (prog_funct … p).
85
86
Note: See TracBrowser for help on using the repository browser.