(* Operations common to the Cminor and RTLabs front end stages. *)

(* Adapted from CompCert's Cminor.ma: *)

(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the GNU General Public License as published by  *)
(*  the Free Software Foundation, either version 2 of the License, or  *)
(*  (at your option) any later version.  This file is also distributed *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

include "common/Values.ma".

inductive constant : Type[0] ≝
  | Ointconst: int → constant     (**r integer constant *)
  | Ofloatconst: float → constant (**r floating-point constant *)
  | Oaddrsymbol: ident → int → constant (**r address of the symbol plus the offset *)
  | Oaddrstack: int → constant.   (**r stack pointer plus the given offset *)

inductive unary_operation : Type[0] ≝
  | Ocast8unsigned: unary_operation        (**r 8-bit zero extension  *)
  | Ocast8signed: unary_operation          (**r 8-bit sign extension  *)
  | Ocast16unsigned: unary_operation       (**r 16-bit zero extension  *)
  | Ocast16signed: unary_operation         (**r 16-bit sign extension *)
  | Onegint: unary_operation               (**r integer opposite *)
  | Onotbool: unary_operation              (**r boolean negation  *)
  | Onotint: unary_operation               (**r bitwise complement  *)
  | Onegf: unary_operation                 (**r float opposite *)
  | Oabsf: unary_operation                 (**r float absolute value *)
  | Osingleoffloat: unary_operation        (**r float truncation *)
  | Ointoffloat: unary_operation           (**r signed integer to float *)
  | Ointuoffloat: unary_operation          (**r unsigned integer to float *)
  | Ofloatofint: unary_operation           (**r float to signed integer *)
  | Ofloatofintu: unary_operation          (**r float to unsigned integer *)
  | Oid: unary_operation                   (**r identity (used to move between registers *)
  | Optrofint: region → unary_operation    (**r int to pointer with given representation *)
  | Ointofptr: unary_operation.            (**r pointer to int *)

inductive binary_operation : Type[0] ≝
  | Oadd: binary_operation                 (**r integer addition *)
  | Osub: binary_operation                 (**r integer subtraction *)
  | Omul: binary_operation                 (**r integer multiplication *)
  | Odiv: binary_operation                 (**r integer signed division *)
  | Odivu: binary_operation                (**r integer unsigned division *)
  | Omod: binary_operation                 (**r integer signed modulus *)
  | Omodu: binary_operation                (**r integer unsigned modulus *)
  | Oand: binary_operation                 (**r bitwise ``and'' *)
  | Oor: binary_operation                  (**r bitwise ``or'' *)
  | Oxor: binary_operation                 (**r bitwise ``xor'' *)
  | Oshl: binary_operation                 (**r left shift *)
  | Oshr: binary_operation                 (**r right signed shift *)
  | Oshru: binary_operation                (**r right unsigned shift *)
  | Oaddf: binary_operation                (**r float addition *)
  | Osubf: binary_operation                (**r float subtraction *)
  | Omulf: binary_operation                (**r float multiplication *)
  | Odivf: binary_operation                (**r float division *)
  | Ocmp: comparison -> binary_operation   (**r integer signed comparison *)
  | Ocmpu: comparison -> binary_operation  (**r integer unsigned comparison *)
  | Ocmpf: comparison -> binary_operation  (**r float comparison *)
  | Oaddp: binary_operation                (**r add an integer to a pointer *)
  | Osubpi: binary_operation               (**r subtract int from a pointers *)
  | Osubpp: binary_operation               (**r subtract two pointers *)
  | Ocmpp: comparison → binary_operation.  (**r compare pointers *)


(* * Evaluation of constants and operator applications.
    [None] is returned when the computation is undefined, e.g.
    if arguments are of the wrong types, or in case of an integer division
    by zero. *)

definition eval_constant : (ident → option block) → block → constant → option val ≝
λfind_symbol,sp,cst.
  match cst with
  [ Ointconst n ⇒ Some ? (Vint n)
  | Ofloatconst n ⇒ Some ? (Vfloat n)
  | Oaddrsymbol s ofs ⇒
      match find_symbol s with
      [ None ⇒ None ?
      | Some b ⇒ Some ? (Vptr Any b (match b with [ mk_block r id ⇒ universal_compat r id ]) (shift_offset zero_offset ofs))
      ]
  | Oaddrstack ofs ⇒
      Some ? (Vptr Any sp ? (shift_offset zero_offset ofs))
  ]. cases sp // qed.

definition eval_unop : unary_operation → val → option val ≝
λop,arg.
  match op with
  [ Ocast8unsigned ⇒ Some ? (zero_ext 8 arg)
  | Ocast8signed ⇒ Some ? (sign_ext 8 arg)
  | Ocast16unsigned ⇒ Some ? (zero_ext 16 arg)
  | Ocast16signed ⇒ Some ? (sign_ext 16 arg)
  | Onegint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vint (neg n1)) | _ ⇒ None ? ]
  | Onotbool ⇒ match arg with [ Vint n1 ⇒ Some ? (of_bool (eq n1 zero))
                              | Vptr _ _ _ _ ⇒ Some ? Vfalse
                              | Vnull _ ⇒ Some ? Vtrue
                              | _ ⇒ None ?
                              ]
  | Onotint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vint (not n1)) | _ ⇒ None ? ]
  | Onegf ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fneg f1)) | _ ⇒ None ? ]
  | Oabsf ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fabs f1)) | _ ⇒ None ? ]
  | Osingleoffloat ⇒ Some ? (singleoffloat arg)
  | Ointoffloat ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint (intoffloat f1)) | _ ⇒ None ? ]
  | Ointuoffloat ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint (intuoffloat f1)) | _ ⇒ None ? ]
  | Ofloatofint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofint n1)) | _ ⇒ None ? ]
  | Ofloatofintu ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofintu n1)) | _ ⇒ None ? ]
  | Oid ⇒ Some ? arg (* XXX should we restricted the values allowed? *)
  (* Only conversion of null pointers is specified. *)
  | Optrofint r ⇒ match arg with [ Vint n1 ⇒ if eq n1 zero then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
  | Ointofptr ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint zero) | _ ⇒ None ? ]
  ].

