source: src/Clight/Clight_abstract.ma @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 8 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: 1.5 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
49definition ClState ≝ State.
Note: See TracBrowser for help on using the repository browser.