extracted/cminor_abstract.ml

   1 open Preamble
   2
   3 open FrontEndOps
   4
   5 open Cminor_syntax
   6
   7 open SmallstepExec
   8
   9 open Extra_bool
  10
  11 open Globalenvs
  12
  13 open IOMonad
  14
  15 open IO
  16
  17 open FrontEndVal
  18
  19 open Hide
  20
  21 open ByteValues
  22
  23 open GenMem
  24
  25 open FrontEndMem
  26
  27 open CostLabel
  28
  29 open Proper
  30
  31 open PositiveMap
  32
  33 open Deqsets
  34
  35 open Extralib
  36
  37 open Lists
  38
  39 open Identifiers
  40
  41 open Integers
  42
  43 open AST
  44
  45 open Division
  46
  47 open Exp
  48
  49 open Arithmetic
  50
  51 open Extranat
  52
  53 open Vector
  54
  55 open FoldStuff
  56
  57 open BitVector
  58
  59 open Z
  60
  61 open BitVectorZ
  62
  63 open Pointers
  64
  65 open ErrorMessages
  66
  67 open Option
  68
  69 open Setoids
  70
  71 open Monad
  72
  73 open Positive
  74
  75 open PreIdentifiers
  76
  77 open Errors
  78
  79 open Div_and_mod
  80
  81 open Jmeq
  82
  83 open Russell
  84
  85 open Util
  86
  87 open Bool
  88
  89 open Relations
  90
  91 open Nat
  92
  93 open List
  94
  95 open Hints_declaration
  96
  97 open Core_notation
  98
  99 open Pts
 100
 101 open Logic
 102
 103 open Types
 104
 105 open Coqlib
 106
 107 open Values
 108
 109 open Events
 110
 111 open Cminor_semantics
 112
 113 type cminor_state = Cminor_semantics.state
 114
 115 (** val cminor_labelled : Cminor_semantics.state -> Bool.bool **)
 116 let cminor_labelled = function
 117 | Cminor_semantics.State (x, st, x0, x3, x4, x5, x7) ->
 118   (match st with
 119    | Cminor_syntax.St_skip -> Bool.False
 120    | Cminor_syntax.St_assign (x8, x9, x10) -> Bool.False
 121    | Cminor_syntax.St_store (x8, x9, x10) -> Bool.False
 122    | Cminor_syntax.St_call (x8, x9, x10) -> Bool.False
 123    | Cminor_syntax.St_seq (x8, x9) -> Bool.False
 124    | Cminor_syntax.St_ifthenelse (x8, x9, x10, x11, x12) -> Bool.False
 125    | Cminor_syntax.St_return x8 -> Bool.False
 126    | Cminor_syntax.St_label (x8, x9) -> Bool.False
 127    | Cminor_syntax.St_goto x8 -> Bool.False
 128    | Cminor_syntax.St_cost (x8, x9) -> Bool.True)
 129 | Cminor_semantics.Callstate (x, x0, x1, x2, x3) -> Bool.False
 130 | Cminor_semantics.Returnstate (x, x0, x1) -> Bool.False
 131 | Cminor_semantics.Finalstate x -> Bool.False
 132
 133 open Sets
 134
 135 open Listb
 136
 137 open StructuredTraces
 138
 139 (** val cminor_classify :
 140     Cminor_semantics.state -> StructuredTraces.status_class **)
 141 let cminor_classify = function
 142 | Cminor_semantics.State (x, x0, x1, x4, x5, x6, x8) ->
 143   StructuredTraces.Cl_other
 144 | Cminor_semantics.Callstate (x, x0, x1, x2, x3) -> StructuredTraces.Cl_call
 145 | Cminor_semantics.Returnstate (x, x0, x1) -> StructuredTraces.Cl_return
 146 | Cminor_semantics.Finalstate x -> StructuredTraces.Cl_other
 147
 148 type cm_genv = Cminor_semantics.genv
 149
 150 type cm_env = Cminor_semantics.env
 151
 152 type cm_cont = Cminor_semantics.cont
 153
 154 (** val cm_eval_expr :
 155     Cminor_semantics.genv -> AST.typ -> Cminor_syntax.expr ->
 156     Cminor_semantics.env -> Pointers.block -> GenMem.mem -> (Events.trace,
 157     Values.val0) Types.prod Errors.res **)
 158 let cm_eval_expr ge ty0 e en sp m =
 159   Cminor_semantics.eval_expr ge ty0 e en sp m
 160
 161 (** val cmState :
 162     Cminor_syntax.internal_function -> Cminor_syntax.stmt ->
 163     Cminor_semantics.env -> GenMem.mem -> Pointers.block ->
 164     Cminor_semantics.cont -> Cminor_semantics.stack -> Cminor_semantics.state **)
 165 let cmState f s en m sp k st =
 166   Cminor_semantics.State (f, s, en, m, sp, k, st)
 167
 168 (** val cmReturnstate :
 169     Values.val0 Types.option -> GenMem.mem -> Cminor_semantics.stack ->
 170     Cminor_semantics.state **)
 171 let cmReturnstate x x0 x1 =
 172   Cminor_semantics.Returnstate (x, x0, x1)
 173
 174 (** val cmCallstate :
 175     AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
 176     List.list -> GenMem.mem -> Cminor_semantics.stack ->
 177     Cminor_semantics.state **)
 178 let cmCallstate x x0 x1 x2 x3 =
 179   Cminor_semantics.Callstate (x, x0, x1, x2, x3)
 180