extracted/liveness.ml

   1 open Preamble
   2
   3 open Div_and_mod
   4
   5 open Jmeq
   6
   7 open Russell
   8
   9 open Bool
  10
  11 open Relations
  12
  13 open Nat
  14
  15 open Hints_declaration
  16
  17 open Core_notation
  18
  19 open Pts
  20
  21 open Logic
  22
  23 open Types
  24
  25 open List
  26
  27 open Util
  28
  29 open Extra_bool
  30
  31 open Coqlib
  32
  33 open Values
  34
  35 open FrontEndVal
  36
  37 open GenMem
  38
  39 open FrontEndMem
  40
  41 open Globalenvs
  42
  43 open String
  44
  45 open Sets
  46
  47 open Listb
  48
  49 open LabelledObjects
  50
  51 open BitVectorTrie
  52
  53 open Graphs
  54
  55 open I8051
  56
  57 open Order
  58
  59 open Registers
  60
  61 open CostLabel
  62
  63 open Hide
  64
  65 open Proper
  66
  67 open PositiveMap
  68
  69 open Deqsets
  70
  71 open ErrorMessages
  72
  73 open PreIdentifiers
  74
  75 open Errors
  76
  77 open Extralib
  78
  79 open Lists
  80
  81 open Identifiers
  82
  83 open Integers
  84
  85 open AST
  86
  87 open Division
  88
  89 open Exp
  90
  91 open Arithmetic
  92
  93 open Setoids
  94
  95 open Monad
  96
  97 open Option
  98
  99 open Extranat
 100
 101 open Vector
 102
 103 open FoldStuff
 104
 105 open BitVector
 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 open Set_adt
 124
 125 open Fixpoints
 126
 127 (** val rl_included :
 128     (PreIdentifiers.identifier Set_adt.set, I8051.register Set_adt.set)
 129     Types.prod -> (PreIdentifiers.identifier Set_adt.set, I8051.register
 130     Set_adt.set) Types.prod -> Bool.bool **)
 131 let rl_included left right =
 132   Bool.andb
 133     (Set_adt.set_subset
 134       (Identifiers.eq_identifier PreIdentifiers.RegisterTag) left.Types.fst
 135       right.Types.fst)
 136     (Set_adt.set_subset I8051.eq_Register left.Types.snd right.Types.snd)
 137
 138 (** val register_lattice : Fixpoints.property_lattice **)
 139 let register_lattice =
 140   { Fixpoints.l_bottom =
 141     (Obj.magic { Types.fst = Set_adt.set_empty; Types.snd =
 142       Set_adt.set_empty }); Fixpoints.l_equal = (fun left right ->
 143     Bool.andb
 144       (Set_adt.set_equal
 145         (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
 146         (Obj.magic left).Types.fst (Obj.magic right).Types.fst)
 147       (Set_adt.set_equal I8051.eq_Register (Obj.magic left).Types.snd
 148         (Obj.magic right).Types.snd)); Fixpoints.l_included =
 149     (Obj.magic rl_included); Fixpoints.l_is_maximal = (fun x -> Bool.False) }
 150
 151 (** val rl_bottom : __ **)
 152 let rl_bottom =
 153   register_lattice.Fixpoints.l_bottom
 154
 155 (** val rl_psingleton : Registers.register -> __ **)
 156 let rl_psingleton r =
 157   Obj.magic { Types.fst = (Set_adt.set_singleton r); Types.snd =
 158     Set_adt.set_empty }
 159
 160 (** val rl_hsingleton : I8051.register -> __ **)
 161 let rl_hsingleton r =
 162   Obj.magic { Types.fst = Set_adt.set_empty; Types.snd =
 163     (Set_adt.set_singleton r) }
 164
 165 (** val pairwise :
 166     ('a1 -> 'a1 -> 'a1) -> ('a2 -> 'a2 -> 'a2) -> ('a1, 'a2) Types.prod ->
 167     ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod **)
 168 let pairwise f g c1 c2 =
 169   { Types.fst = (f c1.Types.fst c2.Types.fst); Types.snd =
 170     (g c1.Types.snd c2.Types.snd) }
 171
 172 (** val rl_join : __ -> __ -> __ **)
 173 let rl_join =
 174   Obj.magic (pairwise Set_adt.set_union Set_adt.set_union)
 175
 176 (** val rl_diff : __ -> __ -> __ **)
 177 let rl_diff =
 178   Obj.magic (pairwise Set_adt.set_diff Set_adt.set_diff)
 179
 180 (** val defined : AST.ident List.list -> Joint.joint_statement -> __ **)
 181 let defined globals = function
 182 | Joint.Sequential (seq, l) ->
 183   (match seq with
 184    | Joint.COST_LABEL clabel -> rl_bottom
 185    | Joint.CALL (x, x0, x1) ->
 186      Obj.magic { Types.fst = Set_adt.set_empty; Types.snd =
 187        (Set_adt.set_from_list I8051.registerCallerSaved) }
 188    | Joint.COND (r, lbl_true) -> rl_bottom
 189    | Joint.Step_seq s0 ->
 190      (match s0 with
 191       | Joint.COMMENT c -> rl_bottom
 192       | Joint.MOVE pair_reg ->
 193         (match (Obj.magic pair_reg).Types.fst with
 194          | ERTL.PSD p -> rl_psingleton p
 195          | ERTL.HDW h -> rl_hsingleton h)
 196       | Joint.POP r -> rl_psingleton (Obj.magic r)
 197       | Joint.PUSH r -> rl_bottom
 198       | Joint.ADDRESS (x, x1, r1, r2) ->
 199         rl_join (rl_psingleton (Obj.magic r1)) (rl_psingleton (Obj.magic r2))
 200       | Joint.OPACCS (opaccs, dr1, dr2, sr1, sr2) ->
 201         rl_join
 202           (rl_join (rl_psingleton (Obj.magic dr1))
 203             (rl_psingleton (Obj.magic dr2)))
 204           (rl_hsingleton I8051.RegisterCarry)
 205       | Joint.OP1 (op1, r1, r2) -> rl_psingleton (Obj.magic r1)
 206       | Joint.OP2 (op2, r1, r2, x) ->
 207         (match op2 with
 208          | BackEndOps.Add ->
 209            rl_join (rl_hsingleton I8051.RegisterCarry)
 210              (rl_psingleton (Obj.magic r1))
 211          | BackEndOps.Addc ->
 212            rl_join (rl_hsingleton I8051.RegisterCarry)
 213              (rl_psingleton (Obj.magic r1))
 214          | BackEndOps.Sub ->
 215            rl_join (rl_hsingleton I8051.RegisterCarry)
 216              (rl_psingleton (Obj.magic r1))
 217          | BackEndOps.And -> rl_psingleton (Obj.magic r1)
 218          | BackEndOps.Or -> rl_psingleton (Obj.magic r1)
 219          | BackEndOps.Xor -> rl_psingleton (Obj.magic r1))
 220       | Joint.CLEAR_CARRY -> rl_hsingleton I8051.RegisterCarry
 221       | Joint.SET_CARRY -> rl_hsingleton I8051.RegisterCarry
 222       | Joint.LOAD (r, x, x0) -> rl_psingleton (Obj.magic r)
 223       | Joint.STORE (acc_a, dpl, dph) -> rl_bottom
 224       | Joint.Extension_seq ext ->
 225         (match Obj.magic ext with
 226          | ERTL.Ertl_new_frame ->
 227            rl_join (rl_hsingleton I8051.registerSPL)
 228              (rl_hsingleton I8051.registerSPH)
 229          | ERTL.Ertl_del_frame ->
 230            rl_join (rl_hsingleton I8051.registerSPL)
 231              (rl_hsingleton I8051.registerSPH)
 232          | ERTL.Ertl_frame_size r -> rl_psingleton r)))
 233 | Joint.Final x -> rl_bottom
 234 | Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
 235
 236 (** val ret_regs : I8051.register Set_adt.set **)
 237 let ret_regs =
 238   Set_adt.set_from_list I8051.registerRets
 239
 240 (** val rl_arg : Joint.psd_argument -> __ **)
 241 let rl_arg = function
 242 | Joint.Reg r -> rl_psingleton r
 243 | Joint.Imm x -> rl_bottom
 244
 245 (** val used :
 246     AST.ident List.list -> Joint.joint_statement -> (Registers.register
 247     Set_adt.set, I8051.register Set_adt.set) Types.prod **)
 248 let used globals = function
 249 | Joint.Sequential (seq, l) ->
 250   (match seq with
 251    | Joint.COST_LABEL clabel -> Obj.magic rl_bottom
 252    | Joint.CALL (f, nparams, x) ->
 253      Obj.magic
 254        (rl_join
 255          (match f with
 256           | Types.Inl x0 -> rl_bottom
 257           | Types.Inr pr ->
 258             rl_join (rl_arg (Obj.magic pr).Types.fst)
 259               (rl_arg (Obj.magic pr).Types.snd))
 260          (Obj.magic { Types.fst = Set_adt.set_empty; Types.snd =
 261            (Set_adt.set_from_list
 262              (Util.prefix (Obj.magic nparams) I8051.registerParams)) }))
 263    | Joint.COND (r, lbl_true) -> Obj.magic (rl_psingleton (Obj.magic r))
 264    | Joint.Step_seq s0 ->
 265      (match s0 with
 266       | Joint.COMMENT x -> Obj.magic rl_bottom
 267       | Joint.MOVE pair_reg ->
 268         let r2 = (Obj.magic pair_reg).Types.snd in
 269         (match r2 with
 270          | Joint.Reg p ->
 271            (match p with
 272             | ERTL.PSD r -> Obj.magic (rl_psingleton r)
 273             | ERTL.HDW r -> Obj.magic (rl_hsingleton r))
 274          | Joint.Imm x -> Obj.magic rl_bottom)
 275       | Joint.POP x -> Obj.magic rl_bottom
 276       | Joint.PUSH r -> Obj.magic (rl_arg (Obj.magic r))
 277       | Joint.ADDRESS (x, x1, x2, x3) -> Obj.magic rl_bottom
 278       | Joint.OPACCS (opaccs, dr1, dr2, sr1, sr2) ->
 279         Obj.magic (rl_join (rl_arg (Obj.magic sr1)) (rl_arg (Obj.magic sr2)))
 280       | Joint.OP1 (op1, r1, r2) -> Obj.magic (rl_psingleton (Obj.magic r2))
 281       | Joint.OP2 (op2, acc_a, r1, r2) ->
 282         Obj.magic
 283           (rl_join (rl_join (rl_arg (Obj.magic r1)) (rl_arg (Obj.magic r2)))
 284             (match op2 with
 285              | BackEndOps.Add -> rl_bottom
 286              | BackEndOps.Addc -> rl_hsingleton I8051.RegisterCarry
 287              | BackEndOps.Sub -> rl_hsingleton I8051.RegisterCarry
 288              | BackEndOps.And -> rl_bottom
 289              | BackEndOps.Or -> rl_bottom
 290              | BackEndOps.Xor -> rl_bottom))
 291       | Joint.CLEAR_CARRY -> Obj.magic rl_bottom
 292       | Joint.SET_CARRY -> Obj.magic rl_bottom
 293       | Joint.LOAD (acc_a, dpl, dph) ->
 294         Obj.magic (rl_join (rl_arg (Obj.magic dpl)) (rl_arg (Obj.magic dph)))
 295       | Joint.STORE (acc_a, dpl, dph) ->
 296         Obj.magic
 297           (rl_join
 298             (rl_join (rl_arg (Obj.magic acc_a)) (rl_arg (Obj.magic dpl)))
 299             (rl_arg (Obj.magic dph)))
 300       | Joint.Extension_seq ext ->
 301         (match Obj.magic ext with
 302          | ERTL.Ertl_new_frame ->
 303            Obj.magic
 304              (rl_join (rl_hsingleton I8051.registerSPL)
 305                (rl_hsingleton I8051.registerSPH))
 306          | ERTL.Ertl_del_frame ->
 307            Obj.magic
 308              (rl_join (rl_hsingleton I8051.registerSPL)
 309                (rl_hsingleton I8051.registerSPH))
 310          | ERTL.Ertl_frame_size r -> Obj.magic rl_bottom)))
 311 | Joint.Final fin ->
 312   (match fin with
 313    | Joint.GOTO l -> Obj.magic rl_bottom
 314    | Joint.RETURN ->
 315      { Types.fst = Set_adt.set_empty; Types.snd =
 316        (Set_adt.set_union (Set_adt.set_from_list I8051.registerCalleeSaved)
 317          ret_regs) }
 318    | Joint.TAILCALL (x, x0) -> assert false (* absurd case *))
 319 | Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
 320
 321 (** val eliminable_step :
 322     AST.ident List.list -> __ -> Joint.joint_step -> Bool.bool **)
 323 let eliminable_step globals l s =
 324   let pliveafter = (Obj.magic l).Types.fst in
 325   let hliveafter = (Obj.magic l).Types.snd in
 326   (match s with
 327    | Joint.COST_LABEL x -> Bool.False
 328    | Joint.CALL (x, x0, x1) -> Bool.False
 329    | Joint.COND (x, x0) -> Bool.False
 330    | Joint.Step_seq s0 ->
 331      (match s0 with
 332       | Joint.COMMENT x -> Bool.False
 333       | Joint.MOVE pair_reg ->
 334         Bool.notb
 335           (match (Obj.magic pair_reg).Types.fst with
 336            | ERTL.PSD p1 ->
 337              Set_adt.set_member
 338                (Identifiers.eq_identifier PreIdentifiers.RegisterTag) p1
 339                pliveafter
 340            | ERTL.HDW h1 ->
 341              Set_adt.set_member I8051.eq_Register h1 hliveafter)
 342       | Joint.POP x -> Bool.False
 343       | Joint.PUSH x -> Bool.False
 344       | Joint.ADDRESS (x, x1, r1, r2) ->
 345         Bool.notb
 346           (Bool.orb
 347             (Set_adt.set_member
 348               (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
 349               (Obj.magic r1) pliveafter)
 350             (Set_adt.set_member
 351               (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
 352               (Obj.magic r2) pliveafter))
 353       | Joint.OPACCS (opaccs, dr1, dr2, sr1, sr2) ->
 354         Bool.notb
 355           (Bool.orb
 356             (Bool.orb
 357               (Set_adt.set_member
 358                 (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
 359                 (Obj.magic dr1) pliveafter)
 360               (Set_adt.set_member
 361                 (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
 362                 (Obj.magic dr2) pliveafter))
 363             (Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
 364               hliveafter))
 365       | Joint.OP1 (op1, r1, r2) ->
 366         Bool.notb
 367           (Set_adt.set_member
 368             (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
 369             (Obj.magic r1) pliveafter)
 370       | Joint.OP2 (op2, r1, r2, r3) ->
 371         Bool.notb
 372           (Bool.orb
 373             (match op2 with
 374              | BackEndOps.Add ->
 375                Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
 376                  hliveafter
 377              | BackEndOps.Addc ->
 378                Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
 379                  hliveafter
 380              | BackEndOps.Sub ->
 381                Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
 382                  hliveafter
 383              | BackEndOps.And -> Bool.False
 384              | BackEndOps.Or -> Bool.False
 385              | BackEndOps.Xor -> Bool.False)
 386             (Set_adt.set_member
 387               (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
 388               (Obj.magic r1) pliveafter))
 389       | Joint.CLEAR_CARRY -> Bool.False
 390       | Joint.SET_CARRY -> Bool.False
 391       | Joint.LOAD (acc_a, dpl, dph) ->
 392         Bool.notb
 393           (Set_adt.set_member
 394             (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
 395             (Obj.magic acc_a) pliveafter)
 396       | Joint.STORE (x, x0, x1) -> Bool.False
 397       | Joint.Extension_seq ext ->
 398         (match Obj.magic ext with
 399          | ERTL.Ertl_new_frame -> Bool.False
 400          | ERTL.Ertl_del_frame -> Bool.False
 401          | ERTL.Ertl_frame_size r ->
 402            Bool.notb
 403              (Set_adt.set_member
 404                (Identifiers.eq_identifier PreIdentifiers.RegisterTag) r
 405                pliveafter))))
 406
 407 (** val eliminable :
 408     AST.ident List.list -> __ -> Joint.joint_statement -> Bool.bool **)
 409 let eliminable globals l s =
 410   let pliveafter = (Obj.magic l).Types.fst in
 411   let hliveafter = (Obj.magic l).Types.snd in
 412   (match s with
 413    | Joint.Sequential (seq, x) -> eliminable_step globals l seq
 414    | Joint.Final x -> Bool.False
 415    | Joint.FCOND (x0, x1, x2) -> Bool.False)
 416
 417 (** val statement_semantics :
 418     AST.ident List.list -> Joint.joint_statement -> __ -> __ **)
 419 let statement_semantics globals stmt liveafter =
 420   match eliminable globals liveafter stmt with
 421   | Bool.True -> liveafter
 422   | Bool.False ->
 423     rl_join (rl_diff liveafter (defined globals stmt))
 424       (Obj.magic (used globals stmt))
 425
 426 (** val livebefore :
 427     AST.ident List.list -> Joint.joint_internal_function ->
 428     Fixpoints.valuation -> Fixpoints.valuation **)
 429 let livebefore globals int_fun liveafter label =
 430   match Identifiers.lookup PreIdentifiers.LabelTag
 431           (Obj.magic int_fun.Joint.joint_if_code) label with
 432   | Types.None -> rl_bottom
 433   | Types.Some stmt -> statement_semantics globals stmt (liveafter label)
 434
 435 (** val liveafter :
 436     AST.ident List.list -> Joint.joint_internal_function ->
 437     PreIdentifiers.identifier -> Fixpoints.valuation -> __ **)
 438 let liveafter globals int_fun label liveafter0 =
 439   match Identifiers.lookup PreIdentifiers.LabelTag
 440           (Obj.magic int_fun.Joint.joint_if_code) label with
 441   | Types.None -> rl_bottom
 442   | Types.Some stmt ->
 443     List.fold rl_join rl_bottom (fun successor -> Bool.True)
 444       (fun successor -> livebefore globals int_fun liveafter0 successor)
 445       (Joint.stmt_labels { Joint.uns_pars = (Joint.g_u_pars ERTL.eRTL);
 446         Joint.succ_label = (Obj.magic (fun x -> Types.Some x));
 447         Joint.has_fcond = Bool.False } globals stmt)
 448
 449 (** val analyse_liveness :
 450     Fixpoints.fixpoint_computer -> AST.ident List.list ->
 451     Joint.joint_internal_function -> Fixpoints.fixpoint **)
 452 let analyse_liveness the_fixpoint globals int_fun =
 453   the_fixpoint register_lattice (liveafter globals int_fun)
 454
 455 type vertex = (Registers.register, I8051.register) Types.sum
 456
 457 (** val plives : Registers.register -> __ -> Bool.bool **)
 458 let plives vertex0 prop =
 459   Set_adt.set_member (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
 460     vertex0 (Obj.magic prop).Types.fst
 461
 462 (** val hlives : I8051.register -> __ -> Bool.bool **)
 463 let hlives vertex0 prop =
 464   Set_adt.set_member I8051.eq_Register vertex0 (Obj.magic prop).Types.snd
 465
 466 (** val lives : vertex -> __ -> Bool.bool **)
 467 let lives = function
 468 | Types.Inl v -> plives v
 469 | Types.Inr v -> hlives v
 470