(* I think this is duplicated somewhere else *)
definition eval_compare_mismatch : comparison → option val ≝
λc. match c with [ Ceq ⇒ Some ? Vfalse | Cne ⇒ Some ? Vtrue | _ ⇒ None ? ].

(* Individual operations, adapted from Values. *)

definition ev_neg : val → option val ≝ λv.
  match v with
  [ Vint n ⇒ Some ? (Vint (neg n))
  | _ ⇒ None ?
  ].

definition ev_negf : val → option val ≝ λv.
  match v with
  [ Vfloat f ⇒ Some ? (Vfloat (Fneg f))
  | _ ⇒ None ?
  ].

definition ev_absf : val → option val ≝ λv.
  match v with
  [ Vfloat f ⇒ Some ? (Vfloat (Fabs f))
  | _ ⇒ None ?
  ].

definition ev_intoffloat : val → option val ≝ λv.
  match v with
  [ Vfloat f ⇒ Some ? (Vint (intoffloat f))
  | _ ⇒ None ?
  ].

definition ev_intuoffloat : val → option val ≝ λv.
  match v with
  [ Vfloat f ⇒ Some ? (Vint (intuoffloat f))
  | _ ⇒ None ?
  ].

definition ev_floatofint : val → option val ≝ λv.
  match v with
  [ Vint n ⇒ Some ? (Vfloat (floatofint n))
  | _ ⇒ None ?
  ].

definition ev_floatofintu : val → option val ≝ λv.
  match v with
  [ Vint n ⇒ Some ? (Vfloat (floatofintu n))
  | _ ⇒ None ?
  ].

definition ev_notint : val → option val ≝ λv.
  match v with
  [ Vint n ⇒ Some ? (Vint (xor n mone))
  | _ ⇒ None ?
  ].
  
definition ev_notbool : val → option val ≝ λv.
  match v with
  [ Vint n ⇒ Some ? (of_bool (int_eq n zero))
  | Vptr _ b _ ofs ⇒ Some ? Vfalse
  | Vnull _ ⇒ Some ? Vtrue
  | _ ⇒ None ?
  ].

