extracted/compiler.mli

   1 open Preamble
   2
   3 open CostLabel
   4
   5 open Coqlib
   6
   7 open Proper
   8
   9 open PositiveMap
  10
  11 open Deqsets
  12
  13 open ErrorMessages
  14
  15 open PreIdentifiers
  16
  17 open Errors
  18
  19 open Extralib
  20
  21 open Lists
  22
  23 open Positive
  24
  25 open Identifiers
  26
  27 open Exp
  28
  29 open Arithmetic
  30
  31 open Vector
  32
  33 open Div_and_mod
  34
  35 open Util
  36
  37 open FoldStuff
  38
  39 open BitVector
  40
  41 open Jmeq
  42
  43 open Russell
  44
  45 open List
  46
  47 open Setoids
  48
  49 open Monad
  50
  51 open Option
  52
  53 open Extranat
  54
  55 open Bool
  56
  57 open Relations
  58
  59 open Nat
  60
  61 open Integers
  62
  63 open Hints_declaration
  64
  65 open Core_notation
  66
  67 open Pts
  68
  69 open Logic
  70
  71 open Types
  72
  73 open AST
  74
  75 open Csyntax
  76
  77 open Label
  78
  79 open Sets
  80
  81 open Listb
  82
  83 open Star
  84
  85 open Frontend_misc
  86
  87 open CexecInd
  88
  89 open Casts
  90
  91 open ClassifyOp
  92
  93 open Smallstep
  94
  95 open Extra_bool
  96
  97 open FrontEndVal
  98
  99 open Hide
 100
 101 open ByteValues
 102
 103 open GenMem
 104
 105 open FrontEndMem
 106
 107 open Globalenvs
 108
 109 open Csem
 110
 111 open SmallstepExec
 112
 113 open Division
 114
 115 open Z
 116
 117 open BitVectorZ
 118
 119 open Pointers
 120
 121 open Values
 122
 123 open Events
 124
 125 open IOMonad
 126
 127 open IO
 128
 129 open Cexec
 130
 131 open TypeComparison
 132
 133 open SimplifyCasts
 134
 135 open MemProperties
 136
 137 open MemoryInjections
 138
 139 open Fresh
 140
 141 open SwitchRemoval
 142
 143 open FrontEndOps
 144
 145 open Cminor_syntax
 146
 147 open ToCminor
 148
 149 open BitVectorTrie
 150
 151 open Graphs
 152
 153 open Order
 154
 155 open Registers
 156
 157 open RTLabs_syntax
 158
 159 open ToRTLabs
 160
 161 open Deqsets_extra
 162
 163 open CostMisc
 164
 165 open Listb_extra
 166
 167 open CostSpec
 168
 169 open CostCheck
 170
 171 open CostInj
 172
 173 open State
 174
 175 open Bind_new
 176
 177 open BindLists
 178
 179 open Blocks
 180
 181 open TranslateUtils
 182
 183 open String
 184
 185 open LabelledObjects
 186
 187 open I8051
 188
 189 open BackEndOps
 190
 191 open Joint
 192
 193 open RTL
 194
 195 open RTLabsToRTL
 196
 197 open ERTL
 198
 199 open RegisterSet
 200
 201 open RTLToERTL
 202
 203 open Fixpoints
 204
 205 open Set_adt
 206
 207 open Liveness
 208
 209 open Interference
 210
 211 open Joint_LTL_LIN
 212
 213 open LTL
 214
 215 open ERTLToLTL
 216
 217 open LIN
 218
 219 open Linearise
 220
 221 open LTLToLIN
 222
 223 open ASM
 224
 225 open BitVectorTrieSet
 226
 227 open LINToASM
 228
 229 type pass =
 230 | Clight_pass
 231 | Clight_switch_removed_pass
 232 | Clight_label_pass
 233 | Clight_simplified_pass
 234 | Cminor_pass
 235 | Rtlabs_pass
 236 | Rtl_separate_pass
 237 | Rtl_uniq_pass
 238 | Ertl_pass
 239 | Ltl_pass
 240 | Lin_pass
 241 | Assembly_pass
 242 | Object_code_pass
 243
 244 val pass_rect_Type4 :
 245   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 246   -> 'a1 -> 'a1 -> pass -> 'a1
 247
 248 val pass_rect_Type5 :
 249   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 250   -> 'a1 -> 'a1 -> pass -> 'a1
 251
 252 val pass_rect_Type3 :
 253   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 254   -> 'a1 -> 'a1 -> pass -> 'a1
 255
 256 val pass_rect_Type2 :
 257   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 258   -> 'a1 -> 'a1 -> pass -> 'a1
 259
 260 val pass_rect_Type1 :
 261   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 262   -> 'a1 -> 'a1 -> pass -> 'a1
 263
 264 val pass_rect_Type0 :
 265   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
 266   -> 'a1 -> 'a1 -> pass -> 'a1
 267
 268 val pass_inv_rect_Type4 :
 269   pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 270   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 271   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 272
 273 val pass_inv_rect_Type3 :
 274   pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 275   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 276   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 277
 278 val pass_inv_rect_Type2 :
 279   pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 280   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 281   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 282
 283 val pass_inv_rect_Type1 :
 284   pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 285   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 286   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 287
 288 val pass_inv_rect_Type0 :
 289   pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 290   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
 291   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 292
 293 val pass_discr : pass -> pass -> __
 294
 295 val pass_jmdiscr : pass -> pass -> __
 296
 297 type 'x with_stack_model = ('x, AST.ident -> Nat.nat Types.option) Types.prod
 298
 299 type syntax_of_pass = __
 300
 301 type observe_pass = pass -> syntax_of_pass -> Types.unit0
 302
 303 val front_end :
 304   observe_pass -> Csyntax.clight_program -> ((CostLabel.costlabel,
 305   Csyntax.clight_program) Types.prod, RTLabs_syntax.rTLabs_program)
 306   Types.prod Errors.res
 307
 308 open Uses
 309
 310 val compute_fixpoint : Fixpoints.fixpoint_computer
 311
 312 val colour_graph : Interference.coloured_graph_computer
 313
 314 open AssocList
 315
 316 val lookup_stack_cost :
 317   Joint.params -> Joint.joint_program -> PreIdentifiers.identifier -> Nat.nat
 318   Types.option
 319
 320 val back_end :
 321   observe_pass -> CostLabel.costlabel -> RTLabs_syntax.rTLabs_program ->
 322   (((ASM.pseudo_assembly_program, CostLabel.costlabel) Types.prod,
 323   Joint.stack_cost_model) Types.prod, Nat.nat) Types.prod Errors.res
 324
 325 open Status
 326
 327 open Fetch
 328
 329 open Assembly
 330
 331 open PolicyFront
 332
 333 open PolicyStep
 334
 335 open Policy
 336
 337 val assembler :
 338   observe_pass -> ASM.pseudo_assembly_program -> ASM.labelled_object_code
 339   Errors.res
 340
 341 open StructuredTraces
 342
 343 open AbstractStatus
 344
 345 open StatusProofs
 346
 347 open Interpret
 348
 349 open ASMCosts
 350
 351 val lift_out_of_sigma :
 352   'a2 -> ('a1 -> (__, __) Types.sum) -> ('a1 Types.sig0 -> 'a2) -> 'a1 -> 'a2
 353
 354 val lift_cost_map_back_to_front :
 355   ASM.labelled_object_code -> StructuredTraces.as_cost_map ->
 356   Label.clight_cost_map
 357
 358 open UtilBranch
 359
 360 open ASMCostsSplit
 361
 362 type compiler_output = { c_labelled_object_code : ASM.labelled_object_code;
 363                          c_stack_cost : Joint.stack_cost_model;
 364                          c_max_stack : Nat.nat;
 365                          c_init_costlabel : CostLabel.costlabel;
 366                          c_labelled_clight : Csyntax.clight_program;
 367                          c_clight_cost_map : Label.clight_cost_map }
 368
 369 val compiler_output_rect_Type4 :
 370   (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
 371   CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
 372   'a1) -> compiler_output -> 'a1
 373
 374 val compiler_output_rect_Type5 :
 375   (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
 376   CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
 377   'a1) -> compiler_output -> 'a1
 378
 379 val compiler_output_rect_Type3 :
 380   (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
 381   CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
 382   'a1) -> compiler_output -> 'a1
 383
 384 val compiler_output_rect_Type2 :
 385   (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
 386   CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
 387   'a1) -> compiler_output -> 'a1
 388
 389 val compiler_output_rect_Type1 :
 390   (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
 391   CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
 392   'a1) -> compiler_output -> 'a1
 393
 394 val compiler_output_rect_Type0 :
 395   (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
 396   CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
 397   'a1) -> compiler_output -> 'a1
 398
 399 val c_labelled_object_code : compiler_output -> ASM.labelled_object_code
 400
 401 val c_stack_cost : compiler_output -> Joint.stack_cost_model
 402
 403 val c_max_stack : compiler_output -> Nat.nat
 404
 405 val c_init_costlabel : compiler_output -> CostLabel.costlabel
 406
 407 val c_labelled_clight : compiler_output -> Csyntax.clight_program
 408
 409 val c_clight_cost_map : compiler_output -> Label.clight_cost_map
 410
 411 val compiler_output_inv_rect_Type4 :
 412   compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
 413   Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
 414   Label.clight_cost_map -> __ -> 'a1) -> 'a1
 415
 416 val compiler_output_inv_rect_Type3 :
 417   compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
 418   Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
 419   Label.clight_cost_map -> __ -> 'a1) -> 'a1
 420
 421 val compiler_output_inv_rect_Type2 :
 422   compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
 423   Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
 424   Label.clight_cost_map -> __ -> 'a1) -> 'a1
 425
 426 val compiler_output_inv_rect_Type1 :
 427   compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
 428   Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
 429   Label.clight_cost_map -> __ -> 'a1) -> 'a1
 430
 431 val compiler_output_inv_rect_Type0 :
 432   compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
 433   Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
 434   Label.clight_cost_map -> __ -> 'a1) -> 'a1
 435
 436 val compiler_output_jmdiscr : compiler_output -> compiler_output -> __
 437
 438 val compile :
 439   observe_pass -> Csyntax.clight_program -> compiler_output Errors.res
 440