Changing to an opaq record in BTL info, this is a broken commit

1 files changed, 81 insertions, 77 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 44c25b75..ca727f82 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -23,29 +23,32 @@ Require Import RTL Op Registers OptionMonad.
 Definition exit := node.  (* we may generalize this with register renamings at exit, 
                              like in "phi" nodes of SSA-form *)
 
-(* node_info is a ghost record to provide and transfert information through oracles *)
-Record node_info := {
-  _pos: node
-}.
+(* inst_info is a ghost record to provide instruction information through oracles *)
+Parameter inst_info: Set.
+Extract Constant inst_info => "BTLaux.inst_info".
+
+(* block_info is a ghost record to provide block information through oracles *)
+Parameter block_info: Set.
+Extract Constant block_info => "BTLaux.block_info".
 
 (** final instructions (that stops block execution) *)
 Inductive final: Type :=
   | Bgoto (succ:exit) (** No operation -- just branch to [succ]. *)
-  | Breturn (res: option reg) (ni: node_info)
+  | Breturn (res: option reg)
       (** terminates the execution of the current function.  It returns the value of the given
           register, or [Vundef] if none is given. *)
-  | Bcall (sig: signature) (fn: reg + ident) (args:list reg) (dest:reg) (succ:exit) (ni: node_info)
+  | Bcall (sig: signature) (fn: reg + ident) (args:list reg) (dest:reg) (succ:exit)
       (** invokes the function determined by [fn] (either a function pointer found in a register or a
           function name), giving it the values of registers [args] as arguments.
           It stores the return value in [dest] and branches to [succ]. *)
-  | Btailcall (sig:signature) (fn: reg + ident) (args: list reg) (ni: node_info)
+  | Btailcall (sig:signature) (fn: reg + ident) (args: list reg)
       (**  performs a function invocation in tail-call position 
           (the current function terminates after the call, returning the result of the callee)  
       *)
-  | Bbuiltin (ef:external_function) (args:list (builtin_arg reg)) (dest:builtin_res reg) (succ:exit) (ni: node_info)
+  | Bbuiltin (ef:external_function) (args:list (builtin_arg reg)) (dest:builtin_res reg) (succ:exit)
       (** calls the built-in function identified by [ef], giving it the values of [args] as arguments.
           It stores the return value in [dest] and branches to [succ]. *)
-  | Bjumptable (arg:reg) (tbl:list exit) (ni: node_info)
+  | Bjumptable (arg:reg) (tbl:list exit)
       (** [Bjumptable arg tbl] transitions to the node that is the [n]-th
           element of the list [tbl], where [n] is the unsigned integer value of register [arg]. *)
   .
@@ -53,16 +56,16 @@ Inductive final: Type :=
 (* instruction block *)
 Inductive iblock: Type :=
 (* final instructions that stops block execution *)
-  | BF (fi: final)
+  | BF (fi: final) (iinfo: inst_info)
 (* basic instructions that continues block execution, except when aborting *)
-  | Bnop (ni: node_info) (* nop instruction *)
-  | Bop (op:operation) (args:list reg) (dest:reg) (ni: node_info)
+  | Bnop (iinfo: inst_info) (* nop instruction *)
+  | Bop (op:operation) (args:list reg) (dest:reg) (iinfo: inst_info)
       (** performs the arithmetic operation [op] over the values of registers [args], stores the result in [dest] *)
-  | Bload (trap:trapping_mode) (chunk:memory_chunk) (addr:addressing) (args:list reg) (dest:reg) (ni: node_info)
+  | Bload (trap:trapping_mode) (chunk:memory_chunk) (addr:addressing) (args:list reg) (dest:reg) (iinfo: inst_info)
       (** loads a [chunk] quantity from the address determined by the addressing mode [addr] 
           and the values of the [args] registers, stores the quantity just read into [dest].
           If trap=NOTRAP, then failures lead to a default value written to [dest]. *)
-  | Bstore (chunk:memory_chunk) (addr:addressing) (args:list reg) (src:reg) (ni: node_info)
+  | Bstore (chunk:memory_chunk) (addr:addressing) (args:list reg) (src:reg) (iinfo: inst_info)
       (** stores the value of register [src] in the [chunk] quantity at the
           the address determined by the addressing mode [addr] and the
           values of the [args] registers. *)
@@ -70,13 +73,13 @@ Inductive iblock: Type :=
   | Bseq (b1 b2: iblock)
       (** starts by running [b1] and stops here if execution of [b1] has reached a final instruction or aborted
           or continue with [b2] otherwise *)
