open Preamble

open Extra_bool

open Coqlib

open Values

open FrontEndVal

open GenMem

open FrontEndMem

open Globalenvs

open String

open Sets

open Listb

open LabelledObjects

open BitVectorTrie

open Graphs

open I8051

open Order

open Registers

open CostLabel

open Hide

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Identifiers

open Integers

open AST

open Division

open Exp

open Arithmetic

open Setoids

open Monad

open Option

open Extranat

open Vector

open Div_and_mod

open Jmeq

open Russell

open List

open Util

open FoldStuff

open BitVector

open Types

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Positive

open Z

open BitVectorZ

open Pointers

open ByteValues

open BackEndOps

open Joint

open ERTL

(** val examine_internal :
    AST.ident List.list -> Joint.joint_internal_function -> Positive.pos
    Identifiers.identifier_map **)
let examine_internal globals fun0 =
  let incr = fun r map ->
    match Identifiers.lookup PreIdentifiers.RegisterTag map r with
    | Types.None ->
      Identifiers.add PreIdentifiers.RegisterTag map r Positive.One
    | Types.Some v ->
      Identifiers.add PreIdentifiers.RegisterTag map r (Positive.succ v)
  in
  let incr_arg = fun arg map ->
    match arg with
    | Joint.Reg r -> incr r map
    | Joint.Imm x -> map
  in
  let f = fun x instr map ->
    match instr with
    | Joint.Sequential (s, x0) ->
      (match s with
       | Joint.COST_LABEL x1 -> map
       | Joint.CALL (id, x1, x2) ->
         (match id with
          | Types.Inl x3 -> map
          | Types.Inr pr ->
            Obj.magic incr_arg pr.Types.fst
              (Obj.magic incr_arg pr.Types.snd map))
       | Joint.COND (r, x1) -> Obj.magic incr r map
       | Joint.Step_seq s0 ->
         (match s0 with
          | Joint.COMMENT x1 -> map
          | Joint.MOVE pair ->
            let { Types.fst = r1; Types.snd = r2 } = Obj.magic pair in
            let incr_dst = fun arg map0 ->
              match arg with
              | ERTL.PSD r -> incr r map0
              | ERTL.HDW x1 -> map0
            in
            incr_dst r1
              (match r2 with
               | Joint.Reg a -> incr_dst a map
               | Joint.Imm x1 -> map)
          | Joint.POP r -> Obj.magic incr r map
          | Joint.PUSH r -> Obj.magic incr_arg r map
          | Joint.ADDRESS (x1, x3, x4, x5) -> map
          | Joint.OPACCS (x1, r1, r2, r3, r4) ->
            Obj.magic incr r1
              (Obj.magic incr r2
                (Obj.magic incr_arg r3 (Obj.magic incr_arg r4 map)))
          | Joint.OP1 (x1, r1, r2) ->
            Obj.magic incr r1 (Obj.magic incr r2 map)
          | Joint.OP2 (x1, r1, r2, r3) ->
            Obj.magic incr r1
              (Obj.magic incr_arg r2 (Obj.magic incr_arg r3 map))
          | Joint.CLEAR_CARRY -> map
          | Joint.SET_CARRY -> map
          | Joint.LOAD (r1, x1, x2) -> Obj.magic incr r1 map
          | Joint.STORE (x1, x2, r) -> Obj.magic incr_arg r map
          | Joint.Extension_seq s1 ->
            (match Obj.magic s1 with
             | ERTL.Ertl_new_frame -> map
             | ERTL.Ertl_del_frame -> map
             | ERTL.Ertl_frame_size r -> incr r map)))
    | Joint.Final x0 -> map
    | Joint.FCOND (x0, x1, x2) -> assert false (* absurd case *)
  in
  Identifiers.foldi PreIdentifiers.LabelTag f
    (Obj.magic fun0.Joint.joint_if_code)
    (Identifiers.empty_map PreIdentifiers.RegisterTag)