extracted/uses.ml

   1 open Preamble
   2
   3 open Extra_bool
   4
   5 open Coqlib
   6
   7 open Values
   8
   9 open FrontEndVal
  10
  11 open GenMem
  12
  13 open FrontEndMem
  14
  15 open Globalenvs
  16
  17 open String
  18
  19 open Sets
  20
  21 open Listb
  22
  23 open LabelledObjects
  24
  25 open BitVectorTrie
  26
  27 open Graphs
  28
  29 open I8051
  30
  31 open Order
  32
  33 open Registers
  34
  35 open CostLabel
  36
  37 open Hide
  38
  39 open Proper
  40
  41 open PositiveMap
  42
  43 open Deqsets
  44
  45 open ErrorMessages
  46
  47 open PreIdentifiers
  48
  49 open Errors
  50
  51 open Extralib
  52
  53 open Lists
  54
  55 open Identifiers
  56
  57 open Integers
  58
  59 open AST
  60
  61 open Division
  62
  63 open Exp
  64
  65 open Arithmetic
  66
  67 open Setoids
  68
  69 open Monad
  70
  71 open Option
  72
  73 open Extranat
  74
  75 open Vector
  76
  77 open Div_and_mod
  78
  79 open Jmeq
  80
  81 open Russell
  82
  83 open List
  84
  85 open Util
  86
  87 open FoldStuff
  88
  89 open BitVector
  90
  91 open Types
  92
  93 open Bool
  94
  95 open Relations
  96
  97 open Nat
  98
  99 open Hints_declaration
 100
 101 open Core_notation
 102
 103 open Pts
 104
 105 open Logic
 106
 107 open Positive
 108
 109 open Z
 110
 111 open BitVectorZ
 112
 113 open Pointers
 114
 115 open ByteValues
 116
 117 open BackEndOps
 118
 119 open Joint
 120
 121 open ERTL
 122
 123 (** val examine_internal :
 124     AST.ident List.list -> Joint.joint_internal_function -> Positive.pos
 125     Identifiers.identifier_map **)
 126 let examine_internal globals fun0 =
 127   let incr = fun r map ->
 128     match Identifiers.lookup PreIdentifiers.RegisterTag map r with
 129     | Types.None ->
 130       Identifiers.add PreIdentifiers.RegisterTag map r Positive.One
 131     | Types.Some v ->
 132       Identifiers.add PreIdentifiers.RegisterTag map r (Positive.succ v)
 133   in
 134   let incr_arg = fun arg map ->
 135     match arg with
 136     | Joint.Reg r -> incr r map
 137     | Joint.Imm x -> map
 138   in
 139   let f = fun x instr map ->
 140     match instr with
 141     | Joint.Sequential (s, x0) ->
 142       (match s with
 143        | Joint.COST_LABEL x1 -> map
 144        | Joint.CALL (id, x1, x2) ->
 145          (match id with
 146           | Types.Inl x3 -> map
 147           | Types.Inr pr ->
 148             Obj.magic incr_arg pr.Types.fst
 149               (Obj.magic incr_arg pr.Types.snd map))
 150        | Joint.COND (r, x1) -> Obj.magic incr r map
 151        | Joint.Step_seq s0 ->
 152          (match s0 with
 153           | Joint.COMMENT x1 -> map
 154           | Joint.MOVE pair ->
 155             let { Types.fst = r1; Types.snd = r2 } = Obj.magic pair in
 156             let incr_dst = fun arg map0 ->
 157               match arg with
 158               | ERTL.PSD r -> incr r map0
 159               | ERTL.HDW x1 -> map0
 160             in
 161             incr_dst r1
 162               (match r2 with
 163                | Joint.Reg a -> incr_dst a map
 164                | Joint.Imm x1 -> map)
 165           | Joint.POP r -> Obj.magic incr r map
 166           | Joint.PUSH r -> Obj.magic incr_arg r map
 167           | Joint.ADDRESS (x1, x3, x4, x5) -> map
 168           | Joint.OPACCS (x1, r1, r2, r3, r4) ->
 169             Obj.magic incr r1
 170               (Obj.magic incr r2
 171                 (Obj.magic incr_arg r3 (Obj.magic incr_arg r4 map)))
 172           | Joint.OP1 (x1, r1, r2) ->
 173             Obj.magic incr r1 (Obj.magic incr r2 map)
 174           | Joint.OP2 (x1, r1, r2, r3) ->
 175             Obj.magic incr r1
 176               (Obj.magic incr_arg r2 (Obj.magic incr_arg r3 map))
 177           | Joint.CLEAR_CARRY -> map
 178           | Joint.SET_CARRY -> map
 179           | Joint.LOAD (r1, x1, x2) -> Obj.magic incr r1 map
 180           | Joint.STORE (x1, x2, r) -> Obj.magic incr_arg r map
 181           | Joint.Extension_seq s1 ->
 182             (match Obj.magic s1 with
 183              | ERTL.Ertl_new_frame -> map
 184              | ERTL.Ertl_del_frame -> map
 185              | ERTL.Ertl_frame_size r -> incr r map)))
 186     | Joint.Final x0 -> map
 187     | Joint.FCOND (x0, x1, x2) -> assert false (* absurd case *)
 188   in
 189   Identifiers.foldi PreIdentifiers.LabelTag f
 190     (Obj.magic fun0.Joint.joint_if_code)
 191     (Identifiers.empty_map PreIdentifiers.RegisterTag)
 192