extracted/semantics.ml

   1 open Preamble
   2
   3 open UtilBranch
   4
   5 open ASMCostsSplit
   6
   7 open StructuredTraces
   8
   9 open AbstractStatus
  10
  11 open StatusProofs
  12
  13 open Interpret
  14
  15 open ASMCosts
  16
  17 open Assembly
  18
  19 open Status
  20
  21 open Fetch
  22
  23 open PolicyFront
  24
  25 open PolicyStep
  26
  27 open Policy
  28
  29 open AssocList
  30
  31 open Uses
  32
  33 open ASM
  34
  35 open BitVectorTrieSet
  36
  37 open LINToASM
  38
  39 open LIN
  40
  41 open Linearise
  42
  43 open LTLToLIN
  44
  45 open Fixpoints
  46
  47 open Set_adt
  48
  49 open Liveness
  50
  51 open Interference
  52
  53 open Joint_LTL_LIN
  54
  55 open LTL
  56
  57 open ERTLToLTL
  58
  59 open ERTL
  60
  61 open RegisterSet
  62
  63 open RTLToERTL
  64
  65 open State
  66
  67 open Bind_new
  68
  69 open BindLists
  70
  71 open Blocks
  72
  73 open TranslateUtils
  74
  75 open String
  76
  77 open LabelledObjects
  78
  79 open I8051
  80
  81 open BackEndOps
  82
  83 open Joint
  84
  85 open RTL
  86
  87 open RTLabsToRTL
  88
  89 open CostInj
  90
  91 open Deqsets_extra
  92
  93 open CostMisc
  94
  95 open Listb_extra
  96
  97 open CostSpec
  98
  99 open CostCheck
 100
 101 open BitVectorTrie
 102
 103 open Graphs
 104
 105 open Order
 106
 107 open Registers
 108
 109 open RTLabs_syntax
 110
 111 open ToRTLabs
 112
 113 open FrontEndOps
 114
 115 open Cminor_syntax
 116
 117 open ToCminor
 118
 119 open MemProperties
 120
 121 open MemoryInjections
 122
 123 open Fresh
 124
 125 open SwitchRemoval
 126
 127 open Sets
 128
 129 open Listb
 130
 131 open Star
 132
 133 open Frontend_misc
 134
 135 open CexecInd
 136
 137 open Casts
 138
 139 open ClassifyOp
 140
 141 open Smallstep
 142
 143 open Extra_bool
 144
 145 open FrontEndVal
 146
 147 open Hide
 148
 149 open ByteValues
 150
 151 open GenMem
 152
 153 open FrontEndMem
 154
 155 open Globalenvs
 156
 157 open Csem
 158
 159 open SmallstepExec
 160
 161 open Division
 162
 163 open Z
 164
 165 open BitVectorZ
 166
 167 open Pointers
 168
 169 open Values
 170
 171 open Events
 172
 173 open IOMonad
 174
 175 open IO
 176
 177 open Cexec
 178
 179 open TypeComparison
 180
 181 open SimplifyCasts
 182
 183 open CostLabel
 184
 185 open Coqlib
 186
 187 open Proper
 188
 189 open PositiveMap
 190
 191 open Deqsets
 192
 193 open ErrorMessages
 194
 195 open PreIdentifiers
 196
 197 open Errors
 198
 199 open Extralib
 200
 201 open Lists
 202
 203 open Positive
 204
 205 open Identifiers
 206
 207 open Exp
 208
 209 open Arithmetic
 210
 211 open Vector
 212
 213 open Div_and_mod
 214
 215 open Util
 216
 217 open FoldStuff
 218
 219 open BitVector
 220
 221 open Jmeq
 222
 223 open Russell
 224
 225 open List
 226
 227 open Setoids
 228
 229 open Monad
 230
 231 open Option
 232
 233 open Extranat
 234
 235 open Bool
 236
 237 open Relations
 238
 239 open Nat
 240
 241 open Integers
 242
 243 open Hints_declaration
 244
 245 open Core_notation
 246
 247 open Pts
 248
 249 open Logic
 250
 251 open Types
 252
 253 open AST
 254
 255 open Csyntax
 256
 257 open Label
 258
 259 open Compiler
 260
 261 open Stacksize
 262
 263 open Executions
 264
 265 open Measurable
 266
 267 open Clight_abstract
 268
 269 open Clight_classified_system
 270
 271 open Cminor_semantics
 272
 273 open Cminor_abstract
 274
 275 open Cminor_classified_system
 276
 277 open RTLabs_semantics
 278
 279 open RTLabs_abstract
 280
 281 open RTLabs_classified_system
 282
 283 open ExtraMonads
 284
 285 open ExtraGlobalenvs
 286
 287 open I8051bis
 288
 289 open BEMem
 290
 291 open Joint_semantics
 292
 293 open SemanticsUtils
 294
 295 open Traces
 296
 297 open Joint_fullexec
 298
 299 open RTL_semantics
 300
 301 open ERTL_semantics
 302
 303 open Joint_LTL_LIN_semantics
 304
 305 open LTL_semantics
 306
 307 open LIN_semantics
 308
 309 open Interpret2
 310
 311 type preclassified_system_pass =
 312   Measurable.preclassified_system
 313   (* singleton inductive, whose constructor was mk_preclassified_system_pass *)
 314
 315 (** val preclassified_system_pass_rect_Type4 :
 316     Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
 317     preclassified_system_pass -> 'a1 **)
 318 let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_25220 =
 319   let pcs_pcs = x_25220 in h_mk_preclassified_system_pass pcs_pcs __
 320
 321 (** val preclassified_system_pass_rect_Type5 :
 322     Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
 323     preclassified_system_pass -> 'a1 **)
 324 let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_25222 =
 325   let pcs_pcs = x_25222 in h_mk_preclassified_system_pass pcs_pcs __
 326
 327 (** val preclassified_system_pass_rect_Type3 :
 328     Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
 329     preclassified_system_pass -> 'a1 **)
 330 let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_25224 =
 331   let pcs_pcs = x_25224 in h_mk_preclassified_system_pass pcs_pcs __
 332
 333 (** val preclassified_system_pass_rect_Type2 :
 334     Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
 335     preclassified_system_pass -> 'a1 **)
 336 let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_25226 =
 337   let pcs_pcs = x_25226 in h_mk_preclassified_system_pass pcs_pcs __
 338
 339 (** val preclassified_system_pass_rect_Type1 :
 340     Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
 341     preclassified_system_pass -> 'a1 **)
 342 let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_25228 =
 343   let pcs_pcs = x_25228 in h_mk_preclassified_system_pass pcs_pcs __
 344
 345 (** val preclassified_system_pass_rect_Type0 :
 346     Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
 347     preclassified_system_pass -> 'a1 **)
 348 let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_25230 =
 349   let pcs_pcs = x_25230 in h_mk_preclassified_system_pass pcs_pcs __
 350
 351 (** val pcs_pcs :
 352     Compiler.pass -> preclassified_system_pass ->
 353     Measurable.preclassified_system **)
 354 let rec pcs_pcs p xxx =
 355   let yyy = xxx in yyy
 356
 357 (** val preclassified_system_pass_inv_rect_Type4 :
 358     Compiler.pass -> preclassified_system_pass ->
 359     (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
 360 let preclassified_system_pass_inv_rect_Type4 x1 hterm h1 =
 361   let hcut = preclassified_system_pass_rect_Type4 x1 h1 hterm in hcut __
 362
 363 (** val preclassified_system_pass_inv_rect_Type3 :
 364     Compiler.pass -> preclassified_system_pass ->
 365     (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
 366 let preclassified_system_pass_inv_rect_Type3 x1 hterm h1 =
 367   let hcut = preclassified_system_pass_rect_Type3 x1 h1 hterm in hcut __
 368
 369 (** val preclassified_system_pass_inv_rect_Type2 :
 370     Compiler.pass -> preclassified_system_pass ->
 371     (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
 372 let preclassified_system_pass_inv_rect_Type2 x1 hterm h1 =
 373   let hcut = preclassified_system_pass_rect_Type2 x1 h1 hterm in hcut __
 374
 375 (** val preclassified_system_pass_inv_rect_Type1 :
 376     Compiler.pass -> preclassified_system_pass ->
 377     (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
 378 let preclassified_system_pass_inv_rect_Type1 x1 hterm h1 =
 379   let hcut = preclassified_system_pass_rect_Type1 x1 h1 hterm in hcut __
 380
 381 (** val preclassified_system_pass_inv_rect_Type0 :
 382     Compiler.pass -> preclassified_system_pass ->
 383     (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
 384 let preclassified_system_pass_inv_rect_Type0 x1 hterm h1 =
 385   let hcut = preclassified_system_pass_rect_Type0 x1 h1 hterm in hcut __
 386
 387 (** val pcs_pcs__o__pcs_exec :
 388     Compiler.pass -> preclassified_system_pass -> (IO.io_out, IO.io_in)
 389     SmallstepExec.fullexec **)
 390 let pcs_pcs__o__pcs_exec x0 x1 =
 391   (pcs_pcs x0 x1).Measurable.pcs_exec
 392
 393 (** val pcs_pcs__o__pcs_exec__o__es1 :
 394     Compiler.pass -> preclassified_system_pass -> (IO.io_out, IO.io_in)
 395     SmallstepExec.trans_system **)
 396 let pcs_pcs__o__pcs_exec__o__es1 x0 x1 =
 397   Measurable.pcs_exec__o__es1 (pcs_pcs x0 x1)
 398
 399 (** val preclassified_system_of_pass :
 400     Compiler.pass -> Compiler.syntax_of_pass -> preclassified_system_pass **)
 401 let preclassified_system_of_pass = function
 402 | Compiler.Clight_pass -> (fun x -> Clight_classified_system.clight_pcs)
 403 | Compiler.Clight_switch_removed_pass ->
 404   (fun x -> Clight_classified_system.clight_pcs)
 405 | Compiler.Clight_label_pass ->
 406   (fun x -> Clight_classified_system.clight_pcs)
 407 | Compiler.Clight_simplified_pass ->
 408   (fun x -> Clight_classified_system.clight_pcs)
 409 | Compiler.Cminor_pass -> (fun x -> Cminor_classified_system.cminor_pcs)
 410 | Compiler.Rtlabs_pass -> (fun x -> RTLabs_classified_system.rTLabs_pcs)
 411 | Compiler.Rtl_separate_pass ->
 412   (fun x ->
 413     Joint_fullexec.joint_preclassified_system
 414       (SemanticsUtils.sem_graph_params_to_sem_params
 415         RTL_semantics.rTL_semantics_separate))
 416 | Compiler.Rtl_uniq_pass ->
 417   (fun x ->
 418     Joint_fullexec.joint_preclassified_system
 419       (SemanticsUtils.sem_graph_params_to_sem_params
 420         RTL_semantics.rTL_semantics_unique))
 421 | Compiler.Ertl_pass ->
 422   (fun x ->
 423     Joint_fullexec.joint_preclassified_system
 424       (SemanticsUtils.sem_graph_params_to_sem_params
 425         ERTL_semantics.eRTL_semantics))
 426 | Compiler.Ltl_pass ->
 427   (fun x ->
 428     Joint_fullexec.joint_preclassified_system
 429       (SemanticsUtils.sem_graph_params_to_sem_params
 430         LTL_semantics.lTL_semantics))
 431 | Compiler.Lin_pass ->
 432   (fun x ->
 433     Joint_fullexec.joint_preclassified_system LIN_semantics.lIN_semantics)
 434 | Compiler.Assembly_pass ->
 435   (fun prog ->
 436     let { Types.fst = eta32049; Types.snd = policy } = Obj.magic prog in
 437     let { Types.fst = code; Types.snd = sigma } = eta32049 in
 438     Interpret2.aSM_preclassified_system code sigma policy)
 439 | Compiler.Object_code_pass ->
 440   (fun prog -> Interpret2.oC_preclassified_system (Obj.magic prog))
 441
 442 (** val run_and_print :
 443     Compiler.pass -> Compiler.syntax_of_pass -> Nat.nat -> (Compiler.pass ->
 444     Types.unit0) -> (StructuredTraces.intensional_event -> Types.unit0) ->
 445     (Errors.errmsg -> Types.unit0) -> (Integers.int -> Types.unit0) ->
 446     Types.unit0 **)
 447 let run_and_print pass prog n print_pass print_event print_error print_exit =
 448   let res =
 449     let pcs = preclassified_system_of_pass pass prog in
 450     let prog0 = prog in
 451     let g = (pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_global prog0
 452     in
 453     Monad.m_bind0 (Monad.max_def Errors.res0)
 454       (Obj.magic
 455         ((pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_initial_state
 456           prog0)) (fun s0 ->
 457       let i = print_pass pass in
 458       let { Types.fst = trace; Types.snd = res } =
 459         Measurable.observe_all_in_measurable n
 460           (Measurable.pcs_to_cs (pcs_pcs pass pcs)
 461             ((pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_global prog0))
 462           print_event List.Nil s0
 463       in
 464       Obj.magic res)
 465   in
 466   (match Obj.magic res with
 467    | Errors.OK n0 -> print_exit n0
 468    | Errors.Error msg -> print_error msg)
 469