-  | Bcond (cond:condition) (args:list reg) (ifso ifnot: iblock) (info:option bool) (ni: node_info)
+  | Bcond (cond:condition) (args:list reg) (ifso ifnot: iblock) (iinfo: inst_info)
       (** evaluates the boolean condition [cond] over the values of registers [args].  
           If the condition is true, it continues on [ifso].
           If the condition is false, it continues on [ifnot].
           [info] is a ghost field there to provide information relative to branch prediction. *)
   .
-Coercion BF: final >-> iblock.
+Coercion BF: final >-> Funclass.
 
 
 (** NB: - a RTL [(Inop pc)] ending a branch of block is encoded by [(Bseq Bnop (Bgoto pc))].
@@ -88,7 +91,8 @@ Coercion BF: final >-> iblock.
 
 Record iblock_info := { 
   entry: iblock;
-  input_regs: Regset.t (* extra liveness information ignored by BTL semantics *)
+  input_regs: Regset.t; (* extra liveness information ignored by BTL semantics *)
+  binfo: block_info (* Ghost field used in oracles *)
 }.
 
 Definition code: Type := PTree.t iblock_info.
@@ -199,24 +203,24 @@ Inductive has_loaded sp rs m chunk addr args v: trapping_mode -> Prop :=
 
 (** internal big-step execution of one iblock *)
 Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option final -> Prop :=
-  | exec_final rs m fin: iblock_istep sp rs m (BF fin) rs m (Some fin)
-  | exec_nop rs m ni: iblock_istep sp rs m (Bnop ni) rs m None
-  | exec_op rs m op args res v ni
+  | exec_final rs m fin iinfo: iblock_istep sp rs m (BF fin iinfo) rs m (Some fin)
+  | exec_nop rs m iinfo: iblock_istep sp rs m (Bnop iinfo) rs m None
+  | exec_op rs m op args res v iinfo
      (EVAL: eval_operation ge sp op rs##args m = Some v)
-     : iblock_istep sp rs m (Bop op args res ni) (rs#res <- v) m None
-  | exec_load_TRAP rs m chunk addr args dst a v ni
+     : iblock_istep sp rs m (Bop op args res iinfo) (rs#res <- v) m None
+  | exec_load_TRAP rs m chunk addr args dst a v iinfo
      (EVAL: eval_addressing ge sp addr rs##args = Some a)
      (LOAD: Mem.loadv chunk m a = Some v)
-     : iblock_istep sp rs m (Bload TRAP chunk addr args dst ni) (rs#dst <- v) m None
+     : iblock_istep sp rs m (Bload TRAP chunk addr args dst iinfo) (rs#dst <- v) m None
 (* TODO: replace [exec_load_TRAP] above by this one. See "new scheme" for "NOTRAP" above
   | exec_load rs m trap chunk addr args dst v
       (LOAD: has_loaded sp rs m chunk addr args v trap)
      : iblock_istep sp rs m (Bload trap chunk addr args dst) (rs#dst <- v) m None
 *)
-  | exec_store rs m chunk addr args src a m' ni
+  | exec_store rs m chunk addr args src a m' iinfo
      (EVAL: eval_addressing ge sp addr rs##args = Some a)
      (STORE: Mem.storev chunk m a rs#src = Some m')
-     : iblock_istep sp rs m (Bstore chunk addr args src ni) rs m' None
+     : iblock_istep sp rs m (Bstore chunk addr args src iinfo) rs m' None
   | exec_seq_stop rs m b1 b2 rs' m' fin
      (EXEC: iblock_istep sp rs m b1 rs' m' (Some fin))
      : iblock_istep sp rs m (Bseq b1 b2) rs' m' (Some fin)
@@ -224,10 +228,10 @@ Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option fi
      (EXEC1: iblock_istep sp rs m b1 rs1 m1 None)
      (EXEC2: iblock_istep sp rs1 m1 b2 rs' m' ofin)
      : iblock_istep sp rs m (Bseq b1 b2) rs' m' ofin
-  | exec_cond rs m cond args ifso ifnot i b rs' m' ofin ni
+  | exec_cond rs m cond args ifso ifnot b rs' m' ofin iinfo
      (EVAL: eval_condition cond rs##args m = Some b)
      (EXEC: iblock_istep sp rs m (if b then ifso else ifnot) rs' m' ofin)
-     : iblock_istep sp rs m (Bcond cond args ifso ifnot i ni) rs' m' ofin
+     : iblock_istep sp rs m (Bcond cond args ifso ifnot iinfo) rs' m' ofin
   .
 Local Hint Constructors iblock_istep: core.
 
@@ -236,7 +240,7 @@ Lemma [iblock_istep_run_equiv] below provides a proof that "relation" [iblock_is
 *)
 Fixpoint iblock_istep_run sp ib rs m: option outcome := 
   match ib with
-  | BF fin =>
+  | BF fin _ =>
       Some {| _rs := rs; _m := m; _fin := Some fin |}
   (* basic instructions *)
   | Bnop _ =>
@@ -261,7 +265,7 @@ Fixpoint iblock_istep_run sp ib rs m: option outcome :=
       | None => iblock_istep_run sp b2 out1.(_rs) out1.(_m)
       | _ => Some out1 (* stop execution on the 1st final instruction *)
       end
-  | Bcond cond args ifso ifnot _ _ =>
+  | Bcond cond args ifso ifnot _ =>
       SOME b <- eval_condition cond rs##args m IN
       iblock_istep_run sp (if b then ifso else ifnot) rs m
   end.
@@ -280,32 +284,32 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop :=
   | exec_Bgoto pc:
       final_step stack f sp rs m (Bgoto pc) E0
                  (State stack f sp pc rs m)
-  | exec_Breturn or stk m' ni:
+  | exec_Breturn or stk m':
       sp = (Vptr stk Ptrofs.zero) ->
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-      final_step stack f sp rs m (Breturn or ni)
+      final_step stack f sp rs m (Breturn or)
         E0 (Returnstate stack (regmap_optget or Vundef rs) m')
-  | exec_Bcall sig ros args res pc' fd ni:
+  | exec_Bcall sig ros args res pc' fd:
       find_function ros rs = Some fd ->
       funsig fd = sig ->
-      final_step stack f sp rs m (Bcall sig ros args res pc' ni)
+      final_step stack f sp rs m (Bcall sig ros args res pc')
         E0 (Callstate (Stackframe res f sp pc' rs :: stack) fd rs##args m)
-  | exec_Btailcall sig ros args stk m' fd ni:
+  | exec_Btailcall sig ros args stk m' fd:
       find_function ros rs = Some fd ->
       funsig fd = sig ->
       sp = (Vptr stk Ptrofs.zero) ->
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-      final_step stack f sp rs m (Btailcall sig ros args ni)
+      final_step stack f sp rs m (Btailcall sig ros args)
         E0 (Callstate stack fd rs##args m')
-  | exec_Bbuiltin ef args res pc' vargs t vres m' ni:
+  | exec_Bbuiltin ef args res pc' vargs t vres m':
       eval_builtin_args ge (fun r => rs#r) sp m args vargs ->
       external_call ef ge vargs m t vres m' ->
-      final_step stack f sp rs m (Bbuiltin ef args res pc' ni)
+      final_step stack f sp rs m (Bbuiltin ef args res pc')
          t (State stack f sp pc' (regmap_setres res vres rs) m')
-  | exec_Bjumptable arg tbl n pc' ni:
+  | exec_Bjumptable arg tbl n pc':
       rs#arg = Vint n ->
       list_nth_z tbl (Int.unsigned n) = Some pc' ->
-      final_step stack f sp rs m (Bjumptable arg tbl ni)
+      final_step stack f sp rs m (Bjumptable arg tbl)
         E0 (State stack f sp pc' rs m)
 .
 
@@ -393,16 +397,16 @@ Inductive match_final_inst (dupmap: PTree.t node): final -> instruction -> Prop
   | mfi_goto pc pc':
       dupmap!pc = (Some pc') -> match_final_inst dupmap (Bgoto pc) (Inop pc')
 *)
-  | mfi_return or ni: match_final_inst dupmap (Breturn or ni) (Ireturn or)
-  | mfi_call pc pc' s ri lr r ni:
-      dupmap!pc = (Some pc') -> match_final_inst dupmap (Bcall s ri lr r pc ni) (Icall s ri lr r pc')
-  | mfi_tailcall s ri lr ni:
-      match_final_inst dupmap (Btailcall s ri lr ni) (Itailcall s ri lr)
-  | mfi_builtin pc pc' ef la br ni:
-      dupmap!pc = (Some pc') -> match_final_inst dupmap (Bbuiltin ef la br pc ni) (Ibuiltin ef la br pc')
-  | mfi_jumptable ln ln' r ni:
+  | mfi_return or: match_final_inst dupmap (Breturn or) (Ireturn or)
+  | mfi_call pc pc' s ri lr r:
+      dupmap!pc = (Some pc') -> match_final_inst dupmap (Bcall s ri lr r pc) (Icall s ri lr r pc')
+  | mfi_tailcall s ri lr:
+      match_final_inst dupmap (Btailcall s ri lr) (Itailcall s ri lr)
+  | mfi_builtin pc pc' ef la br:
+      dupmap!pc = (Some pc') -> match_final_inst dupmap (Bbuiltin ef la br pc) (Ibuiltin ef la br pc')
+  | mfi_jumptable ln ln' r:
       list_forall2 (fun pc pc' => (dupmap!pc = (Some pc'))) ln ln' ->
-      match_final_inst dupmap (Bjumptable r ln ni) (Ijumptable r ln')
+      match_final_inst dupmap (Bjumptable r ln) (Ijumptable r ln')
 .
 
 Inductive is_join_opt {A}: (option A) -> (option A) -> (option A) -> Prop :=
@@ -417,25 +421,25 @@ Inductive is_join_opt {A}: (option A) -> (option A) -> (option A) -> Prop :=
    - if [opc] is [Some pc'], this means that all branches of the block that do not exit, join on [pc'].
 *)
 Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> iblock -> (option node) -> Prop :=
-  | mib_BF isfst fi pc i:
+  | mib_BF isfst fi pc i iinfo:
       cfg!pc = Some i ->
       match_final_inst dupmap fi i ->
-      match_iblock dupmap cfg isfst pc (BF fi) None
-  | mib_nop isfst pc pc' ni:
+      match_iblock dupmap cfg isfst pc (BF fi iinfo) None
+  | mib_nop isfst pc pc' iinfo:
       cfg!pc = Some (Inop pc') ->
-      match_iblock dupmap cfg isfst pc (Bnop ni) (Some pc')
-  | mib_op isfst pc pc' op lr r ni:
+      match_iblock dupmap cfg isfst pc (Bnop iinfo) (Some pc')
+  | mib_op isfst pc pc' op lr r iinfo:
       cfg!pc = Some (Iop op lr r pc') ->
-      match_iblock dupmap cfg isfst pc (Bop op lr r ni) (Some pc')
-  | mib_load isfst pc pc' m a lr r ni:
+      match_iblock dupmap cfg isfst pc (Bop op lr r iinfo) (Some pc')
+  | mib_load isfst pc pc' m a lr r iinfo:
       cfg!pc = Some (Iload TRAP m a lr r pc') -> 
-      match_iblock dupmap cfg isfst pc (Bload TRAP m a lr r ni) (Some pc')
-  | mib_store isfst pc pc' m a lr r ni:
+      match_iblock dupmap cfg isfst pc (Bload TRAP m a lr r iinfo) (Some pc')
+  | mib_store isfst pc pc' m a lr r iinfo:
       cfg!pc = Some (Istore m a lr r pc') -> 
-      match_iblock dupmap cfg isfst pc (Bstore m a lr r ni) (Some pc')
-  | mib_exit pc pc': 
+      match_iblock dupmap cfg isfst pc (Bstore m a lr r iinfo) (Some pc')
+  | mib_exit pc pc' iinfo: 
       dupmap!pc = (Some pc') ->
-      match_iblock dupmap cfg false pc' (Bgoto pc) None
+      match_iblock dupmap cfg false pc' (BF (Bgoto pc) iinfo) None
       (* NB: on RTL side, we exit the block by a "basic" instruction (or Icond). 
          Thus some step should have been executed before [pc'] in the RTL code *)
   | mib_seq_Some isfst b1 b2 pc1 pc2 opc:
@@ -450,12 +454,12 @@ Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> i
          And the verifier could fail if there is such dead code!
       *)
 *)
-  | mib_cond isfst c lr bso bnot pcso pcnot pc opc1 opc2 opc i i' ni:
-      cfg!pc = Some (Icond c lr pcso pcnot i') ->
+  | mib_cond isfst c lr bso bnot pcso pcnot pc opc1 opc2 opc i iinfo:
+      cfg!pc = Some (Icond c lr pcso pcnot i) ->
       match_iblock dupmap cfg false pcso bso opc1 ->
       match_iblock dupmap cfg false pcnot bnot opc2 ->
       is_join_opt opc1 opc2 opc ->
-      match_iblock dupmap cfg isfst pc (Bcond c lr bso bnot i ni) opc
+      match_iblock dupmap cfg isfst pc (Bcond c lr bso bnot iinfo) opc
   .
 
 Definition match_cfg dupmap (cfg: code) (cfg':RTL.code): Prop :=
@@ -528,21 +532,21 @@ Global Opaque builtin_res_eq_pos.
 
 Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) :=
   match ib with
-  | BF fi =>
+  | BF fi _ =>
       match fi with
       | Bgoto pc1 =>
           do u <- verify_is_copy dupmap pc1 pc;
           if negb isfst then
             OK None
           else Error (msg "BTL.verify_block: isfst is true Bgoto")
-      | Breturn or _ =>
+      | Breturn or =>
           match cfg!pc with
           | Some (Ireturn or') =>
               if option_eq Pos.eq_dec or or' then OK None
               else Error (msg "BTL.verify_block: different opt reg in Breturn")
           | _ => Error (msg "BTL.verify_block: incorrect cfg Breturn")
           end
-      | Bcall s ri lr r pc1 _ =>
+      | Bcall s ri lr r pc1 =>
           match cfg!pc with
           | Some (Icall s' ri' lr' r' pc2) =>
               do u <- verify_is_copy dupmap pc1 pc2;
@@ -556,7 +560,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
               else Error (msg "BTL.verify_block: different signatures in Bcall")
           | _ => Error (msg "BTL.verify_block: incorrect cfg Bcall")
           end
-      | Btailcall s ri lr _ =>
+      | Btailcall s ri lr =>
           match cfg!pc with
           | Some (Itailcall s' ri' lr') =>
               if (signature_eq s s') then
@@ -567,7 +571,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
               else Error (msg "BTL.verify_block: different signatures in Btailcall")
           | _ => Error (msg "BTL.verify_block: incorrect cfg Btailcall")
           end
-      | Bbuiltin ef la br pc1 _ =>
+      | Bbuiltin ef la br pc1 =>
           match cfg!pc with
           | Some (Ibuiltin ef' la' br' pc2) =>
               do u <- verify_is_copy dupmap pc1 pc2;
@@ -579,7 +583,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
               else Error (msg "BTL.verify_block: different ef in Bbuiltin")
           | _ => Error (msg "BTL.verify_block: incorrect cfg Bbuiltin")
           end
-      | Bjumptable r ln _ =>
+      | Bjumptable r ln =>
           match cfg!pc with
           | Some (Ijumptable r' ln') =>
               do u <- verify_is_copy_list dupmap ln ln';
@@ -641,7 +645,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
           verify_block dupmap cfg false pc' b2
       | None => Error (msg "BTL.verify_block: None next pc in Bseq (deadcode)")
       end
-  | Bcond c lr bso bnot i _ =>
+  | Bcond c lr bso bnot _ =>
       match cfg!pc with
       | Some (Icond c' lr' pcso pcnot i') =>
           if (list_eq_dec Pos.eq_dec lr lr') then
@@ -793,13 +797,13 @@ Definition verify_function dupmap f f' : res unit :=
 
 Definition is_goto (ib: iblock): bool :=
   match ib with
-  | Bgoto _ => true
+  | BF (Bgoto _) _ => true
   | _ => false
   end.
 
 Definition is_atom (ib: iblock): bool :=
  match ib with
- | Bseq _ _ | Bcond _ _ _ _ _ _ => false 
+ | Bseq _ _ | Bcond _ _ _ _ _ => false 
  | _ => true
  end.
 
@@ -809,10 +813,10 @@ Inductive is_expand: iblock -> Prop :=
      is_atom ib1 = true ->
      is_expand ib2 -> 
      is_expand (Bseq ib1 ib2)
-  | exp_Bcond cond args ib1 ib2 i ni:
+  | exp_Bcond cond args ib1 ib2 iinfo:
      is_expand ib1 ->
      is_expand ib2 -> 
-     is_expand (Bcond cond args ib1 ib2 i ni)
+     is_expand (Bcond cond args ib1 ib2 iinfo)
   | exp_others ib:
      is_atom ib = true ->
      is_expand ib
@@ -822,9 +826,9 @@ Local Hint Constructors is_expand: core.
 Fixpoint expand (ib: iblock) (k: option iblock): iblock :=
   match ib with
   | Bseq ib1 ib2 => expand ib1 (Some (expand ib2 k))
-  | Bcond cond args ib1 ib2 i ni => 
-     Bcond cond args (expand ib1 k) (expand ib2 k) i ni
-  | BF fin => fin
+  | Bcond cond args ib1 ib2 iinfo => 
+     Bcond cond args (expand ib1 k) (expand ib2 k) iinfo
+  | BF fin iinfo => BF fin iinfo
   | ib => 
     match k with 
     | None => ib