include "ASM/ASM.ma".
include "ASM/Arithmetic.ma".
include "ASM/Fetch.ma".
include "ASM/Interpret.ma".
include "common/StructuredTraces.ma".

definition current_instruction0 ≝
  λmem,pc. \fst (\fst (fetch … mem pc)).

definition current_instruction ≝
 λs:Status. current_instruction0 (code_memory … s) (program_counter … s).

definition ASM_classify0: instruction → status_class ≝
 λi.
  match i with
   [ RealInstruction pre ⇒
     match pre with
      [ RET ⇒ cl_return
      | JZ _ ⇒ cl_jump
      | JNZ _ ⇒ cl_jump
      | JC _ ⇒ cl_jump
      | JNC _ ⇒ cl_jump
      | JB _ _ ⇒ cl_jump
      | JNB _ _ ⇒ cl_jump
      | JBC _ _ ⇒ cl_jump
      | CJNE _ _ ⇒ cl_jump
      | DJNZ _ _ ⇒ cl_jump
      | _ ⇒ cl_other
      ]
   | ACALL _ ⇒ cl_call
   | LCALL _ ⇒ cl_call
   | JMP _ ⇒ cl_call
   | AJMP _ ⇒ cl_jump
   | LJMP _ ⇒ cl_jump
   | SJMP _ ⇒ cl_jump
   | _ ⇒ cl_other
   ].

definition ASM_classify: Status → status_class ≝
 λs.ASM_classify0 (current_instruction s).

definition current_instruction_is_labelled ≝
  λcost_labels: BitVectorTrie costlabel 16.
  λs: Status.
  let pc ≝ program_counter … s in
    match lookup_opt … pc cost_labels with
    [ None ⇒ False
    | _    ⇒ True
    ].

definition label_of_current_instruction:
 BitVectorTrie costlabel 16 → Status → list costlabel
 ≝
  λcost_labels,s.
  let pc ≝ program_counter … s in
    match lookup_opt … pc cost_labels with
    [ None ⇒ []
    | Some l ⇒ [l]
    ].

definition next_instruction_properly_relates_program_counters ≝
  λbefore: Status.
  λafter : Status.
  let size ≝ current_instruction_cost before in
  let pc_before ≝ program_counter … before in
  let pc_after ≝ program_counter … after in
  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
    sum = pc_after.

definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝
 λcost_labels.
  mk_abstract_status
   Status
   (λs,s'. eject … (execute_1 s) = s')
   (λs,class. ASM_classify s = class)
   (current_instruction_is_labelled cost_labels)
   next_instruction_properly_relates_program_counters.

(* To be moved in ASM/arithmetic.ma *)
definition addr16_of_addr11: Word → Word11 → Word ≝
  λpc: Word.
  λa: Word11.
  let 〈pc_upper, ignore〉 ≝ split … 8 8 pc in
  let 〈n1, n2〉 ≝ split … 4 4 pc_upper in
  let 〈b123, b〉 ≝ split … 3 8 a in
  let b1 ≝ get_index_v … b123 0 ? in
  let b2 ≝ get_index_v … b123 1 ? in
  let b3 ≝ get_index_v … b123 2 ? in
  let p5 ≝ get_index_v … n2 0 ? in
    (n1 @@ [[ p5; b1; b2; b3 ]]) @@ b.
  //
qed.

let rec block_cost
  (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    (pc: Word) (program_size: nat) on program_size : nat ≝
  match program_size with
  [ O ⇒ 0
  | S program_size ⇒
    let 〈instr,newpc,ticks〉 ≝ fetch … mem pc in
    match lookup_opt … newpc cost_labels with
     [ None ⇒
        match ASM_classify0 instr with
         [ cl_jump ⇒ ticks
         | cl_call ⇒ ticks + block_cost mem cost_labels newpc program_size
         | cl_return ⇒ ticks
         | cl_other ⇒ ticks + block_cost mem cost_labels newpc program_size
         ]
     | Some _ ⇒ ticks ]].

let rec traverse_code_internal
  (program: list Byte) (mem: BitVectorTrie Byte 16)
    (cost_labels: BitVectorTrie costlabel 16) (pc: Word) (program_size: nat)
      on program: identifier_map CostTag nat ≝
 let 〈instr,newpc,ticks〉 ≝ fetch … mem pc in
 match program with
 [ nil ⇒ empty_map …
 | cons hd tl ⇒
   match lookup_opt … pc cost_labels with
   [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size
   | Some lbl ⇒
     let cost ≝ block_cost mem cost_labels pc program_size in
     let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in
       add … cost_mapping lbl cost ]].

definition traverse_code ≝
  λprogram: list Byte.
  λmem: BitVectorTrie Byte 16.
  λcost_labels.
  λprogram_size: nat.
    traverse_code_internal program mem cost_labels (zero …) program_size.

definition compute_costs ≝
  λprogram: list Byte.
  λcost_labels: BitVectorTrie costlabel 16.
  λhas_main: bool.
  let program_size ≝ |program| in
  let memory ≝ load_code_memory program in
   traverse_code program memory cost_labels program_size.