open Preamble

open Div_and_mod

open Jmeq

open Russell

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open List

open Util

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 FoldStuff

open BitVector

open Positive

open Z

open BitVectorZ

open Pointers

open ByteValues

open BackEndOps

open Joint

open ERTL

open Set_adt

open Fixpoints

(** val rl_included :
    (PreIdentifiers.identifier Set_adt.set, I8051.register Set_adt.set)
    Types.prod -> (PreIdentifiers.identifier Set_adt.set, I8051.register
    Set_adt.set) Types.prod -> Bool.bool **)
let rl_included left right =
  Bool.andb
    (Set_adt.set_subset
      (Identifiers.eq_identifier PreIdentifiers.RegisterTag) left.Types.fst
      right.Types.fst)
    (Set_adt.set_subset I8051.eq_Register left.Types.snd right.Types.snd)

(** val register_lattice : Fixpoints.property_lattice **)
let register_lattice =
  { Fixpoints.l_bottom =
    (Obj.magic { Types.fst = Set_adt.set_empty; Types.snd =
      Set_adt.set_empty }); Fixpoints.l_equal = (fun left right ->
    Bool.andb
      (Set_adt.set_equal
        (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
        (Obj.magic left).Types.fst (Obj.magic right).Types.fst)
      (Set_adt.set_equal I8051.eq_Register (Obj.magic left).Types.snd
        (Obj.magic right).Types.snd)); Fixpoints.l_included =
    (Obj.magic rl_included); Fixpoints.l_is_maximal = (fun x -> Bool.False) }

(** val rl_bottom : __ **)
let rl_bottom =
  register_lattice.Fixpoints.l_bottom

(** val rl_psingleton : Registers.register -> __ **)
let rl_psingleton r =
  Obj.magic { Types.fst = (Set_adt.set_singleton r); Types.snd =
    Set_adt.set_empty }

(** val rl_hsingleton : I8051.register -> __ **)
let rl_hsingleton r =
  Obj.magic { Types.fst = Set_adt.set_empty; Types.snd =
    (Set_adt.set_singleton r) }

(** val pairwise :
    ('a1 -> 'a1 -> 'a1) -> ('a2 -> 'a2 -> 'a2) -> ('a1, 'a2) Types.prod ->
    ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod **)
let pairwise f g c1 c2 =
  { Types.fst = (f c1.Types.fst c2.Types.fst); Types.snd =
    (g c1.Types.snd c2.Types.snd) }

(** val rl_join : __ -> __ -> __ **)
let rl_join =
  Obj.magic (pairwise Set_adt.set_union Set_adt.set_union)

(** val rl_diff : __ -> __ -> __ **)
let rl_diff =
  Obj.magic (pairwise Set_adt.set_diff Set_adt.set_diff)

(** val defined : AST.ident List.list -> Joint.joint_statement -> __ **)
let defined globals = function
| Joint.Sequential (seq, l) ->
  (match seq with
   | Joint.COST_LABEL clabel -> rl_bottom
   | Joint.CALL (x, x0, x1) ->
     Obj.magic { Types.fst = Set_adt.set_empty; Types.snd =
       (Set_adt.set_from_list I8051.registerCallerSaved) }
   | Joint.COND (r, lbl_true) -> rl_bottom
   | Joint.Step_seq s0 ->
     (match s0 with
      | Joint.COMMENT c -> rl_bottom
      | Joint.MOVE pair_reg ->
        (match (Obj.magic pair_reg).Types.fst with
         | ERTL.PSD p -> rl_psingleton p
         | ERTL.HDW h -> rl_hsingleton h)
      | Joint.POP r -> rl_psingleton (Obj.magic r)
      | Joint.PUSH r -> rl_bottom
      | Joint.ADDRESS (x, x1, r1, r2) ->
        rl_join (rl_psingleton (Obj.magic r1)) (rl_psingleton (Obj.magic r2))
      | Joint.OPACCS (opaccs, dr1, dr2, sr1, sr2) ->
        rl_join
          (rl_join (rl_psingleton (Obj.magic dr1))
            (rl_psingleton (Obj.magic dr2)))
          (rl_hsingleton I8051.RegisterCarry)
      | Joint.OP1 (op1, r1, r2) -> rl_psingleton (Obj.magic r1)
      | Joint.OP2 (op2, r1, r2, x) ->
        (match op2 with
         | BackEndOps.Add ->
           rl_join (rl_hsingleton I8051.RegisterCarry)
             (rl_psingleton (Obj.magic r1))
         | BackEndOps.Addc ->
           rl_join (rl_hsingleton I8051.RegisterCarry)
             (rl_psingleton (Obj.magic r1))
         | BackEndOps.Sub ->
           rl_join (rl_hsingleton I8051.RegisterCarry)
             (rl_psingleton (Obj.magic r1))
         | BackEndOps.And -> rl_psingleton (Obj.magic r1)
         | BackEndOps.Or -> rl_psingleton (Obj.magic r1)
         | BackEndOps.Xor -> rl_psingleton (Obj.magic r1))
      | Joint.CLEAR_CARRY -> rl_hsingleton I8051.RegisterCarry
      | Joint.SET_CARRY -> rl_hsingleton I8051.RegisterCarry
      | Joint.LOAD (r, x, x0) -> rl_psingleton (Obj.magic r)
      | Joint.STORE (acc_a, dpl, dph) -> rl_bottom
      | Joint.Extension_seq ext ->
        (match Obj.magic ext with
         | ERTL.Ertl_new_frame ->
           rl_join (rl_hsingleton I8051.registerSPL)
             (rl_hsingleton I8051.registerSPH)
         | ERTL.Ertl_del_frame ->
           rl_join (rl_hsingleton I8051.registerSPL)
             (rl_hsingleton I8051.registerSPH)
         | ERTL.Ertl_frame_size r -> rl_psingleton r)))
| Joint.Final x -> rl_bottom
| Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)