definition ev_zero_ext ≝ λnbits: nat. λv: val.
  match v with
  [ Vint n ⇒ Some ? (Vint (zero_ext nbits n))
  | _ ⇒ None ?
  ].

definition ev_sign_ext ≝ λnbits:nat. λv:val.
  match v with
  [ Vint i ⇒ Some ? (Vint (sign_ext nbits i))
  | _ ⇒ None ?
  ].

definition ev_singleoffloat : val → option val ≝ λv.
  match v with
  [ Vfloat f ⇒ Some ? (Vfloat (singleoffloat f))
  | _ ⇒ None ?
  ].

definition ev_add ≝ λv1,v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with
    [ Vint n2 ⇒ Some ? (Vint (addition_n ? n1 n2))
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_sub ≝ λv1,v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with
    [ Vint n2 ⇒ Some ? (Vint (subtraction ? n1 n2))
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

(* NB: requires arguments to be presented pointer first. *)
definition ev_addp ≝ λv1,v2: val.
  match v1 with
  [ Vptr r b1 p ofs1 ⇒ match v2 with
    [ Vint n2 ⇒ Some ? (Vptr r b1 p (shift_offset ofs1 n2))
    | _ ⇒ None ? ]
  | Vnull r ⇒ match v2 with
    [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ?
    | _ ⇒ None ?
    ]
  | _ ⇒ None ? ].

definition ev_subpi ≝ λv1,v2: val.
  match v1 with
  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ofs1 n2))
    | _ ⇒ None ? ]
  | Vnull r ⇒ match v2 with [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_subpp ≝ λv1,v2: val.
  match v1 with
  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    [ Vptr r2 b2 p2 ofs2 ⇒
        if eq_block b1 b2 then Some ? (Vint (sub_offset ofs1 ofs2)) else None ?
    | _ ⇒ None ? ]
  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint zero) | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_mul ≝ λv1, v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with
    [ Vint n2 ⇒ Some ? (Vint (mul n1 n2))
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_divs ≝ λv1, v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with
    [ Vint n2 ⇒ option_map ?? Vint (division_s ? n1 n2)
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_mods ≝ λv1, v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with
    [ Vint n2 ⇒ option_map ?? Vint (modulus_s ? n1 n2)
    | _ ⇒ None ?
    ]
  | _ ⇒ None ?
  ].

definition ev_divu ≝ λv1, v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with 
    [ Vint n2 ⇒ option_map ?? Vint (division_u ? n1 n2)
    | _ ⇒ None ?
    ]
  | _ ⇒ None ?
  ].

definition ev_modu ≝ λv1, v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with 
    [ Vint n2 ⇒ option_map ?? Vint (modulus_u ? n1 n2)
    | _ ⇒ None ?
    ]
  | _ ⇒ None ?
  ].

