(* Type of values used in the dynamic semantics of the back-end intermediate
   languages, and the memory model for the whole compiler. Inspired by
   common/Values.ma, adapted from Compcert *)

include "common/Pointers.ma".
include "utilities/hide.ma".

definition cpointer ≝ Σp.ptype p = Code.
definition xpointer ≝ Σp.ptype p = XData.
unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).
unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer 	(λp.ptype p = XData).

(* this is like a code pointer, but with unbounded offset.
   used only in the back-end, they become code pointers in LIN → ASM *)
record program_counter : Type[0] ≝
  { pc_block : Σb : block.block_region b = Code
  ; pc_offset : Pos
  }.

definition eq_program_counter : program_counter → program_counter → bool ≝
λpc1,pc2.eq_block (pc_block pc1) (pc_block pc2) ∧
         eqb (pc_offset pc1) (pc_offset pc2).

lemma eq_program_counter_elim : ∀P:bool→Prop.
  ∀pc1,pc2.(pc1=pc2→P true)→(pc1≠pc2→P false)→P (eq_program_counter pc1 pc2).
#P ** #bl1 #H1 #o1 ** #bl2 #H2 #o2
#Heq #Hneq whd in ⊢ (?%);
@eq_block_elim #EQ1
[ @eqb_elim #EQ2 ]
[ @Heq destruct %
|*: @Hneq % #ABS destruct
  [ @(absurd ?? EQ2) | @(absurd ?? EQ1) ] %
] qed.

lemma reflexive_eq_program_counter : ∀pc.eq_program_counter pc pc = true.
** #bl1 #H1 #o1 whd in ⊢ (??%?); >eq_block_b_b >eqb_n_n % qed.

definition bitvector_from_pos :
  ∀n.Pos → BitVector n ≝
  λn,p.bitvector_of_Z n (Zpred (pos p)).

definition pos_from_bitvector :
  ∀n.BitVector n → Pos ≝
  λn,v.
  match Zsucc (Z_of_unsigned_bitvector n v)
  return λx.Zsucc (Z_of_unsigned_bitvector n v) = x → ?
  with
  [ OZ ⇒ λprf.⊥
  | pos x ⇒ λ_. x
  | neg x ⇒ λprf.⊥
  ] (refl …).
@hide_prf
elim v in prf;
[2,4: #n * #v #IH [2,4: assumption ]] normalize #ABS destruct(ABS) qed.

definition cpointer_of_pc : program_counter → option cpointer ≝
  λpc.
  let pc_off ≝ pc_offset pc in
  if leb pc_off (two_power_nat offset_size) then
    return «mk_pointer (pc_block pc) (mk_offset (bitvector_from_pos … pc_off)),?»
  else
    None ?.
elim (pc_block pc) #bl #H @H qed.

record part (*r: region*): Type[0] ≝
 { part_no:> nat
 ; part_no_ok: part_no < size_pointer (*r*)
 }.

definition part_from_sig : (Σn:ℕ.n<size_pointer) → part ≝
λn_sig : Σn.n<size_pointer.mk_part n_sig (pi2 … n_sig).

coercion sig_to_part : ∀n_sig:Σn:ℕ.n<size_pointer.part ≝
part_from_sig on _n_sig:Σn.n<size_pointer to part.

(* Byte-sized values used in the back-end.
   Values larger than a single Byte are represented via their parts.
   Values are either:
  - machine integers (Bytes)
  - parts of a pointer seen as a triple giving the representation of the
    pointer (in terms of the memory regions such a pointer could address),
    a memory address and an integer offset with respect to this address;
  - a null pointer: the region denotes the pointer size
  - the [BVundef] value denoting an arbitrary bit pattern, such as the
    value of an uninitialized variable
  - [BVXor] is a formal XOR between (possibly null) pointer parts
  - [BVnonzero] is any nonzero value
*)

inductive beval: Type[0] ≝
  | BVundef: beval
  | BVnonzero: beval
  | BVXor: option pointer → option pointer → part → beval (* option pointer ≈ pointer + null *)
  | BVByte: Byte → beval
  | BVnull: (*∀r:region.*) part  → beval
  | BVptr: pointer → part → beval
  | BVpc: program_counter → part → beval. (* only used in back end, needed to separate
                                      program counters that go in the stack from
                                      function pointers, as they are linked with
                                      different relations in some passes *)

definition eq_bv_suffix : ∀n,m,p.
  BitVector (n + p) → BitVector (m + p) → bool ≝
λn,m,p,v1,v2.
let b1 ≝ \snd (vsplit … v1) in
let b2 ≝ \snd (vsplit … v2) in
eq_bv … b1 b2.

include alias "arithmetics/nat.ma".

axiom CorruptedPointer: String.

(* CSC: use vectors in place of lists? Or even better products of tuples
   (more easily pattern matchable in the finite case)? requires one more parameter *)
definition pointer_of_bevals: list beval → res pointer ≝
 λl.
 match l with
  [ nil ⇒ Error … [MSG CorruptedPointer]
  | cons bv1 tl ⇒
    match tl with
    [ nil ⇒ Error … [MSG CorruptedPointer]
    | cons bv2 tl' ⇒
      match tl' with
      [ cons _ _ ⇒ Error … [MSG CorruptedPointer]
      | nil ⇒
        match bv1 with
        [ BVptr ptr1 p1 ⇒
          match bv2 with
          [ BVptr ptr2 p2 ⇒
            if eqb p1 0 ∧ eqb p2 1 ∧ eq_block (pblock ptr1) (pblock ptr2) ∧
               eq_bv_suffix 8 8 8 (offv (poff ptr1)) (offv (poff ptr2))
            then
              return ptr2
            else Error … [MSG CorruptedPointer]
          | _ ⇒ Error … [MSG CorruptedPointer]
          ]
        | _ ⇒ Error … [MSG CorruptedPointer]
        ]
      ]
    ]
  ].

definition pc_of_bevals: list beval → res program_counter ≝
 λl.
 match l with
  [ nil ⇒ Error … [MSG CorruptedPointer]
  | cons bv1 tl ⇒
    match tl with
    [ nil ⇒ Error … [MSG CorruptedPointer]
    | cons bv2 tl' ⇒
      match tl' with
      [ cons _ _ ⇒ Error … [MSG CorruptedPointer]
      | nil ⇒
        match bv1 with
        [ BVpc ptr1 p1 ⇒
          match bv2 with
          [ BVpc ptr2 p2 ⇒
            if eqb p1 0 ∧ eqb p2 1 ∧ eq_program_counter ptr1 ptr2 then
              return ptr2
            else Error … [MSG CorruptedPointer]
          | _ ⇒ Error … [MSG CorruptedPointer]
          ]
        | _ ⇒ Error … [MSG CorruptedPointer]
        ]
      ]
    ]
  ].

definition bevals_of_pointer ≝
 λp:pointer.
 map ?? (λn_sig.BVptr p (part_from_sig n_sig)) (range_strong size_pointer).

definition bevals_of_pc ≝
 λp:program_counter.
 map ?? (λn_sig.BVpc p (part_from_sig n_sig)) (range_strong size_pointer).

lemma pointer_of_bevals_bevals_of_pointer:
 ∀p. pointer_of_bevals (bevals_of_pointer p) = OK … p.
#ptr
whd in match (bevals_of_pointer ?);
whd in ⊢ (??%?);
>eq_block_b_b
change with (eq_bv ???) in match (eq_bv_suffix ?????);
>eq_bv_refl %
qed.

lemma pc_of_bevals_bevals_of_pc:
 ∀p. pc_of_bevals (bevals_of_pc p) = OK … p.
#ptr
whd in match (bevals_of_pc ?);
whd in ⊢ (??%?);
>reflexive_eq_program_counter
%
qed.

(* CSC: move elsewhere *)
(* CSC: Wrong data-type? Use products of products *)
definition list_to_pair: ∀A:Type[0]. ∀l:list A. length … l = 2 → A × A.
 #A #l cases l [2: #a #tl cases tl [2: #b #tl' cases tl' [1: #_ @〈a,b〉 | #c #tl'']]]
 #abs normalize in abs; destruct
qed.

axiom NotATwoBytesPointer: String.

(* Should fail if the address is not representable as a pair
   As we only have 16 bit addresses atm, it never fails *)
definition beval_pair_of_pointer: pointer → (* res *) (beval × beval) ≝
 λp.list_to_pair … (bevals_of_pointer p) (refl …).
(*
 λp. match p with [ mk_pointer pty pbl pok poff ⇒
  match pty with
   [ XData ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer XData pbl pok poff)) ?)
   | Code ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer Code pbl pok poff)) ?)
   | _ ⇒ λ_. Error … [MSG NotATwoBytesPointer]] pok].*)