(** val ret_regs : I8051.register Set_adt.set **)
let ret_regs =
  Set_adt.set_from_list I8051.registerRets

(** val rl_arg : Joint.psd_argument -> __ **)
let rl_arg = function
| Joint.Reg r -> rl_psingleton r
| Joint.Imm x -> rl_bottom

(** val used :
    AST.ident List.list -> Joint.joint_statement -> (Registers.register
    Set_adt.set, I8051.register Set_adt.set) Types.prod **)
let used globals = function
| Joint.Sequential (seq, l) ->
  (match seq with
   | Joint.COST_LABEL clabel -> Obj.magic rl_bottom
   | Joint.CALL (f, nparams, x) ->
     Obj.magic
       (rl_join
         (match f with
          | Types.Inl x0 -> rl_bottom
          | Types.Inr pr ->
            rl_join (rl_arg (Obj.magic pr).Types.fst)
              (rl_arg (Obj.magic pr).Types.snd))
         (Obj.magic { Types.fst = Set_adt.set_empty; Types.snd =
           (Set_adt.set_from_list
             (Util.prefix (Obj.magic nparams) I8051.registerParams)) }))
   | Joint.COND (r, lbl_true) -> Obj.magic (rl_psingleton (Obj.magic r))
   | Joint.Step_seq s0 ->
     (match s0 with
      | Joint.COMMENT x -> Obj.magic rl_bottom
      | Joint.MOVE pair_reg ->
        let r2 = (Obj.magic pair_reg).Types.snd in
        (match r2 with
         | Joint.Reg p ->
           (match p with
            | ERTL.PSD r -> Obj.magic (rl_psingleton r)
            | ERTL.HDW r -> Obj.magic (rl_hsingleton r))
         | Joint.Imm x -> Obj.magic rl_bottom)
      | Joint.POP x -> Obj.magic rl_bottom
      | Joint.PUSH r -> Obj.magic (rl_arg (Obj.magic r))
      | Joint.ADDRESS (x, x1, x2, x3) -> Obj.magic rl_bottom
      | Joint.OPACCS (opaccs, dr1, dr2, sr1, sr2) ->
        Obj.magic (rl_join (rl_arg (Obj.magic sr1)) (rl_arg (Obj.magic sr2)))
      | Joint.OP1 (op1, r1, r2) -> Obj.magic (rl_psingleton (Obj.magic r2))
      | Joint.OP2 (op2, acc_a, r1, r2) ->
        Obj.magic
          (rl_join (rl_join (rl_arg (Obj.magic r1)) (rl_arg (Obj.magic r2)))
            (match op2 with
             | BackEndOps.Add -> rl_bottom
             | BackEndOps.Addc -> rl_hsingleton I8051.RegisterCarry
             | BackEndOps.Sub -> rl_hsingleton I8051.RegisterCarry
             | BackEndOps.And -> rl_bottom
             | BackEndOps.Or -> rl_bottom
             | BackEndOps.Xor -> rl_bottom))
      | Joint.CLEAR_CARRY -> Obj.magic rl_bottom
      | Joint.SET_CARRY -> Obj.magic rl_bottom
      | Joint.LOAD (acc_a, dpl, dph) ->
        Obj.magic (rl_join (rl_arg (Obj.magic dpl)) (rl_arg (Obj.magic dph)))
      | Joint.STORE (acc_a, dpl, dph) ->
        Obj.magic
          (rl_join
            (rl_join (rl_arg (Obj.magic acc_a)) (rl_arg (Obj.magic dpl)))
            (rl_arg (Obj.magic dph)))
      | Joint.Extension_seq ext ->
        (match Obj.magic ext with
         | ERTL.Ertl_new_frame ->
           Obj.magic
             (rl_join (rl_hsingleton I8051.registerSPL)
               (rl_hsingleton I8051.registerSPH))
         | ERTL.Ertl_del_frame ->
           Obj.magic
             (rl_join (rl_hsingleton I8051.registerSPL)
               (rl_hsingleton I8051.registerSPH))
         | ERTL.Ertl_frame_size r -> Obj.magic rl_bottom)))