definition ev_and ≝ λv1, v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with
    [ Vint n2 ⇒ Some ? (Vint (i_and n1 n2))
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_or ≝ λv1, v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with
    [ Vint n2 ⇒ Some ? (Vint (or n1 n2))
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_xor ≝ λv1, v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with
    [ Vint n2 ⇒ Some ? (Vint (xor n1 n2))
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_shl ≝ λv1, v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with 
    [ Vint n2 ⇒
       if ltu n2 iwordsize
       then Some ? (Vint (shl n1 n2))
       else None ?
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_shr ≝ λv1, v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with 
    [ Vint n2 ⇒
       if ltu n2 iwordsize
       then Some ? (Vint (shr n1 n2))
       else None ?
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_shr_carry ≝ λv1, v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with 
    [ Vint n2 ⇒
       if ltu n2 iwordsize
       then Some ? (Vint (shr_carry n1 n2))
       else None ?
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_shrx ≝ λv1, v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with 
    [ Vint n2 ⇒
       if ltu n2 iwordsize
       then Some ? (Vint (shrx n1 n2))
       else None ?
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_shru ≝ λv1, v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with 
    [ Vint n2 ⇒
       if ltu n2 iwordsize
       then Some ? (Vint (shru n1 n2))
       else None ?
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_rolm ≝
λv: val. λamount, mask: int.
  match v with
  [ Vint n ⇒ Some ? (Vint (rolm n amount mask))
  | _ ⇒ None ?
  ].

definition ev_ror ≝ λv1, v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with 
    [ Vint n2 ⇒
       if ltu n2 iwordsize
       then Some ? (Vint (ror n1 n2))
       else None ?
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_addf ≝ λv1,v2: val.
  match v1 with
  [ Vfloat f1 ⇒ match v2 with
    [ Vfloat f2 ⇒ Some ? (Vfloat (Fadd f1 f2))
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_subf ≝ λv1,v2: val.
  match v1 with
  [ Vfloat f1 ⇒ match v2 with
    [ Vfloat f2 ⇒ Some ? (Vfloat (Fsub f1 f2))
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_mulf ≝ λv1,v2: val.
  match v1 with
  [ Vfloat f1 ⇒ match v2 with
    [ Vfloat f2 ⇒ Some ? (Vfloat (Fmul f1 f2))
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_divf ≝ λv1,v2: val.
  match v1 with
  [ Vfloat f1 ⇒ match v2 with
    [ Vfloat f2 ⇒ Some ? (Vfloat (Fdiv f1 f2))
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_cmp_match : comparison → option val ≝ λc.
  match c with
  [ Ceq ⇒ Some ? Vtrue
  | Cne ⇒ Some ? Vfalse
  | _   ⇒ None ?
  ].

definition ev_cmp_mismatch : comparison → option val ≝ λc.
  match c with
  [ Ceq ⇒ Some ? Vfalse
  | Cne ⇒ Some ? Vtrue
  | _   ⇒ None ?
  ].

definition ev_cmp ≝ λc: comparison. λv1,v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with
    [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2))
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_cmpp ≝ λc: comparison. λv1,v2: val.
  match v1 with
  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    [ Vptr r2 b2 p2 ofs2 ⇒
        if eq_block b1 b2
        then Some ? (of_bool (cmp_offset c ofs1 ofs2))
        else ev_cmp_mismatch c
    | Vnull r2 ⇒ ev_cmp_mismatch c
    | _ ⇒ None ? ]
  | Vnull r1 ⇒ match v2 with
    [ Vptr _ _ _ _ ⇒ ev_cmp_mismatch c
    | Vnull r2 ⇒ ev_cmp_match c
    | _ ⇒ None ?
    ]
  | _ ⇒ None ? ].

(* TODO: check this, it isn't the cmpu used elsewhere *)
definition ev_cmpu ≝ λc: comparison. λv1,v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with
    [ Vint n2 ⇒ Some ? (of_bool (cmpu c n1 n2))
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_cmpf ≝ λc: comparison. λv1,v2: val.
  match v1 with
  [ Vfloat f1 ⇒ match v2 with
    [ Vfloat f2 ⇒ Some ? (of_bool (Fcmp c f1 f2))
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition eval_binop : binary_operation → val → val → option val ≝
λop.
  match op with
  [ Oadd ⇒ ev_add
  | Osub ⇒ ev_sub
  | Omul ⇒ ev_mul
  | Odiv ⇒ ev_divs
  | Odivu ⇒ ev_divu
  | Omod ⇒ ev_mods
  | Omodu ⇒ ev_modu
  | Oand ⇒ ev_and
  | Oor ⇒ ev_or
  | Oxor ⇒ ev_xor
  | Oshl ⇒ ev_shl
  | Oshr ⇒ ev_shr
  | Oshru ⇒ ev_shru
  | Oaddf ⇒ ev_addf
  | Osubf ⇒ ev_subf
  | Omulf ⇒ ev_mulf
  | Odivf ⇒ ev_divf
  | Ocmp c ⇒ ev_cmp c
  | Ocmpu c ⇒ ev_cmpu c
  | Ocmpf c ⇒ ev_cmpf c
  | Oaddp ⇒ ev_addp
  | Osubpi ⇒ ev_subpi
  | Osubpp ⇒ ev_subpp
  | Ocmpp c ⇒ ev_cmpp c
  ].