source: src/Clight/Clight_abstract.ma @ 3367

Last change on this file since 3367 was 2737, checked in by garnier, 7 years ago

Commit of current proof state for Clight to Cminor translation.

File size: 1.7 KB
Line 
1include "Clight/Csem.ma".
2
3(* I previously had a complicated definition that said a labelled Clight state
4   was one with a syntactic form that would emit a cost label in the trace when
5   the next step is evaluated.  This is the wrong notion.
6   
7   We want a labelled Clight state to indicate that we can measure the time of
8   some correspondingly labelled machine code from there.  Only explicit
9   statement level cost labels are useful for this.  Cost labels that appear
10   in the middle of expressions are only useful for allowing the amount of time
11   measured to differ.
12   
13   (Otherwise you see something silly like "x=(y-1) ? c1: 1 : c2: z;" as a
14   labelled state, even though the labels c1 and c2 will appear in the *middle*
15   of the corresponding machine code, and so you measure the wrong thing and
16   can't prove it.)
17 *)
18
19definition Clight_labelled : state → bool ≝
20λs. match s with
21[ State f s k e m ⇒ match s with [ Scost _ _ ⇒ true | _ ⇒ false ]
22| _ ⇒ false
23].
24
25
26(* At the moment this doesn't say anything about "jumps", just calls, returns
27   and everything else. *)
28include "common/StructuredTraces.ma".
29
30definition Clight_classify : state → status_class ≝
31λs. match s with
32[ State _ _ _ _ _ ⇒ cl_other
33| Callstate _ _ _ _ _ ⇒ cl_call
34| Returnstate _ _ _ ⇒ cl_return
35| Finalstate _ ⇒ cl_other
36].
37
38(* Help avoid ambiguous input fun *)
39definition Clight_state ≝ state.
40
41definition cl_genv ≝ genv.
42
43definition cl_env ≝ env.
44
45definition cl_cont ≝ cont.
46
47definition cl_eval_expr ≝ eval_expr.
48
49(* creating aliases constructors for states and continuations *)
50definition ClState ≝ State.
51
52definition ClReturnstate ≝ Returnstate.
53
54definition ClCallstate ≝ Callstate.
55
56definition ClKseq ≝ Kseq.
Note: See TracBrowser for help on using the repository browser.