| Joint.Final fin ->
  (match fin with
   | Joint.GOTO l -> Obj.magic rl_bottom
   | Joint.RETURN ->
     { Types.fst = Set_adt.set_empty; Types.snd =
       (Set_adt.set_union (Set_adt.set_from_list I8051.registerCalleeSaved)
         ret_regs) }
   | Joint.TAILCALL (x, x0) -> assert false (* absurd case *))
| Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)

(** val eliminable_step :
    AST.ident List.list -> __ -> Joint.joint_step -> Bool.bool **)
let eliminable_step globals l s =
  let pliveafter = (Obj.magic l).Types.fst in
  let hliveafter = (Obj.magic l).Types.snd in
  (match s with
   | Joint.COST_LABEL x -> Bool.False
   | Joint.CALL (x, x0, x1) -> Bool.False
   | Joint.COND (x, x0) -> Bool.False
   | Joint.Step_seq s0 ->
     (match s0 with
      | Joint.COMMENT x -> Bool.False
      | Joint.MOVE pair_reg ->
        Bool.notb
          (match (Obj.magic pair_reg).Types.fst with
           | ERTL.PSD p1 ->
             Set_adt.set_member
               (Identifiers.eq_identifier PreIdentifiers.RegisterTag) p1
               pliveafter
           | ERTL.HDW h1 ->
             Set_adt.set_member I8051.eq_Register h1 hliveafter)
      | Joint.POP x -> Bool.False
      | Joint.PUSH x -> Bool.False
      | Joint.ADDRESS (x, x1, r1, r2) ->
        Bool.notb
          (Bool.orb
            (Set_adt.set_member
              (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
              (Obj.magic r1) pliveafter)
            (Set_adt.set_member
              (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
              (Obj.magic r2) pliveafter))
      | Joint.OPACCS (opaccs, dr1, dr2, sr1, sr2) ->
        Bool.notb
          (Bool.orb
            (Bool.orb
              (Set_adt.set_member
                (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
                (Obj.magic dr1) pliveafter)
              (Set_adt.set_member
                (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
                (Obj.magic dr2) pliveafter))
            (Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
              hliveafter))
      | Joint.OP1 (op1, r1, r2) ->
        Bool.notb
          (Set_adt.set_member
            (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
            (Obj.magic r1) pliveafter)
      | Joint.OP2 (op2, r1, r2, r3) ->
        Bool.notb
          (Bool.orb
            (match op2 with
             | BackEndOps.Add ->
               Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
                 hliveafter
             | BackEndOps.Addc ->
               Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
                 hliveafter
             | BackEndOps.Sub ->
               Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
                 hliveafter
             | BackEndOps.And -> Bool.False
             | BackEndOps.Or -> Bool.False
             | BackEndOps.Xor -> Bool.False)
            (Set_adt.set_member
              (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
              (Obj.magic r1) pliveafter))
      | Joint.CLEAR_CARRY -> Bool.False
      | Joint.SET_CARRY -> Bool.False
      | Joint.LOAD (acc_a, dpl, dph) ->
        Bool.notb
          (Set_adt.set_member
            (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
            (Obj.magic acc_a) pliveafter)
      | Joint.STORE (x, x0, x1) -> Bool.False
      | Joint.Extension_seq ext ->
        (match Obj.magic ext with
         | ERTL.Ertl_new_frame -> Bool.False
         | ERTL.Ertl_del_frame -> Bool.False
         | ERTL.Ertl_frame_size r ->
           Bool.notb
             (Set_adt.set_member
               (Identifiers.eq_identifier PreIdentifiers.RegisterTag) r
               pliveafter))))

(** val eliminable :
    AST.ident List.list -> __ -> Joint.joint_statement -> Bool.bool **)
let eliminable globals l s =
  let pliveafter = (Obj.magic l).Types.fst in
  let hliveafter = (Obj.magic l).Types.snd in
  (match s with
   | Joint.Sequential (seq, x) -> eliminable_step globals l seq
   | Joint.Final x -> Bool.False
   | Joint.FCOND (x0, x1, x2) -> Bool.False)

(** val statement_semantics :
    AST.ident List.list -> Joint.joint_statement -> __ -> __ **)
let statement_semantics globals stmt liveafter =
  match eliminable globals liveafter stmt with
  | Bool.True -> liveafter
  | Bool.False ->
    rl_join (rl_diff liveafter (defined globals stmt))
      (Obj.magic (used globals stmt))

(** val livebefore :
    AST.ident List.list -> Joint.joint_internal_function ->
    Fixpoints.valuation -> Fixpoints.valuation **)
let livebefore globals int_fun liveafter label =
  match Identifiers.lookup PreIdentifiers.LabelTag
          (Obj.magic int_fun.Joint.joint_if_code) label with
  | Types.None -> rl_bottom
  | Types.Some stmt -> statement_semantics globals stmt (liveafter label)

(** val liveafter :
    AST.ident List.list -> Joint.joint_internal_function ->
    PreIdentifiers.identifier -> Fixpoints.valuation -> __ **)
let liveafter globals int_fun label liveafter0 =
  match Identifiers.lookup PreIdentifiers.LabelTag
          (Obj.magic int_fun.Joint.joint_if_code) label with
  | Types.None -> rl_bottom
  | Types.Some stmt ->
    List.fold rl_join rl_bottom (fun successor -> Bool.True)
      (fun successor -> livebefore globals int_fun liveafter0 successor)
      (Joint.stmt_labels { Joint.uns_pars = (Joint.g_u_pars ERTL.eRTL);
        Joint.succ_label = (Obj.magic (fun x -> Types.Some x));
        Joint.has_fcond = Bool.False } globals stmt)

(** val analyse_liveness :
    Fixpoints.fixpoint_computer -> AST.ident List.list ->
    Joint.joint_internal_function -> Fixpoints.fixpoint **)
let analyse_liveness the_fixpoint globals int_fun =
  the_fixpoint register_lattice (liveafter globals int_fun)

type vertex = (Registers.register, I8051.register) Types.sum

(** val plives : Registers.register -> __ -> Bool.bool **)
let plives vertex0 prop =
  Set_adt.set_member (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
    vertex0 (Obj.magic prop).Types.fst

(** val hlives : I8051.register -> __ -> Bool.bool **)
let hlives vertex0 prop =
  Set_adt.set_member I8051.eq_Register vertex0 (Obj.magic prop).Types.snd

(** val lives : vertex -> __ -> Bool.bool **)
let lives = function
| Types.Inl v -> plives v
| Types.Inr v -> hlives v