extracted/joint_fullexec.ml

   1 open Preamble
   2
   3 open StructuredTraces
   4
   5 open ExtraMonads
   6
   7 open Deqsets_extra
   8
   9 open State
  10
  11 open Bind_new
  12
  13 open BindLists
  14
  15 open Blocks
  16
  17 open TranslateUtils
  18
  19 open ExtraGlobalenvs
  20
  21 open I8051bis
  22
  23 open String
  24
  25 open Sets
  26
  27 open Listb
  28
  29 open LabelledObjects
  30
  31 open BitVectorTrie
  32
  33 open Graphs
  34
  35 open I8051
  36
  37 open Order
  38
  39 open Registers
  40
  41 open BackEndOps
  42
  43 open Joint
  44
  45 open BEMem
  46
  47 open CostLabel
  48
  49 open Events
  50
  51 open IOMonad
  52
  53 open IO
  54
  55 open Extra_bool
  56
  57 open Coqlib
  58
  59 open Values
  60
  61 open FrontEndVal
  62
  63 open Hide
  64
  65 open ByteValues
  66
  67 open Division
  68
  69 open Z
  70
  71 open BitVectorZ
  72
  73 open Pointers
  74
  75 open GenMem
  76
  77 open FrontEndMem
  78
  79 open Proper
  80
  81 open PositiveMap
  82
  83 open Deqsets
  84
  85 open Extralib
  86
  87 open Lists
  88
  89 open Identifiers
  90
  91 open Exp
  92
  93 open Arithmetic
  94
  95 open Vector
  96
  97 open Div_and_mod
  98
  99 open Util
 100
 101 open FoldStuff
 102
 103 open BitVector
 104
 105 open Extranat
 106
 107 open Integers
 108
 109 open AST
 110
 111 open ErrorMessages
 112
 113 open Option
 114
 115 open Setoids
 116
 117 open Monad
 118
 119 open Jmeq
 120
 121 open Russell
 122
 123 open Positive
 124
 125 open PreIdentifiers
 126
 127 open Bool
 128
 129 open Relations
 130
 131 open Nat
 132
 133 open List
 134
 135 open Hints_declaration
 136
 137 open Core_notation
 138
 139 open Pts
 140
 141 open Logic
 142
 143 open Types
 144
 145 open Errors
 146
 147 open Globalenvs
 148
 149 open Joint_semantics
 150
 151 open SemanticsUtils
 152
 153 open Traces
 154
 155 open Stacksize
 156
 157 open SmallstepExec
 158
 159 open Executions
 160
 161 open Measurable
 162
 163 (** val joint_exec :
 164     Joint_semantics.sem_params -> (IO.io_out, IO.io_in)
 165     SmallstepExec.trans_system **)
 166 let joint_exec g =
 167   { SmallstepExec.is_final = (fun env ->
 168     Obj.magic (Traces.joint_final g (Obj.magic env))); SmallstepExec.step =
 169     (fun env st ->
 170     Obj.magic
 171       (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
 172         (Obj.magic
 173           (Joint_semantics.eval_state g (Obj.magic env).Traces.globals
 174             (Obj.magic env).Traces.ev_genv (Obj.magic st))) (fun st' ->
 175         let charge =
 176           match Traces.joint_label_of_pc g (Obj.magic env)
 177                   (Obj.magic st).Joint_semantics.pc with
 178           | Types.None -> Events.e0
 179           | Types.Some c -> Events.echarge c
 180         in
 181         Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst = charge;
 182           Types.snd = st' }))) }
 183
 184 (** val joint_fullexec :
 185     Joint_semantics.sem_params -> (IO.io_out, IO.io_in)
 186     SmallstepExec.fullexec **)
 187 let joint_fullexec g =
 188   { SmallstepExec.es1 = (joint_exec g); SmallstepExec.make_global =
 189     (fun pr ->
 190     Obj.magic
 191       (Traces.joint_make_global { Traces.prog_spars = g; Traces.prog =
 192         (Obj.magic pr).Types.fst; Traces.stack_sizes =
 193         (Obj.magic pr).Types.snd })); SmallstepExec.make_initial_state =
 194     (fun p_stacks ->
 195     Obj.magic
 196       (Traces.make_initial_state { Traces.prog_spars = g; Traces.prog =
 197         (Obj.magic p_stacks).Types.fst; Traces.stack_sizes =
 198         (Obj.magic p_stacks).Types.snd })) }
 199
 200 (** val joint_preclassified_system :
 201     Joint_semantics.sem_params -> Measurable.preclassified_system **)
 202 let joint_preclassified_system g =
 203   { Measurable.pcs_exec = (joint_fullexec g); Measurable.pcs_labelled =
 204     (fun env st ->
 205     Bool.notb
 206       (PositiveMap.is_none
 207         (Traces.joint_label_of_pc g (Obj.magic env)
 208           (Obj.magic st).Joint_semantics.pc))); Measurable.pcs_classify =
 209     (fun env -> Obj.magic (Traces.joint_classify g (Obj.magic env)));
 210     Measurable.pcs_callee = (fun env s _ ->
 211     Traces.joint_call_ident g (Obj.magic env) (Obj.magic s)) }
 212