definition beval_pair_of_pc: program_counter → beval × beval ≝
 λp. list_to_pair ? (bevals_of_pc p) (refl …).

(* axiom NotACodePointer: String.
definition code_pointer_of_beval_pair: beval × beval → res (Σp:pointer. ptype p = Code) ≝
 λp.
  let 〈v1,v2〉 ≝ p in
  do p ← pointer_of_bevals [v1;v2] ;
  match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = Code) with
  [ Code ⇒ λE.OK ? (mk_Sig … p E)
  | _ ⇒ λ_.Error … [MSG NotACodePointer]] (refl …). *)

axiom ValueNotABoolean: String.

definition bool_of_beval: beval → res bool ≝
 λv.match v with
  [ BVundef ⇒ Error … [MSG ValueNotABoolean]
  | BVXor _ _ _ ⇒ Error … [MSG ValueNotABoolean] (* even if in some cases we can
                                                   tell the value, we will always
                                                   call bool_of_beval after a
                                                   series of XORs has been
                                                   completed *)
  | BVpc _ _ ⇒ Error … [MSG ValueNotABoolean] (* we should never test on a pc *)
  | BVByte b ⇒ OK … (eq_bv … (zero …) b)
  | BVnull _ ⇒  OK … false
  | _ ⇒ OK ? true
  ].

definition Byte_of_val: String → beval → res Byte ≝ (*CSC: move elsewhere *)
 λerr,b.match b with
  [ BVByte b ⇒ OK … b
  | _ ⇒ Error … [MSG err]].

axiom NotAnInt32Val: String.
definition Word_of_list_beval: list beval → res int ≝
 λl.
  let first_byte ≝ λl.
   match l with
    [ nil ⇒ Error ? [MSG NotAnInt32Val]
    | cons hd tl ⇒ do b ← Byte_of_val NotAnInt32Val hd ; OK ? 〈b,tl〉 ] in
  do 〈b1,l〉 ← first_byte l ;
  do 〈b2,l〉 ← first_byte l ;
  do 〈b3,l〉 ← first_byte l ;
  do 〈b4,l〉 ← first_byte l ;
   match l with
    [ nil ⇒ OK ? (b4 @@ b3 @@ b2 @@ b1)
    | _ ⇒ Error ? [MSG NotAnInt32Val] ].

inductive bebit : Type[0] ≝
| BBbit : bool → bebit
| BBundef : bebit
| BBptrcarry :
  (* is add *) bool → pointer → ∀p : part.BitVector (8*S p) → bebit.

definition Bit_of_val: String → bebit → res Bit ≝ (*CSC: move elsewhere *)
 λerr,b.match b with
  [ BBbit b ⇒ OK … b
  | _ ⇒ Error … [MSG err]].