extracted/interpret2.ml

   1 open Preamble
   2
   3 open Fetch
   4
   5 open Hide
   6
   7 open Division
   8
   9 open Z
  10
  11 open BitVectorZ
  12
  13 open Pointers
  14
  15 open Coqlib
  16
  17 open Values
  18
  19 open Events
  20
  21 open IOMonad
  22
  23 open IO
  24
  25 open Sets
  26
  27 open Listb
  28
  29 open StructuredTraces
  30
  31 open AbstractStatus
  32
  33 open BitVectorTrie
  34
  35 open String
  36
  37 open Exp
  38
  39 open Arithmetic
  40
  41 open Vector
  42
  43 open FoldStuff
  44
  45 open BitVector
  46
  47 open Extranat
  48
  49 open Integers
  50
  51 open AST
  52
  53 open LabelledObjects
  54
  55 open Proper
  56
  57 open PositiveMap
  58
  59 open Deqsets
  60
  61 open ErrorMessages
  62
  63 open PreIdentifiers
  64
  65 open Errors
  66
  67 open Extralib
  68
  69 open Setoids
  70
  71 open Monad
  72
  73 open Option
  74
  75 open Div_and_mod
  76
  77 open Util
  78
  79 open List
  80
  81 open Lists
  82
  83 open Bool
  84
  85 open Relations
  86
  87 open Nat
  88
  89 open Positive
  90
  91 open Identifiers
  92
  93 open CostLabel
  94
  95 open ASM
  96
  97 open Types
  98
  99 open Hints_declaration
 100
 101 open Core_notation
 102
 103 open Pts
 104
 105 open Logic
 106
 107 open Jmeq
 108
 109 open Russell
 110
 111 open Status
 112
 113 open StatusProofs
 114
 115 open Interpret
 116
 117 open ASMCosts
 118
 119 open Stacksize
 120
 121 open SmallstepExec
 122
 123 open Executions
 124
 125 open Measurable
 126
 127 (** val mk_trans_system_of_abstract_status :
 128     StructuredTraces.abstract_status -> (__ -> __ Monad.max_def__o__monad) ->
 129     (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
 130 let mk_trans_system_of_abstract_status s as_eval =
 131   { SmallstepExec.is_final = (fun x -> s.StructuredTraces.as_result);
 132     SmallstepExec.step = (fun x status ->
 133     let tr =
 134       match StructuredTraces.as_label s status with
 135       | Types.None -> Events.e0
 136       | Types.Some cst -> Events.echarge cst
 137     in
 138     Obj.magic
 139       (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad) (as_eval status)
 140         (fun status' ->
 141         Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst = tr;
 142           Types.snd = status' }))) }
 143
 144 (** val mk_fullexec_of_abstract_status :
 145     StructuredTraces.abstract_status -> (__ -> __ Monad.max_def__o__monad) ->
 146     __ -> (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
 147 let mk_fullexec_of_abstract_status s as_eval as_init =
 148   { SmallstepExec.es1 = (mk_trans_system_of_abstract_status s as_eval);
 149     SmallstepExec.make_global = (fun x -> Obj.magic Types.It);
 150     SmallstepExec.make_initial_state = (fun x ->
 151     Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) as_init)) }
 152
 153 (** val mk_preclassified_system_of_abstract_status :
 154     StructuredTraces.abstract_status -> (__ -> __ Monad.max_def__o__monad) ->
 155     __ -> Measurable.preclassified_system **)
 156 let mk_preclassified_system_of_abstract_status s as_eval as_init =
 157   { Measurable.pcs_exec = (mk_fullexec_of_abstract_status s as_eval as_init);
 158     Measurable.pcs_labelled = (fun x st ->
 159     Bool.notb (PositiveMap.is_none (StructuredTraces.as_label s st)));
 160     Measurable.pcs_classify = (fun x -> s.StructuredTraces.as_classify);
 161     Measurable.pcs_callee = (fun x st _ ->
 162     s.StructuredTraces.as_call_ident st) }
 163
 164 (** val oC_preclassified_system :
 165     ASM.labelled_object_code -> Measurable.preclassified_system **)
 166 let oC_preclassified_system c =
 167   mk_preclassified_system_of_abstract_status (ASMCosts.oC_abstract_status c)
 168     (fun st ->
 169     Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
 170       (Interpret.execute_1 c.ASM.cm (Obj.magic st)))
 171     (Obj.magic (Status.initialise_status c.ASM.cm))
 172
 173 open Assembly
 174
 175 (** val execute_1_pseudo_instruction' :
 176     ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
 177     (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
 178     -> (BitVector.word -> Bool.bool) -> Status.pseudoStatus ->
 179     Status.pseudoStatus **)
 180 let execute_1_pseudo_instruction' cm addr_of_label addr_of_symbol sigma policy status =
 181   Interpret.execute_1_pseudo_instruction cm (fun x _ ->
 182     Assembly.ticks_of cm addr_of_label sigma policy x) addr_of_label
 183     addr_of_symbol status
 184
 185 (** val classify_pseudo_instruction :
 186     ASM.pseudo_instruction -> StructuredTraces.status_class **)
 187 let classify_pseudo_instruction = function
 188 | ASM.Instruction pre -> AbstractStatus.aSM_classify00 pre
 189 | ASM.Comment x -> StructuredTraces.Cl_other
 190 | ASM.Cost x -> StructuredTraces.Cl_other
 191 | ASM.Jmp x -> StructuredTraces.Cl_other
 192 | ASM.Jnz (x, x0, x1) -> StructuredTraces.Cl_jump
 193 | ASM.Call x -> StructuredTraces.Cl_call
 194 | ASM.Mov (x, x0, x1) -> StructuredTraces.Cl_other
 195
 196 (** val aSM_classify :
 197     ASM.pseudo_assembly_program -> Status.pseudoStatus ->
 198     StructuredTraces.status_class **)
 199 let aSM_classify cm s =
 200   classify_pseudo_instruction
 201     (ASM.fetch_pseudo_instruction cm.ASM.code s.Status.program_counter).Types.fst
 202
 203 (** val aSM_as_label_of_pc :
 204     ASM.pseudo_assembly_program -> BitVector.word -> CostLabel.costlabel
 205     Types.option **)
 206 let aSM_as_label_of_pc prog pc =
 207   match (ASM.fetch_pseudo_instruction prog.ASM.code pc).Types.fst with
 208   | ASM.Instruction x -> Types.None
 209   | ASM.Comment x -> Types.None
 210   | ASM.Cost label -> Types.Some label
 211   | ASM.Jmp x -> Types.None
 212   | ASM.Jnz (x, x0, x1) -> Types.None
 213   | ASM.Call x -> Types.None
 214   | ASM.Mov (x, x0, x1) -> Types.None
 215
 216 (** val aSM_as_result :
 217     ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
 218     Status.pseudoStatus -> Integers.int Types.option **)
 219 let aSM_as_result prog addr_of_labels st =
 220   let finaladdr = addr_of_labels prog.ASM.final_label in
 221   ASMCosts.as_result_of_finaladdr prog st finaladdr
 222
 223 open AssocList
 224
 225 (** val aSM_as_call_ident :
 226     ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
 227     (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
 228     -> (BitVector.word -> Bool.bool) -> Status.pseudoStatus Types.sig0 ->
 229     AST.ident **)
 230 let aSM_as_call_ident prog addr_of_label addr_of_symbol sigma policy s0 =
 231   let st =
 232     execute_1_pseudo_instruction' prog addr_of_label addr_of_symbol sigma
 233       policy (Types.pi1 s0)
 234   in
 235   let { Types.fst = lbl; Types.snd = instr } =
 236     Util.nth_safe
 237       (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 238         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 239         Nat.O)))))))))))))))) st.Status.program_counter) prog.ASM.code
 240   in
 241   (match lbl with
 242    | Types.None -> assert false (* absurd case *)
 243    | Types.Some lbl' ->
 244      (match AssocList.assoc_list_lookup lbl'
 245               (Identifiers.eq_identifier PreIdentifiers.ASMTag)
 246               prog.ASM.renamed_symbols with
 247       | Types.None -> assert false (* absurd case *)
 248       | Types.Some id -> id))
 249
 250 (** val aSM_abstract_status :
 251     ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
 252     (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
 253     -> (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status **)
 254 let aSM_abstract_status prog addr_of_label addr_of_symbol sigma policy =
 255   { StructuredTraces.as_pc = AbstractStatus.word_deqset;
 256     StructuredTraces.as_pc_of = (Obj.magic (Status.program_counter prog));
 257     StructuredTraces.as_classify = (Obj.magic (aSM_classify prog));
 258     StructuredTraces.as_label_of_pc = (Obj.magic (aSM_as_label_of_pc prog));
 259     StructuredTraces.as_result =
 260     (Obj.magic (aSM_as_result prog addr_of_label));
 261     StructuredTraces.as_call_ident =
 262     (Obj.magic
 263       (aSM_as_call_ident prog addr_of_label addr_of_symbol sigma policy));
 264     StructuredTraces.as_tailcall_ident = (fun clearme ->
 265     let st = clearme in
 266     (match (ASM.fetch_pseudo_instruction prog.ASM.code
 267              (Obj.magic st).Status.program_counter).Types.fst with
 268      | ASM.Instruction clearme0 ->
 269        (match clearme0 with
 270         | ASM.ADD (x, y) ->
 271           (fun _ ->
 272             Obj.magic StructuredTraces.status_class_discr
 273               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 274         | ASM.ADDC (x, y) ->
 275           (fun _ ->
 276             Obj.magic StructuredTraces.status_class_discr
 277               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 278         | ASM.SUBB (x, y) ->
 279           (fun _ ->
 280             Obj.magic StructuredTraces.status_class_discr
 281               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 282         | ASM.INC x ->
 283           (fun _ ->
 284             Obj.magic StructuredTraces.status_class_discr
 285               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 286         | ASM.DEC x ->
 287           (fun _ ->
 288             Obj.magic StructuredTraces.status_class_discr
 289               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 290         | ASM.MUL (x, y) ->
 291           (fun _ ->
 292             Obj.magic StructuredTraces.status_class_discr
 293               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 294         | ASM.DIV (x, y) ->
 295           (fun _ ->
 296             Obj.magic StructuredTraces.status_class_discr
 297               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 298         | ASM.DA x ->
 299           (fun _ ->
 300             Obj.magic StructuredTraces.status_class_discr
 301               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 302         | ASM.JC x ->
 303           (fun _ ->
 304             Obj.magic StructuredTraces.status_class_discr
 305               StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
 306         | ASM.JNC x ->
 307           (fun _ ->
 308             Obj.magic StructuredTraces.status_class_discr
 309               StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
 310         | ASM.JB (x, y) ->
 311           (fun _ ->
 312             Obj.magic StructuredTraces.status_class_discr
 313               StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
 314         | ASM.JNB (x, y) ->
 315           (fun _ ->
 316             Obj.magic StructuredTraces.status_class_discr
 317               StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
 318         | ASM.JBC (x, y) ->
 319           (fun _ ->
 320             Obj.magic StructuredTraces.status_class_discr
 321               StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
 322         | ASM.JZ x ->
 323           (fun _ ->
 324             Obj.magic StructuredTraces.status_class_discr
 325               StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
 326         | ASM.JNZ x ->
 327           (fun _ ->
 328             Obj.magic StructuredTraces.status_class_discr
 329               StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
 330         | ASM.CJNE (x, y) ->
 331           (fun _ ->
 332             Obj.magic StructuredTraces.status_class_discr
 333               StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
 334         | ASM.DJNZ (x, y) ->
 335           (fun _ ->
 336             Obj.magic StructuredTraces.status_class_discr
 337               StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
 338         | ASM.ANL x ->
 339           (fun _ ->
 340             Obj.magic StructuredTraces.status_class_discr
 341               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 342         | ASM.ORL x ->
 343           (fun _ ->
 344             Obj.magic StructuredTraces.status_class_discr
 345               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 346         | ASM.XRL x ->
 347           (fun _ ->
 348             Obj.magic StructuredTraces.status_class_discr
 349               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 350         | ASM.CLR x ->
 351           (fun _ ->
 352             Obj.magic StructuredTraces.status_class_discr
 353               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 354         | ASM.CPL x ->
 355           (fun _ ->
 356             Obj.magic StructuredTraces.status_class_discr
 357               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 358         | ASM.RL x ->
 359           (fun _ ->
 360             Obj.magic StructuredTraces.status_class_discr
 361               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 362         | ASM.RLC x ->
 363           (fun _ ->
 364             Obj.magic StructuredTraces.status_class_discr
 365               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 366         | ASM.RR x ->
 367           (fun _ ->
 368             Obj.magic StructuredTraces.status_class_discr
 369               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 370         | ASM.RRC x ->
 371           (fun _ ->
 372             Obj.magic StructuredTraces.status_class_discr
 373               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 374         | ASM.SWAP x ->
 375           (fun _ ->
 376             Obj.magic StructuredTraces.status_class_discr
 377               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 378         | ASM.MOV x ->
 379           (fun _ ->
 380             Obj.magic StructuredTraces.status_class_discr
 381               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 382         | ASM.MOVX x ->
 383           (fun _ ->
 384             Obj.magic StructuredTraces.status_class_discr
 385               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 386         | ASM.SETB x ->
 387           (fun _ ->
 388             Obj.magic StructuredTraces.status_class_discr
 389               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 390         | ASM.PUSH x ->
 391           (fun _ ->
 392             Obj.magic StructuredTraces.status_class_discr
 393               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 394         | ASM.POP x ->
 395           (fun _ ->
 396             Obj.magic StructuredTraces.status_class_discr
 397               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 398         | ASM.XCH (x, y) ->
 399           (fun _ ->
 400             Obj.magic StructuredTraces.status_class_discr
 401               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 402         | ASM.XCHD (x, y) ->
 403           (fun _ ->
 404             Obj.magic StructuredTraces.status_class_discr
 405               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 406         | ASM.RET ->
 407           (fun _ ->
 408             Obj.magic StructuredTraces.status_class_discr
 409               StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
 410         | ASM.RETI ->
 411           (fun _ ->
 412             Obj.magic StructuredTraces.status_class_discr
 413               StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
 414         | ASM.NOP ->
 415           (fun _ ->
 416             Obj.magic StructuredTraces.status_class_discr
 417               StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 418         | ASM.JMP x ->
 419           (fun _ ->
 420             Obj.magic StructuredTraces.status_class_discr
 421               StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __))
 422      | ASM.Comment x ->
 423        (fun _ ->
 424          Obj.magic StructuredTraces.status_class_discr
 425            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 426      | ASM.Cost x ->
 427        (fun _ ->
 428          Obj.magic StructuredTraces.status_class_discr
 429            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 430      | ASM.Jmp x ->
 431        (fun _ ->
 432          Obj.magic StructuredTraces.status_class_discr
 433            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
 434      | ASM.Jnz (x, y, abs) ->
 435        (fun _ ->
 436          Obj.magic StructuredTraces.status_class_discr
 437            StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
 438      | ASM.Call x ->
 439        (fun _ ->
 440          Obj.magic StructuredTraces.status_class_discr
 441            StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __)
 442      | ASM.Mov (x, y, abs) ->
 443        (fun _ ->
 444          Obj.magic StructuredTraces.status_class_discr
 445            StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)) __) }
 446
 447 (** val aSM_preclassified_system :
 448     ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
 449     (BitVector.word -> Bool.bool) -> Measurable.preclassified_system **)
 450 let aSM_preclassified_system c sigma policy =
 451   let label_map = (Fetch.create_label_cost_map c.ASM.code).Types.fst in
 452   let symbol_map = Status.construct_datalabels c.ASM.preamble in
 453   let addr_of_label = fun x ->
 454     Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 455       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 456       Nat.O))))))))))))))))
 457       (Identifiers.lookup_def PreIdentifiers.ASMTag label_map x Nat.O)
 458   in
 459   let addr_of_symbol = fun x ->
 460     Identifiers.lookup_def PreIdentifiers.ASMTag symbol_map x
 461       (addr_of_label x)
 462   in
 463   mk_preclassified_system_of_abstract_status
 464     (aSM_abstract_status c addr_of_label addr_of_symbol sigma policy)
 465     (fun st ->
 466     Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
 467       (execute_1_pseudo_instruction' c addr_of_label addr_of_symbol sigma
 468         policy (Obj.magic st))) (Obj.magic (Status.initialise_status c))
 469