1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(GD_GPL)
9 *)
10
11chapter "Specifications"
12
13(*
14 * List of rules to make various images.
15 *
16 * Some rules have duplicate targets of the form:
17 *
18 *    theories [condition = "MOO", quick_and_dirty]
19 *       "foo"
20 *    theories
21 *       "foo"
22 *
23 * The idea is that if the environment variable "MOO" is defined we
24 * execute the first rule (doing the proof in quick-and-dirty mode), and
25 * then find we need not take any action for the second. Otherwise, we
26 * skip the first rule and only perform the second.
27 *)
28
29(*
30 * Abstract Specification
31 *)
32
33(* Session on which most other sessions build. *)
34session ASpec in "abstract" = Word_Lib +
35  options [document=false]
36  sessions
37    "HOL-Library"
38    Lib
39    ExecSpec
40  theories
41    "Syscall_A"
42
43(* We build the abstract specification document in a separate session,
44   to avoid rebuilding ASpec (and every session that depends on it)
45   whenever the git commit ID changes. *)
46session ASpecDoc in "abstract" = Word_Lib +
47  options [document=pdf]
48  sessions
49    "HOL-Library"
50    Lib
51    ExecSpec
52  theories
53    "Intro_Doc"
54  theories
55    "Syscall_A"
56    "Glossary_Doc"
57    (* "KernelInit_A" *)
58  document_files
59    "VERSION"    (* generated by `make ASpec` *)
60    "gitrev.tex" (* generated by `make ASpec` *)
61    "root.tex"
62    "root.bib"
63    "defs.bib"
64    "ulem.sty"
65    "imgs/CDT.pdf"
66    "imgs/seL4-background_01.pdf"
67    "imgs/seL4-background_03.pdf"
68    "imgs/seL4-background_04.pdf"
69    "imgs/sel4objects_01.pdf"
70    "imgs/sel4objects_05.pdf"
71    "imgs/sel4_internals_01.pdf"
72  document_files (in "document/$L4V_ARCH")
73    "ARCH.tex"
74
75(*
76 * Executable/Design Specification
77 *)
78
79session ExecSpec = Word_Lib +
80  options [document = false]
81  sessions
82    Lib
83    "HOL-Eisbach"
84  theories
85    "design/API_H"
86    "design/$L4V_ARCH/ArchIntermediate_H"
87
88
89(*
90 * C Kernel
91 *)
92
93session CSpec = CKernel +
94  theories [condition = "SORRY_MODIFIES_PROOFS", quick_and_dirty]
95    "cspec/Substitute"
96  theories [condition = "SORRY_BITFIELD_PROOFS", quick_and_dirty]
97    "cspec/KernelInc_C"
98  theories
99    "cspec/KernelInc_C"
100    "cspec/KernelState_C"
101
102session CKernel = CParser +
103  sessions
104    "ExecSpec"
105    "CLib"
106    "AsmRefine"
107  theories [condition = "SORRY_MODIFIES_PROOFS", quick_and_dirty]
108    "cspec/$L4V_ARCH/Kernel_C"
109  theories
110    "cspec/$L4V_ARCH/Kernel_C"
111
112
113(*
114 * CapDL
115 *)
116
117session DSpec in capDL = Word_Lib +
118  sessions
119    ExecSpec
120    ASpec
121  theories
122    Syscall_D
123
124
125(*
126 * Take-Grant.
127 *)
128
129session TakeGrant in "take-grant" = Word_Lib +
130  theories
131    "System_S"
132    "Isolation_S"
133    "Example"
134    "Example2"
135
136
137(*
138 * Separation Kernel Setup Specification
139 *)
140
141session ASepSpec = ASpec +
142  options [document = false]
143  theories
144    "sep-abstract/Syscall_SA"
145
146